From 93a162548e1df0102936deae560b873b7f143bf4 Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Thu, 8 Nov 2012 12:22:06 +0000
Subject: [PATCH] Fixed two small bugs in model generation

---
 src/theory/arrays/theory_arrays.cpp |  1 +
 src/theory/model.cpp                | 15 ++++-----------
 src/theory/model.h                  |  5 ++++-
 3 files changed, 9 insertions(+), 12 deletions(-)

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index c0777f79f..f66f3f7a4 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -684,6 +684,7 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ){
     TNode n = arrays[i];
 
     // Compute default value for this array - there is one default value for every mayEqual equivalence class
+    d_mayEqualEqualityEngine.addTerm(n); // add the term in case it isn't there already
     TNode mayRep = d_mayEqualEqualityEngine.getRepresentative(n);
     it = defValues.find(mayRep);
     // If this mayEqual EC doesn't have a default value associated, get the next available default value for the associated array element type
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 2b819d6bd..b39bea038 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -418,7 +418,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
       // Theories should not specify a rep if there is already a constant in the EC
       Assert(rep.isNull() || rep == const_rep);
       constantReps[eqc] = const_rep;
-      typeConstSet.add(eqct, const_rep);
+      typeConstSet.add(eqct.getBaseType(), const_rep);
     }
     else if (!rep.isNull()) {
       assertedReps[eqc] = rep;
@@ -474,16 +474,10 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
               evaluable = true;
               Node normalized = normalize(tm, n, constantReps, true);
               if (normalized.isConst()) {
-                typeConstSet.add(t, normalized);
+                typeConstSet.add(t.getBaseType(), normalized);
                 constantReps[*i2] = normalized;
                 Trace("model-builder") << "  Eval: Setting constant rep of " << (*i2) << " to " << normalized << endl;
                 changed = true;
-                // if (t.isBoolean()) {
-                //   tm->assertPredicate(*i2, normalized == tm->d_true);
-                // }
-                // else {
-                //   tm->assertEquality(*i2, normalized, true);
-                // }
                 noRepSet.erase(i2);
                 break;
               }
@@ -495,7 +489,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
               Assert(!t.isBoolean());
               Node n;
               if (t.getCardinality().isInfinite()) {
-                n = typeConstSet.nextTypeEnum(t);
+                n = typeConstSet.nextTypeEnum(t, true);
               }
               else {
                 TypeEnumerator te(t);
@@ -505,7 +499,6 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
               constantReps[*i2] = n;
               Trace("model-builder") << "  New Const: Setting constant rep of " << (*i2) << " to " << n << endl;
               changed = true;
-              // tm->assertEquality(*i2, n, true);
               noRepSet.erase(i2);
             }
             else {
@@ -521,7 +514,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
     // 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
-    // the same EC's.  In this case, repeat the whole fixed-point computation with the difference that the first EC
+    // 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;
   }
diff --git a/src/theory/model.h b/src/theory/model.h
index acfcb4849..5581ce777 100644
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -174,7 +174,7 @@ private:
     return (*it).second;
   }
 
-  Node nextTypeEnum(TypeNode t)
+  Node nextTypeEnum(TypeNode t, bool useBaseType = false)
   {
     TypeEnumerator* te;
     TypeToTypeEnumMap::iterator it = d_teMap.find(t);
@@ -189,6 +189,9 @@ private:
       return Node();
     }
 
+    if (useBaseType) {
+      t = t.getBaseType();
+    }
     iterator itSet = d_typeSet.find(t);
     std::set<Node>* s;
     if (itSet == d_typeSet.end()) {
-- 
2.30.2