From f55dfd4df98fbecbd0ef0f86da79d537457109d6 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 16 Nov 2011 03:47:25 +0000 Subject: [PATCH] Addressed many of the concerns raised in the public interface review of CVC4 Datatypes (bug #283) by Chris Conway. Thanks, Chris! --- src/compat/cvc3_compat.cpp | 12 +- src/expr/expr_manager_template.cpp | 8 +- src/expr/expr_manager_template.h | 2 +- src/expr/node_manager.cpp | 4 +- src/expr/node_manager.h | 2 +- src/parser/cvc/Cvc.g | 8 +- src/parser/parser.cpp | 4 +- src/parser/smt2/Smt2.g | 6 +- src/theory/datatypes/datatypes_rewriter.h | 2 +- src/theory/datatypes/theory_datatypes.cpp | 10 +- src/theory/datatypes/theory_datatypes.h | 2 +- src/util/datatype.cpp | 106 ++-- src/util/datatype.h | 593 ++++++++++++---------- src/util/datatype.i | 247 +-------- test/unit/util/datatype_black.h | 66 +-- 15 files changed, 446 insertions(+), 626 deletions(-) diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index fa5919e6a..a5d85821d 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -1079,11 +1079,11 @@ void ValidityChecker::dataType(const std::vector& names, AlwaysAssert(constructors[i].size() == selectors[i].size()); AlwaysAssert(constructors[i].size() == types[i].size()); for(unsigned j = 0; j < constructors[i].size(); ++j) { - CVC4::Datatype::Constructor ctor(constructors[i][j]); + CVC4::DatatypeConstructor ctor(constructors[i][j]); AlwaysAssert(selectors[i][j].size() == types[i][j].size()); for(unsigned k = 0; k < selectors[i][j].size(); ++k) { if(types[i][j][k].getType().isString()) { - ctor.addArg(selectors[i][j][k], CVC4::Datatype::UnresolvedType(types[i][j][k].getConst())); + ctor.addArg(selectors[i][j][k], CVC4::DatatypeUnresolvedType(types[i][j][k].getConst())); } else { ctor.addArg(selectors[i][j][k], exprToType(types[i][j][k])); } @@ -1106,7 +1106,7 @@ void ValidityChecker::dataType(const std::vector& names, // For each constructor, register its name and its selectors names. AlwaysAssert(d_constructors.find((*j).getName()) == d_constructors.end(), "cannot have two constructors with the same name in a ValidityChecker"); d_constructors[(*j).getName()] = &dt; - for(CVC4::Datatype::Constructor::const_iterator k = (*j).begin(); k != (*j).end(); ++k) { + for(CVC4::DatatypeConstructor::const_iterator k = (*j).begin(); k != (*j).end(); ++k) { AlwaysAssert(d_selectors.find((*k).getName()) == d_selectors.end(), "cannot have two selectors with the same name in a ValidityChecker"); d_selectors[(*k).getName()] = make_pair(&dt, (*j).getName()); } @@ -1769,7 +1769,7 @@ Expr ValidityChecker::datatypeConsExpr(const std::string& constructor, const std ConstructorMap::const_iterator i = d_constructors.find(constructor); AlwaysAssert(i != d_constructors.end(), "no such constructor"); const CVC4::Datatype& dt = *(*i).second; - const CVC4::Datatype::Constructor& ctor = dt[constructor]; + const CVC4::DatatypeConstructor& ctor = dt[constructor]; AlwaysAssert(ctor.getNumArgs() == args.size(), "arity mismatch in constructor application"); return d_em->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, ctor.getConstructor(), vector(args.begin(), args.end())); } @@ -1779,7 +1779,7 @@ Expr ValidityChecker::datatypeSelExpr(const std::string& selector, const Expr& a AlwaysAssert(i != d_selectors.end(), "no such selector"); const CVC4::Datatype& dt = *(*i).second.first; string constructor = (*i).second.second; - const CVC4::Datatype::Constructor& ctor = dt[constructor]; + const CVC4::DatatypeConstructor& ctor = dt[constructor]; return d_em->mkExpr(CVC4::kind::APPLY_SELECTOR, ctor.getSelector(selector), arg); } @@ -1787,7 +1787,7 @@ Expr ValidityChecker::datatypeTestExpr(const std::string& constructor, const Exp ConstructorMap::const_iterator i = d_constructors.find(constructor); AlwaysAssert(i != d_constructors.end(), "no such constructor"); const CVC4::Datatype& dt = *(*i).second; - const CVC4::Datatype::Constructor& ctor = dt[constructor]; + const CVC4::DatatypeConstructor& ctor = dt[constructor]; return d_em->mkExpr(CVC4::kind::APPLY_TESTER, ctor.getTester(), arg); } diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 12a60021e..576d0324d 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -638,7 +638,7 @@ void ExprManager::checkResolvedDatatype(DatatypeType dtt) const { for(Datatype::const_iterator i = dt.begin(), i_end = dt.end(); i != i_end; ++i) { - const Datatype::Constructor& c = *i; + const DatatypeConstructor& c = *i; Type testerType CVC4_UNUSED = c.getTester().getType(); Assert(c.isResolved() && testerType.isTester() && @@ -651,10 +651,10 @@ void ExprManager::checkResolvedDatatype(DatatypeType dtt) const { ConstructorType(ctorType).getRangeType() == dtt, "malformed constructor in datatype post-resolution"); // for all selectors... - for(Datatype::Constructor::const_iterator j = c.begin(), j_end = c.end(); + for(DatatypeConstructor::const_iterator j = c.begin(), j_end = c.end(); j != j_end; ++j) { - const Datatype::Constructor::Arg& a = *j; + const DatatypeConstructorArg& a = *j; Type selectorType = a.getSelector().getType(); Assert(a.isResolved() && selectorType.isSelector() && @@ -669,7 +669,7 @@ void ExprManager::checkResolvedDatatype(DatatypeType dtt) const { } } -ConstructorType ExprManager::mkConstructorType(const Datatype::Constructor& constructor, Type range) const { +ConstructorType ExprManager::mkConstructorType(const DatatypeConstructor& constructor, Type range) const { NodeManagerScope nms(d_nodeManager); return Type(d_nodeManager, new TypeNode(d_nodeManager->mkConstructorType(constructor, *range.d_typeNode))); } diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index ade9a334d..81d30fd1e 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -381,7 +381,7 @@ public: /** * Make a type representing a constructor with the given parameterization. */ - ConstructorType mkConstructorType(const Datatype::Constructor& constructor, Type range) const; + ConstructorType mkConstructorType(const DatatypeConstructor& constructor, Type range) const; /** Make a type representing a selector with the given parameterization. */ SelectorType mkSelectorType(Type domain, Type range) const; diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 3b4d8ac66..2bf0a864a 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -298,11 +298,11 @@ TypeNode NodeManager::getType(TNode n, bool check) return typeNode; } -TypeNode NodeManager::mkConstructorType(const Datatype::Constructor& constructor, +TypeNode NodeManager::mkConstructorType(const DatatypeConstructor& constructor, TypeNode range) { std::vector sorts; Debug("datatypes") << "ctor name: " << constructor.getName() << std::endl; - for(Datatype::Constructor::const_iterator i = constructor.begin(); + for(DatatypeConstructor::const_iterator i = constructor.begin(); i != constructor.end(); ++i) { TypeNode selectorType = *(*i).getSelector().getType().d_typeNode; diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index adba8087c..3646e91c5 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -580,7 +580,7 @@ public: inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType); /** Make a type representing a constructor with the given parameterization */ - TypeNode mkConstructorType(const Datatype::Constructor& constructor, TypeNode range); + TypeNode mkConstructorType(const DatatypeConstructor& constructor, TypeNode range); /** Make a type representing a selector with the given parameterization */ inline TypeNode mkSelectorType(TypeNode domain, TypeNode range); diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 22cf368eb..2d659cfe3 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1486,7 +1486,7 @@ postfixTerm[CVC4::Expr& f] { if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && t.isDatatype()) { std::vector v; Expr e = f.getOperator(); - const Datatype::Constructor& dtc = Datatype::datatypeOf(e)[Datatype::indexOf(e)]; + const DatatypeConstructor& dtc = Datatype::datatypeOf(e)[Datatype::indexOf(e)]; v.push_back(MK_EXPR( CVC4::kind::APPLY_TYPE_ASCRIPTION, MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(t))), f.getOperator() )); v.insert(v.end(), f.begin(), f.end()); @@ -1783,14 +1783,14 @@ datatypeDef[std::vector& datatypes] constructorDef[CVC4::Datatype& type] @init { std::string id; - CVC4::Datatype::Constructor* ctor = NULL; + CVC4::DatatypeConstructor* ctor = NULL; } : identifier[id,CHECK_UNDECLARED,SYM_SORT] { // make the tester std::string testerId("is_"); testerId.append(id); PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_SORT); - ctor = new CVC4::Datatype::Constructor(id, testerId); + ctor = new CVC4::DatatypeConstructor(id, testerId); } ( LPAREN selector[*ctor] @@ -1804,7 +1804,7 @@ constructorDef[CVC4::Datatype& type] } ; -selector[CVC4::Datatype::Constructor& ctor] +selector[CVC4::DatatypeConstructor& ctor] @init { std::string id; Type t, t2; diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index f1ad4b330..4418ea18f 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -286,7 +286,7 @@ Parser::mkMutualDatatypeTypes(const std::vector& datatypes) { j_end = dt.end(); j != j_end; ++j) { - const Datatype::Constructor& ctor = *j; + const DatatypeConstructor& ctor = *j; Expr::printtypes::Scope pts(Debug("parser-idt"), true); Expr constructor = ctor.getConstructor(); Debug("parser-idt") << "+ define " << constructor << std::endl; @@ -302,7 +302,7 @@ Parser::mkMutualDatatypeTypes(const std::vector& datatypes) { throw ParserException(testerName + " already declared"); } defineVar(testerName, tester); - for(Datatype::Constructor::const_iterator k = ctor.begin(), + for(DatatypeConstructor::const_iterator k = ctor.begin(), k_end = ctor.end(); k != k_end; ++k) { diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 974de29b2..a093aa1ef 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -824,14 +824,14 @@ datatypeDef[std::vector& datatypes] constructorDef[CVC4::Datatype& type] @init { std::string id; - CVC4::Datatype::Constructor* ctor = NULL; + CVC4::DatatypeConstructor* ctor = NULL; } : symbol[id,CHECK_UNDECLARED,SYM_SORT] { // make the tester std::string testerId("is_"); testerId.append(id); PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_SORT); - ctor = new CVC4::Datatype::Constructor(id, testerId); + ctor = new CVC4::DatatypeConstructor(id, testerId); } ( LPAREN_TOK selector[*ctor] RPAREN_TOK )* { // make the constructor @@ -841,7 +841,7 @@ constructorDef[CVC4::Datatype& type] } ; -selector[CVC4::Datatype::Constructor& ctor] +selector[CVC4::DatatypeConstructor& ctor] @init { std::string id; Type t, t2; diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 7a45c98aa..23768545d 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -67,7 +67,7 @@ public: size_t selectorIndex = Datatype::indexOf(selectorExpr); size_t constructorIndex = Datatype::indexOf(constructorExpr); const Datatype& dt = Datatype::datatypeOf(constructorExpr); - const Datatype::Constructor& c = dt[constructorIndex]; + const DatatypeConstructor& c = dt[constructorIndex]; if(c.getNumArgs() > selectorIndex && c[selectorIndex].getSelector() == selectorExpr) { Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 6b067c681..75980993b 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -32,7 +32,7 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::datatypes; -const Datatype::Constructor& TheoryDatatypes::getConstructor( Node cons ) +const DatatypeConstructor& TheoryDatatypes::getConstructor( Node cons ) { Expr consExpr = cons.toExpr(); return Datatype::datatypeOf(consExpr)[ Datatype::indexOf(consExpr) ]; @@ -272,7 +272,7 @@ void TheoryDatatypes::check(Effort e) { } } if( !cons.isNull() ) { - const Datatype::Constructor& cn = getConstructor( cons ); + const DatatypeConstructor& cn = getConstructor( cons ); Debug("datatypes-split") << "*************Split for possible constructor " << cons << endl; Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( cn.getTester() ), (*i).first ); NodeBuilder<> nb(kind::OR); @@ -464,7 +464,7 @@ bool TheoryDatatypes::checkInstantiate( Node te, Node cons ) vector< Node > selectorVals; selectorVals.push_back( cons ); bool foundSel = false; - const Datatype::Constructor& cn = getConstructor( cons ); + const DatatypeConstructor& cn = getConstructor( cons ); for( unsigned int i=0; imkNode( APPLY_SELECTOR, Node::fromExpr( cn[i].getSelector() ), te ); if( d_selectors.find( s ) != d_selectors.end() ) { @@ -480,7 +480,7 @@ bool TheoryDatatypes::checkInstantiate( Node te, Node cons ) if( val.getType()!=te.getType() ){ //IDT-param Assert( Datatype::datatypeOf( cons.toExpr() ).isParametric() ); Debug("datatypes-gt") << "Inst: ambiguous type for " << cons << ", ascribe to " << te.getType() << std::endl; - const Datatype::Constructor& dtc = Datatype::datatypeOf(cons.toExpr())[Datatype::indexOf(cons.toExpr())]; + const DatatypeConstructor& dtc = Datatype::datatypeOf(cons.toExpr())[Datatype::indexOf(cons.toExpr())]; Debug("datatypes-gt") << "constructor is " << dtc << std::endl; Type tspec = dtc.getSpecializedConstructorType(te.getType().toType()); Debug("datatypes-gt") << "tpec is " << tspec << std::endl; @@ -537,7 +537,7 @@ bool TheoryDatatypes::collapseSelector( Node t ) { Node sel = t.getOperator(); TypeNode selType = sel.getType(); Node cons = getConstructorForSelector( sel ); - const Datatype::Constructor& cn = getConstructor( cons ); + const DatatypeConstructor& cn = getConstructor( cons ); Node tmp = find( t[0] ); Node retNode = t; if( tmp.getKind() == APPLY_CONSTRUCTOR ) { diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 433af38c3..4d429bc54 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -65,7 +65,7 @@ private: /** has seen cycle */ context::CDO< bool > d_hasSeenCycle; /** get the constructor for the node */ - const Datatype::Constructor& getConstructor( Node cons ); + const DatatypeConstructor& getConstructor( Node cons ); /** get the constructor for the selector */ Node getConstructorForSelector( Node sel ); diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 19415769e..f009bbbbe 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -95,6 +95,8 @@ void Datatype::resolve(ExprManager* em, "Datatype::resolve(): resolutions doesn't contain me!"); AssertArgument(placeholders.size() == replacements.size(), placeholders, "placeholders and replacements must be the same size"); + AssertArgument(paramTypes.size() == paramReplacements.size(), paramTypes, + "paramTypes and paramReplacements must be the same size"); CheckArgument(getNumConstructors() > 0, *this, "cannot resolve a Datatype that has no constructors"); DatatypeType self = (*resolutions.find(d_name)).second; AssertArgument(&self.getDatatype() == this, "Datatype::resolve(): resolutions doesn't contain me!"); @@ -110,7 +112,7 @@ void Datatype::resolve(ExprManager* em, Assert(index == getNumConstructors()); } -void Datatype::addConstructor(const Constructor& c) { +void Datatype::addConstructor(const DatatypeConstructor& c) { CheckArgument(!d_resolved, this, "cannot add a constructor to a finalized Datatype"); d_constructors.push_back(c); @@ -233,7 +235,7 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(AssertionException) { i != i_end; ++i) { if( groundTerm.isNull() ){ - Constructor::const_iterator j = (*i).begin(), j_end = (*i).end(); + DatatypeConstructor::const_iterator j = (*i).begin(), j_end = (*i).end(); for(; j != j_end; ++j) { SelectorType stype((*j).getSelector().getType()); if(stype.getDomain() == stype.getRangeType()) { @@ -245,7 +247,7 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(AssertionException) { if(j == j_end && (*i).isWellFounded()) { groundTerm = (*i).mkGroundTerm( t ); - // Constructor::mkGroundTerm() doesn't ever return null when + // DatatypeConstructor::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 @@ -253,7 +255,7 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(AssertionException) { // 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 + // RecursionBreaker<> in DatatypeConstructor::mkGroundTerm(). In the // case of recursion, it returns null. if(!groundTerm.isNull()) { // we found a ground-term-constructing constructor! @@ -323,7 +325,7 @@ bool Datatype::operator==(const Datatype& other) const throw() { if(!(*i).d_tester.isNull() && (*i).d_tester != (*j).d_tester) { return false; } - for(Constructor::const_iterator k = (*i).begin(), l = (*j).begin(); k != (*i).end(); ++k, ++l) { + 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; @@ -359,12 +361,12 @@ bool Datatype::operator==(const Datatype& other) const throw() { return true; } -const Datatype::Constructor& Datatype::operator[](size_t index) const { +const DatatypeConstructor& Datatype::operator[](size_t index) const { CheckArgument(index < getNumConstructors(), index, "index out of bounds"); return d_constructors[index]; } -const Datatype::Constructor& Datatype::operator[](std::string name) const { +const DatatypeConstructor& Datatype::operator[](std::string name) const { for(const_iterator i = begin(); i != end(); ++i) { if((*i).getName() == name) { return *i; @@ -377,12 +379,12 @@ Expr Datatype::getConstructor(std::string name) const { return (*this)[name].getConstructor(); } -void Datatype::Constructor::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) +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) throw(AssertionException, DatatypeResolutionException) { AssertArgument(em != NULL, "cannot resolve a Datatype with a NULL expression manager"); @@ -428,7 +430,7 @@ void Datatype::Constructor::resolve(ExprManager* em, DatatypeType self, Assert(index == getNumArgs()); - // Set constructor/tester last, since Constructor::isResolved() + // 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 @@ -442,7 +444,7 @@ void Datatype::Constructor::resolve(ExprManager* em, DatatypeType self, } } -Type Datatype::Constructor::doParametricSubstitution( Type range, +Type DatatypeConstructor::doParametricSubstitution( Type range, const std::vector< SortConstructorType >& paramTypes, const std::vector< DatatypeType >& paramReplacements ) { TypeNode typn = TypeNode::fromType( range ); @@ -455,23 +457,23 @@ Type Datatype::Constructor::doParametricSubstitution( Type range, origChildren.push_back( (*i).toType() ); children.push_back( doParametricSubstitution( (*i).toType(), paramTypes, paramReplacements ) ); } - for( int i=0; i<(int)paramTypes.size(); i++ ) { - if( paramTypes[i].getArity()==origChildren.size() ) { + for( unsigned i = 0; i < paramTypes.size(); ++i ) { + if( paramTypes[i].getArity() == origChildren.size() ) { Type tn = paramTypes[i].instantiate( origChildren ); - if( range==tn ) { + if( range == tn ) { return paramReplacements[i].instantiate( children ); } } } NodeBuilder<> nb(typn.getKind()); - for( int i=0; i<(int)children.size(); i++ ) { + for( unsigned i = 0; i < children.size(); ++i ) { nb << TypeNode::fromType( children[i] ); } return nb.constructTypeNode().toType(); } } -Datatype::Constructor::Constructor(std::string name) : +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 @@ -482,7 +484,7 @@ Datatype::Constructor::Constructor(std::string name) : CheckArgument(name != "", name, "cannot construct a datatype constructor without a name"); } -Datatype::Constructor::Constructor(std::string name, std::string tester) : +DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester) : // 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 @@ -494,7 +496,7 @@ Datatype::Constructor::Constructor(std::string name, std::string tester) : CheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester"); } -void Datatype::Constructor::addArg(std::string selectorName, Type selectorType) { +void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) { // 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 selector type away inside a var until resolution (when we can @@ -503,30 +505,30 @@ void Datatype::Constructor::addArg(std::string selectorName, Type selectorType) CheckArgument(!selectorType.isNull(), selectorType, "cannot add a null selector type"); Expr type = selectorType.getExprManager()->mkVar(selectorType); Debug("datatypes") << type << endl; - d_args.push_back(Arg(selectorName, type)); + d_args.push_back(DatatypeConstructorArg(selectorName, type)); } -void Datatype::Constructor::addArg(std::string selectorName, Datatype::UnresolvedType selectorType) { +void DatatypeConstructor::addArg(std::string selectorName, DatatypeUnresolvedType selectorType) { // 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 selector type away after a NUL in the name string until // resolution (when we can create the proper selector type) CheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor"); CheckArgument(selectorType.getName() != "", selectorType, "cannot add a null selector type"); - d_args.push_back(Arg(selectorName + '\0' + selectorType.getName(), Expr())); + d_args.push_back(DatatypeConstructorArg(selectorName + '\0' + selectorType.getName(), Expr())); } -void Datatype::Constructor::addArg(std::string selectorName, Datatype::SelfType) { +void DatatypeConstructor::addArg(std::string selectorName, DatatypeSelfType) { // 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 mark // the name string with a NUL to indicate that we have a // self-selecting selector until resolution (when we can create the // proper selector type) CheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor"); - d_args.push_back(Arg(selectorName + '\0', Expr())); + d_args.push_back(DatatypeConstructorArg(selectorName + '\0', Expr())); } -std::string Datatype::Constructor::getName() const throw() { +std::string DatatypeConstructor::getName() const throw() { string name = d_name; if(!isResolved()) { name.resize(name.find('\0')); @@ -534,16 +536,16 @@ std::string Datatype::Constructor::getName() const throw() { return name; } -Expr Datatype::Constructor::getConstructor() const { +Expr DatatypeConstructor::getConstructor() const { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); return d_constructor; } -Type Datatype::Constructor::getSpecializedConstructorType(Type returnType) const { +Type DatatypeConstructor::getSpecializedConstructorType(Type returnType) const { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); const Datatype& dt = Datatype::datatypeOf(d_constructor); CheckArgument(dt.isParametric(), this, "this datatype constructor is not yet resolved"); - DatatypeType dtt = DatatypeType(dt.d_self); + DatatypeType dtt = dt.getDatatypeType(); Matcher m(dtt); m.doMatching( TypeNode::fromType(dtt), TypeNode::fromType(returnType) ); vector subst; @@ -552,12 +554,12 @@ Type Datatype::Constructor::getSpecializedConstructorType(Type returnType) const return d_constructor.getType().substitute(params, subst); } -Expr Datatype::Constructor::getTester() const { +Expr DatatypeConstructor::getTester() const { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); return d_tester; } -Cardinality Datatype::Constructor::getCardinality() const throw(AssertionException) { +Cardinality DatatypeConstructor::getCardinality() const throw(AssertionException) { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); Cardinality c = 1; @@ -569,7 +571,7 @@ Cardinality Datatype::Constructor::getCardinality() const throw(AssertionExcepti return c; } -bool Datatype::Constructor::isFinite() const throw(AssertionException) { +bool DatatypeConstructor::isFinite() const throw(AssertionException) { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); // we're using some internals, so we have to set up this library context @@ -595,7 +597,7 @@ bool Datatype::Constructor::isFinite() const throw(AssertionException) { return true; } -bool Datatype::Constructor::isWellFounded() const throw(AssertionException) { +bool DatatypeConstructor::isWellFounded() const throw(AssertionException) { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); // we're using some internals, so we have to set up this library context @@ -608,7 +610,7 @@ bool Datatype::Constructor::isWellFounded() const throw(AssertionException) { return self.getAttribute(DatatypeWellFoundedAttr()); } - RecursionBreaker breaker(__PRETTY_FUNCTION__, this); + RecursionBreaker breaker(__PRETTY_FUNCTION__, this); if(breaker.isRecursion()) { // This *path* is cyclic, sso may not be well-founded. The // constructor itself might still be well-founded, though (we'll @@ -639,7 +641,7 @@ bool Datatype::Constructor::isWellFounded() const throw(AssertionException) { return true; } -Expr Datatype::Constructor::mkGroundTerm( Type t ) const throw(AssertionException) { +Expr DatatypeConstructor::mkGroundTerm( Type t ) const throw(AssertionException) { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); // we're using some internals, so we have to set up this library context @@ -653,7 +655,7 @@ Expr Datatype::Constructor::mkGroundTerm( Type t ) const throw(AssertionExceptio return groundTerm; } - RecursionBreaker breaker(__PRETTY_FUNCTION__, this); + RecursionBreaker breaker(__PRETTY_FUNCTION__, this); if(breaker.isRecursion()) { // Recursive path, we should skip and go to the next constructor; // see lengthy comments in Datatype::mkGroundTerm(). @@ -693,12 +695,12 @@ Expr Datatype::Constructor::mkGroundTerm( Type t ) const throw(AssertionExceptio return groundTerm; } -const Datatype::Constructor::Arg& Datatype::Constructor::operator[](size_t index) const { +const DatatypeConstructorArg& DatatypeConstructor::operator[](size_t index) const { CheckArgument(index < getNumArgs(), index, "index out of bounds"); return d_args[index]; } -const Datatype::Constructor::Arg& Datatype::Constructor::operator[](std::string name) const { +const DatatypeConstructorArg& DatatypeConstructor::operator[](std::string name) const { for(const_iterator i = begin(); i != end(); ++i) { if((*i).getName() == name) { return *i; @@ -707,18 +709,18 @@ const Datatype::Constructor::Arg& Datatype::Constructor::operator[](std::string CheckArgument(false, name, "No such arg `%s' of constructor `%s'", name.c_str(), d_name.c_str()); } -Expr Datatype::Constructor::getSelector(std::string name) const { +Expr DatatypeConstructor::getSelector(std::string name) const { return (*this)[name].getSelector(); } -Datatype::Constructor::Arg::Arg(std::string name, Expr selector) : +DatatypeConstructorArg::DatatypeConstructorArg(std::string name, Expr selector) : d_name(name), d_selector(selector), d_resolved(false) { CheckArgument(name != "", name, "cannot construct a datatype constructor arg without a name"); } -std::string Datatype::Constructor::Arg::getName() const throw() { +std::string DatatypeConstructorArg::getName() const throw() { string name = d_name; const size_t nul = name.find('\0'); if(nul != string::npos) { @@ -727,28 +729,28 @@ std::string Datatype::Constructor::Arg::getName() const throw() { return name; } -Expr Datatype::Constructor::Arg::getSelector() const { +Expr DatatypeConstructorArg::getSelector() const { CheckArgument(isResolved(), this, "cannot get a selector for an unresolved datatype constructor"); return d_selector; } -Expr Datatype::Constructor::Arg::getConstructor() const { +Expr DatatypeConstructorArg::getConstructor() const { CheckArgument(isResolved(), this, "cannot get a associated constructor for argument of an unresolved datatype constructor"); return d_constructor; } -Type Datatype::Constructor::Arg::getSelectorType() const { +Type DatatypeConstructorArg::getType() const { return getSelector().getType(); } -bool Datatype::Constructor::Arg::isUnresolvedSelf() const throw() { +bool DatatypeConstructorArg::isUnresolvedSelf() const throw() { return d_selector.isNull() && d_name.size() == d_name.find('\0') + 1; } static const int s_printDatatypeNamesOnly = std::ios_base::xalloc(); -std::string Datatype::Constructor::Arg::getSelectorTypeName() const { +std::string DatatypeConstructorArg::getTypeName() const { Type t; if(isResolved()) { t = SelectorType(d_selector.getType()).getRangeType(); @@ -809,13 +811,13 @@ std::ostream& operator<<(std::ostream& os, const Datatype& dt) { return os; } -std::ostream& operator<<(std::ostream& os, const Datatype::Constructor& ctor) { +std::ostream& operator<<(std::ostream& os, const DatatypeConstructor& ctor) { // can only output datatypes in the CVC4 native language Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4); os << ctor.getName(); - Datatype::Constructor::const_iterator i = ctor.begin(), i_end = ctor.end(); + DatatypeConstructor::const_iterator i = ctor.begin(), i_end = ctor.end(); if(i != i_end) { os << "("; do { @@ -830,11 +832,11 @@ std::ostream& operator<<(std::ostream& os, const Datatype::Constructor& ctor) { return os; } -std::ostream& operator<<(std::ostream& os, const Datatype::Constructor::Arg& arg) { +std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) { // can only output datatypes in the CVC4 native language Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4); - os << arg.getName() << ": " << arg.getSelectorTypeName(); + os << arg.getName() << ": " << arg.getTypeName(); return os; } diff --git a/src/util/datatype.h b/src/util/datatype.h index 24a625bd1..5a1d9b931 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -52,6 +52,259 @@ public: inline DatatypeResolutionException(std::string msg); };/* class DatatypeResolutionException */ +/** + * A holder type (used in calls to DatatypeConstructor::addArg()) + * to allow a Datatype to refer to itself. Self-typed fields of + * Datatypes will be properly typed when a Type is created for the + * Datatype by the ExprManager (which calls Datatype::resolve()). + */ +class CVC4_PUBLIC DatatypeSelfType { +};/* class DatatypeSelfType */ + +/** + * An unresolved type (used in calls to + * DatatypeConstructor::addArg()) to allow a Datatype to refer to + * itself or to other mutually-recursive Datatypes. Unresolved-type + * fields of Datatypes will be properly typed when a Type is created + * for the Datatype by the ExprManager (which calls + * Datatype::resolve()). + */ +class CVC4_PUBLIC DatatypeUnresolvedType { + std::string d_name; +public: + inline DatatypeUnresolvedType(std::string name); + inline std::string getName() const throw(); +};/* class DatatypeUnresolvedType */ + +/** + * A Datatype constructor argument (i.e., a Datatype field). + */ +class CVC4_PUBLIC DatatypeConstructorArg { + + std::string d_name; + Expr d_selector; + /** the constructor associated with this selector */ + Expr d_constructor; + bool d_resolved; + + DatatypeConstructorArg(std::string name, Expr selector); + friend class DatatypeConstructor; + friend class Datatype; + + bool isUnresolvedSelf() const throw(); + +public: + + /** Get the name of this constructor argument. */ + std::string getName() const throw(); + + /** + * Get the selector for this constructor argument; this call is + * only permitted after resolution. + */ + Expr getSelector() const; + + /** + * Get the associated constructor for this constructor argument; + * this call is only permitted after resolution. + */ + Expr getConstructor() const; + + /** + * Get the type of the selector for this constructor argument; + * this call is only permitted after resolution. + */ + Type getType() const; + + /** + * Get the name of the type of this constructor argument + * (Datatype field). Can be used for not-yet-resolved Datatypes + * (in which case the name of the unresolved type, or "[self]" + * for a self-referential type is returned). + */ + std::string getTypeName() const; + + /** + * Returns true iff this constructor argument has been resolved. + */ + bool isResolved() const throw(); + +};/* class DatatypeConstructorArg */ + +/** + * A constructor for a Datatype. + */ +class CVC4_PUBLIC DatatypeConstructor { +public: + + /** The type for iterators over constructor arguments. */ + typedef std::vector::iterator iterator; + /** The (const) type for iterators over constructor arguments. */ + typedef std::vector::const_iterator const_iterator; + +private: + + std::string d_name; + Expr d_constructor; + Expr d_tester; + std::vector d_args; + + void 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) + throw(AssertionException, DatatypeResolutionException); + friend class Datatype; + + /** @FIXME document this! */ + Type doParametricSubstitution(Type range, + const std::vector< SortConstructorType >& paramTypes, + const std::vector< DatatypeType >& paramReplacements); +public: + /** + * Create a new Datatype constructor with the given name for the + * constructor and the same name (prefixed with "is_") for the + * tester. The actual constructor and tester (meaning, the Exprs + * representing operators for these entities) aren't created until + * resolution time. + */ + explicit DatatypeConstructor(std::string name); + + /** + * Create a new Datatype constructor with the given name for the + * constructor and the given name for the tester. The actual + * constructor and tester aren't created until resolution time. + */ + DatatypeConstructor(std::string name, std::string tester); + + /** + * Add an argument (i.e., a data field) of the given name and type + * to this Datatype constructor. Selector names need not be unique; + * they are for convenience and pretty-printing only. + */ + void addArg(std::string selectorName, Type selectorType); + + /** + * Add an argument (i.e., a data field) of the given name to this + * Datatype constructor that refers to an as-yet-unresolved + * Datatype (which may be mutually-recursive). Selector names need + * not be unique; they are for convenience and pretty-printing only. + */ + void addArg(std::string selectorName, DatatypeUnresolvedType selectorType); + + /** + * Add a self-referential (i.e., a data field) of the given name + * to this Datatype constructor that refers to the enclosing + * Datatype. For example, using the familiar "nat" Datatype, to + * create the "pred" field for "succ" constructor, one uses + * succ::addArg("pred", DatatypeSelfType())---the actual Type + * cannot be passed because the Datatype is still under + * construction. Selector names need not be unique; they are for + * convenience and pretty-printing only. + * + * This is a special case of + * DatatypeConstructor::addArg(std::string, DatatypeUnresolvedType). + */ + void addArg(std::string selectorName, DatatypeSelfType); + + /** Get the name of this Datatype constructor. */ + std::string getName() const throw(); + + /** + * Get the constructor operator of this Datatype constructor. The + * Datatype must be resolved. + */ + Expr getConstructor() const; + + /** + * Get the tester operator of this Datatype constructor. The + * Datatype must be resolved. + */ + Expr getTester() const; + + /** + * Get the number of arguments (so far) of this Datatype constructor. + */ + inline size_t getNumArgs() const throw(); + + /** + * Get the specialized constructor type for a parametric + * constructor; this call is only permitted after resolution. + * Given a (concrete) returnType, the constructor's concrete + * type in this parametric datatype is returned. + * + * For instance, if the datatype is list[T], with constructor + * "cons[T]" of type "T -> list[T] -> list[T]", then calling + * this function with "list[int]" will return the concrete + * "cons" constructor type for lists of int---namely, + * "int -> list[int] -> list[int]". + */ + Type getSpecializedConstructorType(Type returnType) const; + + /** + * Return the cardinality of this constructor (the product of the + * cardinalities of its arguments). + */ + Cardinality getCardinality() const throw(AssertionException); + + /** + * Return true iff this constructor is finite (it is nullary or + * each of its argument types are finite). This function can + * only be called for resolved constructors. + */ + bool isFinite() const throw(AssertionException); + + /** + * Return true iff this constructor is well-founded (there exist + * ground terms). The constructor must be resolved or an + * exception is thrown. + */ + bool isWellFounded() const throw(AssertionException); + + /** + * Construct and return a ground term of this constructor. The + * constructor must be both resolved and well-founded, or else an + * exception is thrown. + */ + Expr mkGroundTerm( Type t ) const throw(AssertionException); + + /** + * Returns true iff this Datatype constructor has already been + * resolved. + */ + inline bool isResolved() const throw(); + + /** Get the beginning iterator over DatatypeConstructor args. */ + inline iterator begin() throw(); + /** Get the ending iterator over DatatypeConstructor args. */ + inline iterator end() throw(); + /** Get the beginning const_iterator over DatatypeConstructor args. */ + inline const_iterator begin() const throw(); + /** Get the ending const_iterator over DatatypeConstructor args. */ + inline const_iterator end() const throw(); + + /** Get the ith DatatypeConstructor arg. */ + const DatatypeConstructorArg& operator[](size_t index) const; + + /** + * Get the DatatypeConstructor arg named. This is a linear search + * through the arguments, so in the case of multiple, + * similarly-named arguments, the first is returned. + */ + const DatatypeConstructorArg& operator[](std::string name) const; + + /** + * Get the selector named. This is a linear search + * through the arguments, so in the case of multiple, + * similarly-named arguments, the selector for the first + * is returned. + */ + Expr getSelector(std::string name) const; + +};/* class DatatypeConstructor */ + /** * The representation of an inductive datatype. * @@ -66,7 +319,7 @@ public: * You cannot define "nat" until you have a Type for it, but you * cannot have a Type for it until you fill in the type of the "pred" * selector, which needs the Type. So we have a chicken-and-egg - * problem. It's even more complicated when we have mutual recusion + * problem. It's even more complicated when we have mutual recursion * between datatypes, since the CVC presentation language does not * require forward-declarations. Here, we define trees of lists that * contain trees of lists (etc): @@ -94,8 +347,9 @@ public: * on the task of generating its own selectors and testers, for * instance. That means that, after reifying the Datatype with the * ExprManager, the parser needs to go through the (now-resolved) - * Datatype and request ; see src/parser/parser.cpp for how this is - * done. For API usage ideas, see test/unit/util/datatype_black.h. + * Datatype and request the constructor, selector, and tester terms. + * See src/parser/parser.cpp for how this is done. For API usage + * ideas, see test/unit/util/datatype_black.h. */ class CVC4_PUBLIC Datatype { public: @@ -111,255 +365,15 @@ public: */ static size_t indexOf(Expr item) CVC4_PUBLIC; - /** - * A holder type (used in calls to Datatype::Constructor::addArg()) - * to allow a Datatype to refer to itself. Self-typed fields of - * Datatypes will be properly typed when a Type is created for the - * Datatype by the ExprManager (which calls Datatype::resolve()). - */ - class CVC4_PUBLIC SelfType { - };/* class Datatype::SelfType */ - - /** - * An unresolved type (used in calls to - * Datatype::Constructor::addArg()) to allow a Datatype to refer to - * itself or to other mutually-recursive Datatypes. Unresolved-type - * fields of Datatypes will be properly typed when a Type is created - * for the Datatype by the ExprManager (which calls - * Datatype::resolve()). - */ - class CVC4_PUBLIC UnresolvedType { - std::string d_name; - public: - inline UnresolvedType(std::string name); - inline std::string getName() const throw(); - };/* class Datatype::UnresolvedType */ - - /** - * A constructor for a Datatype. - */ - class CVC4_PUBLIC Constructor { - public: - /** - * A Datatype constructor argument (i.e., a Datatype field). - */ - class CVC4_PUBLIC Arg { - - std::string d_name; - Expr d_selector; - /** the constructor associated with this selector */ - Expr d_constructor; - bool d_resolved; - - explicit Arg(std::string name, Expr selector); - friend class Constructor; - friend class Datatype; - - bool isUnresolvedSelf() const throw(); - - public: - - /** Get the name of this constructor argument. */ - std::string getName() const throw(); - - /** - * Get the selector for this constructor argument; this call is - * only permitted after resolution. - */ - Expr getSelector() const; - - /** - * Get the associated constructor for this constructor argument; - * this call is only permitted after resolution. - */ - Expr getConstructor() const; - - /** - * Get the selector for this constructor argument; this call is - * only permitted after resolution. - */ - Type getSelectorType() const; - - /** - * Get the name of the type of this constructor argument - * (Datatype field). Can be used for not-yet-resolved Datatypes - * (in which case the name of the unresolved type, or "[self]" - * for a self-referential type is returned). - */ - std::string getSelectorTypeName() const; - - /** - * Returns true iff this constructor argument has been resolved. - */ - bool isResolved() const throw(); - - };/* class Datatype::Constructor::Arg */ - - /** The type for iterators over constructor arguments. */ - typedef std::vector::iterator iterator; - /** The (const) type for iterators over constructor arguments. */ - typedef std::vector::const_iterator const_iterator; - - private: - - std::string d_name; - Expr d_constructor; - Expr d_tester; - std::vector d_args; - - void 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) - throw(AssertionException, DatatypeResolutionException); - friend class Datatype; - - /** @FIXME document this! */ - Type doParametricSubstitution(Type range, - const std::vector< SortConstructorType >& paramTypes, - const std::vector< DatatypeType >& paramReplacements); - public: - /** - * Create a new Datatype constructor with the given name for the - * constructor and the same name (prefixed with "is_") for the - * tester. The actual constructor and tester aren't created until - * resolution time. - */ - explicit Constructor(std::string name); - - /** - * Create a new Datatype constructor with the given name for the - * constructor and the given name for the tester. The actual - * constructor and tester aren't created until resolution time. - */ - explicit Constructor(std::string name, std::string tester); - - /** - * Add an argument (i.e., a data field) of the given name and type - * to this Datatype constructor. - */ - void addArg(std::string selectorName, Type selectorType); - - /** - * Add an argument (i.e., a data field) of the given name to this - * Datatype constructor that refers to an as-yet-unresolved - * Datatype (which may be mutually-recursive). - */ - void addArg(std::string selectorName, Datatype::UnresolvedType selectorType); - - /** - * Add a self-referential (i.e., a data field) of the given name - * to this Datatype constructor that refers to the enclosing - * Datatype. For example, using the familiar "nat" Datatype, to - * create the "pred" field for "succ" constructor, one uses - * succ::addArg("pred", Datatype::SelfType())---the actual Type - * cannot be passed because the Datatype is still under - * construction. - * - * This is a special case of - * Constructor::addArg(std::string, Datatype::UnresolvedType). - */ - void addArg(std::string selectorName, Datatype::SelfType); - - /** Get the name of this Datatype constructor. */ - std::string getName() const throw(); - - /** - * Get the constructor operator of this Datatype constructor. The - * Datatype must be resolved. - */ - Expr getConstructor() const; - - /** - * Get the tester operator of this Datatype constructor. The - * Datatype must be resolved. - */ - Expr getTester() const; - - /** - * Get the number of arguments (so far) of this Datatype constructor. - */ - inline size_t getNumArgs() const throw(); - - /** - * Get the specialized constructor type for a parametric - * constructor; this call is only permitted after resolution. - */ - Type getSpecializedConstructorType(Type returnType) const; - - /** - * Return the cardinality of this constructor (the product of the - * cardinalities of its arguments). - */ - Cardinality getCardinality() const throw(AssertionException); - - /** - * Return true iff this constructor is finite (it is nullary or - * each of its argument types are finite). This function can - * only be called for resolved constructors. - */ - bool isFinite() const throw(AssertionException); - - /** - * Return true iff this constructor is well-founded (there exist - * ground terms). The constructor must be resolved or an - * exception is thrown. - */ - bool isWellFounded() const throw(AssertionException); - - /** - * Construct and return a ground term of this constructor. The - * constructor must be both resolved and well-founded, or else an - * exception is thrown. - */ - Expr mkGroundTerm( Type t ) const throw(AssertionException); - - /** - * Returns true iff this Datatype constructor has already been - * resolved. - */ - inline bool isResolved() const throw(); - - /** Get the beginning iterator over Constructor args. */ - inline iterator begin() throw(); - /** Get the ending iterator over Constructor args. */ - inline iterator end() throw(); - /** Get the beginning const_iterator over Constructor args. */ - inline const_iterator begin() const throw(); - /** Get the ending const_iterator over Constructor args. */ - inline const_iterator end() const throw(); - - /** Get the ith Constructor arg. */ - const Arg& operator[](size_t index) const; - - /** - * Get the Constructor arg named. This is a linear search - * through the arguments, so in the case of multiple, - * similarly-named arguments, the first is returned. - */ - const Arg& operator[](std::string name) const; - - /** - * Get the selector named. This is a linear search - * through the arguments, so in the case of multiple, - * similarly-named arguments, the selector for the first - * is returned. - */ - Expr getSelector(std::string name) const; - - };/* class Datatype::Constructor */ - /** The type for iterators over constructors. */ - typedef std::vector::iterator iterator; + typedef std::vector::iterator iterator; /** The (const) type for iterators over constructors. */ - typedef std::vector::const_iterator const_iterator; + typedef std::vector::const_iterator const_iterator; private: std::string d_name; std::vector d_params; - std::vector d_constructors; + std::vector d_constructors; bool d_resolved; Type d_self; @@ -368,9 +382,26 @@ private: * chicken-and-egg problem. The DatatypeType around the Datatype * cannot exist until the Datatype is finalized, and the Datatype * cannot refer to the DatatypeType representing itself until it - * exists. resolve() is called by the ExprManager when a Type. Has - * the effect of freezing the object, too; that is, addConstructor() - * will fail after a call to resolve(). + * exists. resolve() is called by the ExprManager when a Type is + * ultimately requested of the Datatype specification (that is, when + * ExprManager::mkDatatypeType() or ExprManager::mkMutualDatatypeTypes() + * is called). Has the effect of freezing the object, too; that is, + * addConstructor() will fail after a call to resolve(). + * + * The basic goal of resolution is to assign constructors, selectors, + * and testers. To do this, any UnresolvedType/SelfType references + * must be cleared up. This is the purpose of the "resolutions" map; + * it includes any mutually-recursive datatypes that are currently + * under resolution. The four vectors come in two pairs (so, really + * 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 be replaced + * @param replacements the corresponding replacements + * @param paramTypes the sort constructors in these Datatypes under resolution that must be replaced + * @param paramReplacements the corresponding (parametric) DatatypeTypes */ void resolve(ExprManager* em, const std::map& resolutions, @@ -390,10 +421,13 @@ public: * Create a new Datatype of the given name, with the given * parameterization. */ - inline explicit Datatype(std::string name, std::vector& params); + inline Datatype(std::string name, std::vector& params); - /** Add a constructor to this Datatype. */ - void addConstructor(const Constructor& c); + /** + * Add a constructor to this Datatype. Constructor names need not + * be unique; they are for convenience and pretty-printing only. + */ + void addConstructor(const DatatypeConstructor& c); /** Get the name of this Datatype. */ inline std::string getName() const throw(); @@ -473,34 +507,37 @@ public: /** Return true iff this Datatype has already been resolved. */ inline bool isResolved() const throw(); - /** Get the beginning iterator over Constructors. */ - inline std::vector::iterator begin() throw(); - /** Get the ending iterator over Constructors. */ - inline std::vector::iterator end() throw(); - /** Get the beginning const_iterator over Constructors. */ - inline std::vector::const_iterator begin() const throw(); - /** Get the ending const_iterator over Constructors. */ - inline std::vector::const_iterator end() const throw(); + /** Get the beginning iterator over DatatypeConstructors. */ + inline std::vector::iterator begin() throw(); + /** Get the ending iterator over DatatypeConstructors. */ + inline std::vector::iterator end() throw(); + /** Get the beginning const_iterator over DatatypeConstructors. */ + inline std::vector::const_iterator begin() const throw(); + /** Get the ending const_iterator over DatatypeConstructors. */ + inline std::vector::const_iterator end() const throw(); - /** Get the ith Constructor. */ - const Constructor& operator[](size_t index) const; + /** Get the ith DatatypeConstructor. */ + const DatatypeConstructor& operator[](size_t index) const; /** - * Get the Constructor named. This is a linear search + * Get the DatatypeConstructor named. This is a linear search * through the constructors, so in the case of multiple, * similarly-named constructors, the first is returned. */ - const Constructor& operator[](std::string name) const; + const DatatypeConstructor& operator[](std::string name) const; /** * Get the constructor operator for the named constructor. + * This is a linear search through the constructors, so in + * the case of multiple, similarly-named constructors, the + * first is returned. + * * This Datatype must be resolved. */ Expr getConstructor(std::string name) const; };/* class Datatype */ - /** * A hash strategy for Datatypes. Needed because Datatypes are used * as the constant payload in CONSTANT-kinded TypeNodes (for @@ -523,10 +560,10 @@ struct CVC4_PUBLIC DatatypeHashFunction { inline size_t operator()(const Datatype* dt) const { return StringHashFunction()(dt->getName()); } - inline size_t operator()(const Datatype::Constructor& dtc) const { + inline size_t operator()(const DatatypeConstructor& dtc) const { return StringHashFunction()(dtc.getName()); } - inline size_t operator()(const Datatype::Constructor* dtc) const { + inline size_t operator()(const DatatypeConstructor* dtc) const { return StringHashFunction()(dtc->getName()); } };/* struct DatatypeHashFunction */ @@ -534,8 +571,8 @@ struct CVC4_PUBLIC DatatypeHashFunction { // FUNCTION DECLARATIONS FOR OUTPUT STREAMS std::ostream& operator<<(std::ostream& os, const Datatype& dt) CVC4_PUBLIC; -std::ostream& operator<<(std::ostream& os, const Datatype::Constructor& ctor) CVC4_PUBLIC; -std::ostream& operator<<(std::ostream& os, const Datatype::Constructor::Arg& arg) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& os, const DatatypeConstructor& ctor) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) CVC4_PUBLIC; // INLINE FUNCTIONS @@ -543,11 +580,11 @@ inline DatatypeResolutionException::DatatypeResolutionException(std::string msg) Exception(msg) { } -inline Datatype::UnresolvedType::UnresolvedType(std::string name) : +inline DatatypeUnresolvedType::DatatypeUnresolvedType(std::string name) : d_name(name) { } -inline std::string Datatype::UnresolvedType::getName() const throw() { +inline std::string DatatypeUnresolvedType::getName() const throw() { return d_name; } @@ -618,15 +655,15 @@ inline Datatype::const_iterator Datatype::end() const throw() { return d_constructors.end(); } -inline bool Datatype::Constructor::isResolved() const throw() { +inline bool DatatypeConstructor::isResolved() const throw() { return !d_tester.isNull(); } -inline size_t Datatype::Constructor::getNumArgs() const throw() { +inline size_t DatatypeConstructor::getNumArgs() const throw() { return d_args.size(); } -inline bool Datatype::Constructor::Arg::isResolved() const throw() { +inline bool DatatypeConstructorArg::isResolved() const throw() { // We could just write: // // return !d_selector.isNull() && d_selector.getType().isSelector(); @@ -643,19 +680,19 @@ inline bool Datatype::Constructor::Arg::isResolved() const throw() { return d_resolved; } -inline Datatype::Constructor::iterator Datatype::Constructor::begin() throw() { +inline DatatypeConstructor::iterator DatatypeConstructor::begin() throw() { return d_args.begin(); } -inline Datatype::Constructor::iterator Datatype::Constructor::end() throw() { +inline DatatypeConstructor::iterator DatatypeConstructor::end() throw() { return d_args.end(); } -inline Datatype::Constructor::const_iterator Datatype::Constructor::begin() const throw() { +inline DatatypeConstructor::const_iterator DatatypeConstructor::begin() const throw() { return d_args.begin(); } -inline Datatype::Constructor::const_iterator Datatype::Constructor::end() const throw() { +inline DatatypeConstructor::const_iterator DatatypeConstructor::end() const throw() { return d_args.end(); } diff --git a/src/util/datatype.i b/src/util/datatype.i index 34e890214..056c15004 100644 --- a/src/util/datatype.i +++ b/src/util/datatype.i @@ -2,15 +2,10 @@ #include "util/datatype.h" %} -namespace CVC4 { -%rename(DatatypeConstructor) CVC4::Datatype::Constructor; -%rename(DatatypeConstructor) CVC4::Constructor; -} - %extend std::vector< CVC4::Datatype > { /* These member functions have slightly different signatures in * different swig language packages. The underlying issue is that - * Datatype::Constructor doesn't have a default constructor */ + * DatatypeConstructor doesn't have a default constructor */ %ignore vector(unsigned int size = 0);// ocaml %ignore set( int i, const CVC4::Datatype &x );// ocaml %ignore to_array();// ocaml @@ -19,17 +14,17 @@ namespace CVC4 { }; %template(vectorDatatype) std::vector< CVC4::Datatype >; -%extend std::vector< CVC4::Datatype::Constructor > { +%extend std::vector< CVC4::DatatypeConstructor > { /* These member functions have slightly different signatures in * different swig language packages. The underlying issue is that - * Datatype::Constructor doesn't have a default constructor */ + * DatatypeConstructor doesn't have a default constructor */ %ignore vector(unsigned int size = 0);// ocaml - %ignore set( int i, const CVC4::Datatype::Constructor &x );// ocaml + %ignore set( int i, const CVC4::DatatypeConstructor &x );// ocaml %ignore to_array();// ocaml %ignore vector(size_type);// java/python %ignore resize(size_type);// java/python }; -%template(vectorDatatypeConstructor) std::vector< CVC4::Datatype::Constructor >; +%template(vectorDatatypeConstructor) std::vector< CVC4::DatatypeConstructor >; %rename(equals) CVC4::Datatype::operator==(const Datatype&) const; %ignore CVC4::Datatype::operator!=(const Datatype&) const; @@ -41,234 +36,20 @@ namespace CVC4 { %rename(apply) CVC4::DatatypeHashFunction::operator()(const Datatype&) const; %ignore CVC4::DatatypeHashFunction::operator()(const Datatype*) const; -%rename(apply) CVC4::DatatypeHashFunction::operator()(const Datatype::Constructor&) const; -%ignore CVC4::DatatypeHashFunction::operator()(const Datatype::Constructor*) const; +%rename(apply) CVC4::DatatypeHashFunction::operator()(const DatatypeConstructor&) const; +%ignore CVC4::DatatypeHashFunction::operator()(const DatatypeConstructor*) const; -%rename(beginConst) CVC4::Constructor::begin() const; -%rename(endConst) CVC4::Constructor::end() const; +%rename(beginConst) CVC4::DatatypeConstructor::begin() const; +%rename(endConst) CVC4::DatatypeConstructor::end() const; -%rename(getArg) CVC4::Constructor::operator[](size_t) const; +%rename(getArg) CVC4::DatatypeConstructor::operator[](size_t) const; %ignore CVC4::operator<<(std::ostream&, const Datatype&); -%ignore CVC4::operator<<(std::ostream&, const Datatype::Constructor&); -%ignore CVC4::operator<<(std::ostream&, const Datatype::Constructor::Arg&); +%ignore CVC4::operator<<(std::ostream&, const DatatypeConstructor&); +%ignore CVC4::operator<<(std::ostream&, const DatatypeConstructorArg&); -%feature("valuewrapper") CVC4::Datatype::UnresolvedType; -%feature("valuewrapper") CVC4::Datatype::Constructor; +%feature("valuewrapper") CVC4::DatatypeUnresolvedType; +%feature("valuewrapper") CVC4::DatatypeConstructor; %include "util/datatype.h" -namespace CVC4 { - class CVC4_PUBLIC Arg { - - std::string d_name; - Expr d_selector; - /** the constructor associated with this selector */ - Expr d_constructor; - bool d_resolved; - - explicit Arg(std::string name, Expr selector); - friend class Constructor; - friend class Datatype; - - bool isUnresolvedSelf() const throw(); - - public: - - /** Get the name of this constructor argument. */ - std::string getName() const throw(); - - /** - * Get the selector for this constructor argument; this call is - * only permitted after resolution. - */ - Expr getSelector() const; - - /** - * Get the associated constructor for this constructor argument; - * this call is only permitted after resolution. - */ - Expr getConstructor() const; - - /** - * Get the selector for this constructor argument; this call is - * only permitted after resolution. - */ - Type getSelectorType() const; - - /** - * Get the name of the type of this constructor argument - * (Datatype field). Can be used for not-yet-resolved Datatypes - * (in which case the name of the unresolved type, or "[self]" - * for a self-referential type is returned). - */ - std::string getSelectorTypeName() const; - - /** - * Returns true iff this constructor argument has been resolved. - */ - bool isResolved() const throw(); - - };/* class Datatype::Constructor::Arg */ - - class Constructor { - public: - - /** The type for iterators over constructor arguments. */ - typedef std::vector::iterator iterator; - /** The (const) type for iterators over constructor arguments. */ - typedef std::vector::const_iterator const_iterator; - - private: - - std::string d_name; - Expr d_constructor; - Expr d_tester; - std::vector d_args; - - void 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) - throw(AssertionException, DatatypeResolutionException); - friend class Datatype; - - /** @FIXME document this! */ - Type doParametricSubstitution(Type range, - const std::vector< SortConstructorType >& paramTypes, - const std::vector< DatatypeType >& paramReplacements); - public: - /** - * Create a new Datatype constructor with the given name for the - * constructor and the given name for the tester. The actual - * constructor and tester aren't created until resolution time. - */ - explicit Constructor(std::string name, std::string tester); - - /** - * Add an argument (i.e., a data field) of the given name and type - * to this Datatype constructor. - */ - void addArg(std::string selectorName, Type selectorType); - - /** - * Add an argument (i.e., a data field) of the given name to this - * Datatype constructor that refers to an as-yet-unresolved - * Datatype (which may be mutually-recursive). - */ - void addArg(std::string selectorName, Datatype::UnresolvedType selectorType); - - /** - * Add a self-referential (i.e., a data field) of the given name - * to this Datatype constructor that refers to the enclosing - * Datatype. For example, using the familiar "nat" Datatype, to - * create the "pred" field for "succ" constructor, one uses - * succ::addArg("pred", Datatype::SelfType())---the actual Type - * cannot be passed because the Datatype is still under - * construction. - * - * This is a special case of - * Constructor::addArg(std::string, Datatype::UnresolvedType). - */ - void addArg(std::string selectorName, Datatype::SelfType); - - /** Get the name of this Datatype constructor. */ - std::string getName() const throw(); - /** - * Get the constructor operator of this Datatype constructor. The - * Datatype must be resolved. - */ - Expr getConstructor() const; - /** - * Get the tester operator of this Datatype constructor. The - * Datatype must be resolved. - */ - Expr getTester() const; - /** - * Get the number of arguments (so far) of this Datatype constructor. - */ - inline size_t getNumArgs() const throw(); - - /** - * Get the specialized constructor type for a parametric - * constructor; this call is only permitted after resolution. - */ - Type getSpecializedConstructorType(Type returnType) const; - - /** - * Return the cardinality of this constructor (the product of the - * cardinalities of its arguments). - */ - Cardinality getCardinality() const throw(AssertionException); - - /** - * Return true iff this constructor is finite (it is nullary or - * each of its argument types are finite). This function can - * only be called for resolved constructors. - */ - bool isFinite() const throw(AssertionException); - - /** - * Return true iff this constructor is well-founded (there exist - * ground terms). The constructor must be resolved or an - * exception is thrown. - */ - bool isWellFounded() const throw(AssertionException); - - /** - * Construct and return a ground term of this constructor. The - * constructor must be both resolved and well-founded, or else an - * exception is thrown. - */ - Expr mkGroundTerm( Type t ) const throw(AssertionException); - - /** - * Returns true iff this Datatype constructor has already been - * resolved. - */ - inline bool isResolved() const throw(); - - /** Get the beginning iterator over Constructor args. */ - inline iterator begin() throw(); - /** Get the ending iterator over Constructor args. */ - inline iterator end() throw(); - /** Get the beginning const_iterator over Constructor args. */ - inline const_iterator begin() const throw(); - /** Get the ending const_iterator over Constructor args. */ - inline const_iterator end() const throw(); - - /** Get the ith Constructor arg. */ - const Arg& operator[](size_t index) const; - - };/* class Datatype::Constructor */ - - class SelfType { - };/* class Datatype::SelfType */ - - /** - * An unresolved type (used in calls to - * Datatype::Constructor::addArg()) to allow a Datatype to refer to - * itself or to other mutually-recursive Datatypes. Unresolved-type - * fields of Datatypes will be properly typed when a Type is created - * for the Datatype by the ExprManager (which calls - * Datatype::resolve()). - */ - class UnresolvedType { - std::string d_name; - public: - inline UnresolvedType(std::string name); - inline std::string getName() const throw(); - };/* class Datatype::UnresolvedType */ -} - -%{ -namespace CVC4 { -typedef Datatype::Constructor Constructor; -typedef Datatype::Constructor::Arg Arg; -typedef Datatype::SelfType SelfType; -typedef Datatype::UnresolvedType UnresolvedType; -} -%} - diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h index 6d5584924..6c449233c 100644 --- a/test/unit/util/datatype_black.h +++ b/test/unit/util/datatype_black.h @@ -46,10 +46,10 @@ public: void testEnumeration() { Datatype colors("colors"); - Datatype::Constructor yellow("yellow", "is_yellow"); - Datatype::Constructor blue("blue", "is_blue"); - Datatype::Constructor green("green", "is_green"); - Datatype::Constructor red("red", "is_red"); + DatatypeConstructor yellow("yellow", "is_yellow"); + DatatypeConstructor blue("blue", "is_blue"); + DatatypeConstructor green("green", "is_green"); + DatatypeConstructor red("red", "is_red"); colors.addConstructor(yellow); colors.addConstructor(blue); @@ -92,11 +92,11 @@ public: void testNat() { Datatype nat("nat"); - Datatype::Constructor succ("succ", "is_succ"); - succ.addArg("pred", Datatype::SelfType()); + DatatypeConstructor succ("succ", "is_succ"); + succ.addArg("pred", DatatypeSelfType()); nat.addConstructor(succ); - Datatype::Constructor zero("zero", "is_zero"); + DatatypeConstructor zero("zero", "is_zero"); nat.addConstructor(zero); Debug("datatypes") << nat << std::endl; @@ -130,12 +130,12 @@ public: Datatype tree("tree"); Type integerType = d_em->integerType(); - Datatype::Constructor node("node", "is_node"); - node.addArg("left", Datatype::SelfType()); - node.addArg("right", Datatype::SelfType()); + DatatypeConstructor node("node", "is_node"); + node.addArg("left", DatatypeSelfType()); + node.addArg("right", DatatypeSelfType()); tree.addConstructor(node); - Datatype::Constructor leaf("leaf", "is_leaf"); + DatatypeConstructor leaf("leaf", "is_leaf"); leaf.addArg("leaf", integerType); tree.addConstructor(leaf); @@ -170,12 +170,12 @@ public: Datatype list("list"); Type integerType = d_em->integerType(); - Datatype::Constructor cons("cons", "is_cons"); + DatatypeConstructor cons("cons", "is_cons"); cons.addArg("car", integerType); - cons.addArg("cdr", Datatype::SelfType()); + cons.addArg("cdr", DatatypeSelfType()); list.addConstructor(cons); - Datatype::Constructor nil("nil", "is_nil"); + DatatypeConstructor nil("nil", "is_nil"); list.addConstructor(nil); Debug("datatypes") << list << std::endl; @@ -204,12 +204,12 @@ public: Datatype list("list"); Type realType = d_em->realType(); - Datatype::Constructor cons("cons", "is_cons"); + DatatypeConstructor cons("cons", "is_cons"); cons.addArg("car", realType); - cons.addArg("cdr", Datatype::SelfType()); + cons.addArg("cdr", DatatypeSelfType()); list.addConstructor(cons); - Datatype::Constructor nil("nil", "is_nil"); + DatatypeConstructor nil("nil", "is_nil"); list.addConstructor(nil); Debug("datatypes") << list << std::endl; @@ -238,12 +238,12 @@ public: Datatype list("list"); Type booleanType = d_em->booleanType(); - Datatype::Constructor cons("cons", "is_cons"); + DatatypeConstructor cons("cons", "is_cons"); cons.addArg("car", booleanType); - cons.addArg("cdr", Datatype::SelfType()); + cons.addArg("cdr", DatatypeSelfType()); list.addConstructor(cons); - Datatype::Constructor nil("nil", "is_nil"); + DatatypeConstructor nil("nil", "is_nil"); list.addConstructor(nil); Debug("datatypes") << list << std::endl; @@ -278,24 +278,24 @@ public: * END; */ Datatype tree("tree"); - Datatype::Constructor node("node", "is_node"); - node.addArg("left", Datatype::SelfType()); - node.addArg("right", Datatype::SelfType()); + DatatypeConstructor node("node", "is_node"); + node.addArg("left", DatatypeSelfType()); + node.addArg("right", DatatypeSelfType()); tree.addConstructor(node); - Datatype::Constructor leaf("leaf", "is_leaf"); - leaf.addArg("leaf", Datatype::UnresolvedType("list")); + DatatypeConstructor leaf("leaf", "is_leaf"); + leaf.addArg("leaf", DatatypeUnresolvedType("list")); tree.addConstructor(leaf); Debug("datatypes") << tree << std::endl; Datatype list("list"); - Datatype::Constructor cons("cons", "is_cons"); - cons.addArg("car", Datatype::UnresolvedType("tree")); - cons.addArg("cdr", Datatype::SelfType()); + DatatypeConstructor cons("cons", "is_cons"); + cons.addArg("car", DatatypeUnresolvedType("tree")); + cons.addArg("cdr", DatatypeSelfType()); list.addConstructor(cons); - Datatype::Constructor nil("nil", "is_nil"); + DatatypeConstructor nil("nil", "is_nil"); list.addConstructor(nil); Debug("datatypes") << list << std::endl; @@ -351,7 +351,7 @@ public: // add another constructor to list datatype resulting in an // "otherNil-list" - Datatype::Constructor otherNil("otherNil", "is_otherNil"); + DatatypeConstructor otherNil("otherNil", "is_otherNil"); dts[1].addConstructor(otherNil); // remake the types @@ -401,9 +401,9 @@ public: void testNotSoWellFounded() { Datatype tree("tree"); - Datatype::Constructor node("node", "is_node"); - node.addArg("left", Datatype::SelfType()); - node.addArg("right", Datatype::SelfType()); + DatatypeConstructor node("node", "is_node"); + node.addArg("left", DatatypeSelfType()); + node.addArg("right", DatatypeSelfType()); tree.addConstructor(node); Debug("datatypes") << tree << std::endl; -- 2.30.2