GCC Code Coverage Report
 Directory: . Exec Total Coverage File: src/theory/arith/constraint.h Lines: 114 120 95.0 % Date: 2021-03-22 Branches: 42 238 17.6 %

 Line Exec Source 1 /********************* */ 2 /*! \file constraint.h 3  ** \verbatim 4  ** Top contributors (to current version): 5  ** Tim King, Alex Ozdemir, Haniel Barbosa 6  ** This file is part of the CVC4 project. 7  ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS 8  ** in the top-level source directory and their institutional affiliations. 9  ** All rights reserved. See the file COPYING in the top-level source 10  ** directory for licensing information.\endverbatim 11  ** 12  ** \brief Defines Constraint and ConstraintDatabase which is the internal 13  ** representation of variables in arithmetic 14  ** 15  ** This file defines Constraint and ConstraintDatabase. 16  ** A Constraint is the internal representation of literals in TheoryArithmetic. 17  ** Constraints are fundamentally a triple: 18  ** - ArithVar associated with the constraint, 19  ** - a DeltaRational value, 20  ** - and a ConstraintType. 21  ** 22  ** Literals: 23  ** The constraint may also keep track of a node corresponding to the 24  ** Constraint. 25  ** This can be accessed by getLiteral() in O(1) if it has been set. 26  ** This node must be in normal form and may be used for communication with 27  ** the TheoryEngine. 28  ** 29  ** In addition, Constraints keep track of the following: 30  ** - A Constraint that is the negation of the Constraint. 31  ** - An iterator into a set of Constraints for the ArithVar sorted by 32  ** DeltaRational value. 33  ** - A context dependent internal proof of the node that can be used for 34  ** explanations. 35  ** - Whether an equality/disequality has been split in the user context via a 36  ** lemma. 37  ** - Whether a constraint, be be used in explanations sent to the context 38  ** 39  ** Looking up constraints: 40  ** - All of the Constraints with associated nodes in the ConstraintDatabase 41  ** can be accessed via a single hashtable lookup until the Constraint is 42  ** removed. 43  ** - Nodes that have not been associated to a constraints can be 44  ** inserted/associated to existing nodes in O(log n) time. 45  ** 46  ** Implications: 47  ** - A Constraint can be used to find unate implications. 48  ** - A unate implication is an implication based purely on the ArithVar 49  ** matching and the DeltaRational value. 50  ** (implies (<= x c) (<= x d)) given c <= d 51  ** - This is done using the iterator into the sorted set of constraints. 52  ** - Given a tight constraint and previous tightest constraint, this will 53  ** efficiently propagate internally. 54  ** 55  ** Additing and Removing Constraints 56  ** - Adding Constraints takes O(log n) time where n is the number of 57  ** constraints associated with the ArithVar. 58  ** - Removing Constraints takes O(1) time. 59  ** 60  ** Internals: 61  ** - Constraints are pointers to ConstraintValues. 62  ** - Undefined Constraints are NullConstraint. 63  ** 64  ** Assumption vs. Assertion: 65  ** - An assertion is anything on the theory d_fact queue. 66  ** This includes any thing propagated and returned to the fact queue. 67  ** These can be used in external conflicts and propagations of earlier 68  ** proofs. 69  ** - An assumption is anything on the theory d_fact queue that has no further 70  ** explanation i.e. this theory did not propagate it. 71  ** - To set something an assumption, first set it as being as assertion. 72  ** - Internal assumptions have no explanations and must be regressed out of the 73  ** proof. 74  **/ 75 76 #include "cvc4_private.h" 77 78 #ifndef CVC4__THEORY__ARITH__CONSTRAINT_H 79 #define CVC4__THEORY__ARITH__CONSTRAINT_H 80 81 #include  82 #include  83 84 #include "base/configuration_private.h" 85 #include "context/cdlist.h" 86 #include "context/cdqueue.h" 87 #include "expr/node.h" 88 #include "theory/arith/arithvar.h" 89 #include "theory/arith/callbacks.h" 90 #include "theory/arith/constraint_forward.h" 91 #include "theory/arith/delta_rational.h" 92 #include "theory/arith/proof_macros.h" 93 #include "theory/trust_node.h" 94 #include "util/statistics_registry.h" 95 96 namespace CVC4 { 97 98 class ProofNodeManager; 99 100 namespace context { 101 class Context; 102 } 103 namespace theory { 104 105 class EagerProofGenerator; 106 107 namespace arith { 108 109 class Comparison; 110 class ArithCongruenceManager; 111 class ArithVariables; 112 113 /** 114  * Logs the types of different proofs. 115  * Current, proof types: 116  * - NoAP : This constraint is not known to be true. 117  * - AssumeAP : This is an input assertion. There is no proof. 118  * : Something can be both asserted and have a proof. 119  * - InternalAssumeAP : An internal assumption. This has no guarantee of having an external proof. 120  * : This must be removed by regression. 121  * - FarkasAP : A proof with Farka's coefficients, i.e. 122  * : \sum lambda_i ( asNode(x_i) <= c_i ) |= 0 < 0 123  * : If proofs are on, coefficients will be logged. 124  * : If proofs are off, coefficients will not be logged. 125  * : A unate implication is a FarkasAP. 126  * - TrichotomyAP : This is any entailment using (x<= a and x >=a) => x = a 127  * : Equivalently, (x > a or x < a or x = a) 128  * : There are 3 candidate ways this can propagate: 129  * : !(x > a) and !(x = a) => x < a 130  * : !(x < a) and !(x = a) => x > a 131  * : !(x > a) and !(x < a) => x = a 132  * - EqualityEngineAP : This is propagated by the equality engine. 133  * : Consult this for the proof. 134  * - IntTightenAP : This is indicates that a bound involving integers was tightened. 135  * : e.g. i < 5.5 became i <= 5, when i is an integer. 136  * - IntHoleAP : This is currently a catch-all for all integer specific reason. 137  */ 138 enum ArithProofType 139  { NoAP, 140  AssumeAP, 141  InternalAssumeAP, 142  FarkasAP, 143  TrichotomyAP, 144  EqualityEngineAP, 145  IntTightenAP, 146  IntHoleAP}; 147 148 /** 149  * The types of constraints. 150  * The convex constraints are the constraints are LowerBound, Equality, 151  * and UpperBound. 152  */ 153 enum ConstraintType {LowerBound, Equality, UpperBound, Disequality}; 154 155 156 typedef context::CDList CDConstraintList; 157 158 typedef std::unordered_map NodetoConstraintMap; 159 160 typedef size_t ConstraintRuleID; 161 static const ConstraintRuleID ConstraintRuleIdSentinel = std::numeric_limits::max(); 162 163 typedef size_t AntecedentId; 164 static const AntecedentId AntecedentIdSentinel = std::numeric_limits::max(); 165 166 167 typedef size_t AssertionOrder; 168 static const AssertionOrder AssertionOrderSentinel = std::numeric_limits::max(); 169 170 171 /** 172  * A ValueCollection binds together convex constraints that have the same 173  * DeltaRational value. 174  */ 175 class ValueCollection { 176 private: 177 178  ConstraintP d_lowerBound; 179  ConstraintP d_upperBound; 180  ConstraintP d_equality; 181  ConstraintP d_disequality; 182 183 public: 184  ValueCollection(); 185 186  static ValueCollection mkFromConstraint(ConstraintP c); 187 188  bool hasLowerBound() const; 189  bool hasUpperBound() const; 190  bool hasEquality() const; 191  bool hasDisequality() const; 192 193  bool hasConstraintOfType(ConstraintType t) const; 194 195  ConstraintP getLowerBound() const; 196  ConstraintP getUpperBound() const; 197  ConstraintP getEquality() const; 198  ConstraintP getDisequality() const; 199 200  ConstraintP getConstraintOfType(ConstraintType t) const; 201 202  /** Returns true if any of the constraints are non-null. */ 203  bool empty() const; 204 205  /** 206  * Remove the constraint of the type t from the collection. 207  * Returns true if the ValueCollection is now empty. 208  * If true is returned, d_value is now NULL. 209  */ 210  void remove(ConstraintType t); 211 212  /** 213  * Adds a constraint to the set. 214  * The collection must not have a constraint of that type already. 215  */ 216  void add(ConstraintP c); 217 218  void push_into(std::vector& vec) const; 219 220  ConstraintP nonNull() const; 221 222  ArithVar getVariable() const; 223  const DeltaRational& getValue() const; 224 }; 225 226 /** 227  * A Map of ValueCollections sorted by the associated DeltaRational values. 228  * 229  * Discussion: 230  * While it is more natural to consider this a set, this cannot be a set as in 231  * sets the type of both iterator and const_iterator in sets are 232  * "constant iterators". We require iterators that dereference to 233  * ValueCollection&. 234  * 235  * See: 236  * http://gcc.gnu.org/onlinedocs/libstdc++/ext/lwg-defects.html#103 237  */ 238 typedef std::map SortedConstraintMap; 239 typedef SortedConstraintMap::iterator SortedConstraintMapIterator; 240 typedef SortedConstraintMap::const_iterator SortedConstraintMapConstIterator; 241 242 /** A Pair associating a variables and a Sorted ConstraintSet. */ 243 146368 struct PerVariableDatabase{ 244  ArithVar d_var; 245  SortedConstraintMap d_constraints; 246 247  // x ? c_1, x ? c_2, x ? c_3, ... 248  // where ? is a non-empty subset of {lb, ub, eq} 249  // c_1 < c_2 < c_3 < ... 250 251 146368  PerVariableDatabase(ArithVar v) : d_var(v), d_constraints() {} 252 253  bool empty() const { 254  return d_constraints.empty(); 255  } 256 257  static bool IsEmpty(const PerVariableDatabase& p){ 258  return p.empty(); 259  } 260 }; 261 262 /** 263  * If proofs are on, there is a vector of rationals for farkas coefficients. 264  * This is the owner of the memory for the vector, and calls delete upon 265  * cleanup. 266  * 267  */ 268 struct ConstraintRule { 269  ConstraintP d_constraint; 270  ArithProofType d_proofType; 271  AntecedentId d_antecedentEnd; 272 273  /** 274  * In this comment, we abbreviate ConstraintDatabase::d_antecedents 275  * and d_farkasCoefficients as ans and fc. 276  * 277  * This list is always empty if proofs are not enabled. 278  * 279  * If proofs are enabled, the proof of constraint c at p in ans[p] of length n 280  * is (NullConstraint, ans[p-(n-1)], ... , ans[p-1], ans[p]) 281  * 282  * Farkas' proofs show a contradiction with the negation of c, c_not = 283  * c->getNegation(). 284  * 285  * We treat the position for NullConstraint (p-n) as the position for the 286  * farkas coefficient for so we pretend c_not is ans[p-n]. So this correlation 287  * for the constraints we are going to use: (c_not, ans[p-n+(1)], ... , 288  * ans[p-n+(n-1)], ans[p-n+(n)]) With the coefficients at positions: (fc[0], 289  * fc[1)], ... fc[n]) 290  * 291  * The index of the constraints in the proof are {i | i <= 0 <= n] } (with 292  * c_not being p-n). Partition the indices into L, U, and E, the lower bounds, 293  * the upper bounds and equalities. 294  * 295  * We standardize the proofs to be upper bound oriented following the 296  * convention: A x <= b with the proof witness of the form (lambda) Ax <= 297  * (lambda) b and lambda >= 0. 298  * 299  * To accomplish this cleanly, the fc coefficients must be negative for lower 300  * bounds. The signs of equalities can be either positive or negative. 301  * 302  * Thus the proof corresponds to (with multiplication over inequalities): 303  * \sum_{u in U} fc[u] ans[p-n+u] + \sum_{e in E} fc[e] ans[p-n+e] 304  * + \sum_{l in L} fc[l] ans[p-n+l] 305  * |= 0 < 0 306  * where fc[u] > 0, fc[l] < 0, and fc[e] != 0 (i.e. it can be either +/-). 307  * 308  * There is no requirement that the proof is minimal. 309  * We do however use all of the constraints by requiring non-zero 310  * coefficients. 311  */ 312  RationalVectorCP d_farkasCoefficients; 313  ConstraintRule() 314  : d_constraint(NullConstraint) 315  , d_proofType(NoAP) 316  , d_antecedentEnd(AntecedentIdSentinel) 317  { 318  d_farkasCoefficients = RationalVectorCPSentinel; 319  } 320 321 4959733  ConstraintRule(ConstraintP con, ArithProofType pt) 322 4959733  : d_constraint(con) 323  , d_proofType(pt) 324 4959733  , d_antecedentEnd(AntecedentIdSentinel) 325  { 326 4959733  d_farkasCoefficients = RationalVectorCPSentinel; 327 4959733  } 328 1666894  ConstraintRule(ConstraintP con, ArithProofType pt, AntecedentId antecedentEnd) 329 1666894  : d_constraint(con) 330  , d_proofType(pt) 331 1666894  , d_antecedentEnd(antecedentEnd) 332  { 333 1666894  d_farkasCoefficients = RationalVectorCPSentinel; 334 1666894  } 335 336 2534815  ConstraintRule(ConstraintP con, ArithProofType pt, AntecedentId antecedentEnd, RationalVectorCP coeffs) 337 2534815  : d_constraint(con) 338  , d_proofType(pt) 339 2534815  , d_antecedentEnd(antecedentEnd) 340  { 341 2534815  Assert(ARITH_PROOF_ON() || coeffs == RationalVectorCPSentinel); 342 2534815  d_farkasCoefficients = coeffs; 343 2534815  } 344 345  void print(std::ostream& out) const; 346  void debugPrint() const; 347 }; /* class ConstraintRule */ 348 349 class Constraint { 350 351  friend class ConstraintDatabase; 352 353  public: 354  /** 355  * This begins construction of a minimal constraint. 356  * 357  * This should only be called by ConstraintDatabase. 358  * 359  * Because of circular dependencies a Constraint is not fully valid until 360  * initialize has been called on it. 361  */ 362  Constraint(ArithVar x, ConstraintType t, const DeltaRational& v); 363 364  /** 365  * Destructor for a constraint. 366  * This should only be called if safeToGarbageCollect() is true. 367  */ 368  ~Constraint(); 369 370  static ConstraintType constraintTypeOfComparison(const Comparison& cmp); 371 372 15923334  inline ConstraintType getType() const { 373 15923334  return d_type; 374  } 375 376 23790592  inline ArithVar getVariable() const { 377 23790592  return d_variable; 378  } 379 380 40322014  const DeltaRational& getValue() const { 381 40322014  return d_value; 382  } 383 384 1681814  inline ConstraintP getNegation() const { 385 1681814  return d_negation; 386  } 387 388 7021306  bool isEquality() const{ 389 7021306  return d_type == Equality; 390  } 391 845651  bool isDisequality() const{ 392 845651  return d_type == Disequality; 393  } 394 5001847  bool isLowerBound() const{ 395 5001847  return d_type == LowerBound; 396  } 397 5083837  bool isUpperBound() const{ 398 5083837  return d_type == UpperBound; 399  } 400 1367172  bool isStrictUpperBound() const{ 401 1367172  Assert(isUpperBound()); 402 1367172  return getValue().infinitesimalSgn() < 0; 403  } 404 405 1213586  bool isStrictLowerBound() const{ 406 1213586  Assert(isLowerBound()); 407 1213586  return getValue().infinitesimalSgn() > 0; 408  } 409 410 1633016  bool isSplit() const { 411 1633016  return d_split; 412  } 413 414  /** 415  * Splits the node in the user context. 416  * Returns a lemma that is assumed to be true for the rest of the user context. 417  * Constraint must be an equality or disequality. 418  */ 419  TrustNode split(); 420 421 10509254  bool canBePropagated() const { 422 10509254  return d_canBePropagated; 423  } 424  void setCanBePropagated(); 425 426  /** 427  * Light wrapper for calling setCanBePropagated(), 428  * on this and this->d_negation. 429  */ 430 343955  void setPreregistered(){ 431 343955  setCanBePropagated(); 432 343955  d_negation->setCanBePropagated(); 433 343955  } 434 435 56790559  bool assertedToTheTheory() const { 436 56790559  Assert((d_assertionOrder < AssertionOrderSentinel) != d_witness.isNull()); 437 56790559  return d_assertionOrder < AssertionOrderSentinel; 438  } 439 5862634  TNode getWitness() const { 440 5862634  Assert(assertedToTheTheory()); 441 5862634  return d_witness; 442  } 443 444 5513967  bool assertedBefore(AssertionOrder time) const { 445 5513967  return d_assertionOrder < time; 446  } 447 448  /** 449  * Sets the witness literal for a node being on the assertion stack. 450  * 451  * If the negation of the node is true, inConflict must be true. 452  * If the negation of the node is false, inConflict must be false. 453  * Hence, negationHasProof() == inConflict. 454  * 455  * This replaces: 456  * void setAssertedToTheTheory(TNode witness); 457  * void setAssertedToTheTheoryWithNegationTrue(TNode witness); 458  */ 459  void setAssertedToTheTheory(TNode witness, bool inConflict); 460 461 13847259  bool hasLiteral() const { 462 13847259  return !d_literal.isNull(); 463  } 464 465  void setLiteral(Node n); 466 467 1503852  Node getLiteral() const { 468 1503852  Assert(hasLiteral()); 469 1503852  return d_literal; 470  } 471 472  /** Gets a literal in the normal form suitable for proofs. 473  * That is, (sum of non-const monomials) >< const. 474  * 475  * This is a sister method to getLiteral, which returns a normal form 476  * literal, suitable for external solving use. 477  */ 478  Node getProofLiteral() const; 479 480  /** 481  * Set the node as having a proof and being an assumption. 482  * The node must be assertedToTheTheory(). 483  * 484  * Precondition: negationHasProof() == inConflict. 485  * 486  * Replaces: 487  * selfExplaining(). 488  * selfExplainingWithNegationTrue(). 489  */ 490  void setAssumption(bool inConflict); 491 492  /** Returns true if the node is an assumption.*/ 493  bool isAssumption() const; 494 495  /** Set the constraint to have an EqualityEngine proof. */ 496  void setEqualityEngineProof(); 497  bool hasEqualityEngineProof() const; 498 499  /** Returns true if the node has a Farkas' proof. */ 500  bool hasFarkasProof() const; 501 502  /** 503  * @brief Returns whether this constraint is provable using a Farkas 504  * proof applied to (possibly tightened) input assertions. 505  * 506  * An example of a constraint that has a simple Farkas proof: 507  * x <= 0 proven from x + y <= 0 and x - y <= 0. 508  * 509  * An example of another constraint that has a simple Farkas proof: 510  * x <= 0 proven from x + y <= 0 and x - y <= 0.5 for integers x, y 511  * (integer bound-tightening is applied first!). 512  * 513  * An example of a constraint that might be proven **without** a simple 514  * Farkas proof: 515  * x < 0 proven from not(x == 0) and not(x > 0). 516  * 517  * This could be proven internally by the arithmetic theory using 518  * TrichotomyAP as the proof type. 519  * 520  */ 521  bool hasSimpleFarkasProof() const; 522  /** 523  * Returns whether this constraint is an assumption or a tightened 524  * assumption. 525  */ 526  bool isPossiblyTightenedAssumption() const; 527 528  /** Returns true if the node has a int bound tightening proof. */ 529  bool hasIntTightenProof() const; 530 531  /** Returns true if the node has a int hole proof. */ 532  bool hasIntHoleProof() const; 533 534  /** Returns true if the node has a trichotomy proof. */ 535  bool hasTrichotomyProof() const; 536 537  void printProofTree(std::ostream & out, size_t depth = 0) const; 538 539  /** 540  * A sets the constraint to be an internal assumption. 541  * 542  * This does not need to have a witness or an associated literal. 543  * This is always itself in the explanation fringe for both conflicts 544  * and propagation. 545  * This cannot be converted back into a Node conflict or explanation. 546  * 547  * This cannot have a proof or be asserted to the theory! 548  * 549  */ 550  void setInternalAssumption(bool inConflict); 551  bool isInternalAssumption() const; 552 553  /** 554  * Returns a explanation of the constraint that is appropriate for conflicts. 555  * 556  * This is not appropriate for propagation! 557  * 558  * This is the minimum fringe of the implication tree s.t. 559  * every constraint is assertedToTheTheory() or hasEqualityEngineProof(). 560  */ 561  TrustNode externalExplainByAssertions() const; 562 563  /** 564  * Writes an explanation of a constraint into the node builder. 565  * Pushes back an explanation that is acceptable to send to the sat solver. 566  * nb is assumed to be an AND. 567  * 568  * This is the minimum fringe of the implication tree s.t. 569  * every constraint is assertedToTheTheory() or hasEqualityEngineProof(). 570  * 571  * This is not appropriate for propagation! 572  * Use explainForPropagation() instead. 573  */ 574 2778061  std::shared_ptr externalExplainByAssertions( 575  NodeBuilder<>& nb) const 576  { 577 2778061  return externalExplain(nb, AssertionOrderSentinel); 578  } 579 580  /* Equivalent to calling externalExplainByAssertions on all constraints in b */ 581  static Node externalExplainByAssertions(const ConstraintCPVec& b); 582  static Node externalExplainByAssertions(ConstraintCP a, ConstraintCP b); 583  static Node externalExplainByAssertions(ConstraintCP a, ConstraintCP b, ConstraintCP c); 584 585  /** 586  * This is the minimum fringe of the implication tree s.t. every constraint is 587  * - assertedToTheTheory(), 588  * - isInternalDecision() or 589  * - hasEqualityEngineProof(). 590  */ 591  static void assertionFringe(ConstraintCPVec& v); 592  static void assertionFringe(ConstraintCPVec& out, const ConstraintCPVec& in); 593 594  /** The fringe of a farkas' proof. */ 595  bool onFringe() const { 596  return assertedToTheTheory() || isInternalAssumption() || hasEqualityEngineProof(); 597  } 598 599  /** 600  * Returns an explanation of a propagation by the ConstraintDatabase. 601  * The constraint must have a proof. 602  * The constraint cannot be an assumption. 603  * 604  * This is the minimum fringe of the implication tree (excluding the 605  * constraint itself) s.t. every constraint is assertedToTheTheory() or 606  * hasEqualityEngineProof(). 607  * 608  * All return conjuncts were asserted before this constraint. 609  * 610  * Requires the given node to rewrite to the canonical literal for this 611  * constraint. 612  * 613  * @params n the literal to prove 614  * n must rewrite to the constraint's canonical literal 615  * 616  * @returns a trust node of the form: 617  * (=> explanation n) 618  */ 619  TrustNode externalExplainForPropagation(TNode n) const; 620 621  /** 622  * Explain the constraint and its negation in terms of assertions. 623  * The constraint must be in conflict. 624  */ 625  TrustNode externalExplainConflict() const; 626 627  /** The constraint is known to be true. */ 628 163134855  inline bool hasProof() const { 629 163134855  return d_crid != ConstraintRuleIdSentinel; 630  } 631 632  /** The negation of the constraint is known to hold. */ 633 52700637  inline bool negationHasProof() const { 634 52700637  return d_negation->hasProof(); 635  } 636 637  /** Neither the contraint has a proof nor the negation has a proof.*/ 638 183980  bool truthIsUnknown() const { 639 183980  return !hasProof() && !negationHasProof(); 640  } 641 642  /** This is a synonym for hasProof(). */ 643 16068157  inline bool isTrue() const { 644 16068157  return hasProof(); 645  } 646 647  /** Both the constraint and its negation are true. */ 648 10557250  inline bool inConflict() const { 649 10557250  return hasProof() && negationHasProof(); 650  } 651 652  /** 653  * Returns the constraint that corresponds to taking 654  * x r ceiling(getValue()) where r is the node's getType(). 655  * Esstentially this is an up branch. 656  */ 657  ConstraintP getCeiling(); 658 659  /** 660  * Returns the constraint that corresponds to taking 661  * x r floor(getValue()) where r is the node's getType(). 662  * Esstentially this is a down branch. 663  */ 664  ConstraintP getFloor(); 665 666  static ConstraintP makeNegation(ArithVar v, ConstraintType t, const DeltaRational& r); 667 668  const ValueCollection& getValueCollection() const; 669 670 671  ConstraintP getStrictlyWeakerUpperBound(bool hasLiteral, bool mustBeAsserted) const; 672  ConstraintP getStrictlyWeakerLowerBound(bool hasLiteral, bool mustBeAsserted) const; 673 674  /** 675  * Marks a the constraint c as being entailed by a. 676  * The Farkas proof 1*(a) + -1 (c) |= 0<0 677  * 678  * After calling impliedByUnate(), the caller should either raise a conflict 679  * or try call tryToPropagate(). 680  */ 681  void impliedByUnate(ConstraintCP a, bool inConflict); 682 683  /** 684  * Marks a the constraint c as being entailed by a. 685  * The reason has to do with integer bound tightening. 686  * 687  * After calling impliedByIntTighten(), the caller should either raise a conflict 688  * or try call tryToPropagate(). 689  */ 690  void impliedByIntTighten(ConstraintCP a, bool inConflict); 691 692  /** 693  * Marks a the constraint c as being entailed by a. 694  * The reason has to do with integer reasoning. 695  * 696  * After calling impliedByIntHole(), the caller should either raise a conflict 697  * or try call tryToPropagate(). 698  */ 699  void impliedByIntHole(ConstraintCP a, bool inConflict); 700 701  /** 702  * Marks a the constraint c as being entailed by a. 703  * The reason has to do with integer reasoning. 704  * 705  * After calling impliedByIntHole(), the caller should either raise a conflict 706  * or try call tryToPropagate(). 707  */ 708  void impliedByIntHole(const ConstraintCPVec& b, bool inConflict); 709 710  /** 711  * This is a lemma of the form: 712  * x < d or x = d or x > d 713  * The current constraint c is one of the above constraints and {a,b} 714  * are the negation of the other two constraints. 715  * 716  * Preconditions: 717  * - negationHasProof() == inConflict. 718  * 719  * After calling impliedByTrichotomy(), the caller should either raise a conflict 720  * or try call tryToPropagate(). 721  */ 722  void impliedByTrichotomy(ConstraintCP a, ConstraintCP b, bool inConflict); 723 724  /** 725  * Marks the node as having a Farkas proof. 726  * 727  * Preconditions: 728  * - coeffs == NULL if proofs are off. 729  * - See the comments for ConstraintRule for the form of coeffs when 730  * proofs are on. 731  * - negationHasProof() == inConflict. 732  * 733  * After calling impliedByFarkas(), the caller should either raise a conflict 734  * or try call tryToPropagate(). 735  */ 736  void impliedByFarkas(const ConstraintCPVec& b, RationalVectorCP coeffs, bool inConflict); 737 738  /** 739  * Generates an implication node, B => getLiteral(), 740  * where B is the result of externalExplainByAssertions(b). 741  * Does not guarantee b is the explanation of the constraint. 742  */ 743  Node externalImplication(const ConstraintCPVec& b) const; 744 745  /** 746  * Returns true if the variable is assigned the value dr, 747  * the constraint would be satisfied. 748  */ 749  bool satisfiedBy(const DeltaRational& dr) const; 750 751  /** 752  * The node must have a proof already and be eligible for propagation! 753  * You probably want to call tryToPropagate() instead. 754  * 755  * Preconditions: 756  * - hasProof() 757  * - canBePropagated() 758  * - !assertedToTheTheory() 759  */ 760  void propagate(); 761 762  /** 763  * If the constraint 764  * canBePropagated() and 765  * !assertedToTheTheory(), 766  * the constraint is added to the database's propagation queue. 767  * 768  * Precondition: 769  * - hasProof() 770  */ 771  void tryToPropagate(); 772 773  /** 774  * Returns a reference to the containing database. 775  * Precondition: the constraint must be initialized. 776  */ 777  const ConstraintDatabase& getDatabase() const; 778 779  /** Returns the constraint rule at the position. */ 780  const ConstraintRule& getConstraintRule() const; 781 782  private: 783  /** Returns true if the constraint has been initialized. */ 784  bool initialized() const; 785 786  /** 787  * This initializes the fields that cannot be set in the constructor due to 788  * circular dependencies. 789  */ 790  void initialize(ConstraintDatabase* db, 791  SortedConstraintMapIterator v, 792  ConstraintP negation); 793 794  class ConstraintRuleCleanup 795  { 796  public: 797 9161442  inline void operator()(ConstraintRule* crp) 798  { 799 9161442  Assert(crp != NULL); 800 9161442  ConstraintP constraint = crp->d_constraint; 801 9161442  Assert(constraint->d_crid != ConstraintRuleIdSentinel); 802 9161442  constraint->d_crid = ConstraintRuleIdSentinel; 803 9161442  ARITH_PROOF({ 804  if (crp->d_farkasCoefficients != RationalVectorCPSentinel) 805  { 806  delete crp->d_farkasCoefficients; 807  } 808  }); 809 9161442  } 810  }; 811 812  class CanBePropagatedCleanup 813  { 814  public: 815 687910  inline void operator()(ConstraintP* p) 816  { 817 687910  ConstraintP constraint = *p; 818 687910  Assert(constraint->d_canBePropagated); 819 687910  constraint->d_canBePropagated = false; 820 687910  } 821  }; 822 823  class AssertionOrderCleanup 824  { 825  public: 826 5716363  inline void operator()(ConstraintP* p) 827  { 828 5716363  ConstraintP constraint = *p; 829 5716363  Assert(constraint->assertedToTheTheory()); 830 5716363  constraint->d_assertionOrder = AssertionOrderSentinel; 831 5716363  constraint->d_witness = TNode::null(); 832 5716363  Assert(!constraint->assertedToTheTheory()); 833 5716363  } 834  }; 835 836  class SplitCleanup 837  { 838  public: 839 29750  inline void operator()(ConstraintP* p) 840  { 841 29750  ConstraintP constraint = *p; 842 29750  Assert(constraint->d_split); 843 29750  constraint->d_split = false; 844 29750  } 845  }; 846 847  /** 848  * Returns true if the node is safe to garbage collect. 849  * Both it and its negation must have no context dependent data set. 850  */ 851  bool safeToGarbageCollect() const; 852 853  /** 854  * Returns true if the constraint has no context dependent data set. 855  */ 856  bool contextDependentDataIsSet() const; 857 858  /** 859  * Returns true if the node correctly corresponds to the constraint that is 860  * being set. 861  */ 862  bool sanityChecking(Node n) const; 863 864  /** Returns a reference to the map for d_variable. */ 865  SortedConstraintMap& constraintSet() const; 866 867  /** Returns coefficients for the proofs for farkas cancellation. */ 868  static std::pair unateFarkasSigns(ConstraintCP a, ConstraintCP b); 869 870  Node externalExplain(AssertionOrder order) const; 871  /** 872  * Returns an explanation of that was assertedBefore(order). 873  * The constraint must have a proof. 874  * The constraint cannot be selfExplaining(). 875  * 876  * This is the minimum fringe of the implication tree 877  * s.t. every constraint is assertedBefore(order) or hasEqualityEngineProof(). 878  */ 879  std::shared_ptr externalExplain(NodeBuilder<>& nb, 880  AssertionOrder order) const; 881 882  static Node externalExplain(const ConstraintCPVec& b, AssertionOrder order); 883 884 23582675  inline ArithProofType getProofType() const { 885 23582675  return getConstraintRule().d_proofType; 886  } 887 888 601879  inline AntecedentId getEndAntecedent() const { 889 601879  return getConstraintRule().d_antecedentEnd; 890  } 891 892 10841  inline RationalVectorCP getFarkasCoefficients() const 893  { 894 10841  return ARITH_NULLPROOF(getConstraintRule().d_farkasCoefficients); 895  } 896 897  void debugPrint() const; 898 899  /** 900  * The proof of the node is empty. 901  * The proof must be a special proof. Either 902  * isSelfExplaining() or 903  * hasEqualityEngineProof() 904  */ 905  bool antecentListIsEmpty() const; 906 907  bool antecedentListLengthIsOne() const; 908 909  /** Return true if every element in b has a proof. */ 910  static bool allHaveProof(const ConstraintCPVec& b); 911 912  /** Precondition: hasFarkasProof() 913  * Computes the combination implied by the farkas coefficients. Sees if it is 914  * a contradiction. 915  */ 916 917  bool wellFormedFarkasProof() const; 918 919  /** The ArithVar associated with the constraint. */ 920  const ArithVar d_variable; 921 922  /** The type of the Constraint. */ 923  const ConstraintType d_type; 924 925  /** The DeltaRational value with the constraint. */ 926  const DeltaRational d_value; 927 928  /** A pointer to the associated database for the Constraint. */ 929  ConstraintDatabase* d_database; 930 931  /** 932  * The node to be communicated with the TheoryEngine. 933  * 934  * This is not context dependent, but may be set once. 935  * 936  * This must be set if the constraint canBePropagated(). 937  * This must be set if the constraint assertedToTheTheory(). 938  * Otherwise, this may be null(). 939  */ 940  Node d_literal; 941 942  /** Pointer to the negation of the Constraint. */ 943  ConstraintP d_negation; 944 945  /** 946  * This is true if the associated node can be propagated. 947  * 948  * This should be enabled if the node has been preregistered. 949  * 950  * Sat Context Dependent. 951  * This is initially false. 952  */ 953  bool d_canBePropagated; 954 955  /** 956  * This is the order the constraint was asserted to the theory. 957  * If this has been set, the node can be used in conflicts. 958  * If this is c.d_assertedOrder < d.d_assertedOrder, then c can be used in the 959  * explanation of d. 960  * 961  * This should be set after the literal is dequeued by Theory::get(). 962  * 963  * Sat Context Dependent. 964  * This is initially AssertionOrderSentinel. 965  */ 966  AssertionOrder d_assertionOrder; 967 968  /** 969  * This is guaranteed to be on the fact queue. 970  * For example if x + y = x + 1 is on the fact queue, then use this 971  */ 972  TNode d_witness; 973 974  /** 975  * The position of the constraint in the constraint rule id. 976  * 977  * Sat Context Dependent. 978  * This is initially 979  */ 980  ConstraintRuleID d_crid; 981 982  /** 983  * True if the equality has been split. 984  * Only meaningful if ConstraintType == Equality. 985  * 986  * User Context Dependent. 987  * This is initially false. 988  */ 989  bool d_split; 990 991  /** 992  * Position in sorted constraint set for the variable. 993  * Unset if d_type is Disequality. 994  */ 995  SortedConstraintMapIterator d_variablePosition; 996 997 }; /* class ConstraintValue */ 998 999 std::ostream& operator<<(std::ostream& o, const Constraint& c); 1000 std::ostream& operator<<(std::ostream& o, const ConstraintP c); 1001 std::ostream& operator<<(std::ostream& o, const ConstraintCP c); 1002 std::ostream& operator<<(std::ostream& o, const ConstraintType t); 1003 std::ostream& operator<<(std::ostream& o, const ValueCollection& c); 1004 std::ostream& operator<<(std::ostream& o, const ConstraintCPVec& v); 1005 std::ostream& operator<<(std::ostream& o, const ArithProofType); 1006 1007 1008 class ConstraintDatabase { 1009 private: 1010  /** 1011  * The map from ArithVars to their unique databases. 1012  * When the vector changes size, we cannot allow the maps to move so this 1013  * is a vector of pointers. 1014  */ 1015  std::vector d_varDatabases; 1016 1017  SortedConstraintMap& getVariableSCM(ArithVar v) const; 1018 1019  /** Maps literals to constraints.*/ 1020  NodetoConstraintMap d_nodetoConstraintMap; 1021 1022  /** 1023  * A queue of propagated constraints. 1024  * ConstraintCP are pointers. 1025  * The elements of the queue do not require destruction. 1026  */ 1027  context::CDQueue d_toPropagate; 1028 1029  /** 1030  * Proofs are lists of valid constraints terminated by the first null 1031  * sentinel value in the proof list. 1032  * We abbreviate d_antecedents as ans in the comment. 1033  * 1034  * The proof at p in ans[p] of length n is 1035  * (NullConstraint, ans[p-(n-1)], ... , ans[p-1], ans[p]) 1036  * 1037  * The proof at p corresponds to the conjunction: 1038  * (and x_i) 1039  * 1040  * So the proof of a Constraint c corresponds to the horn clause: 1041  * (implies (and x_i) c) 1042  * where (and x_i) is the proof at c.d_crid d_antecedentEnd. 1043  * 1044  * Constraints are pointers so this list is designed not to require any destruction. 1045  */ 1046  CDConstraintList d_antecedents; 1047 1048  typedef context::CDList ConstraintRuleList; 1049  typedef context::CDList CBPList; 1050  typedef context::CDList AOList; 1051  typedef context::CDList SplitList; 1052 1053 1054 1055  /** 1056  * The watch lists are collected together as they need to be garbage collected 1057  * carefully. 1058  */ 1059 8992  struct Watches{ 1060 1061  /** 1062  * Contains the exact list of constraints that have a proof. 1063  * Upon pop, this unsets d_crid to NoAP. 1064  * 1065  * The index in this list is the proper ordering of the proofs. 1066  */ 1067  ConstraintRuleList d_constraintProofs; 1068 1069  /** 1070  * Contains the exact list of constraints that can be used for propagation. 1071  */ 1072  CBPList d_canBePropagatedWatches; 1073 1074  /** 1075  * Contains the exact list of constraints that have been asserted to the theory. 1076  */ 1077  AOList d_assertionOrderWatches; 1078 1079 1080  /** 1081  * Contains the exact list of atoms that have been preregistered. 1082  * This is a pointer as it must be destroyed before the elements of 1083  * d_varDatabases. 1084  */ 1085  SplitList d_splitWatches; 1086  Watches(context::Context* satContext, context::Context* userContext); 1087  }; 1088  Watches* d_watches; 1089 1090  void pushSplitWatch(ConstraintP c); 1091  void pushCanBePropagatedWatch(ConstraintP c); 1092  void pushAssertionOrderWatch(ConstraintP c, TNode witness); 1093 1094  /** Assumes that antecedents have already been pushed. */ 1095  void pushConstraintRule(const ConstraintRule& crp); 1096 1097  /** Returns true if all of the entries of the vector are empty. */ 1098  static bool emptyDatabase(const std::vector& vec); 1099 1100  /** Map from nodes to arithvars. */ 1101  const ArithVariables& d_avariables; 1102 1103 818830  const ArithVariables& getArithVariables() const{ 1104 818830  return d_avariables; 1105  } 1106 1107  ArithCongruenceManager& d_congruenceManager; 1108 1109  const context::Context * const d_satContext; 1110  /** Owned by the TheoryArithPrivate, used here. */ 1111  EagerProofGenerator* d_pfGen; 1112  /** Owned by the TheoryArithPrivate, used here. */ 1113  ProofNodeManager* d_pnm; 1114 1115  RaiseConflict d_raiseConflict; 1116 1117 1118  const Rational d_one; 1119  const Rational d_negOne; 1120 1121  friend class Constraint; 1122 1123  public: 1124  ConstraintDatabase(context::Context* satContext, 1125  context::Context* userContext, 1126  const ArithVariables& variables, 1127  ArithCongruenceManager& dm, 1128  RaiseConflict conflictCallBack, 1129  EagerProofGenerator* pfGen, 1130  ProofNodeManager* pnm); 1131 1132  ~ConstraintDatabase(); 1133 1134  /** Adds a literal to the database. */ 1135  ConstraintP addLiteral(TNode lit); 1136 1137  /** 1138  * If hasLiteral() is true, returns the constraint. 1139  * Otherwise, returns NullConstraint. 1140  */ 1141  ConstraintP lookup(TNode literal) const; 1142 1143  /** 1144  * Returns true if the literal has been added to the database. 1145  * This is a hash table lookup. 1146  * It does not look in the database for an equivalent corresponding constraint. 1147  */ 1148  bool hasLiteral(TNode literal) const; 1149 1150 4470566  bool hasMorePropagations() const{ 1151 4470566  return !d_toPropagate.empty(); 1152  } 1153 1154 723548  ConstraintCP nextPropagation(){ 1155 723548  Assert(hasMorePropagations()); 1156 1157 723548  ConstraintCP p = d_toPropagate.front(); 1158 723548  d_toPropagate.pop(); 1159 1160 723548  return p; 1161  } 1162 1163  void addVariable(ArithVar v); 1164  bool variableDatabaseIsSetup(ArithVar v) const; 1165  void removeVariable(ArithVar v); 1166 1167  /** Get an explanation and proof for this constraint from the equality engine 1168  */ 1169  TrustNode eeExplain(ConstraintCP c) const; 1170  /** Get an explanation for this constraint from the equality engine */ 1171  void eeExplain(ConstraintCP c, NodeBuilder<>& nb) const; 1172 1173  /** 1174  * Returns a constraint with the variable v, the constraint type t, and a value 1175  * dominated by r (explained below) if such a constraint exists in the database. 1176  * If no such constraint exists, NullConstraint is returned. 1177  * 1178  * t must be either UpperBound or LowerBound. 1179  * The returned value v is dominated: 1180  * If t is UpperBound, r <= v 1181  * If t is LowerBound, r >= v 1182  * 1183  * variableDatabaseIsSetup(v) must be true. 1184  */ 1185  ConstraintP getBestImpliedBound(ArithVar v, ConstraintType t, const DeltaRational& r) const; 1186 1187  /** Returns the constraint, if it exists */ 1188  ConstraintP lookupConstraint(ArithVar v, ConstraintType t, const DeltaRational& r) const; 1189 1190  /** 1191  * Returns a constraint with the variable v, the constraint type t and the value r. 1192  * If there is such a constraint in the database already, it is returned. 1193  * If there is no such constraint, this constraint is added to the database. 1194  * 1195  */ 1196  ConstraintP getConstraint(ArithVar v, ConstraintType t, const DeltaRational& r); 1197 1198  /** 1199  * Returns a constraint of the given type for the value and variable 1200  * for the given ValueCollection, vc. 1201  * This is made if there is no such constraint. 1202  */ 1203  ConstraintP ensureConstraint(ValueCollection& vc, ConstraintType t); 1204 1205 1206  void deleteConstraintAndNegation(ConstraintP c); 1207 1208  /** Given constraints a and b such that a OR b by unate reasoning, 1209  * adds a TrustNode to out which proves a OR b as a lemma. 1210  * 1211  * Example: x <= 5 OR 5 <= x. 1212  */ 1213  void proveOr(std::vector& out, 1214  ConstraintP a, 1215  ConstraintP b, 1216  bool negateSecond) const; 1217  /** Given constraints a and b such that a implies b by unate 1218  * reasoning, adds a TrustNode to out which proves -a OR b as a lemma. 1219  * 1220  * Example: x >= 5 -> x >= 4. 1221  */ 1222  void implies(std::vector& out, ConstraintP a, ConstraintP b) const; 1223  /** Given constraints a and b such that not(a AND b) by unate reasoning, 1224  * adds a TrustNode to out which proves -a OR -b as a lemma. 1225  * 1226  * Example: x >= 4 -> x <= 3. 1227  */ 1228  void mutuallyExclusive(std::vector& out, 1229  ConstraintP a, 1230  ConstraintP b) const; 1231 1232  /** 1233  * Outputs a minimal set of unate implications onto the vector for the variable. 1234  * This outputs lemmas of the general forms 1235  * (= p c) implies (<= p d) for c < d, or 1236  * (= p c) implies (not (= p d)) for c != d. 1237  */ 1238  void outputUnateEqualityLemmas(std::vector& lemmas) const; 1239  void outputUnateEqualityLemmas(std::vector& lemmas, 1240  ArithVar v) const; 1241 1242  /** 1243  * Outputs a minimal set of unate implications onto the vector for the variable. 1244  * 1245  * If ineqs is true, this outputs lemmas of the general form 1246  * (<= p c) implies (<= p d) for c < d. 1247  */ 1248  void outputUnateInequalityLemmas(std::vector& lemmas) const; 1249  void outputUnateInequalityLemmas(std::vector& lemmas, 1250  ArithVar v) const; 1251 1252  void unatePropLowerBound(ConstraintP curr, ConstraintP prev); 1253  void unatePropUpperBound(ConstraintP curr, ConstraintP prev); 1254  void unatePropEquality(ConstraintP curr, ConstraintP prevLB, ConstraintP prevUB); 1255 1256  /** AntecendentID must be in range. */ 1257  ConstraintCP getAntecedent(AntecedentId p) const; 1258 1259 7114575  bool isProofEnabled() const { return d_pnm != nullptr; } 1260 1261  private: 1262  /** returns true if cons is now in conflict. */ 1263  bool handleUnateProp(ConstraintP ant, ConstraintP cons); 1264 1265  DenseSet d_reclaimable; 1266 1267  class Statistics { 1268  public: 1269  IntStat d_unatePropagateCalls; 1270  IntStat d_unatePropagateImplications; 1271 1272  Statistics(); 1273  ~Statistics(); 1274  } d_statistics; 1275 1276 }; /* ConstraintDatabase */ 1277 1278 1279 }/* CVC4::theory::arith namespace */ 1280 }/* CVC4::theory namespace */ 1281 }/* CVC4 namespace */ 1282 1283 #endif /* CVC4__THEORY__ARITH__CONSTRAINT_H */

 Generated by: GCOVR (Version 3.2)