From 3ee48833fd8cffe897a05a986c08a30d9de57213 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Mon, 26 Apr 2010 21:37:34 +0000 Subject: [PATCH] Adding the intermediary TypeNode to represent (and separate) the Types at the Node level. --- src/expr/Makefile.am | 6 +- src/expr/attribute.cpp | 2 + src/expr/attribute.h | 17 +- src/expr/expr_manager_template.cpp | 32 +- src/expr/node.h | 20 +- src/expr/node_builder.h | 44 ++- src/expr/node_manager.h | 150 ++++++---- src/expr/node_value.h | 33 ++- src/expr/type.cpp | 36 +-- src/expr/type.h | 16 +- src/expr/type_node.cpp | 62 ++++ src/expr/type_node.h | 437 ++++++++++++++++++++++++++++ test/unit/expr/attribute_black.h | 14 +- test/unit/expr/attribute_white.h | 6 +- test/unit/expr/node_black.h | 14 +- test/unit/expr/node_builder_black.h | 4 +- test/unit/expr/node_manager_black.h | 72 ++--- test/unit/theory/theory_black.h | 4 +- test/unit/theory/theory_uf_white.h | 4 +- 19 files changed, 791 insertions(+), 182 deletions(-) create mode 100644 src/expr/type_node.cpp create mode 100644 src/expr/type_node.h diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 0abeebb9e..404334199 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -8,9 +8,12 @@ noinst_LTLIBRARIES = libexpr.la libexpr_la_SOURCES = \ node.h \ node.cpp \ + type_node.h \ + type_node.cpp \ node_builder.h \ @srcdir@/expr.h \ type.h \ + type.cpp \ node_value.h \ node_manager.h \ @srcdir@/expr_manager.h \ @@ -22,7 +25,6 @@ libexpr_la_SOURCES = \ @srcdir@/expr_manager.cpp \ node_value.cpp \ @srcdir@/expr.cpp \ - type.cpp \ command.h \ command.cpp \ declaration_scope.h \ @@ -36,6 +38,8 @@ EXTRA_DIST = \ @srcdir@/expr.h \ @srcdir@/expr_manager.cpp \ @srcdir@/expr.cpp \ + @srcdir@/type.h \ + @srcdir@/type.cpp \ kind_template.h \ metakind_template.h \ expr_manager_template.h \ diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index e5a50591f..bc724cdd1 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -30,6 +30,7 @@ void AttributeManager::deleteAllAttributes(NodeValue* nv) { deleteFromTable(d_ints, nv); deleteFromTable(d_tnodes, nv); deleteFromTable(d_nodes, nv); + deleteFromTable(d_types, nv); deleteFromTable(d_strings, nv); deleteFromTable(d_ptrs, nv); @@ -59,6 +60,7 @@ void AttributeManager::deleteAllAttributes() { deleteAllFromTable(d_ints); deleteAllFromTable(d_tnodes); deleteAllFromTable(d_nodes); + deleteAllFromTable(d_types); deleteAllFromTable(d_strings); deleteAllFromTable(d_ptrs); diff --git a/src/expr/attribute.h b/src/expr/attribute.h index 4250bb3ef..f231b701c 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -18,6 +18,7 @@ /* There are strong constraints on ordering of declarations of * attributes and nodes due to template use */ #include "expr/node.h" +#include "expr/type_node.h" #ifndef __CVC4__EXPR__ATTRIBUTE_H #define __CVC4__EXPR__ATTRIBUTE_H @@ -59,6 +60,8 @@ class AttributeManager { AttrHash d_tnodes; /** Underlying hash table for node-valued attributes */ AttrHash d_nodes; + /** Underlying hash table for types attributes */ + AttrHash d_types; /** Underlying hash table for string-valued attributes */ AttrHash d_strings; /** Underlying hash table for pointer-valued attributes */ @@ -241,6 +244,18 @@ struct getTable { } }; +/** Access the "d_types" member of AttributeManager. */ +template <> +struct getTable { + typedef AttrHash table_type; + static inline table_type& get(AttributeManager& am) { + return am.d_types; + } + static inline const table_type& get(const AttributeManager& am) { + return am.d_types; + } +}; + /** Access the "d_strings" member of AttributeManager. */ template <> struct getTable { @@ -313,7 +328,7 @@ struct getTable { } }; -/** Access the "d_nodes" member of AttributeManager. */ +/** Access the "d_cdnodes" member of AttributeManager. */ template <> struct getTable { typedef CDAttrHash table_type; diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 7407043d2..5d50dd100 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -48,12 +48,12 @@ ExprManager::~ExprManager() { BooleanType ExprManager::booleanType() const { NodeManagerScope nms(d_nodeManager); - return d_nodeManager->booleanType(); + return Type(d_nodeManager, new TypeNode(d_nodeManager->booleanType())); } KindType ExprManager::kindType() const { NodeManagerScope nms(d_nodeManager); - return d_nodeManager->kindType(); + return Type(d_nodeManager, new TypeNode(d_nodeManager->kindType())); } Expr ExprManager::mkExpr(Kind kind) { @@ -154,46 +154,58 @@ Expr ExprManager::mkExpr(Kind kind, const std::vector& children) { /** Make a function type from domain to range. */ FunctionType ExprManager::mkFunctionType(const Type& domain, const Type& range) { NodeManagerScope nms(d_nodeManager); - return d_nodeManager->mkFunctionType(domain, range); + return Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(*domain.d_typeNode, *range.d_typeNode))); } /** Make a function type with input types from argTypes. */ FunctionType ExprManager::mkFunctionType(const std::vector& argTypes, const Type& range) { Assert( argTypes.size() >= 1 ); NodeManagerScope nms(d_nodeManager); - return d_nodeManager->mkFunctionType(argTypes, range); + std::vector argTypeNodes; + for (unsigned i = 0, i_end = argTypes.size(); i < i_end; ++ i) { + argTypeNodes.push_back(*argTypes[i].d_typeNode); + } + return Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(argTypeNodes, *range.d_typeNode))); } FunctionType ExprManager::mkFunctionType(const std::vector& sorts) { Assert( sorts.size() >= 2 ); NodeManagerScope nms(d_nodeManager); - return d_nodeManager->mkFunctionType(sorts); + std::vector sortNodes; + for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) { + sortNodes.push_back(*sorts[i].d_typeNode); + } + return Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(sortNodes))); } FunctionType ExprManager::mkPredicateType(const std::vector& sorts) { Assert( sorts.size() >= 1 ); NodeManagerScope nms(d_nodeManager); - return d_nodeManager->mkPredicateType(sorts); + std::vector sortNodes; + for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) { + sortNodes.push_back(*sorts[i].d_typeNode); + } + return Type(d_nodeManager, new TypeNode(d_nodeManager->mkPredicateType(sortNodes))); } SortType ExprManager::mkSort(const std::string& name) { NodeManagerScope nms(d_nodeManager); - return d_nodeManager->mkSort(name); + return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name))); } Type ExprManager::getType(const Expr& e) { NodeManagerScope nms(d_nodeManager); - return d_nodeManager->getType(e.getNode()); + return Type(d_nodeManager, new TypeNode(d_nodeManager->getType(e.getNode()))); } Expr ExprManager::mkVar(const std::string& name, const Type& type) { NodeManagerScope nms(d_nodeManager); - return Expr(this, d_nodeManager->mkVarPtr(name, type)); + return Expr(this, d_nodeManager->mkVarPtr(name, *type.d_typeNode)); } Expr ExprManager::mkVar(const Type& type) { NodeManagerScope nms(d_nodeManager); - return Expr(this, d_nodeManager->mkVarPtr(type)); + return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode)); } unsigned ExprManager::minArity(Kind kind) { diff --git a/src/expr/node.h b/src/expr/node.h index 27756da5b..f8d9117c7 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -33,7 +33,7 @@ namespace CVC4 { -class Type; +class TypeNode; class NodeManager; template @@ -229,7 +229,7 @@ public: * Returns the unique id of this node * @return the ud */ - uint64_t getId() const { + unsigned getId() const { return d_nv->getId(); } @@ -247,7 +247,7 @@ public: * Returns the type of this node. * @return the type */ - Type getType() const; + TypeNode getType() const; /** * Returns the kind of this node. @@ -322,16 +322,16 @@ public: const typename AttrKind::value_type& value); /** Iterator allowing for scanning through the children. */ - typedef typename expr::NodeValue::iterator iterator; + typedef typename expr::NodeValue::iterator< NodeTemplate > iterator; /** Constant iterator allowing for scanning through the children. */ - typedef typename expr::NodeValue::iterator const_iterator; + typedef typename expr::NodeValue::iterator< NodeTemplate > const_iterator; /** * Returns the iterator pointing to the first child. * @return the iterator */ inline iterator begin() { - return d_nv->begin(); + return d_nv->begin< NodeTemplate >(); } /** @@ -340,7 +340,7 @@ public: * @return the end of the children iterator. */ inline iterator end() { - return d_nv->end(); + return d_nv->end< NodeTemplate >(); } /** @@ -348,7 +348,7 @@ public: * @return the const_iterator */ inline const_iterator begin() const { - return d_nv->begin(); + return d_nv->begin< NodeTemplate >(); } /** @@ -357,7 +357,7 @@ public: * @return the end of the children const_iterator. */ inline const_iterator end() const { - return d_nv->end(); + return d_nv->end< NodeTemplate >(); } /** @@ -814,7 +814,7 @@ inline bool NodeTemplate::hasOperator() const { } template -Type NodeTemplate::getType() const { +TypeNode NodeTemplate::getType() const { Assert( NodeManager::currentNM() != NULL, "There is no current CVC4::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?" ); diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 09e72660e..cefeb2fe2 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -173,6 +173,7 @@ /* strong dependency; make sure node is included first */ #include "node.h" +#include "type_node.h" #ifndef __CVC4__NODE_BUILDER_H #define __CVC4__NODE_BUILDER_H @@ -410,21 +411,21 @@ public: // override this in a derived class. inline ~NodeBuilderBase(); - typedef expr::NodeValue::iterator iterator; - typedef expr::NodeValue::iterator const_iterator; + typedef expr::NodeValue::iterator< NodeTemplate > iterator; + typedef expr::NodeValue::iterator< NodeTemplate > const_iterator; /** Get the begin-const-iterator of this Node-under-construction. */ inline const_iterator begin() const { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); - return d_nv->begin(); + return d_nv->begin< NodeTemplate >(); } /** Get the end-const-iterator of this Node-under-construction. */ inline const_iterator end() const { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); - return d_nv->end(); + return d_nv->end< NodeTemplate >(); } /** Get the kind of this Node-under-construction. */ @@ -505,6 +506,14 @@ public: return append(n); } + /** Append a sequence of children to this TypeNode-under-construction. */ + inline Builder& + append(const std::vector& children) { + Assert(!isUsed(), "NodeBuilder is one-shot only; " + "attempt to access it after conversion"); + return append(children.begin(), children.end()); + } + /** Append a sequence of children to this Node-under-construction. */ template inline Builder& @@ -537,6 +546,18 @@ public: return static_cast(*this); } + /** Append a child to this Node-under-construction. */ + Builder& append(const TypeNode& typeNode) { + Assert(!isUsed(), "NodeBuilder is one-shot only; " + "attempt to access it after conversion"); + Assert(!typeNode.isNull(), "Cannot use NULL Node as a child of a Node"); + allocateNvIfNecessaryForAppend(); + expr::NodeValue* nv = typeNode.d_nv; + nv->inc(); + d_nv->d_children[d_nv->d_nchildren++] = nv; + return static_cast(*this); + } + private: /** Construct the node value out of the node builder */ @@ -553,6 +574,10 @@ public: Node* constructNodePtr(); Node* constructNodePtr() const; + /** Construction of the TypeNode out of the node builder */ + TypeNode constructTypeNode(); + TypeNode constructTypeNode() const; + // two versions, so we can support extraction from (const) // NodeBuilders which are temporaries appearing as rvalues operator Node(); @@ -1245,6 +1270,17 @@ void NodeBuilderBase::decrRefCounts() { d_inlineNv.d_nchildren = 0; } + +template +TypeNode NodeBuilderBase::constructTypeNode() { + return TypeNode(constructNV()); +} + +template +TypeNode NodeBuilderBase::constructTypeNode() const { + return TypeNode(constructNV()); +} + template Node NodeBuilderBase::constructNode() { return Node(constructNV()); diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 138a87493..cbfcdd110 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -20,6 +20,7 @@ /* circular dependency; force node.h first */ #include "expr/attribute.h" #include "expr/node.h" +#include "expr/type_node.h" #ifndef __CVC4__NODE_MANAGER_H #define __CVC4__NODE_MANAGER_H @@ -32,7 +33,6 @@ #include "expr/metakind.h" #include "expr/node_value.h" #include "context/context.h" -#include "expr/type.h" namespace CVC4 { @@ -206,7 +206,7 @@ class NodeManager { // NodeManager's attributes. These aren't exposed outside of this // class; use the getters. - typedef expr::Attribute TypeAttr; + typedef expr::Attribute TypeAttr; typedef expr::Attribute AtomicAttr; /** @@ -290,12 +290,13 @@ public: * lookup is done on the name. If you mkVar("a", type) and then * mkVar("a", type) again, you have two variables. */ - Node mkVar(const std::string& name, const Type& type); - Node* mkVarPtr(const std::string& name, const Type& type); + Node mkVar(const std::string& name, const TypeNode& type); + Node* mkVarPtr(const std::string& name, const TypeNode& type); /** Create a variable with the given type. */ - Node mkVar(const Type& type); - Node* mkVarPtr(const Type& type); + Node mkVar(const TypeNode& type); + Node* mkVarPtr(const TypeNode& type); + /** * Create a constant of type T. It will have the appropriate @@ -304,6 +305,19 @@ public: template Node mkConst(const T&); + template + TypeNode mkTypeConst(const T&); + + template + NodeClass mkConstInternal(const T&); + + /** Create a type-variable */ + TypeNode mkTypeVar(); + TypeNode mkTypeVar(const std::string& name); + + /** Create a node with no children. */ + TypeNode mkTypeNode(Kind kind, const std::vector& children); + /** * Determine whether Nodes of a particular Kind have operators. * @returns true if Nodes of Kind k have operators. @@ -433,10 +447,10 @@ public: const typename AttrKind::value_type& value); /** Get the (singleton) type for booleans. */ - inline BooleanType booleanType(); + inline TypeNode booleanType(); /** Get the (singleton) type for sorts. */ - inline KindType kindType(); + inline TypeNode kindType(); /** * Make a function type from domain to range. @@ -445,7 +459,7 @@ public: * @param range the range type * @returns the functional type domain -> range */ - inline Type mkFunctionType(const Type& domain, const Type& range); + inline TypeNode mkFunctionType(const TypeNode& domain, const TypeNode& range); /** * Make a function type with input types from @@ -455,7 +469,7 @@ public: * @param range the range type * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range */ - inline Type mkFunctionType(const std::vector& argTypes, const Type& range); + inline TypeNode mkFunctionType(const std::vector& argTypes, const TypeNode& range); /** * Make a function type with input types from @@ -463,7 +477,7 @@ public: * sorts[sorts.size()-1]. sorts must have * at least 2 elements. */ - inline Type mkFunctionType(const std::vector& sorts); + inline TypeNode mkFunctionType(const std::vector& sorts); /** * Make a predicate type with input types from @@ -471,18 +485,18 @@ public: * BOOLEAN. sorts must have at least one * element. */ - inline Type mkPredicateType(const std::vector& sorts); + inline TypeNode mkPredicateType(const std::vector& sorts); /** Make a new sort. */ - inline Type mkSort(); + inline TypeNode mkSort(); /** Make a new sort with the given name. */ - inline Type mkSort(const std::string& name); + inline TypeNode mkSort(const std::string& name); /** * Get the type for the given node. */ - inline Type getType(TNode n); + inline TypeNode getType(TNode n); /** * Returns true if this node is atomic (has no more Boolean structure) @@ -589,63 +603,64 @@ NodeManager::setAttribute(TNode n, const AttrKind&, /** Get the (singleton) type for booleans. */ -inline BooleanType NodeManager::booleanType() { - return Type(this, new Node(mkConst(BOOLEAN_TYPE))); +inline TypeNode NodeManager::booleanType() { + return TypeNode(mkTypeConst(BOOLEAN_TYPE)); } /** Get the (singleton) type for sorts. */ -inline KindType NodeManager::kindType() { - return Type(this, new Node(mkConst(KIND_TYPE))); +inline TypeNode NodeManager::kindType() { + return TypeNode(mkTypeConst(KIND_TYPE)); } -/** Make a function type from domain to range. - * TODO: Function types should be unique for this manager. */ -inline Type NodeManager::mkFunctionType(const Type& domain, const Type& range) { - return Type(this, mkNodePtr(kind::FUNCTION_TYPE, *domain.d_typeNode, *range.d_typeNode)); +/** Make a function type from domain to range. */ +inline TypeNode NodeManager::mkFunctionType(const TypeNode& domain, const TypeNode& range) { + std::vector sorts; + sorts.push_back(domain); + sorts.push_back(range); + return mkFunctionType(sorts); } -inline Type NodeManager::mkFunctionType(const std::vector& argTypes, const Type& range) { +inline TypeNode NodeManager::mkFunctionType(const std::vector& argTypes, const TypeNode& range) { Assert(argTypes.size() >= 1); - std::vector sorts(argTypes); + std::vector sorts(argTypes); sorts.push_back(range); return mkFunctionType(sorts); } - -inline Type -NodeManager::mkFunctionType(const std::vector& sorts) { +inline TypeNode +NodeManager::mkFunctionType(const std::vector& sorts) { Assert(sorts.size() >= 2); - std::vector sortNodes; + std::vector sortNodes; for (unsigned i = 0; i < sorts.size(); ++ i) { - sortNodes.push_back(*(sorts[i].d_typeNode)); + sortNodes.push_back(sorts[i]); } - return Type(this, mkNodePtr(kind::FUNCTION_TYPE, sortNodes)); + return mkTypeNode(kind::FUNCTION_TYPE, sortNodes); } -inline Type -NodeManager::mkPredicateType(const std::vector& sorts) { +inline TypeNode +NodeManager::mkPredicateType(const std::vector& sorts) { Assert(sorts.size() >= 1); - std::vector sortNodes; + std::vector sortNodes; for (unsigned i = 0; i < sorts.size(); ++ i) { - sortNodes.push_back(*(sorts[i].d_typeNode)); + sortNodes.push_back(sorts[i]); } - sortNodes.push_back(*(booleanType().d_typeNode)); - return Type(this, mkNodePtr(kind::FUNCTION_TYPE, sortNodes)); + sortNodes.push_back(booleanType()); + return mkTypeNode(kind::FUNCTION_TYPE, sortNodes); } -inline Type NodeManager::mkSort() { - return Type(this, mkVarPtr(kindType())); +inline TypeNode NodeManager::mkSort() { + return mkTypeVar(); } -inline Type NodeManager::mkSort(const std::string& name) { - return Type(this, mkVarPtr(name, kindType())); +inline TypeNode NodeManager::mkSort(const std::string& name) { + return mkTypeVar(name); } -inline Type NodeManager::getType(TNode n) { - Node* typeNode = new Node; - getAttribute(n, TypeAttr(), *typeNode); +inline TypeNode NodeManager::getType(TNode n) { + TypeNode typeNode; + getAttribute(n, TypeAttr(), typeNode); // TODO: Type computation - return Type(this, typeNode); + return typeNode; } inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const { @@ -815,34 +830,61 @@ inline Node* NodeManager::mkNodePtr(Kind kind, return NodeBuilder<>(this, kind).append(children).constructNodePtr(); } -inline Node NodeManager::mkVar(const std::string& name, const Type& type) { +// N-ary version for types +inline TypeNode NodeManager::mkTypeNode(Kind kind, const std::vector& children) { + return NodeBuilder<>(this, kind).append(children).constructTypeNode(); +} + + +inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type) { Node n = mkVar(type); n.setAttribute(expr::VarNameAttr(), name); return n; } -inline Node* NodeManager::mkVarPtr(const std::string& name, const Type& type) { +inline Node* NodeManager::mkVarPtr(const std::string& name, const TypeNode& type) { Node* n = mkVarPtr(type); n->setAttribute(expr::VarNameAttr(), name); return n; } -inline Node NodeManager::mkVar(const Type& type) { +inline Node NodeManager::mkVar(const TypeNode& type) { Node n = NodeBuilder<0>(this, kind::VARIABLE); - n.setAttribute(TypeAttr(), *type.d_typeNode); + n.setAttribute(TypeAttr(), type); return n; } -inline Node* NodeManager::mkVarPtr(const Type& type) { +inline TypeNode NodeManager::mkTypeVar(const std::string& name) { + TypeNode type = mkTypeVar(); + type.setAttribute(expr::VarNameAttr(), name); + return type; +} + +inline TypeNode NodeManager::mkTypeVar() { + TypeNode type = NodeBuilder<0>(this, kind::VARIABLE).constructTypeNode(); + return type; +} + +inline Node* NodeManager::mkVarPtr(const TypeNode& type) { Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr(); - n->setAttribute(TypeAttr(), *type.d_typeNode); + n->setAttribute(TypeAttr(), type); return n; } template Node NodeManager::mkConst(const T& val) { - // typedef typename kind::metakind::constantMap::OwningTheory theory_t; + return mkConstInternal(val); +} + +template +TypeNode NodeManager::mkTypeConst(const T& val) { + return mkConstInternal(val); +} + +template +NodeClass NodeManager::mkConstInternal(const T& val) { + // typedef typename kind::metakind::constantMap::OwningTheory theory_t; NVStorage<1> nvStorage; expr::NodeValue& nvStack = reinterpret_cast(nvStorage); @@ -855,7 +897,7 @@ Node NodeManager::mkConst(const T& val) { expr::NodeValue* nv = poolLookup(&nvStack); if(nv != NULL) { - return Node(nv); + return NodeClass(nv); } nv = (expr::NodeValue*) @@ -876,7 +918,7 @@ Node NodeManager::mkConst(const T& val) { Debug("gc") << "creating node value " << nv << " [" << nv->d_id << "]: " << *nv << "\n"; - return Node(nv); + return NodeClass(nv); } }/* CVC4 namespace */ diff --git a/src/expr/node_value.h b/src/expr/node_value.h index a998dd8e4..260a9daae 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -34,6 +34,7 @@ namespace CVC4 { template class NodeTemplate; +class TypeNode; template class NodeBuilderBase; template class NodeBuilder; class AndNodeBuilder; @@ -101,6 +102,7 @@ class NodeValue { // todo add exprMgr ref in debug case template friend class ::CVC4::NodeTemplate; + friend class ::CVC4::TypeNode; template friend class ::CVC4::NodeBuilderBase; template friend class ::CVC4::NodeBuilder; friend class ::CVC4::NodeManager; @@ -137,13 +139,13 @@ private: const_nv_iterator nv_begin() const; const_nv_iterator nv_end() const; - template + template class iterator { const_nv_iterator d_i; public: explicit iterator(const_nv_iterator i) : d_i(i) {} - inline CVC4::NodeTemplate operator*(); + inline T operator*(); bool operator==(const iterator& i) { return d_i == i.d_i; @@ -172,11 +174,11 @@ private: public: - template - inline iterator begin() const; + template + inline iterator begin() const; - template - inline iterator end() const; + template + inline iterator end() const; /** * Hash this NodeValue. For hash_maps, hash_sets, etc.. but this is @@ -317,18 +319,18 @@ inline NodeValue::const_nv_iterator NodeValue::nv_end() const { return d_children + d_nchildren; } -template -inline NodeValue::iterator NodeValue::begin() const { +template +inline NodeValue::iterator NodeValue::begin() const { NodeValue* const* firstChild = d_children; if(getMetaKind() == kind::metakind::PARAMETERIZED) { ++firstChild; } - return iterator(firstChild); + return iterator(firstChild); } -template -inline NodeValue::iterator NodeValue::end() const { - return iterator(d_children + d_nchildren); +template +inline NodeValue::iterator NodeValue::end() const { + return iterator(d_children + d_nchildren); } inline bool NodeValue::isBeingDeleted() const { @@ -349,13 +351,14 @@ inline NodeValue* NodeValue::getChild(int i) const { }/* CVC4 namespace */ #include "expr/node.h" +#include "expr/type_node.h" namespace CVC4 { namespace expr { -template -inline CVC4::NodeTemplate NodeValue::iterator::operator*() { - return NodeTemplate(*d_i); +template +inline T NodeValue::iterator::operator*() { + return T(*d_i); } inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv) { diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 63d270ac1..98a7e88e7 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -15,6 +15,7 @@ #include "expr/node_manager.h" #include "expr/type.h" +#include "expr/type_node.h" #include "expr/type_constant.h" #include "util/Assert.h" #include @@ -26,12 +27,12 @@ std::ostream& operator<<(std::ostream& out, const Type& e) { return out; } -Type Type::makeType(NodeTemplate typeNode) const +Type Type::makeType(const TypeNode& typeNode) const { - return Type(d_nodeManager, new Node(typeNode)); + return Type(d_nodeManager, new TypeNode(typeNode)); } -Type::Type(NodeManager* nm, NodeTemplate* node) +Type::Type(NodeManager* nm, TypeNode* node) : d_typeNode(node), d_nodeManager(nm) { @@ -43,19 +44,19 @@ Type::~Type() { } Type::Type() -: d_typeNode(new Node()), +: d_typeNode(new TypeNode()), d_nodeManager(NULL) { } Type::Type(uintptr_t n) -: d_typeNode(new Node()), +: d_typeNode(new TypeNode()), d_nodeManager(NULL) { AlwaysAssert(n == 0); } Type::Type(const Type& t) -: d_typeNode(new Node(*t.d_typeNode)), +: d_typeNode(new TypeNode(*t.d_typeNode)), d_nodeManager(t.d_nodeManager) { } @@ -95,8 +96,7 @@ void Type::toStream(std::ostream& out) const { /** Is this the Boolean type? */ bool Type::isBoolean() const { NodeManagerScope nms(d_nodeManager); - return d_typeNode->getKind() == kind::TYPE_CONSTANT - && d_typeNode->getConst() == BOOLEAN_TYPE; + return d_typeNode->isBoolean(); } /** Cast to a Boolean type */ @@ -109,14 +109,14 @@ Type::operator BooleanType() const { /** Is this a function type? */ bool Type::isFunction() const { NodeManagerScope nms(d_nodeManager); - return d_typeNode->getKind() == kind::FUNCTION_TYPE; + return d_typeNode->isFunction(); } /** Is this a predicate type? NOTE: all predicate types are also function types. */ bool Type::isPredicate() const { NodeManagerScope nms(d_nodeManager); - return isFunction() && ((FunctionType)*this).getRangeType().isBoolean(); + return d_typeNode->isPredicate(); } /** Cast to a function type */ @@ -129,8 +129,7 @@ Type::operator FunctionType() const { /** Is this a sort kind */ bool Type::isSort() const { NodeManagerScope nms(d_nodeManager); - return d_typeNode->getKind() == kind::VARIABLE && - d_typeNode->getType().isKind(); + return d_typeNode->isSort(); } /** Cast to a sort type */ @@ -143,8 +142,7 @@ Type::operator SortType() const { /** Is this a kind type (i.e., the type of a type)? */ bool Type::isKind() const { NodeManagerScope nms(d_nodeManager); - return d_typeNode->getKind() == kind::TYPE_CONSTANT - && d_typeNode->getConst() == KIND_TYPE; + return d_typeNode->isKind(); } /** Cast to a kind type */ @@ -157,15 +155,19 @@ Type::operator KindType() const { std::vector FunctionType::getArgTypes() const { NodeManagerScope nms(d_nodeManager); std::vector args; - for (unsigned i = 0, i_end = d_typeNode->getNumChildren() - 1; i < i_end; ++ i) { - args.push_back(makeType((*d_typeNode)[i])); + std::vector argNodes = d_typeNode->getArgTypes(); + std::vector::iterator it = argNodes.begin(); + std::vector::iterator it_end = argNodes.end(); + for(; it != it_end; ++ it) { + args.push_back(makeType(*it)); } return args; } Type FunctionType::getRangeType() const { NodeManagerScope nms(d_nodeManager); - return makeType((*d_typeNode)[d_typeNode->getNumChildren()-1]); + Assert(isFunction()); + return makeType(d_typeNode->getRangeType()); } void BooleanType::toStream(std::ostream& out) const { diff --git a/src/expr/type.h b/src/expr/type.h index 4f9142698..5cbe0613a 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -29,7 +29,7 @@ namespace CVC4 { class NodeManager; -template class NodeTemplate; +class TypeNode; class BooleanType; class FunctionType; @@ -41,12 +41,12 @@ class SortType; */ class CVC4_PUBLIC Type { - friend class NodeManager; + friend class ExprManager; protected: /** The internal expression representation */ - NodeTemplate* d_typeNode; + TypeNode* d_typeNode; /** The responsible expression manager */ NodeManager* d_nodeManager; @@ -54,14 +54,14 @@ protected: /** * Construct a new type given the typeNode; */ - Type makeType(NodeTemplate typeNode) const; + Type makeType(const TypeNode& typeNode) const; /** * Constructor for internal purposes. * @param em the expression manager that handles this expression * @param node the actual expression node pointer for this type */ - Type(NodeManager* em, NodeTemplate* typeNode); + Type(NodeManager* em, TypeNode* typeNode); public: @@ -160,12 +160,6 @@ public: /** Get the range type (i.e., the type of the result). */ Type getRangeType() const; - /** Is this as function type? (Returns true.) */ - bool isFunction() const; - - /** Is this as predicate type? (Returns true if range is Boolean.) */ - bool isPredicate() const; - /** * Outputs a string representation of this type to the stream, * in the format "D -> R" or "(A, B, C) -> R". diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp new file mode 100644 index 000000000..87b6ed58a --- /dev/null +++ b/src/expr/type_node.cpp @@ -0,0 +1,62 @@ +/********************* */ +/** node.cpp + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Reference-counted encapsulation of a pointer to node information. + **/ + +#include "expr/type_node.h" + +namespace CVC4 { + +TypeNode TypeNode::s_null(&expr::NodeValue::s_null); + +bool TypeNode::isBoolean() const { + return getKind() == kind::TYPE_CONSTANT && getConst() == BOOLEAN_TYPE; +} + +/** Is this a function type? */ +bool TypeNode::isFunction() const { + return getKind() == kind::FUNCTION_TYPE; +} + +/** Is this a predicate type? NOTE: all predicate types are also + function types. */ +bool TypeNode::isPredicate() const { + return isFunction() && getRangeType().isBoolean(); +} + +std::vector TypeNode::getArgTypes() const { + Assert(isFunction()); + std::vector args; + for (unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++ i) { + args.push_back((*this)[i]); + } + return args; +} + +TypeNode TypeNode::getRangeType() const { + Assert(isFunction()); + return (*this)[getNumChildren()-1]; +} + + +/** Is this a sort kind */ +bool TypeNode::isSort() const { + return getKind() == kind::VARIABLE; +} + +/** Is this a kind type (i.e., the type of a type)? */ +bool TypeNode::isKind() const { + return getKind() == kind::TYPE_CONSTANT && getConst() == KIND_TYPE; +} + +}/* CVC4 namespace */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h new file mode 100644 index 000000000..7747b93e1 --- /dev/null +++ b/src/expr/type_node.h @@ -0,0 +1,437 @@ +/********************* */ +/** type_node.h + ** Original author: dejan + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Reference-counted encapsulation of a pointer to node information. + **/ + +#include "cvc4_private.h" + +// circular dependency +#include "expr/node_value.h" + +#ifndef __CVC4__TYPE_NODE_H +#define __CVC4__TYPE_NODE_H + +#include +#include +#include +#include + +#include "expr/kind.h" +#include "expr/metakind.h" +#include "util/Assert.h" +#include "util/output.h" + +namespace CVC4 { + +class NodeManager; + +namespace expr { +class NodeValue; +}/* CVC4::expr namespace */ + +/** + * Encapsulation of an NodeValue pointer. The reference count is + * maintained in the NodeValue if ref_count is true. + */ +class TypeNode { + + /** + * The NodeValue has access to the private constructors, so that the + * iterators can can create new nodes. + */ + friend class expr::NodeValue; + + /** A convenient null-valued encapsulated pointer */ + static TypeNode s_null; + + /** The referenced NodeValue */ + expr::NodeValue* d_nv; + + /** + * This constructor is reserved for use by the TypeNode package. + */ + explicit TypeNode(const expr::NodeValue*); + + friend class NodeManager; + + template + friend class NodeBuilderBase; + + /** + * Assigns the expression value and does reference counting. No assumptions + * are made on the expression, and should only be used if we know what we + * are doing. + * + * @param ev the expression value to assign + */ + void assignNodeValue(expr::NodeValue* ev); + +public: + + /** Default constructor, makes a null expression. */ + TypeNode() : d_nv(&expr::NodeValue::s_null) { } + + /** Copy constructor */ + TypeNode(const TypeNode& node); + + /** + * Assignment operator for nodes, copies the relevant information from node + * to this node. + * @param node the node to copy + * @return reference to this node + */ + TypeNode& operator=(const TypeNode& typeNode); + + /** + * Destructor. If ref_count is true it will decrement the reference count + * and, if zero, collect the NodeValue. + */ + ~TypeNode() throw(AssertionException); + + /** + * Return the null node. + * @return the null node + */ + static TypeNode null() { + return s_null; + } + + /** + * Returns true if this type is a null type. + * @return true if null + */ + bool isNull() const { + return d_nv == &expr::NodeValue::s_null; + } + + /** + * Structural comparison operator for expressions. + * @param typeNode the type node to compare to + * @return true if expressions are equal, false otherwise + */ + bool operator==(const TypeNode& typeNode) const { + return d_nv == typeNode.d_nv; + } + + /** + * Structural comparison operator for expressions. + * @param typeNode the type node to compare to + * @return true if expressions are equal, false otherwise + */ + bool operator!=(const TypeNode& typeNode) const { + return d_nv != typeNode.d_nv; + } + + /** + * We compare by expression ids so, keeping things deterministic and having + * that subexpressions have to be smaller than the enclosing expressions. + * @param node the node to compare to + * @return true if this expression is smaller + */ + inline bool operator<(const TypeNode& typeNode) const { + return d_nv->d_id < typeNode.d_nv->d_id; + } + + /** + * Returns the i-th child of this node. + * @param i the index of the child + * @return the node representing the i-th child + */ + TypeNode operator[](int i) const { + return TypeNode(d_nv->getChild(i)); + } + + /** + * Returns the unique id of this node + * @return the id + */ + unsigned getId() const { + return d_nv->getId(); + } + + /** + * Returns the kind of this type node. + * @return the kind + */ + inline Kind getKind() const { + return Kind(d_nv->d_kind); + } + + /** + * Returns the metakind of this type node. + * @return the metakind + */ + inline kind::MetaKind getMetaKind() const { + return kind::metaKindOf(getKind()); + } + + /** + * Returns the number of children this node has. + * @return the number of children + */ + inline size_t getNumChildren() const; + + /** + * If this is a CONST_* TypeNode, extract the constant from it. + */ + template + inline const T& getConst() const; + + /** + * Returns the value of the given attribute that this has been attached. + * @param attKind the kind of the attribute + * @return the value of the attribute + */ + template + inline typename AttrKind::value_type getAttribute(const AttrKind& attKind) const; + + // Note that there are two, distinct hasAttribute() declarations for + // a reason (rather than using a pointer-valued argument with a + // default value): they permit more optimized code in the underlying + // hasAttribute() implementations. + + /** + * Returns true if this node has been associated an attribute of given kind. + * Additionaly, if a pointer to the value_kind is give, and the attribute + * value has been set for this node, it will be returned. + * @param attKind the kind of the attribute + * @return true if this node has the requested attribute + */ + template + inline bool hasAttribute(const AttrKind& attKind) const; + + /** + * Returns true if this node has been associated an attribute of given kind. + * Additionaly, if a pointer to the value_kind is give, and the attribute + * value has been set for this node, it will be returned. + * @param attKind the kind of the attribute + * @param value where to store the value if it exists + * @return true if this node has the requested attribute + */ + template + inline bool getAttribute(const AttrKind& attKind, + typename AttrKind::value_type& value) const; + + /** + * Sets the given attribute of this node to the given value. + * @param attKind the kind of the atribute + * @param value the value to set the attribute to + */ + template + inline void setAttribute(const AttrKind& attKind, + const typename AttrKind::value_type& value); + + /** Iterator allowing for scanning through the children. */ + typedef expr::NodeValue::iterator iterator; + /** Constant iterator allowing for scanning through the children. */ + typedef expr::NodeValue::iterator const_iterator; + + /** + * Returns the iterator pointing to the first child. + * @return the iterator + */ + inline iterator begin() { + return d_nv->begin(); + } + + /** + * Returns the iterator pointing to the end of the children (one beyond the + * last one. + * @return the end of the children iterator. + */ + inline iterator end() { + return d_nv->end(); + } + + /** + * Returns the const_iterator pointing to the first child. + * @return the const_iterator + */ + inline const_iterator begin() const { + return d_nv->begin(); + } + + /** + * Returns the const_iterator pointing to the end of the children (one + * beyond the last one. + * @return the end of the children const_iterator. + */ + inline const_iterator end() const { + return d_nv->end(); + } + + /** + * Converts this node into a string representation. + * @return the string representation of this node. + */ + inline std::string toString() const { + return d_nv->toString(); + } + + /** + * Converst this node into a string representation and sends it to the + * given stream + * @param out the sream to serialise this node to + */ + inline void toStream(std::ostream& out, int toDepth = -1) const { + d_nv->toStream(out, toDepth); + } + + /** + * Very basic pretty printer for Node. + * @param o output stream to print to. + * @param indent number of spaces to indent the formula by. + */ + void printAst(std::ostream & o, int indent = 0) const; + + /** Is this the Boolean type? */ + bool isBoolean() const; + + /** Is this a function type? */ + bool isFunction() const; + + /** Get the argument types */ + std::vector getArgTypes() const; + + /** Get the range type (i.e., the type of the result). */ + TypeNode getRangeType() const; + + /** Is this a predicate type? NOTE: all predicate types are also + function types. */ + bool isPredicate() const; + + /** Is this a sort kind */ + bool isSort() const; + + /** Is this a kind type (i.e., the type of a type)? */ + bool isKind() const; + +private: + + /** + * Indents the given stream a given amount of spaces. + * @param out the stream to indent + * @param indent the numer of spaces + */ + static void indent(std::ostream& out, int indent) { + for(int i = 0; i < indent; i++) { + out << ' '; + } + } + +};/* class TypeNode */ + +/** + * Serializes a given node to the given stream. + * @param out the output stream to use + * @param node the node to output to the stream + * @return the changed stream. + */ +inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) { + n.toStream(out, Node::setdepth::getDepth(out)); + return out; +} + +}/* CVC4 namespace */ + +#include + +#include "expr/node_manager.h" + +namespace CVC4 { + +// for hash_maps, hash_sets.. +struct TypeNodeHashFunction { + size_t operator()(const CVC4::TypeNode& node) const { + return (size_t) node.getId(); + } +}; + +inline size_t TypeNode::getNumChildren() const { + return d_nv->getNumChildren(); +} + +template +inline const T& TypeNode::getConst() const { + return d_nv->getConst(); +} + +inline TypeNode::TypeNode(const expr::NodeValue* ev) : + d_nv(const_cast (ev)) { + Assert(d_nv != NULL, "Expecting a non-NULL expression value!"); + d_nv->inc(); +} + +inline TypeNode::TypeNode(const TypeNode& typeNode) { + Assert(typeNode.d_nv != NULL, "Expecting a non-NULL expression value!"); + d_nv = typeNode.d_nv; + d_nv->inc(); +} + +inline TypeNode::~TypeNode() throw(AssertionException) { + Assert(d_nv != NULL, "Expecting a non-NULL expression value!"); + d_nv->dec(); +} + +inline void TypeNode::assignNodeValue(expr::NodeValue* ev) { + d_nv = ev; + d_nv->inc(); +} + +inline TypeNode& TypeNode::operator=(const TypeNode& typeNode) { + Assert(d_nv != NULL, "Expecting a non-NULL expression value!"); + Assert(typeNode.d_nv != NULL, "Expecting a non-NULL expression value on RHS!"); + if(EXPECT_TRUE( d_nv != typeNode.d_nv )) { + d_nv->dec(); + d_nv = typeNode.d_nv; + d_nv->inc(); + } + return *this; +} + +template +inline typename AttrKind::value_type TypeNode:: +getAttribute(const AttrKind&) const { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + return NodeManager::currentNM()->getAttribute(d_nv, AttrKind()); +} + +template +inline bool TypeNode:: +hasAttribute(const AttrKind&) const { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + return NodeManager::currentNM()->hasAttribute(d_nv, AttrKind()); +} + +template +inline bool TypeNode::getAttribute(const AttrKind&, typename AttrKind::value_type& ret) const { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + return NodeManager::currentNM()->getAttribute(d_nv, AttrKind(), ret); +} + +template +inline void TypeNode:: +setAttribute(const AttrKind&, const typename AttrKind::value_type& value) { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + NodeManager::currentNM()->setAttribute(d_nv, AttrKind(), value); +} + +}/* CVC4 namespace */ + +#endif /* __CVC4__NODE_H */ diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h index d0be9a351..7894743d6 100644 --- a/test/unit/expr/attribute_black.h +++ b/test/unit/expr/attribute_black.h @@ -70,7 +70,7 @@ public: typedef expr::Attribute MyDataAttribute; void testDeallocation() { - Type booleanType = d_nodeManager->booleanType(); + TypeNode booleanType = d_nodeManager->booleanType(); Node* node = new Node(d_nodeManager->mkVar(booleanType)); MyData* data; MyData* data1; @@ -88,7 +88,7 @@ public: typedef expr::Attribute PrimitiveIntAttribute; typedef expr::CDAttribute CDPrimitiveIntAttribute; void testInts(){ - BooleanType booleanType = d_nodeManager->booleanType(); + TypeNode booleanType = d_nodeManager->booleanType(); Node* node = new Node(d_nodeManager->mkVar(booleanType)); const uint64_t val = 63489; uint64_t data0 = 0; @@ -116,7 +116,7 @@ public: typedef expr::Attribute TNodeAttribute; typedef expr::CDAttribute CDTNodeAttribute; void testTNodes(){ - BooleanType booleanType = d_nodeManager->booleanType(); + TypeNode booleanType = d_nodeManager->booleanType(); Node* node = new Node(d_nodeManager->mkVar(booleanType)); Node val(d_nodeManager->mkVar(booleanType)); @@ -151,7 +151,7 @@ public: typedef expr::Attribute PtrAttribute; typedef expr::CDAttribute CDPtrAttribute; void testPtrs(){ - BooleanType booleanType = d_nodeManager->booleanType(); + TypeNode booleanType = d_nodeManager->booleanType(); Node* node = new Node(d_nodeManager->mkVar(booleanType)); Foo* val = new Foo(63489); @@ -182,7 +182,7 @@ public: typedef expr::Attribute ConstPtrAttribute; typedef expr::CDAttribute CDConstPtrAttribute; void testConstPtrs(){ - BooleanType booleanType = d_nodeManager->booleanType(); + TypeNode booleanType = d_nodeManager->booleanType(); Node* node = new Node(d_nodeManager->mkVar(booleanType)); const Foo* val = new Foo(63489); @@ -212,7 +212,7 @@ public: typedef expr::Attribute StringAttribute; typedef expr::CDAttribute CDStringAttribute; void testStrings(){ - BooleanType booleanType = d_nodeManager->booleanType(); + TypeNode booleanType = d_nodeManager->booleanType(); Node* node = new Node(d_nodeManager->mkVar(booleanType)); std::string val("63489"); @@ -241,7 +241,7 @@ public: typedef expr::Attribute BoolAttribute; typedef expr::CDAttribute CDBoolAttribute; void testBools(){ - BooleanType booleanType = d_nodeManager->booleanType(); + TypeNode booleanType = d_nodeManager->booleanType(); Node* node = new Node(d_nodeManager->mkVar(booleanType)); bool val = true; diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index bfe0ef3cf..43bcc7fe3 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -60,7 +60,7 @@ class AttributeWhite : public CxxTest::TestSuite { Context* d_ctxt; NodeManager* d_nm; NodeManagerScope* d_scope; - Type* d_booleanType; + TypeNode* d_booleanType; public: @@ -69,7 +69,7 @@ public: d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); - d_booleanType = new Type(d_nm->booleanType()); + d_booleanType = new TypeNode(d_nm->booleanType()); } void tearDown() { @@ -146,7 +146,7 @@ public: lastId = attr::LastAttributeId::s_id; TS_ASSERT_LESS_THAN(theory::RewriteCache::s_id, lastId); - lastId = attr::LastAttributeId::s_id; + lastId = attr::LastAttributeId::s_id; TS_ASSERT_LESS_THAN(NodeManager::TypeAttr::s_id, lastId); } diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 6469806d6..7e034036a 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -36,7 +36,7 @@ private: Context* d_ctxt; NodeManager* d_nodeManager; NodeManagerScope* d_scope; - Type *d_booleanType; + TypeNode *d_booleanType; public: @@ -44,7 +44,7 @@ public: d_ctxt = new Context; d_nodeManager = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nodeManager); - d_booleanType = new Type(d_nodeManager->booleanType()); + d_booleanType = new TypeNode(d_nodeManager->booleanType()); } void tearDown() { @@ -400,9 +400,9 @@ public: } void testGetOperator() { - Type sort = d_nodeManager->mkSort("T"); - Type booleanType = d_nodeManager->booleanType(); - Type predType = d_nodeManager->mkFunctionType(sort, booleanType); + TypeNode sort = d_nodeManager->mkSort("T"); + TypeNode booleanType = d_nodeManager->booleanType(); + TypeNode predType = d_nodeManager->mkFunctionType(sort, booleanType); Node f = d_nodeManager->mkVar(predType); Node a = d_nodeManager->mkVar(booleanType); @@ -490,7 +490,7 @@ public: } void testToString() { - Type booleanType = d_nodeManager->booleanType(); + TypeNode booleanType = d_nodeManager->booleanType(); Node w = d_nodeManager->mkVar("w",booleanType); Node x = d_nodeManager->mkVar("x",booleanType); @@ -503,7 +503,7 @@ public: } void testToStream() { - Type booleanType = d_nodeManager->booleanType(); + TypeNode booleanType = d_nodeManager->booleanType(); Node w = d_nodeManager->mkVar("w",booleanType); Node x = d_nodeManager->mkVar("x",booleanType); diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index 17e1d6f18..a1887118c 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -37,7 +37,7 @@ private: Context* d_ctxt; NodeManager* d_nm; NodeManagerScope* d_scope; - Type* d_booleanType; + TypeNode* d_booleanType; public: @@ -47,7 +47,7 @@ public: d_scope = new NodeManagerScope(d_nm); specKind = PLUS; - d_booleanType = new Type(d_nm->booleanType()); + d_booleanType = new TypeNode(d_nm->booleanType()); } void tearDown() { diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h index 118ba8173..0e1e09178 100644 --- a/test/unit/expr/node_manager_black.h +++ b/test/unit/expr/node_manager_black.h @@ -142,7 +142,7 @@ public: } void testMkVarWithNoName() { - Type booleanType = d_nodeManager->booleanType(); + TypeNode booleanType = d_nodeManager->booleanType(); Node x = d_nodeManager->mkVar(booleanType); TS_ASSERT_EQUALS(x.getKind(),VARIABLE); TS_ASSERT_EQUALS(x.getNumChildren(),0u); @@ -150,7 +150,7 @@ public: } void testMkVarWithName() { - Type booleanType = d_nodeManager->booleanType(); + TypeNode booleanType = d_nodeManager->booleanType(); Node x = d_nodeManager->mkVar("x", booleanType); TS_ASSERT_EQUALS(x.getKind(),VARIABLE); TS_ASSERT_EQUALS(x.getNumChildren(),0u); @@ -187,9 +187,9 @@ public: } void testBooleanType() { - Type t = d_nodeManager->booleanType(); - Type t2 = d_nodeManager->booleanType(); - Type t3 = d_nodeManager->mkSort("T"); + TypeNode t = d_nodeManager->booleanType(); + TypeNode t2 = d_nodeManager->booleanType(); + TypeNode t3 = d_nodeManager->mkSort("T"); TS_ASSERT( t.isBoolean() ); TS_ASSERT( !t.isFunction() ); TS_ASSERT( !t.isKind() ); @@ -199,14 +199,14 @@ public: TS_ASSERT_EQUALS(t, t2); TS_ASSERT( t != t3 ); - BooleanType bt = t; + TypeNode bt = t; TS_ASSERT_EQUALS( bt, t); } void testKindType() { - Type t = d_nodeManager->kindType(); - Type t2 = d_nodeManager->kindType(); - Type t3 = d_nodeManager->mkSort("T"); + TypeNode t = d_nodeManager->kindType(); + TypeNode t2 = d_nodeManager->kindType(); + TypeNode t3 = d_nodeManager->mkSort("T"); TS_ASSERT( !t.isBoolean() ); TS_ASSERT( !t.isFunction() ); @@ -218,15 +218,15 @@ public: TS_ASSERT_EQUALS(t, t2); TS_ASSERT( t != t3); - KindType kt = t; + TypeNode kt = t; TS_ASSERT_EQUALS( kt, t ); // TODO: Is there a way to get the type of otherType (it should == t)? } void testMkFunctionTypeBoolToBool() { - Type booleanType = d_nodeManager->booleanType(); - Type t = d_nodeManager->mkFunctionType(booleanType,booleanType); - Type t2 = d_nodeManager->mkFunctionType(booleanType,booleanType); + TypeNode booleanType = d_nodeManager->booleanType(); + TypeNode t = d_nodeManager->mkFunctionType(booleanType,booleanType); + TypeNode t2 = d_nodeManager->mkFunctionType(booleanType,booleanType); TS_ASSERT( !t.isBoolean() ); TS_ASSERT( t.isFunction() ); @@ -237,7 +237,7 @@ public: TS_ASSERT_EQUALS( t, t2 ); - FunctionType ft = t; + TypeNode ft = t; TS_ASSERT_EQUALS( ft, t ); TS_ASSERT_EQUALS(ft.getArgTypes().size(), 1u); TS_ASSERT_EQUALS(ft.getArgTypes()[0], booleanType); @@ -246,16 +246,16 @@ public: } void testMkFunctionTypeVectorOfArgsWithReturnType() { - Type a = d_nodeManager->mkSort(); - Type b = d_nodeManager->mkSort(); - Type c = d_nodeManager->mkSort(); + TypeNode a = d_nodeManager->mkSort(); + TypeNode b = d_nodeManager->mkSort(); + TypeNode c = d_nodeManager->mkSort(); - std::vector argTypes; + std::vector argTypes; argTypes.push_back(a); argTypes.push_back(b); - Type t = d_nodeManager->mkFunctionType(argTypes,c); - Type t2 = d_nodeManager->mkFunctionType(argTypes,c); + TypeNode t = d_nodeManager->mkFunctionType(argTypes,c); + TypeNode t2 = d_nodeManager->mkFunctionType(argTypes,c); TS_ASSERT( !t.isBoolean() ); TS_ASSERT( t.isFunction() ); @@ -266,7 +266,7 @@ public: TS_ASSERT_EQUALS( t, t2 ); - FunctionType ft = t; + TypeNode ft = t; TS_ASSERT_EQUALS( ft, t ); TS_ASSERT_EQUALS(ft.getArgTypes().size(), argTypes.size()); TS_ASSERT_EQUALS(ft.getArgTypes()[0], a); @@ -276,17 +276,17 @@ public: } void testMkFunctionTypeVectorOfArguments() { - Type a = d_nodeManager->mkSort(); - Type b = d_nodeManager->mkSort(); - Type c = d_nodeManager->mkSort(); + TypeNode a = d_nodeManager->mkSort(); + TypeNode b = d_nodeManager->mkSort(); + TypeNode c = d_nodeManager->mkSort(); - std::vector types; + std::vector types; types.push_back(a); types.push_back(b); types.push_back(c); - Type t = d_nodeManager->mkFunctionType(types); - Type t2 = d_nodeManager->mkFunctionType(types); + TypeNode t = d_nodeManager->mkFunctionType(types); + TypeNode t2 = d_nodeManager->mkFunctionType(types); TS_ASSERT( !t.isBoolean() ); TS_ASSERT( t.isFunction() ); @@ -297,7 +297,7 @@ public: TS_ASSERT_EQUALS( t, t2 ); - FunctionType ft = t; + TypeNode ft = t; TS_ASSERT_EQUALS( ft, t ); TS_ASSERT_EQUALS(ft.getArgTypes().size(), types.size()-1); TS_ASSERT_EQUALS(ft.getArgTypes()[0], a); @@ -306,18 +306,18 @@ public: } void testMkPredicateType() { - Type a = d_nodeManager->mkSort("a"); - Type b = d_nodeManager->mkSort("b"); - Type c = d_nodeManager->mkSort("c"); - Type booleanType = d_nodeManager->booleanType(); + TypeNode a = d_nodeManager->mkSort("a"); + TypeNode b = d_nodeManager->mkSort("b"); + TypeNode c = d_nodeManager->mkSort("c"); + TypeNode booleanType = d_nodeManager->booleanType(); - std::vector argTypes; + std::vector argTypes; argTypes.push_back(a); argTypes.push_back(b); argTypes.push_back(c); - Type t = d_nodeManager->mkPredicateType(argTypes); - Type t2 = d_nodeManager->mkPredicateType(argTypes); + TypeNode t = d_nodeManager->mkPredicateType(argTypes); + TypeNode t2 = d_nodeManager->mkPredicateType(argTypes); TS_ASSERT( !t.isBoolean() ); TS_ASSERT( t.isFunction() ); @@ -328,7 +328,7 @@ public: TS_ASSERT_EQUALS( t, t2 ); - FunctionType ft = t; + TypeNode ft = t; TS_ASSERT_EQUALS( ft, t ); TS_ASSERT_EQUALS(ft.getArgTypes().size(), argTypes.size()); TS_ASSERT_EQUALS(ft.getArgTypes()[0], a); diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 25c22f196..e0dfd7aa8 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -211,8 +211,8 @@ public: void testRegisterTerm() { TS_ASSERT(d_dummy->doneWrapper()); - Type typeX = d_nm->booleanType(); - Type typeF = d_nm->mkFunctionType(typeX, typeX); + TypeNode typeX = d_nm->booleanType(); + TypeNode typeF = d_nm->mkFunctionType(typeX, typeX); Node x = d_nm->mkVar("x",typeX); Node f = d_nm->mkVar("f",typeF); diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h index 44b13c87c..6b14a38d5 100644 --- a/test/unit/theory/theory_uf_white.h +++ b/test/unit/theory/theory_uf_white.h @@ -94,7 +94,7 @@ class TheoryUFWhite : public CxxTest::TestSuite { TheoryUF* d_euf; - Type* d_booleanType; + TypeNode* d_booleanType; public: @@ -107,7 +107,7 @@ public: d_outputChannel.clear(); d_euf = new TheoryUF(d_ctxt, d_outputChannel); - d_booleanType = new Type(d_nm->booleanType()); + d_booleanType = new TypeNode(d_nm->booleanType()); } void tearDown() { -- 2.30.2