From: Tim King <taking@cs.nyu.edu>
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 {