#include "expr/dtype.h"
#include "expr/dtype_cons.h"
#include "expr/dtype_selector.h"
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
-#include "expr/expr_manager_scope.h"
#include "expr/kind.h"
#include "expr/metakind.h"
#include "expr/node.h"
{
Assert(isDefinedKind(k));
Assert(isDefinedIntKind(extToIntKind(k)));
- uint32_t min = CVC4::ExprManager::minArity(extToIntKind(k));
+ uint32_t min = CVC4::kind::metakind::getLowerBoundForKind(extToIntKind(k));
// At the API level, we treat functions/constructors/selectors/testers as
// normal terms instead of making them part of the operator
{
Assert(isDefinedKind(k));
Assert(isDefinedIntKind(extToIntKind(k)));
- uint32_t max = CVC4::ExprManager::maxArity(extToIntKind(k));
+ uint32_t max = CVC4::kind::metakind::getUpperBoundForKind(extToIntKind(k));
// At the API level, we treat functions/constructors/selectors/testers as
// normal terms instead of making them part of the operator
{
}
-Op::Op(const Solver* slv, const Kind k, const CVC4::Expr& e)
- : d_solver(slv), d_kind(k), d_node(new CVC4::Node(Node::fromExpr(e)))
-{
-}
-
Op::Op(const Solver* slv, const Kind k, const CVC4::Node& n)
: d_solver(slv), d_kind(k), d_node(new CVC4::Node(n))
{
{
if (t.isIndexedHelper())
{
- return ExprHashFunction()(t.d_node->toExpr());
+ return NodeHashFunction()(*t.d_node);
}
else
{
Term::Term() : d_solver(nullptr), d_node(new CVC4::Node()) {}
-Term::Term(const Solver* slv, const CVC4::Expr& e) : d_solver(slv)
-{
- // Ensure that we create the node in the correct node manager.
- NodeManagerScope scope(d_solver->getNodeManager());
- d_node.reset(new CVC4::Node(e));
-}
-
Term::Term(const Solver* slv, const CVC4::Node& n) : d_solver(slv)
{
// Ensure that we create the node in the correct node manager.
if (index == 0)
{
// return the operator
- return Term(d_solver, d_node->getOperator().toExpr());
+ return Term(d_solver, d_node->getOperator());
}
// otherwise we are looking up child at (index-1)
index--;
}
- return Term(d_solver, (*d_node)[index].toExpr());
+ return Term(d_solver, (*d_node)[index]);
}
uint64_t Term::getId() const
Term Term::getConstArrayBase() const
{
- CVC4::ExprManagerScope exmgrs(*(d_solver->getExprManager()));
+ NodeManagerScope scope(d_solver->getNodeManager());
CVC4_API_CHECK_NOT_NULL;
// CONST_ARRAY kind maps to STORE_ALL internal kind
CVC4_API_CHECK(d_node->getKind() == CVC4::Kind::STORE_ALL)
return Term::const_iterator(d_solver, d_node, endpos);
}
-//// !!! This is only temporarily available until the parser is fully migrated
-//// to the new API. !!!
-CVC4::Expr Term::getExpr(void) const
-{
- if (d_node->isNull())
- {
- return Expr();
- }
- NodeManagerScope scope(d_solver->getNodeManager());
- return d_node->toExpr();
-}
-
const CVC4::Node& Term::getNode(void) const { return *d_node; }
namespace detail {
if (!d_sygusVars.empty())
{
- bvl = Term(d_solver,
- d_solver->getExprManager()->mkExpr(
- CVC4::kind::BOUND_VAR_LIST, termVectorToExprs(d_sygusVars)));
+ bvl = Term(
+ d_solver,
+ d_solver->getNodeManager()->mkNode(
+ CVC4::kind::BOUND_VAR_LIST, Term::termVectorToNodes(d_sygusVars)));
}
std::unordered_map<Term, Sort, TermHashFunction> ntsToUnres(d_ntSyms.size());
ssCName << op.getKind();
if (!args.empty())
{
- Term lbvl = Term(d_solver,
- d_solver->getExprManager()->mkExpr(
- CVC4::kind::BOUND_VAR_LIST, termVectorToExprs(args)));
+ Term lbvl =
+ Term(d_solver,
+ d_solver->getNodeManager()->mkNode(CVC4::kind::BOUND_VAR_LIST,
+ Term::termVectorToNodes(args)));
// its operator is a lambda
- op = Term(
- d_solver,
- d_solver->getExprManager()->mkExpr(
- CVC4::kind::LAMBDA, {lbvl.d_node->toExpr(), op.d_node->toExpr()}));
+ op = Term(d_solver,
+ d_solver->getNodeManager()->mkNode(
+ CVC4::kind::LAMBDA, *lbvl.d_node, *op.d_node));
}
std::vector<TypeNode> cargst = Sort::sortVectorToTypeNodes(cargs);
dt.d_dtype->addSygusConstructor(*op.d_node, ssCName.str(), cargst);
Term ptermc = purifySygusGTerm(
Term(d_solver, (*term.d_node)[i]), args, cargs, ntsToUnres);
pchildren.push_back(ptermc);
- childChanged =
- childChanged || ptermc.d_node->toExpr() != (term.d_node->toExpr())[i];
+ childChanged = childChanged || *ptermc.d_node != (*term.d_node)[i];
}
if (!childChanged)
{
Solver::Solver(Options* opts)
{
- d_exprMgr.reset(new ExprManager);
- d_smtEngine.reset(new SmtEngine(d_exprMgr->getNodeManager(), opts));
+ d_nodeMgr.reset(new NodeManager(nullptr));
+ d_smtEngine.reset(new SmtEngine(d_nodeMgr.get(), opts));
d_smtEngine->setSolver(this);
Options& o = d_smtEngine->getOptions();
d_rng.reset(new Random(o[options::seed]));
Term Solver::mkTermFromKind(Kind kind) const
{
+ NodeManagerScope scope(getNodeManager());
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_KIND_CHECK_EXPECTED(
kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, kind)
<< "PI or REGEXP_EMPTY or REGEXP_SIGMA";
- Expr res;
+ Node res;
if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA)
{
CVC4::Kind k = extToIntKind(kind);
Assert(isDefinedIntKind(k));
- res = d_exprMgr->mkExpr(k, std::vector<Expr>());
+ res = d_nodeMgr->mkNode(k, std::vector<Node>());
}
else
{
Assert(kind == PI);
- res = d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
+ res = d_nodeMgr->mkNullaryOperator(d_nodeMgr->realType(), CVC4::kind::PI);
}
(void)res.getType(true); /* kick off type checking */
return Term(this, res);
<< "a child term associated to this solver object";
}
- std::vector<Expr> echildren = termVectorToExprs(children);
+ std::vector<Node> echildren = Term::termVectorToNodes(children);
CVC4::Kind k = extToIntKind(kind);
Assert(isDefinedIntKind(k))
<< "Not a defined internal kind : " << k << " " << kind;
- Expr res;
+ Node res;
if (echildren.size() > 2)
{
if (kind == INTS_DIVISION || kind == XOR || kind == MINUS
|| kind == DIVISION || kind == HO_APPLY || kind == REGEXP_DIFF)
{
// left-associative, but CVC4 internally only supports 2 args
- res = d_exprMgr->mkLeftAssociative(k, echildren);
+ res = d_nodeMgr->mkLeftAssociative(k, echildren);
}
else if (kind == IMPLIES)
{
// right-associative, but CVC4 internally only supports 2 args
- res = d_exprMgr->mkRightAssociative(k, echildren);
+ res = d_nodeMgr->mkRightAssociative(k, echildren);
}
else if (kind == EQUAL || kind == LT || kind == GT || kind == LEQ
|| kind == GEQ)
{
// "chainable", but CVC4 internally only supports 2 args
- res = d_exprMgr->mkChain(k, echildren);
+ res = d_nodeMgr->mkChain(k, echildren);
}
else if (kind::isAssociative(k))
{
// mkAssociative has special treatment for associative operators with lots
// of children
- res = d_exprMgr->mkAssociative(k, echildren);
+ res = d_nodeMgr->mkAssociative(k, echildren);
}
else
{
// default case, must check kind
checkMkTerm(kind, children.size());
- res = d_exprMgr->mkExpr(k, echildren);
+ res = d_nodeMgr->mkNode(k, echildren);
}
}
else if (kind::isAssociative(k))
{
// associative case, same as above
- res = d_exprMgr->mkAssociative(k, echildren);
+ res = d_nodeMgr->mkAssociative(k, echildren);
}
else
{
// integers and reals (both are Rationals).
// At the API, mkReal and mkInteger are different and therefore the
// element type can be used safely here.
- Node singleton = getNodeManager()->mkSingleton(type, *children[0].d_node);
- res = Term(this, singleton).getExpr();
+ res = getNodeManager()->mkSingleton(type, *children[0].d_node);
}
else if (kind == api::MK_BAG)
{
// integers and reals (both are Rationals).
// At the API, mkReal and mkInteger are different and therefore the
// element type can be used safely here.
- Node bag = getNodeManager()->mkBag(
+ res = getNodeManager()->mkBag(
type, *children[0].d_node, *children[1].d_node);
- res = Term(this, bag).getExpr();
}
else
{
- res = d_exprMgr->mkExpr(k, echildren);
+ res = d_nodeMgr->mkNode(k, echildren);
}
}
CVC4_API_SOLVER_TRY_CATCH_END;
}
-/* Helpers for converting vectors. */
-/* .......................................................................... */
-
-std::vector<Expr> Solver::termVectorToExprs(
- const std::vector<Term>& terms) const
-{
- std::vector<Expr> res;
- for (const Term& t : terms)
- {
- CVC4_API_SOLVER_CHECK_TERM(t);
- res.push_back(t.d_node->toExpr());
- }
- return res;
-}
-
/* Helpers for mkTerm checks. */
/* .......................................................................... */
Term Solver::mkTrue(void) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- return Term(this, d_exprMgr->mkConst<bool>(true));
+ return Term(this, d_nodeMgr->mkConst<bool>(true));
CVC4_API_SOLVER_TRY_CATCH_END;
}
Term Solver::mkFalse(void) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- return Term(this, d_exprMgr->mkConst<bool>(false));
+ return Term(this, d_nodeMgr->mkConst<bool>(false));
CVC4_API_SOLVER_TRY_CATCH_END;
}
Term Solver::mkBoolean(bool val) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- return Term(this, d_exprMgr->mkConst<bool>(val));
+ return Term(this, d_nodeMgr->mkConst<bool>(val));
CVC4_API_SOLVER_TRY_CATCH_END;
}
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- Expr res =
- d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
+ Node res =
+ d_nodeMgr->mkNullaryOperator(d_nodeMgr->realType(), CVC4::kind::PI);
(void)res.getType(true); /* kick off type checking */
return Term(this, res);
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- Expr res =
- d_exprMgr->mkExpr(CVC4::kind::REGEXP_EMPTY, std::vector<CVC4::Expr>());
+ Node res =
+ d_nodeMgr->mkNode(CVC4::kind::REGEXP_EMPTY, std::vector<CVC4::Node>());
(void)res.getType(true); /* kick off type checking */
return Term(this, res);
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- Expr res =
- d_exprMgr->mkExpr(CVC4::kind::REGEXP_SIGMA, std::vector<CVC4::Expr>());
+ Node res =
+ d_nodeMgr->mkNode(CVC4::kind::REGEXP_SIGMA, std::vector<CVC4::Node>());
(void)res.getType(true); /* kick off type checking */
return Term(this, res);
CVC4_API_SOLVER_CHECK_SORT(sort);
std::vector<Node> seq;
- Expr res = d_exprMgr->mkConst(Sequence(*sort.d_type, seq));
+ Node res = d_nodeMgr->mkConst(Sequence(*sort.d_type, seq));
return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
Term Solver::mkConstArray(Sort sort, Term val) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ NodeManagerScope scope(getNodeManager());
CVC4_API_ARG_CHECK_NOT_NULL(sort);
CVC4_API_ARG_CHECK_NOT_NULL(val);
CVC4_API_SOLVER_CHECK_SORT(sort);
CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
CVC4_API_SOLVER_CHECK_SORT(sort);
- Expr res = d_exprMgr->mkVar(symbol, sort.d_type->toType());
+ Node res = d_nodeMgr->mkVar(symbol, *sort.d_type);
(void)res.getType(true); /* kick off type checking */
return Term(this, res);
CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
CVC4_API_SOLVER_CHECK_SORT(sort);
- Expr res = d_exprMgr->mkVar(sort.d_type->toType());
+ Node res = d_nodeMgr->mkVar(*sort.d_type);
(void)res.getType(true); /* kick off type checking */
return Term(this, res);
Term Solver::mkVar(Sort sort, const std::string& symbol) const
{
+ NodeManagerScope scope(getNodeManager());
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
CVC4_API_SOLVER_CHECK_SORT(sort);
- Expr res = symbol.empty()
- ? d_exprMgr->mkBoundVar(sort.d_type->toType())
- : d_exprMgr->mkBoundVar(symbol, sort.d_type->toType());
+ Node res = symbol.empty() ? d_nodeMgr->mkBoundVar(*sort.d_type)
+ : d_nodeMgr->mkBoundVar(symbol, *sort.d_type);
(void)res.getType(true); /* kick off type checking */
return Term(this, res);
case BITVECTOR_REPEAT:
res = Op(this,
kind,
- mkValHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg))
- .d_node->toExpr());
+ *mkValHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg))
+ .d_node);
break;
case BITVECTOR_ZERO_EXTEND:
res = Op(this,
Term Solver::simplify(const Term& term)
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ NodeManagerScope scope(getNodeManager());
CVC4_API_ARG_CHECK_NOT_NULL(term);
CVC4_API_SOLVER_CHECK_TERM(term);
- return Term(this, d_smtEngine->simplify(term.d_node->toExpr()));
+ return Term(this, d_smtEngine->simplify(*term.d_node));
CVC4_API_SOLVER_TRY_CATCH_END;
}
Result Solver::checkEntailed(Term term) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ NodeManagerScope scope(getNodeManager());
CVC4_API_CHECK(!d_smtEngine->isQueryMade()
|| d_smtEngine->getOptions()[options::incrementalSolving])
<< "Cannot make multiple queries unless incremental solving is enabled "
Result Solver::checkEntailed(const std::vector<Term>& terms) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ NodeManagerScope scope(getNodeManager());
CVC4_API_CHECK(!d_smtEngine->isQueryMade()
|| d_smtEngine->getOptions()[options::incrementalSolving])
<< "Cannot make multiple queries unless incremental solving is enabled "
Result Solver::checkSat(void) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ NodeManagerScope scope(getNodeManager());
CVC4_API_CHECK(!d_smtEngine->isQueryMade()
|| d_smtEngine->getOptions()[options::incrementalSolving])
<< "Cannot make multiple queries unless incremental solving is enabled "
Result Solver::checkSatAssuming(Term assumption) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ NodeManagerScope scope(getNodeManager());
CVC4_API_CHECK(!d_smtEngine->isQueryMade()
|| d_smtEngine->getOptions()[options::incrementalSolving])
<< "Cannot make multiple queries unless incremental solving is enabled "
Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ NodeManagerScope scope(getNodeManager());
CVC4_API_CHECK(!d_smtEngine->isQueryMade() || assumptions.size() == 0
|| d_smtEngine->getOptions()[options::incrementalSolving])
<< "Cannot make multiple queries unless incremental solving is enabled "
std::vector<TypeNode> types = Sort::sortVectorToTypeNodes(sorts);
type = getNodeManager()->mkFunctionType(types, type);
}
- return Term(this, d_exprMgr->mkVar(symbol, type.toType()));
+ return Term(this, d_nodeMgr->mkVar(symbol, type));
CVC4_API_SOLVER_TRY_CATCH_END;
}
{
type = nm->mkFunctionType(domain_types, type);
}
- Node fun = Node::fromExpr(d_exprMgr->mkVar(symbol, type.toType()));
+ Node fun = d_nodeMgr->mkVar(symbol, type);
std::vector<Node> ebound_vars = Term::termVectorToNodes(bound_vars);
d_smtEngine->defineFunction(fun, ebound_vars, *term.d_node, global);
return Term(this, fun);
{
type = nm->mkFunctionType(domain_types, type);
}
- Node fun = Node::fromExpr(d_exprMgr->mkVar(symbol, type.toType()));
+ Node fun = d_nodeMgr->mkVar(symbol, type);
std::vector<Node> ebound_vars = Term::termVectorToNodes(bound_vars);
- d_smtEngine->defineFunctionRec(
- fun, ebound_vars, term.d_node->toExpr(), global);
+ d_smtEngine->defineFunctionRec(fun, ebound_vars, *term.d_node, global);
return Term(this, fun);
CVC4_API_SOLVER_TRY_CATCH_END;
}
std::vector<Term> Solver::getUnsatAssumptions(void) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ NodeManagerScope scope(getNodeManager());
CVC4_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving])
<< "Cannot get unsat assumptions unless incremental solving is enabled "
"(try --incremental)";
* return std::vector<Term>(uassumptions.begin(), uassumptions.end());
* here since constructor is private */
std::vector<Term> res;
- for (const Node& e : uassumptions)
+ for (const Node& n : uassumptions)
{
- res.push_back(Term(this, e.toExpr()));
+ res.push_back(Term(this, n));
}
return res;
CVC4_API_SOLVER_TRY_CATCH_END;
std::vector<Term> Solver::getUnsatCore(void) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ NodeManagerScope scope(getNodeManager());
CVC4_API_CHECK(d_smtEngine->getOptions()[options::unsatCores])
<< "Cannot get unsat core unless explicitly enabled "
"(try --produce-unsat-cores)";
std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ NodeManagerScope scope(getNodeManager());
CVC4_API_RECOVERABLE_CHECK(d_smtEngine->getOptions()[options::produceModels])
<< "Cannot get value unless model generation is enabled "
"(try --produce-models)";
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_ARG_CHECK_NOT_NULL(q);
CVC4_API_SOLVER_CHECK_TERM(q);
- CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ NodeManagerScope scope(getNodeManager());
return Term(this,
d_smtEngine->getQuantifierElimination(q.getNode(), true, true));
CVC4_API_SOLVER_TRY_CATCH_END;
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_ARG_CHECK_NOT_NULL(q);
CVC4_API_SOLVER_CHECK_TERM(q);
- CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ NodeManagerScope scope(getNodeManager());
return Term(
this, d_smtEngine->getQuantifierElimination(q.getNode(), false, true));
CVC4_API_SOLVER_TRY_CATCH_END;
d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP))
<< "Cannot obtain separation logic expressions if not using the "
"separation logic theory.";
- CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ NodeManagerScope scope(getNodeManager());
CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
<< "Cannot get separation heap term unless model generation is enabled "
"(try --produce-models)";
d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP))
<< "Cannot obtain separation logic expressions if not using the "
"separation logic theory.";
- CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ NodeManagerScope scope(getNodeManager());
CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
<< "Cannot get separation nil term unless model generation is enabled "
"(try --produce-models)";
void Solver::pop(uint32_t nscopes) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ NodeManagerScope scope(getNodeManager());
CVC4_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving])
<< "Cannot pop when not solving incrementally (use --incremental)";
CVC4_API_CHECK(nscopes <= d_smtEngine->getNumUserLevels())
bool Solver::getInterpolant(Term conj, Term& output) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ NodeManagerScope scope(getNodeManager());
Node result;
bool success = d_smtEngine->getInterpol(*conj.d_node, result);
if (success)
bool Solver::getInterpolant(Term conj, Grammar& g, Term& output) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ NodeManagerScope scope(getNodeManager());
Node result;
bool success =
d_smtEngine->getInterpol(*conj.d_node, *g.resolve().d_type, result);
bool Solver::getAbduct(Term conj, Term& output) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ NodeManagerScope scope(getNodeManager());
Node result;
bool success = d_smtEngine->getAbduct(*conj.d_node, result);
if (success)
bool Solver::getAbduct(Term conj, Grammar& g, Term& output) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ NodeManagerScope scope(getNodeManager());
Node result;
bool success =
d_smtEngine->getAbduct(*conj.d_node, *g.resolve().d_type, result);
void Solver::blockModel() const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ NodeManagerScope scope(getNodeManager());
CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
<< "Cannot get value unless model generation is enabled "
"(try --produce-models)";
this == terms[i].d_solver, "term", terms[i], i)
<< "a term associated to this solver object";
}
- CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ NodeManagerScope scope(getNodeManager());
d_smtEngine->blockModelValues(Term::termVectorToNodes(terms));
CVC4_API_SOLVER_TRY_CATCH_END;
}
void Solver::printInstantiations(std::ostream& out) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ NodeManagerScope scope(getNodeManager());
d_smtEngine->printInstantiations(out);
CVC4_API_SOLVER_TRY_CATCH_END;
}
void Solver::push(uint32_t nscopes) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ NodeManagerScope scope(getNodeManager());
CVC4_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving])
<< "Cannot push when not solving incrementally (use --incremental)";
// advantage wrt using TO_REAL since (constant) division is always included
// in the theory.
res = Term(this,
- d_exprMgr->mkExpr(extToIntKind(DIVISION),
- res.d_node->toExpr(),
- d_exprMgr->mkConst(CVC4::Rational(1))));
+ d_nodeMgr->mkNode(extToIntKind(DIVISION),
+ *res.d_node,
+ d_nodeMgr->mkConst(CVC4::Rational(1))));
}
Assert(res.getSort() == sort);
return res;
* !!! This is only temporarily available until the parser is fully migrated to
* the new API. !!!
*/
-ExprManager* Solver::getExprManager(void) const { return d_exprMgr.get(); }
-
-/**
- * !!! This is only temporarily available until the parser is fully migrated to
- * the new API. !!!
- */
-NodeManager* Solver::getNodeManager(void) const
-{
- return d_exprMgr->getNodeManager();
-}
+NodeManager* Solver::getNodeManager(void) const { return d_nodeMgr.get(); }
/**
* !!! This is only temporarily available until the parser is fully migrated to
*/
Options& Solver::getOptions(void) { return d_smtEngine->getOptions(); }
-/* -------------------------------------------------------------------------- */
-/* Conversions */
-/* -------------------------------------------------------------------------- */
-
-std::vector<Expr> termVectorToExprs(const std::vector<Term>& terms)
-{
- std::vector<Expr> exprs;
- for (size_t i = 0, tsize = terms.size(); i < tsize; i++)
- {
- exprs.push_back(terms[i].getExpr());
- }
- return exprs;
-}
-
} // namespace api
/* -------------------------------------------------------------------------- */
class BlockModelValuesCommand;
class CheckSatCommand;
class CheckSatAssumingCommand;
-class Expr;
class DatatypeDeclarationCommand;
class DeclareFunctionCommand;
class DeclareHeapCommand;
class DType;
class DTypeConstructor;
class DTypeSelector;
-class ExprManager;
class GetAbductCommand;
class GetInterpolCommand;
class GetModelCommand;
/**
* The interal result wrapped by this result.
- * This is a shared_ptr rather than a unique_ptr since CVC4::Result is
- * not ref counted.
+ * Note: This is a shared_ptr rather than a unique_ptr since CVC4::Result is
+ * not ref counted.
*/
std::shared_ptr<CVC4::Result> d_result;
};
/** Helper to convert a set of Sorts to internal TypeNodes. */
std::set<TypeNode> static sortSetToTypeNodes(const std::set<Sort>& sorts);
- /* Helper to convert a vector of Sorts to internal TypeNodes. */
+ /** Helper to convert a vector of Sorts to internal TypeNodes. */
std::vector<TypeNode> static sortVectorToTypeNodes(
const std::vector<Sort>& sorts);
/** Helper to convert a vector of internal TypeNodes to Sorts. */
/**
* The interal type wrapped by this sort.
- * This is a shared_ptr rather than a unique_ptr to avoid overhead due to
- * memory allocation (CVC4::Type is already ref counted, so this could be
- * a unique_ptr instead).
+ * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due
+ * to memory allocation (CVC4::Type is already ref counted, so this
+ * could be a unique_ptr instead).
*/
std::shared_ptr<CVC4::TypeNode> d_type;
};
*/
Op(const Solver* slv, const Kind k);
- /**
- * Constructor.
- * @param slv the associated solver object
- * @param k the kind of this Op
- * @param e the internal expression that is to be wrapped by this term
- * @return the Term
- */
- Op(const Solver* slv, const Kind k, const CVC4::Expr& e);
-
/**
* Constructor.
* @param slv the associated solver object
bool isNullHelper() const;
/**
- * Note: An indexed operator has a non-null internal expr, d_expr
+ * Note: An indexed operator has a non-null internal node, d_node
* Note 2: We use a helper method to avoid having API functions call
* other API functions (we need to call this internally)
* @return true iff this Op is indexed
*/
const Solver* d_solver;
- /* The kind of this operator. */
+ /** The kind of this operator. */
Kind d_kind;
/**
- * The internal expression wrapped by this operator.
- * This is a shared_ptr rather than a unique_ptr to avoid overhead due to
- * memory allocation (CVC4::Expr is already ref counted, so this could be
- * a unique_ptr instead).
+ * The internal node wrapped by this operator.
+ * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due
+ * to memory allocation (CVC4::Node is already ref counted, so this
+ * could be a unique_ptr instead).
*/
std::shared_ptr<CVC4::Node> d_node;
};
/**
* Constructor
* @param slv the associated solver object
- * @param e a shared pointer to the expression that we're iterating over
+ * @param e a shared pointer to the node that we're iterating over
* @param p the position of the iterator (e.g. which child it's on)
*/
const_iterator(const Solver* slv,
* The associated solver object.
*/
const Solver* d_solver;
- /* The original node to be iterated over */
+ /** The original node to be iterated over. */
std::shared_ptr<CVC4::Node> d_origNode;
- /* Keeps track of the iteration position */
+ /** Keeps track of the iteration position. */
uint32_t d_pos;
};
*/
const_iterator end() const;
- // !!! This is only temporarily available until the parser is fully migrated
- // to the new API. !!!
- CVC4::Expr getExpr(void) const;
-
/**
* @return true if the term is an integer that fits within std::int32_t.
*/
const Solver* d_solver;
private:
- /* Helper to convert a vector of Terms to internal Nodes. */
+ /** Helper to convert a vector of Terms to internal Nodes. */
std::vector<Node> static termVectorToNodes(const std::vector<Term>& terms);
- /**
- * Constructor.
- * @param slv the associated solver object
- * @param e the internal expression that is to be wrapped by this term
- * @return the Term
- */
- Term(const Solver* slv, const CVC4::Expr& e);
-
/**
* Constructor.
* @param slv the associated solver object
*/
bool isCastedReal() const;
/**
- * The internal expression wrapped by this term.
- * This is a shared_ptr rather than a unique_ptr to avoid overhead due to
- * memory allocation (CVC4::Expr is already ref counted, so this could be
- * a unique_ptr instead).
+ * The internal node wrapped by this term.
+ * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due
+ * to memory allocation (CVC4::Node is already ref counted, so this
+ * could be a unique_ptr instead).
*/
std::shared_ptr<CVC4::Node> d_node;
};
/**
* The internal (intermediate) datatype constructor wrapped by this
* datatype constructor declaration.
- * This is a shared_ptr rather than a unique_ptr since
- * CVC4::DTypeConstructor is not ref counted.
+ * Note: This is a shared_ptr rather than a unique_ptr since
+ * CVC4::DTypeConstructor is not ref counted.
*/
std::shared_ptr<CVC4::DTypeConstructor> d_ctor;
};
*/
const Solver* d_solver;
- /* The internal (intermediate) datatype wrapped by this datatype
- * declaration
- * This is a shared_ptr rather than a unique_ptr since CVC4::DType is
- * not ref counted.
+ /**
+ * The internal (intermediate) datatype wrapped by this datatype
+ * declaration.
+ * Note: This is a shared_ptr rather than a unique_ptr since CVC4::DType is
+ * not ref counted.
*/
std::shared_ptr<CVC4::DType> d_dtype;
};
/**
* The internal datatype selector wrapped by this datatype selector.
- * This is a shared_ptr rather than a unique_ptr since CVC4::DType is
- * not ref counted.
+ * Note: This is a shared_ptr rather than a unique_ptr since CVC4::DType is
+ * not ref counted.
*/
std::shared_ptr<CVC4::DTypeSelector> d_stor;
};
*/
const Solver* d_solver;
- /* A pointer to the list of selectors of the internal datatype
+ /**
+ * A pointer to the list of selectors of the internal datatype
* constructor to iterate over.
- * This pointer is maintained for operators == and != only. */
+ * This pointer is maintained for operators == and != only.
+ */
const void* d_int_stors;
- /* The list of datatype selector (wrappers) to iterate over. */
+ /** The list of datatype selector (wrappers) to iterate over. */
std::vector<DatatypeSelector> d_stors;
- /* The current index of the iterator. */
+ /** The current index of the iterator. */
size_t d_idx;
};
/**
* The internal datatype constructor wrapped by this datatype constructor.
- * This is a shared_ptr rather than a unique_ptr since CVC4::DType is
- * not ref counted.
+ * Note: This is a shared_ptr rather than a unique_ptr since CVC4::DType is
+ * not ref counted.
*/
std::shared_ptr<CVC4::DTypeConstructor> d_ctor;
};
*/
const Solver* d_solver;
- /* A pointer to the list of constructors of the internal datatype
+ /**
+ * A pointer to the list of constructors of the internal datatype
* to iterate over.
- * This pointer is maintained for operators == and != only. */
+ * This pointer is maintained for operators == and != only.
+ */
const void* d_int_ctors;
- /* The list of datatype constructor (wrappers) to iterate over. */
+ /** The list of datatype constructor (wrappers) to iterate over. */
std::vector<DatatypeConstructor> d_ctors;
- /* The current index of the iterator. */
+ /** The current index of the iterator. */
size_t d_idx;
};
/**
* The internal datatype wrapped by this datatype.
- * This is a shared_ptr rather than a unique_ptr since CVC4::DType is
- * not ref counted.
+ * Note: This is a shared_ptr rather than a unique_ptr since CVC4::DType is
+ * not ref counted.
*/
std::shared_ptr<CVC4::DType> d_dtype;
};
*/
class CVC4_PUBLIC Solver
{
+ friend class Datatype;
+ friend class DatatypeDecl;
+ friend class DatatypeConstructor;
+ friend class DatatypeConstructorDecl;
+ friend class DatatypeSelector;
+ friend class Grammar;
+ friend class Op;
+ friend class Sort;
+ friend class Term;
+
public:
/* .................................................................... */
/* Constructors/Destructors */
*/
void printSynthSolution(std::ostream& out) const;
- // !!! This is only temporarily available until the parser is fully migrated
- // to the new API. !!!
- ExprManager* getExprManager(void) const;
-
- // !!! This is only temporarily available until the parser is fully migrated
- // to the new API. !!!
- NodeManager* getNodeManager(void) const;
// !!! This is only temporarily available until the parser is fully migrated
// to the new API. !!!
Options& getOptions(void);
private:
- /* Helper to convert a vector of Terms to internal Exprs. */
- std::vector<Expr> termVectorToExprs(const std::vector<Term>& vector) const;
- /* Helper to check for API misuse in mkOp functions. */
+ /** @return the node manager of this solver */
+ NodeManager* getNodeManager(void) const;
+ /** Helper to check for API misuse in mkOp functions. */
void checkMkTerm(Kind kind, uint32_t nchildren) const;
- /* Helper for mk-functions that call d_exprMgr->mkConst(). */
+ /** Helper for mk-functions that call d_nodeMgr->mkConst(). */
template <typename T>
Term mkValHelper(T t) const;
- /* Helper for mkReal functions that take a string as argument. */
+ /** Helper for mkReal functions that take a string as argument. */
Term mkRealFromStrHelper(const std::string& s) const;
- /* Helper for mkBitVector functions that take a string as argument. */
+ /** Helper for mkBitVector functions that take a string as argument. */
Term mkBVFromStrHelper(const std::string& s, uint32_t base) const;
- /* Helper for mkBitVector functions that take a string and a size as
- * arguments. */
+ /**
+ * Helper for mkBitVector functions that take a string and a size as
+ * arguments.
+ */
Term mkBVFromStrHelper(uint32_t size,
const std::string& s,
uint32_t base) const;
- /* Helper for mkBitVector functions that take an integer as argument. */
+ /** Helper for mkBitVector functions that take an integer as argument. */
Term mkBVFromIntHelper(uint32_t size, uint64_t val) const;
- /* Helper for setLogic. */
+ /** Helper for setLogic. */
void setLogicHelper(const std::string& logic) const;
- /* Helper for mkTerm functions that create Term from a Kind */
+ /** Helper for mkTerm functions that create Term from a Kind */
Term mkTermFromKind(Kind kind) const;
- /* Helper for mkChar functions that take a string as argument. */
+ /** Helper for mkChar functions that take a string as argument. */
Term mkCharFromStrHelper(const std::string& s) const;
/** Get value helper, which accounts for subtyping */
Term getValueHelper(Term term) const;
/** check whether string s is a valid decimal integer */
bool isValidInteger(const std::string& s) const;
- /* The expression manager of this solver. */
- std::unique_ptr<ExprManager> d_exprMgr;
- /* The SMT engine of this solver. */
+ /** The node manager of this solver. */
+ std::unique_ptr<NodeManager> d_nodeMgr;
+ /** The SMT engine of this solver. */
std::unique_ptr<SmtEngine> d_smtEngine;
- /* The random number generator of this solver. */
+ /** The random number generator of this solver. */
std::unique_ptr<Random> d_rng;
};
-// !!! Only temporarily public until the parser is fully migrated to the
-// new API. !!!
-std::vector<Expr> termVectorToExprs(const std::vector<Term>& terms);
-
} // namespace api
// !!! Only temporarily public until the parser is fully migrated to the
projects / cvc5.git / commitdiff