diff options
author | Tim King <taking@cs.nyu.edu> | 2012-08-14 18:01:02 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-08-14 18:01:02 +0000 |
commit | 87dbe20de92232279cf1d48ebfe7113194985208 (patch) | |
tree | a0b12b544a35c3493af303baec05145634c2baec /src/theory | |
parent | 5a6a08df0838b7fb70275a70ddc942c3ac802081 (diff) |
Implements TheoryArith::collectModelInfo(). The current implementation is quite basic. This may need to be revisited.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 6b7efa1ee..ca2d74cf7 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -1926,7 +1926,35 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) { } void TheoryArith::collectModelInfo( TheoryModel* m ){ + Assert(d_qflraStatus == Result::SAT); + Debug("arith::collectModelInfo") << "collectModelInfo() begin " << endl; + + // Delta lasts at least the duration of the function call + const Rational& delta = d_partialModel.getDelta(); + + // TODO: + // This is not very good for user push/pop.... + // Revisit when implementing push/pop + for(ArithVar v = 0; v < d_variables.size(); ++v){ + if(!isSlackVariable(v)){ + Node term = d_arithvarNodeMap.asNode(v); + + 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; + + m->assertEquality(term, qNode, true); + } + } + + // Iterate over equivalence classes in LinearEqualityModule + // const eq::EqualityEngine& ee = d_congruenceManager.getEqualityEngine(); + // m->assertEqualityEngine(&ee); + + Debug("arith::collectModelInfo") << "collectModelInfo() end " << endl; } bool TheoryArith::safeToReset() const { |