hard limit for rec-fun eval (#3485)

2 files changed, 27 insertions, 5 deletions

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 338f5544f..b3c1ffd4d 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1221,6 +1221,14 @@ header = "options/quantifiers_options.h"
   default    = "false"
   help       = "enable efficient support for recursive functions in sygus grammars"
 
+[[option]]
+  name       = "sygusRecFunEvalLimit"
+  category   = "regular"
+  long       = "sygus-rec-fun-eval-limit=N"
+  type       = "int"
+  default    = "1000"
+  help       = "use a hard limit for how many times in a given evaluator call a recursive function can be evaluated (so infinite loops can be avoided)"
+
 # Internal uses of sygus
 
 [[option]]
@@ -1359,7 +1367,7 @@ header = "options/quantifiers_options.h"
   long       = "sygus-expr-miner-check-timeout=N"
   type       = "unsigned long"
   help       = "timeout (in milliseconds) for satisfiability checks in expression miners"
-  
+
 [[option]]
   name       = "sygusRewSynthRec"
   category   = "regular"
@@ -1420,7 +1428,7 @@ header = "options/quantifiers_options.h"
   default    = "false"
   help       = "compute backwards filtering to compute whether previous solutions are filtered based on later ones"
 
-  
+
 [[option]]
   name       = "sygusExprMinerCheckUseExport"
   category   = "expert"
diff --git a/src/theory/quantifiers/fun_def_evaluator.cpp b/src/theory/quantifiers/fun_def_evaluator.cpp
index 1528d5338..ffac9b2c8 100644
--- a/src/theory/quantifiers/fun_def_evaluator.cpp
+++ b/src/theory/quantifiers/fun_def_evaluator.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/quantifiers/fun_def_evaluator.h"
 
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/rewriter.h"
 
@@ -53,6 +54,8 @@ Node FunDefEvaluator::evaluate(Node n) const
   Assert(Rewriter::rewrite(n) == n);
   Trace("fd-eval") << "FunDefEvaluator: evaluate " << n << std::endl;
   NodeManager* nm = NodeManager::currentNM();
+  std::unordered_map<TNode, unsigned, TNodeHashFunction> funDefCount;
+  std::unordered_map<TNode, unsigned, TNodeHashFunction>::iterator itCount;
   std::unordered_map<TNode, Node, TNodeHashFunction> visited;
   std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
   std::map<Node, FunDefInfo>::const_iterator itf;
@@ -146,12 +149,23 @@ Node FunDefEvaluator::evaluate(Node n) const
           Trace("fd-eval-debug2")
               << "FunDefEvaluator: need to eval " << f << "\n";
           itf = d_funDefMap.find(f);
-          if (itf == d_funDefMap.end())
+          itCount = funDefCount.find(f);
+          if (itCount == funDefCount.end())
           {
-            Trace("fd-eval") << "FunDefEvaluator: no definition for " << f
-                             << ", FAIL" << std::endl;
+            funDefCount[f] = 0;
+            itCount = funDefCount.find(f);
+          }
+          if (itf == d_funDefMap.end()
+              || itCount->second > options::sygusRecFunEvalLimit())
+          {
+            Trace("fd-eval")
+                << "FunDefEvaluator: "
+                << (itf == d_funDefMap.end() ? "no definition for "
+                                             : "too many evals for ")
+                << f << ", FAIL" << std::endl;
             return Node::null();
           }
+          ++funDefCount[f];
           // get the function definition
           Node sbody = itf->second.d_body;
           Trace("fd-eval-debug2")