diff options
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 1d89c02d4..74e0ad296 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -674,6 +674,10 @@ bool TheoryArith::AssertDisequality(Constraint constraint){ void TheoryArith::addSharedTerm(TNode n){ Debug("arith::addSharedTerm") << "addSharedTerm: " << n << endl; + if(n.isConst()){ + d_partialModel.invalidateDelta(); + } + d_congruenceManager.addSharedTerm(n); if(!n.isConst() && !isSetup(n)){ Polynomial poly = Polynomial::parsePolynomial(n); @@ -2102,6 +2106,14 @@ Rational TheoryArith::deltaValueForTotalOrder() const{ relevantDeltaValues.insert(rhsValue); } + for(shared_terms_iterator shared_iter = shared_terms_begin(), + shared_end = shared_terms_end(); shared_iter != shared_end; ++shared_iter){ + Node sharedCurr = *shared_iter; + if(sharedCurr.getKind() == CONST_RATIONAL){ + relevantDeltaValues.insert(sharedCurr.getConst<Rational>());: + } + } + for(ArithVar v = 0; v < d_variables.size(); ++v){ const DeltaRational& value = d_partialModel.getAssignment(v); relevantDeltaValues.insert(value); |