Fix model construction for parametric types (#1059)

Fix model construction for parametric types so that we enumerate types in order of dependencies, and avoid subterms of previously enumerated values.

There was a bug in model construction for parametric types which was related to enumerating values that are subterms of other previously enumerated values created during model construction (which were not recorded).

This commit adds all subterms of values we enumerate to the "already used value" sets of their respective types, as reflected in the changes to TypeSet.

There is an extra wrinkle in making the above change, which was caught by the regression test/regress/regress0/fmf/dt-proper-model.smt2. The issue is specific to finite model finding and can be corrected by ensuring that base types (e.g. uninterpreted sorts) are enumerated first.

The change to TheoryModel::buildModel that replaces "allTypes" with "type_list" fixes this wrinkle. This constructs a partially ordered list of types where T1 comes before T2 if values of T2 can contain terms of type T1 but not vice versa. Ordering our enumeration in this way is probably a good idea in general. This ensures we enumerate values for equivalence classes of e.g. Int before (Array Int Int) and means we exclude fewer intermediate values during model construction.

1 files changed, 55 insertions, 9 deletions

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 0f92f976e..75bc40af7 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -581,6 +581,36 @@ bool TheoryEngineModelBuilder::isExcludedUSortValue( std::map< TypeNode, unsigne
   return false;
 }
 
+
+void TheoryEngineModelBuilder::addToTypeList( TypeNode tn, std::vector< TypeNode >& type_list, 
+                                              std::map< TypeNode, bool >& visiting ){
+  if( std::find( type_list.begin(), type_list.end(), tn )==type_list.end() ){
+    if( visiting.find( tn )==visiting.end() ){
+      visiting[tn] = true;
+      /* This must make a recursive call on all types that are subterms of
+       * values of the current type.
+       * Note that recursive traversal here is over enumerated expressions
+       * (very low expression depth). */
+      if( tn.isArray() ){
+        addToTypeList( tn.getArrayIndexType(), type_list, visiting );
+        addToTypeList( tn.getArrayConstituentType(), type_list, visiting );
+      }else if( tn.isSet() ){
+        addToTypeList( tn.getSetElementType(), type_list, visiting );
+      }else if( tn.isDatatype() ){
+        const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+        for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+          for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
+            TypeNode ctn = TypeNode::fromType( dt[i][j].getRangeType() );
+            addToTypeList( ctn, type_list, visiting );
+          }
+        }   
+      }
+      Assert( std::find( type_list.begin(), type_list.end(), tn )==type_list.end() );
+      type_list.push_back( tn );
+    }
+  }
+}
+
 bool TheoryEngineModelBuilder::buildModel(Model* m)
 {
   Trace("model-builder") << "TheoryEngineModelBuilder: buildModel" << std::endl;
@@ -639,7 +669,11 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
     }
     typeConstSet.setTypeEnumeratorProperties( &tep );
   }
-  std::set< TypeNode > allTypes;
+  // AJR: build ordered list of types that ensures that base types are enumerated first.
+  //   (I think) this is only strictly necessary for finite model finding + parametric types 
+  //   instantiated with uninterpreted sorts, but is probably a good idea to do in general
+  //   since it leads to models with smaller term sizes.
+  std::vector< TypeNode > type_list;
   eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
   for ( ; !eqcs_i.isFinished(); ++eqcs_i) {
 
@@ -687,11 +721,13 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
     else if (!rep.isNull()) {
       assertedReps[eqc] = rep;
       typeRepSet.add(eqct.getBaseType(), eqc);
-      allTypes.insert(eqct.getBaseType());
+      std::map< TypeNode, bool > visiting;
+      addToTypeList(eqct.getBaseType(), type_list, visiting);
     }
     else {
       typeNoRepSet.add(eqct, eqc);
-      allTypes.insert(eqct);
+      std::map< TypeNode, bool > visiting;
+      addToTypeList(eqct, type_list, visiting);
     }
   }
 
@@ -700,7 +736,7 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
   Trace("model-builder") << "Processing EC's..." << std::endl;
 
   TypeSet::iterator it;
-  set<TypeNode>::iterator type_it;
+  vector<TypeNode>::iterator type_it;
   set<Node>::iterator i, i2;
   bool changed, unassignedAssignable, assignOne = false;
   set<TypeNode> evaluableSet;
@@ -718,7 +754,7 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
       evaluableSet.clear();
 
       // Iterate over all types we've seen
-      for (type_it = allTypes.begin(); type_it != allTypes.end(); ++type_it) {
+      for (type_it = type_list.begin(); type_it != type_list.end(); ++type_it) {
         TypeNode t = *type_it;
         TypeNode tb = t.getBaseType();
         set<Node>* noRepSet = typeNoRepSet.getSet(t);
@@ -809,13 +845,23 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
     // 2. 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);
+    //must iterate over the ordered type list to ensure that we do not enumerate values with subterms
+    //  having types that we are currently enumerating (when possible)
+    //  for example, this ensures we enumerate uninterpreted sort U before (List of U) and (Array U U)
+    //  however, it does not break cyclic type dependencies for mutually recursive datatypes, but this is handled
+    //  by recording all subterms of enumerated values in TypeSet::addSubTerms.
+    for (type_it = type_list.begin(); type_it != type_list.end(); ++type_it) {
+      TypeNode t = *type_it;
+      // continue if there are no more equivalence classes of this type to assign
+      std::set<Node>* noRepSetPtr = typeNoRepSet.getSet( t );
+      if( noRepSetPtr==NULL ){
+        continue;
+      }
+      set<Node>& noRepSet = *noRepSetPtr;
       if (noRepSet.empty()) {
         continue;
       }
-      TypeNode t = TypeSet::getType(it);
-      
+
       //get properties of this type
       bool isCorecursive = false;
       if( t.isDatatype() ){