summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/api/cvc4cpp.cpp545
-rw-r--r--src/api/cvc4cpp.h111
-rw-r--r--src/parser/cvc/Cvc.g43
-rw-r--r--src/parser/parser.cpp55
-rw-r--r--src/parser/parser.h12
-rw-r--r--src/parser/smt2/Smt2.g18
-rw-r--r--src/parser/smt2/smt2.cpp13
-rw-r--r--src/parser/tptp/Tptp.g4
-rw-r--r--test/unit/api/op_black.h2
-rw-r--r--test/unit/api/solver_black.h6
-rw-r--r--test/unit/api/term_black.h14
-rw-r--r--test/unit/parser/parser_builder_black.h2
12 files changed, 491 insertions, 334 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 1ea421c4b..0bfb9a325 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -702,6 +702,8 @@ class CVC4ApiExceptionStream
CVC4_API_CHECK(isDefinedKind(kind)) \
<< "Invalid kind '" << kindToString(kind) << "'";
+#define CVC4_API_SORT_CHECK_SOLVER(sort)
+
#define CVC4_API_KIND_CHECK_EXPECTED(cond, kind) \
CVC4_PREDICT_TRUE(cond) \
? (void)0 \
@@ -823,9 +825,12 @@ std::ostream& operator<<(std::ostream& out, const Result& r)
/* Sort */
/* -------------------------------------------------------------------------- */
-Sort::Sort(const CVC4::Type& t) : d_type(new CVC4::Type(t)) {}
+Sort::Sort(const Solver* slv, const CVC4::Type& t)
+ : d_solver(slv), d_type(new CVC4::Type(t))
+{
+}
-Sort::Sort() : d_type(new CVC4::Type()) {}
+Sort::Sort() : d_solver(nullptr), d_type(new CVC4::Type()) {}
Sort::~Sort() {}
@@ -909,7 +914,7 @@ bool Sort::isComparableTo(Sort s) const
Datatype Sort::getDatatype() const
{
CVC4_API_CHECK(isDatatype()) << "Expected datatype sort.";
- return DatatypeType(*d_type).getDatatype();
+ return Datatype(d_solver, DatatypeType(*d_type).getDatatype());
}
Sort Sort::instantiate(const std::vector<Sort>& params) const
@@ -923,10 +928,10 @@ Sort Sort::instantiate(const std::vector<Sort>& params) const
}
if (d_type->isDatatype())
{
- return DatatypeType(*d_type).instantiate(tparams);
+ return Sort(d_solver, DatatypeType(*d_type).instantiate(tparams));
}
Assert(d_type->isSortConstructor());
- return SortConstructorType(*d_type).instantiate(tparams);
+ return Sort(d_solver, SortConstructorType(*d_type).instantiate(tparams));
}
std::string Sort::toString() const { return d_type->toString(); }
@@ -947,13 +952,13 @@ std::vector<Sort> Sort::getConstructorDomainSorts() const
{
CVC4_API_CHECK(isConstructor()) << "Not a function sort.";
std::vector<CVC4::Type> types = ConstructorType(*d_type).getArgTypes();
- return typeVectorToSorts(types);
+ return typeVectorToSorts(d_solver, types);
}
Sort Sort::getConstructorCodomainSort() const
{
CVC4_API_CHECK(isConstructor()) << "Not a function sort.";
- return ConstructorType(*d_type).getRangeType();
+ return Sort(d_solver, ConstructorType(*d_type).getRangeType());
}
/* Function sort ------------------------------------------------------- */
@@ -968,13 +973,13 @@ std::vector<Sort> Sort::getFunctionDomainSorts() const
{
CVC4_API_CHECK(isFunction()) << "Not a function sort.";
std::vector<CVC4::Type> types = FunctionType(*d_type).getArgTypes();
- return typeVectorToSorts(types);
+ return typeVectorToSorts(d_solver, types);
}
Sort Sort::getFunctionCodomainSort() const
{
CVC4_API_CHECK(isFunction()) << "Not a function sort.";
- return FunctionType(*d_type).getRangeType();
+ return Sort(d_solver, FunctionType(*d_type).getRangeType());
}
/* Array sort ---------------------------------------------------------- */
@@ -982,13 +987,13 @@ Sort Sort::getFunctionCodomainSort() const
Sort Sort::getArrayIndexSort() const
{
CVC4_API_CHECK(isArray()) << "Not an array sort.";
- return ArrayType(*d_type).getIndexType();
+ return Sort(d_solver, ArrayType(*d_type).getIndexType());
}
Sort Sort::getArrayElementSort() const
{
CVC4_API_CHECK(isArray()) << "Not an array sort.";
- return ArrayType(*d_type).getConstituentType();
+ return Sort(d_solver, ArrayType(*d_type).getConstituentType());
}
/* Set sort ------------------------------------------------------------ */
@@ -996,7 +1001,7 @@ Sort Sort::getArrayElementSort() const
Sort Sort::getSetElementSort() const
{
CVC4_API_CHECK(isSet()) << "Not a set sort.";
- return SetType(*d_type).getElementType();
+ return Sort(d_solver, SetType(*d_type).getElementType());
}
/* Uninterpreted sort -------------------------------------------------- */
@@ -1017,7 +1022,7 @@ std::vector<Sort> Sort::getUninterpretedSortParamSorts() const
{
CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
std::vector<CVC4::Type> types = SortType(*d_type).getParamTypes();
- return typeVectorToSorts(types);
+ return typeVectorToSorts(d_solver, types);
}
/* Sort constructor sort ----------------------------------------------- */
@@ -1062,7 +1067,7 @@ std::vector<Sort> Sort::getDatatypeParamSorts() const
{
CVC4_API_CHECK(isParametricDatatype()) << "Not a parametric datatype sort.";
std::vector<CVC4::Type> types = DatatypeType(*d_type).getParamTypes();
- return typeVectorToSorts(types);
+ return typeVectorToSorts(d_solver, types);
}
size_t Sort::getDatatypeArity() const
@@ -1083,7 +1088,7 @@ std::vector<Sort> Sort::getTupleSorts() const
{
CVC4_API_CHECK(isTuple()) << "Not a tuple sort.";
std::vector<CVC4::Type> types = DatatypeType(*d_type).getTupleTypes();
- return typeVectorToSorts(types);
+ return typeVectorToSorts(d_solver, types);
}
/* --------------------------------------------------------------------- */
@@ -1105,9 +1110,13 @@ size_t SortHashFunction::operator()(const Sort& s) const
Op::Op() : d_kind(NULL_EXPR), d_expr(new CVC4::Expr()) {}
-Op::Op(const Kind k) : d_kind(k), d_expr(new CVC4::Expr()) {}
+Op::Op(const Solver* slv, const Kind k)
+ : d_solver(slv), d_kind(k), d_expr(new CVC4::Expr())
+{
+}
-Op::Op(const Kind k, const CVC4::Expr& e) : d_kind(k), d_expr(new CVC4::Expr(e))
+Op::Op(const Solver* slv, const Kind k, const CVC4::Expr& e)
+ : d_solver(slv), d_kind(k), d_expr(new CVC4::Expr(e))
{
}
@@ -1323,19 +1332,20 @@ size_t OpHashFunction::operator()(const Op& t) const
/* Term */
/* -------------------------------------------------------------------------- */
-Term::Term() : d_expr(new CVC4::Expr()) {}
+Term::Term() : d_solver(nullptr), d_expr(new CVC4::Expr()) {}
-Term::Term(const CVC4::Expr& e) : d_expr(new CVC4::Expr(e)) {}
+Term::Term(const Solver* slv, const CVC4::Expr& e)
+ : d_solver(slv), d_expr(new CVC4::Expr(e))
+{
+}
Term::~Term() {}
-/* Helpers */
-/* -------------------------------------------------------------------------- */
-
-/* Split out to avoid nested API calls (problematic with API tracing). */
-/* .......................................................................... */
-
-bool Term::isNullHelper() const { return d_expr->isNull(); }
+bool Term::isNullHelper() const
+{
+ /* Split out to avoid nested API calls (problematic with API tracing). */
+ return d_expr->isNull();
+}
bool Term::operator==(const Term& t) const { return *d_expr == *t.d_expr; }
@@ -1371,12 +1381,12 @@ Term Term::operator[](size_t index) const
if (index == 0)
{
// return the operator
- return api::Term(d_expr->getOperator());
+ return Term(d_solver, d_expr->getOperator());
}
// otherwise we are looking up child at (index-1)
index--;
}
- return api::Term((*d_expr)[index]);
+ return Term(d_solver, (*d_expr)[index]);
}
uint64_t Term::getId() const
@@ -1394,7 +1404,7 @@ Kind Term::getKind() const
Sort Term::getSort() const
{
CVC4_API_CHECK_NOT_NULL;
- return Sort(d_expr->getType());
+ return Sort(d_solver, d_expr->getType());
}
Term Term::substitute(Term e, Term replacement) const
@@ -1406,7 +1416,7 @@ 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 api::Term(d_expr->substitute(e.getExpr(), replacement.getExpr()));
+ return Term(d_solver, d_expr->substitute(e.getExpr(), replacement.getExpr()));
}
Term Term::substitute(const std::vector<Term> es,
@@ -1424,8 +1434,9 @@ 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";
}
- return api::Term(d_expr->substitute(termVectorToExprs(es),
- termVectorToExprs(replacements)));
+ return Term(d_solver,
+ d_expr->substitute(termVectorToExprs(es),
+ termVectorToExprs(replacements)));
}
bool Term::hasOp() const
@@ -1447,18 +1458,18 @@ Op Term::getOp() const
// is one of the APPLY_* kinds
if (isApplyKind(d_expr->getKind()))
{
- return Op(intToExtKind(d_expr->getKind()));
+ return Op(d_solver, intToExtKind(d_expr->getKind()));
}
else if (d_expr->isParameterized())
{
// it's an indexed operator
// so we should return the indexed op
CVC4::Expr op = d_expr->getOperator();
- return Op(intToExtKind(d_expr->getKind()), op);
+ return Op(d_solver, intToExtKind(d_expr->getKind()), op);
}
else
{
- return Op(intToExtKind(d_expr->getKind()));
+ return Op(d_solver, intToExtKind(d_expr->getKind()));
}
}
@@ -1475,9 +1486,9 @@ Term Term::notTerm() const
CVC4_API_CHECK_NOT_NULL;
try
{
- Term res = d_expr->notExpr();
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ Expr res = d_expr->notExpr();
+ (void)res.getType(true); /* kick off type checking */
+ return Term(d_solver, res);
}
catch (const CVC4::TypeCheckingException& e)
{
@@ -1491,9 +1502,9 @@ Term Term::andTerm(const Term& t) const
CVC4_API_ARG_CHECK_NOT_NULL(t);
try
{
- Term res = d_expr->andExpr(*t.d_expr);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ Expr res = d_expr->andExpr(*t.d_expr);
+ (void)res.getType(true); /* kick off type checking */
+ return Term(d_solver, res);
}
catch (const CVC4::TypeCheckingException& e)
{
@@ -1507,9 +1518,9 @@ Term Term::orTerm(const Term& t) const
CVC4_API_ARG_CHECK_NOT_NULL(t);
try
{
- Term res = d_expr->orExpr(*t.d_expr);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ Expr res = d_expr->orExpr(*t.d_expr);
+ (void)res.getType(true); /* kick off type checking */
+ return Term(d_solver, res);
}
catch (const CVC4::TypeCheckingException& e)
{
@@ -1523,9 +1534,9 @@ Term Term::xorTerm(const Term& t) const
CVC4_API_ARG_CHECK_NOT_NULL(t);
try
{
- Term res = d_expr->xorExpr(*t.d_expr);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ Expr res = d_expr->xorExpr(*t.d_expr);
+ (void)res.getType(true); /* kick off type checking */
+ return Term(d_solver, res);
}
catch (const CVC4::TypeCheckingException& e)
{
@@ -1539,9 +1550,9 @@ Term Term::eqTerm(const Term& t) const
CVC4_API_ARG_CHECK_NOT_NULL(t);
try
{
- Term res = d_expr->eqExpr(*t.d_expr);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ Expr res = d_expr->eqExpr(*t.d_expr);
+ (void)res.getType(true); /* kick off type checking */
+ return Term(d_solver, res);
}
catch (const CVC4::TypeCheckingException& e)
{
@@ -1555,9 +1566,9 @@ Term Term::impTerm(const Term& t) const
CVC4_API_ARG_CHECK_NOT_NULL(t);
try
{
- Term res = d_expr->impExpr(*t.d_expr);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ Expr res = d_expr->impExpr(*t.d_expr);
+ (void)res.getType(true); /* kick off type checking */
+ return Term(d_solver, res);
}
catch (const CVC4::TypeCheckingException& e)
{
@@ -1572,9 +1583,9 @@ Term Term::iteTerm(const Term& then_t, const Term& else_t) const
CVC4_API_ARG_CHECK_NOT_NULL(else_t);
try
{
- Term res = d_expr->iteExpr(*then_t.d_expr, *else_t.d_expr);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ Expr res = d_expr->iteExpr(*then_t.d_expr, *else_t.d_expr);
+ (void)res.getType(true); /* kick off type checking */
+ return Term(d_solver, res);
}
catch (const CVC4::TypeCheckingException& e)
{
@@ -1584,11 +1595,15 @@ Term Term::iteTerm(const Term& then_t, const Term& else_t) const
std::string Term::toString() const { return d_expr->toString(); }
-Term::const_iterator::const_iterator() : d_orig_expr(nullptr), d_pos(0) {}
+Term::const_iterator::const_iterator()
+ : d_solver(nullptr), d_orig_expr(nullptr), d_pos(0)
+{
+}
-Term::const_iterator::const_iterator(const std::shared_ptr<CVC4::Expr>& e,
+Term::const_iterator::const_iterator(const Solver* slv,
+ const std::shared_ptr<CVC4::Expr>& e,
uint32_t p)
- : d_orig_expr(e), d_pos(p)
+ : d_solver(slv), d_orig_expr(e), d_pos(p)
{
}
@@ -1647,7 +1662,7 @@ Term Term::const_iterator::operator*() const
if (!d_pos && extra_child)
{
- return Term(d_orig_expr->getOperator());
+ return Term(d_solver, d_orig_expr->getOperator());
}
else
{
@@ -1658,13 +1673,13 @@ Term Term::const_iterator::operator*() const
--idx;
}
Assert(idx >= 0);
- return Term((*d_orig_expr)[idx]);
+ return Term(d_solver, (*d_orig_expr)[idx]);
}
}
Term::const_iterator Term::begin() const
{
- return Term::const_iterator(d_expr, 0);
+ return Term::const_iterator(d_solver, d_expr, 0);
}
Term::const_iterator Term::end() const
@@ -1681,7 +1696,7 @@ Term::const_iterator Term::end() const
// one more child if this is a UF application (count the UF as a child)
++endpos;
}
- return Term::const_iterator(d_expr, endpos);
+ return Term::const_iterator(d_solver, d_expr, endpos);
}
// !!! This is only temporarily available until the parser is fully migrated
@@ -1789,25 +1804,25 @@ std::ostream& operator<<(std::ostream& out,
/* DatatypeDecl ------------------------------------------------------------- */
-DatatypeDecl::DatatypeDecl(const Solver* s,
+DatatypeDecl::DatatypeDecl(const Solver* slv,
const std::string& name,
bool isCoDatatype)
- : d_dtype(new CVC4::Datatype(s->getExprManager(), name, isCoDatatype))
+ : d_dtype(new CVC4::Datatype(slv->getExprManager(), name, isCoDatatype))
{
}
-DatatypeDecl::DatatypeDecl(const Solver* s,
+DatatypeDecl::DatatypeDecl(const Solver* slv,
const std::string& name,
Sort param,
bool isCoDatatype)
- : d_dtype(new CVC4::Datatype(s->getExprManager(),
+ : d_dtype(new CVC4::Datatype(slv->getExprManager(),
name,
std::vector<Type>{*param.d_type},
isCoDatatype))
{
}
-DatatypeDecl::DatatypeDecl(const Solver* s,
+DatatypeDecl::DatatypeDecl(const Solver* slv,
const std::string& name,
const std::vector<Sort>& params,
bool isCoDatatype)
@@ -1818,7 +1833,7 @@ DatatypeDecl::DatatypeDecl(const Solver* s,
tparams.push_back(*p.d_type);
}
d_dtype = std::shared_ptr<CVC4::Datatype>(
- new CVC4::Datatype(s->getExprManager(), name, tparams, isCoDatatype));
+ new CVC4::Datatype(slv->getExprManager(), name, tparams, isCoDatatype));
}
bool DatatypeDecl::isNullHelper() const { return !d_dtype; }
@@ -1875,8 +1890,9 @@ std::ostream& operator<<(std::ostream& out, const DatatypeDecl& dtdecl)
DatatypeSelector::DatatypeSelector() { d_stor = nullptr; }
-DatatypeSelector::DatatypeSelector(const CVC4::DatatypeConstructorArg& stor)
- : d_stor(new CVC4::DatatypeConstructorArg(stor))
+DatatypeSelector::DatatypeSelector(const Solver* slv,
+ const CVC4::DatatypeConstructorArg& stor)
+ : d_solver(slv), d_stor(new CVC4::DatatypeConstructorArg(stor))
{
CVC4_API_CHECK(d_stor->isResolved()) << "Expected resolved datatype selector";
}
@@ -1887,13 +1903,13 @@ std::string DatatypeSelector::getName() const { return d_stor->getName(); }
Term DatatypeSelector::getSelectorTerm() const
{
- Term sel = d_stor->getSelector();
+ Term sel = Term(d_solver, d_stor->getSelector());
return sel;
}
Sort DatatypeSelector::getRangeSort() const
{
- return Sort(d_stor->getRangeType());
+ return Sort(d_solver, d_stor->getRangeType());
}
std::string DatatypeSelector::toString() const
@@ -1919,10 +1935,13 @@ std::ostream& operator<<(std::ostream& out, const DatatypeSelector& stor)
/* DatatypeConstructor ------------------------------------------------------ */
-DatatypeConstructor::DatatypeConstructor() { d_ctor = nullptr; }
+DatatypeConstructor::DatatypeConstructor() : d_solver(nullptr), d_ctor(nullptr)
+{
+}
-DatatypeConstructor::DatatypeConstructor(const CVC4::DatatypeConstructor& ctor)
- : d_ctor(new CVC4::DatatypeConstructor(ctor))
+DatatypeConstructor::DatatypeConstructor(const Solver* slv,
+ const CVC4::DatatypeConstructor& ctor)
+ : d_solver(slv), d_ctor(new CVC4::DatatypeConstructor(ctor))
{
CVC4_API_CHECK(d_ctor->isResolved())
<< "Expected resolved datatype constructor";
@@ -1934,13 +1953,13 @@ std::string DatatypeConstructor::getName() const { return d_ctor->getName(); }
Term DatatypeConstructor::getConstructorTerm() const
{
- Term ctor = d_ctor->getConstructor();
+ Term ctor = Term(d_solver, d_ctor->getConstructor());
return ctor;
}
Term DatatypeConstructor::getTesterTerm() const
{
- Term tst = d_ctor->getTester();
+ Term tst = Term(d_solver, d_ctor->getTester());
return tst;
}
@@ -1951,7 +1970,7 @@ size_t DatatypeConstructor::getNumSelectors() const
DatatypeSelector DatatypeConstructor::operator[](size_t index) const
{
- return (*d_ctor)[index];
+ return DatatypeSelector(d_solver, (*d_ctor)[index]);
}
DatatypeSelector DatatypeConstructor::operator[](const std::string& name) const
@@ -1972,36 +1991,41 @@ Term DatatypeConstructor::getSelectorTerm(const std::string& name) const
DatatypeConstructor::const_iterator DatatypeConstructor::begin() const
{
- return DatatypeConstructor::const_iterator(*d_ctor, true);
+ return DatatypeConstructor::const_iterator(d_solver, *d_ctor, true);
}
DatatypeConstructor::const_iterator DatatypeConstructor::end() const
{
- return DatatypeConstructor::const_iterator(*d_ctor, false);
+ return DatatypeConstructor::const_iterator(d_solver, *d_ctor, false);
}
DatatypeConstructor::const_iterator::const_iterator(
- const CVC4::DatatypeConstructor& ctor, bool begin)
+ const Solver* slv, const CVC4::DatatypeConstructor& ctor, bool begin)
{
+ d_solver = slv;
d_int_stors = ctor.getArgs();
+
const std::vector<CVC4::DatatypeConstructorArg>* sels =
static_cast<const std::vector<CVC4::DatatypeConstructorArg>*>(
d_int_stors);
for (const auto& s : *sels)
{
/* Can not use emplace_back here since constructor is private. */
- d_stors.push_back(DatatypeSelector(s));
+ d_stors.push_back(DatatypeSelector(d_solver, s));
}
d_idx = begin ? 0 : sels->size();
}
-// Nullary constructor for Cython
-DatatypeConstructor::const_iterator::const_iterator() {}
+DatatypeConstructor::const_iterator::const_iterator()
+ : d_solver(nullptr), d_int_stors(nullptr), d_idx(0)
+{
+}
DatatypeConstructor::const_iterator&
DatatypeConstructor::const_iterator::operator=(
const DatatypeConstructor::const_iterator& it)
{
+ d_solver = it.d_solver;
d_int_stors = it.d_int_stors;
d_stors = it.d_stors;
d_idx = it.d_idx;
@@ -2076,7 +2100,7 @@ DatatypeSelector DatatypeConstructor::getSelectorForName(
}
CVC4_API_CHECK(foundSel) << "No selector " << name << " for constructor "
<< getName() << " exists";
- return (*d_ctor)[index];
+ return DatatypeSelector(d_solver, (*d_ctor)[index]);
}
std::ostream& operator<<(std::ostream& out, const DatatypeConstructor& ctor)
@@ -2087,21 +2111,20 @@ std::ostream& operator<<(std::ostream& out, const DatatypeConstructor& ctor)
/* Datatype ----------------------------------------------------------------- */
-Datatype::Datatype(const CVC4::Datatype& dtype)
- : d_dtype(new CVC4::Datatype(dtype))
+Datatype::Datatype(const Solver* slv, const CVC4::Datatype& dtype)
+ : d_solver(slv), d_dtype(new CVC4::Datatype(dtype))
{
CVC4_API_CHECK(d_dtype->isResolved()) << "Expected resolved datatype";
}
-// Nullary constructor for Cython
-Datatype::Datatype() {}
+Datatype::Datatype() : d_solver(nullptr), d_dtype(nullptr) {}
Datatype::~Datatype() {}
DatatypeConstructor Datatype::operator[](size_t idx) const
{
CVC4_API_CHECK(idx < getNumConstructors()) << "Index out of bounds.";
- return (*d_dtype)[idx];
+ return DatatypeConstructor(d_solver, (*d_dtype)[idx]);
}
DatatypeConstructor Datatype::operator[](const std::string& name) const
@@ -2141,12 +2164,12 @@ std::string Datatype::toString() const { return d_dtype->getName(); }
Datatype::const_iterator Datatype::begin() const
{
- return Datatype::const_iterator(*d_dtype, true);
+ return Datatype::const_iterator(d_solver, *d_dtype, true);
}
Datatype::const_iterator Datatype::end() const
{
- return Datatype::const_iterator(*d_dtype, false);
+ return Datatype::const_iterator(d_solver, *d_dtype, false);
}
// !!! This is only temporarily available until the parser is fully migrated
@@ -2169,28 +2192,33 @@ DatatypeConstructor Datatype::getConstructorForName(
}
CVC4_API_CHECK(foundCons) << "No constructor " << name << " for datatype "
<< getName() << " exists";
- return (*d_dtype)[index];
+ return DatatypeConstructor(d_solver, (*d_dtype)[index]);
}
-Datatype::const_iterator::const_iterator(const CVC4::Datatype& dtype,
+Datatype::const_iterator::const_iterator(const Solver* slv,
+ const CVC4::Datatype& dtype,
bool begin)
+ : d_solver(slv), d_int_ctors(dtype.getConstructors())
{
- d_int_ctors = dtype.getConstructors();
const std::vector<CVC4::DatatypeConstructor>* cons =
static_cast<const std::vector<CVC4::DatatypeConstructor>*>(d_int_ctors);
for (const auto& c : *cons)
{
/* Can not use emplace_back here since constructor is private. */
- d_ctors.push_back(DatatypeConstructor(c));
+ d_ctors.push_back(DatatypeConstructor(d_solver, c));
}
d_idx = begin ? 0 : cons->size();
}
-Datatype::const_iterator::const_iterator() {}
+Datatype::const_iterator::const_iterator()
+ : d_solver(nullptr), d_int_ctors(nullptr), d_idx(0)
+{
+}
Datatype::const_iterator& Datatype::const_iterator::operator=(
const Datatype::const_iterator& it)
{
+ d_solver = it.d_solver;
d_int_ctors = it.d_int_ctors;
d_ctors = it.d_ctors;
d_idx = it.d_idx;
@@ -2235,10 +2263,10 @@ bool Datatype::const_iterator::operator!=(
/* -------------------------------------------------------------------------- */
/* Grammar */
/* -------------------------------------------------------------------------- */
-Grammar::Grammar(const Solver* s,
+Grammar::Grammar(const Solver* slv,
const std::vector<Term>& sygusVars,
const std::vector<Term>& ntSymbols)
- : d_s(s),
+ : d_solver(slv),
d_sygusVars(sygusVars),
d_ntSyms(ntSymbols),
d_ntsToTerms(ntSymbols.size()),
@@ -2326,8 +2354,9 @@ Sort Grammar::resolve()
if (!d_sygusVars.empty())
{
- bvl = d_s->getExprManager()->mkExpr(CVC4::kind::BOUND_VAR_LIST,
- termVectorToExprs(d_sygusVars));
+ bvl = Term(d_solver,
+ d_solver->getExprManager()->mkExpr(
+ CVC4::kind::BOUND_VAR_LIST, termVectorToExprs(d_sygusVars)));
}
std::unordered_map<Term, Sort, TermHashFunction> ntsToUnres(d_ntSyms.size());
@@ -2336,7 +2365,8 @@ Sort Grammar::resolve()
{
// make the unresolved type, used for referencing the final version of
// the ntsymbol's datatype
- ntsToUnres[ntsymbol] = d_s->getExprManager()->mkSort(ntsymbol.toString());
+ ntsToUnres[ntsymbol] =
+ Sort(d_solver, d_solver->getExprManager()->mkSort(ntsymbol.toString()));
}
std::vector<CVC4::Datatype> datatypes;
@@ -2347,7 +2377,7 @@ Sort Grammar::resolve()
for (const Term& ntSym : d_ntSyms)
{
// make the datatype, which encodes terms generated by this non-terminal
- DatatypeDecl dtDecl(d_s, ntSym.toString());
+ DatatypeDecl dtDecl(d_solver, ntSym.toString());
for (const Term& consTerm : d_ntsToTerms[ntSym])
{
@@ -2356,7 +2386,8 @@ Sort Grammar::resolve()
if (d_allowVars.find(ntSym) != d_allowVars.cend())
{
- addSygusConstructorVariables(dtDecl, ntSym.d_expr->getType());
+ addSygusConstructorVariables(dtDecl,
+ Sort(d_solver, ntSym.d_expr->getType()));
}
bool aci = d_allowConst.find(ntSym) != d_allowConst.end();
@@ -2375,11 +2406,11 @@ Sort Grammar::resolve()
}
std::vector<DatatypeType> datatypeTypes =
- d_s->getExprManager()->mkMutualDatatypeTypes(
+ d_solver->getExprManager()->mkMutualDatatypeTypes(
datatypes, unresTypes, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
// return is the first datatype
- return datatypeTypes[0];
+ return Sort(d_solver, datatypeTypes[0]);
}
void Grammar::addSygusConstructorTerm(
@@ -2406,11 +2437,13 @@ void Grammar::addSygusConstructorTerm(
*op.d_expr, termVectorToExprs(args));
if (!args.empty())
{
- Term lbvl = d_s->getExprManager()->mkExpr(CVC4::kind::BOUND_VAR_LIST,
- termVectorToExprs(args));
+ Term lbvl = Term(d_solver,
+ d_solver->getExprManager()->mkExpr(
+ CVC4::kind::BOUND_VAR_LIST, termVectorToExprs(args)));
// its operator is a lambda
- op = d_s->getExprManager()->mkExpr(CVC4::kind::LAMBDA,
- {*lbvl.d_expr, *op.d_expr});
+ op = Term(d_solver,
+ d_solver->getExprManager()->mkExpr(CVC4::kind::LAMBDA,
+ {*lbvl.d_expr, *op.d_expr}));
}
dt.d_dtype->addSygusConstructor(
*op.d_expr, ssCName.str(), sortVectorToTypes(cargs), spc);
@@ -2426,7 +2459,9 @@ Term Grammar::purifySygusGTerm(
ntsToUnres.find(term);
if (itn != ntsToUnres.cend())
{
- Term ret = d_s->getExprManager()->mkBoundVar(term.d_expr->getType());
+ Term ret =
+ Term(d_solver,
+ d_solver->getExprManager()->mkBoundVar(term.d_expr->getType()));
args.push_back(ret);
cargs.push_back(itn->second);
return ret;
@@ -2435,7 +2470,8 @@ Term Grammar::purifySygusGTerm(
bool childChanged = false;
for (unsigned i = 0, nchild = term.d_expr->getNumChildren(); i < nchild; i++)
{
- Term ptermc = purifySygusGTerm((*term.d_expr)[i], args, cargs, ntsToUnres);
+ Term ptermc = purifySygusGTerm(
+ Term(d_solver, (*term.d_expr)[i]), args, cargs, ntsToUnres);
pchildren.push_back(ptermc);
childChanged = childChanged || *ptermc.d_expr != (*term.d_expr)[i];
}
@@ -2444,22 +2480,22 @@ Term Grammar::purifySygusGTerm(
return term;
}
- Term nret;
+ Expr nret;
if (term.d_expr->isParameterized())
{
// it's an indexed operator so we should provide the op
- nret = d_s->getExprManager()->mkExpr(term.d_expr->getKind(),
- term.d_expr->getOperator(),
- termVectorToExprs(pchildren));
+ nret = d_solver->getExprManager()->mkExpr(term.d_expr->getKind(),
+ term.d_expr->getOperator(),
+ termVectorToExprs(pchildren));
}
else
{
- nret = d_s->getExprManager()->mkExpr(term.d_expr->getKind(),
- termVectorToExprs(pchildren));
+ nret = d_solver->getExprManager()->mkExpr(term.d_expr->getKind(),
+ termVectorToExprs(pchildren));
}
- return nret;
+ return Term(d_solver, nret);
}
void Grammar::addSygusConstructorVariables(DatatypeDecl& dt, Sort sort) const
@@ -2538,9 +2574,9 @@ Solver::~Solver() {}
template <typename T>
Term Solver::mkValHelper(T t) const
{
- Term res = d_exprMgr->mkConst(t);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ Expr res = d_exprMgr->mkConst(t);
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
}
Term Solver::mkRealFromStrHelper(const std::string& s) const
@@ -2623,7 +2659,7 @@ Term Solver::mkTermFromKind(Kind kind) const
kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, kind)
<< "PI or REGEXP_EMPTY or REGEXP_SIGMA";
- Term res;
+ Expr res;
if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA)
{
CVC4::Kind k = extToIntKind(kind);
@@ -2635,8 +2671,8 @@ Term Solver::mkTermFromKind(Kind kind) const
Assert(kind == PI);
res = d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
}
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -2656,7 +2692,7 @@ Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const
Assert(isDefinedIntKind(k))
<< "Not a defined internal kind : " << k << " " << kind;
- Term res;
+ Expr res;
if (echildren.size() > 2)
{
if (kind == INTS_DIVISION || kind == XOR || kind == MINUS
@@ -2701,8 +2737,8 @@ Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const
res = d_exprMgr->mkExpr(k, echildren);
}
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -2726,7 +2762,7 @@ std::vector<Sort> Solver::mkDatatypeSortsInternal(
std::vector<Sort> retTypes;
for (CVC4::DatatypeType t : dtypes)
{
- retTypes.push_back(Sort(t));
+ retTypes.push_back(Sort(this, t));
}
return retTypes;
@@ -2786,49 +2822,49 @@ void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const
Sort Solver::getNullSort(void) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- return Type();
+ return Sort(this, Type());
CVC4_API_SOLVER_TRY_CATCH_END;
}
Sort Solver::getBooleanSort(void) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- return d_exprMgr->booleanType();
+ return Sort(this, d_exprMgr->booleanType());
CVC4_API_SOLVER_TRY_CATCH_END;
}
Sort Solver::getIntegerSort(void) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- return d_exprMgr->integerType();
+ return Sort(this, d_exprMgr->integerType());
CVC4_API_SOLVER_TRY_CATCH_END;
}
Sort Solver::getRealSort(void) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- return d_exprMgr->realType();
+ return Sort(this, d_exprMgr->realType());
CVC4_API_SOLVER_TRY_CATCH_END;
}
Sort Solver::getRegExpSort(void) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- return d_exprMgr->regExpType();
+ return Sort(this, d_exprMgr->regExpType());
CVC4_API_SOLVER_TRY_CATCH_END;
}
Sort Solver::getStringSort(void) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- return d_exprMgr->stringType();
+ return Sort(this, d_exprMgr->stringType());
CVC4_API_SOLVER_TRY_CATCH_END;
}
Sort Solver::getRoundingmodeSort(void) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- return d_exprMgr->roundingModeType();
+ return Sort(this, d_exprMgr->roundingModeType());
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -2842,7 +2878,8 @@ Sort Solver::mkArraySort(Sort indexSort, Sort elemSort) const
CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort)
<< "non-null element sort";
- return d_exprMgr->mkArrayType(*indexSort.d_type, *elemSort.d_type);
+ return Sort(this,
+ d_exprMgr->mkArrayType(*indexSort.d_type, *elemSort.d_type));
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -2852,7 +2889,7 @@ Sort Solver::mkBitVectorSort(uint32_t size) const
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "size > 0";
- return d_exprMgr->mkBitVectorType(size);
+ return Sort(this, d_exprMgr->mkBitVectorType(size));
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -2863,7 +2900,7 @@ Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const
CVC4_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "exponent size > 0";
CVC4_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "significand size > 0";
- return d_exprMgr->mkFloatingPointType(exp, sig);
+ return Sort(this, d_exprMgr->mkFloatingPointType(exp, sig));
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -2874,7 +2911,7 @@ Sort Solver::mkDatatypeSort(DatatypeDecl dtypedecl) const
CVC4_API_ARG_CHECK_EXPECTED(dtypedecl.getNumConstructors() > 0, dtypedecl)
<< "a datatype declaration with at least one constructor";
- return d_exprMgr->mkDatatypeType(*dtypedecl.d_dtype);
+ return Sort(this, d_exprMgr->mkDatatypeType(*dtypedecl.d_dtype));
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -2903,7 +2940,8 @@ Sort Solver::mkFunctionSort(Sort domain, Sort codomain) const
<< "first-class sort as codomain sort for function sort";
Assert(!codomain.isFunction()); /* A function sort is not first-class. */
- return d_exprMgr->mkFunctionType(*domain.d_type, *codomain.d_type);
+ return Sort(this,
+ d_exprMgr->mkFunctionType(*domain.d_type, *codomain.d_type));
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -2929,7 +2967,7 @@ Sort Solver::mkFunctionSort(const std::vector<Sort>& sorts, Sort codomain) const
Assert(!codomain.isFunction()); /* A function sort is not first-class. */
std::vector<Type> argTypes = sortVectorToTypes(sorts);
- return d_exprMgr->mkFunctionType(argTypes, *codomain.d_type);
+ return Sort(this, d_exprMgr->mkFunctionType(argTypes, *codomain.d_type));
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -2937,7 +2975,8 @@ Sort Solver::mkFunctionSort(const std::vector<Sort>& sorts, Sort codomain) const
Sort Solver::mkParamSort(const std::string& symbol) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- return d_exprMgr->mkSort(symbol, ExprManager::SORT_FLAG_PLACEHOLDER);
+ return Sort(this,
+ d_exprMgr->mkSort(symbol, ExprManager::SORT_FLAG_PLACEHOLDER));
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -2957,7 +2996,7 @@ Sort Solver::mkPredicateSort(const std::vector<Sort>& sorts) const
}
std::vector<Type> types = sortVectorToTypes(sorts);
- return d_exprMgr->mkPredicateType(types);
+ return Sort(this, d_exprMgr->mkPredicateType(types));
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -2977,7 +3016,7 @@ Sort Solver::mkRecordSort(
f.emplace_back(p.first, *p.second.d_type);
}
- return d_exprMgr->mkRecordType(Record(f));
+ return Sort(this, d_exprMgr->mkRecordType(Record(f)));
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -2988,7 +3027,7 @@ Sort Solver::mkSetSort(Sort elemSort) const
CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort)
<< "non-null element sort";
- return d_exprMgr->mkSetType(*elemSort.d_type);
+ return Sort(this, d_exprMgr->mkSetType(*elemSort.d_type));
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -2996,7 +3035,7 @@ Sort Solver::mkSetSort(Sort elemSort) const
Sort Solver::mkUninterpretedSort(const std::string& symbol) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- return d_exprMgr->mkSort(symbol);
+ return Sort(this, d_exprMgr->mkSort(symbol));
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -3006,7 +3045,7 @@ Sort Solver::mkSortConstructorSort(const std::string& symbol,
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_ARG_CHECK_EXPECTED(arity > 0, arity) << "an arity > 0";
- return d_exprMgr->mkSortConstructor(symbol, arity);
+ return Sort(this, d_exprMgr->mkSortConstructor(symbol, arity));
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -3025,7 +3064,7 @@ Sort Solver::mkTupleSort(const std::vector<Sort>& sorts) const
}
std::vector<Type> types = sortVectorToTypes(sorts);
- return d_exprMgr->mkTupleType(types);
+ return Sort(this, d_exprMgr->mkTupleType(types));
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -3036,21 +3075,21 @@ Sort Solver::mkTupleSort(const std::vector<Sort>& sorts) const
Term Solver::mkTrue(void) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- return d_exprMgr->mkConst<bool>(true);
+ return Term(this, d_exprMgr->mkConst<bool>(true));
CVC4_API_SOLVER_TRY_CATCH_END;
}
Term Solver::mkFalse(void) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- return d_exprMgr->mkConst<bool>(false);
+ return Term(this, d_exprMgr->mkConst<bool>(false));
CVC4_API_SOLVER_TRY_CATCH_END;
}
Term Solver::mkBoolean(bool val) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- return d_exprMgr->mkConst<bool>(val);
+ return Term(this, d_exprMgr->mkConst<bool>(val));
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -3058,10 +3097,10 @@ Term Solver::mkPi() const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- Term res =
+ Expr res =
d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -3143,10 +3182,10 @@ Term Solver::mkRegexpEmpty() const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- Term res =
+ Expr res =
d_exprMgr->mkExpr(CVC4::kind::REGEXP_EMPTY, std::vector<CVC4::Expr>());
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -3155,10 +3194,10 @@ Term Solver::mkRegexpSigma() const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- Term res =
+ Expr res =
d_exprMgr->mkExpr(CVC4::kind::REGEXP_SIGMA, std::vector<CVC4::Expr>());
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -3179,9 +3218,9 @@ Term Solver::mkSepNil(Sort sort) const
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
- Term res = d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::SEP_NIL);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ Expr res = d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::SEP_NIL);
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -3234,11 +3273,11 @@ Term Solver::mkUniverseSet(Sort sort) const
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
- Term res =
+ Expr res =
d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::UNIVERSE_SET);
// TODO(#2771): Reenable?
- // (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ // (void)res->getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -3381,7 +3420,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 d_exprMgr->mkConst(CVC4::AbstractValue(idx));
+ return Term(this, d_exprMgr->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;
@@ -3392,7 +3431,7 @@ 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 d_exprMgr->mkConst(CVC4::AbstractValue(Integer(index)));
+ return Term(this, d_exprMgr->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;
@@ -3427,10 +3466,10 @@ Term Solver::mkConst(Sort sort, const std::string& symbol) const
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
- Term res = symbol.empty() ? d_exprMgr->mkVar(*sort.d_type)
+ Expr res = symbol.empty() ? d_exprMgr->mkVar(*sort.d_type)
: d_exprMgr->mkVar(symbol, *sort.d_type);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -3443,10 +3482,10 @@ Term Solver::mkVar(Sort sort, const std::string& symbol) const
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
- Term res = symbol.empty() ? d_exprMgr->mkBoundVar(*sort.d_type)
+ Expr res = symbol.empty() ? d_exprMgr->mkBoundVar(*sort.d_type)
: d_exprMgr->mkBoundVar(symbol, *sort.d_type);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -3489,9 +3528,9 @@ Term Solver::mkTerm(Kind kind, Term child) const
CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term";
checkMkTerm(kind, 1);
- Term res = d_exprMgr->mkExpr(extToIntKind(kind), *child.d_expr);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ Expr res = d_exprMgr->mkExpr(extToIntKind(kind), *child.d_expr);
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -3503,10 +3542,10 @@ Term Solver::mkTerm(Kind kind, Term child1, Term child2) const
CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
checkMkTerm(kind, 2);
- Term res =
+ Expr res =
d_exprMgr->mkExpr(extToIntKind(kind), *child1.d_expr, *child2.d_expr);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -3530,7 +3569,7 @@ Term Solver::mkTerm(Op op) const
if (op.isIndexedHelper())
{
const CVC4::Kind int_kind = extToIntKind(op.d_kind);
- res = d_exprMgr->mkExpr(int_kind, *op.d_expr);
+ res = Term(this, d_exprMgr->mkExpr(int_kind, *op.d_expr));
}
else
{
@@ -3549,7 +3588,7 @@ Term Solver::mkTerm(Op op, Term child) const
CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term";
const CVC4::Kind int_kind = extToIntKind(op.d_kind);
- Term res;
+ Expr res;
if (op.isIndexedHelper())
{
res = d_exprMgr->mkExpr(int_kind, *op.d_expr, *child.d_expr);
@@ -3559,8 +3598,8 @@ Term Solver::mkTerm(Op op, Term child) const
res = d_exprMgr->mkExpr(int_kind, *child.d_expr);
}
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -3572,7 +3611,7 @@ Term Solver::mkTerm(Op op, Term child1, Term child2) const
CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
const CVC4::Kind int_kind = extToIntKind(op.d_kind);
- Term res;
+ Expr res;
if (op.isIndexedHelper())
{
res =
@@ -3583,8 +3622,8 @@ Term Solver::mkTerm(Op op, Term child1, Term child2) const
res = d_exprMgr->mkExpr(int_kind, *child1.d_expr, *child2.d_expr);
}
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -3596,7 +3635,7 @@ Term Solver::mkTerm(Op op, Term child1, Term child2, Term child3) const
CVC4_API_ARG_CHECK_EXPECTED(!child3.isNull(), child3) << "non-null term";
const CVC4::Kind int_kind = extToIntKind(op.d_kind);
- Term res;
+ Expr res;
if (op.isIndexedHelper())
{
res = d_exprMgr->mkExpr(
@@ -3608,8 +3647,8 @@ Term Solver::mkTerm(Op op, Term child1, Term child2, Term child3) const
int_kind, *child1.d_expr, *child2.d_expr, *child3.d_expr);
}
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -3626,7 +3665,7 @@ Term Solver::mkTerm(Op op, const std::vector<Term>& children) const
const CVC4::Kind int_kind = extToIntKind(op.d_kind);
std::vector<Expr> echildren = termVectorToExprs(children);
- Term res;
+ Expr res;
if (op.isIndexedHelper())
{
res = d_exprMgr->mkExpr(int_kind, *op.d_expr, echildren);
@@ -3636,8 +3675,8 @@ Term Solver::mkTerm(Op op, const std::vector<Term>& children) const
res = d_exprMgr->mkExpr(int_kind, echildren);
}
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -3656,11 +3695,11 @@ Term Solver::mkTuple(const std::vector<Sort>& sorts,
Sort s = mkTupleSort(sorts);
Datatype dt = s.getDatatype();
- Term res = d_exprMgr->mkExpr(extToIntKind(APPLY_CONSTRUCTOR),
+ Expr res = d_exprMgr->mkExpr(extToIntKind(APPLY_CONSTRUCTOR),
*dt[0].getConstructorTerm().d_expr,
args);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -3673,7 +3712,7 @@ Op Solver::mkOp(Kind kind) const
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_CHECK(s_indexed_kinds.find(kind) == s_indexed_kinds.end())
<< "Expected a kind for a non-indexed operator.";
- return Op(kind);
+ return Op(this, kind);
CVC4_API_SOLVER_TRY_CATCH_END
}
@@ -3687,6 +3726,7 @@ Op Solver::mkOp(Kind kind, const std::string& arg) const
if (kind == RECORD_UPDATE)
{
res = Op(
+ this,
kind,
*mkValHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg)).d_expr.get());
}
@@ -3697,7 +3737,8 @@ Op Solver::mkOp(Kind kind, const std::string& arg) const
* as invalid. */
CVC4_API_ARG_CHECK_EXPECTED(arg != ".", arg)
<< "a string representing an integer, real or rational value.";
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::Divisible>(CVC4::Divisible(CVC4::Integer(arg)))
.d_expr.get());
}
@@ -3716,62 +3757,73 @@ Op Solver::mkOp(Kind kind, uint32_t arg) const
{
case DIVISIBLE:
res =
- Op(kind,
+ Op(this,
+ kind,
*mkValHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_expr.get());
break;
case BITVECTOR_REPEAT:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg))
.d_expr.get());
break;
case BITVECTOR_ZERO_EXTEND:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::BitVectorZeroExtend>(
CVC4::BitVectorZeroExtend(arg))
.d_expr.get());
break;
case BITVECTOR_SIGN_EXTEND:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::BitVectorSignExtend>(
CVC4::BitVectorSignExtend(arg))
.d_expr.get());
break;
case BITVECTOR_ROTATE_LEFT:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::BitVectorRotateLeft>(
CVC4::BitVectorRotateLeft(arg))
.d_expr.get());
break;
case BITVECTOR_ROTATE_RIGHT:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::BitVectorRotateRight>(
CVC4::BitVectorRotateRight(arg))
.d_expr.get());
break;
case INT_TO_BITVECTOR:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg))
.d_expr.get());
break;
case FLOATINGPOINT_TO_UBV:
res = Op(
+ this,
kind,
*mkValHelper<CVC4::FloatingPointToUBV>(CVC4::FloatingPointToUBV(arg))
.d_expr.get());
break;
case FLOATINGPOINT_TO_SBV:
res = Op(
+ this,
kind,
*mkValHelper<CVC4::FloatingPointToSBV>(CVC4::FloatingPointToSBV(arg))
.d_expr.get());
break;
case TUPLE_UPDATE:
res = Op(
+ this,
kind,
*mkValHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg)).d_expr.get());
break;
case REGEXP_REPEAT:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::RegExpRepeat>(CVC4::RegExpRepeat(arg))
.d_expr.get());
break;
@@ -3794,49 +3846,57 @@ Op Solver::mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const
switch (kind)
{
case BITVECTOR_EXTRACT:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::BitVectorExtract>(
CVC4::BitVectorExtract(arg1, arg2))
.d_expr.get());
break;
case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::FloatingPointToFPIEEEBitVector>(
CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2))
.d_expr.get());
break;
case FLOATINGPOINT_TO_FP_FLOATINGPOINT:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::FloatingPointToFPFloatingPoint>(
CVC4::FloatingPointToFPFloatingPoint(arg1, arg2))
.d_expr.get());
break;
case FLOATINGPOINT_TO_FP_REAL:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::FloatingPointToFPReal>(
CVC4::FloatingPointToFPReal(arg1, arg2))
.d_expr.get());
break;
case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::FloatingPointToFPSignedBitVector>(
CVC4::FloatingPointToFPSignedBitVector(arg1, arg2))
.d_expr.get());
break;
case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::FloatingPointToFPUnsignedBitVector>(
CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2))
.d_expr.get());
break;
case FLOATINGPOINT_TO_FP_GENERIC:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::FloatingPointToFPGeneric>(
CVC4::FloatingPointToFPGeneric(arg1, arg2))
.d_expr.get());
break;
case REGEXP_LOOP:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::RegExpLoop>(CVC4::RegExpLoop(arg1, arg2))
.d_expr.get());
break;
@@ -3858,7 +3918,7 @@ Term Solver::simplify(const Term& t)
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_ARG_CHECK_NOT_NULL(t);
- return d_smtEngine->simplify(*t.d_expr);
+ return Term(this, d_smtEngine->simplify(*t.d_expr));
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -3961,7 +4021,7 @@ Sort Solver::declareDatatype(
{
dtdecl.addConstructor(ctor);
}
- return d_exprMgr->mkDatatypeType(*dtdecl.d_dtype);
+ return Sort(this, d_exprMgr->mkDatatypeType(*dtdecl.d_dtype));
}
/**
@@ -3986,7 +4046,7 @@ Term Solver::declareFun(const std::string& symbol,
std::vector<Type> types = sortVectorToTypes(sorts);
type = d_exprMgr->mkFunctionType(types, type);
}
- return d_exprMgr->mkVar(symbol, type);
+ return Term(this, d_exprMgr->mkVar(symbol, type));
}
/**
@@ -3994,8 +4054,8 @@ Term Solver::declareFun(const std::string& symbol,
*/
Sort Solver::declareSort(const std::string& symbol, uint32_t arity) const
{
- if (arity == 0) return d_exprMgr->mkSort(symbol);
- return d_exprMgr->mkSortConstructor(symbol, arity);
+ if (arity == 0) return Sort(this, d_exprMgr->mkSort(symbol));
+ return Sort(this, d_exprMgr->mkSortConstructor(symbol, arity));
}
/**
@@ -4037,7 +4097,7 @@ Term Solver::defineFun(const std::string& symbol,
Expr fun = d_exprMgr->mkVar(symbol, type);
std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
d_smtEngine->defineFunction(fun, ebound_vars, *term.d_expr);
- return fun;
+ return Term(this, fun);
}
Term Solver::defineFun(Term fun,
@@ -4115,7 +4175,7 @@ Term Solver::defineFunRec(const std::string& symbol,
Expr fun = d_exprMgr->mkVar(symbol, type);
std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
d_smtEngine->defineFunctionRec(fun, ebound_vars, *term.d_expr);
- return fun;
+ return Term(this, fun);
}
Term Solver::defineFunRec(Term fun,
@@ -4229,7 +4289,7 @@ std::vector<Term> Solver::getAssertions(void) const
std::vector<Term> res;
for (const Expr& e : assertions)
{
- res.push_back(Term(e));
+ res.push_back(Term(this, e));
}
return res;
}
@@ -4245,7 +4305,7 @@ std::vector<std::pair<Term, Term>> Solver::getAssignment(void) const
std::vector<std::pair<Term, Term>> res;
for (const auto& p : assignment)
{
- res.emplace_back(Term(p.first), Term(p.second));
+ res.emplace_back(Term(this, p.first), Term(this, p.second));
}
return res;
}
@@ -4284,7 +4344,7 @@ std::vector<Term> Solver::getUnsatAssumptions(void) const
std::vector<Term> res;
for (const Expr& e : uassumptions)
{
- res.push_back(Term(e));
+ res.push_back(Term(this, e));
}
return res;
}
@@ -4302,7 +4362,7 @@ std::vector<Term> Solver::getUnsatCore(void) const
std::vector<Term> res;
for (const Expr& e : core)
{
- res.push_back(Term(e));
+ res.push_back(Term(this, e));
}
return res;
}
@@ -4315,7 +4375,7 @@ Term Solver::getValue(Term term) const
// CHECK:
// NodeManager::fromExprManager(d_exprMgr)
// == NodeManager::fromExprManager(expr.getExprManager())
- return d_smtEngine->getValue(*term.d_expr);
+ return Term(this, d_smtEngine->getValue(*term.d_expr));
}
/**
@@ -4331,7 +4391,7 @@ std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const
for (const Term& t : terms)
{
/* Can not use emplace_back here since constructor is private. */
- res.push_back(Term(d_smtEngine->getValue(*t.d_expr)));
+ res.push_back(Term(this, d_smtEngine->getValue(*t.d_expr)));
}
return res;
}
@@ -4471,7 +4531,8 @@ Term Solver::ensureTermSort(const Term& term, const Sort& sort) const
// constructors. We do this cast using division with 1. This has the
// advantage wrt using TO_REAL since (constant) division is always included
// in the theory.
- res = Term(d_exprMgr->mkExpr(extToIntKind(DIVISION),
+ res = Term(this,
+ d_exprMgr->mkExpr(extToIntKind(DIVISION),
*res.d_expr,
d_exprMgr->mkConst(CVC4::Rational(1))));
}
@@ -4489,7 +4550,7 @@ Term Solver::mkSygusVar(Sort sort, const std::string& symbol) const
d_smtEngine->declareSygusVar(symbol, res, *sort.d_type);
- return res;
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -4535,14 +4596,16 @@ Term Solver::synthFun(const std::string& symbol,
Term Solver::synthInv(const std::string& symbol,
const std::vector<Term>& boundVars) const
{
- return synthFunHelper(symbol, boundVars, d_exprMgr->booleanType(), true);
+ return synthFunHelper(
+ symbol, boundVars, Sort(this, d_exprMgr->booleanType()), true);
}
Term Solver::synthInv(const std::string& symbol,
const std::vector<Term>& boundVars,
Grammar& g) const
{
- return synthFunHelper(symbol, boundVars, d_exprMgr->booleanType(), true, &g);
+ return synthFunHelper(
+ symbol, boundVars, Sort(this, d_exprMgr->booleanType()), true, &g);
}
Term Solver::synthFunHelper(const std::string& symbol,
@@ -4586,7 +4649,7 @@ Term Solver::synthFunHelper(const std::string& symbol,
isInv,
termVectorToExprs(boundVars));
- return fun;
+ return Term(this, fun);
CVC4_API_SOLVER_TRY_CATCH_END;
}
@@ -4661,7 +4724,7 @@ Term Solver::getSynthSolution(Term term) const
CVC4_API_CHECK(it != map.cend()) << "Synth solution not found for given term";
- return it->second;
+ return Term(this, it->second);
}
std::vector<Term> Solver::getSynthSolutions(
@@ -4692,7 +4755,7 @@ std::vector<Term> Solver::getSynthSolutions(
CVC4_API_CHECK(it != map.cend())
<< "Synth solution not found for term at index " << i;
- synthSolution.push_back(it->second);
+ synthSolution.push_back(Term(this, it->second));
}
return synthSolution;
@@ -4749,22 +4812,24 @@ std::set<Type> sortSetToTypes(const std::set<Sort>& sorts)
return types;
}
-std::vector<Term> exprVectorToTerms(const std::vector<Expr>& exprs)
+std::vector<Term> exprVectorToTerms(const Solver* slv,
+ const std::vector<Expr>& exprs)
{
std::vector<Term> terms;
for (size_t i = 0, esize = exprs.size(); i < esize; i++)
{
- terms.push_back(Term(exprs[i]));
+ terms.push_back(Term(slv, exprs[i]));
}
return terms;
}
-std::vector<Sort> typeVectorToSorts(const std::vector<Type>& types)
+std::vector<Sort> typeVectorToSorts(const Solver* slv,
+ const std::vector<Type>& types)
{
std::vector<Sort> sorts;
for (size_t i = 0, tsize = types.size(); i < tsize; i++)
{
- sorts.push_back(Sort(types[i]));
+ sorts.push_back(Sort(slv, types[i]));
}
return sorts;
}
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 279453747..87be7b74c 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -49,6 +49,8 @@ class Result;
namespace api {
+class Solver;
+
/* -------------------------------------------------------------------------- */
/* Exception */
/* -------------------------------------------------------------------------- */
@@ -199,10 +201,11 @@ class CVC4_PUBLIC Sort
// migrated to the new API. !!!
/**
* Constructor.
+ * @param slv the associated solver object
* @param t the internal type that is to be wrapped by this sort
* @return the Sort
*/
- Sort(const CVC4::Type& t);
+ Sort(const Solver* slv, const CVC4::Type& t);
/**
* Constructor.
@@ -589,6 +592,11 @@ class CVC4_PUBLIC Sort
bool isNullHelper() const;
/**
+ * The associated solver object.
+ */
+ const Solver* d_solver;
+
+ /**
* The interal type wrapped by this sort.
* This is a shared_ptr rather than a unique_ptr to avoid overhead due to
* memory allocation (CVC4::Type is already ref counted, so this could be
@@ -637,19 +645,21 @@ class CVC4_PUBLIC Op
// migrated to the new API. !!!
/**
* Constructor for a single kind (non-indexed operator).
+ * @param slv the associated solver object
* @param k the kind of this Op
*/
- Op(const Kind k);
+ Op(const Solver* slv, const Kind k);
// !!! 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 e the internal expression that is to be wrapped by this term
* @return the Term
*/
- Op(const Kind k, const CVC4::Expr& e);
+ Op(const Solver* slv, const Kind k, const CVC4::Expr& e);
/**
* Destructor.
@@ -726,6 +736,11 @@ class CVC4_PUBLIC Op
*/
bool isIndexedHelper() const;
+ /**
+ * The associated solver object.
+ */
+ const Solver* d_solver;
+
/* The kind of this operator. */
Kind d_kind;
@@ -758,10 +773,11 @@ class CVC4_PUBLIC Term
// migrated to the new API. !!!
/**
* Constructor.
+ * @param slv the associated solver object
* @param e the internal expression that is to be wrapped by this term
* @return the Term
*/
- Term(const CVC4::Expr& e);
+ Term(const Solver* slv, const CVC4::Expr& e);
/**
* Constructor.
@@ -955,10 +971,13 @@ class CVC4_PUBLIC Term
/**
* Constructor
+ * @param slv the associated solver object
* @param e a shared pointer to the expression that we're iterating over
* @param p the position of the iterator (e.g. which child it's on)
*/
- const_iterator(const std::shared_ptr<CVC4::Expr>& e, uint32_t p);
+ const_iterator(const Solver* slv,
+ const std::shared_ptr<CVC4::Expr>& e,
+ uint32_t p);
/**
* Copy constructor.
@@ -1005,6 +1024,10 @@ class CVC4_PUBLIC Term
Term operator*() const;
private:
+ /**
+ * The associated solver object.
+ */
+ const Solver* d_solver;
/* The original expression to be iterated over */
std::shared_ptr<CVC4::Expr> d_orig_expr;
/* Keeps track of the iteration position */
@@ -1025,6 +1048,12 @@ class CVC4_PUBLIC Term
// to the new API. !!!
CVC4::Expr getExpr(void) const;
+ protected:
+ /**
+ * The associated solver object.
+ */
+ const Solver* d_solver;
+
private:
/**
* Helper for isNull checks. This prevents calling an API function with
@@ -1228,24 +1257,24 @@ class CVC4_PUBLIC DatatypeDecl
private:
/**
* Constructor.
- * @param s the solver that created this datatype declaration
+ * @param slv the solver that created this datatype declaration
* @param name the name of the datatype
* @param isCoDatatype true if a codatatype is to be constructed
* @return the DatatypeDecl
*/
- DatatypeDecl(const Solver* s,
+ DatatypeDecl(const Solver* slv,
const std::string& name,
bool isCoDatatype = false);
/**
* Constructor for parameterized datatype declaration.
* Create sorts parameter with Solver::mkParamSort().
- * @param s the solver that created this datatype declaration
+ * @param slv the solver that created this datatype declaration
* @param name the name of the datatype
* @param param the sort parameter
* @param isCoDatatype true if a codatatype is to be constructed
*/
- DatatypeDecl(const Solver* s,
+ DatatypeDecl(const Solver* slv,
const std::string& name,
Sort param,
bool isCoDatatype = false);
@@ -1253,12 +1282,12 @@ class CVC4_PUBLIC DatatypeDecl
/**
* Constructor for parameterized datatype declaration.
* Create sorts parameter with Solver::mkParamSort().
- * @param s the solver that created this datatype declaration
+ * @param slv the solver that created this datatype declaration
* @param name the name of the datatype
* @param params a list of sort parameters
* @param isCoDatatype true if a codatatype is to be constructed
*/
- DatatypeDecl(const Solver* s,
+ DatatypeDecl(const Solver* slv,
const std::string& name,
const std::vector<Sort>& params,
bool isCoDatatype = false);
@@ -1292,10 +1321,11 @@ class CVC4_PUBLIC DatatypeSelector
// migrated to the new API. !!!
/**
* Constructor.
+ * @param slv the associated solver object
* @param stor the internal datatype selector to be wrapped
* @return the DatatypeSelector
*/
- DatatypeSelector(const CVC4::DatatypeConstructorArg& stor);
+ DatatypeSelector(const Solver* slv, const CVC4::DatatypeConstructorArg& stor);
/**
* Destructor.
@@ -1325,6 +1355,11 @@ class CVC4_PUBLIC DatatypeSelector
private:
/**
+ * The associated solver object.
+ */
+ const Solver* d_solver;
+
+ /**
* The internal datatype selector wrapped by this datatype selector.
* This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is
* not ref counted.
@@ -1353,7 +1388,7 @@ class CVC4_PUBLIC DatatypeConstructor
* @param ctor the internal datatype constructor to be wrapped
* @return the DatatypeConstructor
*/
- DatatypeConstructor(const CVC4::DatatypeConstructor& ctor);
+ DatatypeConstructor(const Solver* slv, const CVC4::DatatypeConstructor& ctor);
/**
* Destructor.
@@ -1466,16 +1501,27 @@ class CVC4_PUBLIC DatatypeConstructor
private:
/**
* Constructor.
+ * @param slv the associated Solver object
* @param ctor the internal datatype constructor to iterate over
* @param true if this is a begin() iterator
*/
- const_iterator(const CVC4::DatatypeConstructor& ctor, bool begin);
+ const_iterator(const Solver* slv,
+ const CVC4::DatatypeConstructor& ctor,
+ bool begin);
+
+ /**
+ * The associated solver object.
+ */
+ const Solver* d_solver;
+
/* A pointer to the list of selectors of the internal datatype
* constructor to iterate over.
* This pointer is maintained for operators == and != only. */
const void* d_int_stors;
+
/* The list of datatype selector (wrappers) to iterate over. */
std::vector<DatatypeSelector> d_stors;
+
/* The current index of the iterator. */
size_t d_idx;
};
@@ -1501,6 +1547,12 @@ class CVC4_PUBLIC DatatypeConstructor
* @return the selector object for the name
*/
DatatypeSelector getSelectorForName(const std::string& name) const;
+
+ /**
+ * The associated solver object.
+ */
+ const Solver* d_solver;
+
/**
* The internal datatype constructor wrapped by this datatype constructor.
* This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is
@@ -1525,7 +1577,7 @@ class CVC4_PUBLIC Datatype
* @param dtype the internal datatype to be wrapped
* @return the Datatype
*/
- Datatype(const CVC4::Datatype& dtype);
+ Datatype(const Solver* slv, const CVC4::Datatype& dtype);
// Nullary constructor for Cython
Datatype();
@@ -1654,16 +1706,25 @@ class CVC4_PUBLIC Datatype
private:
/**
* Constructor.
+ * @param slv the associated Solver object
* @param dtype the internal datatype to iterate over
* @param true if this is a begin() iterator
*/
- const_iterator(const CVC4::Datatype& dtype, bool begin);
+ const_iterator(const Solver* slv, const CVC4::Datatype& dtype, bool begin);
+
+ /**
+ * The associated solver object.
+ */
+ const Solver* d_solver;
+
/* A pointer to the list of constructors of the internal datatype
* to iterate over.
* This pointer is maintained for operators == and != only. */
const void* d_int_ctors;
+
/* The list of datatype constructor (wrappers) to iterate over. */
std::vector<DatatypeConstructor> d_ctors;
+
/* The current index of the iterator. */
size_t d_idx;
};
@@ -1689,6 +1750,12 @@ class CVC4_PUBLIC Datatype
* @return the constructor object for the name
*/
DatatypeConstructor getConstructorForName(const std::string& name) const;
+
+ /**
+ * The associated solver object.
+ */
+ const Solver* d_solver;
+
/**
* The internal datatype wrapped by this datatype.
* This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is
@@ -1793,11 +1860,11 @@ class CVC4_PUBLIC Grammar
private:
/**
* Constructor.
- * @param s the solver that created this grammar
+ * @param slv the solver that created this grammar
* @param sygusVars the input variables to synth-fun/synth-var
* @param ntSymbols the non-terminals of this grammar
*/
- Grammar(const Solver* s,
+ Grammar(const Solver* slv,
const std::vector<Term>& sygusVars,
const std::vector<Term>& ntSymbols);
@@ -1863,7 +1930,7 @@ class CVC4_PUBLIC Grammar
void addSygusConstructorVariables(DatatypeDecl& dt, Sort sort) const;
/** The solver that created this grammar. */
- const Solver* d_s;
+ const Solver* d_solver;
/** Input variables to the corresponding function/invariant to synthesize.*/
std::vector<Term> d_sygusVars;
/** The non-terminal symbols of this grammar. */
@@ -3142,9 +3209,11 @@ class CVC4_PUBLIC Solver
// new API. !!!
std::vector<Expr> termVectorToExprs(const std::vector<Term>& terms);
std::vector<Type> sortVectorToTypes(const std::vector<Sort>& sorts);
-std::vector<Term> exprVectorToTerms(const std::vector<Expr>& terms);
-std::vector<Sort> typeVectorToSorts(const std::vector<Type>& sorts);
std::set<Type> sortSetToTypes(const std::set<Sort>& sorts);
+std::vector<Term> exprVectorToTerms(const Solver* slv,
+ const std::vector<Expr>& terms);
+std::vector<Sort> typeVectorToSorts(const Solver* slv,
+ const std::vector<Type>& sorts);
} // namespace api
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 8e4152e2e..fdb6a081c 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1159,7 +1159,7 @@ declareVariables[std::unique_ptr<CVC4::Command>* cmd, CVC4::api::Sort& t,
PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE);
api::Term func = PARSER_STATE->mkVar(
*i,
- t.getType(),
+ api::Sort(PARSER_STATE->getSolver(), t.getType()),
ExprManager::VAR_FLAG_GLOBAL | ExprManager::VAR_FLAG_DEFINED);
PARSER_STATE->defineVar(*i, f);
Command* decl =
@@ -1654,7 +1654,9 @@ tupleStore[CVC4::api::Term& f]
}
const Datatype & dt = ((DatatypeType)t.getType()).getDatatype();
f2 = SOLVER->mkTerm(
- api::APPLY_SELECTOR, api::Term(dt[0][k].getSelector()), f);
+ api::APPLY_SELECTOR,
+ api::Term(PARSER_STATE->getSolver(), dt[0][k].getSelector()),
+ f);
}
( ( arrayStore[f2]
| DOT ( tupleStore[f2]
@@ -1687,7 +1689,9 @@ recordStore[CVC4::api::Term& f]
}
const Datatype & dt = ((DatatypeType)t.getType()).getDatatype();
f2 = SOLVER->mkTerm(
- api::APPLY_SELECTOR, api::Term(dt[0][id].getSelector()), f);
+ api::APPLY_SELECTOR,
+ api::Term(PARSER_STATE->getSolver(), dt[0][id].getSelector()),
+ f);
}
( ( arrayStore[f2]
| DOT ( tupleStore[f2]
@@ -1831,7 +1835,10 @@ postfixTerm[CVC4::api::Term& f]
PARSER_STATE->parseError(std::string("no such field `") + id + "' in record");
}
const Datatype & dt = ((DatatypeType)type.getType()).getDatatype();
- f = SOLVER->mkTerm(api::APPLY_SELECTOR,api::Term(dt[0][id].getSelector()), f);
+ f = SOLVER->mkTerm(
+ api::APPLY_SELECTOR,
+ api::Term(PARSER_STATE->getSolver(), dt[0][id].getSelector()),
+ f);
}
| k=numeral
{
@@ -1846,7 +1853,10 @@ postfixTerm[CVC4::api::Term& f]
PARSER_STATE->parseError(ss.str());
}
const Datatype & dt = ((DatatypeType)type.getType()).getDatatype();
- f = SOLVER->mkTerm(api::APPLY_SELECTOR,api::Term(dt[0][k].getSelector()), f);
+ f = SOLVER->mkTerm(
+ api::APPLY_SELECTOR,
+ api::Term(PARSER_STATE->getSolver(), dt[0][k].getSelector()),
+ f);
}
)
)*
@@ -1857,7 +1867,7 @@ postfixTerm[CVC4::api::Term& f]
| ABS_TOK LPAREN formula[f] RPAREN
{ f = MK_TERM(CVC4::api::ABS, f); }
| DIVISIBLE_TOK LPAREN formula[f] COMMA n=numeral RPAREN
- { f = MK_TERM(SOLVER->mkOp(CVC4::api::DIVISIBLE,n), f); }
+ { f = MK_TERM(SOLVER->mkOp(CVC4::api::DIVISIBLE, n), f); }
| DISTINCT_TOK LPAREN
formula[f] { args.push_back(f); }
( COMMA formula[f] { args.push_back(f); } )* RPAREN
@@ -1868,7 +1878,7 @@ postfixTerm[CVC4::api::Term& f]
)
( typeAscription[f, t]
{
- f = PARSER_STATE->applyTypeAscription(f,t).getExpr();
+ f = PARSER_STATE->applyTypeAscription(f,t);
}
)?
;
@@ -1885,8 +1895,9 @@ relationTerm[CVC4::api::Term& f]
args.push_back(f);
types.push_back(f.getSort());
api::Sort t = SOLVER->mkTupleSort(types);
- const Datatype& dt = ((DatatypeType)t.getType()).getDatatype();
- args.insert( args.begin(), api::Term(dt[0].getConstructor()) );
+ const Datatype& dt = Datatype(((DatatypeType)t.getType()).getDatatype());
+ args.insert(args.begin(),
+ api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
f = MK_TERM(api::APPLY_CONSTRUCTOR, args);
}
| IDEN_TOK LPAREN formula[f] RPAREN
@@ -2136,7 +2147,9 @@ simpleTerm[CVC4::api::Term& f]
}
api::Sort dtype = SOLVER->mkTupleSort(types);
const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype();
- args.insert( args.begin(), dt[0].getConstructor() );
+ args.insert(
+ args.begin(),
+ api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
f = MK_TERM(api::APPLY_CONSTRUCTOR, args);
}
}
@@ -2146,7 +2159,9 @@ simpleTerm[CVC4::api::Term& f]
{ std::vector<api::Sort> types;
api::Sort dtype = SOLVER->mkTupleSort(types);
const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype();
- f = MK_TERM(api::APPLY_CONSTRUCTOR, api::Term(dt[0].getConstructor())); }
+ f = MK_TERM(api::APPLY_CONSTRUCTOR,
+ api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
+ }
/* empty record literal */
| PARENHASH HASHPAREN
@@ -2154,7 +2169,8 @@ simpleTerm[CVC4::api::Term& f]
api::Sort dtype = SOLVER->mkRecordSort(
std::vector<std::pair<std::string, api::Sort>>());
const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype();
- f = MK_TERM(api::APPLY_CONSTRUCTOR, api::Term(dt[0].getConstructor()));
+ f = MK_TERM(api::APPLY_CONSTRUCTOR,
+ api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
}
/* empty set literal */
| LBRACE RBRACE
@@ -2252,7 +2268,8 @@ simpleTerm[CVC4::api::Term& f]
}
api::Sort dtype = SOLVER->mkRecordSort(typeIds);
const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype();
- args.insert( args.begin(), dt[0].getConstructor() );
+ args.insert(args.begin(),
+ api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
f = MK_TERM(api::APPLY_CONSTRUCTOR, args);
}
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index c860d14c7..b24f9ae9d 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -82,14 +82,9 @@ api::Term Parser::getSymbol(const std::string& name, SymbolType type)
{
checkDeclaration(name, CHECK_DECLARED, type);
assert(isDeclared(name, type));
-
- if (type == SYM_VARIABLE) {
- // Functions share var namespace
- return d_symtab->lookup(name);
- }
-
- assert(false); // Unhandled(type);
- return Expr();
+ assert(type == SYM_VARIABLE);
+ // Functions share var namespace
+ return api::Term(d_solver, d_symtab->lookup(name));
}
api::Term Parser::getVariable(const std::string& name)
@@ -166,7 +161,7 @@ api::Sort Parser::getSort(const std::string& name)
{
checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
assert(isDeclared(name, SYM_SORT));
- api::Sort t = api::Sort(d_symtab->lookupType(name));
+ api::Sort t = api::Sort(d_solver, d_symtab->lookupType(name));
return t;
}
@@ -175,8 +170,8 @@ api::Sort Parser::getSort(const std::string& name,
{
checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
assert(isDeclared(name, SYM_SORT));
- api::Sort t =
- api::Sort(d_symtab->lookupType(name, api::sortVectorToTypes(params)));
+ api::Sort t = api::Sort(
+ d_solver, d_symtab->lookupType(name, api::sortVectorToTypes(params)));
return t;
}
@@ -237,7 +232,8 @@ std::vector<api::Term> Parser::bindBoundVars(
std::vector<api::Term> vars;
for (std::pair<std::string, api::Sort>& i : sortedVarNames)
{
- vars.push_back(bindBoundVar(i.first, i.second.getType()));
+ vars.push_back(
+ bindBoundVar(i.first, api::Sort(d_solver, i.second.getType())));
}
return vars;
}
@@ -251,7 +247,7 @@ api::Term Parser::mkAnonymousFunction(const std::string& prefix,
}
stringstream name;
name << prefix << "_anon_" << ++d_anonymousFunctionCount;
- return mkVar(name.str(), type.getType(), flags);
+ return mkVar(name.str(), api::Sort(d_solver, type.getType()), flags);
}
std::vector<api::Term> Parser::bindVars(const std::vector<std::string> names,
@@ -334,7 +330,8 @@ void Parser::defineParameterizedType(const std::string& name,
api::Sort Parser::mkSort(const std::string& name, uint32_t flags)
{
Debug("parser") << "newSort(" << name << ")" << std::endl;
- api::Sort type = d_solver->getExprManager()->mkSort(name, flags);
+ api::Sort type =
+ api::Sort(d_solver, d_solver->getExprManager()->mkSort(name, flags));
defineType(
name,
type,
@@ -348,8 +345,9 @@ api::Sort Parser::mkSortConstructor(const std::string& name,
{
Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")"
<< std::endl;
- api::Sort type =
- d_solver->getExprManager()->mkSortConstructor(name, arity, flags);
+ api::Sort type = api::Sort(
+ d_solver,
+ d_solver->getExprManager()->mkSortConstructor(name, arity, flags));
defineType(
name,
vector<api::Sort>(arity),
@@ -379,8 +377,10 @@ api::Sort Parser::mkUnresolvedTypeConstructor(
{
Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size()
<< ")" << std::endl;
- api::Sort unresolved = d_solver->getExprManager()->mkSortConstructor(
- name, params.size(), ExprManager::SORT_FLAG_PLACEHOLDER);
+ api::Sort unresolved =
+ api::Sort(d_solver,
+ d_solver->getExprManager()->mkSortConstructor(
+ name, params.size(), ExprManager::SORT_FLAG_PLACEHOLDER));
defineType(name, params, unresolved);
api::Sort t = getSort(name, params);
d_unresolved.insert(unresolved);
@@ -588,11 +588,12 @@ api::Term Parser::applyTypeAscription(api::Term t, api::Sort s)
Expr e = t.getExpr();
const DatatypeConstructor& dtc =
Datatype::datatypeOf(e)[Datatype::indexOf(e)];
- t = api::Term(em->mkExpr(
- kind::APPLY_TYPE_ASCRIPTION,
- em->mkConst(
- AscriptionType(dtc.getSpecializedConstructorType(s.getType()))),
- e));
+ t = api::Term(
+ d_solver,
+ em->mkExpr(kind::APPLY_TYPE_ASCRIPTION,
+ em->mkConst(AscriptionType(
+ dtc.getSpecializedConstructorType(s.getType()))),
+ e));
}
// the type of t does not match the sort s by design (constructor type
// vs datatype type), thus we use an alternative check here.
@@ -624,7 +625,7 @@ api::Term Parser::mkVar(const std::string& name,
uint32_t flags)
{
return api::Term(
- d_solver->getExprManager()->mkVar(name, type.getType(), flags));
+ d_solver, d_solver->getExprManager()->mkVar(name, type.getType(), flags));
}
//!!!!!!!!!!! temporary
@@ -892,16 +893,16 @@ std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s)
return str;
}
-Expr Parser::mkStringConstant(const std::string& s)
+api::Term Parser::mkStringConstant(const std::string& s)
{
ExprManager* em = d_solver->getExprManager();
if (language::isInputLang_smt2_6(em->getOptions().getInputLanguage()))
{
- return d_solver->mkString(s, true).getExpr();
+ return api::Term(d_solver, d_solver->mkString(s, true).getExpr());
}
// otherwise, we must process ad-hoc escape sequences
std::vector<unsigned> str = processAdHocStringEsc(s);
- return d_solver->mkString(str).getExpr();
+ return api::Term(d_solver, d_solver->mkString(str).getExpr());
}
} /* CVC4::parser namespace */
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 7941cfdd5..b5dc83902 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -808,7 +808,7 @@ public:
inline SymbolTable* getSymbolTable() const {
return d_symtab;
}
-
+
//------------------------ operator overloading
/** is this function overloaded? */
bool isOverloadedFunction(api::Term fun)
@@ -822,7 +822,8 @@ public:
*/
api::Term getOverloadedConstantForType(const std::string& name, api::Sort t)
{
- return d_symtab->getOverloadedConstantForType(name, t.getType());
+ return api::Term(d_solver,
+ d_symtab->getOverloadedConstantForType(name, t.getType()));
}
/**
@@ -833,8 +834,9 @@ public:
api::Term getOverloadedFunctionForTypes(const std::string& name,
std::vector<api::Sort>& argTypes)
{
- return d_symtab->getOverloadedFunctionForTypes(
- name, api::sortVectorToTypes(argTypes));
+ return api::Term(d_solver,
+ d_symtab->getOverloadedFunctionForTypes(
+ name, api::sortVectorToTypes(argTypes)));
}
//------------------------ end operator overloading
/**
@@ -845,7 +847,7 @@ public:
* SMT-LIB 2.6 or higher), or otherwise calling the solver to construct
* the string.
*/
- Expr mkStringConstant(const std::string& s);
+ api::Term mkStringConstant(const std::string& s);
private:
/** ad-hoc string escaping
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 95f4b1a67..081990a45 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -101,7 +101,7 @@ namespace CVC4 {
struct myExpr : public CVC4::api::Term {
myExpr() : CVC4::api::Term() {}
myExpr(void*) : CVC4::api::Term() {}
- myExpr(const Expr& e) : CVC4::api::Term(e) {}
+ myExpr(const Expr& e) : CVC4::api::Term(d_solver, e) {}
myExpr(const myExpr& e) : CVC4::api::Term(e) {}
};/* struct myExpr */
}/* CVC4::parser::smt2 namespace */
@@ -286,7 +286,7 @@ command [std::unique_ptr<CVC4::Command>* cmd]
{ PARSER_STATE->popScope();
// Do NOT call mkSort, since that creates a new sort!
// This name is not its own distinct sort, it's an alias.
- PARSER_STATE->defineParameterizedType(name, sorts, t.getType());
+ PARSER_STATE->defineParameterizedType(name, sorts, t);
cmd->reset(new DefineTypeCommand(
name, api::sortVectorToTypes(sorts), t.getType()));
}
@@ -800,7 +800,7 @@ sygusGrammarV1[CVC4::api::Sort & ret,
PARSER_STATE->getUnresolvedSorts().clear();
- ret = datatypeTypes[0];
+ ret = api::Sort(PARSER_STATE->getSolver(), datatypeTypes[0]);
};
// SyGuS grammar term.
@@ -893,7 +893,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun]
<< "expression " << atomTerm << std::endl;
std::stringstream ss;
ss << atomTerm;
- sgt.d_op.d_expr = atomTerm.getExpr();
+ sgt.d_op.d_expr = atomTerm;
sgt.d_name = ss.str();
sgt.d_gterm_type = SygusGTerm::gterm_op;
}
@@ -1791,8 +1791,10 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2]
Expr ef = f.getExpr();
if (Datatype::datatypeOf(ef).isParametric())
{
- type = Datatype::datatypeOf(ef)[Datatype::indexOf(ef)]
- .getSpecializedConstructorType(expr.getSort().getType());
+ type = api::Sort(
+ PARSER_STATE->getSolver(),
+ Datatype::datatypeOf(ef)[Datatype::indexOf(ef)]
+ .getSpecializedConstructorType(expr.getSort().getType()));
}
argTypes = type.getConstructorDomainSorts();
}
@@ -1914,10 +1916,10 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2]
sorts.emplace_back(arg.getSort());
terms.emplace_back(arg);
}
- expr = SOLVER->mkTuple(sorts, terms).getExpr();
+ expr = SOLVER->mkTuple(sorts, terms);
}
| /* an atomic term (a term with no subterms) */
- termAtomic[atomTerm] { expr = atomTerm.getExpr(); }
+ termAtomic[atomTerm] { expr = atomTerm; }
;
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 9ca2194f4..608e47a6b 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1377,7 +1377,7 @@ void Smt2::mkSygusDatatype(api::DatatypeDecl& dt,
if( std::find( types.begin(), types.end(), t )==types.end() ){
types.push_back( t );
//identity element
- api::Sort bt = dt.getDatatype().getSygusType();
+ api::Sort bt = api::Sort(d_solver, dt.getDatatype().getSygusType());
Debug("parser-sygus") << ": make identity function for " << bt << ", argument type " << t << std::endl;
std::stringstream ss;
@@ -1481,7 +1481,7 @@ api::Term Smt2::purifySygusGTerm(api::Term term,
api::Term ret = d_solver->mkVar(term.getSort());
Trace("parser-sygus2-debug")
<< "...unresolved non-terminal, intro " << ret << std::endl;
- args.push_back(ret.getExpr());
+ args.push_back(api::Term(d_solver, ret.getExpr()));
cargs.push_back(itn->second);
return ret;
}
@@ -1571,8 +1571,7 @@ void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type)
Trace("parser-qid") << " " << p.d_expr.getKind() << " " << p.d_expr.getSort();
Trace("parser-qid") << std::endl;
// otherwise, we process the type ascription
- p.d_expr =
- applyTypeAscription(api::Term(p.d_expr), api::Sort(type)).getExpr();
+ p.d_expr = applyTypeAscription(p.d_expr, type);
}
api::Term Smt2::parseOpToExpr(ParseOp& p)
@@ -1776,8 +1775,10 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
parseError(ss.str());
}
const Datatype& dt = ((DatatypeType)t.getType()).getDatatype();
- api::Term ret = d_solver->mkTerm(
- api::APPLY_SELECTOR, api::Term(dt[0][n].getSelector()), args[0]);
+ api::Term ret =
+ d_solver->mkTerm(api::APPLY_SELECTOR,
+ api::Term(d_solver, dt[0][n].getSelector()),
+ args[0]);
Debug("parser") << "applyParseOp: return selector " << ret << std::endl;
return ret;
}
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index c2f4675b1..c1d60ca31 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -1441,7 +1441,7 @@ tffLetTermBinding[std::vector<CVC4::api::Term> & bvlist,
PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, false);
std::vector<api::Term> lchildren(++lhs.begin(), lhs.end());
rhs = MK_TERM(api::LAMBDA, MK_TERM(api::BOUND_VAR_LIST, lchildren), rhs);
- lhs = api::Term(lhs.getExpr().getOperator());
+ lhs = api::Term(PARSER_STATE->getSolver(), lhs.getExpr().getOperator());
}
| LPAREN_TOK tffLetTermBinding[bvlist, lhs, rhs] RPAREN_TOK
;
@@ -1463,7 +1463,7 @@ tffLetFormulaBinding[std::vector<CVC4::api::Term> & bvlist,
PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, true);
std::vector<api::Term> lchildren(++lhs.begin(), lhs.end());
rhs = MK_TERM(api::LAMBDA, MK_TERM(api::BOUND_VAR_LIST, lchildren), rhs);
- lhs = api::Term(lhs.getExpr().getOperator());
+ lhs = api::Term(PARSER_STATE->getSolver(), lhs.getExpr().getOperator());
}
| LPAREN_TOK tffLetFormulaBinding[bvlist, lhs, rhs] RPAREN_TOK
;
diff --git a/test/unit/api/op_black.h b/test/unit/api/op_black.h
index e99e8daf2..27ca7bb88 100644
--- a/test/unit/api/op_black.h
+++ b/test/unit/api/op_black.h
@@ -52,7 +52,7 @@ void OpBlack::testIsNull()
void OpBlack::testOpFromKind()
{
- Op plus(PLUS);
+ Op plus(&d_solver, PLUS);
TS_ASSERT(!plus.isIndexed());
TS_ASSERT_THROWS(plus.getIndices<uint32_t>(), CVC4ApiException&);
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 07b5c5aec..90d4c10c1 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -978,13 +978,13 @@ void SolverBlack::testGetOp()
Term listhead = d_solver->mkTerm(APPLY_SELECTOR, headTerm, listcons1);
TS_ASSERT(listnil.hasOp());
- TS_ASSERT_EQUALS(listnil.getOp(), APPLY_CONSTRUCTOR);
+ TS_ASSERT_EQUALS(listnil.getOp(), Op(d_solver.get(), APPLY_CONSTRUCTOR));
TS_ASSERT(listcons1.hasOp());
- TS_ASSERT_EQUALS(listcons1.getOp(), APPLY_CONSTRUCTOR);
+ TS_ASSERT_EQUALS(listcons1.getOp(), Op(d_solver.get(), APPLY_CONSTRUCTOR));
TS_ASSERT(listhead.hasOp());
- TS_ASSERT_EQUALS(listhead.getOp(), APPLY_SELECTOR);
+ TS_ASSERT_EQUALS(listhead.getOp(), Op(d_solver.get(), APPLY_SELECTOR));
}
void SolverBlack::testPush1()
diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h
index 78d6ee5cc..d8f022201 100644
--- a/test/unit/api/term_black.h
+++ b/test/unit/api/term_black.h
@@ -175,10 +175,10 @@ void TermBlack::testGetOp()
Term extb = d_solver.mkTerm(ext, b);
TS_ASSERT(ab.hasOp());
- TS_ASSERT_EQUALS(ab.getOp(), Op(SELECT));
+ TS_ASSERT_EQUALS(ab.getOp(), Op(&d_solver, SELECT));
TS_ASSERT(!ab.getOp().isIndexed());
// can compare directly to a Kind (will invoke Op constructor)
- TS_ASSERT_EQUALS(ab.getOp(), SELECT);
+ TS_ASSERT_EQUALS(ab.getOp(), Op(&d_solver, SELECT));
TS_ASSERT(extb.hasOp());
TS_ASSERT(extb.getOp().isIndexed());
TS_ASSERT_EQUALS(extb.getOp(), ext);
@@ -189,7 +189,7 @@ void TermBlack::testGetOp()
TS_ASSERT(!f.hasOp());
TS_ASSERT_THROWS(f.getOp(), CVC4ApiException&);
TS_ASSERT(fx.hasOp());
- TS_ASSERT_EQUALS(fx.getOp(), APPLY_UF);
+ TS_ASSERT_EQUALS(fx.getOp(), Op(&d_solver, APPLY_UF));
std::vector<Term> children(fx.begin(), fx.end());
// testing rebuild from op and children
TS_ASSERT_EQUALS(fx, d_solver.mkTerm(fx.getOp(), children));
@@ -225,10 +225,10 @@ void TermBlack::testGetOp()
TS_ASSERT(headTerm.hasOp());
TS_ASSERT(tailTerm.hasOp());
- TS_ASSERT_EQUALS(nilTerm.getOp(), APPLY_CONSTRUCTOR);
- TS_ASSERT_EQUALS(consTerm.getOp(), APPLY_CONSTRUCTOR);
- TS_ASSERT_EQUALS(headTerm.getOp(), APPLY_SELECTOR);
- TS_ASSERT_EQUALS(tailTerm.getOp(), APPLY_SELECTOR);
+ TS_ASSERT_EQUALS(nilTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
+ TS_ASSERT_EQUALS(consTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
+ TS_ASSERT_EQUALS(headTerm.getOp(), Op(&d_solver, APPLY_SELECTOR));
+ TS_ASSERT_EQUALS(tailTerm.getOp(), Op(&d_solver, APPLY_SELECTOR));
// Test rebuilding
children.clear();
diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h
index 44bb9293b..2962439ff 100644
--- a/test/unit/parser/parser_builder_black.h
+++ b/test/unit/parser/parser_builder_black.h
@@ -111,7 +111,7 @@ class ParserBuilderBlack : public CxxTest::TestSuite
TS_ASSERT(parser != NULL);
api::Term e = parser->nextExpression();
- TS_ASSERT_EQUALS(e, d_solver->getExprManager()->mkConst(true));
+ TS_ASSERT_EQUALS(e, d_solver->mkTrue());
e = parser->nextExpression();
TS_ASSERT(e.isNull());
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback