diff options
author | Tim King <taking@cs.nyu.edu> | 2012-10-19 19:26:31 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-10-19 19:26:31 +0000 |
commit | 15dd90e7101ae199f15d4ed9976428c93e98cee0 (patch) | |
tree | 89623cf093e5ec013a17d0737b0f6be048ee63b0 /src/theory/arith | |
parent | 5796f9398adfab80860f17f4c99f143801689d56 (diff) |
Fix for model building with shared terms for arithmetic.
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index d813c8e61..6613cfaad 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -2079,6 +2079,7 @@ void TheoryArith::collectModelInfo( TheoryModel* m, bool fullModel ){ // Delta lasts at least the duration of the function call const Rational& delta = d_partialModel.getDelta(); + std::hash_set<TNode, TNodeHashFunction> shared = currentlySharedTerms(); // TODO: // This is not very good for user push/pop.... @@ -2087,13 +2088,18 @@ void TheoryArith::collectModelInfo( TheoryModel* m, bool fullModel ){ if(!isSlackVariable(v)){ Node term = d_arithvarNodeMap.asNode(v); - const DeltaRational& mod = d_partialModel.getAssignment(v); - Rational qmodel = mod.substituteDelta(delta); + if(theoryOf(term) == THEORY_ARITH || shared.find(term) != shared.end()){ + const DeltaRational& mod = d_partialModel.getAssignment(v); + Rational qmodel = mod.substituteDelta(delta); - Node qNode = mkRationalNode(qmodel); - Debug("arith::collectModelInfo") << "m->assertEquality(" << term << ", " << qmodel << ", true)" << endl; + Node qNode = mkRationalNode(qmodel); + Debug("arith::collectModelInfo") << "m->assertEquality(" << term << ", " << qmodel << ", true)" << endl; - m->assertEquality(term, qNode, true); + m->assertEquality(term, qNode, true); + }else{ + Debug("arith::collectModelInfo") << "Skipping m->assertEquality(" << term << ", true)" << endl; + + } } } |