From e8bbee7afb039834955aee96d181b499550a28fe Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 28 Jul 2020 11:59:28 -0700 Subject: [PATCH] Replace Expr with Node in Term/Op (#4781) This commit changes Term and Op to use Nodes internally instead of Exprs. This is a step towards removing the Expr-layer. This commit also adds some missing checks regarding the number of arguments for a given kind that were previously missing, which caused issues in unit tests when using Node instead of Expr. --- src/api/cvc4cpp.cpp | 610 ++++++++++++++++++++++++----------------- src/api/cvc4cpp.h | 44 ++- src/expr/type_node.h | 1 + src/smt/smt_engine.cpp | 4 +- src/smt/smt_engine.h | 2 +- 5 files changed, 402 insertions(+), 259 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index c009f69e5..2da791da0 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -43,6 +43,7 @@ #include "expr/expr_manager_scope.h" #include "expr/kind.h" #include "expr/metakind.h" +#include "expr/node.h" #include "expr/node_manager.h" #include "expr/sequence.h" #include "expr/type.h" @@ -644,7 +645,15 @@ uint32_t minArity(Kind k) { Assert(isDefinedKind(k)); Assert(isDefinedIntKind(extToIntKind(k))); - return CVC4::ExprManager::minArity(extToIntKind(k)); + uint32_t min = CVC4::ExprManager::minArity(extToIntKind(k)); + + // At the API level, we treat functions/constructors/selectors/testers as + // normal terms instead of making them part of the operator + if (isApplyKind(extToIntKind(k))) + { + min++; + } + return min; } uint32_t maxArity(Kind k) @@ -653,9 +662,8 @@ uint32_t maxArity(Kind k) Assert(isDefinedIntKind(extToIntKind(k))); uint32_t max = CVC4::ExprManager::maxArity(extToIntKind(k)); - // special cases for API level - // higher-order logic perspective at API - // functions/constructors/selectors/testers are terms + // At the API level, we treat functions/constructors/selectors/testers as + // normal terms instead of making them part of the operator if (isApplyKind(extToIntKind(k)) && max != std::numeric_limits::max()) // be careful not to // overflow @@ -1159,19 +1167,33 @@ size_t SortHashFunction::operator()(const Sort& s) const /* Op */ /* -------------------------------------------------------------------------- */ -Op::Op() : d_solver(nullptr), d_kind(NULL_EXPR), d_expr(new CVC4::Expr()) {} +Op::Op() : d_solver(nullptr), d_kind(NULL_EXPR), d_node(new CVC4::Node()) {} Op::Op(const Solver* slv, const Kind k) - : d_solver(slv), d_kind(k), d_expr(new CVC4::Expr()) + : d_solver(slv), d_kind(k), d_node(new CVC4::Node()) { } Op::Op(const Solver* slv, const Kind k, const CVC4::Expr& e) - : d_solver(slv), d_kind(k), d_expr(new 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)) { } -Op::~Op() {} +Op::~Op() +{ + if (d_solver != nullptr) + { + // Ensure that the correct node manager is in scope when the node is + // destroyed. + NodeManagerScope scope(d_solver->getNodeManager()); + d_node.reset(); + } +} /* Helpers */ /* -------------------------------------------------------------------------- */ @@ -1181,23 +1203,23 @@ Op::~Op() {} bool Op::isNullHelper() const { - return (d_expr->isNull() && (d_kind == NULL_EXPR)); + return (d_node->isNull() && (d_kind == NULL_EXPR)); } -bool Op::isIndexedHelper() const { return !d_expr->isNull(); } +bool Op::isIndexedHelper() const { return !d_node->isNull(); } /* Public methods */ bool Op::operator==(const Op& t) const { - if (d_expr->isNull() && t.d_expr->isNull()) + if (d_node->isNull() && t.d_node->isNull()) { return (d_kind == t.d_kind); } - else if (d_expr->isNull() || t.d_expr->isNull()) + else if (d_node->isNull() || t.d_node->isNull()) { return false; } - return (d_kind == t.d_kind) && (*d_expr == *t.d_expr); + return (d_kind == t.d_kind) && (*d_node == *t.d_node); } bool Op::operator!=(const Op& t) const { return !(*this == t); } @@ -1216,22 +1238,22 @@ template <> std::string Op::getIndices() const { CVC4_API_CHECK_NOT_NULL; - CVC4_API_CHECK(!d_expr->isNull()) + CVC4_API_CHECK(!d_node->isNull()) << "Expecting a non-null internal expression. This Op is not indexed."; std::string i; - Kind k = intToExtKind(d_expr->getKind()); + Kind k = intToExtKind(d_node->getKind()); if (k == DIVISIBLE) { // DIVISIBLE returns a string index to support // arbitrary precision integers - CVC4::Integer _int = d_expr->getConst().k; + CVC4::Integer _int = d_node->getConst().k; i = _int.toString(); } else if (k == RECORD_UPDATE) { - i = d_expr->getConst().getField(); + i = d_node->getConst().getField(); } else { @@ -1246,37 +1268,37 @@ template <> uint32_t Op::getIndices() const { CVC4_API_CHECK_NOT_NULL; - CVC4_API_CHECK(!d_expr->isNull()) + CVC4_API_CHECK(!d_node->isNull()) << "Expecting a non-null internal expression. This Op is not indexed."; uint32_t i = 0; - Kind k = intToExtKind(d_expr->getKind()); + Kind k = intToExtKind(d_node->getKind()); switch (k) { case BITVECTOR_REPEAT: - i = d_expr->getConst().d_repeatAmount; + i = d_node->getConst().d_repeatAmount; break; case BITVECTOR_ZERO_EXTEND: - i = d_expr->getConst().d_zeroExtendAmount; + i = d_node->getConst().d_zeroExtendAmount; break; case BITVECTOR_SIGN_EXTEND: - i = d_expr->getConst().d_signExtendAmount; + i = d_node->getConst().d_signExtendAmount; break; case BITVECTOR_ROTATE_LEFT: - i = d_expr->getConst().d_rotateLeftAmount; + i = d_node->getConst().d_rotateLeftAmount; break; case BITVECTOR_ROTATE_RIGHT: - i = d_expr->getConst().d_rotateRightAmount; + i = d_node->getConst().d_rotateRightAmount; break; - case INT_TO_BITVECTOR: i = d_expr->getConst().d_size; break; - case IAND: i = d_expr->getConst().d_size; break; + case INT_TO_BITVECTOR: i = d_node->getConst().d_size; break; + case IAND: i = d_node->getConst().d_size; break; case FLOATINGPOINT_TO_UBV: - i = d_expr->getConst().bvs.d_size; + i = d_node->getConst().bvs.d_size; break; case FLOATINGPOINT_TO_SBV: - i = d_expr->getConst().bvs.d_size; + i = d_node->getConst().bvs.d_size; break; - case TUPLE_UPDATE: i = d_expr->getConst().getIndex(); break; + case TUPLE_UPDATE: i = d_node->getConst().getIndex(); break; default: CVC4ApiExceptionStream().ostream() << "Can't get uint32_t index from" << " kind " << kindToString(k); @@ -1288,51 +1310,51 @@ template <> std::pair Op::getIndices() const { CVC4_API_CHECK_NOT_NULL; - CVC4_API_CHECK(!d_expr->isNull()) + CVC4_API_CHECK(!d_node->isNull()) << "Expecting a non-null internal expression. This Op is not indexed."; std::pair indices; - Kind k = intToExtKind(d_expr->getKind()); + Kind k = intToExtKind(d_node->getKind()); // using if/else instead of case statement because want local variables if (k == BITVECTOR_EXTRACT) { - CVC4::BitVectorExtract ext = d_expr->getConst(); + CVC4::BitVectorExtract ext = d_node->getConst(); indices = std::make_pair(ext.d_high, ext.d_low); } else if (k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR) { CVC4::FloatingPointToFPIEEEBitVector ext = - d_expr->getConst(); + d_node->getConst(); indices = std::make_pair(ext.t.exponent(), ext.t.significand()); } else if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT) { CVC4::FloatingPointToFPFloatingPoint ext = - d_expr->getConst(); + d_node->getConst(); indices = std::make_pair(ext.t.exponent(), ext.t.significand()); } else if (k == FLOATINGPOINT_TO_FP_REAL) { - CVC4::FloatingPointToFPReal ext = d_expr->getConst(); + CVC4::FloatingPointToFPReal ext = d_node->getConst(); indices = std::make_pair(ext.t.exponent(), ext.t.significand()); } else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR) { CVC4::FloatingPointToFPSignedBitVector ext = - d_expr->getConst(); + d_node->getConst(); indices = std::make_pair(ext.t.exponent(), ext.t.significand()); } else if (k == FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR) { CVC4::FloatingPointToFPUnsignedBitVector ext = - d_expr->getConst(); + d_node->getConst(); indices = std::make_pair(ext.t.exponent(), ext.t.significand()); } else if (k == FLOATINGPOINT_TO_FP_GENERIC) { CVC4::FloatingPointToFPGeneric ext = - d_expr->getConst(); + d_node->getConst(); indices = std::make_pair(ext.t.exponent(), ext.t.significand()); } else @@ -1346,21 +1368,26 @@ std::pair Op::getIndices() const std::string Op::toString() const { CVC4_API_CHECK_NOT_NULL; - if (d_expr->isNull()) + if (d_node->isNull()) { return kindToString(d_kind); } else { - CVC4_API_CHECK(!d_expr->isNull()) + CVC4_API_CHECK(!d_node->isNull()) << "Expecting a non-null internal expression"; - return d_expr->toString(); + return d_node->toString(); } } // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! -CVC4::Expr Op::getExpr(void) const { return *d_expr; } +CVC4::Expr Op::getExpr(void) const +{ + if (d_node->isNull()) return Expr(); + NodeManagerScope scope(d_solver->getNodeManager()); + return d_node->toExpr(); +} std::ostream& operator<<(std::ostream& out, const Op& t) { @@ -1372,7 +1399,7 @@ size_t OpHashFunction::operator()(const Op& t) const { if (t.isIndexedHelper()) { - return ExprHashFunction()(*t.d_expr); + return ExprHashFunction()(t.d_node->toExpr()); } else { @@ -1384,19 +1411,33 @@ size_t OpHashFunction::operator()(const Op& t) const /* Term */ /* -------------------------------------------------------------------------- */ -Term::Term() : d_solver(nullptr), d_expr(new CVC4::Expr()) {} +Term::Term() : d_solver(nullptr), d_node(new CVC4::Node()) {} Term::Term(const Solver* slv, const CVC4::Expr& e) - : d_solver(slv), d_expr(new CVC4::Expr(e)) + : d_solver(slv), d_node(new CVC4::Node(e)) +{ +} + +Term::Term(const Solver* slv, const CVC4::Node& n) + : d_solver(slv), d_node(new CVC4::Node(n)) { } -Term::~Term() {} +Term::~Term() +{ + if (d_solver != nullptr) + { + // Ensure that the correct node manager is in scope when the node is + // destroyed. + NodeManagerScope scope(d_solver->getNodeManager()); + d_node.reset(); + } +} bool Term::isNullHelper() const { /* Split out to avoid nested API calls (problematic with API tracing). */ - return d_expr->isNull(); + return d_node->isNull(); } Kind Term::getKindHelper() const @@ -1407,7 +1448,7 @@ Kind Term::getKindHelper() const // we check here. if (getNumChildren() > 0 && (*this)[0].getSort().isSequence()) { - switch (d_expr->getKind()) + switch (d_node->getKind()) { case CVC4::Kind::STRING_CONCAT: return SEQ_CONCAT; case CVC4::Kind::STRING_LENGTH: return SEQ_LENGTH; @@ -1427,55 +1468,55 @@ Kind Term::getKindHelper() const } } - return intToExtKind(d_expr->getKind()); + return intToExtKind(d_node->getKind()); } -bool Term::operator==(const Term& t) const { return *d_expr == *t.d_expr; } +bool Term::operator==(const Term& t) const { return *d_node == *t.d_node; } -bool Term::operator!=(const Term& t) const { return *d_expr != *t.d_expr; } +bool Term::operator!=(const Term& t) const { return *d_node != *t.d_node; } -bool Term::operator<(const Term& t) const { return *d_expr < *t.d_expr; } +bool Term::operator<(const Term& t) const { return *d_node < *t.d_node; } -bool Term::operator>(const Term& t) const { return *d_expr > *t.d_expr; } +bool Term::operator>(const Term& t) const { return *d_node > *t.d_node; } -bool Term::operator<=(const Term& t) const { return *d_expr <= *t.d_expr; } +bool Term::operator<=(const Term& t) const { return *d_node <= *t.d_node; } -bool Term::operator>=(const Term& t) const { return *d_expr >= *t.d_expr; } +bool Term::operator>=(const Term& t) const { return *d_node >= *t.d_node; } size_t Term::getNumChildren() const { CVC4_API_CHECK_NOT_NULL; // special case for apply kinds - if (isApplyKind(d_expr->getKind())) + if (isApplyKind(d_node->getKind())) { - return d_expr->getNumChildren() + 1; + return d_node->getNumChildren() + 1; } - return d_expr->getNumChildren(); + return d_node->getNumChildren(); } Term Term::operator[](size_t index) const { CVC4_API_CHECK_NOT_NULL; // special cases for apply kinds - if (isApplyKind(d_expr->getKind())) + if (isApplyKind(d_node->getKind())) { - CVC4_API_CHECK(d_expr->hasOperator()) + CVC4_API_CHECK(d_node->hasOperator()) << "Expected apply kind to have operator when accessing child of Term"; if (index == 0) { // return the operator - return Term(d_solver, d_expr->getOperator()); + return Term(d_solver, d_node->getOperator().toExpr()); } // otherwise we are looking up child at (index-1) index--; } - return Term(d_solver, (*d_expr)[index]); + return Term(d_solver, (*d_node)[index].toExpr()); } uint64_t Term::getId() const { CVC4_API_CHECK_NOT_NULL; - return d_expr->getId(); + return d_node->getId(); } Kind Term::getKind() const @@ -1487,7 +1528,8 @@ Kind Term::getKind() const Sort Term::getSort() const { CVC4_API_CHECK_NOT_NULL; - return Sort(d_solver, d_expr->getType()); + NodeManagerScope scope(d_solver->getNodeManager()); + return Sort(d_solver, d_node->getType().toType()); } Term Term::substitute(Term e, Term replacement) const @@ -1499,7 +1541,8 @@ Term Term::substitute(Term e, Term replacement) const << "Expected non-null term as replacement in substitute"; CVC4_API_CHECK(e.getSort().isComparableTo(replacement.getSort())) << "Expecting terms of comparable sort in substitute"; - return Term(d_solver, d_expr->substitute(e.getExpr(), replacement.getExpr())); + return Term(d_solver, + d_node->substitute(TNode(*e.d_node), TNode(*replacement.d_node))); } Term Term::substitute(const std::vector es, @@ -1517,21 +1560,26 @@ Term Term::substitute(const std::vector es, CVC4_API_CHECK(es[i].getSort().isComparableTo(replacements[i].getSort())) << "Expecting terms of comparable sort in substitute"; } + + std::vector nodes = termVectorToNodes(es); + std::vector nodeReplacements = termVectorToNodes(replacements); return Term(d_solver, - d_expr->substitute(termVectorToExprs(es), - termVectorToExprs(replacements))); + d_node->substitute(nodes.begin(), + nodes.end(), + nodeReplacements.begin(), + nodeReplacements.end())); } bool Term::hasOp() const { CVC4_API_CHECK_NOT_NULL; - return d_expr->hasOperator(); + return d_node->hasOperator(); } Op Term::getOp() const { CVC4_API_CHECK_NOT_NULL; - CVC4_API_CHECK(d_expr->hasOperator()) + CVC4_API_CHECK(d_node->hasOperator()) << "Expecting Term to have an Op when calling getOp()"; // special cases for parameterized operators that are not indexed operators @@ -1539,16 +1587,16 @@ Op Term::getOp() const // indexed operators are stored in Ops // whereas functions and datatype operators are terms, and the Op // is one of the APPLY_* kinds - if (isApplyKind(d_expr->getKind())) + if (isApplyKind(d_node->getKind())) { - return Op(d_solver, intToExtKind(d_expr->getKind())); + return Op(d_solver, intToExtKind(d_node->getKind())); } - else if (d_expr->isParameterized()) + else if (d_node->getMetaKind() == kind::metakind::PARAMETERIZED) { // it's an indexed operator // so we should return the indexed op - CVC4::Expr op = d_expr->getOperator(); - return Op(d_solver, intToExtKind(d_expr->getKind()), op); + CVC4::Node op = d_node->getOperator(); + return Op(d_solver, intToExtKind(d_node->getKind()), op); } // Notice this is the only case where getKindHelper is used, since the // cases above do have special cases for intToExtKind. @@ -1560,7 +1608,7 @@ bool Term::isNull() const { return isNullHelper(); } bool Term::isConst() const { CVC4_API_CHECK_NOT_NULL; - return d_expr->isConst(); + return d_node->isConst(); } Term Term::getConstArrayBase() const @@ -1568,22 +1616,22 @@ Term Term::getConstArrayBase() const CVC4::ExprManagerScope exmgrs(*(d_solver->getExprManager())); CVC4_API_CHECK_NOT_NULL; // CONST_ARRAY kind maps to STORE_ALL internal kind - CVC4_API_CHECK(d_expr->getKind() == CVC4::Kind::STORE_ALL) + CVC4_API_CHECK(d_node->getKind() == CVC4::Kind::STORE_ALL) << "Expecting a CONST_ARRAY Term when calling getConstArrayBase()"; - return Term(d_solver, d_expr->getConst().getValue().toExpr()); + return Term(d_solver, d_node->getConst().getValue()); } std::vector Term::getConstSequenceElements() const { CVC4_API_CHECK_NOT_NULL; - CVC4_API_CHECK(d_expr->getKind() == CVC4::Kind::CONST_SEQUENCE) + CVC4_API_CHECK(d_node->getKind() == CVC4::Kind::CONST_SEQUENCE) << "Expecting a CONST_SEQUENCE Term when calling " "getConstSequenceElements()"; - const std::vector& elems = d_expr->getConst().getVec(); + const std::vector& elems = d_node->getConst().getVec(); std::vector terms; for (const Node& t : elems) { - terms.push_back(Term(d_solver, t.toExpr())); + terms.push_back(Term(d_solver, t)); } return terms; } @@ -1593,11 +1641,11 @@ Term Term::notTerm() const CVC4_API_CHECK_NOT_NULL; try { - Expr res = d_expr->notExpr(); + Node res = d_node->notNode(); (void)res.getType(true); /* kick off type checking */ return Term(d_solver, res); } - catch (const CVC4::TypeCheckingException& e) + catch (const CVC4::TypeCheckingExceptionPrivate& e) { throw CVC4ApiException(e.getMessage()); } @@ -1609,11 +1657,11 @@ Term Term::andTerm(const Term& t) const CVC4_API_ARG_CHECK_NOT_NULL(t); try { - Expr res = d_expr->andExpr(*t.d_expr); + Node res = d_node->andNode(*t.d_node); (void)res.getType(true); /* kick off type checking */ return Term(d_solver, res); } - catch (const CVC4::TypeCheckingException& e) + catch (const CVC4::TypeCheckingExceptionPrivate& e) { throw CVC4ApiException(e.getMessage()); } @@ -1625,11 +1673,11 @@ Term Term::orTerm(const Term& t) const CVC4_API_ARG_CHECK_NOT_NULL(t); try { - Expr res = d_expr->orExpr(*t.d_expr); + Node res = d_node->orNode(*t.d_node); (void)res.getType(true); /* kick off type checking */ return Term(d_solver, res); } - catch (const CVC4::TypeCheckingException& e) + catch (const CVC4::TypeCheckingExceptionPrivate& e) { throw CVC4ApiException(e.getMessage()); } @@ -1641,11 +1689,11 @@ Term Term::xorTerm(const Term& t) const CVC4_API_ARG_CHECK_NOT_NULL(t); try { - Expr res = d_expr->xorExpr(*t.d_expr); + Node res = d_node->xorNode(*t.d_node); (void)res.getType(true); /* kick off type checking */ return Term(d_solver, res); } - catch (const CVC4::TypeCheckingException& e) + catch (const CVC4::TypeCheckingExceptionPrivate& e) { throw CVC4ApiException(e.getMessage()); } @@ -1657,11 +1705,11 @@ Term Term::eqTerm(const Term& t) const CVC4_API_ARG_CHECK_NOT_NULL(t); try { - Expr res = d_expr->eqExpr(*t.d_expr); + Node res = d_node->eqNode(*t.d_node); (void)res.getType(true); /* kick off type checking */ return Term(d_solver, res); } - catch (const CVC4::TypeCheckingException& e) + catch (const CVC4::TypeCheckingExceptionPrivate& e) { throw CVC4ApiException(e.getMessage()); } @@ -1673,11 +1721,11 @@ Term Term::impTerm(const Term& t) const CVC4_API_ARG_CHECK_NOT_NULL(t); try { - Expr res = d_expr->impExpr(*t.d_expr); + Node res = d_node->impNode(*t.d_node); (void)res.getType(true); /* kick off type checking */ return Term(d_solver, res); } - catch (const CVC4::TypeCheckingException& e) + catch (const CVC4::TypeCheckingExceptionPrivate& e) { throw CVC4ApiException(e.getMessage()); } @@ -1690,37 +1738,37 @@ Term Term::iteTerm(const Term& then_t, const Term& else_t) const CVC4_API_ARG_CHECK_NOT_NULL(else_t); try { - Expr res = d_expr->iteExpr(*then_t.d_expr, *else_t.d_expr); + Node res = d_node->iteNode(*then_t.d_node, *else_t.d_node); (void)res.getType(true); /* kick off type checking */ return Term(d_solver, res); } - catch (const CVC4::TypeCheckingException& e) + catch (const CVC4::TypeCheckingExceptionPrivate& e) { throw CVC4ApiException(e.getMessage()); } } -std::string Term::toString() const { return d_expr->toString(); } +std::string Term::toString() const { return d_node->toString(); } Term::const_iterator::const_iterator() - : d_solver(nullptr), d_orig_expr(nullptr), d_pos(0) + : d_solver(nullptr), d_origNode(nullptr), d_pos(0) { } Term::const_iterator::const_iterator(const Solver* slv, - const std::shared_ptr& e, + const std::shared_ptr& n, uint32_t p) - : d_solver(slv), d_orig_expr(e), d_pos(p) + : d_solver(slv), d_origNode(n), d_pos(p) { } Term::const_iterator::const_iterator(const const_iterator& it) - : d_solver(nullptr), d_orig_expr(nullptr) + : d_solver(nullptr), d_origNode(nullptr) { - if (it.d_orig_expr != nullptr) + if (it.d_origNode != nullptr) { d_solver = it.d_solver; - d_orig_expr = it.d_orig_expr; + d_origNode = it.d_origNode; d_pos = it.d_pos; } } @@ -1728,18 +1776,18 @@ Term::const_iterator::const_iterator(const const_iterator& it) Term::const_iterator& Term::const_iterator::operator=(const const_iterator& it) { d_solver = it.d_solver; - d_orig_expr = it.d_orig_expr; + d_origNode = it.d_origNode; d_pos = it.d_pos; return *this; } bool Term::const_iterator::operator==(const const_iterator& it) const { - if (d_orig_expr == nullptr || it.d_orig_expr == nullptr) + if (d_origNode == nullptr || it.d_origNode == nullptr) { return false; } - return (d_solver == it.d_solver && *d_orig_expr == *it.d_orig_expr) + return (d_solver == it.d_solver && *d_origNode == *it.d_origNode) && (d_pos == it.d_pos); } @@ -1750,14 +1798,14 @@ bool Term::const_iterator::operator!=(const const_iterator& it) const Term::const_iterator& Term::const_iterator::operator++() { - Assert(d_orig_expr != nullptr); + Assert(d_origNode != nullptr); ++d_pos; return *this; } Term::const_iterator Term::const_iterator::operator++(int) { - Assert(d_orig_expr != nullptr); + Assert(d_origNode != nullptr); const_iterator it = *this; ++d_pos; return it; @@ -1765,14 +1813,14 @@ Term::const_iterator Term::const_iterator::operator++(int) Term Term::const_iterator::operator*() const { - Assert(d_orig_expr != nullptr); + Assert(d_origNode != nullptr); // this term has an extra child (mismatch between API and internal structure) // the extra child will be the first child - bool extra_child = isApplyKind(d_orig_expr->getKind()); + bool extra_child = isApplyKind(d_origNode->getKind()); if (!d_pos && extra_child) { - return Term(d_solver, d_orig_expr->getOperator()); + return Term(d_solver, d_origNode->getOperator()); } else { @@ -1783,35 +1831,47 @@ Term Term::const_iterator::operator*() const --idx; } Assert(idx >= 0); - return Term(d_solver, (*d_orig_expr)[idx]); + return Term(d_solver, (*d_origNode)[idx]); } } Term::const_iterator Term::begin() const { - return Term::const_iterator(d_solver, d_expr, 0); + return Term::const_iterator(d_solver, d_node, 0); } Term::const_iterator Term::end() const { - int endpos = d_expr->getNumChildren(); + int endpos = d_node->getNumChildren(); // special cases for APPLY_* // the API differs from the internal structure // the API takes a "higher-order" perspective and the applied // function or datatype constructor/selector/tester is a Term // which means it needs to be one of the children, even though // internally it is not - if (isApplyKind(d_expr->getKind())) + if (isApplyKind(d_node->getKind())) { // one more child if this is a UF application (count the UF as a child) ++endpos; } - return Term::const_iterator(d_solver, d_expr, endpos); + 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(); } // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! -CVC4::Expr Term::getExpr(void) const { return *d_expr; } +const CVC4::Node& Term::getNode(void) const { return *d_node; } std::ostream& operator<<(std::ostream& out, const Term& t) { @@ -1857,7 +1917,7 @@ std::ostream& operator<<( size_t TermHashFunction::operator()(const Term& t) const { - return ExprHashFunction()(*t.d_expr); + return ExprHashFunction()(t.d_node->toExpr()); } /* -------------------------------------------------------------------------- */ @@ -2413,7 +2473,7 @@ void Grammar::addRule(Term ntSymbol, Term rule) d_ntsToTerms.find(ntSymbol) != d_ntsToTerms.cend(), ntSymbol) << "ntSymbol to be one of the non-terminal symbols given in the " "predeclaration"; - CVC4_API_CHECK(ntSymbol.d_expr->getType() == rule.d_expr->getType()) + CVC4_API_CHECK(ntSymbol.d_node->getType() == rule.d_node->getType()) << "Expected ntSymbol and rule to have the same sort"; d_ntsToTerms[ntSymbol].push_back(rule); @@ -2434,7 +2494,7 @@ void Grammar::addRules(Term ntSymbol, std::vector rules) CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( !rules[i].isNull(), "parameter rule", rules[i], i) << "non-null term"; - CVC4_API_CHECK(ntSymbol.d_expr->getType() == rules[i].d_expr->getType()) + CVC4_API_CHECK(ntSymbol.d_node->getType() == rules[i].d_node->getType()) << "Expected ntSymbol and rule at index " << i << " to have the same sort"; } @@ -2509,13 +2569,13 @@ Sort Grammar::resolve() if (d_allowVars.find(ntSym) != d_allowVars.cend()) { - addSygusConstructorVariables(dtDecl, - Sort(d_solver, ntSym.d_expr->getType())); + addSygusConstructorVariables( + dtDecl, Sort(d_solver, ntSym.d_node->getType().toType())); } bool aci = d_allowConst.find(ntSym) != d_allowConst.end(); - Type btt = ntSym.d_expr->getType(); - dtDecl.d_dtype->setSygus(btt, *bvl.d_expr, aci, false); + Type btt = ntSym.d_node->getType().toType(); + dtDecl.d_dtype->setSygus(btt, bvl.d_node->toExpr(), aci, false); // We can be in a case where the only rule specified was (Variable T) // and there are no variables of type T, in which case this is a bogus @@ -2560,12 +2620,13 @@ void Grammar::addSygusConstructorTerm( d_solver->getExprManager()->mkExpr( CVC4::kind::BOUND_VAR_LIST, termVectorToExprs(args))); // its operator is a lambda - op = Term(d_solver, - d_solver->getExprManager()->mkExpr(CVC4::kind::LAMBDA, - {*lbvl.d_expr, *op.d_expr})); + op = Term( + d_solver, + d_solver->getExprManager()->mkExpr( + CVC4::kind::LAMBDA, {lbvl.d_node->toExpr(), op.d_node->toExpr()})); } dt.d_dtype->addSygusConstructor( - *op.d_expr, ssCName.str(), sortVectorToTypes(cargs)); + op.d_node->toExpr(), ssCName.str(), sortVectorToTypes(cargs)); } Term Grammar::purifySygusGTerm( @@ -2580,38 +2641,40 @@ Term Grammar::purifySygusGTerm( { Term ret = Term(d_solver, - d_solver->getExprManager()->mkBoundVar(term.d_expr->getType())); + d_solver->getNodeManager()->mkBoundVar(term.d_node->getType())); args.push_back(ret); cargs.push_back(itn->second); return ret; } std::vector pchildren; bool childChanged = false; - for (unsigned i = 0, nchild = term.d_expr->getNumChildren(); i < nchild; i++) + for (unsigned i = 0, nchild = term.d_node->getNumChildren(); i < nchild; i++) { Term ptermc = purifySygusGTerm( - Term(d_solver, (*term.d_expr)[i]), args, cargs, ntsToUnres); + Term(d_solver, (*term.d_node)[i]), args, cargs, ntsToUnres); pchildren.push_back(ptermc); - childChanged = childChanged || *ptermc.d_expr != (*term.d_expr)[i]; + childChanged = + childChanged || ptermc.d_node->toExpr() != (term.d_node->toExpr())[i]; } if (!childChanged) { return term; } - Expr nret; + Node nret; - if (term.d_expr->isParameterized()) + if (term.d_node->getMetaKind() == kind::metakind::PARAMETERIZED) { // it's an indexed operator so we should provide the op - nret = d_solver->getExprManager()->mkExpr(term.d_expr->getKind(), - term.d_expr->getOperator(), - termVectorToExprs(pchildren)); + NodeBuilder<> nb(term.d_node->getKind()); + nb << term.d_node->getOperator(); + nb.append(termVectorToNodes(pchildren)); + nret = nb.constructNode(); } else { - nret = d_solver->getExprManager()->mkExpr(term.d_expr->getKind(), - termVectorToExprs(pchildren)); + nret = d_solver->getNodeManager()->mkNode(term.d_node->getKind(), + termVectorToNodes(pchildren)); } return Term(d_solver, nret); @@ -2624,13 +2687,13 @@ void Grammar::addSygusConstructorVariables(DatatypeDecl& dt, Sort sort) const for (unsigned i = 0, size = d_sygusVars.size(); i < size; i++) { Term v = d_sygusVars[i]; - if (v.d_expr->getType() == *sort.d_type) + if (v.d_node->getType().toType() == *sort.d_type) { std::stringstream ss; ss << v; std::vector cargs; dt.d_dtype->addSygusConstructor( - *v.d_expr, ss.str(), sortVectorToTypes(cargs)); + v.d_node->toExpr(), ss.str(), sortVectorToTypes(cargs)); } } } @@ -2693,7 +2756,8 @@ Solver::~Solver() {} template Term Solver::mkValHelper(T t) const { - Expr res = d_exprMgr->mkConst(t); + NodeManagerScope scope(getNodeManager()); + Node res = getNodeManager()->mkConst(t); (void)res.getType(true); /* kick off type checking */ return Term(this, res); } @@ -2798,6 +2862,7 @@ Term Solver::mkTermFromKind(Kind kind) const Term Solver::mkTermHelper(Kind kind, const std::vector& children) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; for (size_t i = 0, size = children.size(); i < size; ++i) { @@ -2924,7 +2989,7 @@ std::vector Solver::termVectorToExprs( for (const Term& t : terms) { CVC4_API_SOLVER_CHECK_TERM(t); - res.push_back(*t.d_expr); + res.push_back(t.d_node->toExpr()); } return res; } @@ -3519,7 +3584,7 @@ Term Solver::mkConstArray(Sort sort, Term val) const CVC4_API_CHECK(sort.getArrayElementSort().isComparableTo(val.getSort())) << "Value does not match element sort."; Term res = mkValHelper(CVC4::ArrayStoreAll( - TypeNode::fromType(*sort.d_type), Node::fromExpr(*val.d_expr))); + TypeNode::fromType(*sort.d_type), Node::fromExpr(val.d_node->toExpr()))); return res; CVC4_API_SOLVER_TRY_CATCH_END; } @@ -3611,7 +3676,7 @@ Term Solver::mkAbstractValue(const std::string& index) const CVC4::Integer idx(index, 10); CVC4_API_ARG_CHECK_EXPECTED(idx > 0, index) << "a string representing an integer > 0"; - return Term(this, d_exprMgr->mkConst(CVC4::AbstractValue(idx))); + return Term(this, getNodeManager()->mkConst(CVC4::AbstractValue(idx))); // do not call getType(), for abstract values, type can not be computed // until it is substituted away CVC4_API_SOLVER_TRY_CATCH_END; @@ -3622,7 +3687,8 @@ Term Solver::mkAbstractValue(uint64_t index) const CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(index > 0, index) << "an integer > 0"; - return Term(this, d_exprMgr->mkConst(CVC4::AbstractValue(Integer(index)))); + return Term(this, + getNodeManager()->mkConst(CVC4::AbstractValue(Integer(index)))); // do not call getType(), for abstract values, type can not be computed // until it is substituted away CVC4_API_SOLVER_TRY_CATCH_END; @@ -3641,11 +3707,11 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const CVC4_API_ARG_CHECK_EXPECTED(!val.isNull(), val) << "non-null term"; CVC4_API_SOLVER_CHECK_TERM(val); CVC4_API_ARG_CHECK_EXPECTED( - val.getSort().isBitVector() && val.d_expr->isConst(), val) + val.getSort().isBitVector() && val.d_node->isConst(), val) << "bit-vector constant"; return mkValHelper( - CVC4::FloatingPoint(exp, sig, val.d_expr->getConst())); + CVC4::FloatingPoint(exp, sig, val.d_node->getConst())); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -3655,6 +3721,7 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const Term Solver::mkConst(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); @@ -3727,12 +3794,13 @@ Term Solver::mkTerm(Kind kind) const Term Solver::mkTerm(Kind kind, Term child) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term"; CVC4_API_SOLVER_CHECK_TERM(child); checkMkTerm(kind, 1); - Expr res = d_exprMgr->mkExpr(extToIntKind(kind), *child.d_expr); + Node res = getNodeManager()->mkNode(extToIntKind(kind), *child.d_node); (void)res.getType(true); /* kick off type checking */ return Term(this, res); @@ -3741,6 +3809,7 @@ Term Solver::mkTerm(Kind kind, Term child) const Term Solver::mkTerm(Kind kind, Term child1, Term child2) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term"; CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term"; @@ -3748,8 +3817,8 @@ Term Solver::mkTerm(Kind kind, Term child1, Term child2) const CVC4_API_SOLVER_CHECK_TERM(child2); checkMkTerm(kind, 2); - Expr res = - d_exprMgr->mkExpr(extToIntKind(kind), *child1.d_expr, *child2.d_expr); + Node res = getNodeManager()->mkNode( + extToIntKind(kind), *child1.d_node, *child2.d_node); (void)res.getType(true); /* kick off type checking */ return Term(this, res); @@ -3769,21 +3838,23 @@ Term Solver::mkTerm(Kind kind, const std::vector& children) const Term Solver::mkTerm(Op op) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_SOLVER_CHECK_OP(op); + checkMkTerm(op.d_kind, 0); Term res; if (op.isIndexedHelper()) { const CVC4::Kind int_kind = extToIntKind(op.d_kind); - res = Term(this, d_exprMgr->mkExpr(int_kind, *op.d_expr)); + res = Term(this, getNodeManager()->mkNode(int_kind, *op.d_node)); } else { res = mkTermFromKind(op.d_kind); } - (void)res.d_expr->getType(true); /* kick off type checking */ + (void)res.d_node->getType(true); /* kick off type checking */ return res; CVC4_API_SOLVER_TRY_CATCH_END; @@ -3791,20 +3862,22 @@ Term Solver::mkTerm(Op op) const Term Solver::mkTerm(Op op, Term child) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_SOLVER_CHECK_OP(op); CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term"; CVC4_API_SOLVER_CHECK_TERM(child); + checkMkTerm(op.d_kind, 1); const CVC4::Kind int_kind = extToIntKind(op.d_kind); - Expr res; + Node res; if (op.isIndexedHelper()) { - res = d_exprMgr->mkExpr(int_kind, *op.d_expr, *child.d_expr); + res = getNodeManager()->mkNode(int_kind, *op.d_node, *child.d_node); } else { - res = d_exprMgr->mkExpr(int_kind, *child.d_expr); + res = getNodeManager()->mkNode(int_kind, *child.d_node); } (void)res.getType(true); /* kick off type checking */ @@ -3815,23 +3888,25 @@ Term Solver::mkTerm(Op op, Term child) const Term Solver::mkTerm(Op op, Term child1, Term child2) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_SOLVER_CHECK_OP(op); CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term"; CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term"; CVC4_API_SOLVER_CHECK_TERM(child1); CVC4_API_SOLVER_CHECK_TERM(child2); + checkMkTerm(op.d_kind, 2); const CVC4::Kind int_kind = extToIntKind(op.d_kind); - Expr res; + Node res; if (op.isIndexedHelper()) { - res = - d_exprMgr->mkExpr(int_kind, *op.d_expr, *child1.d_expr, *child2.d_expr); + res = getNodeManager()->mkNode( + int_kind, *op.d_node, *child1.d_node, *child2.d_node); } else { - res = d_exprMgr->mkExpr(int_kind, *child1.d_expr, *child2.d_expr); + res = getNodeManager()->mkNode(int_kind, *child1.d_node, *child2.d_node); } (void)res.getType(true); /* kick off type checking */ @@ -3841,6 +3916,7 @@ Term Solver::mkTerm(Op op, Term child1, Term child2) const Term Solver::mkTerm(Op op, Term child1, Term child2, Term child3) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_SOLVER_CHECK_OP(op); CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term"; @@ -3849,18 +3925,19 @@ Term Solver::mkTerm(Op op, Term child1, Term child2, Term child3) const CVC4_API_SOLVER_CHECK_TERM(child1); CVC4_API_SOLVER_CHECK_TERM(child2); CVC4_API_SOLVER_CHECK_TERM(child3); + checkMkTerm(op.d_kind, 3); const CVC4::Kind int_kind = extToIntKind(op.d_kind); - Expr res; + Node res; if (op.isIndexedHelper()) { - res = d_exprMgr->mkExpr( - int_kind, *op.d_expr, *child1.d_expr, *child2.d_expr, *child3.d_expr); + res = getNodeManager()->mkNode( + int_kind, *op.d_node, *child1.d_node, *child2.d_node, *child3.d_node); } else { - res = d_exprMgr->mkExpr( - int_kind, *child1.d_expr, *child2.d_expr, *child3.d_expr); + res = getNodeManager()->mkNode( + int_kind, *child1.d_node, *child2.d_node, *child3.d_node); } (void)res.getType(true); /* kick off type checking */ @@ -3871,8 +3948,10 @@ Term Solver::mkTerm(Op op, Term child1, Term child2, Term child3) const Term Solver::mkTerm(Op op, const std::vector& children) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_SOLVER_CHECK_OP(op); + checkMkTerm(op.d_kind, children.size()); for (size_t i = 0, size = children.size(); i < size; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( @@ -3884,15 +3963,18 @@ Term Solver::mkTerm(Op op, const std::vector& children) const } const CVC4::Kind int_kind = extToIntKind(op.d_kind); - std::vector echildren = termVectorToExprs(children); - Expr res; + std::vector echildren = termVectorToNodes(children); + Node res; if (op.isIndexedHelper()) { - res = d_exprMgr->mkExpr(int_kind, *op.d_expr, echildren); + NodeBuilder<> nb(int_kind); + nb << *op.d_node; + nb.append(echildren); + res = nb.constructNode(); } else { - res = d_exprMgr->mkExpr(int_kind, echildren); + res = getNodeManager()->mkNode(int_kind, echildren); } (void)res.getType(true); /* kick off type checking */ @@ -3907,7 +3989,7 @@ Term Solver::mkTuple(const std::vector& sorts, CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_CHECK(sorts.size() == terms.size()) << "Expected the same number of sorts and elements"; - std::vector args; + std::vector args; for (size_t i = 0, size = sorts.size(); i < size; i++) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( @@ -3916,14 +3998,15 @@ Term Solver::mkTuple(const std::vector& sorts, CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( this == sorts[i].d_solver, "child sort", sorts[i], i) << "child sort associated to this solver object"; - args.push_back(*(ensureTermSort(terms[i], sorts[i])).d_expr); + args.push_back(*(ensureTermSort(terms[i], sorts[i])).d_node); } Sort s = mkTupleSort(sorts); Datatype dt = s.getDatatype(); - Expr res = d_exprMgr->mkExpr(extToIntKind(APPLY_CONSTRUCTOR), - *dt[0].getConstructorTerm().d_expr, - args); + NodeBuilder<> nb(extToIntKind(APPLY_CONSTRUCTOR)); + nb << *dt[0].getConstructorTerm().d_node; + nb.append(args); + Node res = nb.constructNode(); (void)res.getType(true); /* kick off type checking */ return Term(this, res); @@ -3951,10 +4034,9 @@ Op Solver::mkOp(Kind kind, const std::string& arg) const Op res; if (kind == RECORD_UPDATE) { - res = Op( - this, - kind, - *mkValHelper(CVC4::RecordUpdate(arg)).d_expr.get()); + res = Op(this, + kind, + *mkValHelper(CVC4::RecordUpdate(arg)).d_node); } else { @@ -3966,7 +4048,7 @@ Op Solver::mkOp(Kind kind, const std::string& arg) const res = Op(this, kind, *mkValHelper(CVC4::Divisible(CVC4::Integer(arg))) - .d_expr.get()); + .d_node); } return res; @@ -3982,81 +4064,78 @@ Op Solver::mkOp(Kind kind, uint32_t arg) const switch (kind) { case DIVISIBLE: - res = - Op(this, - kind, - *mkValHelper(CVC4::Divisible(arg)).d_expr.get()); + res = Op(this, + kind, + *mkValHelper(CVC4::Divisible(arg)).d_node); break; case BITVECTOR_REPEAT: res = Op(this, kind, - *mkValHelper(CVC4::BitVectorRepeat(arg)) - .d_expr.get()); + mkValHelper(CVC4::BitVectorRepeat(arg)) + .d_node->toExpr()); break; case BITVECTOR_ZERO_EXTEND: res = Op(this, kind, *mkValHelper( CVC4::BitVectorZeroExtend(arg)) - .d_expr.get()); + .d_node); break; case BITVECTOR_SIGN_EXTEND: res = Op(this, kind, *mkValHelper( CVC4::BitVectorSignExtend(arg)) - .d_expr.get()); + .d_node); break; case BITVECTOR_ROTATE_LEFT: res = Op(this, kind, *mkValHelper( CVC4::BitVectorRotateLeft(arg)) - .d_expr.get()); + .d_node); break; case BITVECTOR_ROTATE_RIGHT: res = Op(this, kind, *mkValHelper( CVC4::BitVectorRotateRight(arg)) - .d_expr.get()); + .d_node); break; case INT_TO_BITVECTOR: - res = Op(this, - kind, - *mkValHelper(CVC4::IntToBitVector(arg)) - .d_expr.get()); + res = Op( + this, + kind, + *mkValHelper(CVC4::IntToBitVector(arg)).d_node); break; case IAND: - res = Op(this, - kind, - *mkValHelper(CVC4::IntAnd(arg)).d_expr.get()); + res = + Op(this, kind, *mkValHelper(CVC4::IntAnd(arg)).d_node); break; case FLOATINGPOINT_TO_UBV: res = Op( this, kind, *mkValHelper(CVC4::FloatingPointToUBV(arg)) - .d_expr.get()); + .d_node); break; case FLOATINGPOINT_TO_SBV: res = Op( this, kind, *mkValHelper(CVC4::FloatingPointToSBV(arg)) - .d_expr.get()); + .d_node); break; case TUPLE_UPDATE: - res = Op( - this, - kind, - *mkValHelper(CVC4::TupleUpdate(arg)).d_expr.get()); - break; - case REGEXP_REPEAT: res = Op(this, kind, - *mkValHelper(CVC4::RegExpRepeat(arg)) - .d_expr.get()); + *mkValHelper(CVC4::TupleUpdate(arg)).d_node); + break; + case REGEXP_REPEAT: + res = + Op(this, + kind, + *mkValHelper(CVC4::RegExpRepeat(arg)).d_node); break; default: CVC4_API_KIND_CHECK_EXPECTED(false, kind) @@ -4081,55 +4160,55 @@ Op Solver::mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const kind, *mkValHelper( CVC4::BitVectorExtract(arg1, arg2)) - .d_expr.get()); + .d_node); break; case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: res = Op(this, kind, *mkValHelper( CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2)) - .d_expr.get()); + .d_node); break; case FLOATINGPOINT_TO_FP_FLOATINGPOINT: res = Op(this, kind, *mkValHelper( CVC4::FloatingPointToFPFloatingPoint(arg1, arg2)) - .d_expr.get()); + .d_node); break; case FLOATINGPOINT_TO_FP_REAL: res = Op(this, kind, *mkValHelper( CVC4::FloatingPointToFPReal(arg1, arg2)) - .d_expr.get()); + .d_node); break; case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: res = Op(this, kind, *mkValHelper( CVC4::FloatingPointToFPSignedBitVector(arg1, arg2)) - .d_expr.get()); + .d_node); break; case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: res = Op(this, kind, *mkValHelper( CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2)) - .d_expr.get()); + .d_node); break; case FLOATINGPOINT_TO_FP_GENERIC: res = Op(this, kind, *mkValHelper( CVC4::FloatingPointToFPGeneric(arg1, arg2)) - .d_expr.get()); + .d_node); break; case REGEXP_LOOP: - res = Op(this, - kind, - *mkValHelper(CVC4::RegExpLoop(arg1, arg2)) - .d_expr.get()); + res = Op( + this, + kind, + *mkValHelper(CVC4::RegExpLoop(arg1, arg2)).d_node); break; default: CVC4_API_KIND_CHECK_EXPECTED(false, kind) @@ -4147,10 +4226,11 @@ Op Solver::mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const Term Solver::simplify(const Term& term) { CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); CVC4_API_ARG_CHECK_NOT_NULL(term); CVC4_API_SOLVER_CHECK_TERM(term); - return Term(this, d_smtEngine->simplify(*term.d_expr)); + return Term(this, d_smtEngine->simplify(term.d_node->toExpr())); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4166,7 +4246,7 @@ Result Solver::checkEntailed(Term term) const CVC4_API_ARG_CHECK_NOT_NULL(term); CVC4_API_SOLVER_CHECK_TERM(term); - CVC4::Result r = d_smtEngine->checkEntailed(*term.d_expr); + CVC4::Result r = d_smtEngine->checkEntailed(term.d_node->toExpr()); return Result(r); CVC4_API_SOLVER_TRY_CATCH_END; @@ -4204,7 +4284,7 @@ void Solver::assertFormula(Term term) const CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_SOLVER_CHECK_TERM(term); CVC4_API_ARG_CHECK_NOT_NULL(term); - d_smtEngine->assertFormula(Node::fromExpr(*term.d_expr)); + d_smtEngine->assertFormula(*term.d_node); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4236,7 +4316,7 @@ Result Solver::checkSatAssuming(Term assumption) const << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC4_API_SOLVER_CHECK_TERM(assumption); - CVC4::Result r = d_smtEngine->checkSat(*assumption.d_expr); + CVC4::Result r = d_smtEngine->checkSat(assumption.d_node->toExpr()); return Result(r); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4348,12 +4428,12 @@ Term Solver::defineFun(const std::string& symbol, this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i) << "bound variable associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - bound_vars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE, + bound_vars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, "bound variable", bound_vars[i], i) << "a bound variable"; - CVC4::Type t = bound_vars[i].d_expr->getType(); + CVC4::Type t = bound_vars[i].d_node->getType().toType(); CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( t.isFirstClass(), "sort of parameter", bound_vars[i], i) << "first-class sort of parameter of defined function"; @@ -4370,7 +4450,7 @@ Term Solver::defineFun(const std::string& symbol, } Expr fun = d_exprMgr->mkVar(symbol, type); std::vector ebound_vars = termVectorToExprs(bound_vars); - d_smtEngine->defineFunction(fun, ebound_vars, *term.d_expr, global); + d_smtEngine->defineFunction(fun, ebound_vars, term.d_node->toExpr(), global); return Term(this, fun); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4394,7 +4474,7 @@ Term Solver::defineFun(Term fun, this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i) << "bound variable associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - bound_vars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE, + bound_vars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, "bound variable", bound_vars[i], i) @@ -4420,7 +4500,8 @@ Term Solver::defineFun(Term fun, CVC4_API_SOLVER_CHECK_TERM(term); std::vector ebound_vars = termVectorToExprs(bound_vars); - d_smtEngine->defineFunction(*fun.d_expr, ebound_vars, *term.d_expr, global); + d_smtEngine->defineFunction( + fun.d_node->toExpr(), ebound_vars, term.d_node->toExpr(), global); return fun; CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4434,6 +4515,7 @@ Term Solver::defineFunRec(const std::string& symbol, Term term, bool global) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified()) @@ -4453,12 +4535,12 @@ Term Solver::defineFunRec(const std::string& symbol, this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i) << "bound variable associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - bound_vars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE, + bound_vars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, "bound variable", bound_vars[i], i) << "a bound variable"; - CVC4::Type t = bound_vars[i].d_expr->getType(); + CVC4::Type t = bound_vars[i].d_node->getType().toType(); CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( t.isFirstClass(), "sort of parameter", bound_vars[i], i) << "first-class sort of parameter of defined function"; @@ -4476,7 +4558,8 @@ Term Solver::defineFunRec(const std::string& symbol, } Expr fun = d_exprMgr->mkVar(symbol, type); std::vector ebound_vars = termVectorToExprs(bound_vars); - d_smtEngine->defineFunctionRec(fun, ebound_vars, *term.d_expr, global); + d_smtEngine->defineFunctionRec( + fun, ebound_vars, term.d_node->toExpr(), global); return Term(this, fun); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4486,6 +4569,7 @@ Term Solver::defineFunRec(Term fun, Term term, bool global) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified()) @@ -4507,7 +4591,7 @@ Term Solver::defineFunRec(Term fun, this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i) << "bound variable associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - bound_vars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE, + bound_vars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, "bound variable", bound_vars[i], i) @@ -4533,7 +4617,7 @@ Term Solver::defineFunRec(Term fun, CVC4_API_SOLVER_CHECK_TERM(term); std::vector ebound_vars = termVectorToExprs(bound_vars); d_smtEngine->defineFunctionRec( - *fun.d_expr, ebound_vars, *term.d_expr, global); + fun.d_node->toExpr(), ebound_vars, term.d_node->toExpr(), global); return fun; CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4546,6 +4630,7 @@ void Solver::defineFunsRec(const std::vector& funs, const std::vector& terms, bool global) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified()) @@ -4583,7 +4668,7 @@ void Solver::defineFunsRec(const std::vector& funs, this == bvars[k].d_solver, "bound variable", bvars[k], k) << "bound variable associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - bvars[k].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE, + bvars[k].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, "bound variable", bvars[k], k) @@ -4753,7 +4838,7 @@ Term Solver::getValue(Term term) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_SOLVER_CHECK_TERM(term); - return Term(this, d_smtEngine->getValue(*term.d_expr)); + return Term(this, d_smtEngine->getValue(term.d_node->toExpr())); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4777,7 +4862,7 @@ std::vector Solver::getValue(const std::vector& terms) const this == terms[i].d_solver, "term", terms[i], i) << "term associated to this solver object"; /* Can not use emplace_back here since constructor is private. */ - res.push_back(Term(this, d_smtEngine->getValue(*terms[i].d_expr))); + res.push_back(Term(this, d_smtEngine->getValue(terms[i].d_node->toExpr()))); } return res; CVC4_API_SOLVER_TRY_CATCH_END; @@ -4857,7 +4942,7 @@ bool Solver::getInterpolant(Term conj, Term& output) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; Expr result; - bool success = d_smtEngine->getInterpol(*conj.d_expr, result); + bool success = d_smtEngine->getInterpol(conj.d_node->toExpr(), result); if (success) { output = Term(output.d_solver, result); } @@ -4869,7 +4954,7 @@ bool Solver::getInterpolant(Term conj, const Type& gtype, Term& output) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; Expr result; - bool success = d_smtEngine->getInterpol(*conj.d_expr, gtype, result); + bool success = d_smtEngine->getInterpol(conj.d_node->toExpr(), gtype, result); if (success) { output = Term(output.d_solver, result); @@ -4997,7 +5082,7 @@ Term Solver::ensureTermSort(const Term& term, const Sort& sort) const // in the theory. res = Term(this, d_exprMgr->mkExpr(extToIntKind(DIVISION), - *res.d_expr, + res.d_node->toExpr(), d_exprMgr->mkConst(CVC4::Rational(1)))); } Assert(res.getSort() == sort); @@ -5033,7 +5118,7 @@ Grammar Solver::mkSygusGrammar(const std::vector& boundVars, this == boundVars[i].d_solver, "bound variable", boundVars[i], i) << "bound variable associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - boundVars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE, + boundVars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, "bound variable", boundVars[i], i) @@ -5049,7 +5134,7 @@ Grammar Solver::mkSygusGrammar(const std::vector& boundVars, this == ntSymbols[i].d_solver, "term", ntSymbols[i], i) << "term associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - ntSymbols[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE, + ntSymbols[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, "bound variable", ntSymbols[i], i) @@ -5112,7 +5197,7 @@ Term Solver::synthFunHelper(const std::string& symbol, this == boundVars[i].d_solver, "bound variable", boundVars[i], i) << "bound variable associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - boundVars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE, + boundVars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, "bound variable", boundVars[i], i) @@ -5120,13 +5205,13 @@ Term Solver::synthFunHelper(const std::string& symbol, CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( !boundVars[i].isNull(), "parameter term", boundVars[i], i) << "non-null term"; - varTypes.push_back(boundVars[i].d_expr->getType()); + varTypes.push_back(boundVars[i].d_node->getType().toType()); } CVC4_API_SOLVER_CHECK_SORT(sort); if (g != nullptr) { - CVC4_API_CHECK(g->d_ntSyms[0].d_expr->getType() == *sort.d_type) + CVC4_API_CHECK(g->d_ntSyms[0].d_node->getType().toType() == *sort.d_type) << "Invalid Start symbol for Grammar g, Expected Start's sort to be " << *sort.d_type; } @@ -5152,13 +5237,14 @@ Term Solver::synthFunHelper(const std::string& symbol, void Solver::addSygusConstraint(Term term) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; + NodeManagerScope scope(getNodeManager()); CVC4_API_ARG_CHECK_NOT_NULL(term); CVC4_API_SOLVER_CHECK_TERM(term); CVC4_API_ARG_CHECK_EXPECTED( - term.d_expr->getType() == d_exprMgr->booleanType(), term) + term.d_node->getType() == getNodeManager()->booleanType(), term) << "boolean term"; - d_smtEngine->assertSygusConstraint(*term.d_expr); + d_smtEngine->assertSygusConstraint(*term.d_node); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -5177,18 +5263,18 @@ void Solver::addSygusInvConstraint(Term inv, CVC4_API_ARG_CHECK_NOT_NULL(post); CVC4_API_SOLVER_CHECK_TERM(post); - CVC4_API_ARG_CHECK_EXPECTED(inv.d_expr->getType().isFunction(), inv) + CVC4_API_ARG_CHECK_EXPECTED(inv.d_node->getType().isFunction(), inv) << "a function"; - FunctionType invType = inv.d_expr->getType(); + FunctionType invType = inv.d_node->getType().toType(); CVC4_API_ARG_CHECK_EXPECTED(invType.getRangeType().isBoolean(), inv) << "boolean range"; - CVC4_API_CHECK(pre.d_expr->getType() == invType) + CVC4_API_CHECK(pre.d_node->getType().toType() == invType) << "Expected inv and pre to have the same sort"; - CVC4_API_CHECK(post.d_expr->getType() == invType) + CVC4_API_CHECK(post.d_node->getType().toType() == invType) << "Expected inv and post to have the same sort"; const std::vector& invArgTypes = invType.getArgTypes(); @@ -5205,11 +5291,13 @@ void Solver::addSygusInvConstraint(Term inv, expectedTypes.push_back(invType.getRangeType()); FunctionType expectedTransType = d_exprMgr->mkFunctionType(expectedTypes); - CVC4_API_CHECK(trans.d_expr->getType() == expectedTransType) + CVC4_API_CHECK(trans.d_node->toExpr().getType() == expectedTransType) << "Expected trans's sort to be " << invType; - d_smtEngine->assertSygusInvConstraint( - *inv.d_expr, *pre.d_expr, *trans.d_expr, *post.d_expr); + d_smtEngine->assertSygusInvConstraint(inv.d_node->toExpr(), + pre.d_node->toExpr(), + trans.d_node->toExpr(), + post.d_node->toExpr()); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -5231,7 +5319,8 @@ Term Solver::getSynthSolution(Term term) const << "The solver is not in a state immediately preceeded by a " "successful call to checkSynth"; - std::map::const_iterator it = map.find(*term.d_expr); + std::map::const_iterator it = + map.find(term.d_node->toExpr()); CVC4_API_CHECK(it != map.cend()) << "Synth solution not found for given term"; @@ -5266,7 +5355,7 @@ std::vector Solver::getSynthSolutions( for (size_t i = 0, n = terms.size(); i < n; ++i) { std::map::const_iterator it = - map.find(*terms[i].d_expr); + map.find(terms[i].d_node->toExpr()); CVC4_API_CHECK(it != map.cend()) << "Synth solution not found for term at index " << i; @@ -5291,6 +5380,15 @@ void Solver::printSynthSolution(std::ostream& out) const */ 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(); +} + /** * !!! This is only temporarily available until the parser is fully migrated to * the new API. !!! @@ -5317,6 +5415,16 @@ std::vector termVectorToExprs(const std::vector& terms) return exprs; } +std::vector termVectorToNodes(const std::vector& terms) +{ + std::vector res; + for (const Term& t : terms) + { + res.push_back(t.getNode()); + } + return res; +} + std::vector sortVectorToTypes(const std::vector& sorts) { std::vector types; diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 91db4dd58..997616ae3 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -36,11 +36,15 @@ namespace CVC4 { +template +class NodeTemplate; +typedef NodeTemplate Node; class Expr; class Datatype; class DatatypeConstructor; class DatatypeConstructorArg; class ExprManager; +class NodeManager; class SmtEngine; class Type; class Options; @@ -674,6 +678,17 @@ class CVC4_PUBLIC Op */ Op(const Solver* slv, const Kind k, const CVC4::Expr& e); + // !!! This constructor is only temporarily public until the parser is fully + // migrated to the new API. !!! + /** + * 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 + */ + Op(const Solver* slv, const Kind k, const CVC4::Node& n); + /** * Destructor. */ @@ -763,7 +778,7 @@ class CVC4_PUBLIC Op * memory allocation (CVC4::Expr is already ref counted, so this could be * a unique_ptr instead). */ - std::shared_ptr d_expr; + std::shared_ptr d_node; }; /* -------------------------------------------------------------------------- */ @@ -792,6 +807,16 @@ class CVC4_PUBLIC Term */ Term(const Solver* slv, const CVC4::Expr& e); + // !!! This constructor is only temporarily public until the parser is fully + // migrated to the new API. !!! + /** + * Constructor. + * @param slv the associated solver object + * @param n the internal node that is to be wrapped by this term + * @return the Term + */ + Term(const Solver* slv, const CVC4::Node& n); + /** * Constructor. */ @@ -1003,7 +1028,7 @@ class CVC4_PUBLIC Term * @param p the position of the iterator (e.g. which child it's on) */ const_iterator(const Solver* slv, - const std::shared_ptr& e, + const std::shared_ptr& e, uint32_t p); /** @@ -1055,8 +1080,8 @@ class CVC4_PUBLIC Term * The associated solver object. */ const Solver* d_solver; - /* The original expression to be iterated over */ - std::shared_ptr d_orig_expr; + /* The original node to be iterated over */ + std::shared_ptr d_origNode; /* Keeps track of the iteration position */ uint32_t d_pos; }; @@ -1075,6 +1100,10 @@ class CVC4_PUBLIC Term // to the new API. !!! CVC4::Expr getExpr(void) const; + // !!! This is only temporarily available until the parser is fully migrated + // to the new API. !!! + const CVC4::Node& getNode(void) const; + protected: /** * The associated solver object. @@ -1101,7 +1130,7 @@ class CVC4_PUBLIC Term * memory allocation (CVC4::Expr is already ref counted, so this could be * a unique_ptr instead). */ - std::shared_ptr d_expr; + std::shared_ptr d_node; }; /** @@ -3259,6 +3288,10 @@ class CVC4_PUBLIC Solver // 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. !!! SmtEngine* getSmtEngine(void) const; @@ -3350,6 +3383,7 @@ class CVC4_PUBLIC Solver // !!! Only temporarily public until the parser is fully migrated to the // new API. !!! std::vector termVectorToExprs(const std::vector& terms); +std::vector termVectorToNodes(const std::vector& terms); std::vector sortVectorToTypes(const std::vector& sorts); std::set sortSetToTypes(const std::set& sorts); std::vector exprVectorToTerms(const Solver* slv, diff --git a/src/expr/type_node.h b/src/expr/type_node.h index f957fe0d0..0d0c17edf 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -763,6 +763,7 @@ inline Type TypeNode::toType() const } inline TypeNode TypeNode::fromType(const Type& t) { + NodeManagerScope scope(t.d_nodeManager); return NodeManager::fromType(t); } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 9ff6ec6f5..d8657c7dd 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1731,14 +1731,14 @@ void SmtEngine::declareSynthFun(const std::string& id, setSygusConjectureStale(); } -void SmtEngine::assertSygusConstraint(Expr constraint) +void SmtEngine::assertSygusConstraint(const Node& constraint) { SmtScope smts(this); finalOptionsAreSet(); d_private->d_sygusConstraints.push_back(constraint); Trace("smt") << "SmtEngine::assertSygusConstrant: " << constraint << "\n"; - Dump("raw-benchmark") << SygusConstraintCommand(constraint); + Dump("raw-benchmark") << SygusConstraintCommand(constraint.toExpr()); // sygus conjecture is now stale setSygusConjectureStale(); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index b38ec2d7a..a651b8d1e 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -453,7 +453,7 @@ class CVC4_PUBLIC SmtEngine const std::vector& vars); /** Add a regular sygus constraint.*/ - void assertSygusConstraint(Expr constraint); + void assertSygusConstraint(const Node& constraint); /** * Add an invariant constraint. -- 2.30.2