From: Tim King Date: Tue, 14 Aug 2012 18:01:02 +0000 (+0000) Subject: Implements TheoryArith::collectModelInfo(). The current implementation is quite... X-Git-Tag: cvc5-1.0.0~7870 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=87dbe20de92232279cf1d48ebfe7113194985208;p=cvc5.git Implements TheoryArith::collectModelInfo(). The current implementation is quite basic. This may need to be revisited. --- 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 {