#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"
{
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)
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<uint32_t>::max()) // be careful not to
// overflow
/* 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 */
/* -------------------------------------------------------------------------- */
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); }
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<Divisible>().k;
+ CVC4::Integer _int = d_
node->getConst<Divisible>().k;
i = _int.toString();
}
else if (k == RECORD_UPDATE)
{
- i = d_expr->getConst<RecordUpdate>().getField();
+ i = d_node->getConst<RecordUpdate>().getField();
}
else
{
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<BitVectorRepeat>().d_repeatAmount;
+ i = d_node->getConst<BitVectorRepeat>().d_repeatAmount;
break;
case BITVECTOR_ZERO_EXTEND:
- i = d_expr->getConst<BitVectorZeroExtend>().d_zeroExtendAmount;
+ i = d_node->getConst<BitVectorZeroExtend>().d_zeroExtendAmount;
break;
case BITVECTOR_SIGN_EXTEND:
- i = d_expr->getConst<BitVectorSignExtend>().d_signExtendAmount;
+ i = d_node->getConst<BitVectorSignExtend>().d_signExtendAmount;
break;
case BITVECTOR_ROTATE_LEFT:
- i = d_expr->getConst<BitVectorRotateLeft>().d_rotateLeftAmount;
+ i = d_node->getConst<BitVectorRotateLeft>().d_rotateLeftAmount;
break;
case BITVECTOR_ROTATE_RIGHT:
- i = d_expr->getConst<BitVectorRotateRight>().d_rotateRightAmount;
+ i = d_node->getConst<BitVectorRotateRight>().d_rotateRightAmount;
break;
- case INT_TO_BITVECTOR: i = d_expr->getConst<IntToBitVector>().d_size; break;
- case IAND: i = d_expr->getConst<IntAnd>().d_size; break;
+ case INT_TO_BITVECTOR: i = d_node->getConst<IntToBitVector>().d_size; break;
+ case IAND: i = d_node->getConst<IntAnd>().d_size; break;
case FLOATINGPOINT_TO_UBV:
- i = d_expr->getConst<FloatingPointToUBV>().bvs.d_size;
+ i = d_node->getConst<FloatingPointToUBV>().bvs.d_size;
break;
case FLOATINGPOINT_TO_SBV:
- i = d_expr->getConst<FloatingPointToSBV>().bvs.d_size;
+ i = d_node->getConst<FloatingPointToSBV>().bvs.d_size;
break;
- case TUPLE_UPDATE: i = d_expr->getConst<TupleUpdate>().getIndex(); break;
+ case TUPLE_UPDATE: i = d_node->getConst<TupleUpdate>().getIndex(); break;
default:
CVC4ApiExceptionStream().ostream() << "Can't get uint32_t index from"
<< " kind " << kindToString(k);
std::pair<uint32_t, 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.";
std::pair<uint32_t, uint32_t> 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<BitVectorExtract>();
+ CVC4::BitVectorExtract ext = d_node->getConst<BitVectorExtract>();
indices = std::make_pair(ext.d_high, ext.d_low);
}
else if (k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR)
{
CVC4::FloatingPointToFPIEEEBitVector ext =
- d_expr->getConst<FloatingPointToFPIEEEBitVector>();
+ d_node->getConst<FloatingPointToFPIEEEBitVector>();
indices = std::make_pair(ext.t.exponent(), ext.t.significand());
}
else if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT)
{
CVC4::FloatingPointToFPFloatingPoint ext =
- d_expr->getConst<FloatingPointToFPFloatingPoint>();
+ d_node->getConst<FloatingPointToFPFloatingPoint>();
indices = std::make_pair(ext.t.exponent(), ext.t.significand());
}
else if (k == FLOATINGPOINT_TO_FP_REAL)
{
- CVC4::FloatingPointToFPReal ext = d_expr->getConst<FloatingPointToFPReal>();
+ CVC4::FloatingPointToFPReal ext = d_node->getConst<FloatingPointToFPReal>();
indices = std::make_pair(ext.t.exponent(), ext.t.significand());
}
else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR)
{
CVC4::FloatingPointToFPSignedBitVector ext =
- d_expr->getConst<FloatingPointToFPSignedBitVector>();
+ d_node->getConst<FloatingPointToFPSignedBitVector>();
indices = std::make_pair(ext.t.exponent(), ext.t.significand());
}
else if (k == FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR)
{
CVC4::FloatingPointToFPUnsignedBitVector ext =
- d_expr->getConst<FloatingPointToFPUnsignedBitVector>();
+ d_node->getConst<FloatingPointToFPUnsignedBitVector>();
indices = std::make_pair(ext.t.exponent(), ext.t.significand());
}
else if (k == FLOATINGPOINT_TO_FP_GENERIC)
{
CVC4::FloatingPointToFPGeneric ext =
- d_expr->getConst<FloatingPointToFPGeneric>();
+ d_node->getConst<FloatingPointToFPGeneric>();
indices = std::make_pair(ext.t.exponent(), ext.t.significand());
}
else
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)
{
{
if (t.isIndexedHelper())
{
- return ExprHashFunction()(*t.d_expr);
+ return ExprHashFunction()(t.d_node->toExpr());
}
else
{
/* 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
// 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;
}
}
- 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
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
<< "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<Term> es,
CVC4_API_CHECK(es[i].getSort().isComparableTo(replacements[i].getSort()))
<< "Expecting terms of comparable sort in substitute";
}
+
+ std::vector<Node> nodes = termVectorToNodes(es);
+ std::vector<Node> 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
// 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.
bool Term::isConst() const
{
CVC4_API_CHECK_NOT_NULL;
- return d_expr->isConst();
+ return d_node->isConst();
}
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<ArrayStoreAll>().getValue().toExpr());
+ return Term(d_solver, d_node->getConst<ArrayStoreAll>().getValue());
}
std::vector<Term> 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<Node>& elems = d_expr->getConst<Sequence>().getVec();
+ const std::vector<Node>& elems = d_node->getConst<Sequence>().getVec();
std::vector<Term> terms;
for (const Node& t : elems)
{
- terms.push_back(Term(d_solver, t.toExpr()));
+ terms.push_back(Term(d_solver, t));
}
return terms;
}
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());
}
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());
}
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());
}
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());
}
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());
}
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());
}
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<CVC4::Expr>& e,
+ const std::shared_ptr<CVC4::Node>& 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;
}
}
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);
}
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;
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
{
--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)
{
size_t TermHashFunction::operator()(const Term& t) const
{
- return ExprHashFunction()(*t.d_expr);
+ return ExprHashFunction()(t.d_node->toExpr());
}
/* -------------------------------------------------------------------------- */
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);
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";
}
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
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(
{
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<Term> 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);
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<Sort> cargs;
dt.d_dtype->addSygusConstructor(
- *v.d_expr, ss.str(), sortVectorToTypes(cargs));
+ v.d_node->toExpr(), ss.str(), sortVectorToTypes(cargs));
}
}
}
template <typename T>
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);
}
Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const
{
+ NodeManagerScope scope(getNodeManager());
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
for (size_t i = 0, size = children.size(); i < size; ++i)
{
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;
}
CVC4_API_CHECK(sort.getArrayElementSort().isComparableTo(val.getSort()))
<< "Value does not match element sort.";
Term res = mkValHelper<CVC4::ArrayStoreAll>(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;
}
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;
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;
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>(
- CVC4::FloatingPoint(exp, sig, val.d_expr->getConst<BitVector>()));
+ CVC4::FloatingPoint(exp, sig, val.d_node->getConst<BitVector>()));
CVC4_API_SOLVER_TRY_CATCH_END;
}
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);
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);
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";
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);
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;
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 */
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 */
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";
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 */
Term Solver::mkTerm(Op op, const std::vector<Term>& 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(
}
const CVC4::Kind int_kind = extToIntKind(op.d_kind);
- std::vector<Expr> echildren = termVectorToExprs(children);
- Expr res;
+ std::vector<Node> 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 */
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_CHECK(sorts.size() == terms.size())
<< "Expected the same number of sorts and elements";
- std::vector<CVC4::Expr> args;
+ std::vector<CVC4::Node> args;
for (size_t i = 0, size = sorts.size(); i < size; i++)
{
CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
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);
Op res;
if (kind == RECORD_UPDATE)
{
- res = Op(
- this,
- kind,
- *mkValHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg)).d_expr.get());
+ res = Op(this,
+ kind,
+ *mkValHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg)).d_node);
}
else
{
res = Op(this,
kind,
*mkValHelper<CVC4::Divisible>(CVC4::Divisible(CVC4::Integer(arg)))
- .d_expr.get());
+ .d_node);
}
return res;
switch (kind)
{
case DIVISIBLE:
- res =
- Op(this,
- kind,
- *mkValHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_expr.get());
+ res = Op(this,
+ kind,
+ *mkValHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_node);
break;
case BITVECTOR_REPEAT:
res = Op(this,
kind,
- *mkValHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg))
- .d_expr.get());
+ mkValHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg))
+ .d_node->toExpr());
break;
case BITVECTOR_ZERO_EXTEND:
res = Op(this,
kind,
*mkValHelper<CVC4::BitVectorZeroExtend>(
CVC4::BitVectorZeroExtend(arg))
- .d_expr.get());
+ .d_node);
break;
case BITVECTOR_SIGN_EXTEND:
res = Op(this,
kind,
*mkValHelper<CVC4::BitVectorSignExtend>(
CVC4::BitVectorSignExtend(arg))
- .d_expr.get());
+ .d_node);
break;
case BITVECTOR_ROTATE_LEFT:
res = Op(this,
kind,
*mkValHelper<CVC4::BitVectorRotateLeft>(
CVC4::BitVectorRotateLeft(arg))
- .d_expr.get());
+ .d_node);
break;
case BITVECTOR_ROTATE_RIGHT:
res = Op(this,
kind,
*mkValHelper<CVC4::BitVectorRotateRight>(
CVC4::BitVectorRotateRight(arg))
- .d_expr.get());
+ .d_node);
break;
case INT_TO_BITVECTOR:
- res = Op(this,
- kind,
- *mkValHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg))
- .d_expr.get());
+ res = Op(
+ this,
+ kind,
+ *mkValHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg)).d_node);
break;
case IAND:
- res = Op(this,
- kind,
- *mkValHelper<CVC4::IntAnd>(CVC4::IntAnd(arg)).d_expr.get());
+ res =
+ Op(this, kind, *mkValHelper<CVC4::IntAnd>(CVC4::IntAnd(arg)).d_node);
break;
case FLOATINGPOINT_TO_UBV:
res = Op(
this,
kind,
*mkValHelper<CVC4::FloatingPointToUBV>(CVC4::FloatingPointToUBV(arg))
- .d_expr.get());
+ .d_node);
break;
case FLOATINGPOINT_TO_SBV:
res = Op(
this,
kind,
*mkValHelper<CVC4::FloatingPointToSBV>(CVC4::FloatingPointToSBV(arg))
- .d_expr.get());
+ .d_node);
break;
case TUPLE_UPDATE:
- res = Op(
- this,
- kind,
- *mkValHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg)).d_expr.get());
- break;
- case REGEXP_REPEAT:
res = Op(this,
kind,
- *mkValHelper<CVC4::RegExpRepeat>(CVC4::RegExpRepeat(arg))
- .d_expr.get());
+ *mkValHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg)).d_node);
+ break;
+ case REGEXP_REPEAT:
+ res =
+ Op(this,
+ kind,
+ *mkValHelper<CVC4::RegExpRepeat>(CVC4::RegExpRepeat(arg)).d_node);
break;
default:
CVC4_API_KIND_CHECK_EXPECTED(false, kind)
kind,
*mkValHelper<CVC4::BitVectorExtract>(
CVC4::BitVectorExtract(arg1, arg2))
- .d_expr.get());
+ .d_node);
break;
case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
res = Op(this,
kind,
*mkValHelper<CVC4::FloatingPointToFPIEEEBitVector>(
CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2))
- .d_expr.get());
+ .d_node);
break;
case FLOATINGPOINT_TO_FP_FLOATINGPOINT:
res = Op(this,
kind,
*mkValHelper<CVC4::FloatingPointToFPFloatingPoint>(
CVC4::FloatingPointToFPFloatingPoint(arg1, arg2))
- .d_expr.get());
+ .d_node);
break;
case FLOATINGPOINT_TO_FP_REAL:
res = Op(this,
kind,
*mkValHelper<CVC4::FloatingPointToFPReal>(
CVC4::FloatingPointToFPReal(arg1, arg2))
- .d_expr.get());
+ .d_node);
break;
case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
res = Op(this,
kind,
*mkValHelper<CVC4::FloatingPointToFPSignedBitVector>(
CVC4::FloatingPointToFPSignedBitVector(arg1, arg2))
- .d_expr.get());
+ .d_node);
break;
case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
res = Op(this,
kind,
*mkValHelper<CVC4::FloatingPointToFPUnsignedBitVector>(
CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2))
- .d_expr.get());
+ .d_node);
break;
case FLOATINGPOINT_TO_FP_GENERIC:
res = Op(this,
kind,
*mkValHelper<CVC4::FloatingPointToFPGeneric>(
CVC4::FloatingPointToFPGeneric(arg1, arg2))
- .d_expr.get());
+ .d_node);
break;
case REGEXP_LOOP:
- res = Op(this,
- kind,
- *mkValHelper<CVC4::RegExpLoop>(CVC4::RegExpLoop(arg1, arg2))
- .d_expr.get());
+ res = Op(
+ this,
+ kind,
+ *mkValHelper<CVC4::RegExpLoop>(CVC4::RegExpLoop(arg1, arg2)).d_node);
break;
default:
CVC4_API_KIND_CHECK_EXPECTED(false, kind)
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;
}
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;
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;
}
<< "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;
}
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";
}
Expr fun = d_exprMgr->mkVar(symbol, type);
std::vector<Expr> 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;
}
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)
CVC4_API_SOLVER_CHECK_TERM(term);
std::vector<Expr> 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;
}
Term term,
bool global) const
{
+ NodeManagerScope scope(getNodeManager());
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified())
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";
}
Expr fun = d_exprMgr->mkVar(symbol, type);
std::vector<Expr> 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;
}
Term term,
bool global) const
{
+ NodeManagerScope scope(getNodeManager());
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified())
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)
CVC4_API_SOLVER_CHECK_TERM(term);
std::vector<Expr> 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;
}
const std::vector<Term>& terms,
bool global) const
{
+ NodeManagerScope scope(getNodeManager());
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified())
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)
{
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;
}
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;
{
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);
}
{
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);
// 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);
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)
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)
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)
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;
}
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;
}
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<Type>& invArgTypes = invType.getArgTypes();
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;
}
<< "The solver is not in a state immediately preceeded by a "
"successful call to checkSynth";
- std::map<CVC4::Expr, CVC4::Expr>::const_iterator it = map.find(*term.d_expr);
+ std::map<CVC4::Expr, CVC4::Expr>::const_iterator it =
+ map.find(term.d_node->toExpr());
CVC4_API_CHECK(it != map.cend()) << "Synth solution not found for given term";
for (size_t i = 0, n = terms.size(); i < n; ++i)
{
std::map<CVC4::Expr, CVC4::Expr>::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;
*/
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. !!!
return exprs;
}
+std::vector<Node> termVectorToNodes(const std::vector<Term>& terms)
+{
+ std::vector<Node> res;
+ for (const Term& t : terms)
+ {
+ res.push_back(t.getNode());
+ }
+ return res;
+}
+
std::vector<Type> sortVectorToTypes(const std::vector<Sort>& sorts)
{
std::vector<Type> types;
projects / cvc5.git / commitdiff