diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-12 11:14:08 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-10-12 11:14:08 -0500 |
commit | 3ce6e00068c02286704143d82d5f044fdb356516 (patch) | |
tree | 53d8403a8cc2c92db4cb815861f5c7cd56dee446 /src/smt | |
parent | e93c443a0bfb1a66909e8467b24da399be3d01ac (diff) |
Eliminate uses of Expr in SmtEngine interface (#5240)
This eliminates all use of Expr in the SmtEngine except in a few interfaces (setUserAttribute, getAssignment) whose signature is currently in question.
The next steps will be to (1) eliminate Expr from the smt/model.h interface, (2) replace Type by TypeNode in Sort.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/abduction_solver.cpp | 15 | ||||
-rw-r--r-- | src/smt/defined_function.h | 2 | ||||
-rw-r--r-- | src/smt/interpolation_solver.cpp | 19 | ||||
-rw-r--r-- | src/smt/interpolation_solver.h | 4 | ||||
-rw-r--r-- | src/smt/model_blocker.cpp | 23 | ||||
-rw-r--r-- | src/smt/model_blocker.h | 6 | ||||
-rw-r--r-- | src/smt/model_core_builder.cpp | 9 | ||||
-rw-r--r-- | src/smt/model_core_builder.h | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 283 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 64 |
10 files changed, 178 insertions, 249 deletions
diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp index 1de044fd4..3f03c00e2 100644 --- a/src/smt/abduction_solver.cpp +++ b/src/smt/abduction_solver.cpp @@ -39,12 +39,7 @@ bool AbductionSolver::getAbduct(const Node& goal, throw ModalException(msg); } Trace("sygus-abduct") << "SmtEngine::getAbduct: goal " << goal << std::endl; - std::vector<Expr> easserts = d_parent->getExpandedAssertions(); - std::vector<Node> axioms; - for (unsigned i = 0, size = easserts.size(); i < size; i++) - { - axioms.push_back(Node::fromExpr(easserts[i])); - } + std::vector<Node> axioms = d_parent->getExpandedAssertions(); std::vector<Node> asserts(axioms.begin(), axioms.end()); // must expand definitions Node conjn = d_parent->expandDefinitions(goal); @@ -139,8 +134,8 @@ void AbductionSolver::checkAbduct(Node a) Trace("check-abduct") << "SmtEngine::checkAbduct: get expanded assertions" << std::endl; - std::vector<Expr> asserts = d_parent->getExpandedAssertions(); - asserts.push_back(a.toExpr()); + std::vector<Node> asserts = d_parent->getExpandedAssertions(); + asserts.push_back(a); // two checks: first, consistent with assertions, second, implies negated goal // is unsatisfiable. @@ -153,7 +148,7 @@ void AbductionSolver::checkAbduct(Node a) initializeSubsolver(abdChecker); Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j << ": asserting formulas" << std::endl; - for (const Expr& e : asserts) + for (const Node& e : asserts) { abdChecker->assertFormula(e); } @@ -177,7 +172,7 @@ void AbductionSolver::checkAbduct(Node a) << "SmtEngine::checkAbduct: goal is " << d_abdConj << std::endl; // add the goal to the set of assertions Assert(!d_abdConj.isNull()); - asserts.push_back(d_abdConj.toExpr()); + asserts.push_back(d_abdConj); } else { diff --git a/src/smt/defined_function.h b/src/smt/defined_function.h index 0a4fc181f..c2e594fe7 100644 --- a/src/smt/defined_function.h +++ b/src/smt/defined_function.h @@ -34,7 +34,7 @@ class DefinedFunction { public: DefinedFunction() {} - DefinedFunction(Node func, std::vector<Node>& formals, Node formula) + DefinedFunction(Node func, const std::vector<Node>& formals, Node formula) : d_func(func), d_formals(formals), d_formula(formula) { } diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp index d2193d226..ffcb09a23 100644 --- a/src/smt/interpolation_solver.cpp +++ b/src/smt/interpolation_solver.cpp @@ -44,12 +44,7 @@ bool InterpolationSolver::getInterpol(const Node& conj, } Trace("sygus-interpol") << "SmtEngine::getInterpol: conjecture " << conj << std::endl; - std::vector<Expr> easserts = d_parent->getExpandedAssertions(); - std::vector<Node> axioms; - for (unsigned i = 0, size = easserts.size(); i < size; i++) - { - axioms.push_back(Node::fromExpr(easserts[i])); - } + std::vector<Node> axioms = d_parent->getExpandedAssertions(); // must expand definitions Node conjn = d_parent->expandDefinitions(conj); std::string name("A"); @@ -60,7 +55,7 @@ bool InterpolationSolver::getInterpol(const Node& conj, { if (options::checkInterpols()) { - checkInterpol(interpol.toExpr(), easserts, conj); + checkInterpol(interpol.toExpr(), axioms, conj); } return true; } @@ -73,8 +68,8 @@ bool InterpolationSolver::getInterpol(const Node& conj, Node& interpol) return getInterpol(conj, grammarType, interpol); } -void InterpolationSolver::checkInterpol(Expr interpol, - const std::vector<Expr>& easserts, +void InterpolationSolver::checkInterpol(Node interpol, + const std::vector<Node>& easserts, const Node& conj) { Assert(interpol.getType().isBoolean()); @@ -98,18 +93,18 @@ void InterpolationSolver::checkInterpol(Expr interpol, << ": asserting formulas" << std::endl; if (j == 0) { - for (const Expr& e : easserts) + for (const Node& e : easserts) { itpChecker->assertFormula(e); } - Expr negitp = interpol.notExpr(); + Node negitp = interpol.notNode(); itpChecker->assertFormula(negitp); } else { itpChecker->assertFormula(interpol); Assert(!conj.isNull()); - itpChecker->assertFormula(conj.toExpr().notExpr()); + itpChecker->assertFormula(conj.notNode()); } Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j << ": check the assertions" << std::endl; diff --git a/src/smt/interpolation_solver.h b/src/smt/interpolation_solver.h index 8e6d2cd14..096cf8983 100644 --- a/src/smt/interpolation_solver.h +++ b/src/smt/interpolation_solver.h @@ -71,8 +71,8 @@ class InterpolationSolver * the interpolation problem (interpol), and the solution implies the goal * (conj). If these criteria are not met, an internal error is thrown. */ - void checkInterpol(Expr interpol, - const std::vector<Expr>& easserts, + void checkInterpol(Node interpol, + const std::vector<Node>& easserts, const Node& conj); private: diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp index 8d232ed9e..9d15b5690 100644 --- a/src/smt/model_blocker.cpp +++ b/src/smt/model_blocker.cpp @@ -23,24 +23,15 @@ using namespace CVC4::kind; namespace CVC4 { -Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions, +Node ModelBlocker::getModelBlocker(const std::vector<Node>& assertions, theory::TheoryModel* m, options::BlockModelsMode mode, - const std::vector<Expr>& exprToBlock) + const std::vector<Node>& exprToBlock) { NodeManager* nm = NodeManager::currentNM(); // convert to nodes - std::vector<Node> tlAsserts; - for (const Expr& a : assertions) - { - Node an = Node::fromExpr(a); - tlAsserts.push_back(an); - } - std::vector<Node> nodesToBlock; - for (const Expr& eb : exprToBlock) - { - nodesToBlock.push_back(Node::fromExpr(eb)); - } + std::vector<Node> tlAsserts = assertions; + std::vector<Node> nodesToBlock = exprToBlock; Trace("model-blocker") << "Compute model blocker, assertions:" << std::endl; Node blocker; if (mode == options::BlockModelsMode::LITERALS) @@ -117,7 +108,7 @@ Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions, // rewrite, this ensures that e.g. the propositional value of // quantified formulas can be queried n = theory::Rewriter::rewrite(n); - Node vn = Node::fromExpr(m->getValue(n.toExpr())); + Node vn = m->getValue(n); Assert(vn.isConst()); if (vn.getConst<bool>() == cpol) { @@ -139,7 +130,7 @@ Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions, } else if (catom.getKind() == ITE) { - Node vcond = Node::fromExpr(m->getValue(cur[0].toExpr())); + Node vcond = m->getValue(cur[0]); Assert(vcond.isConst()); Node cond = cur[0]; Node branch; @@ -282,7 +273,7 @@ Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions, } } Trace("model-blocker") << "...model blocker is " << blocker << std::endl; - return blocker.toExpr(); + return blocker; } } /* namespace CVC4 */ diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h index 0ee40a88a..92d200d40 100644 --- a/src/smt/model_blocker.h +++ b/src/smt/model_blocker.h @@ -59,11 +59,11 @@ class ModelBlocker * our input. In other words, we do not return ~(x < 0) V ~(w < 0) since the * left disjunct is always false. */ - static Expr getModelBlocker( - const std::vector<Expr>& assertions, + static Node getModelBlocker( + const std::vector<Node>& assertions, theory::TheoryModel* m, options::BlockModelsMode mode, - const std::vector<Expr>& exprToBlock = std::vector<Expr>()); + const std::vector<Node>& exprToBlock = std::vector<Node>()); }; /* class TheoryModelCoreBuilder */ } // namespace CVC4 diff --git a/src/smt/model_core_builder.cpp b/src/smt/model_core_builder.cpp index c6a73df75..59dac63e8 100644 --- a/src/smt/model_core_builder.cpp +++ b/src/smt/model_core_builder.cpp @@ -20,7 +20,7 @@ using namespace CVC4::kind; namespace CVC4 { -bool ModelCoreBuilder::setModelCore(const std::vector<Expr>& assertions, +bool ModelCoreBuilder::setModelCore(const std::vector<Node>& assertions, Model* m, options::ModelCoresMode mode) { @@ -34,14 +34,9 @@ bool ModelCoreBuilder::setModelCore(const std::vector<Expr>& assertions, } // convert to nodes - std::vector<Node> asserts; - for (unsigned i = 0, size = assertions.size(); i < size; i++) - { - asserts.push_back(Node::fromExpr(assertions[i])); - } NodeManager* nm = NodeManager::currentNM(); - Node formula = asserts.size() > 1? nm->mkNode(AND, asserts) : asserts[0]; + Node formula = nm->mkAnd(assertions); std::vector<Node> vars; std::vector<Node> subs; Trace("model-core") << "Assignments: " << std::endl; diff --git a/src/smt/model_core_builder.h b/src/smt/model_core_builder.h index d4d2a8441..984c61d04 100644 --- a/src/smt/model_core_builder.h +++ b/src/smt/model_core_builder.h @@ -54,7 +54,7 @@ class ModelCoreBuilder * If m is not a model for assertions, this method returns false and m is * left unchanged. */ - static bool setModelCore(const std::vector<Expr>& assertions, + static bool setModelCore(const std::vector<Node>& assertions, Model* m, options::ModelCoresMode mode); }; /* class TheoryModelCoreBuilder */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ff45ce0ce..205865e16 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -71,7 +71,6 @@ #include "smt/abduction_solver.h" #include "smt/abstract_values.h" #include "smt/assertions.h" -#include "smt/node_command.h" #include "smt/defined_function.h" #include "smt/dump_manager.h" #include "smt/expr_names.h" @@ -80,6 +79,7 @@ #include "smt/logic_request.h" #include "smt/model_blocker.h" #include "smt/model_core_builder.h" +#include "smt/node_command.h" #include "smt/options_manager.h" #include "smt/preprocessor.h" #include "smt/proof_manager.h" @@ -94,6 +94,7 @@ #include "smt_util/boolean_simplification.h" #include "smt_util/nary_builder.h" #include "theory/logic_info.h" +#include "theory/quantifiers/quantifiers_attributes.h" #include "theory/rewriter.h" #include "theory/sort_inference.h" #include "theory/substitutions.h" @@ -114,20 +115,6 @@ using namespace CVC4::theory; namespace CVC4 { -// !!! Temporary until commands are migrated to the new API !!! -std::vector<Node> exprVectorToNodes(const std::vector<Expr>& exprs) -{ - std::vector<Node> nodes; - nodes.reserve(exprs.size()); - - for (Expr e : exprs) - { - nodes.push_back(Node::fromExpr(e)); - } - - return nodes; -} - SmtEngine::SmtEngine(ExprManager* em, Options* optr) : d_state(new SmtEngineState(*this)), d_exprManager(em), @@ -650,33 +637,36 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const return SExpr::parseListOfListOfAtoms(current_options); } -void SmtEngine::debugCheckFormals(const std::vector<Expr>& formals, Expr func) +void SmtEngine::debugCheckFormals(const std::vector<Node>& formals, Node func) { - for(std::vector<Expr>::const_iterator i = formals.begin(); i != formals.end(); ++i) { + for (std::vector<Node>::const_iterator i = formals.begin(); + i != formals.end(); + ++i) + { if((*i).getKind() != kind::BOUND_VARIABLE) { stringstream ss; ss << "All formal arguments to defined functions must be BOUND_VARIABLEs, but in the\n" << "definition of function " << func << ", formal\n" << " " << *i << "\n" << "has kind " << (*i).getKind(); - throw TypeCheckingException(func, ss.str()); + throw TypeCheckingException(func.toExpr(), ss.str()); } } } -void SmtEngine::debugCheckFunctionBody(Expr formula, - const std::vector<Expr>& formals, - Expr func) +void SmtEngine::debugCheckFunctionBody(Node formula, + const std::vector<Node>& formals, + Node func) { - Type formulaType = formula.getType(options::typeChecking()); - Type funcType = func.getType(); + TypeNode formulaType = formula.getType(options::typeChecking()); + TypeNode funcType = func.getType(); // We distinguish here between definitions of constants and functions, // because the type checking for them is subtly different. Perhaps we // should instead have SmtEngine::defineFunction() and // SmtEngine::defineConstant() for better clarity, although then that // doesn't match the SMT-LIBv2 standard... if(formals.size() > 0) { - Type rangeType = FunctionType(funcType).getRangeType(); + TypeNode rangeType = funcType.getRangeType(); if(! formulaType.isComparableTo(rangeType)) { stringstream ss; ss << "Type of defined function does not match its declaration\n" @@ -684,24 +674,24 @@ void SmtEngine::debugCheckFunctionBody(Expr formula, << "Declared type : " << rangeType << "\n" << "The body : " << formula << "\n" << "Body type : " << formulaType; - throw TypeCheckingException(func, ss.str()); + throw TypeCheckingException(func.toExpr(), ss.str()); } } else { if(! formulaType.isComparableTo(funcType)) { stringstream ss; ss << "Declared type of defined constant does not match its definition\n" << "The constant : " << func << "\n" - << "Declared type : " << funcType << " " << Type::getTypeNode(funcType)->getId() << "\n" + << "Declared type : " << funcType << "\n" << "The definition : " << formula << "\n" - << "Definition type: " << formulaType << " " << Type::getTypeNode(formulaType)->getId(); - throw TypeCheckingException(func, ss.str()); + << "Definition type: " << formulaType; + throw TypeCheckingException(func.toExpr(), ss.str()); } } } -void SmtEngine::defineFunction(Expr func, - const std::vector<Expr>& formals, - Expr formula, +void SmtEngine::defineFunction(Node func, + const std::vector<Node>& formals, + Node formula, bool global) { SmtScope smts(this); @@ -717,13 +707,12 @@ void SmtEngine::defineFunction(Expr func, std::vector<Node> nFormals; nFormals.reserve(formals.size()); - for (const Expr& formal : formals) + for (const Node& formal : formals) { - nFormals.push_back(formal.getNode()); + nFormals.push_back(formal); } - DefineFunctionNodeCommand nc( - ss.str(), func.getNode(), nFormals, formula.getNode()); + DefineFunctionNodeCommand nc(ss.str(), func, nFormals, formula); d_dumpm->addToModelCommandAndDump( nc, ExprManager::VAR_FLAG_DEFINED, true, "declarations"); @@ -731,36 +720,27 @@ void SmtEngine::defineFunction(Expr func, debugCheckFunctionBody(formula, formals, func); // Substitute out any abstract values in formula - Node formNode = d_absValues->substituteAbstractValues(Node::fromExpr(formula)); - - TNode funcNode = func.getTNode(); - vector<Node> formalsNodes; - for(vector<Expr>::const_iterator i = formals.begin(), - iend = formals.end(); - i != iend; - ++i) { - formalsNodes.push_back((*i).getNode()); - } - DefinedFunction def(funcNode, formalsNodes, formNode); + Node formNode = d_absValues->substituteAbstractValues(formula); + DefinedFunction def(func, formals, formNode); // Permit (check-sat) (define-fun ...) (get-value ...) sequences. // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks // d_haveAdditions = true; - Debug("smt") << "definedFunctions insert " << funcNode << " " << formNode << endl; + Debug("smt") << "definedFunctions insert " << func << " " << formNode << endl; if (global) { - d_definedFunctions->insertAtContextLevelZero(funcNode, def); + d_definedFunctions->insertAtContextLevelZero(func, def); } else { - d_definedFunctions->insert(funcNode, def); + d_definedFunctions->insert(func, def); } } void SmtEngine::defineFunctionsRec( - const std::vector<Expr>& funcs, - const std::vector<std::vector<Expr>>& formals, - const std::vector<Expr>& formulas, + const std::vector<Node>& funcs, + const std::vector<std::vector<Node>>& formals, + const std::vector<Node>& formulas, bool global) { SmtScope smts(this); @@ -789,22 +769,15 @@ void SmtEngine::defineFunctionsRec( if (Dump.isOn("raw-benchmark")) { - std::vector<Node> nFuncs = exprVectorToNodes(funcs); - std::vector<std::vector<Node>> nFormals; - for (const std::vector<Expr>& formal : formals) - { - nFormals.emplace_back(exprVectorToNodes(formal)); - } - std::vector<Node> nFormulas = exprVectorToNodes(formulas); getOutputManager().getPrinter().toStreamCmdDefineFunctionRec( - getOutputManager().getDumpOut(), nFuncs, nFormals, nFormulas); + getOutputManager().getDumpOut(), funcs, formals, formulas); } - ExprManager* em = getExprManager(); + NodeManager* nm = getNodeManager(); for (unsigned i = 0, size = funcs.size(); i < size; i++) { // we assert a quantified formula - Expr func_app; + Node func_app; // make the function application if (formals[i].empty()) { @@ -813,52 +786,49 @@ void SmtEngine::defineFunctionsRec( } else { - std::vector<Expr> children; + std::vector<Node> children; children.push_back(funcs[i]); children.insert(children.end(), formals[i].begin(), formals[i].end()); - func_app = em->mkExpr(kind::APPLY_UF, children); + func_app = nm->mkNode(kind::APPLY_UF, children); } - Expr lem = em->mkExpr(kind::EQUAL, func_app, formulas[i]); + Node lem = nm->mkNode(kind::EQUAL, func_app, formulas[i]); if (!formals[i].empty()) { // set the attribute to denote this is a function definition - std::string attr_name("fun-def"); - Expr aexpr = em->mkExpr(kind::INST_ATTRIBUTE, func_app); - aexpr = em->mkExpr(kind::INST_PATTERN_LIST, aexpr); - std::vector<Expr> expr_values; - std::string str_value; - setUserAttribute(attr_name, func_app, expr_values, str_value); + Node aexpr = nm->mkNode(kind::INST_ATTRIBUTE, func_app); + aexpr = nm->mkNode(kind::INST_PATTERN_LIST, aexpr); + FunDefAttribute fda; + func_app.setAttribute(fda, true); // make the quantified formula - Expr boundVars = em->mkExpr(kind::BOUND_VAR_LIST, formals[i]); - lem = em->mkExpr(kind::FORALL, boundVars, lem, aexpr); + Node boundVars = nm->mkNode(kind::BOUND_VAR_LIST, formals[i]); + lem = nm->mkNode(kind::FORALL, boundVars, lem, aexpr); } // assert the quantified formula // notice we don't call assertFormula directly, since this would // duplicate the output on raw-benchmark. - Node lemn = Node::fromExpr(lem); // add define recursive definition to the assertions - d_asserts->addDefineFunRecDefinition(lemn, global); + d_asserts->addDefineFunRecDefinition(lem, global); } } -void SmtEngine::defineFunctionRec(Expr func, - const std::vector<Expr>& formals, - Expr formula, +void SmtEngine::defineFunctionRec(Node func, + const std::vector<Node>& formals, + Node formula, bool global) { - std::vector<Expr> funcs; + std::vector<Node> funcs; funcs.push_back(func); - std::vector<std::vector<Expr> > formals_multi; + std::vector<std::vector<Node>> formals_multi; formals_multi.push_back(formals); - std::vector<Expr> formulas; + std::vector<Node> formulas; formulas.push_back(formula); defineFunctionsRec(funcs, formals_multi, formulas, global); } -bool SmtEngine::isDefinedFunction( Expr func ){ - Node nf = Node::fromExpr( func ); - Debug("smt") << "isDefined function " << nf << "?" << std::endl; - return d_definedFunctions->find(nf) != d_definedFunctions->end(); +bool SmtEngine::isDefinedFunction(Node func) +{ + Debug("smt") << "isDefined function " << func << "?" << std::endl; + return d_definedFunctions->find(func) != d_definedFunctions->end(); } Result SmtEngine::quickCheck() { @@ -942,7 +912,13 @@ void SmtEngine::notifyPostSolvePost() te->postsolve(); } -Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore) +Result SmtEngine::checkSat() +{ + Node nullNode; + return checkSat(nullNode); +} + +Result SmtEngine::checkSat(const Node& assumption, bool inUnsatCore) { if (Dump.isOn("benchmark")) { @@ -952,12 +928,13 @@ Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore) std::vector<Node> assump; if (!assumption.isNull()) { - assump.push_back(Node::fromExpr(assumption)); + assump.push_back(assumption); } return checkSatInternal(assump, inUnsatCore, false); } -Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore) +Result SmtEngine::checkSat(const std::vector<Node>& assumptions, + bool inUnsatCore) { if (Dump.isOn("benchmark")) { @@ -969,43 +946,33 @@ Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore) else { getOutputManager().getPrinter().toStreamCmdCheckSatAssuming( - getOutputManager().getDumpOut(), exprVectorToNodes(assumptions)); + getOutputManager().getDumpOut(), assumptions); } } - std::vector<Node> assumps; - for (const Expr& e : assumptions) - { - assumps.push_back(Node::fromExpr(e)); - } - return checkSatInternal(assumps, inUnsatCore, false); + return checkSatInternal(assumptions, inUnsatCore, false); } -Result SmtEngine::checkEntailed(const Expr& node, bool inUnsatCore) +Result SmtEngine::checkEntailed(const Node& node, bool inUnsatCore) { if (Dump.isOn("benchmark")) { getOutputManager().getPrinter().toStreamCmdQuery( - getOutputManager().getDumpOut(), node.getNode()); + getOutputManager().getDumpOut(), node); } - return checkSatInternal(node.isNull() - ? std::vector<Node>() - : std::vector<Node>{Node::fromExpr(node)}, - inUnsatCore, - true) + return checkSatInternal( + node.isNull() ? std::vector<Node>() : std::vector<Node>{node}, + inUnsatCore, + true) .asEntailmentResult(); } -Result SmtEngine::checkEntailed(const vector<Expr>& nodes, bool inUnsatCore) +Result SmtEngine::checkEntailed(const std::vector<Node>& nodes, + bool inUnsatCore) { - std::vector<Node> ns; - for (const Expr& e : nodes) - { - ns.push_back(Node::fromExpr(e)); - } - return checkSatInternal(ns, inUnsatCore, true).asEntailmentResult(); + return checkSatInternal(nodes, inUnsatCore, true).asEntailmentResult(); } -Result SmtEngine::checkSatInternal(const vector<Node>& assumptions, +Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions, bool inUnsatCore, bool isEntailmentCheck) { @@ -1272,12 +1239,12 @@ Node SmtEngine::getValue(const Node& ex) const return resultNode; } -vector<Expr> SmtEngine::getValues(const vector<Expr>& exprs) +std::vector<Node> SmtEngine::getValues(const std::vector<Node>& exprs) { - vector<Expr> result; - for (const Expr& e : exprs) + std::vector<Node> result; + for (const Node& e : exprs) { - result.push_back(getValue(e).toExpr()); + result.push_back(getValue(e)); } return result; } @@ -1400,7 +1367,7 @@ Model* SmtEngine::getModel() { { // If we enabled model cores, we compute a model core for m based on our // (expanded) assertions using the model core builder utility - std::vector<Expr> eassertsProc = getExpandedAssertions(); + std::vector<Node> eassertsProc = getExpandedAssertions(); ModelCoreBuilder::setModelCore(eassertsProc, m, options::modelCoresMode()); } m->d_inputName = d_state->getFilename(); @@ -1431,13 +1398,13 @@ Result SmtEngine::blockModel() } // get expanded assertions - std::vector<Expr> eassertsProc = getExpandedAssertions(); - Expr eblocker = ModelBlocker::getModelBlocker( + std::vector<Node> eassertsProc = getExpandedAssertions(); + Node eblocker = ModelBlocker::getModelBlocker( eassertsProc, m, options::blockModelsMode()); - return assertFormula(Node::fromExpr(eblocker)); + return assertFormula(eblocker); } -Result SmtEngine::blockModelValues(const std::vector<Expr>& exprs) +Result SmtEngine::blockModelValues(const std::vector<Node>& exprs) { Trace("smt") << "SMT blockModelValues()" << endl; SmtScope smts(this); @@ -1447,20 +1414,20 @@ Result SmtEngine::blockModelValues(const std::vector<Expr>& exprs) if (Dump.isOn("benchmark")) { getOutputManager().getPrinter().toStreamCmdBlockModelValues( - getOutputManager().getDumpOut(), exprVectorToNodes(exprs)); + getOutputManager().getDumpOut(), exprs); } TheoryModel* m = getAvailableModel("block model values"); // get expanded assertions - std::vector<Expr> eassertsProc = getExpandedAssertions(); + std::vector<Node> eassertsProc = getExpandedAssertions(); // we always do block model values mode here - Expr eblocker = ModelBlocker::getModelBlocker( + Node eblocker = ModelBlocker::getModelBlocker( eassertsProc, m, options::BlockModelsMode::VALUES, exprs); - return assertFormula(Node::fromExpr(eblocker)); + return assertFormula(eblocker); } -std::pair<Expr, Expr> SmtEngine::getSepHeapAndNilExpr(void) +std::pair<Node, Node> SmtEngine::getSepHeapAndNilExpr(void) { if (!d_logic.isTheoryEnabled(THEORY_SEP)) { @@ -1479,27 +1446,26 @@ std::pair<Expr, Expr> SmtEngine::getSepHeapAndNilExpr(void) << "SmtEngine::getSepHeapAndNilExpr(): failed to obtain heap/nil " "expressions from theory model."; } - return std::make_pair(heap, nil); + return std::make_pair(Node::fromExpr(heap), Node::fromExpr(nil)); } -std::vector<Expr> SmtEngine::getExpandedAssertions() +std::vector<Node> SmtEngine::getExpandedAssertions() { - std::vector<Expr> easserts = getAssertions(); + std::vector<Node> easserts = getAssertions(); // must expand definitions - std::vector<Expr> eassertsProc; + std::vector<Node> eassertsProc; std::unordered_map<Node, Node, NodeHashFunction> cache; - for (const Expr& e : easserts) + for (const Node& e : easserts) { - Node ea = Node::fromExpr(e); - Node eae = d_pp->expandDefinitions(ea, cache); - eassertsProc.push_back(eae.toExpr()); + Node eae = d_pp->expandDefinitions(e, cache); + eassertsProc.push_back(eae); } return eassertsProc; } -Expr SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; } +Node SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; } -Expr SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; } +Node SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; } UnsatCore SmtEngine::getUnsatCoreInternal() { @@ -1618,7 +1584,7 @@ void SmtEngine::checkModel(bool hardFailure) { // We'll first do some checks, then add to our substitution map // the mapping: function symbol |-> value - Expr func = c->getFunction().toExpr(); + Node func = c->getFunction(); Node val = m->getValue(func); Notice() << "SmtEngine::checkModel(): adding substitution: " << func << " |-> " << val << endl; @@ -1634,7 +1600,8 @@ void SmtEngine::checkModel(bool hardFailure) { // [func->func2] and checking equality of the Nodes. // (this just a way to check if func is in n.) SubstitutionMap subs(&fakeContext); - Node func2 = NodeManager::currentNM()->mkSkolem("", TypeNode::fromType(func.getType()), "", NodeManager::SKOLEM_NO_NOTIFY); + Node func2 = NodeManager::currentNM()->mkSkolem( + "", func.getType(), "", NodeManager::SKOLEM_NO_NOTIFY); subs.addSubstitution(func, func2); if(subs.apply(n) != n) { Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE DEFINED IN TERMS OF ITSELF ***" << endl; @@ -1853,6 +1820,7 @@ bool SmtEngine::getInterpol(const Node& conj, const TypeNode& grammarType, Node& interpol) { + SmtScope smts(this); bool success = d_interpolSolver->getInterpol(conj, grammarType, interpol); // notify the state of whether the get-interpol call was successfuly, which // impacts the SMT mode. @@ -1870,6 +1838,7 @@ bool SmtEngine::getAbduct(const Node& conj, const TypeNode& grammarType, Node& abd) { + SmtScope smts(this); bool success = d_abductSolver->getAbduct(conj, grammarType, abd); // notify the state of whether the get-abduct call was successfuly, which // impacts the SMT mode. @@ -1883,49 +1852,33 @@ bool SmtEngine::getAbduct(const Node& conj, Node& abd) return getAbduct(conj, grammarType, abd); } -void SmtEngine::getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs ) { +void SmtEngine::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs) +{ SmtScope smts(this); TheoryEngine* te = getTheoryEngine(); Assert(te != nullptr); - std::vector<Node> qs_n; - te->getInstantiatedQuantifiedFormulas(qs_n); - for (std::size_t i = 0, n = qs_n.size(); i < n; i++) - { - qs.push_back(qs_n[i].toExpr()); - } + te->getInstantiatedQuantifiedFormulas(qs); } -void SmtEngine::getInstantiations( Expr q, std::vector< Expr >& insts ) { +void SmtEngine::getInstantiations(Node q, std::vector<Node>& insts) +{ SmtScope smts(this); TheoryEngine* te = getTheoryEngine(); Assert(te != nullptr); - std::vector<Node> insts_n; - te->getInstantiations(Node::fromExpr(q), insts_n); - for (std::size_t i = 0, n = insts_n.size(); i < n; i++) - { - insts.push_back(insts_n[i].toExpr()); - } + te->getInstantiations(q, insts); } -void SmtEngine::getInstantiationTermVectors( Expr q, std::vector< std::vector< Expr > >& tvecs ) { +void SmtEngine::getInstantiationTermVectors( + Node q, std::vector<std::vector<Node>>& tvecs) +{ SmtScope smts(this); Assert(options::trackInstLemmas()); TheoryEngine* te = getTheoryEngine(); Assert(te != nullptr); - std::vector<std::vector<Node>> tvecs_n; - te->getInstantiationTermVectors(Node::fromExpr(q), tvecs_n); - for (std::size_t i = 0, n = tvecs_n.size(); i < n; i++) - { - std::vector<Expr> tvec; - for (std::size_t j = 0, m = tvecs_n[i].size(); j < m; j++) - { - tvec.push_back(tvecs_n[i][j].toExpr()); - } - tvecs.push_back(tvec); - } + te->getInstantiationTermVectors(q, tvecs); } -std::vector<Expr> SmtEngine::getAssertions() +std::vector<Node> SmtEngine::getAssertions() { SmtScope smts(this); finishInit(); @@ -1942,10 +1895,10 @@ std::vector<Expr> SmtEngine::getAssertions() } context::CDList<Node>* al = d_asserts->getAssertionList(); Assert(al != nullptr); - std::vector<Expr> res; + std::vector<Node> res; for (const Node& n : *al) { - res.emplace_back(n.toExpr()); + res.emplace_back(n); } // copy the result out return res; diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 1b8789513..62e54a0c1 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -306,13 +306,13 @@ class CVC4_PUBLIC SmtEngine * * The return value has the same meaning as that of assertFormula. */ - Result blockModelValues(const std::vector<Expr>& exprs); + Result blockModelValues(const std::vector<Node>& exprs); /** When using separation logic, obtain the expression for the heap. */ - Expr getSepHeapExpr(); + Node getSepHeapExpr(); /** When using separation logic, obtain the expression for nil. */ - Expr getSepNilExpr(); + Node getSepNilExpr(); /** * Get an aspect of the current SMT execution environment. @@ -333,13 +333,13 @@ class CVC4_PUBLIC SmtEngine * @param global True if this definition is global (i.e. should persist when * popping the user context) */ - void defineFunction(Expr func, - const std::vector<Expr>& formals, - Expr formula, + void defineFunction(Node func, + const std::vector<Node>& formals, + Node formula, bool global = false); /** Return true if given expression is a defined function. */ - bool isDefinedFunction(Expr func); + bool isDefinedFunction(Node func); /** * Define functions recursive @@ -359,17 +359,17 @@ class CVC4_PUBLIC SmtEngine * @param global True if this definition is global (i.e. should persist when * popping the user context) */ - void defineFunctionsRec(const std::vector<Expr>& funcs, - const std::vector<std::vector<Expr>>& formals, - const std::vector<Expr>& formulas, + void defineFunctionsRec(const std::vector<Node>& funcs, + const std::vector<std::vector<Node>>& formals, + const std::vector<Node>& formulas, bool global = false); /** * Define function recursive * Same as above, but for a single function. */ - void defineFunctionRec(Expr func, - const std::vector<Expr>& formals, - Expr formula, + void defineFunctionRec(Node func, + const std::vector<Node>& formals, + Node formula, bool global = false); /** * Add a formula to the current context: preprocess, do per-theory @@ -391,9 +391,8 @@ class CVC4_PUBLIC SmtEngine * * @throw Exception */ - Result checkEntailed(const Expr& assumption = Expr(), - bool inUnsatCore = true); - Result checkEntailed(const std::vector<Expr>& assumptions, + Result checkEntailed(const Node& assumption, bool inUnsatCore = true); + Result checkEntailed(const std::vector<Node>& assumptions, bool inUnsatCore = true); /** @@ -402,8 +401,9 @@ class CVC4_PUBLIC SmtEngine * * @throw Exception */ - Result checkSat(const Expr& assumption = Expr(), bool inUnsatCore = true); - Result checkSat(const std::vector<Expr>& assumptions, + Result checkSat(); + Result checkSat(const Node& assumption, bool inUnsatCore = true); + Result checkSat(const std::vector<Node>& assumptions, bool inUnsatCore = true); /** @@ -528,7 +528,7 @@ class CVC4_PUBLIC SmtEngine /** * Same as getValue but for a vector of expressions */ - std::vector<Expr> getValues(const std::vector<Expr>& exprs); + std::vector<Node> getValues(const std::vector<Node>& exprs); /** * Add a function to the set of expressions whose value is to be @@ -666,7 +666,7 @@ class CVC4_PUBLIC SmtEngine * Get list of quantified formulas that were instantiated on the last call * to check-sat. */ - void getInstantiatedQuantifiedFormulas(std::vector<Expr>& qs); + void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs); /** * Get instantiations for quantified formula q. @@ -679,7 +679,7 @@ class CVC4_PUBLIC SmtEngine * In particular, if q is of the form forall x. P(x), then insts is a list * of formulas of the form P(t1), ..., P(tn). */ - void getInstantiations(Expr q, std::vector<Expr>& insts); + void getInstantiations(Node q, std::vector<Node>& insts); /** * Get instantiation term vectors for quantified formula q. * @@ -689,8 +689,8 @@ class CVC4_PUBLIC SmtEngine * Notice that these are not guaranteed to come in the same order as the * instantiation lemmas above. */ - void getInstantiationTermVectors(Expr q, - std::vector<std::vector<Expr> >& tvecs); + void getInstantiationTermVectors(Node q, + std::vector<std::vector<Node>>& tvecs); /** * Get an unsatisfiable core (only if immediately preceded by an UNSAT or @@ -703,7 +703,7 @@ class CVC4_PUBLIC SmtEngine * Get the current set of assertions. Only permitted if the * SmtEngine is set to operate interactively. */ - std::vector<Expr> getAssertions(); + std::vector<Node> getAssertions(); /** * Push a user-level context. @@ -879,7 +879,7 @@ class CVC4_PUBLIC SmtEngine * * Return the set of assertions, after expanding definitions. */ - std::vector<Expr> getExpandedAssertions(); + std::vector<Node> getExpandedAssertions(); /* ....................................................................... */ private: /* ....................................................................... */ @@ -949,8 +949,8 @@ class CVC4_PUBLIC SmtEngine * the interpolation problem (interpol), and the solution implies the goal * (conj). If these criteria are not met, an internal error is thrown. */ - void checkInterpol(Expr interpol, - const std::vector<Expr>& easserts, + void checkInterpol(Node interpol, + const std::vector<Node>& easserts, const Node& conj); /** @@ -1037,23 +1037,23 @@ class CVC4_PUBLIC SmtEngine * the function that the formal argument list is for. This method is used * as a helper function when defining (recursive) functions. */ - void debugCheckFormals(const std::vector<Expr>& formals, Expr func); + void debugCheckFormals(const std::vector<Node>& formals, Node func); /** * Checks whether formula is a valid function body for func whose formal * argument list is stored in formals. This method is * used as a helper function when defining (recursive) functions. */ - void debugCheckFunctionBody(Expr formula, - const std::vector<Expr>& formals, - Expr func); + void debugCheckFunctionBody(Node formula, + const std::vector<Node>& formals, + Node func); /** * Helper method to obtain both the heap and nil from the solver. Returns a * std::pair where the first element is the heap expression and the second * element is the nil expression. */ - std::pair<Expr, Expr> getSepHeapAndNilExpr(); + std::pair<Node, Node> getSepHeapAndNilExpr(); /* Members -------------------------------------------------------------- */ |