From: Andrew Reynolds Date: Tue, 3 Nov 2020 01:56:32 +0000 (-0600) Subject: Move sygus qe preproc to its own file (#5375) X-Git-Tag: cvc5-1.0.0~2637 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cf36673d216949bb4306964c81488df3eb42b0c2;p=cvc5.git Move sygus qe preproc to its own file (#5375) --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 20a208939..e763565ad 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -743,6 +743,8 @@ libcvc4_add_sources( theory/quantifiers/sygus/sygus_pbe.h theory/quantifiers/sygus/sygus_process_conj.cpp theory/quantifiers/sygus/sygus_process_conj.h + theory/quantifiers/sygus/sygus_qe_preproc.cpp + theory/quantifiers/sygus/sygus_qe_preproc.h theory/quantifiers/sygus/sygus_repair_const.cpp theory/quantifiers/sygus/sygus_repair_const.h theory/quantifiers/sygus/sygus_stats.cpp diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp new file mode 100644 index 000000000..1a92cfc7f --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp @@ -0,0 +1,147 @@ +/********************* */ +/*! \file sygus_qe_preproc.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Sygus quantifier elimination preprocessor + **/ + +#include "theory/quantifiers/sygus/sygus_qe_preproc.h" + +#include "expr/node_algorithm.h" +#include "theory/quantifiers/single_inv_partition.h" +#include "theory/rewriter.h" +#include "theory/smt_engine_subsolver.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +SygusQePreproc::SygusQePreproc(QuantifiersEngine* qe) {} + +Node SygusQePreproc::preprocess(Node q) +{ + 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 funcs0; + funcs0.insert(funcs0.end(), q[0].begin(), q[0].end()); + sip.init(funcs0, body); + Trace("cegqi-qep") << "...finished, got:" << std::endl; + sip.debugPrint("cegqi-qep"); + + if (sip.isPurelySingleInvocation() || !sip.isNonGroundSingleInvocation()) + { + return Node::null(); + } + // create new smt engine to do quantifier elimination + std::unique_ptr smt_qe; + initializeSubsolver(smt_qe); + 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(funcs0.begin(), funcs0.end(), v) != funcs0.end()) + { + Trace("cegqi-qep") << "- fun var: " << v << std::endl; + } + else if (std::find(si_vars.begin(), si_vars.end(), v) == si_vars.end()) + { + qe_vars.push_back(v); + Trace("cegqi-qep") << "- qe var: " << v << std::endl; + } + else + { + nqe_vars.push_back(v); + Trace("cegqi-qep") << "- non qe var: " << v << std::endl; + } + } + 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 funcs1; + sip.getFunctions(funcs1); + for (unsigned i = 0, size = funcs1.size(); i < size; i++) + { + Node f = funcs1[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; + Node qeRes = smt_qe->getQuantifierElimination(conj_se_ngsi_subs, true, false); + Trace("cegqi-qep") << "Result : " << qeRes << std::endl; + + // create single invocation conjecture, if QE was successful + if (!expr::hasBoundVar(qeRes)) + { + qeRes = + qeRes.substitute(subs.begin(), subs.end(), orig.begin(), orig.end()); + if (!nqe_vars.empty()) + { + qeRes = nm->mkNode(EXISTS, nm->mkNode(BOUND_VAR_LIST, nqe_vars), qeRes); + } + Assert(q.getNumChildren() == 3); + qeRes = nm->mkNode(FORALL, q[0], qeRes, q[2]); + Trace("cegqi-qep") << "Converted conjecture after QE : " << qeRes + << std::endl; + qeRes = Rewriter::rewrite(qeRes); + Node nq = qeRes; + // must assert it is equivalent to the original + Node lem = q.eqNode(nq); + Trace("cegqi-lemma") << "Cegqi::Lemma : qe-preprocess : " << lem + << std::endl; + return lem; + } + return Node::null(); +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.h b/src/theory/quantifiers/sygus/sygus_qe_preproc.h new file mode 100644 index 000000000..2214d4beb --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.h @@ -0,0 +1,60 @@ +/********************* */ +/*! \file sygus_qe_preproc.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Sygus quantifier elimination preprocessor + **/ + +#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H +#define CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H + +#include +#include +#include "expr/node.h" +#include "expr/type.h" + +namespace CVC4 { +namespace theory { + +class QuantifiersEngine; + +namespace quantifiers { + +/** + * This module 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. + */ +class SygusQePreproc +{ + public: + SygusQePreproc(QuantifiersEngine* qe); + ~SygusQePreproc() {} + /** + * Preprocess. Returns a lemma of the form q = nq where nq is obtained + * by the quantifier elimination technique outlined above. + */ + Node preprocess(Node q); + + private: + /** Pointer to quantifiers engine */ + QuantifiersEngine* d_quantEngine; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H */ diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 5358a0aff..ba11490b5 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -21,7 +21,6 @@ #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" -#include "theory/smt_engine_subsolver.h" #include "theory/theory_engine.h" using namespace CVC4::kind; @@ -32,7 +31,10 @@ namespace theory { namespace quantifiers { SynthEngine::SynthEngine(QuantifiersEngine* qe, context::Context* c) - : QuantifiersModule(qe), d_tds(qe->getTermDatabaseSygus()) + : QuantifiersModule(qe), + d_tds(qe->getTermDatabaseSygus()), + d_conj(nullptr), + d_sqp(qe) { d_conjs.push_back(std::unique_ptr( new SynthConjecture(d_quantEngine, this, d_statistics))); @@ -143,130 +145,14 @@ void SynthEngine::assignConjecture(Node q) Trace("sygus-engine") << "SynthEngine::assignConjecture " << q << std::endl; 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) + Node lem = d_sqp.preprocess(q); + if (!lem.isNull()) { - body = body[0][1]; - } - NodeManager* nm = NodeManager::currentNM(); - Trace("cegqi-qep") << "Compute single invocation for " << q << "..." - << std::endl; - quantifiers::SingleInvocationPartition sip; - std::vector funcs0; - funcs0.insert(funcs0.end(), q[0].begin(), q[0].end()); - sip.init(funcs0, 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 - std::unique_ptr smt_qe; - initializeSubsolver(smt_qe); - 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(funcs0.begin(), funcs0.end(), v) != funcs0.end()) - { - Trace("cegqi-qep") << "- fun var: " << v << std::endl; - } - else if (std::find(si_vars.begin(), si_vars.end(), v) == si_vars.end()) - { - qe_vars.push_back(v); - Trace("cegqi-qep") << "- qe var: " << v << std::endl; - } - else - { - nqe_vars.push_back(v); - Trace("cegqi-qep") << "- non qe var: " << v << std::endl; - } - } - 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 + Trace("cegqi-lemma") << "Cegqi::Lemma : qe-preprocess : " << lem << std::endl; - } - std::vector funcs1; - sip.getFunctions(funcs1); - for (unsigned i = 0, size = funcs1.size(); i < size; i++) - { - Node f = funcs1[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; - Node qeRes = - smt_qe->getQuantifierElimination(conj_se_ngsi_subs, true, false); - Trace("cegqi-qep") << "Result : " << qeRes << std::endl; - - // create single invocation conjecture, if QE was successful - if (!expr::hasBoundVar(qeRes)) - { - qeRes = qeRes.substitute( - subs.begin(), subs.end(), orig.begin(), orig.end()); - if (!nqe_vars.empty()) - { - qeRes = - nm->mkNode(EXISTS, nm->mkNode(BOUND_VAR_LIST, nqe_vars), qeRes); - } - Assert(q.getNumChildren() == 3); - qeRes = nm->mkNode(FORALL, q[0], qeRes, q[2]); - Trace("cegqi-qep") << "Converted conjecture after QE : " << qeRes - << std::endl; - qeRes = Rewriter::rewrite(qeRes); - Node nq = qeRes; - // 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; - } + d_quantEngine->getOutputChannel().lemma(lem); + // we've reduced the original to a preprocessed version, return + return; } } // allocate a new synthesis conjecture if not assigned diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index d132054aa..25981748e 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -20,6 +20,7 @@ #include "context/cdhashmap.h" #include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/sygus/sygus_qe_preproc.h" #include "theory/quantifiers/sygus/sygus_stats.h" #include "theory/quantifiers/sygus/synth_conjecture.h" @@ -86,6 +87,10 @@ class SynthEngine : public QuantifiersModule * preregisterAssertion. */ SynthConjecture* d_conj; + /** + * The quantifier elimination preprocess module. + */ + SygusQePreproc d_sqp; /** The statistics */ SygusStatistics d_statistics; /** assign quantified formula q as a conjecture