<!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: theorem_value.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">theorem_value.h</div> </div>
</div>
<div class="contents">
<a href="theorem__value_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 theorem_value.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: Dec 10 01:03:34 GMT 2002</span>
<a name="l00008"></a>00008 <span class="comment"> *</span>
<a name="l00009"></a>00009 <span class="comment"> * <hr></span>
<a name="l00010"></a>00010 <span class="comment"> *</span>
<a name="l00011"></a>00011 <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span>
<a name="l00012"></a>00012 <span class="comment"> * and its documentation for any purpose is hereby granted without</span>
<a name="l00013"></a>00013 <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span>
<a name="l00014"></a>00014 <span class="comment"> * LICENSE file provided with this distribution.</span>
<a name="l00015"></a>00015 <span class="comment"> * </span>
<a name="l00016"></a>00016 <span class="comment"> * <hr></span>
<a name="l00017"></a>00017 <span class="comment"> * </span>
<a name="l00018"></a>00018 <span class="comment"> */</span>
<a name="l00019"></a>00019 <span class="comment">/*****************************************************************************/</span>
<a name="l00020"></a>00020 <span class="comment">// CLASS: TheoremValue</span>
<a name="l00021"></a>00021 <span class="comment">//</span>
<a name="l00022"></a>00022 <span class="comment">// AUTHOR: Sergey Berezin, 07/05/02</span>
<a name="l00023"></a>00023 <span class="comment">//</span>
<a name="l00024"></a>00024 <span class="comment">// Abstract:</span>
<a name="l00025"></a>00025 <span class="comment">//</span>
<a name="l00026"></a>00026 <span class="comment">// A class representing a proven fact in CVC. It stores the theorem</span>
<a name="l00027"></a>00027 <span class="comment">// as a CVC expression, and in the appropriate modes also the set of</span>
<a name="l00028"></a>00028 <span class="comment">// assumptions and the proof.</span>
<a name="l00029"></a>00029 <span class="comment">//</span>
<a name="l00030"></a>00030 <span class="comment">// The idea is to allow only a few trusted classes to create values of</span>
<a name="l00031"></a>00031 <span class="comment">// this class. If all the critical computations in the decision</span>
<a name="l00032"></a>00032 <span class="comment">// procedures are done through the use of Theorems, then soundness of</span>
<a name="l00033"></a>00033 <span class="comment">// these decision procedures will rely only on the soundness of the</span>
<a name="l00034"></a>00034 <span class="comment">// methods in the trusted classes (the inference rules).</span>
<a name="l00035"></a>00035 <span class="comment">//</span>
<a name="l00036"></a>00036 <span class="comment">// Thus, proof checking can effectively be done at run-time on the</span>
<a name="l00037"></a>00037 <span class="comment">// fly. Or the soundness may be potentially proven by static analysis</span>
<a name="l00038"></a>00038 <span class="comment">// and many run-time checks can then be optimized away.</span>
<a name="l00039"></a>00039 <span class="comment">//</span>
<a name="l00040"></a>00040 <span class="comment">// This theorem_value.h file should NOT be used by the decision</span>
<a name="l00041"></a>00041 <span class="comment">// procedures. Use theorem.h instead.</span>
<a name="l00042"></a>00042 <span class="comment">//</span><span class="comment"></span>
<a name="l00043"></a>00043 <span class="comment">////////////////////////////////////////////////////////////////////////</span>
<a name="l00044"></a>00044 <span class="comment"></span>
<a name="l00045"></a>00045 <span class="preprocessor">#ifndef _cvc3__theorem_value_h_</span>
<a name="l00046"></a>00046 <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__theorem_value_h_</span>
<a name="l00047"></a>00047 <span class="preprocessor"></span>
<a name="l00048"></a>00048 <span class="preprocessor">#include "<a class="code" href="assumptions_8h.html">assumptions.h</a>"</span>
<a name="l00049"></a>00049 <span class="preprocessor">#include "<a class="code" href="theorem__manager_8h.html">theorem_manager.h</a>"</span>
<a name="l00050"></a>00050 <span class="comment">//#include "theory_core.h"</span>
<a name="l00051"></a>00051 <span class="comment">//#include "vcl.h"</span>
<a name="l00052"></a>00052
<a name="l00053"></a>00053 <span class="keyword">namespace </span>CVC3 {
<a name="l00054"></a>00054
<a name="l00055"></a>00055 <span class="comment">//extern VCL* myvcl; </span>
<a name="l00056"></a><a class="code" href="classCVC3_1_1TheoremValue.html">00056</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1TheoremValue.html">TheoremValue</a>
<a name="l00057"></a>00057 {
<a name="l00058"></a>00058 <span class="comment">// These are the only classes that can create new TheoremValue classes</span>
<a name="l00059"></a><a class="code" href="classCVC3_1_1TheoremValue.html#a51f48d7e14c97707595cfe5f8f6df209">00059</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>;
<a name="l00060"></a><a class="code" href="classCVC3_1_1TheoremValue.html#a2fc7fcb35dcb6d97f101ffb632ac1dcd">00060</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1RegTheoremValue.html">RegTheoremValue</a>;
<a name="l00061"></a><a class="code" href="classCVC3_1_1TheoremValue.html#add1e5fec863ffafbd22cac7aa0d1b689">00061</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1RWTheoremValue.html">RWTheoremValue</a>;
<a name="l00062"></a>00062
<a name="l00063"></a>00063 <span class="keyword">protected</span>:<span class="comment"></span>
<a name="l00064"></a>00064 <span class="comment"> //! Theorem Manager</span>
<a name="l00065"></a><a class="code" href="classCVC3_1_1TheoremValue.html#af0167eefead6921ed3919808bc0f9845">00065</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1TheoremManager.html">TheoremManager</a>* <a class="code" href="classCVC3_1_1TheoremValue.html#af0167eefead6921ed3919808bc0f9845" title="Theorem Manager.">d_tm</a>;
<a name="l00066"></a>00066 <span class="comment"></span>
<a name="l00067"></a>00067 <span class="comment"> //! The expression representing a theorem</span>
<a name="l00068"></a><a class="code" href="classCVC3_1_1TheoremValue.html#a702623ca8da01e55a811e573a82fd0e4">00068</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoremValue.html#a702623ca8da01e55a811e573a82fd0e4" title="The expression representing a theorem.">d_thm</a>;
<a name="l00069"></a>00069 <span class="comment"></span>
<a name="l00070"></a>00070 <span class="comment"> //! Proof of the theorem</span>
<a name="l00071"></a><a class="code" href="classCVC3_1_1TheoremValue.html#a5cf31c613884270c10170d87ff58817b">00071</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1Proof.html">Proof</a> <a class="code" href="classCVC3_1_1TheoremValue.html#a5cf31c613884270c10170d87ff58817b" title="Proof of the theorem.">d_proof</a>;
<a name="l00072"></a>00072 <span class="comment"></span>
<a name="l00073"></a>00073 <span class="comment"> //! How many pointers to this theorem value</span>
<a name="l00074"></a><a class="code" href="classCVC3_1_1TheoremValue.html#a138c67c7a778d8e0d525a658439f105c">00074</a> <span class="comment"></span> <span class="keywordtype">unsigned</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a138c67c7a778d8e0d525a658439f105c" title="How many pointers to this theorem value.">d_refcount</a>;
<a name="l00075"></a>00075 <span class="comment"></span>
<a name="l00076"></a>00076 <span class="comment"> //! Largest scope level of the assumptions</span>
<a name="l00077"></a><a class="code" href="classCVC3_1_1TheoremValue.html#a44a5fb4e3e9d28ee1d32c2fa61e05d15">00077</a> <span class="comment"></span> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a44a5fb4e3e9d28ee1d32c2fa61e05d15" title="Largest scope level of the assumptions.">d_scopeLevel</a>;
<a name="l00078"></a>00078 <span class="comment"></span>
<a name="l00079"></a>00079 <span class="comment"> //! Quantification level of this theorem</span>
<a name="l00080"></a><a class="code" href="classCVC3_1_1TheoremValue.html#a819e06a02c53175bf33d4d475bd15d09">00080</a> <span class="comment"></span> <span class="keywordtype">unsigned</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a819e06a02c53175bf33d4d475bd15d09" title="Quantification level of this theorem.">d_quantLevel</a>;
<a name="l00081"></a>00081
<a name="l00082"></a>00082 <span class="comment"></span>
<a name="l00083"></a>00083 <span class="comment"> //! debug quantlevel, this one is from proof, not from assumption list</span>
<a name="l00084"></a>00084 <span class="comment"></span> <span class="comment">// unsigned d_quantLevelDebug;</span>
<a name="l00085"></a>00085 <span class="comment"></span>
<a name="l00086"></a>00086 <span class="comment"> //! Temporary flag used during traversals</span>
<a name="l00087"></a><a class="code" href="classCVC3_1_1TheoremValue.html#a1cec81e358483c5459d125eed27c5edf">00087</a> <span class="comment"></span> <span class="keywordtype">unsigned</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a1cec81e358483c5459d125eed27c5edf" title="debug quantlevel, this one is from proof, not from assumption list">d_flag</a>;
<a name="l00088"></a>00088 <span class="comment"></span>
<a name="l00089"></a>00089 <span class="comment"> //! Temporary cache used during traversals</span>
<a name="l00090"></a><a class="code" href="classCVC3_1_1TheoremValue.html#ae5df8e7dcf6660844d291e512b66516d">00090</a> <span class="comment"></span> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoremValue.html#ae5df8e7dcf6660844d291e512b66516d" title="Temporary cache used during traversals.">d_cachedValue</a> : 28;
<a name="l00091"></a>00091
<a name="l00092"></a><a class="code" href="classCVC3_1_1TheoremValue.html#aa2eb4713aae1ff702316707578757b7d">00092</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoremValue.html#aa2eb4713aae1ff702316707578757b7d" title="whether this theorem was generated by substitution">d_isSubst</a> : 1; <span class="comment">//!< whether this theorem was generated by substitution</span>
<a name="l00093"></a><a class="code" href="classCVC3_1_1TheoremValue.html#aac23fbc1ab6d8e32c7dc13bb11c7884d">00093</a> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoremValue.html#aac23fbc1ab6d8e32c7dc13bb11c7884d">d_isAssump</a> : 1;
<a name="l00094"></a><a class="code" href="classCVC3_1_1TheoremValue.html#a74965c0ce02cfba99305eae7fa267ffe">00094</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a74965c0ce02cfba99305eae7fa267ffe" title="whether it should this be expanded in graph traversal">d_expand</a> : 1; <span class="comment">//!< whether it should this be expanded in graph traversal</span>
<a name="l00095"></a><a class="code" href="classCVC3_1_1TheoremValue.html#a376edd9ad7538621cc0fa2c07017c025">00095</a> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a376edd9ad7538621cc0fa2c07017c025" title="whether it belongs to the conflict clause">d_clauselit</a> : 1; <span class="comment">//!< whether it belongs to the conflict clause</span>
<a name="l00096"></a>00096 <span class="comment"></span>
<a name="l00097"></a>00097
<a name="l00098"></a>00098 <span class="keyword">private</span>:
<a name="l00099"></a>00099 <span class="comment">// Constructor. </span><span class="comment"></span>
<a name="l00100"></a>00100 <span class="comment"> /*!</span>
<a name="l00101"></a>00101 <span class="comment"> * NOTE: it is private; only friend classes can call it.</span>
<a name="l00102"></a>00102 <span class="comment"> *</span>
<a name="l00103"></a>00103 <span class="comment"> * If the assumptions refer to only one theorem, grab the</span>
<a name="l00104"></a>00104 <span class="comment"> * assumptions of that theorem instead.</span>
<a name="l00105"></a>00105 <span class="comment"> */</span>
<a name="l00106"></a>00106
<a name="l00107"></a>00107 <span class="comment">//by yeting, we should do something to catch theorems created with empty assumptions.</span>
<a name="l00108"></a>00108 <span class="comment">//one way is to set the d_quantLevel 999 here. </span>
<a name="l00109"></a>00109
<a name="l00110"></a><a class="code" href="classCVC3_1_1TheoremValue.html#a159a1ef9a2ff876cf9d31704ed23f816">00110</a> <a class="code" href="classCVC3_1_1TheoremValue.html#a159a1ef9a2ff876cf9d31704ed23f816">TheoremValue</a>(<a class="code" href="classCVC3_1_1TheoremManager.html">TheoremManager</a>* tm, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> &thm,
<a name="l00111"></a>00111 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Proof.html">Proof</a>& pf, <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoremValue.html#aaaabd2fab47103f9a4574c380c790a11">isAssump</a>) :
<a name="l00112"></a>00112 <a class="code" href="classCVC3_1_1TheoremValue.html#af0167eefead6921ed3919808bc0f9845" title="Theorem Manager.">d_tm</a>(tm), <a class="code" href="classCVC3_1_1TheoremValue.html#a702623ca8da01e55a811e573a82fd0e4" title="The expression representing a theorem.">d_thm</a>(thm), <a class="code" href="classCVC3_1_1TheoremValue.html#a5cf31c613884270c10170d87ff58817b" title="Proof of the theorem.">d_proof</a>(pf), <a class="code" href="classCVC3_1_1TheoremValue.html#a138c67c7a778d8e0d525a658439f105c" title="How many pointers to this theorem value.">d_refcount</a>(0),
<a name="l00113"></a>00113 <a class="code" href="classCVC3_1_1TheoremValue.html#a44a5fb4e3e9d28ee1d32c2fa61e05d15" title="Largest scope level of the assumptions.">d_scopeLevel</a>(0), <a class="code" href="classCVC3_1_1TheoremValue.html#a819e06a02c53175bf33d4d475bd15d09" title="Quantification level of this theorem.">d_quantLevel</a>(0), <a class="code" href="classCVC3_1_1TheoremValue.html#a1cec81e358483c5459d125eed27c5edf" title="debug quantlevel, this one is from proof, not from assumption list">d_flag</a>(0), <a class="code" href="classCVC3_1_1TheoremValue.html#ae5df8e7dcf6660844d291e512b66516d" title="Temporary cache used during traversals.">d_cachedValue</a>(0),
<a name="l00114"></a>00114 <a class="code" href="classCVC3_1_1TheoremValue.html#aa2eb4713aae1ff702316707578757b7d" title="whether this theorem was generated by substitution">d_isSubst</a>(0), <a class="code" href="classCVC3_1_1TheoremValue.html#aac23fbc1ab6d8e32c7dc13bb11c7884d">d_isAssump</a>(isAssump), <a class="code" href="classCVC3_1_1TheoremValue.html#a74965c0ce02cfba99305eae7fa267ffe" title="whether it should this be expanded in graph traversal">d_expand</a>(0), <a class="code" href="classCVC3_1_1TheoremValue.html#a376edd9ad7538621cc0fa2c07017c025" title="whether it belongs to the conflict clause">d_clauselit</a>(0) {}
<a name="l00115"></a>00115
<a name="l00116"></a>00116 <span class="comment">// Disable copy constructor and assignment</span>
<a name="l00117"></a><a class="code" href="classCVC3_1_1TheoremValue.html#ada947e18738c40ed80eb8b2e4fff499b">00117</a> <a class="code" href="classCVC3_1_1TheoremValue.html#ada947e18738c40ed80eb8b2e4fff499b">TheoremValue</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoremValue.html">TheoremValue</a>& t) {
<a name="l00118"></a>00118 <a class="code" href="debug_8h.html#a2637b2fffa22e3c9fad40cda8fcc3bce" title="If something goes horribly wrong, print a message and abort immediately with exit(1).">FatalAssert</a>(<span class="keyword">false</span>, <span class="stringliteral">"TheoremValue() copy constructor called"</span>);
<a name="l00119"></a>00119 }
<a name="l00120"></a><a class="code" href="classCVC3_1_1TheoremValue.html#a217ca4cd1244901bded79a8a8be2692a">00120</a> <a class="code" href="classCVC3_1_1TheoremValue.html">TheoremValue</a>& <a class="code" href="classCVC3_1_1TheoremValue.html#a217ca4cd1244901bded79a8a8be2692a">operator=</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoremValue.html">TheoremValue</a>& t) {
<a name="l00121"></a>00121 <a class="code" href="debug_8h.html#a2637b2fffa22e3c9fad40cda8fcc3bce" title="If something goes horribly wrong, print a message and abort immediately with exit(1).">FatalAssert</a>(<span class="keyword">false</span>, <span class="stringliteral">"TheoremValue assignment operator called"</span>);
<a name="l00122"></a>00122 <span class="keywordflow">return</span> *<span class="keyword">this</span>;
<a name="l00123"></a>00123 }
<a name="l00124"></a>00124
<a name="l00125"></a><a class="code" href="classCVC3_1_1TheoremValue.html#a1b91df4037f8888079646e7aefe174a2">00125</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a1b91df4037f8888079646e7aefe174a2">isFlagged</a>()<span class="keyword"> const </span>{
<a name="l00126"></a>00126 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a1cec81e358483c5459d125eed27c5edf" title="debug quantlevel, this one is from proof, not from assumption list">d_flag</a> == <a class="code" href="classCVC3_1_1TheoremValue.html#af0167eefead6921ed3919808bc0f9845" title="Theorem Manager.">d_tm</a>-><a class="code" href="classCVC3_1_1TheoremManager.html#a146426ed876d276baeeb2b50a9bd7b4b">getFlag</a>();
<a name="l00127"></a>00127 }
<a name="l00128"></a>00128
<a name="l00129"></a><a class="code" href="classCVC3_1_1TheoremValue.html#ace65848828d3d96490a45a52ff7f8f73">00129</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoremValue.html#ace65848828d3d96490a45a52ff7f8f73">clearAllFlags</a>() {
<a name="l00130"></a>00130 <a class="code" href="classCVC3_1_1TheoremValue.html#af0167eefead6921ed3919808bc0f9845" title="Theorem Manager.">d_tm</a>-><a class="code" href="classCVC3_1_1TheoremManager.html#a53386d08efa4d0f18524129b3d653bef">clearAllFlags</a>();
<a name="l00131"></a>00131 }
<a name="l00132"></a>00132
<a name="l00133"></a><a class="code" href="classCVC3_1_1TheoremValue.html#aee29e499025f39a5b04b610dee9dae0c">00133</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoremValue.html#aee29e499025f39a5b04b610dee9dae0c">setFlag</a>() {
<a name="l00134"></a>00134 <a class="code" href="classCVC3_1_1TheoremValue.html#a1cec81e358483c5459d125eed27c5edf" title="debug quantlevel, this one is from proof, not from assumption list">d_flag</a> = <a class="code" href="classCVC3_1_1TheoremValue.html#af0167eefead6921ed3919808bc0f9845" title="Theorem Manager.">d_tm</a>-><a class="code" href="classCVC3_1_1TheoremManager.html#a146426ed876d276baeeb2b50a9bd7b4b">getFlag</a>();
<a name="l00135"></a>00135 }
<a name="l00136"></a>00136
<a name="l00137"></a><a class="code" href="classCVC3_1_1TheoremValue.html#a9d2d00b50cf9eb8f5378cb8d289a412c">00137</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a9d2d00b50cf9eb8f5378cb8d289a412c">setCachedValue</a>(<span class="keywordtype">int</span> value) {
<a name="l00138"></a>00138 <a class="code" href="classCVC3_1_1TheoremValue.html#ae5df8e7dcf6660844d291e512b66516d" title="Temporary cache used during traversals.">d_cachedValue</a> = value;
<a name="l00139"></a>00139 }
<a name="l00140"></a>00140
<a name="l00141"></a><a class="code" href="classCVC3_1_1TheoremValue.html#a223a1c591286bee75524a573bc87518e">00141</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a223a1c591286bee75524a573bc87518e">getCachedValue</a>()<span class="keyword"> const </span>{
<a name="l00142"></a>00142 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremValue.html#ae5df8e7dcf6660844d291e512b66516d" title="Temporary cache used during traversals.">d_cachedValue</a>;
<a name="l00143"></a>00143 }
<a name="l00144"></a>00144
<a name="l00145"></a><a class="code" href="classCVC3_1_1TheoremValue.html#a31762e3d339154a150064b0e91c6497d">00145</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a31762e3d339154a150064b0e91c6497d">setSubst</a>() { <a class="code" href="classCVC3_1_1TheoremValue.html#aa2eb4713aae1ff702316707578757b7d" title="whether this theorem was generated by substitution">d_isSubst</a> = <span class="keyword">true</span>; }
<a name="l00146"></a><a class="code" href="classCVC3_1_1TheoremValue.html#a7bc742af6a03964e8c4d9fc876426e5e">00146</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a7bc742af6a03964e8c4d9fc876426e5e">isSubst</a>() { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremValue.html#aa2eb4713aae1ff702316707578757b7d" title="whether this theorem was generated by substitution">d_isSubst</a>; }
<a name="l00147"></a>00147
<a name="l00148"></a><a class="code" href="classCVC3_1_1TheoremValue.html#a67f5136c43e385f2398841f8ad94d18a">00148</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a67f5136c43e385f2398841f8ad94d18a">setExpandFlag</a>(<span class="keywordtype">bool</span> val) {
<a name="l00149"></a>00149 <a class="code" href="classCVC3_1_1TheoremValue.html#a74965c0ce02cfba99305eae7fa267ffe" title="whether it should this be expanded in graph traversal">d_expand</a> = val;
<a name="l00150"></a>00150 }
<a name="l00151"></a>00151
<a name="l00152"></a><a class="code" href="classCVC3_1_1TheoremValue.html#ae88fe39382cb64565b4a30a0ad170797">00152</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoremValue.html#ae88fe39382cb64565b4a30a0ad170797">getExpandFlag</a>() {
<a name="l00153"></a>00153 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a74965c0ce02cfba99305eae7fa267ffe" title="whether it should this be expanded in graph traversal">d_expand</a>;
<a name="l00154"></a>00154 }
<a name="l00155"></a>00155
<a name="l00156"></a><a class="code" href="classCVC3_1_1TheoremValue.html#ae9091cd1e351cd1e00f9f57e286e1414">00156</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoremValue.html#ae9091cd1e351cd1e00f9f57e286e1414">setLitFlag</a>(<span class="keywordtype">bool</span> val) {
<a name="l00157"></a>00157 <a class="code" href="classCVC3_1_1TheoremValue.html#a376edd9ad7538621cc0fa2c07017c025" title="whether it belongs to the conflict clause">d_clauselit</a> = val;
<a name="l00158"></a>00158 }
<a name="l00159"></a>00159
<a name="l00160"></a><a class="code" href="classCVC3_1_1TheoremValue.html#a74e6ab319ca0b6945ae472ba30698aae">00160</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a74e6ab319ca0b6945ae472ba30698aae">getLitFlag</a>() {
<a name="l00161"></a>00161 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a376edd9ad7538621cc0fa2c07017c025" title="whether it belongs to the conflict clause">d_clauselit</a>;
<a name="l00162"></a>00162 }
<a name="l00163"></a>00163
<a name="l00164"></a><a class="code" href="classCVC3_1_1TheoremValue.html#a9c11008cb459d81b618c10913057435c">00164</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a9c11008cb459d81b618c10913057435c">getScope</a>() {
<a name="l00165"></a>00165 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a44a5fb4e3e9d28ee1d32c2fa61e05d15" title="Largest scope level of the assumptions.">d_scopeLevel</a>;
<a name="l00166"></a>00166 }
<a name="l00167"></a>00167
<a name="l00168"></a><a class="code" href="classCVC3_1_1TheoremValue.html#a5548a7ad205c1fee8fa49309d865cf44">00168</a> <span class="keywordtype">unsigned</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a5548a7ad205c1fee8fa49309d865cf44">getQuantLevel</a>() { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a819e06a02c53175bf33d4d475bd15d09" title="Quantification level of this theorem.">d_quantLevel</a>; }
<a name="l00169"></a>00169
<a name="l00170"></a><a class="code" href="classCVC3_1_1TheoremValue.html#ae091d4527d043cdf0bd83ba56ab98ca3">00170</a> <span class="keywordtype">unsigned</span> <a class="code" href="classCVC3_1_1TheoremValue.html#ae091d4527d043cdf0bd83ba56ab98ca3">getQuantLevelDebug</a>() {
<a name="l00171"></a>00171 <span class="keywordflow">return</span> 0;
<a name="l00172"></a>00172 <span class="comment">// return d_quantLevelDebug; </span>
<a name="l00173"></a>00173 }
<a name="l00174"></a>00174
<a name="l00175"></a><a class="code" href="classCVC3_1_1TheoremValue.html#a4a305d7049aab9528a6205250303c574">00175</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a4a305d7049aab9528a6205250303c574">setQuantLevel</a>(<span class="keywordtype">unsigned</span> level) { <a class="code" href="classCVC3_1_1TheoremValue.html#a819e06a02c53175bf33d4d475bd15d09" title="Quantification level of this theorem.">d_quantLevel</a> = level; }
<a name="l00176"></a>00176
<a name="l00177"></a><a class="code" href="classCVC3_1_1TheoremValue.html#aa437b081740be2d064d8d71e1db90d04">00177</a> <span class="keywordtype">unsigned</span> <a class="code" href="classCVC3_1_1TheoremValue.html#aa437b081740be2d064d8d71e1db90d04">recQuantLevel</a>(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> proof){
<a name="l00178"></a>00178 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a819e06a02c53175bf33d4d475bd15d09" title="Quantification level of this theorem.">d_quantLevel</a>;
<a name="l00179"></a>00179 <span class="comment">/*</span>
<a name="l00180"></a>00180 <span class="comment"> if( ! proof.isNull()){</span>
<a name="l00181"></a>00181 <span class="comment"> // std::cout << "debug level " << proof << std::endl;;</span>
<a name="l00182"></a>00182 <span class="comment"> }</span>
<a name="l00183"></a>00183 <span class="comment"> else {</span>
<a name="l00184"></a>00184 <span class="comment"> // std::cout << "proof null" << proof << std::endl;;</span>
<a name="l00185"></a>00185 <span class="comment"> }</span>
<a name="l00186"></a>00186 <span class="comment"> </span>
<a name="l00187"></a>00187 <span class="comment"> unsigned nch = proof.arity();</span>
<a name="l00188"></a>00188 <span class="comment"> unsigned level(0);</span>
<a name="l00189"></a>00189 <span class="comment"> if (proof.getKind() == PF_APPLY){</span>
<a name="l00190"></a>00190 <span class="comment"> for (unsigned i = 1 ; i < nch ; i++){</span>
<a name="l00191"></a>00191 <span class="comment"> if ((proof[i]).getKind() == PF_APPLY || proof[i].getKind() == LAMBDA || proof[i].isVar()) {</span>
<a name="l00192"></a>00192 <span class="comment"> if(proof[i].isVar()){</span>
<a name="l00193"></a>00193 <span class="comment"> // std::cout << "found var in pf # " << proof << std::endl;</span>
<a name="l00194"></a>00194 <span class="comment"> }</span>
<a name="l00195"></a>00195 <span class="comment"> unsigned chLevel = recQuantLevel(proof[i]);</span>
<a name="l00196"></a>00196 <span class="comment"> level = chLevel > level ? chLevel : level ;</span>
<a name="l00197"></a>00197 <span class="comment"> }</span>
<a name="l00198"></a>00198 <span class="comment"> }</span>
<a name="l00199"></a>00199 <span class="comment"> if(proof[0].getName() == "universal_elimination"){</span>
<a name="l00200"></a>00200 <span class="comment"> level++;</span>
<a name="l00201"></a>00201 <span class="comment"> unsigned gtermLevel = myvcl->core()->getQuantLevelForTerm(proof[4]);</span>
<a name="l00202"></a>00202 <span class="comment"> if((gtermLevel + 1) > level ){</span>
<a name="l00203"></a>00203 <span class="comment"> level = gtermLevel+1;</span>
<a name="l00204"></a>00204 <span class="comment"> }</span>
<a name="l00205"></a>00205 <span class="comment"> // std::cout << "level " << level << std::endl;</span>
<a name="l00206"></a>00206 <span class="comment"> }</span>
<a name="l00207"></a>00207 <span class="comment"> else {</span>
<a name="l00208"></a>00208 <span class="comment"> // std::cout << "proof name non-inst" << proof[0].getName() << std::endl;</span>
<a name="l00209"></a>00209 <span class="comment"> }</span>
<a name="l00210"></a>00210 <span class="comment"> // std::cout << "get level " << d_thm << std::endl;</span>
<a name="l00211"></a>00211 <span class="comment"> // std::cout << "get level " << level << std::endl;</span>
<a name="l00212"></a>00212 <span class="comment"> // std::cout << "get level " << proof << std::endl;</span>
<a name="l00213"></a>00213 <span class="comment"> return level; </span>
<a name="l00214"></a>00214 <span class="comment"> }</span>
<a name="l00215"></a>00215 <span class="comment"> else if (proof.getKind() == LAMBDA){</span>
<a name="l00216"></a>00216 <span class="comment"> std::cout << "lambda " << proof << std::endl;</span>
<a name="l00217"></a>00217 <span class="comment"> std::cout << "lambda body " << proof << std::endl;</span>
<a name="l00218"></a>00218 <span class="comment"> return recQuantLevel(proof.getBody());</span>
<a name="l00219"></a>00219 <span class="comment"> }</span>
<a name="l00220"></a>00220 <span class="comment"> else if (proof.isNull() ){</span>
<a name="l00221"></a>00221 <span class="comment"> // std::cout <<" error in get quantleveldebug " << std::endl;</span>
<a name="l00222"></a>00222 <span class="comment"> // std::cout << proof << std::endl;</span>
<a name="l00223"></a>00223 <span class="comment"> return 100000;</span>
<a name="l00224"></a>00224 <span class="comment"> } </span>
<a name="l00225"></a>00225 <span class="comment"> else if (proof.isVar()){</span>
<a name="l00226"></a>00226 <span class="comment"> if(proof.getType().getExpr().getType().isBool()){</span>
<a name="l00227"></a>00227 <span class="comment"> //std::cout << "var proof " << proof.getType().getExpr() << std::endl;</span>
<a name="l00228"></a>00228 <span class="comment"> // std::cout << "found proof var # " << proof << std::endl;</span>
<a name="l00229"></a>00229 <span class="comment"> // std::cout << proof.getType() << std::endl;</span>
<a name="l00230"></a>00230 <span class="comment"> // std::cout << "the quant level is " << myvcl->core()->getQuantLevelForTerm(proof.getType().getExpr()) << std::endl;</span>
<a name="l00231"></a>00231 <span class="comment"> return myvcl->core()->getQuantLevelForTerm(proof.getType().getExpr());</span>
<a name="l00232"></a>00232 <span class="comment"> }</span>
<a name="l00233"></a>00233 <span class="comment"> else{</span>
<a name="l00234"></a>00234 <span class="comment"> return 0;</span>
<a name="l00235"></a>00235 <span class="comment"> }</span>
<a name="l00236"></a>00236 <span class="comment"> }</span>
<a name="l00237"></a>00237 <span class="comment"> else{</span>
<a name="l00238"></a>00238 <span class="comment"> std::cout <<" error in get quantleveldebug " << std::endl;</span>
<a name="l00239"></a>00239 <span class="comment"> std::cout << proof << std::endl;</span>
<a name="l00240"></a>00240 <span class="comment"> std::cout << proof.isVar() << std::endl;</span>
<a name="l00241"></a>00241 <span class="comment"> return 200000;</span>
<a name="l00242"></a>00242 <span class="comment"> }</span>
<a name="l00243"></a>00243 <span class="comment"> return 0;</span>
<a name="l00244"></a>00244 <span class="comment"> */</span>
<a name="l00245"></a>00245 }
<a name="l00246"></a>00246
<a name="l00247"></a><a class="code" href="classCVC3_1_1TheoremValue.html#a8f33f1f21c512afeed47e16346dd168c">00247</a> <span class="keywordtype">unsigned</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a8f33f1f21c512afeed47e16346dd168c">findQuantLevelDebug</a>(){
<a name="l00248"></a>00248 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a819e06a02c53175bf33d4d475bd15d09" title="Quantification level of this theorem.">d_quantLevel</a>;
<a name="l00249"></a>00249 <span class="comment">/*</span>
<a name="l00250"></a>00250 <span class="comment"> Expr p (d_proof.getExpr());</span>
<a name="l00251"></a>00251 <span class="comment"> unsigned ret ; </span>
<a name="l00252"></a>00252 <span class="comment"> if (isAssump()){ </span>
<a name="l00253"></a>00253 <span class="comment"> if(d_thm.inUserAssumption()){</span>
<a name="l00254"></a>00254 <span class="comment"> ret = 0 ;</span>
<a name="l00255"></a>00255 <span class="comment"> // return 0;</span>
<a name="l00256"></a>00256 <span class="comment"> }</span>
<a name="l00257"></a>00257 <span class="comment"> else {</span>
<a name="l00258"></a>00258 <span class="comment"> // std::cout <<" why here " << std::endl;</span>
<a name="l00259"></a>00259 <span class="comment"> // std::cout << "the quant level is " << myvcl->core()->getQuantLevelForTerm(d_thm) << std::endl;</span>
<a name="l00260"></a>00260 <span class="comment"> // std::cout << d_thm << std::endl;</span>
<a name="l00261"></a>00261 <span class="comment"> // std::cout <<" == end of why here " << std::endl;</span>
<a name="l00262"></a>00262 <span class="comment"> ret = myvcl->core()->getQuantLevelForTerm(d_thm);</span>
<a name="l00263"></a>00263 <span class="comment"> // </span>
<a name="l00264"></a>00264 <span class="comment"> // return myvcl->core()->getQuantLevelForTerm(d_thm);</span>
<a name="l00265"></a>00265 <span class="comment"> }</span>
<a name="l00266"></a>00266 <span class="comment"> }</span>
<a name="l00267"></a>00267 <span class="comment"> else if (p.isVar()){</span>
<a name="l00268"></a>00268 <span class="comment"> unsigned level1 = myvcl->core()->getQuantLevelForTerm(p.getType().getExpr());</span>
<a name="l00269"></a>00269 <span class="comment"> unsigned level2 = d_quantLevel;</span>
<a name="l00270"></a>00270 <span class="comment"> if(level1 != level2){</span>
<a name="l00271"></a>00271 <span class="comment"> std::cout <<"not rq" << std::endl;</span>
<a name="l00272"></a>00272 <span class="comment"> }</span>
<a name="l00273"></a>00273 <span class="comment"> else{</span>
<a name="l00274"></a>00274 <span class="comment"> ret = level1;</span>
<a name="l00275"></a>00275 <span class="comment"> // return level1;</span>
<a name="l00276"></a>00276 <span class="comment"> }</span>
<a name="l00277"></a>00277 <span class="comment"> }</span>
<a name="l00278"></a>00278 <span class="comment"> else {</span>
<a name="l00279"></a>00279 <span class="comment"> ret = recQuantLevel(p);</span>
<a name="l00280"></a>00280 <span class="comment"> // return recQuantLevel(p);</span>
<a name="l00281"></a>00281 <span class="comment"> }</span>
<a name="l00282"></a>00282 <span class="comment"> // std::cout << " get -- begin with debug level " << ret << std::endl;</span>
<a name="l00283"></a>00283 <span class="comment"> // std::cout << " quant level " << d_quantLevel << std::endl;</span>
<a name="l00284"></a>00284 <span class="comment"> // std::cout << " get level thm " << d_thm << std::endl;</span>
<a name="l00285"></a>00285 <span class="comment"> // std::cout << " get level is var " << p.isVar() << std::endl;</span>
<a name="l00286"></a>00286 <span class="comment"> if(p.isVar()){</span>
<a name="l00287"></a>00287 <span class="comment"> // std::cout << "var proof " << p.getType().getExpr()<< std::endl;</span>
<a name="l00288"></a>00288 <span class="comment"> }</span>
<a name="l00289"></a>00289 <span class="comment"> return ret;</span>
<a name="l00290"></a>00290 <span class="comment"> */</span>
<a name="l00291"></a>00291 }
<a name="l00292"></a>00292
<a name="l00293"></a>00293
<a name="l00294"></a>00294 <span class="comment">// virtual bool isRewrite() const { return d_thm.isEq() || d_thm.isIff(); }</span>
<a name="l00295"></a><a class="code" href="classCVC3_1_1TheoremValue.html#a123ac5cf8dde8d8ba3ca7d47a7d9bfde">00295</a> <span class="keyword">virtual</span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a123ac5cf8dde8d8ba3ca7d47a7d9bfde">isRewrite</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <span class="keyword">false</span>; }
<a name="l00296"></a>00296
<a name="l00297"></a><a class="code" href="classCVC3_1_1TheoremValue.html#ada6a2145dda62e6d3bd6781c7ef96141">00297</a> <span class="keyword">virtual</span> <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_1TheoremValue.html#ada6a2145dda62e6d3bd6781c7ef96141">getExpr</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a702623ca8da01e55a811e573a82fd0e4" title="The expression representing a theorem.">d_thm</a>; }
<a name="l00298"></a><a class="code" href="classCVC3_1_1TheoremValue.html#a183c518edb1e346997882c5cce931fa3">00298</a> <span class="keyword">virtual</span> <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_1TheoremValue.html#a183c518edb1e346997882c5cce931fa3">getLHS</a>()<span class="keyword"> const </span>{
<a name="l00299"></a>00299 <span class="comment">// TRACE("getExpr","TheoremValue::getLHS called (",d_thm,")");</span>
<a name="l00300"></a>00300 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1TheoremValue.html#a123ac5cf8dde8d8ba3ca7d47a7d9bfde">isRewrite</a>(),
<a name="l00301"></a>00301 <span class="stringliteral">"TheoremValue::getLHS() called on non-rewrite theorem:\n"</span>
<a name="l00302"></a>00302 +<a class="code" href="classCVC3_1_1TheoremValue.html#a6862e6f9c77deced7b0ae841c01af3a8">toString</a>());
<a name="l00303"></a>00303 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a702623ca8da01e55a811e573a82fd0e4" title="The expression representing a theorem.">d_thm</a>[0];
<a name="l00304"></a>00304 }
<a name="l00305"></a><a class="code" href="classCVC3_1_1TheoremValue.html#ae28c3198351296f187065e78bba73a1f">00305</a> <span class="keyword">virtual</span> <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_1TheoremValue.html#ae28c3198351296f187065e78bba73a1f">getRHS</a>()<span class="keyword"> const </span>{
<a name="l00306"></a>00306 <span class="comment">// TRACE("getExpr","TheoremValue::getRHS called (",d_thm,")");</span>
<a name="l00307"></a>00307 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1TheoremValue.html#a123ac5cf8dde8d8ba3ca7d47a7d9bfde">isRewrite</a>(),
<a name="l00308"></a>00308 <span class="stringliteral">"TheoremValue::getRHS() called on non-rewrite theorem:\n"</span>
<a name="l00309"></a>00309 +<a class="code" href="classCVC3_1_1TheoremValue.html#a6862e6f9c77deced7b0ae841c01af3a8">toString</a>());
<a name="l00310"></a>00310 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a702623ca8da01e55a811e573a82fd0e4" title="The expression representing a theorem.">d_thm</a>[1];
<a name="l00311"></a>00311 }
<a name="l00312"></a>00312
<a name="l00313"></a>00313 <span class="keyword">virtual</span> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a>& <a class="code" href="classCVC3_1_1TheoremValue.html#a375f504a8a9844005b2eb8e055483829">getAssumptionsRef</a>() <span class="keyword">const</span> = 0;
<a name="l00314"></a>00314
<a name="l00315"></a><a class="code" href="classCVC3_1_1TheoremValue.html#aaaabd2fab47103f9a4574c380c790a11">00315</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoremValue.html#aaaabd2fab47103f9a4574c380c790a11">isAssump</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremValue.html#aac23fbc1ab6d8e32c7dc13bb11c7884d">d_isAssump</a>; }
<a name="l00316"></a><a class="code" href="classCVC3_1_1TheoremValue.html#af7120729a27c693ca032d176cf33e595">00316</a> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Proof.html">Proof</a>& <a class="code" href="classCVC3_1_1TheoremValue.html#af7120729a27c693ca032d176cf33e595">getProof</a>() { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a5cf31c613884270c10170d87ff58817b" title="Proof of the theorem.">d_proof</a>; }
<a name="l00317"></a>00317
<a name="l00318"></a>00318 <span class="keyword">public</span>:
<a name="l00319"></a>00319 <span class="comment">// Destructor</span>
<a name="l00320"></a><a class="code" href="classCVC3_1_1TheoremValue.html#a9b8baaeba9459d6b036086f9d0d67a1b">00320</a> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a9b8baaeba9459d6b036086f9d0d67a1b">~TheoremValue</a>() {
<a name="l00321"></a>00321 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(<a class="code" href="debug_8h.html#a2637b2fffa22e3c9fad40cda8fcc3bce" title="If something goes horribly wrong, print a message and abort immediately with exit(1).">FatalAssert</a>(<a class="code" href="classCVC3_1_1TheoremValue.html#a138c67c7a778d8e0d525a658439f105c" title="How many pointers to this theorem value.">d_refcount</a> == 0,
<a name="l00322"></a>00322 <span class="stringliteral">"Thm::TheoremValue::~TheoremValue(): refcount != 0."</span>);)
<a name="l00323"></a>00323 }
<a name="l00324"></a>00324
<a name="l00325"></a><a class="code" href="classCVC3_1_1TheoremValue.html#a6862e6f9c77deced7b0ae841c01af3a8">00325</a> std::string <a class="code" href="classCVC3_1_1TheoremValue.html#a6862e6f9c77deced7b0ae841c01af3a8">toString</a>() <span class="keyword">const</span> {
<a name="l00326"></a>00326 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a375f504a8a9844005b2eb8e055483829">getAssumptionsRef</a>().<a class="code" href="classCVC3_1_1Assumptions.html#ab1e6eca463ad7b98c0c2d2d31bb5d1dd">toString</a>() + <span class="stringliteral">" |- "</span> + <a class="code" href="classCVC3_1_1TheoremValue.html#ada6a2145dda62e6d3bd6781c7ef96141">getExpr</a>().<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>();
<a name="l00327"></a>00327 }
<a name="l00328"></a>00328
<a name="l00329"></a>00329 <span class="comment">// Memory management</span>
<a name="l00330"></a>00330 <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1MemoryManager.html">MemoryManager</a>* <a class="code" href="classCVC3_1_1TheoremValue.html#af8bf999e469afe124c04bfbbb6aba1e2">getMM</a>() = 0;
<a name="l00331"></a>00331
<a name="l00332"></a>00332 }; <span class="comment">// end of class TheoremValue</span>
<a name="l00333"></a>00333 <span class="comment"></span>
<a name="l00334"></a>00334 <span class="comment">///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00335"></a>00335 <span class="comment"></span><span class="comment">// //</span>
<a name="l00336"></a>00336 <span class="comment">// Class: RegTheoremValue //</span>
<a name="l00337"></a>00337 <span class="comment">// Author: Clark Barrett //</span>
<a name="l00338"></a>00338 <span class="comment">// Created: Fri May 2 12:51:55 2003 //</span>
<a name="l00339"></a>00339 <span class="comment">// Description: A special subclass for non-rewrite theorems. Assumptions are//</span>
<a name="l00340"></a>00340 <span class="comment">// embedded in the object for easy reference. //</span>
<a name="l00341"></a>00341 <span class="comment">// //</span><span class="comment"></span>
<a name="l00342"></a>00342 <span class="comment">///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00343"></a><a class="code" href="classCVC3_1_1RegTheoremValue.html">00343</a> <span class="comment"></span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1RegTheoremValue.html">RegTheoremValue</a> :<span class="keyword">public</span> <a class="code" href="classCVC3_1_1TheoremValue.html">TheoremValue</a>
<a name="l00344"></a>00344 {
<a name="l00345"></a><a class="code" href="classCVC3_1_1RegTheoremValue.html#a51f48d7e14c97707595cfe5f8f6df209">00345</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>;
<a name="l00346"></a>00346
<a name="l00347"></a>00347 <span class="keyword">protected</span>:<span class="comment"></span>
<a name="l00348"></a>00348 <span class="comment"> //! The assumptions for the theorem</span>
<a name="l00349"></a><a class="code" href="classCVC3_1_1RegTheoremValue.html#a5d6f8b40841e007c6908bc46b220c1a7">00349</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a> <a class="code" href="classCVC3_1_1RegTheoremValue.html#a5d6f8b40841e007c6908bc46b220c1a7" title="The assumptions for the theorem.">d_assump</a>;
<a name="l00350"></a>00350
<a name="l00351"></a>00351
<a name="l00352"></a>00352 <span class="keyword">private</span>:
<a name="l00353"></a>00353 <span class="comment">// Constructor. NOTE: it is private; only friend classes can call it.</span>
<a name="l00354"></a><a class="code" href="classCVC3_1_1RegTheoremValue.html#a50beadc804ee4d42e7b55195f97b865b">00354</a> <a class="code" href="classCVC3_1_1TheoremValue.html#a2fc7fcb35dcb6d97f101ffb632ac1dcd">RegTheoremValue</a>(<a class="code" href="classCVC3_1_1TheoremManager.html">TheoremManager</a>* tm, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& thm,
<a name="l00355"></a>00355 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a>& assump, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Proof.html">Proof</a>& pf, <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoremValue.html#aaaabd2fab47103f9a4574c380c790a11">isAssump</a>,
<a name="l00356"></a>00356 <span class="keywordtype">int</span> scope = -1)
<a name="l00357"></a>00357 : <a class="code" href="classCVC3_1_1TheoremValue.html">TheoremValue</a>(tm, thm, pf, isAssump), d_assump(assump)
<a name="l00358"></a>00358 {
<a name="l00359"></a>00359 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1TheoremValue.html#af0167eefead6921ed3919808bc0f9845" title="Theorem Manager.">d_tm</a>-><a class="code" href="classCVC3_1_1TheoremManager.html#ae1b25a77c570ef32031f982dc67a5ce1" title="Test whether the TheoremManager is still active.">isActive</a>(), <span class="stringliteral">"TheoremValue()"</span>);
<a name="l00360"></a>00360 <span class="keywordflow">if</span> (isAssump) {
<a name="l00361"></a>00361 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(assump.<a class="code" href="classCVC3_1_1Assumptions.html#a37da34b71944a11667d6af0fbd45651b">empty</a>(), <span class="stringliteral">"Expected empty assumptions"</span>);
<a name="l00362"></a>00362 <span class="comment">// refcount tricks are because a loop is created with Assumptions</span>
<a name="l00363"></a>00363 <a class="code" href="classCVC3_1_1TheoremValue.html#a138c67c7a778d8e0d525a658439f105c" title="How many pointers to this theorem value.">d_refcount</a> = 1;
<a name="l00364"></a>00364 {
<a name="l00365"></a>00365 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> t(<span class="keyword">this</span>);
<a name="l00366"></a>00366 d_assump.add1(t);
<a name="l00367"></a>00367 }
<a name="l00368"></a>00368 d_refcount = 0;
<a name="l00369"></a>00369 <span class="keywordflow">if</span> (scope == -1) <a class="code" href="classCVC3_1_1TheoremValue.html#a44a5fb4e3e9d28ee1d32c2fa61e05d15" title="Largest scope level of the assumptions.">d_scopeLevel</a> = tm-><a class="code" href="classCVC3_1_1TheoremManager.html#ab7f4c16522ac05cca1ca83ff79fc3e0f">getCM</a>()-><a class="code" href="classCVC3_1_1ContextManager.html#a194f7ddd794eaa876544a45006a3ff6f">scopeLevel</a>();
<a name="l00370"></a>00370 <span class="keywordflow">else</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a44a5fb4e3e9d28ee1d32c2fa61e05d15" title="Largest scope level of the assumptions.">d_scopeLevel</a> = scope;
<a name="l00371"></a>00371 <span class="comment">// TRACE("quantlevel", d_quantLevel, " theorem init assump", thm.toString()); </span>
<a name="l00372"></a>00372 }
<a name="l00373"></a>00373 <span class="keywordflow">else</span> {
<a name="l00374"></a>00374 <span class="keywordflow">if</span> (!d_assump.empty()) {
<a name="l00375"></a>00375 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Assumptions_1_1iterator.html" title="Iterator for the Assumptions: points to class Theorem.">Assumptions::iterator</a> iend = d_assump.end();
<a name="l00376"></a>00376 <span class="keywordflow">for</span> (<a class="code" href="classCVC3_1_1Assumptions_1_1iterator.html" title="Iterator for the Assumptions: points to class Theorem.">Assumptions::iterator</a> i = d_assump.begin();
<a name="l00377"></a>00377 i != iend; ++i) {
<a name="l00378"></a>00378 <span class="keywordflow">if</span> (i->getScope() > <a class="code" href="classCVC3_1_1TheoremValue.html#a44a5fb4e3e9d28ee1d32c2fa61e05d15" title="Largest scope level of the assumptions.">d_scopeLevel</a>)
<a name="l00379"></a>00379 <a class="code" href="classCVC3_1_1TheoremValue.html#a44a5fb4e3e9d28ee1d32c2fa61e05d15" title="Largest scope level of the assumptions.">d_scopeLevel</a> = i->getScope();
<a name="l00380"></a>00380 <span class="keywordflow">if</span> (i->getQuantLevel() > <a class="code" href="classCVC3_1_1TheoremValue.html#a819e06a02c53175bf33d4d475bd15d09" title="Quantification level of this theorem.">d_quantLevel</a>){
<a name="l00381"></a>00381 <a class="code" href="classCVC3_1_1TheoremValue.html#a819e06a02c53175bf33d4d475bd15d09" title="Quantification level of this theorem.">d_quantLevel</a> = i->getQuantLevel();
<a name="l00382"></a>00382 }
<a name="l00383"></a>00383 }
<a name="l00384"></a>00384 <span class="comment">// TRACE("quantlevel", d_quantLevel, " theorem non-null assump", thm.toString()); </span>
<a name="l00385"></a>00385 }
<a name="l00386"></a>00386 <span class="keywordflow">else</span>{
<a name="l00387"></a>00387 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"quantlevel"</span>,<span class="stringliteral">"empty assumptions found "</span>, thm , <span class="stringliteral">""</span>);
<a name="l00388"></a>00388 }
<a name="l00389"></a>00389 }
<a name="l00390"></a>00390 <span class="comment">//yeting, let me check d_quantleveldebug here</span>
<a name="l00391"></a>00391 <span class="comment">// d_quantLevelDebug = findQuantLevelDebug();</span>
<a name="l00392"></a>00392
<a name="l00393"></a>00393 }
<a name="l00394"></a>00394
<a name="l00395"></a>00395 <span class="keyword">public</span>:
<a name="l00396"></a>00396 <span class="comment">// Destructor</span>
<a name="l00397"></a><a class="code" href="classCVC3_1_1RegTheoremValue.html#ae0875f609ba238e52b9f059045ce32db">00397</a> <a class="code" href="classCVC3_1_1RegTheoremValue.html#ae0875f609ba238e52b9f059045ce32db">~RegTheoremValue</a>() {
<a name="l00398"></a>00398 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoremValue.html#aac23fbc1ab6d8e32c7dc13bb11c7884d">d_isAssump</a>) {
<a name="l00399"></a>00399 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(<a class="code" href="debug_8h.html#a2637b2fffa22e3c9fad40cda8fcc3bce" title="If something goes horribly wrong, print a message and abort immediately with exit(1).">FatalAssert</a>(d_assump.size() == 1, <span class="stringliteral">"Expected size 1"</span>);)
<a name="l00400"></a>00400 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(<a class="code" href="debug_8h.html#a2637b2fffa22e3c9fad40cda8fcc3bce" title="If something goes horribly wrong, print a message and abort immediately with exit(1).">FatalAssert</a>(d_assump.getFirst().thm() == <span class="keyword">this</span>, <span class="stringliteral">"Expected loop"</span>);)
<a name="l00401"></a>00401 d_assump.getFirst().d_thm = 0;
<a name="l00402"></a>00402 }
<a name="l00403"></a>00403 }
<a name="l00404"></a>00404
<a name="l00405"></a><a class="code" href="classCVC3_1_1RegTheoremValue.html#a695377925f8cc4f3607f304bec4cc325">00405</a> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a>& <a class="code" href="classCVC3_1_1RegTheoremValue.html#a695377925f8cc4f3607f304bec4cc325">getAssumptionsRef</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> d_assump; }
<a name="l00406"></a>00406
<a name="l00407"></a>00407 <span class="comment">// Memory management</span>
<a name="l00408"></a><a class="code" href="classCVC3_1_1RegTheoremValue.html#a7ee05bf85a8647cfaf296a2d76091bc0">00408</a> <a class="code" href="classCVC3_1_1MemoryManager.html">MemoryManager</a>* <a class="code" href="classCVC3_1_1RegTheoremValue.html#a7ee05bf85a8647cfaf296a2d76091bc0">getMM</a>() { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremValue.html#af0167eefead6921ed3919808bc0f9845" title="Theorem Manager.">d_tm</a>-><a class="code" href="classCVC3_1_1TheoremManager.html#a62b8cd3f917ca0fb580dde6c483db361">getMM</a>(); }
<a name="l00409"></a>00409
<a name="l00410"></a><a class="code" href="classCVC3_1_1RegTheoremValue.html#ab25aecf7df2593ed415f3d48a8459413">00410</a> <span class="keywordtype">void</span>* <a class="code" href="classCVC3_1_1RegTheoremValue.html#ab25aecf7df2593ed415f3d48a8459413">operator new</a>(<span class="keywordtype">size_t</span> size, <a class="code" href="classCVC3_1_1MemoryManager.html">MemoryManager</a>* mm) {
<a name="l00411"></a>00411 <span class="keywordflow">return</span> mm-><a class="code" href="classCVC3_1_1MemoryManager.html#a3db7efbc4b956bd423a73e1157d70ce0">newData</a>(size);
<a name="l00412"></a>00412 }
<a name="l00413"></a><a class="code" href="classCVC3_1_1RegTheoremValue.html#a42a9da336cd847f3dd4a02ecba7e9d49">00413</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1RegTheoremValue.html#a42a9da336cd847f3dd4a02ecba7e9d49">operator delete</a>(<span class="keywordtype">void</span>* pMem, <a class="code" href="classCVC3_1_1MemoryManager.html">MemoryManager</a>* mm) {
<a name="l00414"></a>00414 mm-><a class="code" href="classCVC3_1_1MemoryManager.html#ad29fac88d3a07566d9a8f9dc8d8e059c">deleteData</a>(pMem);
<a name="l00415"></a>00415 }
<a name="l00416"></a>00416
<a name="l00417"></a><a class="code" href="classCVC3_1_1RegTheoremValue.html#a0cfebc292531f0dfe31da67ac4c4006b">00417</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1RegTheoremValue.html#a0cfebc292531f0dfe31da67ac4c4006b">operator delete</a>(<span class="keywordtype">void</span>* d) { }
<a name="l00418"></a>00418
<a name="l00419"></a>00419 }; <span class="comment">// end of class RegTheoremValue</span>
<a name="l00420"></a>00420 <span class="comment"></span>
<a name="l00421"></a>00421 <span class="comment">///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00422"></a>00422 <span class="comment"></span><span class="comment">// //</span>
<a name="l00423"></a>00423 <span class="comment">// Class: RWTheoremValue //</span>
<a name="l00424"></a>00424 <span class="comment">// Author: Clark Barrett //</span>
<a name="l00425"></a>00425 <span class="comment">// Created: Fri May 2 12:51:55 2003 //</span>
<a name="l00426"></a>00426 <span class="comment">// Description: A special subclass for theorems of the form A |- t=t' or //</span>
<a name="l00427"></a>00427 <span class="comment">// A |- phi iff phi'. The actual Expr is only created on //</span>
<a name="l00428"></a>00428 <span class="comment">// demand. The idea is that getLHS and getRHS should be used //</span>
<a name="l00429"></a>00429 <span class="comment">// whenever possible, avoiding creating unnecessary Expr's. //</span>
<a name="l00430"></a>00430 <span class="comment">// //</span><span class="comment"></span>
<a name="l00431"></a>00431 <span class="comment">///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00432"></a><a class="code" href="classCVC3_1_1RWTheoremValue.html">00432</a> <span class="comment"></span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1RWTheoremValue.html">RWTheoremValue</a> :<span class="keyword">public</span> <a class="code" href="classCVC3_1_1TheoremValue.html">TheoremValue</a>
<a name="l00433"></a>00433 {
<a name="l00434"></a><a class="code" href="classCVC3_1_1RWTheoremValue.html#a51f48d7e14c97707595cfe5f8f6df209">00434</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>;
<a name="l00435"></a>00435
<a name="l00436"></a>00436 <span class="keyword">protected</span>:
<a name="l00437"></a>00437 <span class="comment">// d_thm in the base class contains the full expression, which is</span>
<a name="l00438"></a>00438 <span class="comment">// only constructed on demand.</span>
<a name="l00439"></a><a class="code" href="classCVC3_1_1RWTheoremValue.html#a8b9edd885956943f042bfb0ab13144d8">00439</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1RWTheoremValue.html#a8b9edd885956943f042bfb0ab13144d8">d_lhs</a>;
<a name="l00440"></a><a class="code" href="classCVC3_1_1RWTheoremValue.html#a017b26db1d8710ac3ffe2eb5b2bfaac4">00440</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1RWTheoremValue.html#a017b26db1d8710ac3ffe2eb5b2bfaac4">d_rhs</a>;
<a name="l00441"></a><a class="code" href="classCVC3_1_1RWTheoremValue.html#ab056c5711fae0e2d6ec30724a5321130">00441</a> <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a>* <a class="code" href="classCVC3_1_1RWTheoremValue.html#ab056c5711fae0e2d6ec30724a5321130">d_assump</a>;
<a name="l00442"></a>00442
<a name="l00443"></a>00443 <span class="keyword">private</span>:
<a name="l00444"></a><a class="code" href="classCVC3_1_1RWTheoremValue.html#ae270ede5a4e13ee66cc0ecdd9218032f">00444</a> <span class="keywordtype">void</span> init(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a>& assump, <span class="keywordtype">int</span> scope)
<a name="l00445"></a>00445 {
<a name="l00446"></a>00446 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1TheoremValue.html#af0167eefead6921ed3919808bc0f9845" title="Theorem Manager.">d_tm</a>-><a class="code" href="classCVC3_1_1TheoremManager.html#ae1b25a77c570ef32031f982dc67a5ce1" title="Test whether the TheoremManager is still active.">isActive</a>(), <span class="stringliteral">"TheoremValue()"</span>);
<a name="l00447"></a>00447 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoremValue.html#aac23fbc1ab6d8e32c7dc13bb11c7884d">d_isAssump</a>) {
<a name="l00448"></a>00448 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(assump.<a class="code" href="classCVC3_1_1Assumptions.html#a37da34b71944a11667d6af0fbd45651b">empty</a>(), <span class="stringliteral">"Expected empty assumptions"</span>);
<a name="l00449"></a>00449 <span class="comment">// refcount tricks are because a loop is created with Assumptions</span>
<a name="l00450"></a>00450 <a class="code" href="classCVC3_1_1TheoremValue.html#a138c67c7a778d8e0d525a658439f105c" title="How many pointers to this theorem value.">d_refcount</a> = 1;
<a name="l00451"></a>00451 {
<a name="l00452"></a>00452 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> t(<span class="keyword">this</span>);
<a name="l00453"></a>00453 d_assump = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a>(t);
<a name="l00454"></a>00454 }
<a name="l00455"></a>00455 d_refcount = 0;
<a name="l00456"></a>00456 <span class="keywordflow">if</span> (scope == -1) <a class="code" href="classCVC3_1_1TheoremValue.html#a44a5fb4e3e9d28ee1d32c2fa61e05d15" title="Largest scope level of the assumptions.">d_scopeLevel</a> = <a class="code" href="classCVC3_1_1TheoremValue.html#af0167eefead6921ed3919808bc0f9845" title="Theorem Manager.">d_tm</a>-><a class="code" href="classCVC3_1_1TheoremManager.html#ab7f4c16522ac05cca1ca83ff79fc3e0f">getCM</a>()-><a class="code" href="classCVC3_1_1ContextManager.html#a194f7ddd794eaa876544a45006a3ff6f">scopeLevel</a>();
<a name="l00457"></a>00457 <span class="keywordflow">else</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a44a5fb4e3e9d28ee1d32c2fa61e05d15" title="Largest scope level of the assumptions.">d_scopeLevel</a> = scope;
<a name="l00458"></a>00458 <span class="comment">// TRACE("quantlevel", d_quantLevel, " RW theorem init is assump ", d_thm.toString()); </span>
<a name="l00459"></a>00459 }
<a name="l00460"></a>00460 <span class="keywordflow">else</span> {
<a name="l00461"></a>00461 <span class="keywordflow">if</span> (!assump.<a class="code" href="classCVC3_1_1Assumptions.html#a37da34b71944a11667d6af0fbd45651b">empty</a>()) {
<a name="l00462"></a>00462 d_assump = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a>(assump);
<a name="l00463"></a>00463 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Assumptions_1_1iterator.html" title="Iterator for the Assumptions: points to class Theorem.">Assumptions::iterator</a> iend = assump.<a class="code" href="classCVC3_1_1Assumptions.html#afc875bbe97e4e2d74a2cdc824f783bfb">end</a>();
<a name="l00464"></a>00464 <span class="keywordflow">for</span> (<a class="code" href="classCVC3_1_1Assumptions_1_1iterator.html" title="Iterator for the Assumptions: points to class Theorem.">Assumptions::iterator</a> i = assump.<a class="code" href="classCVC3_1_1Assumptions.html#ac3e7d0e1796c83edf687aac063bdba06">begin</a>();
<a name="l00465"></a>00465 i != iend; ++i) {
<a name="l00466"></a>00466 <span class="keywordflow">if</span> (i->getScope() > <a class="code" href="classCVC3_1_1TheoremValue.html#a44a5fb4e3e9d28ee1d32c2fa61e05d15" title="Largest scope level of the assumptions.">d_scopeLevel</a>)
<a name="l00467"></a>00467 <a class="code" href="classCVC3_1_1TheoremValue.html#a44a5fb4e3e9d28ee1d32c2fa61e05d15" title="Largest scope level of the assumptions.">d_scopeLevel</a> = i->getScope();
<a name="l00468"></a>00468 <span class="keywordflow">if</span> (i->getQuantLevel() > <a class="code" href="classCVC3_1_1TheoremValue.html#a819e06a02c53175bf33d4d475bd15d09" title="Quantification level of this theorem.">d_quantLevel</a>){
<a name="l00469"></a>00469 <a class="code" href="classCVC3_1_1TheoremValue.html#a819e06a02c53175bf33d4d475bd15d09" title="Quantification level of this theorem.">d_quantLevel</a> = i->getQuantLevel();
<a name="l00470"></a>00470 <span class="comment">// TRACE("quantlevel", d_quantLevel, "=========\n RW theorem init has non-null assump ", this->toString()); </span>
<a name="l00471"></a>00471 }
<a name="l00472"></a>00472 }
<a name="l00473"></a>00473 <span class="comment">// TRACE("quantlevel", d_quantLevel, " RW theorem init has non-null assump ", d_thm.toString()); </span>
<a name="l00474"></a>00474 }
<a name="l00475"></a>00475 <span class="keywordflow">else</span>{
<a name="l00476"></a>00476 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"quantlevel"</span>, <span class="stringliteral">"RW empty assup found lhs << "</span> , d_lhs, <span class="stringliteral">""</span> );
<a name="l00477"></a>00477 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"quantlevel"</span>, <span class="stringliteral">"RW empty assup found rhs >> "</span> , d_rhs, <span class="stringliteral">""</span> );
<a name="l00478"></a>00478 }
<a name="l00479"></a>00479 <span class="comment">// TRACE("quantlevel", d_quantLevel, " RW theorem init has null assump ", d_thm.toString()); </span>
<a name="l00480"></a>00480 }
<a name="l00481"></a>00481
<a name="l00482"></a>00482 <span class="comment">// d_quantLevelDebug = findQuantLevelDebug();</span>
<a name="l00483"></a>00483
<a name="l00484"></a>00484 }
<a name="l00485"></a>00485
<a name="l00486"></a>00486 <span class="comment">// Constructor. NOTE: it is private; only friend classes can call it.</span>
<a name="l00487"></a><a class="code" href="classCVC3_1_1RWTheoremValue.html#aa11aa09f79c6fe48a3d8edd7722162d5">00487</a> <a class="code" href="classCVC3_1_1TheoremValue.html#add1e5fec863ffafbd22cac7aa0d1b689">RWTheoremValue</a>(<a class="code" href="classCVC3_1_1TheoremManager.html">TheoremManager</a>* tm, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& lhs, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& rhs,
<a name="l00488"></a>00488 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a>& assump, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Proof.html">Proof</a>& pf, <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoremValue.html#aaaabd2fab47103f9a4574c380c790a11">isAssump</a>,
<a name="l00489"></a>00489 <span class="keywordtype">int</span> scope = -1)
<a name="l00490"></a>00490 : <a class="code" href="classCVC3_1_1TheoremValue.html">TheoremValue</a>(tm, <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(), pf, isAssump), d_lhs(lhs), d_rhs(rhs), d_assump(NULL)
<a name="l00491"></a>00491 { init(assump, scope); }
<a name="l00492"></a>00492
<a name="l00493"></a>00493 <span class="comment">// Sometimes we have the full expression already created</span>
<a name="l00494"></a><a class="code" href="classCVC3_1_1RWTheoremValue.html#a0609a1142e41b1d43d43d5f60f8f701c">00494</a> <a class="code" href="classCVC3_1_1TheoremValue.html#add1e5fec863ffafbd22cac7aa0d1b689">RWTheoremValue</a>(<a class="code" href="classCVC3_1_1TheoremManager.html">TheoremManager</a>* tm, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& thm,
<a name="l00495"></a>00495 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a>& assump, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Proof.html">Proof</a>& pf, <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoremValue.html#aaaabd2fab47103f9a4574c380c790a11">isAssump</a>,
<a name="l00496"></a>00496 <span class="keywordtype">int</span> scope = -1)
<a name="l00497"></a>00497 : <a class="code" href="classCVC3_1_1TheoremValue.html">TheoremValue</a>(tm, thm, pf, isAssump), d_lhs(thm[0]), d_rhs(thm[1]), d_assump(NULL)
<a name="l00498"></a>00498 { init(assump, scope); }
<a name="l00499"></a>00499
<a name="l00500"></a><a class="code" href="classCVC3_1_1RWTheoremValue.html#a84ba3b591680ab321aa2f855298a41f2">00500</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_1RWTheoremValue.html#a84ba3b591680ab321aa2f855298a41f2">getExpr</a>()<span class="keyword"> const </span>{
<a name="l00501"></a>00501 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoremValue.html#a702623ca8da01e55a811e573a82fd0e4" title="The expression representing a theorem.">d_thm</a>.<a class="code" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a>()) {
<a name="l00502"></a>00502 <span class="keywordtype">bool</span> isBool = d_lhs.<a class="code" href="group__ExprPkg.html#ga42929221eb172250697b72c28af6de07" title="Get the type. Recursively compute if necessary.">getType</a>().<a class="code" href="classCVC3_1_1Type.html#a38bba404056eadf3c283a67ab2347e02">isBool</a>();
<a name="l00503"></a>00503 <span class="comment">// have to fake out the const qualifier</span>
<a name="l00504"></a>00504 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>* pexpr = <span class="keyword">const_cast<</span><a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>*<span class="keyword">></span>(&<a class="code" href="classCVC3_1_1TheoremValue.html#a702623ca8da01e55a811e573a82fd0e4" title="The expression representing a theorem.">d_thm</a>);
<a name="l00505"></a>00505 *pexpr = isBool ? d_lhs.<a class="code" href="group__ExprPkg.html#gaae017ca8e68af655ba285c985dd9fba5">iffExpr</a>(d_rhs) : d_lhs.<a class="code" href="group__ExprPkg.html#gacb48495ca445c895f95d0c3c1ae2070b">eqExpr</a>(d_rhs);
<a name="l00506"></a>00506 <span class="comment">// TRACE("getExpr", "getExpr called on RWTheorem (", d_thm, ")");</span>
<a name="l00507"></a>00507 }
<a name="l00508"></a>00508 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremValue.html#a702623ca8da01e55a811e573a82fd0e4" title="The expression representing a theorem.">d_thm</a>;
<a name="l00509"></a>00509 }
<a name="l00510"></a>00510
<a name="l00511"></a><a class="code" href="classCVC3_1_1RWTheoremValue.html#ac3a024c1f0a4aa4cf8d8aa6200ac9911">00511</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_1RWTheoremValue.html#ac3a024c1f0a4aa4cf8d8aa6200ac9911">getLHS</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> d_lhs; }
<a name="l00512"></a><a class="code" href="classCVC3_1_1RWTheoremValue.html#a61466f64bcb5fd3664fe2bed35ad7f97">00512</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_1RWTheoremValue.html#a61466f64bcb5fd3664fe2bed35ad7f97">getRHS</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> d_rhs; }
<a name="l00513"></a>00513
<a name="l00514"></a>00514 <span class="keyword">public</span>:
<a name="l00515"></a>00515 <span class="comment">// Destructor</span>
<a name="l00516"></a><a class="code" href="classCVC3_1_1RWTheoremValue.html#a060b5754b6d6ea2efb43e4c97abba6c3">00516</a> <a class="code" href="classCVC3_1_1RWTheoremValue.html#a060b5754b6d6ea2efb43e4c97abba6c3">~RWTheoremValue</a>() {
<a name="l00517"></a>00517 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoremValue.html#aac23fbc1ab6d8e32c7dc13bb11c7884d">d_isAssump</a>) {
<a name="l00518"></a>00518 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(<a class="code" href="debug_8h.html#a2637b2fffa22e3c9fad40cda8fcc3bce" title="If something goes horribly wrong, print a message and abort immediately with exit(1).">FatalAssert</a>(d_assump && d_assump->size() == 1, <span class="stringliteral">"Expected size 1"</span>);)
<a name="l00519"></a>00519 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(<a class="code" href="debug_8h.html#a2637b2fffa22e3c9fad40cda8fcc3bce" title="If something goes horribly wrong, print a message and abort immediately with exit(1).">FatalAssert</a>(d_assump->getFirst().thm() == <span class="keyword">this</span>, <span class="stringliteral">"Expected loop"</span>);)
<a name="l00520"></a>00520 d_assump->getFirst().d_thm = 0;
<a name="l00521"></a>00521 }
<a name="l00522"></a>00522 <span class="keywordflow">if</span> (d_assump) <span class="keyword">delete</span> d_assump;
<a name="l00523"></a>00523 }
<a name="l00524"></a>00524
<a name="l00525"></a><a class="code" href="classCVC3_1_1RWTheoremValue.html#a6fdd9581600000bdb9b521203e20275b">00525</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1RWTheoremValue.html#a6fdd9581600000bdb9b521203e20275b">isRewrite</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <span class="keyword">true</span>; }
<a name="l00526"></a><a class="code" href="classCVC3_1_1RWTheoremValue.html#a90d334b1d81a6ecaed725b689920733c">00526</a> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a>& <a class="code" href="classCVC3_1_1RWTheoremValue.html#a90d334b1d81a6ecaed725b689920733c">getAssumptionsRef</a>()<span class="keyword"> const </span>{
<a name="l00527"></a>00527 <span class="keywordflow">if</span> (d_assump) <span class="keywordflow">return</span> *d_assump;
<a name="l00528"></a>00528 <span class="keywordflow">else</span> <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Assumptions.html#af309a39e2e013cc62b6d94c5812ad86b">Assumptions::emptyAssump</a>();
<a name="l00529"></a>00529 }
<a name="l00530"></a>00530
<a name="l00531"></a>00531 <span class="comment">// Memory management</span>
<a name="l00532"></a><a class="code" href="classCVC3_1_1RWTheoremValue.html#a4593444ed15ecbd4b1be7b44e5b5bc48">00532</a> <a class="code" href="classCVC3_1_1MemoryManager.html">MemoryManager</a>* <a class="code" href="classCVC3_1_1RWTheoremValue.html#a4593444ed15ecbd4b1be7b44e5b5bc48">getMM</a>() { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremValue.html#af0167eefead6921ed3919808bc0f9845" title="Theorem Manager.">d_tm</a>-><a class="code" href="classCVC3_1_1TheoremManager.html#a1ab310c8d6cfd68063379902b371a924">getRWMM</a>(); }
<a name="l00533"></a>00533
<a name="l00534"></a><a class="code" href="classCVC3_1_1RWTheoremValue.html#ad7807e6659f09c8a8b07ba9b9ccffc02">00534</a> <span class="keywordtype">void</span>* <a class="code" href="classCVC3_1_1RWTheoremValue.html#ad7807e6659f09c8a8b07ba9b9ccffc02">operator new</a>(<span class="keywordtype">size_t</span> size, <a class="code" href="classCVC3_1_1MemoryManager.html">MemoryManager</a>* mm) {
<a name="l00535"></a>00535 <span class="keywordflow">return</span> mm-><a class="code" href="classCVC3_1_1MemoryManager.html#a3db7efbc4b956bd423a73e1157d70ce0">newData</a>(size);
<a name="l00536"></a>00536 }
<a name="l00537"></a><a class="code" href="classCVC3_1_1RWTheoremValue.html#a0e75cf3dcce7598fbfb1222a96a89ba3">00537</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1RWTheoremValue.html#a0e75cf3dcce7598fbfb1222a96a89ba3">operator delete</a>(<span class="keywordtype">void</span>* pMem, <a class="code" href="classCVC3_1_1MemoryManager.html">MemoryManager</a>* mm) {
<a name="l00538"></a>00538 mm-><a class="code" href="classCVC3_1_1MemoryManager.html#ad29fac88d3a07566d9a8f9dc8d8e059c">deleteData</a>(pMem);
<a name="l00539"></a>00539 }
<a name="l00540"></a>00540
<a name="l00541"></a><a class="code" href="classCVC3_1_1RWTheoremValue.html#a6361d6ecbc7b02d7d10d5b7b26589d45">00541</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1RWTheoremValue.html#a6361d6ecbc7b02d7d10d5b7b26589d45">operator delete</a>(<span class="keywordtype">void</span>* d) { }
<a name="l00542"></a>00542
<a name="l00543"></a>00543 }; <span class="comment">// end of class RWTheoremValue</span>
<a name="l00544"></a>00544
<a name="l00545"></a>00545 } <span class="comment">// end of namespace CVC3</span>
<a name="l00546"></a>00546
<a name="l00547"></a>00547 <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>
