diff options
Diffstat (limited to 'src/theory/arith/constraint.h')
-rw-r--r-- | src/theory/arith/constraint.h | 28 |
1 files changed, 20 insertions, 8 deletions
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index dcc3bf8bb..be4197a26 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -273,7 +273,12 @@ private: * Sat Context Dependent. * This is initially AssertionOrderSentinel. */ - AssertionOrder d_assertionOrder; + AssertionOrder _d_assertionOrder; + /** + * This is guarenteed to be on the fact queue. + * For example if x + y = x + 1 is on the fact queue, then use this + */ + TNode d_witness; /** * This points at the proof for the constraint in the current context. @@ -347,7 +352,8 @@ private: inline void operator()(Constraint* p){ Constraint constraint = *p; Assert(constraint->assertedToTheTheory()); - constraint->d_assertionOrder = AssertionOrderSentinel; + constraint->_d_assertionOrder = AssertionOrderSentinel; + constraint->d_witness = TNode::null(); Assert(!constraint->assertedToTheTheory()); } }; @@ -439,15 +445,20 @@ public: } bool assertedToTheTheory() const { - return d_assertionOrder < AssertionOrderSentinel; + Assert((_d_assertionOrder < AssertionOrderSentinel) != d_witness.isNull()); + return _d_assertionOrder < AssertionOrderSentinel; + } + TNode getWitness() const { + Assert(assertedToTheTheory()); + return d_witness; } bool assertedBefore(AssertionOrder time) const { - return d_assertionOrder < time; + return _d_assertionOrder < time; } - void setAssertedToTheTheory(); + void setAssertedToTheTheory(TNode witness); bool hasLiteral() const { @@ -518,7 +529,7 @@ public: Node explainForPropagation() const { Assert(hasProof()); Assert(!isSelfExplaining()); - return explainBefore(d_assertionOrder); + return explainBefore(_d_assertionOrder); } private: @@ -733,9 +744,10 @@ private: d_watches->d_canBePropagatedWatches.push_back(c); } - void pushAssertionOrderWatch(Constraint c){ + void pushAssertionOrderWatch(Constraint c, TNode witness){ Assert(!c->assertedToTheTheory()); - c->d_assertionOrder = d_watches->d_assertionOrderWatches.size(); + c->_d_assertionOrder = d_watches->d_assertionOrderWatches.size(); + c->d_witness = witness; d_watches->d_assertionOrderWatches.push_back(c); } |