More fixes to model generation, with previously failing testcases

Also refactored some header file includes to reduce compile time

1 files changed, 119 insertions, 67 deletions

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 72352f6d3..63772cc1f 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -415,6 +415,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
   std::set< TypeNode > allTypes;
   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;
@@ -470,7 +471,9 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
 
   TypeSet::iterator it;
   set<TypeNode>::iterator type_it;
+  set<Node>::iterator i, i2;
   bool changed, unassignedAssignable, assignOne = false;
+  set<TypeNode> evaluableSet;
 
   // Double-fixed-point loop
   // Outer loop handles a special corner case (see code at end of loop for details)
@@ -482,60 +485,26 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
     do {
       changed = false;
       unassignedAssignable = false;
+      evaluableSet.clear();
 
       // 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;
-
-        // 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 {
-              if (normalized != rep) {
-                assertedReps[*i] = normalized;
-                changed = true;
-                done = false;
-              }
-              ++i;
-            }
-          }
-        }
-
-        // 2. Now try to evaluate or assign the EC's in this type
         set<Node>* noRepSet = typeNoRepSet.getSet(t);
+
+        // 1. Try to evaluate the EC's in this type
         if (noRepSet != NULL && !noRepSet->empty()) {
-          Trace("model-builder") << "   Eval/assign working on type: " << t << endl;
-          bool assignable, evaluable;
+          Trace("model-builder") << "  Eval phase, working on type: " << t << endl;
+          bool assignable, evaluable, evaluated;
           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;
+            evaluated = false;
+            eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, &tm->d_equalityEngine);
             for ( ; !eqc_i.isFinished(); ++eqc_i) {
               Node n = *eqc_i;
               if (isAssignable(n)) {
@@ -545,55 +514,138 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
                 evaluable = true;
                 Node normalized = normalize(tm, n, constantReps, true);
                 if (normalized.isConst()) {
-                  typeConstSet.add(t.getBaseType(), normalized);
+                  typeConstSet.add(tb, normalized);
                   constantReps[*i2] = normalized;
                   Trace("model-builder") << "    Eval: Setting constant rep of " << (*i2) << " to " << normalized << endl;
                   changed = true;
+                  evaluated = true;
                   noRepSet->erase(i2);
                   break;
                 }
               }
             }
-            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);
+            if (!evaluated) {
+              if (evaluable) {
+                evaluableSet.insert(tb);
               }
-              else {
+              if (assignable) {
                 unassignedAssignable = true;
               }
             }
           }
         }
+
+        // 2. Normalize any non-const representative terms for this type
+        set<Node>* repSet = typeRepSet.getSet(t);
+        if (repSet != NULL && !repSet->empty()) {
+          Trace("model-builder") << "  Normalization phase, working on type: " << t << endl;
+          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;
+              typeConstSet.add(t.getBaseType(), normalized);
+              constantReps[*i] = normalized;
+              assertedReps.erase(*i);
+              i2 = i;
+              ++i;
+              repSet->erase(i2);
+            }
+            else {
+              if (normalized != rep) {
+                assertedReps[*i] = normalized;
+                changed = true;
+              }
+              ++i;
+            }
+          }
+        }
       }
     } while (changed);
-    if (!unassignedAssignable || !fullModel) {
+
+    if (!fullModel || !unassignedAssignable) {
       break;
     }
+
+    // 3. Assign unassigned assignable EC's using type enumeration - assign a value *different* from all other EC's if the type is infinite
+    // Assign first value from type enumerator otherwise - for finite types, we rely on polite framework to ensure that EC's that have to be
+    // different are different.
+
+    // Only make assignments on a type if:
+    // 1. fullModel is true
+    // 2. there are no terms that share the same base type with un-normalized representatives
+    // 3. there are no terms that share teh same base type that are unevaluated evaluable terms
+    // Alternatively, if 2 or 3 don't hold but we are in a special deadlock-breaking mode where assignOne is true, go ahead and make one assignment
+    changed = false;
+    for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) {
+      set<Node>& noRepSet = TypeSet::getSet(it);
+      if (noRepSet.empty()) {
+        continue;
+      }
+      TypeNode t = TypeSet::getType(it);
+      TypeNode tb = t.getBaseType();
+      if (!assignOne) {
+        set<Node>* repSet = typeRepSet.getSet(tb);
+        if (repSet != NULL && !repSet->empty()) {
+          continue;
+        }
+        if (evaluableSet.find(tb) != evaluableSet.end()) {
+          continue;
+        }
+      }
+      Trace("model-builder") << "  Assign phase, working on type: " << t << endl;
+      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;
+          }
+          else {
+            evaluable = true;
+          }
+        }
+        if (assignable) {
+          Assert(!evaluable || assignOne);
+          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);
+          if (assignOne) {
+            assignOne = false;
+            break;
+          }
+        }
+      }
+    }
+
     // Corner case - I'm not sure this can even happen - but it's theoretically possible to have a cyclical dependency
     // in EC assignment/evaluation, e.g. EC1 = {a, b + 1}; EC2 = {b, a - 1}.  In this case, neither one will get assigned because we are waiting
     // to be able to evaluate.  But we will never be able to evaluate because the variables that need to be assigned are in
     // these same EC's.  In this case, repeat the whole fixed-point computation with the difference that the first EC
     // that has both assignable and evaluable expressions will get assigned.
-    assignOne = true;
+    if (!changed) {
+      Assert(!assignOne); // check for infinite loop!
+      assignOne = true;
+    }
   }
 
 #ifdef CVC4_ASSERTIONS