From: Andrew Reynolds Date: Thu, 12 Dec 2019 00:09:16 +0000 (-0600) Subject: Activate node-level datatype API (#3540) X-Git-Tag: cvc5-1.0.0~3774 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d803e7f;p=cvc5.git Activate node-level datatype API (#3540) --- diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 07af9617d..14b21a96a 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -37,42 +37,23 @@ using namespace std; 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 DatatypeIndexAttr; -typedef expr::Attribute DatatypeConsIndexAttr; -typedef expr::Attribute DatatypeFiniteAttr; -typedef expr::Attribute DatatypeFiniteComputedAttr; -typedef expr::Attribute DatatypeUFiniteAttr; -typedef expr::Attribute 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(name, isCo); } Datatype::Datatype(ExprManager* em, @@ -80,26 +61,18 @@ Datatype::Datatype(ExprManager* em, const std::vector& 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 paramsn; + for (const Type& t : params) + { + paramsn.push_back(TypeNode::fromType(t)); + } + d_internal = std::make_shared(name, paramsn, isCo); } const Datatype& Datatype::datatypeOf(Expr item) { @@ -132,8 +105,8 @@ size_t Datatype::indexOfInternal(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()); } } @@ -150,46 +123,82 @@ size_t Datatype::cindexOfInternal(Expr item) 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& resolutions, +void Datatype::resolve(const std::map& resolutions, const std::vector& placeholders, const std::vector& replacements, - const std::vector< SortConstructorType >& paramTypes, - const std::vector< DatatypeType >& paramReplacements) + const std::vector& paramTypes, + const std::vector& 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::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 resolutionsn; + std::vector placeholdersn; + std::vector replacementsn; + std::vector paramTypesn; + std::vector paramReplacementsn; + for (const std::pair& r : resolutions) + { + resolutionsn[r.first] = TypeNode::fromType(r.second); + } + for (const Type& t : placeholders) + { + placeholdersn.push_back(TypeNode::fromType(t)); + } + for (const Type& t : replacements) + { + replacementsn.push_back(TypeNode::fromType(t)); + } + for (const Type& t : paramTypes) + { + paramTypesn.push_back(TypeNode::fromType(t)); + } + for (const Type& t : paramReplacements) + { + paramReplacementsn.push_back(TypeNode::fromType(t)); + } + bool res = d_internal->resolve(resolutionsn, + placeholdersn, + replacementsn, + paramTypesn, + paramReplacementsn); + if (!res) + { + IllegalArgument(*this, + "could not resolve datatype that is not well formed"); + } + Trace("dt-debug") << "Datatype::resolve: finished " << getName() << " " + << d_constructors.size() << std::endl; + AlwaysAssert(isResolved()); + // + d_self = d_internal->getTypeNode().toType(); + for (DatatypeConstructor& c : d_constructors) + { + AlwaysAssert(c.isResolved()); + c.d_constructor = c.d_internal->getConstructor().toExpr(); + for (size_t i = 0, nargs = c.getNumArgs(); i < nargs; i++) + { + AlwaysAssert(c.d_args[i].isResolved()); + c.d_args[i].d_selector = c.d_args[i].d_internal->getSelector().toExpr(); } } @@ -200,52 +209,24 @@ void Datatype::resolve(ExprManager* em, } 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 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 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, @@ -254,8 +235,6 @@ void Datatype::addSygusConstructor(Expr op, std::shared_ptr 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; @@ -275,12 +254,14 @@ void Datatype::addSygusConstructor(Expr op, } 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; } @@ -288,347 +269,143 @@ Cardinality Datatype::getCardinality(Type t) const { 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& 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; iisRecursiveSingleton(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& processing, - std::vector& 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; igetRecursiveSingletonArgType(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& 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& cache = isValue ? d_ground_value : d_ground_term; - std::map::iterator it = cache.find(t); - if (it != cache.end()) - { - Debug("datatypes") << "\nin cache: " << d_self << " => " << it->second << std::endl; - return it->second; - } - std::vector 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& 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& 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 @@ -639,70 +416,6 @@ 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; } @@ -717,31 +430,11 @@ const DatatypeConstructor& Datatype::operator[](std::string name) const { 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 { @@ -749,27 +442,27 @@ 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* Datatype::getConstructors() const @@ -777,136 +470,22 @@ const std::vector* Datatype::getConstructors() const return &d_constructors; } -void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self, - const std::map& resolutions, - const std::vector& placeholders, - const std::vector& 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::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::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::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(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(name, weight); } void DatatypeConstructor::setSygus(Expr op, @@ -914,7 +493,9 @@ 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; } @@ -938,6 +519,7 @@ void DatatypeConstructor::addArg(std::string selectorName, Type 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) { @@ -948,6 +530,7 @@ void DatatypeConstructor::addArg(std::string selectorName, DatatypeUnresolvedTyp 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) { @@ -958,16 +541,18 @@ 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 { @@ -979,44 +564,34 @@ 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); - 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 sns; - m.getMatches(sns); - std::vector subst; - for (TypeNode& s : sns) - { - subst.push_back(s.toType()); - } - vector 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 DatatypeConstructor::getSygusPrintCallback() const @@ -1029,214 +604,27 @@ std::shared_ptr DatatypeConstructor::getSygusPrintCallback() 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& 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& 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& processing, - std::map& gt, - bool isValue) const -{ - // we're using some internals, so we have to set up this library context - ExprManagerScope ems(d_constructor); - - std::vector groundTerms; - groundTerms.push_back(getConstructor()); - - // for each selector, get a ground term - std::vector< Type > instTypes; - std::vector< Type > paramTypes; - bool isParam = static_cast(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() counter; - for( unsigned j=0; j((*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(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); @@ -1306,42 +689,27 @@ Expr DatatypeConstructorArg::getSelector() const { 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 { @@ -1350,7 +718,25 @@ 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) @@ -1423,7 +809,8 @@ std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) { void DatatypeConstructorArg::toStream(std::ostream& out) const { - out << getName() << ": "; + std::string name = getName(); + out << name << ": "; Type t; if (isResolved()) @@ -1432,7 +819,7 @@ void DatatypeConstructorArg::toStream(std::ostream& out) const } 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; } @@ -1448,4 +835,119 @@ std::ostream& operator<<(std::ostream& out, const DatatypeIndexConstant& dic) { 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 Datatype::getParameters() const +{ + CheckArgument(isParametric(), + this, + "Cannot get type parameters of a non-parametric datatype."); + std::vector params; + std::vector paramsn = d_internal->getParameters(); + // convert to type + for (unsigned i = 0, nparams = paramsn.size(); i < nparams; i++) + { + params.push_back(paramsn[i].toType()); + } + return params; +} + +bool Datatype::isCodatatype() const +{ + ExprManagerScope ems(*d_em); + return d_internal->isCodatatype(); +} + +bool Datatype::isSygus() const +{ + ExprManagerScope ems(*d_em); + return d_internal->isSygus(); +} + +bool Datatype::isTuple() const +{ + ExprManagerScope ems(*d_em); + return d_internal->isTuple(); +} + +bool Datatype::isRecord() const { return d_isRecord; } + +Record* Datatype::getRecord() const { return d_record; } +bool Datatype::operator!=(const Datatype& other) const +{ + return !(*this == other); +} + +bool Datatype::isResolved() const +{ + ExprManagerScope ems(*d_em); + return d_internal->isResolved(); +} +Datatype::iterator Datatype::begin() { return iterator(d_constructors, true); } + +Datatype::iterator Datatype::end() { return iterator(d_constructors, false); } + +Datatype::const_iterator Datatype::begin() const +{ + return const_iterator(d_constructors, true); +} + +Datatype::const_iterator Datatype::end() const +{ + return const_iterator(d_constructors, false); +} + +bool DatatypeConstructor::isResolved() const +{ + return d_internal->isResolved(); +} + +size_t DatatypeConstructor::getNumArgs() const { return d_args.size(); } + +DatatypeConstructor::iterator DatatypeConstructor::begin() +{ + return iterator(d_args, true); +} + +DatatypeConstructor::iterator DatatypeConstructor::end() +{ + return iterator(d_args, false); +} + +DatatypeConstructor::const_iterator DatatypeConstructor::begin() const +{ + return const_iterator(d_args, true); +} + +DatatypeConstructor::const_iterator DatatypeConstructor::end() const +{ + return const_iterator(d_args, false); +} }/* CVC4 namespace */ diff --git a/src/expr/datatype.h b/src/expr/datatype.h index c9191aadf..dccda5ad4 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -163,14 +163,8 @@ class CVC4_PUBLIC DatatypeConstructorArg { private: /** The internal representation */ std::shared_ptr 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 */ @@ -323,7 +317,7 @@ class CVC4_PUBLIC DatatypeConstructor { /** * 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 @@ -363,16 +357,16 @@ class CVC4_PUBLIC DatatypeConstructor { * 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; @@ -462,102 +456,14 @@ class CVC4_PUBLIC DatatypeConstructor { private: /** The internal representation */ std::shared_ptr 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 d_args; - /** sygus operator */ - Expr d_sygus_op; /** sygus print callback */ std::shared_ptr 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 > d_shared_selectors; - /** for each type, a cache mapping from shared selectors to - * its argument index for this constructor. - */ - mutable std::map > 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& resolutions, - const std::vector& placeholders, - const std::vector& replacements, - const std::vector& paramTypes, - const std::vector& 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& paramTypes, - const std::vector& paramReplacements); - - /** compute the cardinality of this datatype */ - Cardinality computeCardinality(Type t, std::vector& processing) const; - /** compute whether this datatype is well-founded */ - bool computeWellFounded(std::vector& 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& processing, - std::map& 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; @@ -623,6 +529,7 @@ 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: /** @@ -731,37 +638,37 @@ class CVC4_PUBLIC Datatype { 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 getParameters() const; + std::vector 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. @@ -887,19 +794,19 @@ class CVC4_PUBLIC 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; @@ -981,67 +888,14 @@ class CVC4_PUBLIC Datatype { ExprManager* d_em; /** The internal representation */ std::shared_ptr d_internal; - /** name of this datatype */ - std::string d_name; - /** the type parameters of this datatype (if this is a parametric datatype) - */ - std::vector 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 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 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 > 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 d_ground_term; - /** cache of ground values for this datatype */ - mutable std::map d_ground_value; - /** cache of shared selectors for this datatype */ - mutable std::map > > - d_shared_sel; - /** * Datatypes refer to themselves, recursively, and we have a * chicken-and-egg problem. The DatatypeType around the Datatype @@ -1061,7 +915,6 @@ class CVC4_PUBLIC 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 @@ -1071,52 +924,11 @@ class CVC4_PUBLIC Datatype { * that must be replaced * @param paramReplacements the corresponding (parametric) DatatypeTypes */ - void resolve(ExprManager* em, - const std::map& resolutions, + void resolve(const std::map& resolutions, const std::vector& placeholders, const std::vector& replacements, const std::vector& paramTypes, const std::vector& paramReplacements); - friend class ExprManager; // for access to resolve() - - /** compute the cardinality of this datatype */ - Cardinality computeCardinality(Type t, std::vector& processing) const; - /** compute whether this datatype is a recursive singleton */ - bool computeCardinalityRecSingleton(Type t, - std::vector& processing, - std::vector& u_assume) const; - /** compute whether this datatype is well-founded */ - bool computeWellFounded(std::vector& 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& 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 */ /** @@ -1202,116 +1014,6 @@ inline DatatypeUnresolvedType::DatatypeUnresolvedType(std::string name) : 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 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 */ diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 09555da1b..411d64a1b 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -766,9 +766,11 @@ std::vector ExprManager::mkMutualDatatypeTypes( ++i) { const Datatype& dt = (*i).getDatatype(); if(!dt.isResolved()) { - const_cast(dt).resolve(this, nameResolutions, - placeholders, replacements, - paramTypes, paramReplacements); + const_cast(dt).resolve(nameResolutions, + placeholders, + replacements, + paramTypes, + paramReplacements); } // Now run some checks, including a check to make sure that no diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 1142da429..0c3f1b4cb 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -262,12 +262,8 @@ const Datatype & NodeManager::getDatatypeForIndex( unsigned index ) const{ const DType& NodeManager::getDTypeForIndex(unsigned index) const { - // when the Node-level API is in place, this function will be replaced by a - // direct lookup into a d_ownedDTypes vector, similar to d_ownedDatatypes - // above. - Unreachable() << "NodeManager::getDTypeForIndex: DType is not available in " - "the current implementation."; const Datatype& d = getDatatypeForIndex(index); + // return its internal representation return *d.d_internal; }