<!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: variable.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">variable.h</div> </div>
</div>
<div class="contents">
<a href="variable_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 variable.h</span>
<a name="l00004"></a>00004 <span class="comment"> * </span>
<a name="l00005"></a>00005 <span class="comment"> * Author: Sergey Berezin</span>
<a name="l00006"></a>00006 <span class="comment"> * </span>
<a name="l00007"></a>00007 <span class="comment"> * Created: Fri Apr 25 11:52:17 2003</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"> * A data structure representing a variable in the search engine. It</span>
<a name="l00019"></a>00019 <span class="comment"> * is a smart pointer with a uniquifying mechanism similar to Expr,</span>
<a name="l00020"></a>00020 <span class="comment"> * and a variable is uniquely determined by its expression. It can be</span>
<a name="l00021"></a>00021 <span class="comment"> * thought of as an Expr with additional attributes, but the type is</span>
<a name="l00022"></a>00022 <span class="comment"> * different, so it will not be confused with other Exprs.</span>
<a name="l00023"></a>00023 <span class="comment"> */</span>
<a name="l00024"></a>00024 <span class="comment">/*****************************************************************************/</span>
<a name="l00025"></a>00025
<a name="l00026"></a>00026 <span class="preprocessor">#ifndef _cvc3__variable_h_</span>
<a name="l00027"></a>00027 <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__variable_h_</span>
<a name="l00028"></a>00028 <span class="preprocessor"></span>
<a name="l00029"></a>00029 <span class="preprocessor">#include "<a class="code" href="expr_8h.html" title="Definition of the API to expression package. See class Expr for details.">expr.h</a>"</span>
<a name="l00030"></a>00030
<a name="l00031"></a>00031 <span class="keyword">namespace </span>CVC3 {
<a name="l00032"></a>00032
<a name="l00033"></a>00033 <span class="keyword">class </span>VariableManager;
<a name="l00034"></a>00034 <span class="keyword">class </span>VariableValue;
<a name="l00035"></a>00035 <span class="keyword">class </span>Clause;
<a name="l00036"></a>00036 <span class="keyword">class </span>SearchEngineRules;
<a name="l00037"></a>00037
<a name="l00038"></a>00038 <span class="comment">// The main "smart pointer" class</span>
<a name="l00039"></a><a class="code" href="classCVC3_1_1Variable.html">00039</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1Variable.html">Variable</a> {
<a name="l00040"></a>00040 <span class="keyword">private</span>:
<a name="l00041"></a><a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">00041</a> <a class="code" href="classCVC3_1_1VariableValue.html">VariableValue</a>* <a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>;
<a name="l00042"></a>00042 <span class="comment">// Private methods</span>
<a name="l00043"></a>00043 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1Variable.html#a3511123177ecb1126031b1b88d37fd0a">deriveThmRec</a>(<span class="keywordtype">bool</span> checkAssump) <span class="keyword">const</span>;
<a name="l00044"></a>00044 <span class="keyword">public</span>:
<a name="l00045"></a>00045 <span class="comment">// Default constructor</span>
<a name="l00046"></a><a class="code" href="classCVC3_1_1Variable.html#a7659f63344c25dbc8209c4c531b2f0be">00046</a> <a class="code" href="classCVC3_1_1Variable.html#a7659f63344c25dbc8209c4c531b2f0be">Variable</a>(): <a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>(NULL) { }
<a name="l00047"></a>00047 <span class="comment">// Constructor from an Expr; if such variable already exists, it</span>
<a name="l00048"></a>00048 <span class="comment">// will be found and used.</span>
<a name="l00049"></a>00049 <a class="code" href="classCVC3_1_1Variable.html#a7659f63344c25dbc8209c4c531b2f0be">Variable</a>(<a class="code" href="classCVC3_1_1VariableManager.html">VariableManager</a>* vm, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);
<a name="l00050"></a>00050 <span class="comment">// Copy constructor</span>
<a name="l00051"></a>00051 <a class="code" href="classCVC3_1_1Variable.html#a7659f63344c25dbc8209c4c531b2f0be">Variable</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Variable.html">Variable</a>& l);
<a name="l00052"></a>00052 <span class="comment">// Destructor</span>
<a name="l00053"></a>00053 <a class="code" href="classCVC3_1_1Variable.html#a21a9c85dd3b1320e8192fd581da15af4">~Variable</a>();
<a name="l00054"></a>00054 <span class="comment">// Assignment</span>
<a name="l00055"></a>00055 <a class="code" href="classCVC3_1_1Variable.html">Variable</a>& <a class="code" href="classCVC3_1_1Variable.html#a551554c97de770f4160444c440342ac5">operator=</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Variable.html">Variable</a>& l);
<a name="l00056"></a>00056
<a name="l00057"></a><a class="code" href="classCVC3_1_1Variable.html#a35c435274fa96599d47f16239b843584">00057</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Variable.html#a35c435274fa96599d47f16239b843584">isNull</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a> == NULL; }
<a name="l00058"></a>00058
<a name="l00059"></a>00059 <span class="comment">// Accessors</span>
<a name="l00060"></a>00060
<a name="l00061"></a>00061 <span class="comment">// Expr is the only constant attribute of a variable; other</span>
<a name="l00062"></a>00062 <span class="comment">// attributes can be changed.</span>
<a name="l00063"></a>00063 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="classCVC3_1_1Variable.html#af85a6bbfd1529fce66f70d0012556fdf">getExpr</a>() <span class="keyword">const</span>;
<a name="l00064"></a>00064 <span class="comment">// The Expr of the inverse of the variable. This function is</span>
<a name="l00065"></a>00065 <span class="comment">// caching, so !e is only constructed once.</span>
<a name="l00066"></a>00066 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="classCVC3_1_1Variable.html#a6d8d3752f50dc4ce55d12e252398c837">getNegExpr</a>() <span class="keyword">const</span>;
<a name="l00067"></a>00067
<a name="l00068"></a>00068 <span class="comment">// IMPORTANT: Value can be -1 (false), 1 (true), or 0 (unresolved)</span>
<a name="l00069"></a>00069 <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1Variable.html#a36e8ce7a305e07e00adc90f6c22c4916">getValue</a>() <span class="keyword">const</span>;
<a name="l00070"></a>00070 <span class="comment">// If the value is set, scope level and either a theorem or</span>
<a name="l00071"></a>00071 <span class="comment">// an antecedent clause must be defined</span>
<a name="l00072"></a>00072 <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1Variable.html#a6e50e61e2eaf7054bd1d84e4137ba270">getScope</a>() <span class="keyword">const</span>;
<a name="l00073"></a>00073 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& <a class="code" href="classCVC3_1_1Variable.html#a6cdc655ea6aaf36c8e8029af0dc41075">getTheorem</a>() <span class="keyword">const</span>;
<a name="l00074"></a>00074 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Clause.html" title="A class representing a CNF clause (a smart pointer)">Clause</a>& <a class="code" href="classCVC3_1_1Variable.html#a5bbd362f586ab0dbbc3432d140f77aab">getAntecedent</a>() <span class="keyword">const</span>;
<a name="l00075"></a>00075 <span class="comment">// Index of this variable in the antecedent clause; if it is -1,</span>
<a name="l00076"></a>00076 <span class="comment">// the variable is FALSE, and that clause caused the contradiction</span>
<a name="l00077"></a>00077 <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1Variable.html#a681407094080368feea5c496ed3bdb69">getAntecedentIdx</a>() <span class="keyword">const</span>;
<a name="l00078"></a>00078 <span class="comment">// Theorem of the form l |- l produced by the 'assump' rule, if</span>
<a name="l00079"></a>00079 <span class="comment">// this variable is a splitter, or a new intermediate assumption</span>
<a name="l00080"></a>00080 <span class="comment">// is generated for it.</span>
<a name="l00081"></a>00081 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& <a class="code" href="classCVC3_1_1Variable.html#a535715bc38709f902feb3f77aef4f89d">getAssumpThm</a>() <span class="keyword">const</span>;
<a name="l00082"></a>00082 <span class="comment">// Setting the attributes: it can be either derived from the</span>
<a name="l00083"></a>00083 <span class="comment">// antecedent clause, or by a theorem. The scope level is set to</span>
<a name="l00084"></a>00084 <span class="comment">// the current scope.</span>
<a name="l00085"></a>00085 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Variable.html#ac1d2bf9a1a8eec600ffa18b679ef4d2c">setValue</a>(<span class="keywordtype">int</span> val, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Clause.html" title="A class representing a CNF clause (a smart pointer)">Clause</a>& c, <span class="keywordtype">int</span> idx);
<a name="l00086"></a>00086 <span class="comment">// The theorem's expr must be the same as the variable's expr or</span>
<a name="l00087"></a>00087 <span class="comment">// its negation, and the scope is the lowest scope where all</span>
<a name="l00088"></a>00088 <span class="comment">// assumptions of the theorem are true</span>
<a name="l00089"></a>00089 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Variable.html#ac1d2bf9a1a8eec600ffa18b679ef4d2c">setValue</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);
<a name="l00090"></a>00090 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Variable.html#ac1d2bf9a1a8eec600ffa18b679ef4d2c">setValue</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm, <span class="keywordtype">int</span> scope);
<a name="l00091"></a>00091
<a name="l00092"></a>00092 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Variable.html#a688678fbc2dc4e25d9dbba2e4c7d72a5">setAssumpThm</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& a, <span class="keywordtype">int</span> scope);
<a name="l00093"></a>00093 <span class="comment">// Derive the theorem for either the variable or its negation. If</span>
<a name="l00094"></a>00094 <span class="comment">// the value is set by a theorem, that theorem is returned;</span>
<a name="l00095"></a>00095 <span class="comment">// otherwise a unit propagation rule is applied to the antecedent</span>
<a name="l00096"></a>00096 <span class="comment">// clause.</span>
<a name="l00097"></a>00097 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1Variable.html#ad499afb9e33f92c2efd7cf92638e0396">deriveTheorem</a>() <span class="keyword">const</span>;
<a name="l00098"></a>00098
<a name="l00099"></a>00099 <span class="comment">// Accessing Chaff counters (read and modified by reference)</span>
<a name="l00100"></a>00100 <span class="keywordtype">unsigned</span>& <a class="code" href="classCVC3_1_1Variable.html#ac78bae977cd6dead5e79debc77f52efc">count</a>(<span class="keywordtype">bool</span> neg);
<a name="l00101"></a>00101 <span class="keywordtype">unsigned</span>& <a class="code" href="classCVC3_1_1Variable.html#acc8e18908c0b3c74811225c58f57c50d">countPrev</a>(<span class="keywordtype">bool</span> neg);
<a name="l00102"></a>00102 <span class="keywordtype">int</span>& <a class="code" href="classCVC3_1_1Variable.html#aa4c74c18d5e3b6dff3a87dbb9600ea54">score</a>(<span class="keywordtype">bool</span> neg);
<a name="l00103"></a>00103 <span class="keywordtype">bool</span>& <a class="code" href="classCVC3_1_1Variable.html#a0e4d827e11f6308f9c9bc957f0f7d2f7">added</a>(<span class="keywordtype">bool</span> neg);
<a name="l00104"></a>00104 <span class="comment">// Read-only versions</span>
<a name="l00105"></a>00105 <span class="keywordtype">unsigned</span> <a class="code" href="classCVC3_1_1Variable.html#ac78bae977cd6dead5e79debc77f52efc">count</a>(<span class="keywordtype">bool</span> neg) <span class="keyword">const</span>;
<a name="l00106"></a>00106 <span class="keywordtype">unsigned</span> <a class="code" href="classCVC3_1_1Variable.html#acc8e18908c0b3c74811225c58f57c50d">countPrev</a>(<span class="keywordtype">bool</span> neg) <span class="keyword">const</span>;
<a name="l00107"></a>00107 <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1Variable.html#aa4c74c18d5e3b6dff3a87dbb9600ea54">score</a>(<span class="keywordtype">bool</span> neg) <span class="keyword">const</span>;
<a name="l00108"></a>00108 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Variable.html#a0e4d827e11f6308f9c9bc957f0f7d2f7">added</a>(<span class="keywordtype">bool</span> neg) <span class="keyword">const</span>;
<a name="l00109"></a>00109 <span class="comment">// Watch pointer access</span>
<a name="l00110"></a>00110 std::vector<std::pair<Clause, int> >& <a class="code" href="classCVC3_1_1Variable.html#a561c4d0ef9d246de12d5b22aef375315">wp</a>(<span class="keywordtype">bool</span> neg) <span class="keyword">const</span>;
<a name="l00111"></a>00111 <span class="comment">// Friend methods</span>
<a name="l00112"></a><a class="code" href="classCVC3_1_1Variable.html#a0f0f37a880864202b17cff52e9526026">00112</a> <span class="keyword">friend</span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Variable.html#a0f0f37a880864202b17cff52e9526026">operator==</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Variable.html">Variable</a>& l1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Variable.html">Variable</a>& l2) {
<a name="l00113"></a>00113 <span class="keywordflow">return</span> l1.<a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a> == l2.<a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>;
<a name="l00114"></a>00114 }
<a name="l00115"></a>00115 <span class="comment">// Printing</span>
<a name="l00116"></a>00116 <span class="keyword">friend</span> std::ostream& <a class="code" href="classCVC3_1_1Variable.html#a998720ee70ba784d399ec3a97c8719b6">operator<<</a>(std::ostream& os, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Variable.html">Variable</a>& l);
<a name="l00117"></a>00117 std::string <a class="code" href="classCVC3_1_1Variable.html#a82f724d0ece90488867aa2de8cc43c32">toString</a>() <span class="keyword">const</span>;
<a name="l00118"></a>00118 }; <span class="comment">// end of class Variable</span>
<a name="l00119"></a>00119
<a name="l00120"></a><a class="code" href="classCVC3_1_1Literal.html">00120</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1Literal.html">Literal</a> {
<a name="l00121"></a>00121 <span class="keyword">private</span>:
<a name="l00122"></a><a class="code" href="classCVC3_1_1Literal.html#a9ade1c15df2b3f10d263c4f01d6ea8d5">00122</a> <a class="code" href="classCVC3_1_1Variable.html">Variable</a> <a class="code" href="classCVC3_1_1Literal.html#a9ade1c15df2b3f10d263c4f01d6ea8d5">d_var</a>;
<a name="l00123"></a><a class="code" href="classCVC3_1_1Literal.html#a674fd67861c9bca1aef2179728745f36">00123</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Literal.html#a674fd67861c9bca1aef2179728745f36">d_negative</a>;
<a name="l00124"></a>00124 <span class="keyword">public</span>:
<a name="l00125"></a>00125 <span class="comment">// Constructors: from a variable</span>
<a name="l00126"></a><a class="code" href="classCVC3_1_1Literal.html#a1066f94f42e8277ca8aa33e2bebfc1fb">00126</a> <a class="code" href="classCVC3_1_1Literal.html#aa24c193b2ed3df0b23278a81703a496a">Literal</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Variable.html">Variable</a>& v, <span class="keywordtype">bool</span> positive = <span class="keyword">true</span>)
<a name="l00127"></a>00127 : <a class="code" href="classCVC3_1_1Literal.html#a9ade1c15df2b3f10d263c4f01d6ea8d5">d_var</a>(v), <a class="code" href="classCVC3_1_1Literal.html#a674fd67861c9bca1aef2179728745f36">d_negative</a>(!positive) { }
<a name="l00128"></a>00128 <span class="comment">// Default constructor</span>
<a name="l00129"></a><a class="code" href="classCVC3_1_1Literal.html#aa24c193b2ed3df0b23278a81703a496a">00129</a> <a class="code" href="classCVC3_1_1Literal.html#aa24c193b2ed3df0b23278a81703a496a">Literal</a>(): <a class="code" href="classCVC3_1_1Literal.html#a674fd67861c9bca1aef2179728745f36">d_negative</a>(false) { }
<a name="l00130"></a>00130 <span class="comment">// from Expr: if e == !e', construct negative literal of e',</span>
<a name="l00131"></a>00131 <span class="comment">// otherwise positive of e</span>
<a name="l00132"></a><a class="code" href="classCVC3_1_1Literal.html#a3146ac3b39f4045619d16e346dba973a">00132</a> <a class="code" href="classCVC3_1_1Literal.html#aa24c193b2ed3df0b23278a81703a496a">Literal</a>(<a class="code" href="classCVC3_1_1VariableManager.html">VariableManager</a>* vm, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e)
<a name="l00133"></a>00133 : <a class="code" href="classCVC3_1_1Literal.html#a9ade1c15df2b3f10d263c4f01d6ea8d5">d_var</a>(vm, (e.isNot())? e[0] : e), <a class="code" href="classCVC3_1_1Literal.html#a674fd67861c9bca1aef2179728745f36">d_negative</a>(e.isNot()) { }
<a name="l00134"></a><a class="code" href="classCVC3_1_1Literal.html#af43cfe38032a00cc8e8e60b0389eeb3e">00134</a> <a class="code" href="classCVC3_1_1Variable.html">Variable</a>& <a class="code" href="classCVC3_1_1Literal.html#af43cfe38032a00cc8e8e60b0389eeb3e">getVar</a>() { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Literal.html#a9ade1c15df2b3f10d263c4f01d6ea8d5">d_var</a>; }
<a name="l00135"></a><a class="code" href="classCVC3_1_1Literal.html#a2f2c48302fa499905d1eb690331f66de">00135</a> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Variable.html">Variable</a>& <a class="code" href="classCVC3_1_1Literal.html#a2f2c48302fa499905d1eb690331f66de">getVar</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Literal.html#a9ade1c15df2b3f10d263c4f01d6ea8d5">d_var</a>; }
<a name="l00136"></a><a class="code" href="classCVC3_1_1Literal.html#aefb2cb8f18bdc70d3130ee7d8dca614c">00136</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Literal.html#aefb2cb8f18bdc70d3130ee7d8dca614c">isPositive</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> !<a class="code" href="classCVC3_1_1Literal.html#a674fd67861c9bca1aef2179728745f36">d_negative</a>; }
<a name="l00137"></a><a class="code" href="classCVC3_1_1Literal.html#aad653dd8534feb823b9d30f060b4e181">00137</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Literal.html#aad653dd8534feb823b9d30f060b4e181">isNegative</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Literal.html#a674fd67861c9bca1aef2179728745f36">d_negative</a>; }
<a name="l00138"></a><a class="code" href="classCVC3_1_1Literal.html#aa63f859d19f8c132864d41bb1805c4c0">00138</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Literal.html#aa63f859d19f8c132864d41bb1805c4c0">isNull</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Literal.html#a9ade1c15df2b3f10d263c4f01d6ea8d5">d_var</a>.<a class="code" href="classCVC3_1_1Variable.html#a35c435274fa96599d47f16239b843584">isNull</a>(); }
<a name="l00139"></a>00139 <span class="comment">// Return var or !var</span>
<a name="l00140"></a><a class="code" href="classCVC3_1_1Literal.html#a4a2e0a421bfcb590c3a7964d2583a94c">00140</a> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="classCVC3_1_1Literal.html#a4a2e0a421bfcb590c3a7964d2583a94c">getExpr</a>()<span class="keyword"> const </span>{
<a name="l00141"></a>00141 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1Literal.html#a674fd67861c9bca1aef2179728745f36">d_negative</a>) <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Literal.html#a9ade1c15df2b3f10d263c4f01d6ea8d5">d_var</a>.<a class="code" href="classCVC3_1_1Variable.html#a6d8d3752f50dc4ce55d12e252398c837">getNegExpr</a>();
<a name="l00142"></a>00142 <span class="keywordflow">else</span> <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Literal.html#a9ade1c15df2b3f10d263c4f01d6ea8d5">d_var</a>.<a class="code" href="classCVC3_1_1Variable.html#af85a6bbfd1529fce66f70d0012556fdf">getExpr</a>();
<a name="l00143"></a>00143 }
<a name="l00144"></a><a class="code" href="classCVC3_1_1Literal.html#a48feb6e7cf83b3a59b94ca0e75627d0f">00144</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1Literal.html#a48feb6e7cf83b3a59b94ca0e75627d0f">getValue</a>()<span class="keyword"> const </span>{
<a name="l00145"></a>00145 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1Literal.html#a674fd67861c9bca1aef2179728745f36">d_negative</a>) <span class="keywordflow">return</span> -(<a class="code" href="classCVC3_1_1Literal.html#a9ade1c15df2b3f10d263c4f01d6ea8d5">d_var</a>.<a class="code" href="classCVC3_1_1Variable.html#a36e8ce7a305e07e00adc90f6c22c4916">getValue</a>());
<a name="l00146"></a>00146 <span class="keywordflow">else</span> <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Literal.html#a9ade1c15df2b3f10d263c4f01d6ea8d5">d_var</a>.<a class="code" href="classCVC3_1_1Variable.html#a36e8ce7a305e07e00adc90f6c22c4916">getValue</a>();
<a name="l00147"></a>00147 }
<a name="l00148"></a><a class="code" href="classCVC3_1_1Literal.html#a2abe99239ecdf75235e242282cd672f2">00148</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1Literal.html#a2abe99239ecdf75235e242282cd672f2">getScope</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Literal.html#af43cfe38032a00cc8e8e60b0389eeb3e">getVar</a>().<a class="code" href="classCVC3_1_1Variable.html#a6e50e61e2eaf7054bd1d84e4137ba270">getScope</a>(); }
<a name="l00149"></a>00149 <span class="comment">// Set the value of the literal</span>
<a name="l00150"></a>00150 <span class="comment">// void setValue(int val, const Clause& c, int idx) {</span>
<a name="l00151"></a>00151 <span class="comment">// d_var.setValue(d_negative? -val : val, c, idx);</span>
<a name="l00152"></a>00152 <span class="comment">// }</span>
<a name="l00153"></a><a class="code" href="classCVC3_1_1Literal.html#ad731e76b4037cb3e5d797543596514a1">00153</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Literal.html#ad731e76b4037cb3e5d797543596514a1">setValue</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm) {
<a name="l00154"></a>00154 <a class="code" href="classCVC3_1_1Literal.html#a9ade1c15df2b3f10d263c4f01d6ea8d5">d_var</a>.<a class="code" href="classCVC3_1_1Variable.html#ac1d2bf9a1a8eec600ffa18b679ef4d2c">setValue</a>(thm, thm.<a class="code" href="classCVC3_1_1Theorem.html#a112466d9793abcf97015233ffdc4ec5e">getScope</a>());
<a name="l00155"></a>00155 }
<a name="l00156"></a><a class="code" href="classCVC3_1_1Literal.html#afd1c69616427acb7bac118dfa627b611">00156</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Literal.html#afd1c69616427acb7bac118dfa627b611">setValue</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm, <span class="keywordtype">int</span> scope) {
<a name="l00157"></a>00157 <a class="code" href="classCVC3_1_1Literal.html#a9ade1c15df2b3f10d263c4f01d6ea8d5">d_var</a>.<a class="code" href="classCVC3_1_1Variable.html#ac1d2bf9a1a8eec600ffa18b679ef4d2c">setValue</a>(thm, scope);
<a name="l00158"></a>00158 }
<a name="l00159"></a><a class="code" href="classCVC3_1_1Literal.html#a9d607c46f54954c7c1371cb8452f8e6f">00159</a> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& <a class="code" href="classCVC3_1_1Literal.html#a9d607c46f54954c7c1371cb8452f8e6f">getTheorem</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Literal.html#a9ade1c15df2b3f10d263c4f01d6ea8d5">d_var</a>.<a class="code" href="classCVC3_1_1Variable.html#a6cdc655ea6aaf36c8e8029af0dc41075">getTheorem</a>(); }
<a name="l00160"></a>00160 <span class="comment">// const Clause& getAntecedent() const { return d_var.getAntecedent(); }</span>
<a name="l00161"></a>00161 <span class="comment">// int getAntecedentIdx() const { return d_var.getAntecedentIdx(); }</span>
<a name="l00162"></a>00162 <span class="comment">// Defined when the literal has a value. Derives a theorem</span>
<a name="l00163"></a>00163 <span class="comment">// proving either this literal or its inverse.</span>
<a name="l00164"></a><a class="code" href="classCVC3_1_1Literal.html#a9d040e10a412d4a86642a9b2776dd258">00164</a> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1Literal.html#a9d040e10a412d4a86642a9b2776dd258">deriveTheorem</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Literal.html#a9ade1c15df2b3f10d263c4f01d6ea8d5">d_var</a>.<a class="code" href="classCVC3_1_1Variable.html#ad499afb9e33f92c2efd7cf92638e0396">deriveTheorem</a>(); }
<a name="l00165"></a>00165 <span class="comment">// Accessing Chaff counters (read and modified by reference)</span>
<a name="l00166"></a><a class="code" href="classCVC3_1_1Literal.html#a4823b2e9ec3a6a13a28c209d22269564">00166</a> <span class="keywordtype">unsigned</span>& <a class="code" href="classCVC3_1_1Literal.html#a4823b2e9ec3a6a13a28c209d22269564">count</a>() { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Literal.html#a9ade1c15df2b3f10d263c4f01d6ea8d5">d_var</a>.<a class="code" href="classCVC3_1_1Variable.html#ac78bae977cd6dead5e79debc77f52efc">count</a>(<a class="code" href="classCVC3_1_1Literal.html#a674fd67861c9bca1aef2179728745f36">d_negative</a>); }
<a name="l00167"></a><a class="code" href="classCVC3_1_1Literal.html#ab2a9170779ff251399c8d197c5c5c8ce">00167</a> <span class="keywordtype">unsigned</span>& <a class="code" href="classCVC3_1_1Literal.html#ab2a9170779ff251399c8d197c5c5c8ce">countPrev</a>() { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Literal.html#a9ade1c15df2b3f10d263c4f01d6ea8d5">d_var</a>.<a class="code" href="classCVC3_1_1Variable.html#acc8e18908c0b3c74811225c58f57c50d">countPrev</a>(<a class="code" href="classCVC3_1_1Literal.html#a674fd67861c9bca1aef2179728745f36">d_negative</a>); }
<a name="l00168"></a><a class="code" href="classCVC3_1_1Literal.html#a436c5126780bd81c31bc01a868b5b857">00168</a> <span class="keywordtype">int</span>& <a class="code" href="classCVC3_1_1Literal.html#a436c5126780bd81c31bc01a868b5b857">score</a>() { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Literal.html#a9ade1c15df2b3f10d263c4f01d6ea8d5">d_var</a>.<a class="code" href="classCVC3_1_1Variable.html#aa4c74c18d5e3b6dff3a87dbb9600ea54">score</a>(<a class="code" href="classCVC3_1_1Literal.html#a674fd67861c9bca1aef2179728745f36">d_negative</a>); }
<a name="l00169"></a><a class="code" href="classCVC3_1_1Literal.html#a49129c1ccac9ad6380af512daae84b34">00169</a> <span class="keywordtype">bool</span>& <a class="code" href="classCVC3_1_1Literal.html#a49129c1ccac9ad6380af512daae84b34">added</a>() { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Literal.html#a9ade1c15df2b3f10d263c4f01d6ea8d5">d_var</a>.<a class="code" href="classCVC3_1_1Variable.html#a0e4d827e11f6308f9c9bc957f0f7d2f7">added</a>(<a class="code" href="classCVC3_1_1Literal.html#a674fd67861c9bca1aef2179728745f36">d_negative</a>); }
<a name="l00170"></a>00170 <span class="comment">// Read-only versions</span>
<a name="l00171"></a><a class="code" href="classCVC3_1_1Literal.html#a8a8aaec71bc7d9603b83dec2d4b3feeb">00171</a> <span class="keywordtype">unsigned</span> <a class="code" href="classCVC3_1_1Literal.html#a8a8aaec71bc7d9603b83dec2d4b3feeb">count</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Literal.html#a9ade1c15df2b3f10d263c4f01d6ea8d5">d_var</a>.<a class="code" href="classCVC3_1_1Variable.html#ac78bae977cd6dead5e79debc77f52efc">count</a>(<a class="code" href="classCVC3_1_1Literal.html#a674fd67861c9bca1aef2179728745f36">d_negative</a>); }
<a name="l00172"></a><a class="code" href="classCVC3_1_1Literal.html#a673002c88b2767a90c4112c946119080">00172</a> <span class="keywordtype">unsigned</span> <a class="code" href="classCVC3_1_1Literal.html#a673002c88b2767a90c4112c946119080">countPrev</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Literal.html#a9ade1c15df2b3f10d263c4f01d6ea8d5">d_var</a>.<a class="code" href="classCVC3_1_1Variable.html#acc8e18908c0b3c74811225c58f57c50d">countPrev</a>(<a class="code" href="classCVC3_1_1Literal.html#a674fd67861c9bca1aef2179728745f36">d_negative</a>); }
<a name="l00173"></a><a class="code" href="classCVC3_1_1Literal.html#af7709a0b26086c61e516460b41c032d2">00173</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1Literal.html#af7709a0b26086c61e516460b41c032d2">score</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Literal.html#a9ade1c15df2b3f10d263c4f01d6ea8d5">d_var</a>.<a class="code" href="classCVC3_1_1Variable.html#aa4c74c18d5e3b6dff3a87dbb9600ea54">score</a>(<a class="code" href="classCVC3_1_1Literal.html#a674fd67861c9bca1aef2179728745f36">d_negative</a>); }
<a name="l00174"></a><a class="code" href="classCVC3_1_1Literal.html#a4db8e1bbf73145f6453a04cec746c67d">00174</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Literal.html#a4db8e1bbf73145f6453a04cec746c67d">added</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Literal.html#a9ade1c15df2b3f10d263c4f01d6ea8d5">d_var</a>.<a class="code" href="classCVC3_1_1Variable.html#a0e4d827e11f6308f9c9bc957f0f7d2f7">added</a>(<a class="code" href="classCVC3_1_1Literal.html#a674fd67861c9bca1aef2179728745f36">d_negative</a>); }
<a name="l00175"></a>00175 <span class="comment">// Watch pointer access</span>
<a name="l00176"></a><a class="code" href="classCVC3_1_1Literal.html#a93986b2c3cd2889cbbf35fca5d216251">00176</a> std::vector<std::pair<Clause, int> >& <a class="code" href="classCVC3_1_1Literal.html#a93986b2c3cd2889cbbf35fca5d216251">wp</a>()<span class="keyword"> const</span>
<a name="l00177"></a>00177 <span class="keyword"> </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Literal.html#a9ade1c15df2b3f10d263c4f01d6ea8d5">d_var</a>.<a class="code" href="classCVC3_1_1Variable.html#a561c4d0ef9d246de12d5b22aef375315">wp</a>(<a class="code" href="classCVC3_1_1Literal.html#a674fd67861c9bca1aef2179728745f36">d_negative</a>); }
<a name="l00178"></a>00178 <span class="comment">// Printing</span>
<a name="l00179"></a>00179 <span class="keyword">friend</span> std::ostream& <a class="code" href="classCVC3_1_1Literal.html#a8b8d2fbbe7ee1896d8be5be1c4974580">operator<<</a>(std::ostream& os, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Literal.html">Literal</a>& l);
<a name="l00180"></a>00180 std::string <a class="code" href="classCVC3_1_1Literal.html#aff53e6b3e4da8c649816441046983a30">toString</a>() <span class="keyword">const</span>;
<a name="l00181"></a>00181 <span class="comment">// Equality</span>
<a name="l00182"></a><a class="code" href="classCVC3_1_1Literal.html#af8bdb08600f29ef91133ad24bf850c49">00182</a> <span class="keyword">friend</span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Literal.html#af8bdb08600f29ef91133ad24bf850c49">operator==</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Literal.html">Literal</a>& l1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Literal.html">Literal</a>& l2) {
<a name="l00183"></a>00183 <span class="keywordflow">return</span> (l1.<a class="code" href="classCVC3_1_1Literal.html#a674fd67861c9bca1aef2179728745f36">d_negative</a> == l2.<a class="code" href="classCVC3_1_1Literal.html#a674fd67861c9bca1aef2179728745f36">d_negative</a> && l1.<a class="code" href="classCVC3_1_1Literal.html#a9ade1c15df2b3f10d263c4f01d6ea8d5">d_var</a>==l1.<a class="code" href="classCVC3_1_1Literal.html#a9ade1c15df2b3f10d263c4f01d6ea8d5">d_var</a>);
<a name="l00184"></a>00184 }
<a name="l00185"></a>00185 }; <span class="comment">// end of class Literal</span>
<a name="l00186"></a>00186
<a name="l00187"></a>00187 <span class="comment">// Non-member methods: negation of Variable and Literal</span>
<a name="l00188"></a><a class="code" href="namespaceCVC3.html#a836d1b9fc2aa13791ad282f3a2d4551e">00188</a> <span class="keyword">inline</span> <a class="code" href="classCVC3_1_1Literal.html">Literal</a> <a class="code" href="namespaceCVC3.html#a836d1b9fc2aa13791ad282f3a2d4551e">operator!</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Variable.html">Variable</a>& v) {
<a name="l00189"></a>00189 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Literal.html">Literal</a>(v, <span class="keyword">false</span>);
<a name="l00190"></a>00190 }
<a name="l00191"></a>00191
<a name="l00192"></a><a class="code" href="namespaceCVC3.html#a77bbb9e579ed8077d27c91cfc0d40d26">00192</a> <span class="keyword">inline</span> <a class="code" href="classCVC3_1_1Literal.html">Literal</a> <a class="code" href="namespaceCVC3.html#a836d1b9fc2aa13791ad282f3a2d4551e">operator!</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Literal.html">Literal</a>& l) {
<a name="l00193"></a>00193 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Literal.html">Literal</a>(l.<a class="code" href="classCVC3_1_1Literal.html#af43cfe38032a00cc8e8e60b0389eeb3e">getVar</a>(), l.<a class="code" href="classCVC3_1_1Literal.html#aad653dd8534feb823b9d30f060b4e181">isNegative</a>());
<a name="l00194"></a>00194 }
<a name="l00195"></a>00195
<a name="l00196"></a>00196 std::ostream& <a class="code" href="namespaceCVC3.html#a6b7e38d3c97da1e91e12a6c9555b8163">operator<<</a>(std::ostream& os, <span class="keyword">const</span> Literal& l);
<a name="l00197"></a>00197
<a name="l00198"></a>00198 } <span class="comment">// end of namespace CVC3</span>
<a name="l00199"></a>00199
<a name="l00200"></a>00200 <span class="comment">// Clause uses class Variable, have to include it here</span>
<a name="l00201"></a>00201 <span class="preprocessor">#include "<a class="code" href="clause_8h.html">clause.h</a>"</span>
<a name="l00202"></a>00202
<a name="l00203"></a>00203 <span class="keyword">namespace </span>CVC3 {
<a name="l00204"></a>00204
<a name="l00205"></a>00205 <span class="comment">// The value holding class</span>
<a name="l00206"></a><a class="code" href="classCVC3_1_1VariableValue.html">00206</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1VariableValue.html">VariableValue</a> {
<a name="l00207"></a><a class="code" href="classCVC3_1_1VariableValue.html#a9b0a9a1a9dc58fc36b535bb33c612b49">00207</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1Variable.html">Variable</a>;
<a name="l00208"></a><a class="code" href="classCVC3_1_1VariableValue.html#a06b58135e80b3f9cee3779c4012bb13b">00208</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1VariableManager.html">VariableManager</a>;
<a name="l00209"></a>00209 <span class="keyword">private</span>:
<a name="l00210"></a><a class="code" href="classCVC3_1_1VariableValue.html#a8b9cd77982124084ed87e4fde0e6460a">00210</a> <a class="code" href="classCVC3_1_1VariableManager.html">VariableManager</a>* <a class="code" href="classCVC3_1_1VariableValue.html#a8b9cd77982124084ed87e4fde0e6460a">d_vm</a>;
<a name="l00211"></a><a class="code" href="classCVC3_1_1VariableValue.html#ac70959550ac5f1a1c22351519e5547df">00211</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1VariableValue.html#ac70959550ac5f1a1c22351519e5547df">d_refcount</a>;
<a name="l00212"></a>00212
<a name="l00213"></a><a class="code" href="classCVC3_1_1VariableValue.html#aa38abcee5fb57b183108f033a150fdda">00213</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1VariableValue.html#aa38abcee5fb57b183108f033a150fdda">d_expr</a>;
<a name="l00214"></a>00214 <span class="comment">// The inverse expression (initally Null)</span>
<a name="l00215"></a><a class="code" href="classCVC3_1_1VariableValue.html#a81cdfc55101adca8df55890a92db1109">00215</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1VariableValue.html#a81cdfc55101adca8df55890a92db1109">d_neg</a>;
<a name="l00216"></a>00216
<a name="l00217"></a>00217 <span class="comment">// Non-backtracking attributes (Chaff counters)</span>
<a name="l00218"></a>00218
<a name="l00219"></a>00219 <span class="comment">// For positive instances</span>
<a name="l00220"></a><a class="code" href="classCVC3_1_1VariableValue.html#a87a7674d38dfaac8412e058b1fe6b5b2">00220</a> <span class="keywordtype">unsigned</span> <a class="code" href="classCVC3_1_1VariableValue.html#a87a7674d38dfaac8412e058b1fe6b5b2">d_count</a>;
<a name="l00221"></a><a class="code" href="classCVC3_1_1VariableValue.html#a09de4b7db41f8014cd373b310426bc0a">00221</a> <span class="keywordtype">unsigned</span> <a class="code" href="classCVC3_1_1VariableValue.html#a09de4b7db41f8014cd373b310426bc0a">d_countPrev</a>;
<a name="l00222"></a><a class="code" href="classCVC3_1_1VariableValue.html#a2eddcb5a3c79328b3883d96992d2084b">00222</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1VariableValue.html#a2eddcb5a3c79328b3883d96992d2084b">d_score</a>;
<a name="l00223"></a>00223 <span class="comment">// For negative instances</span>
<a name="l00224"></a><a class="code" href="classCVC3_1_1VariableValue.html#a986077d2b32826ad0a4b89e9e0fbf154">00224</a> <span class="keywordtype">unsigned</span> <a class="code" href="classCVC3_1_1VariableValue.html#a986077d2b32826ad0a4b89e9e0fbf154">d_negCount</a>;
<a name="l00225"></a><a class="code" href="classCVC3_1_1VariableValue.html#a07651f2073988b6f55e9bcef189b8101">00225</a> <span class="keywordtype">unsigned</span> <a class="code" href="classCVC3_1_1VariableValue.html#a07651f2073988b6f55e9bcef189b8101">d_negCountPrev</a>;
<a name="l00226"></a><a class="code" href="classCVC3_1_1VariableValue.html#a114271041ca1acf5bb747dff3e342772">00226</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1VariableValue.html#a114271041ca1acf5bb747dff3e342772">d_negScore</a>;
<a name="l00227"></a>00227 <span class="comment">// Whether the corresponding literal is in the list of active literals</span>
<a name="l00228"></a><a class="code" href="classCVC3_1_1VariableValue.html#a6b1b02477e37cbf41a32cfb98ceb1f95">00228</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1VariableValue.html#a6b1b02477e37cbf41a32cfb98ceb1f95">d_added</a>;
<a name="l00229"></a><a class="code" href="classCVC3_1_1VariableValue.html#a930417c6ef4d34ff9e6e78e301eea90a">00229</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1VariableValue.html#a930417c6ef4d34ff9e6e78e301eea90a">d_negAdded</a>;
<a name="l00230"></a>00230 <span class="comment">// Watch pointer lists</span>
<a name="l00231"></a><a class="code" href="classCVC3_1_1VariableValue.html#aff4914c922e23b0845f5f709d76c6ad1">00231</a> std::vector<std::pair<Clause, int> > <a class="code" href="classCVC3_1_1VariableValue.html#aff4914c922e23b0845f5f709d76c6ad1">d_wp</a>;
<a name="l00232"></a><a class="code" href="classCVC3_1_1VariableValue.html#ad98bda46818737481c653e452a5236c1">00232</a> std::vector<std::pair<Clause, int> > <a class="code" href="classCVC3_1_1VariableValue.html#ad98bda46818737481c653e452a5236c1">d_negwp</a>;
<a name="l00233"></a>00233
<a name="l00234"></a>00234 <span class="comment">// Backtracking attributes</span>
<a name="l00235"></a>00235
<a name="l00236"></a>00236 <span class="comment">// Value of the variable: -1 (false), 1 (true), 0 (unresolved)</span>
<a name="l00237"></a><a class="code" href="classCVC3_1_1VariableValue.html#ada795515a6c29d6301cdb643c7b0479e">00237</a> <a class="code" href="classCVC3_1_1CDO.html">CDO<int></a>* <a class="code" href="classCVC3_1_1VariableValue.html#ada795515a6c29d6301cdb643c7b0479e">d_val</a>;
<a name="l00238"></a><a class="code" href="classCVC3_1_1VariableValue.html#a091dd8e7d8ba7c99080e169931e5007a">00238</a> <a class="code" href="classCVC3_1_1CDO.html">CDO<int></a>* <a class="code" href="classCVC3_1_1VariableValue.html#a091dd8e7d8ba7c99080e169931e5007a">d_scope</a>; <span class="comment">// Scope level where the variable is assigned</span>
<a name="l00239"></a>00239 <span class="comment">// Theorem of the form (d_expr) or (!d_expr), reflecting d_val</span>
<a name="l00240"></a><a class="code" href="classCVC3_1_1VariableValue.html#a4f427c91c94b29fac5fe8280e2cc45d9">00240</a> <a class="code" href="classCVC3_1_1CDO.html">CDO<Theorem></a>* <a class="code" href="classCVC3_1_1VariableValue.html#a4f427c91c94b29fac5fe8280e2cc45d9">d_thm</a>;
<a name="l00241"></a><a class="code" href="classCVC3_1_1VariableValue.html#a87f6665f00344a0503c10bbe265f2432">00241</a> <a class="code" href="classCVC3_1_1CDO.html">CDO<Clause></a>* <a class="code" href="classCVC3_1_1VariableValue.html#a87f6665f00344a0503c10bbe265f2432">d_ante</a>; <span class="comment">// Antecedent clause and index of the variable</span>
<a name="l00242"></a><a class="code" href="classCVC3_1_1VariableValue.html#a4724b62ffc80fa403bd9f4aa9aa95578">00242</a> <a class="code" href="classCVC3_1_1CDO.html">CDO<int></a>* <a class="code" href="classCVC3_1_1VariableValue.html#a4724b62ffc80fa403bd9f4aa9aa95578">d_anteIdx</a>;
<a name="l00243"></a><a class="code" href="classCVC3_1_1VariableValue.html#a345214752d3f0349a91c60a26cf53f29">00243</a> <a class="code" href="classCVC3_1_1CDO.html">CDO<Theorem></a>* <a class="code" href="classCVC3_1_1VariableValue.html#a345214752d3f0349a91c60a26cf53f29">d_assump</a>; <span class="comment">// Theorem generated by assump rule, if any</span>
<a name="l00244"></a>00244 <span class="comment">// Constructor is private; only class Variable can create it</span>
<a name="l00245"></a><a class="code" href="classCVC3_1_1VariableValue.html#a97912bc131f38a4d5f93bb1456118a0b">00245</a> <a class="code" href="classCVC3_1_1VariableValue.html#a97912bc131f38a4d5f93bb1456118a0b">VariableValue</a>(<a class="code" href="classCVC3_1_1VariableManager.html">VariableManager</a>* vm, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e)
<a name="l00246"></a>00246 : <a class="code" href="classCVC3_1_1VariableValue.html#a8b9cd77982124084ed87e4fde0e6460a">d_vm</a>(vm), <a class="code" href="classCVC3_1_1VariableValue.html#ac70959550ac5f1a1c22351519e5547df">d_refcount</a>(0), <a class="code" href="classCVC3_1_1VariableValue.html#aa38abcee5fb57b183108f033a150fdda">d_expr</a>(e),
<a name="l00247"></a>00247 <a class="code" href="classCVC3_1_1VariableValue.html#a87a7674d38dfaac8412e058b1fe6b5b2">d_count</a>(0), <a class="code" href="classCVC3_1_1VariableValue.html#a09de4b7db41f8014cd373b310426bc0a">d_countPrev</a>(0), <a class="code" href="classCVC3_1_1VariableValue.html#a2eddcb5a3c79328b3883d96992d2084b">d_score</a>(0),
<a name="l00248"></a>00248 <a class="code" href="classCVC3_1_1VariableValue.html#a986077d2b32826ad0a4b89e9e0fbf154">d_negCount</a>(0), <a class="code" href="classCVC3_1_1VariableValue.html#a07651f2073988b6f55e9bcef189b8101">d_negCountPrev</a>(0), <a class="code" href="classCVC3_1_1VariableValue.html#a114271041ca1acf5bb747dff3e342772">d_negScore</a>(0),
<a name="l00249"></a>00249 <a class="code" href="classCVC3_1_1VariableValue.html#a6b1b02477e37cbf41a32cfb98ceb1f95">d_added</a>(false), <a class="code" href="classCVC3_1_1VariableValue.html#a930417c6ef4d34ff9e6e78e301eea90a">d_negAdded</a>(false),
<a name="l00250"></a>00250 <a class="code" href="classCVC3_1_1VariableValue.html#ada795515a6c29d6301cdb643c7b0479e">d_val</a>(NULL), <a class="code" href="classCVC3_1_1VariableValue.html#a091dd8e7d8ba7c99080e169931e5007a">d_scope</a>(NULL), <a class="code" href="classCVC3_1_1VariableValue.html#a4f427c91c94b29fac5fe8280e2cc45d9">d_thm</a>(NULL),
<a name="l00251"></a>00251 <a class="code" href="classCVC3_1_1VariableValue.html#a87f6665f00344a0503c10bbe265f2432">d_ante</a>(NULL), <a class="code" href="classCVC3_1_1VariableValue.html#a4724b62ffc80fa403bd9f4aa9aa95578">d_anteIdx</a>(NULL), <a class="code" href="classCVC3_1_1VariableValue.html#a345214752d3f0349a91c60a26cf53f29">d_assump</a>(NULL) { }
<a name="l00252"></a>00252 <span class="keyword">public</span>:
<a name="l00253"></a>00253 <a class="code" href="classCVC3_1_1VariableValue.html#ac74e3ee4ad23bfeb6254a6e4769d104c">~VariableValue</a>();
<a name="l00254"></a>00254 <span class="comment">// Accessor methods</span>
<a name="l00255"></a><a class="code" href="classCVC3_1_1VariableValue.html#a5e3bf7de7f3bd16d1b274e16d4292893">00255</a> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="classCVC3_1_1VariableValue.html#a5e3bf7de7f3bd16d1b274e16d4292893">getExpr</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1VariableValue.html#aa38abcee5fb57b183108f033a150fdda">d_expr</a>; }
<a name="l00256"></a>00256
<a name="l00257"></a><a class="code" href="classCVC3_1_1VariableValue.html#a798fc6fa670819203aa7e2ecf3a609de">00257</a> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="classCVC3_1_1VariableValue.html#a798fc6fa670819203aa7e2ecf3a609de">getNegExpr</a>()<span class="keyword"> const </span>{
<a name="l00258"></a>00258 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1VariableValue.html#a81cdfc55101adca8df55890a92db1109">d_neg</a>.<a class="code" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a>()) {
<a name="l00259"></a>00259 <span class="keyword">const_cast<</span><a class="code" href="classCVC3_1_1VariableValue.html">VariableValue</a>*<span class="keyword">></span>(<span class="keyword">this</span>)-><a class="code" href="classCVC3_1_1VariableValue.html#a81cdfc55101adca8df55890a92db1109">d_neg</a>
<a name="l00260"></a>00260 = <a class="code" href="classCVC3_1_1VariableValue.html#aa38abcee5fb57b183108f033a150fdda">d_expr</a>.<a class="code" href="group__ExprPkg.html#gab1ce461dc931af73bf04e88c8d37dcbc">negate</a>();
<a name="l00261"></a>00261 }
<a name="l00262"></a>00262 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1VariableValue.html#a81cdfc55101adca8df55890a92db1109">d_neg</a>;
<a name="l00263"></a>00263 }
<a name="l00264"></a>00264
<a name="l00265"></a><a class="code" href="classCVC3_1_1VariableValue.html#a6f83bd36830c43e35d21984cd5b3a3ff">00265</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1VariableValue.html#a6f83bd36830c43e35d21984cd5b3a3ff">getValue</a>()<span class="keyword"> const </span>{
<a name="l00266"></a>00266 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1VariableValue.html#ada795515a6c29d6301cdb643c7b0479e">d_val</a>==NULL) <span class="keywordflow">return</span> 0;
<a name="l00267"></a>00267 <span class="keywordflow">else</span> <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1VariableValue.html#ada795515a6c29d6301cdb643c7b0479e">d_val</a>-><a class="code" href="classCVC3_1_1CDO.html#a818fcacc7b30b0f05347335ab125626c">get</a>();
<a name="l00268"></a>00268 }
<a name="l00269"></a>00269
<a name="l00270"></a><a class="code" href="classCVC3_1_1VariableValue.html#aabc451feb269d84dc19bdc1148bc8af8">00270</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1VariableValue.html#aabc451feb269d84dc19bdc1148bc8af8">getScope</a>()<span class="keyword"> const </span>{
<a name="l00271"></a>00271 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1VariableValue.html#a091dd8e7d8ba7c99080e169931e5007a">d_scope</a>==NULL) <span class="keywordflow">return</span> 0;
<a name="l00272"></a>00272 <span class="keywordflow">else</span> <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1VariableValue.html#a091dd8e7d8ba7c99080e169931e5007a">d_scope</a>-><a class="code" href="classCVC3_1_1CDO.html#a818fcacc7b30b0f05347335ab125626c">get</a>();
<a name="l00273"></a>00273 }
<a name="l00274"></a>00274
<a name="l00275"></a><a class="code" href="classCVC3_1_1VariableValue.html#a2a186bfae906f1fa27d64457f2428125">00275</a> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& <a class="code" href="classCVC3_1_1VariableValue.html#a2a186bfae906f1fa27d64457f2428125">getTheorem</a>()<span class="keyword"> const </span>{
<a name="l00276"></a>00276 <span class="keyword">static</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> null;
<a name="l00277"></a>00277 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1VariableValue.html#a4f427c91c94b29fac5fe8280e2cc45d9">d_thm</a>==NULL) <span class="keywordflow">return</span> null;
<a name="l00278"></a>00278 <span class="keywordflow">else</span> <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1VariableValue.html#a4f427c91c94b29fac5fe8280e2cc45d9">d_thm</a>-><a class="code" href="classCVC3_1_1CDO.html#a818fcacc7b30b0f05347335ab125626c">get</a>();
<a name="l00279"></a>00279 }
<a name="l00280"></a>00280
<a name="l00281"></a><a class="code" href="classCVC3_1_1VariableValue.html#aac80324d8bc82742954381946066c103">00281</a> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Clause.html" title="A class representing a CNF clause (a smart pointer)">Clause</a>& <a class="code" href="classCVC3_1_1VariableValue.html#aac80324d8bc82742954381946066c103">getAntecedent</a>()<span class="keyword"> const </span>{
<a name="l00282"></a>00282 <span class="keyword">static</span> <a class="code" href="classCVC3_1_1Clause.html" title="A class representing a CNF clause (a smart pointer)">Clause</a> null;
<a name="l00283"></a>00283 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1VariableValue.html#a87f6665f00344a0503c10bbe265f2432">d_ante</a>==NULL) <span class="keywordflow">return</span> null;
<a name="l00284"></a>00284 <span class="keywordflow">else</span> <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1VariableValue.html#a87f6665f00344a0503c10bbe265f2432">d_ante</a>-><a class="code" href="classCVC3_1_1CDO.html#a818fcacc7b30b0f05347335ab125626c">get</a>();
<a name="l00285"></a>00285 }
<a name="l00286"></a>00286
<a name="l00287"></a><a class="code" href="classCVC3_1_1VariableValue.html#a5ead45485317b8beb32d1489d71b7274">00287</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1VariableValue.html#a5ead45485317b8beb32d1489d71b7274">getAntecedentIdx</a>()<span class="keyword"> const </span>{
<a name="l00288"></a>00288 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1VariableValue.html#a4724b62ffc80fa403bd9f4aa9aa95578">d_anteIdx</a>==NULL) <span class="keywordflow">return</span> 0;
<a name="l00289"></a>00289 <span class="keywordflow">else</span> <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1VariableValue.html#a4724b62ffc80fa403bd9f4aa9aa95578">d_anteIdx</a>-><a class="code" href="classCVC3_1_1CDO.html#a818fcacc7b30b0f05347335ab125626c">get</a>();
<a name="l00290"></a>00290 }
<a name="l00291"></a>00291
<a name="l00292"></a><a class="code" href="classCVC3_1_1VariableValue.html#a600aed64a238804fc7e6e5717a07a6f5">00292</a> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& <a class="code" href="classCVC3_1_1VariableValue.html#a600aed64a238804fc7e6e5717a07a6f5">getAssumpThm</a>()<span class="keyword"> const </span>{
<a name="l00293"></a>00293 <span class="keyword">static</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> null;
<a name="l00294"></a>00294 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1VariableValue.html#a345214752d3f0349a91c60a26cf53f29">d_assump</a>==NULL) <span class="keywordflow">return</span> null;
<a name="l00295"></a>00295 <span class="keywordflow">else</span> <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1VariableValue.html#a345214752d3f0349a91c60a26cf53f29">d_assump</a>-><a class="code" href="classCVC3_1_1CDO.html#a818fcacc7b30b0f05347335ab125626c">get</a>();
<a name="l00296"></a>00296 }
<a name="l00297"></a>00297
<a name="l00298"></a>00298 <span class="comment">// Setting the attributes: it can be either derived from the</span>
<a name="l00299"></a>00299 <span class="comment">// antecedent clause, or by a theorem</span>
<a name="l00300"></a>00300 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1VariableValue.html#aefcf6649a5dcfa1382c3a296659b57a5">setValue</a>(<span class="keywordtype">int</span> val, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Clause.html" title="A class representing a CNF clause (a smart pointer)">Clause</a>& c, <span class="keywordtype">int</span> idx);
<a name="l00301"></a>00301 <span class="comment">// The theorem's expr must be the same as the variable's expr or</span>
<a name="l00302"></a>00302 <span class="comment">// its negation</span>
<a name="l00303"></a>00303 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1VariableValue.html#aefcf6649a5dcfa1382c3a296659b57a5">setValue</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm, <span class="keywordtype">int</span> scope);
<a name="l00304"></a>00304
<a name="l00305"></a>00305 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1VariableValue.html#abfd2af792b3d79935abf5fa2db7e8218">setAssumpThm</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& a, <span class="keywordtype">int</span> scope);
<a name="l00306"></a>00306
<a name="l00307"></a>00307 <span class="comment">// Chaff counters: read and modified by reference</span>
<a name="l00308"></a><a class="code" href="classCVC3_1_1VariableValue.html#acb5347247874196d09dcfb829dac80a4">00308</a> <span class="keywordtype">unsigned</span>& <a class="code" href="classCVC3_1_1VariableValue.html#acb5347247874196d09dcfb829dac80a4">count</a>(<span class="keywordtype">bool</span> neg) {
<a name="l00309"></a>00309 <span class="keywordflow">if</span>(neg) <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1VariableValue.html#a986077d2b32826ad0a4b89e9e0fbf154">d_negCount</a>;
<a name="l00310"></a>00310 <span class="keywordflow">else</span> <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1VariableValue.html#a87a7674d38dfaac8412e058b1fe6b5b2">d_count</a>;
<a name="l00311"></a>00311 }
<a name="l00312"></a><a class="code" href="classCVC3_1_1VariableValue.html#a64350354329075928e80eb4f133521ad">00312</a> <span class="keywordtype">unsigned</span>& <a class="code" href="classCVC3_1_1VariableValue.html#a64350354329075928e80eb4f133521ad">countPrev</a>(<span class="keywordtype">bool</span> neg) {
<a name="l00313"></a>00313 <span class="keywordflow">if</span>(neg) <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1VariableValue.html#a07651f2073988b6f55e9bcef189b8101">d_negCountPrev</a>;
<a name="l00314"></a>00314 <span class="keywordflow">else</span> <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1VariableValue.html#a09de4b7db41f8014cd373b310426bc0a">d_countPrev</a>;
<a name="l00315"></a>00315 }
<a name="l00316"></a><a class="code" href="classCVC3_1_1VariableValue.html#ad585655ed33dcc2c541d300b09370083">00316</a> <span class="keywordtype">int</span>& <a class="code" href="classCVC3_1_1VariableValue.html#ad585655ed33dcc2c541d300b09370083">score</a>(<span class="keywordtype">bool</span> neg) {
<a name="l00317"></a>00317 <span class="keywordflow">if</span>(neg) <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1VariableValue.html#a114271041ca1acf5bb747dff3e342772">d_negScore</a>;
<a name="l00318"></a>00318 <span class="keywordflow">else</span> <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1VariableValue.html#a2eddcb5a3c79328b3883d96992d2084b">d_score</a>;
<a name="l00319"></a>00319 }
<a name="l00320"></a><a class="code" href="classCVC3_1_1VariableValue.html#ab9c05cca095742f0fd66d7084084e237">00320</a> <span class="keywordtype">bool</span>& <a class="code" href="classCVC3_1_1VariableValue.html#ab9c05cca095742f0fd66d7084084e237">added</a>(<span class="keywordtype">bool</span> neg) {
<a name="l00321"></a>00321 <span class="keywordflow">if</span>(neg) <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1VariableValue.html#a930417c6ef4d34ff9e6e78e301eea90a">d_negAdded</a>;
<a name="l00322"></a>00322 <span class="keywordflow">else</span> <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1VariableValue.html#a6b1b02477e37cbf41a32cfb98ceb1f95">d_added</a>;
<a name="l00323"></a>00323 }
<a name="l00324"></a>00324
<a name="l00325"></a>00325 <span class="comment">// Memory management</span>
<a name="l00326"></a><a class="code" href="classCVC3_1_1VariableValue.html#a4d31224a03391dd9c418da7590e3cc92">00326</a> <span class="keywordtype">void</span>* <a class="code" href="classCVC3_1_1VariableValue.html#a4d31224a03391dd9c418da7590e3cc92">operator new</a>(<span class="keywordtype">size_t</span> size, <a class="code" href="classCVC3_1_1MemoryManager.html">MemoryManager</a>* mm) {
<a name="l00327"></a>00327 <span class="keywordflow">return</span> mm-><a class="code" href="classCVC3_1_1MemoryManager.html#a3db7efbc4b956bd423a73e1157d70ce0">newData</a>(size);
<a name="l00328"></a>00328 }
<a name="l00329"></a><a class="code" href="classCVC3_1_1VariableValue.html#a00f105f23de53316c9f6c0d799a1caed">00329</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1VariableValue.html#a00f105f23de53316c9f6c0d799a1caed">operator delete</a>(<span class="keywordtype">void</span>* pMem, <a class="code" href="classCVC3_1_1MemoryManager.html">MemoryManager</a>* mm) {
<a name="l00330"></a>00330 mm-><a class="code" href="classCVC3_1_1MemoryManager.html#ad29fac88d3a07566d9a8f9dc8d8e059c">deleteData</a>(pMem);
<a name="l00331"></a>00331 }
<a name="l00332"></a><a class="code" href="classCVC3_1_1VariableValue.html#afffed1d47c732ae86261cff5db8387de">00332</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1VariableValue.html#afffed1d47c732ae86261cff5db8387de">operator delete</a>(<span class="keywordtype">void</span>*) { }
<a name="l00333"></a>00333
<a name="l00334"></a>00334 <span class="comment">// friend methods</span>
<a name="l00335"></a>00335 <span class="keyword">friend</span> std::ostream& <a class="code" href="classCVC3_1_1VariableValue.html#a98e3d083ca34ed383ea51259c73fc81b">operator<<</a>(std::ostream& os, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1VariableValue.html">VariableValue</a>& v);
<a name="l00336"></a><a class="code" href="classCVC3_1_1VariableValue.html#ab6a288d87c21f6e977bd9daa2a34946f">00336</a> <span class="keyword">friend</span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1VariableValue.html#ab6a288d87c21f6e977bd9daa2a34946f">operator==</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1VariableValue.html">VariableValue</a>& v1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1VariableValue.html">VariableValue</a>& v2) {
<a name="l00337"></a>00337 <span class="keywordflow">return</span> v1.<a class="code" href="classCVC3_1_1VariableValue.html#aa38abcee5fb57b183108f033a150fdda">d_expr</a> == v2.<a class="code" href="classCVC3_1_1VariableValue.html#aa38abcee5fb57b183108f033a150fdda">d_expr</a>;
<a name="l00338"></a>00338 }
<a name="l00339"></a>00339 }; <span class="comment">// end of class VariableValue</span>
<a name="l00340"></a>00340
<a name="l00341"></a>00341 <span class="comment">// Accessing Chaff counters (read and modified by reference)</span>
<a name="l00342"></a><a class="code" href="classCVC3_1_1Variable.html#ac78bae977cd6dead5e79debc77f52efc">00342</a> <span class="keyword">inline</span> <span class="keywordtype">unsigned</span>& <a class="code" href="classCVC3_1_1Variable.html#ac78bae977cd6dead5e79debc77f52efc">Variable::count</a>(<span class="keywordtype">bool</span> neg) { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>-><a class="code" href="classCVC3_1_1VariableValue.html#acb5347247874196d09dcfb829dac80a4">count</a>(neg); }
<a name="l00343"></a><a class="code" href="classCVC3_1_1Variable.html#acc8e18908c0b3c74811225c58f57c50d">00343</a> <span class="keyword">inline</span> <span class="keywordtype">unsigned</span>& <a class="code" href="classCVC3_1_1Variable.html#acc8e18908c0b3c74811225c58f57c50d">Variable::countPrev</a>(<span class="keywordtype">bool</span> neg)
<a name="l00344"></a>00344 { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>-><a class="code" href="classCVC3_1_1VariableValue.html#a64350354329075928e80eb4f133521ad">countPrev</a>(neg); }
<a name="l00345"></a><a class="code" href="classCVC3_1_1Variable.html#aa4c74c18d5e3b6dff3a87dbb9600ea54">00345</a> <span class="keyword">inline</span> <span class="keywordtype">int</span>& <a class="code" href="classCVC3_1_1Variable.html#aa4c74c18d5e3b6dff3a87dbb9600ea54">Variable::score</a>(<span class="keywordtype">bool</span> neg) { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>-><a class="code" href="classCVC3_1_1VariableValue.html#ad585655ed33dcc2c541d300b09370083">score</a>(neg); }
<a name="l00346"></a><a class="code" href="classCVC3_1_1Variable.html#a0e4d827e11f6308f9c9bc957f0f7d2f7">00346</a> <span class="keyword">inline</span> <span class="keywordtype">bool</span>& <a class="code" href="classCVC3_1_1Variable.html#a0e4d827e11f6308f9c9bc957f0f7d2f7">Variable::added</a>(<span class="keywordtype">bool</span> neg) { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>-><a class="code" href="classCVC3_1_1VariableValue.html#ab9c05cca095742f0fd66d7084084e237">added</a>(neg); }
<a name="l00347"></a>00347
<a name="l00348"></a><a class="code" href="classCVC3_1_1Variable.html#ac14d877633308fefc91fea8a07005fee">00348</a> <span class="keyword">inline</span> <span class="keywordtype">unsigned</span> <a class="code" href="classCVC3_1_1Variable.html#ac78bae977cd6dead5e79debc77f52efc">Variable::count</a>(<span class="keywordtype">bool</span> neg)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>-><a class="code" href="classCVC3_1_1VariableValue.html#acb5347247874196d09dcfb829dac80a4">count</a>(neg); }
<a name="l00349"></a><a class="code" href="classCVC3_1_1Variable.html#a987bd4125ec63afc7577b3dbf9cb7b76">00349</a> <span class="keyword">inline</span> <span class="keywordtype">unsigned</span> <a class="code" href="classCVC3_1_1Variable.html#acc8e18908c0b3c74811225c58f57c50d">Variable::countPrev</a>(<span class="keywordtype">bool</span> neg)<span class="keyword"> const</span>
<a name="l00350"></a>00350 <span class="keyword"> </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>-><a class="code" href="classCVC3_1_1VariableValue.html#a64350354329075928e80eb4f133521ad">countPrev</a>(neg); }
<a name="l00351"></a><a class="code" href="classCVC3_1_1Variable.html#a81e07d7b4272797fb31ed99ab88359ca">00351</a> <span class="keyword">inline</span> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1Variable.html#aa4c74c18d5e3b6dff3a87dbb9600ea54">Variable::score</a>(<span class="keywordtype">bool</span> neg)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>-><a class="code" href="classCVC3_1_1VariableValue.html#ad585655ed33dcc2c541d300b09370083">score</a>(neg); }
<a name="l00352"></a><a class="code" href="classCVC3_1_1Variable.html#ab7d99f6dfbadfbbf71ee23a4fd49a5e0">00352</a> <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Variable.html#a0e4d827e11f6308f9c9bc957f0f7d2f7">Variable::added</a>(<span class="keywordtype">bool</span> neg)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>-><a class="code" href="classCVC3_1_1VariableValue.html#ab9c05cca095742f0fd66d7084084e237">added</a>(neg); }
<a name="l00353"></a>00353
<a name="l00354"></a><a class="code" href="classCVC3_1_1Variable.html#a561c4d0ef9d246de12d5b22aef375315">00354</a> <span class="keyword">inline</span> std::vector<std::pair<Clause, int> >& <a class="code" href="classCVC3_1_1Variable.html#a561c4d0ef9d246de12d5b22aef375315">Variable::wp</a>(<span class="keywordtype">bool</span> neg)<span class="keyword"> const </span>{
<a name="l00355"></a>00355 <span class="keywordflow">if</span>(neg) <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>-><a class="code" href="classCVC3_1_1VariableValue.html#ad98bda46818737481c653e452a5236c1">d_negwp</a>;
<a name="l00356"></a>00356 <span class="keywordflow">else</span> <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>-><a class="code" href="classCVC3_1_1VariableValue.html#aff4914c922e23b0845f5f709d76c6ad1">d_wp</a>;
<a name="l00357"></a>00357 }
<a name="l00358"></a>00358
<a name="l00359"></a>00359
<a name="l00360"></a>00360 <span class="keyword">class </span><a class="code" href="classCVC3_1_1VariableManagerNotifyObj.html" title="Notifies VariableManager before and after each pop()">VariableManagerNotifyObj</a>;
<a name="l00361"></a>00361
<a name="l00362"></a>00362 <span class="comment">// The manager class</span>
<a name="l00363"></a><a class="code" href="classCVC3_1_1VariableManager.html">00363</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1VariableManager.html">VariableManager</a> {
<a name="l00364"></a><a class="code" href="classCVC3_1_1VariableManager.html#a9b0a9a1a9dc58fc36b535bb33c612b49">00364</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1Variable.html">Variable</a>;
<a name="l00365"></a><a class="code" href="classCVC3_1_1VariableManager.html#a03a95394237b65c38d2dc8e7af617131">00365</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1VariableValue.html">VariableValue</a>;
<a name="l00366"></a>00366 <span class="keyword">private</span>:
<a name="l00367"></a><a class="code" href="classCVC3_1_1VariableManager.html#aa9a63ca44ee29e3e11b843abf64680fd">00367</a> <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_1VariableManager.html#aa9a63ca44ee29e3e11b843abf64680fd">d_cm</a>;
<a name="l00368"></a><a class="code" href="classCVC3_1_1VariableManager.html#a19ff37ae7bc9f7e807cd66aa8e5f18f4">00368</a> <a class="code" href="classCVC3_1_1MemoryManager.html">MemoryManager</a>* <a class="code" href="classCVC3_1_1VariableManager.html#a19ff37ae7bc9f7e807cd66aa8e5f18f4">d_mm</a>;
<a name="l00369"></a><a class="code" href="classCVC3_1_1VariableManager.html#aade2fac567b8a5e09a275e409b132e21">00369</a> <a class="code" href="classCVC3_1_1SearchEngineRules.html" title="API to the proof rules for the Search Engines.">SearchEngineRules</a>* <a class="code" href="classCVC3_1_1VariableManager.html#aade2fac567b8a5e09a275e409b132e21">d_rules</a>;
<a name="l00370"></a><a class="code" href="classCVC3_1_1VariableManager.html#a17f4827ea92ce6e1ad0a1d5fa5726146">00370</a> <a class="code" href="classCVC3_1_1VariableManagerNotifyObj.html" title="Notifies VariableManager before and after each pop()">VariableManagerNotifyObj</a>* <a class="code" href="classCVC3_1_1VariableManager.html#a17f4827ea92ce6e1ad0a1d5fa5726146">d_notifyObj</a>;<span class="comment"></span>
<a name="l00371"></a>00371 <span class="comment"> //! Disable the garbage collection</span>
<a name="l00372"></a>00372 <span class="comment"></span><span class="comment"> /*! Normally, it's set in the destructor, so that we can delete</span>
<a name="l00373"></a>00373 <span class="comment"> * all remaining variables without GC getting in the way</span>
<a name="l00374"></a>00374 <span class="comment"> */</span>
<a name="l00375"></a><a class="code" href="classCVC3_1_1VariableManager.html#a87d086a76555966bb4e6f62b9e32bbac">00375</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1VariableManager.html#a87d086a76555966bb4e6f62b9e32bbac" title="Disable the garbage collection.">d_disableGC</a>;<span class="comment"></span>
<a name="l00376"></a>00376 <span class="comment"> //! Postpone garbage collection</span>
<a name="l00377"></a><a class="code" href="classCVC3_1_1VariableManager.html#adcdbfcae4aa2f069cfcb15d9b308b727">00377</a> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1VariableManager.html#adcdbfcae4aa2f069cfcb15d9b308b727" title="Postpone garbage collection.">d_postponeGC</a>;<span class="comment"></span>
<a name="l00378"></a>00378 <span class="comment"> //! Vector of variables to be deleted (postponed during pop())</span>
<a name="l00379"></a><a class="code" href="classCVC3_1_1VariableManager.html#af71a9d9933957edede81db48be5da5a3">00379</a> <span class="comment"></span> std::vector<VariableValue*> <a class="code" href="classCVC3_1_1VariableManager.html#af71a9d9933957edede81db48be5da5a3" title="Vector of variables to be deleted (postponed during pop())">d_deleted</a>;
<a name="l00380"></a>00380
<a name="l00381"></a>00381 <span class="comment">// Hash only by the Expr</span>
<a name="l00382"></a><a class="code" href="classCVC3_1_1VariableManager_1_1HashLV.html">00382</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1VariableManager_1_1HashLV.html">HashLV</a> {
<a name="l00383"></a>00383 <span class="keyword">public</span>:
<a name="l00384"></a><a class="code" href="classCVC3_1_1VariableManager_1_1HashLV.html#a84e1f54c7cd36f19abd50c6a26362e73">00384</a> <span class="keywordtype">size_t</span> <a class="code" href="classCVC3_1_1VariableManager_1_1HashLV.html#a84e1f54c7cd36f19abd50c6a26362e73">operator()</a>(<a class="code" href="classCVC3_1_1VariableValue.html">VariableValue</a>* v)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> v-><a class="code" href="classCVC3_1_1VariableValue.html#a5e3bf7de7f3bd16d1b274e16d4292893">getExpr</a>().<a class="code" href="group__ExprPkg.html#gadf3d59da15e4f78daf0c41ef7779a749">hash</a>(); }
<a name="l00385"></a>00385 };
<a name="l00386"></a><a class="code" href="classCVC3_1_1VariableManager_1_1EqLV.html">00386</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1VariableManager_1_1EqLV.html">EqLV</a> {
<a name="l00387"></a>00387 <span class="keyword">public</span>:
<a name="l00388"></a><a class="code" href="classCVC3_1_1VariableManager_1_1EqLV.html#a0f76612cb02a63da4ffe792a65a00723">00388</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1VariableManager_1_1EqLV.html#a0f76612cb02a63da4ffe792a65a00723">operator()</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1VariableValue.html">VariableValue</a>* lv1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1VariableValue.html">VariableValue</a>* lv2)<span class="keyword"> const</span>
<a name="l00389"></a>00389 <span class="keyword"> </span>{ <span class="keywordflow">return</span> lv1-><a class="code" href="classCVC3_1_1VariableValue.html#a5e3bf7de7f3bd16d1b274e16d4292893">getExpr</a>() == lv2-><a class="code" href="classCVC3_1_1VariableValue.html#a5e3bf7de7f3bd16d1b274e16d4292893">getExpr</a>(); }
<a name="l00390"></a>00390 };
<a name="l00391"></a>00391
<a name="l00392"></a>00392 <span class="comment">// Hash set for existing variables</span>
<a name="l00393"></a><a class="code" href="classCVC3_1_1VariableManager.html#acc3ee56d53bab748a41b71b9986eaab9">00393</a> <span class="keyword">typedef</span> <a class="code" href="classHash_1_1hash__set.html">std::hash_set<VariableValue*, HashLV, EqLV></a> <a class="code" href="classCVC3_1_1VariableManager.html#acc3ee56d53bab748a41b71b9986eaab9">VariableValueSet</a>;
<a name="l00394"></a><a class="code" href="classCVC3_1_1VariableManager.html#aeebf5ed3c88627c0b43f61c4f1ba42e5">00394</a> <a class="code" href="classHash_1_1hash__set.html">VariableValueSet</a> <a class="code" href="classCVC3_1_1VariableManager.html#aeebf5ed3c88627c0b43f61c4f1ba42e5">d_varSet</a>;
<a name="l00395"></a>00395
<a name="l00396"></a>00396 <span class="comment">// Creating unique VariableValue</span>
<a name="l00397"></a>00397 <a class="code" href="classCVC3_1_1VariableValue.html">VariableValue</a>* <a class="code" href="classCVC3_1_1VariableManager.html#a2052323b56685b21f16d1062917dfe38">newVariableValue</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);
<a name="l00398"></a>00398
<a name="l00399"></a>00399 <span class="keyword">public</span>:
<a name="l00400"></a>00400 <span class="comment">// Constructor. mmFlag indicates which memory manager to use.</span>
<a name="l00401"></a>00401 <a class="code" href="classCVC3_1_1VariableManager.html#a7faa284a5e5a72a87426de1f5cbf1bc9">VariableManager</a>(<a class="code" href="classCVC3_1_1ContextManager.html" title="Manager for multiple contexts. Also holds current context.">ContextManager</a>* cm, <a class="code" href="classCVC3_1_1SearchEngineRules.html" title="API to the proof rules for the Search Engines.">SearchEngineRules</a>* rules,
<a name="l00402"></a>00402 <span class="keyword">const</span> std::string& mmFlag);
<a name="l00403"></a>00403 <span class="comment">// Destructor</span>
<a name="l00404"></a>00404 <a class="code" href="classCVC3_1_1VariableManager.html#a321959b4af5952884d5215ca1eeb3bcc">~VariableManager</a>();
<a name="l00405"></a>00405 <span class="comment"></span>
<a name="l00406"></a>00406 <span class="comment"> //! Garbage collect VariableValue pointer</span>
<a name="l00407"></a>00407 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1VariableManager.html#a5f35575560aac2140e817aa49190894d" title="Garbage collect VariableValue pointer.">gc</a>(<a class="code" href="classCVC3_1_1VariableValue.html">VariableValue</a>* v);<span class="comment"></span>
<a name="l00408"></a>00408 <span class="comment"> //! Postpone garbage collection</span>
<a name="l00409"></a><a class="code" href="classCVC3_1_1VariableManager.html#a04703a93a52748b0a2e4b31cc4f42ea2">00409</a> <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1VariableManager.html#a04703a93a52748b0a2e4b31cc4f42ea2" title="Postpone garbage collection.">postponeGC</a>() { <a class="code" href="classCVC3_1_1VariableManager.html#adcdbfcae4aa2f069cfcb15d9b308b727" title="Postpone garbage collection.">d_postponeGC</a> = <span class="keyword">true</span>; }<span class="comment"></span>
<a name="l00410"></a>00410 <span class="comment"> //! Resume garbage collection</span>
<a name="l00411"></a>00411 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1VariableManager.html#ad7d360514fcfd910668eabd097dbe81c" title="Resume garbage collection.">resumeGC</a>();
<a name="l00412"></a>00412 <span class="comment">// Accessors</span>
<a name="l00413"></a><a class="code" href="classCVC3_1_1VariableManager.html#a02e36e773779bc9e17472e265b70627c">00413</a> <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_1VariableManager.html#a02e36e773779bc9e17472e265b70627c">getCM</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1VariableManager.html#aa9a63ca44ee29e3e11b843abf64680fd">d_cm</a>; }
<a name="l00414"></a><a class="code" href="classCVC3_1_1VariableManager.html#a0d68fbe0c1eb8b19d8d91984c290ef28">00414</a> <a class="code" href="classCVC3_1_1SearchEngineRules.html" title="API to the proof rules for the Search Engines.">SearchEngineRules</a>* <a class="code" href="classCVC3_1_1VariableManager.html#a0d68fbe0c1eb8b19d8d91984c290ef28">getRules</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1VariableManager.html#aade2fac567b8a5e09a275e409b132e21">d_rules</a>; }
<a name="l00415"></a>00415
<a name="l00416"></a>00416 }; <span class="comment">// end of class VariableManager</span>
<a name="l00417"></a>00417
<a name="l00418"></a>00418 <span class="comment">/*****************************************************************************/</span><span class="comment"></span>
<a name="l00419"></a>00419 <span class="comment">/*!</span>
<a name="l00420"></a>00420 <span class="comment"> *\class VariableManagerNotifyObj</span>
<a name="l00421"></a>00421 <span class="comment"> *\brief Notifies VariableManager before and after each pop()</span>
<a name="l00422"></a>00422 <span class="comment"> *</span>
<a name="l00423"></a>00423 <span class="comment"> * Author: Sergey Berezin</span>
<a name="l00424"></a>00424 <span class="comment"> *</span>
<a name="l00425"></a>00425 <span class="comment"> * Created: Tue Mar 1 13:52:28 2005</span>
<a name="l00426"></a>00426 <span class="comment"> *</span>
<a name="l00427"></a>00427 <span class="comment"> * Disables the deletion of VariableValue objects during context</span>
<a name="l00428"></a>00428 <span class="comment"> * restoration (backtracking). This solves the problem of circular</span>
<a name="l00429"></a>00429 <span class="comment"> * dependencies (e.g. a Variable pointing to its antecedent Clause).</span>
<a name="l00430"></a>00430 <span class="comment"> */</span>
<a name="l00431"></a>00431 <span class="comment">/*****************************************************************************/</span>
<a name="l00432"></a><a class="code" href="classCVC3_1_1VariableManagerNotifyObj.html">00432</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1VariableManagerNotifyObj.html" title="Notifies VariableManager before and after each pop()">VariableManagerNotifyObj</a>: <span class="keyword">public</span> <a class="code" href="classCVC3_1_1ContextNotifyObj.html">ContextNotifyObj</a> {
<a name="l00433"></a><a class="code" href="classCVC3_1_1VariableManagerNotifyObj.html#a24de96df43ce7e50a3c142fb04790c1c">00433</a> <a class="code" href="classCVC3_1_1VariableManager.html">VariableManager</a>* <a class="code" href="classCVC3_1_1VariableManagerNotifyObj.html#a24de96df43ce7e50a3c142fb04790c1c">d_vm</a>;
<a name="l00434"></a>00434 <span class="keyword">public</span>:<span class="comment"></span>
<a name="l00435"></a>00435 <span class="comment"> //! Constructor</span>
<a name="l00436"></a><a class="code" href="classCVC3_1_1VariableManagerNotifyObj.html#a21ace78bece400d43aa42506d9256d68">00436</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1VariableManagerNotifyObj.html#a21ace78bece400d43aa42506d9256d68" title="Constructor.">VariableManagerNotifyObj</a>(<a class="code" href="classCVC3_1_1VariableManager.html">VariableManager</a>* vm, <a class="code" href="classCVC3_1_1Context.html">Context</a>* cxt)
<a name="l00437"></a>00437 : <a class="code" href="classCVC3_1_1ContextNotifyObj.html">ContextNotifyObj</a>(cxt), <a class="code" href="classCVC3_1_1VariableManagerNotifyObj.html#a24de96df43ce7e50a3c142fb04790c1c">d_vm</a>(vm) { }
<a name="l00438"></a>00438
<a name="l00439"></a><a class="code" href="classCVC3_1_1VariableManagerNotifyObj.html#a67ee9f591420b325b6f3bf88fa78d9b1">00439</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1VariableManagerNotifyObj.html#a67ee9f591420b325b6f3bf88fa78d9b1">notifyPre</a>(<span class="keywordtype">void</span>) { <a class="code" href="classCVC3_1_1VariableManagerNotifyObj.html#a24de96df43ce7e50a3c142fb04790c1c">d_vm</a>-><a class="code" href="classCVC3_1_1VariableManager.html#a04703a93a52748b0a2e4b31cc4f42ea2" title="Postpone garbage collection.">postponeGC</a>(); }
<a name="l00440"></a><a class="code" href="classCVC3_1_1VariableManagerNotifyObj.html#a1c7a6e4ffe9b150d74a382f33ea561e5">00440</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1VariableManagerNotifyObj.html#a1c7a6e4ffe9b150d74a382f33ea561e5">notify</a>(<span class="keywordtype">void</span>) { <a class="code" href="classCVC3_1_1VariableManagerNotifyObj.html#a24de96df43ce7e50a3c142fb04790c1c">d_vm</a>-><a class="code" href="classCVC3_1_1VariableManager.html#ad7d360514fcfd910668eabd097dbe81c" title="Resume garbage collection.">resumeGC</a>(); }
<a name="l00441"></a>00441 };
<a name="l00442"></a>00442
<a name="l00443"></a>00443
<a name="l00444"></a>00444 } <span class="comment">// end of namespace CVC3</span>
<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>
