From: Andrew Reynolds Date: Tue, 7 Aug 2018 22:57:39 +0000 (-0500) Subject: Wait to do sygus qe preprocess until full effort check (#2282) X-Git-Tag: cvc5-1.0.0~4806 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=82515cbaef14918c7ce825e29a30de01c13d90ac;p=cvc5.git Wait to do sygus qe preprocess until full effort check (#2282) --- diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp index 919a8f008..378c2f1d7 100644 --- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp @@ -52,6 +52,19 @@ QuantifiersModule::QEffort CegInstantiation::needsModel(Theory::Effort e) void CegInstantiation::check(Theory::Effort e, QEffort quant_e) { + // if we are waiting to assign the conjecture, do it now + if (!d_waiting_conj.isNull()) + { + Node q = d_waiting_conj; + d_waiting_conj = Node::null(); + if (!d_conj->isAssigned()) + { + if (!assignConjecture(q)) + { + return; + } + } + } unsigned echeck = d_conj->isSingleInvocation() ? QEFFORT_STANDARD : QEFFORT_MODEL; if( quant_e==echeck ){ @@ -79,134 +92,152 @@ void CegInstantiation::check(Theory::Effort e, QEffort quant_e) } } -void CegInstantiation::registerQuantifier( Node q ) { - if( d_quantEngine->getOwner( q )==this ){ // && d_eval_axioms.find( q )==d_eval_axioms.end() ){ - if( !d_conj->isAssigned() ){ - Trace("cegqi") << "Register conjecture : " << q << std::endl; - Node conj = q; - if (options::sygusQePreproc()) +bool CegInstantiation::assignConjecture(Node q) +{ + if (d_conj->isAssigned()) + { + return false; + } + if (options::sygusQePreproc()) + { + // the following does quantifier elimination as a preprocess step + // for "non-ground single invocation synthesis conjectures": + // exists f. forall xy. P[ f(x), x, y ] + // We run quantifier elimination: + // exists y. P[ z, x, y ] ----> Q[ z, x ] + // Where we replace the original conjecture with: + // exists f. forall x. Q[ f(x), x ] + // For more details, see Example 6 of Reynolds et al. SYNT 2017. + Node body = q[1]; + if (body.getKind() == NOT && body[0].getKind() == FORALL) + { + body = body[0][1]; + } + NodeManager* nm = NodeManager::currentNM(); + Trace("cegqi-qep") << "Compute single invocation for " << q << "..." + << std::endl; + quantifiers::SingleInvocationPartition sip; + std::vector funcs; + funcs.insert(funcs.end(), q[0].begin(), q[0].end()); + sip.init(funcs, body); + Trace("cegqi-qep") << "...finished, got:" << std::endl; + sip.debugPrint("cegqi-qep"); + + if (!sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation()) + { + // create new smt engine to do quantifier elimination + SmtEngine smt_qe(nm->toExprManager()); + smt_qe.setLogic(smt::currentSmtEngine()->getLogicInfo()); + Trace("cegqi-qep") << "Property is non-ground single invocation, run " + "QE to obtain single invocation." + << std::endl; + // partition variables + std::vector all_vars; + sip.getAllVariables(all_vars); + std::vector si_vars; + sip.getSingleInvocationVariables(si_vars); + std::vector qe_vars; + std::vector nqe_vars; + for (unsigned i = 0, size = all_vars.size(); i < size; i++) { - // the following does quantifier elimination as a preprocess step - // for "non-ground single invocation synthesis conjectures": - // exists f. forall xy. P[ f(x), x, y ] - // We run quantifier elimination: - // exists y. P[ z, x, y ] ----> Q[ z, x ] - // Where we replace the original conjecture with: - // exists f. forall x. Q[ f(x), x ] - // For more details, see Example 6 of Reynolds et al. SYNT 2017. - Node body = q[1]; - if (body.getKind() == NOT && body[0].getKind() == FORALL) + Node v = all_vars[i]; + if (std::find(si_vars.begin(), si_vars.end(), v) == si_vars.end()) { - body = body[0][1]; + qe_vars.push_back(v); } - NodeManager* nm = NodeManager::currentNM(); - Trace("cegqi-qep") << "Compute single invocation for " << conj << "..." + else + { + nqe_vars.push_back(v); + } + } + std::vector orig; + std::vector subs; + // skolemize non-qe variables + for (unsigned i = 0, size = nqe_vars.size(); i < size; i++) + { + Node k = nm->mkSkolem( + "k", nqe_vars[i].getType(), "qe for non-ground single invocation"); + orig.push_back(nqe_vars[i]); + subs.push_back(k); + Trace("cegqi-qep") << " subs : " << nqe_vars[i] << " -> " << k << std::endl; - quantifiers::SingleInvocationPartition sip; - std::vector funcs; - funcs.insert(funcs.end(), conj[0].begin(), conj[0].end()); - sip.init(funcs, body); - Trace("cegqi-qep") << "...finished, got:" << std::endl; - sip.debugPrint("cegqi-qep"); + } + std::vector funcs; + sip.getFunctions(funcs); + for (unsigned i = 0, size = funcs.size(); i < size; i++) + { + Node f = funcs[i]; + Node fi = sip.getFunctionInvocationFor(f); + Node fv = sip.getFirstOrderVariableForFunction(f); + Assert(!fi.isNull()); + orig.push_back(fi); + Node k = + nm->mkSkolem("k", + fv.getType(), + "qe for function in non-ground single invocation"); + subs.push_back(k); + Trace("cegqi-qep") << " subs : " << fi << " -> " << k << std::endl; + } + Node conj_se_ngsi = sip.getFullSpecification(); + Trace("cegqi-qep") << "Full specification is " << conj_se_ngsi + << std::endl; + Node conj_se_ngsi_subs = conj_se_ngsi.substitute( + orig.begin(), orig.end(), subs.begin(), subs.end()); + Assert(!qe_vars.empty()); + conj_se_ngsi_subs = nm->mkNode(EXISTS, + nm->mkNode(BOUND_VAR_LIST, qe_vars), + conj_se_ngsi_subs.negate()); - if (!sip.isPurelySingleInvocation() - && sip.isNonGroundSingleInvocation()) - { - // create new smt engine to do quantifier elimination - SmtEngine smt_qe(nm->toExprManager()); - smt_qe.setLogic(smt::currentSmtEngine()->getLogicInfo()); - Trace("cegqi-qep") << "Property is non-ground single invocation, run " - "QE to obtain single invocation." - << std::endl; - // partition variables - std::vector all_vars; - sip.getAllVariables(all_vars); - std::vector si_vars; - sip.getSingleInvocationVariables(si_vars); - std::vector qe_vars; - std::vector nqe_vars; - for (unsigned i = 0, size = all_vars.size(); i < size; i++) - { - Node v = all_vars[i]; - if (std::find(si_vars.begin(), si_vars.end(), v) == si_vars.end()) - { - qe_vars.push_back(v); - } - else - { - nqe_vars.push_back(v); - } - } - std::vector orig; - std::vector subs; - // skolemize non-qe variables - for (unsigned i = 0, size = nqe_vars.size(); i < size; i++) - { - Node k = nm->mkSkolem("k", - nqe_vars[i].getType(), - "qe for non-ground single invocation"); - orig.push_back(nqe_vars[i]); - subs.push_back(k); - Trace("cegqi-qep") - << " subs : " << nqe_vars[i] << " -> " << k << std::endl; - } - std::vector funcs; - sip.getFunctions(funcs); - for (unsigned i = 0, size = funcs.size(); i < size; i++) - { - Node f = funcs[i]; - Node fi = sip.getFunctionInvocationFor(f); - Node fv = sip.getFirstOrderVariableForFunction(f); - Assert(!fi.isNull()); - orig.push_back(fi); - Node k = - nm->mkSkolem("k", - fv.getType(), - "qe for function in non-ground single invocation"); - subs.push_back(k); - Trace("cegqi-qep") << " subs : " << fi << " -> " << k << std::endl; - } - Node conj_se_ngsi = sip.getFullSpecification(); - Trace("cegqi-qep") - << "Full specification is " << conj_se_ngsi << std::endl; - Node conj_se_ngsi_subs = conj_se_ngsi.substitute( - orig.begin(), orig.end(), subs.begin(), subs.end()); - Assert(!qe_vars.empty()); - conj_se_ngsi_subs = nm->mkNode(EXISTS, - nm->mkNode(BOUND_VAR_LIST, qe_vars), - conj_se_ngsi_subs.negate()); + Trace("cegqi-qep") << "Run quantifier elimination on " + << conj_se_ngsi_subs << std::endl; + Expr qe_res = smt_qe.doQuantifierElimination( + conj_se_ngsi_subs.toExpr(), true, false); + Trace("cegqi-qep") << "Result : " << qe_res << std::endl; - Trace("cegqi-qep") << "Run quantifier elimination on " - << conj_se_ngsi_subs << std::endl; - Expr qe_res = smt_qe.doQuantifierElimination( - conj_se_ngsi_subs.toExpr(), true, false); - Trace("cegqi-qep") << "Result : " << qe_res << std::endl; + // create single invocation conjecture + Node qe_res_n = Node::fromExpr(qe_res); + qe_res_n = qe_res_n.substitute( + subs.begin(), subs.end(), orig.begin(), orig.end()); + if (!nqe_vars.empty()) + { + qe_res_n = + nm->mkNode(EXISTS, nm->mkNode(BOUND_VAR_LIST, nqe_vars), qe_res_n); + } + Assert(q.getNumChildren() == 3); + qe_res_n = nm->mkNode(FORALL, q[0], qe_res_n, q[2]); + Trace("cegqi-qep") << "Converted conjecture after QE : " << qe_res_n + << std::endl; + qe_res_n = Rewriter::rewrite(qe_res_n); + Node nq = qe_res_n; + // must assert it is equivalent to the original + Node lem = q.eqNode(nq); + Trace("cegqi-lemma") << "Cegqi::Lemma : qe-preprocess : " << lem + << std::endl; + d_quantEngine->getOutputChannel().lemma(lem); + // we've reduced the original to a preprocessed version, return + return false; + } + } + d_conj->assign(q); + return true; +} - // create single invocation conjecture - Node qe_res_n = Node::fromExpr(qe_res); - qe_res_n = qe_res_n.substitute( - subs.begin(), subs.end(), orig.begin(), orig.end()); - if (!nqe_vars.empty()) - { - qe_res_n = nm->mkNode( - EXISTS, nm->mkNode(BOUND_VAR_LIST, nqe_vars), qe_res_n); - } - Assert(conj.getNumChildren() == 3); - qe_res_n = nm->mkNode(FORALL, conj[0], qe_res_n, conj[2]); - Trace("cegqi-qep") - << "Converted conjecture after QE : " << qe_res_n << std::endl; - qe_res_n = Rewriter::rewrite(qe_res_n); - conj = qe_res_n; - // must assert it is equivalent to the original - Node lem = conj.eqNode(q); - Trace("cegqi-lemma") - << "Cegqi::Lemma : qe-preprocess : " << lem << std::endl; - d_quantEngine->getOutputChannel().lemma(lem); - // we've reduced the original to a preprocessed version, return - return; - } +void CegInstantiation::registerQuantifier(Node q) +{ + if (d_quantEngine->getOwner(q) == this) + { // && d_eval_axioms.find( q )==d_eval_axioms.end() ){ + if (!d_conj->isAssigned()) + { + Trace("cegqi") << "Register conjecture : " << q << std::endl; + if (options::sygusQePreproc()) + { + d_waiting_conj = q; + } + else + { + // assign it now + d_conj->assign(q); } - d_conj->assign(conj); }else{ Assert( d_conj->getEmbeddedConjecture()==q ); } diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.h b/src/theory/quantifiers/sygus/ce_guided_instantiation.h index 502244d25..03b4c4cc1 100644 --- a/src/theory/quantifiers/sygus/ce_guided_instantiation.h +++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.h @@ -33,7 +33,20 @@ private: CegConjecture * d_conj; /** last instantiation by single invocation module? */ bool d_last_inst_si; -private: + /** the conjecture we are waiting to assign */ + Node d_waiting_conj; + + private: + /** assign quantified formula q as the conjecture + * + * This method returns true if q was successfully assigned as the synthesis + * conjecture considered by this class. This method may return false, for + * instance, if this class determines that it would rather rewrite q to + * an equivalent form r (in which case this method returns the lemma + * q <=> r). An example of this is the quantifier elimination step + * option::sygusQePreproc(). + */ + bool assignConjecture(Node q); /** check conjecture */ void checkCegConjecture( CegConjecture * conj ); public: