diff options
author | Tim King <taking@cs.nyu.edu> | 2012-11-14 22:43:57 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-11-14 22:43:57 +0000 |
commit | aa4b06d4f1db1942d7ad3833e071baa356cefd60 (patch) | |
tree | a05375bd9766663f5e095c91e016464ce16ed413 /src | |
parent | 56013a80a76b0d46f6f8497d7570e51877dbf99d (diff) |
Fix to bug449. Adds shared constants to the set of DeltaRationals that must be in the final total order.
Diffstat (limited to 'src')
-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); |