From 15dd90e7101ae199f15d4ed9976428c93e98cee0 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Fri, 19 Oct 2012 19:26:31 +0000
Subject: [PATCH] Fix for model building with shared terms for arithmetic.

(this commit was certified error- and warning-free by the test-and-commit script.)
---
 src/theory/arith/theory_arith.cpp | 16 +++++++++++-----
 src/theory/theory.cpp             |  7 +++++++
 src/theory/theory.h               |  9 +++++++++
 3 files changed, 27 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;
+
+      }
     }
   }
 
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index cdad1e19c..43574f6e4 100644
--- 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 a57f7646d..e51b8594e 100644
--- 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(){}
-- 
2.30.2