From 17d0499e11cc40e795a1a13ffa7b24f585372d9e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 21 Jul 2018 23:50:57 -0500 Subject: [PATCH] sygusComp2018: Improvements to CEGIS loop (#2187) --- src/options/quantifiers_options.toml | 8 ++ .../sygus/ce_guided_conjecture.cpp | 126 +++++++++++++----- .../quantifiers/sygus/ce_guided_conjecture.h | 8 +- 3 files changed, 107 insertions(+), 35 deletions(-) diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 8c7414fa7..3c0438d95 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1144,6 +1144,14 @@ header = "options/quantifiers_options.h" default = "false" help = "enumerate a stream of solutions instead of terminating after the first one" +[[option]] + name = "sygusVerifySubcall" + category = "regular" + long = "sygus-verify-subcall" + type = "bool" + default = "true" + help = "use separate copy of the SMT solver for verification lemmas in sygus" + [[option]] name = "sygusExtRew" category = "regular" diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index b2b00a31c..37cfc25f1 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -20,6 +20,9 @@ #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/first_order_model.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_attributes.h" @@ -270,8 +273,6 @@ void CegConjecture::doCheck(std::vector& lems) // constants here. if (options::sygusRepairConst() && !d_master->usingRepairConst()) { - Trace("cegqi-check") << "CegConjuncture : repair previous solution..." - << std::endl; // have we tried to repair the previous solution? // if not, call the repair constant utility unsigned ninst = d_cinfo[d_candidates[0]].d_inst.size(); @@ -283,6 +284,17 @@ void CegConjecture::doCheck(std::vector& lems) Assert(d_repair_index < d_cinfo[cprog].d_inst.size()); fail_cvs.push_back(d_cinfo[cprog].d_inst[d_repair_index]); } + if (Trace.isOn("cegqi-check")) + { + Trace("cegqi-check") << "CegConjuncture : repair previous solution "; + for (const Node& fc : fail_cvs) + { + std::stringstream ss; + Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, fc); + Trace("cegqi-check") << ss.str() << " "; + } + Trace("cegqi-check") << std::endl; + } d_repair_index++; if (d_sygus_rconst->repairSolution( d_candidates, fail_cvs, candidate_values, true)) @@ -347,13 +359,12 @@ void CegConjecture::doCheck(std::vector& lems) } //immediately skolemize inner existentials - d_set_ce_sk_vars = sk_refine; Node lem; - if (inst.getKind() == NOT && inst[0].getKind() == FORALL) + // introduce the skolem variables + std::vector sks; + if (constructed_cand) { - // introduce the skolem variables - std::vector sks; - if (constructed_cand) + if (inst.getKind() == NOT && inst[0].getKind() == FORALL) { std::vector vars; for (const Node& v : inst[0][0]) @@ -361,27 +372,25 @@ void CegConjecture::doCheck(std::vector& lems) Node sk = nm->mkSkolem("rsk", v.getType()); sks.push_back(sk); vars.push_back(v); + Trace("cegqi-check-debug") + << " introduce skolem " << sk << " for " << v << "\n"; } lem = inst[0][1].substitute( vars.begin(), vars.end(), sks.begin(), sks.end()); lem = lem.negate(); } - if (sk_refine) - { - d_ce_sk_vars.insert(d_ce_sk_vars.end(), sks.begin(), sks.end()); - } - Assert(!isGround()); - } - else - { - if (constructed_cand) + else { // use the instance itself lem = inst; } - // we add null so that one test of the conjecture for the empty - // substitution is checked } + if (sk_refine) + { + d_ce_sk_vars.insert(d_ce_sk_vars.end(), sks.begin(), sks.end()); + d_set_ce_sk_vars = true; + } + if (!lem.isNull()) { lem = Rewriter::rewrite( lem ); @@ -392,22 +401,52 @@ void CegConjecture::doCheck(std::vector& lems) // record the instantiation // this is used for remembering the solution recordInstantiation(candidate_values); - if (lem.isConst() && !lem.getConst() && options::sygusStream()) + Node query = lem; + if (query.isConst() && !query.getConst() && options::sygusStream()) { // short circuit the check // instead, we immediately print the current solution. // this saves us from introducing a check lemma and a new guard. printAndContinueStream(); + return; } - else + // This is the "verification lemma", which states + // either this conjecture does not have a solution, or candidate_values + // is a solution for this conjecture. + lem = nm->mkNode(OR, d_quant.negate(), query); + if (options::sygusVerifySubcall()) { - // This is the "verification lemma", which states - // either this conjecture does not have a solution, or candidate_values - // is a solution for this conjecture. - lem = nm->mkNode(OR, d_quant.negate(), lem); - lem = getStreamGuardedLemma(lem); - lems.push_back(lem); + Trace("cegqi-engine") << " *** Direct verify..." << std::endl; + SmtEngine verifySmt(nm->toExprManager()); + verifySmt.setLogic(smt::currentSmtEngine()->getLogicInfo()); + verifySmt.assertFormula(query.toExpr()); + Result r = verifySmt.checkSat(); + Trace("cegqi-engine") << " ...got " << r << std::endl; + if (r.asSatisfiabilityResult().isSat() == Result::SAT) + { + Trace("cegqi-engine") << " * Verification lemma failed for:\n "; + // do not send out + for (const Node& v : d_ce_sk_vars) + { + Node mv = Node::fromExpr(verifySmt.getValue(v.toExpr())); + Trace("cegqi-engine") << v << " -> " << mv << " "; + d_ce_sk_var_mvs.push_back(mv); + } + Trace("cegqi-engine") << std::endl; + return; + } + else if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) + { + // if the result in the subcall was unsatisfiable, we avoid + // rechecking, hence we drop "query" from the verification lemma + lem = d_quant.negate(); + } + // In the rare case that the subcall is unknown, we add the verification + // lemma in the main solver. This should only happen if the quantifier + // free logic is undecidable. } + lem = getStreamGuardedLemma(lem); + lems.push_back(lem); } } @@ -424,10 +463,19 @@ void CegConjecture::doRefine( std::vector< Node >& lems ){ { Trace("cegqi-refine") << "Get model values for skolems..." << std::endl; Assert(d_inner_vars.size() == d_ce_sk_vars.size()); - std::vector model_values; - getModelValues(d_ce_sk_vars, model_values); + if (d_ce_sk_var_mvs.empty()) + { + std::vector model_values; + getModelValues(d_ce_sk_vars, model_values); + sk_subs.insert(sk_subs.end(), model_values.begin(), model_values.end()); + } + else + { + Assert(d_ce_sk_var_mvs.size() == d_ce_sk_vars.size()); + sk_subs.insert( + sk_subs.end(), d_ce_sk_var_mvs.begin(), d_ce_sk_var_mvs.end()); + } sk_vars.insert(sk_vars.end(), d_inner_vars.begin(), d_inner_vars.end()); - sk_subs.insert(sk_subs.end(), model_values.begin(), model_values.end()); } else { @@ -460,6 +508,7 @@ void CegConjecture::doRefine( std::vector< Node >& lems ){ Trace("cegqi-refine") << "doRefine : finished" << std::endl; d_set_ce_sk_vars = false; d_ce_sk_vars.clear(); + d_ce_sk_var_mvs.clear(); } void CegConjecture::preregisterConjecture( Node q ) { @@ -612,6 +661,7 @@ void CegConjecture::printAndContinueStream() // thus, we clear information regarding the current refinement d_set_ce_sk_vars = false; d_ce_sk_vars.clear(); + d_ce_sk_var_mvs.clear(); // However, we need to exclude the current solution using an explicit // blocking clause, so that we proceed to the next solution. std::vector terms; @@ -643,7 +693,10 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation Assert( d_quant[0].getNumChildren()==d_embed_quant[0].getNumChildren() ); std::vector sols; std::vector statuses; - getSynthSolutionsInternal(sols, statuses, singleInvocation); + if (!getSynthSolutionsInternal(sols, statuses, singleInvocation)) + { + return; + } for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++) { Node sol = sols[i]; @@ -717,7 +770,10 @@ void CegConjecture::getSynthSolutions(std::map& sol_map, TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus(); std::vector sols; std::vector statuses; - getSynthSolutionsInternal(sols, statuses, singleInvocation); + if (!getSynthSolutionsInternal(sols, statuses, singleInvocation)) + { + return; + } for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++) { Node sol = sols[i]; @@ -744,7 +800,7 @@ void CegConjecture::getSynthSolutions(std::map& sol_map, } } -void CegConjecture::getSynthSolutionsInternal(std::vector& sols, +bool CegConjecture::getSynthSolutionsInternal(std::vector& sols, std::vector& statuses, bool singleInvocation) { @@ -761,10 +817,11 @@ void CegConjecture::getSynthSolutionsInternal(std::vector& sols, { Assert(d_ceg_si != NULL); sol = d_ceg_si->getSolution(i, tn, status, true); - if (!sol.isNull()) + if (sol.isNull()) { - sol = sol.getKind() == LAMBDA ? sol[1] : sol; + return false; } + sol = sol.getKind() == LAMBDA ? sol[1] : sol; } else { @@ -824,6 +881,7 @@ void CegConjecture::getSynthSolutionsInternal(std::vector& sols, sols.push_back(sol); statuses.push_back(status); } + return true; } Node CegConjecture::getSymmetryBreakingPredicate( diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/ce_guided_conjecture.h index 3f978ce66..0b6f0e1a8 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.h @@ -178,6 +178,12 @@ private: * skolems are analyzed during doRefine(). */ std::vector d_ce_sk_vars; + /** + * If we have already tested the satisfiability of the current verification + * lemma, this stores the model values of d_ce_sk_vars in the current + * (satisfiable, failed) verification lemma. + */ + std::vector d_ce_sk_var_mvs; /** * Whether the above vector has been set. We have this flag since the above * vector may be set to empty (e.g. for ground synthesis conjectures). @@ -232,7 +238,7 @@ private: * may set ( sols, status ) to ( { x+1, d_x() }, { 1, 0 } ), where d_x() is * the sygus datatype constructor corresponding to variable x. */ - void getSynthSolutionsInternal(std::vector& sols, + bool getSynthSolutionsInternal(std::vector& sols, std::vector& status, bool singleInvocation); //-------------------------------- sygus stream -- 2.30.2