From: Clark Barrett Date: Fri, 29 Jan 2010 21:02:15 +0000 (+0000) Subject: Fixed compile errors X-Git-Tag: cvc5-1.0.0~9326 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c732da16287657609a80734b29ab785698960672;p=cvc5.git Fixed compile errors --- diff --git a/src/context/context.cpp b/src/context/context.cpp index 5729c2283..76cc03666 100644 --- 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 6c9f01acf..114c8ed69 100644 --- 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 af524a51f..8c870c603 100644 --- 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 +#include + namespace CVC4 { namespace context {