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

* Decouple sygus term database and term database.

* Clang format

* Fix include

1 files changed, 15 insertions, 4 deletions

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index ac0de29e3..f6b920cda 100644
--- 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 );
         }
       }