diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-11-16 03:47:25 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-11-16 03:47:25 +0000 |
commit | f55dfd4df98fbecbd0ef0f86da79d537457109d6 (patch) | |
tree | 8979e0e92e4d228d285c847f4af4913d4d8a7638 /src/expr | |
parent | b9118b75a8ee24a94a693cd3f850c63eb5085ef1 (diff) |
Addressed many of the concerns raised in the public interface review of CVC4 Datatypes (bug #283) by Chris Conway. Thanks, Chris!
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 8 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 2 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 4 | ||||
-rw-r--r-- | src/expr/node_manager.h | 2 |
4 files changed, 8 insertions, 8 deletions
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<TypeNode> 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); |