1 /*****************************************************************************/ 2 /*! 3 * \file theory_arith_old.h 4 * 5 * Author: Clark Barrett 6 * 7 * Created: Thu Jun 14 13:22:11 2007 8 * 9 * <hr> 10 * 11 * License to use, copy, modify, sell and/or distribute this software 12 * and its documentation for any purpose is hereby granted without 13 * royalty, subject to the terms and conditions defined in the \ref 14 * LICENSE file provided with this distribution. 15 * 16 * <hr> 17 * 18 */ 19 /*****************************************************************************/ 20 21 #ifndef _cvc3__include__theory_arith_old_h_ 22 #define _cvc3__include__theory_arith_old_h_ 23 24 #include "theory_arith.h" 25 #include <set> 26 #include <list> 27 28 namespace CVC3 { 29 30 class TheoryArithOld :public TheoryArith { 31 CDList<Theorem> d_diseq; // For concrete model generation 32 CDO<size_t> d_diseqIdx; // Index to the next unprocessed disequality 33 CDMap<Expr, bool> diseqSplitAlready; // Have we eplit on this disequality already 34 ArithProofRules* d_rules; 35 CDO<bool> d_inModelCreation; 36 37 //! Data class for the strongest free constant in separation inqualities 38 class FreeConst { 39 private: 40 Rational d_r; 41 bool d_strict; 42 public: FreeConst()43 FreeConst() { } FreeConst(const Rational & r,bool strict)44 FreeConst(const Rational& r, bool strict): d_r(r), d_strict(strict) { } getConst()45 const Rational& getConst() const { return d_r; } strict()46 bool strict() const { return d_strict; } 47 }; 48 //! Printing 49 friend std::ostream& operator<<(std::ostream& os, const FreeConst& fc); 50 51 //! Private class for an inequality in the Fourier-Motzkin database 52 class Ineq { 53 private: 54 Theorem d_ineq; //!< The inequality 55 bool d_rhs; //!< Var is isolated on the RHS 56 const FreeConst* d_const; //!< The max/min const for subsumption check 57 //! Default constructor is disabled Ineq()58 Ineq() { } 59 public: 60 //! Initial constructor. 'r' is taken from the subsumption database. Ineq(const Theorem & ineq,bool varOnRHS,const FreeConst & c)61 Ineq(const Theorem& ineq, bool varOnRHS, const FreeConst& c): 62 d_ineq(ineq), d_rhs(varOnRHS), d_const(&c) { } 63 //! Get the inequality ineq()64 const Theorem ineq() const { return d_ineq; } 65 //! Get the max/min constant getConst()66 const FreeConst& getConst() const { return *d_const; } 67 //! Flag whether var is isolated on the RHS varOnRHS()68 bool varOnRHS() const { return d_rhs; } 69 //! Flag whether var is isolated on the LHS varOnLHS()70 bool varOnLHS() const { return !d_rhs; } 71 //! Auto-cast to Theorem Theorem()72 operator Theorem() const { return d_ineq; } 73 }; 74 //! Printing 75 friend std::ostream& operator<<(std::ostream& os, const Ineq& ineq); 76 77 //! Database of inequalities with a variable isolated on the right 78 ExprMap<CDList<Ineq> *> d_inequalitiesRightDB; 79 80 //! Database of inequalities with a variable isolated on the left 81 ExprMap<CDList<Ineq> *> d_inequalitiesLeftDB; 82 83 //! Mapping of inequalities to the largest/smallest free constant 84 /*! The Expr is the original inequality with the free constant 85 * removed and inequality converted to non-strict (for indexing 86 * purposes). I.e. ax<c+t becomes ax<=t. This inequality is mapped 87 * to a pair<c,strict>, the smallest (largest for c+t<ax) constant 88 * among inequalities with the same 'a', 'x', and 't', and a boolean 89 * flag indicating whether the strongest inequality is strict. 90 */ 91 CDMap<Expr, FreeConst> d_freeConstDB; 92 93 // /** Is the problem only difference logic */ 94 // CDO<bool> isDL; 95 // CDO<int> total_buf_size; 96 // CDO<int> processed; 97 // 98 // Input buffer to store the incoming inequalities 99 CDList<Theorem> d_buffer_0; //!< Buffer of input inequalities (high priority) 100 CDList<Theorem> d_buffer_1; //!< Buffer of input inequalities (one variable) 101 CDList<Theorem> d_buffer_2; //!< Buffer of input inequalities (small constraints) 102 CDList<Theorem> d_buffer_3; //!< Buffer of input inequalities (big constraint) 103 104 CDO<size_t> d_bufferIdx_0; //!< Buffer index of the next unprocessed inequality 105 CDO<size_t> d_bufferIdx_1; //!< Buffer index of the next unprocessed inequality 106 CDO<size_t> d_bufferIdx_2; //!< Buffer index of the next unprocessed inequality 107 CDO<size_t> d_bufferIdx_3; //!< Buffer index of the next unprocessed inequality 108 109 CDO<size_t> diff_logic_size; //!< Number of queries that are just difference logic 110 111 const int* d_bufferThres; //!< Threshold when the buffer must be processed 112 113 const bool* d_splitSign; // Whether to split on the signs of non-trivial nonlinear products 114 115 const int* d_grayShadowThres; //!< Threshold on gray shadow size (ignore it and set incomplete) 116 117 // Statistics for the variables 118 119 /*! @brief Mapping of a variable to the number of inequalities where 120 the variable would be isolated on the right */ 121 CDMap<Expr, int> d_countRight; 122 123 /*! @brief Mapping of a variable to the number of inequalities where 124 the variable would be isolated on the left */ 125 CDMap<Expr, int> d_countLeft; 126 127 //! Set of shared terms (for counterexample generation) 128 CDMap<Expr, bool> d_sharedTerms; 129 CDList<Expr> d_sharedTermsList; 130 131 //! Set of shared integer variables (i-leaves) 132 CDMap<Expr, bool> d_sharedVars; 133 134 //Directed Acyclic Graph representing partial variable ordering for 135 //variable projection over inequalities. 136 class VarOrderGraph { 137 ExprMap<std::vector<Expr> > d_edges; 138 ExprMap<bool> d_cache; 139 bool dfs(const Expr& e1, const Expr& e2); 140 void dfs(const Expr& e1, std::vector<Expr>& output_list); 141 public: 142 void addEdge(const Expr& e1, const Expr& e2); 143 //returns true if e1 < e2, false otherwise. 144 bool lessThan(const Expr& e1, const Expr& e2); 145 //selects those variables which are largest and incomparable among 146 //v1 and puts it into v2 147 void selectLargest(const std::vector<Expr>& v1, std::vector<Expr>& v2); 148 //selects those variables which are smallest and incomparable among 149 //v1, removes them from v1 and puts them into v2. 150 void selectSmallest( std::vector<Expr>& v1, std::vector<Expr>& v2); 151 //returns the list of vertices in the topological order 152 void getVerticesTopological(std::vector<Expr>& output_list); 153 }; 154 155 VarOrderGraph d_graph; 156 157 // Private methods 158 159 //! Check the term t for integrality. 160 /*! \return a theorem of IS_INTEGER(t) or Null. */ 161 Theorem isIntegerThm(const Expr& e); 162 163 //! A helper method for isIntegerThm() 164 /*! Check if IS_INTEGER(e) is easily derivable from the given 'thm' */ 165 Theorem isIntegerDerive(const Expr& isIntE, const Theorem& thm); 166 167 //! Extract the free constant from an inequality 168 const Rational& freeConstIneq(const Expr& ineq, bool varOnRHS); 169 170 //! Update the free constant subsumption database with new inequality 171 /*! \return a reference to the max/min constant. 172 * 173 * Also, sets 'subsumed' argument to true if the inequality is 174 * subsumed by an existing inequality. 175 */ 176 const FreeConst& updateSubsumptionDB(const Expr& ineq, bool varOnRHS, 177 bool& subsumed); 178 //! Check if the kids of e are fully simplified and canonized (for debugging) 179 bool kidsCanonical(const Expr& e); 180 181 //! Canonize the expression e, assuming, all children are canonical 182 Theorem canon(const Expr& e); 183 184 /*! @brief Canonize and reduce e w.r.t. union-find database; assume 185 * all children are canonical */ 186 Theorem canonSimplify(const Expr& e); 187 188 /*! @brief Composition of canonSimplify(const Expr&) by 189 * transitivity: take e0 = e1, canonize and simplify e1 to e2, 190 * return e0 = e2. */ canonSimplify(const Theorem & thm)191 Theorem canonSimplify(const Theorem& thm) { 192 return transitivityRule(thm, canonSimplify(thm.getRHS())); 193 } 194 195 //! Canonize predicate (x = y, x < y, etc.) 196 Theorem canonPred(const Theorem& thm); 197 198 //! Canonize predicate like canonPred except that the input theorem 199 //! is an equivalent transformation. 200 Theorem canonPredEquiv(const Theorem& thm); 201 202 //! Solve an equation and return an equivalent Theorem in the solved form 203 Theorem doSolve(const Theorem& e); 204 205 //! takes in a conjunction equivalence Thm and canonizes it. 206 Theorem canonConjunctionEquiv(const Theorem& thm); 207 208 //! picks the monomial with the smallest abs(coeff) from the input 209 //integer equation. 210 bool pickIntEqMonomial(const Expr& right, Expr& isolated, bool& nonlin); 211 212 //! processes equalities with 1 or more vars of type REAL 213 Theorem processRealEq(const Theorem& eqn); 214 215 //! processes equalities whose vars are all of type INT 216 Theorem processIntEq(const Theorem& eqn); 217 218 //! One step of INT equality processing (aux. method for processIntEq()) 219 Theorem processSimpleIntEq(const Theorem& eqn); 220 221 //! Process inequalities in the buffer 222 void processBuffer(); 223 224 //! Take an inequality and isolate a variable 225 Theorem isolateVariable(const Theorem& inputThm, bool& e1); 226 227 //! Update the statistics counters for the variable with a coeff. c 228 void updateStats(const Rational& c, const Expr& var); 229 230 //! Update the statistics counters for the monomial 231 void updateStats(const Expr& monomial); 232 233 //! Add an inequality to the input buffer. See also d_buffer 234 bool addToBuffer(const Theorem& thm, bool priority = false); 235 236 /*! @brief Given a canonized term, compute a factor to make all 237 coefficients integer and relatively prime */ 238 Expr computeNormalFactor(const Expr& rhs, bool normalizeConstants); 239 240 //! Normalize an equation (make all coefficients rel. prime integers) 241 Theorem normalize(const Expr& e); 242 243 //! Normalize an equation (make all coefficients rel. prime integers) 244 /*! accepts a rewrite theorem over eqn|ineqn and normalizes it 245 * and returns a theorem to that effect. 246 */ 247 Theorem normalize(const Theorem& thm); 248 249 Expr pickMonomial(const Expr& right); 250 251 void getFactors(const Expr& e, std::set<Expr>& factors); 252 253 public: // ArithTheoremProducer needs these functions, so make them public 254 //! Separate monomial e = c*p1*...*pn into c and 1*p1*...*pn 255 void separateMonomial(const Expr& e, Expr& c, Expr& var); 256 257 //! Check the term t for integrality (return bool) isInteger(const Expr & e)258 bool isInteger(const Expr& e) 259 { return 260 isInt(e.getType()) ? true : 261 (isReal(e.getType()) ? false : !(isIntegerThm(e).isNull())); } 262 263 private: 264 265 bool lessThanVar(const Expr& isolatedVar, const Expr& var2); 266 267 //! Check if the term expression is "stale" 268 bool isStale(const Expr& e); 269 270 //! Check if the inequality is "stale" or subsumed 271 bool isStale(const Ineq& ineq); 272 273 void projectInequalities(const Theorem& theInequality,bool isolatedVarOnRHS); 274 275 void assignVariables(std::vector<Expr>&v); 276 277 void findRationalBound(const Expr& varSide, const Expr& ratSide, 278 const Expr& var, 279 Rational &r); 280 281 bool findBounds(const Expr& e, Rational& lub, Rational& glb); 282 283 Theorem normalizeProjectIneqs(const Theorem& ineqThm1, 284 const Theorem& ineqThm2); 285 286 //! Take a system of equations and turn it into a solved form 287 Theorem solvedForm(const std::vector<Theorem>& solvedEqs); 288 289 /*! @brief Substitute all vars in term 't' according to the 290 * substitution 'subst' and canonize the result. 291 */ 292 Theorem substAndCanonize(const Expr& t, ExprMap<Theorem>& subst); 293 294 /*! @brief Substitute all vars in the RHS of the equation 'eq' of 295 * the form (x = t) according to the substitution 'subst', and 296 * canonize the result. 297 */ 298 Theorem substAndCanonize(const Theorem& eq, ExprMap<Theorem>& subst); 299 300 //! Traverse 'e' and push all the i-leaves into 'vars' vector 301 void collectVars(const Expr& e, std::vector<Expr>& vars, 302 std::set<Expr>& cache); 303 304 /*! @brief Check if alpha <= ax & bx <= beta is a finite interval 305 * for integer var 'x', and assert the corresponding constraint 306 */ 307 void processFiniteInterval(const Theorem& alphaLEax, 308 const Theorem& bxLEbeta); 309 310 //! For an integer var 'x', find and process all constraints A <= ax <= A+c 311 void processFiniteIntervals(const Expr& x); 312 313 //! Recursive setup for isolated inequalities (and other new expressions) 314 void setupRec(const Expr& e); 315 316 public: 317 TheoryArithOld(TheoryCore* core); 318 ~TheoryArithOld(); 319 320 // Trusted method that creates the proof rules class (used in constructor). 321 // Implemented in arith_theorem_producer.cpp 322 ArithProofRules* createProofRulesOld(); 323 324 // Theory interface 325 void addSharedTerm(const Expr& e); 326 void assertFact(const Theorem& e); 327 void refineCounterExample(); 328 void computeModelBasic(const std::vector<Expr>& v); 329 void computeModel(const Expr& e, std::vector<Expr>& vars); 330 void checkSat(bool fullEffort); 331 Theorem rewrite(const Expr& e); 332 void setup(const Expr& e); 333 void update(const Theorem& e, const Expr& d); 334 Theorem solve(const Theorem& e); 335 void checkAssertEqInvariant(const Theorem& e); 336 void checkType(const Expr& e); 337 Cardinality finiteTypeInfo(Expr& e, Unsigned& n, 338 bool enumerate, bool computeSize); 339 void computeType(const Expr& e); 340 Type computeBaseType(const Type& t); 341 void computeModelTerm(const Expr& e, std::vector<Expr>& v); 342 Expr computeTypePred(const Type& t, const Expr& e); 343 Expr computeTCC(const Expr& e); 344 ExprStream& print(ExprStream& os, const Expr& e); 345 Expr parseExprOp(const Expr& e); 346 347 private: 348 349 /** Map from variables to the maximal (by absolute value) of one of it's coefficients */ 350 ExprMap<Rational> maxCoefficientLeft; 351 ExprMap<Rational> maxCoefficientRight; 352 353 /** Map from variables to the fixed value of one of it's coefficients */ 354 ExprMap<Rational> fixedMaxCoefficient; 355 356 /** 357 * Returns the current maximal coefficient of the variable. 358 * 359 * @param var the variable. 360 */ 361 Rational currentMaxCoefficient(Expr var); 362 363 /** 364 * Fixes the current max coefficient to be used in the ordering. If the maximal coefficient 365 * changes in the future, it will not be used in the ordering. 366 * 367 * @param variable the variable 368 * @param max the value to set it to 369 */ 370 void fixCurrentMaxCoefficient(Expr variable, Rational max); 371 372 /** 373 * Among given input variables, select the smallest ones with respect to the coefficients. 374 */ 375 void selectSmallestByCoefficient(const std::vector<Expr>& input, std::vector<Expr>& output); 376 377 /** 378 * Given an inequality theorem check if it is on integers and get rid of the non-integer 379 * constants. 380 */ 381 Theorem rafineInequalityToInteger(const Theorem& thm); 382 383 /** 384 * Given an equality theorem check if it is on integers with a non-integer constant. If 385 * yes, return a theorem 0 = 1 386 */ 387 Theorem checkIntegerEquality(const Theorem& thm); 388 389 /** Keep the expressions that are already in the buffer */ 390 CDMap<Expr, Theorem> bufferedInequalities; 391 392 /** Strict lower bounds on terms, so that we don't add inequalities to the buffer */ 393 CDMap<Expr, Rational> termLowerBound; 394 CDMap<Expr, Theorem> termLowerBoundThm; 395 /** Strict upper bounds on terms, so that we don't add inequalities to the buffer */ 396 CDMap<Expr, Rational> termUpperBound; 397 CDMap<Expr, Theorem> termUpperBoundThm; 398 399 /** 400 * Which inequalities have already been projected (on which monomial). 401 * - if we get an update of an inequality that's not been projected, we don't care 402 * it will get projected (it's find) 403 * - when projecting, project the finds, not the originals 404 * - when done projecting add here, both original and the find 405 */ 406 CDMap<Expr, Expr> alreadyProjected; 407 408 /** 409 * Sometimes we know an inequality is in the buffer (as a find of something) and 410 * we don't want it in the buffer, but we do want to pre-process it, so we put it 411 * here. 412 */ 413 CDMap<Expr, bool> dontBuffer; 414 415 /** 416 * Are we doing only difference logic? 417 */ 418 CDO<bool> diffLogicOnly; 419 420 /** 421 * Takes an inequality theorem and substitutes the rhs for it's find. It also get's normalized. 422 */ 423 Theorem inequalityToFind(const Theorem& inequalityThm, bool normalizeRHS); 424 425 // x -y <= c 426 struct GraphEdge { 427 Expr x; 428 Expr y; 429 Rational c; 430 }; 431 432 /** 433 * Take inequality of the form 0 op t and extract the c1, t1, c2 and t2, such that 434 * c1 <= t1 and t2 <= c2, where c1 and c2 are constants, and t1 and t2 are either 435 * sums of monomials or a monomial. 436 * 437 * @return the number of variables in terms t1 and t2 438 */ 439 int extractTermsFromInequality(const Expr& inequality, 440 Rational& c1, Expr& t1, 441 Rational& c2, Expr& t2); 442 443 void registerAtom(const Expr& e); 444 445 typedef ExprMap< std::set< std::pair<Rational, Expr> > > AtomsMap; 446 447 /** Map from terms to their lower bound (and the original formula expression) */ 448 AtomsMap formulaAtomLowerBound; 449 450 /** Map from terms to their upper bound (and the original formula expression) */ 451 AtomsMap formulaAtomUpperBound; 452 453 /** Map of all the atoms in the formula */ 454 ExprMap<bool> formulaAtoms; 455 456 class DifferenceLogicGraph { 457 458 public: 459 460 /** 461 * EpsRational class ecapsulates the rationals with a symbolic small \f$\epsilon\f$ added. Each rational 462 * number is presented as a pair \f$(q, k) = q + k\epsilon\f$, where \f$\epsilon\f$ is treated symbolically. 463 * The operations on the new rationals are defined as 464 * <ul> 465 * <li>\f$(q_1, k_1) + (q_2, k_2) \equiv (q_1 + q_2, k_1 + k_2)\f$ 466 * <li>\f$a \times (q, k) \equiv (a \times q, a \times k)\f$ 467 * <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$ 468 * </ul> 469 * 470 * Note that the operations on the infinite values are not defined, as they are never used currently. Infinities can 471 * only be asigned or compared. 472 */ 473 class EpsRational { 474 475 protected: 476 477 /** Type of rationals, normal and the two infinities */ 478 typedef enum { FINITE, PLUS_INFINITY, MINUS_INFINITY } RationalType; 479 480 /** The type of this rational */ 481 RationalType type; 482 483 /** The rational part */ 484 Rational q; 485 486 /** The epsilon multiplier */ 487 Rational k; 488 489 /** 490 * Private constructor to construt infinities. 491 */ EpsRational(RationalType type)492 EpsRational(RationalType type) : type(type) {} 493 494 public: 495 496 /** 497 * Returns if the numbe is finite. 498 */ isFinite()499 inline bool isFinite() const { return type == FINITE; } 500 501 /** 502 * Returns if the number is a plain rational. 503 * 504 * @return true if rational, false otherwise 505 */ isRational()506 inline bool isRational() const { return k == 0; } 507 508 /** 509 * Returns if the number is a plain integer. 510 * 511 * @return true if rational, false otherwise 512 */ isInteger()513 inline bool isInteger() const { return k == 0 && q.isInteger(); } 514 515 /** 516 * Returns the floor of the number \f$x = q + k \epsilon\f$ using the following fomula 517 * \f[ 518 * \lfloor \beta(x) \rfloor = 519 * \begin{cases} 520 * \lfloor q \rfloor & \text{ if } q \notin Z\\ 521 * q & \text{ if } q \in Z \text{ and } k \geq 0\\ 522 * q - 1 & \text{ if } q \in Z \text{ and } k < 0 523 * \end{cases} 524 * \f] 525 */ getFloor()526 inline Rational getFloor() const { 527 if (q.isInteger()) { 528 if (k >= 0) return q; 529 else return q - 1; 530 } else 531 // If not an integer, just floor it 532 return floor(q); 533 } 534 535 536 /** 537 * Returns the rational part of the number 538 * 539 * @return the rational 540 */ getRational()541 inline Rational getRational() const { return q; } 542 543 /** 544 * Returns the epsilon part of the number 545 * 546 * @return the epsilon 547 */ getEpsilon()548 inline Rational getEpsilon() const { return k; } 549 550 /** The infinity constant */ 551 static const EpsRational PlusInfinity; 552 /** The negative infinity constant */ 553 static const EpsRational MinusInfinity; 554 /** The zero constant */ 555 static const EpsRational Zero; 556 557 558 /** The blank constructor */ EpsRational()559 EpsRational() : type(FINITE), q(0), k(0) {} 560 561 /** Copy constructor */ EpsRational(const EpsRational & r)562 EpsRational(const EpsRational& r) : type(r.type), q(r.q), k(r.k) {} 563 564 /** 565 * Constructor from a rational, constructs a new pair (q, 0). 566 * 567 * @param q the rational 568 */ EpsRational(const Rational & q)569 EpsRational(const Rational& q) : type(FINITE), q(q), k(0) {} 570 571 /** 572 * Constructor from a rational and a given epsilon multiplier, constructs a 573 * new pair (q, k). 574 * 575 * @param q the rational 576 * @param k the epsilon multiplier 577 */ EpsRational(const Rational & q,const Rational & k)578 EpsRational(const Rational& q, const Rational& k) : type(FINITE), q(q), k(k) {} 579 580 /** 581 * Addition operator for two EpsRational numbers. 582 * 583 * @param r the number to be added 584 * @return the sum as defined in the class 585 */ 586 inline EpsRational operator + (const EpsRational& r) const { 587 DebugAssert(type == FINITE, "EpsRational::operator +, adding to infinite number"); 588 DebugAssert(r.type == FINITE, "EpsRational::operator +, adding an infinite number"); 589 return EpsRational(q + r.q, k + r.k); 590 } 591 592 /** 593 * Addition operator for two EpsRational numbers. 594 * 595 * @param r the number to be added 596 * @return the sum as defined in the class 597 */ 598 inline EpsRational& operator += (const EpsRational& r) { 599 DebugAssert(type == FINITE, "EpsRational::operator +, adding to infinite number"); 600 q = q + r.q; 601 k = k + r.k; 602 return *this; 603 } 604 605 /** 606 * Subtraction operator for two EpsRational numbers. 607 * 608 * @param r the number to be added 609 * @return the sum as defined in the class 610 */ 611 inline EpsRational operator - (const EpsRational& r) const { 612 DebugAssert(type == FINITE, "EpsRational::operator -, subtracting from infinite number"); 613 DebugAssert(r.type == FINITE, "EpsRational::operator -, subtracting an infinite number"); 614 return EpsRational(q - r.q, k - r.k); 615 } 616 617 /** 618 * Unary minus operator 619 */ 620 inline EpsRational operator - () { 621 DebugAssert(type == FINITE, "EpsRational::operator -, subtracting from infinite number"); 622 q = -q; 623 k = -k; 624 return *this; 625 } 626 627 628 /** 629 * Multiplication operator EpsRational number and a rational number. 630 * 631 * @param a the number to be multiplied 632 * @return the product as defined in the class 633 */ 634 inline EpsRational operator * (const Rational& a) const { 635 DebugAssert(type == FINITE, "EpsRational::operator *, multiplying an infinite number"); 636 return EpsRational(a * q, a * k); 637 } 638 639 /** 640 * Division operator EpsRational number and a rational number. 641 * 642 * @param a the number to be multiplied 643 * @return the product as defined in the class 644 */ 645 inline EpsRational operator / (const Rational& a) const { 646 DebugAssert(type == FINITE, "EpsRational::operator *, dividing an infinite number"); 647 return EpsRational(q / a, k / a); 648 } 649 650 /** 651 * Equality comparison operator. 652 */ 653 inline bool operator == (const EpsRational& r) const { return (q == r.q && k == r.k); } 654 655 /** 656 * Less than or equal comparison operator. 657 */ 658 inline bool operator <= (const EpsRational& r) const { 659 switch (r.type) { 660 case FINITE: 661 if (type == FINITE) 662 // Normal comparison 663 return (q < r.q || (q == r.q && k <= r.k)); 664 else 665 // Finite number is bigger only of the negative infinity 666 return type == MINUS_INFINITY; 667 case PLUS_INFINITY: 668 // Everything is less then or equal than +inf 669 return true; 670 case MINUS_INFINITY: 671 // Only -inf is less then or equal than -inf 672 return (type == MINUS_INFINITY); 673 default: 674 // Ohohohohohoooooo, whats up 675 FatalAssert(false, "EpsRational::operator <=, what kind of number is this????"); 676 } 677 return false; 678 } 679 680 /** 681 * Less than comparison operator. 682 */ 683 inline bool operator < (const EpsRational& r) const { return !(r <= *this); } 684 685 /** 686 * Greater than comparison operator. 687 */ 688 inline bool operator > (const EpsRational& r) const { return !(*this <= r); } 689 690 /** 691 * Returns the string representation of the number. 692 * 693 * @return the string representation of the number 694 */ toString()695 std::string toString() const { 696 switch (type) { 697 case FINITE: 698 return "(" + q.toString() + ", " + k.toString() + ")"; 699 case PLUS_INFINITY: 700 return "+inf"; 701 case MINUS_INFINITY: 702 return "-inf"; 703 default: 704 FatalAssert(false, "EpsRational::toString, what kind of number is this????"); 705 } 706 return "hm, what am I?"; 707 } 708 }; 709 710 struct EdgeInfo { 711 /** The length of this edge */ 712 EpsRational length; 713 /** The number of edges in this path */ 714 int path_length_in_edges; 715 /** If this is a summary edge, a vertex in the path */ 716 Expr in_path_vertex; 717 /** If this is an original edge, the theorem that explains it */ 718 Theorem explanation; 719 720 /** Returnes if the edge is well define (i.e. not +infinity) */ isDefinedEdgeInfo721 bool isDefined() const { return path_length_in_edges != 0; } 722 EdgeInfoEdgeInfo723 EdgeInfo(): path_length_in_edges(0) {} 724 }; 725 726 /** 727 * Given two vertices in the graph and an path edge, reconstruct all the theorems and put them 728 * in the output vector 729 */ 730 void getEdgeTheorems(const Expr& x, const Expr& y, const EdgeInfo& edgeInfo, std::vector<Theorem>& outputTheorems); 731 732 /** 733 * Returns the current weight of the edge. 734 */ 735 EpsRational getEdgeWeight(const Expr& x, const Expr& y); 736 737 /** 738 * Returns whether a vertex has incoming edges. 739 */ 740 bool hasIncoming(const Expr& x); 741 742 /** 743 * Returns whether a vertex has outgoing edges. 744 */ 745 bool hasOutgoing(const Expr& x); 746 747 protected: 748 749 /** Threshold on path length to process (ignore bigger than and set incomplete) */ 750 const int* d_pathLenghtThres; 751 752 /** The arithmetic that's using this graph */ 753 TheoryArithOld* arith; 754 755 /** The core theory */ 756 TheoryCore* core; 757 758 /** The arithmetic that is using u us */ 759 ArithProofRules* rules; 760 761 /** The unsat theorem if available */ 762 CDO<Theorem> unsat_theorem; 763 764 /** The biggest epsilon from EpsRational we used in paths */ 765 CDO<Rational> biggestEpsilon; 766 767 /** The smallest rational difference we used in path relaxation */ 768 CDO<Rational> smallestPathDifference; 769 770 /** The graph itself, maps expressions (x-y) to the edge information */ 771 typedef CDMap<Expr, EdgeInfo> Graph; 772 773 /** Graph of <= paths */ 774 Graph leGraph; 775 776 typedef ExprMap<CDList<Expr>*> EdgesList; 777 778 /** List of vertices adjacent backwards to a vertex */ 779 EdgesList incomingEdges; 780 /** List of vertices adjacent forward to a vertex */ 781 EdgesList outgoingEdges; 782 783 /** 784 * Returns the edge (path) info for the given kind 785 * 786 * @param x the starting vertex 787 * @param y the ending vertex 788 * @return the edge information 789 */ 790 Graph::ElementReference getEdge(const Expr& x, const Expr& y); 791 792 /** 793 * Try to update the shortest path from x to z using y. 794 */ 795 bool tryUpdate(const Expr& x, const Expr& y, const Expr& z); 796 797 public: 798 799 void writeGraph(std::ostream& out); 800 801 /** 802 * Fills the vector with all the variables (vertices) in the graph 803 */ 804 void getVariables(std::vector<Expr>& variables); 805 setRules(ArithProofRules * rules)806 void setRules(ArithProofRules* rules) { 807 this->rules = rules; 808 } 809 setArith(TheoryArithOld * arith)810 void setArith(TheoryArithOld* arith) { 811 this->arith = arith; 812 } 813 814 /** 815 * Class constructor. 816 */ 817 DifferenceLogicGraph(TheoryArithOld* arith, TheoryCore* core, ArithProofRules* rules, Context* context); 818 819 /** 820 * Destructor 821 */ 822 ~DifferenceLogicGraph(); 823 824 /** 825 * Returns the reference to the unsat theorem if there is a negative 826 * cycle in the graph. 827 * 828 * @return the unsat theorem 829 */ 830 831 Theorem getUnsatTheorem(); 832 833 /** 834 * Returns true if there is a negative cycle in the graph. 835 */ 836 bool isUnsat(); 837 838 void computeModel(); 839 840 Rational getValuation(const Expr& x); 841 842 843 /** 844 * Adds an edge corresponding to the constraint x - y <= c. 845 * 846 * @param x variable x::Difference 847 * @param y variable y 848 * @param c rational c 849 * @param edge_thm the theorem for this edge 850 */ 851 void addEdge(const Expr& x, const Expr& y, const Rational& c, const Theorem& edge_thm); 852 853 /** 854 * Check if there is an edge from x to y 855 */ 856 bool existsEdge(const Expr& x, const Expr& y); 857 858 /** 859 * Check if x is in a cycle 860 */ 861 bool inCycle(const Expr& x); 862 863 /** 864 * Given a shared integer term expand it into the gray shadow on the bounds (if bounded from both sides). 865 */ 866 void expandSharedTerm(const Expr& x); 867 868 protected: 869 870 /** Whether the variable is in a cycle */ 871 CDMap<Expr, bool> varInCycle; 872 873 Expr sourceVertex; 874 875 /** 876 * Produced the unsat theorem from a cycle x --> x of negative length 877 * 878 * @param x the variable to use for the conflict 879 * @param kind the kind of edges to consider 880 */ 881 void analyseConflict(const Expr& x, int kind); 882 }; 883 884 /** The graph for difference logic */ 885 DifferenceLogicGraph diffLogicGraph; 886 887 Expr zero; 888 889 /** Index for expanding on shared term equalities */ 890 CDO<unsigned> shared_index_1; 891 /** Index for expanding on shared term equalities */ 892 CDO<unsigned> shared_index_2; 893 894 std::vector<Theorem> multiplicativeSignSplits; 895 896 int termDegree(const Expr& e); 897 898 bool canPickEqMonomial(const Expr& right); 899 900 private: 901 902 // Keeps all expressions that are bounded for disequality splitting and shared term comparisons 903 CDMap<Expr, DifferenceLogicGraph::EpsRational> termUpperBounded; 904 CDMap<Expr, DifferenceLogicGraph::EpsRational> termLowerBounded; 905 906 CDMap<Expr, bool> d_varConstrainedPlus; 907 CDMap<Expr, bool> d_varConstrainedMinus; 908 909 // Keeps all expressions that are constrained 910 CDMap<Expr, bool> termConstrainedBelow; 911 CDMap<Expr, bool> termConstrainedAbove; 912 913 enum BoundsQueryType { 914 /** Query the bounds/constrained using cache for leaves */ 915 QueryWithCacheLeaves, 916 /** Query the bounds/constrained using cashe for leaves, but also see if the value is constrained */ 917 QueryWithCacheLeavesAndConstrainedComputation, 918 /** Query the bounds/constrained by only querying the cache, don't try to figure it out */ 919 QueryWithCacheAll 920 }; 921 922 /** 923 * Check if the term is bounded. If the term is non-linear, just returns false. 924 */ 925 bool isBounded(const Expr& t, BoundsQueryType queryType = QueryWithCacheLeaves); 926 bool hasLowerBound(const Expr& t, BoundsQueryType queryType = QueryWithCacheLeaves) { return getLowerBound(t, queryType).isFinite(); } 927 bool hasUpperBound(const Expr& t, BoundsQueryType queryType = QueryWithCacheLeaves) { return getUpperBound(t, queryType).isFinite(); } 928 929 bool isConstrained(const Expr& t, bool intOnly = true, BoundsQueryType queryType = QueryWithCacheLeaves); 930 bool isConstrainedAbove(const Expr& t, BoundsQueryType queryType = QueryWithCacheLeaves); 931 bool isConstrainedBelow(const Expr& t, BoundsQueryType queryType = QueryWithCacheLeaves); 932 933 /** 934 * Check if the term is bounded from above. If the term is non-linear, just returns false. 935 */ 936 DifferenceLogicGraph::EpsRational getUpperBound(const Expr& t, BoundsQueryType queryType = QueryWithCacheLeaves); 937 938 /** 939 * Check if the term is bouned from below. If the term is non-linear, just return false. 940 */ 941 DifferenceLogicGraph::EpsRational getLowerBound(const Expr& t, BoundsQueryType queryType = QueryWithCacheLeaves); 942 943 /** 944 * See whether and which terms are bounded. 945 */ 946 int computeTermBounds(); 947 948 public: 949 950 void updateConstrained(const Expr& t); 951 bool isUnconstrained(const Expr& t); 952 953 void tryPropagate(const Expr& x, const Expr& y, const DifferenceLogicGraph::EdgeInfo& x_y_edge, int kind); 954 955 void addMultiplicativeSignSplit(const Theorem& case_split_thm); 956 957 bool addPairToArithOrder(const Expr& smaller, const Expr& bigger); 958 nonlinearSignSplit()959 bool nonlinearSignSplit() const { return *d_splitSign; } 960 961 /** 962 * Check if equation is nonlinear. An equation is nonlinear if there is at least one nonlinear term in the sum 963 * on either side of the equation. 964 */ 965 bool isNonlinearEq(const Expr& e); 966 967 /** 968 * Check if a sum term is nonlinear 969 */ 970 bool isNonlinearSumTerm(const Expr& term); 971 972 /** 973 * Check if the equality is of the form c + power1^n - power2^n = 0; 974 */ 975 bool isPowersEquality(const Expr& nonlinearEq, Expr& power1, Expr& power2); 976 977 /** 978 * Check if the equality is of the form c - x^n = 0 979 */ 980 bool isPowerEquality(const Expr& nonlinearEq, Rational& constant, Expr& power1); 981 982 }; 983 984 } 985 986 #endif 987