Fix for another model assertion failure

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index f66f3f7a43c98bf3ac13a79c46b564bc690a6038..4931a18f0b2f0c6515c63e9c0584c8a40cbe7450 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -707,8 +707,6 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ){
     // For each read, require that the rep stores the right value
     vector<Node>& reads = selects[n];
     for (unsigned j = 0; j < reads.size(); ++j) {
-      m->addTerm(reads[j]);
-      m->addTerm(reads[j][1]);
       rep = nm->mkNode(kind::STORE, rep, reads[j][1], reads[j]);
     }
     m->assertEquality(n, rep, true);

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index b39bea038cb5448b43bfe6b2b472a6e273878b32..d8b09516193e36791f59e84bd97f8e80fb1193fb 100644 (file)
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -208,9 +208,7 @@ void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){
 
 /** add term */
 void TheoryModel::addTerm( Node n ){
-  if( !d_equalityEngine.hasTerm( n ) ){
-    d_equalityEngine.addTerm( n );
-  }
+  Assert(d_equalityEngine.hasTerm(n));
   //must collect UF terms
   if (n.getKind()==APPLY_UF) {
     Node op = n.getOperator();
@@ -364,6 +362,22 @@ bool TheoryEngineModelBuilder::isAssignable(TNode n)
 }
 
 
+void TheoryEngineModelBuilder::checkTerms(TNode n, TheoryModel* tm, NodeSet& cache)
+{
+  NodeSet::iterator it = cache.find(n);
+  if (it != cache.end()) {
+    return;
+  }
+  if (isAssignable(n)) {
+    tm->d_equalityEngine.addTerm(n);
+  }
+  for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) {
+    checkTerms(*child_it, tm, cache);
+  }
+  cache.insert(n);
+}
+
+
 void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
 {
   TheoryModel* tm = (TheoryModel*)m;
@@ -375,13 +389,25 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
   Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..." << std::endl;
   d_te->collectModelInfo(tm, fullModel);
 
+  // Loop through all terms and make sure that assignable sub-terms are in the equality engine
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &tm->d_equalityEngine );
+  {
+    NodeSet cache;
+    for ( ; !eqcs_i.isFinished(); ++eqcs_i) {
+      eq::EqClassIterator eqc_i = eq::EqClassIterator((*eqcs_i), &tm->d_equalityEngine);
+      for ( ; !eqc_i.isFinished(); ++eqc_i) {
+        checkTerms(*eqc_i, tm, cache);
+      }
+    }
+  }
+
   Trace("model-builder") << "Collect representatives..." << std::endl;
+
   // Process all terms in the equality engine, store representatives for each EC
   std::map< Node, Node > assertedReps, constantReps;
   TypeSet typeConstSet, typeRepSet, typeNoRepSet;
-  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &tm->d_equalityEngine );
+  eqcs_i = eq::EqClassesIterator(&tm->d_equalityEngine);
   for ( ; !eqcs_i.isFinished(); ++eqcs_i) {
-
     // eqc is the equivalence class representative
     Node eqc = (*eqcs_i);
     Trace("model-builder") << "Processing EC: " << eqc << endl;

diff --git a/src/theory/model.h b/src/theory/model.h
index 5581ce7776fb42ebe9065f37bcf76541f91b5816..229d1f25ed2e6e1ab6a2a782aa6ba691520635b3 100644 (file)
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -247,12 +247,14 @@ protected:
   TheoryEngine* d_te;
   typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
   NodeMap d_normalizedCache;
+  typedef std::hash_set<Node, NodeHashFunction> NodeSet;
 
   /** process build model */
   virtual void processBuildModel(TheoryModel* m, bool fullModel);
   /** normalize representative */
   Node normalize(TheoryModel* m, TNode r, std::map<Node, Node>& constantReps, bool evalOnly);
   bool isAssignable(TNode n);
+  void checkTerms(TNode n, TheoryModel* tm, NodeSet& cache);
 
 public:
   TheoryEngineModelBuilder(TheoryEngine* te);