From c110363ccf39c9415c1a32bda6273fe8221db182 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 20 Aug 2020 06:04:43 -0500 Subject: Split QuantElimSolver from SmtEngine (#4919) Towards refactoring SmtEngine / converting Expr -> Node. --- src/CMakeLists.txt | 2 + src/smt/command.cpp | 4 +- src/smt/quant_elim_solver.cpp | 106 ++++++++++++++++++++++++++ src/smt/quant_elim_solver.h | 93 ++++++++++++++++++++++ src/smt/smt_engine.cpp | 74 ++---------------- src/smt/smt_engine.h | 15 ++-- src/theory/quantifiers/sygus/synth_engine.cpp | 23 +++--- 7 files changed, 230 insertions(+), 87 deletions(-) create mode 100644 src/smt/quant_elim_solver.cpp create mode 100644 src/smt/quant_elim_solver.h (limited to 'src') diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 48bd99f44..f1e01a7cb 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -249,6 +249,8 @@ libcvc4_add_sources( smt/model_blocker.h smt/options_manager.cpp smt/options_manager.h + smt/quant_elim_solver.cpp + smt/quant_elim_solver.h smt/preprocessor.cpp smt/preprocessor.h smt/preprocess_proof_generator.cpp diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 99e0a6c25..88f04f885 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -2692,7 +2692,9 @@ void GetQuantifierEliminationCommand::invoke(SmtEngine* smtEngine) { try { - d_result = smtEngine->doQuantifierElimination(d_expr, d_doFull); + d_result = + smtEngine->getQuantifierElimination(Node::fromExpr(d_expr), d_doFull) + .toExpr(); d_commandStatus = CommandSuccess::instance(); } catch (exception& e) diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp new file mode 100644 index 000000000..89bd8615a --- /dev/null +++ b/src/smt/quant_elim_solver.cpp @@ -0,0 +1,106 @@ +/********************* */ +/*! \file quant_elim_solver.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 The solver for quantifier elimination queries + **/ + +#include "smt/quant_elim_solver.h" + +#include "smt/smt_solver.h" +#include "theory/quantifiers/extended_rewrite.h" +#include "theory/rewriter.h" +#include "theory/theory_engine.h" + +using namespace CVC4::theory; +using namespace CVC4::kind; + +namespace CVC4 { +namespace smt { + +QuantElimSolver::QuantElimSolver(SmtSolver& sms) : d_smtSolver(sms) {} + +QuantElimSolver::~QuantElimSolver() {} + +Node QuantElimSolver::getQuantifierElimination(Assertions& as, + Node q, + bool doFull) +{ + Trace("smt-qe") << "Do quantifier elimination " << q << std::endl; + if (q.getKind() != EXISTS && q.getKind() != FORALL) + { + throw ModalException( + "Expecting a quantified formula as argument to get-qe."); + } + NodeManager* nm = NodeManager::currentNM(); + // tag the quantified formula with the quant-elim attribute + TypeNode t = nm->booleanType(); + Node n_attr = nm->mkSkolem("qe", t, "Auxiliary variable for qe attr."); + std::vector node_values; + TheoryEngine* te = d_smtSolver.getTheoryEngine(); + Assert(te != nullptr); + te->setUserAttribute( + doFull ? "quant-elim" : "quant-elim-partial", n_attr, node_values, ""); + n_attr = nm->mkNode(INST_ATTRIBUTE, n_attr); + n_attr = nm->mkNode(INST_PATTERN_LIST, n_attr); + std::vector children; + children.push_back(q[0]); + children.push_back(q.getKind() == EXISTS ? q[1] : q[1].negate()); + children.push_back(n_attr); + Node ne = nm->mkNode(EXISTS, children); + Trace("smt-qe-debug") << "Query for quantifier elimination : " << ne + << std::endl; + Assert(ne.getNumChildren() == 3); + // We consider this to be an entailment check, which also avoids incorrect + // status reporting (see SmtEngineState::d_expectedStatus). + Result r = + d_smtSolver.checkSatisfiability(as, std::vector{ne}, false, true); + Trace("smt-qe") << "Query returned " << r << std::endl; + if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) + { + if (r.asSatisfiabilityResult().isSat() != Result::SAT && doFull) + { + Notice() + << "While performing quantifier elimination, unexpected result : " + << r << " for query."; + // failed, return original + return q; + } + std::vector inst_qs; + te->getInstantiatedQuantifiedFormulas(inst_qs); + Assert(inst_qs.size() <= 1); + Node ret; + if (inst_qs.size() == 1) + { + Node topq = inst_qs[0]; + Assert(topq.getKind() == FORALL); + Trace("smt-qe") << "Get qe for " << topq << std::endl; + ret = te->getInstantiatedConjunction(topq); + Trace("smt-qe") << "Returned : " << ret << std::endl; + if (q.getKind() == EXISTS) + { + ret = Rewriter::rewrite(ret.negate()); + } + } + else + { + ret = nm->mkConst(q.getKind() != EXISTS); + } + // do extended rewrite to minimize the size of the formula aggressively + theory::quantifiers::ExtendedRewriter extr(true); + ret = extr.extendedRewrite(ret); + return ret; + } + // otherwise, just true/false + return nm->mkConst(q.getKind() == EXISTS); +} + +} // namespace smt +} // namespace CVC4 diff --git a/src/smt/quant_elim_solver.h b/src/smt/quant_elim_solver.h new file mode 100644 index 000000000..0d300dca7 --- /dev/null +++ b/src/smt/quant_elim_solver.h @@ -0,0 +1,93 @@ +/********************* */ +/*! \file quant_elim_solver.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 The solver for quantifier elimination queries + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__SMT__QUANT_ELIM_SOLVER_H +#define CVC4__SMT__QUANT_ELIM_SOLVER_H + +#include "expr/node.h" +#include "smt/assertions.h" + +namespace CVC4 { +namespace smt { + +class SmtSolver; + +/** + * A solver for quantifier elimination queries. + * + * This class is responsible for responding to get-qe and get-qe-partial + * commands. It uses an underlying SmtSolver, which it queries for + * quantifier instantiations used for unsat which are in turn used for + * constructing the solution for the quantifier elimination query. + */ +class QuantElimSolver +{ + public: + QuantElimSolver(SmtSolver& sms); + ~QuantElimSolver(); + + /** + * This function takes as input a quantified formula q + * of the form: + * Q x1...xn. P( x1...xn, y1...yn ) + * where P( x1...xn, y1...yn ) is a quantifier-free + * formula in a logic that supports quantifier elimination. + * Currently, the only logics supported by quantifier + * elimination is LRA and LIA. + * + * This function returns a formula ret such that, given + * the current set of formulas A asserted to this SmtEngine : + * + * If doFull = true, then + * - ( A ^ q ) and ( A ^ ret ) are equivalent + * - ret is quantifier-free formula containing + * only free variables in y1...yn. + * + * If doFull = false, then + * - (A ^ q) => (A ^ ret) if Q is forall or + * (A ^ ret) => (A ^ q) if Q is exists, + * - ret is quantifier-free formula containing + * only free variables in y1...yn, + * - If Q is exists, let A^Q_n be the formula + * A ^ ~ret^Q_1 ^ ... ^ ~ret^Q_n + * where for each i=1,...n, formula ret^Q_i + * is the result of calling doQuantifierElimination + * for q with the set of assertions A^Q_{i-1}. + * Similarly, if Q is forall, then let A^Q_n be + * A ^ ret^Q_1 ^ ... ^ ret^Q_n + * where ret^Q_i is the same as above. + * In either case, we have that ret^Q_j will + * eventually be true or false, for some finite j. + * + * The former feature is quantifier elimination, and + * is run on invocations of the smt2 extended command get-qe. + * The latter feature is referred to as partial quantifier + * elimination, and is run on invocations of the smt2 + * extended command get-qe-disjunct, which can be used + * for incrementally computing the result of a + * quantifier elimination. + */ + Node getQuantifierElimination(Assertions& as, Node q, bool doFull); + + private: + /** The SMT solver, which is used during doQuantifierElimination. */ + SmtSolver& d_smtSolver; +}; + +} // namespace smt +} // namespace CVC4 + +#endif /* CVC4__SMT__QUANT_ELIM_SOLVER_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d4b7eecbf..59df10195 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -92,6 +92,7 @@ #include "smt/model_core_builder.h" #include "smt/options_manager.h" #include "smt/preprocessor.h" +#include "smt/quant_elim_solver.h" #include "smt/smt_engine_scope.h" #include "smt/smt_engine_state.h" #include "smt/smt_engine_stats.h" @@ -104,11 +105,6 @@ #include "theory/booleans/circuit_propagator.h" #include "theory/bv/theory_bv_rewriter.h" #include "theory/logic_info.h" -#include "theory/quantifiers/fun_def_process.h" -#include "theory/quantifiers/single_inv_partition.h" -#include "theory/quantifiers/sygus/synth_engine.h" -#include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" #include "theory/rewriter.h" #include "theory/sort_inference.h" #include "theory/strings/theory_strings.h" @@ -159,6 +155,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_definedFunctions(nullptr), d_sygusSolver(nullptr), d_abductSolver(nullptr), + d_quantElimSolver(nullptr), d_assignments(nullptr), d_defineCommands(), d_logic(), @@ -207,6 +204,8 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) new SmtSolver(*this, *d_state, d_resourceManager.get(), *d_pp, *d_stats)); // make the SyGuS solver d_sygusSolver.reset(new SygusSolver(*d_smtSolver, *d_pp, getUserContext())); + // make the quantifier elimination solver + d_quantElimSolver.reset(new QuantElimSolver(*d_smtSolver)); // The ProofManager is constructed before any other proof objects such as // SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are @@ -1892,75 +1891,14 @@ bool SmtEngine::getSynthSolutions(std::map& solMap) return d_sygusSolver->getSynthSolutions(solMap); } -Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) +Node SmtEngine::getQuantifierElimination(Node q, bool doFull, bool strict) { SmtScope smts(this); finishInit(); if(!d_logic.isPure(THEORY_ARITH) && strict){ Warning() << "Unexpected logic for quantifier elimination " << d_logic << endl; } - Trace("smt-qe") << "Do quantifier elimination " << e << std::endl; - Node n_e = Node::fromExpr( e ); - if (n_e.getKind() != kind::EXISTS && n_e.getKind() != kind::FORALL) - { - throw ModalException( - "Expecting a quantified formula as argument to get-qe."); - } - //tag the quantified formula with the quant-elim attribute - TypeNode t = NodeManager::currentNM()->booleanType(); - Node n_attr = NodeManager::currentNM()->mkSkolem("qe", t, "Auxiliary variable for qe attr."); - std::vector< Node > node_values; - TheoryEngine* te = getTheoryEngine(); - Assert(te != nullptr); - te->setUserAttribute( - doFull ? "quant-elim" : "quant-elim-partial", n_attr, node_values, ""); - n_attr = NodeManager::currentNM()->mkNode(kind::INST_ATTRIBUTE, n_attr); - n_attr = NodeManager::currentNM()->mkNode(kind::INST_PATTERN_LIST, n_attr); - std::vector< Node > e_children; - e_children.push_back( n_e[0] ); - e_children.push_back(n_e.getKind() == kind::EXISTS ? n_e[1] - : n_e[1].negate()); - e_children.push_back( n_attr ); - Node nn_e = NodeManager::currentNM()->mkNode( kind::EXISTS, e_children ); - Trace("smt-qe-debug") << "Query for quantifier elimination : " << nn_e << std::endl; - Assert(nn_e.getNumChildren() == 3); - Result r = checkSatInternal(std::vector{nn_e}, true, true); - Trace("smt-qe") << "Query returned " << r << std::endl; - if(r.asSatisfiabilityResult().isSat() != Result::UNSAT ) { - if( r.asSatisfiabilityResult().isSat() != Result::SAT && doFull ){ - Notice() - << "While performing quantifier elimination, unexpected result : " - << r << " for query."; - // failed, return original - return e; - } - std::vector< Node > inst_qs; - te->getInstantiatedQuantifiedFormulas(inst_qs); - Assert(inst_qs.size() <= 1); - Node ret_n; - if( inst_qs.size()==1 ){ - Node top_q = inst_qs[0]; - //Node top_q = Rewriter::rewrite( nn_e ).negate(); - Assert(top_q.getKind() == kind::FORALL); - Trace("smt-qe") << "Get qe for " << top_q << std::endl; - ret_n = te->getInstantiatedConjunction(top_q); - Trace("smt-qe") << "Returned : " << ret_n << std::endl; - if (n_e.getKind() == kind::EXISTS) - { - ret_n = Rewriter::rewrite(ret_n.negate()); - } - }else{ - ret_n = NodeManager::currentNM()->mkConst(n_e.getKind() != kind::EXISTS); - } - // do extended rewrite to minimize the size of the formula aggressively - theory::quantifiers::ExtendedRewriter extr(true); - ret_n = extr.extendedRewrite(ret_n); - return ret_n.toExpr(); - }else { - return NodeManager::currentNM() - ->mkConst(n_e.getKind() == kind::EXISTS) - .toExpr(); - } + return d_quantElimSolver->getQuantifierElimination(*d_asserts, q, doFull); } bool SmtEngine::getInterpol(const Node& conj, diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index a6688578d..28dc8726b 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -106,6 +106,7 @@ class Preprocessor; class SmtSolver; class SygusSolver; class AbductionSolver; +class QuantElimSolver; /** * Representation of a defined function. We keep these around in * SmtEngine to permit expanding definitions late (and lazily), to @@ -584,7 +585,7 @@ class CVC4_PUBLIC SmtEngine /** * Do quantifier elimination. * - * This function takes as input a quantified formula e + * This function takes as input a quantified formula q * of the form: * Q x1...xn. P( x1...xn, y1...yn ) * where P( x1...xn, y1...yn ) is a quantifier-free @@ -596,20 +597,20 @@ class CVC4_PUBLIC SmtEngine * the current set of formulas A asserted to this SmtEngine : * * If doFull = true, then - * - ( A ^ e ) and ( A ^ ret ) are equivalent + * - ( A ^ q ) and ( A ^ ret ) are equivalent * - ret is quantifier-free formula containing * only free variables in y1...yn. * * If doFull = false, then - * - (A ^ e) => (A ^ ret) if Q is forall or - * (A ^ ret) => (A ^ e) if Q is exists, + * - (A ^ q) => (A ^ ret) if Q is forall or + * (A ^ ret) => (A ^ q) if Q is exists, * - ret is quantifier-free formula containing * only free variables in y1...yn, * - If Q is exists, let A^Q_n be the formula * A ^ ~ret^Q_1 ^ ... ^ ~ret^Q_n * where for each i=1,...n, formula ret^Q_i * is the result of calling doQuantifierElimination - * for e with the set of assertions A^Q_{i-1}. + * for q with the set of assertions A^Q_{i-1}. * Similarly, if Q is forall, then let A^Q_n be * A ^ ret^Q_1 ^ ... ^ ret^Q_n * where ret^Q_i is the same as above. @@ -629,7 +630,7 @@ class CVC4_PUBLIC SmtEngine * * throw@ Exception */ - Expr doQuantifierElimination(const Expr& e, bool doFull, bool strict = true); + Node getQuantifierElimination(Node q, bool doFull, bool strict = true); /** * This method asks this SMT engine to find an interpolant with respect to @@ -1106,6 +1107,8 @@ class CVC4_PUBLIC SmtEngine /** The solver for abduction queries */ std::unique_ptr d_abductSolver; + /** The solver for quantifier elimination queries */ + std::unique_ptr d_quantElimSolver; /** * List of items for which to retrieve values using getAssignment(). */ diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index f8349c834..3e47c1155 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -233,27 +233,26 @@ void SynthEngine::assignConjecture(Node q) 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; + 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 - Node qe_res_n = Node::fromExpr(qe_res); - if (!expr::hasBoundVar(qe_res_n)) + if (!expr::hasBoundVar(qeRes)) { - qe_res_n = qe_res_n.substitute( + qeRes = qeRes.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); + qeRes = + nm->mkNode(EXISTS, nm->mkNode(BOUND_VAR_LIST, nqe_vars), qeRes); } 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 + qeRes = nm->mkNode(FORALL, q[0], qeRes, q[2]); + Trace("cegqi-qep") << "Converted conjecture after QE : " << qeRes << std::endl; - qe_res_n = Rewriter::rewrite(qe_res_n); - Node nq = qe_res_n; + qeRes = Rewriter::rewrite(qeRes); + Node nq = qeRes; // must assert it is equivalent to the original Node lem = q.eqNode(nq); Trace("cegqi-lemma") -- cgit v1.2.3