<!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.cpp 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.cpp</div> </div>
</div>
<div class="contents">
<a href="variable_8cpp.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.cpp</span>
<a name="l00004"></a>00004 <span class="comment"> * \brief Implementation of class Variable; see variable.h for detail.</span>
<a name="l00005"></a>00005 <span class="comment"> * </span>
<a name="l00006"></a>00006 <span class="comment"> * Author: Sergey Berezin</span>
<a name="l00007"></a>00007 <span class="comment"> * </span>
<a name="l00008"></a>00008 <span class="comment"> * Created: Fri Apr 25 12:30:17 2003</span>
<a name="l00009"></a>00009 <span class="comment"> *</span>
<a name="l00010"></a>00010 <span class="comment"> * <hr></span>
<a name="l00011"></a>00011 <span class="comment"> *</span>
<a name="l00012"></a>00012 <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span>
<a name="l00013"></a>00013 <span class="comment"> * and its documentation for any purpose is hereby granted without</span>
<a name="l00014"></a>00014 <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span>
<a name="l00015"></a>00015 <span class="comment"> * LICENSE file provided with this distribution.</span>
<a name="l00016"></a>00016 <span class="comment"> * </span>
<a name="l00017"></a>00017 <span class="comment"> * <hr></span>
<a name="l00018"></a>00018 <span class="comment"> * </span>
<a name="l00019"></a>00019 <span class="comment"> */</span>
<a name="l00020"></a>00020 <span class="comment">/*****************************************************************************/</span>
<a name="l00021"></a>00021
<a name="l00022"></a>00022 <span class="preprocessor">#include <sstream></span>
<a name="l00023"></a>00023 <span class="preprocessor">#include "<a class="code" href="variable_8h.html">variable.h</a>"</span>
<a name="l00024"></a>00024 <span class="preprocessor">#include "<a class="code" href="search__rules_8h.html" title="Abstract proof rules interface to the simple search engine.">search_rules.h</a>"</span>
<a name="l00025"></a>00025 <span class="preprocessor">#include "<a class="code" href="memory__manager__chunks_8h.html">memory_manager_chunks.h</a>"</span>
<a name="l00026"></a>00026 <span class="preprocessor">#include "<a class="code" href="memory__manager__malloc_8h.html">memory_manager_malloc.h</a>"</span>
<a name="l00027"></a>00027
<a name="l00028"></a>00028 <span class="keyword">using namespace </span>std;
<a name="l00029"></a>00029
<a name="l00030"></a>00030 <span class="keyword">namespace </span>CVC3 {
<a name="l00031"></a>00031 <span class="comment"></span>
<a name="l00032"></a>00032 <span class="comment">///////////////////////////////////////////////////////////////////////</span>
<a name="l00033"></a>00033 <span class="comment"></span><span class="comment">// class Variable methods</span><span class="comment"></span>
<a name="l00034"></a>00034 <span class="comment">///////////////////////////////////////////////////////////////////////</span>
<a name="l00035"></a>00035 <span class="comment"></span>
<a name="l00036"></a>00036 <span class="comment">// Constructors</span>
<a name="l00037"></a><a class="code" href="classCVC3_1_1Variable.html#a32d191ff6db4d462c902f07fe4d5045b">00037</a> Variable::Variable(<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="l00038"></a>00038 : d_val(vm->newVariableValue(e))
<a name="l00039"></a>00039 {
<a name="l00040"></a>00040 <a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>-><a class="code" href="classCVC3_1_1VariableValue.html#ac70959550ac5f1a1c22351519e5547df">d_refcount</a>++;
<a name="l00041"></a>00041 }
<a name="l00042"></a>00042
<a name="l00043"></a><a class="code" href="classCVC3_1_1Variable.html#a76a03757802705d6496c35f296a935aa">00043</a> <a class="code" href="classCVC3_1_1Variable.html#a7659f63344c25dbc8209c4c531b2f0be">Variable::Variable</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Variable.html">Variable</a>& l): d_val(l.d_val) {
<a name="l00044"></a>00044 <span class="keywordflow">if</span>(!<a class="code" href="classCVC3_1_1Variable.html#a35c435274fa96599d47f16239b843584">isNull</a>()) <a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>-><a class="code" href="classCVC3_1_1VariableValue.html#ac70959550ac5f1a1c22351519e5547df">d_refcount</a>++;
<a name="l00045"></a>00045 }
<a name="l00046"></a>00046
<a name="l00047"></a>00047 <span class="comment">// Destructor</span>
<a name="l00048"></a><a class="code" href="classCVC3_1_1Variable.html#a21a9c85dd3b1320e8192fd581da15af4">00048</a> <a class="code" href="classCVC3_1_1Variable.html#a21a9c85dd3b1320e8192fd581da15af4">Variable::~Variable</a>() {
<a name="l00049"></a>00049 <span class="keywordflow">if</span>(!<a class="code" href="classCVC3_1_1Variable.html#a35c435274fa96599d47f16239b843584">isNull</a>()) {
<a name="l00050"></a>00050 <span class="keywordflow">if</span>(--(<a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>-><a class="code" href="classCVC3_1_1VariableValue.html#ac70959550ac5f1a1c22351519e5547df">d_refcount</a>) == 0)
<a name="l00051"></a>00051 <a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>-><a class="code" href="classCVC3_1_1VariableValue.html#a8b9cd77982124084ed87e4fde0e6460a">d_vm</a>-><a class="code" href="classCVC3_1_1VariableManager.html#a5f35575560aac2140e817aa49190894d" title="Garbage collect VariableValue pointer.">gc</a>(<a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>);
<a name="l00052"></a>00052 }
<a name="l00053"></a>00053 }
<a name="l00054"></a>00054
<a name="l00055"></a>00055 <span class="comment">// Assignment</span>
<a name="l00056"></a>00056 <a class="code" href="classCVC3_1_1Variable.html">Variable</a>&
<a name="l00057"></a><a class="code" href="classCVC3_1_1Variable.html#a551554c97de770f4160444c440342ac5">00057</a> <a class="code" href="classCVC3_1_1Variable.html#a551554c97de770f4160444c440342ac5">Variable::operator=</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Variable.html">Variable</a>& l) {
<a name="l00058"></a>00058 <span class="keywordflow">if</span>(&l == <span class="keyword">this</span>) <span class="keywordflow">return</span> *<span class="keyword">this</span>; <span class="comment">// Self-assignment</span>
<a name="l00059"></a>00059 <span class="keywordflow">if</span>(!<a class="code" href="classCVC3_1_1Variable.html#a35c435274fa96599d47f16239b843584">isNull</a>()) {
<a name="l00060"></a>00060 <span class="keywordflow">if</span>(--(<a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>-><a class="code" href="classCVC3_1_1VariableValue.html#ac70959550ac5f1a1c22351519e5547df">d_refcount</a>) == 0) <a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>-><a class="code" href="classCVC3_1_1VariableValue.html#a8b9cd77982124084ed87e4fde0e6460a">d_vm</a>-><a class="code" href="classCVC3_1_1VariableManager.html#a5f35575560aac2140e817aa49190894d" title="Garbage collect VariableValue pointer.">gc</a>(<a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>);
<a name="l00061"></a>00061 }
<a name="l00062"></a>00062 <a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a> = l.<a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>;
<a name="l00063"></a>00063 <span class="keywordflow">if</span>(!<a class="code" href="classCVC3_1_1Variable.html#a35c435274fa96599d47f16239b843584">isNull</a>()) <a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>-><a class="code" href="classCVC3_1_1VariableValue.html#ac70959550ac5f1a1c22351519e5547df">d_refcount</a>++;
<a name="l00064"></a>00064 <span class="keywordflow">return</span> *<span class="keyword">this</span>;
<a name="l00065"></a>00065 }
<a name="l00066"></a>00066
<a name="l00067"></a>00067 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>&
<a name="l00068"></a><a class="code" href="classCVC3_1_1Variable.html#af85a6bbfd1529fce66f70d0012556fdf">00068</a> <a class="code" href="classCVC3_1_1Variable.html#af85a6bbfd1529fce66f70d0012556fdf">Variable::getExpr</a>()<span class="keyword"> const </span>{
<a name="l00069"></a>00069 <span class="keyword">static</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> null;
<a name="l00070"></a>00070 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1Variable.html#a35c435274fa96599d47f16239b843584">isNull</a>()) <span class="keywordflow">return</span> null;
<a name="l00071"></a>00071 <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#a5e3bf7de7f3bd16d1b274e16d4292893">getExpr</a>();
<a name="l00072"></a>00072 }
<a name="l00073"></a>00073
<a name="l00074"></a>00074 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>&
<a name="l00075"></a><a class="code" href="classCVC3_1_1Variable.html#a6d8d3752f50dc4ce55d12e252398c837">00075</a> <a class="code" href="classCVC3_1_1Variable.html#a6d8d3752f50dc4ce55d12e252398c837">Variable::getNegExpr</a>()<span class="keyword"> const </span>{
<a name="l00076"></a>00076 <span class="keyword">static</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> null;
<a name="l00077"></a>00077 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1Variable.html#a35c435274fa96599d47f16239b843584">isNull</a>()) <span class="keywordflow">return</span> null;
<a name="l00078"></a>00078 <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#a798fc6fa670819203aa7e2ecf3a609de">getNegExpr</a>();
<a name="l00079"></a>00079 }
<a name="l00080"></a>00080
<a name="l00081"></a>00081 <span class="comment">// IMPORTANT: Value can be -1 (false), 1 (true), or 0 (unresolved)</span>
<a name="l00082"></a>00082 <span class="keywordtype">int</span>
<a name="l00083"></a><a class="code" href="classCVC3_1_1Variable.html#a36e8ce7a305e07e00adc90f6c22c4916">00083</a> <a class="code" href="classCVC3_1_1Variable.html#a36e8ce7a305e07e00adc90f6c22c4916">Variable::getValue</a>()<span class="keyword"> const </span>{
<a name="l00084"></a>00084 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1Variable.html#a35c435274fa96599d47f16239b843584">isNull</a>()) <span class="keywordflow">return</span> 0;
<a name="l00085"></a>00085 <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#a6f83bd36830c43e35d21984cd5b3a3ff">getValue</a>();
<a name="l00086"></a>00086 }
<a name="l00087"></a>00087
<a name="l00088"></a>00088
<a name="l00089"></a>00089 <span class="keywordtype">int</span>
<a name="l00090"></a><a class="code" href="classCVC3_1_1Variable.html#a6e50e61e2eaf7054bd1d84e4137ba270">00090</a> <a class="code" href="classCVC3_1_1Variable.html#a6e50e61e2eaf7054bd1d84e4137ba270">Variable::getScope</a>()<span class="keyword"> const </span>{
<a name="l00091"></a>00091 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1Variable.html#a35c435274fa96599d47f16239b843584">isNull</a>()) <span class="keywordflow">return</span> 0;
<a name="l00092"></a>00092 <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#aabc451feb269d84dc19bdc1148bc8af8">getScope</a>();
<a name="l00093"></a>00093 }
<a name="l00094"></a>00094
<a name="l00095"></a>00095 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>&
<a name="l00096"></a><a class="code" href="classCVC3_1_1Variable.html#a6cdc655ea6aaf36c8e8029af0dc41075">00096</a> <a class="code" href="classCVC3_1_1Variable.html#a6cdc655ea6aaf36c8e8029af0dc41075">Variable::getTheorem</a>()<span class="keyword"> const </span>{
<a name="l00097"></a>00097 <span class="keyword">static</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> null;
<a name="l00098"></a>00098 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1Variable.html#a35c435274fa96599d47f16239b843584">isNull</a>()) <span class="keywordflow">return</span> null;
<a name="l00099"></a>00099 <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#a2a186bfae906f1fa27d64457f2428125">getTheorem</a>();
<a name="l00100"></a>00100 }
<a name="l00101"></a>00101
<a name="l00102"></a>00102 <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 name="l00103"></a><a class="code" href="classCVC3_1_1Variable.html#a5bbd362f586ab0dbbc3432d140f77aab">00103</a> <a class="code" href="classCVC3_1_1Variable.html#a5bbd362f586ab0dbbc3432d140f77aab">Variable::getAntecedent</a>()<span class="keyword"> const </span>{
<a name="l00104"></a>00104 <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="l00105"></a>00105 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1Variable.html#a35c435274fa96599d47f16239b843584">isNull</a>()) <span class="keywordflow">return</span> null;
<a name="l00106"></a>00106 <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#aac80324d8bc82742954381946066c103">getAntecedent</a>();
<a name="l00107"></a>00107 }
<a name="l00108"></a>00108
<a name="l00109"></a>00109 <span class="keywordtype">int</span>
<a name="l00110"></a><a class="code" href="classCVC3_1_1Variable.html#a681407094080368feea5c496ed3bdb69">00110</a> <a class="code" href="classCVC3_1_1Variable.html#a681407094080368feea5c496ed3bdb69">Variable::getAntecedentIdx</a>()<span class="keyword"> const </span>{
<a name="l00111"></a>00111 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1Variable.html#a35c435274fa96599d47f16239b843584">isNull</a>()) <span class="keywordflow">return</span> 0;
<a name="l00112"></a>00112 <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#a5ead45485317b8beb32d1489d71b7274">getAntecedentIdx</a>();
<a name="l00113"></a>00113 }
<a name="l00114"></a>00114
<a name="l00115"></a>00115 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>&
<a name="l00116"></a><a class="code" href="classCVC3_1_1Variable.html#a535715bc38709f902feb3f77aef4f89d">00116</a> <a class="code" href="classCVC3_1_1Variable.html#a535715bc38709f902feb3f77aef4f89d">Variable::getAssumpThm</a>()<span class="keyword"> const </span>{
<a name="l00117"></a>00117 <span class="keyword">static</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> null;
<a name="l00118"></a>00118 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1Variable.html#a35c435274fa96599d47f16239b843584">isNull</a>()) <span class="keywordflow">return</span> null;
<a name="l00119"></a>00119 <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#a600aed64a238804fc7e6e5717a07a6f5">getAssumpThm</a>();
<a name="l00120"></a>00120 }
<a name="l00121"></a>00121
<a name="l00122"></a>00122 <span class="comment">// Setting the attributes: it can be either derived from the</span>
<a name="l00123"></a>00123 <span class="comment">// antecedent clause, or by a theorem. The scope level is set to</span>
<a name="l00124"></a>00124 <span class="comment">// the current scope.</span>
<a name="l00125"></a>00125 <span class="keywordtype">void</span>
<a name="l00126"></a><a class="code" href="classCVC3_1_1Variable.html#ac1d2bf9a1a8eec600ffa18b679ef4d2c">00126</a> <a class="code" href="classCVC3_1_1Variable.html#ac1d2bf9a1a8eec600ffa18b679ef4d2c">Variable::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="l00127"></a>00127 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!<a class="code" href="classCVC3_1_1Variable.html#a35c435274fa96599d47f16239b843584">isNull</a>(), <span class="stringliteral">"Variable::setValue(antecedent): var is NULL"</span>);
<a name="l00128"></a>00128 <a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>-><a class="code" href="classCVC3_1_1VariableValue.html#aefcf6649a5dcfa1382c3a296659b57a5">setValue</a>(val, c, idx);
<a name="l00129"></a>00129 }
<a name="l00130"></a>00130
<a name="l00131"></a>00131 <span class="comment">// The theorem's expr must be the same as the variable's expr or</span>
<a name="l00132"></a>00132 <span class="comment">// its negation</span>
<a name="l00133"></a>00133 <span class="keywordtype">void</span>
<a name="l00134"></a><a class="code" href="classCVC3_1_1Variable.html#a860c092f668decb472202b137ca6e683">00134</a> <a class="code" href="classCVC3_1_1Variable.html#ac1d2bf9a1a8eec600ffa18b679ef4d2c">Variable::setValue</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm) {
<a name="l00135"></a>00135 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!<a class="code" href="classCVC3_1_1Variable.html#a35c435274fa96599d47f16239b843584">isNull</a>(), <span class="stringliteral">"Variable::setValue(Theorem): var is NULL"</span>);
<a name="l00136"></a>00136 <a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>-><a class="code" href="classCVC3_1_1VariableValue.html#aefcf6649a5dcfa1382c3a296659b57a5">setValue</a>(thm, thm.<a class="code" href="classCVC3_1_1Theorem.html#a112466d9793abcf97015233ffdc4ec5e">getScope</a>());
<a name="l00137"></a>00137 }
<a name="l00138"></a>00138
<a name="l00139"></a>00139 <span class="keywordtype">void</span>
<a name="l00140"></a><a class="code" href="classCVC3_1_1Variable.html#aeccc8931258bf6931c9a40a82e761144">00140</a> <a class="code" href="classCVC3_1_1Variable.html#ac1d2bf9a1a8eec600ffa18b679ef4d2c">Variable::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="l00141"></a>00141 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!<a class="code" href="classCVC3_1_1Variable.html#a35c435274fa96599d47f16239b843584">isNull</a>(), <span class="stringliteral">"Variable::setValue(Theorem,scope): var is NULL"</span>);
<a name="l00142"></a>00142 <a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>-><a class="code" href="classCVC3_1_1VariableValue.html#aefcf6649a5dcfa1382c3a296659b57a5">setValue</a>(thm, scope);
<a name="l00143"></a>00143 }
<a name="l00144"></a>00144
<a name="l00145"></a>00145 <span class="keywordtype">void</span>
<a name="l00146"></a><a class="code" href="classCVC3_1_1Variable.html#a688678fbc2dc4e25d9dbba2e4c7d72a5">00146</a> <a class="code" href="classCVC3_1_1Variable.html#a688678fbc2dc4e25d9dbba2e4c7d72a5">Variable::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="l00147"></a>00147 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!<a class="code" href="classCVC3_1_1Variable.html#a35c435274fa96599d47f16239b843584">isNull</a>(), <span class="stringliteral">"Variable::setAssumpThm(): var is NULL"</span>);
<a name="l00148"></a>00148 <a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>-><a class="code" href="classCVC3_1_1VariableValue.html#abfd2af792b3d79935abf5fa2db7e8218">setAssumpThm</a>(a, scope);
<a name="l00149"></a>00149 }
<a name="l00150"></a>00150
<a name="l00151"></a>00151 <span class="comment">// Derive the theorem for either the variable or its negation. If</span>
<a name="l00152"></a>00152 <span class="comment">// the value is set by a theorem, that theorem is returned;</span>
<a name="l00153"></a>00153 <span class="comment">// otherwise a unit propagation rule is applied to the antecedent</span>
<a name="l00154"></a>00154 <span class="comment">// clause, and the theorem is cached for a quick access later.</span>
<a name="l00155"></a>00155 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l00156"></a><a class="code" href="classCVC3_1_1Variable.html#ad499afb9e33f92c2efd7cf92638e0396">00156</a> <a class="code" href="classCVC3_1_1Variable.html#ad499afb9e33f92c2efd7cf92638e0396">Variable::deriveTheorem</a>()<span class="keyword"> const </span>{
<a name="l00157"></a>00157 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Variable.html#a3511123177ecb1126031b1b88d37fd0a">deriveThmRec</a>(<span class="keyword">false</span>);
<a name="l00158"></a>00158 }
<a name="l00159"></a>00159
<a name="l00160"></a>00160
<a name="l00161"></a>00161 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l00162"></a><a class="code" href="classCVC3_1_1Variable.html#a3511123177ecb1126031b1b88d37fd0a">00162</a> <a class="code" href="classCVC3_1_1Variable.html#a3511123177ecb1126031b1b88d37fd0a">Variable::deriveThmRec</a>(<span class="keywordtype">bool</span> checkAssump)<span class="keyword"> const </span>{
<a name="l00163"></a>00163 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!<a class="code" href="classCVC3_1_1Variable.html#a35c435274fa96599d47f16239b843584">isNull</a>(), <span class="stringliteral">"Variable::deriveTheorem(): called on Null"</span>);
<a name="l00164"></a>00164 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1Variable.html#a36e8ce7a305e07e00adc90f6c22c4916">getValue</a>() != 0, <span class="stringliteral">"Variable::deriveTheorem(): value is not set: "</span>
<a name="l00165"></a>00165 + <a class="code" href="classCVC3_1_1Variable.html#a82f724d0ece90488867aa2de8cc43c32">toString</a>());
<a name="l00166"></a>00166 <span class="keywordflow">if</span>(!<a class="code" href="classCVC3_1_1Variable.html#a6cdc655ea6aaf36c8e8029af0dc41075">getTheorem</a>().<a class="code" href="classCVC3_1_1Variable.html#a35c435274fa96599d47f16239b843584">isNull</a>()) <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Variable.html#a6cdc655ea6aaf36c8e8029af0dc41075">getTheorem</a>();
<a name="l00167"></a>00167 <span class="keywordflow">if</span>(checkAssump && !<a class="code" href="classCVC3_1_1Variable.html#a535715bc38709f902feb3f77aef4f89d">getAssumpThm</a>().<a class="code" href="classCVC3_1_1Variable.html#a35c435274fa96599d47f16239b843584">isNull</a>()) <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Variable.html#a535715bc38709f902feb3f77aef4f89d">getAssumpThm</a>();
<a name="l00168"></a>00168 <span class="comment">// Have to derive the theorem</span>
<a name="l00169"></a>00169 <a class="code" href="classCVC3_1_1Clause.html" title="A class representing a CNF clause (a smart pointer)">Clause</a> c(<a class="code" href="classCVC3_1_1Variable.html#a5bbd362f586ab0dbbc3432d140f77aab">getAntecedent</a>());
<a name="l00170"></a>00170 <span class="keywordtype">int</span> idx(<a class="code" href="classCVC3_1_1Variable.html#a681407094080368feea5c496ed3bdb69">getAntecedentIdx</a>());
<a name="l00171"></a>00171 <span class="keyword">const</span> vector<Literal>& lits = c.<a class="code" href="classCVC3_1_1Clause.html#afbdcb9cd34cb4ff3e14f2e5aace81d7e">getLiterals</a>();
<a name="l00172"></a>00172 <span class="comment">// Theorems for the other literals in the antecedent clause</span>
<a name="l00173"></a>00173 vector<Theorem> thms;
<a name="l00174"></a>00174 <span class="keywordtype">int</span> size(lits.size());
<a name="l00175"></a>00175 <span class="comment">// Derive theorems recursively</span>
<a name="l00176"></a>00176 <span class="keywordflow">for</span>(<span class="keywordtype">int</span> i=0; i<size; ++i)
<a name="l00177"></a>00177 <span class="keywordflow">if</span>(i!=idx) thms.push_back(lits[i].getVar().<a class="code" href="classCVC3_1_1Variable.html#a3511123177ecb1126031b1b88d37fd0a">deriveThmRec</a>(<span class="keyword">true</span>));
<a name="l00178"></a>00178 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> thm;
<a name="l00179"></a>00179 <span class="keywordflow">if</span>(idx!=-1)
<a name="l00180"></a>00180 thm = <a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>-><a class="code" href="classCVC3_1_1VariableValue.html#a8b9cd77982124084ed87e4fde0e6460a">d_vm</a>-><a class="code" href="classCVC3_1_1VariableManager.html#a0d68fbe0c1eb8b19d8d91984c290ef28">getRules</a>()-><a class="code" href="group__SE__Rules.html#gae7221bb8b77313a9b53a4beca9cc0aa0" title="Unit propagation rule: .">unitProp</a>(thms, c.<a class="code" href="classCVC3_1_1Clause.html#aa933cec7528780d7971be0c10b76dc02">getTheorem</a>(), idx);
<a name="l00181"></a>00181 <span class="keywordflow">else</span>
<a name="l00182"></a>00182 thm = <a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>-><a class="code" href="classCVC3_1_1VariableValue.html#a8b9cd77982124084ed87e4fde0e6460a">d_vm</a>-><a class="code" href="classCVC3_1_1VariableManager.html#a0d68fbe0c1eb8b19d8d91984c290ef28">getRules</a>()-><a class="code" href="group__SE__Rules.html#ga9c74425b4471d411f58f16781951c441" title=""Conflict" rule (all literals in a clause become FALSE) ">conflictRule</a>(thms, c.<a class="code" href="classCVC3_1_1Clause.html#aa933cec7528780d7971be0c10b76dc02">getTheorem</a>());
<a name="l00183"></a>00183
<a name="l00184"></a>00184 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e(thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());)
<a name="l00185"></a>00185 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(e == <a class="code" href="classCVC3_1_1Variable.html#af85a6bbfd1529fce66f70d0012556fdf">getExpr</a>()
<a name="l00186"></a>00186 || (e.isNot() && e[0] == <a class="code" href="classCVC3_1_1Variable.html#af85a6bbfd1529fce66f70d0012556fdf">getExpr</a>()),
<a name="l00187"></a>00187 <span class="stringliteral">"Variable::deriveTheorem: bad theorem derived: expr ="</span>
<a name="l00188"></a>00188 + <a class="code" href="classCVC3_1_1Variable.html#a82f724d0ece90488867aa2de8cc43c32">toString</a>() + <span class="stringliteral">", thm = "</span> + thm.<a class="code" href="classCVC3_1_1Theorem.html#ac4b1c9570ffb9cc901627ef2abb9ff77">toString</a>());
<a name="l00189"></a>00189 <span class="comment">// Cache the result</span>
<a name="l00190"></a>00190 <a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>-><a class="code" href="classCVC3_1_1VariableValue.html#aefcf6649a5dcfa1382c3a296659b57a5">setValue</a>(thm, <a class="code" href="classCVC3_1_1Variable.html#a6e50e61e2eaf7054bd1d84e4137ba270">getScope</a>());
<a name="l00191"></a>00191 <span class="keywordflow">return</span> thm;
<a name="l00192"></a>00192 }
<a name="l00193"></a>00193
<a name="l00194"></a>00194 <span class="keywordtype">string</span>
<a name="l00195"></a><a class="code" href="classCVC3_1_1Variable.html#a82f724d0ece90488867aa2de8cc43c32">00195</a> <a class="code" href="classCVC3_1_1Variable.html#a82f724d0ece90488867aa2de8cc43c32">Variable::toString</a>()<span class="keyword"> const </span>{
<a name="l00196"></a>00196 ostringstream ss;
<a name="l00197"></a>00197 ss << *<span class="keyword">this</span>;
<a name="l00198"></a>00198 <span class="keywordflow">return</span> ss.str();
<a name="l00199"></a>00199 }
<a name="l00200"></a>00200
<a name="l00201"></a>00201 <span class="comment">// Friend methods</span>
<a name="l00202"></a><a class="code" href="namespaceCVC3.html#a71fd4b09b9f60277f81c79f7d3e9ec1b">00202</a> ostream& <a class="code" href="namespaceCVC3.html#a6b7e38d3c97da1e91e12a6c9555b8163">operator<<</a>(ostream& os, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Variable.html">Variable</a>& l) {
<a name="l00203"></a>00203 <span class="keywordflow">return</span> os << (*l.<a class="code" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>);
<a name="l00204"></a>00204 }
<a name="l00205"></a>00205 <span class="comment"></span>
<a name="l00206"></a>00206 <span class="comment">///////////////////////////////////////////////////////////////////////</span>
<a name="l00207"></a>00207 <span class="comment"></span><span class="comment">// class Literal methods</span><span class="comment"></span>
<a name="l00208"></a>00208 <span class="comment">///////////////////////////////////////////////////////////////////////</span>
<a name="l00209"></a>00209 <span class="comment"></span>
<a name="l00210"></a>00210 <span class="keywordtype">string</span>
<a name="l00211"></a><a class="code" href="classCVC3_1_1Literal.html#aff53e6b3e4da8c649816441046983a30">00211</a> <a class="code" href="classCVC3_1_1Literal.html#aff53e6b3e4da8c649816441046983a30">Literal::toString</a>()<span class="keyword"> const </span>{
<a name="l00212"></a>00212 ostringstream ss;
<a name="l00213"></a>00213 ss << *<span class="keyword">this</span>;
<a name="l00214"></a>00214 <span class="keywordflow">return</span> ss.str();
<a name="l00215"></a>00215 }
<a name="l00216"></a>00216
<a name="l00217"></a><a class="code" href="namespaceCVC3.html#a7acef296d5c77cb9e3cc84c996d57cef">00217</a> ostream& <a class="code" href="namespaceCVC3.html#a6b7e38d3c97da1e91e12a6c9555b8163">operator<<</a>(ostream& os, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Literal.html">Literal</a>& l) {
<a name="l00218"></a>00218 os << <span class="stringliteral">"Lit("</span> << (l.<a class="code" href="classCVC3_1_1Literal.html#aad653dd8534feb823b9d30f060b4e181">isNegative</a>()? <span class="stringliteral">"!"</span> : <span class="stringliteral">""</span>)
<a name="l00219"></a>00219 << l.<a class="code" href="classCVC3_1_1Literal.html#af43cfe38032a00cc8e8e60b0389eeb3e">getVar</a>();
<a name="l00220"></a>00220 <span class="comment">// Attributes</span>
<a name="l00221"></a>00221 os << <span class="stringliteral">", count="</span> << l.<a class="code" href="classCVC3_1_1Literal.html#a4823b2e9ec3a6a13a28c209d22269564">count</a>() << <span class="stringliteral">", score="</span> << l.<a class="code" href="classCVC3_1_1Literal.html#a436c5126780bd81c31bc01a868b5b857">score</a>();
<a name="l00222"></a>00222 <span class="keywordflow">return</span> os << <span class="stringliteral">")"</span>;
<a name="l00223"></a>00223 }
<a name="l00224"></a>00224 <span class="comment"></span>
<a name="l00225"></a>00225 <span class="comment">///////////////////////////////////////////////////////////////////////</span>
<a name="l00226"></a>00226 <span class="comment"></span><span class="comment">// class VariableValue methods</span><span class="comment"></span>
<a name="l00227"></a>00227 <span class="comment">///////////////////////////////////////////////////////////////////////</span>
<a name="l00228"></a>00228 <span class="comment"></span>
<a name="l00229"></a>00229 <span class="comment">// Destructor</span>
<a name="l00230"></a><a class="code" href="classCVC3_1_1VariableValue.html#ac74e3ee4ad23bfeb6254a6e4769d104c">00230</a> <a class="code" href="classCVC3_1_1VariableValue.html#ac74e3ee4ad23bfeb6254a6e4769d104c">VariableValue::~VariableValue</a>() {
<a name="l00231"></a>00231 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1VariableValue.html#ada795515a6c29d6301cdb643c7b0479e">d_val</a>!=NULL) { <span class="keyword">delete</span> <a class="code" href="classCVC3_1_1VariableValue.html#ada795515a6c29d6301cdb643c7b0479e">d_val</a>; free(<a class="code" href="classCVC3_1_1VariableValue.html#ada795515a6c29d6301cdb643c7b0479e">d_val</a>); <a class="code" href="classCVC3_1_1VariableValue.html#ada795515a6c29d6301cdb643c7b0479e">d_val</a> = NULL; }
<a name="l00232"></a>00232 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1VariableValue.html#a091dd8e7d8ba7c99080e169931e5007a">d_scope</a>!=NULL) { <span class="keyword">delete</span> <a class="code" href="classCVC3_1_1VariableValue.html#a091dd8e7d8ba7c99080e169931e5007a">d_scope</a>; free(<a class="code" href="classCVC3_1_1VariableValue.html#a091dd8e7d8ba7c99080e169931e5007a">d_scope</a>); <a class="code" href="classCVC3_1_1VariableValue.html#a091dd8e7d8ba7c99080e169931e5007a">d_scope</a> = NULL; }
<a name="l00233"></a>00233 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1VariableValue.html#a4f427c91c94b29fac5fe8280e2cc45d9">d_thm</a>!=NULL) { <span class="keyword">delete</span> <a class="code" href="classCVC3_1_1VariableValue.html#a4f427c91c94b29fac5fe8280e2cc45d9">d_thm</a>; free(<a class="code" href="classCVC3_1_1VariableValue.html#a4f427c91c94b29fac5fe8280e2cc45d9">d_thm</a>); <a class="code" href="classCVC3_1_1VariableValue.html#a4f427c91c94b29fac5fe8280e2cc45d9">d_thm</a> = NULL; }
<a name="l00234"></a>00234 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1VariableValue.html#a87f6665f00344a0503c10bbe265f2432">d_ante</a>!=NULL) { <span class="keyword">delete</span> <a class="code" href="classCVC3_1_1VariableValue.html#a87f6665f00344a0503c10bbe265f2432">d_ante</a>; free(<a class="code" href="classCVC3_1_1VariableValue.html#a87f6665f00344a0503c10bbe265f2432">d_ante</a>); <a class="code" href="classCVC3_1_1VariableValue.html#a87f6665f00344a0503c10bbe265f2432">d_ante</a> = NULL; }
<a name="l00235"></a>00235 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1VariableValue.html#a4724b62ffc80fa403bd9f4aa9aa95578">d_anteIdx</a>!=NULL) { <span class="keyword">delete</span> <a class="code" href="classCVC3_1_1VariableValue.html#a4724b62ffc80fa403bd9f4aa9aa95578">d_anteIdx</a>; free(<a class="code" href="classCVC3_1_1VariableValue.html#a4724b62ffc80fa403bd9f4aa9aa95578">d_anteIdx</a>); <a class="code" href="classCVC3_1_1VariableValue.html#a4724b62ffc80fa403bd9f4aa9aa95578">d_anteIdx</a> = NULL; }
<a name="l00236"></a>00236 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1VariableValue.html#a345214752d3f0349a91c60a26cf53f29">d_assump</a>!=NULL) { <span class="keyword">delete</span> <a class="code" href="classCVC3_1_1VariableValue.html#a345214752d3f0349a91c60a26cf53f29">d_assump</a>; free(<a class="code" href="classCVC3_1_1VariableValue.html#a345214752d3f0349a91c60a26cf53f29">d_assump</a>); <a class="code" href="classCVC3_1_1VariableValue.html#a345214752d3f0349a91c60a26cf53f29">d_assump</a> = NULL; }
<a name="l00237"></a>00237 }
<a name="l00238"></a>00238
<a name="l00239"></a>00239 <span class="comment">// Setting the attributes: it can be either derived from the</span>
<a name="l00240"></a>00240 <span class="comment">// antecedent clause, or by a theorem</span>
<a name="l00241"></a>00241 <span class="keywordtype">void</span>
<a name="l00242"></a><a class="code" href="classCVC3_1_1VariableValue.html#aefcf6649a5dcfa1382c3a296659b57a5">00242</a> <a class="code" href="classCVC3_1_1VariableValue.html#aefcf6649a5dcfa1382c3a296659b57a5">VariableValue::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="l00243"></a>00243 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1VariableValue.html#ada795515a6c29d6301cdb643c7b0479e">d_val</a>==NULL) {
<a name="l00244"></a>00244 <span class="comment">// Make sure d_val==0 all the way to scope 0</span>
<a name="l00245"></a>00245 <a class="code" href="classCVC3_1_1VariableValue.html#ada795515a6c29d6301cdb643c7b0479e">d_val</a> = <span class="keyword">new</span>(<span class="keyword">true</span>) <a class="code" href="classCVC3_1_1CDO.html">CDO<int></a>(<a class="code" href="classCVC3_1_1VariableValue.html#a8b9cd77982124084ed87e4fde0e6460a">d_vm</a>-><a class="code" href="classCVC3_1_1VariableManager.html#a02e36e773779bc9e17472e265b70627c">getCM</a>()-><a class="code" href="classCVC3_1_1ContextManager.html#a66a7d900301c1459de90b048623d9297">getCurrentContext</a>(), 0, 0);
<a name="l00246"></a>00246 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(<a class="code" href="classCVC3_1_1VariableValue.html#ada795515a6c29d6301cdb643c7b0479e">d_val</a>->setName(<span class="stringliteral">"CDO[VariableValue::d_val]"</span>);)
<a name="l00247"></a>00247 }
<a name="l00248"></a>00248 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1VariableValue.html#a091dd8e7d8ba7c99080e169931e5007a">d_scope</a>==NULL) {
<a name="l00249"></a>00249 <a class="code" href="classCVC3_1_1VariableValue.html#a091dd8e7d8ba7c99080e169931e5007a">d_scope</a> = <span class="keyword">new</span>(<span class="keyword">true</span>) <a class="code" href="classCVC3_1_1CDO.html">CDO<int></a>(<a class="code" href="classCVC3_1_1VariableValue.html#a8b9cd77982124084ed87e4fde0e6460a">d_vm</a>-><a class="code" href="classCVC3_1_1VariableManager.html#a02e36e773779bc9e17472e265b70627c">getCM</a>()-><a class="code" href="classCVC3_1_1ContextManager.html#a66a7d900301c1459de90b048623d9297">getCurrentContext</a>());
<a name="l00250"></a>00250 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(<a class="code" href="classCVC3_1_1VariableValue.html#a091dd8e7d8ba7c99080e169931e5007a">d_scope</a>->setName(<span class="stringliteral">"CDO[VariableValue::d_scope]"</span>);)
<a name="l00251"></a>00251 }
<a name="l00252"></a>00252 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1VariableValue.html#a87f6665f00344a0503c10bbe265f2432">d_ante</a>==NULL) {
<a name="l00253"></a>00253 <a class="code" href="classCVC3_1_1VariableValue.html#a87f6665f00344a0503c10bbe265f2432">d_ante</a> = <span class="keyword">new</span>(<span class="keyword">true</span>) <a class="code" href="classCVC3_1_1CDO.html">CDO<Clause></a>(<a class="code" href="classCVC3_1_1VariableValue.html#a8b9cd77982124084ed87e4fde0e6460a">d_vm</a>-><a class="code" href="classCVC3_1_1VariableManager.html#a02e36e773779bc9e17472e265b70627c">getCM</a>()-><a class="code" href="classCVC3_1_1ContextManager.html#a66a7d900301c1459de90b048623d9297">getCurrentContext</a>());
<a name="l00254"></a>00254 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(<a class="code" href="classCVC3_1_1VariableValue.html#a87f6665f00344a0503c10bbe265f2432">d_ante</a>->setName(<span class="stringliteral">"CDO[VariableValue::d_ante]"</span>);)
<a name="l00255"></a>00255 }
<a name="l00256"></a>00256 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1VariableValue.html#a4724b62ffc80fa403bd9f4aa9aa95578">d_anteIdx</a>==NULL) {
<a name="l00257"></a>00257 <a class="code" href="classCVC3_1_1VariableValue.html#a4724b62ffc80fa403bd9f4aa9aa95578">d_anteIdx</a> = <span class="keyword">new</span>(<span class="keyword">true</span>) <a class="code" href="classCVC3_1_1CDO.html">CDO<int></a>(<a class="code" href="classCVC3_1_1VariableValue.html#a8b9cd77982124084ed87e4fde0e6460a">d_vm</a>-><a class="code" href="classCVC3_1_1VariableManager.html#a02e36e773779bc9e17472e265b70627c">getCM</a>()-><a class="code" href="classCVC3_1_1ContextManager.html#a66a7d900301c1459de90b048623d9297">getCurrentContext</a>());
<a name="l00258"></a>00258 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(<a class="code" href="classCVC3_1_1VariableValue.html#a4724b62ffc80fa403bd9f4aa9aa95578">d_anteIdx</a>->setName(<span class="stringliteral">"CDO[VariableValue::d_anteIdx]"</span>);)
<a name="l00259"></a>00259 }
<a name="l00260"></a>00260
<a name="l00261"></a>00261 <span class="comment">// Compute the scope from the antecedent clause</span>
<a name="l00262"></a>00262 <span class="comment">// Assume the clause is valid exactly at the bottom scope</span>
<a name="l00263"></a>00263 <span class="keywordtype">int</span> scope(c.<a class="code" href="classCVC3_1_1Clause.html#af505679fdb9d5b220115747cb4548612">getScope</a>());
<a name="l00264"></a>00264 <span class="keywordflow">for</span>(<span class="keywordtype">int</span> i=0, iend=c.<a class="code" href="classCVC3_1_1Clause.html#a7cfde40c65fc8eb4f733094fad07dfa1">size</a>(); i!=iend; ++i) {
<a name="l00265"></a>00265 <span class="keywordflow">if</span>(i!=idx) {
<a name="l00266"></a>00266 <span class="keywordtype">int</span> s(c[i].<a class="code" href="classCVC3_1_1VariableValue.html#aabc451feb269d84dc19bdc1148bc8af8">getScope</a>());
<a name="l00267"></a>00267 <span class="keywordflow">if</span>(s > scope) scope = s;
<a name="l00268"></a>00268 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(c[i].<a class="code" href="classCVC3_1_1VariableValue.html#a6f83bd36830c43e35d21984cd5b3a3ff">getValue</a>() != 0,
<a name="l00269"></a>00269 <span class="stringliteral">"VariableValue::setValue(ante): literal has no value: "</span>
<a name="l00270"></a>00270 <span class="stringliteral">"i="</span>+<a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(i)+<span class="stringliteral">" in\n clause = "</span>
<a name="l00271"></a>00271 +c.<a class="code" href="classCVC3_1_1Clause.html#a97eeb3430667cd3c05a3c977d7285102">toString</a>());
<a name="l00272"></a>00272 }
<a name="l00273"></a>00273 }
<a name="l00274"></a>00274
<a name="l00275"></a>00275 <a class="code" href="classCVC3_1_1VariableValue.html#ada795515a6c29d6301cdb643c7b0479e">d_val</a>-><a class="code" href="classCVC3_1_1CDO.html#ab4e881820af78a628c72691cb9c2128e">set</a>(val, scope);
<a name="l00276"></a>00276 <a class="code" href="classCVC3_1_1VariableValue.html#a091dd8e7d8ba7c99080e169931e5007a">d_scope</a>-><a class="code" href="classCVC3_1_1CDO.html#ab4e881820af78a628c72691cb9c2128e">set</a>(scope, scope); <span class="comment">// d_vm->getCM()->scopeLevel();</span>
<a name="l00277"></a>00277 <a class="code" href="classCVC3_1_1VariableValue.html#a87f6665f00344a0503c10bbe265f2432">d_ante</a>-><a class="code" href="classCVC3_1_1CDO.html#ab4e881820af78a628c72691cb9c2128e">set</a>(c, scope);
<a name="l00278"></a>00278 <a class="code" href="classCVC3_1_1VariableValue.html#a4724b62ffc80fa403bd9f4aa9aa95578">d_anteIdx</a>-><a class="code" href="classCVC3_1_1CDO.html#ab4e881820af78a628c72691cb9c2128e">set</a>(idx, scope);
<a name="l00279"></a>00279 <span class="comment">// Set the theorem to null, to clean up the old value</span>
<a name="l00280"></a>00280 <span class="keywordflow">if</span>(!<a class="code" href="classCVC3_1_1VariableValue.html#a2a186bfae906f1fa27d64457f2428125">getTheorem</a>().isNull()) <a class="code" href="classCVC3_1_1VariableValue.html#a4f427c91c94b29fac5fe8280e2cc45d9">d_thm</a>-><a class="code" href="classCVC3_1_1CDO.html#ab4e881820af78a628c72691cb9c2128e">set</a>(<a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>(), scope);
<a name="l00281"></a>00281
<a name="l00282"></a>00282 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> l((idx == -1)? <a class="code" href="classCVC3_1_1VariableValue.html#a5e3bf7de7f3bd16d1b274e16d4292893">getExpr</a>().getEM()->falseExpr()
<a name="l00283"></a>00283 : c[idx].<a class="code" href="classCVC3_1_1VariableValue.html#a5e3bf7de7f3bd16d1b274e16d4292893">getExpr</a>());)
<a name="l00284"></a>00284 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>((val > 0 && l == <a class="code" href="classCVC3_1_1VariableValue.html#a5e3bf7de7f3bd16d1b274e16d4292893">getExpr</a>())
<a name="l00285"></a>00285 || (val < 0 && l.isNot() && l[0] == <a class="code" href="classCVC3_1_1VariableValue.html#a5e3bf7de7f3bd16d1b274e16d4292893">getExpr</a>()),
<a name="l00286"></a>00286 <span class="stringliteral">"VariableValue::setValue(val = "</span> + <a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(val)
<a name="l00287"></a>00287 + <span class="stringliteral">", c = "</span> + c.<a class="code" href="classCVC3_1_1Clause.html#a97eeb3430667cd3c05a3c977d7285102">toString</a>() + <span class="stringliteral">", idx = "</span> + <a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(idx)
<a name="l00288"></a>00288 + <span class="stringliteral">"):\n expr = "</span> + <a class="code" href="classCVC3_1_1VariableValue.html#a5e3bf7de7f3bd16d1b274e16d4292893">getExpr</a>().<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>()
<a name="l00289"></a>00289 + <span class="stringliteral">"\n literal = "</span> + l.toString());
<a name="l00290"></a>00290 }
<a name="l00291"></a>00291
<a name="l00292"></a>00292 <span class="comment">// The theorem's expr must be the same as the variable's expr or</span>
<a name="l00293"></a>00293 <span class="comment">// its negation</span>
<a name="l00294"></a>00294 <span class="keywordtype">void</span>
<a name="l00295"></a><a class="code" href="classCVC3_1_1VariableValue.html#a3be05859755a92bd60ceeb4b5a2e99d6">00295</a> <a class="code" href="classCVC3_1_1VariableValue.html#aefcf6649a5dcfa1382c3a296659b57a5">VariableValue::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="l00296"></a>00296 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1VariableValue.html#ada795515a6c29d6301cdb643c7b0479e">d_val</a>==NULL) {
<a name="l00297"></a>00297 <span class="comment">// Make sure d_val==0 all the way to scope 0</span>
<a name="l00298"></a>00298 <a class="code" href="classCVC3_1_1VariableValue.html#ada795515a6c29d6301cdb643c7b0479e">d_val</a> = <span class="keyword">new</span>(<span class="keyword">true</span>) <a class="code" href="classCVC3_1_1CDO.html">CDO<int></a>(<a class="code" href="classCVC3_1_1VariableValue.html#a8b9cd77982124084ed87e4fde0e6460a">d_vm</a>-><a class="code" href="classCVC3_1_1VariableManager.html#a02e36e773779bc9e17472e265b70627c">getCM</a>()-><a class="code" href="classCVC3_1_1ContextManager.html#a66a7d900301c1459de90b048623d9297">getCurrentContext</a>(),0,0);
<a name="l00299"></a>00299 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(<a class="code" href="classCVC3_1_1VariableValue.html#ada795515a6c29d6301cdb643c7b0479e">d_val</a>->setName(<span class="stringliteral">"CDO[VariableValue::d_val]"</span>);)
<a name="l00300"></a>00300 }
<a name="l00301"></a>00301 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1VariableValue.html#a091dd8e7d8ba7c99080e169931e5007a">d_scope</a>==NULL) {
<a name="l00302"></a>00302 <a class="code" href="classCVC3_1_1VariableValue.html#a091dd8e7d8ba7c99080e169931e5007a">d_scope</a> = <span class="keyword">new</span>(<span class="keyword">true</span>) <a class="code" href="classCVC3_1_1CDO.html">CDO<int></a>(<a class="code" href="classCVC3_1_1VariableValue.html#a8b9cd77982124084ed87e4fde0e6460a">d_vm</a>-><a class="code" href="classCVC3_1_1VariableManager.html#a02e36e773779bc9e17472e265b70627c">getCM</a>()-><a class="code" href="classCVC3_1_1ContextManager.html#a66a7d900301c1459de90b048623d9297">getCurrentContext</a>());
<a name="l00303"></a>00303 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(<a class="code" href="classCVC3_1_1VariableValue.html#a091dd8e7d8ba7c99080e169931e5007a">d_scope</a>->setName(<span class="stringliteral">"CDO[VariableValue::d_scope]"</span>);)
<a name="l00304"></a>00304 }
<a name="l00305"></a>00305 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1VariableValue.html#a4f427c91c94b29fac5fe8280e2cc45d9">d_thm</a>==NULL) {
<a name="l00306"></a>00306 <a class="code" href="classCVC3_1_1VariableValue.html#a4f427c91c94b29fac5fe8280e2cc45d9">d_thm</a> = <span class="keyword">new</span>(<span class="keyword">true</span>) <a class="code" href="classCVC3_1_1CDO.html">CDO<Theorem></a>(<a class="code" href="classCVC3_1_1VariableValue.html#a8b9cd77982124084ed87e4fde0e6460a">d_vm</a>-><a class="code" href="classCVC3_1_1VariableManager.html#a02e36e773779bc9e17472e265b70627c">getCM</a>()-><a class="code" href="classCVC3_1_1ContextManager.html#a66a7d900301c1459de90b048623d9297">getCurrentContext</a>());
<a name="l00307"></a>00307 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(<a class="code" href="classCVC3_1_1VariableValue.html#a4f427c91c94b29fac5fe8280e2cc45d9">d_thm</a>->setName(<span class="stringliteral">"CDO[VariableValue::d_thm]"</span>);)
<a name="l00308"></a>00308 }
<a name="l00309"></a>00309
<a name="l00310"></a>00310 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e(thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00311"></a>00311 <span class="keywordtype">int</span> val(0);
<a name="l00312"></a>00312 <span class="keywordflow">if</span>(e == <a class="code" href="classCVC3_1_1VariableValue.html#aa38abcee5fb57b183108f033a150fdda">d_expr</a>) val = 1;
<a name="l00313"></a>00313 <span class="keywordflow">else</span> {
<a name="l00314"></a>00314 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(e.isNot() && e[0] == <a class="code" href="classCVC3_1_1VariableValue.html#aa38abcee5fb57b183108f033a150fdda">d_expr</a>,
<a name="l00315"></a>00315 <span class="stringliteral">"VariableValue::setValue(thm = "</span>
<a name="l00316"></a>00316 + thm.<a class="code" href="classCVC3_1_1Theorem.html#ac4b1c9570ffb9cc901627ef2abb9ff77">toString</a>() + <span class="stringliteral">"): expr = "</span> + <a class="code" href="classCVC3_1_1VariableValue.html#aa38abcee5fb57b183108f033a150fdda">d_expr</a>.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00317"></a>00317 val = -1;
<a name="l00318"></a>00318 }
<a name="l00319"></a>00319 <span class="comment">// Set the values on that scope</span>
<a name="l00320"></a>00320 <a class="code" href="classCVC3_1_1VariableValue.html#ada795515a6c29d6301cdb643c7b0479e">d_val</a>-><a class="code" href="classCVC3_1_1CDO.html#ab4e881820af78a628c72691cb9c2128e">set</a>(val, scope);
<a name="l00321"></a>00321 <a class="code" href="classCVC3_1_1VariableValue.html#a091dd8e7d8ba7c99080e169931e5007a">d_scope</a>-><a class="code" href="classCVC3_1_1CDO.html#ab4e881820af78a628c72691cb9c2128e">set</a>(scope, scope); <span class="comment">// d_vm->getCM()->scopeLevel();</span>
<a name="l00322"></a>00322 <a class="code" href="classCVC3_1_1VariableValue.html#a4f427c91c94b29fac5fe8280e2cc45d9">d_thm</a>-><a class="code" href="classCVC3_1_1CDO.html#ab4e881820af78a628c72691cb9c2128e">set</a>(thm, scope);
<a name="l00323"></a>00323 <span class="comment">// Set clause to null, to clean up the old value</span>
<a name="l00324"></a>00324 <span class="keywordflow">if</span>(!<a class="code" href="classCVC3_1_1VariableValue.html#aac80324d8bc82742954381946066c103">getAntecedent</a>().isNull()) <a class="code" href="classCVC3_1_1VariableValue.html#a87f6665f00344a0503c10bbe265f2432">d_ante</a>-><a class="code" href="classCVC3_1_1CDO.html#ab4e881820af78a628c72691cb9c2128e">set</a>(<a class="code" href="classCVC3_1_1Clause.html" title="A class representing a CNF clause (a smart pointer)">Clause</a>(), scope);
<a name="l00325"></a>00325 }
<a name="l00326"></a>00326
<a name="l00327"></a>00327 <span class="keywordtype">void</span>
<a name="l00328"></a><a class="code" href="classCVC3_1_1VariableValue.html#abfd2af792b3d79935abf5fa2db7e8218">00328</a> <a class="code" href="classCVC3_1_1VariableValue.html#abfd2af792b3d79935abf5fa2db7e8218">VariableValue::setAssumpThm</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="l00329"></a>00329 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1VariableValue.html#a345214752d3f0349a91c60a26cf53f29">d_assump</a>==NULL) {
<a name="l00330"></a>00330 <span class="comment">// Make sure d_val==0 all the way to scope 0</span>
<a name="l00331"></a>00331 <a class="code" href="classCVC3_1_1VariableValue.html#a345214752d3f0349a91c60a26cf53f29">d_assump</a> = <span class="keyword">new</span>(<span class="keyword">true</span>) <a class="code" href="classCVC3_1_1CDO.html">CDO<Theorem></a>(<a class="code" href="classCVC3_1_1VariableValue.html#a8b9cd77982124084ed87e4fde0e6460a">d_vm</a>-><a class="code" href="classCVC3_1_1VariableManager.html#a02e36e773779bc9e17472e265b70627c">getCM</a>()-><a class="code" href="classCVC3_1_1ContextManager.html#a66a7d900301c1459de90b048623d9297">getCurrentContext</a>());
<a name="l00332"></a>00332 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(<a class="code" href="classCVC3_1_1VariableValue.html#ada795515a6c29d6301cdb643c7b0479e">d_val</a>->setName(<span class="stringliteral">"CDO[VariableValue::d_val]"</span>);)
<a name="l00333"></a>00333 }
<a name="l00334"></a>00334 <a class="code" href="classCVC3_1_1VariableValue.html#a345214752d3f0349a91c60a26cf53f29">d_assump</a>-><a class="code" href="classCVC3_1_1CDO.html#ab4e881820af78a628c72691cb9c2128e">set</a>(thm, scope);
<a name="l00335"></a>00335 }
<a name="l00336"></a>00336
<a name="l00337"></a><a class="code" href="namespaceCVC3.html#abed99cdcb909aa149d9efca57fb11b15">00337</a> ostream& <a class="code" href="classCVC3_1_1VariableValue.html#a98e3d083ca34ed383ea51259c73fc81b">operator<<</a>(ostream& os, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1VariableValue.html">VariableValue</a>& v) {
<a name="l00338"></a>00338 os << <span class="stringliteral">"Var("</span> << v.<a class="code" href="classCVC3_1_1VariableValue.html#a5e3bf7de7f3bd16d1b274e16d4292893">getExpr</a>() << <span class="stringliteral">" = "</span> << v.<a class="code" href="classCVC3_1_1VariableValue.html#a6f83bd36830c43e35d21984cd5b3a3ff">getValue</a>();
<a name="l00339"></a>00339 <span class="keywordflow">if</span>(v.<a class="code" href="classCVC3_1_1VariableValue.html#a6f83bd36830c43e35d21984cd5b3a3ff">getValue</a>() != 0) {
<a name="l00340"></a>00340 os << <span class="stringliteral">" @ "</span> << v.<a class="code" href="classCVC3_1_1VariableValue.html#aabc451feb269d84dc19bdc1148bc8af8">getScope</a>();
<a name="l00341"></a>00341 <span class="keywordflow">if</span>(!v.<a class="code" href="classCVC3_1_1VariableValue.html#a2a186bfae906f1fa27d64457f2428125">getTheorem</a>().<a class="code" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</a>())
<a name="l00342"></a>00342 os << <span class="stringliteral">"; "</span> << v.<a class="code" href="classCVC3_1_1VariableValue.html#a2a186bfae906f1fa27d64457f2428125">getTheorem</a>();
<a name="l00343"></a>00343 <span class="keywordflow">else</span> <span class="keywordflow">if</span>(!v.<a class="code" href="classCVC3_1_1VariableValue.html#aac80324d8bc82742954381946066c103">getAntecedent</a>().<a class="code" href="classCVC3_1_1Clause.html#a60c298aa79d5cec791f8eeef2086e92f">isNull</a>()) {
<a name="l00344"></a>00344 os << <span class="stringliteral">"; #"</span> << v.<a class="code" href="classCVC3_1_1VariableValue.html#a5ead45485317b8beb32d1489d71b7274">getAntecedentIdx</a>()
<a name="l00345"></a>00345 << <span class="stringliteral">" in "</span> << <a class="code" href="classCVC3_1_1CompactClause.html">CompactClause</a>(v.<a class="code" href="classCVC3_1_1VariableValue.html#aac80324d8bc82742954381946066c103">getAntecedent</a>());
<a name="l00346"></a>00346 }
<a name="l00347"></a>00347 }
<a name="l00348"></a>00348 <span class="keywordflow">return</span> os << <span class="stringliteral">")"</span>;
<a name="l00349"></a>00349 }
<a name="l00350"></a>00350 <span class="comment"></span>
<a name="l00351"></a>00351 <span class="comment">///////////////////////////////////////////////////////////////////////</span>
<a name="l00352"></a>00352 <span class="comment"></span><span class="comment">// class VariableManager methods</span><span class="comment"></span>
<a name="l00353"></a>00353 <span class="comment">///////////////////////////////////////////////////////////////////////</span>
<a name="l00354"></a>00354 <span class="comment"></span>
<a name="l00355"></a>00355 <span class="comment">// Creating unique VariableValue</span>
<a name="l00356"></a>00356 <a class="code" href="classCVC3_1_1VariableValue.html#a97912bc131f38a4d5f93bb1456118a0b">VariableValue</a>*
<a name="l00357"></a><a class="code" href="classCVC3_1_1VariableManager.html#a2052323b56685b21f16d1062917dfe38">00357</a> <a class="code" href="classCVC3_1_1VariableManager.html#a2052323b56685b21f16d1062917dfe38">VariableManager::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="l00358"></a>00358 <a class="code" href="classCVC3_1_1VariableValue.html">VariableValue</a> vv(<span class="keyword">this</span>, e);
<a name="l00359"></a>00359 <a class="code" href="classHash_1_1hash__set.html#a87a125f71dd85de65e662559bd5a66dc">VariableValueSet::iterator</a> i(d_varSet.find(&vv)), iend(d_varSet.end());
<a name="l00360"></a>00360 <span class="keywordflow">if</span>(i != iend) <span class="keywordflow">return</span> (*i);
<a name="l00361"></a>00361 <span class="comment">// No such variable, create and insert one</span>
<a name="l00362"></a>00362 <a class="code" href="classCVC3_1_1VariableValue.html">VariableValue</a>* p_vv(<span class="keyword">new</span>(d_mm) <a class="code" href="classCVC3_1_1VariableValue.html#a97912bc131f38a4d5f93bb1456118a0b">VariableValue</a>(<span class="keyword">this</span>, e));
<a name="l00363"></a>00363 d_varSet.insert(p_vv);
<a name="l00364"></a>00364 <span class="keywordflow">return</span> p_vv;
<a name="l00365"></a>00365 }
<a name="l00366"></a>00366
<a name="l00367"></a>00367 <span class="comment">// Constructor</span>
<a name="l00368"></a><a class="code" href="classCVC3_1_1VariableManager.html#a7faa284a5e5a72a87426de1f5cbf1bc9">00368</a> <a class="code" href="classCVC3_1_1VariableValue.html#a06b58135e80b3f9cee3779c4012bb13b">VariableManager::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="l00369"></a>00369 <span class="keyword">const</span> <span class="keywordtype">string</span>& mmFlag)
<a name="l00370"></a>00370 : d_cm(cm), d_rules(rules), d_disableGC(false), d_postponeGC(false) {
<a name="l00371"></a>00371 <span class="keywordflow">if</span>(mmFlag == <span class="stringliteral">"chunks"</span>)
<a name="l00372"></a>00372 <a class="code" href="classCVC3_1_1VariableManager.html#a19ff37ae7bc9f7e807cd66aa8e5f18f4">d_mm</a> = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1MemoryManagerChunks.html">MemoryManagerChunks</a>(<span class="keyword">sizeof</span>(<a class="code" href="classCVC3_1_1VariableValue.html">VariableValue</a>));
<a name="l00373"></a>00373 <span class="keywordflow">else</span>
<a name="l00374"></a>00374 <a class="code" href="classCVC3_1_1VariableManager.html#a19ff37ae7bc9f7e807cd66aa8e5f18f4">d_mm</a> = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1MemoryManagerMalloc.html">MemoryManagerMalloc</a>();
<a name="l00375"></a>00375
<a name="l00376"></a>00376 <a class="code" href="classCVC3_1_1VariableManager.html#a17f4827ea92ce6e1ad0a1d5fa5726146">d_notifyObj</a> = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1VariableManagerNotifyObj.html" title="Notifies VariableManager before and after each pop()">VariableManagerNotifyObj</a>(<span class="keyword">this</span>, <a class="code" href="classCVC3_1_1VariableManager.html#aa9a63ca44ee29e3e11b843abf64680fd">d_cm</a>-><a class="code" href="classCVC3_1_1ContextManager.html#a66a7d900301c1459de90b048623d9297">getCurrentContext</a>());
<a name="l00377"></a>00377 }
<a name="l00378"></a>00378
<a name="l00379"></a>00379 <span class="comment">// Destructor</span>
<a name="l00380"></a><a class="code" href="classCVC3_1_1VariableManager.html#a321959b4af5952884d5215ca1eeb3bcc">00380</a> <a class="code" href="classCVC3_1_1VariableManager.html#a321959b4af5952884d5215ca1eeb3bcc">VariableManager::~VariableManager</a>() {
<a name="l00381"></a>00381 <span class="keyword">delete</span> <a class="code" href="classCVC3_1_1VariableManager.html#a17f4827ea92ce6e1ad0a1d5fa5726146">d_notifyObj</a>;
<a name="l00382"></a>00382 <span class="comment">// Delete the remaining variables</span>
<a name="l00383"></a>00383 <a class="code" href="classCVC3_1_1VariableManager.html#a87d086a76555966bb4e6f62b9e32bbac" title="Disable the garbage collection.">d_disableGC</a> = <span class="keyword">true</span>;
<a name="l00384"></a>00384 vector<VariableValue*> vars;
<a name="l00385"></a>00385 <span class="keywordflow">for</span>(<a class="code" href="classHash_1_1hash__set.html#a87a125f71dd85de65e662559bd5a66dc">VariableValueSet::iterator</a> i=<a class="code" href="classCVC3_1_1VariableManager.html#aeebf5ed3c88627c0b43f61c4f1ba42e5">d_varSet</a>.<a class="code" href="classHash_1_1hash__set.html#a69de75543eb1e9fa3510bb5090ad61a6" title="iterators">begin</a>(), iend=<a class="code" href="classCVC3_1_1VariableManager.html#aeebf5ed3c88627c0b43f61c4f1ba42e5">d_varSet</a>.<a class="code" href="classHash_1_1hash__set.html#ae3ee82665499970f29a93df9948a5757">end</a>();
<a name="l00386"></a>00386 i!=iend; ++i) {
<a name="l00387"></a>00387 vars.push_back(*i);
<a name="l00388"></a>00388 <span class="comment">// delete(*i);</span>
<a name="l00389"></a>00389 <span class="comment">// No need to free memory; we'll delete the entire d_mm</span>
<a name="l00390"></a>00390 <span class="comment">// d_mm->deleteData(*i);</span>
<a name="l00391"></a>00391 }
<a name="l00392"></a>00392 <a class="code" href="classCVC3_1_1VariableManager.html#aeebf5ed3c88627c0b43f61c4f1ba42e5">d_varSet</a>.<a class="code" href="classHash_1_1hash__set.html#a2d699de2bb0dac0d1ea819fdc8acda96">clear</a>();
<a name="l00393"></a>00393 <span class="keywordflow">for</span>(vector<VariableValue*>::iterator i=vars.begin(), iend=vars.end();
<a name="l00394"></a>00394 i!=iend; ++i) <span class="keyword">delete</span> *i;
<a name="l00395"></a>00395 <span class="keyword">delete</span> <a class="code" href="classCVC3_1_1VariableManager.html#a19ff37ae7bc9f7e807cd66aa8e5f18f4">d_mm</a>;
<a name="l00396"></a>00396 }
<a name="l00397"></a>00397
<a name="l00398"></a>00398 <span class="comment">// Garbage collect VariableValue pointer</span>
<a name="l00399"></a>00399 <span class="keywordtype">void</span>
<a name="l00400"></a><a class="code" href="classCVC3_1_1VariableManager.html#a5f35575560aac2140e817aa49190894d">00400</a> <a class="code" href="classCVC3_1_1VariableManager.html#a5f35575560aac2140e817aa49190894d" title="Garbage collect VariableValue pointer.">VariableManager::gc</a>(<a class="code" href="classCVC3_1_1VariableValue.html">VariableValue</a>* v) {
<a name="l00401"></a>00401 <span class="keywordflow">if</span>(!<a class="code" href="classCVC3_1_1VariableManager.html#a87d086a76555966bb4e6f62b9e32bbac" title="Disable the garbage collection.">d_disableGC</a>) {
<a name="l00402"></a>00402 <a class="code" href="classCVC3_1_1VariableManager.html#aeebf5ed3c88627c0b43f61c4f1ba42e5">d_varSet</a>.<a class="code" href="classHash_1_1hash__set.html#a82dbe044048d8e25f0ffd148d726d1e4">erase</a>(v);
<a name="l00403"></a>00403 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1VariableManager.html#adcdbfcae4aa2f069cfcb15d9b308b727" title="Postpone garbage collection.">d_postponeGC</a>) <a class="code" href="classCVC3_1_1VariableManager.html#af71a9d9933957edede81db48be5da5a3" title="Vector of variables to be deleted (postponed during pop())">d_deleted</a>.push_back(v);
<a name="l00404"></a>00404 <span class="keywordflow">else</span> {
<a name="l00405"></a>00405 <span class="keyword">delete</span> v;
<a name="l00406"></a>00406 <a class="code" href="classCVC3_1_1VariableManager.html#a19ff37ae7bc9f7e807cd66aa8e5f18f4">d_mm</a>-><a class="code" href="classCVC3_1_1MemoryManager.html#ad29fac88d3a07566d9a8f9dc8d8e059c">deleteData</a>(v);
<a name="l00407"></a>00407 }
<a name="l00408"></a>00408 }
<a name="l00409"></a>00409 }
<a name="l00410"></a>00410
<a name="l00411"></a>00411
<a name="l00412"></a>00412 <span class="keywordtype">void</span>
<a name="l00413"></a><a class="code" href="classCVC3_1_1VariableManager.html#ad7d360514fcfd910668eabd097dbe81c">00413</a> <a class="code" href="classCVC3_1_1VariableManager.html#ad7d360514fcfd910668eabd097dbe81c" title="Resume garbage collection.">VariableManager::resumeGC</a>() {
<a name="l00414"></a>00414 <a class="code" href="classCVC3_1_1VariableManager.html#adcdbfcae4aa2f069cfcb15d9b308b727" title="Postpone garbage collection.">d_postponeGC</a> = <span class="keyword">false</span>;
<a name="l00415"></a>00415 <span class="keywordflow">while</span>(<a class="code" href="classCVC3_1_1VariableManager.html#af71a9d9933957edede81db48be5da5a3" title="Vector of variables to be deleted (postponed during pop())">d_deleted</a>.size() > 0) {
<a name="l00416"></a>00416 <a class="code" href="classCVC3_1_1VariableValue.html">VariableValue</a>* v = <a class="code" href="classCVC3_1_1VariableManager.html#af71a9d9933957edede81db48be5da5a3" title="Vector of variables to be deleted (postponed during pop())">d_deleted</a>.back();
<a name="l00417"></a>00417 <a class="code" href="classCVC3_1_1VariableManager.html#af71a9d9933957edede81db48be5da5a3" title="Vector of variables to be deleted (postponed during pop())">d_deleted</a>.pop_back();
<a name="l00418"></a>00418 <span class="keyword">delete</span> v;
<a name="l00419"></a>00419 <a class="code" href="classCVC3_1_1VariableManager.html#a19ff37ae7bc9f7e807cd66aa8e5f18f4">d_mm</a>-><a class="code" href="classCVC3_1_1MemoryManager.html#ad29fac88d3a07566d9a8f9dc8d8e059c">deleteData</a>(v);
<a name="l00420"></a>00420 }
<a name="l00421"></a>00421 }
<a name="l00422"></a>00422
<a name="l00423"></a>00423 } <span class="comment">// end of namespace CVC3</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>
