Fixed compile errors

diff --git a/src/context/context.cpp b/src/context/context.cpp
index 5729c22838f93d2c46893475f8aab7a631b23039..76cc03666ec3d295e2c666fbfc69fb7e7cc9dd92 100644 (file)
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -21,12 +21,12 @@ namespace CVC4 {
 namespace context {
 
 
-Context::Context() : d_pContextNotifyObj(NULL) {
+Context::Context() : d_pCNOpre(NULL), d_pCNOpost(NULL) {
   // Create new memory manager
   d_pCMM = new ContextMemoryManager();
 
   // Create initial Scope
-  d_pScopeTop = new(cmm) Scope(this, cmm);
+  d_pScopeTop = new(d_pCMM) Scope(this, d_pCMM);
   d_pScopeBottom = d_pScopeTop;
 }
 
@@ -43,13 +43,13 @@ Context::~Context() {
   while (d_pCNOpre != NULL) {
     pCNO = d_pCNOpre;
     pCNO->d_ppCNOprev = NULL;
-    d_pContextNotifyObj = pCNO->d_pCNOnext;
+    d_pCNOpre = pCNO->d_pCNOnext;
     pCNO->d_pCNOnext = NULL;
   }
   while (d_pCNOpost != NULL) {
     pCNO = d_pCNOpost;
     pCNO->d_ppCNOprev = NULL;
-    d_pContextNotifyObj = pCNO->d_pCNOnext;
+    d_pCNOpost = pCNO->d_pCNOnext;
     pCNO->d_pCNOnext = NULL;
   }
 }
@@ -68,7 +68,7 @@ void Context::push() {
 
 void Context::pop() {
   // Notify the (pre-pop) ContextNotifyObj objects
-  ContextNotifyObj* pCNO = d_pCNOPre;
+  ContextNotifyObj* pCNO = d_pCNOpre;
   while (pCNO != NULL) {
     pCNO->notify();
     pCNO = pCNO->d_pCNOnext;
@@ -81,13 +81,13 @@ void Context::pop() {
   d_pScopeTop = pScope->getScopePrev();
 
   // Restore all objects in the top Scope
-  delete(d_pCMM) pScope;
+  delete pScope;
 
   // Pop the memory region
   d_pCMM->pop();
 
   // Notify the (post-pop) ContextNotifyObj objects
-  ContextNotifyObj* pCNO = d_pCNOPost;
+  pCNO = d_pCNOpost;
   while (pCNO != NULL) {
     pCNO->notify();
     pCNO = pCNO->d_pCNOnext;
@@ -99,7 +99,7 @@ void Context::pop() {
 
 void Context::popto(int toLevel) {
   // Pop scopes until there are none left or toLevel is reached
-  while (d_pScopeTop != NULL && toLevel < d_pScopeTop()->getLevel()) pop();
+  while (d_pScopeTop != NULL && toLevel < d_pScopeTop->getLevel()) pop();
 }
 
 
@@ -168,7 +168,7 @@ ContextObj* ContextObj::restoreAndContinue()
     // Restore the base class data
     d_pScope = d_pContextObjRestore->d_pScope;
     next() = d_pContextObjRestore->d_pContextObjNext;
-    prev() = d_pContextObjRestore->d_pContextObjPrev;
+    prev() = d_pContextObjRestore->d_ppContextObjPrev;
     d_pContextObjRestore = d_pContextObjRestore->d_pContextObjRestore;
   }
   // Return the next object in the list
@@ -198,7 +198,7 @@ ContextObj::~ContextObj()
 }
 
 
-ContextNotifyObj::ContextNotifyObj(Context* pContext, bool preNotify = false) {
+ContextNotifyObj::ContextNotifyObj(Context* pContext, bool preNotify) {
   if (preNotify) {
     pContext->addNotifyObjPre(this);
   }
@@ -211,10 +211,10 @@ ContextNotifyObj::ContextNotifyObj(Context* pContext, bool preNotify = false) {
 ContextNotifyObj::~ContextNotifyObj()
 {
   if (d_pCNOnext != NULL) {
-    d_pCNOnext->d_pCNOprev = d_pCNOprev;
+    d_pCNOnext->d_ppCNOprev = d_ppCNOprev;
   }
-  if (d_pCNOprev != NULL) {
-    *(d_pCNOprev) = d_pCNOnext;
+  if (d_ppCNOprev != NULL) {
+    *(d_ppCNOprev) = d_pCNOnext;
   }
 }
 

diff --git a/src/context/context.h b/src/context/context.h
index 6c9f01acfae33b3bae262624ec7e142833ed2f1e..114c8ed69176276e8248f7ebd13131c7c56a0bf6 100644 (file)
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -16,6 +16,8 @@
 #ifndef __CVC4__CONTEXT__CONTEXT_H
 #define __CVC4__CONTEXT__CONTEXT_H
 
+#include "context/context_mm.h"
+
 namespace CVC4 {
 namespace context {
 
@@ -182,7 +184,7 @@ public:
    */
   Scope(Context* pContext, ContextMemoryManager* pCMM,
         Scope* pScopePrev = NULL)
-    : d_pContext(context), d_pCMM(pCMM), d_pScopePrev(pScopePrev),
+    : d_pContext(pContext), d_pCMM(pCMM), d_pScopePrev(pScopePrev),
       d_level(0), d_pContextObjList(NULL)
     { if (pScopePrev != NULL) d_level = pScopePrev->getLevel() + 1; }
 
@@ -237,7 +239,7 @@ public:
    * ContextMemoryManager.  No need to do anything because memory is freed
    * automatically when the ContextMemoryManager pop() method is called.
    */
-  void operator delete(void* pMem, ContextMemoryManager* pCMM) {}
+  void operator delete(void* pMem) {}
 
   //FIXME:  //! Check for memory leaks
   //  void check(void);
@@ -374,7 +376,7 @@ class ContextNotifyObj {
    * Context is our friend so that when the Context is deleted, any remaining
    * ContextNotifyObj can be removed from the Context list.
    */
-  friend Context;
+  friend class Context;
 
   /**
    * Pointer to next ContextNotifyObject in this List
@@ -386,6 +388,18 @@ class ContextNotifyObj {
    */
   ContextNotifyObj** d_ppCNOprev;
 
+  /**
+   * Return reference to next link in ContextNotifyObj list.  Used by
+   * Context::addNotifyObj methods.
+   */
+  ContextNotifyObj*& next() { return d_pCNOnext; }
+
+  /**
+   * Return reference to prev link in ContextNotifyObj list.  Used by
+   * Context::addNotifyObj methods.
+   */
+  ContextNotifyObj**& prev() { return d_ppCNOprev; }
+
 public:
   /**
    * Constructor for ContextNotifyObj.  Parameters are the context to which
@@ -412,7 +426,7 @@ public:
 
 inline int Context::getLevel() const { return getTopScope()->getLevel(); }
 
-inline void Scope::~Scope() {
+inline 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.
@@ -421,7 +435,7 @@ inline void Scope::~Scope() {
   }
 }
 
-inline void Scope::addToChain(ContextObjChain* pContextObj) {
+inline void Scope::addToChain(ContextObj* pContextObj) {
   if(d_pContextObjList != NULL)
     d_pContextObjList->prev() = &(pContextObj->next());
   pContextObj->next() = d_pContextObjList;

diff --git a/src/context/context_mm.h b/src/context/context_mm.h
index af524a51ffdd0e72f3eb7b730476f545dffb9279..8c870c603ac6b7b27516bd024311f2d55dd3c6b6 100644 (file)
--- a/src/context/context_mm.h
+++ b/src/context/context_mm.h
@@ -17,6 +17,9 @@
 #ifndef __CVC4__CONTEXT__CONTEXT_MM_H
 #define __CVC4__CONTEXT__CONTEXT_MM_H
 
+#include <vector>
+#include <deque>
+
 namespace CVC4 {
 namespace context {