From 3ce6e00068c02286704143d82d5f044fdb356516 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 12 Oct 2020 11:14:08 -0500 Subject: [PATCH] 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. --- src/api/cvc4cpp.cpp | 61 ++-- src/preprocessing/passes/bv_to_int.cpp | 7 +- .../passes/quantifier_macros.cpp | 7 +- src/preprocessing/passes/real_to_int.cpp | 5 +- src/preprocessing/passes/sygus_inference.cpp | 8 +- src/smt/abduction_solver.cpp | 15 +- src/smt/defined_function.h | 2 +- src/smt/interpolation_solver.cpp | 19 +- src/smt/interpolation_solver.h | 4 +- src/smt/model_blocker.cpp | 23 +- src/smt/model_blocker.h | 6 +- src/smt/model_core_builder.cpp | 9 +- src/smt/model_core_builder.h | 2 +- src/smt/smt_engine.cpp | 283 ++++++++---------- src/smt/smt_engine.h | 64 ++-- .../sygus/ce_guided_single_inv.cpp | 24 +- src/theory/theory_model.cpp | 11 + src/theory/theory_model.h | 2 + test/unit/expr/type_node_white.h | 6 +- 19 files changed, 246 insertions(+), 312 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 4dda6098e..0384b573e 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -4556,7 +4556,7 @@ Result Solver::checkEntailed(Term term) const CVC4_API_ARG_CHECK_NOT_NULL(term); CVC4_API_SOLVER_CHECK_TERM(term); - CVC4::Result r = d_smtEngine->checkEntailed(term.d_node->toExpr()); + CVC4::Result r = d_smtEngine->checkEntailed(*term.d_node); return Result(r); CVC4_API_SOLVER_TRY_CATCH_END; @@ -4576,7 +4576,7 @@ Result Solver::checkEntailed(const std::vector& terms) const CVC4_API_ARG_CHECK_NOT_NULL(term); } - std::vector exprs = termVectorToExprs(terms); + std::vector exprs = termVectorToNodes(terms); CVC4::Result r = d_smtEngine->checkEntailed(exprs); return Result(r); @@ -4626,7 +4626,7 @@ Result Solver::checkSatAssuming(Term assumption) const << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC4_API_SOLVER_CHECK_TERM(assumption); - CVC4::Result r = d_smtEngine->checkSat(assumption.d_node->toExpr()); + CVC4::Result r = d_smtEngine->checkSat(*assumption.d_node); return Result(r); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4647,7 +4647,7 @@ Result Solver::checkSatAssuming(const std::vector& assumptions) const CVC4_API_SOLVER_CHECK_TERM(term); CVC4_API_ARG_CHECK_NOT_NULL(term); } - std::vector eassumptions = termVectorToExprs(assumptions); + std::vector eassumptions = termVectorToNodes(assumptions); CVC4::Result r = d_smtEngine->checkSat(eassumptions); return Result(r); CVC4_API_SOLVER_TRY_CATCH_END; @@ -4731,7 +4731,7 @@ Term Solver::defineFun(const std::string& symbol, CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort) << "first-class sort as codomain sort for function sort"; - std::vector domain_types; + std::vector domain_types; for (size_t i = 0, size = bound_vars.size(); i < size; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( @@ -4747,20 +4747,21 @@ Term Solver::defineFun(const std::string& symbol, CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( t.isFirstClass(), "sort of parameter", bound_vars[i], i) << "first-class sort of parameter of defined function"; - domain_types.push_back(t); + domain_types.push_back(TypeNode::fromType(t)); } CVC4_API_SOLVER_CHECK_SORT(sort); CVC4_API_CHECK(sort == term.getSort()) << "Invalid sort of function body '" << term << "', expected '" << sort << "'"; - Type type = *sort.d_type; + NodeManager* nm = getNodeManager(); + TypeNode type = TypeNode::fromType(*sort.d_type); if (!domain_types.empty()) { - type = d_exprMgr->mkFunctionType(domain_types, type); + type = nm->mkFunctionType(domain_types, type); } - Expr fun = d_exprMgr->mkVar(symbol, type); - std::vector ebound_vars = termVectorToExprs(bound_vars); - d_smtEngine->defineFunction(fun, ebound_vars, term.d_node->toExpr(), global); + Node fun = Node::fromExpr(d_exprMgr->mkVar(symbol, type.toType())); + std::vector ebound_vars = termVectorToNodes(bound_vars); + d_smtEngine->defineFunction(fun, ebound_vars, *term.d_node, global); return Term(this, fun); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4809,9 +4810,8 @@ Term Solver::defineFun(Term fun, CVC4_API_SOLVER_CHECK_TERM(term); - std::vector ebound_vars = termVectorToExprs(bound_vars); - d_smtEngine->defineFunction( - fun.d_node->toExpr(), ebound_vars, term.d_node->toExpr(), global); + std::vector ebound_vars = termVectorToNodes(bound_vars); + d_smtEngine->defineFunction(*fun.d_node, ebound_vars, *term.d_node, global); return fun; CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4838,7 +4838,7 @@ Term Solver::defineFunRec(const std::string& symbol, CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort) << "first-class sort as function codomain sort"; Assert(!sort.isFunction()); /* A function sort is not first-class. */ - std::vector domain_types; + std::vector domain_types; for (size_t i = 0, size = bound_vars.size(); i < size; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( @@ -4850,7 +4850,7 @@ Term Solver::defineFunRec(const std::string& symbol, bound_vars[i], i) << "a bound variable"; - CVC4::Type t = bound_vars[i].d_node->getType().toType(); + CVC4::TypeNode t = bound_vars[i].d_node->getType(); CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( t.isFirstClass(), "sort of parameter", bound_vars[i], i) << "first-class sort of parameter of defined function"; @@ -4861,13 +4861,14 @@ Term Solver::defineFunRec(const std::string& symbol, << "Invalid sort of function body '" << term << "', expected '" << sort << "'"; CVC4_API_SOLVER_CHECK_TERM(term); - Type type = *sort.d_type; + NodeManager* nm = getNodeManager(); + TypeNode type = TypeNode::fromType(*sort.d_type); if (!domain_types.empty()) { - type = d_exprMgr->mkFunctionType(domain_types, type); + type = nm->mkFunctionType(domain_types, type); } - Expr fun = d_exprMgr->mkVar(symbol, type); - std::vector ebound_vars = termVectorToExprs(bound_vars); + Node fun = Node::fromExpr(d_exprMgr->mkVar(symbol, type.toType())); + std::vector ebound_vars = termVectorToNodes(bound_vars); d_smtEngine->defineFunctionRec( fun, ebound_vars, term.d_node->toExpr(), global); return Term(this, fun); @@ -4925,9 +4926,9 @@ Term Solver::defineFunRec(Term fun, } CVC4_API_SOLVER_CHECK_TERM(term); - std::vector ebound_vars = termVectorToExprs(bound_vars); + std::vector ebound_vars = termVectorToNodes(bound_vars); d_smtEngine->defineFunctionRec( - fun.d_node->toExpr(), ebound_vars, term.d_node->toExpr(), global); + *fun.d_node, ebound_vars, *term.d_node, global); return fun; CVC4_API_SOLVER_TRY_CATCH_END; } @@ -5003,13 +5004,13 @@ void Solver::defineFunsRec(const std::vector& funs, << "function or nullary symbol"; } } - std::vector efuns = termVectorToExprs(funs); - std::vector> ebound_vars; + std::vector efuns = termVectorToNodes(funs); + std::vector> ebound_vars; for (const auto& v : bound_vars) { - ebound_vars.push_back(termVectorToExprs(v)); + ebound_vars.push_back(termVectorToNodes(v)); } - std::vector exprs = termVectorToExprs(terms); + std::vector exprs = termVectorToNodes(terms); d_smtEngine->defineFunctionsRec(efuns, ebound_vars, exprs, global); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -5028,12 +5029,12 @@ void Solver::echo(std::ostream& out, const std::string& str) const std::vector Solver::getAssertions(void) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - std::vector assertions = d_smtEngine->getAssertions(); + std::vector assertions = d_smtEngine->getAssertions(); /* Can not use * return std::vector(assertions.begin(), assertions.end()); * here since constructor is private */ std::vector res; - for (const Expr& e : assertions) + for (const Node& e : assertions) { res.push_back(Term(this, e)); } @@ -5359,7 +5360,7 @@ void Solver::blockModelValues(const std::vector& terms) const << "Cannot get value when in unsat mode."; CVC4_API_ARG_SIZE_CHECK_EXPECTED(!terms.empty(), terms) << "a non-empty set of terms"; - for (int i = 0; i < terms.size(); ++i) + for (size_t i = 0, tsize = terms.size(); i < tsize; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( !terms[i].isNull(), "term", terms[i], i) @@ -5369,7 +5370,7 @@ void Solver::blockModelValues(const std::vector& terms) const << "a term associated to this solver object"; } CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); - d_smtEngine->blockModelValues(termVectorToExprs(terms)); + d_smtEngine->blockModelValues(termVectorToNodes(terms)); CVC4_API_SOLVER_TRY_CATCH_END; } diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index 06a5714d3..eaae7d71d 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -815,7 +815,7 @@ void BVToInt::defineBVUFAsIntUF(Node bvUF, Node intUF) // The type of the resulting term TypeNode resultType; // symbolic arguments of original function - vector args; + vector args; if (!bvUF.getType().isFunction()) { // bvUF is a variable. // in this case, the result is just the original term @@ -837,7 +837,7 @@ void BVToInt::defineBVUFAsIntUF(Node bvUF, Node intUF) // Each bit-vector argument is casted to a natural number // Other arguments are left intact. Node fresh_bound_var = d_nm->mkBoundVar(d); - args.push_back(fresh_bound_var.toExpr()); + args.push_back(fresh_bound_var); Node castedArg = args[i]; if (d.isBitVector()) { @@ -851,8 +851,7 @@ void BVToInt::defineBVUFAsIntUF(Node bvUF, Node intUF) // If the result is BV, it needs to be casted back. result = castToType(result, resultType); // add the function definition to the smt engine. - smt::currentSmtEngine()->defineFunction( - bvUF.toExpr(), args, result.toExpr(), true); + d_preprocContext->getSmt()->defineFunction(bvUF, args, result, true); } bool BVToInt::childrenTypesChanged(Node n) diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp index 8fea4cbac..604f8719c 100644 --- a/src/preprocessing/passes/quantifier_macros.cpp +++ b/src/preprocessing/passes/quantifier_macros.cpp @@ -504,20 +504,21 @@ void QuantifierMacros::finalizeDefinitions() { if( options::incrementalSolving() || options::produceModels() || doDefs ){ Trace("macros") << "Store as defined functions..." << std::endl; //also store as defined functions + SmtEngine* smt = d_preprocContext->getSmt(); for( std::map< Node, Node >::iterator it = d_macro_defs.begin(); it != d_macro_defs.end(); ++it ){ Trace("macros-def") << "Macro definition for " << it->first << " : " << it->second << std::endl; Trace("macros-def") << " basis is : "; std::vector< Node > nargs; - std::vector< Expr > args; + std::vector args; for( unsigned i=0; ifirst].size(); i++ ){ Node bv = NodeManager::currentNM()->mkBoundVar( d_macro_basis[it->first][i].getType() ); Trace("macros-def") << d_macro_basis[it->first][i] << " "; nargs.push_back( bv ); - args.push_back( bv.toExpr() ); + args.push_back(bv); } Trace("macros-def") << std::endl; Node sbody = it->second.substitute( d_macro_basis[it->first].begin(), d_macro_basis[it->first].end(), nargs.begin(), nargs.end() ); - smt::currentSmtEngine()->defineFunction( it->first.toExpr(), args, sbody.toExpr() ); + smt->defineFunction(it->first, args, sbody); if( Trace.isOn("macros-warn") ){ debugMacroDefinition( it->first, sbody ); diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp index 046a1c990..672e281d7 100644 --- a/src/preprocessing/passes/real_to_int.cpp +++ b/src/preprocessing/passes/real_to_int.cpp @@ -181,9 +181,8 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector& va var_eq.push_back(n.eqNode(ret)); // ensure that the original variable is defined to be the returned // one, which is important for models and for incremental solving. - std::vector args; - smt::currentSmtEngine()->defineFunction( - n.toExpr(), args, ret.toExpr()); + std::vector args; + d_preprocContext->getSmt()->defineFunction(n, args, ret); } } } diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index cdacd740a..ea767e771 100644 --- a/src/preprocessing/passes/sygus_inference.cpp +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -44,21 +44,21 @@ PreprocessingPassResult SygusInference::applyInternal( { Assert(funs.size() == sols.size()); // if so, sygus gives us function definitions - SmtEngine* master_smte = smt::currentSmtEngine(); + SmtEngine* master_smte = d_preprocContext->getSmt(); for (unsigned i = 0, size = funs.size(); i < size; i++) { - std::vector args; + std::vector args; Node sol = sols[i]; // if it is a non-constant function if (sol.getKind() == LAMBDA) { for (const Node& v : sol[0]) { - args.push_back(v.toExpr()); + args.push_back(v); } sol = sol[1]; } - master_smte->defineFunction(funs[i].toExpr(), args, sol.toExpr()); + master_smte->defineFunction(funs[i], args, sol); } // apply substitution to everything, should result in SAT 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 easserts = d_parent->getExpandedAssertions(); - std::vector axioms; - for (unsigned i = 0, size = easserts.size(); i < size; i++) - { - axioms.push_back(Node::fromExpr(easserts[i])); - } + std::vector axioms = d_parent->getExpandedAssertions(); std::vector 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 asserts = d_parent->getExpandedAssertions(); - asserts.push_back(a.toExpr()); + std::vector 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& formals, Node formula) + DefinedFunction(Node func, const std::vector& 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 easserts = d_parent->getExpandedAssertions(); - std::vector axioms; - for (unsigned i = 0, size = easserts.size(); i < size; i++) - { - axioms.push_back(Node::fromExpr(easserts[i])); - } + std::vector 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& easserts, +void InterpolationSolver::checkInterpol(Node interpol, + const std::vector& 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& easserts, + void checkInterpol(Node interpol, + const std::vector& 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& assertions, +Node ModelBlocker::getModelBlocker(const std::vector& assertions, theory::TheoryModel* m, options::BlockModelsMode mode, - const std::vector& exprToBlock) + const std::vector& exprToBlock) { NodeManager* nm = NodeManager::currentNM(); // convert to nodes - std::vector tlAsserts; - for (const Expr& a : assertions) - { - Node an = Node::fromExpr(a); - tlAsserts.push_back(an); - } - std::vector nodesToBlock; - for (const Expr& eb : exprToBlock) - { - nodesToBlock.push_back(Node::fromExpr(eb)); - } + std::vector tlAsserts = assertions; + std::vector 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& 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() == cpol) { @@ -139,7 +130,7 @@ Expr ModelBlocker::getModelBlocker(const std::vector& 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& 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& assertions, + static Node getModelBlocker( + const std::vector& assertions, theory::TheoryModel* m, options::BlockModelsMode mode, - const std::vector& exprToBlock = std::vector()); + const std::vector& exprToBlock = std::vector()); }; /* 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& assertions, +bool ModelCoreBuilder::setModelCore(const std::vector& assertions, Model* m, options::ModelCoresMode mode) { @@ -34,14 +34,9 @@ bool ModelCoreBuilder::setModelCore(const std::vector& assertions, } // convert to nodes - std::vector 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 vars; std::vector 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& assertions, + static bool setModelCore(const std::vector& 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 exprVectorToNodes(const std::vector& exprs) -{ - std::vector 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& formals, Expr func) +void SmtEngine::debugCheckFormals(const std::vector& formals, Node func) { - for(std::vector::const_iterator i = formals.begin(); i != formals.end(); ++i) { + for (std::vector::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& formals, - Expr func) +void SmtEngine::debugCheckFunctionBody(Node formula, + const std::vector& 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& formals, - Expr formula, +void SmtEngine::defineFunction(Node func, + const std::vector& formals, + Node formula, bool global) { SmtScope smts(this); @@ -717,13 +707,12 @@ void SmtEngine::defineFunction(Expr func, std::vector 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 formalsNodes; - for(vector::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& funcs, - const std::vector>& formals, - const std::vector& formulas, + const std::vector& funcs, + const std::vector>& formals, + const std::vector& formulas, bool global) { SmtScope smts(this); @@ -789,22 +769,15 @@ void SmtEngine::defineFunctionsRec( if (Dump.isOn("raw-benchmark")) { - std::vector nFuncs = exprVectorToNodes(funcs); - std::vector> nFormals; - for (const std::vector& formal : formals) - { - nFormals.emplace_back(exprVectorToNodes(formal)); - } - std::vector 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 children; + std::vector 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_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& formals, - Expr formula, +void SmtEngine::defineFunctionRec(Node func, + const std::vector& formals, + Node formula, bool global) { - std::vector funcs; + std::vector funcs; funcs.push_back(func); - std::vector > formals_multi; + std::vector> formals_multi; formals_multi.push_back(formals); - std::vector formulas; + std::vector 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 assump; if (!assumption.isNull()) { - assump.push_back(Node::fromExpr(assumption)); + assump.push_back(assumption); } return checkSatInternal(assump, inUnsatCore, false); } -Result SmtEngine::checkSat(const vector& assumptions, bool inUnsatCore) +Result SmtEngine::checkSat(const std::vector& assumptions, + bool inUnsatCore) { if (Dump.isOn("benchmark")) { @@ -969,43 +946,33 @@ Result SmtEngine::checkSat(const vector& assumptions, bool inUnsatCore) else { getOutputManager().getPrinter().toStreamCmdCheckSatAssuming( - getOutputManager().getDumpOut(), exprVectorToNodes(assumptions)); + getOutputManager().getDumpOut(), assumptions); } } - std::vector 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() - : std::vector{Node::fromExpr(node)}, - inUnsatCore, - true) + return checkSatInternal( + node.isNull() ? std::vector() : std::vector{node}, + inUnsatCore, + true) .asEntailmentResult(); } -Result SmtEngine::checkEntailed(const vector& nodes, bool inUnsatCore) +Result SmtEngine::checkEntailed(const std::vector& nodes, + bool inUnsatCore) { - std::vector 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& assumptions, +Result SmtEngine::checkSatInternal(const std::vector& assumptions, bool inUnsatCore, bool isEntailmentCheck) { @@ -1272,12 +1239,12 @@ Node SmtEngine::getValue(const Node& ex) const return resultNode; } -vector SmtEngine::getValues(const vector& exprs) +std::vector SmtEngine::getValues(const std::vector& exprs) { - vector result; - for (const Expr& e : exprs) + std::vector 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 eassertsProc = getExpandedAssertions(); + std::vector 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 eassertsProc = getExpandedAssertions(); - Expr eblocker = ModelBlocker::getModelBlocker( + std::vector eassertsProc = getExpandedAssertions(); + Node eblocker = ModelBlocker::getModelBlocker( eassertsProc, m, options::blockModelsMode()); - return assertFormula(Node::fromExpr(eblocker)); + return assertFormula(eblocker); } -Result SmtEngine::blockModelValues(const std::vector& exprs) +Result SmtEngine::blockModelValues(const std::vector& exprs) { Trace("smt") << "SMT blockModelValues()" << endl; SmtScope smts(this); @@ -1447,20 +1414,20 @@ Result SmtEngine::blockModelValues(const std::vector& 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 eassertsProc = getExpandedAssertions(); + std::vector 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 SmtEngine::getSepHeapAndNilExpr(void) +std::pair SmtEngine::getSepHeapAndNilExpr(void) { if (!d_logic.isTheoryEnabled(THEORY_SEP)) { @@ -1479,27 +1446,26 @@ std::pair 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 SmtEngine::getExpandedAssertions() +std::vector SmtEngine::getExpandedAssertions() { - std::vector easserts = getAssertions(); + std::vector easserts = getAssertions(); // must expand definitions - std::vector eassertsProc; + std::vector eassertsProc; std::unordered_map 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& qs) +{ SmtScope smts(this); TheoryEngine* te = getTheoryEngine(); Assert(te != nullptr); - std::vector 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& insts) +{ SmtScope smts(this); TheoryEngine* te = getTheoryEngine(); Assert(te != nullptr); - std::vector 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>& tvecs) +{ SmtScope smts(this); Assert(options::trackInstLemmas()); TheoryEngine* te = getTheoryEngine(); Assert(te != nullptr); - std::vector> tvecs_n; - te->getInstantiationTermVectors(Node::fromExpr(q), tvecs_n); - for (std::size_t i = 0, n = tvecs_n.size(); i < n; i++) - { - std::vector 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 SmtEngine::getAssertions() +std::vector SmtEngine::getAssertions() { SmtScope smts(this); finishInit(); @@ -1942,10 +1895,10 @@ std::vector SmtEngine::getAssertions() } context::CDList* al = d_asserts->getAssertionList(); Assert(al != nullptr); - std::vector res; + std::vector 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& exprs); + Result blockModelValues(const std::vector& 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& formals, - Expr formula, + void defineFunction(Node func, + const std::vector& 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& funcs, - const std::vector>& formals, - const std::vector& formulas, + void defineFunctionsRec(const std::vector& funcs, + const std::vector>& formals, + const std::vector& formulas, bool global = false); /** * Define function recursive * Same as above, but for a single function. */ - void defineFunctionRec(Expr func, - const std::vector& formals, - Expr formula, + void defineFunctionRec(Node func, + const std::vector& 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& assumptions, + Result checkEntailed(const Node& assumption, bool inUnsatCore = true); + Result checkEntailed(const std::vector& 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& assumptions, + Result checkSat(); + Result checkSat(const Node& assumption, bool inUnsatCore = true); + Result checkSat(const std::vector& assumptions, bool inUnsatCore = true); /** @@ -528,7 +528,7 @@ class CVC4_PUBLIC SmtEngine /** * Same as getValue but for a vector of expressions */ - std::vector getValues(const std::vector& exprs); + std::vector getValues(const std::vector& 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& qs); + void getInstantiatedQuantifiedFormulas(std::vector& 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& insts); + void getInstantiations(Node q, std::vector& 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 >& tvecs); + void getInstantiationTermVectors(Node q, + std::vector>& 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 getAssertions(); + std::vector getAssertions(); /** * Push a user-level context. @@ -879,7 +879,7 @@ class CVC4_PUBLIC SmtEngine * * Return the set of assertions, after expanding definitions. */ - std::vector getExpandedAssertions(); + std::vector 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& easserts, + void checkInterpol(Node interpol, + const std::vector& 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& formals, Expr func); + void debugCheckFormals(const std::vector& 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& formals, - Expr func); + void debugCheckFunctionBody(Node formula, + const std::vector& 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 getSepHeapAndNilExpr(); + std::pair getSepHeapAndNilExpr(); /* Members -------------------------------------------------------------- */ diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 4ab92f6a7..4b45072f7 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -386,7 +386,7 @@ bool CegSingleInv::solve() return false; } // now, get the instantiations - std::vector qs; + std::vector qs; siSmt->getInstantiatedQuantifiedFormulas(qs); Assert(qs.size() <= 1); // track the instantiations, as solution construction is based on this @@ -394,15 +394,13 @@ bool CegSingleInv::solve() << std::endl; d_inst.clear(); d_instConds.clear(); - for (const Expr& q : qs) + for (const Node& q : qs) { - TNode qn = Node::fromExpr(q); - Assert(qn.getKind() == FORALL); - std::vector > tvecs; - siSmt->getInstantiationTermVectors(q, tvecs); - Trace("sygus-si") << "#instantiations of " << q << "=" << tvecs.size() + Assert(q.getKind() == FORALL); + siSmt->getInstantiationTermVectors(q, d_inst); + Trace("sygus-si") << "#instantiations of " << q << "=" << d_inst.size() << std::endl; - // We use the original synthesis conjecture siq, since qn may contain + // We use the original synthesis conjecture siq, since q may contain // internal symbols e.g. termITE skolem after preprocessing. std::vector vars; for (const Node& v : siq[0]) @@ -410,16 +408,10 @@ bool CegSingleInv::solve() vars.push_back(v); } Node body = siq[1]; - for (unsigned i = 0, ninsts = tvecs.size(); i < ninsts; i++) + for (unsigned i = 0, ninsts = d_inst.size(); i < ninsts; i++) { - std::vector& tvi = tvecs[i]; - std::vector inst; - for (const Expr& t : tvi) - { - inst.push_back(Node::fromExpr(t)); - } + std::vector& inst = d_inst[i]; Trace("sygus-si") << " Instantiation: " << inst << std::endl; - d_inst.push_back(inst); // instantiation should have same arity since we are not allowed to // eliminate variables from quantifiers marked with QuantElimAttribute. Assert(inst.size() == vars.size()); diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 2d0a80599..b8cbdf6b3 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -98,6 +98,17 @@ void TheoryModel::setHeapModel( Node h, Node neq ) { d_sep_nil_eq = neq; } +bool TheoryModel::getHeapModel(Node& h, Node& neq) const +{ + if (d_sep_heap.isNull() || d_sep_nil_eq.isNull()) + { + return false; + } + h = d_sep_heap; + neq = d_sep_nil_eq; + return true; +} + bool TheoryModel::getHeapModel( Expr& h, Expr& neq ) const { if( d_sep_heap.isNull() || d_sep_nil_eq.isNull() ){ return false; diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index b1401c074..9f330ff6c 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -301,6 +301,8 @@ public: /** set the heap and value sep.nil is equal to */ void setHeapModel(Node h, Node neq); /** get the heap and value sep.nil is equal to */ + bool getHeapModel(Node& h, Node& neq) const; + /** get the heap and value sep.nil is equal to */ bool getHeapModel(Expr& h, Expr& neq) const override; //---------------------------- end separation logic diff --git a/test/unit/expr/type_node_white.h b/test/unit/expr/type_node_white.h index 4d268fbf6..22d3f0d84 100644 --- a/test/unit/expr/type_node_white.h +++ b/test/unit/expr/type_node_white.h @@ -64,9 +64,9 @@ class TypeNodeWhite : public CxxTest::TestSuite { Node xPos = d_nm->mkNode(GT, x, d_nm->mkConst(Rational(0))); TypeNode funtype = d_nm->mkFunctionType(integerType, booleanType); Node lambda = d_nm->mkVar("lambda", funtype); - vector formals; - formals.push_back(x.toExpr()); - d_smt->defineFunction(lambda.toExpr(), formals, xPos.toExpr()); + vector formals; + formals.push_back(x); + d_smt->defineFunction(lambda, formals, xPos); TS_ASSERT( not realType.isComparableTo(booleanType) ); TS_ASSERT( realType.isComparableTo(integerType) ); -- 2.30.2