From 46eeb6a507c31b4ac65b0ef70c32898667097377 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Wed, 27 Nov 2019 17:52:36 -0300 Subject: [PATCH] Enable sygusRecFun by default and fixes SyGuS+RecFun+HO issues (#3502) --- src/options/quantifiers_options.toml | 4 +- src/smt/smt_engine.cpp | 1 + src/theory/quantifiers/fun_def_evaluator.cpp | 41 ++++++---- .../quantifiers/sygus/synth_conjecture.cpp | 2 +- src/theory/quantifiers/sygus/synth_engine.cpp | 39 +++++----- .../quantifiers/sygus/term_database_sygus.cpp | 7 +- src/theory/quantifiers_engine.cpp | 5 +- test/regress/CMakeLists.txt | 1 + test/regress/regress1/sygus/list_recursor.sy | 2 +- test/regress/regress1/sygus/rec-fun-swap.sy | 76 +++++++++++++++++++ test/regress/regress1/sygus/rec-fun-sygus.sy | 2 +- .../regress/regress1/sygus/rec-fun-while-1.sy | 2 +- .../regress/regress1/sygus/rec-fun-while-2.sy | 2 +- .../regress1/sygus/rec-fun-while-infinite.sy | 2 +- 14 files changed, 139 insertions(+), 47 deletions(-) create mode 100644 test/regress/regress1/sygus/rec-fun-swap.sy diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index b3c1ffd4d..019b052bc 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1218,14 +1218,14 @@ header = "options/quantifiers_options.h" category = "regular" long = "sygus-rec-fun" type = "bool" - default = "false" + default = "true" help = "enable efficient support for recursive functions in sygus grammars" [[option]] name = "sygusRecFunEvalLimit" category = "regular" long = "sygus-rec-fun-eval-limit=N" - type = "int" + type = "unsigned" 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)" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 073c2ebc5..dfd3c9fee 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4861,6 +4861,7 @@ void SmtEngine::checkSynthSolution() SmtEngine solChecker(d_exprManager); solChecker.setLogic(getLogicInfo()); setOption("check-synth-sol", SExpr("false")); + setOption("sygus-rec-fun", SExpr("false")); Trace("check-synth-sol") << "Retrieving assertions\n"; // Build conjecture from original assertions diff --git a/src/theory/quantifiers/fun_def_evaluator.cpp b/src/theory/quantifiers/fun_def_evaluator.cpp index ffac9b2c8..8eb0ef686 100644 --- a/src/theory/quantifiers/fun_def_evaluator.cpp +++ b/src/theory/quantifiers/fun_def_evaluator.cpp @@ -118,7 +118,12 @@ Node FunDefEvaluator::evaluate(Node n) const it = visited.find(cur[0]); Assert(it != visited.end()); Assert(!it->second.isNull()); - Assert(it->second.isConst()); + if (!it->second.isConst()) + { + Trace("fd-eval") << "FunDefEvaluator: couldn't reduce condition of " + "ITE to const, FAIL\n"; + return Node::null(); + } // pick child to evaluate depending on condition eval unsigned childIdxToEval = it->second.getConst() ? 1 : 2; Trace("fd-eval-debug2") @@ -134,6 +139,7 @@ Node FunDefEvaluator::evaluate(Node n) const << cur[childIdxToEval] << "\n"; continue; } + unsigned child CVC4_UNUSED = 0; for (const Node& cn : cur) { it = visited.find(cn); @@ -141,6 +147,8 @@ Node FunDefEvaluator::evaluate(Node n) const Assert(!it->second.isNull()); childChanged = childChanged || cn != it->second; children.push_back(it->second); + Trace("fd-eval-debug2") << "argument " << child++ + << " eval : " << it->second << std::endl; } if (cur.getKind() == APPLY_UF) { @@ -197,6 +205,8 @@ Node FunDefEvaluator::evaluate(Node n) const // evaluating the body. if (!sbody.isConst()) { + Trace("fd-eval-debug2") << "FunDefEvaluator: will map " << cur + << " from body " << sbody << "\n"; visit.push_back(cur); visit.push_back(sbody); } @@ -208,32 +218,35 @@ Node FunDefEvaluator::evaluate(Node n) const ret = nm->mkNode(cur.getKind(), children); ret = Rewriter::rewrite(ret); } + Trace("fd-eval-debug2") << "built from arguments " << ret << "\n"; visited[cur] = ret; } } else if (cur != curEval && !curEval.isConst()) { Trace("fd-eval-debug") << "from body " << cur << std::endl; + Trace("fd-eval-debug") << "and eval " << curEval << std::endl; // we had to evaluate our body, which should have a definition now it = visited.find(curEval); - Assert(it != visited.end()); - // our definition is the result of the body - visited[cur] = it->second; + if (it == visited.end()) + { + Trace("fd-eval-debug2") << "eval without definition\n"; + // this is the case where curEval was not a constant but it was + // irreducible, for example (DT_SYGUS_EVAL e args) + visited[cur] = curEval; + } + else + { + Trace("fd-eval-debug2") + << "eval with definition " << it->second << "\n"; + visited[cur] = it->second; } } + } } while (!visit.empty()); - Trace("fd-eval") << "FunDefEvaluator: return " << visited[n]; + Trace("fd-eval") << "FunDefEvaluator: return " << visited[n] << ", SUCCESS\n"; Assert(visited.find(n) != visited.end()); Assert(!visited.find(n)->second.isNull()); - 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 6591e6828..da4275365 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -712,7 +712,7 @@ void SynthConjecture::doRefine(std::vector& lems) base_lem = base_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end()); Trace("cegqi-refine") << "doRefine : rewrite..." << std::endl; - base_lem = Rewriter::rewrite(base_lem); + base_lem = d_tds->rewriteNode(base_lem); Trace("cegqi-refine") << "doRefine : register refinement lemma " << base_lem << "..." << std::endl; d_master->registerRefinementLemma(sk_vars, base_lem, lems); diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index cbe907d41..4a708e66c 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -276,28 +276,29 @@ void SynthEngine::registerQuantifier(Node q) { Trace("cegqi-debug") << "SynthEngine: Register quantifier : " << q << std::endl; - if (d_quantEngine->getOwner(q) == this) + if (d_quantEngine->getOwner(q) != this) { - Trace("cegqi") << "Register conjecture : " << q << std::endl; - if (options::sygusQePreproc()) - { - d_waiting_conj.push_back(q); - } - else - { - // assign it now - assignConjecture(q); - } + return; } - if (options::sygusRecFun()) + if (d_quantEngine->getQuantAttributes()->isFunDef(q)) { - if (d_quantEngine->getQuantAttributes()->isFunDef(q)) - { - // If it is a recursive function definition, add it to the function - // definition evaluator class. - FunDefEvaluator* fde = d_tds->getFunDefEvaluator(); - fde->assertDefinition(q); - } + Assert(options::sygusRecFun()); + // If it is a recursive function definition, add it to the function + // definition evaluator class. + Trace("cegqi") << "Registering function definition : " << q << "\n"; + FunDefEvaluator* fde = d_tds->getFunDefEvaluator(); + fde->assertDefinition(q); + return; + } + Trace("cegqi") << "Register conjecture : " << q << std::endl; + if (options::sygusQePreproc()) + { + d_waiting_conj.push_back(q); + } + else + { + // assign it now + assignConjecture(q); } } diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 679d47779..d664a462d 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -741,9 +741,9 @@ Node TermDbSygus::rewriteNode(Node n) const { return fres; } - // It may have failed, in which case there are undefined symbols in res. - // In this case, we revert to the result of rewriting in the return - // statement below. + // It may have failed, in which case there are undefined symbols in res or + // we reached the limit of evaluations. In this case, we revert to the + // result of rewriting in the return statement below. } } return res; @@ -1082,4 +1082,3 @@ bool TermDbSygus::isEvaluationPoint(Node n) const }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ - diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 8337ba0b0..8730e3a97 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -407,14 +407,15 @@ void QuantifiersEngine::setOwner(Node q, quantifiers::QAttributes& qa) // set rewrite engine as owner setOwner(q, d_private->d_rr_engine.get(), 2); } - if (qa.d_sygus) + if (qa.d_sygus || (options::sygusRecFun() && !qa.d_fundef_f.isNull())) { if (d_private->d_synth_e.get() == nullptr) { Trace("quant-warn") << "WARNING : synth engine is null, and we have : " << q << std::endl; } - // set synth engine as owner + // set synth engine as owner since this is either a conjecture or a function + // definition to be used by sygus setOwner(q, d_private->d_synth_e.get(), 2); } } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index fda31cfdb..2182beaa8 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1744,6 +1744,7 @@ set(regress_1_tests regress1/sygus/qe.sy regress1/sygus/qf_abv.smt2 regress1/sygus/real-grammar.sy + regress1/sygus/rec-fun-swap.sy regress1/sygus/rec-fun-sygus.sy regress1/sygus/rec-fun-while-1.sy regress1/sygus/rec-fun-while-2.sy diff --git a/test/regress/regress1/sygus/list_recursor.sy b/test/regress/regress1/sygus/list_recursor.sy index 53c55397e..2e10a0c71 100644 --- a/test/regress/regress1/sygus/list_recursor.sy +++ b/test/regress/regress1/sygus/list_recursor.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2 --uf-ho +; COMMAND-LINE: --sygus-out=status --lang=sygus2 --uf-ho (set-logic ALL) diff --git a/test/regress/regress1/sygus/rec-fun-swap.sy b/test/regress/regress1/sygus/rec-fun-swap.sy new file mode 100644 index 000000000..056d6a8fc --- /dev/null +++ b/test/regress/regress1/sygus/rec-fun-swap.sy @@ -0,0 +1,76 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status --lang=sygus2 + +(set-logic ALL) + +; The environment datatypes +(declare-datatype NVars ((x) (y))) + +(declare-datatype Pair ((pair (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 (pair var value) env) + (ite (= var (first (head env))) + (cons (pair 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) + (- 1) + (ite (= var (first (head env))) + (second (head env)) + (envSelect var (tail env)) + ) + ) + ) + +; Syntax for arithmetic expressions +(declare-datatype Aexp + ( + (Val (val Int)) + ) + ) + +; Function to evaluate arithmetic expressions +(define-fun-rec evalA ((env Env) (a Aexp)) Int + (val a) + ) + +; Syntax for commands +(declare-datatype Com + ( + (Skip) + (Assign (lhs NVars) (rhs Aexp)) + (CSeq (cBef Com) (aAft Com)) + ) + ) + +; Function to evaluate statements +(define-fun-rec evalC ((env Env) (c Com)) Env + (ite (is-Skip c) + env + (ite (is-Assign c) + (envStore (lhs c) (evalA env (rhs c)) env) + (evalC (evalC env (cBef c)) (aAft c))) + ) + ) + +(synth-fun prog () Com + ((C Com) (V NVars) (A Aexp) (I Int)) + ( + (C Com (Skip (Assign V A) (CSeq C C))) + (V NVars (x y)) + (A Aexp ((Val I))) + (I Int (0 1)) + ) +) + +(constraint (= (evalC (cons (pair y 0) (cons (pair x 1) nil)) prog) (cons (pair y 1) (cons (pair x 0) nil)))) + +(check-synth) diff --git a/test/regress/regress1/sygus/rec-fun-sygus.sy b/test/regress/regress1/sygus/rec-fun-sygus.sy index 13d4782d4..769e173de 100644 --- a/test/regress/regress1/sygus/rec-fun-sygus.sy +++ b/test/regress/regress1/sygus/rec-fun-sygus.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2 +; COMMAND-LINE: --sygus-out=status --lang=sygus2 (set-logic ALL) diff --git a/test/regress/regress1/sygus/rec-fun-while-1.sy b/test/regress/regress1/sygus/rec-fun-while-1.sy index c175094ee..e805fdc20 100644 --- a/test/regress/regress1/sygus/rec-fun-while-1.sy +++ b/test/regress/regress1/sygus/rec-fun-while-1.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --lang=sygus2 --sygus-rec-fun --no-e-matching --no-check-synth-sol +; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol (set-logic ALL) diff --git a/test/regress/regress1/sygus/rec-fun-while-2.sy b/test/regress/regress1/sygus/rec-fun-while-2.sy index 87a4f2a6e..7e32384b3 100644 --- a/test/regress/regress1/sygus/rec-fun-while-2.sy +++ b/test/regress/regress1/sygus/rec-fun-while-2.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --lang=sygus2 --sygus-rec-fun --no-e-matching --no-check-synth-sol +; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol (set-logic ALL) diff --git a/test/regress/regress1/sygus/rec-fun-while-infinite.sy b/test/regress/regress1/sygus/rec-fun-while-infinite.sy index 85f8268c5..b43b3d5e2 100644 --- a/test/regress/regress1/sygus/rec-fun-while-infinite.sy +++ b/test/regress/regress1/sygus/rec-fun-while-infinite.sy @@ -1,5 +1,5 @@ ; EXPECT: unknown -; COMMAND-LINE: --sygus-out=status --lang=sygus2 --sygus-rec-fun --no-e-matching --no-check-synth-sol +; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol (set-logic ALL) -- 2.30.2