From 50edf184492d20f4acb7b8d82f3843f3146f77d5 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 2 Jun 2020 09:09:15 -0700 Subject: [PATCH] New C++ API: Keep reference to solver object in non-solver objects. (#4549) This is in preparation for adding guards to ensure that sort and term arguments belong to the same solver. --- src/api/cvc4cpp.cpp | 545 +++++++++++++----------- src/api/cvc4cpp.h | 111 ++++- src/parser/cvc/Cvc.g | 43 +- src/parser/parser.cpp | 55 +-- src/parser/parser.h | 12 +- src/parser/smt2/Smt2.g | 18 +- src/parser/smt2/smt2.cpp | 13 +- src/parser/tptp/Tptp.g | 4 +- test/unit/api/op_black.h | 2 +- test/unit/api/solver_black.h | 6 +- test/unit/api/term_black.h | 14 +- test/unit/parser/parser_builder_black.h | 2 +- 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& params) const @@ -923,10 +928,10 @@ Sort Sort::instantiate(const std::vector& 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::getConstructorDomainSorts() const { CVC4_API_CHECK(isConstructor()) << "Not a function sort."; std::vector 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::getFunctionDomainSorts() const { CVC4_API_CHECK(isFunction()) << "Not a function sort."; std::vector 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::getUninterpretedSortParamSorts() const { CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort."; std::vector types = SortType(*d_type).getParamTypes(); - return typeVectorToSorts(types); + return typeVectorToSorts(d_solver, types); } /* Sort constructor sort ----------------------------------------------- */ @@ -1062,7 +1067,7 @@ std::vector Sort::getDatatypeParamSorts() const { CVC4_API_CHECK(isParametricDatatype()) << "Not a parametric datatype sort."; std::vector 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::getTupleSorts() const { CVC4_API_CHECK(isTuple()) << "Not a tuple sort."; std::vector 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 es, @@ -1424,8 +1434,9 @@ Term Term::substitute(const std::vector 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& e, +Term::const_iterator::const_iterator(const Solver* slv, + const std::shared_ptr& 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{*param.d_type}, isCoDatatype)) { } -DatatypeDecl::DatatypeDecl(const Solver* s, +DatatypeDecl::DatatypeDecl(const Solver* slv, const std::string& name, const std::vector& params, bool isCoDatatype) @@ -1818,7 +1833,7 @@ DatatypeDecl::DatatypeDecl(const Solver* s, tparams.push_back(*p.d_type); } d_dtype = std::shared_ptr( - 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* sels = static_cast*>( 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* cons = static_cast*>(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& sygusVars, const std::vector& 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 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 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 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 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& 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& 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 Solver::mkDatatypeSortsInternal( std::vector 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& sorts, Sort codomain) const Assert(!codomain.isFunction()); /* A function sort is not first-class. */ std::vector 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& 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& sorts) const } std::vector 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& sorts) const } std::vector 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& sorts) const Term Solver::mkTrue(void) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return d_exprMgr->mkConst(true); + return Term(this, d_exprMgr->mkConst(true)); CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkFalse(void) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return d_exprMgr->mkConst(false); + return Term(this, d_exprMgr->mkConst(false)); CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkBoolean(bool val) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return d_exprMgr->mkConst(val); + return Term(this, d_exprMgr->mkConst(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()); - (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()); - (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& children) const const CVC4::Kind int_kind = extToIntKind(op.d_kind); std::vector 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& 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& 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(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::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(arg)).d_expr.get()); break; case BITVECTOR_REPEAT: - res = Op(kind, + res = Op(this, + kind, *mkValHelper(CVC4::BitVectorRepeat(arg)) .d_expr.get()); break; case BITVECTOR_ZERO_EXTEND: - res = Op(kind, + res = Op(this, + kind, *mkValHelper( CVC4::BitVectorZeroExtend(arg)) .d_expr.get()); break; case BITVECTOR_SIGN_EXTEND: - res = Op(kind, + res = Op(this, + kind, *mkValHelper( CVC4::BitVectorSignExtend(arg)) .d_expr.get()); break; case BITVECTOR_ROTATE_LEFT: - res = Op(kind, + res = Op(this, + kind, *mkValHelper( CVC4::BitVectorRotateLeft(arg)) .d_expr.get()); break; case BITVECTOR_ROTATE_RIGHT: - res = Op(kind, + res = Op(this, + kind, *mkValHelper( CVC4::BitVectorRotateRight(arg)) .d_expr.get()); break; case INT_TO_BITVECTOR: - res = Op(kind, + res = Op(this, + kind, *mkValHelper(CVC4::IntToBitVector(arg)) .d_expr.get()); break; case FLOATINGPOINT_TO_UBV: res = Op( + this, kind, *mkValHelper(CVC4::FloatingPointToUBV(arg)) .d_expr.get()); break; case FLOATINGPOINT_TO_SBV: res = Op( + this, kind, *mkValHelper(CVC4::FloatingPointToSBV(arg)) .d_expr.get()); break; case TUPLE_UPDATE: res = Op( + this, kind, *mkValHelper(CVC4::TupleUpdate(arg)).d_expr.get()); break; case REGEXP_REPEAT: - res = Op(kind, + res = Op(this, + kind, *mkValHelper(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(arg1, arg2)) .d_expr.get()); break; case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: - res = Op(kind, + res = Op(this, + kind, *mkValHelper( CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2)) .d_expr.get()); break; case FLOATINGPOINT_TO_FP_FLOATINGPOINT: - res = Op(kind, + res = Op(this, + kind, *mkValHelper( CVC4::FloatingPointToFPFloatingPoint(arg1, arg2)) .d_expr.get()); break; case FLOATINGPOINT_TO_FP_REAL: - res = Op(kind, + res = Op(this, + kind, *mkValHelper( CVC4::FloatingPointToFPReal(arg1, arg2)) .d_expr.get()); break; case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: - res = Op(kind, + res = Op(this, + kind, *mkValHelper( CVC4::FloatingPointToFPSignedBitVector(arg1, arg2)) .d_expr.get()); break; case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: - res = Op(kind, + res = Op(this, + kind, *mkValHelper( CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2)) .d_expr.get()); break; case FLOATINGPOINT_TO_FP_GENERIC: - res = Op(kind, + res = Op(this, + kind, *mkValHelper( CVC4::FloatingPointToFPGeneric(arg1, arg2)) .d_expr.get()); break; case REGEXP_LOOP: - res = Op(kind, + res = Op(this, + kind, *mkValHelper(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 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 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 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 Solver::getAssertions(void) const std::vector 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> Solver::getAssignment(void) const std::vector> 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 Solver::getUnsatAssumptions(void) const std::vector 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 Solver::getUnsatCore(void) const std::vector 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 Solver::getValue(const std::vector& 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& 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& 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 Solver::getSynthSolutions( @@ -4692,7 +4755,7 @@ std::vector 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 sortSetToTypes(const std::set& sorts) return types; } -std::vector exprVectorToTerms(const std::vector& exprs) +std::vector exprVectorToTerms(const Solver* slv, + const std::vector& exprs) { std::vector 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 typeVectorToSorts(const std::vector& types) +std::vector typeVectorToSorts(const Solver* slv, + const std::vector& types) { std::vector 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. @@ -588,6 +591,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 @@ -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& e, uint32_t p); + const_iterator(const Solver* slv, + const std::shared_ptr& 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 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& 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. @@ -1324,6 +1354,11 @@ class CVC4_PUBLIC DatatypeSelector CVC4::DatatypeConstructorArg getDatatypeConstructorArg(void) const; 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 @@ -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 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 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& sygusVars, const std::vector& 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 d_sygusVars; /** The non-terminal symbols of this grammar. */ @@ -3142,9 +3209,11 @@ class CVC4_PUBLIC Solver // new API. !!! std::vector termVectorToExprs(const std::vector& terms); std::vector sortVectorToTypes(const std::vector& sorts); -std::vector exprVectorToTerms(const std::vector& terms); -std::vector typeVectorToSorts(const std::vector& sorts); std::set sortSetToTypes(const std::set& sorts); +std::vector exprVectorToTerms(const Solver* slv, + const std::vector& terms); +std::vector typeVectorToSorts(const Solver* slv, + const std::vector& 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* 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 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>()); 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 Parser::bindBoundVars( std::vector vars; for (std::pair& 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 Parser::bindVars(const std::vector 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(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 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 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& 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* 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& 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 & bvlist, PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, false); std::vector 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 & bvlist, PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, true); std::vector 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(), 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 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()); -- 2.30.2