Decouple sygus term database and term database. (#1317)

* Decouple sygus term database and term database.

* Clang format

* Fix include

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index a3225e404c6bde88efe52d523a59188b6114c4b8..5db58067fe2ae2bd03ed0a1f0bff083474b90703 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -14,20 +14,12 @@
 
 #include "theory/quantifiers/term_database.h"
 
-#include "expr/datatype.h"
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
-#include "options/datatypes_options.h"
 #include "options/uf_options.h"
-#include "theory/quantifiers/ce_guided_instantiation.h"
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/fun_def_engine.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/quantifiers/rewrite_engine.h"
-#include "theory/quantifiers/theory_quantifiers.h"
-#include "theory/quantifiers/trigger.h"
-#include "theory/quantifiers/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers/trigger.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
 
@@ -250,10 +242,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi
           d_ops.push_back(op);
           d_op_map[op].push_back( n );
           added.insert( n );
-          
-          if( d_quantEngine->getTermDatabaseSygus() ){
-            d_quantEngine->getTermDatabaseSygus()->registerEvalTerm( n );
-          }
         }
       }else{
         setTermInactive( n );

diff --git a/src/theory/quantifiers/term_database_sygus.cpp b/src/theory/quantifiers/term_database_sygus.cpp
index f298e971162d61606ef034f4a80f80d62a0a6caf..d8d120eab945469b47c93d7dbd45707a8d68f9e2 100644 (file)
--- a/src/theory/quantifiers/term_database_sygus.cpp
+++ b/src/theory/quantifiers/term_database_sygus.cpp
@@ -1912,32 +1912,38 @@ unsigned TermDbSygus::getAnchorDepth( Node n ) {
 void TermDbSygus::registerEvalTerm( Node n ) {
   if( options::sygusDirectEval() ){
     if( n.getKind()==APPLY_UF && !n.getType().isBoolean() ){
-      Trace("sygus-eager") << "TermDbSygus::eager: Register eval term : " << n
-                           << std::endl;
       TypeNode tn = n[0].getType();
       if( tn.isDatatype() ){
         const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
         if( dt.isSygus() ){
           Node f = n.getOperator();
-          Trace("sygus-eager") << "...the evaluation function is : " << f << std::endl;
           if( n[0].getKind()!=APPLY_CONSTRUCTOR ){
-            d_evals[n[0]].push_back( n );
-            TypeNode tn = n[0].getType();
-            Assert( tn.isDatatype() );
-            const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-            Node var_list = Node::fromExpr( dt.getSygusVarList() );
-            Assert( dt.isSygus() );
-            d_eval_args[n[0]].push_back( std::vector< Node >() );
-            bool isConst = true;
-            for( unsigned j=1; j<n.getNumChildren(); j++ ){
-              d_eval_args[n[0]].back().push_back( n[j] );
-              if( !n[j].isConst() ){
-                isConst = false;
+            if (d_eval_processed.find(n) == d_eval_processed.end())
+            {
+              Trace("sygus-eager")
+                  << "TermDbSygus::eager: Register eval term : " << n
+                  << std::endl;
+              d_eval_processed.insert(n);
+              d_evals[n[0]].push_back(n);
+              TypeNode tn = n[0].getType();
+              Assert(tn.isDatatype());
+              const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+              Node var_list = Node::fromExpr(dt.getSygusVarList());
+              Assert(dt.isSygus());
+              d_eval_args[n[0]].push_back(std::vector<Node>());
+              bool isConst = true;
+              for (unsigned j = 1; j < n.getNumChildren(); j++)
+              {
+                d_eval_args[n[0]].back().push_back(n[j]);
+                if (!n[j].isConst())
+                {
+                  isConst = false;
+                }
               }
+              d_eval_args_const[n[0]].push_back(isConst);
+              Node a = getAnchor(n[0]);
+              d_subterms[a][n[0]] = true;
             }
-            d_eval_args_const[n[0]].push_back( isConst );
-            Node a = getAnchor( n[0] );
-            d_subterms[a][n[0]] = true;
           }
         }
       }    

diff --git a/src/theory/quantifiers/term_database_sygus.h b/src/theory/quantifiers/term_database_sygus.h
index c819bc78142b46714784834dc95cec038d354e22..4786f053b4a01925db679e03289afd7d54026274 100644 (file)
--- a/src/theory/quantifiers/term_database_sygus.h
+++ b/src/theory/quantifiers/term_database_sygus.h
@@ -17,6 +17,8 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H
 #define __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H
 
+#include <unordered_set>
+
 #include "theory/quantifiers/sygus_explain.h"
 #include "theory/quantifiers/term_database.h"
 
@@ -243,6 +245,8 @@ public: // for symmetry breaking
 //for eager instantiation
   // TODO (as part of #1235) move some of these functions to sygus_explain.h
  private:
+  /** the set of evaluation terms we have already processed */
+  std::unordered_set<Node, NodeHashFunction> d_eval_processed;
   std::map< Node, std::map< Node, bool > > d_subterms;
   std::map< Node, std::vector< Node > > d_evals;
   std::map< Node, std::vector< std::vector< Node > > > d_eval_args;

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index ac0de29e32b9c65f795bf585bf86e9a8ba66c365..f6b920cda58a41c159a597d5b3ea93fb8ec91126 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -854,10 +854,21 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool within
     std::set< Node > added;
     d_term_db->addTerm(n, added, withinQuant, withinInstClosure);
 
-    //added contains also the Node that just have been asserted in this branch
-    if( d_quant_rel ){
-      for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){
-        if( !withinQuant ){
+    if (!withinQuant)
+    {
+      if (d_sygus_tdb)
+      {
+        d_sygus_tdb->registerEvalTerm(n);
+      }
+
+      // added contains also the Node that just have been asserted in this
+      // branch
+      if (d_quant_rel)
+      {
+        for (std::set<Node>::iterator i = added.begin(), end = added.end();
+             i != end;
+             i++)
+        {
           d_quant_rel->setRelevance( i->getOperator(), 0 );
         }
       }