CVC3

theory_arith_old.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file theory_arith_old.h
00004  *
00005  * Author: Clark Barrett
00006  *
00007  * Created: Thu Jun 14 13:22:11 2007
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  *
00016  * <hr>
00017  *
00018  */
00019 /*****************************************************************************/
00020 
00021 #ifndef _cvc3__include__theory_arith_old_h_
00022 #define _cvc3__include__theory_arith_old_h_
00023 
00024 #include "theory_arith.h"
00025 #include <set>
00026 #include <list>
00027 
00028 namespace CVC3 {
00029 
00030 class TheoryArithOld :public TheoryArith {
00031   CDList<Theorem> d_diseq;  // For concrete model generation
00032   CDO<size_t> d_diseqIdx; // Index to the next unprocessed disequality
00033   CDMap<Expr, bool> diseqSplitAlready; // Have we eplit on this disequality already
00034   ArithProofRules* d_rules;
00035   CDO<bool> d_inModelCreation;
00036 
00037   //! Data class for the strongest free constant in separation inqualities
00038   class FreeConst {
00039   private:
00040     Rational d_r;
00041     bool d_strict;
00042   public:
00043     FreeConst() { }
00044     FreeConst(const Rational& r, bool strict): d_r(r), d_strict(strict) { }
00045     const Rational& getConst() const { return d_r; }
00046     bool strict() const { return d_strict; }
00047   };
00048   //! Printing
00049   friend std::ostream& operator<<(std::ostream& os, const FreeConst& fc);
00050 
00051   //! Private class for an inequality in the Fourier-Motzkin database
00052   class Ineq {
00053   private:
00054     Theorem d_ineq; //!< The inequality
00055     bool d_rhs; //!< Var is isolated on the RHS
00056     const FreeConst* d_const; //!< The max/min const for subsumption check
00057     //! Default constructor is disabled
00058     Ineq() { }
00059   public:
00060     //! Initial constructor.  'r' is taken from the subsumption database.
00061     Ineq(const Theorem& ineq, bool varOnRHS, const FreeConst& c):
00062       d_ineq(ineq), d_rhs(varOnRHS), d_const(&c) { }
00063     //! Get the inequality
00064     const Theorem ineq() const { return d_ineq; }
00065     //! Get the max/min constant
00066     const FreeConst& getConst() const { return *d_const; }
00067     //! Flag whether var is isolated on the RHS
00068     bool varOnRHS() const { return d_rhs; }
00069     //! Flag whether var is isolated on the LHS
00070     bool varOnLHS() const { return !d_rhs; }
00071     //! Auto-cast to Theorem
00072     operator Theorem() const { return d_ineq; }
00073   };
00074   //! Printing
00075   friend std::ostream& operator<<(std::ostream& os, const Ineq& ineq);
00076 
00077   //! Database of inequalities with a variable isolated on the right
00078   ExprMap<CDList<Ineq> *> d_inequalitiesRightDB;
00079 
00080   //! Database of inequalities with a variable isolated on the left
00081   ExprMap<CDList<Ineq> *> d_inequalitiesLeftDB;
00082 
00083   //! Mapping of inequalities to the largest/smallest free constant
00084   /*! The Expr is the original inequality with the free constant
00085    * removed and inequality converted to non-strict (for indexing
00086    * purposes).  I.e. ax<c+t becomes ax<=t.  This inequality is mapped
00087    * to a pair<c,strict>, the smallest (largest for c+t<ax) constant
00088    * among inequalities with the same 'a', 'x', and 't', and a boolean
00089    * flag indicating whether the strongest inequality is strict.
00090    */
00091   CDMap<Expr, FreeConst> d_freeConstDB;
00092 
00093 //  /** Is the problem only difference logic */
00094 //  CDO<bool> isDL;
00095 //  CDO<int> total_buf_size;
00096 //  CDO<int> processed;
00097 //
00098   // Input buffer to store the incoming inequalities
00099   CDList<Theorem> d_buffer_0; //!< Buffer of input inequalities (high priority)
00100   CDList<Theorem> d_buffer_1; //!< Buffer of input inequalities (one variable)
00101   CDList<Theorem> d_buffer_2; //!< Buffer of input inequalities (small constraints)
00102   CDList<Theorem> d_buffer_3; //!< Buffer of input inequalities (big constraint)
00103 
00104   CDO<size_t> d_bufferIdx_0; //!< Buffer index of the next unprocessed inequality
00105   CDO<size_t> d_bufferIdx_1; //!< Buffer index of the next unprocessed inequality
00106   CDO<size_t> d_bufferIdx_2; //!< Buffer index of the next unprocessed inequality
00107   CDO<size_t> d_bufferIdx_3; //!< Buffer index of the next unprocessed inequality
00108 
00109   CDO<size_t> diff_logic_size; //!< Number of queries that are just difference logic
00110 
00111   const int* d_bufferThres; //!< Threshold when the buffer must be processed
00112 
00113   const bool* d_splitSign; // Whether to split on the signs of non-trivial nonlinear products
00114 
00115   const int* d_grayShadowThres; //!< Threshold on gray shadow size (ignore it and set incomplete)
00116 
00117   // Statistics for the variables
00118 
00119   /*! @brief Mapping of a variable to the number of inequalities where
00120     the variable would be isolated on the right */
00121   CDMap<Expr, int> d_countRight;
00122 
00123   /*! @brief Mapping of a variable to the number of inequalities where
00124     the variable would be isolated on the left */
00125   CDMap<Expr, int> d_countLeft;
00126 
00127   //! Set of shared terms (for counterexample generation)
00128   CDMap<Expr, bool> d_sharedTerms;
00129   CDList<Expr> d_sharedTermsList;
00130 
00131   //! Set of shared integer variables (i-leaves)
00132   CDMap<Expr, bool> d_sharedVars;
00133 
00134   //Directed Acyclic Graph representing partial variable ordering for
00135   //variable projection over inequalities.
00136   class VarOrderGraph {
00137     ExprMap<std::vector<Expr> > d_edges;
00138     ExprMap<bool> d_cache;
00139     bool dfs(const Expr& e1, const Expr& e2);
00140     void dfs(const Expr& e1, std::vector<Expr>& output_list);
00141   public:
00142     void addEdge(const Expr& e1, const Expr& e2);
00143     //returns true if e1 < e2, false otherwise.
00144     bool lessThan(const Expr& e1, const Expr& e2);
00145     //selects those variables which are largest and incomparable among
00146     //v1 and puts it into v2
00147     void selectLargest(const std::vector<Expr>& v1, std::vector<Expr>& v2);
00148     //selects those variables which are smallest and incomparable among
00149     //v1, removes them from v1 and  puts them into v2.
00150     void selectSmallest( std::vector<Expr>& v1, std::vector<Expr>& v2);
00151     //returns the list of vertices in the topological order
00152     void getVerticesTopological(std::vector<Expr>& output_list);
00153   };
00154 
00155   VarOrderGraph d_graph;
00156 
00157   // Private methods
00158 
00159   //! Check the term t for integrality.
00160   /*! \return a theorem of IS_INTEGER(t) or Null. */
00161   Theorem isIntegerThm(const Expr& e);
00162 
00163   //! A helper method for isIntegerThm()
00164   /*! Check if IS_INTEGER(e) is easily derivable from the given 'thm' */
00165   Theorem isIntegerDerive(const Expr& isIntE, const Theorem& thm);
00166 
00167   //! Extract the free constant from an inequality
00168   const Rational& freeConstIneq(const Expr& ineq, bool varOnRHS);
00169 
00170   //! Update the free constant subsumption database with new inequality
00171   /*! \return a reference to the max/min constant.
00172    *
00173    * Also, sets 'subsumed' argument to true if the inequality is
00174    * subsumed by an existing inequality.
00175    */
00176   const FreeConst& updateSubsumptionDB(const Expr& ineq, bool varOnRHS,
00177               bool& subsumed);
00178   //! Check if the kids of e are fully simplified and canonized (for debugging)
00179   bool kidsCanonical(const Expr& e);
00180 
00181   //! Canonize the expression e, assuming,  all children are canonical
00182   Theorem canon(const Expr& e);
00183 
00184   /*! @brief Canonize and reduce e w.r.t. union-find database; assume
00185    * all children are canonical */
00186   Theorem canonSimplify(const Expr& e);
00187 
00188   /*! @brief Composition of canonSimplify(const Expr&) by
00189    * transitivity: take e0 = e1, canonize and simplify e1 to e2,
00190    * return e0 = e2. */
00191   Theorem canonSimplify(const Theorem& thm) {
00192     return transitivityRule(thm, canonSimplify(thm.getRHS()));
00193   }
00194 
00195   //! Canonize predicate (x = y, x < y, etc.)
00196   Theorem canonPred(const Theorem& thm);
00197 
00198   //! Canonize predicate like canonPred except that the input theorem
00199   //! is an equivalent transformation.
00200   Theorem canonPredEquiv(const Theorem& thm);
00201 
00202   //! Solve an equation and return an equivalent Theorem in the solved form
00203   Theorem doSolve(const Theorem& e);
00204 
00205   //! takes in a conjunction equivalence Thm and canonizes it.
00206   Theorem canonConjunctionEquiv(const Theorem& thm);
00207 
00208   //! picks the monomial with the smallest abs(coeff) from the input
00209   //integer equation.
00210   bool pickIntEqMonomial(const Expr& right, Expr& isolated, bool& nonlin);
00211 
00212   //! processes equalities with 1 or more vars of type REAL
00213   Theorem processRealEq(const Theorem& eqn);
00214 
00215   //! processes equalities whose vars are all of type INT
00216   Theorem processIntEq(const Theorem& eqn);
00217 
00218   //! One step of INT equality processing (aux. method for processIntEq())
00219   Theorem processSimpleIntEq(const Theorem& eqn);
00220 
00221   //! Process inequalities in the buffer
00222   void processBuffer();
00223 
00224   //! Take an inequality and isolate a variable
00225   Theorem isolateVariable(const Theorem& inputThm, bool& e1);
00226 
00227   //! Update the statistics counters for the variable with a coeff. c
00228   void updateStats(const Rational& c, const Expr& var);
00229 
00230   //! Update the statistics counters for the monomial
00231   void updateStats(const Expr& monomial);
00232 
00233   //! Add an inequality to the input buffer.  See also d_buffer
00234   bool addToBuffer(const Theorem& thm, bool priority = false);
00235 
00236   /*! @brief Given a canonized term, compute a factor to make all
00237     coefficients integer and relatively prime */
00238   Expr computeNormalFactor(const Expr& rhs, bool normalizeConstants);
00239 
00240   //! Normalize an equation (make all coefficients rel. prime integers)
00241   Theorem normalize(const Expr& e);
00242 
00243   //! Normalize an equation (make all coefficients rel. prime integers)
00244   /*! accepts a rewrite theorem over eqn|ineqn and normalizes it
00245    *  and returns a theorem to that effect.
00246    */
00247   Theorem normalize(const Theorem& thm);
00248 
00249   Expr pickMonomial(const Expr& right);
00250 
00251   void getFactors(const Expr& e, std::set<Expr>& factors);
00252 
00253  public: // ArithTheoremProducer needs these functions, so make them public
00254   //! Separate monomial e = c*p1*...*pn into c and 1*p1*...*pn
00255   void separateMonomial(const Expr& e, Expr& c, Expr& var);
00256 
00257   //! Check the term t for integrality (return bool)
00258   bool isInteger(const Expr& e)
00259   { return
00260       isInt(e.getType()) ? true :
00261       (isReal(e.getType()) ? false : !(isIntegerThm(e).isNull())); }
00262 
00263  private:
00264 
00265   bool lessThanVar(const Expr& isolatedVar, const Expr& var2);
00266 
00267   //! Check if the term expression is "stale"
00268   bool isStale(const Expr& e);
00269 
00270   //! Check if the inequality is "stale" or subsumed
00271   bool isStale(const Ineq& ineq);
00272 
00273   void projectInequalities(const Theorem& theInequality,bool isolatedVarOnRHS);
00274 
00275   void assignVariables(std::vector<Expr>&v);
00276 
00277   void findRationalBound(const Expr& varSide, const Expr& ratSide,
00278        const Expr& var,
00279        Rational &r);
00280 
00281   bool findBounds(const Expr& e, Rational& lub, Rational&  glb);
00282 
00283   Theorem normalizeProjectIneqs(const Theorem& ineqThm1,
00284         const Theorem& ineqThm2);
00285 
00286   //! Take a system of equations and turn it into a solved form
00287   Theorem solvedForm(const std::vector<Theorem>& solvedEqs);
00288 
00289   /*! @brief Substitute all vars in term 't' according to the
00290    * substitution 'subst' and canonize the result.
00291    */
00292   Theorem substAndCanonize(const Expr& t, ExprMap<Theorem>& subst);
00293 
00294   /*! @brief Substitute all vars in the RHS of the equation 'eq' of
00295    * the form (x = t) according to the substitution 'subst', and
00296    * canonize the result.
00297    */
00298   Theorem substAndCanonize(const Theorem& eq, ExprMap<Theorem>& subst);
00299 
00300   //! Traverse 'e' and push all the i-leaves into 'vars' vector
00301   void collectVars(const Expr& e, std::vector<Expr>& vars,
00302        std::set<Expr>& cache);
00303 
00304   /*! @brief Check if alpha <= ax & bx <= beta is a finite interval
00305    *  for integer var 'x', and assert the corresponding constraint
00306    */
00307   void processFiniteInterval(const Theorem& alphaLEax,
00308            const Theorem& bxLEbeta);
00309 
00310   //! For an integer var 'x', find and process all constraints A <= ax <= A+c
00311   void processFiniteIntervals(const Expr& x);
00312 
00313   //! Recursive setup for isolated inequalities (and other new expressions)
00314   void setupRec(const Expr& e);
00315 
00316 public:
00317   TheoryArithOld(TheoryCore* core);
00318   ~TheoryArithOld();
00319 
00320   // Trusted method that creates the proof rules class (used in constructor).
00321   // Implemented in arith_theorem_producer.cpp
00322   ArithProofRules* createProofRulesOld();
00323 
00324   // Theory interface
00325   void addSharedTerm(const Expr& e);
00326   void assertFact(const Theorem& e);
00327   void refineCounterExample();
00328   void computeModelBasic(const std::vector<Expr>& v);
00329   void computeModel(const Expr& e, std::vector<Expr>& vars);
00330   void checkSat(bool fullEffort);
00331   Theorem rewrite(const Expr& e);
00332   void setup(const Expr& e);
00333   void update(const Theorem& e, const Expr& d);
00334   Theorem solve(const Theorem& e);
00335   void checkAssertEqInvariant(const Theorem& e);
00336   void checkType(const Expr& e);
00337   Cardinality finiteTypeInfo(Expr& e, Unsigned& n,
00338                              bool enumerate, bool computeSize);
00339   void computeType(const Expr& e);
00340   Type computeBaseType(const Type& t);
00341   void computeModelTerm(const Expr& e, std::vector<Expr>& v);
00342   Expr computeTypePred(const Type& t, const Expr& e);
00343   Expr computeTCC(const Expr& e);
00344   ExprStream& print(ExprStream& os, const Expr& e);
00345   Expr parseExprOp(const Expr& e);
00346 
00347 private:
00348 
00349   /** Map from variables to the maximal (by absolute value) of one of it's coefficients */
00350   ExprMap<Rational> maxCoefficientLeft;
00351   ExprMap<Rational> maxCoefficientRight;
00352 
00353   /** Map from variables to the fixed value of one of it's coefficients */
00354   ExprMap<Rational> fixedMaxCoefficient;
00355 
00356   /**
00357    * Returns the current maximal coefficient of the variable.
00358    *
00359    * @param var the variable.
00360    */
00361   Rational currentMaxCoefficient(Expr var);
00362 
00363   /**
00364    * Fixes the current max coefficient to be used in the ordering. If the maximal coefficient
00365    * changes in the future, it will not be used in the ordering.
00366    *
00367    * @param variable the variable
00368    * @param max the value to set it to
00369    */
00370   void fixCurrentMaxCoefficient(Expr variable, Rational max);
00371 
00372   /**
00373    * Among given input variables, select the smallest ones with respect to the coefficients.
00374    */
00375   void selectSmallestByCoefficient(const std::vector<Expr>& input, std::vector<Expr>& output);
00376 
00377   /**
00378    * Given an inequality theorem check if it is on integers and get rid of the non-integer
00379    * constants.
00380    */
00381   Theorem rafineInequalityToInteger(const Theorem& thm);
00382 
00383   /**
00384    * Given an equality theorem check if it is on integers with a non-integer constant. If
00385    * yes, return a theorem 0 = 1
00386    */
00387   Theorem checkIntegerEquality(const Theorem& thm);
00388 
00389   /** Keep the expressions that are already in the buffer */
00390   CDMap<Expr, Theorem> bufferedInequalities;
00391 
00392   /** Strict lower bounds on terms, so that we don't add inequalities to the buffer */
00393   CDMap<Expr, Rational> termLowerBound;
00394   CDMap<Expr, Theorem> termLowerBoundThm;
00395   /** Strict upper bounds on terms, so that we don't add inequalities to the buffer */
00396   CDMap<Expr, Rational> termUpperBound;
00397   CDMap<Expr, Theorem> termUpperBoundThm;
00398 
00399   /**
00400    * Which inequalities have already been projected (on which monomial).
00401    *  - if we get an update of an inequality that's not been projected, we don't care
00402    *    it will get projected (it's find)
00403    *  - when projecting, project the finds, not the originals
00404    *  - when done projecting add here, both original and the find
00405    */
00406   CDMap<Expr, Expr> alreadyProjected;
00407 
00408   /**
00409    * Sometimes we know an inequality is in the buffer (as a find of something) and
00410    * we don't want it in the buffer, but we do want to pre-process it, so we put it
00411    * here.
00412    */
00413   CDMap<Expr, bool> dontBuffer;
00414 
00415   /**
00416    * Are we doing only difference logic?
00417    */
00418   CDO<bool> diffLogicOnly;
00419 
00420   /**
00421    * Takes an inequality theorem and substitutes the rhs for it's find. It also get's normalized.
00422    */
00423   Theorem inequalityToFind(const Theorem& inequalityThm, bool normalizeRHS);
00424 
00425   // x -y <= c
00426   struct GraphEdge {
00427     Expr x;
00428     Expr y;
00429     Rational c;
00430   };
00431 
00432   /**
00433    * Take inequality of the form 0 op t and extract the c1, t1, c2 and t2, such that
00434    * c1 <= t1 and t2 <= c2, where c1 and c2 are constants, and t1 and t2 are either
00435    * sums of monomials or a monomial.
00436    *
00437    * @return the number of variables in terms t1 and t2
00438    */
00439   int extractTermsFromInequality(const Expr& inequality,
00440       Rational& c1, Expr& t1,
00441       Rational& c2, Expr& t2);
00442 
00443   void registerAtom(const Expr& e);
00444 
00445   typedef ExprMap< std::set< std::pair<Rational, Expr> > > AtomsMap;
00446 
00447   /** Map from terms to their lower bound (and the original formula expression) */
00448   AtomsMap formulaAtomLowerBound;
00449 
00450   /** Map from terms to their upper bound (and the original formula expression) */
00451   AtomsMap formulaAtomUpperBound;
00452 
00453   /** Map of all the atoms in the formula */
00454   ExprMap<bool> formulaAtoms;
00455 
00456   class DifferenceLogicGraph {
00457 
00458     public:
00459 
00460       /**
00461          * EpsRational class ecapsulates the rationals with a symbolic small \f$\epsilon\f$ added. Each rational
00462          * number is presented as a pair \f$(q, k) = q + k\epsilon\f$, where \f$\epsilon\f$ is treated symbolically.
00463          * The operations on the new rationals are defined as
00464          * <ul>
00465          *  <li>\f$(q_1, k_1) + (q_2, k_2) \equiv (q_1 + q_2, k_1 + k_2)\f$
00466          *  <li>\f$a \times (q, k) \equiv (a \times q, a \times k)\f$
00467          *  <li>\f$(q_1, k_1) \leq (q_2, k_2) \equiv (q_1 < q_2) \vee (q_1 = q_2 \wedge k_1 \leq k_2)\f$
00468          * </ul>
00469          *
00470          * Note that the operations on the infinite values are not defined, as they are never used currently. Infinities can
00471          * only be asigned or compared.
00472          */
00473         class EpsRational {
00474 
00475           protected:
00476 
00477             /** Type of rationals, normal and the two infinities */
00478             typedef enum { FINITE, PLUS_INFINITY, MINUS_INFINITY } RationalType;
00479 
00480             /** The type of this rational */
00481             RationalType type;
00482 
00483             /** The rational part */
00484             Rational q;
00485 
00486             /** The epsilon multiplier */
00487             Rational k;
00488 
00489             /**
00490              * Private constructor to construt infinities.
00491              */
00492             EpsRational(RationalType type) : type(type) {}
00493 
00494           public:
00495 
00496             /**
00497              * Returns if the numbe is finite.
00498              */
00499             inline bool isFinite() const { return type == FINITE; }
00500 
00501             /**
00502              * Returns if the number is a plain rational.
00503              *
00504              * @return true if rational, false otherwise
00505              */
00506             inline bool isRational() const { return k == 0; }
00507 
00508             /**
00509              * Returns if the number is a plain integer.
00510              *
00511              * @return true if rational, false otherwise
00512              */
00513             inline bool isInteger() const { return k == 0 && q.isInteger(); }
00514 
00515             /**
00516              * Returns the floor of the number \f$x = q + k \epsilon\f$ using the following fomula
00517              * \f[
00518              * \lfloor \beta(x) \rfloor =
00519              * \begin{cases}
00520              * \lfloor q \rfloor & \text{ if } q \notin Z\\
00521              * q & \text{ if } q \in Z \text{ and } k \geq 0\\
00522              * q - 1 & \text{ if } q \in Z \text{ and } k < 0
00523              * \end{cases}
00524              * \f]
00525              */
00526             inline Rational getFloor() const {
00527               if (q.isInteger()) {
00528                 if (k >= 0) return q;
00529                 else return q - 1;
00530               } else
00531                 // If not an integer, just floor it
00532                 return floor(q);
00533             }
00534 
00535 
00536           /**
00537            * Returns the rational part of the number
00538            *
00539            * @return the rational
00540            */
00541           inline Rational getRational() const { return q; }
00542 
00543           /**
00544            * Returns the epsilon part of the number
00545            *
00546            * @return the epsilon
00547            */
00548           inline Rational getEpsilon() const { return k; }
00549 
00550           /** The infinity constant */
00551           static const EpsRational PlusInfinity;
00552           /** The negative infinity constant */
00553           static const EpsRational MinusInfinity;
00554           /** The zero constant */
00555           static const EpsRational Zero;
00556 
00557 
00558           /** The blank constructor */
00559           EpsRational() : type(FINITE), q(0), k(0) {}
00560 
00561           /** Copy constructor */
00562           EpsRational(const EpsRational& r) : type(r.type), q(r.q), k(r.k) {}
00563 
00564             /**
00565              * Constructor from a rational, constructs a new pair (q, 0).
00566              *
00567              * @param q the rational
00568              */
00569           EpsRational(const Rational& q) : type(FINITE), q(q), k(0) {}
00570 
00571             /**
00572              * Constructor from a rational and a given epsilon multiplier, constructs a
00573              * new pair (q, k).
00574              *
00575              * @param q the rational
00576              * @param k the epsilon multiplier
00577              */
00578           EpsRational(const Rational& q, const Rational& k) : type(FINITE), q(q), k(k) {}
00579 
00580             /**
00581              * Addition operator for two EpsRational numbers.
00582              *
00583              * @param r the number to be added
00584              * @return the sum as defined in the class
00585              */
00586             inline EpsRational operator + (const EpsRational& r) const {
00587               DebugAssert(type == FINITE, "EpsRational::operator +, adding to infinite number");
00588               DebugAssert(r.type == FINITE, "EpsRational::operator +, adding an infinite number");
00589               return EpsRational(q + r.q, k + r.k);
00590             }
00591 
00592             /**
00593              * Addition operator for two EpsRational numbers.
00594              *
00595              * @param r the number to be added
00596              * @return the sum as defined in the class
00597              */
00598             inline EpsRational& operator += (const EpsRational& r) {
00599               DebugAssert(type == FINITE, "EpsRational::operator +, adding to infinite number");
00600               q = q + r.q;
00601               k = k + r.k;
00602               return *this;
00603             }
00604 
00605             /**
00606              * Subtraction operator for two EpsRational numbers.
00607              *
00608              * @param r the number to be added
00609              * @return the sum as defined in the class
00610              */
00611             inline EpsRational operator - (const EpsRational& r) const {
00612             DebugAssert(type == FINITE, "EpsRational::operator -, subtracting from infinite number");
00613               DebugAssert(r.type == FINITE, "EpsRational::operator -, subtracting an infinite number");
00614               return EpsRational(q - r.q, k - r.k);
00615             }
00616 
00617             /**
00618              * Unary minus operator
00619              */
00620             inline EpsRational operator - () {
00621             DebugAssert(type == FINITE, "EpsRational::operator -, subtracting from infinite number");
00622               q = -q;
00623               k = -k;
00624             return *this;
00625             }
00626 
00627 
00628             /**
00629              * Multiplication operator EpsRational number and a rational number.
00630              *
00631              * @param a the number to be multiplied
00632              * @return the product as defined in the class
00633              */
00634             inline EpsRational operator * (const Rational& a) const {
00635             DebugAssert(type == FINITE, "EpsRational::operator *, multiplying an infinite number");
00636               return EpsRational(a * q, a * k);
00637             }
00638 
00639             /**
00640              * Division operator EpsRational number and a rational number.
00641              *
00642              * @param a the number to be multiplied
00643              * @return the product as defined in the class
00644              */
00645             inline EpsRational operator / (const Rational& a) const {
00646             DebugAssert(type == FINITE, "EpsRational::operator *, dividing an infinite number");
00647               return EpsRational(q / a, k / a);
00648             }
00649 
00650             /**
00651              * Equality comparison operator.
00652              */
00653             inline bool operator == (const EpsRational& r) const { return (q == r.q && k == r.k); }
00654 
00655             /**
00656              * Less than or equal comparison operator.
00657              */
00658             inline bool operator <= (const EpsRational& r) const {
00659               switch (r.type) {
00660                 case FINITE:
00661                   if (type == FINITE)
00662                     // Normal comparison
00663                     return (q < r.q || (q == r.q && k <= r.k));
00664                   else
00665                     // Finite number is bigger only of the negative infinity
00666                     return type == MINUS_INFINITY;
00667                 case PLUS_INFINITY:
00668                   // Everything is less then or equal than +inf
00669                   return true;
00670                 case MINUS_INFINITY:
00671                   // Only -inf is less then or equal than -inf
00672                   return (type == MINUS_INFINITY);
00673                 default:
00674                   // Ohohohohohoooooo, whats up
00675                   FatalAssert(false, "EpsRational::operator <=, what kind of number is this????");
00676               }
00677               return false;
00678             }
00679 
00680             /**
00681              * Less than comparison operator.
00682              */
00683             inline bool operator < (const EpsRational& r) const { return !(r <= *this); }
00684 
00685             /**
00686              * Greater than comparison operator.
00687              */
00688             inline bool operator > (const EpsRational& r) const { return !(*this <= r); }
00689 
00690             /**
00691              * Returns the string representation of the number.
00692              *
00693              * @return the string representation of the number
00694              */
00695             std::string toString() const {
00696               switch (type) {
00697                 case FINITE:
00698                   return "(" + q.toString() + ", " + k.toString() + ")";
00699                 case PLUS_INFINITY:
00700                   return "+inf";
00701                 case MINUS_INFINITY:
00702                   return "-inf";
00703                 default:
00704                   FatalAssert(false, "EpsRational::toString, what kind of number is this????");
00705               }
00706               return "hm, what am I?";
00707             }
00708         };
00709 
00710       struct EdgeInfo {
00711         /** The length of this edge */
00712         EpsRational length;
00713         /** The number of edges in this path */
00714         int path_length_in_edges;
00715         /** If this is a summary edge, a vertex in the path */
00716         Expr in_path_vertex;
00717         /** If this is an original edge, the theorem that explains it */
00718         Theorem explanation;
00719 
00720         /** Returnes if the edge is well define (i.e. not +infinity) */
00721         bool isDefined() const { return path_length_in_edges != 0; }
00722 
00723         EdgeInfo(): path_length_in_edges(0) {}
00724       };
00725 
00726       /**
00727        * Given two vertices in the graph and an path edge, reconstruct all the theorems and put them
00728        * in the output vector
00729        */
00730       void getEdgeTheorems(const Expr& x, const Expr& y, const EdgeInfo& edgeInfo, std::vector<Theorem>& outputTheorems);
00731 
00732       /**
00733        * Returns the current weight of the edge.
00734        */
00735       EpsRational getEdgeWeight(const Expr& x, const Expr& y);
00736 
00737       /**
00738        * Returns whether a vertex has incoming edges.
00739        */
00740       bool hasIncoming(const Expr& x);
00741 
00742       /**
00743        * Returns whether a vertex has outgoing edges.
00744        */
00745       bool hasOutgoing(const Expr& x);
00746 
00747     protected:
00748 
00749       /** Threshold on path length to process (ignore bigger than and set incomplete) */
00750       const int* d_pathLenghtThres;
00751 
00752       /** The arithmetic that's using this graph */
00753       TheoryArithOld* arith;
00754 
00755       /** The core theory */
00756       TheoryCore* core;
00757 
00758       /** The arithmetic that is using u us */
00759       ArithProofRules* rules;
00760 
00761       /** The unsat theorem if available */
00762       CDO<Theorem> unsat_theorem;
00763 
00764       /** The biggest epsilon from EpsRational we used in paths */
00765       CDO<Rational> biggestEpsilon;
00766 
00767       /** The smallest rational difference we used in path relaxation */
00768       CDO<Rational> smallestPathDifference;
00769 
00770       /** The graph itself, maps expressions (x-y) to the edge information */
00771       typedef CDMap<Expr, EdgeInfo> Graph;
00772 
00773       /** Graph of <= paths */
00774       Graph leGraph;
00775 
00776       typedef ExprMap<CDList<Expr>*> EdgesList;
00777 
00778       /** List of vertices adjacent backwards to a vertex */
00779       EdgesList incomingEdges;
00780       /** List of vertices adjacent forward to a vertex */
00781       EdgesList outgoingEdges;
00782 
00783       /**
00784        * Returns the edge (path) info for the given kind
00785        *
00786        * @param x the starting vertex
00787        * @param y the ending vertex
00788        * @return the edge information
00789        */
00790       Graph::ElementReference getEdge(const Expr& x, const Expr& y);
00791 
00792       /**
00793        * Try to update the shortest path from x to z using y.
00794        */
00795       bool tryUpdate(const Expr& x, const Expr& y, const Expr& z);
00796 
00797     public:
00798 
00799       void writeGraph(std::ostream& out);
00800 
00801       /**
00802        * Fills the vector with all the variables (vertices) in the graph
00803        */
00804       void getVariables(std::vector<Expr>& variables);
00805 
00806       void setRules(ArithProofRules* rules) {
00807         this->rules = rules;
00808       }
00809 
00810       void setArith(TheoryArithOld* arith) {
00811         this->arith = arith;
00812       }
00813 
00814       /**
00815        * Class constructor.
00816        */
00817       DifferenceLogicGraph(TheoryArithOld* arith, TheoryCore* core, ArithProofRules* rules, Context* context);
00818 
00819       /**
00820        * Destructor
00821        */
00822       ~DifferenceLogicGraph();
00823 
00824       /**
00825        * Returns the reference to the unsat theorem if there is a negative
00826        * cycle in the graph.
00827        *
00828        * @return the unsat theorem
00829        */
00830 
00831       Theorem getUnsatTheorem();
00832 
00833       /**
00834        * Returns true if there is a negative cycle in the graph.
00835        */
00836       bool isUnsat();
00837 
00838       void computeModel();
00839 
00840       Rational getValuation(const Expr& x);
00841 
00842 
00843       /**
00844        * Adds an edge corresponding to the constraint x - y <= c.
00845        *
00846        * @param x variable x::Difference
00847        * @param y variable y
00848        * @param c rational c
00849        * @param edge_thm the theorem for this edge
00850        */
00851       void addEdge(const Expr& x, const Expr& y, const Rational& c, const Theorem& edge_thm);
00852 
00853       /**
00854        * Check if there is an edge from x to y
00855        */
00856       bool existsEdge(const Expr& x, const Expr& y);
00857 
00858       /**
00859        * Check if x is in a cycle
00860        */
00861       bool inCycle(const Expr& x);
00862 
00863       /**
00864        * Given a shared integer term expand it into the gray shadow on the bounds (if bounded from both sides).
00865        */
00866       void expandSharedTerm(const Expr& x);
00867 
00868     protected:
00869 
00870       /** Whether the variable is in a cycle */
00871       CDMap<Expr, bool> varInCycle;
00872 
00873       Expr sourceVertex;
00874 
00875       /**
00876        * Produced the unsat theorem from a cycle x --> x of negative length
00877        *
00878        * @param x the variable to use for the conflict
00879        * @param kind the kind of edges to consider
00880        */
00881       void analyseConflict(const Expr& x, int kind);
00882   };
00883 
00884   /** The graph for difference logic */
00885   DifferenceLogicGraph diffLogicGraph;
00886 
00887   Expr zero;
00888 
00889   /** Index for expanding on shared term equalities */
00890   CDO<unsigned> shared_index_1;
00891   /** Index for expanding on shared term equalities */
00892   CDO<unsigned> shared_index_2;
00893 
00894   std::vector<Theorem> multiplicativeSignSplits;
00895 
00896   int termDegree(const Expr& e);
00897 
00898   bool canPickEqMonomial(const Expr& right);
00899 
00900 private:
00901 
00902   // Keeps all expressions that are bounded for disequality splitting and shared term comparisons
00903   CDMap<Expr, DifferenceLogicGraph::EpsRational> termUpperBounded;
00904   CDMap<Expr, DifferenceLogicGraph::EpsRational> termLowerBounded;
00905 
00906   // Keeps all expressions that are constrained
00907   CDMap<Expr, bool> termConstrainedBelow;
00908   CDMap<Expr, bool> termConstrainedAbove;
00909 
00910   enum BoundsQueryType {
00911     /** Query the bounds/constrained using cache for leaves */
00912     QueryWithCacheLeaves,
00913     /** Query the bounds/constrained using cashe for leaves, but also see if the value is constrained */
00914     QueryWithCacheLeavesAndConstrainedComputation,
00915     /** Query the bounds/constrained by only querying the cache, don't try to figure it out */
00916     QueryWithCacheAll
00917   };
00918 
00919   /**
00920    * Check if the term is bounded. If the term is non-linear, just returns false.
00921    */
00922   bool isBounded(const Expr& t, BoundsQueryType queryType = QueryWithCacheLeaves);
00923   bool hasLowerBound(const Expr& t, BoundsQueryType queryType = QueryWithCacheLeaves) { return getLowerBound(t, queryType).isFinite(); }
00924   bool hasUpperBound(const Expr& t, BoundsQueryType queryType = QueryWithCacheLeaves) { return getUpperBound(t, queryType).isFinite(); }
00925 
00926   bool isConstrained(const Expr& t, bool intOnly = true, BoundsQueryType queryType = QueryWithCacheLeaves);
00927   bool isConstrainedAbove(const Expr& t, BoundsQueryType queryType = QueryWithCacheLeaves);
00928   bool isConstrainedBelow(const Expr& t, BoundsQueryType queryType = QueryWithCacheLeaves);
00929 
00930   /**
00931    * Check if the term is bounded from above. If the term is non-linear, just returns false.
00932    */
00933   DifferenceLogicGraph::EpsRational getUpperBound(const Expr& t, BoundsQueryType queryType = QueryWithCacheLeaves);
00934 
00935   /**
00936    * Check if the term is bouned from below. If the term is non-linear, just return false.
00937    */
00938   DifferenceLogicGraph::EpsRational getLowerBound(const Expr& t, BoundsQueryType queryType = QueryWithCacheLeaves);
00939 
00940   /**
00941    * See whether and which terms are bounded.
00942    */
00943   int computeTermBounds();
00944 
00945 public:
00946 
00947   void tryPropagate(const Expr& x, const Expr& y, const DifferenceLogicGraph::EdgeInfo& x_y_edge, int kind);
00948 
00949   void addMultiplicativeSignSplit(const Theorem& case_split_thm);
00950 
00951   bool addPairToArithOrder(const Expr& smaller, const Expr& bigger);
00952 
00953   bool nonlinearSignSplit() const { return *d_splitSign; }
00954 
00955   /**
00956    * Check if equation is nonlinear. An equation is nonlinear if there is at least one nonlinear term in the sum
00957    * on either side of the equation.
00958    */
00959   bool isNonlinearEq(const Expr& e);
00960 
00961   /**
00962    * Check if a sum term is nonlinear
00963    */
00964   bool isNonlinearSumTerm(const Expr& term);
00965 
00966   /**
00967    * Check if the equality is of the form c + power1^n - power2^n = 0;
00968    */
00969   bool isPowersEquality(const Expr& nonlinearEq, Expr& power1, Expr& power2);
00970 
00971   /**
00972    * Check if the equality is of the form c - x^n = 0
00973    */
00974   bool isPowerEquality(const Expr& nonlinearEq, Rational& constant, Expr& power1);
00975 
00976 };
00977 
00978 }
00979 
00980 #endif