From d7dadde871ae4775748695b0b7f9deee49576c0a Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 31 Aug 2017 00:59:24 +0200
Subject: 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.
---
 src/theory/theory_model.h | 21 ++++++++++++++++++++-
 1 file changed, 20 insertions(+), 1 deletion(-)

(limited to 'src/theory/theory_model.h')

diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index c1c57795b..6c9e706d4 100644
--- 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 );
-- 
cgit v1.2.3