diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/Makefile.am | 6 | ||||
-rw-r--r-- | src/expr/attribute.cpp | 2 | ||||
-rw-r--r-- | src/expr/attribute.h | 17 | ||||
-rw-r--r-- | src/expr/expr_manager_template.cpp | 32 | ||||
-rw-r--r-- | src/expr/node.h | 20 | ||||
-rw-r--r-- | src/expr/node_builder.h | 44 | ||||
-rw-r--r-- | src/expr/node_manager.h | 150 | ||||
-rw-r--r-- | src/expr/node_value.h | 33 | ||||
-rw-r--r-- | src/expr/type.cpp | 36 | ||||
-rw-r--r-- | src/expr/type.h | 16 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 62 | ||||
-rw-r--r-- | src/expr/type_node.h | 437 |
12 files changed, 732 insertions, 123 deletions
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<TNode> d_tnodes; /** Underlying hash table for node-valued attributes */ AttrHash<Node> d_nodes; + /** Underlying hash table for types attributes */ + AttrHash<TypeNode> d_types; /** Underlying hash table for string-valued attributes */ AttrHash<std::string> d_strings; /** Underlying hash table for pointer-valued attributes */ @@ -241,6 +244,18 @@ struct getTable<Node, false> { } }; +/** Access the "d_types" member of AttributeManager. */ +template <> +struct getTable<TypeNode, false> { + typedef AttrHash<TypeNode> 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<std::string, false> { @@ -313,7 +328,7 @@ struct getTable<TNode, true> { } }; -/** Access the "d_nodes" member of AttributeManager. */ +/** Access the "d_cdnodes" member of AttributeManager. */ template <> struct getTable<Node, true> { typedef CDAttrHash<Node> 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<Expr>& 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<Type>& argTypes, const Type& range) { Assert( argTypes.size() >= 1 ); NodeManagerScope nms(d_nodeManager); - return d_nodeManager->mkFunctionType(argTypes, range); + std::vector<TypeNode> 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<Type>& sorts) { Assert( sorts.size() >= 2 ); NodeManagerScope nms(d_nodeManager); - return d_nodeManager->mkFunctionType(sorts); + std::vector<TypeNode> 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<Type>& sorts) { Assert( sorts.size() >= 1 ); NodeManagerScope nms(d_nodeManager); - return d_nodeManager->mkPredicateType(sorts); + std::vector<TypeNode> 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 <bool ref_count> @@ -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<ref_count> iterator; + typedef typename expr::NodeValue::iterator< NodeTemplate<ref_count> > iterator; /** Constant iterator allowing for scanning through the children. */ - typedef typename expr::NodeValue::iterator<ref_count> const_iterator; + typedef typename expr::NodeValue::iterator< NodeTemplate<ref_count> > const_iterator; /** * Returns the iterator pointing to the first child. * @return the iterator */ inline iterator begin() { - return d_nv->begin<ref_count>(); + return d_nv->begin< NodeTemplate<ref_count> >(); } /** @@ -340,7 +340,7 @@ public: * @return the end of the children iterator. */ inline iterator end() { - return d_nv->end<ref_count>(); + return d_nv->end< NodeTemplate<ref_count> >(); } /** @@ -348,7 +348,7 @@ public: * @return the const_iterator */ inline const_iterator begin() const { - return d_nv->begin<ref_count>(); + return d_nv->begin< NodeTemplate<ref_count> >(); } /** @@ -357,7 +357,7 @@ public: * @return the end of the children const_iterator. */ inline const_iterator end() const { - return d_nv->end<ref_count>(); + return d_nv->end< NodeTemplate<ref_count> >(); } /** @@ -814,7 +814,7 @@ inline bool NodeTemplate<ref_count>::hasOperator() const { } template <bool ref_count> -Type NodeTemplate<ref_count>::getType() const { +TypeNode NodeTemplate<ref_count>::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<true> iterator; - typedef expr::NodeValue::iterator<true> const_iterator; + typedef expr::NodeValue::iterator< NodeTemplate<true> > iterator; + typedef expr::NodeValue::iterator< NodeTemplate<true> > 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<true>(); + return d_nv->begin< NodeTemplate<true> >(); } /** 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<true>(); + return d_nv->end< NodeTemplate<true> >(); } /** 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<TypeNode>& 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 <bool ref_count> inline Builder& @@ -537,6 +546,18 @@ public: return static_cast<Builder&>(*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<Builder&>(*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<Builder>::decrRefCounts() { d_inlineNv.d_nchildren = 0; } + +template <class Builder> +TypeNode NodeBuilderBase<Builder>::constructTypeNode() { + return TypeNode(constructNV()); +} + +template <class Builder> +TypeNode NodeBuilderBase<Builder>::constructTypeNode() const { + return TypeNode(constructNV()); +} + template <class Builder> Node NodeBuilderBase<Builder>::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<TypeTag, Node> TypeAttr; + typedef expr::Attribute<TypeTag, TypeNode> TypeAttr; typedef expr::Attribute<AtomicTag, bool> 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 <class T> Node mkConst(const T&); + template <class T> + TypeNode mkTypeConst(const T&); + + template <class NodeClass, class T> + 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<TypeNode>& 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<Type>& argTypes, const Type& range); + inline TypeNode mkFunctionType(const std::vector<TypeNode>& argTypes, const TypeNode& range); /** * Make a function type with input types from @@ -463,7 +477,7 @@ public: * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have * at least 2 elements. */ - inline Type mkFunctionType(const std::vector<Type>& sorts); + inline TypeNode mkFunctionType(const std::vector<TypeNode>& sorts); /** * Make a predicate type with input types from @@ -471,18 +485,18 @@ public: * <code>BOOLEAN</code>. <code>sorts</code> must have at least one * element. */ - inline Type mkPredicateType(const std::vector<Type>& sorts); + inline TypeNode mkPredicateType(const std::vector<TypeNode>& 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<TypeConstant>(BOOLEAN_TYPE))); +inline TypeNode NodeManager::booleanType() { + return TypeNode(mkTypeConst<TypeConstant>(BOOLEAN_TYPE)); } /** Get the (singleton) type for sorts. */ -inline KindType NodeManager::kindType() { - return Type(this, new Node(mkConst<TypeConstant>(KIND_TYPE))); +inline TypeNode NodeManager::kindType() { + return TypeNode(mkTypeConst<TypeConstant>(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<TypeNode> sorts; + sorts.push_back(domain); + sorts.push_back(range); + return mkFunctionType(sorts); } -inline Type NodeManager::mkFunctionType(const std::vector<Type>& argTypes, const Type& range) { +inline TypeNode NodeManager::mkFunctionType(const std::vector<TypeNode>& argTypes, const TypeNode& range) { Assert(argTypes.size() >= 1); - std::vector<Type> sorts(argTypes); + std::vector<TypeNode> sorts(argTypes); sorts.push_back(range); return mkFunctionType(sorts); } - -inline Type -NodeManager::mkFunctionType(const std::vector<Type>& sorts) { +inline TypeNode +NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts) { Assert(sorts.size() >= 2); - std::vector<Node> sortNodes; + std::vector<TypeNode> 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<Type>& sorts) { +inline TypeNode +NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) { Assert(sorts.size() >= 1); - std::vector<Node> sortNodes; + std::vector<TypeNode> 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<TypeNode>& 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 <class T> Node NodeManager::mkConst(const T& val) { - // typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t; + return mkConstInternal<Node, T>(val); +} + +template <class T> +TypeNode NodeManager::mkTypeConst(const T& val) { + return mkConstInternal<TypeNode, T>(val); +} + +template <class NodeClass, class T> +NodeClass NodeManager::mkConstInternal(const T& val) { + // typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t; NVStorage<1> nvStorage; expr::NodeValue& nvStack = reinterpret_cast<expr::NodeValue&>(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 <bool ref_count> class NodeTemplate; +class TypeNode; template <class Builder> class NodeBuilderBase; template <unsigned N> class NodeBuilder; class AndNodeBuilder; @@ -101,6 +102,7 @@ class NodeValue { // todo add exprMgr ref in debug case template <bool> friend class ::CVC4::NodeTemplate; + friend class ::CVC4::TypeNode; template <class Builder> friend class ::CVC4::NodeBuilderBase; template <unsigned nchild_thresh> 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 <bool ref_count> + template <typename T> class iterator { const_nv_iterator d_i; public: explicit iterator(const_nv_iterator i) : d_i(i) {} - inline CVC4::NodeTemplate<ref_count> operator*(); + inline T operator*(); bool operator==(const iterator& i) { return d_i == i.d_i; @@ -172,11 +174,11 @@ private: public: - template <bool ref_count> - inline iterator<ref_count> begin() const; + template <typename T> + inline iterator<T> begin() const; - template <bool ref_count> - inline iterator<ref_count> end() const; + template <typename T> + inline iterator<T> 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 <bool ref_count> -inline NodeValue::iterator<ref_count> NodeValue::begin() const { +template <typename T> +inline NodeValue::iterator<T> NodeValue::begin() const { NodeValue* const* firstChild = d_children; if(getMetaKind() == kind::metakind::PARAMETERIZED) { ++firstChild; } - return iterator<ref_count>(firstChild); + return iterator<T>(firstChild); } -template <bool ref_count> -inline NodeValue::iterator<ref_count> NodeValue::end() const { - return iterator<ref_count>(d_children + d_nchildren); +template <typename T> +inline NodeValue::iterator<T> NodeValue::end() const { + return iterator<T>(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 <bool ref_count> -inline CVC4::NodeTemplate<ref_count> NodeValue::iterator<ref_count>::operator*() { - return NodeTemplate<ref_count>(*d_i); +template <typename T> +inline T NodeValue::iterator<T>::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 <string> @@ -26,12 +27,12 @@ std::ostream& operator<<(std::ostream& out, const Type& e) { return out; } -Type Type::makeType(NodeTemplate<false> 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<true>* 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<TypeConstant>() == 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<TypeConstant>() == KIND_TYPE; + return d_typeNode->isKind(); } /** Cast to a kind type */ @@ -157,15 +155,19 @@ Type::operator KindType() const { std::vector<Type> FunctionType::getArgTypes() const { NodeManagerScope nms(d_nodeManager); std::vector<Type> args; - for (unsigned i = 0, i_end = d_typeNode->getNumChildren() - 1; i < i_end; ++ i) { - args.push_back(makeType((*d_typeNode)[i])); + std::vector<TypeNode> argNodes = d_typeNode->getArgTypes(); + std::vector<TypeNode>::iterator it = argNodes.begin(); + std::vector<TypeNode>::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 <bool ref_count> 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<true>* 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<false> 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<true>* 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<TypeConstant>() == 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> TypeNode::getArgTypes() const { + Assert(isFunction()); + std::vector<TypeNode> 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<TypeConstant>() == 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 <vector> +#include <string> +#include <iostream> +#include <stdint.h> + +#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 <class Builder> + 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 <class T> + 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 <class AttrKind> + 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 <class AttrKind> + 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 <class AttrKind> + 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 <class AttrKind> + inline void setAttribute(const AttrKind& attKind, + const typename AttrKind::value_type& value); + + /** Iterator allowing for scanning through the children. */ + typedef expr::NodeValue::iterator<TypeNode> iterator; + /** Constant iterator allowing for scanning through the children. */ + typedef expr::NodeValue::iterator<TypeNode> const_iterator; + + /** + * Returns the iterator pointing to the first child. + * @return the iterator + */ + inline iterator begin() { + return d_nv->begin<TypeNode>(); + } + + /** + * 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<TypeNode>(); + } + + /** + * Returns the const_iterator pointing to the first child. + * @return the const_iterator + */ + inline const_iterator begin() const { + return d_nv->begin<TypeNode>(); + } + + /** + * 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<TypeNode>(); + } + + /** + * 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<TypeNode> 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 <ext/hash_map> + +#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 <class T> +inline const T& TypeNode::getConst() const { + return d_nv->getConst<T>(); +} + +inline TypeNode::TypeNode(const expr::NodeValue* ev) : + d_nv(const_cast<expr::NodeValue*> (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 <class AttrKind> +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 <class AttrKind> +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 <class AttrKind> +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 <class AttrKind> +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 */ |