From 596fe8c79106dd9b7764df2ddce6b2d3344fea34 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Wed, 20 Nov 2019 16:42:58 -0300 Subject: [PATCH] Lazy evaluation via rec-funs of ITE expressions (#3482) --- src/theory/quantifiers/fun_def_evaluator.cpp | 57 +++++++++++- .../quantifiers/sygus/synth_conjecture.cpp | 3 +- test/regress/CMakeLists.txt | 2 + .../regress/regress1/sygus/rec-fun-while-1.sy | 92 ++++++++++++++++++ .../regress/regress1/sygus/rec-fun-while-2.sy | 93 +++++++++++++++++++ 5 files changed, 243 insertions(+), 4 deletions(-) create mode 100644 test/regress/regress1/sygus/rec-fun-while-1.sy create mode 100644 test/regress/regress1/sygus/rec-fun-while-2.sy diff --git a/src/theory/quantifiers/fun_def_evaluator.cpp b/src/theory/quantifiers/fun_def_evaluator.cpp index 376d0eb47..1528d5338 100644 --- a/src/theory/quantifiers/fun_def_evaluator.cpp +++ b/src/theory/quantifiers/fun_def_evaluator.cpp @@ -75,6 +75,13 @@ Node FunDefEvaluator::evaluate(Node n) const Trace("fd-eval-debug") << "constant " << cur << std::endl; visited[cur] = cur; } + else if (cur.getKind() == ITE) + { + Trace("fd-eval-debug") << "ITE " << cur << std::endl; + visited[cur] = Node::null(); + visit.push_back(cur); + visit.push_back(cur[0]); + } else { Trace("fd-eval-debug") << "recurse " << cur << std::endl; @@ -102,6 +109,28 @@ Node FunDefEvaluator::evaluate(Node n) const { children.push_back(cur.getOperator()); } + else if (ck == ITE) + { + // get evaluation of condition + it = visited.find(cur[0]); + Assert(it != visited.end()); + Assert(!it->second.isNull()); + Assert(it->second.isConst()); + // pick child to evaluate depending on condition eval + unsigned childIdxToEval = it->second.getConst() ? 1 : 2; + Trace("fd-eval-debug2") + << "FunDefEvaluator: result of ITE condition : " + << it->second.getConst() << "\n"; + // the result will be the result of evaluation the child + visited[cur] = cur[childIdxToEval]; + // push back self and child. The child will be evaluated first and + // result will be the result of evaluation child + visit.push_back(cur); + visit.push_back(cur[childIdxToEval]); + Trace("fd-eval-debug2") << "FunDefEvaluator: result will be from : " + << cur[childIdxToEval] << "\n"; + continue; + } for (const Node& cn : cur) { it = visited.find(cn); @@ -114,6 +143,8 @@ Node FunDefEvaluator::evaluate(Node n) const { // need to evaluate it f = cur.getOperator(); + Trace("fd-eval-debug2") + << "FunDefEvaluator: need to eval " << f << "\n"; itf = d_funDefMap.find(f); if (itf == d_funDefMap.end()) { @@ -123,6 +154,8 @@ Node FunDefEvaluator::evaluate(Node n) const } // get the function definition Node sbody = itf->second.d_body; + Trace("fd-eval-debug2") + << "FunDefEvaluator: definition: " << sbody << "\n"; const std::vector& args = itf->second.d_args; if (!args.empty()) { @@ -131,6 +164,17 @@ Node FunDefEvaluator::evaluate(Node n) const args.begin(), args.end(), children.begin(), children.end()); // rewrite it sbody = Rewriter::rewrite(sbody); + if (Trace.isOn("fd-eval-debug2")) + { + Trace("fd-eval-debug2") + << "FunDefEvaluator: evaluation with args:\n"; + for (const Node& child : children) + { + Trace("fd-eval-debug2") << "..." << child << "\n"; + } + Trace("fd-eval-debug2") + << "FunDefEvaluator: results in " << sbody << "\n"; + } } // our result is the result of the body visited[cur] = sbody; @@ -164,11 +208,18 @@ Node FunDefEvaluator::evaluate(Node n) const } } } while (!visit.empty()); + Trace("fd-eval") << "FunDefEvaluator: return " << visited[n]; Assert(visited.find(n) != visited.end()); Assert(!visited.find(n)->second.isNull()); - Assert(visited.find(n)->second.isConst()); - Trace("fd-eval") << "FunDefEvaluator: return SUCCESS " << visited[n] - << std::endl; + if (!visited.find(n)->second.isConst()) + { + visited[n] = Node::null(); + Trace("fd-eval") << "\n with NONCONST\n"; + } + else + { + Trace("fd-eval") << "\n with SUCCESS\n"; + } return visited[n]; } diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 6e69715ef..6591e6828 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -591,7 +591,8 @@ bool SynthConjecture::doCheck(std::vector& lems) Trace("cegqi-debug") << "...squery : " << squery << std::endl; squery = Rewriter::rewrite(squery); Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl; - Assert(squery.isConst() && squery.getConst()); + Assert(options::sygusRecFun() + || (squery.isConst() && squery.getConst())); #endif return false; } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 3c060a304..d810aa5be 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1743,6 +1743,8 @@ set(regress_1_tests regress1/sygus/qf_abv.smt2 regress1/sygus/real-grammar.sy regress1/sygus/rec-fun-sygus.sy + regress1/sygus/rec-fun-while-1.sy + regress1/sygus/rec-fun-while-2.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-1.sy b/test/regress/regress1/sygus/rec-fun-while-1.sy new file mode 100644 index 000000000..c175094ee --- /dev/null +++ b/test/regress/regress1/sygus/rec-fun-while-1.sy @@ -0,0 +1,92 @@ +; EXPECT: unsat +; 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))) + +(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) + (envSelect (name a) env) + )) + +; Syntax for boolean expressions +(declare-datatype Bexp + ( + (LT (ltL Aexp) (ltR Aexp)) + ) + ) + +; Function to evaluate boolean expressions +(define-fun-rec evalB ((env Env) (b Bexp)) Bool + (< (evalA env (ltL b)) (evalA env (ltR 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) + (ite (evalB env (wCond c)) (evalC (evalC env (wCom c)) c) env) + ) + ) + +(synth-fun prog () Com + ((C1 Com) (C2 Com) (VX NVars) (A1 Aexp) (A2 Aexp) (B Bexp) (I Int)) + ( + (C1 Com ((While B C2))) + (C2 Com ((Assign VX A2))) + (VX NVars (x)) + (A1 Aexp ((Var VX))) + (A2 Aexp ((Val I))) + (B Bexp ((LT A1 A2))) + (I Int (0 1 (+ I I))) + ) +) + +(constraint (= (evalC (cons (build x 0) nil) prog) (cons (build x 2) nil))) + +(check-synth) diff --git a/test/regress/regress1/sygus/rec-fun-while-2.sy b/test/regress/regress1/sygus/rec-fun-while-2.sy new file mode 100644 index 000000000..87a4f2a6e --- /dev/null +++ b/test/regress/regress1/sygus/rec-fun-while-2.sy @@ -0,0 +1,93 @@ +; EXPECT: unsat +; 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)) + (Sub (subL Aexp) (subR Aexp)) + ) + ) + +; Function to evaluate arithmetic expressions +(define-fun-rec evalA ((env Env) (a Aexp)) Int + (ite (is-Val a) + (val a) + (envSelect (name a) env) + )) + +; Syntax for boolean expressions +(declare-datatype Bexp + ( + (GTH (geqL Aexp) (geqR Aexp)) + ) + ) + +; Function to evaluate boolean expressions +(define-fun-rec evalB ((env Env) (b Bexp)) Bool + (> (evalA env (geqL b)) (evalA env (geqR 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) + (ite (evalB env (wCond c)) (evalC (evalC env (wCom c)) c) env) + ) + ) + +(synth-fun prog () Com + ((C1 Com) (C2 Com) (VX NVars) (A1 Aexp) (A2 Aexp) (B Bexp) (I Int)) + ( + (C1 Com ((While B C2))) + (C2 Com ((Assign VX A2))) + (VX NVars (x)) + (A1 Aexp ((Var VX))) + (A2 Aexp ((Val I))) + (B Bexp ((GTH A2 A1))) + (I Int (2)) + ) +) + +(constraint (= (evalC (cons (build x 0) nil) prog) (cons (build x 2) nil))) + +(check-synth) -- 2.30.2