Minor fixes to model construction to take singleton equivalence classes into account (fixes sets+dt model bug). Minor fix for mixed int/real quantifier instantiation.

1 files changed, 15 insertions, 7 deletions

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index cccd5c350..3cdaeb106 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -375,6 +375,11 @@ void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set<Node>*
       } else {
         if (first) {
           rep = (*eqc_i);
+          //add the term (this is specifically for the case of singleton equivalence classes)
+          if( !rep.getType().isRegExp() ){
+            d_equalityEngine->addTerm( rep );
+            Trace("model-builder-debug") << "Add term to ee within assertEqualityEngine: " << rep << std::endl;
+          }
           first = false;
         }
         else {
@@ -674,7 +679,8 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
     // Assign representative for this EC
     if (!const_rep.isNull()) {
       // Theories should not specify a rep if there is already a constant in the EC
-      Assert(rep.isNull() || rep == const_rep);
+      //AJR: I believe this assertion is too strict, eqc with asserted reps may merge with constant eqc
+      //Assert(rep.isNull() || rep == const_rep);
       assignConstantRep( tm, constantReps, eqc, const_rep, fullModel );
       typeConstSet.add(eqct.getBaseType(), const_rep);
     }
@@ -812,14 +818,16 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
       
       //get properties of this type
       bool isCorecursive = false;
-      bool isUSortFiniteRestricted = false;
       if( t.isDatatype() ){
         const Datatype& dt = ((DatatypeType)(t).toType()).getDatatype();
         isCorecursive = dt.isCodatatype() && ( !dt.isFinite() || dt.isRecursiveSingleton() );
       }
+#ifdef CVC4_ASSERTIONS
+      bool isUSortFiniteRestricted = false;
       if( options::finiteModelFind() ){
         isUSortFiniteRestricted = !t.isSort() && involvesUSort( t );
       }
+#endif
       
       set<Node>* repSet = typeRepSet.getSet(t);
       TypeNode tb = t.getBaseType();
@@ -864,8 +872,8 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
               Assert( !n.isNull() );
               success = true;
               Trace("model-builder-debug") << "Check if excluded : " << n << std::endl;
-              if( isUSortFiniteRestricted ){
 #ifdef CVC4_ASSERTIONS
+              if( isUSortFiniteRestricted ){
                 //must not involve uninterpreted constants beyond cardinality bound (which assumed to coincide with #eqc)
                 //this is just an assertion now, since TypeEnumeratorProperties should ensure that only legal values are enumerated wrt this constraint.
                 std::map< Node, bool > visited;
@@ -874,8 +882,8 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
                   Trace("model-builder") << "Excluded value for " << t << " : " << n << " due to out of range uninterpreted constant." << std::endl;
                 }
                 Assert( success );
-#endif
               }
+#endif
               if( success && isCorecursive ){
                 if (repSet != NULL && !repSet->empty()) {
                   // in the case of codatatypes, check if it is in the set of values that we cannot assign
@@ -960,9 +968,9 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
   //modelBuilder-specific initialization
   processBuildModel( tm, fullModel );
 
-  // Collect model comments from the theories
+  // Do post-processing of model from the theories (used for THEORY_SEP to construct heap model)
   if( fullModel ){
-    Trace("model-builder") << "TheoryEngineModelBuilder: Collect model comments..." << std::endl;
+    Trace("model-builder") << "TheoryEngineModelBuilder: Post-process model..." << std::endl;
     d_te->postProcessModel(tm);
   }
   
@@ -1044,7 +1052,7 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node
     retNode = NodeManager::currentNM()->mkNode( r.getKind(), children );
     if (childrenConst) {
       retNode = Rewriter::rewrite(retNode);
-      Assert(retNode.getKind()==kind::APPLY_UF || retNode.getKind()==kind::REGEXP_RANGE || retNode.isConst());
+      Assert(retNode.getKind()==kind::APPLY_UF || retNode.getType().isRegExp() || retNode.isConst());
     }
   }
   d_normalizedCache[r] = retNode;