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
#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"
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(); }
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<Sort>& params) const
{
+ NodeManagerScope scope(d_solver->getNodeManager());
CVC4_API_CHECK(isParametricDatatype() || isSortConstructor())
<< "Expected parametric datatype or sort constructor sort.";
- std::vector<Type> tparams;
+ std::vector<TypeNode> 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(); }
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> Sort::getConstructorDomainSorts() const
{
- CVC4_API_CHECK(isConstructor()) << "Not a function sort: " << (*this);
+ CVC4_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
std::vector<CVC4::Type> 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());
}
std::vector<Sort> Sort::getDatatypeParamSorts() const
{
CVC4_API_CHECK(isParametricDatatype()) << "Not a parametric datatype sort.";
- std::vector<CVC4::Type> types = DatatypeType(*d_type).getParamTypes();
- return typeVectorToSorts(d_solver, types);
+ std::vector<CVC4::TypeNode> typeNodes =
+ TypeNode::fromType(*d_type).getParamTypes();
+ std::vector<Sort> 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 ---------------------------------------------------------- */
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> Sort::getTupleSorts() const
{
CVC4_API_CHECK(isTuple()) << "Not a tuple sort.";
- std::vector<CVC4::Type> types = DatatypeType(*d_type).getTupleTypes();
- return typeVectorToSorts(d_solver, types);
+ std::vector<CVC4::TypeNode> typeNodes =
+ TypeNode::fromType(*d_type).getTupleTypes();
+ std::vector<Sort> sorts;
+ for (size_t i = 0, tsize = typeNodes.size(); i < tsize; i++)
+ {
+ sorts.push_back(Sort(d_solver, typeNodes[i].toType()));
+ }
+ return sorts;
}
/* --------------------------------------------------------------------- */
break;
}
}
-
+ // Notice that kinds like APPLY_TYPE_ASCRIPTION will be converted to
+ // INTERNAL_KIND.
return intToExtKind(d_node->getKind());
}
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());
}
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
// !!! 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;
}
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))
{
}
Sort param,
bool isCoDatatype)
: d_solver(slv),
- d_dtype(new CVC4::Datatype(slv->getExprManager(),
- name,
- std::vector<Type>{*param.d_type},
- isCoDatatype))
+ d_dtype(new CVC4::DType(
+ name,
+ std::vector<TypeNode>{TypeNode::fromType(*param.d_type)},
+ isCoDatatype))
{
}
bool isCoDatatype)
: d_solver(slv)
{
- std::vector<Type> tparams;
+ std::vector<TypeNode> 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<CVC4::Datatype>(
- new CVC4::Datatype(slv->getExprManager(), name, tparams, isCoDatatype));
+ d_dtype = std::shared_ptr<CVC4::DType>(
+ 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
// !!! 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)
{
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(); }
Sort DatatypeSelector::getRangeSort() const
{
- return Sort(d_solver, d_stor->getRangeType());
+ return Sort(d_solver, d_stor->getRangeType().toType());
}
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;
}
}
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(); }
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 =
}
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<CVC4::DatatypeConstructorArg>* sels =
- static_cast<const std::vector<CVC4::DatatypeConstructorArg>*>(
- d_int_stors);
- for (const auto& s : *sels)
+ const std::vector<std::shared_ptr<CVC4::DTypeSelector>>& sels =
+ ctor.getArgs();
+ for (const std::shared_ptr<CVC4::DTypeSelector>& 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()
// !!! 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;
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]);
}
/* 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
{
// !!! 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
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<CVC4::DatatypeConstructor>* cons =
- static_cast<const std::vector<CVC4::DatatypeConstructor>*>(d_int_ctors);
- for (const auto& c : *cons)
+ const std::vector<std::shared_ptr<DTypeConstructor>>& cons =
+ dtype.getConstructors();
+ for (const std::shared_ptr<DTypeConstructor>& 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()
Sort(d_solver, d_solver->getExprManager()->mkSort(ntsymbol.toString()));
}
- std::vector<CVC4::Datatype> datatypes;
- std::set<Type> unresTypes;
+ std::vector<CVC4::DType> datatypes;
+ std::set<TypeNode> unresTypes;
datatypes.reserve(d_ntSyms.size());
}
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
<< " 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<DatatypeType> datatypeTypes =
- d_solver->getExprManager()->mkMutualDatatypeTypes(
- datatypes, unresTypes, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
+ std::vector<TypeNode> 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(
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<TypeNode> 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(
{
std::stringstream ss;
ss << v;
- std::vector<Sort> cargs;
- dt.d_dtype->addSygusConstructor(
- v.d_node->toExpr(), ss.str(), sortVectorToTypes(cargs));
+ std::vector<TypeNode> cargs;
+ dt.d_dtype->addSygusConstructor(*v.d_node, ss.str(), cargs);
}
}
}
std::vector<DatatypeDecl>& dtypedecls,
std::set<Sort>& unresolvedSorts) const
{
+ NodeManagerScope scope(getNodeManager());
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- std::vector<CVC4::Datatype> datatypes;
+ std::vector<CVC4::DType> datatypes;
for (size_t i = 0, ndts = dtypedecls.size(); i < ndts; ++i)
{
CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(this == dtypedecls[i].d_solver,
{
CVC4_API_SOLVER_CHECK_SORT(sort);
}
- std::set<Type> utypes = sortSetToTypes(unresolvedSorts);
- std::vector<CVC4::DatatypeType> dtypes =
- d_exprMgr->mkMutualDatatypeTypes(datatypes, utypes);
+
+ std::set<TypeNode> utypes;
+ for (const Sort& s : unresolvedSorts)
+ {
+ utypes.insert(TypeNode::fromType(s.getType()));
+ }
+ std::vector<CVC4::TypeNode> dtypes =
+ getNodeManager()->mkMutualDatatypeTypes(datatypes, utypes);
std::vector<Sort> 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;
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;
}
std::vector<Sort> Solver::mkDatatypeSorts(
std::vector<DatatypeDecl>& dtypedecls) const
{
+ CVC4_API_SOLVER_TRY_CATCH_BEGIN;
std::set<Sort> unresolvedSorts;
return mkDatatypeSortsInternal(dtypedecls, unresolvedSorts);
+ CVC4_API_SOLVER_TRY_CATCH_END;
}
std::vector<Sort> Solver::mkDatatypeSorts(std::vector<DatatypeDecl>& dtypedecls,
std::set<Sort>& 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
Sort Solver::mkRecordSort(
const std::vector<std::pair<std::string, Sort>>& fields) const
{
+ NodeManagerScope scope(getNodeManager());
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
std::vector<std::pair<std::string, Type>> f;
size_t i = 0;
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;
}
!sorts[i].isFunctionLike(), "parameter sort", sorts[i], i)
<< "non-function-like sort as parameter sort for tuple sort";
}
- std::vector<Type> types = sortVectorToTypes(sorts);
-
- return Sort(this, d_exprMgr->mkTupleType(types));
+ std::vector<TypeNode> 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;
}
DatatypeConstructorDecl Solver::mkDatatypeConstructorDecl(
const std::string& name)
{
+ NodeManagerScope scope(getNodeManager());
return DatatypeConstructorDecl(this, name);
}
DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, bool isCoDatatype)
{
+ NodeManagerScope scope(getNodeManager());
return DatatypeDecl(this, name, isCoDatatype);
}
Sort param,
bool isCoDatatype)
{
+ NodeManagerScope scope(getNodeManager());
return DatatypeDecl(this, name, param, isCoDatatype);
}
const std::vector<Sort>& params,
bool isCoDatatype)
{
+ NodeManagerScope scope(getNodeManager());
return DatatypeDecl(this, name, params, isCoDatatype);
}
Term Solver::mkTuple(const std::vector<Sort>& sorts,
const std::vector<Term>& 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";
<< "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;
}
class NodeTemplate;
typedef NodeTemplate<true> Node;
class Expr;
-class Datatype;
-class DatatypeConstructor;
-class DatatypeConstructorArg;
+class DType;
+class DTypeConstructor;
+class DTypeSelector;
class ExprManager;
class GetAbductCommand;
class GetInterpolCommand;
*/
DatatypeConstructorDecl();
+ /**
+ * Destructor.
+ */
+ ~DatatypeConstructorDecl();
+
/**
* Add datatype selector declaration.
* @param name the name of the datatype selector declaration to add
// !!! 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:
/**
* 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<CVC4::DatatypeConstructor> d_ctor;
+ std::shared_ptr<CVC4::DTypeConstructor> d_ctor;
};
class Solver;
// !!! 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:
/**
/* 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<CVC4::Datatype> d_dtype;
+ std::shared_ptr<CVC4::DType> d_dtype;
};
/**
* @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.
// !!! 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:
/**
/**
* 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<CVC4::DatatypeConstructorArg> d_stor;
+ std::shared_ptr<CVC4::DTypeSelector> d_stor;
};
/**
* @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.
* @param true if this is a begin() iterator
*/
const_iterator(const Solver* slv,
- const CVC4::DatatypeConstructor& ctor,
+ const CVC4::DTypeConstructor& ctor,
bool begin);
/**
// !!! 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:
/**
/**
* 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<CVC4::DatatypeConstructor> d_ctor;
+ std::shared_ptr<CVC4::DTypeConstructor> d_ctor;
};
/*
* @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();
* @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.
// !!! 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:
/**
/**
* 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<CVC4::Datatype> d_dtype;
+ std::shared_ptr<CVC4::DType> d_dtype;
};
/**
type_node.cpp
type_node.h
variable_type_map.h
- datatype.h
- datatype.cpp
datatype_index.h
datatype_index.cpp
dtype.h
+++ /dev/null
-/********************* */
-/*! \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 <string>
-#include <sstream>
-
-#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<DType>(name, isCo);
-}
-
-Datatype::Datatype(ExprManager* em,
- std::string name,
- const std::vector<Type>& params,
- bool isCo)
- : d_em(em),
- d_internal(nullptr),
- d_record(NULL),
- d_isRecord(false),
- d_constructors()
-{
- ExprManagerScope ems(*d_em);
- std::vector<TypeNode> paramsn;
- for (const Type& t : params)
- {
- paramsn.push_back(TypeNode::fromType(t));
- }
- d_internal = std::make_shared<DType>(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<std::string, DatatypeType>& resolutions,
- const std::vector<Type>& placeholders,
- const std::vector<Type>& replacements,
- const std::vector<SortConstructorType>& paramTypes,
- const std::vector<DatatypeType>& 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<std::string, TypeNode> resolutionsn;
- std::vector<TypeNode> placeholdersn;
- std::vector<TypeNode> replacementsn;
- std::vector<TypeNode> paramTypesn;
- std::vector<TypeNode> paramReplacementsn;
- for (const std::pair<const std::string, DatatypeType>& 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<std::string, Type> > fields;
- for( unsigned i=0; i<(*this)[0].getNumArgs(); i++ ){
- fields.push_back( std::pair<std::string, Type>( (*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<Type> 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<Type>& 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.size(); j++ ){
- Debug("parser-sygus-debug") << " arg " << j << " : " << cargs[j] << std::endl;
- std::stringstream sname;
- sname << name << "_" << j;
- c.addArg(sname.str(), cargs[j]);
- }
- addConstructor(c);
-}
-
-void Datatype::addSygusConstructor(Kind k,
- const std::string& cname,
- const std::vector<Type>& 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<Type>& 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<DatatypeConstructor>* 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<DTypeConstructor>(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<DatatypeConstructorArg>* 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<DTypeSelector>(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<Type> Datatype::getParameters() const
-{
- CheckArgument(isParametric(),
- this,
- "Cannot get type parameters of a non-parametric datatype.");
- std::vector<Type> params;
- std::vector<TypeNode> 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 */
+++ /dev/null
-/********************* */
-/*! \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 <functional>
-#include <iostream>
-#include <string>
-#include <vector>
-#include <map>
-
-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<DatatypeConstructor>* d_v;
- size_t d_i;
-
- friend class Datatype;
-
- DatatypeConstructorIterator(const std::vector<DatatypeConstructor>& 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<DatatypeConstructorArg>* d_v;
- size_t d_i;
-
- friend class DatatypeConstructor;
-
- DatatypeConstructorArgIterator(const std::vector<DatatypeConstructorArg>& 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<DTypeSelector> 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<DatatypeConstructorArg>* getArgs() const;
-
- /** prints this datatype constructor to stream */
- void toStream(std::ostream& out) const;
-
- private:
- /** The internal representation */
- std::shared_ptr<DTypeConstructor> d_internal;
- /** The constructor */
- Expr d_constructor;
- /** the arguments of this constructor */
- std::vector<DatatypeConstructorArg> 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<Type>& 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<Type>& cargs,
- int weight = -1);
- /**
- * Same as above, with builtin kind k.
- */
- void addSygusConstructor(Kind k,
- const std::string& cname,
- const std::vector<Type>& 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<Type> 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<Type>& 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<DatatypeConstructor>* 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<DType> d_internal;
- /** self type */
- Type d_self;
- /** the data of the record for this datatype (if applicable) */
- std::shared_ptr<Record> d_record;
- /** whether the datatype is a record */
- bool d_isRecord;
- /** the constructors of this datatype */
- std::vector<DatatypeConstructor> 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<std::string, DatatypeType>& resolutions,
- const std::vector<Type>& placeholders,
- const std::vector<Type>& replacements,
- const std::vector<SortConstructorType>& paramTypes,
- const std::vector<DatatypeType>& 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<std::string>()(dt.getName());
- }
- inline size_t operator()(const Datatype* dt) const {
- return std::hash<std::string>()(dt->getName());
- }
- inline size_t operator()(const DatatypeConstructor& dtc) const {
- return std::hash<std::string>()(dtc.getName());
- }
- inline size_t operator()(const DatatypeConstructor* dtc) const {
- return std::hash<std::string>()(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 */
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<DTypeConstructor> c =
+ std::make_shared<DTypeConstructor>(ss.str(), 0);
+ c->setSygus(op);
+ addConstructor(c);
+ }
+ }
+
d_sygusType = st;
d_sygusBvl = bvl;
d_sygusAllowConst = allowConst || allowAll;
// ----------------------- end datatype attributes
class NodeManager;
-class Datatype;
/**
* The Node-level representation of an inductive datatype, which currently
*/
class DType
{
- friend class Datatype;
friend class DTypeConstructor;
friend class NodeManager; // for access to resolve()
}
}
#endif
- // clear the datatypes
- d_ownedDatatypes.clear();
delete d_nodeManager;
d_nodeManager = NULL;
return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkPredicateType(sortNodes))));
}
-DatatypeType ExprManager::mkTupleType(const std::vector<Type>& types) {
- NodeManagerScope nms(d_nodeManager);
- std::vector<TypeNode> 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<Type>& types) {
NodeManagerScope nms(d_nodeManager);
std::vector<TypeNode> typeNodes;
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<Datatype> datatypes;
- datatypes.push_back(datatype);
- std::vector<DatatypeType> result = mkMutualDatatypeTypes(datatypes, flags);
- Assert(result.size() == 1);
- return result.front();
-}
-
-std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(
- std::vector<Datatype>& datatypes, uint32_t flags)
-{
- std::set<Type> unresolvedTypes;
- return mkMutualDatatypeTypes(datatypes, unresolvedTypes, flags);
-}
-
-std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(
- std::vector<Datatype>& datatypes,
- std::set<Type>& unresolvedTypes,
- uint32_t flags)
-{
- NodeManagerScope nms(d_nodeManager);
- std::map<std::string, DatatypeType> nameResolutions;
- std::vector<DatatypeType> dtts;
-
- // have to build deep copy so that datatypes will live in this class
- std::vector< Datatype* > dt_copies;
- for(std::vector<Datatype>::iterator i = datatypes.begin(), i_end = datatypes.end(); i != i_end; ++i) {
- d_ownedDatatypes.push_back(std::unique_ptr<Datatype>(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<Datatype*>::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<Type> placeholders;// to hold the "unresolved placeholders"
- std::vector<Type> replacements;// to hold our final, resolved types
- for(std::set<Type>::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<std::string, DatatypeType>::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<TypeNode> tns;
- for(std::vector<DatatypeType>::iterator i = dtts.begin(),
- i_end = dtts.end();
- i != i_end;
- ++i) {
- const Datatype& dt = (*i).getDatatype();
- if(!dt.isResolved()) {
- const_cast<Datatype&>(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<NodeManagerListener*>::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))));
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 */
*/
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.
// 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<std::unique_ptr<Datatype> > d_ownedDatatypes;
-
/** Creates an expression manager. */
ExprManager();
public:
*/
FunctionType mkPredicateType(const std::vector<Type>& sorts);
- /**
- * Make a tuple type with types from
- * <code>types[0..types.size()-1]</code>. <code>types</code> must
- * have at least one element.
- */
- DatatypeType mkTupleType(const std::vector<Type>& types);
-
- /**
- * Make a record type with types from the rec parameter.
- */
- DatatypeType mkRecordType(const Record& rec);
-
/**
* Make a symbolic expressiontype with types from
* <code>types[0..types.size()-1]</code>. <code>types</code> may
/** 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<DatatypeType> mkMutualDatatypeTypes(
- std::vector<Datatype>& 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<DatatypeType> mkMutualDatatypeTypes(
- std::vector<Datatype>& datatypes,
- std::set<Type>& 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,
* 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}
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];
}
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<DTypeConstructor> c =
+ std::make_shared<DTypeConstructor>(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;
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<DTypeConstructor> c =
+ std::make_shared<DTypeConstructor>(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;
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<DatatypeType> ExprManager::mkMutualDatatypeTypes(
- std::vector<Datatype>&, std::set<Type>&, uint32_t);
-
/** Predicate for use with STL algorithms */
struct NodeValueReferenceCountNonZero {
bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; }
/** 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();
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(); }
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<Type> 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());
#include <vector>
#include "expr/attribute.h"
-#include "expr/datatype.h"
+#include "expr/dtype.h"
#include "expr/node.h"
#include "expr/type_node.h"
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;
/** Information for each constructor. */
std::vector<SygusDatatypeConstructor> d_cons;
/** Datatype to represent type's structure */
- Datatype d_dt;
+ DType d_dt;
};
} // namespace CVC4
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<DatatypeIndexConstant>();
- 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();
}
/** 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;
/**
if(isTester()) {
return NodeManager::currentNM()->booleanType();
}
- Assert(isFunction() || isConstructor() || isSelector());
+ Assert(isFunction() || isConstructor() || isSelector())
+ << "Cannot get range type of " << *this;
return (*this)[getNumChildren() - 1];
}
#include <cvc4/base/configuration.h>
#include <cvc4/base/exception.h>
-#include <cvc4/expr/datatype.h>
+#include <cvc4/expr/datatype_index.h>
#include <cvc4/expr/expr.h>
#include <cvc4/expr/expr_manager.h>
#include <cvc4/options/options.h>
{
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();
}
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;
}
Trace("srs-input") << "Construct unresolved types..." << std::endl;
// each canonical subterm corresponds to a grammar type
- std::set<Type> unres;
+ std::set<TypeNode> unres;
std::vector<SygusDatatype> sdts;
// make unresolved types for each canonical term
std::map<Node, TypeNode> cterm_to_utype;
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;
Trace("srs-input") << "Make mutual datatype types for subterms..."
<< std::endl;
// extract the datatypes
- std::vector<Datatype> datatypes;
+ std::vector<DType> datatypes;
for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++)
{
datatypes.push_back(sdts[i].getDatatype());
}
- std::vector<DatatypeType> types = nm->toExprManager()->mkMutualDatatypeTypes(
- datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
+ std::vector<TypeNode> types = nm->mkMutualDatatypeTypes(
+ datatypes, unres, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
Trace("srs-input") << "...finished." << std::endl;
Assert(types.size() == unres.size());
std::map<Node, TypeNode> 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;
}
// 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;
break;
case kind::DATATYPE_TYPE: {
- const Datatype& dt =
- NodeManager::currentNM()->toExprManager()->getDatatypeForIndex(
- n.getConst<DatatypeIndexConstant>().getIndex());
-
+ const DType& dt = NodeManager::currentNM()->getDTypeForIndex(
+ n.getConst<DatatypeIndexConstant>().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 << ']';
if (i > 0) {
out << ", ";
}
- Type t = dt[0][i].getRangeType();
+ TypeNode t = dt[0][i].getRangeType();
out << dt[0][i].getSelector() << ":" << t;
}
out << " #]";
#include <vector>
#include "api/cvc4cpp.h"
-#include "expr/datatype.h"
#include "expr/expr.h"
#include "expr/type.h"
#include "expr/variable_type_map.h"
void SmtNodeManagerListener::nmNotifyNewDatatypes(
const std::vector<TypeNode>& dtts, uint32_t flags)
{
- if ((flags & ExprManager::DATATYPE_FLAG_PLACEHOLDER) == 0)
+ if ((flags & NodeManager::DATATYPE_FLAG_PLACEHOLDER) == 0)
{
std::vector<Type> types;
for (const TypeNode& dt : dtts)
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%)" \
// must convert all constructors to version with variables in "vars"
std::vector<SygusDatatype> sdts;
- std::set<Type> unres;
+ std::set<TypeNode> unres;
Trace("dtsygus-gen-debug") << "Process sygus type:" << std::endl;
Trace("dtsygus-gen-debug") << sdtd.getName() << std::endl;
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
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);
}
Trace("dtsygus-gen-debug")
<< "Make " << sdts.size() << " datatype types..." << std::endl;
// extract the datatypes
- std::vector<Datatype> datatypes;
+ std::vector<DType> datatypes;
for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++)
{
datatypes.push_back(sdts[i].getDatatype());
}
// make the datatype types
- std::vector<DatatypeType> datatypeTypes =
- nm->toExprManager()->mkMutualDatatypeTypes(
- datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
- TypeNode sdtS = TypeNode::fromType(datatypeTypes[0]);
+ std::vector<TypeNode> 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++)
{
#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"
#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"
**/
#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"
#include <unordered_set>
#include "context/cdhashmap.h"
-#include "expr/datatype.h"
#include "expr/node.h"
#include "expr/type_node.h"
#include "theory/quantifiers/quant_util.h"
#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"
std::string veName("_virtual_enum_grammar");
SygusDatatype sdt(veName);
TypeNode u = nm->mkSort(veName, ExprManager::SORT_FLAG_PLACEHOLDER);
- std::set<Type> unresolvedTypes;
- unresolvedTypes.insert(u.toType());
+ std::set<TypeNode> unresolvedTypes;
+ unresolvedTypes.insert(u);
std::vector<TypeNode> cargsEmpty;
Node cr = nm->mkConst(Rational(1));
sdt.addConstructor(cr, "1", cargsEmpty);
cargsPlus.push_back(u);
sdt.addConstructor(PLUS, cargsPlus);
sdt.initializeDatatype(nm->integerType(), bvl, false, false);
- std::vector<Datatype> datatypes;
+ std::vector<DType> datatypes;
datatypes.push_back(sdt.getDatatype());
- std::vector<DatatypeType> 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<TypeNode> 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);
}
#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"
#include <stack>
-#include "expr/datatype.h"
#include "options/quantifiers_options.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/datatypes/sygus_datatype_utils.h"
return visited[n];
}
-
-TypeNode CegGrammarConstructor::mkUnresolvedType(const std::string& name, std::set<Type>& unres) {
+TypeNode CegGrammarConstructor::mkUnresolvedType(const std::string& name,
+ std::set<TypeNode>& unres)
+{
TypeNode unresolved = NodeManager::currentNM()->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER);
- unres.insert( unresolved.toType() );
+ unres.insert(unresolved);
return unresolved;
}
include_cons,
std::unordered_set<Node, NodeHashFunction>& term_irrelevant,
std::vector<SygusDatatypeGenerator>& sdts,
- std::set<Type>& unres)
+ std::set<TypeNode>& unres)
{
NodeManager* nm = NodeManager::currentNM();
Trace("sygus-grammar-def") << "Construct default grammar for " << fun << " "
{
Trace("sygus-grammar-def") << " ...using " << it->second.size() << " extra constants for " << it->first << std::endl;
}
- std::set<Type> unres;
+ std::set<TypeNode> unres;
std::vector<SygusDatatypeGenerator> sdts;
mkSygusDefaultGrammar(range,
bvl,
sdts,
unres);
// extract the datatypes from the sygus datatype generator objects
- std::vector<Datatype> datatypes;
+ std::vector<DType> 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<DatatypeType> types =
- NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(
- datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
+ std::vector<TypeNode> 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,
return templ_arg_sygus_type;
}else{
tcount++;
- std::set<Type> unres;
+ std::set<TypeNode> unres;
std::vector<SygusDatatype> sdts;
std::stringstream ssd;
ssd << fun << "_templ_" << tcount;
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<Datatype> datatypes;
+ std::vector<DType> datatypes;
for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++)
{
datatypes.push_back(sdts[i].getDatatype());
}
- std::vector<DatatypeType> types =
- NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(
- datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
+ std::vector<TypeNode> types =
+ NodeManager::currentNM()->mkMutualDatatypeTypes(
+ datatypes, unres, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
Assert(types.size() == 1);
- return TypeNode::fromType( types[0] );
+ return types[0];
}
}
};
// helper for mkSygusDefaultGrammar (makes unresolved type for mutually recursive datatype construction)
- static TypeNode mkUnresolvedType(const std::string& name, std::set<Type>& unres);
+ static TypeNode mkUnresolvedType(const std::string& name,
+ std::set<TypeNode>& unres);
// collect the list of types that depend on type range
static void collectSygusGrammarTypesFor(TypeNode range,
std::vector<TypeNode>& types);
include_cons,
std::unordered_set<Node, NodeHashFunction>& term_irrelevant,
std::vector<SygusDatatypeGenerator>& sdts,
- std::set<Type>& unres);
+ std::set<TypeNode>& unres);
// helper function for mkSygusTemplateType
static TypeNode mkSygusTemplateTypeRec(Node templ,
#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"
<< "...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";
}
// 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];
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<DatatypeType> types =
- NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(
- d_dt_all, d_unres_t_all, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
+ std::vector<TypeNode> 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
#include <string>
#include <vector>
-#include "expr/datatype.h"
#include "expr/node.h"
#include "expr/sygus_datatype.h"
#include "expr/type.h"
*/
TNode d_sygus_vars;
/* Datatypes to be resolved */
- std::vector<Datatype> d_dt_all;
+ std::vector<DType> d_dt_all;
/* Types to be resolved */
- std::set<Type> d_unres_t_all;
+ std::set<TypeNode> d_unres_t_all;
/* Associates type nodes with OpPosTries */
std::map<TypeNode, OpPosTrie> d_tries;
/* Map of type nodes into their identity operators (\lambda x. x) */
#include <map>
#include <vector>
-#include "expr/datatype.h"
#include "expr/node.h"
namespace CVC4 {
#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 {
std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> include_cons;
getIncludeCons(axioms, conj, include_cons);
std::unordered_set<Node, NodeHashFunction> 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;
// 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<Node> iplc;
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;
**/
#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"
#include <stack>
-#include "expr/datatype.h"
#include "options/quantifiers_options.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
**/
#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"
#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"
**/
#include "theory/sets/theory_sets_rels.h"
-#include "expr/datatype.h"
#include "theory/sets/theory_sets_private.h"
#include "theory/sets/theory_sets.h"
#include <unordered_set>
#include "expr/array_store_all.h"
+#include "expr/dtype.h"
#include "expr/expr_manager.h"
#include "expr/kind.h"
#include "expr/node_manager.h"
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<DTypeConstructor>("red"));
+ dt.addConstructor(std::make_shared<DTypeConstructor>("orange"));
+ dt.addConstructor(std::make_shared<DTypeConstructor>("yellow"));
+ dt.addConstructor(std::make_shared<DTypeConstructor>("green"));
+ dt.addConstructor(std::make_shared<DTypeConstructor>("blue"));
+ dt.addConstructor(std::make_shared<DTypeConstructor>("violet"));
+ TypeNode datatype = d_nm->mkDatatypeType(dt);
+ const std::vector<std::shared_ptr<DTypeConstructor> >& 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<DTypeConstructor>("red"));
+ colors.addConstructor(std::make_shared<DTypeConstructor>("orange"));
+ colors.addConstructor(std::make_shared<DTypeConstructor>("yellow"));
+ colors.addConstructor(std::make_shared<DTypeConstructor>("green"));
+ colors.addConstructor(std::make_shared<DTypeConstructor>("blue"));
+ colors.addConstructor(std::make_shared<DTypeConstructor>("violet"));
+ TypeNode colorsType = d_nm->mkDatatypeType(colors);
+ const std::vector<std::shared_ptr<DTypeConstructor> >& ctCons =
+ colorsType.getDType().getConstructors();
+ DType listColors("ListColors");
+ std::shared_ptr<DTypeConstructor> consC =
+ std::make_shared<DTypeConstructor>("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<DTypeConstructor>("nil"));
+ TypeNode listColorsType = d_nm->mkDatatypeType(listColors);
+ const std::vector<std::shared_ptr<DTypeConstructor> >& 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() );
TS_ASSERT( ! te.isFinished() );
}
- void NOTYETtestDatatypesInfinite2() {
+ void NOTYETtestDTypesInfinite2()
+ {
//TypeNode datatype;
//TypeEnumerator te(datatype);
//TS_ASSERT( ! te.isFinished() );
projects / cvc5.git / commitdiff