From 374e28dcc625f1694cfc87f7b4c376dc329694c4 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 25 Feb 2010 18:26:22 +0000 Subject: [PATCH] * src/expr/node_builder.h: fixed some overly-aggressive refcount decrementing. There remain memory leaks (and some over-decrementing of refcounts) that I've identified; another commit forthcoming. * src/expr/attribute.h: keys are now NodeValue* instead of TNode * src/theory/output_channel.h: change OutputChannel::conflict() to the negation of what we had before: it now takes an AND of TRUE literals as a conflict clause rather than an OR of FALSE ones. * src/expr/node.cpp: (non-template) CVC4::expr::debugPrint() routine for use inside gdb * src/expr/node.h: remove Node::debugPrint() member (now a function instead of a member function, since Node is now a template it wasn't being properly instantiated(?) and couldn't be called from gdb) * src/expr/Makefile.am: add node.cpp * src/expr/node_manager.h: code formatting --- src/expr/Makefile.am | 1 + src/expr/attribute.h | 56 ++++++++++++++++++------------------- src/expr/node.cpp | 46 ++++++++++++++++++++++++++++++ src/expr/node.h | 25 ++++------------- src/expr/node_builder.h | 7 +++-- src/expr/node_manager.h | 2 +- src/theory/output_channel.h | 5 ++-- 7 files changed, 90 insertions(+), 52 deletions(-) create mode 100644 src/expr/node.cpp diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 27c64e9ef..1aa2e61fa 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -7,6 +7,7 @@ noinst_LTLIBRARIES = libexpr.la libexpr_la_SOURCES = \ node.h \ + node.cpp \ node_builder.h \ expr.h \ type.h \ diff --git a/src/expr/attribute.h b/src/expr/attribute.h index 4bc569620..c56725f18 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -45,8 +45,8 @@ namespace attr { */ struct AttrHashFcn { enum { LARGE_PRIME = 32452843ul }; - std::size_t operator()(const std::pair& p) const { - return p.first * LARGE_PRIME + p.second.hash(); + std::size_t operator()(const std::pair& p) const { + return p.first * LARGE_PRIME + p.second->hash(); } }; @@ -56,8 +56,8 @@ struct AttrHashFcn { * in [0..63] for each attribute */ struct AttrHashBoolFcn { - std::size_t operator()(TNode n) const { - return n.hash(); + std::size_t operator()(NodeValue* nv) const { + return nv->hash(); } }; @@ -157,7 +157,7 @@ namespace attr { */ template struct AttrHash : - public __gnu_cxx::hash_map, + public __gnu_cxx::hash_map, value_type, AttrHashFcn> { }; @@ -168,12 +168,12 @@ struct AttrHash : */ template <> class AttrHash : - protected __gnu_cxx::hash_map { /** A "super" type, like in Java, for easy reference below. */ - typedef __gnu_cxx::hash_map super; + typedef __gnu_cxx::hash_map super; /** * BitAccessor allows us to return a bit "by reference." Of course, @@ -218,7 +218,7 @@ class AttrHash : */ class BitIterator { - std::pair* d_entry; + std::pair* d_entry; unsigned d_bit; @@ -229,12 +229,12 @@ class AttrHash : d_bit(0) { } - BitIterator(std::pair& entry, unsigned bit) : + BitIterator(std::pair& entry, unsigned bit) : d_entry(&entry), d_bit(bit) { } - std::pair operator*() { + std::pair operator*() { return std::make_pair(d_entry->first, BitAccessor(d_entry->second, d_bit)); } @@ -251,7 +251,7 @@ class AttrHash : */ class ConstBitIterator { - const std::pair* d_entry; + const std::pair* d_entry; unsigned d_bit; @@ -262,12 +262,12 @@ class AttrHash : d_bit(0) { } - ConstBitIterator(const std::pair& entry, unsigned bit) : + ConstBitIterator(const std::pair& entry, unsigned bit) : d_entry(&entry), d_bit(bit) { } - std::pair operator*() { + std::pair operator*() { return std::make_pair(d_entry->first, (d_entry->second & (1 << d_bit)) ? true : false); } @@ -278,7 +278,7 @@ class AttrHash : public: - typedef std::pair key_type; + typedef std::pair key_type; typedef bool data_type; typedef std::pair value_type; @@ -291,7 +291,7 @@ public: * Find the boolean value in the hash table. Returns something == * end() if not found. */ - BitIterator find(const std::pair& k) { + BitIterator find(const std::pair& k) { super::iterator i = super::find(k.second); if(i == super::end()) { return BitIterator(); @@ -313,7 +313,7 @@ public: * Find the boolean value in the hash table. Returns something == * end() if not found. */ - ConstBitIterator find(const std::pair& k) const { + ConstBitIterator find(const std::pair& k) const { super::const_iterator i = super::find(k.second); if(i == super::end()) { return ConstBitIterator(); @@ -336,7 +336,7 @@ public: * the key into the table (associated to default value) if it's not * already there. */ - BitAccessor operator[](const std::pair& k) { + BitAccessor operator[](const std::pair& k) { uint64_t& word = super::operator[](k.second); return BitAccessor(word, k.first); } @@ -708,7 +708,7 @@ typename AttrKind::value_type AttributeManager::getAttribute(TNode n, typedef typename getTable::table_type table_type; const table_type& ah = getTable::get(*this); - typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), n)); + typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), n.d_nv)); if(i == ah.end()) { return typename AttrKind::value_type(); @@ -731,7 +731,7 @@ template struct HasAttribute { /** This implementation is simple; it's always true. */ static inline bool hasAttribute(const AttributeManager* am, - TNode n) { + NodeValue* nv) { return true; } @@ -740,14 +740,14 @@ struct HasAttribute { * Node doesn't have the given attribute. */ static inline bool hasAttribute(const AttributeManager* am, - TNode n, + NodeValue* nv, typename AttrKind::value_type& ret) { typedef typename AttrKind::value_type value_type; typedef KindValueToTableValueMapping mapping; typedef typename getTable::table_type table_type; const table_type& ah = getTable::get(*am); - typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), n)); + typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); if(i == ah.end()) { ret = AttrKind::default_value; @@ -766,13 +766,13 @@ struct HasAttribute { template struct HasAttribute { static inline bool hasAttribute(const AttributeManager* am, - TNode n) { + NodeValue* nv) { typedef typename AttrKind::value_type value_type; typedef KindValueToTableValueMapping mapping; typedef typename getTable::table_type table_type; const table_type& ah = getTable::get(*am); - typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), n)); + typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); if(i == ah.end()) { return false; @@ -782,14 +782,14 @@ struct HasAttribute { } static inline bool hasAttribute(const AttributeManager* am, - TNode n, + NodeValue* nv, typename AttrKind::value_type& ret) { typedef typename AttrKind::value_type value_type; typedef KindValueToTableValueMapping mapping; typedef typename getTable::table_type table_type; const table_type& ah = getTable::get(*am); - typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), n)); + typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); if(i == ah.end()) { return false; @@ -804,14 +804,14 @@ struct HasAttribute { template bool AttributeManager::hasAttribute(TNode n, const AttrKind&) const { - return HasAttribute::hasAttribute(this, n); + return HasAttribute::hasAttribute(this, n.d_nv); } template bool AttributeManager::hasAttribute(TNode n, const AttrKind&, typename AttrKind::value_type& ret) const { - return HasAttribute::hasAttribute(this, n, ret); + return HasAttribute::hasAttribute(this, n.d_nv, ret); } template @@ -824,7 +824,7 @@ inline void AttributeManager::setAttribute(TNode n, typedef typename getTable::table_type table_type; table_type& ah = getTable::get(*this); - ah[std::make_pair(AttrKind::getId(), n)] = mapping::convert(value); + ah[std::make_pair(AttrKind::getId(), n.d_nv)] = mapping::convert(value); } }/* CVC4::expr::attr namespace */ diff --git a/src/expr/node.cpp b/src/expr/node.cpp new file mode 100644 index 000000000..213171124 --- /dev/null +++ b/src/expr/node.cpp @@ -0,0 +1,46 @@ +/********************* */ +/** node.cpp + ** Original author: mdeters + ** 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/node.h" +#include "util/output.h" + +namespace CVC4 { +namespace expr { + +#ifdef CVC4_DEBUG + +/** + * Pretty printer for use within gdb. This is not intended to be used + * outside of gdb. This writes to the Warning() stream and immediately + * flushes the stream. + * + * Note that this function cannot be a template, since the compiler + * won't instantiate it. Even if we explicitly instantiate. (Odd?) + * So we implement twice. + */ +void CVC4_PUBLIC debugPrint(const NodeTemplate& n) { + n.printAst(Warning(), 0); + Warning().flush(); +} + +void CVC4_PUBLIC debugPrint(const NodeTemplate& n) { + n.printAst(Warning(), 0); + Warning().flush(); +} + +#endif /* CVC4_DEBUG */ + +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ diff --git a/src/expr/node.h b/src/expr/node.h index 19e50c5c2..474a175b1 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -36,7 +36,6 @@ class Type; class NodeManager; template class NodeTemplate; - /** * The Node class encapsulates the NodeValue with reference counting. */ @@ -48,7 +47,11 @@ typedef NodeTemplate Node; typedef NodeTemplate TNode; namespace expr { -class NodeValue; + class NodeValue; + + namespace attr { + class AttributeManager; + }/* CVC4::expr::attr namespace */ }/* CVC4::expr namespace */ using CVC4::expr::NodeValue; @@ -93,6 +96,7 @@ template friend class NodeManager; template friend class NodeBuilder; + friend class ::CVC4::expr::attr::AttributeManager; /** * Assigns the expression value and does reference counting. No assumptions @@ -355,19 +359,8 @@ template NodeTemplate impNode(const NodeTemplate& right) const; NodeTemplate xorNode(const NodeTemplate& right) const; - NodeTemplate plusNode(const NodeTemplate& right) const; - NodeTemplate uMinusNode() const; - NodeTemplate multNode(const NodeTemplate& right) const; - private: - /** - * Pretty printer for use within gdb. This is not intended to be used - * outside of gdb. This writes to the Warning() stream and immediately - * flushes the stream. - */ - void debugPrint(); - /** * Indents the given stream a given amount of spaces. * @param out the stream to indent @@ -606,12 +599,6 @@ template out << ')'; } -template - void NodeTemplate::debugPrint() { - printAst(Warning(), 0); - Warning().flush(); - } - template const Type* NodeTemplate::getType() const { Assert( NodeManager::currentNM() != NULL, diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 0b89fcb5e..03936c89a 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -509,7 +509,7 @@ void NodeBuilder::clear(Kind k) { d_used = false; d_nv = &d_inlineNv; d_inlineNv.d_kind = k; - d_inlineNv.d_nchildren = 0; + d_inlineNv.d_nchildren = 0;//FIXME leak } template @@ -551,6 +551,8 @@ void NodeBuilder::realloc(size_t toSize, bool copy) { std::copy(d_inlineNv.d_children, d_inlineNv.d_children + nchild_thresh, d_nv->d_children); + // inhibit decr'ing refcounts of children in dtor + d_inlineNv.d_nchildren = 0; } } } @@ -583,7 +585,7 @@ NodeBuilder::operator Node() {// not const Assert(d_nv->d_nchildren == 0); NodeValue *nv = (NodeValue*) std::malloc(sizeof(NodeValue) + - ( sizeof(NodeValue*) * d_inlineNv.d_nchildren )); + (sizeof(NodeValue*) * d_inlineNv.d_nchildren ));// FIXME :: WTF?? nv->d_nchildren = 0; nv->d_kind = kind::VARIABLE; nv->d_id = NodeValue::next_id++;// FIXME multithreading @@ -641,6 +643,7 @@ NodeBuilder::operator Node() {// not const ev->d_children); d_used = true; d_nv = NULL; + d_inlineNv.d_nchildren = 0;// inhibit decr'ing refcounts of children in dtor // Make the new expression d_nm->poolInsert(ev); diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index bcb5f6d47..a200a6d77 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -160,7 +160,7 @@ inline void NodeManager::setAttribute(TNode n, } inline const Type* NodeManager::getType(TNode n) { - return getAttribute(n,CVC4::expr::TypeAttr()); + return getAttribute(n, CVC4::expr::TypeAttr()); } inline void NodeManager::poolInsert(NodeValue* nv) { diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index ad558e115..efd2911ef 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -58,8 +58,9 @@ public: * Indicate a theory conflict has arisen. * * @param n - a conflict at the current decision level. This should - * be an OR-kinded node of literals that are false in the current - * assignment. + * be an AND-kinded node of literals that are TRUE in the current + * assignment and are in conflict (i.e., at least one must be + * assigned false). * * @param safe - whether it is safe to be interrupted */ -- 2.30.2