theory_arith_new.mine.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file theory_arith_new.h
00004  * 
00005  * Author: Dejan Jovanovic
00006  *
00007  * Created: Thu Jun 14 13:38:16 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_new_h_
00022 #define _cvc3__include__theory_arith_new_h_
00023 
00024 #include "theory_arith.h"
00025 
00026 #include <hash_fun.h>
00027 #include <hash_map.h>
00028 #include <queryresult.h>
00029 #include <map>
00030 
00031 namespace CVC3 {
00032 
00033 
00034 /**
00035  * This theory handles basic linear arithmetic.
00036  *
00037  * @author Clark Barrett
00038  * 
00039  * @since Sat Feb  8 14:44:32 2003
00040  */
00041 class TheoryArithNew :public TheoryArith {
00042     
00043   /** For concrete model generation */
00044   CDList<Theorem> d_diseq;
00045   /** Index to the next unprocessed disequality */   
00046   CDO<size_t> d_diseqIdx; 
00047   ArithProofRules* d_rules;
00048   CDO<bool> d_inModelCreation;
00049 
00050   /** Data class for the strongest free constant in separation inqualities **/
00051   class FreeConst {
00052   private:
00053     Rational d_r;
00054     bool d_strict;
00055   public:
00056     FreeConst() { }
00057     FreeConst(const Rational& r, bool strict): d_r(r), d_strict(strict) { }
00058     const Rational& getConst() const { return d_r; }
00059     bool strict() const { return d_strict; }
00060   };
00061   //! Printing
00062   friend std::ostream& operator<<(std::ostream& os, const FreeConst& fc);
00063   //! Private class for an inequality in the Fourier-Motzkin database
00064   class Ineq {
00065   private:
00066     Theorem d_ineq; //!< The inequality
00067     bool d_rhs; //!< Var is isolated on the RHS
00068     const FreeConst* d_const; //!< The max/min const for subsumption check
00069     //! Default constructor is disabled
00070     Ineq() { }
00071   public:
00072     //! Initial constructor.  'r' is taken from the subsumption database.
00073     Ineq(const Theorem& ineq, bool varOnRHS, const FreeConst& c):
00074       d_ineq(ineq), d_rhs(varOnRHS), d_const(&c) { }
00075     //! Get the inequality
00076     const Theorem& ineq() const { return d_ineq; }
00077     //! Get the max/min constant
00078     const FreeConst& getConst() const { return *d_const; }
00079     //! Flag whether var is isolated on the RHS
00080     bool varOnRHS() const { return d_rhs; }
00081     //! Flag whether var is isolated on the LHS
00082     bool varOnLHS() const { return !d_rhs; }
00083     //! Auto-cast to Theorem
00084     operator Theorem() const { return d_ineq; }
00085   };
00086   //! Printing
00087   friend std::ostream& operator<<(std::ostream& os, const Ineq& ineq);
00088   //! Database of inequalities with a variable isolated on the right
00089   ExprMap<CDList<Ineq> *> d_inequalitiesRightDB;
00090   //! Database of inequalities with a variable isolated on the left
00091   ExprMap<CDList<Ineq> *> d_inequalitiesLeftDB;
00092   //! Mapping of inequalities to the largest/smallest free constant
00093   /*! The Expr is the original inequality with the free constant
00094    * removed and inequality converted to non-strict (for indexing
00095    * purposes).  I.e. ax<c+t becomes ax<=t.  This inequality is mapped
00096    * to a pair<c,strict>, the smallest (largest for c+t<ax) constant
00097    * among inequalities with the same 'a', 'x', and 't', and a boolean
00098    * flag indicating whether the strongest inequality is strict.
00099    */
00100   CDMap<Expr, FreeConst> d_freeConstDB;
00101   // Input buffer to store the incoming inequalities
00102   CDList<Theorem> d_buffer; //!< Buffer of input inequalities
00103   CDO<size_t> d_bufferIdx; //!< Buffer index of the next unprocessed inequality
00104   const int* d_bufferThres; //!< Threshold when the buffer must be processed
00105   // Statistics for the variables
00106   /*! @brief Mapping of a variable to the number of inequalities where
00107     the variable would be isolated on the right */
00108   CDMap<Expr, int> d_countRight;
00109   /*! @brief Mapping of a variable to the number of inequalities where
00110     the variable would be isolated on the left */
00111   CDMap<Expr, int> d_countLeft;
00112   //! Set of shared terms
00113   CDMap<Expr, Expr> d_sharedTerms;
00114   //! Backtracking database of subterms of shared terms
00115   CDList<Expr> d_sharedTermsList;
00116   //! Used in checkSat
00117   CDO<unsigned> d_index1;
00118   //! Set of shared integer variables (i-leaves)
00119   CDMap<Expr, bool> d_sharedVars;
00120   //Directed Acyclic Graph representing partial variable ordering for
00121   //variable projection over inequalities.
00122   class VarOrderGraph {
00123     ExprMap<std::vector<Expr> > d_edges;
00124     ExprMap<bool> d_cache;
00125     bool dfs(const Expr& e1, const Expr& e2);
00126   public:
00127     void addEdge(const Expr& e1, const Expr& e2);
00128     //returns true if e1 < e2, false otherwise.
00129     bool lessThan(const Expr& e1, const Expr& e2);
00130     //selects those variables which are largest and incomparable among
00131     //v1 and puts it into v2
00132     void selectLargest(const std::vector<Expr>& v1, std::vector<Expr>& v2);
00133     //selects those variables which are smallest and incomparable among
00134     //v1, removes them from v1 and  puts them into v2. 
00135     void selectSmallest( std::vector<Expr>& v1, std::vector<Expr>& v2);
00136 
00137   };
00138   
00139   VarOrderGraph d_graph;
00140 
00141   // Private methods
00142   //! Check the term t for integrality.  
00143   /*! \return a theorem of IS_INTEGER(t) or Null. */
00144   Theorem isIntegerThm(const Expr& e);
00145   //! A helper method for isIntegerThm()
00146   /*! Check if IS_INTEGER(e) is easily derivable from the given 'thm' */
00147   Theorem isIntegerDerive(const Expr& isIntE, const Theorem& thm);
00148   //! Check the term t for integrality (return bool)
00149   bool isInteger(const Expr& e) { return !(isIntegerThm(e).isNull()); }
00150   //! Check if the kids of e are fully simplified and canonized (for debugging)
00151   bool kidsCanonical(const Expr& e);
00152   
00153   //! Canonize the expression e, assuming all children are canonical
00154   Theorem canon(const Expr& e);
00155   /*! @brief Canonize and reduce e w.r.t. union-find database; assume
00156    * all children are canonical */
00157   Theorem canonSimplify(const Expr& e);
00158   /*! @brief Composition of canonSimplify(const Expr&) by
00159    * transitivity: take e0 = e1, canonize and simplify e1 to e2,
00160    * return e0 = e2. */
00161   Theorem canonSimplify(const Theorem& thm) {
00162     return transitivityRule(thm, canonSimplify(thm.getRHS()));
00163   }
00164   //! Canonize predicate (x = y, x < y, etc.)
00165   Theorem canonPred(const Theorem& thm);
00166   //! Canonize predicate like canonPred except that the input theorem
00167   //! is an equivalent transformation.
00168   Theorem canonPredEquiv(const Theorem& thm);
00169   //! Solve an equation and return an equivalent Theorem in the solved form
00170   Theorem doSolve(const Theorem& e);
00171   //! takes in a conjunction equivalence Thm and canonizes it.
00172   Theorem canonConjunctionEquiv(const Theorem& thm);
00173   //! picks the monomial with the smallest abs(coeff) from the input
00174   //integer equation.
00175   Expr pickIntEqMonomial(const Expr& right);
00176   //! processes equalities with 1 or more vars of type REAL
00177   Theorem processRealEq(const Theorem& eqn);
00178   //! processes equalities whose vars are all of type INT
00179   Theorem processIntEq(const Theorem& eqn);
00180   //! One step of INT equality processing (aux. method for processIntEq())
00181   Theorem processSimpleIntEq(const Theorem& eqn);
00182   //! Take an inequality and isolate a variable
00183   Theorem isolateVariable(const Theorem& inputThm, bool& e1);
00184   //! Update the statistics counters for the variable with a coeff. c
00185   void updateStats(const Rational& c, const Expr& var);
00186   //! Update the statistics counters for the monomial
00187   void updateStats(const Expr& monomial);
00188   //! Add an inequality to the input buffer.  See also d_buffer
00189   void addToBuffer(const Theorem& thm);
00190   Expr pickMonomial(const Expr& right);
00191  public: // ArithTheoremProducer needs this function, so make it public
00192   //! Separate monomial e = c*p1*...*pn into c and 1*p1*...*pn
00193   void separateMonomial(const Expr& e, Expr& c, Expr& var);
00194  private:
00195   bool lessThanVar(const Expr& isolatedVar, const Expr& var2);
00196   //! Check if the term expression is "stale"
00197   bool isStale(const Expr& e);
00198   //! Check if the inequality is "stale" or subsumed
00199   bool isStale(const Ineq& ineq);
00200   void projectInequalities(const Theorem& theInequality,bool isolatedVarOnRHS);
00201   void assignVariables(std::vector<Expr>&v);
00202   void findRationalBound(const Expr& varSide, const Expr& ratSide, 
00203        const Expr& var,
00204        Rational &r);
00205   bool findBounds(const Expr& e, Rational& lub, Rational&  glb);
00206 
00207   Theorem normalizeProjectIneqs(const Theorem& ineqThm1,
00208         const Theorem& ineqThm2);
00209   //! Take a system of equations and turn it into a solved form
00210   Theorem solvedForm(const std::vector<Theorem>& solvedEqs);
00211   /*! @brief Substitute all vars in term 't' according to the
00212    * substitution 'subst' and canonize the result.
00213    */
00214   Theorem substAndCanonize(const Expr& t, ExprMap<Theorem>& subst);
00215   /*! @brief Substitute all vars in the RHS of the equation 'eq' of
00216    * the form (x = t) according to the substitution 'subst', and
00217    * canonize the result.
00218    */
00219   Theorem substAndCanonize(const Theorem& eq, ExprMap<Theorem>& subst);
00220   //! Traverse 'e' and push all the i-leaves into 'vars' vector
00221   void collectVars(const Expr& e, std::vector<Expr>& vars,
00222        std::set<Expr>& cache);
00223   /*! @brief Check if alpha <= ax & bx <= beta is a finite interval
00224    *  for integer var 'x', and assert the corresponding constraint
00225    */
00226   void processFiniteInterval(const Theorem& alphaLEax,
00227            const Theorem& bxLEbeta);
00228   //! For an integer var 'x', find and process all constraints A <= ax <= A+c 
00229   void processFiniteIntervals(const Expr& x);
00230   //! Recursive setup for isolated inequalities (and other new expressions)
00231   void setupRec(const Expr& e);
00232 
00233 public:
00234   TheoryArithNew(TheoryCore* core);
00235   ~TheoryArithNew();
00236 
00237   // Trusted method that creates the proof rules class (used in constructor).
00238   // Implemented in arith_theorem_producer.cpp
00239   ArithProofRules* createProofRules();
00240 
00241   // Theory interface
00242   void addSharedTerm(const Expr& e);
00243   void assertFact(const Theorem& e);
00244   void refineCounterExample();
00245   void computeModelBasic(const std::vector<Expr>& v);
00246   void computeModel(const Expr& e, std::vector<Expr>& vars);
00247   void checkSat(bool fullEffort);
00248   Theorem rewrite(const Expr& e);
00249   void setup(const Expr& e);
00250   void update(const Theorem& e, const Expr& d);
00251   Theorem solve(const Theorem& e);
00252   void checkAssertEqInvariant(const Theorem& e);
00253   void checkType(const Expr& e);
00254   void computeType(const Expr& e);
00255   Type computeBaseType(const Type& t);
00256   void computeModelTerm(const Expr& e, std::vector<Expr>& v);
00257   Expr computeTypePred(const Type& t, const Expr& e);
00258   Expr computeTCC(const Expr& e);
00259   ExprStream& print(ExprStream& os, const Expr& e);
00260   virtual Expr parseExprOp(const Expr& e);
00261 
00262   // DDDDDDDDDDDDDDDDDDDDDDDDEEEEEEEEEEEEEEEEEEEEEEEJJJJJJJJJJJJJJJJJJJJJAAAAAAAAAAAAAAAAAAAAAAANNNNNNNNNNNNNNNNNNNNNNN
00263   
00264     public: 
00265     
00266       /**
00267        * EpsRational class ecapsulates the rationals with a symbolic small \f$\epsilon\f$ added. Each rational
00268        * number is presented as a pair \f$(q, k) = q + k\epsilon\f$, where \f$\epsilon\f$ is treated symbolically.
00269        * The operations on the new rationals are defined as
00270        * <ul>
00271        *  <li>\f$(q_1, k_1) + (q_2, k_2) \equiv (q_1 + q_2, k_1 + k_2)\f$
00272        *  <li>\f$a \times (q, k) \equiv (a \times q, a \times k)\f$
00273        *  <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$
00274        * </ul>
00275        * 
00276        * Note that the operations on the infinite values are not defined, as they are never used currently. Infinities can
00277        * only be asigned or compared. 
00278        */
00279       class EpsRational {
00280         
00281         protected:
00282         
00283           /** Type of rationals, normal and the two infinities */
00284           typedef enum { FINITE, PLUS_INFINITY, MINUS_INFINITY } RationalType;
00285           
00286           /** The type of this rational */
00287           RationalType type;      
00288 
00289           /** The rational part */
00290           Rational q; 
00291           
00292           /** The epsilon multiplier */
00293           Rational k;       
00294         
00295           /**
00296            * Private constructor to construt infinities.
00297            */
00298           EpsRational(RationalType type) : type(type) {}
00299         
00300         public:
00301         
00302           /**
00303            * Returns if the number is a plain rational.
00304            * 
00305            * @return true if rational, false otherwise
00306            */
00307           inline bool isRational() const { return k == 0; }
00308           
00309           /**
00310            * Returns if the number is a plain integer.
00311            * 
00312            * @return true if rational, false otherwise
00313            */
00314           inline bool isInteger() const { return k == 0 && q.isInteger(); }
00315           
00316           /** 
00317            * Returns the floor of the number \f$x = q + k \epsilon\f$ using the following fomula
00318            * \f[
00319            * \lfloor \beta(x) \rfloor =
00320            * \begin{cases}
00321            * \lfloor q \rfloor & \text{ if } q \notin Z\\
00322            * q & \text{ if } q \in Z \text{ and } k \geq 0\\
00323            * q - 1 & \text{ if } q \in Z \text{ and } k < 0
00324            * \end{cases}
00325            * \f]
00326            */
00327           inline Rational getFloor() const { 
00328             if (q.isInteger()) {
00329               if (k >= 0) return q;
00330               else return q - 1;
00331             } else 
00332               // If not an integer, just floor it
00333               return floor(q);
00334           } 
00335           
00336 
00337         /** 
00338          * Returns the rational part of the number
00339          * 
00340          * @return the rational 
00341          */
00342         inline Rational getRational() const { return q; }
00343 
00344         /** The infinity constant */
00345         static const EpsRational PlusInfinity;
00346         /** The negative infinity constant */
00347         static const EpsRational MinusInfinity;
00348         /** The zero constant */
00349         static const EpsRational Zero;
00350         
00351 
00352         /** The blank constructor */
00353         EpsRational() : type(FINITE), q(0), k(0) {}
00354 
00355         /** Copy constructor */
00356         EpsRational(const EpsRational& r) : type(r.type), q(r.q), k(r.k) {} 
00357         
00358           /**
00359            * Constructor from a rational, constructs a new pair (q, 0).
00360            * 
00361            * @param q the rational
00362            */
00363         EpsRational(const Rational q) : type(FINITE), q(q), k(0) {} 
00364       
00365           /**
00366            * Constructor from a rational and a given epsilon multiplier, constructs a 
00367            * new pair (q, k).
00368            * 
00369            * @param q the rational
00370            * @param k the epsilon multiplier
00371            */
00372         EpsRational(const Rational q, const Rational k) : type(FINITE), q(q), k(k) {} 
00373       
00374           /**
00375            * Addition operator for two EpsRational numbers.
00376            * 
00377            * @param r the number to be added
00378            * @return the sum as defined in the class 
00379            */
00380           inline EpsRational operator + (const EpsRational& r) const {
00381             DebugAssert(type == FINITE, "EpsRational::operator +, adding to infinite number");
00382             DebugAssert(r.type == FINITE, "EpsRational::operator +, adding an infinite number");
00383             return EpsRational(q + r.q, k + r.k);
00384           }
00385           
00386           /**
00387            * Addition operator for two EpsRational numbers.
00388            * 
00389            * @param r the number to be added
00390            * @return the sum as defined in the class 
00391            */
00392           inline EpsRational& operator += (const EpsRational& r) {
00393             DebugAssert(type == FINITE, "EpsRational::operator +, adding to infinite number");
00394             q = q + r.q;
00395             k = k + r.k;
00396             return *this;
00397           }
00398           
00399           /**
00400            * Subtraction operator for two EpsRational numbers.
00401            * 
00402            * @param r the number to be added
00403            * @return the sum as defined in the class 
00404            */
00405           inline EpsRational operator - (const EpsRational& r) const {
00406           DebugAssert(type == FINITE, "EpsRational::operator -, subtracting from infinite number");
00407             DebugAssert(r.type == FINITE, "EpsRational::operator -, subtracting an infinite number");
00408             return EpsRational(q - r.q, k - r.k);
00409           }
00410           
00411           /**
00412            * Multiplication operator EpsRational number and a rational number.
00413            * 
00414            * @param a the number to be multiplied
00415            * @return the product as defined in the class 
00416            */
00417           inline EpsRational operator * (const Rational& a) const {
00418           DebugAssert(type == FINITE, "EpsRational::operator *, multiplying an infinite number");
00419             return EpsRational(a * q, a * k);
00420           }
00421           
00422           /**
00423            * Division operator EpsRational number and a rational number.
00424            * 
00425            * @param a the number to be multiplied
00426            * @return the product as defined in the class 
00427            */
00428           inline EpsRational operator / (const Rational& a) const {
00429           DebugAssert(type == FINITE, "EpsRational::operator *, dividing an infinite number");
00430             return EpsRational(q / a, k / a);
00431           }
00432           
00433           /**
00434            * Equality comparison operator.
00435            */
00436           inline bool operator == (const EpsRational& r) const { return (q == r.q && k == r.k); }
00437           
00438           /**
00439            * Les then or equal comparison operator.
00440            */
00441           inline bool operator <= (const EpsRational& r) const { 
00442             switch (r.type) {
00443               case FINITE:
00444                 if (type == FINITE) 
00445                   // Normal comparison
00446                   return (q < r.q || (q == r.q && k <= r.k));
00447                 else
00448                   // Finite number is bigger only of the negative infinity 
00449                   return type == MINUS_INFINITY;
00450               case PLUS_INFINITY:
00451                 // Everything is less then or equal than +inf
00452                 return true;
00453               case MINUS_INFINITY:
00454                 // Only -inf is less then or equal than -inf
00455                 return (type == MINUS_INFINITY);
00456               default:
00457                 // Ohohohohohoooooo, whats up
00458                 FatalAssert(false, "EpsRational::operator <=, what kind of number is this????");    
00459             }
00460             return false;
00461           }
00462           
00463           /**
00464            * Les then comparison operator.
00465            */
00466           inline bool operator < (const EpsRational& r) const { return !(r <= *this); }
00467           
00468           /**
00469            * Bigger then equal comparison operator.
00470            */
00471           inline bool operator > (const EpsRational& r) const { return !(*this <= r); }
00472           
00473           /**
00474            * Returns the string representation of the number.
00475            * 
00476            * @param the string representation of the number
00477            */
00478           std::string toString() const { 
00479             switch (type) {
00480               case FINITE:
00481                 return "(" + q.toString() + ", " + k.toString() + ")";
00482               case PLUS_INFINITY:
00483                 return "+inf";
00484               case MINUS_INFINITY:
00485                 return "-inf";
00486               default:
00487                 FatalAssert(false, "EpsRational::toString, what kind of number is this????");
00488             } 
00489             return "hm, what am I?";
00490           }
00491       };
00492   
00493       /**
00494        * Registers the atom given from the core. This atoms are stored so that they can be used
00495        * for theory propagation.
00496        * 
00497        * @param e the expression (atom) that is part of the input formula
00498        */ 
00499     void registerAtom(const Expr& e);
00500  
00501     private:    
00502         
00503         /** A set of all integer variables */
00504         std::set<Expr> intVariables;
00505         
00506         /**
00507          * Return a Gomory cut plane derivation of the variable $x_i$. Mixed integer
00508          * Gomory cut can be constructed if 
00509          * <ul>
00510          * <li>\f$x_i\f$ is a integer basic variable with a non-integer value
00511          * <li>all non-basic variables in the row of \f$x_i\f$ are assigned to their
00512          *     upper or lower bounds
00513          * <li>all the values on the right side of the row have rational values (non
00514          *     eps-rational values)
00515          * </ul>
00516          */ 
00517         Theorem deriveGomoryCut(const Expr& x_i);
00518         
00519         /**
00520          * Tries to rafine the integer constraint of the theorem. For example,
00521          * x < 1 is rewritten as x <= 0, and x <(=) 1.5 is rewritten as x <= 1.
00522          * The constraint should be in the normal form.
00523          * 
00524          * @param thm the derivation of the constraint 
00525          */
00526         Theorem rafineIntegerConstraints(const Theorem& thm);
00527         
00528         /** Are we consistent or not */
00529         CDO<QueryResult> consistent;
00530         
00531         /** The theorem explaining the inconsistency */
00532         Theorem explanation;
00533         
00534         /** 
00535          * The structure necessaty to hold the bounds.
00536          */
00537         struct BoundInfo {
00538           /** The bound itself */
00539           EpsRational bound;
00540           /** The assertion theoreem of the bound */
00541           Theorem theorem;
00542           
00543           /** Constructor */
00544           BoundInfo(const EpsRational& bound, const Theorem& thm): bound(bound), theorem(thm) {}
00545           
00546           /** The empty constructor for the map */
00547           BoundInfo(): bound(0), theorem() {}
00548           
00549           /** 
00550            * The comparator, just if we need it. Compares first by expressions then by bounds 
00551            */
00552           bool operator < (const BoundInfo& bI) const {
00553             // Get tje expressoins
00554             const Expr& expr1 = (theorem.isRewrite() ? theorem.getRHS() : theorem.getExpr());
00555             const Expr& expr2 = (bI.theorem.isRewrite() ? bI.theorem.getRHS() : bI.theorem.getExpr());
00556             
00557             std::cout << expr1 << " @ " << expr2 << std::endl;
00558             
00559             // Compare first by the expressions (right sides of expressions)
00560             if (expr1[1] == expr2[1])
00561               // If the same, just return the bound comparison (plus a trick to order equal bounds, different relations) 
00562               if (bound == bI.bound && expr1.getKind() != expr2.getKind())
00563                 return expr1.getKind() == LE; // LE before GE -- only case that can happen                              
00564               else
00565                 return bound < bI.bound;
00566             else
00567               // Return the expression comparison
00568               return expr1[1] < expr2[1];
00569           }
00570         };
00571 
00572 
00573         /** 
00574          * The structure necessaty to hold the bounds on expressions (for theory propagation).
00575          */
00576         struct ExprBoundInfo {
00577           /** The bound itself */
00578           EpsRational bound;
00579           /** The assertion theoreem of the bound */
00580           Expr e;
00581           
00582           /** Constructor */
00583           ExprBoundInfo(const EpsRational& bound, const Expr& e): bound(bound), e(e) {}
00584           
00585           /** The empty constructor for the map */
00586           ExprBoundInfo(): bound(0) {}
00587           
00588           /** 
00589            * The comparator, just if we need it. Compares first by expressions then by bounds 
00590            */
00591           bool operator < (const ExprBoundInfo& bI) const {
00592             
00593             // Compare first by the expressions (right sides of expressions)
00594             if (e[1] == bI.e[1])
00595               // If the same, just return the bound comparison (plus a trick to order equal bounds, different relations) 
00596               if (bound == bI.bound && e.getKind() != bI.e.getKind())
00597                 return e.getKind() == LE; // LE before GE -- only case that can happen                              
00598               else
00599                 return bound < bI.bound;
00600             else
00601               // Return the expression comparison
00602               return e[1] < bI.e[1];
00603           }
00604         };
00605         
00606         /** The map from variables to lower bounds (these must be backtrackable) */  
00607       CDMap<Expr, BoundInfo> lowerBound;
00608       /** The map from variables to upper bounds (these must be backtrackable) */ 
00609       CDMap<Expr, BoundInfo> upperBound;
00610       /** The current real valuation of the variables (these must be backtrackable for the last succesefull checkSAT!!!) */
00611       CDMap<Expr, EpsRational> beta;
00612           
00613       typedef Hash::hash_map<Expr, Theorem> TebleauxMap;
00614       //typedef google::sparse_hash_map<Expr, Theorem, Hash::hash<Expr> > TebleauxMap;
00615       //typedef std::map<Expr, Theorem> TebleauxMap;
00616       
00617       typedef std::set<Expr> SetOfVariables;
00618       typedef Hash::hash_map<Expr, SetOfVariables> DependenciesMap;
00619       
00620       /** Maps variables to sets of variables that depend on it in the tableaux */
00621       DependenciesMap dependenciesMap;  
00622           
00623         /** The tableaux, a map from basic variables to the expressions over the non-basic ones (theorems that explain them how we got there) */ 
00624       TebleauxMap tableaux;
00625 
00626     /** Additional tableaux map from expressions asserted to the corresponding theorems explaining the introduction of the new variables */
00627     TebleauxMap freshVariables;
00628     
00629     /** A set containing all the unsatisfied basic variables */
00630     std::set<Expr> unsatBasicVariables;
00631     
00632     /** The vector to keep the assignments from fresh variables to expressions they represent */  
00633     std::vector<Expr> assertedExpr;
00634     /** The backtrackable number of fresh variables asserted so far */
00635     CDO<unsigned int> assertedExprCount;
00636     
00637     /** A set of BoundInfo objects */
00638     typedef std::set<ExprBoundInfo> BoundInfoSet;
00639     
00640     /** Internal variable to see wheather to propagate or not */
00641     bool propagate;
00642     
00643     /** 
00644      * Propagate all that is possible from given assertion and its bound
00645      */
00646     void propagateTheory(const Expr& assertExpr, const EpsRational& bound, const EpsRational& oldBound);    
00647     
00648     /**
00649      * Store all the atoms from the formula in this set. It is searchable by an expression
00650      * and the bound. To get all the implied atoms, one just has to go up (down) and check if the 
00651      * atom or it's negation are implied.
00652      */
00653     BoundInfoSet allBounds;
00654     
00655     /**
00656      * Adds var to the dependencies sets of all the variables in the sum.
00657      * 
00658      * @param var the variable on the left side 
00659      * @param the sum that defines the variable
00660      */
00661     void updateDependenciesAdd(const Expr& var, const Expr& sum);
00662     
00663     /**
00664      * Remove var from the dependencies sets of all the variables in the sum.
00665      * 
00666      * @param var the variable on the left side 
00667      * @param the sum that defines the variable
00668      */
00669     void updateDependenciesRemove(const Expr& var, const Expr& sum);
00670   
00671     /**
00672      * Updates the dependencies if a right side of an expression in the tableaux is changed. For example,
00673      * if oldExpr is x + y and newExpr is y + z, var will be added to the dependency list of z, and removed
00674      * from the dependency list of x.
00675      * 
00676      * @param oldExpr the old right side of the tableaux 
00677      * @param newExpr the new right side of the tableaux
00678      * @param var the variable that is defined by these two expressions
00679      * @param var a variable to skip when going through the expressions
00680      */
00681     void updateDependencies(const Expr& oldExpr, const Expr& newExpr, const Expr& var, const Expr& skipVar);
00682     
00683     /**
00684      * Update the values of variables that have appeared in the tableaux due to backtracking.
00685      */
00686     void updateFreshVariables();
00687     
00688     /** 
00689      * Updates the value of variable var by computing the value of expression e.
00690      * 
00691      * @param var the variable to update
00692      * @param e the expression to compute
00693      */
00694     void updateValue(const Expr& var, const Expr& e);
00695     
00696     /**
00697      * Returns a string representation of the tableaux.
00698      * 
00699      * @return tableaux as string
00700      */
00701     std::string tableauxAsString() const;
00702     
00703     /**
00704      * Returns a string representation of the unsat variables.
00705      * 
00706      * @return unsat as string
00707      */
00708     std::string unsatAsString() const;
00709     
00710     /**
00711      * Returns a string representation of the current bounds.
00712      * 
00713      * @return tableaux as string
00714      */
00715     std::string boundsAsString();
00716 
00717     /**
00718      * Gets the equality of the fresh variable tableaux variable corresponding to this expression. If the expression has already been
00719      * asserted, the coresponding variable is returned, othervise a fresh variable is created and the theorem is returned.
00720      * 
00721      * @param leftSide the left side of the asserted constraint
00722      * @return the equality theorem s = leftSide
00723      */
00724     Theorem getVariableIntroThm(const Expr& leftSide);
00725 
00726     /**
00727      * Find the coefficient standing by the variable var in the expression expr. Expresion is expected to be
00728      * in canonical form, i.e either a rational constant, an arithmetic leaf (i.e. variable or term from some 
00729      * other theory), (MULT rat leaf) where rat is a non-zero rational constant, leaf is an arithmetic leaf or
00730      * (PLUS \f$const term_0 term_1 ... term_n\f$) where each \f$term_i\f$ is either a leaf or (MULT \f$rat leaf\f$) 
00731      * and each leaf in \f$term_i\f$ must be strictly greater than the leaf in \f$term_{i+1}\f$.               
00732      * 
00733      * @param var the variable
00734      * @param expr the expression to search in
00735      */     
00736       const Rational& findCoefficient(const Expr& var, const Expr& expr); 
00737     
00738       /**
00739        * Return true iof the given variable is basic in the tableaux, i.e. it is on the left side, expressed
00740        * in terms of the non-basic variables.
00741        * 
00742        * @param x the variable to be checked
00743        * @return true if the variable is basic, false if the variable is non-basic
00744        */
00745       bool isBasic(const Expr& x) const;
00746       
00747       /**
00748        * Returns the coefficient at a_ij in the current tableaux, i.e. the coefficient 
00749        * at x_j in the row of x_i.
00750        * 
00751        * @param x_i a basic variable
00752        * @param x_j a non-basic variable
00753        * @return the reational coefficient 
00754        */
00755       Rational getTableauxEntry(const Expr& x_i, const Expr& x_j); 
00756       
00757       /**
00758        * Swaps a basic variable \f$x_r\f$ and a non-basic variable \f$x_s\f$ such
00759        * that ars \f$a_{rs} \neq 0\f$. After pivoting, \f$x_s\f$ becomes basic and \f$x_r\f$ becomes non-basic. 
00760        * The tableau is updated by replacing equation \f[x_r = \sum_{x_j \in N}{a_{rj}xj}\f] with
00761        * \f[x_s = \frac{x_r}{a_{rs}} - \sum_{x_j \in N }{\frac{a_{rj}}{a_rs}x_j}\f] and this equation 
00762        * is used to eliminate \f$x_s\f$ from the rest of the tableau by substitution.
00763        * 
00764        * @param x_r a basic variable
00765        * @param x_s a non-basic variable
00766        */
00767       void pivot(const Expr& x_r, const Expr& x_s);
00768     
00769       /**
00770        * Sets the value of a non-basic variable \f$x_i\f$ to \f$v\f$ and adjusts the value of all 
00771        * the basic variables so that all equations remain satisfied.
00772        * 
00773        * @param x_i a non-basic variable
00774        * @param v the value to set the variable \f$x_i\f$ to 
00775        */
00776       void update(const Expr& x_i, const EpsRational& v);
00777       
00778       /**
00779        * Pivots the basic variable \f$x_i\f$ and the non-basic variable \f$x_j\f$. It also sets \f$x_i\f$ to \f$v\f$ and adjusts all basic 
00780        * variables to keep the equations satisfied.
00781        * 
00782        * @param x_i a basic variable
00783        * @param x_j a non-basic variable
00784        * @param v the valie to assign to x_i
00785        */ 
00786       void pivotAndUpdate(const Expr& x_i, const Expr& x_j, const EpsRational& v);
00787       
00788       /**
00789        * Asserts a new upper bound constraint on a variable and performs a simple check for consistency (not complete).
00790        * 
00791        * @param x_i the variable to assert the bound on
00792      */
00793       QueryResult assertUpper(const Expr& x_i, const EpsRational& c, const Theorem& thm);
00794 
00795       /**
00796        * Asserts a new lower bound constraint on a variable and performs a simple check for consistency (not complete).
00797        * 
00798        * @param x_i the variable to assert the bound on
00799      */
00800       QueryResult assertLower(const Expr& x_i, const EpsRational& c, const Theorem& thm);
00801       
00802       /**
00803        * Asserts a new equality constraint on a variable by asserting both upper and lower bound.
00804        * 
00805        * @param x_i the variable to assert the bound on
00806      */
00807       QueryResult assertEqual(const Expr& x_i, const EpsRational& c, const Theorem& thm);     
00808 
00809     /**
00810        * Type of noramlization GCD = 1 or just first coefficient 1
00811        */
00812       typedef enum { NORMALIZE_GCD, NORMALIZE_UNIT } NormalizationType;
00813       
00814       /**
00815        * Given a canonized term, compute a factor to make all coefficients integer and relatively prime 
00816        */
00817       Expr computeNormalFactor(const Expr& rhs, NormalizationType type = NORMALIZE_GCD);
00818   
00819       /**
00820        * Normalize an equation (make all coefficients rel. prime integers)
00821        */
00822       Theorem normalize(const Expr& e, NormalizationType type = NORMALIZE_GCD);
00823       
00824       /**
00825        * Normalize an equation (make all coefficients rel. prime integers) accepts a rewrite theorem over 
00826        * eqn|ineqn and normalizes it and returns a theorem to that effect.
00827        */
00828       Theorem normalize(const Theorem& thm, NormalizationType type = NORMALIZE_GCD);
00829     
00830     /**
00831      * Canonise the equation using the tebleaux equations, i.e. replace all the tableaux right sides
00832      * with the corresponding left sides and canonise the result. 
00833      * 
00834      * @param eq the equation to canonise
00835      * @return the explaining theorem
00836      */   
00837       Theorem substAndCanonizeModTableaux(const Theorem& eq);
00838       
00839       /**
00840      * Canonise the sum using the tebleaux equations, i.e. replace all the tableaux right sides
00841      * with the corresponding left sides and canonise the result. 
00842      * 
00843      * @param sum the canonised sum to canonise
00844      * @param the explaining theorem
00845      */   
00846       Theorem substAndCanonizeModTableaux(const Expr& sum);
00847       
00848       /**
00849        * Sustitute the given equation everywhere in the tableaux.
00850        * 
00851        * @param eq the equation to use for substitution
00852        * @return the explaining theorem
00853        */
00854       void substAndCanonizeTableaux(const Theorem& eq);
00855       
00856       /**
00857        * Given an equality eq: \f$\sum a_i x_i = y\f$ and a variable $var$ that appears in
00858        * on the left hand side, pivots $y$ and $var$ so that $y$ comes to the right-hand 
00859        * side.
00860        * 
00861        * @param eq the proof of the equality
00862        * @param var the variable to move to the right-hand side
00863        */
00864       Theorem pivotRule(const Theorem& eq, const Expr& var);
00865       
00866       /**
00867        * Knowing that the tableaux row for \f$x_i\f$ is the problematic one, generate the
00868        * explanation clause. The variables in the row of \f$x_i = \sum_{x_j \in \mathcal{N}}{a_ij x_j}\f$ are separatied to
00869        * <ul>
00870        * <li>\f$\mathcal{N}^+ = \left\lbrace x_j \in \mathcal{N} \; | \; a_{ij} > 0 \right\rbrace\f$
00871      * <li>\f$\mathcal{N}^- = \left\lbrace  x_j \in \mathcal{N} \; | \; a_{ij} < 0\right\rbrace\f$ 
00872        * </ul>
00873        * Then, the explanation clause to be returned is 
00874        * \f[\Gamma = \left\lbrace x_j \leq u_j \; | \; x_j \in \mathcal{N}^+\right\rbrace \cup \left\lbrace l_j \leq x_j \; | \; 
00875        * x_j \in \mathcal{N}^-\right\rbrace \cup \left\lbrace l_i \leq x_i  \right\rbrace\f]
00876        * 
00877        * @param var the variable that caused the clash
00878        * @return the theorem explainang the clash
00879        */ 
00880       Theorem getLowerBoundExplanation(const TebleauxMap::iterator& var_it);
00881 
00882       /**
00883        * Knowing that the tableaux row for \f$x_i\f$ is the problematic one, generate the
00884        * explanation clause. The variables in the row of \f$x_i = \sum_{x_j \in \mathcal{N}}{a_ij x_j}\f$ are separatied to
00885        * <ul>
00886        * <li>\f$\mathcal{N}^+ = \left\lbrace x_j \in \mathcal{N} \; | \; a_{ij} > 0 \right\rbrace\f$
00887      * <li>\f$\mathcal{N}^- = \left\lbrace  x_j \in \mathcal{N} \; | \; a_{ij} < 0\right\rbrace\f$ 
00888        * </ul>
00889        * Then, the explanation clause to be returned is 
00890        * \f[\Gamma = \left\lbrace x_j \leq u_j \; | \; x_j \in \mathcal{N}^-\right\rbrace \cup \left\lbrace l_j \leq x_j \; | \; 
00891        * x_j \in \mathcal{N}^+\right\rbrace \cup \left\lbrace x_i \leq u_i \right\rbrace\f]
00892        * 
00893        * @param var the variable that caused the clash
00894        * @return the theorem explainang the clash
00895        */ 
00896     Theorem getUpperBoundExplanation(const TebleauxMap::iterator& var_it);
00897       
00898       Theorem addInequalities(const Theorem& le_1, const Theorem& le_2);
00899         
00900       /**
00901        * Check the satisfiability 
00902        */
00903       QueryResult checkSatSimplex();
00904       
00905       /**
00906        * Check the satisfiability of integer constraints
00907        */
00908       QueryResult checkSatInteger();
00909       
00910       /** 
00911        * The last lemma that we asserted to check the integer satisfiability. We don't do checksat until
00912        * the lemma split has been asserted.
00913        */
00914       CDO<Theorem> integer_lemma;
00915       
00916   public:
00917     
00918       /**
00919        * Gets the current lower bound on variable x.
00920        * 
00921        * @param x the variable
00922        * @return the current lower bound on x
00923        */
00924       EpsRational getLowerBound(const Expr& x) const;
00925       
00926       /**
00927        * Get the current upper bound on variable x.
00928        * 
00929        * @param x the variable
00930        * @return the current upper bound on x
00931        */
00932       EpsRational getUpperBound(const Expr& x) const;
00933 
00934     /**
00935        * Gets the theorem of the current lower bound on variable x.
00936        * 
00937        * @param x the variable
00938        * @return the current lower bound on x
00939        */
00940       Theorem getLowerBoundThm(const Expr& x) const;
00941       
00942       /**
00943        * Get the theorem of the current upper bound on variable x.
00944        * 
00945        * @param x the variable
00946        * @return the current upper bound on x
00947        */
00948       Theorem getUpperBoundThm(const Expr& x) const;
00949       
00950       /**
00951        * Gets the current valuation of variable x (beta).
00952        * 
00953        * @param x the variable
00954        * @return the current value of variable x
00955        */
00956       EpsRational getBeta(const Expr& x);
00957           
00958   // DDDDDDDDDDDDDDDDDDDDDDDDEEEEEEEEEEEEEEEEEEEEEEEJJJJJJJJJJJJJJJJJJJJJAAAAAAAAAAAAAAAAAAAAAAANNNNNNNNNNNNNNNNNNNNNNN
00959 
00960 };
00961 
00962 }
00963 
00964 #endif

Generated on Tue Jul 3 14:33:40 2007 for CVC3 by  doxygen 1.5.1