Fix for model building with shared terms for arithmetic.

(this commit was certified error- and warning-free by the test-and-commit script.)

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index d813c8e61a2ec7efce2e5e5f725f020bcba86b74..6613cfaad2b803c48b73ad5125d2cd7687f0cf3c 100644 (file)
--- 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;
+
+      }
     }
   }
 

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index cdad1e19ca21a927e17dbceeb7a6a5bc54ca9e8a..43574f6e40bdaf7ef2912b89b371a3509375d8b2 100644 (file)
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -237,6 +237,13 @@ int Instantiator::doInstantiation(Node f, Theory::Effort effort, int e ) {
 //  }
 //}
 
+std::hash_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{
+  std::hash_set<TNode, TNodeHashFunction> currentlyShared;
+  for(shared_terms_iterator i = shared_terms_begin(), i_end = shared_terms_end(); i != i_end; ++i){
+    currentlyShared.insert (*i);
+  }
+  return currentlyShared;
+}
 
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */

diff --git a/src/theory/theory.h b/src/theory/theory.h
index a57f7646d419308403503458fd69ccee5cbac7a3..e51b8594ea1c1327c15bfe1bccfeae2e6cd581de 100644 (file)
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -38,6 +38,7 @@
 #include <iostream>
 
 #include <strings.h>
+#include <ext/hash_set>
 
 namespace CVC4 {
 
@@ -785,6 +786,12 @@ public:
     return d_sharedTerms.end();
   }
 
+
+  /**
+   * This is a utility function for constructing a copy of the currently shared terms
+   * in a queriable form.  As this is 
+   */
+  std::hash_set<TNode, TNodeHashFunction> currentlySharedTerms() const;
 };/* class Theory */
 
 std::ostream& operator<<(std::ostream& os, Theory::Effort level);
@@ -804,6 +811,8 @@ public:
 protected:
   /** reference to the instantiation engine */
   QuantifiersEngine* d_quantEngine;
+
+
 public:
   InstStrategy( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
   virtual ~InstStrategy(){}