00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022 #ifndef _cvc3__include__context_h_
00023 #define _cvc3__include__context_h_
00024
00025 #include <string>
00026 #include <vector>
00027 #include "debug.h"
00028 #include "memory_manager_context.h"
00029
00030 namespace CVC3 {
00031
00032
00033
00034
00035
00036
00037
00038
00039
00040 class Context;
00041 class ContextManager;
00042 class ContextNotifyObj;
00043 class ContextObj;
00044 class ContextObjChain;
00045
00046
00047
00048
00049
00050
00051
00052
00053
00054
00055
00056
00057
00058 class Scope {
00059 friend class ContextObj;
00060 friend class ContextObjChain;
00061 friend class CDFlags;
00062
00063 Context* d_context;
00064
00065
00066 ContextMemoryManager* d_cmm;
00067
00068
00069 Scope* d_prevScope;
00070
00071
00072 int d_level;
00073
00074
00075
00076 ContextObjChain* d_restoreChain;
00077
00078
00079 void addToChain(ContextObjChain* obj);
00080
00081 public:
00082
00083 Scope(Context* context, ContextMemoryManager* cmm,
00084 Scope* prevScope = NULL)
00085 : d_context(context), d_cmm(cmm), d_prevScope(prevScope),
00086 d_restoreChain(NULL)
00087 { if (prevScope) d_level = prevScope->level() + 1; else d_level = 0; }
00088
00089 ~Scope() {}
00090
00091
00092 Scope* prevScope() const { return d_prevScope; }
00093 int level(void) const { return d_level; }
00094 bool isCurrent(void) const;
00095 Scope* topScope() const;
00096 Context* getContext() const { return d_context; }
00097 ContextMemoryManager* getCMM() const { return d_cmm; }
00098
00099 void* operator new(size_t size, MemoryManager* mm)
00100 { return mm->newData(size); }
00101 void operator delete(void* pMem, MemoryManager* mm) {
00102 mm->deleteData(pMem);
00103 }
00104 void operator delete(void*) { }
00105
00106
00107 void restore(void);
00108
00109
00110 void finalize(void);
00111
00112
00113 void check(void);
00114 };
00115
00116
00117
00118
00119
00120
00121
00122
00123
00124
00125
00126
00127
00128 class ContextObjChain {
00129 friend class Scope;
00130 friend class ContextObj;
00131 friend class CDFlags;
00132 private:
00133
00134 ContextObjChain* d_restoreChainNext;
00135
00136
00137
00138
00139 ContextObjChain** d_restoreChainPrev;
00140
00141
00142 ContextObjChain* d_restore;
00143
00144
00145 ContextObj* d_data;
00146
00147
00148 ContextObj* d_master;
00149
00150
00151 ContextObjChain(ContextObj* data, ContextObj* master,
00152 ContextObjChain* restore)
00153 : d_restoreChainNext(NULL), d_restoreChainPrev(NULL),
00154 d_restore(restore), d_data(data), d_master(master)
00155 { }
00156
00157
00158 ContextObjChain* restore(void);
00159 public:
00160
00161 ~ContextObjChain() {}
00162
00163 void* operator new(size_t size, MemoryManager* mm) {
00164 return mm->newData(size);
00165 }
00166 void operator delete(void* pMem, MemoryManager* mm) {
00167 mm->deleteData(pMem);
00168 }
00169
00170 void operator delete(void*) { }
00171
00172
00173
00174 void* operator new(size_t size, bool b) {
00175 return malloc(size);
00176 }
00177 void operator delete(void* pMem, bool b) {
00178 free(pMem);
00179 }
00180
00181 IF_DEBUG(std::string name() const;)
00182 };
00183
00184
00185
00186
00187
00188
00189
00190
00191
00192
00193
00194
00195 class CVC_DLL ContextObj {
00196 friend class Scope;
00197 friend class ContextObjChain;
00198 friend class CDFlags;
00199 private:
00200
00201 Scope* d_scope;
00202
00203
00204
00205 ContextObjChain* d_restore;
00206
00207 IF_DEBUG(std::string d_name);
00208 IF_DEBUG(bool d_active);
00209
00210
00211 void update(int scope = -1);
00212
00213 protected:
00214
00215 ContextObj(const ContextObj& co)
00216 : d_scope(co.d_scope), d_restore(co.d_restore) {
00217 IF_DEBUG(d_name=co.d_name);
00218 DebugAssert(co.d_active, "ContextObj["+co.name()+"] copy constructor");
00219 IF_DEBUG(d_active = co.d_active);
00220
00221 }
00222
00223
00224 ContextObj& operator=(const ContextObj& co) {
00225 DebugAssert(false, "ContextObj::operator=(): shouldn't be called");
00226 return *this;
00227 }
00228
00229
00230
00231 virtual ContextObj* makeCopy(ContextMemoryManager* cmm) = 0;
00232
00233
00234 virtual void restoreData(ContextObj* data) {
00235 FatalAssert(false,
00236 "ContextObj::restoreData(): call in the base abstract class");
00237 }
00238
00239 const ContextObj* getRestore() {
00240 return d_restore ? d_restore->d_data : NULL;
00241 }
00242
00243
00244 virtual void setNull(void) = 0;
00245
00246
00247 IF_DEBUG(virtual std::string name() const { return d_name; });
00248
00249
00250 ContextMemoryManager* getCMM() { return d_scope->getCMM(); }
00251
00252 public:
00253
00254
00255
00256
00257
00258
00259
00260
00261 ContextObj(Context* context, bool atBottomScope = true);
00262 virtual ~ContextObj();
00263
00264 int level() const { return (d_scope==NULL)? 0 : d_scope->level(); }
00265 bool isCurrent(int scope = -1) const {
00266 if(scope >= 0) return d_scope->level() == scope;
00267 else return d_scope->isCurrent();
00268 }
00269 void makeCurrent(int scope = -1) { if (!isCurrent(scope)) update(scope); }
00270 IF_DEBUG(void setName(const std::string& name) { d_name=name; });
00271
00272 void* operator new(size_t size, MemoryManager* mm) {
00273 return mm->newData(size);
00274 }
00275 void operator delete(void* pMem, MemoryManager* mm) {
00276 mm->deleteData(pMem);
00277 }
00278
00279
00280
00281 void* operator new(size_t size, bool b) {
00282 return malloc(size);
00283 }
00284 void operator delete(void* pMem, bool b) {
00285 free(pMem);
00286 }
00287
00288 void operator delete(void*) { }
00289 };
00290
00291
00292
00293
00294
00295
00296
00297
00298
00299
00300
00301 class Context {
00302
00303 ContextManager* d_cm;
00304
00305
00306 std::string d_name;
00307
00308
00309 int d_id;
00310
00311
00312 Scope* d_topScope;
00313 Scope* d_bottomScope;
00314
00315
00316 std::vector<ContextNotifyObj*> d_notifyObjList;
00317
00318
00319 std::vector<ContextMemoryManager*> d_cmmStack;
00320
00321 public:
00322 Context(ContextManager* cm, const std::string& name, int id);
00323 ~Context();
00324
00325
00326 ContextManager* getCM() const { return d_cm; }
00327 const std::string& name() const { return d_name; }
00328 int id() const { return d_id; }
00329 Scope* topScope() const { return d_topScope; }
00330 Scope* bottomScope() const { return d_bottomScope; }
00331 int level() const { return d_topScope->level(); }
00332
00333 void push();
00334 void pop();
00335 void popto(int toLevel);
00336 void addNotifyObj(ContextNotifyObj* obj) { d_notifyObjList.push_back(obj); }
00337 void deleteNotifyObj(ContextNotifyObj* obj);
00338 unsigned long getMemory();
00339 };
00340
00341
00342 inline bool Scope::isCurrent(void) const
00343 { return this == d_context->topScope(); }
00344
00345 inline void Scope::addToChain(ContextObjChain* obj) {
00346 if(d_restoreChain != NULL)
00347 d_restoreChain->d_restoreChainPrev = &(obj->d_restoreChainNext);
00348 obj->d_restoreChainNext = d_restoreChain;
00349 obj->d_restoreChainPrev = &d_restoreChain;
00350 d_restoreChain = obj;
00351 }
00352
00353 inline Scope* Scope::topScope() const { return d_context->topScope(); }
00354
00355 inline void Scope::restore(void) {
00356
00357 while (d_restoreChain != NULL) d_restoreChain = d_restoreChain->restore();
00358
00359 }
00360
00361
00362
00363
00364
00365
00366 inline ContextObj::ContextObj(Context* context, bool atBottomScope)
00367 IF_DEBUG(: d_name("ContextObj"))
00368 {
00369 IF_DEBUG(d_active=true);
00370 DebugAssert(context != NULL, "NULL context pointer");
00371 if (atBottomScope) d_scope = context->bottomScope();
00372 else d_scope = context->topScope();
00373 d_restore = new(true) ContextObjChain(NULL, this, NULL);
00374 d_scope->addToChain(d_restore);
00375
00376
00377 }
00378
00379
00380
00381
00382
00383
00384
00385
00386
00387
00388
00389 class ContextManager {
00390 Context* d_curContext;
00391 std::vector<Context*> d_contexts;
00392
00393 public:
00394 ContextManager();
00395 ~ContextManager();
00396
00397 void push() { d_curContext->push(); }
00398 void pop() { d_curContext->pop(); }
00399 void popto(int toLevel) { d_curContext->popto(toLevel); }
00400 int scopeLevel() { return d_curContext->level(); }
00401 Context* createContext(const std::string& name="");
00402 Context* getCurrentContext() { return d_curContext; }
00403 Context* switchContext(Context* context);
00404 unsigned long getMemory();
00405 };
00406
00407
00408
00409
00410
00411
00412
00413
00414
00415
00416
00417
00418
00419 class ContextNotifyObj {
00420 friend class Context;
00421 protected:
00422 Context* d_context;
00423 public:
00424 ContextNotifyObj(Context* context): d_context(context)
00425 { context->addNotifyObj(this); }
00426 virtual ~ContextNotifyObj() {
00427
00428
00429
00430 if(d_context!=NULL) d_context->deleteNotifyObj(this);
00431 }
00432 virtual void notifyPre(void) {}
00433 virtual void notify(void) {}
00434 };
00435
00436
00437
00438 }
00439
00440 #endif