hard limit for rec-fun eval (#3485)

4 files changed, 125 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")
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d810aa5be..841b18fce 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1745,6 +1745,7 @@ set(regress_1_tests
   regress1/sygus/rec-fun-sygus.sy
   regress1/sygus/rec-fun-while-1.sy
   regress1/sygus/rec-fun-while-2.sy
+  regress1/sygus/rec-fun-while-infinite.sy
   regress1/sygus/re-concat.sy
   regress1/sygus/repair-const-rl.sy
   regress1/sygus/simple-regexp.sy
diff --git a/test/regress/regress1/sygus/rec-fun-while-infinite.sy b/test/regress/regress1/sygus/rec-fun-while-infinite.sy
new file mode 100644
index 000000000..77ddb04bc
--- /dev/null
+++ b/test/regress/regress1/sygus/rec-fun-while-infinite.sy
@@ -0,0 +1,97 @@
+; EXPECT: unkown
+; COMMAND-LINE: --sygus-out=status --lang=sygus2 --sygus-rec-fun --no-e-matching --no-check-synth-sol
+
+(set-logic ALL)
+
+; The environment datatypes
+(declare-datatype NVars ((x) (y)))
+
+(declare-datatype Pair ((build (first NVars) (second Int))))
+
+(declare-datatype Env ((cons (head Pair) (tail Env)) (nil)))
+
+(define-fun-rec envStore ((var NVars) (value Int) (env Env)) Env
+  (ite (is-nil env)
+    (cons (build var value) env)
+    (ite (= var (first (head env)))
+      (cons (build var value) (tail env))
+      (cons (head env) (envStore var value (tail env)))
+      )
+    )
+  )
+
+(define-fun-rec envSelect ((var NVars) (env Env)) Int
+  (ite (is-nil env)
+    0
+    (ite (= var (first (head env)))
+      (second (head env))
+      (envSelect var (tail env))
+      )
+    )
+  )
+
+; Syntax for arithmetic expressions
+(declare-datatype Aexp
+  (
+    (Val (val Int))
+    (Var (name NVars))
+    (Add (addL Aexp) (addR Aexp))
+    )
+  )
+
+; Function to evaluate arithmetic expressions
+(define-fun-rec evalA ((env Env) (a Aexp)) Int
+  (ite (is-Val a)
+    (val a)
+    (ite (is-Var a)
+      (envSelect (name a) env)
+      ; (is-Add a)
+      (+ (evalA env (addL a)) (evalA env (addR a)))
+      )))
+
+; Syntax for boolean expressions
+(declare-datatype Bexp
+  (
+    (TRUE)
+    ))
+
+; Function to evaluate boolean expressions
+(define-fun-rec evalB ((env Env) (b Bexp)) Bool
+  (is-TRUE b)
+)
+
+; Syntax for commands
+(declare-datatype Com
+  (
+    (Assign (lhs NVars) (rhs Aexp))
+    (While (wCond Bexp) (wCom Com))
+    )
+  )
+
+; Function to evaluate statements
+(define-fun-rec evalC ((env Env) (c Com)) Env
+  (ite (is-Assign c)
+    (envStore (lhs c) (evalA env (rhs c)) env)
+        ; (is-While c)
+          (ite (evalB env (wCond c)) (evalC (evalC env (wCom c)) c) env)
+        )
+      )
+
+
+(synth-fun prog () Com
+  ((C1 Com) (C2 Com) (V NVars) (A1 Aexp) (A2 Aexp) (A3 Aexp) (B Bexp) (I Int))
+  (
+    (C1 Com ((While B C2)))
+    (C2 Com ((Assign V A1)))
+    (V NVars (x))
+    (A1 Aexp ((Var V)))
+    (A2 Aexp ((Val I)))
+    (A3 Aexp ((Add A1 A2)))
+    (B Bexp (TRUE))
+    (I Int (1))
+    )
+)
+
+(constraint (= (evalC (cons (build x 1) nil) prog) (cons (build x 1) nil)))
+
+(check-synth)