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.

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 0f92f976e846e52e12407751c03d6e0dfc70403e..75bc40af78eabd1d216a6b186b5a1554f33e9b58 100644 (file)
--- 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() ){

diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index c1c57795b3540e0019c52033070b3f611b39b84e..6c9e706d496cd8346c231e0f6f8b24cadd7637c7 100644 (file)
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -152,7 +152,20 @@ private:
   TypeToTypeEnumMap d_teMap;
   TypeEnumeratorProperties * d_tep;
 
-  public:
+  /* Note that recursive traversal here is over enumerated expressions
+   * (very low expression depth). */
+  void addSubTerms(TNode n, std::map< TNode, bool >& visited, bool topLevel=true){
+    if( visited.find( n )==visited.end() ){
+      visited[n] = true;
+      if( !topLevel ){
+        add(n.getType(), n);
+      }
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        addSubTerms( n[i], visited, false );
+      }
+    }
+  }
+public:
   TypeSet() : d_tep(NULL) {}
   ~TypeSet() {
     iterator it;
@@ -228,6 +241,11 @@ private:
       n = **te;
     }
     s->insert(n);
+    // add all subterms of n to this set as well
+    // this is necessary for parametric types whose values are constructed from other types 
+    // to ensure that we do not enumerate subterms of other previous enumerated values
+    std::map< TNode, bool > visited;
+    addSubTerms(n, visited);
     ++(*te);
     return n;
   }
@@ -282,6 +300,7 @@ protected:
   bool isAssignable(TNode n);
   void checkTerms(TNode n, TheoryModel* tm, NodeSet& cache);
   void assignConstantRep( TheoryModel* tm, Node eqc, Node const_rep );
+  void addToTypeList( TypeNode tn, std::vector< TypeNode >& type_list, std::map< TypeNode, bool >& visiting );
   /** is v an excluded codatatype value */
   bool isExcludedCdtValue( Node v, std::set<Node>* repSet, std::map< Node, Node >& assertedReps, Node eqc );
   bool isCdtValueMatch( Node v, Node r, Node eqc, Node& eqc_m );

diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index bdbbca706b3bd838ad9d125caff10a1c2e5bf571..adad0da32516b7c7a447fd4b26d2de1e5c79ff06 100644 (file)
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -82,7 +82,8 @@ TESTS =       \
        dt-match-pat-param-2.6.smt2 \
        tuple-no-clash.cvc \
        jsat-2.6.smt2 \
-       acyclicity-sr-ground096.smt2
+       acyclicity-sr-ground096.smt2 \
+       model-subterms-min.smt2
 
 # rec5 -- no longer support subrange types
 FAILING_TESTS = \

diff --git a/test/regress/regress0/datatypes/model-subterms-min.smt2 b/test/regress/regress0/datatypes/model-subterms-min.smt2
new file mode 100644 (file)
index 0000000..3866a50
--- /dev/null
+++ b/test/regress/regress0/datatypes/model-subterms-min.smt2
@@ -0,0 +1,18 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatypes ((A 0) (B 0)) (
+((a (sa B)))
+((e1) (e2 (se2 A)))
+))
+
+(declare-const x1 A)
+(declare-const x2 B)
+
+(assert (distinct x1 (a x2)))
+
+(declare-const x3 A)
+
+(assert (distinct x2 (e2 x3)))
+
+(check-sat)
+