diff options
| -rw-r--r-- | src/options/quantifiers_options.toml | 15 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_conjecture.cpp | 116 |
2 files changed, 109 insertions, 22 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index c40491a40..ad05aa5cd 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1147,6 +1147,21 @@ header = "options/quantifiers_options.h" read_only = true help = "when applicable, use grammar for choosing sample points" +[[option]] + name = "sygusRewSynthAccel" + category = "regular" + long = "sygus-rr-synth-accel" + type = "bool" + default = "false" + help = "add dynamic symmetry breaking clauses based on candidate rewrites" + +[[option]] + name = "sygusRewSynthCheck" + category = "regular" + long = "sygus-rr-synth-check" + type = "bool" + default = "false" + help = "use satisfiability check to verify correctness of candidate rewrites" # CEGQI applied to general quantified formulas diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index 2273db5ea..98855a7ca 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -19,12 +19,14 @@ #include "options/quantifiers_options.h" #include "printer/printer.h" #include "prop/prop_engine.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" -#include "theory/quantifiers/sygus/ce_guided_instantiation.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/skolemize.h" +#include "theory/quantifiers/sygus/ce_guided_instantiation.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" #include "theory/theory_engine.h" @@ -615,28 +617,98 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation // e.g. one that is alpha-equivalent to another. if (!eq_sol.isNull()) { - // The analog of terms sol and eq_sol are equivalent under sample - // points but do not rewrite to the same term. Hence, this indicates - // a candidate rewrite. - Printer* p = Printer::getPrinter(options::outputLanguage()); - out << "(candidate-rewrite "; - p->toStreamSygus(out, sol); - out << " "; - p->toStreamSygus(out, eq_sol); - out << ")" << std::endl; - ++(cei->d_statistics.d_candidate_rewrites_print); - // debugging information - if (Trace.isOn("sygus-rr-debug")) + ExtendedRewriter* er = sygusDb->getExtRewriter(); + Node solb = sygusDb->sygusToBuiltin(sol); + Node solbr = er->extendedRewrite(solb); + Node eq_solb = sygusDb->sygusToBuiltin(eq_sol); + Node eq_solr = er->extendedRewrite(eq_solb); + bool success = true; + bool verified = false; + // verify it if applicable + if (options::sygusRewSynthCheck()) + { + Trace("rr-check") << "Check candidate rewrite..." << std::endl; + // Notice we don't set produce-models. rrChecker takes the same + // options as the SmtEngine we belong to, where we ensure that + // produce-models is set. + SmtEngine rrChecker(NodeManager::currentNM()->toExprManager()); + rrChecker.setLogic(smt::currentSmtEngine()->getLogicInfo()); + Node crr = solbr.eqNode(eq_solr).negate(); + Trace("rr-check") + << "Check candidate rewrite : " << crr << std::endl; + rrChecker.assertFormula(crr.toExpr()); + Result r = rrChecker.checkSat(); + Trace("rr-check") << "...result : " << r << std::endl; + if (r.asSatisfiabilityResult().isUnknown() + || r.asSatisfiabilityResult().isSat()) + { + Trace("rr-check") + << "...rewrite does not hold for: " << std::endl; + success = false; + std::vector<Node> vars; + d_sampler[prog].getVariables(vars); + std::vector<Node> pt; + for (const Node& v : vars) + { + Node val = Node::fromExpr(rrChecker.getValue(v.toExpr())); + Trace("rr-check") << " " << v << " -> " << val << std::endl; + pt.push_back(val); + } + d_sampler[prog].addSamplePoint(pt); + // add the solution again + Node eq_sol_new = its->second.registerTerm(sol); + Assert(!r.asSatisfiabilityResult().isSat() + || eq_sol_new == sol); + } + else + { + verified = true; + } + } + if (success) { - ExtendedRewriter* er = sygusDb->getExtRewriter(); - Node solb = sygusDb->sygusToBuiltin(sol); - Node solbr = er->extendedRewrite(solb); - Node eq_solb = sygusDb->sygusToBuiltin(eq_sol); - Node eq_solr = er->extendedRewrite(eq_solb); - Trace("sygus-rr-debug") - << "; candidate #1 ext-rewrites to: " << solbr << std::endl; - Trace("sygus-rr-debug") - << "; candidate #2 ext-rewrites to: " << eq_solr << std::endl; + // The analog of terms sol and eq_sol are equivalent under sample + // points but do not rewrite to the same term. Hence, this + // indicates a candidate rewrite. + Printer* p = Printer::getPrinter(options::outputLanguage()); + out << "(" << (verified ? "" : "candidate-") << "rewrite "; + p->toStreamSygus(out, sol); + out << " "; + p->toStreamSygus(out, eq_sol); + out << ")" << std::endl; + ++(cei->d_statistics.d_candidate_rewrites_print); + // debugging information + if (Trace.isOn("sygus-rr-debug")) + { + Trace("sygus-rr-debug") + << "; candidate #1 ext-rewrites to: " << solbr << std::endl; + Trace("sygus-rr-debug") + << "; candidate #2 ext-rewrites to: " << eq_solr + << std::endl; + } + if (options::sygusRewSynthAccel()) + { + // Add a symmetry breaking clause that excludes the larger + // of sol and eq_sol. This effectively states that we no longer + // wish to enumerate any term that contains sol (resp. eq_sol) + // as a subterm. + Node exc_sol = sol; + unsigned sz = sygusDb->getSygusTermSize(sol); + unsigned eqsz = sygusDb->getSygusTermSize(eq_sol); + if (eqsz > sz) + { + sz = eqsz; + exc_sol = eq_sol; + } + TypeNode ptn = prog.getType(); + Node x = sygusDb->getFreeVar(ptn, 0); + Node lem = sygusDb->getExplain()->getExplanationForEquality( + x, exc_sol); + lem = lem.negate(); + Trace("sygus-rr-sb") + << "Symmetry breaking lemma : " << lem << std::endl; + sygusDb->registerSymBreakLemma(d_candidates[i], lem, ptn, sz); + } } } } |