diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/context/cdhashmap.h | 48 | ||||
-rw-r--r-- | src/expr/attribute.cpp | 33 | ||||
-rw-r--r-- | src/expr/attribute.h | 182 | ||||
-rw-r--r-- | src/expr/attribute_internals.h | 224 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 9 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 18 |
6 files changed, 26 insertions, 488 deletions
diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h index 21e30cef6..575bde120 100644 --- a/src/context/cdhashmap.h +++ b/src/context/cdhashmap.h @@ -60,14 +60,7 @@ ** itself from the map completely and put itself on a "trash ** list" for its scope. ** - ** Third, you might obliterate() the key. This calls the CDOhash_map - ** destructor, which calls destroy(), which does a successive - ** restore() until level 0. If the key was in the map since - ** level 0, the restore() won't remove it, so in that case - ** obliterate() removes it from the map and frees the CDOhash_map's - ** memory. - ** - ** Fourth, you might delete the cdhashmap(calling CDHashMap::~CDHashMap()). + ** Third, you might delete the cdhashmap(calling CDHashMap::~CDHashMap()). ** This first calls destroy(), as per ContextObj contract, but ** cdhashmapdoesn't save/restore itself, so that does nothing at the ** CDHashMap-level. Then, for each element in the map, it marks it as being @@ -75,7 +68,7 @@ ** CDOhash_map::restore() (see CDOhash_map::restore()), then deallocates ** it. ** - ** Fifth, you might clear() the CDHashMap. This does exactly the + ** Fourth, you might clear() the CDHashMap. This does exactly the ** same as CDHashMap::~CDHashMap(), except that it doesn't call destroy() ** on itself. ** @@ -403,43 +396,6 @@ public: // FIXME: no erase(), too much hassle to implement efficiently... - /** - * "Obliterating" is kind of like erasing, except it's not - * backtrackable; the key is permanently removed from the map. - * (Naturally, it can be re-added as a new element.) - */ - void obliterate(const Key& k) { - typename table_type::iterator i = d_map.find(k); - if(i != d_map.end()) { - Debug("gc") << "key " << k << " obliterated" << std::endl; - // Restore this object to level 0. If it was inserted after level 0, - // nothing else to do as restore will put it in the trash. - (*i).second->destroy(); - - // Check if object was inserted at level 0: in that case, still have - // to do some work. - typename table_type::iterator j = d_map.find(k); - if(j != d_map.end()) { - Element* elt = (*j).second; - if(d_first == elt) { - if(elt->d_next == elt) { - Assert(elt->d_prev == elt); - d_first = NULL; - } else { - d_first = elt->d_next; - } - } - elt->d_prev->d_next = elt->d_next; - elt->d_next->d_prev = elt->d_prev; - d_map.erase(j);//FIXME multithreading - Debug("gc") << "key " << k << " obliterated zero-scope: " << elt << std::endl; - if(!elt->d_noTrash) { - elt->deleteSelf(); - } - } - } - } - class iterator { const Element* d_it; diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index 2f938736e..f221c7c7e 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -13,12 +13,12 @@ ** ** AttributeManager implementation. **/ +#include "expr/attribute.h" + #include <utility> #include "base/output.h" -#include "expr/attribute.h" #include "expr/node_value.h" -#include "smt/smt_engine.h" using namespace std; @@ -26,15 +26,6 @@ namespace CVC4 { namespace expr { namespace attr { -SmtAttributes::SmtAttributes(context::Context* ctxt) : - d_cdbools(ctxt), - d_cdints(ctxt), - d_cdtnodes(ctxt), - d_cdnodes(ctxt), - d_cdstrings(ctxt), - d_cdptrs(ctxt) { -} - AttributeManager::AttributeManager() : d_inGarbageCollection(false) {} @@ -43,15 +34,6 @@ bool AttributeManager::inGarbageCollection() const { return d_inGarbageCollection; } -SmtAttributes& AttributeManager::getSmtAttributes(SmtEngine* smt) { - Assert(smt != NULL); - return *smt->d_smtAttributes; -} - -const SmtAttributes& AttributeManager::getSmtAttributes(SmtEngine* smt) const { - return *smt->d_smtAttributes; -} - void AttributeManager::debugHook(int debugFlag) { /* DO NOT CHECK IN ANY CODE INTO THE DEBUG HOOKS! * debugHook() is an empty function for the purpose of debugging @@ -71,17 +53,6 @@ void AttributeManager::deleteAllAttributes(NodeValue* nv) { deleteFromTable(d_ptrs, nv); } -void SmtAttributes::deleteAllAttributes(TNode n) { - NodeValue* nv = n.d_nv; - - d_cdbools.erase(nv); - deleteFromTable(d_cdints, nv); - deleteFromTable(d_cdtnodes, nv); - deleteFromTable(d_cdnodes, nv); - deleteFromTable(d_cdstrings, nv); - deleteFromTable(d_cdptrs, nv); -} - void AttributeManager::deleteAllAttributes() { d_bools.clear(); deleteAllFromTable(d_ints); diff --git a/src/expr/attribute.h b/src/expr/attribute.h index b5897ac51..5aea4a4d1 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -20,7 +20,6 @@ * attributes and nodes due to template use */ #include "expr/node.h" #include "expr/type_node.h" -#include "context/context.h" #ifndef __CVC4__EXPR__ATTRIBUTE_H #define __CVC4__EXPR__ATTRIBUTE_H @@ -35,45 +34,11 @@ #undef CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H namespace CVC4 { - -class SmtEngine; - -namespace smt { - extern CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current; -}/* CVC4::smt namespace */ - namespace expr { namespace attr { // ATTRIBUTE MANAGER =========================================================== -struct SmtAttributes { - SmtAttributes(context::Context*); - - // IF YOU ADD ANY TABLES, don't forget to add them also to the - // implementation of deleteAllAttributes(). - - /** Underlying hash table for context-dependent boolean-valued attributes */ - CDAttrHash<bool> d_cdbools; - /** Underlying hash table for context-dependent integral-valued attributes */ - CDAttrHash<uint64_t> d_cdints; - /** Underlying hash table for context-dependent node-valued attributes */ - CDAttrHash<TNode> d_cdtnodes; - /** Underlying hash table for context-dependent node-valued attributes */ - CDAttrHash<Node> d_cdnodes; - /** Underlying hash table for context-dependent string-valued attributes */ - CDAttrHash<std::string> d_cdstrings; - /** Underlying hash table for context-dependent pointer-valued attributes */ - CDAttrHash<void*> d_cdptrs; - - /** Delete all attributes of given node */ - void deleteAllAttributes(TNode n); - - template <class T> - void deleteFromTable(CDAttrHash<T>& table, NodeValue* nv); - -};/* struct SmtAttributes */ - /** * A container for the main attribute tables of the system. There's a * one-to-one NodeManager : AttributeManager correspondence. @@ -103,9 +68,6 @@ class AttributeManager { void clearDeleteAllAttributesBuffer(); - SmtAttributes& getSmtAttributes(SmtEngine*); - const SmtAttributes& getSmtAttributes(SmtEngine*) const; - public: /** Construct an attribute manager. */ @@ -239,10 +201,10 @@ template <> struct getTable<bool, false> { static const AttrTableId id = AttrTableBool; typedef AttrHash<bool> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + static inline table_type& get(AttributeManager& am) { return am.d_bools; } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + static inline const table_type& get(const AttributeManager& am) { return am.d_bools; } }; @@ -252,10 +214,10 @@ template <> struct getTable<uint64_t, false> { static const AttrTableId id = AttrTableUInt64; typedef AttrHash<uint64_t> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + static inline table_type& get(AttributeManager& am) { return am.d_ints; } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + static inline const table_type& get(const AttributeManager& am) { return am.d_ints; } }; @@ -265,10 +227,10 @@ template <> struct getTable<TNode, false> { static const AttrTableId id = AttrTableTNode; typedef AttrHash<TNode> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + static inline table_type& get(AttributeManager& am) { return am.d_tnodes; } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + static inline const table_type& get(const AttributeManager& am) { return am.d_tnodes; } }; @@ -278,10 +240,10 @@ template <> struct getTable<Node, false> { static const AttrTableId id = AttrTableNode; typedef AttrHash<Node> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + static inline table_type& get(AttributeManager& am) { return am.d_nodes; } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + static inline const table_type& get(const AttributeManager& am) { return am.d_nodes; } }; @@ -291,10 +253,10 @@ template <> struct getTable<TypeNode, false> { static const AttrTableId id = AttrTableTypeNode; typedef AttrHash<TypeNode> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + static inline table_type& get(AttributeManager& am) { return am.d_types; } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + static inline const table_type& get(const AttributeManager& am) { return am.d_types; } }; @@ -304,10 +266,10 @@ template <> struct getTable<std::string, false> { static const AttrTableId id = AttrTableString; typedef AttrHash<std::string> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + static inline table_type& get(AttributeManager& am) { return am.d_strings; } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + static inline const table_type& get(const AttributeManager& am) { return am.d_strings; } }; @@ -317,10 +279,10 @@ template <class T> struct getTable<T*, false> { static const AttrTableId id = AttrTablePointer; typedef AttrHash<void*> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + static inline table_type& get(AttributeManager& am) { return am.d_ptrs; } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + static inline const table_type& get(const AttributeManager& am) { return am.d_ptrs; } }; @@ -330,105 +292,14 @@ template <class T> struct getTable<const T*, false> { static const AttrTableId id = AttrTablePointer; typedef AttrHash<void*> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + static inline table_type& get(AttributeManager& am) { return am.d_ptrs; } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + static inline const table_type& get(const AttributeManager& am) { return am.d_ptrs; } }; -/** Access the "d_cdbools" member of AttributeManager. */ -template <> -struct getTable<bool, true> { - static const AttrTableId id = AttrTableCDBool; - typedef CDAttrHash<bool> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdbools; - } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdbools; - } -}; - -/** Access the "d_cdints" member of AttributeManager. */ -template <> -struct getTable<uint64_t, true> { - static const AttrTableId id = AttrTableCDUInt64; - typedef CDAttrHash<uint64_t> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdints; - } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdints; - } -}; - -/** Access the "d_tnodes" member of AttributeManager. */ -template <> -struct getTable<TNode, true> { - static const AttrTableId id = AttrTableCDTNode; - typedef CDAttrHash<TNode> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdtnodes; - } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdtnodes; - } -}; - -/** Access the "d_cdnodes" member of AttributeManager. */ -template <> -struct getTable<Node, true> { - static const AttrTableId id = AttrTableCDNode; - typedef CDAttrHash<Node> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdnodes; - } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdnodes; - } -}; - -/** Access the "d_cdstrings" member of AttributeManager. */ -template <> -struct getTable<std::string, true> { - static const AttrTableId id = AttrTableCDString; - typedef CDAttrHash<std::string> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdstrings; - } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdstrings; - } -}; - -/** Access the "d_cdptrs" member of AttributeManager. */ -template <class T> -struct getTable<T*, true> { - static const AttrTableId id = AttrTableCDPointer; - typedef CDAttrHash<void*> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdptrs; - } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdptrs; - } -}; - -/** Access the "d_cdptrs" member of AttributeManager. */ -template <class T> -struct getTable<const T*, true> { - static const AttrTableId id = AttrTableCDPointer; - typedef CDAttrHash<void*> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdptrs; - } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdptrs; - } -}; - }/* CVC4::expr::attr namespace */ // ATTRIBUTE MANAGER IMPLEMENTATIONS =========================================== @@ -445,7 +316,7 @@ AttributeManager::getAttribute(NodeValue* nv, const AttrKind&) const { table_type table_type; const table_type& ah = - getTable<value_type, AttrKind::context_dependent>::get(*this, smt::s_smtEngine_current); + getTable<value_type, AttrKind::context_dependent>::get(*this); typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); @@ -488,7 +359,7 @@ struct HasAttribute<true, AttrKind> { table_type; const table_type& ah = - getTable<value_type, AttrKind::context_dependent>::get(*am, smt::s_smtEngine_current); + getTable<value_type, AttrKind::context_dependent>::get(*am); typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); @@ -516,7 +387,7 @@ struct HasAttribute<false, AttrKind> { table_type table_type; const table_type& ah = - getTable<value_type, AttrKind::context_dependent>::get(*am, smt::s_smtEngine_current); + getTable<value_type, AttrKind::context_dependent>::get(*am); typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); @@ -536,7 +407,7 @@ struct HasAttribute<false, AttrKind> { table_type table_type; const table_type& ah = - getTable<value_type, AttrKind::context_dependent>::get(*am, smt::s_smtEngine_current); + getTable<value_type, AttrKind::context_dependent>::get(*am); typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); @@ -576,7 +447,7 @@ AttributeManager::setAttribute(NodeValue* nv, table_type table_type; table_type& ah = - getTable<value_type, AttrKind::context_dependent>::get(*this, smt::s_smtEngine_current); + getTable<value_type, AttrKind::context_dependent>::get(*this); ah[std::make_pair(AttrKind::getId(), nv)] = mapping::convert(value); } @@ -606,17 +477,6 @@ inline void AttributeManager::deleteFromTable(AttrHash<T>& table, } /** - * Obliterate a NodeValue from a (context-dependent) attribute table. - */ -template <class T> -inline void SmtAttributes::deleteFromTable(CDAttrHash<T>& table, - NodeValue* nv) { - for(unsigned id = 0; id < attr::LastAttributeId<T, true>::getId(); ++id) { - table.obliterate(std::make_pair(id, nv)); - } -} - -/** * Remove all attributes from the table calling the cleanup function * if one is defined. */ diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index 861739932..28c618cb0 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -25,8 +25,6 @@ #include <ext/hash_map> -#include "context/cdhashmap.h" - namespace CVC4 { namespace expr { @@ -368,217 +366,6 @@ public: } };/* class AttrHash<bool> */ -/** - * A "CDAttrHash<value_type>"---the hash table underlying - * attributes---is simply a context-dependent mapping of - * pair<unique-attribute-id, Node> to value_type using our specialized - * hash function for these pairs. - */ -template <class value_type> -class CDAttrHash : - public context::CDHashMap<std::pair<uint64_t, NodeValue*>, - value_type, - AttrHashFunction> { -public: - CDAttrHash(context::Context* ctxt) : - context::CDHashMap<std::pair<uint64_t, NodeValue*>, - value_type, - AttrHashFunction>(ctxt) { - } -};/* class CDAttrHash<> */ - -/** - * In the case of Boolean-valued attributes we have a special - * "CDAttrHash<bool>" to pack bits together in words. - */ -template <> -class CDAttrHash<bool> : - protected context::CDHashMap<NodeValue*, - uint64_t, - AttrBoolHashFunction> { - - /** A "super" type, like in Java, for easy reference below. */ - typedef context::CDHashMap<NodeValue*, uint64_t, AttrBoolHashFunction> super; - - /** - * BitAccessor allows us to return a bit "by reference." Of course, - * we don't require bit-addressibility supported by the system, we - * do it with a complex type. - */ - class BitAccessor { - - super& d_map; - - NodeValue* d_key; - - uint64_t d_word; - - unsigned d_bit; - - public: - - BitAccessor(super& map, NodeValue* key, uint64_t word, unsigned bit) : - d_map(map), - d_key(key), - d_word(word), - d_bit(bit) { - /* - Debug.printf("cdboolattr", - "CDAttrHash<bool>::BitAccessor(%p, %p, %016llx, %u)\n", - &map, key, (unsigned long long) word, bit); - */ - } - - BitAccessor& operator=(bool b) { - if(b) { - // set the bit - d_word |= (1 << d_bit); - d_map.insert(d_key, d_word); - /* - Debug.printf("cdboolattr", - "CDAttrHash<bool>::BitAccessor::set(%p, %p, %016llx, %u)\n", - &d_map, d_key, (unsigned long long) d_word, d_bit); - */ - } else { - // clear the bit - d_word &= ~(1 << d_bit); - d_map.insert(d_key, d_word); - /* - Debug.printf("cdboolattr", - "CDAttrHash<bool>::BitAccessor::clr(%p, %p, %016llx, %u)\n", - &d_map, d_key, (unsigned long long) d_word, d_bit); - */ - } - - return *this; - } - - operator bool() const { - /* - Debug.printf("cdboolattr", - "CDAttrHash<bool>::BitAccessor::toBool(%p, %p, %016llx, %u)\n", - &d_map, d_key, (unsigned long long) d_word, d_bit); - */ - return (d_word & (1 << d_bit)) ? true : false; - } - };/* class CDAttrHash<bool>::BitAccessor */ - - /** - * A (somewhat degenerate) const_iterator over boolean-valued - * attributes. This const_iterator doesn't support anything except - * comparison and dereference. It's intended just for the result of - * find() on the table. - */ - class ConstBitIterator { - - const std::pair<NodeValue* const, uint64_t> d_entry; - - unsigned d_bit; - - public: - - ConstBitIterator() : - d_entry(), - d_bit(0) { - } - - ConstBitIterator(const std::pair<NodeValue* const, uint64_t>& entry, - unsigned bit) : - d_entry(entry), - d_bit(bit) { - } - - std::pair<NodeValue* const, bool> operator*() { - return std::make_pair(d_entry.first, - (d_entry.second & (1 << d_bit)) ? true : false); - } - - bool operator==(const ConstBitIterator& b) { - return d_entry == b.d_entry && d_bit == b.d_bit; - } - };/* class CDAttrHash<bool>::ConstBitIterator */ - - /* remove non-permitted operations */ - CDAttrHash(const CDAttrHash<bool>&) CVC4_UNDEFINED; - CDAttrHash<bool>& operator=(const CDAttrHash<bool>&) CVC4_UNDEFINED; - -public: - - CDAttrHash(context::Context* context) : super(context) { } - - typedef std::pair<uint64_t, NodeValue*> key_type; - typedef bool data_type; - typedef std::pair<const key_type, data_type> value_type; - - /** an iterator type; see above for limitations */ - typedef ConstBitIterator iterator; - /** a const_iterator type; see above for limitations */ - typedef ConstBitIterator const_iterator; - - /** - * Find the boolean value in the hash table. Returns something == - * end() if not found. - */ - ConstBitIterator find(const std::pair<uint64_t, NodeValue*>& k) const { - super::const_iterator i = super::find(k.second); - if(i == super::end()) { - return ConstBitIterator(); - } - /* - Debug.printf("cdboolattr", - "underlying word at address looks like 0x%016llx, bit is %u\n", - (unsigned long long)((*i).second), - unsigned(k.first)); - */ - return ConstBitIterator(*i, k.first); - } - - /** The "off the end" const_iterator */ - ConstBitIterator end() const { - return ConstBitIterator(); - } - - /** - * Access the hash table using the underlying operator[]. Inserts - * the key into the table (associated to default value) if it's not - * already there. - */ - BitAccessor operator[](const std::pair<uint64_t, NodeValue*>& k) { - uint64_t word = super::operator[](k.second); - return BitAccessor(*this, k.second, word, k.first); - } - - /** - * Delete all flags from the given node. Simply calls superclass's - * obliterate(). Note this removes all attributes at all context - * levels for this NodeValue! This is important when the NodeValue - * is no longer referenced and is being collected, but otherwise - * it probably isn't useful to do this. - */ - void erase(NodeValue* nv) { - super::obliterate(nv); - } - - /** - * Clear the hash table. This simply exposes the protected superclass - * version of clear() to clients. - */ - void clear() { - super::clear(); - } - - /** Is the hash table empty? */ - bool empty() const { - return super::empty(); - } - - /** This is currently very misleading! */ - size_t size() const { - return super::size(); - } - -};/* class CDAttrHash<bool> */ - }/* CVC4::expr::attr namespace */ // ATTRIBUTE CLEANUP FUNCTIONS ================================================= @@ -853,17 +640,6 @@ public: };/* class Attribute<..., bool, ...> */ /** - * This is a context-dependent attribute kind (the only difference - * between CDAttribute<> and Attribute<> (with the fourth argument - * "true") is that you cannot supply a cleanup function (a no-op one - * is used). - */ -template <class T, - class value_type> -struct CDAttribute : - public Attribute<T, value_type, attr::NullCleanupStrategy, true> {}; - -/** * This is a managed attribute kind (the only difference between * ManagedAttribute<> and Attribute<> is the default cleanup function * and the fact that ManagedAttributes cannot be context-dependent). diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 327f978e4..837968aa2 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -794,9 +794,7 @@ public: } } - void nmNotifyDeleteNode(TNode n) { - d_smt.d_smtAttributes->deleteAllAttributes(n); - } + void nmNotifyDeleteNode(TNode n) {} Node applySubstitutions(TNode node) const { return Rewriter::rewrite(d_topLevelSubstitutions.apply(node)); @@ -981,14 +979,12 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_status(), d_replayStream(NULL), d_private(NULL), - d_smtAttributes(NULL), d_statisticsRegistry(NULL), d_stats(NULL), d_channels(new LemmaChannels()) { SmtScope smts(this); d_originalOptions.copyValues(em->getOptions()); - d_smtAttributes = new expr::attr::SmtAttributes(d_context); d_private = new smt::SmtEnginePrivate(*this); d_statisticsRegistry = new StatisticsRegistry(); d_stats = new SmtEngineStatistics(); @@ -1204,9 +1200,6 @@ SmtEngine::~SmtEngine() throw() { delete d_private; d_private = NULL; - delete d_smtAttributes; - d_smtAttributes = NULL; - delete d_userContext; d_userContext = NULL; delete d_context; diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 3df1dbea8..ed265e2b8 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -74,13 +74,6 @@ namespace prop { class PropEngine; }/* CVC4::prop namespace */ -namespace expr { - namespace attr { - class AttributeManager; - struct SmtAttributes; - }/* CVC4::expr::attr namespace */ -}/* CVC4::expr namespace */ - namespace smt { /** * Representation of a defined function. We keep these around in @@ -357,20 +350,9 @@ class CVC4_PUBLIC SmtEngine { // to access d_modelCommands friend class ::CVC4::Model; friend class ::CVC4::theory::TheoryModel; - // to access SmtAttributes - friend class expr::attr::AttributeManager; // to access getModel(), which is private (for now) friend class GetModelCommand; - /** - * There's something of a handshake between the expr package's - * AttributeManager and the SmtEngine because the expr package - * doesn't have a Context on its own (that's owned by the - * SmtEngine). Thus all context-dependent attributes are stored - * here. - */ - expr::attr::SmtAttributes* d_smtAttributes; - StatisticsRegistry* d_statisticsRegistry; smt::SmtEngineStatistics* d_stats; |