From 7d859b19c2755dc5071f4bedbbeab8a37870e69a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 29 Sep 2021 16:23:27 -0500 Subject: [PATCH] Properly restrict PBE symmetry breaking for abduction queries (#7269) This ensures we infer when a conjecture is PBE based on the conjecture plus the side condition for abduction. This fixes issues where the sygus solver was over-pruning solutions for abduction queries. It also changes the names of internal symbols used for abduction/interpolation queries. These names are used when the experimental sygus-stream is used. These symbols are changed (from "A") to avoid confusion with user symbols. --- src/smt/abduction_solver.cpp | 2 +- src/smt/interpolation_solver.cpp | 2 +- .../quantifiers/sygus/sygus_enumerator_callback.cpp | 4 +--- src/theory/quantifiers/sygus/synth_conjecture.cpp | 13 +++++++++++-- test/regress/CMakeLists.txt | 1 + .../regress1/sygus/abduction-no-pbe-sym-break.smt2 | 11 +++++++++++ 6 files changed, 26 insertions(+), 7 deletions(-) create mode 100644 test/regress/regress1/sygus/abduction-no-pbe-sym-break.smt2 diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp index b66daefd3..3bdf13efb 100644 --- a/src/smt/abduction_solver.cpp +++ b/src/smt/abduction_solver.cpp @@ -53,7 +53,7 @@ bool AbductionSolver::getAbduct(const std::vector& axioms, conjn = conjn.negate(); d_abdConj = conjn; asserts.push_back(conjn); - std::string name("A"); + std::string name("__internal_abduct"); Node aconj = quantifiers::SygusAbduct::mkAbductionConjecture( name, asserts, axioms, grammarType); // should be a quantified conjecture with one function-to-synthesize diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp index 3e227fa31..ff8e14e9b 100644 --- a/src/smt/interpolation_solver.cpp +++ b/src/smt/interpolation_solver.cpp @@ -51,7 +51,7 @@ bool InterpolationSolver::getInterpol(const std::vector& axioms, << std::endl; // must expand definitions Node conjn = d_env.getTopLevelSubstitutions().apply(conj); - std::string name("A"); + std::string name("__internal_interpol"); quantifiers::SygusInterpol interpolSolver(d_env); if (interpolSolver.solveInterpolation( diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp b/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp index 1b5b3f5af..1170eee82 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp @@ -46,7 +46,7 @@ bool SygusEnumeratorCallback::addTerm(Node n, std::unordered_set& bterms) // First, must be unique up to rewriting if (bterms.find(bnr) != bterms.end()) { - Trace("sygus-enum-exc") << "Exclude: " << bn << std::endl; + Trace("sygus-enum-exc") << "Exclude (by rewriting): " << bn << std::endl; return false; } // insert to builtin term cache, regardless of whether it is redundant @@ -55,8 +55,6 @@ bool SygusEnumeratorCallback::addTerm(Node n, std::unordered_set& bterms) // callback-specific add term if (!addTermInternal(n, bn, bnr)) { - Trace("sygus-enum-exc") - << "Exclude: " << bn << " due to callback" << std::endl; return false; } Trace("sygus-enum-terms") << "tc(" << d_tn << "): term " << bn << std::endl; diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index ab2a73cb0..4fa8ba78e 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -204,7 +204,16 @@ void SynthConjecture::assign(Node q) } } // initialize the example inference utility - if (!d_exampleInfer->initialize(d_base_inst, d_candidates)) + // Notice that we must also consider the side condition when inferring + // whether the conjecture is PBE. This ensures we do not prune solutions + // that may satisfy the side condition based on equivalence-up-to-examples + // with solutions that do not. + Node conjForExamples = d_base_inst; + if (!d_embedSideCondition.isNull()) + { + conjForExamples = nm->mkNode(AND, d_embedSideCondition, d_base_inst); + } + if (d_exampleInfer!=nullptr && !d_exampleInfer->initialize(conjForExamples, d_candidates)) { // there is a contradictory example pair, the conjecture is infeasible. Node infLem = d_feasible_guard.negate(); @@ -761,7 +770,7 @@ EnumValueManager* SynthConjecture::getEnumValueManagerFor(Node e) } // otherwise, allocate it Node f = d_tds->getSynthFunForEnumerator(e); - bool hasExamples = (d_exampleInfer->hasExamples(f) + bool hasExamples = (d_exampleInfer != nullptr && d_exampleInfer->hasExamples(f) && d_exampleInfer->getNumExamples(f) != 0); d_enumManager[e].reset(new EnumValueManager( d_env, d_qstate, d_qim, d_treg, d_stats, e, hasExamples)); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 55b932f81..3bfe356fa 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2283,6 +2283,7 @@ set(regress_1_tests regress1/sygus/abd-simple-conj-4.smt2 regress1/sygus/abduction_1255.corecstrs.readable.smt2 regress1/sygus/abduction_streq.readable.smt2 + regress1/sygus/abduction-no-pbe-sym-break.smt2 regress1/sygus/abv.sy regress1/sygus/array-grammar-store.sy regress1/sygus/array_search_5-Q-easy.sy diff --git a/test/regress/regress1/sygus/abduction-no-pbe-sym-break.smt2 b/test/regress/regress1/sygus/abduction-no-pbe-sym-break.smt2 new file mode 100644 index 000000000..79fa4f230 --- /dev/null +++ b/test/regress/regress1/sygus/abduction-no-pbe-sym-break.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --produce-abducts +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 + +(set-logic UF) +(set-option :produce-abducts true) +(declare-const A Bool) +(declare-const B Bool) +(declare-const C Bool) +(assert (=> A C)) +(get-abduct D (=> A B)) -- 2.30.2