sygusComp2018: optimization for collect model info (#2105)

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index bfd7a550923de57fe3fdcdec507bb9e19f91cc2b..e3b48a4da8f7c82ae763c82bf827c2a2a2892747 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -2226,35 +2226,53 @@ bool TheoryDatatypes::checkClashModEq( TNode n1, TNode n2, std::vector< Node >&
 
 void TheoryDatatypes::getRelevantTerms( std::set<Node>& termSet ) {
   // Compute terms appearing in assertions and shared terms
-  computeRelevantTerms(termSet);
-  
+  std::set<Kind> irr_kinds;
+  // testers are not relevant for model construction
+  irr_kinds.insert(APPLY_TESTER);
+  computeRelevantTerms(termSet, irr_kinds);
+
+  Trace("dt-cmi") << "Have " << termSet.size() << " relevant terms..."
+                  << std::endl;
+
   //also include non-singleton equivalence classes  TODO : revisit this
   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;
-        //always include all datatypes
-        if( n.getType().isDatatype() ){
-          addedFirst = true;
-          termSet.insert( n );
+    TypeNode rtn = r.getType();
+    if (!rtn.isBoolean())
+    {
+      eq::EqClassIterator eqc_i = eq::EqClassIterator(r, &d_equalityEngine);
+      while (!eqc_i.isFinished())
+      {
+        TNode n = (*eqc_i);
+        if (first.isNull())
+        {
+          first = n;
+          // always include all datatypes
+          if (rtn.isDatatype())
+          {
+            addedFirst = true;
+            termSet.insert(n);
+          }
         }
-      }else{
-        if( !addedFirst ){
-          addedFirst = true;
-          termSet.insert( first );
+        else
+        {
+          if (!addedFirst)
+          {
+            addedFirst = true;
+            termSet.insert(first);
+          }
+          termSet.insert(n);
         }
-        termSet.insert( n );
+        ++eqc_i;
       }
-      ++eqc_i;
     }
     ++eqcs_i;
   }
+  Trace("dt-cmi") << "After adding non-singletons, has " << termSet.size()
+                  << " relevant terms..." << std::endl;
 }
 
 std::pair<bool, Node> TheoryDatatypes::entailmentCheck(TNode lit, const EntailmentCheckParameters* params, EntailmentCheckSideEffects* out) {

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 10504b487995833d52e26298f9db6fc9a8ab14b0..31177669349f75367b966a76699d777ada4bc596 100644 (file)
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -232,36 +232,54 @@ std::unordered_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() cons
   return currentlyShared;
 }
 
-
-void Theory::collectTerms(TNode n, set<Node>& termSet) const
+void Theory::collectTerms(TNode n,
+                          set<Kind>& irrKinds,
+                          set<Node>& termSet) const
 {
   if (termSet.find(n) != termSet.end()) {
     return;
   }
-  Trace("theory::collectTerms") << "Theory::collectTerms: adding " << n << endl;
-  termSet.insert(n);
-  if (n.getKind() == kind::NOT || n.getKind() == kind::EQUAL || !isLeaf(n)) {
+  Kind nk = n.getKind();
+  if (irrKinds.find(nk) == irrKinds.end())
+  {
+    Trace("theory::collectTerms")
+        << "Theory::collectTerms: adding " << n << endl;
+    termSet.insert(n);
+  }
+  if (nk == kind::NOT || nk == kind::EQUAL || !isLeaf(n))
+  {
     for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) {
-      collectTerms(*child_it, termSet);
+      collectTerms(*child_it, irrKinds, termSet);
     }
   }
 }
 
 
 void Theory::computeRelevantTerms(set<Node>& termSet, bool includeShared) const
+{
+  set<Kind> irrKinds;
+  computeRelevantTerms(termSet, irrKinds, includeShared);
+}
+
+void Theory::computeRelevantTerms(set<Node>& termSet,
+                                  set<Kind>& irrKinds,
+                                  bool includeShared) const
 {
   // Collect all terms appearing in assertions
+  irrKinds.insert(kind::EQUAL);
+  irrKinds.insert(kind::NOT);
   context::CDList<Assertion>::const_iterator assert_it = facts_begin(), assert_it_end = facts_end();
   for (; assert_it != assert_it_end; ++assert_it) {
-    collectTerms(*assert_it, termSet);
+    collectTerms(*assert_it, irrKinds, termSet);
   }
 
   if (!includeShared) return;
 
   // Add terms that are shared terms
+  set<Kind> kempty;
   context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end();
   for (; shared_it != shared_it_end; ++shared_it) {
-    collectTerms(*shared_it, termSet);
+    collectTerms(*shared_it, kempty, termSet);
   }
 }
 

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 3721806add0f166d988105e9c63e6a4c463b254c..2c3c727cbcba947c8ac901ba86c32909bf635e0f 100644 (file)
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -161,14 +161,27 @@ private:
   /**
    * Helper function for computeRelevantTerms
    */
-  void collectTerms(TNode n, std::set<Node>& termSet) const;
+  void collectTerms(TNode n,
+                    std::set<Kind>& irrKinds,
+                    std::set<Node>& termSet) const;
 
   /**
    * Scans the current set of assertions and shared terms top-down
    * until a theory-leaf is reached, and adds all terms found to
    * termSet.  This is used by collectModelInfo to delimit the set of
-   * terms that should be used when constructing a model
+   * terms that should be used when constructing a model.
+   *
+   * irrKinds: The kinds of terms that appear in assertions that should *not*
+   * be included in termSet. Note that the kinds EQUAL and NOT are always
+   * treated as irrelevant kinds.
+   *
+   * includeShared: Whether to include shared terms in termSet. Notice that
+   * shared terms are not influenced by irrKinds.
    */
+  void computeRelevantTerms(std::set<Node>& termSet,
+                            std::set<Kind>& irrKinds,
+                            bool includeShared = true) const;
+  /** same as above, but with empty irrKinds */
   void computeRelevantTerms(std::set<Node>& termSet, bool includeShared = true) const;
 
   /**

diff --git a/test/regress/regress0/tptp/DAT001=1.p b/test/regress/regress0/tptp/DAT001=1.p
index 922a6cfc344c8436810ed08f4f0a77b30e191e9b..f30db563a7639dc4e399d0c3c5b90443ef3185b1 100644 (file)
--- a/test/regress/regress0/tptp/DAT001=1.p
+++ b/test/regress/regress0/tptp/DAT001=1.p
@@ -1,3 +1,4 @@
+% COMMAND-LINE: --no-finite-model-find
 %------------------------------------------------------------------------------
 % File     : DAT001=1 : TPTP v5.5.0. Released v5.0.0.
 % Domain   : Data Structures