summaryrefslogtreecommitdiff
path: root/src/api/cvc4cpp.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/api/cvc4cpp.cpp')
-rw-r--r--src/api/cvc4cpp.cpp239
1 files changed, 86 insertions, 153 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 974567380..bca1d147c 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -41,9 +41,6 @@
#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"
@@ -687,7 +684,7 @@ uint32_t minArity(Kind k)
{
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
@@ -702,7 +699,7 @@ uint32_t maxArity(Kind k)
{
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
@@ -1401,11 +1398,6 @@ Op::Op(const Solver* slv, const Kind k)
{
}
-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))
{
@@ -1636,7 +1628,7 @@ size_t OpHashFunction::operator()(const Op& t) const
{
if (t.isIndexedHelper())
{
- return ExprHashFunction()(t.d_node->toExpr());
+ return NodeHashFunction()(*t.d_node);
}
else
{
@@ -1650,13 +1642,6 @@ size_t OpHashFunction::operator()(const Op& t) const
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.
@@ -1768,12 +1753,12 @@ Term Term::operator[](size_t index) const
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
@@ -1870,7 +1855,7 @@ bool Term::isNull() const { return isNullHelper(); }
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)
@@ -2122,18 +2107,6 @@ Term::const_iterator Term::end() const
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 {
@@ -3045,9 +3018,10 @@ Sort Grammar::resolve()
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());
@@ -3124,14 +3098,14 @@ void Grammar::addSygusConstructorTerm(
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);
@@ -3161,8 +3135,7 @@ Term Grammar::purifySygusGTerm(
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)
{
@@ -3250,8 +3223,8 @@ size_t RoundingModeHashFunction::operator()(const RoundingMode& rm) const
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]));
@@ -3366,22 +3339,23 @@ Term Solver::getValueHelper(Term term) const
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);
@@ -3403,48 +3377,48 @@ Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const
<< "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
{
@@ -3460,8 +3434,7 @@ Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const
// 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)
{
@@ -3473,13 +3446,12 @@ Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const
// 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);
}
}
@@ -3524,21 +3496,6 @@ std::vector<Sort> Solver::mkDatatypeSortsInternal(
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. */
/* .......................................................................... */
@@ -3903,21 +3860,21 @@ Sort Solver::mkTupleSort(const std::vector<Sort>& sorts) const
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;
}
@@ -3925,8 +3882,8 @@ Term Solver::mkPi() const
{
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);
@@ -4037,8 +3994,8 @@ Term Solver::mkRegexpEmpty() const
{
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);
@@ -4049,8 +4006,8 @@ Term Solver::mkRegexpSigma() const
{
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);
@@ -4133,7 +4090,7 @@ Term Solver::mkEmptySequence(Sort sort) const
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;
@@ -4180,7 +4137,7 @@ Term Solver::mkBitVector(uint32_t size,
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);
@@ -4340,7 +4297,7 @@ Term Solver::mkConst(Sort sort, const std::string& symbol) const
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);
@@ -4354,7 +4311,7 @@ Term Solver::mkConst(Sort sort) const
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);
@@ -4366,13 +4323,13 @@ Term Solver::mkConst(Sort sort) const
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);
@@ -4610,8 +4567,8 @@ Op Solver::mkOp(Kind kind, uint32_t arg) const
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,
@@ -4794,11 +4751,11 @@ Op Solver::mkOp(Kind kind, const std::vector<uint32_t>& args) const
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;
}
@@ -4806,7 +4763,7 @@ Term Solver::simplify(const Term& term)
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 "
@@ -4823,7 +4780,7 @@ Result Solver::checkEntailed(Term term) const
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 "
@@ -4862,7 +4819,7 @@ void Solver::assertFormula(Term term) const
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 "
@@ -4878,7 +4835,7 @@ Result Solver::checkSat(void) const
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 "
@@ -4895,7 +4852,7 @@ Result Solver::checkSatAssuming(Term assumption) const
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 "
@@ -4962,7 +4919,7 @@ Term Solver::declareFun(const std::string& symbol,
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;
}
@@ -5020,7 +4977,7 @@ Term Solver::defineFun(const std::string& symbol,
{
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);
@@ -5128,10 +5085,9 @@ Term Solver::defineFunRec(const std::string& symbol,
{
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;
}
@@ -5333,7 +5289,7 @@ std::string Solver::getOption(const std::string& option) const
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)";
@@ -5348,9 +5304,9 @@ std::vector<Term> Solver::getUnsatAssumptions(void) const
* 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;
@@ -5362,7 +5318,7 @@ std::vector<Term> Solver::getUnsatAssumptions(void) const
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)";
@@ -5398,7 +5354,7 @@ Term Solver::getValue(Term term) const
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)";
@@ -5422,7 +5378,7 @@ Term Solver::getQuantifierElimination(api::Term q) const
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;
@@ -5433,7 +5389,7 @@ Term Solver::getQuantifierEliminationDisjunct(api::Term q) const
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;
@@ -5457,7 +5413,7 @@ Term Solver::getSeparationHeap() const
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)";
@@ -5474,7 +5430,7 @@ Term Solver::getSeparationNilTerm() const
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)";
@@ -5490,7 +5446,7 @@ Term Solver::getSeparationNilTerm() const
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())
@@ -5507,7 +5463,7 @@ void Solver::pop(uint32_t nscopes) const
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)
@@ -5521,7 +5477,7 @@ bool Solver::getInterpolant(Term conj, Term& output) const
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);
@@ -5536,7 +5492,7 @@ bool Solver::getInterpolant(Term conj, Grammar& g, Term& output) const
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)
@@ -5550,7 +5506,7 @@ bool Solver::getAbduct(Term conj, Term& output) const
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);
@@ -5565,7 +5521,7 @@ bool Solver::getAbduct(Term conj, Grammar& g, Term& output) const
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)";
@@ -5594,7 +5550,7 @@ void Solver::blockModelValues(const std::vector<Term>& terms) const
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;
}
@@ -5602,7 +5558,7 @@ void Solver::blockModelValues(const std::vector<Term>& terms) const
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;
}
@@ -5613,7 +5569,7 @@ void Solver::printInstantiations(std::ostream& out) const
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)";
@@ -5711,9 +5667,9 @@ Term Solver::ensureTermSort(const Term& term, const Sort& sort) const
// 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;
@@ -6001,16 +5957,7 @@ void Solver::printSynthSolution(std::ostream& out) const
* !!! 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
@@ -6024,20 +5971,6 @@ SmtEngine* Solver::getSmtEngine(void) const { return d_smtEngine.get(); }
*/
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
/* -------------------------------------------------------------------------- */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback