Towards refactoring SmtEngine / converting Expr -> Node.
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
{
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)
--- /dev/null
+/********************* */
+/*! \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> 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<Node> 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<Node>{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<Node> 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
--- /dev/null
+/********************* */
+/*! \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 */
#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"
#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"
d_definedFunctions(nullptr),
d_sygusSolver(nullptr),
d_abductSolver(nullptr),
+ d_quantElimSolver(nullptr),
d_assignments(nullptr),
d_defineCommands(),
d_logic(),
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
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<Node>{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,
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
/**
* 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
* 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.
*
* 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
/** The solver for abduction queries */
std::unique_ptr<smt::AbductionSolver> d_abductSolver;
+ /** The solver for quantifier elimination queries */
+ std::unique_ptr<smt::QuantElimSolver> d_quantElimSolver;
/**
* List of items for which to retrieve values using getAssignment().
*/
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")
projects / cvc5.git / commitdiff