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.
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;
CVC4_API_ARG_CHECK_NOT_NULL(term);
}
- std::vector<Expr> exprs = termVectorToExprs(terms);
+ std::vector<Node> exprs = termVectorToNodes(terms);
CVC4::Result r = d_smtEngine->checkEntailed(exprs);
return Result(r);
<< "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;
}
CVC4_API_SOLVER_CHECK_TERM(term);
CVC4_API_ARG_CHECK_NOT_NULL(term);
}
- std::vector<Expr> eassumptions = termVectorToExprs(assumptions);
+ std::vector<Node> eassumptions = termVectorToNodes(assumptions);
CVC4::Result r = d_smtEngine->checkSat(eassumptions);
return Result(r);
CVC4_API_SOLVER_TRY_CATCH_END;
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<Type> domain_types;
+ std::vector<TypeNode> domain_types;
for (size_t i = 0, size = bound_vars.size(); i < size; ++i)
{
CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
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<Expr> 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<Node> 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;
}
CVC4_API_SOLVER_CHECK_TERM(term);
- std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
- d_smtEngine->defineFunction(
- fun.d_node->toExpr(), ebound_vars, term.d_node->toExpr(), global);
+ std::vector<Node> 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;
}
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<Type> domain_types;
+ std::vector<TypeNode> domain_types;
for (size_t i = 0, size = bound_vars.size(); i < size; ++i)
{
CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
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";
<< "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<Expr> ebound_vars = termVectorToExprs(bound_vars);
+ Node fun = Node::fromExpr(d_exprMgr->mkVar(symbol, type.toType()));
+ std::vector<Node> ebound_vars = termVectorToNodes(bound_vars);
d_smtEngine->defineFunctionRec(
fun, ebound_vars, term.d_node->toExpr(), global);
return Term(this, fun);
}
CVC4_API_SOLVER_CHECK_TERM(term);
- std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
+ std::vector<Node> 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;
}
<< "function or nullary symbol";
}
}
- std::vector<Expr> efuns = termVectorToExprs(funs);
- std::vector<std::vector<Expr>> ebound_vars;
+ std::vector<Node> efuns = termVectorToNodes(funs);
+ std::vector<std::vector<Node>> ebound_vars;
for (const auto& v : bound_vars)
{
- ebound_vars.push_back(termVectorToExprs(v));
+ ebound_vars.push_back(termVectorToNodes(v));
}
- std::vector<Expr> exprs = termVectorToExprs(terms);
+ std::vector<Node> exprs = termVectorToNodes(terms);
d_smtEngine->defineFunctionsRec(efuns, ebound_vars, exprs, global);
CVC4_API_SOLVER_TRY_CATCH_END;
}
std::vector<Term> Solver::getAssertions(void) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- std::vector<Expr> assertions = d_smtEngine->getAssertions();
+ std::vector<Node> assertions = d_smtEngine->getAssertions();
/* Can not use
* return std::vector<Term>(assertions.begin(), assertions.end());
* here since constructor is private */
std::vector<Term> res;
- for (const Expr& e : assertions)
+ for (const Node& e : assertions)
{
res.push_back(Term(this, e));
}
<< "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)
<< "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;
}
// The type of the resulting term
TypeNode resultType;
// symbolic arguments of original function
- vector<Expr> args;
+ vector<Node> args;
if (!bvUF.getType().isFunction()) {
// bvUF is a variable.
// in this case, the result is just the original term
// 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())
{
// 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)
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<Node> args;
for( unsigned i=0; i<d_macro_basis[it->first].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 );
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<Expr> args;
- smt::currentSmtEngine()->defineFunction(
- n.toExpr(), args, ret.toExpr());
+ std::vector<Node> args;
+ d_preprocContext->getSmt()->defineFunction(n, args, ret);
}
}
}
{
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<Expr> args;
+ std::vector<Node> 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
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);
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.
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);
}
<< "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
{
{
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)
{
}
}
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");
{
if (options::checkInterpols())
{
- checkInterpol(interpol.toExpr(), easserts, conj);
+ checkInterpol(interpol.toExpr(), axioms, conj);
}
return true;
}
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());
<< ": 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;
* 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:
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)
// 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)
{
}
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;
}
}
Trace("model-blocker") << "...model blocker is " << blocker << std::endl;
- return blocker.toExpr();
+ return blocker;
}
} /* namespace CVC4 */
* 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
namespace CVC4 {
-bool ModelCoreBuilder::setModelCore(const std::vector<Expr>& assertions,
+bool ModelCoreBuilder::setModelCore(const std::vector<Node>& assertions,
Model* m,
options::ModelCoresMode mode)
{
}
// 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;
* 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 */
#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"
#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"
#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"
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),
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"
<< "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);
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");
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);
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())
{
}
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() {
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"))
{
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"))
{
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)
{
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;
}
{
// 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();
}
// 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);
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))
{
<< "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()
{
// 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;
// [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;
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.
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.
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();
}
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;
*
* 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.
* @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
* @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
*
* @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);
/**
*
* @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);
/**
/**
* 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
* 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.
* 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.
*
* 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
* 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.
*
* Return the set of assertions, after expanding definitions.
*/
- std::vector<Expr> getExpandedAssertions();
+ std::vector<Node> getExpandedAssertions();
/* ....................................................................... */
private:
/* ....................................................................... */
* 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);
/**
* 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 -------------------------------------------------------------- */
return false;
}
// now, get the instantiations
- std::vector<Expr> qs;
+ std::vector<Node> qs;
siSmt->getInstantiatedQuantifiedFormulas(qs);
Assert(qs.size() <= 1);
// track the instantiations, as solution construction is based on this
<< 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<std::vector<Expr> > 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<Node> vars;
for (const Node& v : siq[0])
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<Expr>& tvi = tvecs[i];
- std::vector<Node> inst;
- for (const Expr& t : tvi)
- {
- inst.push_back(Node::fromExpr(t));
- }
+ std::vector<Node>& 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());
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;
/** 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
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<Expr> formals;
- formals.push_back(x.toExpr());
- d_smt->defineFunction(lambda.toExpr(), formals, xPos.toExpr());
+ vector<Node> formals;
+ formals.push_back(x);
+ d_smt->defineFunction(lambda, formals, xPos);
TS_ASSERT( not realType.isComparableTo(booleanType) );
TS_ASSERT( realType.isComparableTo(integerType) );
projects / cvc5.git / commitdiff