From: Andrew Reynolds Date: Wed, 26 Aug 2020 00:04:39 +0000 (-0500) Subject: Replace Expr-level datatype with Node-level DType (#4875) X-Git-Tag: cvc5-1.0.0~2955 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=34eac85599875517732d53a5cc1acd3ab60479d1;p=cvc5.git Replace Expr-level datatype with Node-level DType (#4875) This PR makes two simultaneous changes: The new API uses Node-level DType instead of Expr-level Datatype. This required converting 2 of the last remaining calls in the parser that used Expr to use the new API. Internally constructed datatypes (e.g. for sygus) use Node-level DType instead of Expr-level Datatype. Note this required moving a block of code for handling a corner case of sygus from Datatype -> DType. This PR removes : ExprManger::mkDatatypeType. The Expr-level datatype itself. This PR removes all references to its include file. It also updates one remaining unit test from Expr -> Node. This PR will enable further removal of other datatype-specific things in the Expr layer. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index f6c5187c7..c55c29ed4 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1032,7 +1032,6 @@ install(FILES expr/array.h expr/array_store_all.h expr/ascription_type.h - expr/datatype.h expr/emptyset.h expr/expr_iomanip.h expr/record.h diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 150f84301..0a35981d2 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -38,6 +38,7 @@ #include "base/check.h" #include "base/configuration.h" +#include "expr/dtype.h" #include "expr/expr.h" #include "expr/expr_manager.h" #include "expr/expr_manager_scope.h" @@ -927,7 +928,7 @@ bool Sort::isDatatype() const { return d_type->isDatatype(); } bool Sort::isParametricDatatype() const { if (!d_type->isDatatype()) return false; - return DatatypeType(*d_type).isParametric(); + return TypeNode::fromType(*d_type).isParametricDatatype(); } bool Sort::isConstructor() const { return d_type->isConstructor(); } @@ -965,25 +966,33 @@ bool Sort::isComparableTo(Sort s) const Datatype Sort::getDatatype() const { + NodeManagerScope scope(d_solver->getNodeManager()); CVC4_API_CHECK(isDatatype()) << "Expected datatype sort."; - return Datatype(d_solver, DatatypeType(*d_type).getDatatype()); + return Datatype(d_solver, TypeNode::fromType(*d_type).getDType()); } Sort Sort::instantiate(const std::vector& params) const { + NodeManagerScope scope(d_solver->getNodeManager()); CVC4_API_CHECK(isParametricDatatype() || isSortConstructor()) << "Expected parametric datatype or sort constructor sort."; - std::vector tparams; + std::vector tparams; for (const Sort& s : params) { - tparams.push_back(*s.d_type.get()); + tparams.push_back(TypeNode::fromType(*s.d_type.get())); } if (d_type->isDatatype()) { - return Sort(d_solver, DatatypeType(*d_type).instantiate(tparams)); + return Sort(d_solver, + TypeNode::fromType(*d_type) + .instantiateParametricDatatype(tparams) + .toType()); } Assert(d_type->isSortConstructor()); - return Sort(d_solver, SortConstructorType(*d_type).instantiate(tparams)); + return Sort(d_solver, + d_solver->getNodeManager() + ->mkSort(TypeNode::fromType(*d_type), tparams) + .toType()); } std::string Sort::toString() const { return d_type->toString(); } @@ -996,20 +1005,20 @@ CVC4::Type Sort::getType(void) const { return *d_type; } size_t Sort::getConstructorArity() const { - CVC4_API_CHECK(isConstructor()) << "Not a function sort: " << (*this); + CVC4_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this); return ConstructorType(*d_type).getArity(); } std::vector Sort::getConstructorDomainSorts() const { - CVC4_API_CHECK(isConstructor()) << "Not a function sort: " << (*this); + CVC4_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this); std::vector types = ConstructorType(*d_type).getArgTypes(); return typeVectorToSorts(d_solver, types); } Sort Sort::getConstructorCodomainSort() const { - CVC4_API_CHECK(isConstructor()) << "Not a function sort: " << (*this); + CVC4_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this); return Sort(d_solver, ConstructorType(*d_type).getRangeType()); } @@ -1126,14 +1135,20 @@ uint32_t Sort::getFPSignificandSize() const std::vector Sort::getDatatypeParamSorts() const { CVC4_API_CHECK(isParametricDatatype()) << "Not a parametric datatype sort."; - std::vector types = DatatypeType(*d_type).getParamTypes(); - return typeVectorToSorts(d_solver, types); + std::vector typeNodes = + TypeNode::fromType(*d_type).getParamTypes(); + std::vector sorts; + for (size_t i = 0, tsize = typeNodes.size(); i < tsize; i++) + { + sorts.push_back(Sort(d_solver, typeNodes[i].toType())); + } + return sorts; } size_t Sort::getDatatypeArity() const { CVC4_API_CHECK(isDatatype()) << "Not a datatype sort."; - return DatatypeType(*d_type).getArity(); + return TypeNode::fromType(*d_type).getNumChildren() - 1; } /* Tuple sort ---------------------------------------------------------- */ @@ -1141,14 +1156,20 @@ size_t Sort::getDatatypeArity() const size_t Sort::getTupleLength() const { CVC4_API_CHECK(isTuple()) << "Not a tuple sort."; - return DatatypeType(*d_type).getTupleLength(); + return TypeNode::fromType(*d_type).getTupleLength(); } std::vector Sort::getTupleSorts() const { CVC4_API_CHECK(isTuple()) << "Not a tuple sort."; - std::vector types = DatatypeType(*d_type).getTupleTypes(); - return typeVectorToSorts(d_solver, types); + std::vector typeNodes = + TypeNode::fromType(*d_type).getTupleTypes(); + std::vector sorts; + for (size_t i = 0, tsize = typeNodes.size(); i < tsize; i++) + { + sorts.push_back(Sort(d_solver, typeNodes[i].toType())); + } + return sorts; } /* --------------------------------------------------------------------- */ @@ -1472,7 +1493,8 @@ Kind Term::getKindHelper() const break; } } - + // Notice that kinds like APPLY_TYPE_ASCRIPTION will be converted to + // INTERNAL_KIND. return intToExtKind(d_node->getKind()); } @@ -1604,7 +1626,7 @@ Op Term::getOp() const return Op(d_solver, intToExtKind(d_node->getKind()), op); } // Notice this is the only case where getKindHelper is used, since the - // cases above do have special cases for intToExtKind. + // cases above do not have special cases for intToExtKind. return Op(d_solver, getKindHelper()); } @@ -1938,20 +1960,31 @@ DatatypeConstructorDecl::DatatypeConstructorDecl() DatatypeConstructorDecl::DatatypeConstructorDecl(const Solver* slv, const std::string& name) - : d_solver(slv), d_ctor(new CVC4::DatatypeConstructor(name)) + : d_solver(slv), d_ctor(new CVC4::DTypeConstructor(name)) +{ +} +DatatypeConstructorDecl::~DatatypeConstructorDecl() { + if (d_ctor != nullptr) + { + // ensure proper node manager is in scope + NodeManagerScope scope(d_solver->getNodeManager()); + d_ctor.reset(); + } } void DatatypeConstructorDecl::addSelector(const std::string& name, Sort sort) { + NodeManagerScope scope(d_solver->getNodeManager()); CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null range sort for selector"; - d_ctor->addArg(name, *sort.d_type); + d_ctor->addArg(name, TypeNode::fromType(*sort.d_type)); } void DatatypeConstructorDecl::addSelectorSelf(const std::string& name) { - d_ctor->addArg(name, DatatypeSelfType()); + NodeManagerScope scope(d_solver->getNodeManager()); + d_ctor->addArgSelf(name); } std::string DatatypeConstructorDecl::toString() const @@ -1963,8 +1996,8 @@ std::string DatatypeConstructorDecl::toString() const // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! -const CVC4::DatatypeConstructor& -DatatypeConstructorDecl::getDatatypeConstructor(void) const +const CVC4::DTypeConstructor& DatatypeConstructorDecl::getDatatypeConstructor( + void) const { return *d_ctor; } @@ -1990,8 +2023,7 @@ DatatypeDecl::DatatypeDecl() : d_solver(nullptr), d_dtype(nullptr) {} DatatypeDecl::DatatypeDecl(const Solver* slv, const std::string& name, bool isCoDatatype) - : d_solver(slv), - d_dtype(new CVC4::Datatype(slv->getExprManager(), name, isCoDatatype)) + : d_solver(slv), d_dtype(new CVC4::DType(name, isCoDatatype)) { } @@ -2000,10 +2032,10 @@ DatatypeDecl::DatatypeDecl(const Solver* slv, Sort param, bool isCoDatatype) : d_solver(slv), - d_dtype(new CVC4::Datatype(slv->getExprManager(), - name, - std::vector{*param.d_type}, - isCoDatatype)) + d_dtype(new CVC4::DType( + name, + std::vector{TypeNode::fromType(*param.d_type)}, + isCoDatatype)) { } @@ -2013,23 +2045,32 @@ DatatypeDecl::DatatypeDecl(const Solver* slv, bool isCoDatatype) : d_solver(slv) { - std::vector tparams; + std::vector tparams; for (const Sort& p : params) { - tparams.push_back(*p.d_type); + tparams.push_back(TypeNode::fromType(*p.d_type)); } - d_dtype = std::shared_ptr( - new CVC4::Datatype(slv->getExprManager(), name, tparams, isCoDatatype)); + d_dtype = std::shared_ptr( + new CVC4::DType(name, tparams, isCoDatatype)); } bool DatatypeDecl::isNullHelper() const { return !d_dtype; } -DatatypeDecl::~DatatypeDecl() {} +DatatypeDecl::~DatatypeDecl() +{ + if (d_dtype != nullptr) + { + // ensure proper node manager is in scope + NodeManagerScope scope(d_solver->getNodeManager()); + d_dtype.reset(); + } +} void DatatypeDecl::addConstructor(const DatatypeConstructorDecl& ctor) { + NodeManagerScope scope(d_solver->getNodeManager()); CVC4_API_CHECK_NOT_NULL; - d_dtype->addConstructor(*ctor.d_ctor); + d_dtype->addConstructor(ctor.d_ctor); } size_t DatatypeDecl::getNumConstructors() const @@ -2062,7 +2103,7 @@ bool DatatypeDecl::isNull() const { return isNullHelper(); } // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! -CVC4::Datatype& DatatypeDecl::getDatatype(void) const { return *d_dtype; } +CVC4::DType& DatatypeDecl::getDatatype(void) const { return *d_dtype; } std::ostream& operator<<(std::ostream& out, const DatatypeDecl& dtdecl) { @@ -2075,13 +2116,21 @@ std::ostream& operator<<(std::ostream& out, const DatatypeDecl& dtdecl) DatatypeSelector::DatatypeSelector() : d_solver(nullptr), d_stor(nullptr) {} DatatypeSelector::DatatypeSelector(const Solver* slv, - const CVC4::DatatypeConstructorArg& stor) - : d_solver(slv), d_stor(new CVC4::DatatypeConstructorArg(stor)) + const CVC4::DTypeSelector& stor) + : d_solver(slv), d_stor(new CVC4::DTypeSelector(stor)) { CVC4_API_CHECK(d_stor->isResolved()) << "Expected resolved datatype selector"; } -DatatypeSelector::~DatatypeSelector() {} +DatatypeSelector::~DatatypeSelector() +{ + if (d_stor != nullptr) + { + // ensure proper node manager is in scope + NodeManagerScope scope(d_solver->getNodeManager()); + d_stor.reset(); + } +} std::string DatatypeSelector::getName() const { return d_stor->getName(); } @@ -2093,7 +2142,7 @@ Term DatatypeSelector::getSelectorTerm() const Sort DatatypeSelector::getRangeSort() const { - return Sort(d_solver, d_stor->getRangeType()); + return Sort(d_solver, d_stor->getRangeType().toType()); } std::string DatatypeSelector::toString() const @@ -2105,8 +2154,7 @@ std::string DatatypeSelector::toString() const // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! -CVC4::DatatypeConstructorArg DatatypeSelector::getDatatypeConstructorArg( - void) const +CVC4::DTypeSelector DatatypeSelector::getDatatypeConstructorArg(void) const { return *d_stor; } @@ -2124,14 +2172,22 @@ DatatypeConstructor::DatatypeConstructor() : d_solver(nullptr), d_ctor(nullptr) } DatatypeConstructor::DatatypeConstructor(const Solver* slv, - const CVC4::DatatypeConstructor& ctor) - : d_solver(slv), d_ctor(new CVC4::DatatypeConstructor(ctor)) + const CVC4::DTypeConstructor& ctor) + : d_solver(slv), d_ctor(new CVC4::DTypeConstructor(ctor)) { CVC4_API_CHECK(d_ctor->isResolved()) << "Expected resolved datatype constructor"; } -DatatypeConstructor::~DatatypeConstructor() {} +DatatypeConstructor::~DatatypeConstructor() +{ + if (d_ctor != nullptr) + { + // ensure proper node manager is in scope + NodeManagerScope scope(d_solver->getNodeManager()); + d_ctor.reset(); + } +} std::string DatatypeConstructor::getName() const { return d_ctor->getName(); } @@ -2143,15 +2199,22 @@ Term DatatypeConstructor::getConstructorTerm() const Term DatatypeConstructor::getSpecializedConstructorTerm(Sort retSort) const { + NodeManagerScope scope(d_solver->getNodeManager()); + CVC4_API_CHECK(d_ctor->isResolved()) + << "Expected resolved datatype constructor"; + CVC4_API_CHECK(retSort.isDatatype()) + << "Cannot get specialized constructor type for non-datatype type " + << retSort; CVC4_API_SOLVER_TRY_CATCH_BEGIN; NodeManager* nm = d_solver->getNodeManager(); - Node ret = nm->mkNode(kind::APPLY_TYPE_ASCRIPTION, - nm->mkConst(AscriptionType( - d_ctor - ->getSpecializedConstructorType( - retSort.getType()))), - d_ctor->getConstructor()); + Node ret = nm->mkNode( + kind::APPLY_TYPE_ASCRIPTION, + nm->mkConst(AscriptionType(d_ctor + ->getSpecializedConstructorType( + TypeNode::fromType(retSort.getType())) + .toType())), + d_ctor->getConstructor()); (void)ret.getType(true); /* kick off type checking */ // apply type ascription to the operator Term sctor = @@ -2205,20 +2268,19 @@ DatatypeConstructor::const_iterator DatatypeConstructor::end() const } DatatypeConstructor::const_iterator::const_iterator( - const Solver* slv, const CVC4::DatatypeConstructor& ctor, bool begin) + const Solver* slv, const CVC4::DTypeConstructor& ctor, bool begin) { d_solver = slv; - d_int_stors = ctor.getArgs(); + d_int_stors = &ctor.getArgs(); - const std::vector* sels = - static_cast*>( - d_int_stors); - for (const auto& s : *sels) + const std::vector>& sels = + ctor.getArgs(); + for (const std::shared_ptr& s : sels) { /* Can not use emplace_back here since constructor is private. */ - d_stors.push_back(DatatypeSelector(d_solver, s)); + d_stors.push_back(DatatypeSelector(d_solver, *s.get())); } - d_idx = begin ? 0 : sels->size(); + d_idx = begin ? 0 : sels.size(); } DatatypeConstructor::const_iterator::const_iterator() @@ -2283,7 +2345,7 @@ std::string DatatypeConstructor::toString() const // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! -const CVC4::DatatypeConstructor& DatatypeConstructor::getDatatypeConstructor( +const CVC4::DTypeConstructor& DatatypeConstructor::getDatatypeConstructor( void) const { return *d_ctor; @@ -2303,8 +2365,18 @@ DatatypeSelector DatatypeConstructor::getSelectorForName( break; } } - CVC4_API_CHECK(foundSel) << "No selector " << name << " for constructor " - << getName() << " exists"; + if (!foundSel) + { + std::stringstream snames; + snames << "{ "; + for (size_t i = 0, ncons = getNumSelectors(); i < ncons; i++) + { + snames << (*d_ctor)[i].getName() << " "; + } + snames << "} "; + CVC4_API_CHECK(foundSel) << "No selector " << name << " for constructor " + << getName() << " exists among " << snames.str(); + } return DatatypeSelector(d_solver, (*d_ctor)[index]); } @@ -2316,15 +2388,23 @@ std::ostream& operator<<(std::ostream& out, const DatatypeConstructor& ctor) /* Datatype ----------------------------------------------------------------- */ -Datatype::Datatype(const Solver* slv, const CVC4::Datatype& dtype) - : d_solver(slv), d_dtype(new CVC4::Datatype(dtype)) +Datatype::Datatype(const Solver* slv, const CVC4::DType& dtype) + : d_solver(slv), d_dtype(new CVC4::DType(dtype)) { CVC4_API_CHECK(d_dtype->isResolved()) << "Expected resolved datatype"; } Datatype::Datatype() : d_solver(nullptr), d_dtype(nullptr) {} -Datatype::~Datatype() {} +Datatype::~Datatype() +{ + if (d_dtype != nullptr) + { + // ensure proper node manager is in scope + NodeManagerScope scope(d_solver->getNodeManager()); + d_dtype.reset(); + } +} DatatypeConstructor Datatype::operator[](size_t idx) const { @@ -2383,7 +2463,7 @@ Datatype::const_iterator Datatype::end() const // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! -const CVC4::Datatype& Datatype::getDatatype(void) const { return *d_dtype; } +const CVC4::DType& Datatype::getDatatype(void) const { return *d_dtype; } DatatypeConstructor Datatype::getConstructorForName( const std::string& name) const @@ -2399,24 +2479,34 @@ DatatypeConstructor Datatype::getConstructorForName( break; } } - CVC4_API_CHECK(foundCons) << "No constructor " << name << " for datatype " - << getName() << " exists"; + if (!foundCons) + { + std::stringstream snames; + snames << "{ "; + for (size_t i = 0, ncons = getNumConstructors(); i < ncons; i++) + { + snames << (*d_dtype)[i].getName() << " "; + } + snames << "}"; + CVC4_API_CHECK(foundCons) << "No constructor " << name << " for datatype " + << getName() << " exists, among " << snames.str(); + } return DatatypeConstructor(d_solver, (*d_dtype)[index]); } Datatype::const_iterator::const_iterator(const Solver* slv, - const CVC4::Datatype& dtype, + const CVC4::DType& dtype, bool begin) - : d_solver(slv), d_int_ctors(dtype.getConstructors()) + : d_solver(slv), d_int_ctors(&dtype.getConstructors()) { - const std::vector* cons = - static_cast*>(d_int_ctors); - for (const auto& c : *cons) + const std::vector>& cons = + dtype.getConstructors(); + for (const std::shared_ptr& c : cons) { /* Can not use emplace_back here since constructor is private. */ - d_ctors.push_back(DatatypeConstructor(d_solver, c)); + d_ctors.push_back(DatatypeConstructor(d_solver, *c.get())); } - d_idx = begin ? 0 : cons->size(); + d_idx = begin ? 0 : cons.size(); } Datatype::const_iterator::const_iterator() @@ -2662,8 +2752,8 @@ Sort Grammar::resolve() Sort(d_solver, d_solver->getExprManager()->mkSort(ntsymbol.toString())); } - std::vector datatypes; - std::set unresTypes; + std::vector datatypes; + std::set unresTypes; datatypes.reserve(d_ntSyms.size()); @@ -2684,8 +2774,8 @@ Sort Grammar::resolve() } bool aci = d_allowConst.find(ntSym) != d_allowConst.end(); - Type btt = ntSym.d_node->getType().toType(); - dtDecl.d_dtype->setSygus(btt, bvl.d_node->toExpr(), aci, false); + TypeNode btt = ntSym.d_node->getType(); + dtDecl.d_dtype->setSygus(btt, *bvl.d_node, aci, false); // We can be in a case where the only rule specified was (Variable T) // and there are no variables of type T, in which case this is a bogus @@ -2695,15 +2785,15 @@ Sort Grammar::resolve() << " produced an empty rule list"; datatypes.push_back(*dtDecl.d_dtype); - unresTypes.insert(*ntsToUnres[ntSym].d_type); + unresTypes.insert(TypeNode::fromType(*ntsToUnres[ntSym].d_type)); } - std::vector datatypeTypes = - d_solver->getExprManager()->mkMutualDatatypeTypes( - datatypes, unresTypes, ExprManager::DATATYPE_FLAG_PLACEHOLDER); + std::vector datatypeTypes = + d_solver->getNodeManager()->mkMutualDatatypeTypes( + datatypes, unresTypes, NodeManager::DATATYPE_FLAG_PLACEHOLDER); // return is the first datatype - return Sort(d_solver, datatypeTypes[0]); + return Sort(d_solver, datatypeTypes[0].toType()); } void Grammar::addSygusConstructorTerm( @@ -2735,8 +2825,12 @@ void Grammar::addSygusConstructorTerm( d_solver->getExprManager()->mkExpr( CVC4::kind::LAMBDA, {lbvl.d_node->toExpr(), op.d_node->toExpr()})); } - dt.d_dtype->addSygusConstructor( - op.d_node->toExpr(), ssCName.str(), sortVectorToTypes(cargs)); + std::vector cargst; + for (const Sort& s : cargs) + { + cargst.push_back(TypeNode::fromType(s.getType())); + } + dt.d_dtype->addSygusConstructor(*op.d_node, ssCName.str(), cargst); } Term Grammar::purifySygusGTerm( @@ -2801,9 +2895,8 @@ void Grammar::addSygusConstructorVariables(DatatypeDecl& dt, Sort sort) const { std::stringstream ss; ss << v; - std::vector cargs; - dt.d_dtype->addSygusConstructor( - v.d_node->toExpr(), ss.str(), sortVectorToTypes(cargs)); + std::vector cargs; + dt.d_dtype->addSygusConstructor(*v.d_node, ss.str(), cargs); } } } @@ -3048,9 +3141,10 @@ std::vector Solver::mkDatatypeSortsInternal( std::vector& dtypedecls, std::set& unresolvedSorts) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; - std::vector datatypes; + std::vector datatypes; for (size_t i = 0, ndts = dtypedecls.size(); i < ndts; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(this == dtypedecls[i].d_solver, @@ -3069,13 +3163,18 @@ std::vector Solver::mkDatatypeSortsInternal( { CVC4_API_SOLVER_CHECK_SORT(sort); } - std::set utypes = sortSetToTypes(unresolvedSorts); - std::vector dtypes = - d_exprMgr->mkMutualDatatypeTypes(datatypes, utypes); + + std::set utypes; + for (const Sort& s : unresolvedSorts) + { + utypes.insert(TypeNode::fromType(s.getType())); + } + std::vector dtypes = + getNodeManager()->mkMutualDatatypeTypes(datatypes, utypes); std::vector retTypes; - for (CVC4::DatatypeType t : dtypes) + for (CVC4::TypeNode t : dtypes) { - retTypes.push_back(Sort(this, t)); + retTypes.push_back(Sort(this, t.toType())); } return retTypes; @@ -3224,13 +3323,15 @@ Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const Sort Solver::mkDatatypeSort(DatatypeDecl dtypedecl) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_CHECK(this == dtypedecl.d_solver) << "Given datatype declaration is not associated with this solver"; CVC4_API_ARG_CHECK_EXPECTED(dtypedecl.getNumConstructors() > 0, dtypedecl) << "a datatype declaration with at least one constructor"; - return Sort(this, d_exprMgr->mkDatatypeType(*dtypedecl.d_dtype)); + return Sort(this, + getNodeManager()->mkDatatypeType(*dtypedecl.d_dtype).toType()); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -3238,14 +3339,18 @@ Sort Solver::mkDatatypeSort(DatatypeDecl dtypedecl) const std::vector Solver::mkDatatypeSorts( std::vector& dtypedecls) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; std::set unresolvedSorts; return mkDatatypeSortsInternal(dtypedecls, unresolvedSorts); + CVC4_API_SOLVER_TRY_CATCH_END; } std::vector Solver::mkDatatypeSorts(std::vector& dtypedecls, std::set& unresolvedSorts) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; return mkDatatypeSortsInternal(dtypedecls, unresolvedSorts); + CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::mkFunctionSort(Sort domain, Sort codomain) const @@ -3332,6 +3437,7 @@ Sort Solver::mkPredicateSort(const std::vector& sorts) const Sort Solver::mkRecordSort( const std::vector>& fields) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; std::vector> f; size_t i = 0; @@ -3347,7 +3453,7 @@ Sort Solver::mkRecordSort( f.emplace_back(p.first, *p.second.d_type); } - return Sort(this, d_exprMgr->mkRecordType(Record(f))); + return Sort(this, getNodeManager()->mkRecordType(Record(f)).toType()); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -3409,9 +3515,12 @@ Sort Solver::mkTupleSort(const std::vector& sorts) const !sorts[i].isFunctionLike(), "parameter sort", sorts[i], i) << "non-function-like sort as parameter sort for tuple sort"; } - std::vector types = sortVectorToTypes(sorts); - - return Sort(this, d_exprMgr->mkTupleType(types)); + std::vector typeNodes; + for (const Sort& s : sorts) + { + typeNodes.push_back(TypeNode::fromType(*s.d_type)); + } + return Sort(this, getNodeManager()->mkTupleType(typeNodes).toType()); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -3789,6 +3898,7 @@ Term Solver::mkVar(Sort sort, const std::string& symbol) const DatatypeConstructorDecl Solver::mkDatatypeConstructorDecl( const std::string& name) { + NodeManagerScope scope(getNodeManager()); return DatatypeConstructorDecl(this, name); } @@ -3797,6 +3907,7 @@ DatatypeConstructorDecl Solver::mkDatatypeConstructorDecl( DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, bool isCoDatatype) { + NodeManagerScope scope(getNodeManager()); return DatatypeDecl(this, name, isCoDatatype); } @@ -3804,6 +3915,7 @@ DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, Sort param, bool isCoDatatype) { + NodeManagerScope scope(getNodeManager()); return DatatypeDecl(this, name, param, isCoDatatype); } @@ -3811,6 +3923,7 @@ DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, const std::vector& params, bool isCoDatatype) { + NodeManagerScope scope(getNodeManager()); return DatatypeDecl(this, name, params, isCoDatatype); } @@ -4018,6 +4131,7 @@ Term Solver::mkTerm(Op op, const std::vector& children) const Term Solver::mkTuple(const std::vector& sorts, const std::vector& terms) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_CHECK(sorts.size() == terms.size()) << "Expected the same number of sorts and elements"; @@ -4395,7 +4509,7 @@ Sort Solver::declareDatatype( << "datatype constructor declaration associated to this solver object"; dtdecl.addConstructor(ctors[i]); } - return Sort(this, d_exprMgr->mkDatatypeType(*dtdecl.d_dtype)); + return Sort(this, getNodeManager()->mkDatatypeType(*dtdecl.d_dtype).toType()); CVC4_API_SOLVER_TRY_CATCH_END; } diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 6c84b73bc..0c322d7da 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -40,9 +40,9 @@ template class NodeTemplate; typedef NodeTemplate Node; class Expr; -class Datatype; -class DatatypeConstructor; -class DatatypeConstructorArg; +class DType; +class DTypeConstructor; +class DTypeSelector; class ExprManager; class GetAbductCommand; class GetInterpolCommand; @@ -1241,6 +1241,11 @@ class CVC4_PUBLIC DatatypeConstructorDecl */ DatatypeConstructorDecl(); + /** + * Destructor. + */ + ~DatatypeConstructorDecl(); + /** * Add datatype selector declaration. * @param name the name of the datatype selector declaration to add @@ -1260,7 +1265,7 @@ class CVC4_PUBLIC DatatypeConstructorDecl // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! - const CVC4::DatatypeConstructor& getDatatypeConstructor(void) const; + const CVC4::DTypeConstructor& getDatatypeConstructor(void) const; private: /** @@ -1280,9 +1285,9 @@ class CVC4_PUBLIC DatatypeConstructorDecl * The internal (intermediate) datatype constructor wrapped by this * datatype constructor declaration. * This is a shared_ptr rather than a unique_ptr since - * CVC4::DatatypeConstructor is not ref counted. + * CVC4::DTypeConstructor is not ref counted. */ - std::shared_ptr d_ctor; + std::shared_ptr d_ctor; }; class Solver; @@ -1333,7 +1338,7 @@ class CVC4_PUBLIC DatatypeDecl // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! - CVC4::Datatype& getDatatype(void) const; + CVC4::DType& getDatatype(void) const; private: /** @@ -1386,10 +1391,10 @@ class CVC4_PUBLIC DatatypeDecl /* The internal (intermediate) datatype wrapped by this datatype * declaration - * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is + * This is a shared_ptr rather than a unique_ptr since CVC4::DType is * not ref counted. */ - std::shared_ptr d_dtype; + std::shared_ptr d_dtype; }; /** @@ -1414,7 +1419,7 @@ class CVC4_PUBLIC DatatypeSelector * @param stor the internal datatype selector to be wrapped * @return the DatatypeSelector */ - DatatypeSelector(const Solver* slv, const CVC4::DatatypeConstructorArg& stor); + DatatypeSelector(const Solver* slv, const CVC4::DTypeSelector& stor); /** * Destructor. @@ -1440,7 +1445,7 @@ class CVC4_PUBLIC DatatypeSelector // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! - CVC4::DatatypeConstructorArg getDatatypeConstructorArg(void) const; + CVC4::DTypeSelector getDatatypeConstructorArg(void) const; private: /** @@ -1450,10 +1455,10 @@ class CVC4_PUBLIC DatatypeSelector /** * The internal datatype selector wrapped by this datatype selector. - * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is + * This is a shared_ptr rather than a unique_ptr since CVC4::DType is * not ref counted. */ - std::shared_ptr d_stor; + std::shared_ptr d_stor; }; /** @@ -1477,7 +1482,7 @@ class CVC4_PUBLIC DatatypeConstructor * @param ctor the internal datatype constructor to be wrapped * @return the DatatypeConstructor */ - DatatypeConstructor(const Solver* slv, const CVC4::DatatypeConstructor& ctor); + DatatypeConstructor(const Solver* slv, const CVC4::DTypeConstructor& ctor); /** * Destructor. @@ -1620,7 +1625,7 @@ class CVC4_PUBLIC DatatypeConstructor * @param true if this is a begin() iterator */ const_iterator(const Solver* slv, - const CVC4::DatatypeConstructor& ctor, + const CVC4::DTypeConstructor& ctor, bool begin); /** @@ -1652,7 +1657,7 @@ class CVC4_PUBLIC DatatypeConstructor // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! - const CVC4::DatatypeConstructor& getDatatypeConstructor(void) const; + const CVC4::DTypeConstructor& getDatatypeConstructor(void) const; private: /** @@ -1669,10 +1674,10 @@ class CVC4_PUBLIC DatatypeConstructor /** * The internal datatype constructor wrapped by this datatype constructor. - * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is + * This is a shared_ptr rather than a unique_ptr since CVC4::DType is * not ref counted. */ - std::shared_ptr d_ctor; + std::shared_ptr d_ctor; }; /* @@ -1691,7 +1696,7 @@ class CVC4_PUBLIC Datatype * @param dtype the internal datatype to be wrapped * @return the Datatype */ - Datatype(const Solver* slv, const CVC4::Datatype& dtype); + Datatype(const Solver* slv, const CVC4::DType& dtype); // Nullary constructor for Cython Datatype(); @@ -1835,7 +1840,7 @@ class CVC4_PUBLIC Datatype * @param dtype the internal datatype to iterate over * @param true if this is a begin() iterator */ - const_iterator(const Solver* slv, const CVC4::Datatype& dtype, bool begin); + const_iterator(const Solver* slv, const CVC4::DType& dtype, bool begin); /** * The associated solver object. @@ -1866,7 +1871,7 @@ class CVC4_PUBLIC Datatype // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! - const CVC4::Datatype& getDatatype(void) const; + const CVC4::DType& getDatatype(void) const; private: /** @@ -1883,10 +1888,10 @@ class CVC4_PUBLIC Datatype /** * The internal datatype wrapped by this datatype. - * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is + * This is a shared_ptr rather than a unique_ptr since CVC4::DType is * not ref counted. */ - std::shared_ptr d_dtype; + std::shared_ptr d_dtype; }; /** diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 0092b78c6..8bc732314 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -73,8 +73,6 @@ libcvc4_add_sources( type_node.cpp type_node.h variable_type_map.h - datatype.h - datatype.cpp datatype_index.h datatype_index.cpp dtype.h diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp deleted file mode 100644 index a9ac3fbbf..000000000 --- a/src/expr/datatype.cpp +++ /dev/null @@ -1,970 +0,0 @@ -/********************* */ -/*! \file datatype.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A class representing a Datatype definition - ** - ** A class representing a Datatype definition for the theory of - ** inductive datatypes. - **/ -#include "expr/datatype.h" - -#include -#include - -#include "base/check.h" -#include "expr/attribute.h" -#include "expr/datatype.h" -#include "expr/dtype.h" -#include "expr/expr_manager.h" -#include "expr/expr_manager_scope.h" -#include "expr/node.h" -#include "expr/node_algorithm.h" -#include "expr/node_manager.h" -#include "expr/type.h" -#include "expr/type_matcher.h" -#include "options/datatypes_options.h" -#include "options/set_language.h" -#include "theory/type_enumerator.h" - -using namespace std; - -namespace CVC4 { - -Datatype::~Datatype() -{ - ExprManagerScope ems(*d_em); - d_internal.reset(); - d_constructors.clear(); -} - -Datatype::Datatype(ExprManager* em, std::string name, bool isCo) - : d_em(em), - d_internal(nullptr), - d_record(NULL), - d_isRecord(false), - d_constructors() -{ - ExprManagerScope ems(*d_em); - d_internal = std::make_shared(name, isCo); -} - -Datatype::Datatype(ExprManager* em, - std::string name, - const std::vector& params, - bool isCo) - : d_em(em), - d_internal(nullptr), - d_record(NULL), - d_isRecord(false), - d_constructors() -{ - ExprManagerScope ems(*d_em); - std::vector paramsn; - for (const Type& t : params) - { - paramsn.push_back(TypeNode::fromType(t)); - } - d_internal = std::make_shared(name, paramsn, isCo); -} - -const Datatype& Datatype::datatypeOf(Expr item) { - ExprManagerScope ems(item); - TypeNode t = Node::fromExpr(item).getType(); - switch(t.getKind()) { - case kind::CONSTRUCTOR_TYPE: - return DatatypeType(t[t.getNumChildren() - 1].toType()).getDatatype(); - case kind::SELECTOR_TYPE: - case kind::TESTER_TYPE: - return DatatypeType(t[0].toType()).getDatatype(); - default: - Unhandled() << "arg must be a datatype constructor, selector, or tester"; - } -} - -size_t Datatype::indexOf(Expr item) { - ExprManagerScope ems(item); - PrettyCheckArgument(item.getType().isConstructor() || - item.getType().isTester() || - item.getType().isSelector(), - item, - "arg must be a datatype constructor, selector, or tester"); - return indexOfInternal(item); -} - -size_t Datatype::indexOfInternal(Expr item) -{ - TNode n = Node::fromExpr(item); - if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){ - return indexOf( item[0] ); - }else{ - Assert(n.hasAttribute(DTypeIndexAttr())); - return n.getAttribute(DTypeIndexAttr()); - } -} - -size_t Datatype::cindexOf(Expr item) { - ExprManagerScope ems(item); - PrettyCheckArgument(item.getType().isSelector(), - item, - "arg must be a datatype selector"); - return cindexOfInternal(item); -} -size_t Datatype::cindexOfInternal(Expr item) -{ - TNode n = Node::fromExpr(item); - if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){ - return cindexOf( item[0] ); - }else{ - Assert(n.hasAttribute(DTypeConsIndexAttr())); - return n.getAttribute(DTypeConsIndexAttr()); - } -} - -void Datatype::resolve(const std::map& resolutions, - const std::vector& placeholders, - const std::vector& replacements, - const std::vector& paramTypes, - const std::vector& paramReplacements) -{ - PrettyCheckArgument(!isResolved(), this, "cannot resolve a Datatype twice"); - PrettyCheckArgument(resolutions.find(getName()) != resolutions.end(), - resolutions, - "Datatype::resolve(): resolutions doesn't contain me!"); - PrettyCheckArgument(placeholders.size() == replacements.size(), placeholders, - "placeholders and replacements must be the same size"); - PrettyCheckArgument(paramTypes.size() == paramReplacements.size(), paramTypes, - "paramTypes and paramReplacements must be the same size"); - PrettyCheckArgument(getNumConstructors() > 0, *this, "cannot resolve a Datatype that has no constructors"); - - // we're using some internals, so we have to make sure that the Datatype's - // ExprManager is active - ExprManagerScope ems(*d_em); - - Trace("datatypes") << "Datatype::resolve: " << getName() - << ", #placeholders=" << placeholders.size() << std::endl; - - std::map resolutionsn; - std::vector placeholdersn; - std::vector replacementsn; - std::vector paramTypesn; - std::vector paramReplacementsn; - for (const std::pair& r : resolutions) - { - resolutionsn[r.first] = TypeNode::fromType(r.second); - } - for (const Type& t : placeholders) - { - placeholdersn.push_back(TypeNode::fromType(t)); - } - for (const Type& t : replacements) - { - replacementsn.push_back(TypeNode::fromType(t)); - } - for (const Type& t : paramTypes) - { - paramTypesn.push_back(TypeNode::fromType(t)); - } - for (const Type& t : paramReplacements) - { - paramReplacementsn.push_back(TypeNode::fromType(t)); - } - bool res = d_internal->resolve(resolutionsn, - placeholdersn, - replacementsn, - paramTypesn, - paramReplacementsn); - if (!res) - { - IllegalArgument(*this, - "could not resolve datatype that is not well formed"); - } - Trace("dt-debug") << "Datatype::resolve: finished " << getName() << " " - << d_constructors.size() << std::endl; - AlwaysAssert(isResolved()); - // - d_self = d_internal->getTypeNode().toType(); - for (DatatypeConstructor& c : d_constructors) - { - AlwaysAssert(c.isResolved()); - c.d_constructor = c.d_internal->getConstructor().toExpr(); - for (size_t i = 0, nargs = c.getNumArgs(); i < nargs; i++) - { - AlwaysAssert(c.d_args[i].isResolved()); - c.d_args[i].d_selector = c.d_args[i].d_internal->getSelector().toExpr(); - } - } - - if( d_isRecord ){ - std::vector< std::pair > fields; - for( unsigned i=0; i<(*this)[0].getNumArgs(); i++ ){ - fields.push_back( std::pair( (*this)[0][i].getName(), (*this)[0][i].getRangeType() ) ); - } - d_record.reset(new Record(fields)); - } -} - -void Datatype::addConstructor(const DatatypeConstructor& c) { - Trace("dt-debug") << "Datatype::addConstructor" << std::endl; - PrettyCheckArgument( - !isResolved(), this, "cannot add a constructor to a finalized Datatype"); - d_constructors.push_back(c); - d_internal->addConstructor(c.d_internal); - Trace("dt-debug") << "Datatype::addConstructor: finished" << std::endl; -} - - -void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){ - PrettyCheckArgument( - !isResolved(), this, "cannot set sygus type to a finalized Datatype"); - // We can be in a case where the only rule specified was - // (Constant T), in which case we have not yet added a constructor. We - // ensure an arbitrary constant is added in this case. We additionally - // add a constant if the grammar has only non-nullary constructors, since this - // ensures the datatype is well-founded (see 3423). - // Notice we only want to do this for sygus datatypes that are user-provided. - // At the moment, the condition !allow_all implies the grammar is - // user-provided and hence may require a default constant. - // TODO (https://github.com/CVC4/cvc4-projects/issues/38): - // In an API for SyGuS, it probably makes more sense for the user to - // explicitly add the "any constant" constructor with a call instead of - // passing a flag. This would make the block of code unnecessary. - if (allow_const && !allow_all) - { - // if i don't already have a constant (0-ary constructor) - bool hasConstant = false; - for (unsigned i = 0, ncons = getNumConstructors(); i < ncons; i++) - { - if ((*this)[i].getNumArgs() == 0) - { - hasConstant = true; - break; - } - } - if (!hasConstant) - { - // add an arbitrary one - Expr op = st.mkGroundTerm(); - std::stringstream cname; - cname << op; - std::vector cargs; - addSygusConstructor(op, cname.str(), cargs); - } - } - - TypeNode stn = TypeNode::fromType(st); - Node bvln = Node::fromExpr(bvl); - d_internal->setSygus(stn, bvln, allow_const, allow_all); -} - -void Datatype::addSygusConstructor(Expr op, - const std::string& cname, - const std::vector& cargs, - int weight) -{ - // avoid name clashes - std::stringstream ss; - ss << getName() << "_" << getNumConstructors() << "_" << cname; - std::string name = ss.str(); - unsigned cweight = weight >= 0 ? weight : (cargs.empty() ? 0 : 1); - DatatypeConstructor c(name, cweight); - c.setSygus(op); - for( unsigned j=0; j& cargs, - int weight) -{ - ExprManagerScope ems(*d_em); - Expr op = d_em->operatorOf(k); - addSygusConstructor(op, cname, cargs, weight); -} - -void Datatype::setTuple() { - PrettyCheckArgument( - !isResolved(), this, "cannot set tuple to a finalized Datatype"); - d_internal->setTuple(); -} - -void Datatype::setRecord() { - PrettyCheckArgument( - !isResolved(), this, "cannot set record to a finalized Datatype"); - d_isRecord = true; - d_internal->setRecord(); -} - -Cardinality Datatype::getCardinality(Type t) const -{ - PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); - Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this); - ExprManagerScope ems(d_self); - TypeNode tn = TypeNode::fromType(t); - return d_internal->getCardinality(tn); -} - -Cardinality Datatype::getCardinality() const -{ - PrettyCheckArgument(!isParametric(), this, "for getCardinality, this datatype cannot be parametric"); - ExprManagerScope ems(d_self); - return d_internal->getCardinality(); -} - -bool Datatype::isRecursiveSingleton(Type t) const -{ - PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); - Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this); - ExprManagerScope ems(d_self); - TypeNode tn = TypeNode::fromType(t); - return d_internal->isRecursiveSingleton(tn); -} - -bool Datatype::isRecursiveSingleton() const -{ - PrettyCheckArgument(!isParametric(), this, "for isRecursiveSingleton, this datatype cannot be parametric"); - ExprManagerScope ems(d_self); - return d_internal->isRecursiveSingleton(); -} - -unsigned Datatype::getNumRecursiveSingletonArgTypes(Type t) const -{ - Assert(isRecursiveSingleton(t)); - ExprManagerScope ems(d_self); - TypeNode tn = TypeNode::fromType(t); - return d_internal->getNumRecursiveSingletonArgTypes(tn); -} - -unsigned Datatype::getNumRecursiveSingletonArgTypes() const -{ - PrettyCheckArgument(!isParametric(), this, "for getNumRecursiveSingletonArgTypes, this datatype cannot be parametric"); - ExprManagerScope ems(d_self); - return d_internal->getNumRecursiveSingletonArgTypes(); -} - -Type Datatype::getRecursiveSingletonArgType(Type t, unsigned i) const -{ - Assert(isRecursiveSingleton(t)); - ExprManagerScope ems(d_self); - TypeNode tn = TypeNode::fromType(t); - return d_internal->getRecursiveSingletonArgType(tn, i).toType(); -} - -Type Datatype::getRecursiveSingletonArgType(unsigned i) const -{ - PrettyCheckArgument(!isParametric(), this, "for getRecursiveSingletonArgType, this datatype cannot be parametric"); - ExprManagerScope ems(d_self); - return d_internal->getRecursiveSingletonArgType(i).toType(); -} - -bool Datatype::isFinite(Type t) const -{ - PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); - Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this); - ExprManagerScope ems(d_self); - TypeNode tn = TypeNode::fromType(t); - return d_internal->isFinite(tn); -} -bool Datatype::isFinite() const -{ - PrettyCheckArgument(isResolved() && !isParametric(), this, "this datatype must be resolved and not parametric"); - ExprManagerScope ems(d_self); - return d_internal->isFinite(); -} - -bool Datatype::isInterpretedFinite(Type t) const -{ - PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); - Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this); - ExprManagerScope ems(d_self); - TypeNode tn = TypeNode::fromType(t); - return d_internal->isInterpretedFinite(tn); -} -bool Datatype::isInterpretedFinite() const -{ - PrettyCheckArgument(isResolved() && !isParametric(), this, "this datatype must be resolved and not parametric"); - ExprManagerScope ems(d_self); - return d_internal->isInterpretedFinite(); -} - -bool Datatype::isWellFounded() const -{ - ExprManagerScope ems(d_self); - return d_internal->isWellFounded(); -} - -bool Datatype::hasNestedRecursion() const -{ - ExprManagerScope ems(d_self); - return d_internal->hasNestedRecursion(); -} - -Expr Datatype::mkGroundTerm(Type t) const -{ - PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); - ExprManagerScope ems(d_self); - TypeNode tn = TypeNode::fromType(t); - Node gterm = d_internal->mkGroundTerm(tn); - PrettyCheckArgument( - !gterm.isNull(), - this, - "datatype is not well-founded, cannot construct a ground term!"); - return gterm.toExpr(); -} - -Expr Datatype::mkGroundValue(Type t) const -{ - PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); - ExprManagerScope ems(d_self); - TypeNode tn = TypeNode::fromType(t); - Node gvalue = d_internal->mkGroundValue(tn); - PrettyCheckArgument( - !gvalue.isNull(), - this, - "datatype is not well-founded, cannot construct a ground value!"); - return gvalue.toExpr(); -} - -DatatypeType Datatype::getDatatypeType() const -{ - PrettyCheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType"); - ExprManagerScope ems(d_self); - Type self = d_internal->getTypeNode().toType(); - PrettyCheckArgument(!self.isNull(), *this); - return DatatypeType(self); -} - -DatatypeType Datatype::getDatatypeType(const std::vector& params) const -{ - PrettyCheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType"); - ExprManagerScope ems(d_self); - Type self = d_internal->getTypeNode().toType(); - PrettyCheckArgument(!self.isNull() && DatatypeType(self).isParametric(), - this); - return DatatypeType(self).instantiate(params); -} - -bool Datatype::operator==(const Datatype& other) const -{ - // two datatypes are == iff the name is the same and they have - // exactly matching constructors (in the same order) - - if(this == &other) { - return true; - } - return true; -} - -const DatatypeConstructor& Datatype::operator[](size_t index) const { - PrettyCheckArgument(index < getNumConstructors(), index, "index out of bounds"); - return d_constructors[index]; -} - -const DatatypeConstructor& Datatype::operator[](std::string name) const { - for(const_iterator i = begin(); i != end(); ++i) { - if((*i).getName() == name) { - return *i; - } - } - std::string dname = getName(); - IllegalArgument(name, - "No such constructor `%s' of datatype `%s'", - name.c_str(), - dname.c_str()); -} - -Expr Datatype::getConstructor(std::string name) const { - return (*this)[name].getConstructor(); -} - -Type Datatype::getSygusType() const { - return d_internal->getSygusType().toType(); -} - -Expr Datatype::getSygusVarList() const { - return d_internal->getSygusVarList().toExpr(); -} - -bool Datatype::getSygusAllowConst() const { - return d_internal->getSygusAllowConst(); -} - -bool Datatype::getSygusAllowAll() const { - return d_internal->getSygusAllowAll(); -} - -bool Datatype::involvesExternalType() const{ - return d_internal->involvesExternalType(); -} - -bool Datatype::involvesUninterpretedType() const{ - return d_internal->involvesUninterpretedType(); -} - -const std::vector* Datatype::getConstructors() const -{ - return &d_constructors; -} - -DatatypeConstructor::DatatypeConstructor(std::string name, unsigned weight) - : d_internal(nullptr) -{ - PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name"); - d_internal = std::make_shared(name, weight); -} - -void DatatypeConstructor::setSygus(Expr op) -{ - PrettyCheckArgument( - !isResolved(), this, "cannot modify a finalized Datatype constructor"); - Node opn = Node::fromExpr(op); - d_internal->setSygus(op); -} - -const std::vector* DatatypeConstructor::getArgs() - const -{ - return &d_args; -} - -void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) { - // We don't want to introduce a new data member, because eventually - // we're going to be a constant stuffed inside a node. So we stow - // the selector type away inside a var until resolution (when we can - // create the proper selector type) - PrettyCheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor"); - PrettyCheckArgument(!selectorType.isNull(), selectorType, "cannot add a null selector type"); - - // we're using some internals, so we have to set up this library context - ExprManagerScope ems(selectorType); - - Expr type = NodeManager::currentNM()->mkSkolem("unresolved_" + selectorName, TypeNode::fromType(selectorType), "is an unresolved selector type placeholder", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr(); - Debug("datatypes") << type << endl; - d_args.push_back(DatatypeConstructorArg(selectorName, type)); - d_internal->addArg(d_args.back().d_internal); -} - -void DatatypeConstructor::addArg(std::string selectorName, DatatypeUnresolvedType selectorType) { - // We don't want to introduce a new data member, because eventually - // we're going to be a constant stuffed inside a node. So we stow - // the selector type away after a NUL in the name string until - // resolution (when we can create the proper selector type) - PrettyCheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor"); - PrettyCheckArgument(selectorType.getName() != "", selectorType, "cannot add a null selector type"); - d_args.push_back(DatatypeConstructorArg(selectorName + '\0' + selectorType.getName(), Expr())); - d_internal->addArg(d_args.back().d_internal); -} - -void DatatypeConstructor::addArg(std::string selectorName, DatatypeSelfType) { - // We don't want to introduce a new data member, because eventually - // we're going to be a constant stuffed inside a node. So we mark - // the name string with a NUL to indicate that we have a - // self-selecting selector until resolution (when we can create the - // proper selector type) - PrettyCheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor"); - d_args.push_back(DatatypeConstructorArg(selectorName + '\0', Expr())); - d_internal->addArg(d_args.back().d_internal); -} - -std::string DatatypeConstructor::getName() const -{ - return d_internal->getName(); -} - -Expr DatatypeConstructor::getConstructor() const { - PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); - return d_constructor; -} - -Type DatatypeConstructor::getSpecializedConstructorType(Type returnType) const { - PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); - PrettyCheckArgument(returnType.isDatatype(), this, "cannot get specialized constructor type for non-datatype type"); - ExprManagerScope ems(d_constructor); - TypeNode tn = TypeNode::fromType(returnType); - return d_internal->getSpecializedConstructorType(tn).toType(); -} - -Expr DatatypeConstructor::getTester() const { - PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); - ExprManagerScope ems(d_constructor); - return d_internal->getTester().toExpr(); -} - -Expr DatatypeConstructor::getSygusOp() const { - PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); - ExprManagerScope ems(d_constructor); - return d_internal->getSygusOp().toExpr(); -} - -bool DatatypeConstructor::isSygusIdFunc() const { - PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); - ExprManagerScope ems(d_constructor); - return d_internal->isSygusIdFunc(); -} - -unsigned DatatypeConstructor::getWeight() const -{ - PrettyCheckArgument( - isResolved(), this, "this datatype constructor is not yet resolved"); - ExprManagerScope ems(d_constructor); - return d_internal->getWeight(); -} - -Cardinality DatatypeConstructor::getCardinality(Type t) const -{ - PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); - ExprManagerScope ems(d_constructor); - TypeNode tn = TypeNode::fromType(t); - return d_internal->getCardinality(tn); -} - -bool DatatypeConstructor::isFinite(Type t) const -{ - PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); - ExprManagerScope ems(d_constructor); - TypeNode tn = TypeNode::fromType(t); - return d_internal->isFinite(tn); -} - -bool DatatypeConstructor::isInterpretedFinite(Type t) const -{ - PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); - ExprManagerScope ems(d_constructor); - TypeNode tn = TypeNode::fromType(t); - return d_internal->isInterpretedFinite(tn); -} - -const DatatypeConstructorArg& DatatypeConstructor::operator[](size_t index) const { - PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds"); - return d_args[index]; -} - -const DatatypeConstructorArg& DatatypeConstructor::operator[](std::string name) const { - for(const_iterator i = begin(); i != end(); ++i) { - if((*i).getName() == name) { - return *i; - } - } - std::string dname = getName(); - IllegalArgument(name, - "No such arg `%s' of constructor `%s'", - name.c_str(), - dname.c_str()); -} - -Expr DatatypeConstructor::getSelector(std::string name) const { - return (*this)[name].d_selector; -} - -Type DatatypeConstructor::getArgType(unsigned index) const -{ - PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds"); - ExprManagerScope ems(d_constructor); - return d_internal->getArgType(index).toType(); -} - -bool DatatypeConstructor::involvesExternalType() const{ - ExprManagerScope ems(d_constructor); - return d_internal->involvesExternalType(); -} - -bool DatatypeConstructor::involvesUninterpretedType() const{ - ExprManagerScope ems(d_constructor); - return d_internal->involvesUninterpretedType(); -} - -DatatypeConstructorArg::DatatypeConstructorArg(std::string name, Expr selector) - : d_internal(nullptr) -{ - PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor arg without a name"); - d_internal = std::make_shared(name, Node::fromExpr(selector)); -} - -std::string DatatypeConstructorArg::getName() const -{ - string name = d_internal->getName(); - const size_t nul = name.find('\0'); - if(nul != string::npos) { - name.resize(nul); - } - return name; -} - -Expr DatatypeConstructorArg::getSelector() const { - PrettyCheckArgument(isResolved(), this, "cannot get a selector for an unresolved datatype constructor"); - return d_selector; -} - -Expr DatatypeConstructor::getSelectorInternal( Type domainType, size_t index ) const { - PrettyCheckArgument(isResolved(), this, "cannot get an internal selector for an unresolved datatype constructor"); - PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds"); - ExprManagerScope ems(d_constructor); - TypeNode dtn = TypeNode::fromType(domainType); - return d_internal->getSelectorInternal(dtn, index).toExpr(); -} - -int DatatypeConstructor::getSelectorIndexInternal( Expr sel ) const { - PrettyCheckArgument(isResolved(), this, "cannot get an internal selector index for an unresolved datatype constructor"); - ExprManagerScope ems(d_constructor); - Node seln = Node::fromExpr(sel); - return d_internal->getSelectorIndexInternal(seln); -} - -Expr DatatypeConstructorArg::getConstructor() const { - PrettyCheckArgument(isResolved(), this, - "cannot get a associated constructor for argument of an unresolved datatype constructor"); - ExprManagerScope ems(d_selector); - return d_internal->getConstructor().toExpr(); -} - -SelectorType DatatypeConstructorArg::getType() const { - return d_selector.getType(); -} - -Type DatatypeConstructorArg::getRangeType() const { - return getType().getRangeType(); -} - -bool DatatypeConstructorArg::isUnresolvedSelf() const -{ - return d_selector.isNull(); -} - -bool DatatypeConstructorArg::isResolved() const -{ - // We could just write: - // - // return !d_selector.isNull() && d_selector.getType().isSelector(); - // - // HOWEVER, this causes problems in ExprManager tear-down, because - // the attributes are removed before the pool is purged. When the - // pool is purged, this triggers an equality test between Datatypes, - // and this triggers a call to isResolved(), which breaks because - // d_selector has no type after attributes are stripped. - // - // This problem, coupled with the fact that this function is called - // _often_, means we should just use a boolean flag. - // - return d_internal->isResolved(); -} - -std::ostream& operator<<(std::ostream& os, const Datatype& dt) -{ - // can only output datatypes in the CVC4 native language - language::SetLanguage::Scope ls(os, language::output::LANG_CVC4); - dt.toStream(os); - return os; -} - -void Datatype::toStream(std::ostream& out) const -{ - out << "DATATYPE " << getName(); - if (isParametric()) - { - out << '['; - for (size_t i = 0; i < getNumParameters(); ++i) - { - if(i > 0) { - out << ','; - } - out << getParameter(i); - } - out << ']'; - } - out << " =" << endl; - Datatype::const_iterator i = begin(), i_end = end(); - if(i != i_end) { - out << " "; - do { - out << *i << endl; - if(++i != i_end) { - out << "| "; - } - } while(i != i_end); - } - out << "END;" << endl; -} - -std::ostream& operator<<(std::ostream& os, const DatatypeConstructor& ctor) { - // can only output datatypes in the CVC4 native language - language::SetLanguage::Scope ls(os, language::output::LANG_CVC4); - ctor.toStream(os); - return os; -} - -void DatatypeConstructor::toStream(std::ostream& out) const -{ - out << getName(); - - DatatypeConstructor::const_iterator i = begin(), i_end = end(); - if(i != i_end) { - out << "("; - do { - out << *i; - if(++i != i_end) { - out << ", "; - } - } while(i != i_end); - out << ")"; - } -} - -std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) { - // can only output datatypes in the CVC4 native language - language::SetLanguage::Scope ls(os, language::output::LANG_CVC4); - arg.toStream(os); - return os; -} - -void DatatypeConstructorArg::toStream(std::ostream& out) const -{ - std::string name = getName(); - out << name << ": "; - - Type t; - if (isResolved()) - { - t = getRangeType(); - } - else if (d_selector.isNull()) - { - string typeName = name.substr(name.find('\0') + 1); - out << ((typeName == "") ? "[self]" : typeName); - return; - } - else - { - t = d_selector.getType(); - } - out << t; -} - -std::string Datatype::getName() const -{ - ExprManagerScope ems(*d_em); - return d_internal->getName(); -} -size_t Datatype::getNumConstructors() const { return d_constructors.size(); } - -bool Datatype::isParametric() const -{ - ExprManagerScope ems(*d_em); - return d_internal->isParametric(); -} -size_t Datatype::getNumParameters() const -{ - ExprManagerScope ems(*d_em); - return d_internal->getNumParameters(); -} -Type Datatype::getParameter(unsigned int i) const -{ - CheckArgument(isParametric(), - this, - "Cannot get type parameter of a non-parametric datatype."); - CheckArgument(i < getNumParameters(), - i, - "Type parameter index out of range for datatype."); - ExprManagerScope ems(*d_em); - return d_internal->getParameter(i).toType(); -} - -std::vector Datatype::getParameters() const -{ - CheckArgument(isParametric(), - this, - "Cannot get type parameters of a non-parametric datatype."); - std::vector params; - std::vector paramsn = d_internal->getParameters(); - // convert to type - for (unsigned i = 0, nparams = paramsn.size(); i < nparams; i++) - { - params.push_back(paramsn[i].toType()); - } - return params; -} - -bool Datatype::isCodatatype() const -{ - ExprManagerScope ems(*d_em); - return d_internal->isCodatatype(); -} - -bool Datatype::isSygus() const -{ - ExprManagerScope ems(*d_em); - return d_internal->isSygus(); -} - -bool Datatype::isTuple() const -{ - ExprManagerScope ems(*d_em); - return d_internal->isTuple(); -} - -bool Datatype::isRecord() const { return d_isRecord; } - -Record* Datatype::getRecord() const { return d_record.get(); } -bool Datatype::operator!=(const Datatype& other) const -{ - return !(*this == other); -} - -bool Datatype::isResolved() const -{ - ExprManagerScope ems(*d_em); - return d_internal->isResolved(); -} -Datatype::iterator Datatype::begin() { return iterator(d_constructors, true); } - -Datatype::iterator Datatype::end() { return iterator(d_constructors, false); } - -Datatype::const_iterator Datatype::begin() const -{ - return const_iterator(d_constructors, true); -} - -Datatype::const_iterator Datatype::end() const -{ - return const_iterator(d_constructors, false); -} - -bool DatatypeConstructor::isResolved() const -{ - return d_internal->isResolved(); -} - -size_t DatatypeConstructor::getNumArgs() const { return d_args.size(); } - -DatatypeConstructor::iterator DatatypeConstructor::begin() -{ - return iterator(d_args, true); -} - -DatatypeConstructor::iterator DatatypeConstructor::end() -{ - return iterator(d_args, false); -} - -DatatypeConstructor::const_iterator DatatypeConstructor::begin() const -{ - return const_iterator(d_args, true); -} - -DatatypeConstructor::const_iterator DatatypeConstructor::end() const -{ - return const_iterator(d_args, false); -} -}/* CVC4 namespace */ diff --git a/src/expr/datatype.h b/src/expr/datatype.h deleted file mode 100644 index 0deb20d8f..000000000 --- a/src/expr/datatype.h +++ /dev/null @@ -1,933 +0,0 @@ -/********************* */ -/*! \file datatype.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A class representing a Datatype definition - ** - ** A class representing a Datatype definition for the theory of - ** inductive datatypes. - **/ - -#include "cvc4_public.h" - -#ifndef CVC4__DATATYPE_H -#define CVC4__DATATYPE_H - -#include -#include -#include -#include -#include - -namespace CVC4 { - // messy; Expr needs Datatype (because it's the payload of a - // CONSTANT-kinded expression), and Datatype needs Expr. - //class CVC4_PUBLIC Datatype; - class CVC4_PUBLIC DatatypeIndexConstant; -}/* CVC4 namespace */ - -#include "base/exception.h" -#include "expr/expr.h" -#include "expr/type.h" -#include "expr/datatype_index.h" -#include "util/hash.h" - - -namespace CVC4 { - -class CVC4_PUBLIC ExprManager; - -class CVC4_PUBLIC DatatypeConstructor; -class CVC4_PUBLIC DatatypeConstructorArg; - -class CVC4_PUBLIC DatatypeConstructorIterator { - const std::vector* d_v; - size_t d_i; - - friend class Datatype; - - DatatypeConstructorIterator(const std::vector& v, bool start) : d_v(&v), d_i(start ? 0 : v.size()) { - } - -public: - typedef const DatatypeConstructor& value_type; - const DatatypeConstructor& operator*() const { return (*d_v)[d_i]; } - const DatatypeConstructor* operator->() const { return &(*d_v)[d_i]; } - DatatypeConstructorIterator& operator++() { ++d_i; return *this; } - DatatypeConstructorIterator operator++(int) { DatatypeConstructorIterator i(*this); ++d_i; return i; } - bool operator==(const DatatypeConstructorIterator& other) const { return d_v == other.d_v && d_i == other.d_i; } - bool operator!=(const DatatypeConstructorIterator& other) const { return d_v != other.d_v || d_i != other.d_i; } -};/* class DatatypeConstructorIterator */ - -class CVC4_PUBLIC DatatypeConstructorArgIterator { - const std::vector* d_v; - size_t d_i; - - friend class DatatypeConstructor; - - DatatypeConstructorArgIterator(const std::vector& v, bool start) : d_v(&v), d_i(start ? 0 : v.size()) { - } - -public: - typedef const DatatypeConstructorArg& value_type; - const DatatypeConstructorArg& operator*() const { return (*d_v)[d_i]; } - const DatatypeConstructorArg* operator->() const { return &(*d_v)[d_i]; } - DatatypeConstructorArgIterator& operator++() { ++d_i; return *this; } - DatatypeConstructorArgIterator operator++(int) { DatatypeConstructorArgIterator i(*this); ++d_i; return i; } - bool operator==(const DatatypeConstructorArgIterator& other) const { return d_v == other.d_v && d_i == other.d_i; } - bool operator!=(const DatatypeConstructorArgIterator& other) const { return d_v != other.d_v || d_i != other.d_i; } -};/* class DatatypeConstructorArgIterator */ - -/** - * An exception that is thrown when a datatype resolution fails. - */ -class CVC4_PUBLIC DatatypeResolutionException : public Exception { - public: - inline DatatypeResolutionException(std::string msg); -};/* class DatatypeResolutionException */ - -/** - * A holder type (used in calls to DatatypeConstructor::addArg()) - * to allow a Datatype to refer to itself. Self-typed fields of - * Datatypes will be properly typed when a Type is created for the - * Datatype by the ExprManager (which calls Datatype::resolve()). - */ -class CVC4_PUBLIC DatatypeSelfType { -};/* class DatatypeSelfType */ - -class DTypeSelector; - -/** - * An unresolved type (used in calls to - * DatatypeConstructor::addArg()) to allow a Datatype to refer to - * itself or to other mutually-recursive Datatypes. Unresolved-type - * fields of Datatypes will be properly typed when a Type is created - * for the Datatype by the ExprManager (which calls - * Datatype::resolve()). - */ -class CVC4_PUBLIC DatatypeUnresolvedType { - std::string d_name; -public: - inline DatatypeUnresolvedType(std::string name); - inline std::string getName() const; -};/* class DatatypeUnresolvedType */ - -/** - * A Datatype constructor argument (i.e., a Datatype field). - */ -class CVC4_PUBLIC DatatypeConstructorArg { - friend class DatatypeConstructor; - friend class Datatype; - - public: - /** Get the name of this constructor argument. */ - std::string getName() const; - - /** - * Get the selector for this constructor argument; this call is - * only permitted after resolution. - */ - Expr getSelector() const; - - /** - * Get the associated constructor for this constructor argument; - * this call is only permitted after resolution. - */ - Expr getConstructor() const; - - /** - * Get the type of the selector for this constructor argument; - * this call is only permitted after resolution. - */ - SelectorType getType() const; - - /** - * Get the range type of this argument. - */ - Type getRangeType() const; - - /** - * Returns true iff this constructor argument has been resolved. - */ - bool isResolved() const; - - /** prints this datatype constructor argument to stream */ - void toStream(std::ostream& out) const; - - private: - /** The internal representation */ - std::shared_ptr d_internal; - /** The selector */ - Expr d_selector; - /** is this selector unresolved? */ - bool isUnresolvedSelf() const; - /** constructor */ - DatatypeConstructorArg(std::string name, Expr selector); -};/* class DatatypeConstructorArg */ - -class DTypeConstructor; - -/** - * A constructor for a Datatype. - */ -class CVC4_PUBLIC DatatypeConstructor { - friend class Datatype; - - public: - /** The type for iterators over constructor arguments. */ - typedef DatatypeConstructorArgIterator iterator; - /** The (const) type for iterators over constructor arguments. */ - typedef DatatypeConstructorArgIterator const_iterator; - - /** - * Create a new Datatype constructor with the given name for the - * constructor. The actual constructor and tester (meaning, the Exprs - * representing operators for these entities) aren't created until - * resolution time. - * weight is the value that this constructor carries when computing size. - * For example, if A, B, C have weights 0, 1, and 3 respectively, then - * C( B( A() ), B( A() ) ) has size 5. - */ - explicit DatatypeConstructor(std::string name, unsigned weight = 1); - - ~DatatypeConstructor() {} - /** - * Add an argument (i.e., a data field) of the given name and type - * to this Datatype constructor. Selector names need not be unique; - * they are for convenience and pretty-printing only. - */ - void addArg(std::string selectorName, Type selectorType); - - /** - * Add an argument (i.e., a data field) of the given name to this - * Datatype constructor that refers to an as-yet-unresolved - * Datatype (which may be mutually-recursive). Selector names need - * not be unique; they are for convenience and pretty-printing only. - */ - void addArg(std::string selectorName, DatatypeUnresolvedType selectorType); - - /** - * Add a self-referential (i.e., a data field) of the given name - * to this Datatype constructor that refers to the enclosing - * Datatype. For example, using the familiar "nat" Datatype, to - * create the "pred" field for "succ" constructor, one uses - * succ::addArg("pred", DatatypeSelfType())---the actual Type - * cannot be passed because the Datatype is still under - * construction. Selector names need not be unique; they are for - * convenience and pretty-printing only. - * - * This is a special case of - * DatatypeConstructor::addArg(std::string, DatatypeUnresolvedType). - */ - void addArg(std::string selectorName, DatatypeSelfType); - - /** Get the name of this Datatype constructor. */ - std::string getName() const; - - /** - * Get the constructor operator of this Datatype constructor. The - * Datatype must be resolved. - */ - Expr getConstructor() const; - - /** - * Get the tester operator of this Datatype constructor. The - * Datatype must be resolved. - */ - Expr getTester() const; - - /** get sygus op - * - * This method returns the operator or - * term that this constructor represents - * in the sygus encoding. This may be a - * builtin operator, defined function, variable, - * or constant that this constructor encodes in this - * deep embedding. - */ - Expr getSygusOp() const; - /** is this a sygus identity function? - * - * This returns true if the sygus operator of this datatype constructor is - * of the form (lambda (x) x). - */ - bool isSygusIdFunc() const; - /** get weight - * - * Get the weight of this constructor. This value is used when computing the - * size of datatype terms that involve this constructor. - */ - unsigned getWeight() const; - - /** - * Get the number of arguments (so far) of this Datatype constructor. - */ - size_t getNumArgs() const; - - /** - * Get the specialized constructor type for a parametric - * constructor; this call is only permitted after resolution. - * Given a (concrete) returnType, the constructor's concrete - * type in this parametric datatype is returned. - * - * For instance, if the datatype is list[T], with constructor - * "cons[T]" of type "T -> list[T] -> list[T]", then calling - * this function with "list[int]" will return the concrete - * "cons" constructor type for lists of int---namely, - * "int -> list[int] -> list[int]". - */ - Type getSpecializedConstructorType(Type returnType) const; - - /** - * Return the cardinality of this constructor (the product of the - * cardinalities of its arguments). - */ - Cardinality getCardinality(Type t) const; - - /** - * Return true iff this constructor is finite (it is nullary or - * each of its argument types are finite). This function can - * only be called for resolved constructors. - */ - bool isFinite(Type t) const; - /** - * Return true iff this constructor is finite (it is nullary or - * each of its argument types are finite) under assumption - * uninterpreted sorts are finite. This function can - * only be called for resolved constructors. - */ - bool isInterpretedFinite(Type t) const; - - /** - * Returns true iff this Datatype constructor has already been - * resolved. - */ - bool isResolved() const; - - /** Get the beginning iterator over DatatypeConstructor args. */ - iterator begin(); - /** Get the ending iterator over DatatypeConstructor args. */ - iterator end(); - /** Get the beginning const_iterator over DatatypeConstructor args. */ - const_iterator begin() const; - /** Get the ending const_iterator over DatatypeConstructor args. */ - const_iterator end() const; - - /** Get the ith DatatypeConstructor arg. */ - const DatatypeConstructorArg& operator[](size_t index) const; - - /** - * Get the DatatypeConstructor arg named. This is a linear search - * through the arguments, so in the case of multiple, - * similarly-named arguments, the first is returned. - */ - const DatatypeConstructorArg& operator[](std::string name) const; - - /** - * Get the selector named. This is a linear search - * through the arguments, so in the case of multiple, - * similarly-named arguments, the selector for the first - * is returned. - */ - Expr getSelector(std::string name) const; - /** - * Get argument type. Returns the return type of the i^th selector of this - * constructor. - */ - Type getArgType(unsigned i) const; - - /** get selector internal - * - * This gets selector for the index^th argument - * of this constructor. The type dtt is the datatype - * type whose datatype is the owner of this constructor, - * where this type may be an instantiated parametric datatype. - * - * If shared selectors are enabled, - * this returns a shared (constructor-agnotic) selector, which - * in the terminology of "Datatypes with Shared Selectors", is: - * sel_{dtt}^{T,atos(T,C,index)} - * where C is this constructor, and T is the type - * of the index^th field of this constructor. - * The semantics of sel_{dtt}^{T,n}( t ) is the n^th field of - * type T of constructor term t if one exists, or is - * unconstrained otherwise. - */ - Expr getSelectorInternal(Type dtt, size_t index) const; - - /** get selector index internal - * - * This gets the argument number of this constructor - * that the selector sel accesses. It returns -1 if the - * selector sel is not a selector for this constructor. - * - * In the terminology of "Datatypes with Shared Selectors", - * if sel is sel_{dtt}^{T,index} for some (T, index), where - * dtt is the datatype type whose datatype is the owner - * of this constructor, then this method returns - * stoa(T,C,index) - */ - int getSelectorIndexInternal( Expr sel ) const; - - /** involves external type - * - * Get whether this constructor has a subfield - * in any constructor that is not a datatype type. - */ - bool involvesExternalType() const; - /** involves external type - * - * Get whether this constructor has a subfield - * in any constructor that is an uninterpreted type. - */ - bool involvesUninterpretedType() const; - - /** set sygus - * - * Set that this constructor is a sygus datatype constructor that encodes - * operator op. spc is the sygus callback of this datatype constructor, - * which is stored in a shared pointer. - */ - void setSygus(Expr op); - - /** - * Get the list of arguments to this constructor. - */ - const std::vector* getArgs() const; - - /** prints this datatype constructor to stream */ - void toStream(std::ostream& out) const; - - private: - /** The internal representation */ - std::shared_ptr d_internal; - /** The constructor */ - Expr d_constructor; - /** the arguments of this constructor */ - std::vector d_args; -};/* class DatatypeConstructor */ - -class DType; - -/** - * The representation of an inductive datatype. - * - * This is far more complicated than it first seems. Consider this - * datatype definition: - * - * DATATYPE nat = - * succ(pred: nat) - * | zero - * END; - * - * You cannot define "nat" until you have a Type for it, but you - * cannot have a Type for it until you fill in the type of the "pred" - * selector, which needs the Type. So we have a chicken-and-egg - * problem. It's even more complicated when we have mutual recursion - * between datatypes, since the CVC presentation language does not - * require forward-declarations. Here, we define trees of lists that - * contain trees of lists (etc): - * - * DATATYPE - * tree = node(left: tree, right: tree) | leaf(list), - * list = cons(car: tree, cdr: list) | nil - * END; - * - * Note that while parsing the "tree" definition, we have to take it - * on faith that "list" is a valid type. We build Datatype objects to - * describe "tree" and "list", and their constructors and constructor - * arguments, but leave any unknown types (including self-references) - * in an "unresolved" state. After parsing the whole DATATYPE block, - * we create a DatatypeType through - * ExprManager::mkMutualDatatypeTypes(). The ExprManager creates a - * DatatypeType for each, but before "releasing" this type into the - * wild, it does a round of in-place "resolution" on each Datatype by - * calling Datatype::resolve() with a map of string -> DatatypeType to - * allow the datatype to construct the necessary testers and - * selectors. - * - * An additional point to make is that we want to ease the burden on - * both the parser AND the users of the CVC4 API, so this class takes - * on the task of generating its own selectors and testers, for - * instance. That means that, after reifying the Datatype with the - * ExprManager, the parser needs to go through the (now-resolved) - * Datatype and request the constructor, selector, and tester terms. - * See src/parser/parser.cpp for how this is done. For API usage - * ideas, see test/unit/util/datatype_black.h. - * - * Datatypes may also be defined parametrically, such as this example: - * - * DATATYPE - * list[T] = cons(car : T, cdr : list[T]) | null, - * tree = node(children : list[tree]) | leaf - * END; - * - * Here, the definition of the parametric datatype list, where T is a type variable. - * In other words, this defines a family of types list[C] where C is any concrete - * type. Datatypes can be parameterized over multiple type variables using the - * syntax sym[ T1, ..., Tn ] = ..., - * - */ -class CVC4_PUBLIC Datatype { - friend class DatatypeConstructor; - friend class ExprManager; // for access to resolve() - friend class NodeManager; // temporary, for access to d_internal - public: - /** - * Get the datatype of a constructor, selector, or tester operator. - */ - static const Datatype& datatypeOf(Expr item) CVC4_PUBLIC; - - /** - * Get the index of a constructor or tester in its datatype, or the - * index of a selector in its constructor. (Zero is always the - * first index.) - */ - static size_t indexOf(Expr item) CVC4_PUBLIC; - - /** - * Get the index of constructor corresponding to selector. (Zero is - * always the first index.) - */ - static size_t cindexOf(Expr item) CVC4_PUBLIC; - - /** - * Same as above, but without checks. These methods should be used by - * internal (Node-level) code. - */ - static size_t indexOfInternal(Expr item); - static size_t cindexOfInternal(Expr item); - - /** The type for iterators over constructors. */ - typedef DatatypeConstructorIterator iterator; - /** The (const) type for iterators over constructors. */ - typedef DatatypeConstructorIterator const_iterator; - - /** Create a new Datatype of the given name. */ - explicit Datatype(ExprManager* em, std::string name, bool isCo = false); - - /** - * Create a new Datatype of the given name, with the given - * parameterization. - */ - Datatype(ExprManager* em, - std::string name, - const std::vector& params, - bool isCo = false); - - ~Datatype(); - - /** Add a constructor to this Datatype. - * - * Notice that constructor names need not - * be unique; they are for convenience and pretty-printing only. - */ - void addConstructor(const DatatypeConstructor& c); - - /** set sygus - * - * This marks this datatype as a sygus datatype. - * A sygus datatype is one that represents terms of type st - * via a deep embedding described in Section 4 of - * Reynolds et al. CAV 2015. We say that this sygus datatype - * "encodes" its sygus type st in the following. - * - * st : the type this datatype encodes (this can be Int, Bool, etc.), - * bvl : the list of arguments for the synth-fun - * allow_const : whether all constants are (implicitly) allowed by the - * datatype - * allow_all : whether all terms are (implicitly) allowed by the datatype - * - * Notice that allow_const/allow_all do not reflect the constructors - * for this datatype, and instead are used solely for relaxing constraints - * when doing solution reconstruction (Figure 5 of Reynolds et al. - * CAV 2015). - */ - void setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ); - /** add sygus constructor - * - * This adds a sygus constructor to this datatype, where - * this datatype should be currently unresolved. - * - * op : the builtin operator, constant, or variable that - * this constructor encodes - * cname : the name of the constructor (for printing only) - * cargs : the arguments of the constructor - * - * It should be the case that cargs are sygus datatypes that - * encode the arguments of op. For example, a sygus constructor - * with op = PLUS should be such that cargs.size()>=2 and - * the sygus type of cargs[i] is Real/Int for each i. - * - * weight denotes the value added by the constructor when computing the size - * of datatype terms. Passing a value <0 denotes the default weight for the - * constructor, which is 0 for nullary constructors and 1 for non-nullary - * constructors. - */ - void addSygusConstructor(Expr op, - const std::string& cname, - const std::vector& cargs, - int weight = -1); - /** - * Same as above, with builtin kind k. - */ - void addSygusConstructor(Kind k, - const std::string& cname, - const std::vector& cargs, - int weight = -1); - - /** set that this datatype is a tuple */ - void setTuple(); - - /** set that this datatype is a record */ - void setRecord(); - - /** Get the name of this Datatype. */ - std::string getName() const; - - /** Get the number of constructors (so far) for this Datatype. */ - size_t getNumConstructors() const; - - /** Is this datatype parametric? */ - bool isParametric() const; - - /** Get the nubmer of type parameters */ - size_t getNumParameters() const; - - /** Get parameter */ - Type getParameter(unsigned int i) const; - - /** Get parameters */ - std::vector getParameters() const; - - /** is this a co-datatype? */ - bool isCodatatype() const; - - /** is this a sygus datatype? */ - bool isSygus() const; - - /** is this a tuple datatype? */ - bool isTuple() const; - - /** is this a record datatype? */ - bool isRecord() const; - - /** get the record representation for this datatype */ - Record* getRecord() const; - - /** - * Return the cardinality of this datatype. - * The Datatype must be resolved. - * - * The version of this method that takes Type t is required - * for parametric datatypes, where t is an instantiated - * parametric datatype type whose datatype is this class. - */ - Cardinality getCardinality(Type t) const; - Cardinality getCardinality() const; - - /** - * Return true iff this Datatype has finite cardinality. If the - * datatype is not well-founded, this method returns false. The - * Datatype must be resolved or an exception is thrown. - * - * The version of this method that takes Type t is required - * for parametric datatypes, where t is an instantiated - * parametric datatype type whose datatype is this class. - */ - bool isFinite(Type t) const; - bool isFinite() const; - - /** - * Return true iff this Datatype is finite (all constructors are - * finite, i.e., there are finitely many ground terms) under the - * assumption unintepreted sorts are finite. If the - * datatype is not well-founded, this method returns false. The - * Datatype must be resolved or an exception is thrown. - * - * The versions of these methods that takes Type t is required - * for parametric datatypes, where t is an instantiated - * parametric datatype type whose datatype is this class. - */ - bool isInterpretedFinite(Type t) const; - bool isInterpretedFinite() const; - - /** is well-founded - * - * Return true iff this datatype is well-founded (there exist finite - * values of this type). - * This datatype must be resolved or an exception is thrown. - */ - bool isWellFounded() const; - /** has nested recursion - * - * Return true iff this datatype has nested recursion. - * This datatype must be resolved or an exception is thrown. - */ - bool hasNestedRecursion() const; - - /** is recursive singleton - * - * Return true iff this datatype is a recursive singleton - * (a recursive singleton is a recursive datatype with only - * one infinite value). For details, see Reynolds et al. CADE 2015. - * - * The versions of these methods that takes Type t is required - * for parametric datatypes, where t is an instantiated - * parametric datatype type whose datatype is this class. - */ - bool isRecursiveSingleton(Type t) const; - bool isRecursiveSingleton() const; - - /** recursive single arguments - * - * Get recursive singleton argument types (uninterpreted sorts that the - * cardinality of this datatype is dependent upon). For example, for : - * stream := cons( head1 : U1, head2 : U2, tail : stream ) - * Then, the recursive singleton argument types of stream are { U1, U2 }, - * since if U1 and U2 have cardinality one, then stream has cardinality - * one as well. - * - * The versions of these methods that takes Type t is required - * for parametric datatypes, where t is an instantiated - * parametric datatype type whose datatype is this class. - */ - unsigned getNumRecursiveSingletonArgTypes(Type t) const; - Type getRecursiveSingletonArgType(Type t, unsigned i) const; - unsigned getNumRecursiveSingletonArgTypes() const; - Type getRecursiveSingletonArgType(unsigned i) const; - - /** - * Construct and return a ground term of this Datatype. The - * Datatype must be both resolved and well-founded, or else an - * exception is thrown. - * - * This method takes a Type t, which is a datatype type whose - * datatype is this class, which may be an instantiated datatype - * type if this datatype is parametric. - */ - Expr mkGroundTerm(Type t) const; - /** Make ground value - * - * Same as above, but constructs a constant value instead of a ground term. - * These two notions typically coincide. However, for uninterpreted sorts, - * they do not: mkGroundTerm returns a fresh variable whereas mkValue returns - * an uninterpreted constant. The motivation for mkGroundTerm is that - * unintepreted constants should never appear in lemmas. The motivation for - * mkGroundValue is for things like type enumeration and model construction. - */ - Expr mkGroundValue(Type t) const; - - /** - * Get the DatatypeType associated to this Datatype. Can only be - * called post-resolution. - */ - DatatypeType getDatatypeType() const; - - /** - * Get the DatatypeType associated to this (parameterized) Datatype. Can only be - * called post-resolution. - */ - DatatypeType getDatatypeType(const std::vector& params) const; - - /** - * Return true iff the two Datatypes are the same. - * - * We need == for mkConst(Datatype) to properly work---since if the - * Datatype Expr requested is the same as an already-existing one, - * we need to return that one. For that, we have a hash and - * operator==. We provide != for symmetry. We don't provide - * operator<() etc. because given two Datatype Exprs, you could - * simply compare those rather than the (bare) Datatypes. This - * means, though, that Datatype cannot be stored in a sorted list or - * RB tree directly, so maybe we can consider adding these - * comparison operators later on. - */ - bool operator==(const Datatype& other) const; - /** Return true iff the two Datatypes are not the same. */ - bool operator!=(const Datatype& other) const; - - /** Return true iff this Datatype has already been resolved. */ - bool isResolved() const; - - /** Get the beginning iterator over DatatypeConstructors. */ - iterator begin(); - /** Get the ending iterator over DatatypeConstructors. */ - iterator end(); - /** Get the beginning const_iterator over DatatypeConstructors. */ - const_iterator begin() const; - /** Get the ending const_iterator over DatatypeConstructors. */ - const_iterator end() const; - - /** Get the ith DatatypeConstructor. */ - const DatatypeConstructor& operator[](size_t index) const; - - /** - * Get the DatatypeConstructor named. This is a linear search - * through the constructors, so in the case of multiple, - * similarly-named constructors, the first is returned. - */ - const DatatypeConstructor& operator[](std::string name) const; - - /** - * Get the constructor operator for the named constructor. - * This is a linear search through the constructors, so in - * the case of multiple, similarly-named constructors, the - * first is returned. - * - * This Datatype must be resolved. - */ - Expr getConstructor(std::string name) const; - - /** get sygus type - * This gets the built-in type associated with - * this sygus datatype, i.e. the type of the - * term that this sygus datatype encodes. - */ - Type getSygusType() const; - - /** get sygus var list - * This gets the variable list of the function - * to synthesize using this sygus datatype. - * For example, if we are synthesizing a binary - * function f where solutions are of the form: - * f = (lambda (xy) t[x,y]) - * In this case, this method returns the - * bound variable list containing x and y. - */ - Expr getSygusVarList() const; - /** get sygus allow constants - * - * Does this sygus datatype allow constants? - * Notice that this is not a property of the - * constructors of this datatype. Instead, it is - * an auxiliary flag (provided in the call - * to setSygus). - */ - bool getSygusAllowConst() const; - /** get sygus allow all - * - * Does this sygus datatype allow all terms? - * Notice that this is not a property of the - * constructors of this datatype. Instead, it is - * an auxiliary flag (provided in the call - * to setSygus). - */ - bool getSygusAllowAll() const; - - /** involves external type - * Get whether this datatype has a subfield - * in any constructor that is not a datatype type. - */ - bool involvesExternalType() const; - /** involves uninterpreted type - * Get whether this datatype has a subfield - * in any constructor that is an uninterpreted type. - */ - bool involvesUninterpretedType() const; - - /** - * Get the list of constructors. - */ - const std::vector* getConstructors() const; - - /** prints this datatype to stream */ - void toStream(std::ostream& out) const; - - private: - /** The expression manager that created this datatype */ - ExprManager* d_em; - /** The internal representation */ - std::shared_ptr d_internal; - /** self type */ - Type d_self; - /** the data of the record for this datatype (if applicable) */ - std::shared_ptr d_record; - /** whether the datatype is a record */ - bool d_isRecord; - /** the constructors of this datatype */ - std::vector d_constructors; - /** - * Datatypes refer to themselves, recursively, and we have a - * chicken-and-egg problem. The DatatypeType around the Datatype - * cannot exist until the Datatype is finalized, and the Datatype - * cannot refer to the DatatypeType representing itself until it - * exists. resolve() is called by the ExprManager when a Type is - * ultimately requested of the Datatype specification (that is, when - * ExprManager::mkDatatypeType() or ExprManager::mkMutualDatatypeTypes() - * is called). Has the effect of freezing the object, too; that is, - * addConstructor() will fail after a call to resolve(). - * - * The basic goal of resolution is to assign constructors, selectors, - * and testers. To do this, any UnresolvedType/SelfType references - * must be cleared up. This is the purpose of the "resolutions" map; - * it includes any mutually-recursive datatypes that are currently - * under resolution. The four vectors come in two pairs (so, really - * they are two maps). placeholders->replacements give type variables - * that should be resolved in the case of parametric datatypes. - * - * @param resolutions a map of strings to DatatypeTypes currently under - * resolution - * @param placeholders the types in these Datatypes under resolution that must - * be replaced - * @param replacements the corresponding replacements - * @param paramTypes the sort constructors in these Datatypes under resolution - * that must be replaced - * @param paramReplacements the corresponding (parametric) DatatypeTypes - */ - void resolve(const std::map& resolutions, - const std::vector& placeholders, - const std::vector& replacements, - const std::vector& paramTypes, - const std::vector& paramReplacements); -};/* class Datatype */ - -/** - * A hash function for Datatypes. Needed to store them in hash sets - * and hash maps. - */ -struct CVC4_PUBLIC DatatypeHashFunction { - inline size_t operator()(const Datatype& dt) const { - return std::hash()(dt.getName()); - } - inline size_t operator()(const Datatype* dt) const { - return std::hash()(dt->getName()); - } - inline size_t operator()(const DatatypeConstructor& dtc) const { - return std::hash()(dtc.getName()); - } - inline size_t operator()(const DatatypeConstructor* dtc) const { - return std::hash()(dtc->getName()); - } -};/* struct DatatypeHashFunction */ - - -// FUNCTION DECLARATIONS FOR OUTPUT STREAMS - -std::ostream& operator<<(std::ostream& os, const Datatype& dt) CVC4_PUBLIC; -std::ostream& operator<<(std::ostream& os, const DatatypeConstructor& ctor) CVC4_PUBLIC; -std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) CVC4_PUBLIC; - -// INLINE FUNCTIONS - -inline DatatypeResolutionException::DatatypeResolutionException(std::string msg) : - Exception(msg) { -} - -inline DatatypeUnresolvedType::DatatypeUnresolvedType(std::string name) : - d_name(name) { -} - -inline std::string DatatypeUnresolvedType::getName() const { return d_name; } - - -}/* CVC4 namespace */ - -#endif /* CVC4__DATATYPE_H */ diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index bfc33ef87..fa9bb9793 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -245,6 +245,45 @@ void DType::addSygusConstructor(Node op, void DType::setSygus(TypeNode st, Node bvl, bool allowConst, bool allowAll) { Assert(!d_resolved); + // We can be in a case where the only rule specified was + // (Constant T), in which case we have not yet added a constructor. We + // ensure an arbitrary constant is added in this case. We additionally + // add a constant if the grammar has only non-nullary constructors, since this + // ensures the datatype is well-founded (see 3423). + // Notice we only want to do this for sygus datatypes that are user-provided. + // At the moment, the condition !allow_all implies the grammar is + // user-provided and hence may require a default constant. + // TODO (https://github.com/CVC4/cvc4-projects/issues/38): + // In an API for SyGuS, it probably makes more sense for the user to + // explicitly add the "any constant" constructor with a call instead of + // passing a flag. This would make the block of code unnecessary. + if (allowConst && !allowAll) + { + // if I don't already have a constant (0-ary constructor) + bool hasConstant = false; + for (size_t i = 0, ncons = getNumConstructors(); i < ncons; i++) + { + if ((*this)[i].getNumArgs() == 0) + { + hasConstant = true; + break; + } + } + if (!hasConstant) + { + // add an arbitrary one + Node op = st.mkGroundTerm(); + // use same naming convention as SygusDatatype + std::stringstream ss; + ss << getName() << "_" << getNumConstructors() << "_" << op; + // it has zero weight + std::shared_ptr c = + std::make_shared(ss.str(), 0); + c->setSygus(op); + addConstructor(c); + } + } + d_sygusType = st; d_sygusBvl = bvl; d_sygusAllowConst = allowConst || allowAll; diff --git a/src/expr/dtype.h b/src/expr/dtype.h index f48997748..44482c6cf 100644 --- a/src/expr/dtype.h +++ b/src/expr/dtype.h @@ -77,7 +77,6 @@ typedef expr::Attribute DTypeUFiniteComputedAttr; // ----------------------- end datatype attributes class NodeManager; -class Datatype; /** * The Node-level representation of an inductive datatype, which currently @@ -141,7 +140,6 @@ class Datatype; */ class DType { - friend class Datatype; friend class DTypeConstructor; friend class NodeManager; // for access to resolve() diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 66824c07a..0d22a3c41 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -114,8 +114,6 @@ ExprManager::~ExprManager() } } #endif - // clear the datatypes - d_ownedDatatypes.clear(); delete d_nodeManager; d_nodeManager = NULL; @@ -597,20 +595,6 @@ FunctionType ExprManager::mkPredicateType(const std::vector& sorts) { return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkPredicateType(sortNodes)))); } -DatatypeType ExprManager::mkTupleType(const std::vector& types) { - NodeManagerScope nms(d_nodeManager); - std::vector typeNodes; - for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) { - typeNodes.push_back(*types[i].d_typeNode); - } - return DatatypeType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes)))); -} - -DatatypeType ExprManager::mkRecordType(const Record& rec) { - NodeManagerScope nms(d_nodeManager); - return DatatypeType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkRecordType(rec)))); -} - SExprType ExprManager::mkSExprType(const std::vector& types) { NodeManagerScope nms(d_nodeManager); std::vector typeNodes; @@ -648,195 +632,6 @@ SequenceType ExprManager::mkSequenceType(Type elementType) const new TypeNode(d_nodeManager->mkSequenceType(*elementType.d_typeNode)))); } -DatatypeType ExprManager::mkDatatypeType(Datatype& datatype, uint32_t flags) -{ - // Not worth a special implementation; this doesn't need to be fast - // code anyway. - vector datatypes; - datatypes.push_back(datatype); - std::vector result = mkMutualDatatypeTypes(datatypes, flags); - Assert(result.size() == 1); - return result.front(); -} - -std::vector ExprManager::mkMutualDatatypeTypes( - std::vector& datatypes, uint32_t flags) -{ - std::set unresolvedTypes; - return mkMutualDatatypeTypes(datatypes, unresolvedTypes, flags); -} - -std::vector ExprManager::mkMutualDatatypeTypes( - std::vector& datatypes, - std::set& unresolvedTypes, - uint32_t flags) -{ - NodeManagerScope nms(d_nodeManager); - std::map nameResolutions; - std::vector dtts; - - // have to build deep copy so that datatypes will live in this class - std::vector< Datatype* > dt_copies; - for(std::vector::iterator i = datatypes.begin(), i_end = datatypes.end(); i != i_end; ++i) { - d_ownedDatatypes.push_back(std::unique_ptr(new Datatype(*i))); - dt_copies.push_back(d_ownedDatatypes.back().get()); - } - - // First do some sanity checks, set up the final Type to be used for - // each datatype, and set up the "named resolutions" used to handle - // simple self- and mutual-recursion, for example in the definition - // "nat = succ(pred:nat) | zero", a named resolution can handle the - // pred selector. - for(std::vector::iterator i = dt_copies.begin(), i_end = dt_copies.end(); i != i_end; ++i) { - TypeNode* typeNode; - // register datatype with the node manager - size_t index = d_nodeManager->registerDatatype((*i)->d_internal); - if( (*i)->getNumParameters() == 0 ) { - typeNode = new TypeNode(d_nodeManager->mkTypeConst(DatatypeIndexConstant(index))); - //typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i)); - } else { - TypeNode cons = d_nodeManager->mkTypeConst(DatatypeIndexConstant(index)); - //TypeNode cons = d_nodeManager->mkTypeConst(*i); - std::vector< TypeNode > params; - params.push_back( cons ); - for( unsigned int ip = 0; ip < (*i)->getNumParameters(); ++ip ) { - params.push_back( TypeNode::fromType( (*i)->getParameter( ip ) ) ); - } - - typeNode = new TypeNode(d_nodeManager->mkTypeNode(kind::PARAMETRIC_DATATYPE, params)); - } - Type type(d_nodeManager, typeNode); - DatatypeType dtt(type); - PrettyCheckArgument( - nameResolutions.find((*i)->getName()) == nameResolutions.end(), - dt_copies, - "cannot construct two datatypes at the same time " - "with the same name `%s'", - (*i)->getName().c_str()); - nameResolutions.insert(std::make_pair((*i)->getName(), dtt)); - dtts.push_back(dtt); - } - - // Second, set up the type substitution map for complex type - // resolution (e.g. if "list" is the type we're defining, and it has - // a selector of type "ARRAY INT OF list", this can't be taken care - // of using the named resolutions that we set up above. A - // preliminary array type was set up, and now needs to have "list" - // substituted in it for the correct type. - // - // @TODO get rid of named resolutions altogether and handle - // everything with these resolutions? - std::vector< SortConstructorType > paramTypes; - std::vector< DatatypeType > paramReplacements; - std::vector placeholders;// to hold the "unresolved placeholders" - std::vector replacements;// to hold our final, resolved types - for(std::set::iterator i = unresolvedTypes.begin(), i_end = unresolvedTypes.end(); i != i_end; ++i) { - std::string name; - if( (*i).isSort() ) { - name = SortType(*i).getName(); - } else { - Assert((*i).isSortConstructor()); - name = SortConstructorType(*i).getName(); - } - std::map::const_iterator resolver = - nameResolutions.find(name); - PrettyCheckArgument( - resolver != nameResolutions.end(), - unresolvedTypes, - "cannot resolve type `%s'; it's not among " - "the datatypes being defined", name.c_str()); - // We will instruct the Datatype to substitute "*i" (the - // unresolved SortType used as a placeholder in complex types) - // with "(*resolver).second" (the DatatypeType we created in the - // first step, above). - if( (*i).isSort() ) { - placeholders.push_back(*i); - replacements.push_back( (*resolver).second ); - } else { - Assert((*i).isSortConstructor()); - paramTypes.push_back( SortConstructorType(*i) ); - paramReplacements.push_back( (*resolver).second ); - } - } - - // Lastly, perform the final resolutions and checks. - std::vector tns; - for(std::vector::iterator i = dtts.begin(), - i_end = dtts.end(); - i != i_end; - ++i) { - const Datatype& dt = (*i).getDatatype(); - if(!dt.isResolved()) { - const_cast(dt).resolve(nameResolutions, - placeholders, - replacements, - paramTypes, - paramReplacements); - } - - // Now run some checks, including a check to make sure that no - // selector is function-valued. - checkResolvedDatatype(*i); - tns.push_back(TypeNode::fromType(*i)); - } - - for(std::vector::iterator i = d_nodeManager->d_listeners.begin(); i != d_nodeManager->d_listeners.end(); ++i) { - (*i)->nmNotifyNewDatatypes(tns, flags); - } - - return dtts; -} - -void ExprManager::checkResolvedDatatype(DatatypeType dtt) const { - const Datatype& dt = dtt.getDatatype(); - - AssertArgument(dt.isResolved(), dtt, "datatype should have been resolved"); - - // for all constructors... - for(Datatype::const_iterator i = dt.begin(), i_end = dt.end(); - i != i_end; - ++i) { - const DatatypeConstructor& c = *i; - Type testerType CVC4_UNUSED = c.getTester().getType(); - Assert(c.isResolved() && testerType.isTester() - && TesterType(testerType).getDomain() == dtt - && TesterType(testerType).getRangeType() == booleanType()) - << "malformed tester in datatype post-resolution"; - Type ctorType CVC4_UNUSED = c.getConstructor().getType(); - Assert(ctorType.isConstructor() - && ConstructorType(ctorType).getArity() == c.getNumArgs() - && ConstructorType(ctorType).getRangeType() == dtt) - << "malformed constructor in datatype post-resolution"; - // for all selectors... - for(DatatypeConstructor::const_iterator j = c.begin(), j_end = c.end(); - j != j_end; - ++j) { - const DatatypeConstructorArg& a = *j; - Type selectorType = a.getType(); - Assert(a.isResolved() && selectorType.isSelector() - && SelectorType(selectorType).getDomain() == dtt) - << "malformed selector in datatype post-resolution"; - // This next one's a "hard" check, performed in non-debug builds - // as well; the other ones should all be guaranteed by the - // CVC4::Datatype class, but this actually needs to be checked. - AlwaysAssert(!SelectorType(selectorType) - .getRangeType() - .d_typeNode->isFunctionLike()) - << "cannot put function-like things in datatypes"; - } - } -} - -SelectorType ExprManager::mkSelectorType(Type domain, Type range) const { - NodeManagerScope nms(d_nodeManager); - return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSelectorType(*domain.d_typeNode, *range.d_typeNode))); -} - -TesterType ExprManager::mkTesterType(Type domain) const { - NodeManagerScope nms(d_nodeManager); - return Type(d_nodeManager, new TypeNode(d_nodeManager->mkTesterType(*domain.d_typeNode))); -} - SortType ExprManager::mkSort(const std::string& name, uint32_t flags) const { NodeManagerScope nms(d_nodeManager); return SortType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name, flags)))); @@ -1110,13 +905,6 @@ Type ExprManager::exportType(const Type& t, ExprManager* em, ExprManagerMapColle new TypeNode(expr::exportTypeInternal(*t.d_typeNode, t.d_nodeManager, em->d_nodeManager, vmap))); } -const Datatype& ExprManager::getDatatypeForIndex(unsigned index) const -{ - // when the Node-level API is in place, this function will be deleted. - Assert(index < d_ownedDatatypes.size()); - return *d_ownedDatatypes[index]; -} - ${mkConst_implementations} }/* CVC4 namespace */ diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 2b9a85aca..a6fce56a2 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -64,11 +64,6 @@ class CVC4_PUBLIC ExprManager { */ NodeManager* getNodeManager() const; - /** - * Check some things about a newly-created DatatypeType. - */ - void checkResolvedDatatype(DatatypeType dtt) const; - /** * SmtEngine will use all the internals, so it will grab the * NodeManager. @@ -84,10 +79,6 @@ class CVC4_PUBLIC ExprManager { // undefined, private copy constructor and assignment op (disallow copy) ExprManager(const ExprManager&) = delete; ExprManager& operator=(const ExprManager&) = delete; - - /** A list of datatypes owned by this expr manager. */ - std::vector > d_ownedDatatypes; - /** Creates an expression manager. */ ExprManager(); public: @@ -345,18 +336,6 @@ class CVC4_PUBLIC ExprManager { */ FunctionType mkPredicateType(const std::vector& sorts); - /** - * Make a tuple type with types from - * types[0..types.size()-1]. types must - * have at least one element. - */ - DatatypeType mkTupleType(const std::vector& types); - - /** - * Make a record type with types from the rec parameter. - */ - DatatypeType mkRecordType(const Record& rec); - /** * Make a symbolic expressiontype with types from * types[0..types.size()-1]. types may @@ -379,68 +358,6 @@ class CVC4_PUBLIC ExprManager { /** Make the type of sequence with the given parameterization. */ SequenceType mkSequenceType(Type elementType) const; - /** Bits for use in mkDatatypeType() flags. - * - * DATATYPE_FLAG_PLACEHOLDER indicates that the type should not be printed - * out as a definition, for example, in models or during dumping. - */ - enum - { - DATATYPE_FLAG_NONE = 0, - DATATYPE_FLAG_PLACEHOLDER = 1 - }; /* enum */ - - /** Make a type representing the given datatype. */ - DatatypeType mkDatatypeType(Datatype& datatype, - uint32_t flags = DATATYPE_FLAG_NONE); - - /** - * Make a set of types representing the given datatypes, which may be - * mutually recursive. - */ - std::vector mkMutualDatatypeTypes( - std::vector& datatypes, uint32_t flags = DATATYPE_FLAG_NONE); - - /** - * Make a set of types representing the given datatypes, which may - * be mutually recursive. unresolvedTypes is a set of SortTypes - * that were used as placeholders in the Datatypes for the Datatypes - * of the same name. This is just a more complicated version of the - * above mkMutualDatatypeTypes() function, but is required to handle - * complex types. - * - * For example, unresolvedTypes might contain the single sort "list" - * (with that name reported from SortType::getName()). The - * datatypes list might have the single datatype - * - * DATATYPE - * list = cons(car:ARRAY INT OF list, cdr:list) | nil; - * END; - * - * To represent the Type of the array, the user had to create a - * placeholder type (an uninterpreted sort) to stand for "list" in - * the type of "car". It is this placeholder sort that should be - * passed in unresolvedTypes. If the datatype was of the simpler - * form: - * - * DATATYPE - * list = cons(car:list, cdr:list) | nil; - * END; - * - * then no complicated Type needs to be created, and the above, - * simpler form of mkMutualDatatypeTypes() is enough. - */ - std::vector mkMutualDatatypeTypes( - std::vector& datatypes, - std::set& unresolvedTypes, - uint32_t flags = DATATYPE_FLAG_NONE); - - /** Make a type representing a selector with the given parameterization. */ - SelectorType mkSelectorType(Type domain, Type range) const; - - /** Make a type representing a tester with the given parameterization. */ - TesterType mkTesterType(Type domain) const; - /** Bits for use in mkSort() flags. */ enum { SORT_FLAG_NONE = 0, @@ -573,13 +490,6 @@ class CVC4_PUBLIC ExprManager { * maximal arity as the maximal possible number of children of a node. **/ static bool isNAryKind(Kind fun); - - /** - * Return the datatype at the given index owned by this class. Type nodes are - * associated with datatypes through the DatatypeIndexConstant class. The - * argument index is intended to be a value taken from that class. - */ - const Datatype& getDatatypeForIndex(unsigned index) const; };/* class ExprManager */ ${mkConst_instantiations} diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index bcddc23f5..0f2db7869 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -207,6 +207,8 @@ size_t NodeManager::registerDatatype(std::shared_ptr dt) const DType& NodeManager::getDTypeForIndex(size_t index) const { + // if this assertion fails, it is likely due to not managing datatypes + // properly w.r.t. multiple NodeManagers. Assert(index < d_registeredDTypes.size()); return *d_registeredDTypes[index]; } @@ -635,18 +637,19 @@ TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vecto for (unsigned i = 0; i < types.size(); ++ i) { sst << "_" << types[i]; } - Datatype dt(nm->toExprManager(), sst.str()); + DType dt(sst.str()); dt.setTuple(); std::stringstream ssc; ssc << sst.str() << "_ctor"; - DatatypeConstructor c(ssc.str()); + std::shared_ptr c = + std::make_shared(ssc.str()); for (unsigned i = 0; i < types.size(); ++ i) { std::stringstream ss; ss << sst.str() << "_stor_" << i; - c.addArg(ss.str().c_str(), types[i].toType()); + c->addArg(ss.str().c_str(), types[i]); } dt.addConstructor(c); - d_data = TypeNode::fromType(nm->toExprManager()->mkDatatypeType(dt)); + d_data = nm->mkDatatypeType(dt); Debug("tuprec-debug") << "Return type : " << d_data << std::endl; } return d_data; @@ -664,16 +667,17 @@ TypeNode NodeManager::RecTypeCache::getRecordType( NodeManager * nm, const Recor for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) { sst << "_" << (*i).first << "_" << (*i).second; } - Datatype dt(nm->toExprManager(), sst.str()); + DType dt(sst.str()); dt.setRecord(); std::stringstream ssc; ssc << sst.str() << "_ctor"; - DatatypeConstructor c(ssc.str()); + std::shared_ptr c = + std::make_shared(ssc.str()); for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) { - c.addArg((*i).first, (*i).second); + c->addArg((*i).first, TypeNode::fromType((*i).second)); } dt.addConstructor(c); - d_data = TypeNode::fromType(nm->toExprManager()->mkDatatypeType(dt)); + d_data = nm->mkDatatypeType(dt); Debug("tuprec-debug") << "Return type : " << d_data << std::endl; } return d_data; diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index cfe771ca5..592b5e7e9 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -91,10 +91,6 @@ class NodeManager { friend Expr ExprManager::mkVar(const std::string&, Type, uint32_t flags); friend Expr ExprManager::mkVar(Type, uint32_t flags); - // friend so it can access NodeManager's d_listeners and notify clients - friend std::vector ExprManager::mkMutualDatatypeTypes( - std::vector&, std::set&, uint32_t); - /** Predicate for use with STL algorithms */ struct NodeValueReferenceCountNonZero { bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; } @@ -380,8 +376,8 @@ class NodeManager { /** Create a variable with the given type. */ Node mkVar(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE); Node* mkVarPtr(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE); - -public: + + public: explicit NodeManager(ExprManager* exprManager); ~NodeManager(); diff --git a/src/expr/sygus_datatype.cpp b/src/expr/sygus_datatype.cpp index 1efea4e15..d6004e7cb 100644 --- a/src/expr/sygus_datatype.cpp +++ b/src/expr/sygus_datatype.cpp @@ -18,10 +18,7 @@ using namespace CVC4::kind; namespace CVC4 { -SygusDatatype::SygusDatatype(const std::string& name) - : d_dt(Datatype(NodeManager::currentNM()->toExprManager(), name)) -{ -} +SygusDatatype::SygusDatatype(const std::string& name) : d_dt(DType(name)) {} std::string SygusDatatype::getName() const { return d_dt.getName(); } @@ -79,25 +76,19 @@ void SygusDatatype::initializeDatatype(TypeNode sygusType, Assert(!d_cons.empty()); /* Use the sygus type to not lose reference to the original types (Bool, * Int, etc) */ - d_dt.setSygus(sygusType.toType(), sygusVars.toExpr(), allowConst, allowAll); + d_dt.setSygus(sygusType, sygusVars, allowConst, allowAll); for (unsigned i = 0, ncons = d_cons.size(); i < ncons; ++i) { - // must convert to type now - std::vector cargs; - for (TypeNode& ct : d_cons[i].d_argTypes) - { - cargs.push_back(ct.toType()); - } // add (sygus) constructor - d_dt.addSygusConstructor(d_cons[i].d_op.toExpr(), + d_dt.addSygusConstructor(d_cons[i].d_op, d_cons[i].d_name, - cargs, + d_cons[i].d_argTypes, d_cons[i].d_weight); } Trace("sygus-type-cons") << "...built datatype " << d_dt << " "; } -const Datatype& SygusDatatype::getDatatype() const +const DType& SygusDatatype::getDatatype() const { // should have initialized by this point Assert(isInitialized()); diff --git a/src/expr/sygus_datatype.h b/src/expr/sygus_datatype.h index 4342aa291..6fe0531fb 100644 --- a/src/expr/sygus_datatype.h +++ b/src/expr/sygus_datatype.h @@ -20,7 +20,7 @@ #include #include "expr/attribute.h" -#include "expr/datatype.h" +#include "expr/dtype.h" #include "expr/node.h" #include "expr/type_node.h" @@ -122,7 +122,7 @@ class SygusDatatype bool allowConst, bool allowAll); /** Get the sygus datatype initialized by this class */ - const Datatype& getDatatype() const; + const DType& getDatatype() const; /** is initialized */ bool isInitialized() const; @@ -131,7 +131,7 @@ class SygusDatatype /** Information for each constructor. */ std::vector d_cons; /** Datatype to represent type's structure */ - Datatype d_dt; + DType d_dt; }; } // namespace CVC4 diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 8232ef339..5dd15dd37 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -585,19 +585,6 @@ std::vector ConstructorType::getArgTypes() const { return args; } -const Datatype& DatatypeType::getDatatype() const -{ - NodeManagerScope nms(d_nodeManager); - Assert(isDatatype()); - if (d_typeNode->getKind() == kind::DATATYPE_TYPE) - { - DatatypeIndexConstant dic = d_typeNode->getConst(); - return d_nodeManager->toExprManager()->getDatatypeForIndex(dic.getIndex()); - } - Assert(d_typeNode->getKind() == kind::PARAMETRIC_DATATYPE); - return DatatypeType((*d_typeNode)[0].toType()).getDatatype(); -} - bool DatatypeType::isParametric() const { return d_typeNode->isParametricDatatype(); } diff --git a/src/expr/type.h b/src/expr/type.h index 0067ba7e7..d58643811 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -616,9 +616,6 @@ class CVC4_PUBLIC DatatypeType : public Type { /** Construct from the base type */ DatatypeType(const Type& type = Type()); - /** Get the underlying datatype */ - const Datatype& getDatatype() const; - /** Is this datatype parametric? */ bool isParametric() const; /** diff --git a/src/expr/type_node.h b/src/expr/type_node.h index b836e5069..2c5be80aa 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -1011,7 +1011,8 @@ inline TypeNode TypeNode::getRangeType() const { if(isTester()) { return NodeManager::currentNM()->booleanType(); } - Assert(isFunction() || isConstructor() || isSelector()); + Assert(isFunction() || isConstructor() || isSelector()) + << "Cannot get range type of " << *this; return (*this)[getNumChildren() - 1]; } diff --git a/src/include/cvc4.h b/src/include/cvc4.h index 89c90a8c4..4b2bde810 100644 --- a/src/include/cvc4.h +++ b/src/include/cvc4.h @@ -20,7 +20,7 @@ #include #include -#include +#include #include #include #include diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 354f2d472..4bb253603 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1463,13 +1463,14 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2] { PARSER_STATE->parseError("Pattern must be application of a constructor or a variable."); } - Expr ef = f.getExpr(); - if (Datatype::datatypeOf(ef).isParametric()) + api::Datatype dt = type.getConstructorCodomainSort().getDatatype(); + if (dt.isParametric()) { - type = api::Sort( - SOLVER, - Datatype::datatypeOf(ef)[Datatype::indexOf(ef)] - .getSpecializedConstructorType(expr.getSort().getType())); + // lookup constructor by name + api::DatatypeConstructor dc = dt.getConstructor(f.toString()); + api::Term scons = dc.getSpecializedConstructorTerm(expr.getSort()); + // take the type of the specialized constructor instead + type = scons.getSort(); } argTypes = type.getConstructorDomainSorts(); } diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index fa0f8af43..1e5d2155a 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1149,11 +1149,9 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector& args) ss << "tuple is of length " << length << "; cannot access index " << n; parseError(ss.str()); } - const Datatype& dt = ((DatatypeType)t.getType()).getDatatype(); - api::Term ret = - d_solver->mkTerm(api::APPLY_SELECTOR, - api::Term(d_solver, dt[0][n].getSelector()), - args[0]); + const api::Datatype& dt = t.getDatatype(); + api::Term ret = d_solver->mkTerm( + api::APPLY_SELECTOR, dt[0][n].getSelectorTerm(), args[0]); Debug("parser") << "applyParseOp: return selector " << ret << std::endl; return ret; } diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp index d0ebe5f19..b34ff59f5 100644 --- a/src/preprocessing/passes/synth_rew_rules.cpp +++ b/src/preprocessing/passes/synth_rew_rules.cpp @@ -241,7 +241,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( Trace("srs-input") << "Construct unresolved types..." << std::endl; // each canonical subterm corresponds to a grammar type - std::set unres; + std::set unres; std::vector sdts; // make unresolved types for each canonical term std::map cterm_to_utype; @@ -253,7 +253,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( std::string tname = ss.str(); TypeNode tnu = nm->mkSort(tname, ExprManager::SORT_FLAG_PLACEHOLDER); cterm_to_utype[ct] = tnu; - unres.insert(tnu.toType()); + unres.insert(tnu); sdts.push_back(SygusDatatype(tname)); } Trace("srs-input") << "...finished." << std::endl; @@ -369,19 +369,19 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( Trace("srs-input") << "Make mutual datatype types for subterms..." << std::endl; // extract the datatypes - std::vector datatypes; + std::vector datatypes; for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++) { datatypes.push_back(sdts[i].getDatatype()); } - std::vector types = nm->toExprManager()->mkMutualDatatypeTypes( - datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER); + std::vector types = nm->mkMutualDatatypeTypes( + datatypes, unres, NodeManager::DATATYPE_FLAG_PLACEHOLDER); Trace("srs-input") << "...finished." << std::endl; Assert(types.size() == unres.size()); std::map subtermTypes; for (unsigned i = 0, ncterms = cterms.size(); i < ncterms; i++) { - subtermTypes[cterms[i]] = TypeNode::fromType(types[i]); + subtermTypes[cterms[i]] = types[i]; } Trace("srs-input") << "Construct the top-level types..." << std::endl; @@ -418,12 +418,12 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( } // set that this is a sygus datatype sdttl.initializeDatatype(t, sygusVarList, false, false); - Datatype dttl = sdttl.getDatatype(); - DatatypeType tlt = nm->toExprManager()->mkDatatypeType( - dttl, ExprManager::DATATYPE_FLAG_PLACEHOLDER); - tlGrammarTypes[t] = TypeNode::fromType(tlt); + DType dttl = sdttl.getDatatype(); + TypeNode tlt = + nm->mkDatatypeType(dttl, NodeManager::DATATYPE_FLAG_PLACEHOLDER); + tlGrammarTypes[t] = tlt; Trace("srs-input") << "Grammar is: " << std::endl; - Trace("srs-input") << tlt.getDatatype() << std::endl; + Trace("srs-input") << tlt.getDType() << std::endl; } Trace("srs-input") << "...finished." << std::endl; diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 8120d1d88..89b516511 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -211,17 +211,15 @@ void CvcPrinter::toStream( break; case kind::DATATYPE_TYPE: { - const Datatype& dt = - NodeManager::currentNM()->toExprManager()->getDatatypeForIndex( - n.getConst().getIndex()); - + const DType& dt = NodeManager::currentNM()->getDTypeForIndex( + n.getConst().getIndex()); if( dt.isTuple() ){ out << '['; for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) { if (i > 0) { out << ", "; } - Type t = dt[0][i].getRangeType(); + TypeNode t = dt[0][i].getRangeType(); out << t; } out << ']'; @@ -233,7 +231,7 @@ void CvcPrinter::toStream( if (i > 0) { out << ", "; } - Type t = dt[0][i].getRangeType(); + TypeNode t = dt[0][i].getRangeType(); out << dt[0][i].getSelector() << ":" << t; } out << " #]"; diff --git a/src/smt/command.h b/src/smt/command.h index 95274884f..a0e591269 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -29,7 +29,6 @@ #include #include "api/cvc4cpp.h" -#include "expr/datatype.h" #include "expr/expr.h" #include "expr/type.h" #include "expr/variable_type_map.h" diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp index 41602dab2..539d6ba2f 100644 --- a/src/smt/listeners.cpp +++ b/src/smt/listeners.cpp @@ -62,7 +62,7 @@ void SmtNodeManagerListener::nmNotifyNewSortConstructor(TypeNode tn, void SmtNodeManagerListener::nmNotifyNewDatatypes( const std::vector& dtts, uint32_t flags) { - if ((flags & ExprManager::DATATYPE_FLAG_PLACEHOLDER) == 0) + if ((flags & NodeManager::DATATYPE_FLAG_PLACEHOLDER) == 0) { std::vector types; for (const TypeNode& dt : dtts) diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index 26bff20b7..ef8dd47f1 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -41,7 +41,7 @@ parameterized APPLY_TESTER TESTER_TYPE 1 "tester application; first parameter is constant DATATYPE_TYPE \ ::CVC4::DatatypeIndexConstant \ "::CVC4::DatatypeIndexConstantHashFunction" \ - "expr/datatype.h" \ + "expr/datatype_index.h" \ "a datatype type index" cardinality DATATYPE_TYPE \ "%TYPE%.getDType().getCardinality(%TYPE%)" \ diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp index bd14f8a2c..0aa44e170 100644 --- a/src/theory/datatypes/sygus_datatype_utils.cpp +++ b/src/theory/datatypes/sygus_datatype_utils.cpp @@ -648,7 +648,7 @@ TypeNode substituteAndGeneralizeSygusType(TypeNode sdt, // must convert all constructors to version with variables in "vars" std::vector sdts; - std::set unres; + std::set unres; Trace("dtsygus-gen-debug") << "Process sygus type:" << std::endl; Trace("dtsygus-gen-debug") << sdtd.getName() << std::endl; @@ -662,7 +662,7 @@ TypeNode substituteAndGeneralizeSygusType(TypeNode sdt, ssutn0 << sdtd.getName() << "_s"; TypeNode abdTNew = nm->mkSort(ssutn0.str(), ExprManager::SORT_FLAG_PLACEHOLDER); - unres.insert(abdTNew.toType()); + unres.insert(abdTNew); dtProcessed[sdt] = abdTNew; // We must convert all symbols in the sygus datatype type sdt to @@ -706,7 +706,7 @@ TypeNode substituteAndGeneralizeSygusType(TypeNode sdt, nm->mkSort(ssutn.str(), ExprManager::SORT_FLAG_PLACEHOLDER); Trace("dtsygus-gen-debug") << " ...unresolved type " << argtNew << " for " << argt << std::endl; - unres.insert(argtNew.toType()); + unres.insert(argtNew); dtProcessed[argt] = argtNew; dtNextToProcess.push_back(argt); } @@ -736,22 +736,21 @@ TypeNode substituteAndGeneralizeSygusType(TypeNode sdt, Trace("dtsygus-gen-debug") << "Make " << sdts.size() << " datatype types..." << std::endl; // extract the datatypes - std::vector datatypes; + std::vector datatypes; for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++) { datatypes.push_back(sdts[i].getDatatype()); } // make the datatype types - std::vector datatypeTypes = - nm->toExprManager()->mkMutualDatatypeTypes( - datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER); - TypeNode sdtS = TypeNode::fromType(datatypeTypes[0]); + std::vector datatypeTypes = nm->mkMutualDatatypeTypes( + datatypes, unres, NodeManager::DATATYPE_FLAG_PLACEHOLDER); + TypeNode sdtS = datatypeTypes[0]; if (Trace.isOn("dtsygus-gen-debug")) { Trace("dtsygus-gen-debug") << "Made datatype types:" << std::endl; for (unsigned j = 0, ndts = datatypeTypes.size(); j < ndts; j++) { - const DType& dtj = TypeNode::fromType(datatypeTypes[j]).getDType(); + const DType& dtj = datatypeTypes[j].getDType(); Trace("dtsygus-gen-debug") << "#" << j << ": " << dtj << std::endl; for (unsigned k = 0, ncons = dtj.getNumConstructors(); k < ncons; k++) { diff --git a/src/theory/datatypes/sygus_extension.h b/src/theory/datatypes/sygus_extension.h index 0c475a8e0..e2b36c463 100644 --- a/src/theory/datatypes/sygus_extension.h +++ b/src/theory/datatypes/sygus_extension.h @@ -25,7 +25,7 @@ #include "context/cdlist.h" #include "context/cdo.h" #include "context/context.h" -#include "expr/datatype.h" +#include "expr/dtype.h" #include "expr/node.h" #include "theory/datatypes/sygus_simple_sym.h" #include "theory/quantifiers/sygus/sygus_explain.h" diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 6dd990b30..e9a0ba052 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -24,7 +24,6 @@ #include "context/cdlist.h" #include "expr/attribute.h" -#include "expr/datatype.h" #include "expr/node_trie.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/datatypes/sygus_extension.h" diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 176f275f0..d971a373d 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -14,7 +14,6 @@ **/ #include "theory/quantifiers/ematching/inst_match_generator.h" -#include "expr/datatype.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" #include "theory/datatypes/theory_datatypes_utils.h" diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h index 0fe6bef00..f5c13b183 100644 --- a/src/theory/quantifiers/skolemize.h +++ b/src/theory/quantifiers/skolemize.h @@ -21,7 +21,6 @@ #include #include "context/cdhashmap.h" -#include "expr/datatype.h" #include "expr/node.h" #include "expr/type_node.h" #include "theory/quantifiers/quant_util.h" diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index 9126aad94..8595ab673 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -14,7 +14,6 @@ #include "theory/quantifiers/sygus/cegis_core_connective.h" -#include "expr/datatype.h" #include "options/base_options.h" #include "printer/printer.h" #include "proof/unsat_core.h" diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 582fa067d..d0536a1ea 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -465,8 +465,8 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n) std::string veName("_virtual_enum_grammar"); SygusDatatype sdt(veName); TypeNode u = nm->mkSort(veName, ExprManager::SORT_FLAG_PLACEHOLDER); - std::set unresolvedTypes; - unresolvedTypes.insert(u.toType()); + std::set unresolvedTypes; + unresolvedTypes.insert(u); std::vector cargsEmpty; Node cr = nm->mkConst(Rational(1)); sdt.addConstructor(cr, "1", cargsEmpty); @@ -475,15 +475,11 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n) cargsPlus.push_back(u); sdt.addConstructor(PLUS, cargsPlus); sdt.initializeDatatype(nm->integerType(), bvl, false, false); - std::vector datatypes; + std::vector datatypes; datatypes.push_back(sdt.getDatatype()); - std::vector dtypes = - nm->toExprManager()->mkMutualDatatypeTypes( - datatypes, - unresolvedTypes, - ExprManager::DATATYPE_FLAG_PLACEHOLDER); - TypeNode vtn = TypeNode::fromType(dtypes[0]); - d_virtual_enum = nm->mkSkolem("_ve", vtn); + std::vector dtypes = nm->mkMutualDatatypeTypes( + datatypes, unresolvedTypes, NodeManager::DATATYPE_FLAG_PLACEHOLDER); + d_virtual_enum = nm->mkSkolem("_ve", dtypes[0]); d_tds->registerEnumerator( d_virtual_enum, Node::null(), d_parent, ROLE_ENUM_CONSTRAINED); } diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp index ee37d7b4b..f31a9a977 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.cpp +++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp @@ -15,7 +15,6 @@ #include "theory/quantifiers/sygus/sygus_abduct.h" -#include "expr/datatype.h" #include "expr/dtype.h" #include "expr/node_algorithm.h" #include "expr/sygus_datatype.h" diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index bd5f7ae50..b89b94fc8 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -16,7 +16,6 @@ #include -#include "expr/datatype.h" #include "options/quantifiers_options.h" #include "theory/bv/theory_bv_utils.h" #include "theory/datatypes/sygus_datatype_utils.h" @@ -378,10 +377,11 @@ Node CegGrammarConstructor::convertToEmbedding(Node n) return visited[n]; } - -TypeNode CegGrammarConstructor::mkUnresolvedType(const std::string& name, std::set& unres) { +TypeNode CegGrammarConstructor::mkUnresolvedType(const std::string& name, + std::set& unres) +{ TypeNode unresolved = NodeManager::currentNM()->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER); - unres.insert( unresolved.toType() ); + unres.insert(unresolved); return unresolved; } @@ -529,7 +529,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( include_cons, std::unordered_set& term_irrelevant, std::vector& sdts, - std::set& unres) + std::set& unres) { NodeManager* nm = NodeManager::currentNM(); Trace("sygus-grammar-def") << "Construct default grammar for " << fun << " " @@ -1389,7 +1389,7 @@ TypeNode CegGrammarConstructor::mkSygusDefaultType( { Trace("sygus-grammar-def") << " ...using " << it->second.size() << " extra constants for " << it->first << std::endl; } - std::set unres; + std::set unres; std::vector sdts; mkSygusDefaultGrammar(range, bvl, @@ -1401,19 +1401,18 @@ TypeNode CegGrammarConstructor::mkSygusDefaultType( sdts, unres); // extract the datatypes from the sygus datatype generator objects - std::vector datatypes; + std::vector datatypes; for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++) { datatypes.push_back(sdts[i].d_sdt.getDatatype()); } Trace("sygus-grammar-def") << "...made " << datatypes.size() << " datatypes, now make mutual datatype types..." << std::endl; Assert(!datatypes.empty()); - std::vector types = - NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes( - datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER); + std::vector types = NodeManager::currentNM()->mkMutualDatatypeTypes( + datatypes, unres, NodeManager::DATATYPE_FLAG_PLACEHOLDER); Trace("sygus-grammar-def") << "...finished" << std::endl; Assert(types.size() == datatypes.size()); - return TypeNode::fromType( types[0] ); + return types[0]; } TypeNode CegGrammarConstructor::mkSygusTemplateTypeRec( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, @@ -1423,7 +1422,7 @@ TypeNode CegGrammarConstructor::mkSygusTemplateTypeRec( Node templ, Node templ_a return templ_arg_sygus_type; }else{ tcount++; - std::set unres; + std::set unres; std::vector sdts; std::stringstream ssd; ssd << fun << "_templ_" << tcount; @@ -1450,16 +1449,16 @@ TypeNode CegGrammarConstructor::mkSygusTemplateTypeRec( Node templ, Node templ_a sdts.back().addConstructor(op, ssdc.str(), argTypes); sdts.back().initializeDatatype(templ.getType(), bvl, true, true); // extract the datatypes from the sygus datatype objects - std::vector datatypes; + std::vector datatypes; for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++) { datatypes.push_back(sdts[i].getDatatype()); } - std::vector types = - NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes( - datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER); + std::vector types = + NodeManager::currentNM()->mkMutualDatatypeTypes( + datatypes, unres, NodeManager::DATATYPE_FLAG_PLACEHOLDER); Assert(types.size() == 1); - return TypeNode::fromType( types[0] ); + return types[0]; } } diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index fd7f84484..c0113b31c 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -222,7 +222,8 @@ public: }; // helper for mkSygusDefaultGrammar (makes unresolved type for mutually recursive datatype construction) - static TypeNode mkUnresolvedType(const std::string& name, std::set& unres); + static TypeNode mkUnresolvedType(const std::string& name, + std::set& unres); // collect the list of types that depend on type range static void collectSygusGrammarTypesFor(TypeNode range, std::vector& types); @@ -243,7 +244,7 @@ public: include_cons, std::unordered_set& term_irrelevant, std::vector& sdts, - std::set& unres); + std::set& unres); // helper function for mkSygusTemplateType static TypeNode mkSygusTemplateTypeRec(Node templ, diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index 939256b2b..d9deb78f5 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -15,7 +15,6 @@ #include "theory/quantifiers/sygus/sygus_grammar_norm.h" -#include "expr/datatype.h" #include "expr/node_manager_attributes.h" // for VarNameAttr #include "options/quantifiers_options.h" #include "smt/smt_engine.h" @@ -122,7 +121,7 @@ void SygusGrammarNorm::TypeObject::initializeDatatype( << "...built datatype " << d_sdt.getDatatype() << " "; /* Add to global accumulators */ sygus_norm->d_dt_all.push_back(d_sdt.getDatatype()); - sygus_norm->d_unres_t_all.insert(d_unres_tn.toType()); + sygus_norm->d_unres_t_all.insert(d_unres_tn); Trace("sygus-grammar-normalize") << "---------------------------------\n"; } @@ -463,7 +462,6 @@ TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn, // Remaining operators are rebuilt as they are. // Notice that we must extract the Datatype here to get the (Expr-layer) // sygus print callback. - const Datatype& dtt = DatatypeType(tn.toType()).getDatatype(); for (unsigned i = 0, size = op_pos.size(); i < size; ++i) { unsigned oi = op_pos[i]; @@ -520,22 +518,21 @@ TypeNode SygusGrammarNorm::normalizeSygusType(TypeNode tn, Node sygus_vars) Trace("sygus-grammar-normalize-build") << d_dt_all[i]; } Trace("sygus-grammar-normalize-build") << " and unresolved types\n"; - for (const Type& unres_t : d_unres_t_all) + for (const TypeNode& unres_t : d_unres_t_all) { Trace("sygus-grammar-normalize-build") << unres_t << " "; } Trace("sygus-grammar-normalize-build") << "\n"; } Assert(d_dt_all.size() == d_unres_t_all.size()); - std::vector types = - NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes( - d_dt_all, d_unres_t_all, ExprManager::DATATYPE_FLAG_PLACEHOLDER); + std::vector types = NodeManager::currentNM()->mkMutualDatatypeTypes( + d_dt_all, d_unres_t_all, NodeManager::DATATYPE_FLAG_PLACEHOLDER); Assert(types.size() == d_dt_all.size()); /* Clear accumulators */ d_dt_all.clear(); d_unres_t_all.clear(); /* By construction the normalized type node will be the last one considered */ - return TypeNode::fromType(types.back()); + return types.back(); } } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h index 5994d0e7d..8ffa81e9e 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h @@ -22,7 +22,6 @@ #include #include -#include "expr/datatype.h" #include "expr/node.h" #include "expr/sygus_datatype.h" #include "expr/type.h" @@ -376,9 +375,9 @@ class SygusGrammarNorm */ TNode d_sygus_vars; /* Datatypes to be resolved */ - std::vector d_dt_all; + std::vector d_dt_all; /* Types to be resolved */ - std::set d_unres_t_all; + std::set d_unres_t_all; /* Associates type nodes with OpPosTries */ std::map d_tries; /* Map of type nodes into their identity operators (\lambda x. x) */ diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.h b/src/theory/quantifiers/sygus/sygus_grammar_red.h index 361226678..9bb2c977c 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_red.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_red.h @@ -20,7 +20,6 @@ #include #include -#include "expr/datatype.h" #include "expr/node.h" namespace CVC4 { diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index 0ecd888e0..c2ca83e41 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -16,16 +16,12 @@ #include "theory/quantifiers/sygus/sygus_interpol.h" -#include "expr/datatype.h" #include "expr/dtype.h" #include "expr/node_algorithm.h" -#include "expr/sygus_datatype.h" #include "options/smt_options.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" -#include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" namespace CVC4 { @@ -188,15 +184,14 @@ TypeNode SygusInterpol::setSynthGrammar(const TypeNode& itpGType, std::map> include_cons; getIncludeCons(axioms, conj, include_cons); std::unordered_set terms_irrelevant; - itpGTypeS = - CVC4::theory::quantifiers::CegGrammarConstructor::mkSygusDefaultType( - NodeManager::currentNM()->booleanType(), - d_ibvlShared, - "interpolation_grammar", - extra_cons, - exclude_cons, - include_cons, - terms_irrelevant); + itpGTypeS = CegGrammarConstructor::mkSygusDefaultType( + NodeManager::currentNM()->booleanType(), + d_ibvlShared, + "interpolation_grammar", + extra_cons, + exclude_cons, + include_cons, + terms_irrelevant); } Trace("sygus-interpol-debug") << "...finish setting up grammar" << std::endl; return itpGTypeS; @@ -235,10 +230,10 @@ void SygusInterpol::mkSygusConjecture(Node itp, // set the sygus bound variable list Trace("sygus-interpol-debug") << "Set attributes..." << std::endl; - itp.setAttribute(theory::SygusSynthFunVarListAttribute(), d_ibvlShared); + itp.setAttribute(SygusSynthFunVarListAttribute(), d_ibvlShared); // sygus attribute Node sygusVar = nm->mkSkolem("sygus", nm->booleanType()); - theory::SygusAttribute ca; + SygusAttribute ca; sygusVar.setAttribute(ca, true); Node instAttr = nm->mkNode(kind::INST_ATTRIBUTE, sygusVar); std::vector iplc; @@ -265,7 +260,7 @@ void SygusInterpol::mkSygusConjecture(Node itp, constraint = constraint.substitute( d_syms.begin(), d_syms.end(), d_vars.begin(), d_vars.end()); Trace("sygus-interpol-debug") << constraint << "...finish" << std::endl; - constraint = theory::Rewriter::rewrite(constraint); + constraint = Rewriter::rewrite(constraint); d_sygusConj = constraint; Trace("sygus-interpol") << "Generate: " << d_sygusConj << std::endl; diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 0921fba30..573db99c7 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -14,7 +14,6 @@ **/ #include "theory/quantifiers/sygus/sygus_pbe.h" -#include "expr/datatype.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/sygus/example_infer.h" #include "theory/quantifiers/sygus/synth_conjecture.h" diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp index 6df8619f7..729a12c66 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp +++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp @@ -16,7 +16,6 @@ #include -#include "expr/datatype.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 9608de743..5b7ad2049 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -14,7 +14,6 @@ **/ #include "theory/quantifiers/sygus/synth_conjecture.h" -#include "expr/datatype.h" #include "options/base_options.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index f657062ed..42b560c59 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -14,7 +14,6 @@ #include "theory/quantifiers/term_util.h" -#include "expr/datatype.h" #include "expr/node_algorithm.h" #include "options/base_options.h" #include "options/datatypes_options.h" diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 82f32337e..c8eeece4a 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -15,7 +15,6 @@ **/ #include "theory/sets/theory_sets_rels.h" -#include "expr/datatype.h" #include "theory/sets/theory_sets_private.h" #include "theory/sets/theory_sets.h" diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h index c86408a52..f1b25515c 100644 --- a/test/unit/theory/type_enumerator_white.h +++ b/test/unit/theory/type_enumerator_white.h @@ -20,6 +20,7 @@ #include #include "expr/array_store_all.h" +#include "expr/dtype.h" #include "expr/expr_manager.h" #include "expr/kind.h" #include "expr/node_manager.h" @@ -145,51 +146,66 @@ class TypeEnumeratorWhite : public CxxTest::TestSuite { TS_ASSERT( ! te.isFinished() ); } - void testDatatypesFinite() { - Datatype dt(d_em, "Colors"); - dt.addConstructor(DatatypeConstructor("red")); - dt.addConstructor(DatatypeConstructor("orange")); - dt.addConstructor(DatatypeConstructor("yellow")); - dt.addConstructor(DatatypeConstructor("green")); - dt.addConstructor(DatatypeConstructor("blue")); - dt.addConstructor(DatatypeConstructor("violet")); - TypeNode datatype = TypeNode::fromType(d_em->mkDatatypeType(dt)); + void testDTypesFinite() + { + DType dt("Colors"); + dt.addConstructor(std::make_shared("red")); + dt.addConstructor(std::make_shared("orange")); + dt.addConstructor(std::make_shared("yellow")); + dt.addConstructor(std::make_shared("green")); + dt.addConstructor(std::make_shared("blue")); + dt.addConstructor(std::make_shared("violet")); + TypeNode datatype = d_nm->mkDatatypeType(dt); + const std::vector >& dtcons = + datatype.getDType().getConstructors(); TypeEnumerator te(datatype); - TS_ASSERT_EQUALS(*te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("red"))); - TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("orange"))); - TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("yellow"))); - TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("green"))); - TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("blue"))); - TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("violet"))); + TS_ASSERT_EQUALS( + *te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[0]->getConstructor())); + TS_ASSERT_EQUALS( + *++te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[1]->getConstructor())); + TS_ASSERT_EQUALS( + *++te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[2]->getConstructor())); + TS_ASSERT_EQUALS( + *++te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[3]->getConstructor())); + TS_ASSERT_EQUALS( + *++te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[4]->getConstructor())); + TS_ASSERT_EQUALS( + *++te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[5]->getConstructor())); TS_ASSERT_THROWS(*++te, NoMoreValuesException&); TS_ASSERT_THROWS(*++te, NoMoreValuesException&); TS_ASSERT_THROWS(*++te, NoMoreValuesException&); } - void testDatatypesInfinite1() { - Datatype colors(d_em, "Colors"); - colors.addConstructor(DatatypeConstructor("red")); - colors.addConstructor(DatatypeConstructor("orange")); - colors.addConstructor(DatatypeConstructor("yellow")); - colors.addConstructor(DatatypeConstructor("green")); - colors.addConstructor(DatatypeConstructor("blue")); - colors.addConstructor(DatatypeConstructor("violet")); - TypeNode colorsType = TypeNode::fromType(d_em->mkDatatypeType(colors)); - Datatype listColors(d_em, "ListColors"); - DatatypeConstructor consC("cons"); - consC.addArg("car", colorsType.toType()); - consC.addArg("cdr", DatatypeSelfType()); + void testDTypesInfinite1() + { + DType colors("Colors"); + colors.addConstructor(std::make_shared("red")); + colors.addConstructor(std::make_shared("orange")); + colors.addConstructor(std::make_shared("yellow")); + colors.addConstructor(std::make_shared("green")); + colors.addConstructor(std::make_shared("blue")); + colors.addConstructor(std::make_shared("violet")); + TypeNode colorsType = d_nm->mkDatatypeType(colors); + const std::vector >& ctCons = + colorsType.getDType().getConstructors(); + DType listColors("ListColors"); + std::shared_ptr consC = + std::make_shared("cons"); + consC->addArg("car", colorsType); + consC->addArgSelf("cdr"); listColors.addConstructor(consC); - listColors.addConstructor(DatatypeConstructor("nil")); - TypeNode listColorsType = TypeNode::fromType(d_em->mkDatatypeType(listColors)); + listColors.addConstructor(std::make_shared("nil")); + TypeNode listColorsType = d_nm->mkDatatypeType(listColors); + const std::vector >& lctCons = + listColorsType.getDType().getConstructors(); TypeEnumerator te(listColorsType); TS_ASSERT( ! te.isFinished() ); - Node cons = Node::fromExpr(DatatypeType(listColorsType.toType()).getDatatype().getConstructor("cons")); - Node nil = d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(listColorsType.toType()).getDatatype().getConstructor("nil")); - Node red = d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(colorsType.toType()).getDatatype().getConstructor("red")); - Node orange = d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(colorsType.toType()).getDatatype().getConstructor("orange")); - Node yellow = d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(colorsType.toType()).getDatatype().getConstructor("yellow")); + Node cons = lctCons[0]->getConstructor(); + Node nil = d_nm->mkNode(APPLY_CONSTRUCTOR, lctCons[1]->getConstructor()); + Node red = d_nm->mkNode(APPLY_CONSTRUCTOR, ctCons[0]->getConstructor()); + Node orange = d_nm->mkNode(APPLY_CONSTRUCTOR, ctCons[1]->getConstructor()); + Node yellow = d_nm->mkNode(APPLY_CONSTRUCTOR, ctCons[2]->getConstructor()); TS_ASSERT_EQUALS(*te, nil); TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)); TS_ASSERT( ! te.isFinished() ); @@ -212,7 +228,8 @@ class TypeEnumeratorWhite : public CxxTest::TestSuite { TS_ASSERT( ! te.isFinished() ); } - void NOTYETtestDatatypesInfinite2() { + void NOTYETtestDTypesInfinite2() + { //TypeNode datatype; //TypeEnumerator te(datatype); //TS_ASSERT( ! te.isFinished() );