<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<title>CVC3: context.h Source File</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li><a href="annotated.html"><span>Classes</span></a></li>
<li class="current"><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="files.html"><span>File List</span></a></li>
<li><a href="globals.html"><span>File Members</span></a></li>
</ul>
</div>
<div class="header">
<div class="headertitle">
<div class="title">context.h</div> </div>
</div>
<div class="contents">
<a href="context_8h.html">Go to the documentation of this file.</a><div class="fragment"><pre class="fragment"><a name="l00001"></a>00001 <span class="comment">/*****************************************************************************/</span><span class="comment"></span>
<a name="l00002"></a>00002 <span class="comment">/*!</span>
<a name="l00003"></a>00003 <span class="comment"> * \file context.h</span>
<a name="l00004"></a>00004 <span class="comment"> *</span>
<a name="l00005"></a>00005 <span class="comment"> * Author: Clark Barrett</span>
<a name="l00006"></a>00006 <span class="comment"> *</span>
<a name="l00007"></a>00007 <span class="comment"> * Created: Tue Dec 31 19:07:38 2002</span>
<a name="l00008"></a>00008 <span class="comment"> *</span>
<a name="l00009"></a>00009 <span class="comment"> * <hr></span>
<a name="l00010"></a>00010 <span class="comment"> *</span>
<a name="l00011"></a>00011 <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span>
<a name="l00012"></a>00012 <span class="comment"> * and its documentation for any purpose is hereby granted without</span>
<a name="l00013"></a>00013 <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span>
<a name="l00014"></a>00014 <span class="comment"> * LICENSE file provided with this distribution.</span>
<a name="l00015"></a>00015 <span class="comment"> *</span>
<a name="l00016"></a>00016 <span class="comment"> * <hr></span>
<a name="l00017"></a>00017 <span class="comment"> *</span>
<a name="l00018"></a>00018 <span class="comment"> */</span>
<a name="l00019"></a>00019 <span class="comment">/*****************************************************************************/</span>
<a name="l00020"></a>00020
<a name="l00021"></a>00021
<a name="l00022"></a>00022 <span class="preprocessor">#ifndef _cvc3__include__context_h_</span>
<a name="l00023"></a>00023 <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__include__context_h_</span>
<a name="l00024"></a>00024 <span class="preprocessor"></span>
<a name="l00025"></a>00025 <span class="preprocessor">#include <string></span>
<a name="l00026"></a>00026 <span class="preprocessor">#include <vector></span>
<a name="l00027"></a>00027 <span class="preprocessor">#include <stdlib.h></span>
<a name="l00028"></a>00028 <span class="preprocessor">#include "<a class="code" href="debug_8h.html" title="Description: Collection of debugging macros and functions.">debug.h</a>"</span>
<a name="l00029"></a>00029 <span class="preprocessor">#include "<a class="code" href="memory__manager__context_8h.html" title="Stack-based memory manager.">memory_manager_context.h</a>"</span>
<a name="l00030"></a>00030 <span class="preprocessor">#include "<a class="code" href="os_8h.html" title="Abstraction over different operating systems.">os.h</a>"</span>
<a name="l00031"></a>00031
<a name="l00032"></a>00032 <span class="keyword">namespace </span>CVC3 {
<a name="l00033"></a>00033
<a name="l00034"></a>00034 <span class="comment">/****************************************************************************/</span><span class="comment"></span>
<a name="l00035"></a>00035 <span class="comment">/*! \defgroup Context Context Management</span>
<a name="l00036"></a>00036 <span class="comment"> * \ingroup BuildingBlocks</span>
<a name="l00037"></a>00037 <span class="comment"> * Infrastructure for backtrackable data structures.</span>
<a name="l00038"></a>00038 <span class="comment"> * @{</span>
<a name="l00039"></a>00039 <span class="comment"> */</span>
<a name="l00040"></a>00040 <span class="comment">/****************************************************************************/</span>
<a name="l00041"></a>00041
<a name="l00042"></a>00042 <span class="keyword">class </span>Context;
<a name="l00043"></a>00043 <span class="keyword">class </span>ContextManager;
<a name="l00044"></a>00044 <span class="keyword">class </span>ContextNotifyObj;
<a name="l00045"></a>00045 <span class="keyword">class </span>ContextObj;
<a name="l00046"></a>00046 <span class="keyword">class </span>ContextObjChain;
<a name="l00047"></a>00047
<a name="l00048"></a>00048 <span class="comment">/****************************************************************************/</span><span class="comment"></span>
<a name="l00049"></a>00049 <span class="comment">/*!</span>
<a name="l00050"></a>00050 <span class="comment"> * Author: Clark Barrett</span>
<a name="l00051"></a>00051 <span class="comment"> *</span>
<a name="l00052"></a>00052 <span class="comment"> * Created: Thu Feb 13 00:19:15 2003</span>
<a name="l00053"></a>00053 <span class="comment"> *</span>
<a name="l00054"></a>00054 <span class="comment"> * A scope encapsulates the portion of a context which has changed</span>
<a name="l00055"></a>00055 <span class="comment"> * since the last call to push(). Thus, when pop() is called,</span>
<a name="l00056"></a>00056 <span class="comment"> * everything in this scope is restored to its previous state.</span>
<a name="l00057"></a>00057 <span class="comment"> */</span>
<a name="l00058"></a>00058 <span class="comment">/****************************************************************************/</span>
<a name="l00059"></a>00059
<a name="l00060"></a><a class="code" href="classCVC3_1_1Scope.html">00060</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1Scope.html">Scope</a> {
<a name="l00061"></a><a class="code" href="classCVC3_1_1Scope.html#aaa3d900ada369da566fe2d896aee9a5a">00061</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1ContextObj.html">ContextObj</a>;
<a name="l00062"></a><a class="code" href="classCVC3_1_1Scope.html#a78b6f5579433f2891e2bb17c011ec112">00062</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1ContextObjChain.html">ContextObjChain</a>;
<a name="l00063"></a><a class="code" href="classCVC3_1_1Scope.html#ade09c87996f604683ba4726bfdd79121">00063</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1CDFlags.html">CDFlags</a>;<span class="comment"></span>
<a name="l00064"></a>00064 <span class="comment"> //! Context that created this scope</span>
<a name="l00065"></a><a class="code" href="classCVC3_1_1Scope.html#a7d2d367f8da7a9d216f1de35d65bda37">00065</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1Context.html">Context</a>* <a class="code" href="classCVC3_1_1Scope.html#a7d2d367f8da7a9d216f1de35d65bda37" title="Context that created this scope.">d_context</a>;
<a name="l00066"></a>00066 <span class="comment"></span>
<a name="l00067"></a>00067 <span class="comment"> //! Memory manager for this scope</span>
<a name="l00068"></a><a class="code" href="classCVC3_1_1Scope.html#a1ff51670a2263ba69ccd35d13cdb1395">00068</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1ContextMemoryManager.html" title="ContextMemoryManager.">ContextMemoryManager</a>* <a class="code" href="classCVC3_1_1Scope.html#a1ff51670a2263ba69ccd35d13cdb1395" title="Memory manager for this scope.">d_cmm</a>;
<a name="l00069"></a>00069 <span class="comment"></span>
<a name="l00070"></a>00070 <span class="comment"> //! Previous scope in this context</span>
<a name="l00071"></a><a class="code" href="classCVC3_1_1Scope.html#a9844d24cb03f6c43fd738350fa6447c5">00071</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1Scope.html">Scope</a>* <a class="code" href="classCVC3_1_1Scope.html#a9844d24cb03f6c43fd738350fa6447c5" title="Previous scope in this context.">d_prevScope</a>;
<a name="l00072"></a>00072 <span class="comment"></span>
<a name="l00073"></a>00073 <span class="comment"> //! Scope level</span>
<a name="l00074"></a><a class="code" href="classCVC3_1_1Scope.html#aac245fe3aaa3bf2578867ec669b162e9">00074</a> <span class="comment"></span> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1Scope.html#aac245fe3aaa3bf2578867ec669b162e9" title="Scope level.">d_level</a>;
<a name="l00075"></a>00075 <span class="comment"></span>
<a name="l00076"></a>00076 <span class="comment"> /*! @brief Linked list of objects which are "current" in this scope,</span>
<a name="l00077"></a>00077 <span class="comment"> and thus need to be restored when the scope is deleted */</span>
<a name="l00078"></a><a class="code" href="classCVC3_1_1Scope.html#a0940c7152f4eeb881856460985a83cb6">00078</a> <a class="code" href="classCVC3_1_1ContextObjChain.html">ContextObjChain</a>* <a class="code" href="classCVC3_1_1Scope.html#a0940c7152f4eeb881856460985a83cb6" title="Linked list of objects which are "current" in this scope, and thus need to be restored when the scope...">d_restoreChain</a>;
<a name="l00079"></a>00079 <span class="comment"></span>
<a name="l00080"></a>00080 <span class="comment"> //! Called by ContextObj when created</span>
<a name="l00081"></a>00081 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="group__Context.html#ga3fcf473cd27da6c7498f462650f75ac8" title="Called by ContextObj when created.">addToChain</a>(<a class="code" href="classCVC3_1_1ContextObjChain.html">ContextObjChain</a>* obj);
<a name="l00082"></a>00082
<a name="l00083"></a>00083 <span class="keyword">public</span>:<span class="comment"></span>
<a name="l00084"></a>00084 <span class="comment"> //! Constructor</span>
<a name="l00085"></a><a class="code" href="classCVC3_1_1Scope.html#aaed4373135bf8803a725eafc37466dd5">00085</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1Scope.html#aaed4373135bf8803a725eafc37466dd5" title="Constructor.">Scope</a>(<a class="code" href="classCVC3_1_1Context.html">Context</a>* context, <a class="code" href="classCVC3_1_1ContextMemoryManager.html" title="ContextMemoryManager.">ContextMemoryManager</a>* cmm,
<a name="l00086"></a>00086 <a class="code" href="classCVC3_1_1Scope.html">Scope</a>* <a class="code" href="classCVC3_1_1Scope.html#aaf14b7225ee54df52812aaa7f6d08a30" title="Access functions.">prevScope</a> = NULL)
<a name="l00087"></a>00087 : <a class="code" href="classCVC3_1_1Scope.html#a7d2d367f8da7a9d216f1de35d65bda37" title="Context that created this scope.">d_context</a>(context), <a class="code" href="classCVC3_1_1Scope.html#a1ff51670a2263ba69ccd35d13cdb1395" title="Memory manager for this scope.">d_cmm</a>(cmm), <a class="code" href="classCVC3_1_1Scope.html#a9844d24cb03f6c43fd738350fa6447c5" title="Previous scope in this context.">d_prevScope</a>(<a class="code" href="classCVC3_1_1Scope.html#aaf14b7225ee54df52812aaa7f6d08a30" title="Access functions.">prevScope</a>),
<a name="l00088"></a>00088 <a class="code" href="classCVC3_1_1Scope.html#a0940c7152f4eeb881856460985a83cb6" title="Linked list of objects which are "current" in this scope, and thus need to be restored when the scope...">d_restoreChain</a>(NULL)
<a name="l00089"></a>00089 { <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1Scope.html#aaf14b7225ee54df52812aaa7f6d08a30" title="Access functions.">prevScope</a>) <a class="code" href="classCVC3_1_1Scope.html#aac245fe3aaa3bf2578867ec669b162e9" title="Scope level.">d_level</a> = <a class="code" href="classCVC3_1_1Scope.html#aaf14b7225ee54df52812aaa7f6d08a30" title="Access functions.">prevScope</a>-><a class="code" href="classCVC3_1_1Scope.html#ad5c67e42cab76cf985c2aff1fab5f16e">level</a>() + 1; <span class="keywordflow">else</span> <a class="code" href="classCVC3_1_1Scope.html#aac245fe3aaa3bf2578867ec669b162e9" title="Scope level.">d_level</a> = 0; }<span class="comment"></span>
<a name="l00090"></a>00090 <span class="comment"> //! Destructor</span>
<a name="l00091"></a><a class="code" href="classCVC3_1_1Scope.html#a03a8d51e2a01b97bedc96d1e67488c7f">00091</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1Scope.html#a03a8d51e2a01b97bedc96d1e67488c7f" title="Destructor.">~Scope</a>() {}
<a name="l00092"></a>00092 <span class="comment"></span>
<a name="l00093"></a>00093 <span class="comment"> //! Access functions</span>
<a name="l00094"></a><a class="code" href="classCVC3_1_1Scope.html#aaf14b7225ee54df52812aaa7f6d08a30">00094</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1Scope.html">Scope</a>* <a class="code" href="classCVC3_1_1Scope.html#aaf14b7225ee54df52812aaa7f6d08a30" title="Access functions.">prevScope</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Scope.html#a9844d24cb03f6c43fd738350fa6447c5" title="Previous scope in this context.">d_prevScope</a>; }
<a name="l00095"></a><a class="code" href="classCVC3_1_1Scope.html#ad5c67e42cab76cf985c2aff1fab5f16e">00095</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1Scope.html#ad5c67e42cab76cf985c2aff1fab5f16e">level</a>(<span class="keywordtype">void</span>)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Scope.html#aac245fe3aaa3bf2578867ec669b162e9" title="Scope level.">d_level</a>; }
<a name="l00096"></a>00096 <span class="keywordtype">bool</span> <a class="code" href="group__Context.html#ga3a1efd364586330635a668eae3d2612d">isCurrent</a>(<span class="keywordtype">void</span>) <span class="keyword">const</span>;
<a name="l00097"></a>00097 <a class="code" href="classCVC3_1_1Scope.html">Scope</a>* <a class="code" href="group__Context.html#ga745d55cc6d3ab3bea1afe675fd7ce7a7">topScope</a>() <span class="keyword">const</span>;
<a name="l00098"></a><a class="code" href="classCVC3_1_1Scope.html#ade77b2683969176cb35cb7d8f39079ba">00098</a> <a class="code" href="classCVC3_1_1Context.html">Context</a>* <a class="code" href="classCVC3_1_1Scope.html#ade77b2683969176cb35cb7d8f39079ba">getContext</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Scope.html#a7d2d367f8da7a9d216f1de35d65bda37" title="Context that created this scope.">d_context</a>; }
<a name="l00099"></a><a class="code" href="classCVC3_1_1Scope.html#a95900e8234970f533045827446e05e64">00099</a> <a class="code" href="classCVC3_1_1ContextMemoryManager.html" title="ContextMemoryManager.">ContextMemoryManager</a>* <a class="code" href="classCVC3_1_1Scope.html#a95900e8234970f533045827446e05e64">getCMM</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Scope.html#a1ff51670a2263ba69ccd35d13cdb1395" title="Memory manager for this scope.">d_cmm</a>; }
<a name="l00100"></a>00100
<a name="l00101"></a><a class="code" href="classCVC3_1_1Scope.html#abadab46860137ebbd886a695ae9c9e46">00101</a> <span class="keywordtype">void</span>* <a class="code" href="classCVC3_1_1Scope.html#abadab46860137ebbd886a695ae9c9e46">operator new</a>(<span class="keywordtype">size_t</span> size, <a class="code" href="classCVC3_1_1MemoryManager.html">MemoryManager</a>* mm)
<a name="l00102"></a>00102 { <span class="keywordflow">return</span> mm-><a class="code" href="classCVC3_1_1MemoryManager.html#a3db7efbc4b956bd423a73e1157d70ce0">newData</a>(size); }
<a name="l00103"></a><a class="code" href="classCVC3_1_1Scope.html#aae8bd5faeb04b443612cd724445f8462">00103</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Scope.html#aae8bd5faeb04b443612cd724445f8462">operator delete</a>(<span class="keywordtype">void</span>* pMem, <a class="code" href="classCVC3_1_1MemoryManager.html">MemoryManager</a>* mm) {
<a name="l00104"></a>00104 mm-><a class="code" href="classCVC3_1_1MemoryManager.html#ad29fac88d3a07566d9a8f9dc8d8e059c">deleteData</a>(pMem);
<a name="l00105"></a>00105 }
<a name="l00106"></a><a class="code" href="classCVC3_1_1Scope.html#adf2e0e25af9ba26c5477367a88314d3f">00106</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Scope.html#adf2e0e25af9ba26c5477367a88314d3f">operator delete</a>(<span class="keywordtype">void</span>*) { }
<a name="l00107"></a>00107 <span class="comment"></span>
<a name="l00108"></a>00108 <span class="comment"> //! Restore all the values</span>
<a name="l00109"></a>00109 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="group__Context.html#ga1b0a5ef8d8aef498218f0dfddea851a7" title="Restore all the values.">restore</a>(<span class="keywordtype">void</span>);
<a name="l00110"></a>00110 <span class="comment"></span>
<a name="l00111"></a>00111 <span class="comment"> //! Called by ~ContextManager</span>
<a name="l00112"></a>00112 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Scope.html#a288d98e934b96112a131f0bbd068680f" title="Called by ~ContextManager.">finalize</a>(<span class="keywordtype">void</span>);
<a name="l00113"></a>00113 <span class="comment"></span>
<a name="l00114"></a>00114 <span class="comment"> //! Check for memory leaks</span>
<a name="l00115"></a>00115 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Scope.html#a796f074fbe4834687942c43b6456dabb" title="Check for memory leaks.">check</a>(<span class="keywordtype">void</span>);
<a name="l00116"></a>00116 <span class="comment"></span>
<a name="l00117"></a>00117 <span class="comment"> //! Compute memory used</span>
<a name="l00118"></a>00118 <span class="comment"></span> <span class="keywordtype">unsigned</span> <span class="keywordtype">long</span> <a class="code" href="classCVC3_1_1Scope.html#a007e070f14d1158207a28293354ed106" title="Compute memory used.">getMemory</a>(<span class="keywordtype">int</span> verbosity);
<a name="l00119"></a>00119 };
<a name="l00120"></a>00120 <span class="comment"></span>
<a name="l00121"></a>00121 <span class="comment">///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00122"></a>00122 <span class="comment"></span><span class="comment">// //</span>
<a name="l00123"></a>00123 <span class="comment">// Class: ContextObjChain //</span>
<a name="l00124"></a>00124 <span class="comment">// Author: Sergey Berezin //</span>
<a name="l00125"></a>00125 <span class="comment">// Created: Wed Mar 12 11:25:22 2003 //</span>
<a name="l00126"></a>00126 <span class="comment"></span>
<a name="l00127"></a>00127 <span class="comment">/*! Description: An element of a doubly linked list holding a copy of</span>
<a name="l00128"></a>00128 <span class="comment"> * ContextObj in a scope. It is made separate from ContextObj to keep</span>
<a name="l00129"></a>00129 <span class="comment"> * the list pointers valid in all scopes at all times, so that the</span>
<a name="l00130"></a>00130 <span class="comment"> * object can be easily removed from the list when the master</span>
<a name="l00131"></a>00131 <span class="comment"> * ContextObj is destroyed. */</span><span class="comment"></span>
<a name="l00132"></a>00132 <span class="comment">///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00133"></a><a class="code" href="classCVC3_1_1ContextObjChain.html">00133</a> <span class="comment"></span><span class="keyword">class </span><a class="code" href="classCVC3_1_1ContextObjChain.html">ContextObjChain</a> {
<a name="l00134"></a><a class="code" href="classCVC3_1_1ContextObjChain.html#a921193447f6e42f596ac0a7694b02830">00134</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1Scope.html">Scope</a>;
<a name="l00135"></a><a class="code" href="classCVC3_1_1ContextObjChain.html#aaa3d900ada369da566fe2d896aee9a5a">00135</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1ContextObj.html">ContextObj</a>;
<a name="l00136"></a><a class="code" href="classCVC3_1_1ContextObjChain.html#ade09c87996f604683ba4726bfdd79121">00136</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1CDFlags.html">CDFlags</a>;
<a name="l00137"></a>00137 <span class="keyword">private</span>:<span class="comment"></span>
<a name="l00138"></a>00138 <span class="comment"> //! Next link in chain</span>
<a name="l00139"></a><a class="code" href="classCVC3_1_1ContextObjChain.html#afa940ba625d121fe37a659d7caf7f558">00139</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1ContextObjChain.html">ContextObjChain</a>* <a class="code" href="classCVC3_1_1ContextObjChain.html#afa940ba625d121fe37a659d7caf7f558" title="Next link in chain.">d_restoreChainNext</a>;
<a name="l00140"></a>00140 <span class="comment"></span>
<a name="l00141"></a>00141 <span class="comment"> /*! @brief Pointer to the pointer of the previous object which</span>
<a name="l00142"></a>00142 <span class="comment"> points to us. This makes a doubly-linked list for easy element</span>
<a name="l00143"></a>00143 <span class="comment"> deletion */</span>
<a name="l00144"></a><a class="code" href="classCVC3_1_1ContextObjChain.html#af0e39b718fff489ee96dfb6b4e59d03d">00144</a> <a class="code" href="classCVC3_1_1ContextObjChain.html">ContextObjChain</a>** <a class="code" href="classCVC3_1_1ContextObjChain.html#af0e39b718fff489ee96dfb6b4e59d03d" title="Pointer to the pointer of the previous object which points to us. This makes a doubly-linked list for...">d_restoreChainPrev</a>;
<a name="l00145"></a>00145 <span class="comment"></span>
<a name="l00146"></a>00146 <span class="comment"> //! Pointer to the previous copy which belongs to the same master</span>
<a name="l00147"></a><a class="code" href="classCVC3_1_1ContextObjChain.html#a64049e510cf64e4a96d6e1134479f467">00147</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1ContextObjChain.html">ContextObjChain</a>* <a class="code" href="classCVC3_1_1ContextObjChain.html#a64049e510cf64e4a96d6e1134479f467" title="Pointer to the previous copy which belongs to the same master.">d_restore</a>;
<a name="l00148"></a>00148 <span class="comment"></span>
<a name="l00149"></a>00149 <span class="comment"> //! Pointer to copy of master to be restored when restore() is called</span>
<a name="l00150"></a><a class="code" href="classCVC3_1_1ContextObjChain.html#a7574a1b2995d61f9b3ea8e81cd3b7d87">00150</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1ContextObj.html">ContextObj</a>* <a class="code" href="classCVC3_1_1ContextObjChain.html#a7574a1b2995d61f9b3ea8e81cd3b7d87" title="Pointer to copy of master to be restored when restore() is called.">d_data</a>;
<a name="l00151"></a>00151 <span class="comment"></span>
<a name="l00152"></a>00152 <span class="comment"> //! Pointer to the master object</span>
<a name="l00153"></a><a class="code" href="classCVC3_1_1ContextObjChain.html#a3f4c203169ba7c8f1528de48fa95eedf">00153</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1ContextObj.html">ContextObj</a>* <a class="code" href="classCVC3_1_1ContextObjChain.html#a3f4c203169ba7c8f1528de48fa95eedf" title="Pointer to the master object.">d_master</a>;
<a name="l00154"></a>00154 <span class="comment"></span>
<a name="l00155"></a>00155 <span class="comment"> //! Private constructor (only friends can use it)</span>
<a name="l00156"></a><a class="code" href="classCVC3_1_1ContextObjChain.html#a689d17e7768d0f95cc6c36d27bdb8368">00156</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1ContextObjChain.html#a689d17e7768d0f95cc6c36d27bdb8368" title="Private constructor (only friends can use it)">ContextObjChain</a>(<a class="code" href="classCVC3_1_1ContextObj.html">ContextObj</a>* data, <a class="code" href="classCVC3_1_1ContextObj.html">ContextObj</a>* master,
<a name="l00157"></a>00157 <a class="code" href="classCVC3_1_1ContextObjChain.html">ContextObjChain</a>* <a class="code" href="classCVC3_1_1ContextObjChain.html#a83e5207b9d496337691b30f072c117c7" title="Restore from d_data to d_master.">restore</a>)
<a name="l00158"></a>00158 : <a class="code" href="classCVC3_1_1ContextObjChain.html#afa940ba625d121fe37a659d7caf7f558" title="Next link in chain.">d_restoreChainNext</a>(NULL), <a class="code" href="classCVC3_1_1ContextObjChain.html#af0e39b718fff489ee96dfb6b4e59d03d" title="Pointer to the pointer of the previous object which points to us. This makes a doubly-linked list for...">d_restoreChainPrev</a>(NULL),
<a name="l00159"></a>00159 <a class="code" href="classCVC3_1_1ContextObjChain.html#a64049e510cf64e4a96d6e1134479f467" title="Pointer to the previous copy which belongs to the same master.">d_restore</a>(restore), <a class="code" href="classCVC3_1_1ContextObjChain.html#a7574a1b2995d61f9b3ea8e81cd3b7d87" title="Pointer to copy of master to be restored when restore() is called.">d_data</a>(data), <a class="code" href="classCVC3_1_1ContextObjChain.html#a3f4c203169ba7c8f1528de48fa95eedf" title="Pointer to the master object.">d_master</a>(master)
<a name="l00160"></a>00160 { }
<a name="l00161"></a>00161 <span class="comment"></span>
<a name="l00162"></a>00162 <span class="comment"> //! Restore from d_data to d_master</span>
<a name="l00163"></a>00163 <span class="comment"></span> <a class="code" href="classCVC3_1_1ContextObjChain.html">ContextObjChain</a>* <a class="code" href="classCVC3_1_1ContextObjChain.html#a83e5207b9d496337691b30f072c117c7" title="Restore from d_data to d_master.">restore</a>(<span class="keywordtype">void</span>);
<a name="l00164"></a>00164 <span class="keyword">public</span>:<span class="comment"></span>
<a name="l00165"></a>00165 <span class="comment"> //! Destructor</span>
<a name="l00166"></a><a class="code" href="classCVC3_1_1ContextObjChain.html#a788988a56a5a6c9a0adf0854041dcb07">00166</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1ContextObjChain.html#a788988a56a5a6c9a0adf0854041dcb07" title="Destructor.">~ContextObjChain</a>() {}
<a name="l00167"></a>00167
<a name="l00168"></a><a class="code" href="classCVC3_1_1ContextObjChain.html#afa47cd0df02aa00f68b78c00ba46c1ce">00168</a> <span class="keywordtype">void</span>* <a class="code" href="classCVC3_1_1ContextObjChain.html#afa47cd0df02aa00f68b78c00ba46c1ce">operator new</a>(<span class="keywordtype">size_t</span> size, <a class="code" href="classCVC3_1_1MemoryManager.html">MemoryManager</a>* mm) {
<a name="l00169"></a>00169 <span class="keywordflow">return</span> mm-><a class="code" href="classCVC3_1_1MemoryManager.html#a3db7efbc4b956bd423a73e1157d70ce0">newData</a>(size);
<a name="l00170"></a>00170 }
<a name="l00171"></a><a class="code" href="classCVC3_1_1ContextObjChain.html#a6de67c7f87aa17d4b3ea62bbfb28e3c6">00171</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ContextObjChain.html#a6de67c7f87aa17d4b3ea62bbfb28e3c6">operator delete</a>(<span class="keywordtype">void</span>* pMem, <a class="code" href="classCVC3_1_1MemoryManager.html">MemoryManager</a>* mm) {
<a name="l00172"></a>00172 mm-><a class="code" href="classCVC3_1_1MemoryManager.html#ad29fac88d3a07566d9a8f9dc8d8e059c">deleteData</a>(pMem);
<a name="l00173"></a>00173 }
<a name="l00174"></a>00174
<a name="l00175"></a><a class="code" href="classCVC3_1_1ContextObjChain.html#ae8a63005ffe97aa5d59394cf67320287">00175</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ContextObjChain.html#ae8a63005ffe97aa5d59394cf67320287">operator delete</a>(<span class="keywordtype">void</span>*) { }
<a name="l00176"></a>00176
<a name="l00177"></a>00177 <span class="comment">// If you use this operator, you have to call free yourself when the memory</span>
<a name="l00178"></a>00178 <span class="comment">// is freed.</span>
<a name="l00179"></a><a class="code" href="classCVC3_1_1ContextObjChain.html#a4e3a0a6e9b99c74108d8006e9b7e0210">00179</a> <span class="keywordtype">void</span>* <a class="code" href="classCVC3_1_1ContextObjChain.html#a4e3a0a6e9b99c74108d8006e9b7e0210">operator new</a>(<span class="keywordtype">size_t</span> size, <span class="keywordtype">bool</span> b) {
<a name="l00180"></a>00180 <span class="keywordflow">return</span> malloc(size);
<a name="l00181"></a>00181 }
<a name="l00182"></a><a class="code" href="classCVC3_1_1ContextObjChain.html#a4e9cf7f1ec93515fe347716e4fcd28d2">00182</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ContextObjChain.html#a4e9cf7f1ec93515fe347716e4fcd28d2">operator delete</a>(<span class="keywordtype">void</span>* pMem, <span class="keywordtype">bool</span> b) {
<a name="l00183"></a>00183 free(pMem);
<a name="l00184"></a>00184 }
<a name="l00185"></a>00185
<a name="l00186"></a>00186 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(std::string name() <span class="keyword">const</span>;)
<a name="l00187"></a>00187 };
<a name="l00188"></a>00188 <span class="comment"></span>
<a name="l00189"></a>00189 <span class="comment">///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00190"></a>00190 <span class="comment"></span><span class="comment">// //</span>
<a name="l00191"></a>00191 <span class="comment">// Class: ContextObj //</span>
<a name="l00192"></a>00192 <span class="comment">// Author: Clark Barrett //</span>
<a name="l00193"></a>00193 <span class="comment">// Created: Thu Feb 13 00:21:13 2003 //</span>
<a name="l00194"></a>00194 <span class="comment"></span>
<a name="l00195"></a>00195 <span class="comment">/*! Description: This is a generic class from which all objects that</span>
<a name="l00196"></a>00196 <span class="comment"> * are context-dependent should inherit. Subclasses need to implement</span>
<a name="l00197"></a>00197 <span class="comment"> * makeCopy, restoreData, and setNull.</span>
<a name="l00198"></a>00198 <span class="comment"> */</span><span class="comment"></span>
<a name="l00199"></a>00199 <span class="comment">///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00200"></a><a class="code" href="classCVC3_1_1ContextObj.html">00200</a> <span class="comment"></span><span class="keyword">class </span><a class="code" href="os_8h.html#a0035aac6379df39aa69feba98b2751ba">CVC_DLL</a> <a class="code" href="classCVC3_1_1ContextObj.html">ContextObj</a> {
<a name="l00201"></a><a class="code" href="classCVC3_1_1ContextObj.html#a921193447f6e42f596ac0a7694b02830">00201</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1Scope.html">Scope</a>;
<a name="l00202"></a><a class="code" href="classCVC3_1_1ContextObj.html#a78b6f5579433f2891e2bb17c011ec112">00202</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1ContextObjChain.html">ContextObjChain</a>;
<a name="l00203"></a><a class="code" href="classCVC3_1_1ContextObj.html#ade09c87996f604683ba4726bfdd79121">00203</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1CDFlags.html">CDFlags</a>;
<a name="l00204"></a>00204 <span class="keyword">private</span>:<span class="comment"></span>
<a name="l00205"></a>00205 <span class="comment"> //! Last scope in which this object was modified.</span>
<a name="l00206"></a><a class="code" href="classCVC3_1_1ContextObj.html#ab4ce4a31b6ac3e9def89503a5bbaa365">00206</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1Scope.html">Scope</a>* <a class="code" href="classCVC3_1_1ContextObj.html#ab4ce4a31b6ac3e9def89503a5bbaa365" title="Last scope in which this object was modified.">d_scope</a>;
<a name="l00207"></a>00207 <span class="comment"></span>
<a name="l00208"></a>00208 <span class="comment"> /*! @brief The list of values on previous scopes; our destructor</span>
<a name="l00209"></a>00209 <span class="comment"> * should clean up those. */</span>
<a name="l00210"></a><a class="code" href="classCVC3_1_1ContextObj.html#a60c1d2e2b5f4b8055a2a6619ce173bdc">00210</a> <a class="code" href="classCVC3_1_1ContextObjChain.html">ContextObjChain</a>* <a class="code" href="classCVC3_1_1ContextObj.html#a60c1d2e2b5f4b8055a2a6619ce173bdc" title="The list of values on previous scopes; our destructor should clean up those.">d_restore</a>;
<a name="l00211"></a>00211
<a name="l00212"></a>00212 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(std::string d_name;)
<a name="l00213"></a>00213 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(<span class="keywordtype">bool</span> d_active;)
<a name="l00214"></a>00214 <span class="comment"></span>
<a name="l00215"></a>00215 <span class="comment"> //! Update on the given scope, on the current scope if 'scope' == -1</span>
<a name="l00216"></a>00216 <span class="comment"></span> <span class="keywordtype">void</span> update(<span class="keywordtype">int</span> scope = -1);
<a name="l00217"></a>00217
<a name="l00218"></a>00218 <span class="keyword">protected</span>:<span class="comment"></span>
<a name="l00219"></a>00219 <span class="comment"> //! Copy constructor (defined mainly for debugging purposes)</span>
<a name="l00220"></a><a class="code" href="classCVC3_1_1ContextObj.html#a624778eea4d75cb7cf4b93c98f57514b">00220</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1ContextObjChain.html#aaa3d900ada369da566fe2d896aee9a5a">ContextObj</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1ContextObj.html">ContextObj</a>& co)
<a name="l00221"></a>00221 : d_scope(co.d_scope), <a class="code" href="classCVC3_1_1ContextObjChain.html#a64049e510cf64e4a96d6e1134479f467" title="Pointer to the previous copy which belongs to the same master.">d_restore</a>(co.<a class="code" href="classCVC3_1_1ContextObjChain.html#a64049e510cf64e4a96d6e1134479f467" title="Pointer to the previous copy which belongs to the same master.">d_restore</a>) {
<a name="l00222"></a>00222 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(d_name=co.d_name;)
<a name="l00223"></a>00223 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(co.d_active, <span class="stringliteral">"ContextObj["</span>+co.name()+<span class="stringliteral">"] copy constructor"</span>);
<a name="l00224"></a>00224 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(d_active = co.d_active;)
<a name="l00225"></a>00225 <span class="comment">// TRACE("context verbose", "ContextObj()[", this, "]: copy constructor");</span>
<a name="l00226"></a>00226 }
<a name="l00227"></a>00227 <span class="comment"></span>
<a name="l00228"></a>00228 <span class="comment"> //! Assignment operator (defined mainly for debugging purposes)</span>
<a name="l00229"></a><a class="code" href="classCVC3_1_1ContextObj.html#a9ac307d69eca045bb3ea47bd2450e842">00229</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1ContextObj.html">ContextObj</a>& <a class="code" href="classCVC3_1_1ContextObj.html#a9ac307d69eca045bb3ea47bd2450e842" title="Assignment operator (defined mainly for debugging purposes)">operator=</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1ContextObj.html">ContextObj</a>& co) {
<a name="l00230"></a>00230 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<span class="keyword">false</span>, <span class="stringliteral">"ContextObj::operator=(): shouldn't be called"</span>);
<a name="l00231"></a>00231 <span class="keywordflow">return</span> *<span class="keyword">this</span>;
<a name="l00232"></a>00232 }
<a name="l00233"></a>00233 <span class="comment"></span>
<a name="l00234"></a>00234 <span class="comment"> /*! @brief Make a copy of the current object so it can be restored</span>
<a name="l00235"></a>00235 <span class="comment"> * to its current state */</span>
<a name="l00236"></a>00236 <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1ContextObj.html">ContextObj</a>* makeCopy(<a class="code" href="classCVC3_1_1ContextMemoryManager.html" title="ContextMemoryManager.">ContextMemoryManager</a>* cmm) = 0;
<a name="l00237"></a>00237 <span class="comment"></span>
<a name="l00238"></a>00238 <span class="comment"> //! Restore the current object from the given data</span>
<a name="l00239"></a><a class="code" href="classCVC3_1_1ContextObj.html#a37109b576b9dbaeee06f37cdc78f1a2e">00239</a> <span class="comment"></span> <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ContextObj.html#a37109b576b9dbaeee06f37cdc78f1a2e" title="Restore the current object from the given data.">restoreData</a>(<a class="code" href="classCVC3_1_1ContextObj.html">ContextObj</a>* data) {
<a name="l00240"></a>00240 <a class="code" href="debug_8h.html#a2637b2fffa22e3c9fad40cda8fcc3bce" title="If something goes horribly wrong, print a message and abort immediately with exit(1).">FatalAssert</a>(<span class="keyword">false</span>,
<a name="l00241"></a>00241 <span class="stringliteral">"ContextObj::restoreData(): call in the base abstract class"</span>);
<a name="l00242"></a>00242 }
<a name="l00243"></a>00243
<a name="l00244"></a><a class="code" href="classCVC3_1_1ContextObj.html#a6d37a721fd7fc3b4eabdae16cdf133c0">00244</a> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1ContextObj.html">ContextObj</a>* <a class="code" href="classCVC3_1_1ContextObj.html#a6d37a721fd7fc3b4eabdae16cdf133c0">getRestore</a>() {
<a name="l00245"></a>00245 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1ContextObjChain.html#a64049e510cf64e4a96d6e1134479f467" title="Pointer to the previous copy which belongs to the same master.">d_restore</a> ? <a class="code" href="classCVC3_1_1ContextObjChain.html#a64049e510cf64e4a96d6e1134479f467" title="Pointer to the previous copy which belongs to the same master.">d_restore</a>-><a class="code" href="classCVC3_1_1ContextObjChain.html#a7574a1b2995d61f9b3ea8e81cd3b7d87" title="Pointer to copy of master to be restored when restore() is called.">d_data</a> : NULL;
<a name="l00246"></a>00246 }
<a name="l00247"></a>00247 <span class="comment"></span>
<a name="l00248"></a>00248 <span class="comment"> //! Set the current object to be invalid</span>
<a name="l00249"></a>00249 <span class="comment"></span> <span class="keyword">virtual</span> <span class="keywordtype">void</span> setNull(<span class="keywordtype">void</span>) = 0;
<a name="l00250"></a>00250 <span class="comment"></span>
<a name="l00251"></a>00251 <span class="comment"> //! Return our name (for debugging)</span>
<a name="l00252"></a>00252 <span class="comment"></span> <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(<span class="keyword">virtual</span> std::string name() <span class="keyword">const</span> { <span class="keywordflow">return</span> d_name; })
<a name="l00253"></a>00253 <span class="comment"></span>
<a name="l00254"></a>00254 <span class="comment"> //! Get context memory manager</span>
<a name="l00255"></a><a class="code" href="classCVC3_1_1ContextObj.html#a0214fcea72b0bbb4de7a8cfa4fde47d0">00255</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1ContextMemoryManager.html" title="ContextMemoryManager.">ContextMemoryManager</a>* <a class="code" href="classCVC3_1_1ContextObj.html#a0214fcea72b0bbb4de7a8cfa4fde47d0" title="Return our name (for debugging)">getCMM</a>() { <span class="keywordflow">return</span> d_scope->getCMM(); }
<a name="l00256"></a>00256
<a name="l00257"></a>00257 <span class="keyword">public</span>:<span class="comment"></span>
<a name="l00258"></a>00258 <span class="comment"> //! Create a new ContextObj.</span>
<a name="l00259"></a>00259 <span class="comment"></span><span class="comment"> /*!</span>
<a name="l00260"></a>00260 <span class="comment"> * The initial scope is set to the bottom scope by default, to</span>
<a name="l00261"></a>00261 <span class="comment"> * reduce the work of pop() (otherwise, if the object is defined</span>
<a name="l00262"></a>00262 <span class="comment"> * only on a very high scope, its scope will be moved down with each</span>
<a name="l00263"></a>00263 <span class="comment"> * pop). If 'atBottomScope' == false, the scope is set to the</span>
<a name="l00264"></a>00264 <span class="comment"> * current scope.</span>
<a name="l00265"></a>00265 <span class="comment"> */</span>
<a name="l00266"></a>00266 <a class="code" href="classCVC3_1_1ContextObjChain.html#aaa3d900ada369da566fe2d896aee9a5a">ContextObj</a>(<a class="code" href="classCVC3_1_1Context.html">Context</a>* context);
<a name="l00267"></a>00267 <span class="keyword">virtual</span> ~<a class="code" href="classCVC3_1_1ContextObj.html">ContextObj</a>();
<a name="l00268"></a>00268
<a name="l00269"></a><a class="code" href="classCVC3_1_1ContextObj.html#abf9828c2d05c7d48a55827ae4c117b91">00269</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1ContextObj.html#abf9828c2d05c7d48a55827ae4c117b91">level</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> (d_scope==NULL)? 0 : d_scope->level(); }
<a name="l00270"></a><a class="code" href="classCVC3_1_1ContextObj.html#a136ad204e9ea96ee300de82ea534277e">00270</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1ContextObj.html#a136ad204e9ea96ee300de82ea534277e">isCurrent</a>(<span class="keywordtype">int</span> scope = -1)<span class="keyword"> const </span>{
<a name="l00271"></a>00271 <span class="keywordflow">if</span>(scope >= 0) <span class="keywordflow">return</span> d_scope->level() == scope;
<a name="l00272"></a>00272 <span class="keywordflow">else</span> <span class="keywordflow">return</span> d_scope->isCurrent();
<a name="l00273"></a>00273 }
<a name="l00274"></a><a class="code" href="classCVC3_1_1ContextObj.html#a780166170b1df8eb7a7632eae66c3511">00274</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ContextObj.html#a780166170b1df8eb7a7632eae66c3511">makeCurrent</a>(<span class="keywordtype">int</span> scope = -1) { <span class="keywordflow">if</span> (!isCurrent(scope)) update(scope); }
<a name="l00275"></a>00275 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(<span class="keywordtype">void</span> setName(<span class="keyword">const</span> std::string& name) { d_name=name; })
<a name="l00276"></a>00276
<a name="l00277"></a><a class="code" href="classCVC3_1_1ContextObj.html#ae7d472424f3564f2891b3817cf663a82">00277</a> <span class="keywordtype">void</span>* <span class="keyword">operator</span> <span class="keyword">new</span>(<span class="keywordtype">size_t</span> size, <a class="code" href="classCVC3_1_1MemoryManager.html">MemoryManager</a>* mm) {
<a name="l00278"></a>00278 <span class="keywordflow">return</span> mm-><a class="code" href="classCVC3_1_1MemoryManager.html#a3db7efbc4b956bd423a73e1157d70ce0">newData</a>(size);
<a name="l00279"></a>00279 }
<a name="l00280"></a><a class="code" href="classCVC3_1_1ContextObj.html#a4dae6e1bc97dc38561af62b1487f0255">00280</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ContextObj.html#a4dae6e1bc97dc38561af62b1487f0255">operator delete</a>(<span class="keywordtype">void</span>* pMem, <a class="code" href="classCVC3_1_1MemoryManager.html">MemoryManager</a>* mm) {
<a name="l00281"></a>00281 mm-><a class="code" href="classCVC3_1_1MemoryManager.html#ad29fac88d3a07566d9a8f9dc8d8e059c">deleteData</a>(pMem);
<a name="l00282"></a>00282 }
<a name="l00283"></a>00283
<a name="l00284"></a>00284 <span class="comment">// If you use this operator, you have to call free yourself when the memory</span>
<a name="l00285"></a>00285 <span class="comment">// is freed.</span>
<a name="l00286"></a><a class="code" href="classCVC3_1_1ContextObj.html#ae955149dca0473868724c8805a7027a0">00286</a> <span class="keywordtype">void</span>* <a class="code" href="classCVC3_1_1ContextObj.html#ae955149dca0473868724c8805a7027a0">operator new</a>(<span class="keywordtype">size_t</span> size, <span class="keywordtype">bool</span> b) {
<a name="l00287"></a>00287 <span class="keywordflow">return</span> malloc(size);
<a name="l00288"></a>00288 }
<a name="l00289"></a><a class="code" href="classCVC3_1_1ContextObj.html#ab58c5aed682cce1741b361c1e5737b60">00289</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ContextObj.html#ab58c5aed682cce1741b361c1e5737b60">operator delete</a>(<span class="keywordtype">void</span>* pMem, <span class="keywordtype">bool</span> b) {
<a name="l00290"></a>00290 free(pMem);
<a name="l00291"></a>00291 }
<a name="l00292"></a>00292
<a name="l00293"></a><a class="code" href="classCVC3_1_1ContextObj.html#a01534742bb67d56320ed5bf12d50bcdf">00293</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ContextObj.html#a01534742bb67d56320ed5bf12d50bcdf">operator delete</a>(<span class="keywordtype">void</span>*) { }
<a name="l00294"></a>00294 };
<a name="l00295"></a>00295 <span class="comment"></span>
<a name="l00296"></a>00296 <span class="comment">///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00297"></a>00297 <span class="comment"></span><span class="comment">// //</span>
<a name="l00298"></a>00298 <span class="comment">// Class: Context //</span>
<a name="l00299"></a>00299 <span class="comment">// Author: Clark Barrett //</span>
<a name="l00300"></a>00300 <span class="comment">// Created: Thu Feb 13 00:24:59 2003 //</span><span class="comment"></span>
<a name="l00301"></a>00301 <span class="comment">/*!</span>
<a name="l00302"></a>00302 <span class="comment"> * Encapsulates the general notion of stack-based saving and restoring</span>
<a name="l00303"></a>00303 <span class="comment"> * of a database.</span>
<a name="l00304"></a>00304 <span class="comment"> */</span><span class="comment"></span>
<a name="l00305"></a>00305 <span class="comment">///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00306"></a><a class="code" href="classCVC3_1_1Context.html">00306</a> <span class="comment"></span><span class="keyword">class </span><a class="code" href="os_8h.html#a0035aac6379df39aa69feba98b2751ba">CVC_DLL</a> <a class="code" href="classCVC3_1_1Context.html">Context</a> {<span class="comment"></span>
<a name="l00307"></a>00307 <span class="comment"> //! Context Manager</span>
<a name="l00308"></a><a class="code" href="classCVC3_1_1Context.html#a7343dd981f95ec6ba21b671dd35bd1c0">00308</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1ContextManager.html" title="Manager for multiple contexts. Also holds current context.">ContextManager</a>* <a class="code" href="classCVC3_1_1Context.html#a7343dd981f95ec6ba21b671dd35bd1c0" title="Context Manager.">d_cm</a>;
<a name="l00309"></a>00309 <span class="comment"></span>
<a name="l00310"></a>00310 <span class="comment"> //! Name of context</span>
<a name="l00311"></a><a class="code" href="classCVC3_1_1Context.html#a0c8783f0025ea074a884e1e3e812e0c3">00311</a> <span class="comment"></span> std::string <a class="code" href="classCVC3_1_1Context.html#a0c8783f0025ea074a884e1e3e812e0c3" title="Name of context.">d_name</a>;
<a name="l00312"></a>00312 <span class="comment"></span>
<a name="l00313"></a>00313 <span class="comment"> //! Context ID</span>
<a name="l00314"></a><a class="code" href="classCVC3_1_1Context.html#a2f27f6781c9e1928c75c2bb5021fc818">00314</a> <span class="comment"></span> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1Context.html#a2f27f6781c9e1928c75c2bb5021fc818" title="Context ID.">d_id</a>;
<a name="l00315"></a>00315 <span class="comment"></span>
<a name="l00316"></a>00316 <span class="comment"> //! Pointer to top and bottom scopes of context</span>
<a name="l00317"></a><a class="code" href="classCVC3_1_1Context.html#a144c6c91ffad1f3df7f9532aaa534695">00317</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1Scope.html">Scope</a>* <a class="code" href="classCVC3_1_1Context.html#a144c6c91ffad1f3df7f9532aaa534695" title="Pointer to top and bottom scopes of context.">d_topScope</a>;
<a name="l00318"></a><a class="code" href="classCVC3_1_1Context.html#ad90387cfc51d161f939a8525eac7199b">00318</a> <a class="code" href="classCVC3_1_1Scope.html">Scope</a>* <a class="code" href="classCVC3_1_1Context.html#ad90387cfc51d161f939a8525eac7199b">d_bottomScope</a>;
<a name="l00319"></a>00319 <span class="comment"></span>
<a name="l00320"></a>00320 <span class="comment"> //! List of objects to notify with every pop</span>
<a name="l00321"></a><a class="code" href="classCVC3_1_1Context.html#aa6bb646c4dbf761ca323a1103810f25a">00321</a> <span class="comment"></span> std::vector<ContextNotifyObj*> <a class="code" href="classCVC3_1_1Context.html#aa6bb646c4dbf761ca323a1103810f25a" title="List of objects to notify with every pop.">d_notifyObjList</a>;
<a name="l00322"></a>00322 <span class="comment"></span>
<a name="l00323"></a>00323 <span class="comment"> //! Stack of free ContextMemoryManager's</span>
<a name="l00324"></a><a class="code" href="classCVC3_1_1Context.html#a17d9c2d8a1cd6d75be47348e17ba9505">00324</a> <span class="comment"></span> std::vector<ContextMemoryManager*> <a class="code" href="classCVC3_1_1Context.html#a17d9c2d8a1cd6d75be47348e17ba9505" title="Stack of free ContextMemoryManager's.">d_cmmStack</a>;
<a name="l00325"></a>00325
<a name="l00326"></a>00326 <span class="keyword">public</span>:
<a name="l00327"></a>00327 <a class="code" href="classCVC3_1_1Context.html">Context</a>(<a class="code" href="classCVC3_1_1ContextManager.html" title="Manager for multiple contexts. Also holds current context.">ContextManager</a>* cm, <span class="keyword">const</span> std::string& name, <span class="keywordtype">int</span> <span class="keywordtype">id</span>);
<a name="l00328"></a>00328 ~<a class="code" href="classCVC3_1_1Context.html">Context</a>();
<a name="l00329"></a>00329 <span class="comment"></span>
<a name="l00330"></a>00330 <span class="comment"> //! Access methods</span>
<a name="l00331"></a><a class="code" href="classCVC3_1_1Context.html#a87538d75fe05145d4cab7da241ff92df">00331</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1ContextManager.html" title="Manager for multiple contexts. Also holds current context.">ContextManager</a>* <a class="code" href="classCVC3_1_1Context.html#a87538d75fe05145d4cab7da241ff92df" title="Access methods.">getCM</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> d_cm; }
<a name="l00332"></a><a class="code" href="classCVC3_1_1Context.html#a7e9ab76906d4f823b1d17daf52c65846">00332</a> <span class="keyword">const</span> std::string& <a class="code" href="classCVC3_1_1Context.html#a7e9ab76906d4f823b1d17daf52c65846">name</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> d_name; }
<a name="l00333"></a><a class="code" href="classCVC3_1_1Context.html#a6fdea8b10aa19405ddee68cfe56f3fda">00333</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1Context.html#a6fdea8b10aa19405ddee68cfe56f3fda">id</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> d_id; }
<a name="l00334"></a><a class="code" href="classCVC3_1_1Context.html#ab898cecdad657568057e6bf989833b35">00334</a> <a class="code" href="classCVC3_1_1Scope.html">Scope</a>* <a class="code" href="classCVC3_1_1Context.html#ab898cecdad657568057e6bf989833b35">topScope</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> d_topScope; }
<a name="l00335"></a><a class="code" href="classCVC3_1_1Context.html#a27c1b08b898fefa46f7a300de95b6f0b">00335</a> <a class="code" href="classCVC3_1_1Scope.html">Scope</a>* <a class="code" href="classCVC3_1_1Context.html#a27c1b08b898fefa46f7a300de95b6f0b">bottomScope</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> d_bottomScope; }
<a name="l00336"></a><a class="code" href="classCVC3_1_1Context.html#ac93285ad9ce68c161eedf7888414bffe">00336</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1Context.html#ac93285ad9ce68c161eedf7888414bffe">level</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> d_topScope->level(); }
<a name="l00337"></a>00337
<a name="l00338"></a>00338 <span class="keywordtype">void</span> <a class="code" href="group__ExprStream__Manip.html#ga2a0348c6d3f94f2f8febc6dd0a9c3218" title="Set the indentation to the current position.">push</a>();
<a name="l00339"></a>00339 <span class="keywordtype">void</span> <a class="code" href="group__ExprStream__Manip.html#gaddb050a787be87116afc51791293d3be" title="Restore the indentation.">pop</a>();
<a name="l00340"></a>00340 <span class="keywordtype">void</span> popto(<span class="keywordtype">int</span> toLevel);
<a name="l00341"></a><a class="code" href="classCVC3_1_1Context.html#ab6ca3250ba3bbf41a813d9feb077ffef">00341</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Context.html#ab6ca3250ba3bbf41a813d9feb077ffef">addNotifyObj</a>(<a class="code" href="classCVC3_1_1ContextNotifyObj.html">ContextNotifyObj</a>* obj) { d_notifyObjList.push_back(obj); }
<a name="l00342"></a>00342 <span class="keywordtype">void</span> deleteNotifyObj(<a class="code" href="classCVC3_1_1ContextNotifyObj.html">ContextNotifyObj</a>* obj);
<a name="l00343"></a>00343 <span class="keywordtype">unsigned</span> <span class="keywordtype">long</span> getMemory(<span class="keywordtype">int</span> verbosity);
<a name="l00344"></a>00344 };
<a name="l00345"></a>00345
<a name="l00346"></a>00346 <span class="comment">// Have to define after Context class</span>
<a name="l00347"></a><a class="code" href="group__Context.html#ga3a1efd364586330635a668eae3d2612d">00347</a> <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="group__Context.html#ga3a1efd364586330635a668eae3d2612d">Scope::isCurrent</a>(<span class="keywordtype">void</span>)<span class="keyword"> const</span>
<a name="l00348"></a>00348 <span class="keyword"> </span>{ <span class="keywordflow">return</span> <span class="keyword">this</span> == d_context->topScope(); }
<a name="l00349"></a>00349
<a name="l00350"></a><a class="code" href="group__Context.html#ga3fcf473cd27da6c7498f462650f75ac8">00350</a> <span class="keyword">inline</span> <span class="keywordtype">void</span> <a class="code" href="group__Context.html#ga3fcf473cd27da6c7498f462650f75ac8" title="Called by ContextObj when created.">Scope::addToChain</a>(<a class="code" href="classCVC3_1_1ContextObjChain.html">ContextObjChain</a>* obj) {
<a name="l00351"></a>00351 <span class="keywordflow">if</span>(d_restoreChain != NULL)
<a name="l00352"></a>00352 d_restoreChain->d_restoreChainPrev = &(obj-><a class="code" href="classCVC3_1_1ContextObjChain.html#afa940ba625d121fe37a659d7caf7f558" title="Next link in chain.">d_restoreChainNext</a>);
<a name="l00353"></a>00353 obj-><a class="code" href="classCVC3_1_1ContextObjChain.html#afa940ba625d121fe37a659d7caf7f558" title="Next link in chain.">d_restoreChainNext</a> = d_restoreChain;
<a name="l00354"></a>00354 obj-><a class="code" href="classCVC3_1_1ContextObjChain.html#af0e39b718fff489ee96dfb6b4e59d03d" title="Pointer to the pointer of the previous object which points to us. This makes a doubly-linked list for...">d_restoreChainPrev</a> = &d_restoreChain;
<a name="l00355"></a>00355 d_restoreChain = obj;
<a name="l00356"></a>00356 }
<a name="l00357"></a>00357
<a name="l00358"></a><a class="code" href="group__Context.html#ga745d55cc6d3ab3bea1afe675fd7ce7a7">00358</a> <span class="keyword">inline</span> <a class="code" href="classCVC3_1_1Scope.html">Scope</a>* <a class="code" href="group__Context.html#ga745d55cc6d3ab3bea1afe675fd7ce7a7">Scope::topScope</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> d_context-><a class="code" href="group__Context.html#ga745d55cc6d3ab3bea1afe675fd7ce7a7">topScope</a>(); }
<a name="l00359"></a>00359
<a name="l00360"></a><a class="code" href="group__Context.html#ga1b0a5ef8d8aef498218f0dfddea851a7">00360</a> <span class="keyword">inline</span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ContextObjChain.html#a83e5207b9d496337691b30f072c117c7" title="Restore from d_data to d_master.">Scope::restore</a>(<span class="keywordtype">void</span>) {
<a name="l00361"></a>00361 <span class="comment">// TRACE_MSG("context verbose", "Scope::restore() {");</span>
<a name="l00362"></a>00362 <span class="keywordflow">while</span> (d_restoreChain != NULL) d_restoreChain = d_restoreChain-><a class="code" href="classCVC3_1_1ContextObjChain.html#a83e5207b9d496337691b30f072c117c7" title="Restore from d_data to d_master.">restore</a>();
<a name="l00363"></a>00363 <span class="comment">// TRACE_MSG("context verbose", "Scope::restore() }");</span>
<a name="l00364"></a>00364 }
<a name="l00365"></a>00365
<a name="l00366"></a>00366 <span class="comment">// Create a new ContextObj. The initial scope is set to the bottom</span>
<a name="l00367"></a>00367 <span class="comment">// scope by default, to reduce the work of pop() (otherwise, if the</span>
<a name="l00368"></a>00368 <span class="comment">// object is defined only on a very high scope, its scope will be</span>
<a name="l00369"></a>00369 <span class="comment">// moved down with each pop). If 'atBottomScope' == false, the</span>
<a name="l00370"></a>00370 <span class="comment">// scope is set to the current scope.</span>
<a name="l00371"></a><a class="code" href="group__Context.html#gab3133d36e9074eb69255c4f36ccc3aad">00371</a> <span class="keyword">inline</span> <a class="code" href="classCVC3_1_1ContextObjChain.html#aaa3d900ada369da566fe2d896aee9a5a">ContextObj::ContextObj</a>(<a class="code" href="classCVC3_1_1Context.html">Context</a>* context)
<a name="l00372"></a>00372 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(: d_name(<span class="stringliteral">"ContextObj"</span>))
<a name="l00373"></a>00373 {
<a name="l00374"></a>00374 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(d_active=<span class="keyword">true</span>;)
<a name="l00375"></a>00375 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(context != NULL, <span class="stringliteral">"NULL context pointer"</span>);
<a name="l00376"></a>00376 d_scope = context->bottomScope();
<a name="l00377"></a>00377 <a class="code" href="classCVC3_1_1ContextObjChain.html#a64049e510cf64e4a96d6e1134479f467" title="Pointer to the previous copy which belongs to the same master.">d_restore</a> = <span class="keyword">new</span>(<span class="keyword">true</span>) <a class="code" href="classCVC3_1_1ContextObjChain.html#a689d17e7768d0f95cc6c36d27bdb8368" title="Private constructor (only friends can use it)">ContextObjChain</a>(NULL, <span class="keyword">this</span>, NULL);
<a name="l00378"></a>00378 d_scope->addToChain(<a class="code" href="classCVC3_1_1ContextObjChain.html#a64049e510cf64e4a96d6e1134479f467" title="Pointer to the previous copy which belongs to the same master.">d_restore</a>);
<a name="l00379"></a>00379 <span class="comment">// if (atBottomScope) d_scope->addSpecialObject(d_restore);</span>
<a name="l00380"></a>00380 <span class="comment">// TRACE("context verbose", "ContextObj()[", this, "]");</span>
<a name="l00381"></a>00381 }
<a name="l00382"></a>00382
<a name="l00383"></a>00383
<a name="l00384"></a>00384 <span class="comment">/****************************************************************************/</span><span class="comment"></span>
<a name="l00385"></a>00385 <span class="comment">//! Manager for multiple contexts. Also holds current context.</span>
<a name="l00386"></a>00386 <span class="comment"></span><span class="comment">/*!</span>
<a name="l00387"></a>00387 <span class="comment"> * Author: Clark Barrett</span>
<a name="l00388"></a>00388 <span class="comment"> *</span>
<a name="l00389"></a>00389 <span class="comment"> * Created: Thu Feb 13 00:26:29 2003</span>
<a name="l00390"></a>00390 <span class="comment"> */</span>
<a name="l00391"></a>00391 <span class="comment">/****************************************************************************/</span>
<a name="l00392"></a>00392
<a name="l00393"></a><a class="code" href="classCVC3_1_1ContextManager.html">00393</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1ContextManager.html" title="Manager for multiple contexts. Also holds current context.">ContextManager</a> {
<a name="l00394"></a><a class="code" href="classCVC3_1_1ContextManager.html#aac2e185eb1efd9ee1d201c86cf5f32a1">00394</a> <a class="code" href="classCVC3_1_1Context.html">Context</a>* <a class="code" href="classCVC3_1_1ContextManager.html#aac2e185eb1efd9ee1d201c86cf5f32a1">d_curContext</a>;
<a name="l00395"></a><a class="code" href="classCVC3_1_1ContextManager.html#abc7293587eae6e58750a7b44597169f4">00395</a> std::vector<Context*> <a class="code" href="classCVC3_1_1ContextManager.html#abc7293587eae6e58750a7b44597169f4">d_contexts</a>;
<a name="l00396"></a>00396
<a name="l00397"></a>00397 <span class="keyword">public</span>:
<a name="l00398"></a>00398 <a class="code" href="classCVC3_1_1ContextManager.html" title="Manager for multiple contexts. Also holds current context.">ContextManager</a>();
<a name="l00399"></a>00399 ~<a class="code" href="classCVC3_1_1ContextManager.html" title="Manager for multiple contexts. Also holds current context.">ContextManager</a>();
<a name="l00400"></a>00400
<a name="l00401"></a><a class="code" href="classCVC3_1_1ContextManager.html#a90e301927cc935d561b81761d4ab2ee8">00401</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ContextManager.html#a90e301927cc935d561b81761d4ab2ee8">push</a>() { d_curContext->push(); }
<a name="l00402"></a><a class="code" href="classCVC3_1_1ContextManager.html#ae74b114a270baff44940a8916d958e9c">00402</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ContextManager.html#ae74b114a270baff44940a8916d958e9c">pop</a>() { d_curContext->pop(); }
<a name="l00403"></a><a class="code" href="classCVC3_1_1ContextManager.html#a0a0dc6f3a5a7ce61cf02566fe31b8691">00403</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ContextManager.html#a0a0dc6f3a5a7ce61cf02566fe31b8691">popto</a>(<span class="keywordtype">int</span> toLevel) { d_curContext->popto(toLevel); }
<a name="l00404"></a><a class="code" href="classCVC3_1_1ContextManager.html#a194f7ddd794eaa876544a45006a3ff6f">00404</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1ContextManager.html#a194f7ddd794eaa876544a45006a3ff6f">scopeLevel</a>() { <span class="keywordflow">return</span> d_curContext->level(); }
<a name="l00405"></a>00405 <a class="code" href="classCVC3_1_1Context.html">Context</a>* createContext(<span class="keyword">const</span> std::string& name=<span class="stringliteral">""</span>);
<a name="l00406"></a><a class="code" href="classCVC3_1_1ContextManager.html#a66a7d900301c1459de90b048623d9297">00406</a> <a class="code" href="classCVC3_1_1Context.html">Context</a>* <a class="code" href="classCVC3_1_1ContextManager.html#a66a7d900301c1459de90b048623d9297">getCurrentContext</a>() { <span class="keywordflow">return</span> d_curContext; }
<a name="l00407"></a>00407 <a class="code" href="classCVC3_1_1Context.html">Context</a>* switchContext(<a class="code" href="classCVC3_1_1Context.html">Context</a>* context);
<a name="l00408"></a>00408 <span class="keywordtype">unsigned</span> <span class="keywordtype">long</span> getMemory(<span class="keywordtype">int</span> verbosity);
<a name="l00409"></a>00409 };
<a name="l00410"></a>00410
<a name="l00411"></a>00411 <span class="comment">/****************************************************************************/</span><span class="comment"></span>
<a name="l00412"></a>00412 <span class="comment">/*! Author: Clark Barrett</span>
<a name="l00413"></a>00413 <span class="comment"> *</span>
<a name="l00414"></a>00414 <span class="comment"> * Created: Sat Feb 22 16:21:47 2003</span>
<a name="l00415"></a>00415 <span class="comment"> *</span>
<a name="l00416"></a>00416 <span class="comment"> * Lightweight version of ContextObj: objects are simply notified</span>
<a name="l00417"></a>00417 <span class="comment"> * every time there's a pop. notifyPre() is called right before the</span>
<a name="l00418"></a>00418 <span class="comment"> * context is restored, and notify() is called after the context is</span>
<a name="l00419"></a>00419 <span class="comment"> * restored.</span>
<a name="l00420"></a>00420 <span class="comment"> */</span>
<a name="l00421"></a>00421 <span class="comment">/****************************************************************************/</span>
<a name="l00422"></a>00422
<a name="l00423"></a><a class="code" href="classCVC3_1_1ContextNotifyObj.html">00423</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1ContextNotifyObj.html">ContextNotifyObj</a> {
<a name="l00424"></a><a class="code" href="classCVC3_1_1ContextNotifyObj.html#ac26c806e60ca4a0547680edb68f6e39b">00424</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1Context.html">Context</a>;
<a name="l00425"></a>00425 <span class="keyword">protected</span>:
<a name="l00426"></a><a class="code" href="classCVC3_1_1ContextNotifyObj.html#a6ce2c7b1560e4435a89aeafba8d25147">00426</a> <a class="code" href="classCVC3_1_1Context.html">Context</a>* <a class="code" href="classCVC3_1_1ContextNotifyObj.html#a6ce2c7b1560e4435a89aeafba8d25147">d_context</a>;
<a name="l00427"></a>00427 <span class="keyword">public</span>:
<a name="l00428"></a><a class="code" href="classCVC3_1_1ContextNotifyObj.html#a01133c17489dfe8765d792b5c4daea80">00428</a> <a class="code" href="classCVC3_1_1ContextNotifyObj.html">ContextNotifyObj</a>(<a class="code" href="classCVC3_1_1Context.html">Context</a>* context): d_context(context)
<a name="l00429"></a>00429 { context-><a class="code" href="classCVC3_1_1Context.html#ab6ca3250ba3bbf41a813d9feb077ffef">addNotifyObj</a>(<span class="keyword">this</span>); }
<a name="l00430"></a><a class="code" href="classCVC3_1_1ContextNotifyObj.html#adbe5190ea6a81f00fb07d805fa89ad03">00430</a> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1ContextNotifyObj.html#adbe5190ea6a81f00fb07d805fa89ad03">~ContextNotifyObj</a>() {
<a name="l00431"></a>00431 <span class="comment">// If we are being deleted before the context, remove ourselves</span>
<a name="l00432"></a>00432 <span class="comment">// from the notify list. However, if the context is deleted</span>
<a name="l00433"></a>00433 <span class="comment">// before we are, then our d_context will be cleared from ~Context()</span>
<a name="l00434"></a>00434 <span class="keywordflow">if</span>(d_context!=NULL) d_context->deleteNotifyObj(<span class="keyword">this</span>);
<a name="l00435"></a>00435 }
<a name="l00436"></a><a class="code" href="classCVC3_1_1ContextNotifyObj.html#a71e8fc4cf1ab52a2cba9708dfe74633e">00436</a> <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ContextNotifyObj.html#a71e8fc4cf1ab52a2cba9708dfe74633e">notifyPre</a>(<span class="keywordtype">void</span>) {}
<a name="l00437"></a><a class="code" href="classCVC3_1_1ContextNotifyObj.html#abad0e373f144d6004cc61ff4604b54c0">00437</a> <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ContextNotifyObj.html#abad0e373f144d6004cc61ff4604b54c0">notify</a>(<span class="keywordtype">void</span>) {}
<a name="l00438"></a><a class="code" href="classCVC3_1_1ContextNotifyObj.html#aa5be41ab0c2f9dfd4d5f86d7cda3b85e">00438</a> <span class="keyword">virtual</span> <span class="keywordtype">unsigned</span> <span class="keywordtype">long</span> <a class="code" href="classCVC3_1_1ContextNotifyObj.html#aa5be41ab0c2f9dfd4d5f86d7cda3b85e">getMemory</a>(<span class="keywordtype">int</span> verbosity) { <span class="keywordflow">return</span> <span class="keyword">sizeof</span>(<a class="code" href="classCVC3_1_1ContextNotifyObj.html">ContextNotifyObj</a>); }
<a name="l00439"></a>00439 };
<a name="l00440"></a>00440 <span class="comment"></span>
<a name="l00441"></a>00441 <span class="comment">/*@}*/</span> <span class="comment">// end of group Context</span>
<a name="l00442"></a>00442
<a name="l00443"></a>00443 }
<a name="l00444"></a>00444
<a name="l00445"></a>00445 <span class="preprocessor">#endif</span>
</pre></div></div>
</div>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
