From 8592fa1e2226e2c8b301ad9ed8caa13fad4c5913 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Thu, 21 Nov 2019 15:17:16 -0300 Subject: [PATCH] hard limit for rec-fun eval (#3485) --- src/options/quantifiers_options.toml | 12 ++- src/theory/quantifiers/fun_def_evaluator.cpp | 20 +++- test/regress/CMakeLists.txt | 1 + .../regress1/sygus/rec-fun-while-infinite.sy | 97 +++++++++++++++++++ 4 files changed, 125 insertions(+), 5 deletions(-) create mode 100644 test/regress/regress1/sygus/rec-fun-while-infinite.sy 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 funDefCount; + std::unordered_map::iterator itCount; std::unordered_map visited; std::unordered_map::iterator it; std::map::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) -- 2.30.2