SmtScope smts(this);
Trace("smt") << "Check synth: " << e << std::endl;
Trace("smt-synth") << "Check synthesis conjecture: " << e << std::endl;
- Expr e_check = e;
- 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 conj = Node::fromExpr(e);
- if (conj.getKind() == kind::FORALL && conj[1].getKind() == kind::EXISTS)
- {
- Node conj_se = Node::fromExpr(expandDefinitions(conj[1][1].toExpr()));
-
- Trace("smt-synth") << "Compute single invocation for " << conj_se << "..."
- << std::endl;
- quantifiers::SingleInvocationPartition sip;
- std::vector<Node> funcs;
- funcs.insert(funcs.end(), conj[0].begin(), conj[0].end());
- sip.init(funcs, conj_se.negate());
- Trace("smt-synth") << "...finished, got:" << std::endl;
- sip.debugPrint("smt-synth");
-
- if (!sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation())
- {
- // create new smt engine to do quantifier elimination
- SmtEngine smt_qe(d_exprManager);
- smt_qe.setLogic(getLogicInfo());
- Trace("smt-synth") << "Property is non-ground single invocation, run "
- "QE to obtain single invocation."
- << std::endl;
- NodeManager* nm = NodeManager::currentNM();
- // 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(si_vars.begin(), si_vars.end(), v) == si_vars.end())
- {
- qe_vars.push_back(v);
- }
- else
- {
- nqe_vars.push_back(v);
- }
- }
- std::vector<Node> orig;
- std::vector<Node> subs;
- // skolemize non-qe variables
- for (unsigned i = 0; i < nqe_vars.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("smt-synth") << " subs : " << nqe_vars[i] << " -> " << k
- << std::endl;
- }
- std::vector<Node> 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("smt-synth") << " subs : " << fi << " -> " << k << std::endl;
- }
- Node conj_se_ngsi = sip.getFullSpecification();
- Trace("smt-synth") << "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(kind::EXISTS,
- nm->mkNode(kind::BOUND_VAR_LIST, qe_vars),
- conj_se_ngsi_subs.negate());
-
- Trace("smt-synth") << "Run quantifier elimination on "
- << conj_se_ngsi_subs << std::endl;
- Expr qe_res = smt_qe.doQuantifierElimination(
- conj_se_ngsi_subs.toExpr(), true, false);
- Trace("smt-synth") << "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(kind::EXISTS,
- nm->mkNode(kind::BOUND_VAR_LIST, nqe_vars),
- qe_res_n);
- }
- Assert(conj.getNumChildren() == 3);
- qe_res_n = nm->mkNode(kind::FORALL, conj[0], qe_res_n, conj[2]);
- Trace("smt-synth") << "Converted conjecture after QE : " << qe_res_n
- << std::endl;
- e_check = qe_res_n.toExpr();
- }
- }
- }
-
- return checkSatisfiability( e_check, true, false );
+ return checkSatisfiability(e, true, false);
}
Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore)
#include "theory/quantifiers/sygus/ce_guided_instantiation.h"
#include "options/quantifiers_options.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
#include "smt/smt_statistics_registry.h"
-#include "theory/theory_engine.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
+#include "theory/theory_engine.h"
using namespace CVC4::kind;
using namespace std;
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;
- d_conj->assign( q );
+ Node conj = q;
+ 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 " << conj << "..."
+ << std::endl;
+ quantifiers::SingleInvocationPartition sip;
+ std::vector<Node> 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");
+
+ 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<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(si_vars.begin(), si_vars.end(), v) == si_vars.end())
+ {
+ qe_vars.push_back(v);
+ }
+ else
+ {
+ nqe_vars.push_back(v);
+ }
+ }
+ 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> 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;
+
+ // 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;
+ }
+ }
+ d_conj->assign(conj);
}else{
Assert( d_conj->getEmbeddedConjecture()==q );
}
projects / cvc5.git / commitdiff