Guard eval by option, fix.

4 files changed, 19 insertions, 13 deletions

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index a2bbce1f8..eae2d410b 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1168,6 +1168,14 @@ header = "options/quantifiers_options.h"
   default    = "true"
   help       = "Minimize synthesis solutions"
 
+[[option]]
+  name       = "sygusEvalOpt"
+  category   = "regular"
+  long       = "sygus-eval-opt"
+  type       = "bool"
+  default    = "true"
+  help       = "use optimized approach for evaluation in sygus"
+
 # Internal uses of sygus
 
 [[option]]
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 9ba955995..c0bd0a118 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -989,10 +989,6 @@ void SygusSymBreakNew::registerSymBreakLemma( TypeNode tn, Node lem, unsigned sz
   Trace("sygus-sb-debug") << "     size : " << sz << std::endl;
   Assert( !a.isNull() );
   d_cache[a].d_sb_lemmas[tn][sz].push_back( lem );
-  if( options::sygusSymBreakLazy() )
-  {
-    return;
-  }
   TNode x = getFreeVar( tn );
   unsigned csz = getSearchSizeForAnchor( a );
   int max_depth = ((int)csz)-((int)sz);
@@ -1002,7 +998,7 @@ void SygusSymBreakNew::registerSymBreakLemma( TypeNode tn, Node lem, unsigned sz
     if( itt!=d_cache[a].d_search_terms[tn].end() ){
       for (const TNode& t : itt->second)
       {
-        if( d_active_terms.find( t )!=d_active_terms.end() ){
+        if( !options::sygusSymBreakLazy() || d_active_terms.find( t )!=d_active_terms.end() ){
           Node slem = lem.substitute(x, t);
           Node rlv = getRelevancyCondition(t);
           if (!rlv.isNull())
@@ -1184,10 +1180,6 @@ void SygusSymBreakNew::incrementCurrentSearchSize( Node m, std::vector< Node >&
   std::map< Node, SearchSizeInfo * >::iterator itsz = d_szinfo.find( m );
   Assert( itsz!=d_szinfo.end() );
   itsz->second->d_curr_search_size++;
-  if( options::sygusSymBreakLazy() )
-  {
-    return;
-  }
   Trace("sygus-fair") << "  register search size " << itsz->second->d_curr_search_size << " for " << m << std::endl;
   NodeManager* nm = NodeManager::currentNM();
   for( std::map< Node, SearchCache >::iterator itc = d_cache.begin(); itc != d_cache.end(); ++itc ){
@@ -1207,7 +1199,8 @@ void SygusSymBreakNew::incrementCurrentSearchSize( Node m, std::vector< Node >&
           if( itt!=itc->second.d_search_terms[tn].end() ){
             for (const TNode& t : itt->second)
             {
-              if (d_active_terms.find(t) != d_active_terms.end()
+              if (!options::sygusSymBreakLazy() ||
+                   d_active_terms.find(t) != d_active_terms.end()
                          && !it->second.empty())
               {
                 std::vector<Node> slemmas;
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index 127cf005d..4309efceb 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -516,7 +516,8 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
   }
   // get the results for each slave enumerator
   std::map<Node, std::vector< Node > > srmap;
-  Evaluator ev;
+  Evaluator * ev = d_tds->getEvaluator();
+  bool tryEval = options::sygusEvalOpt();
   for( const Node& xs : ei.d_enum_slave )
   {
     Assert( srmap.find(xs)==srmap.end());
@@ -533,7 +534,11 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
         TNode tres = res;
         std::vector< Node > vals;
         vals.push_back(tres);
-        Node sres = ev.eval(templ,args,vals);
+        Node sres;
+        if( tryEval )
+        {
+          sres = ev->eval(templ,args,vals);
+        }
         if( sres.isNull() )
         {
           // fall back on rewriter
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index d2df41fd2..6cc52fe01 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -1641,7 +1641,7 @@ Node TermDbSygus::evaluateBuiltin(TypeNode tn,
     Assert( it->second.size()==args.size() );
 
     Node res;
-    if (tryEval)
+    if (tryEval && options::sygusEvalOpt())
     {
       // Try evaluating, which is much faster than substitution+rewriting.
       // This may fail if there is a subterm of bn under the