From 9576517676138a8ca2887a967f1b056662ef6754 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 16 Mar 2010 20:24:37 +0000 Subject: * test/unit/Makefile.am, test/unit/expr/attribute_white.h, test/unit/expr/node_white.h: add whitebox attribute test (pulled out attribute stuff from node_white) * test/unit/parser/parser_black.h: fix memory leaks uncovered by valgrind * src/theory/interrupted.h: actually make this "lightweight" (not derived from CVC4::Exception), as promised in my last commit * src/theory/uf/theory_uf.h, test/unit/expr/attribute_black.h: match the new-style cleanup function definition * src/expr/attribute.cpp, src/expr/attribute.h: support for attribute deletion, custom cleanup functions, clearer cleanup function definition. * src/expr/node_manager.h, src/expr/node_manager.cpp: reclaim remaining zombies in dtor, rename NodeValueSet ==> "NodeValuePool", and enable freeing of NodeValues * src/expr/type.h, src/expr/type.cpp: reference-counting for types, customized cleanup function for types, also code cleanup * (various): changed "const Type*" to "Type*" (to enable reference-counting etc. Types are still immutable.) * src/util/output.h: add ::isOn()-- which queries whether a Debug/Trace flag is currently on or not. * src/smt/smt_engine.cpp, src/parser/antlr_parser.cpp, src/expr/type.cpp, src/expr/expr_manager.cpp, various others: minor code cleanup --- src/expr/node_manager.h | 59 +++++++++++++++++++++++++------------------------ 1 file changed, 30 insertions(+), 29 deletions(-) (limited to 'src/expr/node_manager.h') diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index b40ec2978..a3be61e48 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -30,6 +30,7 @@ #include "expr/expr.h" #include "expr/node_value.h" #include "context/context.h" +#include "expr/type.h" namespace CVC4 { @@ -44,7 +45,7 @@ struct Type {}; }/* CVC4::expr::attr namespace */ typedef Attribute VarNameAttr; -typedef Attribute TypeAttr; +typedef ManagedAttribute TypeAttr; }/* CVC4::expr namespace */ @@ -55,12 +56,12 @@ class NodeManager { typedef __gnu_cxx::hash_set NodeValueSet; + expr::NodeValue::NodeValueEq> NodeValuePool; typedef __gnu_cxx::hash_set ZombieSet; - NodeValueSet d_nodeValueSet; + NodeValuePool d_nodeValuePool; expr::attr::AttributeManager d_attrManager; @@ -108,6 +109,8 @@ public: poolInsert( &expr::NodeValue::s_null ); } + ~NodeManager(); + static NodeManager* currentNM() { return s_current; } // general expression-builders @@ -121,8 +124,8 @@ public: Node mkNode(Kind kind, const std::vector& children); // variables are special, because duplicates are permitted - Node mkVar(const Type* type, const std::string& name); - Node mkVar(const Type* type); + Node mkVar(Type* type, const std::string& name); + Node mkVar(Type* type); Node mkVar(); template @@ -172,27 +175,26 @@ public: const typename AttrKind::value_type& value); /** Get the type for booleans. */ - inline const BooleanType* booleanType() const { + inline BooleanType* booleanType() const { return BooleanType::getInstance(); } /** Get the type for sorts. */ - inline const KindType* kindType() const { + inline KindType* kindType() const { return KindType::getInstance(); } /** Make a function type from domain to range. */ - inline const FunctionType* - mkFunctionType(const Type* domain, const Type* range) const; + inline FunctionType* mkFunctionType(Type* domain, Type* range) const; /** Make a function type with input types from argTypes. */ - inline const FunctionType* - mkFunctionType(const std::vector& argTypes, const Type* range) const; + inline FunctionType* mkFunctionType(const std::vector& argTypes, + Type* range) const; /** Make a new sort with the given name. */ - inline const Type* mkSort(const std::string& name) const; + inline Type* mkSort(const std::string& name) const; - inline const Type* getType(TNode n) const; + inline Type* getType(TNode n) const; }; /** @@ -308,41 +310,39 @@ inline void NodeManager::setAttribute(TNode n, /** Make a function type from domain to range. * TODO: Function types should be unique for this manager. */ -const FunctionType* -NodeManager::mkFunctionType(const Type* domain, - const Type* range) const { - std::vector argTypes; +FunctionType* NodeManager::mkFunctionType(Type* domain, + Type* range) const { + std::vector argTypes; argTypes.push_back(domain); return new FunctionType(argTypes, range); } /** Make a function type with input types from argTypes. * TODO: Function types should be unique for this manager. */ -const FunctionType* -NodeManager::mkFunctionType(const std::vector& argTypes, - const Type* range) const { +FunctionType* NodeManager::mkFunctionType(const std::vector& argTypes, + Type* range) const { Assert( argTypes.size() > 0 ); return new FunctionType(argTypes, range); } -const Type* -NodeManager::mkSort(const std::string& name) const { +Type* NodeManager::mkSort(const std::string& name) const { return new SortType(name); } -inline const Type* NodeManager::getType(TNode n) const { + +inline Type* NodeManager::getType(TNode n) const { return getAttribute(n, CVC4::expr::TypeAttr()); } inline void NodeManager::poolInsert(expr::NodeValue* nv) { - Assert(d_nodeValueSet.find(nv) == d_nodeValueSet.end(), + Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end(), "NodeValue already in the pool!"); - d_nodeValueSet.insert(nv);// FIXME multithreading + d_nodeValuePool.insert(nv);// FIXME multithreading } inline void NodeManager::poolRemove(expr::NodeValue* nv) { - Assert(d_nodeValueSet.find(nv) != d_nodeValueSet.end(), + Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end(), "NodeValue is not in the pool!"); - d_nodeValueSet.erase(nv);// FIXME multithreading + d_nodeValuePool.erase(nv);// FIXME multithreading } }/* CVC4 namespace */ @@ -382,14 +382,15 @@ inline Node NodeManager::mkNode(Kind kind, const std::vector& children) { return NodeBuilder<>(this, kind).append(children); } -inline Node NodeManager::mkVar(const Type* type, const std::string& name) { +inline Node NodeManager::mkVar(Type* type, const std::string& name) { Node n = mkVar(type); n.setAttribute(expr::VarNameAttr(), name); return n; } -inline Node NodeManager::mkVar(const Type* type) { +inline Node NodeManager::mkVar(Type* type) { Node n = mkVar(); + type->inc();// reference-count the type n.setAttribute(expr::TypeAttr(), type); return n; } -- cgit v1.2.3