diff options
-rw-r--r-- | src/context/context.h | 2 | ||||
-rw-r--r-- | src/expr/node_builder.h | 16 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 8 | ||||
-rw-r--r-- | src/expr/node_manager.h | 19 | ||||
-rw-r--r-- | src/util/backtrackable.h | 44 | ||||
-rw-r--r-- | src/util/stats.cpp | 6 |
6 files changed, 63 insertions, 32 deletions
diff --git a/src/context/context.h b/src/context/context.h index aabe4e7c2..6375707b9 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -577,7 +577,7 @@ public: * ContextMemoryManager as an argument. */ void deleteSelf() { - Debug("context") << "deleteSelf(" << this << ")" << std::endl; + Debug("context") << "deleteSelf(" << this << ") " << typeid(*this).name() << std::endl; this->~ContextObj(); ::operator delete(this); } diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index cc7e89bc8..95f7c0437 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -900,8 +900,12 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() { nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading nv->d_rc = 0; setUsed(); - Debug("gc") << "creating node value " << nv - << " [" << nv->d_id << "]: " << *nv << "\n"; + if(Debug.isOn("gc")) { + Debug("gc") << "creating node value " << nv + << " [" << nv->d_id << "]: "; + nv->printAst(Debug("gc")); + Debug("gc") << std::endl; + } return nv; } @@ -982,8 +986,12 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() { //poolNv = nv; d_nm->poolInsert(nv); - Debug("gc") << "creating node value " << nv - << " [" << nv->d_id << "]: " << *nv << "\n"; + if(Debug.isOn("gc")) { + Debug("gc") << "creating node value " << nv + << " [" << nv->d_id << "]: "; + nv->printAst(Debug("gc")); + Debug("gc") << std::endl; + } return nv; } } else { diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 4cde0c624..95124d297 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -202,8 +202,12 @@ void NodeManager::reclaimZombies() { // collect ONLY IF still zero if(nv->d_rc == 0) { - Debug("gc") << "deleting node value " << nv - << " [" << nv->d_id << "]: " << *nv << "\n"; + if(Debug.isOn("gc")) { + Debug("gc") << "deleting node value " << nv + << " [" << nv->d_id << "]: "; + nv->printAst(Debug("gc")); + Debug("gc") << std::endl; + } // remove from the pool kind::MetaKind mk = nv->getMetaKind(); diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 9974df6ca..54266db13 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -185,10 +185,13 @@ class NodeManager { // if d_reclaiming is set, make sure we don't call // reclaimZombies(), because it's already running. - Debug("gc") << "zombifying node value " << nv - << " [" << nv->d_id << "]: " << *nv - << (d_inReclaimZombies ? " [CURRENTLY-RECLAIMING]" : "") - << std::endl; + if(Debug.isOn("gc")) { + Debug("gc") << "zombifying node value " << nv + << " [" << nv->d_id << "]: "; + nv->printAst(Debug("gc")); + Debug("gc") << (d_inReclaimZombies ? " [CURRENTLY-RECLAIMING]" : "") + << std::endl; + } d_zombies.insert(nv);// FIXME multithreading if(!d_inReclaimZombies) {// FIXME multithreading @@ -1269,8 +1272,12 @@ NodeClass NodeManager::mkConstInternal(const T& val) { new (&nv->d_children) T(val); poolInsert(nv); - Debug("gc") << "creating node value " << nv - << " [" << nv->d_id << "]: " << *nv << "\n"; + if(Debug.isOn("gc")) { + Debug("gc") << "creating node value " << nv + << " [" << nv->d_id << "]: "; + nv->printAst(Debug("gc")); + Debug("gc") << std::endl; + } return NodeClass(nv); } diff --git a/src/util/backtrackable.h b/src/util/backtrackable.h index b11ebf957..418172235 100644 --- a/src/util/backtrackable.h +++ b/src/util/backtrackable.h @@ -1,3 +1,4 @@ +/********************* */ /*! \file backtrackable.h ** \verbatim ** Original author: lianah @@ -12,26 +13,26 @@ ** ** \brief Contains a backtrackable list ** - ** + ** Contains a backtrackable list. **/ #include "cvc4_private.h" + #ifndef __CVC4__UTIL__BACKTRACKABLE_H #define __CVC4__UTIL__BACKTRACKABLE_H - #include <cstdlib> #include <vector> #include "context/cdo.h" -namespace CVC4{ +namespace CVC4 { template <class T> class List; template <class T> class List_iterator; template <class T> class Backtracker; template <class T> -class ListNode{ +class ListNode { private: T data; ListNode<T>* next; @@ -45,10 +46,10 @@ private: friend class List<T>; friend class List_iterator<T>; -}; /*class ListNode */ +};/* class ListNode<T> */ template <class T> -class List_iterator: public std::iterator <std::forward_iterator_tag, T> { +class List_iterator : public std::iterator <std::forward_iterator_tag, T> { friend class List<T>; public: @@ -56,17 +57,20 @@ public: List_iterator<T>& operator++(); List_iterator<T> operator++(int); bool operator!=(const List_iterator<T> & other) const; + private: const ListNode<T>* pointee; List_iterator(const ListNode<T>* p) : pointee(p) {} -}; /* class List_iterator */ +};/* class List_iterator<T> */ -template <class T> const T& List_iterator<T>::operator*() { +template <class T> +const T& List_iterator<T>::operator*() { return pointee->data; } -template <class T> List_iterator<T>& List_iterator<T>::operator++() { +template <class T> +List_iterator<T>& List_iterator<T>::operator++() { Assert(pointee != NULL); pointee = pointee->next; while(pointee != NULL && pointee->empty ) { @@ -75,19 +79,22 @@ template <class T> List_iterator<T>& List_iterator<T>::operator++() { return *this; } -template <class T> List_iterator<T> List_iterator<T>::operator++(int) { +template <class T> +List_iterator<T> List_iterator<T>::operator++(int) { List_iterator<T> it = *this; ++*this; return it; } -template <class T> bool List_iterator<T>::operator!=(const List_iterator<T>& other) const { +template <class T> +bool List_iterator<T>::operator!=(const List_iterator<T>& other) const { return (this->pointee != other.pointee); } // !! for the backtracking to work the lists must be allocated on the heap // therefore the hashmap from TNode to List<TNode> should store pointers! -template <class T> class List { +template <class T> +class List { ListNode<T>* head; ListNode<T>* tail; ListNode<T>* ptr_to_head; @@ -96,7 +103,7 @@ template <class T> class List { List (const List&) {} public: List(Backtracker<T>* b) : ptr_to_head(NULL), uninitialized(true), bck(b) { - head = tail = (ListNode<T>*)calloc(1,sizeof(ListNode<T>*)); + head = tail = (ListNode<T>*)calloc(1,sizeof(ListNode<T>)); head->next = NULL; head->empty = true; } @@ -128,7 +135,7 @@ public: } void concat(List<T>* other); void unconcat(List<T>* other); -}; /* class List */ +};/* class List */ template <class T> void List<T>::append (const T& d) { @@ -174,7 +181,8 @@ void List<T>::unconcat(List<T>* other) { /* Backtrackable Table */ -template <class T> class Backtracker { +template <class T> +class Backtracker { friend class List<T>; std::vector<std::pair<List<T>*,List<T>*> > undo_stack; @@ -187,7 +195,7 @@ public: Backtracker(context::Context* c) : undo_stack(), curr_level(0), pop_level(c, 0) {} ~Backtracker() {} -}; /*class Backtrackable */ +};/* class Backtrackable */ template <class T> void Backtracker<T>::notifyConcat(List<T>* a, List<T>* b) { curr_level++; @@ -210,5 +218,7 @@ template <class T> void Backtracker<T>::checkConsistency() { } Assert(curr_level == pop_level); } -} /* CVC4 namespace */ + +}/* CVC4 namespace */ + #endif /* __CVC4__UTIL__BACKTRACKABLE_H */ diff --git a/src/util/stats.cpp b/src/util/stats.cpp index 428f051e0..70d486ff6 100644 --- a/src/util/stats.cpp +++ b/src/util/stats.cpp @@ -32,7 +32,8 @@ StatisticsRegistry* StatisticsRegistry::current() { void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) { #ifdef CVC4_STATISTICS_ON StatSet& registeredStats = NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats; - AlwaysAssert(registeredStats.find(s) == registeredStats.end()); + AlwaysAssert(registeredStats.find(s) == registeredStats.end(), + "Statistic `%s' was already registered with this registry.", s->getName().c_str()); registeredStats.insert(s); #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::registerStat() */ @@ -40,7 +41,8 @@ void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) { void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) { #ifdef CVC4_STATISTICS_ON StatSet& registeredStats = NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats; - AlwaysAssert(registeredStats.find(s) != registeredStats.end()); + AlwaysAssert(registeredStats.find(s) != registeredStats.end(), + "Statistic `%s' was not registered with this registry.", s->getName().c_str()); registeredStats.erase(s); #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::unregisterStat() */ |