More fixes to model generation, with previously failing testcases

Also refactored some header file includes to reduce compile time

10 files changed, 129 insertions, 78 deletions

diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index ec29a407c..d291e79d6 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -21,7 +21,6 @@
 
 #include "theory/theory.h"
 #include "context/context.h"
-#include "theory/model.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp
index f8e6882a9..17ea7034b 100644
--- a/src/theory/bv/bv_subtheory_eq.cpp
+++ b/src/theory/bv/bv_subtheory_eq.cpp
@@ -18,6 +18,7 @@
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/model.h"
+
 using namespace std;
 using namespace CVC4;
 using namespace CVC4::context;
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index e82a2c75c..a37ed59c8 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -22,6 +22,7 @@
 #include "theory/bv/options.h"
 #include "theory/bv/theory_bv_rewrite_rules_normalization.h"
 #include "theory/model.h"
+
 using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
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
diff --git a/src/theory/model.h b/src/theory/model.h
index d17192281..19415ae7b 100644
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -216,6 +216,11 @@ private:
     return n;
   }
 
+  bool empty()
+  {
+    return d_typeSet.empty();
+  }
+
   iterator begin()
   {
     return d_typeSet.begin();
diff --git a/src/theory/rewriterules/theory_rewriterules.h b/src/theory/rewriterules/theory_rewriterules.h
index 4a27b4559..e7a24bb79 100644
--- a/src/theory/rewriterules/theory_rewriterules.h
+++ b/src/theory/rewriterules/theory_rewriterules.h
@@ -30,7 +30,6 @@
 #include "theory/rewriterules/rr_inst_match.h"
 #include "util/statistics_registry.h"
 #include "theory/rewriterules/theory_rewriterules_preprocess.h"
-#include "theory/model.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index a8e4485e0..ced845a27 100644
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -261,7 +261,3 @@ Node SharedTermsDatabase::explain(TNode literal) const {
   d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
   return mkAnd(assumptions);
 }
-
-void SharedTermsDatabase::collectModelInfo( theory::TheoryModel* m, bool fullModel ){
-  m->assertEqualityEngine( &d_equalityEngine );
-}
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index a1217d5c6..655918986 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -241,10 +241,6 @@ public:
    */
   theory::eq::EqualityEngine* getEqualityEngine() { return &d_equalityEngine; }
 
-  /**
-   * collect model info
-   */
-  void collectModelInfo( theory::TheoryModel* m, bool fullModel );
 protected:
 
   /**
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index c65fb7ed7..67830390c 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -43,7 +43,6 @@
 #include "util/cvc4_assert.h"
 #include "theory/ite_simplifier.h"
 #include "theory/unconstrained_simplifier.h"
-#include "theory/model.h"
 
 namespace CVC4 {
 
@@ -75,6 +74,8 @@ struct NodeTheoryPairHashFunction {
 
 namespace theory {
   class Instantiator;
+  class TheoryModel;
+  class TheoryEngineModelBuilder;
 }/* CVC4::theory namespace */
 
 class DecisionEngine;
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index edeb6b6ec..0ec89af0b 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -19,6 +19,7 @@
 #include "theory/theory_engine.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/uf/options.h"
+#include "theory/model.h"
 
 //#define ONE_SPLIT_REGION
 //#define DISABLE_QUICK_CLIQUE_CHECKS