Fix for collectModelInfo related to finite types + preregistration. Generalize previous fix for sets, minor changes to Datatypes.

8 files changed, 109 insertions, 77 deletions

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index b66cb15ff..d285f292a 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -173,7 +173,7 @@ void TheoryDatatypes::check(Effort e) {
         return;
       }
     }while( d_addedFact );
-
+  
     //check for splits
     Trace("datatypes-debug") << "Check for splits " << e << endl;
     do {
@@ -183,6 +183,7 @@ void TheoryDatatypes::check(Effort e) {
       eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
       while( !eqcs_i.isFinished() ){
         Node n = (*eqcs_i);
+        //TODO : avoid irrelevant (pre-registered but not asserted) terms here?
         TypeNode tn = n.getType();
         if( tn.isDatatype() ){
           Trace("datatypes-debug") << "Process equivalence class " << n << std::endl;
@@ -1414,9 +1415,15 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
   Trace("dt-model") << std::endl;
   printModelDebug( "dt-model" );
   Trace("dt-model") << std::endl;
+  
+  set<Node> termSet;
+  
+  // Compute terms appearing in assertions and shared terms, and in inferred equalities
+  getRelevantTerms(termSet);
 
   //combine the equality engine
-  m->assertEqualityEngine( &d_equalityEngine );
+  m->assertEqualityEngine( &d_equalityEngine, &termSet );
+  
 
   //get all constructors
   eq::EqClassesIterator eqccs_i = eq::EqClassesIterator( &d_equalityEngine );
@@ -1426,18 +1433,22 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
   while( !eqccs_i.isFinished() ){
     Node eqc = (*eqccs_i);
     //for all equivalence classes that are datatypes
-    if( eqc.getType().isDatatype() ){
-      EqcInfo* ei = getOrMakeEqcInfo( eqc );
-      if( ei && !ei->d_constructor.get().isNull() ){
-        Node c = ei->d_constructor.get();
-        cons.push_back( c );
-        eqc_cons[ eqc ] = c;
-      }else{
-        //if eqc contains a symbol known to datatypes (a selector), then we must assign
-        //should assign constructors to EQC if they have a selector or a tester
-        bool shouldConsider = ( ei && ei->d_selectors ) || hasTester( eqc );
-        if( shouldConsider ){
-          nodes.push_back( eqc );
+    if( termSet.find( eqc )==termSet.end() ){
+      Trace("dt-cmi-debug") << "Irrelevant eqc : " << eqc << std::endl;
+    }else{
+      if( eqc.getType().isDatatype() ){
+        EqcInfo* ei = getOrMakeEqcInfo( eqc );
+        if( ei && !ei->d_constructor.get().isNull() ){
+          Node c = ei->d_constructor.get();
+          cons.push_back( c );
+          eqc_cons[ eqc ] = c;
+        }else{
+          //if eqc contains a symbol known to datatypes (a selector), then we must assign
+          //should assign constructors to EQC if they have a selector or a tester
+          bool shouldConsider = ( ei && ei->d_selectors ) || hasTester( eqc );
+          if( shouldConsider ){
+            nodes.push_back( eqc );
+          }
         }
       }
     }
@@ -1456,54 +1467,6 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
     const Datatype& dt = ((DatatypeType)tt).getDatatype();
     if( !d_equalityEngine.hasTerm( eqc ) ){
       Assert( false );
-      /*
-      if( !dt.isCodatatype() ){
-        Trace("dt-cmi") << "NOTICE : Datatypes: need to assign constructor for " << eqc << std::endl;
-        Trace("dt-cmi") << "   Type : " << eqc.getType() << std::endl;
-        TypeNode tn = eqc.getType();
-        //if it is infinite, make sure it is fresh
-        //  this ensures that the term that this is an argument of is distinct.
-        if( eqc.getType().getCardinality().isInfinite() ){
-          std::map< TypeNode, int >::iterator it = typ_enum_map.find( tn );
-          int teIndex;
-          if( it==typ_enum_map.end() ){
-            teIndex = (int)typ_enum.size();
-            typ_enum_map[tn] = teIndex;
-            typ_enum.push_back( TypeEnumerator(tn) );
-          }else{
-            teIndex = it->second;
-          }
-          bool success;
-          do{
-            success = true;
-            Assert( !typ_enum[teIndex].isFinished() );
-            neqc = *typ_enum[teIndex];
-            Trace("dt-cmi-debug") << "Try " << neqc << " ... " << std::endl;
-            ++typ_enum[teIndex];
-            for( unsigned i=0; i<cons.size(); i++ ){
-              //check if it is modulo equality the same
-              if( cons[i].getOperator()==neqc.getOperator() ){
-                bool diff = false;
-                for( unsigned j=0; j<cons[i].getNumChildren(); j++ ){
-                  if( !m->areEqual( cons[i][j], neqc[j] ) ){
-                    diff = true;
-                    break;
-                  }
-                }
-                if( !diff ){
-                  Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl;
-                  success = false;
-                  break;
-                }
-              }
-            }
-          }while( !success );
-        }else{
-          TypeEnumerator te(tn);
-          neqc = *te;
-        }
-      }
-      */
     }else{
       Trace("dt-cmi") << "NOTICE : Datatypes: no constructor in equivalence class " << eqc << std::endl;
       Trace("dt-cmi") << "   Type : " << eqc.getType() << std::endl;
@@ -2186,6 +2149,34 @@ bool TheoryDatatypes::checkClashModEq( TNode n1, TNode n2, std::vector< Node >&
   return false;
 }
 
+void TheoryDatatypes::getRelevantTerms( std::set<Node>& termSet ) {
+  // Compute terms appearing in assertions and shared terms
+  computeRelevantTerms(termSet);
+  
+  //also include non-singleton equivalence classes
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
+  while( !eqcs_i.isFinished() ){
+    TNode r = (*eqcs_i);
+    bool addedFirst = false;
+    Node first;
+    eq::EqClassIterator eqc_i = eq::EqClassIterator( r, &d_equalityEngine );
+    while( !eqc_i.isFinished() ){
+      TNode n = (*eqc_i);
+      if( first.isNull() ){
+        first = n;
+      }else{
+        if( !addedFirst ){
+          addedFirst = true;
+          termSet.insert( first );
+        }
+        termSet.insert( n );
+      }
+      ++eqc_i;
+    }
+    ++eqcs_i;
+  }
+}
+
 std::pair<bool, Node> TheoryDatatypes::entailmentCheck(TNode lit, const EntailmentCheckParameters* params, EntailmentCheckSideEffects* out) {
   Trace("dt-entail") << "Check entailed : " << lit << std::endl;
   Node atom = lit.getKind()==NOT ? lit[0] : lit;
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 49c45590c..770c3a9d4 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -310,6 +310,8 @@ private:
   bool mustCommunicateFact( Node n, Node exp );
   /** check clash mod eq */
   bool checkClashModEq( TNode n1, TNode n2, std::vector< Node >& exp, std::vector< std::pair< TNode, TNode > >& deq_cand );
+  /** get relevant terms */
+  void getRelevantTerms( std::set<Node>& termSet );
 private:
   //equality queries
   bool hasTerm( TNode a );
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 81afc0da2..4f31f10b5 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -201,8 +201,13 @@ void TheorySep::computeCareGraph() {
 
 
 void TheorySep::collectModelInfo( TheoryModel* m, bool fullModel ){
+  set<Node> termSet;
+
+  // Compute terms appearing in assertions and shared terms
+  computeRelevantTerms(termSet);
+
   // Send the equality engine information to the model
-  m->assertEqualityEngine( &d_equalityEngine );
+  m->assertEqualityEngine( &d_equalityEngine, &termSet );
 }
 
 void TheorySep::postProcessModel( TheoryModel* m ){
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 7d2bbf3d1..e78575791 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -506,7 +506,6 @@ void TheorySetsPrivate::fullEffortCheck(){
     d_sentLemma = false;
     d_addedFact = false;
     d_set_eqc.clear();
-    d_set_eqc_relevant.clear();
     d_set_eqc_list.clear();
     d_eqc_emptyset.clear();
     d_eqc_singleton.clear();
@@ -532,9 +531,6 @@ void TheorySetsPrivate::fullEffortCheck(){
       if( tn.isSet() ){
         isSet = true;
         d_set_eqc.push_back( eqc );
-        if( d_equalityEngine.isTriggerTerm(eqc, THEORY_SETS) ){
-          d_set_eqc_relevant[eqc] = true;
-        }
       }
       Trace("sets-eqc") << "[" << eqc << "] : ";
       eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
@@ -551,7 +547,6 @@ void TheorySetsPrivate::fullEffortCheck(){
             if( pindex!=-1  ){
               if( d_pol_mems[pindex][s].find( x )==d_pol_mems[pindex][s].end() ){
                 d_pol_mems[pindex][s][x] = n;
-                d_set_eqc_relevant[s] = true;
                 Trace("sets-debug2") << "Membership[" << x << "][" << s << "] : " << n << ", pindex = " << pindex << std::endl;
               }
               if( d_members_index[s].find( x )==d_members_index[s].end() ){
@@ -579,8 +574,6 @@ void TheorySetsPrivate::fullEffortCheck(){
           }else{
             Node r1 = d_equalityEngine.getRepresentative( n[0] );
             Node r2 = d_equalityEngine.getRepresentative( n[1] );
-            d_set_eqc_relevant[r1] = true;
-            d_set_eqc_relevant[r2] = true;
             if( d_bop_index[n.getKind()][r1].find( r2 )==d_bop_index[n.getKind()][r1].end() ){
               d_bop_index[n.getKind()][r1][r2] = n;
               d_op_list[n.getKind()].push_back( n );
@@ -601,7 +594,6 @@ void TheorySetsPrivate::fullEffortCheck(){
             //TODO: extend approach for this case
           }
           Node r = d_equalityEngine.getRepresentative( n[0] );
-          d_set_eqc_relevant[r] = true;
           if( d_eqc_to_card_term.find( r )==d_eqc_to_card_term.end() ){
             d_eqc_to_card_term[ r ] = n;
             registerCardinalityTerm( n[0], lemmas );
@@ -1740,14 +1732,18 @@ EqualityStatus TheorySetsPrivate::getEqualityStatus(TNode a, TNode b) {
 
 
 void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) {
-  Trace("sets") << "Set collect model info" << std::endl;
+  Trace("sets-model") << "Set collect model info" << std::endl;
+  set<Node> termSet;
+  // Compute terms appearing in assertions and shared terms
+  d_external.computeRelevantTerms(termSet);
+  
   // Assert equalities and disequalities to the model
-  m->assertEqualityEngine(&d_equalityEngine);
+  m->assertEqualityEngine(&d_equalityEngine,&termSet);
   
   std::map< Node, Node > mvals;
   for( int i=(int)(d_set_eqc.size()-1); i>=0; i-- ){
     Node eqc = d_set_eqc[i];
-    if( d_set_eqc_relevant.find( eqc )==d_set_eqc_relevant.end() ){
+    if( termSet.find( eqc )==termSet.end() ){
       Trace("sets-model") << "* Do not assign value for " << eqc << " since is not relevant." << std::endl;
     }else{
       std::vector< Node > els;
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 09cc3cb3b..45a6a93d1 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -442,7 +442,16 @@ void TheoryStrings::presolve() {
 void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
   Trace("strings-model") << "TheoryStrings : Collect model info, fullModel = " << fullModel << std::endl;
   Trace("strings-model") << "TheoryStrings : assertEqualityEngine." << std::endl;
+  
+  //AJR : no use doing this since we cannot preregister terms with finite types that don't belong to strings.
+  //      change this if we generalize to sequences.
+  //set<Node> termSet;
+  // Compute terms appearing in assertions and shared terms
+  //computeRelevantTerms(termSet);
+  //m->assertEqualityEngine( &d_equalityEngine, &termSet );
+  
   m->assertEqualityEngine( &d_equalityEngine );
+  
   // Generate model
   std::vector< Node > nodes;
   getEquivalenceClasses( nodes );
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index e4a3ac78c..35aee5305 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -246,7 +246,12 @@ Node TheoryUF::explain(TNode literal, eq::EqProof* pf) {
 }
 
 void TheoryUF::collectModelInfo( TheoryModel* m, bool fullModel ){
-  m->assertEqualityEngine( &d_equalityEngine );
+  set<Node> termSet;
+
+  // Compute terms appearing in assertions and shared terms
+  computeRelevantTerms(termSet);
+
+  m->assertEqualityEngine( &d_equalityEngine, &termSet );
   // if( fullModel ){
   //   std::map< TypeNode, TypeEnumerator* > type_enums;
   //   //must choose proper representatives
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index 62f8665ec..f4f921c43 100644
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -73,8 +73,8 @@ TESTS =	\
 	card-6.smt2 \
 	card-7.smt2 \
 	abt-min.smt2 \
-	abt-te-exh.smt2
-
+	abt-te-exh.smt2 \
+	abt-te-exh2.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/sets/abt-te-exh2.smt2 b/test/regress/regress0/sets/abt-te-exh2.smt2
new file mode 100644
index 000000000..9ff80e14c
--- /dev/null
+++ b/test/regress/regress0/sets/abt-te-exh2.smt2
@@ -0,0 +1,24 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+(set-logic ALL)
+(declare-sort Atom 0)
+
+(declare-fun p ((Set Atom) (Set Atom)) (Set Atom))
+(declare-fun j ((Set Atom) (Set Atom)) (Set Atom))
+(declare-fun k ((Set Atom) (Set Atom)) (Set Atom))
+(declare-fun d ((Set Atom) (Set Atom)) (Set Atom))
+
+(declare-fun a () (Set Atom))
+(declare-fun n () Atom)
+(declare-fun v () Atom)
+
+(assert (forall ((b Atom) (c Atom)) 
+(or 
+(member v (k (singleton n) (j (singleton b) a)))
+(= (as emptyset (Set Atom)) (d (j (singleton b) a) (singleton n)))
+)
+)
+)
+
+(check-sat)
+