<< std::endl;
return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]);
} else {
+ TNode gt = in.getType().mkGroundTerm();
+ TypeNode gtt = gt.getType();
+ Assert( gtt.isDatatype() || gtt.isParametricDatatype() );
+ if( !gtt.isInstantiatedDatatype() ){
+ gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
+ NodeManager::currentNM()->mkConst(AscriptionType(in.getType().toType())), gt);
+ }
Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
<< "Rewrite trivial selector " << in
<< " to distinguished ground term "
<< in.getType().mkGroundTerm() << std::endl;
- return RewriteResponse(REWRITE_DONE,in.getType().mkGroundTerm() );
+ return RewriteResponse(REWRITE_DONE,gt );
}
}
"util/datatype.h"
well-founded DATATYPE_TYPE \
"%TYPE%.getConst<Datatype>().isWellFounded()" \
- "%TYPE%.getConst<Datatype>().mkGroundTerm()" \
+ "%TYPE%.getConst<Datatype>().mkGroundTerm(%TYPE%.toType())" \
"util/datatype.h"
operator PARAMETRIC_DATATYPE 1: "parametric datatype"
"util/datatype.h"
well-founded PARAMETRIC_DATATYPE\
"DatatypeType(%TYPE%.toType()).getDatatype().isWellFounded()" \
- "DatatypeType(%TYPE%.toType()).getDatatype().mkGroundTerm()" \
+ "DatatypeType(%TYPE%.toType()).getDatatype().mkGroundTerm(%TYPE%.toType())" \
"util/datatype.h"
parameterized APPLY_TYPE_ASCRIPTION ASCRIPTION_TYPE 1 \
d_inst_map[ te ] = true;
//instantiate, add equality
Node val = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, selectorVals );
+ val = doTypeAscription( val, te.getType() ); //IDT-param
if( find( val ) != find( te ) ) {
//build explaination
NodeBuilder<> nb(kind::AND);
bool TheoryDatatypes::collapseSelector( Node t ) {
if( !hasConflict() && t.getKind() == APPLY_SELECTOR ) {
//collapse constructor
+ TypeNode retTyp = t.getType();
TypeNode typ = t[0].getType();
Node sel = t.getOperator();
TypeNode selType = sel.getType();
retNode = tmp[ Datatype::indexOf( sel.toExpr() ) ];
} else {
Debug("datatypes") << "Applied selector " << t << " to wrong constructor." << endl;
- retNode = selType[1].mkGroundTerm();
+ retNode = doTypeAscription( retTyp.mkGroundTerm(), selType[1] ); //IDT-param
+ //retNode = selType[1].mkGroundTerm();
}
if( tmp!=t[0] ){
t = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, t.getOperator(), tmp );
unsigned r;
checkTester( tester, conflict, r );
if( !conflict.isNull() ) {
- Debug("datatypes") << "Applied selector " << t << " to provably wrong constructor." << endl;
+ Debug("datatypes") << "Applied selector " << t << " to provably wrong constructor. " << retTyp << endl;
//conflict is c ^ tester, where conflict => false, but we want to say c => ~tester
//must remove tester from conflict
if( conflict.getKind()==kind::AND ){
tester = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( cn.getTester() ), t[0] );
d_em.addNode( tester.notNode(), exp, Reason::idt_tcong );
}
- retNode = selType[1].mkGroundTerm();
+ retNode = doTypeAscription( retTyp.mkGroundTerm(), retTyp ); //IDT-param
+ //retNode = selType[1].mkGroundTerm();
Node neq = NodeManager::currentNM()->mkNode( EQUAL, retNode, t );
d_em.addNode( neq, tester.notNode(), Reason::idt_collapse2 );
}
return false;
}
+
+Node TheoryDatatypes::doTypeAscription( Node t, TypeNode typ )
+{
+ TypeNode tt = t.getType();
+ if( (tt.isDatatype() || tt.isParametricDatatype()) && !tt.isInstantiatedDatatype() ){
+ return NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
+ NodeManager::currentNM()->mkConst(AscriptionType(typ.toType())), t);
+ }else{
+ return t;
+ }
+}
bool searchForCycle( Node n, Node on,
std::map< Node, bool >& visited,
NodeBuilder<>& explanation );
+ Node doTypeAscription( Node t, TypeNode typ );
};/* class TheoryDatatypes */
inline bool TheoryDatatypes::hasConflict() {
i != i_end;
++i) {
if(TypeNode::fromType((*i).getConstructor().getType()) == type) {
- groundTerm = Node::fromExpr((*i).mkGroundTerm());
+ groundTerm = Node::fromExpr((*i).mkGroundTerm( type.toType() ));
type.setAttribute(GroundTermAttr(), groundTerm);
return groundTerm;
}
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
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) {
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);
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);
* 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
/** 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
* 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
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);
}
++i) {
TS_ASSERT((*i).isWellFounded());
Debug("groundterms") << "ground term of " << *i << endl
- << " is " << (*i).mkGroundTerm() << endl;
- TS_ASSERT((*i).mkGroundTerm().getType() == colorsType);
+ << " is " << (*i).mkGroundTerm( colorsType ) << endl;
+ TS_ASSERT((*i).mkGroundTerm( colorsType ).getType() == colorsType);
}
}
Debug("datatypes") << "checking " << (*i).getName() << endl;
TS_ASSERT((*i).isWellFounded());
Debug("groundterms") << "ground term of " << *i << endl
- << " is " << (*i).mkGroundTerm() << endl;
- TS_ASSERT((*i).mkGroundTerm().getType() == natType);
+ << " is " << (*i).mkGroundTerm( natType ) << endl;
+ TS_ASSERT((*i).mkGroundTerm( natType ).getType() == natType);
}
}
++i) {
TS_ASSERT((*i).isWellFounded());
Debug("groundterms") << "ground term of " << *i << endl
- << " is " << (*i).mkGroundTerm() << endl;
- TS_ASSERT((*i).mkGroundTerm().getType() == treeType);
+ << " is " << (*i).mkGroundTerm( treeType ) << endl;
+ TS_ASSERT((*i).mkGroundTerm( treeType ).getType() == treeType);
}
}
++i) {
TS_ASSERT((*i).isWellFounded());
Debug("groundterms") << "ground term of " << *i << endl
- << " is " << (*i).mkGroundTerm() << endl;
- TS_ASSERT((*i).mkGroundTerm().getType() == listType);
+ << " is " << (*i).mkGroundTerm( listType ) << endl;
+ TS_ASSERT((*i).mkGroundTerm( listType ).getType() == listType);
}
}
++i) {
TS_ASSERT((*i).isWellFounded());
Debug("groundterms") << "ground term of " << *i << endl
- << " is " << (*i).mkGroundTerm() << endl;
- TS_ASSERT((*i).mkGroundTerm().getType() == listType);
+ << " is " << (*i).mkGroundTerm( listType ) << endl;
+ TS_ASSERT((*i).mkGroundTerm( listType ).getType() == listType);
}
}
++i) {
TS_ASSERT((*i).isWellFounded());
Debug("groundterms") << "ground term of " << *i << endl
- << " is " << (*i).mkGroundTerm() << endl;
- TS_ASSERT((*i).mkGroundTerm().getType() == listType);
+ << " is " << (*i).mkGroundTerm( listType ) << endl;
+ TS_ASSERT((*i).mkGroundTerm( listType ).getType() == listType);
}
}
++i) {
TS_ASSERT((*i).isWellFounded());
Debug("groundterms") << "ground term of " << *i << endl
- << " is " << (*i).mkGroundTerm() << endl;
- TS_ASSERT((*i).mkGroundTerm().getType() == dtts[0]);
+ << " is " << (*i).mkGroundTerm( dtts[0] ) << endl;
+ TS_ASSERT((*i).mkGroundTerm( dtts[0] ).getType() == dtts[0]);
}
TS_ASSERT(! dtts[1].getDatatype().isFinite());
++i) {
TS_ASSERT((*i).isWellFounded());
Debug("groundterms") << "ground term of " << *i << endl
- << " is " << (*i).mkGroundTerm() << endl;
- TS_ASSERT((*i).mkGroundTerm().getType() == dtts[1]);
+ << " is " << (*i).mkGroundTerm( dtts[1] ) << endl;
+ TS_ASSERT((*i).mkGroundTerm( dtts[1] ).getType() == dtts[1]);
}
// add another constructor to list datatype resulting in an
++i) {
TS_ASSERT((*i).isWellFounded());
Debug("groundterms") << "ground term of " << *i << endl
- << " is " << (*i).mkGroundTerm() << endl;
- TS_ASSERT((*i).mkGroundTerm().getType() == dtts2[0]);
+ << " is " << (*i).mkGroundTerm( dtts2[0] ) << endl;
+ TS_ASSERT((*i).mkGroundTerm( dtts2[0] ).getType() == dtts2[0]);
}
TS_ASSERT(! dtts2[1].getDatatype().isFinite());
++i) {
TS_ASSERT((*i).isWellFounded());
Debug("groundterms") << "ground term of " << *i << endl
- << " is " << (*i).mkGroundTerm() << endl;
- TS_ASSERT((*i).mkGroundTerm().getType() == dtts2[1]);
+ << " is " << (*i).mkGroundTerm( dtts2[1] ) << endl;
+ TS_ASSERT((*i).mkGroundTerm( dtts2[1] ).getType() == dtts2[1]);
}
}
TS_ASSERT(treeType.getDatatype().getCardinality() == Cardinality::INTEGERS);
TS_ASSERT(! treeType.getDatatype().isWellFounded());
TS_ASSERT_THROWS_ANYTHING( treeType.mkGroundTerm() );
- TS_ASSERT_THROWS_ANYTHING( treeType.getDatatype().mkGroundTerm() );
+ TS_ASSERT_THROWS_ANYTHING( treeType.getDatatype().mkGroundTerm( treeType ) );
// all ctors should be not-well-founded either
for(Datatype::const_iterator i = treeType.getDatatype().begin(),
i_end = treeType.getDatatype().end();
i != i_end;
++i) {
TS_ASSERT(! (*i).isWellFounded());
- TS_ASSERT_THROWS_ANYTHING( (*i).mkGroundTerm() );
+ TS_ASSERT_THROWS_ANYTHING( (*i).mkGroundTerm( treeType ) );
}
}
projects / cvc5.git / commitdiff