diff options
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 54 |
1 files changed, 42 insertions, 12 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 7e0cfd0cf..3586440d4 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -329,7 +329,11 @@ public: template <class NodeClass, class T> NodeClass mkConstInternal(const T&); - /** Create a node with no children. */ + /** Create a node with children. */ + TypeNode mkTypeNode(Kind kind, TypeNode child1); + TypeNode mkTypeNode(Kind kind, TypeNode child1, TypeNode child2); + TypeNode mkTypeNode(Kind kind, TypeNode child1, TypeNode child2, + TypeNode child3); TypeNode mkTypeNode(Kind kind, const std::vector<TypeNode>& children); /** @@ -472,9 +476,6 @@ public: /** Get the (singleton) type for sorts. */ inline TypeNode kindType(); - /** Get the type of bitvectors of size <code>size</code> */ - inline TypeNode bitVectorType(unsigned size); - /** * Make a function type from domain to range. * @@ -492,7 +493,8 @@ public: * @param range the range type * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range */ - inline TypeNode mkFunctionType(const std::vector<TypeNode>& argTypes, const TypeNode& range); + inline TypeNode mkFunctionType(const std::vector<TypeNode>& argTypes, + const TypeNode& range); /** * Make a function type with input types from @@ -510,6 +512,12 @@ public: */ inline TypeNode mkPredicateType(const std::vector<TypeNode>& sorts); + /** Make the type of bitvectors of size <code>size</code> */ + inline TypeNode mkBitVectorType(unsigned size); + + /** Make the type of arrays with the given parameterization */ + inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType); + /** Make a new sort. */ inline TypeNode mkSort(); @@ -519,7 +527,8 @@ public: /** * Get the type for the given node. */ - TypeNode getType(TNode n) throw (TypeCheckingExceptionPrivate); + TypeNode getType(TNode n) + throw (TypeCheckingExceptionPrivate, AssertionException); }; @@ -637,10 +646,6 @@ inline TypeNode NodeManager::kindType() { return TypeNode(mkTypeConst<TypeConstant>(KIND_TYPE)); } -inline TypeNode NodeManager::bitVectorType(unsigned size) { - return TypeNode(mkTypeConst<BitVectorSize>(BitVectorSize(size))); -} - /** Make a function type from domain to range. */ inline TypeNode NodeManager::mkFunctionType(const TypeNode& domain, const TypeNode& range) { std::vector<TypeNode> sorts; @@ -677,6 +682,15 @@ NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) { return mkTypeNode(kind::FUNCTION_TYPE, sortNodes); } +inline TypeNode NodeManager::mkBitVectorType(unsigned size) { + return TypeNode(mkTypeConst<BitVectorSize>(BitVectorSize(size))); +} + +inline TypeNode NodeManager::mkArrayType(TypeNode indexType, + TypeNode constituentType) { + return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType); +} + inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const { NodeValuePool::const_iterator find = d_nodeValuePool.find(nv); if(find == d_nodeValuePool.end()) { @@ -836,8 +850,23 @@ inline Node* NodeManager::mkNodePtr(TNode opNode, } +inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1) { + return (NodeBuilder<1>(this, kind) << child1).constructTypeNode(); +} + +inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1, + TypeNode child2) { + return (NodeBuilder<2>(this, kind) << child1 << child2).constructTypeNode(); +} + +inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1, + TypeNode child2, TypeNode child3) { + return (NodeBuilder<3>(this, kind) << child1 << child2 << child3).constructTypeNode();; +} + // N-ary version for types -inline TypeNode NodeManager::mkTypeNode(Kind kind, const std::vector<TypeNode>& children) { +inline TypeNode NodeManager::mkTypeNode(Kind kind, + const std::vector<TypeNode>& children) { return NodeBuilder<>(this, kind).append(children).constructTypeNode(); } @@ -848,7 +877,8 @@ inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type) { return n; } -inline Node* NodeManager::mkVarPtr(const std::string& name, const TypeNode& type) { +inline Node* NodeManager::mkVarPtr(const std::string& name, + const TypeNode& type) { Node* n = mkVarPtr(type); n->setAttribute(expr::VarNameAttr(), name); return n; |