From: Andrew Reynolds Date: Thu, 29 Nov 2018 18:09:19 +0000 (-0600) Subject: Infrastructure for sygus side conditions (#2729) X-Git-Tag: cvc5-1.0.0~4341 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=41b38de8b059d346764cd5ca112740aa09e1d163;p=cvc5.git Infrastructure for sygus side conditions (#2729) --- diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index ff906a95b..e3463df0d 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -267,6 +267,14 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){ Trace("quant-attr") << "Attribute : sygus : " << q << std::endl; qa.d_sygus = true; } + if (avar.hasAttribute(SygusSideConditionAttribute())) + { + qa.d_sygusSideCondition = + avar.getAttribute(SygusSideConditionAttribute()); + Trace("quant-attr") + << "Attribute : sygus side condition : " + << qa.d_sygusSideCondition << " : " << q << std::endl; + } if (avar.getAttribute(QuantNameAttribute())) { Trace("quant-attr") << "Attribute : quantifier name : " << avar diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 918269bbe..d3acc9434 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -73,6 +73,17 @@ struct SygusPrintProxyAttributeId typedef expr::Attribute SygusPrintProxyAttribute; +/** Attribute for specifying a "side condition" for a sygus conjecture + * + * A sygus conjecture of the form exists f. forall x. P[f,x] whose side + * condition is C[f] has the semantics exists f. C[f] ^ forall x. P[f,x]. + */ +struct SygusSideConditionAttributeId +{ +}; +typedef expr::Attribute + SygusSideConditionAttribute; + namespace quantifiers { /** Attribute priority for rewrite rules */ @@ -109,6 +120,8 @@ struct QAttributes Node d_fundef_f; /** is this formula marked as a sygus conjecture? */ bool d_sygus; + /** side condition for sygus conjectures */ + Node d_sygusSideCondition; /** if a rewrite rule, then this is the priority value for the rewrite rule */ int d_rr_priority; /** stores the maximum instantiation level allowed for this quantified formula diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index ff7bb6378..e25e8a225 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -87,10 +87,14 @@ void SynthConjecture::assign(Node q) // pre-simplify the quantified formula based on the process utility d_simp_quant = d_ceg_proc->preSimplify(d_quant); + // compute its attributes + QAttributes qa; + QuantAttributes::computeQuantAttributes(q, qa); + std::map templates; std::map templates_arg; // register with single invocation if applicable - if (d_qe->getQuantAttributes()->isSygus(q)) + if (qa.d_sygus) { d_ceg_si->initialize(d_simp_quant); d_simp_quant = d_ceg_si->getSimplifiedConjecture(); @@ -117,9 +121,18 @@ void SynthConjecture::assign(Node q) Trace("cegqi") << "SynthConjecture : converted to embedding : " << d_embed_quant << std::endl; + Node sc = qa.d_sygusSideCondition; + if (!sc.isNull()) + { + // convert to deep embedding + d_embedSideCondition = d_ceg_gc->convertToEmbedding(sc); + Trace("cegqi") << "SynthConjecture : side condition : " + << d_embedSideCondition << std::endl; + } + // we now finalize the single invocation module, based on the syntax // restrictions - if (d_qe->getQuantAttributes()->isSygus(q)) + if (qa.d_sygus) { d_ceg_si->finishInit(d_ceg_gc->isSyntaxRestricted()); } @@ -138,6 +151,11 @@ void SynthConjecture::assign(Node q) // construct base instantiation d_base_inst = Rewriter::rewrite(d_qe->getInstantiate()->getInstantiation( d_embed_quant, vars, d_candidates)); + if (!d_embedSideCondition.isNull()) + { + d_embedSideCondition = d_embedSideCondition.substitute( + vars.begin(), vars.end(), d_candidates.begin(), d_candidates.end()); + } Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl; // initialize the sygus constant repair utility @@ -509,6 +527,33 @@ bool SynthConjecture::doCheck(std::vector& lems) // record the instantiation // this is used for remembering the solution recordInstantiation(candidate_values); + + // check the side condition + Node sc; + if (!d_embedSideCondition.isNull() && constructed_cand) + { + sc = d_embedSideCondition.substitute(d_candidates.begin(), + d_candidates.end(), + candidate_values.begin(), + candidate_values.end()); + sc = Rewriter::rewrite(sc); + Trace("cegqi-engine") << "Check side condition..." << std::endl; + Trace("cegqi-debug") << "Check side condition : " << sc << std::endl; + SmtEngine scSmt(nm->toExprManager()); + scSmt.setLogic(smt::currentSmtEngine()->getLogicInfo()); + scSmt.assertFormula(sc.toExpr()); + Result r = scSmt.checkSat(); + Trace("cegqi-debug") << "...got side condition : " << r << std::endl; + if (r == Result::UNSAT) + { + // exclude the current solution TODO + excludeCurrentSolution(); + Trace("cegqi-engine") << "...failed side condition" << std::endl; + return false; + } + Trace("cegqi-engine") << "...passed side condition" << std::endl; + } + Node query = lem; bool success = false; if (query.isConst() && !query.getConst()) @@ -968,7 +1013,11 @@ void SynthConjecture::printAndContinueStream() // this output stream should coincide with wherever --dump-synth is output on Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); printSynthSolution(*nodeManagerOptions.getOut()); + excludeCurrentSolution(); +} +void SynthConjecture::excludeCurrentSolution() +{ // We will not refine the current candidate solution since it is a solution // thus, we clear information regarding the current refinement d_set_ce_sk_vars = false; diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 3a43eb83d..cf6178fdb 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -280,6 +280,11 @@ class SynthConjecture /** the asserted (negated) conjecture */ Node d_quant; + /** + * The side condition for solving the conjecture, after conversion to deep + * embedding. + */ + Node d_embedSideCondition; /** (negated) conjecture after simplification */ Node d_simp_quant; /** (negated) conjecture after simplification, conversion to deep embedding */ @@ -363,6 +368,8 @@ class SynthConjecture * output channel, which we refer to as a "stream exclusion lemma". */ void printAndContinueStream(); + /** exclude the current solution */ + void excludeCurrentSolution(); /** * Whether we have guarded a stream exclusion lemma when using sygusStream. * This is an optimization that allows us to guard only the first stream