summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2011-06-02 15:23:16 +0000
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2011-06-02 15:23:16 +0000
commit256bb47bb56e3ae1913035503769a76435f79e2a (patch)
tree04fcaa239380a5f68cfa9708ecee6ca26fb4019b /src/util
parentc6a8319b05cf1b156691132b3bec1f56ca6588e0 (diff)
added (temporary) support for ensuring that all ambiguously typed constructor nodes created internally are given a type ascription
Diffstat (limited to 'src/util')
-rw-r--r--src/util/datatype.cpp140
-rw-r--r--src/util/datatype.h11
2 files changed, 87 insertions, 64 deletions
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 31b68c9a4..4b84d2955 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -182,7 +182,7 @@ bool Datatype::isWellFounded() const throw(AssertionException) {
return false;
}
-Expr Datatype::mkGroundTerm() const throw(AssertionException) {
+Expr Datatype::mkGroundTerm( Type t ) const throw(AssertionException) {
CheckArgument(isResolved(), this, "this datatype is not yet resolved");
// we're using some internals, so we have to set up this library context
@@ -194,73 +194,78 @@ Expr Datatype::mkGroundTerm() const throw(AssertionException) {
Expr groundTerm = self.getAttribute(DatatypeGroundTermAttr()).toExpr();
if(!groundTerm.isNull()) {
Debug("datatypes") << "\nin cache: " << d_self << " => " << groundTerm << std::endl;
- return groundTerm;
} else {
Debug("datatypes") << "\nNOT in cache: " << d_self << std::endl;
- }
-
- // look for a nullary ctor and use that
- for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
- // prefer the nullary constructor
- if((*i).getNumArgs() == 0) {
- groundTerm = (*i).getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, (*i).getConstructor());
- self.setAttribute(DatatypeGroundTermAttr(), groundTerm);
- Debug("datatypes") << "constructed nullary: " << getName() << " => " << groundTerm << std::endl;
- return groundTerm;
- }
- }
-
- // No ctors are nullary, but we can't just use the first ctor
- // because that might recurse! In fact, since this datatype is
- // well-founded by assumption, we know that at least one constructor
- // doesn't contain a self-reference. We search for that one and use
- // it to construct the ground term, as that is often a simpler
- // ground term (e.g. in a tree datatype, something like "(leaf 0)"
- // is simpler than "(node (leaf 0) (leaf 0))".
- //
- // Of course this check doesn't always work, if the self-reference
- // is through other Datatypes (or other non-Datatype types), but it
- // does simplify a common case. It requires a bit of extra work,
- // but since we cache the results of these, it only happens once,
- // ever, per Datatype.
- //
- // If the datatype is not actually well-founded, something below
- // will throw an exception.
- for(const_iterator i = begin(), i_end = end();
- i != i_end;
- ++i) {
- Constructor::const_iterator j = (*i).begin(), j_end = (*i).end();
- for(; j != j_end; ++j) {
- SelectorType stype((*j).getSelector().getType());
- if(stype.getDomain() == stype.getRangeType()) {
- Debug("datatypes") << "self-reference, skip " << getName() << "::" << (*i).getName() << std::endl;
- // the constructor contains a direct self-reference
- break;
+ // look for a nullary ctor and use that
+ for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
+ // prefer the nullary constructor
+ if( groundTerm.isNull() && (*i).getNumArgs() == 0) {
+ groundTerm = (*i).getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, (*i).getConstructor());
+ self.setAttribute(DatatypeGroundTermAttr(), groundTerm);
+ Debug("datatypes-gt") << "constructed nullary: " << getName() << " => " << groundTerm << std::endl;
}
}
+ // No ctors are nullary, but we can't just use the first ctor
+ // because that might recurse! In fact, since this datatype is
+ // well-founded by assumption, we know that at least one constructor
+ // doesn't contain a self-reference. We search for that one and use
+ // it to construct the ground term, as that is often a simpler
+ // ground term (e.g. in a tree datatype, something like "(leaf 0)"
+ // is simpler than "(node (leaf 0) (leaf 0))".
+ //
+ // Of course this check doesn't always work, if the self-reference
+ // is through other Datatypes (or other non-Datatype types), but it
+ // does simplify a common case. It requires a bit of extra work,
+ // but since we cache the results of these, it only happens once,
+ // ever, per Datatype.
+ //
+ // If the datatype is not actually well-founded, something below
+ // will throw an exception.
+ for(const_iterator i = begin(), i_end = end();
+ i != i_end;
+ ++i) {
+ if( groundTerm.isNull() ){
+ Constructor::const_iterator j = (*i).begin(), j_end = (*i).end();
+ for(; j != j_end; ++j) {
+ SelectorType stype((*j).getSelector().getType());
+ if(stype.getDomain() == stype.getRangeType()) {
+ Debug("datatypes") << "self-reference, skip " << getName() << "::" << (*i).getName() << std::endl;
+ // the constructor contains a direct self-reference
+ break;
+ }
+ }
- if(j == j_end && (*i).isWellFounded()) {
- groundTerm = (*i).mkGroundTerm();
- // Constructor::mkGroundTerm() doesn't ever return null when
- // called from the outside. But in recursive invocations, it
- // can: say you have dt = a(one:dt) | b(two:INT), and you ask
- // the "a" constructor for a ground term. It asks "dt" for a
- // ground term, which in turn asks the "a" constructor for a
- // ground term! Thus, even though "a" is a well-founded
- // constructor, it cannot construct a ground-term by itself. We
- // have to skip past it, and we do that with a
- // RecursionBreaker<> in Constructor::mkGroundTerm(). In the
- // case of recursion, it returns null.
- if(!groundTerm.isNull()) {
- // we found a ground-term-constructing constructor!
- self.setAttribute(DatatypeGroundTermAttr(), groundTerm);
- Debug("datatypes") << "constructed: " << getName() << " => " << groundTerm << std::endl;
- return groundTerm;
+ if(j == j_end && (*i).isWellFounded()) {
+ groundTerm = (*i).mkGroundTerm( t );
+ // Constructor::mkGroundTerm() doesn't ever return null when
+ // called from the outside. But in recursive invocations, it
+ // can: say you have dt = a(one:dt) | b(two:INT), and you ask
+ // the "a" constructor for a ground term. It asks "dt" for a
+ // ground term, which in turn asks the "a" constructor for a
+ // ground term! Thus, even though "a" is a well-founded
+ // constructor, it cannot construct a ground-term by itself. We
+ // have to skip past it, and we do that with a
+ // RecursionBreaker<> in Constructor::mkGroundTerm(). In the
+ // case of recursion, it returns null.
+ if(!groundTerm.isNull()) {
+ // we found a ground-term-constructing constructor!
+ self.setAttribute(DatatypeGroundTermAttr(), groundTerm);
+ Debug("datatypes") << "constructed: " << getName() << " => " << groundTerm << std::endl;
+ }
+ }
}
}
}
- // if we get all the way here, we aren't well-founded
- CheckArgument(false, *this, "this datatype is not well-founded, cannot construct a ground term!");
+ if( groundTerm.isNull() ){
+ // if we get all the way here, we aren't well-founded
+ CheckArgument(false, *this, "this datatype is not well-founded, cannot construct a ground term!");
+ }else{
+ if( t!=groundTerm.getType() ){
+ groundTerm = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
+ NodeManager::currentNM()->mkConst(AscriptionType(t)), groundTerm).toExpr();
+ }
+ return groundTerm;
+ }
}
DatatypeType Datatype::getDatatypeType() const throw(AssertionException) {
@@ -593,9 +598,10 @@ bool Datatype::Constructor::isWellFounded() const throw(AssertionException) {
return true;
}
-Expr Datatype::Constructor::mkGroundTerm() const throw(AssertionException) {
+Expr Datatype::Constructor::mkGroundTerm( Type t ) const throw(AssertionException) {
CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+ Debug("datatypes-gt") << "mkGroundTerm " << t << std::endl;
// we're using some internals, so we have to set up this library context
ExprManagerScope ems(d_constructor);
@@ -618,8 +624,18 @@ Expr Datatype::Constructor::mkGroundTerm() const throw(AssertionException) {
groundTerms.push_back(getConstructor());
// for each selector, get a ground term
+ Assert( t.isDatatype() );
+ std::vector< Type > instTypes;
+ std::vector< Type > paramTypes = DatatypeType(t).getDatatype().getParameters();
+ if( DatatypeType(t).isParametric() ){
+ instTypes = DatatypeType(t).getParamTypes();
+ }
for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
- groundTerms.push_back(SelectorType((*i).getSelector().getType()).getRangeType().mkGroundTerm());
+ Type selType = SelectorType((*i).getSelector().getType()).getRangeType();
+ if( DatatypeType(t).isParametric() ){
+ selType = selType.substitute( paramTypes, instTypes );
+ }
+ groundTerms.push_back(selType.mkGroundTerm());
}
groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms);
diff --git a/src/util/datatype.h b/src/util/datatype.h
index 90dd8775f..3506616d6 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -297,7 +297,7 @@ public:
* constructor must be both resolved and well-founded, or else an
* exception is thrown.
*/
- Expr mkGroundTerm() const throw(AssertionException);
+ Expr mkGroundTerm( Type t ) const throw(AssertionException);
/**
* Returns true iff this Datatype constructor has already been
@@ -375,6 +375,9 @@ public:
/** Get parameter */
inline Type getParameter( unsigned int i ) const;
+ /** Get parameters */
+ inline std::vector<Type> getParameters() const;
+
/**
* Return the cardinality of this datatype (the sum of the
* cardinalities of its constructors). The Datatype must be
@@ -401,7 +404,7 @@ public:
* Datatype must be both resolved and well-founded, or else an
* exception is thrown.
*/
- Expr mkGroundTerm() const throw(AssertionException);
+ Expr mkGroundTerm( Type t ) const throw(AssertionException);
/**
* Get the DatatypeType associated to this Datatype. Can only be
@@ -532,6 +535,10 @@ inline Type Datatype::getParameter( unsigned int i ) const {
return d_params[i];
}
+inline std::vector<Type> Datatype::getParameters() const {
+ return d_params;
+}
+
inline bool Datatype::operator!=(const Datatype& other) const throw() {
return !(*this == other);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback