Branch data Line data Source code
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-2024 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 : : * Context class and context manager.
14 : : */
15 : :
16 : : #include "cvc5parser_public.h"
17 : :
18 : : #ifndef CVC5__CONTEXT__CONTEXT_H
19 : : #define CVC5__CONTEXT__CONTEXT_H
20 : :
21 : : #include <cstdlib>
22 : : #include <iostream>
23 : : #include <memory>
24 : : #include <typeinfo>
25 : : #include <vector>
26 : :
27 : : #include "base/check.h"
28 : : #include "base/output.h"
29 : : #include "context/context_mm.h"
30 : :
31 : : namespace cvc5::context {
32 : :
33 : : class Context;
34 : : class Scope;
35 : : class ContextObj;
36 : : class ContextNotifyObj;
37 : :
38 : : /** Pretty-printing of Contexts (for debugging) */
39 : : std::ostream& operator<<(std::ostream&, const Context&);
40 : :
41 : : /** Pretty-printing of Scopes (for debugging) */
42 : : std::ostream& operator<<(std::ostream&, const Scope&);
43 : :
44 : : /**
45 : : * A Context encapsulates all of the dynamic state of the system. Its main
46 : : * methods are push() and pop(). A call to push() saves the current state,
47 : : * and a call to pop() restores the state saved by the most recent call to
48 : : * push().
49 : : *
50 : : * Objects which want to participate in this global save and restore
51 : : * mechanism must inherit from ContextObj (see below).
52 : : *
53 : : * For more flexible context-dependent behavior, objects may implement the
54 : : * ContextNotifyObj interface and simply get a notification when a pop has
55 : : * occurred.
56 : : *
57 : : * Context also uses a helper class called Scope which stores information
58 : : * specific to the portion of the Context since the last call to push() (see
59 : : * below).
60 : : *
61 : : * Memory allocation in Contexts is done with the help of the
62 : : * ContextMemoryManager. A copy is stored in each Scope object for quick
63 : : * access.
64 : : */
65 : : class CVC5_EXPORT Context
66 : : {
67 : : /**
68 : : * Pointer to the ContextMemoryManager for this Context.
69 : : */
70 : : ContextMemoryManager* d_pCMM;
71 : :
72 : : /**
73 : : * List of all scopes for this context.
74 : : */
75 : : std::vector<Scope*> d_scopeList;
76 : :
77 : : /**
78 : : * Doubly-linked list of objects to notify before every pop. See
79 : : * ContextNotifyObj for structure of linked list.
80 : : */
81 : : ContextNotifyObj* d_pCNOpre;
82 : :
83 : : /**
84 : : * Doubly-linked list of objects to notify after every pop. See
85 : : * ContextNotifyObj for structure of linked list.
86 : : */
87 : : ContextNotifyObj* d_pCNOpost;
88 : :
89 : : friend std::ostream& operator<<(std::ostream&, const Context&);
90 : :
91 : : // disable copy, assignment
92 : : Context(const Context&) = delete;
93 : : Context& operator=(const Context&) = delete;
94 : :
95 : : public:
96 : :
97 : : /**
98 : : * A mechanism by which a "scoped" bit of contextual speculation can
99 : : * be applied. One might create a Context::ScopedPush in a function
100 : : * (as a local variable on the stack), then manipulate some
101 : : * context-dependent data structures in some fashion, speculatively.
102 : : * When the ScopedPush goes out of scope and is destructed, the
103 : : * context-dependent data structures will return to their original
104 : : * state.
105 : : *
106 : : * When such speculation occurs in a lexically-scoped manner, like
107 : : * described above, it is FAR preferable to use ScopedPush than to
108 : : * call ->push() and ->pop() on the Context directly. If you do the
109 : : * latter, it's extremely easy to forget to pop() on exceptional
110 : : * exit of the function, or if a short-circuited "early" return is
111 : : * later added to the function, etc. Further, ScopedPush includes
112 : : * an assertion that the Context at the end looks like the Context
113 : : * at the beginning (the topmost Scope pointer should be the same).
114 : : * This assertion is only an approximate check for correct behavior,
115 : : * but should catch egregious mismatches of ->push() and ->pop()
116 : : * while the ScopedPush is being applied---egregious mismatches that
117 : : * could exist, for example, if a Theory does some speculative
118 : : * reasoning but accidently gives control back to some other mechanism
119 : : * which does some speculation which isn't properly scoped inside the
120 : : * first.
121 : : */
122 : : class ScopedPush {
123 : : Context* const d_context;
124 : : const Scope* const d_scope;
125 : : public:
126 : 2834 : ScopedPush(Context* ctxt) :
127 : : d_context(ctxt),
128 : 2834 : d_scope(d_context->getTopScope()) {
129 : 2834 : d_context->push();
130 : 2834 : }
131 : 5668 : ~ScopedPush() noexcept(false) {
132 : 2834 : d_context->pop();
133 [ - + ][ - + ]: 2834 : AlwaysAssert(d_context->getTopScope() == d_scope)
[ - - ]
134 : : << "Context::ScopedPush observed an uneven Context (at pop, "
135 : : "top scope doesn't match what it was at the time the "
136 : 0 : "ScopedPush was applied)";
137 : 2834 : }
138 : : };/* Context::ScopedPush */
139 : :
140 : : /**
141 : : * Constructor: create ContextMemoryManager and initial Scope
142 : : */
143 : : Context();
144 : :
145 : : /**
146 : : * Destructor: pop all scopes, delete ContextMemoryManager
147 : : */
148 : : ~Context();
149 : :
150 : : /**
151 : : * Return the current (top) scope
152 : : */
153 : 1799965490 : Scope* getTopScope() const { return d_scopeList.back(); }
154 : :
155 : : /**
156 : : * Return the initial (bottom) scope
157 : : */
158 : 234494005 : Scope* getBottomScope() const { return d_scopeList[0]; }
159 : :
160 : : /**
161 : : * Return the current Scope level.
162 : : */
163 : : uint32_t getLevel() const;
164 : :
165 : : /**
166 : : * Return the ContextMemoryManager associated with the context.
167 : : */
168 : 0 : ContextMemoryManager* getCMM() { return d_pCMM; }
169 : :
170 : : /**
171 : : * Save the current state, create a new Scope
172 : : */
173 : : void push();
174 : :
175 : : /**
176 : : * Restore the previous state, delete the top Scope
177 : : */
178 : : void pop();
179 : :
180 : : /**
181 : : * Pop all the way back to given level
182 : : */
183 : : void popto(uint32_t toLevel);
184 : :
185 : : /**
186 : : * Add pCNO to the list of objects notified before every pop
187 : : */
188 : : void addNotifyObjPre(ContextNotifyObj* pCNO);
189 : :
190 : : /**
191 : : * Add pCNO to the list of objects notified after every pop
192 : : */
193 : : void addNotifyObjPost(ContextNotifyObj* pCNO);
194 : :
195 : : }; /* class Context */
196 : :
197 : : /**
198 : : * A UserContext is different from a Context only because it's used for
199 : : * different purposes---so separating the two types gives type errors where
200 : : * appropriate.
201 : : */
202 : : class UserContext : public Context {
203 : : private:
204 : : // disable copy, assignment
205 : : UserContext(const UserContext&) = delete;
206 : : UserContext& operator=(const UserContext&) = delete;
207 : : public:
208 : 67888 : UserContext() {}
209 : : };/* class UserContext */
210 : :
211 : :
212 : : /**
213 : : * Conceptually, a Scope encapsulates that portion of the context that
214 : : * changes after a call to push() and must be undone on a subsequent call to
215 : : * pop(). In particular, each call to push() creates a new Scope object .
216 : : * This new Scope object becomes the top scope and it points (via the
217 : : * d_pScopePrev member) to the previous top Scope. Each call to pop()
218 : : * deletes the current top scope and restores the previous one. The main
219 : : * purpose of a Scope is to maintain a linked list of ContexObj objects which
220 : : * change while the Scope is the top scope and which must be restored when
221 : : * the Scope is deleted.
222 : : *
223 : : * A Scope is also associated with a ContextMemoryManager. All memory
224 : : * allocated by the Scope is allocated in a single region using the
225 : : * ContextMemoryManager and released all at once when the Scope is popped.
226 : : */
227 : : class Scope {
228 : :
229 : : /**
230 : : * Context that created this Scope
231 : : */
232 : : Context* d_pContext;
233 : :
234 : : /**
235 : : * Memory manager for this Scope. Same as in Context, but stored here too
236 : : * for faster access by ContextObj objects.
237 : : */
238 : : ContextMemoryManager* d_pCMM;
239 : :
240 : : /**
241 : : * Scope level (total number of outstanding push() calls when this Scope was
242 : : * created).
243 : : */
244 : : uint32_t d_level;
245 : :
246 : : /**
247 : : * Linked list of objects which changed in this scope,
248 : : * and thus need to be restored when the scope is deleted.
249 : : */
250 : : ContextObj* d_pContextObjList;
251 : :
252 : : /**
253 : : * A list of ContextObj to be garbage collected before the destruction of this
254 : : * scope. deleteSelf() will be called on each element during ~Scope().
255 : : *
256 : : * This is either nullptr or list owned by this scope.
257 : : */
258 : : std::vector<ContextObj*> d_garbage;
259 : :
260 : : friend std::ostream& operator<<(std::ostream&, const Scope&);
261 : :
262 : : public:
263 : : /**
264 : : * Constructor: Create a new Scope; set the level and the previous Scope
265 : : * if any.
266 : : */
267 : 35605500 : Scope(Context* pContext, ContextMemoryManager* pCMM, uint32_t level)
268 : 35605500 : : d_pContext(pContext),
269 : : d_pCMM(pCMM),
270 : : d_level(level),
271 : : d_pContextObjList(nullptr),
272 : 35605500 : d_garbage()
273 : : {
274 : 35605500 : }
275 : :
276 : : /**
277 : : * Destructor: Clears out all of the garbage and restore all of the objects
278 : : * in ContextObjList.
279 : : */
280 : : ~Scope();
281 : :
282 : : /**
283 : : * Get the Context for this Scope
284 : : */
285 : 312011082 : Context* getContext() const { return d_pContext; }
286 : :
287 : : /**
288 : : * Get the ContextMemoryManager for this Scope
289 : : */
290 : 312011000 : ContextMemoryManager* getCMM() const { return d_pCMM; }
291 : :
292 : : /**
293 : : * Get the level of the current Scope
294 : : */
295 : 0 : uint32_t getLevel() const { return d_level; }
296 : :
297 : : /**
298 : : * Return true iff this Scope is the current top Scope
299 : : */
300 : 1487950438 : bool isCurrent() const { return this == d_pContext->getTopScope(); }
301 : :
302 : : /**
303 : : * When a ContextObj object is modified for the first time in this
304 : : * Scope, it should call this method to add itself to the list of
305 : : * objects that will need to be restored. Defined inline below.
306 : : */
307 : : void addToChain(ContextObj* pContextObj);
308 : :
309 : : /**
310 : : * Overload operator new for use with ContextMemoryManager to allow
311 : : * creation of new Scope objects in the current memory region.
312 : : */
313 : 35605500 : static void* operator new(size_t size, ContextMemoryManager* pCMM)
314 : : {
315 : 35605500 : return pCMM->newData(size);
316 : : }
317 : :
318 : : /**
319 : : * Enqueues a ContextObj to be garbage collected via a call to deleteSelf()
320 : : * during the destruction of this scope.
321 : : */
322 : : void enqueueToGarbageCollect(ContextObj* obj);
323 : :
324 : : /**
325 : : * Overload operator delete for Scope objects allocated using
326 : : * ContextMemoryManager. No need to do anything because memory is
327 : : * freed automatically when the ContextMemoryManager pop() method is
328 : : * called. Include both placement and standard delete for
329 : : * completeness.
330 : : */
331 : : static void operator delete(void* pMem, ContextMemoryManager* pCMM) {}
332 : 21919000 : static void operator delete(void* pMem) {}
333 : :
334 : : //FIXME: //! Check for memory leaks
335 : : // void check();
336 : :
337 : : };/* class Scope */
338 : :
339 : : /**
340 : : * This is an abstract base class from which all objects that are
341 : : * context-dependent should inherit. For any data structure that you
342 : : * want to have be automatically backtracked, do the following:
343 : : *
344 : : * 1. Create a class for the data structure that inherits from ContextObj
345 : : *
346 : : * 2. Implement save()
347 : : * The role of save() is to create a new ContexObj object that contains
348 : : * enough information to restore the object to its current state, even if
349 : : * it gets changed later. Note that save should call the (default)
350 : : * ContextObj Copy Constructor to copy the information in the base class.
351 : : * It is recommended that any memory allocated by save() should be done
352 : : * through the ContextMemoryManager. This way, it does not need to be
353 : : * explicitly freed when restore is called. However, it is only required
354 : : * that the ContextObj itself be allocated using the
355 : : * ContextMemoryManager. If other memory is allocated not using the
356 : : * ContextMemoryManager, it should be freed when restore() is called. In
357 : : * fact, any clean-up work on a saved object must be done by restore().
358 : : * This is because the destructor is never called explicitly on saved
359 : : * objects.
360 : : *
361 : : * 3. Implement restore()
362 : : * The role of restore() is, given the ContextObj returned by a previous
363 : : * call to save(), to restore the current object to the state it was in
364 : : * when save() was called. Note that the implementation of restore does
365 : : * *not* need to worry about restoring the base class data. This is done
366 : : * automatically. Ideally, restore() should not have to free any memory
367 : : * as any memory allocated by save() should have been done using the
368 : : * ContextMemoryManager (see item 2 above).
369 : : *
370 : : * 4. In the subclass implementation, any time the state is about to be
371 : : * changed, first call makeCurrent().
372 : : *
373 : : * 5. In the subclass implementation, the destructor should call destroy(),
374 : : * which repeatedly calls restore() until the object is restored to context
375 : : * level 0. Note, however, that if there is additional cleanup required at
376 : : * level 0, destroy() does not do this. It has to be implemented in the
377 : : * destructor of the subclass. The reason the destroy() functionality
378 : : * cannot be in the ContextObj destructor is that it needs to call the
379 : : * subclass-specific restore() method in order to properly clean up saved
380 : : * copies.
381 : : *
382 : : * GOTCHAS WHEN ALLOCATING CONTEXTUAL OBJECTS WITH NON-STANDARD ALLOCATORS
383 : : *
384 : : * Be careful if you intend to allocate ContextObj in (for example)
385 : : * ContextMemoryManager memory. ContextMemoryManager doesn't call the
386 : : * destructors of contained objects, which means the objects aren't
387 : : * properly unregistered from the Context (as in point #5, above).
388 : : * This can be remedied by allocating the ContextObj in the "top
389 : : * scope" rather than the "bottom scope" (which is what the
390 : : * "allocatedInCMM" flag to the special constructor in ContextObj
391 : : * does).
392 : : *
393 : : * But why allocate in CMM if it's so complicated? There's a big
394 : : * advantage: you don't have to track the lifetime of the ContextObj.
395 : : * The object simply ceases to exist when the Context is popped. Thus
396 : : * you can create an object in context memory, and if you stow
397 : : * pointers to it only in context memory as well, all is cleaned up
398 : : * for you when the scope pops. Here's a list of gotchas:
399 : : *
400 : : * 1. For data structures intended solely to be allocated in context
401 : : * memory, privately declare (but don't define) an operator
402 : : * new(size_t) and destructor (as currently in the Link class, in
403 : : * src/theory/uf/ecdata.h).
404 : : *
405 : : * 2. For data structures that may or may not be allocated in context
406 : : * memory, and are designed to be that way (esp. if they contain
407 : : * ContextObj instances), they should be heavily documented --
408 : : * especially the destructor, since it _may_or_may_not_be_called_.
409 : : *
410 : : * 3. There's also an issue for generic code -- some class Foo<T>
411 : : * might be allocated in context memory, and that might normally be
412 : : * fine, but if T is a ContextObj this requires certain care.
413 : : *
414 : : * 4. Note that certain care is required for ContextObj inside of data
415 : : * structures. If the (enclosing) data structure can be allocated
416 : : * in CMM, that means the (enclosed) ContextObj can be, even if it
417 : : * was not designed to be allocated in that way. In many
418 : : * instances, it may be required that data structures enclosing
419 : : * ContextObj be parameterized with a similar "bool allocatedInCMM"
420 : : * argument as the special constructor in this class (and pass it
421 : : * on to all ContextObj instances).
422 : : */
423 : : class CVC5_EXPORT ContextObj
424 : : {
425 : : /**
426 : : * Pointer to Scope in which this object was last modified.
427 : : */
428 : : Scope* d_pScope;
429 : :
430 : : /**
431 : : * Pointer to most recent version of same ContextObj in a previous Scope
432 : : */
433 : : ContextObj* d_pContextObjRestore;
434 : :
435 : : /**
436 : : * Next link in ContextObjList list maintained by Scope class.
437 : : */
438 : : ContextObj* d_pContextObjNext;
439 : :
440 : : /**
441 : : * Previous link in ContextObjList list maintained by Scope class. We use
442 : : * double-indirection here to make element deletion easy.
443 : : */
444 : : ContextObj** d_ppContextObjPrev;
445 : :
446 : : /**
447 : : * Helper method for makeCurrent (see below). Separated out to allow common
448 : : * case to be inlined without making a function call. It calls save() and
449 : : * does the necessary bookkeeping to ensure that object can be restored to
450 : : * its current state when restore is called.
451 : : */
452 : : void update();
453 : :
454 : : // The rest of the private methods are for the benefit of the Scope. We make
455 : : // Scope our friend so it is the only one that can use them.
456 : :
457 : : friend class Scope;
458 : :
459 : : friend std::ostream& operator<<(std::ostream&, const Scope&);
460 : :
461 : : /**
462 : : * Return reference to next link in ContextObjList. Used by
463 : : * Scope::addToChain method.
464 : : */
465 : 3892700000 : ContextObj*& next() { return d_pContextObjNext; }
466 : :
467 : : /**
468 : : * Return reference to prev link in ContextObjList. Used by
469 : : * Scope::addToChain method.
470 : : */
471 : 3269870000 : ContextObj**& prev() { return d_ppContextObjPrev; }
472 : :
473 : : /**
474 : : * This method is called by Scope during a pop: it does the necessary work to
475 : : * restore the object from its saved copy and then returns the next object in
476 : : * the list that needs to be restored.
477 : : */
478 : : ContextObj* restoreAndContinue();
479 : :
480 : : protected:
481 : : /**
482 : : * This is a method that must be implemented by all classes inheriting from
483 : : * ContextObj. See the comment before the class declaration.
484 : : */
485 : : virtual ContextObj* save(ContextMemoryManager* pCMM) = 0;
486 : :
487 : : /**
488 : : * This is a method that must be implemented by all classes inheriting from
489 : : * ContextObj. See the comment before the class declaration.
490 : : */
491 : : virtual void restore(ContextObj* pContextObjRestore) = 0;
492 : :
493 : : /**
494 : : * This method checks if the object has been modified in this Scope
495 : : * yet. If not, it calls update().
496 : : */
497 : : inline void makeCurrent();
498 : :
499 : : /**
500 : : * Just calls update(), but given a different name for the derived
501 : : * class-facing interface. This is a "forced" makeCurrent(), useful
502 : : * for ContextObjs allocated in CMM that need a special "bottom"
503 : : * case when they disappear out of existence (kind of a destructor).
504 : : * See CDOhash_map (in cdhashmap.h) for an example.
505 : : */
506 : : inline void makeSaveRestorePoint();
507 : :
508 : : /**
509 : : * Should be called from sub-class destructor: calls restore until restored
510 : : * to initial version (version at context level 0). Also removes object from
511 : : * all Scope lists. Note that this doesn't actually free the memory
512 : : * allocated by the ContextMemoryManager for this object. This isn't done
513 : : * until the corresponding Scope is popped.
514 : : */
515 : : void destroy();
516 : :
517 : : /////
518 : : //
519 : : // These next four accessors return properties of the Scope to
520 : : // derived classes without giving them the Scope object directly.
521 : : //
522 : : /////
523 : :
524 : : /**
525 : : * Get the Context with which this ContextObj was created. This is
526 : : * part of the protected interface, intended for derived classes to
527 : : * use if necessary.
528 : : */
529 : 0 : Context* getContext() const { return d_pScope->getContext(); }
530 : :
531 : : /**
532 : : * Get the ContextMemoryManager with which this ContextObj was
533 : : * created. This is part of the protected interface, intended for
534 : : * derived classes to use if necessary. If a ContextObj-derived
535 : : * class needs to allocate memory somewhere other than the save()
536 : : * member function (where it is explicitly given a
537 : : * ContextMemoryManager), it can use this accessor to get the memory
538 : : * manager.
539 : : */
540 : : ContextMemoryManager* getCMM() const { return d_pScope->getCMM(); }
541 : :
542 : : /**
543 : : * Get the level associated to this ContextObj. Useful if a
544 : : * ContextObj-derived class needs to compare the level of its last
545 : : * update with another ContextObj.
546 : : */
547 : 0 : uint32_t getLevel() const { return d_pScope->getLevel(); }
548 : :
549 : : /**
550 : : * Returns true if the object is "current"-- that is, updated in the
551 : : * topmost contextual scope. Useful if a ContextObj-derived class
552 : : * needs to determine if it has been modified in the current scope.
553 : : * Note that it is always safe to call makeCurrent() without first
554 : : * checking if the object is current, so this function need not be
555 : : * used under normal circumstances.
556 : : */
557 : : bool isCurrent() const { return d_pScope->isCurrent(); }
558 : :
559 : : public:
560 : : /**
561 : : * Disable delete: objects allocated with new(ContextMemorymanager) should
562 : : * never be deleted. Objects allocated with new(bool) should be deleted by
563 : : * calling deleteSelf().
564 : : */
565 : 0 : static void operator delete(void* pMem) {
566 : 0 : AlwaysAssert(false) << "It is not allowed to delete a ContextObj this way!";
567 : : }
568 : :
569 : : /**
570 : : * operator new using ContextMemoryManager (common case used by
571 : : * subclasses during save()). No delete is required for memory
572 : : * allocated this way, since it is automatically released when the
573 : : * context is popped. Also note that allocations using this
574 : : * operator never have their destructor called, so any clean-up has
575 : : * to be done using the restore method.
576 : : */
577 : 312011083 : static void* operator new(size_t size, ContextMemoryManager* pCMM) {
578 : 312011083 : return pCMM->newData(size);
579 : : }
580 : :
581 : : /**
582 : : * Corresponding placement delete. Note that this is provided just
583 : : * to satisfy the requirement that a placement delete should be
584 : : * provided for every placement new. It would only be called if a
585 : : * ContextObj constructor throws an exception after a successful
586 : : * call to the above new operator.
587 : : */
588 : 0 : static void operator delete(void* pMem, ContextMemoryManager* pCMM) {}
589 : :
590 : : /**
591 : : * Create a new ContextObj. The initial scope is set to the bottom
592 : : * scope of the Context. Note that in the common case, the copy
593 : : * constructor is called to create new ContextObj objects. The
594 : : * default copy constructor does the right thing, so we do not
595 : : * explicitly define it.
596 : : */
597 : : ContextObj(Context* context);
598 : :
599 : : /**
600 : : * Destructor does nothing: subclass must explicitly call destroy() instead.
601 : : */
602 : 234285263 : virtual ~ContextObj() {}
603 : :
604 : : /**
605 : : * If you want to allocate a ContextObj object on the heap, use this
606 : : * special new operator. To free this memory, instead of
607 : : * "delete p", use "p->deleteSelf()".
608 : : */
609 : 169685200 : static void* operator new(size_t size, bool) {
610 : 169685200 : return ::operator new(size);
611 : : }
612 : :
613 : : /**
614 : : * Corresponding placement delete. Note that this is provided for
615 : : * the compiler in case the ContextObj constructor throws an
616 : : * exception. The client can't call it.
617 : : */
618 : 0 : static void operator delete(void* pMem, bool) {
619 : 0 : ::operator delete(pMem);
620 : 0 : }
621 : :
622 : : /**
623 : : * Use this instead of delete to delete memory allocated using the special
624 : : * new function provided above that takes a bool argument. Do not call this
625 : : * function on memory allocated using the new that takes a
626 : : * ContextMemoryManager as an argument.
627 : : */
628 : 169679197 : void deleteSelf() {
629 : 169679197 : this->~ContextObj();
630 : 169679197 : ::operator delete(this);
631 : 169679197 : }
632 : :
633 : : /**
634 : : * Use this to enqueue calling deleteSelf() at the time of the destruction of
635 : : * the enclosing Scope.
636 : : */
637 : : void enqueueToGarbageCollect();
638 : :
639 : : }; /* class ContextObj */
640 : :
641 : : /**
642 : : * For more flexible context-dependent behavior than that provided by
643 : : * ContextObj, objects may implement the ContextNotifyObj interface
644 : : * and simply get a notification when a pop has occurred. See
645 : : * Context class for how to register a ContextNotifyObj with the
646 : : * Context (you can choose to have notification come before or after
647 : : * the ContextObj objects have been restored).
648 : : */
649 : : class ContextNotifyObj {
650 : :
651 : : /**
652 : : * Context is our friend so that when the Context is deleted, any
653 : : * remaining ContextNotifyObj can be removed from the Context list.
654 : : */
655 : : friend class Context;
656 : :
657 : : /**
658 : : * Pointer to next ContextNotifyObject in this List
659 : : */
660 : : ContextNotifyObj* d_pCNOnext;
661 : :
662 : : /**
663 : : * Pointer to previous ContextNotifyObject in this list
664 : : */
665 : : ContextNotifyObj** d_ppCNOprev;
666 : :
667 : : /**
668 : : * Return reference to next link in ContextNotifyObj list. Used by
669 : : * Context::addNotifyObj methods.
670 : : */
671 : 2948500 : ContextNotifyObj*& next() { return d_pCNOnext; }
672 : :
673 : : /**
674 : : * Return reference to prev link in ContextNotifyObj list. Used by
675 : : * Context::addNotifyObj methods.
676 : : */
677 : 2948500 : ContextNotifyObj**& prev() { return d_ppCNOprev; }
678 : :
679 : : protected:
680 : : /**
681 : : * This is the method called to notify the object of a pop. It must be
682 : : * implemented by the subclass. It is protected since context is out
683 : : * friend.
684 : : */
685 : : virtual void contextNotifyPop() = 0;
686 : :
687 : : public:
688 : :
689 : : /**
690 : : * Constructor for ContextNotifyObj. Parameters are the context to
691 : : * which this notify object will be added, and a flag which, if
692 : : * true, tells the context to notify this object *before* the
693 : : * ContextObj objects are restored. Otherwise, the context notifies
694 : : * the object after the ContextObj objects are restored. The
695 : : * default is for notification after.
696 : : */
697 : : ContextNotifyObj(Context* pContext, bool preNotify = false);
698 : :
699 : : /**
700 : : * Destructor: removes object from list
701 : : */
702 : : virtual ~ContextNotifyObj();
703 : :
704 : : };/* class ContextNotifyObj */
705 : :
706 : 1487950438 : inline void ContextObj::makeCurrent()
707 : : {
708 [ + + ]: 1487950438 : if(!(d_pScope->isCurrent())) {
709 : 312011089 : update();
710 : : }
711 : 1487950438 : }
712 : :
713 : : inline void ContextObj::makeSaveRestorePoint() { update(); }
714 : :
715 : 546506000 : inline void Scope::addToChain(ContextObj* pContextObj)
716 : : {
717 [ + + ]: 546506000 : if(d_pContextObjList != NULL) {
718 : 519872000 : d_pContextObjList->prev() = &pContextObj->next();
719 : : }
720 : :
721 : 546506000 : pContextObj->next() = d_pContextObjList;
722 : 546506000 : pContextObj->prev() = &d_pContextObjList;
723 : 546506000 : d_pContextObjList = pContextObj;
724 : 546506000 : }
725 : :
726 : : } // namespace cvc5::context
727 : :
728 : : #endif /* CVC5__CONTEXT__CONTEXT_H */
|
