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