theory_arith_new.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 (for counterexample generation)
00113   CDMap<Expr, bool> d_sharedTerms;
00114   //! Set of shared integer variables (i-leaves)
00115   CDMap<Expr, bool> d_sharedVars;
00116   //Directed Acyclic Graph representing partial variable ordering for
00117   //variable projection over inequalities.
00118   class VarOrderGraph {
00119     ExprMap<std::vector<Expr> > d_edges;
00120     ExprMap<bool> d_cache;
00121     bool dfs(const Expr& e1, const Expr& e2);
00122   public:
00123     void addEdge(const Expr& e1, const Expr& e2);
00124     //returns true if e1 < e2, false otherwise.
00125     bool lessThan(const Expr& e1, const Expr& e2);
00126     //selects those variables which are largest and incomparable among
00127     //v1 and puts it into v2
00128     void selectLargest(const std::vector<Expr>& v1, std::vector<Expr>& v2);
00129     //selects those variables which are smallest and incomparable among
00130     //v1, removes them from v1 and  puts them into v2. 
00131     void selectSmallest( std::vector<Expr>& v1, std::vector<Expr>& v2);
00132 
00133   };
00134   
00135   VarOrderGraph d_graph;
00136 
00137   // Private methods
00138   //! Check the term t for integrality.  
00139   /*! \return a theorem of IS_INTEGER(t) or Null. */
00140   Theorem isIntegerThm(const Expr& e);
00141   //! A helper method for isIntegerThm()
00142   /*! Check if IS_INTEGER(e) is easily derivable from the given 'thm' */
00143   Theorem isIntegerDerive(const Expr& isIntE, const Theorem& thm);
00144   //! Check if the kids of e are fully simplified and canonized (for debugging)
00145   bool kidsCanonical(const Expr& e);
00146   
00147   //! Canonize the expression e, assuming all children are canonical
00148   Theorem canon(const Expr& e);
00149   /*! @brief Canonize and reduce e w.r.t. union-find database; assume
00150    * all children are canonical */
00151   Theorem canonSimplify(const Expr& e);
00152   /*! @brief Composition of canonSimplify(const Expr&) by
00153    * transitivity: take e0 = e1, canonize and simplify e1 to e2,
00154    * return e0 = e2. */
00155   Theorem canonSimplify(const Theorem& thm) {
00156     return transitivityRule(thm, canonSimplify(thm.getRHS()));
00157   }
00158   //! Canonize predicate (x = y, x < y, etc.)
00159   Theorem canonPred(const Theorem& thm);
00160   //! Canonize predicate like canonPred except that the input theorem
00161   //! is an equivalent transformation.
00162   Theorem canonPredEquiv(const Theorem& thm);
00163   //! Solve an equation and return an equivalent Theorem in the solved form
00164   Theorem doSolve(const Theorem& e);
00165   //! takes in a conjunction equivalence Thm and canonizes it.
00166   Theorem canonConjunctionEquiv(const Theorem& thm);
00167   //! picks the monomial with the smallest abs(coeff) from the input
00168   //integer equation.
00169   Expr pickIntEqMonomial(const Expr& right);
00170   //! processes equalities with 1 or more vars of type REAL
00171   Theorem processRealEq(const Theorem& eqn);
00172   //! processes equalities whose vars are all of type INT
00173   Theorem processIntEq(const Theorem& eqn);
00174   //! One step of INT equality processing (aux. method for processIntEq())
00175   Theorem processSimpleIntEq(const Theorem& eqn);
00176   //! Take an inequality and isolate a variable
00177   Theorem isolateVariable(const Theorem& inputThm, bool& e1);
00178   //! Update the statistics counters for the variable with a coeff. c
00179   void updateStats(const Rational& c, const Expr& var);
00180   //! Update the statistics counters for the monomial
00181   void updateStats(const Expr& monomial);
00182   //! Add an inequality to the input buffer.  See also d_buffer
00183   void addToBuffer(const Theorem& thm);
00184   Expr pickMonomial(const Expr& right);
00185  public: // ArithTheoremProducer needs this function, so make it public
00186   //! Separate monomial e = c*p1*...*pn into c and 1*p1*...*pn
00187   void separateMonomial(const Expr& e, Expr& c, Expr& var);
00188   //! Check the term t for integrality (return bool)
00189   bool isInteger(const Expr& e) { return !(isIntegerThm(e).isNull()); }
00190  private:
00191   bool lessThanVar(const Expr& isolatedVar, const Expr& var2);
00192   //! Check if the term expression is "stale"
00193   bool isStale(const Expr& e);
00194   //! Check if the inequality is "stale" or subsumed
00195   bool isStale(const Ineq& ineq);
00196   void projectInequalities(const Theorem& theInequality,bool isolatedVarOnRHS);
00197   void assignVariables(std::vector<Expr>&v);
00198   void findRationalBound(const Expr& varSide, const Expr& ratSide, 
00199        const Expr& var,
00200        Rational &r);
00201   bool findBounds(const Expr& e, Rational& lub, Rational&  glb);
00202 
00203   Theorem normalizeProjectIneqs(const Theorem& ineqThm1,
00204         const Theorem& ineqThm2);
00205   //! Take a system of equations and turn it into a solved form
00206   Theorem solvedForm(const std::vector<Theorem>& solvedEqs);
00207   /*! @brief Substitute all vars in term 't' according to the
00208    * substitution 'subst' and canonize the result.
00209    */
00210   Theorem substAndCanonize(const Expr& t, ExprMap<Theorem>& subst);
00211   /*! @brief Substitute all vars in the RHS of the equation 'eq' of
00212    * the form (x = t) according to the substitution 'subst', and
00213    * canonize the result.
00214    */
00215   Theorem substAndCanonize(const Theorem& eq, ExprMap<Theorem>& subst);
00216   //! Traverse 'e' and push all the i-leaves into 'vars' vector
00217   void collectVars(const Expr& e, std::vector<Expr>& vars,
00218        std::set<Expr>& cache);
00219   /*! @brief Check if alpha <= ax & bx <= beta is a finite interval
00220    *  for integer var 'x', and assert the corresponding constraint
00221    */
00222   void processFiniteInterval(const Theorem& alphaLEax,
00223            const Theorem& bxLEbeta);
00224   //! For an integer var 'x', find and process all constraints A <= ax <= A+c 
00225   void processFiniteIntervals(const Expr& x);
00226   //! Recursive setup for isolated inequalities (and other new expressions)
00227   void setupRec(const Expr& e);
00228 
00229 public:
00230   TheoryArithNew(TheoryCore* core);
00231   ~TheoryArithNew();
00232 
00233   // Trusted method that creates the proof rules class (used in constructor).
00234   // Implemented in arith_theorem_producer.cpp
00235   ArithProofRules* createProofRules();
00236 
00237   // Theory interface
00238   void addSharedTerm(const Expr& e);
00239   void assertFact(const Theorem& e);
00240   void refineCounterExample();
00241   void computeModelBasic(const std::vector<Expr>& v);
00242   void computeModel(const Expr& e, std::vector<Expr>& vars);
00243   void checkSat(bool fullEffort);
00244   Theorem rewrite(const Expr& e);
00245   void setup(const Expr& e);
00246   void update(const Theorem& e, const Expr& d);
00247   Theorem solve(const Theorem& e);
00248   void checkAssertEqInvariant(const Theorem& e);
00249   void checkType(const Expr& e);
00250   Cardinality finiteTypeInfo(Expr& e, Unsigned& n,
00251                              bool enumerate, bool computeSize);
00252   void computeType(const Expr& e);
00253   Type computeBaseType(const Type& t);
00254   void computeModelTerm(const Expr& e, std::vector<Expr>& v);
00255   Expr computeTypePred(const Type& t, const Expr& e);
00256   Expr computeTCC(const Expr& e);
00257   ExprStream& print(ExprStream& os, const Expr& e);
00258   virtual Expr parseExprOp(const Expr& e);
00259 
00260   // DDDDDDDDDDDDDDDDDDDDDDDDEEEEEEEEEEEEEEEEEEEEEEEJJJJJJJJJJJJJJJJJJJJJAAAAAAAAAAAAAAAAAAAAAAANNNNNNNNNNNNNNNNNNNNNNN
00261   
00262     public: 
00263     
00264       /**
00265        * EpsRational class ecapsulates the rationals with a symbolic small \f$\epsilon\f$ added. Each rational
00266        * number is presented as a pair \f$(q, k) = q + k\epsilon\f$, where \f$\epsilon\f$ is treated symbolically.
00267        * The operations on the new rationals are defined as
00268        * <ul>
00269        *  <li>\f$(q_1, k_1) + (q_2, k_2) \equiv (q_1 + q_2, k_1 + k_2)\f$
00270        *  <li>\f$a \times (q, k) \equiv (a \times q, a \times k)\f$
00271        *  <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$
00272        * </ul>
00273        * 
00274        * Note that the operations on the infinite values are not defined, as they are never used currently. Infinities can
00275        * only be asigned or compared. 
00276        */
00277       class EpsRational {
00278         
00279         protected:
00280         
00281           /** Type of rationals, normal and the two infinities */
00282           typedef enum { FINITE, PLUS_INFINITY, MINUS_INFINITY } RationalType;
00283           
00284           /** The type of this rational */
00285           RationalType type;      
00286 
00287           /** The rational part */
00288           Rational q; 
00289           
00290           /** The epsilon multiplier */
00291           Rational k;       
00292         
00293           /**
00294            * Private constructor to construt infinities.
00295            */
00296           EpsRational(RationalType type) : type(type) {}
00297         
00298         public:
00299         
00300           /**
00301            * Returns if the number is a plain rational.
00302            * 
00303            * @return true if rational, false otherwise
00304            */
00305           inline bool isRational() const { return k == 0; }
00306           
00307           /**
00308            * Returns if the number is a plain integer.
00309            * 
00310            * @return true if rational, false otherwise
00311            */
00312           inline bool isInteger() const { return k == 0 && q.isInteger(); }
00313           
00314           /** 
00315            * Returns the floor of the number \f$x = q + k \epsilon\f$ using the following formula
00316            * \f[
00317            * \lfloor \beta(x) \rfloor = \left\{
00318            * \begin{tabular}{ll}
00319            * $\lfloor q \rfloor$ & $\mathrm{if\ } q \notin Z$\\
00320            * $q$ & $\mathrm{if\ } q \in Z \mathrm{\ and\ } k \geq 0$\\
00321            * $q - 1$ & $\mathrm{if\ } q \in Z \mathrm{\ and\ } k < 0$
00322            * \end{tabular}\right.
00323            * \f]
00324            */
00325           inline Rational getFloor() const { 
00326             if (q.isInteger()) {
00327               if (k >= 0) return q;
00328               else return q - 1;
00329             } else 
00330               // If not an integer, just floor it
00331               return floor(q);
00332           } 
00333           
00334 
00335         /** 
00336          * Returns the rational part of the number
00337          * 
00338          * @return the rational 
00339          */
00340         inline Rational getRational() const { return q; }
00341 
00342         /** The infinity constant */
00343         static const EpsRational PlusInfinity;
00344         /** The negative infinity constant */
00345         static const EpsRational MinusInfinity;
00346         /** The zero constant */
00347         static const EpsRational Zero;
00348         
00349 
00350         /** The blank constructor */
00351         EpsRational() : type(FINITE), q(0), k(0) {}
00352 
00353         /** Copy constructor */
00354         EpsRational(const EpsRational& r) : type(r.type), q(r.q), k(r.k) {} 
00355         
00356           /**
00357            * Constructor from a rational, constructs a new pair (q, 0).
00358            * 
00359            * @param q the rational
00360            */
00361         EpsRational(const Rational q) : type(FINITE), q(q), k(0) {} 
00362       
00363           /**
00364            * Constructor from a rational and a given epsilon multiplier, constructs a 
00365            * new pair (q, k).
00366            * 
00367            * @param q the rational
00368            * @param k the epsilon multiplier
00369            */
00370         EpsRational(const Rational q, const Rational k) : type(FINITE), q(q), k(k) {} 
00371       
00372           /**
00373            * Addition operator for two EpsRational numbers.
00374            * 
00375            * @param r the number to be added
00376            * @return the sum as defined in the class 
00377            */
00378           inline EpsRational operator + (const EpsRational& r) const {
00379             DebugAssert(type == FINITE, "EpsRational::operator +, adding to infinite number");
00380             DebugAssert(r.type == FINITE, "EpsRational::operator +, adding an infinite number");
00381             return EpsRational(q + r.q, k + r.k);
00382           }
00383           
00384           /**
00385            * Addition operator for two EpsRational numbers.
00386            * 
00387            * @param r the number to be added
00388            * @return the sum as defined in the class 
00389            */
00390           inline EpsRational& operator += (const EpsRational& r) {
00391             DebugAssert(type == FINITE, "EpsRational::operator +, adding to infinite number");
00392             q = q + r.q;
00393             k = k + r.k;
00394             return *this;
00395           }
00396           
00397           /**
00398            * Subtraction operator for two EpsRational numbers.
00399            * 
00400            * @param r the number to be added
00401            * @return the sum as defined in the class 
00402            */
00403           inline EpsRational operator - (const EpsRational& r) const {
00404           DebugAssert(type == FINITE, "EpsRational::operator -, subtracting from infinite number");
00405             DebugAssert(r.type == FINITE, "EpsRational::operator -, subtracting an infinite number");
00406             return EpsRational(q - r.q, k - r.k);
00407           }
00408           
00409           /**
00410            * Multiplication operator EpsRational number and a rational number.
00411            * 
00412            * @param a the number to be multiplied
00413            * @return the product as defined in the class 
00414            */
00415           inline EpsRational operator * (const Rational& a) const {
00416           DebugAssert(type == FINITE, "EpsRational::operator *, multiplying an infinite number");
00417             return EpsRational(a * q, a * k);
00418           }
00419           
00420           /**
00421            * Division operator EpsRational number and a rational number.
00422            * 
00423            * @param a the number to be multiplied
00424            * @return the product as defined in the class 
00425            */
00426           inline EpsRational operator / (const Rational& a) const {
00427           DebugAssert(type == FINITE, "EpsRational::operator *, dividing an infinite number");
00428             return EpsRational(q / a, k / a);
00429           }
00430           
00431           /**
00432            * Equality comparison operator.
00433            */
00434           inline bool operator == (const EpsRational& r) const { return (q == r.q && k == r.k); }
00435           
00436           /**
00437            * Less than or equal comparison operator.
00438            */
00439           inline bool operator <= (const EpsRational& r) const { 
00440             switch (r.type) {
00441               case FINITE:
00442                 if (type == FINITE) 
00443                   // Normal comparison
00444                   return (q < r.q || (q == r.q && k <= r.k));
00445                 else
00446                   // Finite number is bigger only of the negative infinity 
00447                   return type == MINUS_INFINITY;
00448               case PLUS_INFINITY:
00449                 // Everything is less then or equal than +inf
00450                 return true;
00451               case MINUS_INFINITY:
00452                 // Only -inf is less then or equal than -inf
00453                 return (type == MINUS_INFINITY);
00454               default:
00455                 // Ohohohohohoooooo, whats up
00456                 FatalAssert(false, "EpsRational::operator <=, what kind of number is this????");    
00457             }
00458             return false;
00459           }
00460           
00461           /**
00462            * Less than comparison operator.
00463            */
00464           inline bool operator < (const EpsRational& r) const { return !(r <= *this); }
00465           
00466           /**
00467            * Greater than comparison operator.
00468            */
00469           inline bool operator > (const EpsRational& r) const { return !(*this <= r); }
00470           
00471           /**
00472            * Returns the string representation of the number.
00473            * 
00474            * @return the string representation of the number
00475            */
00476           std::string toString() const { 
00477             switch (type) {
00478               case FINITE:
00479                 return "(" + q.toString() + ", " + k.toString() + ")";
00480               case PLUS_INFINITY:
00481                 return "+inf";
00482               case MINUS_INFINITY:
00483                 return "-inf";
00484               default:
00485                 FatalAssert(false, "EpsRational::toString, what kind of number is this????");
00486             } 
00487             return "hm, what am I?";
00488           }
00489       };
00490   
00491       /**
00492        * Registers the atom given from the core. This atoms are stored so that they can be used
00493        * for theory propagation.
00494        * 
00495        * @param e the expression (atom) that is part of the input formula
00496        */ 
00497     void registerAtom(const Expr& e);
00498  
00499     private:    
00500         
00501         /** A set of all integer variables */
00502         std::set<Expr> intVariables;
00503         
00504         /**
00505          * Return a Gomory cut plane derivation of the variable $x_i$. Mixed integer
00506          * Gomory cut can be constructed if 
00507          * <ul>
00508          * <li>\f$x_i\f$ is a integer basic variable with a non-integer value
00509          * <li>all non-basic variables in the row of \f$x_i\f$ are assigned to their
00510          *     upper or lower bounds
00511          * <li>all the values on the right side of the row have rational values (non
00512          *     eps-rational values)
00513          * </ul>
00514          */ 
00515         Theorem deriveGomoryCut(const Expr& x_i);
00516         
00517         /**
00518          * Tries to rafine the integer constraint of the theorem. For example,
00519          * x < 1 is rewritten as x <= 0, and x <(=) 1.5 is rewritten as x <= 1.
00520          * The constraint should be in the normal form.
00521          * 
00522          * @param thm the derivation of the constraint 
00523          */
00524         Theorem rafineIntegerConstraints(const Theorem& thm);
00525         
00526         /** Are we consistent or not */
00527         CDO<QueryResult> consistent;
00528         
00529         /** The theorem explaining the inconsistency */
00530         Theorem explanation;
00531         
00532         /** 
00533          * The structure necessaty to hold the bounds.
00534          */
00535         struct BoundInfo {
00536           /** The bound itself */
00537           EpsRational bound;
00538           /** The assertion theoreem of the bound */
00539           Theorem theorem;
00540           
00541           /** Constructor */
00542           BoundInfo(const EpsRational& bound, const Theorem& thm): bound(bound), theorem(thm) {}
00543           
00544           /** The empty constructor for the map */
00545           BoundInfo(): bound(0), theorem() {}
00546           
00547           /** 
00548            * The comparator, just if we need it. Compares first by expressions then by bounds 
00549            */
00550           bool operator < (const BoundInfo& bI) const {
00551             // Get tje expressoins
00552             const Expr& expr1 = (theorem.isRewrite() ? theorem.getRHS() : theorem.getExpr());
00553             const Expr& expr2 = (bI.theorem.isRewrite() ? bI.theorem.getRHS() : bI.theorem.getExpr());
00554             
00555             std::cout << expr1 << " @ " << expr2 << std::endl;
00556             
00557             // Compare first by the expressions (right sides of expressions)
00558             if (expr1[1] == expr2[1])
00559               // If the same, just return the bound comparison (plus a trick to order equal bounds, different relations) 
00560               if (bound == bI.bound && expr1.getKind() != expr2.getKind())
00561                 return expr1.getKind() == LE; // LE before GE -- only case that can happen                              
00562               else
00563                 return bound < bI.bound;
00564             else
00565               // Return the expression comparison
00566               return expr1[1] < expr2[1];
00567           }
00568         };
00569 
00570 
00571         /** 
00572          * The structure necessaty to hold the bounds on expressions (for theory propagation).
00573          */
00574         struct ExprBoundInfo {
00575           /** The bound itself */
00576           EpsRational bound;
00577           /** The assertion theoreem of the bound */
00578           Expr e;
00579           
00580           /** Constructor */
00581           ExprBoundInfo(const EpsRational& bound, const Expr& e): bound(bound), e(e) {}
00582           
00583           /** The empty constructor for the map */
00584           ExprBoundInfo(): bound(0) {}
00585           
00586           /** 
00587            * The comparator, just if we need it. Compares first by expressions then by bounds 
00588            */
00589           bool operator < (const ExprBoundInfo& bI) const {
00590             
00591             // Compare first by the expressions (right sides of expressions)
00592             if (e[1] == bI.e[1])
00593               // If the same, just return the bound comparison (plus a trick to order equal bounds, different relations) 
00594               if (bound == bI.bound && e.getKind() != bI.e.getKind())
00595                 return e.getKind() == LE; // LE before GE -- only case that can happen                              
00596               else
00597                 return bound < bI.bound;
00598             else
00599               // Return the expression comparison
00600               return e[1] < bI.e[1];
00601           }
00602         };
00603         
00604         /** The map from variables to lower bounds (these must be backtrackable) */  
00605       CDMap<Expr, BoundInfo> lowerBound;
00606       /** The map from variables to upper bounds (these must be backtrackable) */ 
00607       CDMap<Expr, BoundInfo> upperBound;
00608       /** The current real valuation of the variables (these must be backtrackable for the last succesefull checkSAT!!!) */
00609       CDMap<Expr, EpsRational> beta;
00610           
00611       typedef Hash::hash_map<Expr, Theorem> TebleauxMap;
00612       //typedef google::sparse_hash_map<Expr, Theorem, Hash::hash<Expr> > TebleauxMap;
00613       //typedef std::map<Expr, Theorem> TebleauxMap;
00614       
00615       typedef std::set<Expr> SetOfVariables;
00616       typedef Hash::hash_map<Expr, SetOfVariables> DependenciesMap;
00617       
00618       /** Maps variables to sets of variables that depend on it in the tableaux */
00619       DependenciesMap dependenciesMap;  
00620           
00621         /** The tableaux, a map from basic variables to the expressions over the non-basic ones (theorems that explain them how we got there) */ 
00622       TebleauxMap tableaux;
00623 
00624     /** Additional tableaux map from expressions asserted to the corresponding theorems explaining the introduction of the new variables */
00625     TebleauxMap freshVariables;
00626     
00627     /** A set containing all the unsatisfied basic variables */
00628     std::set<Expr> unsatBasicVariables;
00629     
00630     /** The vector to keep the assignments from fresh variables to expressions they represent */  
00631     std::vector<Expr> assertedExpr;
00632     /** The backtrackable number of fresh variables asserted so far */
00633     CDO<unsigned int> assertedExprCount;
00634     
00635     /** A set of BoundInfo objects */
00636     typedef std::set<ExprBoundInfo> BoundInfoSet;
00637     
00638     /** Internal variable to see wheather to propagate or not */
00639     bool propagate;
00640     
00641     /** 
00642      * Propagate all that is possible from given assertion and its bound
00643      */
00644     void propagateTheory(const Expr& assertExpr, const EpsRational& bound, const EpsRational& oldBound);    
00645     
00646     /**
00647      * Store all the atoms from the formula in this set. It is searchable by an expression
00648      * and the bound. To get all the implied atoms, one just has to go up (down) and check if the 
00649      * atom or it's negation are implied.
00650      */
00651     BoundInfoSet allBounds;
00652     
00653     /**
00654      * Adds var to the dependencies sets of all the variables in the sum.
00655      * 
00656      * @param var the variable on the left side 
00657      * @param sum the sum that defines the variable
00658      */
00659     void updateDependenciesAdd(const Expr& var, const Expr& sum);
00660     
00661     /**
00662      * Remove var from the dependencies sets of all the variables in the sum.
00663      * 
00664      * @param var the variable on the left side 
00665      * @param sum the sum that defines the variable
00666      */
00667     void updateDependenciesRemove(const Expr& var, const Expr& sum);
00668   
00669     /**
00670      * Updates the dependencies if a right side of an expression in the tableaux is changed. For example,
00671      * if oldExpr is x + y and newExpr is y + z, var will be added to the dependency list of z, and removed
00672      * from the dependency list of x.
00673      * 
00674      * @param oldExpr the old right side of the tableaux 
00675      * @param newExpr the new right side of the tableaux
00676      * @param var the variable that is defined by these two expressions
00677      * @param skipVar a variable to skip when going through the expressions
00678      */
00679     void updateDependencies(const Expr& oldExpr, const Expr& newExpr, const Expr& var, const Expr& skipVar);
00680     
00681     /**
00682      * Update the values of variables that have appeared in the tableaux due to backtracking.
00683      */
00684     void updateFreshVariables();
00685     
00686     /** 
00687      * Updates the value of variable var by computing the value of expression e.
00688      * 
00689      * @param var the variable to update
00690      * @param e the expression to compute
00691      */
00692     void updateValue(const Expr& var, const Expr& e);
00693     
00694     /**
00695      * Returns a string representation of the tableaux.
00696      * 
00697      * @return tableaux as string
00698      */
00699     std::string tableauxAsString() const;
00700     
00701     /**
00702      * Returns a string representation of the unsat variables.
00703      * 
00704      * @return unsat as string
00705      */
00706     std::string unsatAsString() const;
00707     
00708     /**
00709      * Returns a string representation of the current bounds.
00710      * 
00711      * @return tableaux as string
00712      */
00713     std::string boundsAsString();
00714 
00715     /**
00716      * Gets the equality of the fresh variable tableaux variable corresponding to this expression. If the expression has already been
00717      * asserted, the coresponding variable is returned, othervise a fresh variable is created and the theorem is returned.
00718      * 
00719      * @param leftSide the left side of the asserted constraint
00720      * @return the equality theorem s = leftSide
00721      */
00722     Theorem getVariableIntroThm(const Expr& leftSide);
00723 
00724     /**
00725      * Find the coefficient standing by the variable var in the expression expr. Expresion is expected to be
00726      * in canonical form, i.e either a rational constant, an arithmetic leaf (i.e. variable or term from some 
00727      * other theory), (MULT rat leaf) where rat is a non-zero rational constant, leaf is an arithmetic leaf or
00728      * (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$) 
00729      * and each leaf in \f$term_i\f$ must be strictly greater than the leaf in \f$term_{i+1}\f$.               
00730      * 
00731      * @param var the variable
00732      * @param expr the expression to search in
00733      */     
00734       const Rational& findCoefficient(const Expr& var, const Expr& expr); 
00735     
00736       /**
00737        * Return true iof the given variable is basic in the tableaux, i.e. it is on the left side, expressed
00738        * in terms of the non-basic variables.
00739        * 
00740        * @param x the variable to be checked
00741        * @return true if the variable is basic, false if the variable is non-basic
00742        */
00743       bool isBasic(const Expr& x) const;
00744       
00745       /**
00746        * Returns the coefficient at a_ij in the current tableaux, i.e. the coefficient 
00747        * at x_j in the row of x_i.
00748        * 
00749        * @param x_i a basic variable
00750        * @param x_j a non-basic variable
00751        * @return the reational coefficient 
00752        */
00753       Rational getTableauxEntry(const Expr& x_i, const Expr& x_j); 
00754       
00755       /**
00756        * Swaps a basic variable \f$x_r\f$ and a non-basic variable \f$x_s\f$ such
00757        * that ars \f$a_{rs} \neq 0\f$. After pivoting, \f$x_s\f$ becomes basic and \f$x_r\f$ becomes non-basic. 
00758        * The tableau is updated by replacing equation \f[x_r = \sum_{x_j \in N}{a_{rj}xj}\f] with
00759        * \f[x_s = \frac{x_r}{a_{rs}} - \sum_{x_j \in N }{\frac{a_{rj}}{a_rs}x_j}\f] and this equation 
00760        * is used to eliminate \f$x_s\f$ from the rest of the tableau by substitution.
00761        * 
00762        * @param x_r a basic variable
00763        * @param x_s a non-basic variable
00764        */
00765       void pivot(const Expr& x_r, const Expr& x_s);
00766     
00767       /**
00768        * Sets the value of a non-basic variable \f$x_i\f$ to \f$v\f$ and adjusts the value of all 
00769        * the basic variables so that all equations remain satisfied.
00770        * 
00771        * @param x_i a non-basic variable
00772        * @param v the value to set the variable \f$x_i\f$ to 
00773        */
00774       void update(const Expr& x_i, const EpsRational& v);
00775       
00776       /**
00777        * 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 
00778        * variables to keep the equations satisfied.
00779        * 
00780        * @param x_i a basic variable
00781        * @param x_j a non-basic variable
00782        * @param v the valie to assign to x_i
00783        */ 
00784       void pivotAndUpdate(const Expr& x_i, const Expr& x_j, const EpsRational& v);
00785       
00786       /**
00787        * Asserts a new upper bound constraint on a variable and performs a simple check for consistency (not complete).
00788        * 
00789        * @param x_i the variable to assert the bound on
00790        * @param c the bound to assert
00791      */
00792       QueryResult assertUpper(const Expr& x_i, const EpsRational& c, const Theorem& thm);
00793 
00794       /**
00795        * Asserts a new lower bound constraint on a variable and performs a simple check for consistency (not complete).
00796        * 
00797        * @param x_i the variable to assert the bound on
00798        * @param c the bound to assert
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 bounds.
00804        * 
00805        * @param x_i the variable to assert the bound on
00806        * @param c the bound to assert
00807      */
00808       QueryResult assertEqual(const Expr& x_i, const EpsRational& c, const Theorem& thm);     
00809 
00810     /**
00811        * Type of noramlization GCD = 1 or just first coefficient 1
00812        */
00813       typedef enum { NORMALIZE_GCD, NORMALIZE_UNIT } NormalizationType;
00814       
00815       /**
00816        * Given a canonized term, compute a factor to make all coefficients integer and relatively prime 
00817        */
00818       Expr computeNormalFactor(const Expr& rhs, NormalizationType type = NORMALIZE_GCD);
00819   
00820       /**
00821        * Normalize an equation (make all coefficients rel. prime integers)
00822        */
00823       Theorem normalize(const Expr& e, NormalizationType type = NORMALIZE_GCD);
00824       
00825       /**
00826        * Normalize an equation (make all coefficients rel. prime integers) accepts a rewrite theorem over 
00827        * eqn|ineqn and normalizes it and returns a theorem to that effect.
00828        */
00829       Theorem normalize(const Theorem& thm, NormalizationType type = NORMALIZE_GCD);
00830     
00831     /**
00832      * Canonise the equation using the tebleaux equations, i.e. replace all the tableaux right sides
00833      * with the corresponding left sides and canonise the result. 
00834      * 
00835      * @param eq the equation to canonise
00836      * @return the explaining theorem
00837      */   
00838       Theorem substAndCanonizeModTableaux(const Theorem& eq);
00839       
00840       /**
00841      * Canonise the sum using the tebleaux equations, i.e. replace all the tableaux right sides
00842      * with the corresponding left sides and canonise the result. 
00843      * 
00844      * @param sum the canonised sum to canonise
00845      * @return the explaining theorem
00846      */   
00847       Theorem substAndCanonizeModTableaux(const Expr& sum);
00848       
00849       /**
00850        * Sustitute the given equation everywhere in the tableaux.
00851        * 
00852        * @param eq the equation to use for substitution
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 separated 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_it 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 separated 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_it 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 Wed Nov 18 16:13:31 2009 for CVC3 by  doxygen 1.5.2