From 46eeb6a507c31b4ac65b0ef70c32898667097377 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Wed, 27 Nov 2019 17:52:36 -0300 Subject: Enable sygusRecFun by default and fixes SyGuS+RecFun+HO issues (#3502) --- src/theory/quantifiers/fun_def_evaluator.cpp | 41 ++++++++++++++-------- src/theory/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 +-- 5 files changed, 54 insertions(+), 40 deletions(-) (limited to 'src/theory') 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); } } -- cgit v1.2.3