From 256bb47bb56e3ae1913035503769a76435f79e2a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 2 Jun 2011 15:23:16 +0000 Subject: [PATCH] added (temporary) support for ensuring that all ambiguously typed constructor nodes created internally are given a type ascription --- src/theory/datatypes/datatypes_rewriter.h | 9 +- src/theory/datatypes/kinds | 4 +- src/theory/datatypes/theory_datatypes.cpp | 21 ++- src/theory/datatypes/theory_datatypes.h | 1 + .../datatypes/theory_datatypes_type_rules.h | 2 +- src/util/datatype.cpp | 140 ++++++++++-------- src/util/datatype.h | 11 +- test/unit/util/datatype_black.h | 44 +++--- 8 files changed, 139 insertions(+), 93 deletions(-) diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index b493b8c41..b4ff7e135 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -75,11 +75,18 @@ public: << 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 ); } } diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index a11990075..1cdefa60b 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -50,7 +50,7 @@ cardinality DATATYPE_TYPE \ "util/datatype.h" well-founded DATATYPE_TYPE \ "%TYPE%.getConst().isWellFounded()" \ - "%TYPE%.getConst().mkGroundTerm()" \ + "%TYPE%.getConst().mkGroundTerm(%TYPE%.toType())" \ "util/datatype.h" operator PARAMETRIC_DATATYPE 1: "parametric datatype" @@ -59,7 +59,7 @@ cardinality 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 \ diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 2f0b82f7c..20668a5ff 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -474,6 +474,7 @@ bool TheoryDatatypes::checkInstantiate( Node te, Node cons ) 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); @@ -518,6 +519,7 @@ bool TheoryDatatypes::checkInstantiate( Node te, Node cons ) 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(); @@ -531,7 +533,8 @@ bool TheoryDatatypes::collapseSelector( Node t ) { 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 ); @@ -548,7 +551,7 @@ bool TheoryDatatypes::collapseSelector( Node t ) { 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 ){ @@ -574,7 +577,8 @@ bool TheoryDatatypes::collapseSelector( Node t ) { 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 ); @@ -1044,3 +1048,14 @@ bool TheoryDatatypes::searchForCycle( Node n, Node on, } 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; + } +} diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 1b9e357ed..9dfb8c818 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -178,6 +178,7 @@ private: 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() { diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index c9c76a15b..270313e0f 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -304,7 +304,7 @@ struct ConstructorProperties { 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; } 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 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 Datatype::getParameters() const { + return d_params; +} + inline bool Datatype::operator!=(const Datatype& other) const throw() { return !(*this == other); } diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h index 1ac4caaec..485820a61 100644 --- a/test/unit/util/datatype_black.h +++ b/test/unit/util/datatype_black.h @@ -78,8 +78,8 @@ public: ++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); } } @@ -115,8 +115,8 @@ public: 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); } } @@ -150,8 +150,8 @@ public: ++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); } } @@ -184,8 +184,8 @@ public: ++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); } } @@ -218,8 +218,8 @@ public: ++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); } } @@ -252,8 +252,8 @@ public: ++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); } } @@ -317,8 +317,8 @@ public: ++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()); @@ -334,8 +334,8 @@ public: ++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 @@ -365,8 +365,8 @@ public: ++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()); @@ -382,8 +382,8 @@ public: ++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]); } } @@ -403,14 +403,14 @@ public: 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 ) ); } } -- 2.30.2