GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/context/context.h Lines: 54 63 85.7 %
Date: 2021-03-23 Branches: 28 82 34.1 %

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