More bugfixes for models

3 files changed, 123 insertions, 99 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index b9f027afa..342e67654 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -664,23 +664,40 @@ void TheoryArrays::collectReads(TNode n, set<Node>& readSet, set<Node>& cache)
 }
 
 
+void TheoryArrays::collectArrays(TNode n, set<Node>& arraySet, set<Node>& cache)
+{
+  if (cache.find(n) != cache.end()) {
+    return;
+  }
+  if (n.getType().isArray()) {
+    arraySet.insert(n);
+  }
+  for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) {
+    collectArrays(*child_it, arraySet, cache);
+  }
+  cache.insert(n);
+}
+
+
 void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ){
   m->assertEqualityEngine( &d_equalityEngine );
 
   std::map<Node, std::vector<Node> > selects;
 
-  set<Node> readSet;
-  set<Node> cache;
-  // Collect all selects appearing in assertions
+  set<Node> readSet, arraySet;
+  set<Node> readCache, arrayCache;
+  // Collect all arrays and selects appearing in assertions
   context::CDList<Assertion>::const_iterator assert_it = facts_begin(), assert_it_end = facts_end();
   for (; assert_it != assert_it_end; ++assert_it) {
-    collectReads(*assert_it, readSet, cache);
+    collectReads(*assert_it, readSet, readCache);
+    collectArrays(*assert_it, arraySet, arrayCache);
   }
 
-  // Add selects that are shared terms
+  // Add arrays and selects that are shared terms
   context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end();
   for (; shared_it != shared_it_end; ++ shared_it) {
-    collectReads(*shared_it, readSet, cache);
+    collectReads(*shared_it, readSet, readCache);
+    collectArrays(*shared_it, arraySet, arrayCache);
   }
 
   // Add selects that were generated internally
@@ -692,16 +709,15 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ){
   // Go through all equivalence classes and collect relevant arrays and reads
   std::vector<Node> arrays;
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
-  bool isArray, computeRep;
+  bool computeRep;
   while( !eqcs_i.isFinished() ){
     Node eqc = (*eqcs_i);
-    isArray = eqc.getType().isArray();
     computeRep = false;
     eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
     while( !eqc_i.isFinished() ){
       Node n = *eqc_i;
       // If this EC is an array type and it contains something other than STORE nodes, we have to compute a representative explicitly
-      if (isArray && n.getKind() != kind::STORE) {
+      if (!computeRep && n.getKind() != kind::STORE && arraySet.find(n) != arraySet.end()) {
         arrays.push_back(eqc);
         computeRep = true;
       }
@@ -712,11 +728,6 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ){
       }
       ++eqc_i;
     }
-    // If this is an array EC but it only contains STORE nodes, then the value of this EC is derived from the others -
-    // no need to do extra work to compute it
-    if (isArray && !computeRep) {
-      m->assertRepresentative(eqc);
-    }
     ++eqcs_i;
   }
 
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 8358fe6c9..a47c8440e 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -218,8 +218,9 @@ class TheoryArrays : public Theory {
   /////////////////////////////////////////////////////////////////////////////
 
   private:
-  /** Helper function for collectModelInfo */
+  /** Helper functions for collectModelInfo */
   void collectReads(TNode n, std::set<Node>& readSet, std::set<Node>& cache);
+  void collectArrays(TNode n, std::set<Node>& arraySet, std::set<Node>& cache);
   public:
 
   void collectModelInfo( TheoryModel* m, bool fullModel );
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 7853c2d17..a01844f77 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -410,6 +410,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
   // Process all terms in the equality engine, store representatives for each EC
   std::map< Node, Node > assertedReps, constantReps;
   TypeSet typeConstSet, typeRepSet, typeNoRepSet;
+  std::set< TypeNode > allTypes;
   eqcs_i = eq::EqClassesIterator(&tm->d_equalityEngine);
   for ( ; !eqcs_i.isFinished(); ++eqcs_i) {
     // eqc is the equivalence class representative
@@ -452,87 +453,131 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
     }
     else if (!rep.isNull()) {
       assertedReps[eqc] = rep;
-      typeRepSet.add(eqct, eqc);
+      typeRepSet.add(eqct.getBaseType(), eqc);
+      allTypes.insert(eqct);
     }
     else {
       typeNoRepSet.add(eqct, eqc);
+      allTypes.insert(eqct);
     }
   }
 
   // Need to ensure that each EC has a constant representative.
 
-  // Phase 1: For types that do not have asserted reps, assign the unassigned EC's using either evaluation or type enumeration
-  Trace("model-builder") << "Starting phase 1..." << std::endl;
+  Trace("model-builder") << "Processing EC's..." << std::endl;
 
   TypeSet::iterator it;
+  set<TypeNode>::iterator type_it;
   bool changed, unassignedAssignable, assignOne = false;
 
   // Double-fixed-point loop
   // Outer loop handles a special corner case (see code at end of loop for details)
   for (;;) {
 
-    // In this loop, we find a value for this EC using evaluation if possible.  If not, and
-    // the EC contains a single "assignable" expression, then we assign it using type enumeration
-    // If the EC contains both, we wait, hoping to be able to evaluate the evaluable expression later
+    // Inner fixed-point loop: we are trying to learn constant values for every EC.  Each time through this loop, we process all of the
+    // types by type and may learn some new EC values.  EC's in one type may depend on EC's in another type, so we need a fixed-point loop
+    // to ensure that we learn as many EC values as possible
     do {
       changed = false;
       unassignedAssignable = false;
-      d_normalizedCache.clear();
-      for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) {
-        TypeNode t = TypeSet::getType(it);
-        Trace("model-builder") << "  Working on type: " << t << endl;
-        set<Node>& noRepSet = TypeSet::getSet(it);
-        if (noRepSet.empty()) {
-          continue;
-        }
 
+      // Iterate over all types we've seen
+      for (type_it = allTypes.begin(); type_it != allTypes.end(); ++type_it) {
+        TypeNode t = *type_it;
+        TypeNode tb = t.getBaseType();
         set<Node>::iterator i, i2;
-        bool assignable, evaluable;
-
-        for (i = noRepSet.begin(); i != noRepSet.end(); ) {
-          i2 = i;
-          ++i;
-          eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, &tm->d_equalityEngine);
-          assignable = false;
-          evaluable = false;
-          for ( ; !eqc_i.isFinished(); ++eqc_i) {
-            Node n = *eqc_i;
-            if (isAssignable(n)) {
-              assignable = true;
+
+        // 1. First normalize any non-const representative terms for this type
+        set<Node>* repSet = typeRepSet.getSet(tb);
+        bool done = repSet == NULL || repSet->empty();
+        if (!done) {
+          Trace("model-builder") << "  Normalizing base type: " << tb << endl;
+        }
+        while (!done) {
+          done = true;
+          d_normalizedCache.clear();
+          for (i = repSet->begin(); i != repSet->end(); ) {
+            Assert(assertedReps.find(*i) != assertedReps.end());
+            Node rep = assertedReps[*i];
+            Node normalized = normalize(tm, rep, constantReps, false);
+            Trace("model-builder") << "    Normalizing rep (" << rep << "), normalized to (" << normalized << ")" << endl;
+            if (normalized.isConst()) {
+              changed = true;
+              done = false;
+              typeConstSet.add(tb, normalized);
+              constantReps[*i] = normalized;
+              assertedReps.erase(*i);
+              i2 = i;
+              ++i;
+              repSet->erase(i2);
             }
             else {
-              evaluable = true;
-              Node normalized = normalize(tm, n, constantReps, true);
-              if (normalized.isConst()) {
-                typeConstSet.add(t.getBaseType(), normalized);
-                constantReps[*i2] = normalized;
-                Trace("model-builder") << "  Eval: Setting constant rep of " << (*i2) << " to " << normalized << endl;
+              if (normalized != rep) {
+                assertedReps[*i] = normalized;
                 changed = true;
-                noRepSet.erase(i2);
-                break;
+                done = false;
               }
+              ++i;
             }
           }
-          if (assignable) {
-            if ((assignOne || !evaluable) && fullModel) {
-              assignOne = false;
-              Assert(!t.isBoolean() || (*i2).getKind() == kind::APPLY_UF);
-              Node n;
-              if (t.getCardinality().isInfinite()) {
-                n = typeConstSet.nextTypeEnum(t, true);
+        }
+
+        // 2. Now try to evaluate or assign the EC's in this type
+        set<Node>* noRepSet = typeNoRepSet.getSet(t);
+        if (noRepSet != NULL && !noRepSet->empty()) {
+          Trace("model-builder") << "   Eval/assign working on type: " << t << endl;
+          bool assignable, evaluable;
+          d_normalizedCache.clear();
+          for (i = noRepSet->begin(); i != noRepSet->end(); ) {
+            i2 = i;
+            ++i;
+            eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, &tm->d_equalityEngine);
+            assignable = false;
+            evaluable = false;
+            for ( ; !eqc_i.isFinished(); ++eqc_i) {
+              Node n = *eqc_i;
+              if (isAssignable(n)) {
+                assignable = true;
               }
               else {
-                TypeEnumerator te(t);
-                n = *te;
+                evaluable = true;
+                Node normalized = normalize(tm, n, constantReps, true);
+                if (normalized.isConst()) {
+                  typeConstSet.add(t.getBaseType(), normalized);
+                  constantReps[*i2] = normalized;
+                  Trace("model-builder") << "    Eval: Setting constant rep of " << (*i2) << " to " << normalized << endl;
+                  changed = true;
+                  noRepSet->erase(i2);
+                  break;
+                }
               }
-              Assert(!n.isNull());
-              constantReps[*i2] = n;
-              Trace("model-builder") << "  New Const: Setting constant rep of " << (*i2) << " to " << n << endl;
-              changed = true;
-              noRepSet.erase(i2);
             }
-            else {
-              unassignedAssignable = true;
+            if (assignable) {
+              // We are about to make a choice - we have to make sure we have learned everything we can first.  Only make a choice if:
+              // 1. fullModel is true
+              // 2. there are no terms of this type with un-normalized representatives
+              // 3. there are no evaluable terms in this EC
+              // Alternatively, if 2 or 3 don't hold but we are in a special deadlock-breaking mode, go ahead and make one assignment
+              if (fullModel && (((repSet == NULL || repSet->empty()) && !evaluable) || assignOne)) {
+                assignOne = false;
+                Assert(!t.isBoolean() || (*i2).getKind() == kind::APPLY_UF);
+                Node n;
+                if (t.getCardinality().isInfinite()) {
+                  n = typeConstSet.nextTypeEnum(t, true);
+                }
+                else {
+                  TypeEnumerator te(t);
+                  n = *te;
+                }
+                Assert(!n.isNull());
+                constantReps[*i2] = n;
+                Trace("model-builder") << "    Assign: Setting constant rep of " << (*i2) << " to " << n << endl;
+                changed = true;
+                noRepSet->erase(i2);
+              }
+              else {
+                unassignedAssignable = true;
+              }
             }
           }
         }
@@ -549,46 +594,13 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
     assignOne = true;
   }
 
-  // Phase 2: Substitute into asserted reps using constReps.
-  // Iterate until a fixed point is reached.
-  Trace("model-builder") << "Starting phase 2..." << std::endl;
-  do {
-    changed = false;
-    d_normalizedCache.clear();
-    for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it) {
-      set<Node>& repSet = TypeSet::getSet(it);
-      set<Node>::iterator i;
-      for (i = repSet.begin(); i != repSet.end(); ) {
-        Assert(assertedReps.find(*i) != assertedReps.end());
-        Node rep = assertedReps[*i];
-        Node normalized = normalize(tm, rep, constantReps, false);
-        Trace("model-builder") << "  Normalizing rep (" << rep << "), normalized to (" << normalized << ")" << endl;
-        if (normalized.isConst()) {
-          changed = true;
-          constantReps[*i] = normalized;
-          assertedReps.erase(*i);
-          set<Node>::iterator i2 = i;
-          ++i;
-          repSet.erase(i2);
-        }
-        else {
-          if (normalized != rep) {
-            assertedReps[*i] = normalized;
-            changed = true;
-          }
-          ++i;
-        }
-      }
-    }
-  } while (changed);
-
 #ifdef CVC4_ASSERTIONS
   if (fullModel) {
     // Assert that all representatives have been converted to constants
     for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it) {
       set<Node>& repSet = TypeSet::getSet(it);
       if (!repSet.empty()) {
-        Trace("model-builder") << "Non-empty repSet, size = " << repSet.size() << ", first = " << *(repSet.begin()) << endl;
+        Trace("model-builder") << "***Non-empty repSet, size = " << repSet.size() << ", first = " << *(repSet.begin()) << endl;
         Assert(false);
       }
     }