CVC3  2.4.1
cdflags.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file cdflags.cpp
4  *\brief Implementation for CDFlags class
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Thu Jan 26 16:53:28 2006
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  *
19  */
20 /*****************************************************************************/
21 
22 
23 #include "cdflags.h"
24 #include "memory_manager_context.h"
25 
26 
27 using namespace CVC3;
28 using namespace std;
29 
30 
31 void CDFlags::update(unsigned mask, int scope, bool setMask)
32 {
33  DebugAssert(mask && (mask & (mask-1)) == 0, "Expected single bit mask");
34  if (scope < 0 || d_scope->level() <= scope) {
35  makeCurrent(scope);
36  if (setMask) d_flags = d_flags | mask;
37  else d_flags = d_flags & ~mask;
38  }
39  else {
40  // Kind of ugly: have to "change the past", but that's the price we pay for
41  // keeping all the flags in one word for efficiency.
42  IF_DEBUG(bool on = (d_flags & mask) != 0;)
43 
44  // Update current object
45  if (setMask) d_flags = d_flags | mask;
46  else d_flags = d_flags & ~mask;
47 
48  ContextObjChain** lastPtr = &d_restore;
49  CDFlags* pastFlags;
50  Scope* lastScope = d_scope;
51  bool done = false;
52 
53  // Update past objects
54  while (true) {
55  pastFlags = (CDFlags*)((*lastPtr)->d_data);
56  DebugAssert(pastFlags != NULL, "expected non-NULL data");
57  if (pastFlags->d_scope->level() >= scope) {
58  DebugAssert((on && (pastFlags->d_flags & mask))
59  || (!on && !(pastFlags->d_flags & mask)),
60  "Expected no change in flag since scope");
61  if (setMask) {
62  pastFlags->d_flags = pastFlags->d_flags | mask;
63  }
64  else {
65  pastFlags->d_flags = pastFlags->d_flags & ~mask;
66  }
67  if (pastFlags->d_scope->level() == scope) {
68  done = true; break;
69  }
70  lastScope = pastFlags->d_scope;
71  } else break;
72  lastPtr = &((*lastPtr)->d_restore);
73  DebugAssert(*lastPtr != NULL, "Should always be object at scope 0");
74  }
75  if (done) return;
76 
77  // No past object exists at the target scope: create one
78  DebugAssert(lastScope != NULL &&
79  lastScope->level() > scope,
80  "Expected lastScope to be above target scope");
81  while (lastScope->level() > scope) lastScope = lastScope->prevScope();
82 
83  ContextObj* data = pastFlags->makeCopy(lastScope->getCMM());
84 
85  pastFlags->d_scope = lastScope;
86 
87  ContextObjChain* obj = new(lastScope->getCMM())
88  ContextObjChain(data, this, (*lastPtr)->d_restore);
89  (*lastPtr)->d_restore = obj;
90  lastScope->addToChain(obj);
91 
92  // Update newly created past object
93  if (setMask) {
94  pastFlags->d_flags = pastFlags->d_flags | mask;
95  }
96  else {
97  pastFlags->d_flags = pastFlags->d_flags & ~mask;
98  }
99  }
100 }
int level() const
Definition: context.h:269
ContextObjChain * d_restore
The list of values on previous scopes; our destructor should clean up those.
Definition: context.h:210
ContextObjChain * d_restore
Pointer to the previous copy which belongs to the same master.
Definition: context.h:147
STL namespace.
#define DebugAssert(cond, str)
Definition: debug.h:408
virtual ContextObj * makeCopy(ContextMemoryManager *cmm)
Make a copy of the current object so it can be restored to its current state.
Definition: cdflags.h:40
Context Dependent Vector of Flags.
ContextMemoryManager * getCMM() const
Definition: context.h:99
#define IF_DEBUG(code)
Definition: debug.h:406
void addToChain(ContextObjChain *obj)
Called by ContextObj when created.
Definition: context.h:350
Scope * prevScope() const
Access functions.
Definition: context.h:94
Stack-based memory manager.
void update(unsigned mask, int scope, bool setMask)
Definition: cdflags.cpp:31
int level(void) const
Definition: context.h:95
Definition: expr.cpp:35
unsigned d_flags
Definition: cdflags.h:38