Also, some debugging improvements.
* 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);
}
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;
}
//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 {
// 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();
// 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
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);
}
+/********************* */
/*! \file backtrackable.h
** \verbatim
** Original author: lianah
**
** \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;
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:
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 ) {
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;
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;
}
}
void concat(List<T>* other);
void unconcat(List<T>* other);
-}; /* class List */
+};/* class List */
template <class T>
void List<T>::append (const T& d) {
/* 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;
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++;
}
Assert(curr_level == pop_level);
}
-} /* CVC4 namespace */
+
+}/* CVC4 namespace */
+
#endif /* __CVC4__UTIL__BACKTRACKABLE_H */
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() */
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() */