summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/api/cvc4cpp.cpp239
-rw-r--r--src/api/cvc4cpp.h163
-rw-r--r--src/expr/expr_manager_template.cpp6
-rw-r--r--src/expr/node_manager.h17
-rw-r--r--src/expr/type_checker_template.cpp2
5 files changed, 176 insertions, 251 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
/* -------------------------------------------------------------------------- */
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 962fa55ab..84e6cd496 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -44,7 +44,6 @@ class AssertCommand;
class BlockModelValuesCommand;
class CheckSatCommand;
class CheckSatAssumingCommand;
-class Expr;
class DatatypeDeclarationCommand;
class DeclareFunctionCommand;
class DeclareHeapCommand;
@@ -56,7 +55,6 @@ class DefineSortCommand;
class DType;
class DTypeConstructor;
class DTypeSelector;
-class ExprManager;
class GetAbductCommand;
class GetInterpolCommand;
class GetModelCommand;
@@ -211,8 +209,8 @@ class CVC4_PUBLIC Result
/**
* 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;
};
@@ -710,7 +708,7 @@ class CVC4_PUBLIC Sort
/** 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. */
@@ -739,9 +737,9 @@ class CVC4_PUBLIC Sort
/**
* 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;
};
@@ -851,15 +849,6 @@ class CVC4_PUBLIC Op
* 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
- * @param k the kind of this Op
* @param n the internal node that is to be wrapped by this term
* @return the Term
*/
@@ -872,7 +861,7 @@ class CVC4_PUBLIC Op
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
@@ -884,14 +873,14 @@ class CVC4_PUBLIC Op
*/
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;
};
@@ -1128,7 +1117,7 @@ class CVC4_PUBLIC Term
/**
* 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,
@@ -1184,9 +1173,9 @@ class CVC4_PUBLIC Term
* 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;
};
@@ -1200,10 +1189,6 @@ class CVC4_PUBLIC Term
*/
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.
*/
@@ -1270,20 +1255,12 @@ class CVC4_PUBLIC Term
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
* @param n the internal node that is to be wrapped by this term
* @return the Term
*/
@@ -1311,10 +1288,10 @@ class CVC4_PUBLIC Term
*/
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;
};
@@ -1461,8 +1438,8 @@ class CVC4_PUBLIC DatatypeConstructorDecl
/**
* 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;
};
@@ -1564,10 +1541,11 @@ class CVC4_PUBLIC DatatypeDecl
*/
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;
};
@@ -1624,8 +1602,8 @@ class CVC4_PUBLIC DatatypeSelector
/**
* 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;
};
@@ -1793,15 +1771,17 @@ class CVC4_PUBLIC DatatypeConstructor
*/
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;
};
@@ -1837,8 +1817,8 @@ class CVC4_PUBLIC DatatypeConstructor
/**
* 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;
};
@@ -2001,15 +1981,17 @@ class CVC4_PUBLIC Datatype
*/
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;
};
@@ -2045,8 +2027,8 @@ class CVC4_PUBLIC Datatype
/**
* 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;
};
@@ -2286,6 +2268,16 @@ struct CVC4_PUBLIC RoundingModeHashFunction
*/
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 */
@@ -3545,13 +3537,6 @@ class CVC4_PUBLIC Solver
*/
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. !!!
@@ -3562,29 +3547,31 @@ class CVC4_PUBLIC Solver
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;
@@ -3644,18 +3631,14 @@ class CVC4_PUBLIC Solver
/** 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
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 43161fe04..5dd7a4dfd 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -695,7 +695,8 @@ Expr ExprManager::mkVar(Type type)
return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode));
}
-Expr ExprManager::mkBoundVar(const std::string& name, Type type) {
+Expr ExprManager::mkBoundVar(const std::string& name, Type type)
+{
NodeManagerScope nms(d_nodeManager);
Node* n = d_nodeManager->mkBoundVarPtr(name, *type.d_typeNode);
Debug("nm") << "set " << name << " on " << *n << std::endl;
@@ -703,7 +704,8 @@ Expr ExprManager::mkBoundVar(const std::string& name, Type type) {
return Expr(this, n);
}
-Expr ExprManager::mkBoundVar(Type type) {
+Expr ExprManager::mkBoundVar(Type type)
+{
NodeManagerScope nms(d_nodeManager);
INC_STAT_VAR(type, true);
return Expr(this, d_nodeManager->mkBoundVarPtr(*type.d_typeNode));
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 076b6d164..319ab4461 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -40,6 +40,10 @@
namespace CVC4 {
+namespace api {
+class Solver;
+}
+
class StatisticsRegistry;
class ResourceManager;
class SkolemManager;
@@ -82,16 +86,19 @@ class NodeManagerListener {
virtual void nmNotifyDeleteNode(TNode n) {}
}; /* class NodeManagerListener */
-class NodeManager {
- template <unsigned nchild_thresh> friend class CVC4::NodeBuilder;
- friend class NodeManagerScope;
+class NodeManager
+{
+ friend class api::Solver;
friend class expr::NodeValue;
friend class expr::TypeChecker;
-
// friends so they can access mkVar() here, which is private
friend Expr ExprManager::mkVar(const std::string&, Type);
friend Expr ExprManager::mkVar(Type);
+ template <unsigned nchild_thresh>
+ friend class NodeBuilder;
+ friend class NodeManagerScope;
+
/** Predicate for use with STL algorithms */
struct NodeValueReferenceCountNonZero {
bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; }
@@ -1147,7 +1154,7 @@ class NodeManager {
* any published code!
*/
void debugHook(int debugFlag);
-};/* class NodeManager */
+}; /* class NodeManager */
/**
* This class changes the "current" thread-global
diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
index f5a729b36..3436cc138 100644
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -44,7 +44,7 @@ ${typerules}
default:
Debug("getType") << "FAILURE" << std::endl;
- Unhandled() << n.getKind();
+ Unhandled() << " " << n.getKind();
}
nodeManager->setAttribute(n, TypeAttr(), typeNode);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback