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
--- /dev/null
+/********************* */
+/*! \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<Node> 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<SmtEngine> 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<Node> all_vars;
+ sip.getAllVariables(all_vars);
+ std::vector<Node> si_vars;
+ sip.getSingleInvocationVariables(si_vars);
+ std::vector<Node> qe_vars;
+ std::vector<Node> 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<Node> orig;
+ std::vector<Node> 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<Node> 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
--- /dev/null
+/********************* */
+/*! \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 <string>
+#include <vector>
+#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 */
#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;
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<SynthConjecture>(
new SynthConjecture(d_quantEngine, this, d_statistics)));
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<Node> 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<SmtEngine> 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<Node> all_vars;
- sip.getAllVariables(all_vars);
- std::vector<Node> si_vars;
- sip.getSingleInvocationVariables(si_vars);
- std::vector<Node> qe_vars;
- std::vector<Node> 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<Node> orig;
- std::vector<Node> 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<Node> 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
#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"
* preregisterAssertion.
*/
SynthConjecture* d_conj;
+ /**
+ * The quantifier elimination preprocess module.
+ */
+ SygusQePreproc d_sqp;
/** The statistics */
SygusStatistics d_statistics;
/** assign quantified formula q as a conjecture
projects / cvc5.git / commitdiff