diff options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 120 |
1 files changed, 1 insertions, 119 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 15b6e2fc9..ab14904ff 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4826,125 +4826,7 @@ Result SmtEngine::checkSynth(const Expr& e) 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) |