Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/context/context.cpp	Lines:	171	198	86.4 %
Date:	2021-08-13	Branches:	211	582	36.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Clark Barrett, Morgan Deters, Tim King
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Implementation of base context operations.
 */

#include <iostream>
#include <string>
#include <vector>

#include "base/check.h"
#include "context/context.h"

namespace cvc5 {
namespace context {


Context::Context() : d_pCNOpre(NULL), d_pCNOpost(NULL) {
  // Create new memory manager
  d_pCMM = new ContextMemoryManager();

  // Create initial Scope
  d_scopeList.push_back(new(d_pCMM) Scope(this, d_pCMM, 0));
}


Context::~Context() {
  // Delete all Scopes
  popto(0);

  // Delete the memory manager
  delete d_pCMM;

  // Clear ContextNotifyObj lists so there are no dangling pointers
  ContextNotifyObj* pCNO;
  while(d_pCNOpre != NULL) {
    pCNO = d_pCNOpre;
    pCNO->d_ppCNOprev = NULL;
    d_pCNOpre = pCNO->d_pCNOnext;
    pCNO->d_pCNOnext = NULL;
  }
  while(d_pCNOpost != NULL) {
    pCNO = d_pCNOpost;
    pCNO->d_ppCNOprev = NULL;
    d_pCNOpost = pCNO->d_pCNOnext;
    pCNO->d_pCNOnext = NULL;
  }
}


void Context::push() {
  Trace("pushpop") << std::string(2 * getLevel(), ' ') << "Push [to "
                   << getLevel() + 1 << "] { " << this << std::endl;

  // Create a new memory region
  d_pCMM->push();

  // Create a new top Scope
  d_scopeList.push_back(new(d_pCMM) Scope(this, d_pCMM, getLevel()+1));
}


void Context::pop() {
  Assert(getLevel() > 0) << "Cannot pop below level 0";

  // Notify the (pre-pop) ContextNotifyObj objects
  ContextNotifyObj* pCNO = d_pCNOpre;
  while(pCNO != NULL) {
    // pre-store the "next" pointer in case pCNO deletes itself on notify()
    ContextNotifyObj* next = pCNO->d_pCNOnext;
    pCNO->contextNotifyPop();
    pCNO = next;
  }

  // Grab the top Scope
  Scope* pScope = d_scopeList.back();

  // Restore the previous Scope
  d_scopeList.pop_back();

  // Restore all objects in the top Scope
  delete pScope;

  // Pop the memory region
  d_pCMM->pop();

  // Notify the (post-pop) ContextNotifyObj objects
  pCNO = d_pCNOpost;
  while(pCNO != NULL) {
    // pre-store the "next" pointer in case pCNO deletes itself on notify()
    ContextNotifyObj* next = pCNO->d_pCNOnext;
    pCNO->contextNotifyPop();
    pCNO = next;
  }

  Trace("pushpop") << std::string(2 * getLevel(), ' ') << "} Pop [to "
                   << getLevel() << "] " << this << std::endl;
}


void Context::popto(int toLevel) {
  // Pop scopes until there are none left or toLevel is reached
  if(toLevel < 0) toLevel = 0;
  while(toLevel < getLevel()) pop();
}


void Context::addNotifyObjPre(ContextNotifyObj* pCNO) {
  // Insert pCNO at *front* of list
  if(d_pCNOpre != NULL)
    d_pCNOpre->prev() = &(pCNO->next());
  pCNO->next() = d_pCNOpre;
  pCNO->prev() = &d_pCNOpre;
  d_pCNOpre = pCNO;
}


void Context::addNotifyObjPost(ContextNotifyObj* pCNO) {
  // Insert pCNO at *front* of list
  if(d_pCNOpost != NULL)
    d_pCNOpost->prev() = &(pCNO->next());
  pCNO->next() = d_pCNOpost;
  pCNO->prev() = &d_pCNOpost;
  d_pCNOpost = pCNO;
}

void ContextObj::update()
{
  Debug("context") << "before update(" << this << "):" << std::endl
                   << "context is " << getContext() << std::endl
                   << *getContext() << std::endl;

  // Call save() to save the information in the current object
  ContextObj* pContextObjSaved = save(d_pScope->getCMM());

  Debug("context") << "in update(" << this << ") with restore "
                   << pContextObjSaved << ": waypoint 1" << std::endl
                   << *getContext() << std::endl;

  // Check that base class data was saved
  Assert((pContextObjSaved->d_pContextObjNext == d_pContextObjNext
          && pContextObjSaved->d_ppContextObjPrev == d_ppContextObjPrev
          && pContextObjSaved->d_pContextObjRestore == d_pContextObjRestore
          && pContextObjSaved->d_pScope == d_pScope))
      << "save() did not properly copy information in base class";

  // Link the "saved" object in place of this ContextObj in the scope
  // we're moving it FROM.
  Debug("context") << "in update(" << this
                   << "): next() == " << next() << std::endl;
  if(next() != NULL) {
    Debug("context") << "in update(" << this
                     << "): next()->prev() == " << next()->prev() << std::endl;
    next()->prev() = &pContextObjSaved->next();
    Debug("context") << "in update(" << this
                     << "): next()->prev() is now "
                     << next()->prev() << std::endl;
  }
  Debug("context") << "in update(" << this
                   << "): prev() == " << prev() << std::endl;
  Debug("context") << "in update(" << this
                   << "): *prev() == " << *prev() << std::endl;
  *prev() = pContextObjSaved;
  Debug("context") << "in update(" << this
                   << "): *prev() is now " << *prev() << std::endl;

  Debug("context") << "in update(" << this << ") with restore "
                   << pContextObjSaved << ": waypoint 3" << std::endl
                   << *getContext() << std::endl;

  // Update Scope pointer to current top Scope
  d_pScope = d_pScope->getContext()->getTopScope();

  // Store the saved copy in the restore pointer
  d_pContextObjRestore = pContextObjSaved;

  // Insert object into the list of objects that need to be restored when this
  // Scope is popped.
  d_pScope->addToChain(this);

  Debug("context") << "after update(" << this << ") with restore "
                   << pContextObjSaved << ":" << std::endl
                   << *getContext() << std::endl;
}

ContextObj* ContextObj::restoreAndContinue()
{
  // Variable to hold next object in list
  ContextObj* pContextObjNext;

  // Check the restore pointer.  If NULL, this must be the bottom Scope
  if(d_pContextObjRestore == NULL) {
    // might not be bottom scope, since objects allocated in context
    // memory don't get linked to scope 0
    //
    // Assert(d_pScope == d_pScope->getContext()->getBottomScope()) <<
    //        "Expected bottom scope";

    Debug("context") << "NULL restore object! " << this << std::endl;
    pContextObjNext = d_pContextObjNext;
    d_pScope = nullptr;

    // Nothing else to do
  } else {
    // Call restore to update the subclass data
    restore(d_pContextObjRestore);

    // Remember the next object in the list
    pContextObjNext = d_pContextObjNext;

    // Restore the base class data
    d_pScope = d_pContextObjRestore->d_pScope;
    next() = d_pContextObjRestore->d_pContextObjNext;
    prev() = d_pContextObjRestore->d_ppContextObjPrev;
    d_pContextObjRestore = d_pContextObjRestore->d_pContextObjRestore;

    // Re-link this ContextObj to the list in this scope
    if(next() != NULL) {
      next()->prev() = &next();
    }
    *prev() = this;
  }

  // Return the next object in the list
  return pContextObjNext;
}

void ContextObj::destroy()
{
  /* The object to destroy must be valid, i.e., its current state must belong
   * to a scope. We remove the object and its previous versions from their
   * respective scopes below. If this assertion is failing, you may have
   * created an object at a non-zero level and let it outlive the destruction
   * of that level. */
  Assert(d_pScope != nullptr);
  /* Context can be big and complicated, so we only want to process this output
   * if we're really going to use it. (Same goes below.) */
  Debug("context") << "before destroy " << this << " (level " << getLevel()
                   << "):" << std::endl << *getContext() << std::endl;

  for (;;)
  {
    // If valgrind reports invalid writes on the next few lines,
    // here's a hint: make sure all classes derived from ContextObj in
    // the system properly call destroy() in their destructors.
    // That's needed to maintain this linked list properly.
    if (next() != nullptr)
    {
      next()->prev() = prev();
    }
    *prev() = next();
    if (d_pContextObjRestore == nullptr)
    {
      break;
    }
    Debug("context") << "in destroy " << this << ", restore object is "
                     << d_pContextObjRestore << " at level "
                     << d_pContextObjRestore->getLevel() << ":" << std::endl
                     << *getContext() << std::endl;
    restoreAndContinue();
  }
  Debug("context") << "after destroy " << this << ":" << std::endl
                   << *getContext() << std::endl;
}


ContextObj::ContextObj(Context* pContext) :
  d_pScope(NULL),
  d_pContextObjRestore(NULL),
  d_pContextObjNext(NULL),
  d_ppContextObjPrev(NULL) {
  Assert(pContext != NULL) << "NULL context pointer";

  Debug("context") << "create new ContextObj(" << this << " inCMM=false)" << std::endl;
  d_pScope = pContext->getBottomScope();
  d_pScope->addToChain(this);
}


ContextObj::ContextObj(bool allocatedInCMM, Context* pContext) :
  d_pScope(NULL),
  d_pContextObjRestore(NULL),
  d_pContextObjNext(NULL),
  d_ppContextObjPrev(NULL) {
  Assert(pContext != NULL) << "NULL context pointer";

  Debug("context") << "create new ContextObj(" << this << " inCMM=" << allocatedInCMM << ")" << std::endl;
  if(allocatedInCMM) {
    d_pScope = pContext->getTopScope();
  } else {
    d_pScope = pContext->getBottomScope();
  }
  d_pScope->addToChain(this);
}

void ContextObj::enqueueToGarbageCollect() {
  Assert(d_pScope != NULL);
  d_pScope->enqueueToGarbageCollect(this);
}

ContextNotifyObj::ContextNotifyObj(Context* pContext, bool preNotify) {
  if(preNotify) {
    pContext->addNotifyObjPre(this);
  } else {
    pContext->addNotifyObjPost(this);
  }
}


ContextNotifyObj::~ContextNotifyObj() {
  if(d_pCNOnext != NULL) {
    d_pCNOnext->d_ppCNOprev = d_ppCNOprev;
  }
  if(d_ppCNOprev != NULL) {
    *d_ppCNOprev = d_pCNOnext;
  }
}

std::ostream& operator<<(std::ostream& out, const Context& context)
{
  static const std::string separator(79, '-');

  int level = context.d_scopeList.size() - 1;
  typedef std::vector<Scope*>::const_reverse_iterator const_reverse_iterator;
  for(const_reverse_iterator i = context.d_scopeList.rbegin();
      i != context.d_scopeList.rend();
      ++i, --level) {
    Scope* pScope = *i;
    Assert(pScope->getLevel() == level);
    Assert(pScope->getContext() == &context);
    out << separator << std::endl
        << *pScope << std::endl;
  }
  return out << separator << std::endl;
}

std::ostream& operator<<(std::ostream& out, const Scope& scope)
{
  out << "Scope " << scope.d_level << " [" << &scope << "]:";
  ContextObj* pContextObj = scope.d_pContextObjList;
  Assert(pContextObj == NULL
         || pContextObj->prev() == &scope.d_pContextObjList);
  while(pContextObj != NULL) {
    out << " <--> " << pContextObj;
    if(pContextObj->d_pScope != &scope) {
      out << " XXX bad scope" << std::endl;
    }
    Assert(pContextObj->d_pScope == &scope);
    Assert(pContextObj->next() == NULL
           || pContextObj->next()->prev() == &pContextObj->next());
    pContextObj = pContextObj->next();
  }
  return out << " --> NULL";
}

Scope::~Scope() {
  // Call restore() method on each ContextObj object in the list.
  // Note that it is the responsibility of restore() to return the
  // next item in the list.
  while (d_pContextObjList != NULL) {
    d_pContextObjList = d_pContextObjList->restoreAndContinue();
  }

  if (d_garbage) {
    while (!d_garbage->empty()) {
      ContextObj* obj = d_garbage->back();
      d_garbage->pop_back();
      obj->deleteSelf();
    }
  }
}

void Scope::enqueueToGarbageCollect(ContextObj* obj) {
  if (!d_garbage) {
    d_garbage.reset(new std::vector<ContextObj*>);
  }
  d_garbage->push_back(obj);
}

}  // namespace context
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Clark Barrett, Morgan Deters, Tim King
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Implementation of base context operations.
14		*/
15
16		#include <iostream>
17		#include <string>
18		#include <vector>
19
20		#include "base/check.h"
21		#include "context/context.h"
22
23		namespace cvc5 {
24		namespace context {
25
26
27	1886198	Context::Context() : d_pCNOpre(NULL), d_pCNOpost(NULL) {
28		// Create new memory manager
29	1886198	d_pCMM = new ContextMemoryManager();
30
31		// Create initial Scope
32	1886198	d_scopeList.push_back(new(d_pCMM) Scope(this, d_pCMM, 0));
33	1886198	}
34
35
36	3772396	Context::~Context() {
37		// Delete all Scopes
38	1886198	popto(0);
39
40		// Delete the memory manager
41	1886198	delete d_pCMM;
42
43		// Clear ContextNotifyObj lists so there are no dangling pointers
44		ContextNotifyObj* pCNO;
45	1886202	while(d_pCNOpre != NULL) {
46	2	pCNO = d_pCNOpre;
47	2	pCNO->d_ppCNOprev = NULL;
48	2	d_pCNOpre = pCNO->d_pCNOnext;
49	2	pCNO->d_pCNOnext = NULL;
50		}
51	1886202	while(d_pCNOpost != NULL) {
52	2	pCNO = d_pCNOpost;
53	2	pCNO->d_ppCNOprev = NULL;
54	2	d_pCNOpost = pCNO->d_pCNOnext;
55	2	pCNO->d_pCNOnext = NULL;
56		}
57	1886198	}
58
59
60	3457690	void Context::push() {
61	6915380	Trace("pushpop") << std::string(2 * getLevel(), ' ') << "Push [to "
62	3457690	<< getLevel() + 1 << "] { " << this << std::endl;
63
64		// Create a new memory region
65	3457690	d_pCMM->push();
66
67		// Create a new top Scope
68	3457690	d_scopeList.push_back(new(d_pCMM) Scope(this, d_pCMM, getLevel()+1));
69	3457690	}
70
71
72	3457690	void Context::pop() {
73	3457690	Assert(getLevel() > 0) << "Cannot pop below level 0";
74
75		// Notify the (pre-pop) ContextNotifyObj objects
76	3457690	ContextNotifyObj* pCNO = d_pCNOpre;
77	3457718	while(pCNO != NULL) {
78		// pre-store the "next" pointer in case pCNO deletes itself on notify()
79	14	ContextNotifyObj* next = pCNO->d_pCNOnext;
80	14	pCNO->contextNotifyPop();
81	14	pCNO = next;
82		}
83
84		// Grab the top Scope
85	3457690	Scope* pScope = d_scopeList.back();
86
87		// Restore the previous Scope
88	3457690	d_scopeList.pop_back();
89
90		// Restore all objects in the top Scope
91	3457690	delete pScope;
92
93		// Pop the memory region
94	3457690	d_pCMM->pop();
95
96		// Notify the (post-pop) ContextNotifyObj objects
97	3457690	pCNO = d_pCNOpost;
98	99379534	while(pCNO != NULL) {
99		// pre-store the "next" pointer in case pCNO deletes itself on notify()
100	47960922	ContextNotifyObj* next = pCNO->d_pCNOnext;
101	47960922	pCNO->contextNotifyPop();
102	47960922	pCNO = next;
103		}
104
105	6915380	Trace("pushpop") << std::string(2 * getLevel(), ' ') << "} Pop [to "
106	3457690	<< getLevel() << "] " << this << std::endl;
107	3457690	}
108
109
110	1907332	void Context::popto(int toLevel) {
111		// Pop scopes until there are none left or toLevel is reached
112	1907332	if(toLevel < 0) toLevel = 0;
113	1928378	while(toLevel < getLevel()) pop();
114	1907332	}
115
116
117	8	void Context::addNotifyObjPre(ContextNotifyObj* pCNO) {
118		// Insert pCNO at front of list
119	8	if(d_pCNOpre != NULL)
120	2	d_pCNOpre->prev() = &(pCNO->next());
121	8	pCNO->next() = d_pCNOpre;
122	8	pCNO->prev() = &d_pCNOpre;
123	8	d_pCNOpre = pCNO;
124	8	}
125
126
127	328714	void Context::addNotifyObjPost(ContextNotifyObj* pCNO) {
128		// Insert pCNO at front of list
129	328714	if(d_pCNOpost != NULL)
130	240999	d_pCNOpost->prev() = &(pCNO->next());
131	328714	pCNO->next() = d_pCNOpost;
132	328714	pCNO->prev() = &d_pCNOpost;
133	328714	d_pCNOpost = pCNO;
134	328714	}
135
136	114705396	void ContextObj::update()
137		{
138	229410792	Debug("context") << "before update(" << this << "):" << std::endl
139	229410792	<< "context is " << getContext() << std::endl
140	114705396	<< *getContext() << std::endl;
141
142		// Call save() to save the information in the current object
143	114705396	ContextObj* pContextObjSaved = save(d_pScope->getCMM());
144
145	229410792	Debug("context") << "in update(" << this << ") with restore "
146	114705396	<< pContextObjSaved << ": waypoint 1" << std::endl
147	114705396	<< *getContext() << std::endl;
148
149		// Check that base class data was saved
150	114705396	Assert((pContextObjSaved->d_pContextObjNext == d_pContextObjNext
151		&& pContextObjSaved->d_ppContextObjPrev == d_ppContextObjPrev
152		&& pContextObjSaved->d_pContextObjRestore == d_pContextObjRestore
153		&& pContextObjSaved->d_pScope == d_pScope))
154		<< "save() did not properly copy information in base class";
155
156		// Link the "saved" object in place of this ContextObj in the scope
157		// we're moving it FROM.
158	229410792	Debug("context") << "in update(" << this
159	114705396	<< "): next() == " << next() << std::endl;
160	114705396	if(next() != NULL) {
161	223665828	Debug("context") << "in update(" << this
162	111832914	<< "): next()->prev() == " << next()->prev() << std::endl;
163	111832914	next()->prev() = &pContextObjSaved->next();
164	223665828	Debug("context") << "in update(" << this
165	111832914	<< "): next()->prev() is now "
166	111832914	<< next()->prev() << std::endl;
167		}
168	229410792	Debug("context") << "in update(" << this
169	114705396	<< "): prev() == " << prev() << std::endl;
170	229410792	Debug("context") << "in update(" << this
171	114705396	<< "): prev() == " << prev() << std::endl;
172	114705396	*prev() = pContextObjSaved;
173	229410792	Debug("context") << "in update(" << this
174	114705396	<< "): prev() is now " << prev() << std::endl;
175
176	229410792	Debug("context") << "in update(" << this << ") with restore "
177	114705396	<< pContextObjSaved << ": waypoint 3" << std::endl
178	114705396	<< *getContext() << std::endl;
179
180		// Update Scope pointer to current top Scope
181	114705396	d_pScope = d_pScope->getContext()->getTopScope();
182
183		// Store the saved copy in the restore pointer
184	114705396	d_pContextObjRestore = pContextObjSaved;
185
186		// Insert object into the list of objects that need to be restored when this
187		// Scope is popped.
188	114705396	d_pScope->addToChain(this);
189
190	229410792	Debug("context") << "after update(" << this << ") with restore "
191	114705396	<< pContextObjSaved << ":" << std::endl
192	114705396	<< *getContext() << std::endl;
193	114705396	}
194
195	114705396	ContextObj* ContextObj::restoreAndContinue()
196		{
197		// Variable to hold next object in list
198		ContextObj* pContextObjNext;
199
200		// Check the restore pointer. If NULL, this must be the bottom Scope
201	114705396	if(d_pContextObjRestore == NULL) {
202		// might not be bottom scope, since objects allocated in context
203		// memory don't get linked to scope 0
204		//
205		// Assert(d_pScope == d_pScope->getContext()->getBottomScope()) <<
206		// "Expected bottom scope";
207
208		Debug("context") << "NULL restore object! " << this << std::endl;
209		pContextObjNext = d_pContextObjNext;
210		d_pScope = nullptr;
211
212		// Nothing else to do
213		} else {
214		// Call restore to update the subclass data
215	114705396	restore(d_pContextObjRestore);
216
217		// Remember the next object in the list
218	114705396	pContextObjNext = d_pContextObjNext;
219
220		// Restore the base class data
221	114705396	d_pScope = d_pContextObjRestore->d_pScope;
222	114705396	next() = d_pContextObjRestore->d_pContextObjNext;
223	114705396	prev() = d_pContextObjRestore->d_ppContextObjPrev;
224	114705396	d_pContextObjRestore = d_pContextObjRestore->d_pContextObjRestore;
225
226		// Re-link this ContextObj to the list in this scope
227	114705396	if(next() != NULL) {
228	111832134	next()->prev() = &next();
229		}
230	114705396	*prev() = this;
231		}
232
233		// Return the next object in the list
234	114705396	return pContextObjNext;
235		}
236
237	77412875	void ContextObj::destroy()
238		{
239		/* The object to destroy must be valid, i.e., its current state must belong
240		* to a scope. We remove the object and its previous versions from their
241		* respective scopes below. If this assertion is failing, you may have
242		* created an object at a non-zero level and let it outlive the destruction
243		* of that level. */
244	77412875	Assert(d_pScope != nullptr);
245		/* Context can be big and complicated, so we only want to process this output
246		* if we're really going to use it. (Same goes below.) */
247	154825750	Debug("context") << "before destroy " << this << " (level " << getLevel()
248	77412875	<< "):" << std::endl << *getContext() << std::endl;
249
250		for (;;)
251		{
252		// If valgrind reports invalid writes on the next few lines,
253		// here's a hint: make sure all classes derived from ContextObj in
254		// the system properly call destroy() in their destructors.
255		// That's needed to maintain this linked list properly.
256	77812759	if (next() != nullptr)
257		{
258	73058128	next()->prev() = prev();
259		}
260	77612817	*prev() = next();
261	77612817	if (d_pContextObjRestore == nullptr)
262		{
263	77412875	break;
264		}
265	399884	Debug("context") << "in destroy " << this << ", restore object is "
266	199942	<< d_pContextObjRestore << " at level "
267	399884	<< d_pContextObjRestore->getLevel() << ":" << std::endl
268	199942	<< *getContext() << std::endl;
269	199942	restoreAndContinue();
270		}
271	154825750	Debug("context") << "after destroy " << this << ":" << std::endl
272	77412875	<< *getContext() << std::endl;
273	77412875	}
274
275
276	8205181	ContextObj::ContextObj(Context* pContext) :
277		d_pScope(NULL),
278		d_pContextObjRestore(NULL),
279		d_pContextObjNext(NULL),
280	8205181	d_ppContextObjPrev(NULL) {
281	8205181	Assert(pContext != NULL) << "NULL context pointer";
282
283	8205181	Debug("context") << "create new ContextObj(" << this << " inCMM=false)" << std::endl;
284	8205181	d_pScope = pContext->getBottomScope();
285	8205181	d_pScope->addToChain(this);
286	8205181	}
287
288
289	69207694	ContextObj::ContextObj(bool allocatedInCMM, Context* pContext) :
290		d_pScope(NULL),
291		d_pContextObjRestore(NULL),
292		d_pContextObjNext(NULL),
293	69207694	d_ppContextObjPrev(NULL) {
294	69207694	Assert(pContext != NULL) << "NULL context pointer";
295
296	69207694	Debug("context") << "create new ContextObj(" << this << " inCMM=" << allocatedInCMM << ")" << std::endl;
297	69207694	if(allocatedInCMM) {
298	2	d_pScope = pContext->getTopScope();
299		} else {
300	69207692	d_pScope = pContext->getBottomScope();
301		}
302	69207694	d_pScope->addToChain(this);
303	69207694	}
304
305	56582525	void ContextObj::enqueueToGarbageCollect() {
306	56582525	Assert(d_pScope != NULL);
307	56582525	d_pScope->enqueueToGarbageCollect(this);
308	56582525	}
309
310	328722	ContextNotifyObj::ContextNotifyObj(Context* pContext, bool preNotify) {
311	328722	if(preNotify) {
312	8	pContext->addNotifyObjPre(this);
313		} else {
314	328714	pContext->addNotifyObjPost(this);
315		}
316	328722	}
317
318
319	657444	ContextNotifyObj::~ContextNotifyObj() {
320	328722	if(d_pCNOnext != NULL) {
321	204671	d_pCNOnext->d_ppCNOprev = d_ppCNOprev;
322		}
323	328722	if(d_ppCNOprev != NULL) {
324	328718	*d_ppCNOprev = d_pCNOnext;
325		}
326	328722	}
327
328		std::ostream& operator<<(std::ostream& out, const Context& context)
329		{
330		static const std::string separator(79, '-');
331
332		int level = context.d_scopeList.size() - 1;
333		typedef std::vector<Scope*>::const_reverse_iterator const_reverse_iterator;
334		for(const_reverse_iterator i = context.d_scopeList.rbegin();
335		i != context.d_scopeList.rend();
336		++i, --level) {
337		Scope* pScope = *i;
338		Assert(pScope->getLevel() == level);
339		Assert(pScope->getContext() == &context);
340		out << separator << std::endl
341		<< *pScope << std::endl;
342		}
343		return out << separator << std::endl;
344		}
345
346		std::ostream& operator<<(std::ostream& out, const Scope& scope)
347		{
348		out << "Scope " << scope.d_level << " [" << &scope << "]:";
349		ContextObj* pContextObj = scope.d_pContextObjList;
350		Assert(pContextObj == NULL
351		\|\| pContextObj->prev() == &scope.d_pContextObjList);
352		while(pContextObj != NULL) {
353		out << " <--> " << pContextObj;
354		if(pContextObj->d_pScope != &scope) {
355		out << " XXX bad scope" << std::endl;
356		}
357		Assert(pContextObj->d_pScope == &scope);
358		Assert(pContextObj->next() == NULL
359		\|\| pContextObj->next()->prev() == &pContextObj->next());
360		pContextObj = pContextObj->next();
361		}
362		return out << " --> NULL";
363		}
364
365	121420834	Scope::~Scope() {
366		// Call restore() method on each ContextObj object in the list.
367		// Note that it is the responsibility of restore() to return the
368		// next item in the list.
369	232468598	while (d_pContextObjList != NULL) {
370	114505454	d_pContextObjList = d_pContextObjList->restoreAndContinue();
371		}
372
373	3457690	if (d_garbage) {
374	115341111	while (!d_garbage->empty()) {
375	56582525	ContextObj* obj = d_garbage->back();
376	56582525	d_garbage->pop_back();
377	56582525	obj->deleteSelf();
378		}
379		}
380	3457690	}
381
382	56582525	void Scope::enqueueToGarbageCollect(ContextObj* obj) {
383	56582525	if (!d_garbage) {
384	2176061	d_garbage.reset(new std::vector<ContextObj*>);
385		}
386	56582525	d_garbage->push_back(obj);
387	56582525	}
388
389		} // namespace context
390	29346	} // namespace cvc5