Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Context class and context manager.
11 : : */
12 : :
13 : : #include "cvc5parser_public.h"
14 : :
15 : : #ifndef CVC5__CONTEXT__CONTEXT_H
16 : : #define CVC5__CONTEXT__CONTEXT_H
17 : :
18 : : #include <cstdlib>
19 : : #include <iostream>
20 : : #include <memory>
21 : : #include <typeinfo>
22 : : #include <vector>
23 : :
24 : : #include "base/check.h"
25 : : #include "base/output.h"
26 : : #include "context/context_mm.h"
27 : :
28 : : namespace cvc5::context {
29 : :
30 : : class Context;
31 : : class Scope;
32 : : class ContextObj;
33 : : class ContextNotifyObj;
34 : :
35 : : /** Pretty-printing of Contexts (for debugging) */
36 : : std::ostream& operator<<(std::ostream&, const Context&);
37 : :
38 : : /** Pretty-printing of Scopes (for debugging) */
39 : : std::ostream& operator<<(std::ostream&, const Scope&);
40 : :
41 : : /**
42 : : * A Context encapsulates all of the dynamic state of the system. Its main
43 : : * methods are push() and pop(). A call to push() saves the current state,
44 : : * and a call to pop() restores the state saved by the most recent call to
45 : : * push().
46 : : *
47 : : * Objects which want to participate in this global save and restore
48 : : * mechanism must inherit from ContextObj (see below).
49 : : *
50 : : * For more flexible context-dependent behavior, objects may implement the
51 : : * ContextNotifyObj interface and simply get a notification when a pop has
52 : : * occurred.
53 : : *
54 : : * Context also uses a helper class called Scope which stores information
55 : : * specific to the portion of the Context since the last call to push() (see
56 : : * below).
57 : : *
58 : : * Memory allocation in Contexts is done with the help of the
59 : : * ContextMemoryManager. A copy is stored in each Scope object for quick
60 : : * access.
61 : : */
62 : : class CVC5_EXPORT Context
63 : : {
64 : : /**
65 : : * Pointer to the ContextMemoryManager for this Context.
66 : : */
67 : : ContextMemoryManager* d_pCMM;
68 : :
69 : : /**
70 : : * List of all scopes for this context.
71 : : */
72 : : std::vector<Scope*> d_scopeList;
73 : :
74 : : /**
75 : : * Doubly-linked list of objects to notify before every pop. See
76 : : * ContextNotifyObj for structure of linked list.
77 : : */
78 : : ContextNotifyObj* d_pCNOpre;
79 : :
80 : : /**
81 : : * Doubly-linked list of objects to notify after every pop. See
82 : : * ContextNotifyObj for structure of linked list.
83 : : */
84 : : ContextNotifyObj* d_pCNOpost;
85 : :
86 : : friend std::ostream& operator<<(std::ostream&, const Context&);
87 : :
88 : : // disable copy, assignment
89 : : Context(const Context&) = delete;
90 : : Context& operator=(const Context&) = delete;
91 : :
92 : : public:
93 : :
94 : : /**
95 : : * A mechanism by which a "scoped" bit of contextual speculation can
96 : : * be applied. One might create a Context::ScopedPush in a function
97 : : * (as a local variable on the stack), then manipulate some
98 : : * context-dependent data structures in some fashion, speculatively.
99 : : * When the ScopedPush goes out of scope and is destructed, the
100 : : * context-dependent data structures will return to their original
101 : : * state.
102 : : *
103 : : * When such speculation occurs in a lexically-scoped manner, like
104 : : * described above, it is FAR preferable to use ScopedPush than to
105 : : * call ->push() and ->pop() on the Context directly. If you do the
106 : : * latter, it's extremely easy to forget to pop() on exceptional
107 : : * exit of the function, or if a short-circuited "early" return is
108 : : * later added to the function, etc. Further, ScopedPush includes
109 : : * an assertion that the Context at the end looks like the Context
110 : : * at the beginning (the topmost Scope pointer should be the same).
111 : : * This assertion is only an approximate check for correct behavior,
112 : : * but should catch egregious mismatches of ->push() and ->pop()
113 : : * while the ScopedPush is being applied---egregious mismatches that
114 : : * could exist, for example, if a Theory does some speculative
115 : : * reasoning but accidently gives control back to some other mechanism
116 : : * which does some speculation which isn't properly scoped inside the
117 : : * first.
118 : : */
119 : : class ScopedPush {
120 : : Context* const d_context;
121 : : const Scope* const d_scope;
122 : : public:
123 : 2769 : ScopedPush(Context* ctxt) :
124 : 2769 : d_context(ctxt),
125 : 2769 : d_scope(d_context->getTopScope()) {
126 : 2769 : d_context->push();
127 : 2769 : }
128 : 2769 : ~ScopedPush() noexcept(false) {
129 : 2769 : d_context->pop();
130 [ - + ][ - + ]: 2769 : AlwaysAssert(d_context->getTopScope() == d_scope)
[ - - ]
131 : : << "Context::ScopedPush observed an uneven Context (at pop, "
132 : : "top scope doesn't match what it was at the time the "
133 : 0 : "ScopedPush was applied)";
134 : 2769 : }
135 : : };/* Context::ScopedPush */
136 : :
137 : : /**
138 : : * Constructor: create ContextMemoryManager and initial Scope
139 : : */
140 : : Context();
141 : :
142 : : /**
143 : : * Destructor: pop all scopes, delete ContextMemoryManager
144 : : */
145 : : ~Context();
146 : :
147 : : /**
148 : : * Return the current (top) scope
149 : : */
150 : 1838752242 : Scope* getTopScope() const { return d_scopeList.back(); }
151 : :
152 : : /**
153 : : * Return the initial (bottom) scope
154 : : */
155 : 265746443 : Scope* getBottomScope() const { return d_scopeList[0]; }
156 : :
157 : : /**
158 : : * Return the current Scope level.
159 : : */
160 : : uint32_t getLevel() const;
161 : :
162 : : /**
163 : : * Return the ContextMemoryManager associated with the context.
164 : : */
165 : 0 : ContextMemoryManager* getCMM() { return d_pCMM; }
166 : :
167 : : /**
168 : : * Save the current state, create a new Scope
169 : : */
170 : : void push();
171 : :
172 : : /**
173 : : * Restore the previous state, delete the top Scope
174 : : */
175 : : void pop();
176 : :
177 : : /**
178 : : * Pop all the way back to given level
179 : : */
180 : : void popto(uint32_t toLevel);
181 : :
182 : : /**
183 : : * Add pCNO to the list of objects notified before every pop
184 : : */
185 : : void addNotifyObjPre(ContextNotifyObj* pCNO);
186 : :
187 : : /**
188 : : * Add pCNO to the list of objects notified after every pop
189 : : */
190 : : void addNotifyObjPost(ContextNotifyObj* pCNO);
191 : :
192 : : }; /* class Context */
193 : :
194 : : /**
195 : : * A UserContext is different from a Context only because it's used for
196 : : * different purposes---so separating the two types gives type errors where
197 : : * appropriate.
198 : : */
199 : : class UserContext : public Context {
200 : : private:
201 : : // disable copy, assignment
202 : : UserContext(const UserContext&) = delete;
203 : : UserContext& operator=(const UserContext&) = delete;
204 : : public:
205 : 74845 : UserContext() {}
206 : : };/* class UserContext */
207 : :
208 : :
209 : : /**
210 : : * Conceptually, a Scope encapsulates that portion of the context that
211 : : * changes after a call to push() and must be undone on a subsequent call to
212 : : * pop(). In particular, each call to push() creates a new Scope object .
213 : : * This new Scope object becomes the top scope and it points (via the
214 : : * d_pScopePrev member) to the previous top Scope. Each call to pop()
215 : : * deletes the current top scope and restores the previous one. The main
216 : : * purpose of a Scope is to maintain a linked list of ContexObj objects which
217 : : * change while the Scope is the top scope and which must be restored when
218 : : * the Scope is deleted.
219 : : *
220 : : * A Scope is also associated with a ContextMemoryManager. All memory
221 : : * allocated by the Scope is allocated in a single region using the
222 : : * ContextMemoryManager and released all at once when the Scope is popped.
223 : : */
224 : : class Scope {
225 : :
226 : : /**
227 : : * Context that created this Scope
228 : : */
229 : : Context* d_pContext;
230 : :
231 : : /**
232 : : * Memory manager for this Scope. Same as in Context, but stored here too
233 : : * for faster access by ContextObj objects.
234 : : */
235 : : ContextMemoryManager* d_pCMM;
236 : :
237 : : /**
238 : : * Scope level (total number of outstanding push() calls when this Scope was
239 : : * created).
240 : : */
241 : : uint32_t d_level;
242 : :
243 : : /**
244 : : * Linked list of objects which changed in this scope,
245 : : * and thus need to be restored when the scope is deleted.
246 : : */
247 : : ContextObj* d_pContextObjList;
248 : :
249 : : /**
250 : : * A list of ContextObj to be garbage collected before the destruction of this
251 : : * scope. deleteSelf() will be called on each element during ~Scope().
252 : : *
253 : : * This is either nullptr or list owned by this scope.
254 : : */
255 : : std::vector<ContextObj*> d_garbage;
256 : :
257 : : friend std::ostream& operator<<(std::ostream&, const Scope&);
258 : :
259 : : public:
260 : : /**
261 : : * Constructor: Create a new Scope; set the level and the previous Scope
262 : : * if any.
263 : : */
264 : 36287320 : Scope(Context* pContext, ContextMemoryManager* pCMM, uint32_t level)
265 : 36287320 : : d_pContext(pContext),
266 : 36287320 : d_pCMM(pCMM),
267 : 36287320 : d_level(level),
268 : 36287320 : d_pContextObjList(nullptr),
269 : 36287320 : d_garbage()
270 : : {
271 : 36287320 : }
272 : :
273 : : /**
274 : : * Destructor: Clears out all of the garbage and restore all of the objects
275 : : * in ContextObjList.
276 : : */
277 : : ~Scope();
278 : :
279 : : /**
280 : : * Get the Context for this Scope
281 : : */
282 : 316743539 : Context* getContext() const { return d_pContext; }
283 : :
284 : : /**
285 : : * Get the ContextMemoryManager for this Scope
286 : : */
287 : 316743539 : ContextMemoryManager* getCMM() const { return d_pCMM; }
288 : :
289 : : /**
290 : : * Get the level of the current Scope
291 : : */
292 : 0 : uint32_t getLevel() const { return d_level; }
293 : :
294 : : /**
295 : : * Return true iff this Scope is the current top Scope
296 : : */
297 : 1522003162 : bool isCurrent() const { return this == d_pContext->getTopScope(); }
298 : :
299 : : /**
300 : : * When a ContextObj object is modified for the first time in this
301 : : * Scope, it should call this method to add itself to the list of
302 : : * objects that will need to be restored. Defined inline below.
303 : : */
304 : : void addToChain(ContextObj* pContextObj);
305 : :
306 : : /**
307 : : * Overload operator new for use with ContextMemoryManager to allow
308 : : * creation of new Scope objects in the current memory region.
309 : : */
310 : 36287320 : static void* operator new(size_t size, ContextMemoryManager* pCMM)
311 : : {
312 : 36287320 : return pCMM->newData(size);
313 : : }
314 : :
315 : : /**
316 : : * Enqueues a ContextObj to be garbage collected via a call to deleteSelf()
317 : : * during the destruction of this scope.
318 : : */
319 : : void enqueueToGarbageCollect(ContextObj* obj);
320 : :
321 : : /**
322 : : * Overload operator delete for Scope objects allocated using
323 : : * ContextMemoryManager. No need to do anything because memory is
324 : : * freed automatically when the ContextMemoryManager pop() method is
325 : : * called. Include both placement and standard delete for
326 : : * completeness.
327 : : */
328 : : static void operator delete(CVC5_UNUSED void* pMem,
329 : : CVC5_UNUSED ContextMemoryManager* pCMM)
330 : : {
331 : : }
332 : 19885056 : static void operator delete(CVC5_UNUSED 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 : 4099148975 : ContextObj*& next() { return d_pContextObjNext; }
466 : :
467 : : /**
468 : : * Return reference to prev link in ContextObjList. Used by
469 : : * Scope::addToChain method.
470 : : */
471 : 3454686202 : 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(CVC5_UNUSED void* pMem)
566 : : {
567 : 0 : AlwaysAssert(false) << "It is not allowed to delete a ContextObj this way!";
568 : : }
569 : :
570 : : /**
571 : : * operator new using ContextMemoryManager (common case used by
572 : : * subclasses during save()). No delete is required for memory
573 : : * allocated this way, since it is automatically released when the
574 : : * context is popped. Also note that allocations using this
575 : : * operator never have their destructor called, so any clean-up has
576 : : * to be done using the restore method.
577 : : */
578 : 316743539 : static void* operator new(size_t size, ContextMemoryManager* pCMM) {
579 : 316743539 : return pCMM->newData(size);
580 : : }
581 : :
582 : : /**
583 : : * Corresponding placement delete. Note that this is provided just
584 : : * to satisfy the requirement that a placement delete should be
585 : : * provided for every placement new. It would only be called if a
586 : : * ContextObj constructor throws an exception after a successful
587 : : * call to the above new operator.
588 : : */
589 : 0 : static void operator delete(CVC5_UNUSED void* pMem,
590 : : CVC5_UNUSED ContextMemoryManager* pCMM)
591 : : {
592 : 0 : }
593 : :
594 : : /**
595 : : * Create a new ContextObj. The initial scope is set to the bottom
596 : : * scope of the Context. Note that in the common case, the copy
597 : : * constructor is called to create new ContextObj objects. The
598 : : * default copy constructor does the right thing, so we do not
599 : : * explicitly define it.
600 : : */
601 : : ContextObj(Context* context);
602 : :
603 : : /**
604 : : * Destructor does nothing: subclass must explicitly call destroy() instead.
605 : : */
606 : 265476790 : virtual ~ContextObj() {}
607 : :
608 : : /**
609 : : * If you want to allocate a ContextObj object on the heap, use this
610 : : * special new operator. To free this memory, instead of
611 : : * "delete p", use "p->deleteSelf()".
612 : : */
613 : 197974060 : static void* operator new(size_t size, bool) {
614 : 197974060 : return ::operator new(size);
615 : : }
616 : :
617 : : /**
618 : : * Corresponding placement delete. Note that this is provided for
619 : : * the compiler in case the ContextObj constructor throws an
620 : : * exception. The client can't call it.
621 : : */
622 : 0 : static void operator delete(void* pMem, bool) {
623 : 0 : ::operator delete(pMem);
624 : 0 : }
625 : :
626 : : /**
627 : : * Use this instead of delete to delete memory allocated using the special
628 : : * new function provided above that takes a bool argument. Do not call this
629 : : * function on memory allocated using the new that takes a
630 : : * ContextMemoryManager as an argument.
631 : : */
632 : 197966490 : void deleteSelf() {
633 : 197966490 : this->~ContextObj();
634 : 197966490 : ::operator delete(this);
635 : 197966490 : }
636 : :
637 : : /**
638 : : * Use this to enqueue calling deleteSelf() at the time of the destruction of
639 : : * the enclosing Scope.
640 : : */
641 : : void enqueueToGarbageCollect();
642 : :
643 : : }; /* class ContextObj */
644 : :
645 : : /**
646 : : * For more flexible context-dependent behavior than that provided by
647 : : * ContextObj, objects may implement the ContextNotifyObj interface
648 : : * and simply get a notification when a pop has occurred. See
649 : : * Context class for how to register a ContextNotifyObj with the
650 : : * Context (you can choose to have notification come before or after
651 : : * the ContextObj objects have been restored).
652 : : */
653 : : class ContextNotifyObj {
654 : :
655 : : /**
656 : : * Context is our friend so that when the Context is deleted, any
657 : : * remaining ContextNotifyObj can be removed from the Context list.
658 : : */
659 : : friend class Context;
660 : :
661 : : /**
662 : : * Pointer to next ContextNotifyObject in this List
663 : : */
664 : : ContextNotifyObj* d_pCNOnext;
665 : :
666 : : /**
667 : : * Pointer to previous ContextNotifyObject in this list
668 : : */
669 : : ContextNotifyObj** d_ppCNOprev;
670 : :
671 : : /**
672 : : * Return reference to next link in ContextNotifyObj list. Used by
673 : : * Context::addNotifyObj methods.
674 : : */
675 : 3123844 : ContextNotifyObj*& next() { return d_pCNOnext; }
676 : :
677 : : /**
678 : : * Return reference to prev link in ContextNotifyObj list. Used by
679 : : * Context::addNotifyObj methods.
680 : : */
681 : 3123844 : ContextNotifyObj**& prev() { return d_ppCNOprev; }
682 : :
683 : : protected:
684 : : /**
685 : : * This is the method called to notify the object of a pop. It must be
686 : : * implemented by the subclass. It is protected since context is out
687 : : * friend.
688 : : */
689 : : virtual void contextNotifyPop() = 0;
690 : :
691 : : public:
692 : :
693 : : /**
694 : : * Constructor for ContextNotifyObj. Parameters are the context to
695 : : * which this notify object will be added, and a flag which, if
696 : : * true, tells the context to notify this object *before* the
697 : : * ContextObj objects are restored. Otherwise, the context notifies
698 : : * the object after the ContextObj objects are restored. The
699 : : * default is for notification after.
700 : : */
701 : : ContextNotifyObj(Context* pContext, bool preNotify = false);
702 : :
703 : : /**
704 : : * Destructor: removes object from list
705 : : */
706 : : virtual ~ContextNotifyObj();
707 : :
708 : : };/* class ContextNotifyObj */
709 : :
710 : 1522003162 : inline void ContextObj::makeCurrent()
711 : : {
712 [ + + ]: 1522003162 : if(!(d_pScope->isCurrent())) {
713 : 316743539 : update();
714 : : }
715 : 1522003162 : }
716 : :
717 : : inline void ContextObj::makeSaveRestorePoint() { update(); }
718 : :
719 : 582489980 : inline void Scope::addToChain(ContextObj* pContextObj)
720 : : {
721 [ + + ]: 582489980 : if(d_pContextObjList != NULL) {
722 : 555140685 : d_pContextObjList->prev() = &pContextObj->next();
723 : : }
724 : :
725 : 582489980 : pContextObj->next() = d_pContextObjList;
726 : 582489980 : pContextObj->prev() = &d_pContextObjList;
727 : 582489980 : d_pContextObjList = pContextObj;
728 : 582489980 : }
729 : :
730 : : } // namespace cvc5::context
731 : :
732 : : #endif /* CVC5__CONTEXT__CONTEXT_H */
|
