From bd0cf32db7d115e52e243b165a26edb319e91316 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 7 Apr 2021 15:28:47 -0500 Subject: [PATCH] Fixes for abducts (#6279) Fixes benchmarks 2 and 3 from #5848. --- src/smt/smt_engine.cpp | 4 +++- src/theory/quantifiers/sygus/sygus_abduct.cpp | 9 ++++++--- src/theory/quantifiers/sygus/synth_conjecture.cpp | 8 ++++++-- .../regress1/sygus/issue5848-3-trivial-no-abduct.smt2 | 5 +++++ 4 files changed, 20 insertions(+), 6 deletions(-) create mode 100644 test/regress/regress1/sygus/issue5848-3-trivial-no-abduct.smt2 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index a925c04ab..bb14232bb 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -337,8 +337,10 @@ SmtEngine::~SmtEngine() d_asserts.reset(nullptr); d_model.reset(nullptr); + d_abductSolver.reset(nullptr); + d_interpolSolver.reset(nullptr); + d_quantElimSolver.reset(nullptr); d_sygusSolver.reset(nullptr); - d_smtSolver.reset(nullptr); d_stats.reset(nullptr); diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp index 278d708ee..5cffda78f 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.cpp +++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp @@ -123,7 +123,7 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, abvl = agtsd.getSygusVarList(); Assert(!abvl.isNull() && abvl.getKind() == BOUND_VAR_LIST); } - else + else if (!varlist.empty()) { // the bound variable list of the abduct-to-synthesize is determined by // the variable list above @@ -166,8 +166,11 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, aconj = aconj.substitute(syms.begin(), syms.end(), vars.begin(), vars.end()); Trace("sygus-abduct") << "---> Assumptions: " << aconj << std::endl; Node sc = nm->mkNode(AND, aconj, abdApp); - Node vbvl = nm->mkNode(BOUND_VAR_LIST, vars); - sc = nm->mkNode(EXISTS, vbvl, sc); + if (!vars.empty()) + { + Node vbvl = nm->mkNode(BOUND_VAR_LIST, vars); + sc = nm->mkNode(EXISTS, vbvl, sc); + } Node sygusScVar = sm->mkDummySkolem("sygus_sc", nm->booleanType()); sygusScVar.setAttribute(theory::SygusSideConditionAttribute(), sc); Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusScVar); diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index f63941b1c..6db632b11 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -180,7 +180,7 @@ void SynthConjecture::assign(Node q) // construct base instantiation d_base_inst = Rewriter::rewrite(d_qim.getInstantiate()->getInstantiation( d_embed_quant, vars, d_candidates)); - if (!d_embedSideCondition.isNull()) + if (!d_embedSideCondition.isNull() && !vars.empty()) { d_embedSideCondition = d_embedSideCondition.substitute( vars.begin(), vars.end(), d_candidates.begin(), d_candidates.end()); @@ -641,8 +641,12 @@ bool SynthConjecture::checkSideCondition(const std::vector& cvals) const { if (!d_embedSideCondition.isNull()) { - Node sc = d_embedSideCondition.substitute( + Node sc = d_embedSideCondition; + if (!cvals.empty()) + { + sc = sc.substitute( d_candidates.begin(), d_candidates.end(), cvals.begin(), cvals.end()); + } Trace("sygus-engine") << "Check side condition..." << std::endl; Trace("cegqi-debug") << "Check side condition : " << sc << std::endl; Result r = checkWithSubsolver(sc); diff --git a/test/regress/regress1/sygus/issue5848-3-trivial-no-abduct.smt2 b/test/regress/regress1/sygus/issue5848-3-trivial-no-abduct.smt2 new file mode 100644 index 000000000..b64e27b45 --- /dev/null +++ b/test/regress/regress1/sygus/issue5848-3-trivial-no-abduct.smt2 @@ -0,0 +1,5 @@ +; COMMAND-LINE: --produce-abducts +; EXPECT: none +(set-logic ALL) +(assert (= 0.0 (sqrt 1.0))) +(get-abduct A false) -- 2.30.2