diff options
Diffstat (limited to 'src/api/cvc4cpp.cpp')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 545 |
1 files changed, 305 insertions, 240 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; } |