From: Clark Barrett <barrett@cs.nyu.edu>
Date: Fri, 9 Nov 2012 03:18:00 +0000 (+0000)
Subject: Fix for another model assertion failure
X-Git-Tag: cvc5-1.0.0~7636
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cad60d99f8fe38dd5098d14958d2dd844bbe6584;p=cvc5.git

Fix for another model assertion failure
---

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index f66f3f7a4..4931a18f0 100644
--- 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 b39bea038..d8b095161 100644
--- 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 5581ce777..229d1f25e 100644
--- 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);