namespace CVC4 {
-namespace expr {
- namespace attr {
- struct DatatypeIndexTag {};
- struct DatatypeConsIndexTag {};
- struct DatatypeFiniteTag {};
- struct DatatypeFiniteComputedTag {};
- struct DatatypeUFiniteTag {};
- struct DatatypeUFiniteComputedTag {};
- }/* CVC4::expr::attr namespace */
-}/* CVC4::expr namespace */
-
-typedef expr::Attribute<expr::attr::DatatypeIndexTag, uint64_t> DatatypeIndexAttr;
-typedef expr::Attribute<expr::attr::DatatypeConsIndexTag, uint64_t> DatatypeConsIndexAttr;
-typedef expr::Attribute<expr::attr::DatatypeFiniteTag, bool> DatatypeFiniteAttr;
-typedef expr::Attribute<expr::attr::DatatypeFiniteComputedTag, bool> DatatypeFiniteComputedAttr;
-typedef expr::Attribute<expr::attr::DatatypeUFiniteTag, bool> DatatypeUFiniteAttr;
-typedef expr::Attribute<expr::attr::DatatypeUFiniteComputedTag, bool> DatatypeUFiniteComputedAttr;
+Datatype::~Datatype()
+{
+ ExprManagerScope ems(*d_em);
+ d_internal.reset();
+ d_constructors.clear();
+ delete d_record;
+}
Datatype::Datatype(ExprManager* em, std::string name, bool isCo)
: d_em(em),
- d_name(name),
- d_params(),
- d_isCo(isCo),
- d_isTuple(false),
- d_isRecord(false),
+ d_internal(nullptr),
d_record(NULL),
- d_constructors(),
- d_resolved(false),
- d_self(),
- d_involvesExt(false),
- d_involvesUt(false),
- d_sygus_allow_const(false),
- d_sygus_allow_all(false),
- d_card(CardinalityUnknown()),
- d_well_founded(0)
+ d_isRecord(false),
+ d_constructors()
{
+ ExprManagerScope ems(*d_em);
+ d_internal = std::make_shared<DType>(name, isCo);
}
Datatype::Datatype(ExprManager* em,
const std::vector<Type>& params,
bool isCo)
: d_em(em),
- d_name(name),
- d_params(params),
- d_isCo(isCo),
- d_isTuple(false),
- d_isRecord(false),
+ d_internal(nullptr),
d_record(NULL),
- d_constructors(),
- d_resolved(false),
- d_self(),
- d_involvesExt(false),
- d_involvesUt(false),
- d_sygus_allow_const(false),
- d_sygus_allow_all(false),
- d_card(CardinalityUnknown()),
- d_well_founded(0)
+ d_isRecord(false),
+ d_constructors()
{
-}
-
-Datatype::~Datatype(){
- delete d_record;
+ 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) {
if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){
return indexOf( item[0] );
}else{
- Assert(n.hasAttribute(DatatypeIndexAttr()));
- return n.getAttribute(DatatypeIndexAttr());
+ Assert(n.hasAttribute(DTypeIndexAttr()));
+ return n.getAttribute(DTypeIndexAttr());
}
}
if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){
return cindexOf( item[0] );
}else{
- Assert(n.hasAttribute(DatatypeConsIndexAttr()));
- return n.getAttribute(DatatypeConsIndexAttr());
+ Assert(n.hasAttribute(DTypeConsIndexAttr()));
+ return n.getAttribute(DTypeConsIndexAttr());
}
}
-void Datatype::resolve(ExprManager* em,
- const std::map<std::string, DatatypeType>& resolutions,
+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)
+ const std::vector<SortConstructorType>& paramTypes,
+ const std::vector<DatatypeType>& paramReplacements)
{
- PrettyCheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager");
- PrettyCheckArgument(!d_resolved, this, "cannot resolve a Datatype twice");
- PrettyCheckArgument(resolutions.find(d_name) != resolutions.end(), resolutions,
- "Datatype::resolve(): resolutions doesn't contain me!");
+ 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");
- DatatypeType self = (*resolutions.find(d_name)).second;
- PrettyCheckArgument(&self.getDatatype() == this, resolutions, "Datatype::resolve(): resolutions doesn't contain me!");
- d_resolved = true;
- size_t index = 0;
- for(std::vector<DatatypeConstructor>::iterator i = d_constructors.begin(), i_end = d_constructors.end(); i != i_end; ++i) {
- (*i).resolve(em, self, resolutions, placeholders, replacements, paramTypes, paramReplacements, index);
- Node::fromExpr((*i).d_constructor).setAttribute(DatatypeIndexAttr(), index);
- Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++);
- }
- d_self = self;
- d_involvesExt = false;
- d_involvesUt = false;
- for(const_iterator i = begin(); i != end(); ++i) {
- if( (*i).involvesExternalType() ){
- d_involvesExt = true;
- }
- if( (*i).involvesUninterpretedType() ){
- d_involvesUt = true;
+ // 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();
}
}
}
d_record = new Record(fields);
}
-
- if (isSygus())
- {
- // all datatype constructors should be sygus and have sygus operators whose
- // free variables are subsets of sygus bound var list.
- Node sbvln = Node::fromExpr(d_sygus_bvl);
- std::unordered_set<Node, NodeHashFunction> svs;
- for (const Node& sv : sbvln)
- {
- svs.insert(sv);
- }
- for (unsigned i = 0, ncons = d_constructors.size(); i < ncons; i++)
- {
- Expr sop = d_constructors[i].getSygusOp();
- PrettyCheckArgument(!sop.isNull(),
- this,
- "Sygus datatype contains a non-sygus constructor");
- Node sopn = Node::fromExpr(sop);
- std::unordered_set<Node, NodeHashFunction> fvs;
- expr::getFreeVariables(sopn, fvs);
- for (const Node& v : fvs)
- {
- PrettyCheckArgument(
- svs.find(v) != svs.end(),
- this,
- "Sygus constructor has an operator with a free variable that is "
- "not in the formal argument list of the function-to-synthesize");
- }
- }
- }
}
void Datatype::addConstructor(const DatatypeConstructor& c) {
- PrettyCheckArgument(!d_resolved, this,
- "cannot add a constructor to a finalized Datatype");
+ 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(!d_resolved, this,
- "cannot set sygus type to a finalized Datatype");
- d_sygus_type = st;
- d_sygus_bvl = bvl;
- d_sygus_allow_const = allow_const || allow_all;
- d_sygus_allow_all = allow_all;
+ PrettyCheckArgument(
+ !isResolved(), this, "cannot set sygus type to a finalized Datatype");
+ TypeNode stn = TypeNode::fromType(st);
+ Node bvln = Node::fromExpr(bvl);
+ d_internal->setSygus(stn, bvln, allow_const, allow_all);
}
void Datatype::addSygusConstructor(Expr op,
std::shared_ptr<SygusPrintCallback> spc,
int weight)
{
- Debug("dt-sygus") << "--> Add constructor " << cname << " to " << getName() << std::endl;
- Debug("dt-sygus") << " sygus op : " << op << std::endl;
// avoid name clashes
std::stringstream ss;
ss << getName() << "_" << getNumConstructors() << "_" << cname;
}
void Datatype::setTuple() {
- PrettyCheckArgument(!d_resolved, this, "cannot set tuple to a finalized Datatype");
- d_isTuple = true;
+ PrettyCheckArgument(
+ !isResolved(), this, "cannot set tuple to a finalized Datatype");
+ d_internal->setTuple();
}
void Datatype::setRecord() {
- PrettyCheckArgument(!d_resolved, this, "cannot set record to a finalized Datatype");
+ PrettyCheckArgument(
+ !isResolved(), this, "cannot set record to a finalized Datatype");
d_isRecord = true;
}
{
PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this);
- std::vector< Type > processing;
- computeCardinality( t, processing );
- return d_card;
+ 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");
- return getCardinality( d_self );
-}
-
-Cardinality Datatype::computeCardinality(Type t,
- std::vector<Type>& processing) const
-{
- PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
- if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){
- d_card = Cardinality::INTEGERS;
- }else{
- processing.push_back( d_self );
- Cardinality c = 0;
- for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
- c += (*i).computeCardinality( t, processing );
- }
- d_card = c;
- processing.pop_back();
- }
- return d_card;
+ 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);
- if( d_card_rec_singleton.find( t )==d_card_rec_singleton.end() ){
- if( isCodatatype() ){
- Assert(d_card_u_assume[t].empty());
- std::vector< Type > processing;
- if( computeCardinalityRecSingleton( t, processing, d_card_u_assume[t] ) ){
- d_card_rec_singleton[t] = 1;
- }else{
- d_card_rec_singleton[t] = -1;
- }
- if( d_card_rec_singleton[t]==1 ){
- Trace("dt-card") << "Datatype " << getName() << " is recursive singleton, dependent upon " << d_card_u_assume[t].size() << " uninterpreted sorts: " << std::endl;
- for( unsigned i=0; i<d_card_u_assume[t].size(); i++ ){
- Trace("dt-card") << " " << d_card_u_assume[t][i] << std::endl;
- }
- Trace("dt-card") << std::endl;
- }
- }else{
- d_card_rec_singleton[t] = -1;
- }
- }
- return d_card_rec_singleton[t]==1;
+ 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");
- return isRecursiveSingleton( d_self );
+ ExprManagerScope ems(d_self);
+ return d_internal->isRecursiveSingleton();
}
unsigned Datatype::getNumRecursiveSingletonArgTypes(Type t) const
{
- Assert(d_card_rec_singleton.find(t) != d_card_rec_singleton.end());
Assert(isRecursiveSingleton(t));
- return d_card_u_assume[t].size();
+ 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");
- return getNumRecursiveSingletonArgTypes( d_self );
+ ExprManagerScope ems(d_self);
+ return d_internal->getNumRecursiveSingletonArgTypes();
}
Type Datatype::getRecursiveSingletonArgType(Type t, unsigned i) const
{
- Assert(d_card_rec_singleton.find(t) != d_card_rec_singleton.end());
Assert(isRecursiveSingleton(t));
- return d_card_u_assume[t][i];
+ 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");
- return getRecursiveSingletonArgType( d_self, i );
-}
-
-bool Datatype::computeCardinalityRecSingleton(Type t,
- std::vector<Type>& processing,
- std::vector<Type>& u_assume) const
-{
- if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){
- return true;
- }else{
- if( d_card_rec_singleton[t]==0 ){
- //if not yet computed
- if( d_constructors.size()==1 ){
- bool success = false;
- processing.push_back( d_self );
- for(unsigned i = 0; i<d_constructors[0].getNumArgs(); i++ ) {
- Type tc = ((SelectorType)d_constructors[0][i].getType()).getRangeType();
- //if it is an uninterpreted sort, then we depend on it having cardinality one
- if( tc.isSort() ){
- if( std::find( u_assume.begin(), u_assume.end(), tc )==u_assume.end() ){
- u_assume.push_back( tc );
- }
- //if it is a datatype, recurse
- }else if( tc.isDatatype() ){
- const Datatype & dt = ((DatatypeType)tc).getDatatype();
- if( !dt.computeCardinalityRecSingleton( t, processing, u_assume ) ){
- return false;
- }else{
- success = true;
- }
- //if it is a builtin type, it must have cardinality one
- }else if( !tc.getCardinality().isOne() ){
- return false;
- }
- }
- processing.pop_back();
- return success;
- }else{
- return false;
- }
- }else if( d_card_rec_singleton[t]==-1 ){
- return false;
- }else{
- for( unsigned i=0; i<d_card_u_assume[t].size(); i++ ){
- if( std::find( u_assume.begin(), u_assume.end(), d_card_u_assume[t][i] )==u_assume.end() ){
- u_assume.push_back( d_card_u_assume[t][i] );
- }
- }
- return true;
- }
- }
+ 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);
-
- // we're using some internals, so we have to set up this library context
ExprManagerScope ems(d_self);
- TypeNode self = TypeNode::fromType(d_self);
- // is this already in the cache ?
- if(self.getAttribute(DatatypeFiniteComputedAttr())) {
- return self.getAttribute(DatatypeFiniteAttr());
- }
- for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
- if(! (*i).isFinite( t )) {
- self.setAttribute(DatatypeFiniteComputedAttr(), true);
- self.setAttribute(DatatypeFiniteAttr(), false);
- return false;
- }
- }
- self.setAttribute(DatatypeFiniteComputedAttr(), true);
- self.setAttribute(DatatypeFiniteAttr(), true);
- return true;
+ 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");
- return isFinite( d_self );
+ 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);
- // we're using some internals, so we have to set up this library context
ExprManagerScope ems(d_self);
- TypeNode self = TypeNode::fromType(d_self);
- // is this already in the cache ?
- if(self.getAttribute(DatatypeUFiniteComputedAttr())) {
- return self.getAttribute(DatatypeUFiniteAttr());
- }
- //start by assuming it is not
- self.setAttribute(DatatypeUFiniteComputedAttr(), true);
- self.setAttribute(DatatypeUFiniteAttr(), false);
- for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
- if(! (*i).isInterpretedFinite( t )) {
- return false;
- }
- }
- self.setAttribute(DatatypeUFiniteComputedAttr(), true);
- self.setAttribute(DatatypeUFiniteAttr(), true);
- return true;
+ 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");
- return isInterpretedFinite( d_self );
+ ExprManagerScope ems(d_self);
+ return d_internal->isInterpretedFinite();
}
bool Datatype::isWellFounded() const
{
- PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
- if( d_well_founded==0 ){
- // we're using some internals, so we have to set up this library context
- ExprManagerScope ems(d_self);
- std::vector< Type > processing;
- if( computeWellFounded( processing ) ){
- d_well_founded = 1;
- }else{
- d_well_founded = -1;
- }
- }
- return d_well_founded==1;
-}
-
-bool Datatype::computeWellFounded(std::vector<Type>& processing) const
-{
- PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
- if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){
- return d_isCo;
- }else{
- processing.push_back( d_self );
- for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
- if( (*i).computeWellFounded( processing ) ){
- processing.pop_back();
- return true;
- }else{
- Trace("dt-wf") << "Constructor " << (*i).getName() << " is not well-founded." << std::endl;
- }
- }
- processing.pop_back();
- Trace("dt-wf") << "Datatype " << getName() << " is not well-founded." << std::endl;
- return false;
- }
+ ExprManagerScope ems(d_self);
+ return d_internal->isWellFounded();
}
Expr Datatype::mkGroundTerm(Type t) const
{
PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
- return mkGroundTermInternal(t, false);
+ 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");
- return mkGroundTermInternal(t, true);
-}
-
-Expr Datatype::mkGroundTermInternal(Type t, bool isValue) const
-{
ExprManagerScope ems(d_self);
- Debug("datatypes") << "mkGroundTerm of type " << t
- << ", isValue = " << isValue << std::endl;
- // is this already in the cache ?
- std::map<Type, Expr>& cache = isValue ? d_ground_value : d_ground_term;
- std::map<Type, Expr>::iterator it = cache.find(t);
- if (it != cache.end())
- {
- Debug("datatypes") << "\nin cache: " << d_self << " => " << it->second << std::endl;
- return it->second;
- }
- std::vector<Type> processing;
- Expr groundTerm = computeGroundTerm(t, processing, isValue);
- if (!groundTerm.isNull())
- {
- // we found a ground-term-constructing constructor!
- cache[t] = groundTerm;
- Debug("datatypes") << "constructed: " << getName() << " => " << groundTerm
- << std::endl;
- }
- if (groundTerm.isNull())
- {
- if (!d_isCo)
- {
- // if we get all the way here, we aren't well-founded
- IllegalArgument(
- *this,
- "datatype is not well-founded, cannot construct a ground term!");
- }
- }
- return groundTerm;
-}
-
-Expr getSubtermWithType( Expr e, Type t, bool isTop ){
- if( !isTop && e.getType()==t ){
- return e;
- }else{
- for( unsigned i=0; i<e.getNumChildren(); i++ ){
- Expr se = getSubtermWithType( e[i], t, false );
- if( !se.isNull() ){
- return se;
- }
- }
- return Expr();
- }
-}
-
-Expr Datatype::computeGroundTerm(Type t,
- std::vector<Type>& processing,
- bool isValue) const
-{
- if( std::find( processing.begin(), processing.end(), t )==processing.end() ){
- processing.push_back( t );
- for( unsigned r=0; r<2; r++ ){
- for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
- //do nullary constructors first
- if( ((*i).getNumArgs()==0)==(r==0)){
- Debug("datatypes") << "Try constructing for " << (*i).getName() << ", processing = " << processing.size() << std::endl;
- Expr e =
- (*i).computeGroundTerm(t, processing, d_ground_term, isValue);
- if( !e.isNull() ){
- //must check subterms for the same type to avoid infinite loops in type enumeration
- Expr se = getSubtermWithType( e, t, true );
- if( !se.isNull() ){
- Debug("datatypes") << "Take subterm " << se << std::endl;
- e = se;
- }
- processing.pop_back();
- return e;
- }else{
- Debug("datatypes") << "...failed." << std::endl;
- }
- }
- }
- }
- processing.pop_back();
- }else{
- Debug("datatypes") << "...already processing " << t << " " << d_self << std::endl;
- }
- return Expr();
+ 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");
- PrettyCheckArgument(!d_self.isNull(), *this);
- return DatatypeType(d_self);
+ 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");
- PrettyCheckArgument(!d_self.isNull() && DatatypeType(d_self).isParametric(), this);
- return DatatypeType(d_self).instantiate(params);
+ 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
if(this == &other) {
return true;
}
-
- if(isResolved() != other.isResolved()) {
- return false;
- }
-
- if( d_name != other.d_name ||
- getNumConstructors() != other.getNumConstructors() ) {
- return false;
- }
- for(const_iterator i = begin(), j = other.begin(); i != end(); ++i, ++j) {
- Assert(j != other.end());
- // two constructors are == iff they have the same name, their
- // constructors and testers are equal and they have exactly
- // matching args (in the same order)
- if((*i).getName() != (*j).getName() ||
- (*i).getNumArgs() != (*j).getNumArgs()) {
- return false;
- }
- // testing equivalence of constructors and testers is harder b/c
- // this constructor might not be resolved yet; only compare them
- // if they are both resolved
- Assert(isResolved() == !(*i).d_constructor.isNull()
- && isResolved() == !(*i).d_tester.isNull()
- && (*i).d_constructor.isNull() == (*j).d_constructor.isNull()
- && (*i).d_tester.isNull() == (*j).d_tester.isNull());
- if(!(*i).d_constructor.isNull() && (*i).d_constructor != (*j).d_constructor) {
- return false;
- }
- if(!(*i).d_tester.isNull() && (*i).d_tester != (*j).d_tester) {
- return false;
- }
- for(DatatypeConstructor::const_iterator k = (*i).begin(), l = (*j).begin(); k != (*i).end(); ++k, ++l) {
- Assert(l != (*j).end());
- if((*k).getName() != (*l).getName()) {
- return false;
- }
- // testing equivalence of selectors is harder b/c args might not
- // be resolved yet
- Assert(isResolved() == (*k).isResolved()
- && (*k).isResolved() == (*l).isResolved());
- if((*k).isResolved()) {
- // both are resolved, so simply compare the selectors directly
- if((*k).d_selector != (*l).d_selector) {
- return false;
- }
- } else {
- // neither is resolved, so compare their (possibly unresolved)
- // types; we don't know if they'll be resolved the same way,
- // so we can't ever say unresolved types are equal
- if(!(*k).d_selector.isNull() && !(*l).d_selector.isNull()) {
- if((*k).d_selector.getType() != (*l).d_selector.getType()) {
- return false;
- }
- } else {
- if((*k).isUnresolvedSelf() && (*l).isUnresolvedSelf()) {
- // Fine, the selectors are equal if the rest of the
- // enclosing datatypes are equal...
- } else {
- return false;
- }
- }
- }
- }
- }
return true;
}
return *i;
}
}
- IllegalArgument(name, "No such constructor `%s' of datatype `%s'", name.c_str(), d_name.c_str());
-}
-
-
-Expr Datatype::getSharedSelector( Type dtt, Type t, unsigned index ) const{
- PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
- std::map< Type, std::map< Type, std::map< unsigned, Expr > > >::iterator itd = d_shared_sel.find( dtt );
- if( itd!=d_shared_sel.end() ){
- std::map< Type, std::map< unsigned, Expr > >::iterator its = itd->second.find( t );
- if( its!=itd->second.end() ){
- std::map< unsigned, Expr >::iterator it = its->second.find( index );
- if( it!=its->second.end() ){
- return it->second;
- }
- }
- }
- //make the shared selector
- Expr s;
- NodeManager* nm = NodeManager::fromExprManager( d_self.getExprManager() );
- std::stringstream ss;
- ss << "sel_" << index;
- s = nm->mkSkolem(ss.str(), nm->mkSelectorType(TypeNode::fromType(dtt), TypeNode::fromType(t)), "is a shared selector", NodeManager::SKOLEM_NO_NOTIFY).toExpr();
- d_shared_sel[dtt][t][index] = s;
- Trace("dt-shared-sel") << "Made " << s << " of type " << dtt << " -> " << t << std::endl;
- return s;
+ 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 {
}
Type Datatype::getSygusType() const {
- return d_sygus_type;
+ return d_internal->getSygusType().toType();
}
Expr Datatype::getSygusVarList() const {
- return d_sygus_bvl;
+ return d_internal->getSygusVarList().toExpr();
}
bool Datatype::getSygusAllowConst() const {
- return d_sygus_allow_const;
+ return d_internal->getSygusAllowConst();
}
bool Datatype::getSygusAllowAll() const {
- return d_sygus_allow_all;
+ return d_internal->getSygusAllowAll();
}
bool Datatype::involvesExternalType() const{
- return d_involvesExt;
+ return d_internal->involvesExternalType();
}
bool Datatype::involvesUninterpretedType() const{
- return d_involvesUt;
+ return d_internal->involvesUninterpretedType();
}
const std::vector<DatatypeConstructor>* Datatype::getConstructors() const
return &d_constructors;
}
-void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
- 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, size_t cindex)
-{
- PrettyCheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager");
- PrettyCheckArgument(!isResolved(),
- "cannot resolve a Datatype constructor twice; "
- "perhaps the same constructor was added twice, "
- "or to two datatypes?");
-
- // we're using some internals, so we have to set up this library context
- ExprManagerScope ems(*em);
-
- NodeManager* nm = NodeManager::fromExprManager(em);
- TypeNode selfTypeNode = TypeNode::fromType(self);
- size_t index = 0;
- for(std::vector<DatatypeConstructorArg>::iterator i = d_args.begin(), i_end = d_args.end(); i != i_end; ++i) {
- if((*i).d_selector.isNull()) {
- // the unresolved type wasn't created here; do name resolution
- string typeName = (*i).d_name.substr((*i).d_name.find('\0') + 1);
- (*i).d_name.resize((*i).d_name.find('\0'));
- if(typeName == "") {
- (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, selfTypeNode), "is a selector", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
- } else {
- map<string, DatatypeType>::const_iterator j = resolutions.find(typeName);
- if(j == resolutions.end()) {
- stringstream msg;
- msg << "cannot resolve type \"" << typeName << "\" "
- << "in selector \"" << (*i).d_name << "\" "
- << "of constructor \"" << d_name << "\"";
- throw DatatypeResolutionException(msg.str());
- } else {
- (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType((*j).second)), "is a selector", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
- }
- }
- } else {
- // the type for the selector already exists; may need
- // complex-type substitution
- Type range = (*i).d_selector.getType();
- if(!placeholders.empty()) {
- range = range.substitute(placeholders, replacements);
- }
- if(!paramTypes.empty() ) {
- range = doParametricSubstitution( range, paramTypes, paramReplacements );
- }
- (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType(range)), "is a selector", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
- }
- Node::fromExpr((*i).d_selector).setAttribute(DatatypeConsIndexAttr(), cindex);
- Node::fromExpr((*i).d_selector).setAttribute(DatatypeIndexAttr(), index++);
- (*i).d_resolved = true;
- }
-
- Assert(index == getNumArgs());
-
- // Set constructor/tester last, since DatatypeConstructor::isResolved()
- // returns true when d_tester is not the null Expr. If something
- // fails above, we want Constuctor::isResolved() to remain "false".
- // Further, mkConstructorType() iterates over the selectors, so
- // should get the results of any resolutions we did above.
- d_tester = nm->mkSkolem(getTesterName(), nm->mkTesterType(selfTypeNode), "is a tester", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
- d_constructor = nm->mkSkolem(getName(), nm->mkConstructorType(*this, selfTypeNode), "is a constructor", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
- // associate constructor with all selectors
- for(std::vector<DatatypeConstructorArg>::iterator i = d_args.begin(), i_end = d_args.end(); i != i_end; ++i) {
- (*i).d_constructor = d_constructor;
- }
-}
-
-Type DatatypeConstructor::doParametricSubstitution( Type range,
- const std::vector< SortConstructorType >& paramTypes,
- const std::vector< DatatypeType >& paramReplacements ) {
- TypeNode typn = TypeNode::fromType( range );
- if(typn.getNumChildren() == 0) {
- return range;
- } else {
- std::vector< Type > origChildren;
- std::vector< Type > children;
- for(TypeNode::const_iterator i = typn.begin(), iend = typn.end();i != iend; ++i) {
- origChildren.push_back( (*i).toType() );
- children.push_back( doParametricSubstitution( (*i).toType(), paramTypes, paramReplacements ) );
- }
- for( unsigned i = 0; i < paramTypes.size(); ++i ) {
- if( paramTypes[i].getArity() == origChildren.size() ) {
- Type tn = paramTypes[i].instantiate( origChildren );
- if( range == tn ) {
- return paramReplacements[i].instantiate( children );
- }
- }
- }
- NodeBuilder<> nb(typn.getKind());
- for( unsigned i = 0; i < children.size(); ++i ) {
- nb << TypeNode::fromType( children[i] );
- }
- return nb.constructTypeNode().toType();
- }
-}
-
DatatypeConstructor::DatatypeConstructor(std::string name)
- : // 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 tester name away inside the constructor name until
- // resolution.
- d_internal(nullptr), // until the Node-level datatype API is activated
- d_name(name + '\0' + "is_" + name), // default tester name is "is_FOO"
- d_tester(),
- d_args(),
- d_sygus_pc(nullptr),
- d_weight(1)
+ : d_internal(nullptr),
+ d_testerName("is_" + name) // default tester name is "is_FOO"
{
PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
+ d_internal = std::make_shared<DTypeConstructor>(name, 1);
}
DatatypeConstructor::DatatypeConstructor(std::string name,
std::string tester,
unsigned weight)
- : // 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 tester name away inside the constructor name until
- // resolution.
- d_internal(nullptr), // until the Node-level datatype API is activated
- d_name(name + '\0' + tester),
- d_tester(),
- d_args(),
- d_sygus_pc(nullptr),
- d_weight(weight)
+ : d_internal(nullptr), d_testerName(tester)
{
PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
PrettyCheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
+ d_internal = std::make_shared<DTypeConstructor>(name, weight);
}
void DatatypeConstructor::setSygus(Expr op,
{
PrettyCheckArgument(
!isResolved(), this, "cannot modify a finalized Datatype constructor");
- d_sygus_op = op;
+ Node opn = Node::fromExpr(op);
+ d_internal->setSygus(op);
+ // print callback lives at the expression level currently
d_sygus_pc = spc;
}
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) {
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) {
// 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_name.substr(0, d_name.find('\0'));
+ return d_internal->getName();
}
std::string DatatypeConstructor::getTesterName() const
{
- return d_name.substr(d_name.find('\0') + 1);
+ // not stored internally, since tester names only pertain to parsing
+ return d_testerName;
}
Expr DatatypeConstructor::getConstructor() 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);
- const Datatype& dt = Datatype::datatypeOf(d_constructor);
- PrettyCheckArgument(dt.isParametric(), this, "this datatype constructor is not parametric");
- TypeNode dtt = TypeNode::fromType(dt.getDatatypeType());
- TypeMatcher m(dtt);
- m.doMatching(dtt, TypeNode::fromType(returnType));
- std::vector<TypeNode> sns;
- m.getMatches(sns);
- std::vector<Type> subst;
- for (TypeNode& s : sns)
- {
- subst.push_back(s.toType());
- }
- vector<Type> params = dt.getParameters();
- return d_constructor.getType().substitute(params, subst);
+ 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");
- return d_tester;
+ ExprManagerScope ems(d_constructor);
+ return d_internal->getTester().toExpr();
}
Expr DatatypeConstructor::getSygusOp() const {
PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
- return d_sygus_op;
+ ExprManagerScope ems(d_constructor);
+ return d_internal->getSygusOp().toExpr();
}
bool DatatypeConstructor::isSygusIdFunc() const {
PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
- return (d_sygus_op.getKind() == kind::LAMBDA
- && d_sygus_op[0].getNumChildren() == 1
- && d_sygus_op[0][0] == d_sygus_op[1]);
+ ExprManagerScope ems(d_constructor);
+ return d_internal->isSygusIdFunc();
}
unsigned DatatypeConstructor::getWeight() const
{
PrettyCheckArgument(
isResolved(), this, "this datatype constructor is not yet resolved");
- return d_weight;
+ ExprManagerScope ems(d_constructor);
+ return d_internal->getWeight();
}
std::shared_ptr<SygusPrintCallback> DatatypeConstructor::getSygusPrintCallback() const
Cardinality DatatypeConstructor::getCardinality(Type t) const
{
PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
-
- Cardinality c = 1;
-
- for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
- c *= SelectorType((*i).getSelector().getType()).getRangeType().getCardinality();
- }
-
- return c;
-}
-
-/** compute the cardinality of this datatype */
-Cardinality DatatypeConstructor::computeCardinality(
- Type t, std::vector<Type>& processing) const
-{
- Cardinality c = 1;
- std::vector< Type > instTypes;
- std::vector< Type > paramTypes;
- if( DatatypeType(t).isParametric() ){
- paramTypes = DatatypeType(t).getDatatype().getParameters();
- instTypes = DatatypeType(t).getParamTypes();
- }
- for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
- Type tc = SelectorType((*i).getSelector().getType()).getRangeType();
- if( DatatypeType(t).isParametric() ){
- tc = tc.substitute( paramTypes, instTypes );
- }
- if( tc.isDatatype() ){
- const Datatype& dt = ((DatatypeType)tc).getDatatype();
- c *= dt.computeCardinality( t, processing );
- }else{
- c *= tc.getCardinality();
- }
- }
- return c;
-}
-
-bool DatatypeConstructor::computeWellFounded(
- std::vector<Type>& processing) const
-{
- for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
- Type t = SelectorType((*i).getSelector().getType()).getRangeType();
- if( t.isDatatype() ){
- const Datatype& dt = ((DatatypeType)t).getDatatype();
- if( !dt.computeWellFounded( processing ) ){
- return false;
- }
- }
- }
- return true;
+ 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");
-
- // we're using some internals, so we have to set up this library context
ExprManagerScope ems(d_constructor);
- TNode self = Node::fromExpr(d_constructor);
- // is this already in the cache ?
- if(self.getAttribute(DatatypeFiniteComputedAttr())) {
- return self.getAttribute(DatatypeFiniteAttr());
- }
- std::vector< Type > instTypes;
- std::vector< Type > paramTypes;
- if( DatatypeType(t).isParametric() ){
- paramTypes = DatatypeType(t).getDatatype().getParameters();
- instTypes = DatatypeType(t).getParamTypes();
- }
- for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
- Type tc = (*i).getRangeType();
- if( DatatypeType(t).isParametric() ){
- tc = tc.substitute( paramTypes, instTypes );
- }
- if (!tc.isFinite())
- {
- self.setAttribute(DatatypeFiniteComputedAttr(), true);
- self.setAttribute(DatatypeFiniteAttr(), false);
- return false;
- }
- }
- self.setAttribute(DatatypeFiniteComputedAttr(), true);
- self.setAttribute(DatatypeFiniteAttr(), true);
- return true;
+ 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");
- // we're using some internals, so we have to set up this library context
ExprManagerScope ems(d_constructor);
- TNode self = Node::fromExpr(d_constructor);
- // is this already in the cache ?
- if(self.getAttribute(DatatypeUFiniteComputedAttr())) {
- return self.getAttribute(DatatypeUFiniteAttr());
- }
- std::vector< Type > instTypes;
- std::vector< Type > paramTypes;
- if( DatatypeType(t).isParametric() ){
- paramTypes = DatatypeType(t).getDatatype().getParameters();
- instTypes = DatatypeType(t).getParamTypes();
- }
- for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
- Type tc = (*i).getRangeType();
- if( DatatypeType(t).isParametric() ){
- tc = tc.substitute( paramTypes, instTypes );
- }
- TypeNode tcn = TypeNode::fromType( tc );
- if(!tcn.isInterpretedFinite()) {
- self.setAttribute(DatatypeUFiniteComputedAttr(), true);
- self.setAttribute(DatatypeUFiniteAttr(), false);
- return false;
- }
- }
- self.setAttribute(DatatypeUFiniteComputedAttr(), true);
- self.setAttribute(DatatypeUFiniteAttr(), true);
- return true;
+ TypeNode tn = TypeNode::fromType(t);
+ return d_internal->isInterpretedFinite(tn);
}
-Expr DatatypeConstructor::computeGroundTerm(Type t,
- std::vector<Type>& processing,
- std::map<Type, Expr>& gt,
- bool isValue) const
-{
- // we're using some internals, so we have to set up this library context
- ExprManagerScope ems(d_constructor);
-
- std::vector<Expr> groundTerms;
- groundTerms.push_back(getConstructor());
-
- // for each selector, get a ground term
- std::vector< Type > instTypes;
- std::vector< Type > paramTypes;
- bool isParam = static_cast<DatatypeType>(t).isParametric();
- if (isParam)
- {
- paramTypes = DatatypeType(t).getDatatype().getParameters();
- instTypes = DatatypeType(t).getParamTypes();
- }
- for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
- Type selType = SelectorType((*i).getSelector().getType()).getRangeType();
- if (isParam)
- {
- selType = selType.substitute( paramTypes, instTypes );
- }
- Expr arg;
- if( selType.isDatatype() ){
- std::map< Type, Expr >::iterator itgt = gt.find( selType );
- if( itgt != gt.end() ){
- arg = itgt->second;
- }else{
- const Datatype & dt = DatatypeType(selType).getDatatype();
- arg = dt.computeGroundTerm(selType, processing, isValue);
- }
- }
- else
- {
- // call mkGroundValue or mkGroundTerm based on isValue
- arg = isValue ? selType.mkGroundValue() : selType.mkGroundTerm();
- }
- if( arg.isNull() ){
- Debug("datatypes") << "...unable to construct arg of " << (*i).getName() << std::endl;
- return Expr();
- }else{
- Debug("datatypes") << "...constructed arg " << arg.getType() << std::endl;
- groundTerms.push_back(arg);
- }
- }
-
- Expr groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms);
- if (isParam)
- {
- Assert( Datatype::datatypeOf( d_constructor ).isParametric() );
- // type is parametric, must apply type ascription
- Debug("datatypes-gt") << "ambiguous type for " << groundTerm << ", ascribe to " << t << std::endl;
- groundTerms[0] = getConstructor().getExprManager()->mkExpr(kind::APPLY_TYPE_ASCRIPTION,
- getConstructor().getExprManager()->mkConst(AscriptionType(getSpecializedConstructorType(t))),
- groundTerms[0]);
- groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms);
- }
- return groundTerm;
-}
-
-void DatatypeConstructor::computeSharedSelectors( Type domainType ) const {
- if( d_shared_selectors[domainType].size()<getNumArgs() ){
- TypeNode ctype;
- if( DatatypeType(domainType).isParametric() ){
- ctype = TypeNode::fromType( getSpecializedConstructorType( domainType ) );
- }else{
- ctype = TypeNode::fromType( d_constructor.getType() );
- }
- Assert(ctype.isConstructor());
- Assert(ctype.getNumChildren() - 1 == getNumArgs());
- //compute the shared selectors
- const Datatype& dt = Datatype::datatypeOf(d_constructor);
- std::map< TypeNode, unsigned > counter;
- for( unsigned j=0; j<ctype.getNumChildren()-1; j++ ){
- TypeNode t = ctype[j];
- Expr ss = dt.getSharedSelector( domainType, t.toType(), counter[t] );
- d_shared_selectors[domainType].push_back( ss );
- Assert(d_shared_selector_index[domainType].find(ss)
- == d_shared_selector_index[domainType].end());
- d_shared_selector_index[domainType][ss] = j;
- counter[t]++;
- }
- }
-}
-
-
const DatatypeConstructorArg& DatatypeConstructor::operator[](size_t index) const {
PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds");
return d_args[index];
return *i;
}
}
- IllegalArgument(name, "No such arg `%s' of constructor `%s'", name.c_str(), d_name.c_str());
+ 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].getSelector();
+ return (*this)[name].d_selector;
}
Type DatatypeConstructor::getArgType(unsigned index) const
{
PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds");
- return static_cast<SelectorType>((*this)[index].getType()).getRangeType();
+ ExprManagerScope ems(d_constructor);
+ return d_internal->getArgType(index).toType();
}
bool DatatypeConstructor::involvesExternalType() const{
- for(const_iterator i = begin(); i != end(); ++i) {
- if(! SelectorType((*i).getSelector().getType()).getRangeType().isDatatype()) {
- return true;
- }
- }
- return false;
+ ExprManagerScope ems(d_constructor);
+ return d_internal->involvesExternalType();
}
bool DatatypeConstructor::involvesUninterpretedType() const{
- for(const_iterator i = begin(); i != end(); ++i) {
- if(SelectorType((*i).getSelector().getType()).getRangeType().isSort()) {
- return true;
- }
- }
- return false;
+ ExprManagerScope ems(d_constructor);
+ return d_internal->involvesUninterpretedType();
}
DatatypeConstructorArg::DatatypeConstructorArg(std::string name, Expr selector)
- : d_internal(nullptr), // until the Node-level datatype API is activated
- d_name(name),
- d_selector(selector),
- d_resolved(false)
+ : 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_name;
+ string name = d_internal->getName();
const size_t nul = name.find('\0');
if(nul != string::npos) {
name.resize(nul);
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");
- if( options::dtSharedSelectors() ){
- computeSharedSelectors( domainType );
- Assert(d_shared_selectors[domainType].size() == getNumArgs());
- return d_shared_selectors[domainType][index];
- }else{
- return d_args[index].getSelector();
- }
+ 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");
- if( options::dtSharedSelectors() ){
- Assert(sel.getType().isSelector());
- Type domainType = ((SelectorType)sel.getType()).getDomain();
- computeSharedSelectors( domainType );
- std::map< Expr, unsigned >::iterator its = d_shared_selector_index[domainType].find( sel );
- if( its!=d_shared_selector_index[domainType].end() ){
- return (int)its->second;
- }
- }else{
- unsigned sindex = Datatype::indexOf(sel);
- if( getNumArgs() > sindex && d_args[sindex].getSelector() == sel ){
- return (int)sindex;
- }
- }
- return -1;
+ 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");
- return d_constructor;
+ ExprManagerScope ems(d_selector);
+ return d_internal->getConstructor().toExpr();
}
SelectorType DatatypeConstructorArg::getType() const {
- return getSelector().getType();
+ return d_selector.getType();
}
Type DatatypeConstructorArg::getRangeType() const {
bool DatatypeConstructorArg::isUnresolvedSelf() const
{
- return d_selector.isNull() && d_name.size() == d_name.find('\0') + 1;
+ 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)
void DatatypeConstructorArg::toStream(std::ostream& out) const
{
- out << getName() << ": ";
+ std::string name = getName();
+ out << name << ": ";
Type t;
if (isResolved())
}
else if (d_selector.isNull())
{
- string typeName = d_name.substr(d_name.find('\0') + 1);
+ string typeName = name.substr(name.find('\0') + 1);
out << ((typeName == "") ? "[self]" : typeName);
return;
}
return out << "index_" << dic.getIndex();
}
+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; }
+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 */
private:
/** The internal representation */
std::shared_ptr<DTypeSelector> d_internal;
- /** the name of this selector */
- std::string d_name;
- /** the selector expression */
+ /** The selector */
Expr d_selector;
- /** the constructor associated with this selector */
- Expr d_constructor;
- /** whether this class has been resolved */
- bool d_resolved;
/** is this selector unresolved? */
bool isUnresolvedSelf() const;
/** constructor */
/**
* Get the number of arguments (so far) of this Datatype constructor.
*/
- inline size_t getNumArgs() const;
+ size_t getNumArgs() const;
/**
* Get the specialized constructor type for a parametric
* Returns true iff this Datatype constructor has already been
* resolved.
*/
- inline bool isResolved() const;
+ bool isResolved() const;
/** Get the beginning iterator over DatatypeConstructor args. */
- inline iterator begin();
+ iterator begin();
/** Get the ending iterator over DatatypeConstructor args. */
- inline iterator end();
+ iterator end();
/** Get the beginning const_iterator over DatatypeConstructor args. */
- inline const_iterator begin() const;
+ const_iterator begin() const;
/** Get the ending const_iterator over DatatypeConstructor args. */
- inline const_iterator end() const;
+ const_iterator end() const;
/** Get the ith DatatypeConstructor arg. */
const DatatypeConstructorArg& operator[](size_t index) const;
private:
/** The internal representation */
std::shared_ptr<DTypeConstructor> d_internal;
- /** the name of the constructor */
- std::string d_name;
- /** the constructor expression */
+ /** the name of the tester */
+ std::string d_testerName;
+ /** The constructor */
Expr d_constructor;
- /** the tester for this constructor */
- Expr d_tester;
/** the arguments of this constructor */
std::vector<DatatypeConstructorArg> d_args;
- /** sygus operator */
- Expr d_sygus_op;
/** sygus print callback */
std::shared_ptr<SygusPrintCallback> d_sygus_pc;
- /** weight */
- unsigned d_weight;
-
- /** shared selectors for each type
- *
- * This stores the shared (constructor-agnotic)
- * selectors that access the fields of this datatype.
- * In the terminology of "Datatypes with Shared Selectors",
- * this stores:
- * sel_{dtt}^{T1,atos(T1,C,1)}, ...,
- * sel_{dtt}^{Tn,atos(Tn,C,n)}
- * where C is this constructor, which has type
- * T1 x ... x Tn -> dtt above.
- * We store this information for (possibly multiple)
- * datatype types dtt, since this constructor may be
- * for a parametric datatype, where dtt is an instantiated
- * parametric datatype.
- */
- mutable std::map<Type, std::vector<Expr> > d_shared_selectors;
- /** for each type, a cache mapping from shared selectors to
- * its argument index for this constructor.
- */
- mutable std::map<Type, std::map<Expr, unsigned> > d_shared_selector_index;
- /** resolve
- *
- * This resolves (initializes) the constructor. For details
- * on how datatypes and their constructors are resolved, see
- * documentation for Datatype::resolve.
- */
- void resolve(ExprManager* em,
- DatatypeType self,
- 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,
- size_t cindex);
-
- /** Helper function for resolving parametric datatypes.
- *
- * This replaces instances of the SortConstructorType produced for unresolved
- * parametric datatypes, with the corresponding resolved DatatypeType. For
- * example, take the parametric definition of a list,
- * list[T] = cons(car : T, cdr : list[T]) | null.
- * If "range" is the unresolved parametric datatype:
- * DATATYPE list =
- * cons(car: SORT_TAG_1,
- * cdr: SORT_TAG_2(SORT_TAG_1)) | null END;,
- * this function will return the resolved type:
- * DATATYPE list =
- * cons(car: SORT_TAG_1,
- * cdr: (list PARAMETERIC_DATATYPE SORT_TAG_1)) | null END;
- */
- Type doParametricSubstitution(
- Type range,
- const std::vector<SortConstructorType>& paramTypes,
- const std::vector<DatatypeType>& paramReplacements);
-
- /** compute the cardinality of this datatype */
- Cardinality computeCardinality(Type t, std::vector<Type>& processing) const;
- /** compute whether this datatype is well-founded */
- bool computeWellFounded(std::vector<Type>& processing) const;
- /** compute ground term
- *
- * This method is used for constructing a term that is an application
- * of this constructor whose type is t.
- *
- * The argument processing is the set of datatype types we are currently
- * traversing. This is used to avoid infinite loops.
- *
- * The argument gt caches the ground terms we have computed so far.
- *
- * The argument isValue is whether we are constructing a constant value. If
- * this flag is false, we are constructing a canonical ground term that is
- * not necessarily constant.
- */
- Expr computeGroundTerm(Type t,
- std::vector<Type>& processing,
- std::map<Type, Expr>& gt,
- bool isValue) const;
- /** compute shared selectors
- * This computes the maps d_shared_selectors and d_shared_selector_index.
- */
- void computeSharedSelectors(Type domainType) const;
};/* class DatatypeConstructor */
class DType;
*/
class CVC4_PUBLIC Datatype {
friend class DatatypeConstructor;
+ friend class ExprManager; // for access to resolve()
friend class NodeManager; // temporary, for access to d_internal
public:
/**
void setRecord();
/** Get the name of this Datatype. */
- inline std::string getName() const;
+ std::string getName() const;
/** Get the number of constructors (so far) for this Datatype. */
- inline size_t getNumConstructors() const;
+ size_t getNumConstructors() const;
/** Is this datatype parametric? */
- inline bool isParametric() const;
+ bool isParametric() const;
/** Get the nubmer of type parameters */
- inline size_t getNumParameters() const;
+ size_t getNumParameters() const;
/** Get parameter */
- inline Type getParameter( unsigned int i ) const;
+ Type getParameter(unsigned int i) const;
/** Get parameters */
- inline std::vector<Type> getParameters() const;
+ std::vector<Type> getParameters() const;
/** is this a co-datatype? */
- inline bool isCodatatype() const;
+ bool isCodatatype() const;
/** is this a sygus datatype? */
- inline bool isSygus() const;
+ bool isSygus() const;
/** is this a tuple datatype? */
- inline bool isTuple() const;
+ bool isTuple() const;
/** is this a record datatype? */
- inline bool isRecord() const;
+ bool isRecord() const;
/** get the record representation for this datatype */
- inline Record * getRecord() const;
+ Record* getRecord() const;
/**
* Return the cardinality of this datatype.
*/
bool operator==(const Datatype& other) const;
/** Return true iff the two Datatypes are not the same. */
- inline bool operator!=(const Datatype& other) const;
+ bool operator!=(const Datatype& other) const;
/** Return true iff this Datatype has already been resolved. */
- inline bool isResolved() const;
+ bool isResolved() const;
/** Get the beginning iterator over DatatypeConstructors. */
- inline iterator begin();
+ iterator begin();
/** Get the ending iterator over DatatypeConstructors. */
- inline iterator end();
+ iterator end();
/** Get the beginning const_iterator over DatatypeConstructors. */
- inline const_iterator begin() const;
+ const_iterator begin() const;
/** Get the ending const_iterator over DatatypeConstructors. */
- inline const_iterator end() const;
+ const_iterator end() const;
/** Get the ith DatatypeConstructor. */
const DatatypeConstructor& operator[](size_t index) const;
ExprManager* d_em;
/** The internal representation */
std::shared_ptr<DType> d_internal;
- /** name of this datatype */
- std::string d_name;
- /** the type parameters of this datatype (if this is a parametric datatype)
- */
- std::vector<Type> d_params;
- /** whether the datatype is a codatatype. */
- bool d_isCo;
- /** whether the datatype is a tuple */
- bool d_isTuple;
- /** whether the datatype is a record */
- bool d_isRecord;
+ /** self type */
+ Type d_self;
/** the data of the record for this datatype (if applicable) */
Record* d_record;
+ /** whether the datatype is a record */
+ bool d_isRecord;
/** the constructors of this datatype */
std::vector<DatatypeConstructor> d_constructors;
- /** whether this datatype has been resolved */
- bool d_resolved;
- Type d_self;
- /** cache for involves external type */
- bool d_involvesExt;
- /** cache for involves uninterpreted type */
- bool d_involvesUt;
- /** the builtin type that this sygus type encodes */
- Type d_sygus_type;
- /** the variable list for the sygus function to synthesize */
- Expr d_sygus_bvl;
- /** whether all constants are allowed as solutions */
- bool d_sygus_allow_const;
- /** whether all terms are allowed as solutions */
- bool d_sygus_allow_all;
-
- /** the cardinality of this datatype
- * "mutable" because computing the cardinality can be expensive,
- * and so it's computed just once, on demand---this is the cache
- */
- mutable Cardinality d_card;
-
- /** is this type a recursive singleton type?
- * The range of this map stores
- * 0 if the field has not been computed,
- * 1 if this datatype is a recursive singleton type,
- * -1 if this datatype is not a recursive singleton type.
- * For definition of (co)recursive singleton, see
- * Section 2 of Reynolds et al. CADE 2015.
- */
- mutable std::map<Type, int> d_card_rec_singleton;
- /** if d_card_rec_singleton is true,
- * This datatype has infinite cardinality if at least one of the
- * following uninterpreted sorts having cardinality > 1.
- */
- mutable std::map<Type, std::vector<Type> > d_card_u_assume;
- /** cache of whether this datatype is well-founded */
- mutable int d_well_founded;
- /** cache of ground term for this datatype */
- mutable std::map<Type, Expr> d_ground_term;
- /** cache of ground values for this datatype */
- mutable std::map<Type, Expr> d_ground_value;
- /** cache of shared selectors for this datatype */
- mutable std::map<Type, std::map<Type, std::map<unsigned, Expr> > >
- d_shared_sel;
-
/**
* Datatypes refer to themselves, recursively, and we have a
* chicken-and-egg problem. The DatatypeType around the Datatype
* they are two maps). placeholders->replacements give type variables
* that should be resolved in the case of parametric datatypes.
*
- * @param em the ExprManager at play
* @param resolutions a map of strings to DatatypeTypes currently under
* resolution
* @param placeholders the types in these Datatypes under resolution that must
* that must be replaced
* @param paramReplacements the corresponding (parametric) DatatypeTypes
*/
- void resolve(ExprManager* em,
- const std::map<std::string, DatatypeType>& resolutions,
+ 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);
- friend class ExprManager; // for access to resolve()
-
- /** compute the cardinality of this datatype */
- Cardinality computeCardinality(Type t, std::vector<Type>& processing) const;
- /** compute whether this datatype is a recursive singleton */
- bool computeCardinalityRecSingleton(Type t,
- std::vector<Type>& processing,
- std::vector<Type>& u_assume) const;
- /** compute whether this datatype is well-founded */
- bool computeWellFounded(std::vector<Type>& processing) const;
- /** compute ground term
- *
- * This method checks if there is a term of this datatype whose type is t
- * that is finitely constructable. As needed, it traverses its subfield types.
- *
- * The argument processing is the set of datatype types we are currently
- * traversing.
- *
- * The argument isValue is whether we are constructing a constant value. If
- * this flag is false, we are constructing a canonical ground term that is
- * not necessarily constant.
- */
- Expr computeGroundTerm(Type t,
- std::vector<Type>& processing,
- bool isValue) const;
- /** Get the shared selector
- *
- * This returns the index^th (constructor-agnostic)
- * selector for type t. The type dtt is the datatype
- * type whose datatype is this class, where this may
- * be an instantiated parametric datatype.
- *
- * In the terminology of "Datatypes with Shared Selectors",
- * this returns the term sel_{dtt}^{t,index}.
- */
- Expr getSharedSelector(Type dtt, Type t, unsigned index) const;
- /**
- * Helper for mkGroundTerm and mkGroundValue above.
- */
- Expr mkGroundTermInternal(Type t, bool isValue) const;
};/* class Datatype */
/**
inline std::string DatatypeUnresolvedType::getName() const { return d_name; }
-inline std::string Datatype::getName() const { return d_name; }
-inline size_t Datatype::getNumConstructors() const
-{
- return d_constructors.size();
-}
-
-inline bool Datatype::isParametric() const { return d_params.size() > 0; }
-inline size_t Datatype::getNumParameters() const { return d_params.size(); }
-inline Type Datatype::getParameter( unsigned int i ) const {
- CheckArgument(isParametric(), this,
- "Cannot get type parameter of a non-parametric datatype.");
- CheckArgument(i < d_params.size(), i,
- "Type parameter index out of range for datatype.");
- return d_params[i];
-}
-
-inline std::vector<Type> Datatype::getParameters() const {
- CheckArgument(isParametric(), this,
- "Cannot get type parameters of a non-parametric datatype.");
- return d_params;
-}
-
-inline bool Datatype::isCodatatype() const {
- return d_isCo;
-}
-
-inline bool Datatype::isSygus() const {
- return !d_sygus_type.isNull();
-}
-
-inline bool Datatype::isTuple() const {
- return d_isTuple;
-}
-
-inline bool Datatype::isRecord() const {
- return d_isRecord;
-}
-
-inline Record * Datatype::getRecord() const {
- return d_record;
-}
-inline bool Datatype::operator!=(const Datatype& other) const
-{
- return !(*this == other);
-}
-
-inline bool Datatype::isResolved() const { return d_resolved; }
-inline Datatype::iterator Datatype::begin()
-{
- return iterator(d_constructors, true);
-}
-
-inline Datatype::iterator Datatype::end()
-{
- return iterator(d_constructors, false);
-}
-
-inline Datatype::const_iterator Datatype::begin() const
-{
- return const_iterator(d_constructors, true);
-}
-
-inline Datatype::const_iterator Datatype::end() const
-{
- return const_iterator(d_constructors, false);
-}
-
-inline bool DatatypeConstructor::isResolved() const
-{
- return !d_tester.isNull();
-}
-
-inline size_t DatatypeConstructor::getNumArgs() const { return d_args.size(); }
-inline 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_resolved;
-}
-
-inline DatatypeConstructor::iterator DatatypeConstructor::begin()
-{
- return iterator(d_args, true);
-}
-
-inline DatatypeConstructor::iterator DatatypeConstructor::end()
-{
- return iterator(d_args, false);
-}
-
-inline DatatypeConstructor::const_iterator DatatypeConstructor::begin() const
-{
- return const_iterator(d_args, true);
-}
-
-inline DatatypeConstructor::const_iterator DatatypeConstructor::end() const
-{
- return const_iterator(d_args, false);
-}
}/* CVC4 namespace */
projects / cvc5.git / commitdiff