<!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.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.h</div> </div>
</div>
<div class="contents">
<a href="theorem_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.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 00:37:49 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: Theorem</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 proof prodicing mode also its</span>
<a name="l00028"></a>00028 <span class="comment">// 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.h file should be used by the decision procedures that</span>
<a name="l00041"></a>00041 <span class="comment">// use Theorem.</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="comment">// expr.h Has to be included outside of #ifndef, since it sources us</span>
<a name="l00046"></a>00046 <span class="comment">// recursively (read comments in expr_value.h).</span>
<a name="l00047"></a>00047 <span class="preprocessor">#ifndef _cvc3__expr_h_</span>
<a name="l00048"></a>00048 <span class="preprocessor"></span><span class="preprocessor">#include "<a class="code" href="expr_8h.html" title="Definition of the API to expression package. See class Expr for details.">expr.h</a>"</span>
<a name="l00049"></a>00049 <span class="preprocessor">#endif</span>
<a name="l00050"></a>00050 <span class="preprocessor"></span>
<a name="l00051"></a>00051 <span class="preprocessor">#ifndef _cvc3__theorem_h_</span>
<a name="l00052"></a>00052 <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__theorem_h_</span>
<a name="l00053"></a>00053 <span class="preprocessor"></span>
<a name="l00054"></a>00054 <span class="preprocessor">#include "<a class="code" href="os_8h.html" title="Abstraction over different operating systems.">os.h</a>"</span>
<a name="l00055"></a>00055 <span class="preprocessor">#include "<a class="code" href="proof_8h.html">proof.h</a>"</span>
<a name="l00056"></a>00056
<a name="l00057"></a>00057 <span class="keyword">namespace </span>CVC3 {
<a name="l00058"></a>00058
<a name="l00059"></a>00059 <span class="comment">// Declare the data holding classes but hide the definitions</span>
<a name="l00060"></a>00060 <span class="keyword">class </span>TheoremManager;
<a name="l00061"></a>00061 <span class="keyword">class </span>TheoremValue;
<a name="l00062"></a>00062 <span class="keyword">class </span>Assumptions;
<a name="l00063"></a>00063
<a name="l00064"></a>00064 <span class="comment">// Theorem is basically a wrapper around a pointer to a</span>
<a name="l00065"></a>00065 <span class="comment">// TheoremValue, so that we can pass this class around by value.</span>
<a name="l00066"></a>00066 <span class="comment">// All the constructors of this class are private, so do not inherit</span>
<a name="l00067"></a>00067 <span class="comment">// from it and do not try to create a value directly. Only</span>
<a name="l00068"></a>00068 <span class="comment">// TheoremProducer can create new Theorem instances.</span>
<a name="l00069"></a>00069 <span class="comment">//</span>
<a name="l00070"></a>00070 <span class="comment">// Theorems, unlike expressions, are NOT made unique, and it is</span>
<a name="l00071"></a>00071 <span class="comment">// possible to have the same theorem in different scopes with</span>
<a name="l00072"></a>00072 <span class="comment">// different assumptions and proofs. It is a deliberate feature,</span>
<a name="l00073"></a>00073 <span class="comment">// since natural deduction sometimes requires proving the same</span>
<a name="l00074"></a>00074 <span class="comment">// conclusion from different assumptions independently, e.g. in</span>
<a name="l00075"></a>00075 <span class="comment">// disjunction elimination rule.</span>
<a name="l00076"></a><a class="code" href="classCVC3_1_1Theorem.html">00076</a> <span class="keyword">class </span><a class="code" href="os_8h.html#a0035aac6379df39aa69feba98b2751ba">CVC_DLL</a> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> {
<a name="l00077"></a>00077 <span class="keyword">private</span>:
<a name="l00078"></a>00078 <span class="comment">// Make a theorem producing class our friend. No definition is</span>
<a name="l00079"></a>00079 <span class="comment">// exposed here.</span>
<a name="l00080"></a><a class="code" href="classCVC3_1_1Theorem.html#adb16a6e6bad96912c4150299576eaf9a">00080</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1TheoremProducer.html">TheoremProducer</a>;
<a name="l00081"></a>00081 <span class="comment">// Also allow our 3-valued cousin to create us</span>
<a name="l00082"></a><a class="code" href="classCVC3_1_1Theorem.html#acc3b40272a636c6365e02a387cfc4c82">00082</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1Theorem3.html" title="Theorem3.">Theorem3</a>;
<a name="l00083"></a>00083 <span class="comment">// Also TheoremValue classes for assumptions</span>
<a name="l00084"></a><a class="code" href="classCVC3_1_1Theorem.html#a2fc7fcb35dcb6d97f101ffb632ac1dcd">00084</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1RegTheoremValue.html">RegTheoremValue</a>;
<a name="l00085"></a><a class="code" href="classCVC3_1_1Theorem.html#add1e5fec863ffafbd22cac7aa0d1b689">00085</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1RWTheoremValue.html">RWTheoremValue</a>;
<a name="l00086"></a>00086
<a name="l00087"></a>00087 <span class="comment">// Optimization: reflexivity theorems just store the exprValue pointer</span>
<a name="l00088"></a>00088 <span class="comment">// directly. Also, the lowest bit is set to 1 to indicate that its</span>
<a name="l00089"></a>00089 <span class="comment">// a reflexivity theorem. This really helps performance!</span>
<a name="l00090"></a>00090 <span class="keyword">union </span>{
<a name="l00091"></a><a class="code" href="classCVC3_1_1Theorem.html#a696e2281069af317ec3fb6510845ca6c">00091</a> intptr_t <a class="code" href="classCVC3_1_1Theorem.html#a696e2281069af317ec3fb6510845ca6c">d_thm</a>;
<a name="l00092"></a><a class="code" href="classCVC3_1_1Theorem.html#a798f8085ec077b69aae198a155077774">00092</a> <a class="code" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>* <a class="code" href="classCVC3_1_1Theorem.html#a798f8085ec077b69aae198a155077774">d_expr</a>;
<a name="l00093"></a>00093 };
<a name="l00094"></a>00094 <span class="comment"></span>
<a name="l00095"></a>00095 <span class="comment"> //! Compare Theorems by their expressions. Return -1, 0, or 1.</span>
<a name="l00096"></a>00096 <span class="comment"></span> <span class="keyword">friend</span> <span class="keywordtype">int</span> <a class="code" href="namespaceCVC3.html#ac06ac2fd4db699104b790f98b7abba71">compare</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t2);<span class="comment"></span>
<a name="l00097"></a>00097 <span class="comment"> //! Compare a Theorem with an Expr (as if Expr is a Theorem)</span>
<a name="l00098"></a>00098 <span class="comment"></span> <span class="keyword">friend</span> <span class="keywordtype">int</span> <a class="code" href="namespaceCVC3.html#ac06ac2fd4db699104b790f98b7abba71">compare</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e2);<span class="comment"></span>
<a name="l00099"></a>00099 <span class="comment"> //! Compare Theorems by TheoremValue pointers. Return -1, 0, or 1.</span>
<a name="l00100"></a>00100 <span class="comment"></span> <span class="keyword">friend</span> <span class="keywordtype">int</span> <a class="code" href="namespaceCVC3.html#af87b5038044e2f5706e30e5ed6f7584e">compareByPtr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t2);<span class="comment"></span>
<a name="l00101"></a>00101 <span class="comment"> //! Equality is w.r.t. compare()</span>
<a name="l00102"></a><a class="code" href="classCVC3_1_1Theorem.html#a6f08e5df7b32fccb7bba2e689518569e">00102</a> <span class="comment"></span> <span class="keyword">friend</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#a8e164436388f2d87c971d9bbde973c58">operator==</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t2)
<a name="l00103"></a>00103 { <span class="keywordflow">return</span> (<a class="code" href="namespaceCVC3.html#ac06ac2fd4db699104b790f98b7abba71">compare</a>(t1, t2)==0); }<span class="comment"></span>
<a name="l00104"></a>00104 <span class="comment"> //! Disequality is w.r.t. compare()</span>
<a name="l00105"></a><a class="code" href="classCVC3_1_1Theorem.html#acf65eea626a36c24c83abcee026ec205">00105</a> <span class="comment"></span> <span class="keyword">friend</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#a5aa953c549c2e103f3834c48bf6cb9a1">operator!=</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t2)
<a name="l00106"></a>00106 { <span class="keywordflow">return</span> (<a class="code" href="namespaceCVC3.html#ac06ac2fd4db699104b790f98b7abba71">compare</a>(t1, t2) != 0); }
<a name="l00107"></a>00107 <span class="comment"></span>
<a name="l00108"></a>00108 <span class="comment"> //! Constructor only used by TheoremValue for assumptions</span>
<a name="l00109"></a><a class="code" href="classCVC3_1_1Theorem.html#a2fefec275dfdf6d8932c6f74b03bec4d">00109</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html#a2fefec275dfdf6d8932c6f74b03bec4d" title="Constructor only used by TheoremValue for assumptions.">Theorem</a>(<a class="code" href="classCVC3_1_1TheoremValue.html">TheoremValue</a>* thm) :d_thm(((intptr_t)thm) | 0x1) {}
<a name="l00110"></a>00110 <span class="comment"></span>
<a name="l00111"></a>00111 <span class="comment"> //! Constructor for a new theorem </span>
<a name="l00112"></a>00112 <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</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, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a>& assump,
<a name="l00113"></a>00113 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Proof.html">Proof</a>& pf, <span class="keywordtype">bool</span> isAssump = <span class="keyword">false</span>, <span class="keywordtype">int</span> scope = -1);
<a name="l00114"></a>00114 <span class="comment"></span>
<a name="l00115"></a>00115 <span class="comment"> //! Constructor for rewrite theorems.</span>
<a name="l00116"></a>00116 <span class="comment"></span><span class="comment"> /*! These use a special efficient subclass of TheoremValue for</span>
<a name="l00117"></a>00117 <span class="comment"> * theorems which represent rewrites: A |- t = t' or A |- phi<=>phi'</span>
<a name="l00118"></a>00118 <span class="comment"> */</span>
<a name="l00119"></a>00119 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</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="l00120"></a>00120 <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> isAssump = <span class="keyword">false</span>,
<a name="l00121"></a>00121 <span class="keywordtype">int</span> scope = -1);
<a name="l00122"></a>00122 <span class="comment"></span>
<a name="l00123"></a>00123 <span class="comment"> //! Constructor for a reflexivity theorem: |-t=t or |-phi<=>phi</span>
<a name="l00124"></a>00124 <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</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="l00125"></a>00125
<a name="l00126"></a>00126 <span class="keywordtype">void</span> recursivePrint(<span class="keywordtype">int</span>& i) <span class="keyword">const</span>;
<a name="l00127"></a>00127 <span class="keywordtype">void</span> getAssumptionsRec(std::set<Expr>& assumptions) <span class="keyword">const</span>;
<a name="l00128"></a>00128 <span class="keywordtype">void</span> getAssumptionsAndCongRec(std::set<Expr>& assumptions,
<a name="l00129"></a>00129 std::vector<Expr>& congruences) <span class="keyword">const</span>;
<a name="l00130"></a>00130 <span class="keywordtype">void</span> GetSatAssumptionsRec(std::vector<Theorem>& assumptions) <span class="keyword">const</span>;
<a name="l00131"></a>00131
<a name="l00132"></a><a class="code" href="classCVC3_1_1Theorem.html#a67e2a295b1598057cfbb51120a0c1ad6">00132</a> <a class="code" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>* <a class="code" href="classCVC3_1_1Theorem.html#a67e2a295b1598057cfbb51120a0c1ad6">exprValue</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> d_expr; }
<a name="l00133"></a><a class="code" href="classCVC3_1_1Theorem.html#a12de358e2b6cb67415f508ceca6913d1">00133</a> <a class="code" href="classCVC3_1_1TheoremValue.html">TheoremValue</a>* <a class="code" href="classCVC3_1_1Theorem.html#a12de358e2b6cb67415f508ceca6913d1">thm</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> (<a class="code" href="classCVC3_1_1TheoremValue.html">TheoremValue</a>*)(d_thm & (~(0x1))); }
<a name="l00134"></a>00134
<a name="l00135"></a>00135 <span class="keyword">public</span>:
<a name="l00136"></a>00136 <span class="comment">// recusive function to print theorems and all assumptions recursively</span>
<a name="l00137"></a>00137 <span class="comment">// important: this function will corrupt all flags!! so exercise </span>
<a name="l00138"></a>00138 <span class="comment">// caution when using in any graph traversals </span>
<a name="l00139"></a>00139 <span class="comment">// (probably more useful to call it only before a crash)</span>
<a name="l00140"></a><a class="code" href="classCVC3_1_1Theorem.html#ad9da69b34ab2bab4192e5977e5c10498">00140</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Theorem.html#ad9da69b34ab2bab4192e5977e5c10498">printDebug</a>()<span class="keyword"> const </span>{
<a name="l00141"></a>00141 clearAllFlags();
<a name="l00142"></a>00142 setCachedValue(0);
<a name="l00143"></a>00143 setFlag();
<a name="l00144"></a>00144 <span class="keywordtype">int</span> i = 1;
<a name="l00145"></a>00145 recursivePrint(i);
<a name="l00146"></a>00146 }
<a name="l00147"></a>00147
<a name="l00148"></a>00148 <span class="comment">// Default constructor creates Null theorem to allow untrusted</span>
<a name="l00149"></a>00149 <span class="comment">// code declare local vars without initialization (vector<Theorem></span>
<a name="l00150"></a>00150 <span class="comment">// may need that, for instance).</span>
<a name="l00151"></a><a class="code" href="classCVC3_1_1Theorem.html#a4b7574a16eed728fac6e37d2404fdbf8">00151</a> <a class="code" href="classCVC3_1_1Theorem.html#a4b7574a16eed728fac6e37d2404fdbf8">Theorem</a>(): d_thm(0) { }
<a name="l00152"></a>00152 <span class="comment">// Copy constructor</span>
<a name="l00153"></a>00153 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> &th);
<a name="l00154"></a>00154 <span class="comment">// Assignment operator</span>
<a name="l00155"></a>00155 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& operator=(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> &th);
<a name="l00156"></a>00156
<a name="l00157"></a>00157 <span class="comment">// Destructor</span>
<a name="l00158"></a>00158 ~<a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>();
<a name="l00159"></a>00159
<a name="l00160"></a>00160 <span class="comment">// Test if we are running in a proof production mode and with assumptions</span>
<a name="l00161"></a>00161 <span class="keywordtype">bool</span> withProof() <span class="keyword">const</span>;
<a name="l00162"></a>00162 <span class="keywordtype">bool</span> withAssumptions() <span class="keyword">const</span>;
<a name="l00163"></a>00163
<a name="l00164"></a><a class="code" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">00164</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> d_thm == 0; }
<a name="l00165"></a>00165
<a name="l00166"></a>00166 <span class="comment">// True if theorem is of the form t=t' or phi iff phi'</span>
<a name="l00167"></a>00167 <span class="keywordtype">bool</span> isRewrite() <span class="keyword">const</span>;
<a name="l00168"></a>00168 <span class="comment">// True if theorem was created using assumpRule</span>
<a name="l00169"></a>00169 <span class="keywordtype">bool</span> isAssump() <span class="keyword">const</span>;
<a name="l00170"></a>00170 <span class="comment">// True if reflexivity theorem</span>
<a name="l00171"></a><a class="code" href="classCVC3_1_1Theorem.html#a16f074e60b9e076187efb478889d2c47">00171</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Theorem.html#a16f074e60b9e076187efb478889d2c47">isRefl</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> d_thm && !(d_thm & 0x1); }
<a name="l00172"></a>00172
<a name="l00173"></a>00173 <span class="comment">// Return the theorem value as an Expr</span>
<a name="l00174"></a>00174 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> getExpr() <span class="keyword">const</span>;
<a name="l00175"></a>00175 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& getLHS() <span class="keyword">const</span>;
<a name="l00176"></a>00176 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& getRHS() <span class="keyword">const</span>;
<a name="l00177"></a>00177
<a name="l00178"></a>00178 <span class="keywordtype">void</span> GetSatAssumptions(std::vector<Theorem>& assumptions) <span class="keyword">const</span>;
<a name="l00179"></a>00179
<a name="l00180"></a>00180
<a name="l00181"></a>00181 <span class="comment">// Return the assumptions. a should be empty and uninitialized</span>
<a name="l00182"></a>00182 <span class="comment">// void getAssumptions(Assumptions& a) const;</span>
<a name="l00183"></a>00183 <span class="comment">// Recurse to get actual assumptions</span>
<a name="l00184"></a>00184
<a name="l00185"></a>00185 <span class="keywordtype">void</span> getLeafAssumptions(std::vector<Expr>& assumptions,
<a name="l00186"></a>00186 <span class="keywordtype">bool</span> negate = <span class="keyword">false</span>) <span class="keyword">const</span>;
<a name="l00187"></a>00187 <span class="comment">// Same as above but also collects congruences in the proof tree</span>
<a name="l00188"></a>00188 <span class="keywordtype">void</span> getAssumptionsAndCong(std::vector<Expr>& assumptions,
<a name="l00189"></a>00189 std::vector<Expr>& congruences,
<a name="l00190"></a>00190 <span class="keywordtype">bool</span> negate = <span class="keyword">false</span>) <span class="keyword">const</span>;
<a name="l00191"></a>00191 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a>& getAssumptionsRef() <span class="keyword">const</span>;
<a name="l00192"></a>00192 <span class="comment">// Return the proof of the theorem. If running without proofs,</span>
<a name="l00193"></a>00193 <span class="comment">// return the Null proof.</span>
<a name="l00194"></a>00194 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> getProof() <span class="keyword">const</span>;
<a name="l00195"></a>00195 <span class="comment">// Return the lowest scope level at which this theorem is valid.</span>
<a name="l00196"></a>00196 <span class="comment">// Value -1 means no information is available.</span>
<a name="l00197"></a>00197 <span class="keywordtype">int</span> getScope() <span class="keyword">const</span>;<span class="comment"></span>
<a name="l00198"></a>00198 <span class="comment"> //! Return quantification level for this theorem</span>
<a name="l00199"></a>00199 <span class="comment"></span> <span class="keywordtype">unsigned</span> getQuantLevel() <span class="keyword">const</span>;
<a name="l00200"></a>00200
<a name="l00201"></a>00201 <span class="keywordtype">unsigned</span> getQuantLevelDebug() <span class="keyword">const</span>;
<a name="l00202"></a>00202 <span class="comment"></span>
<a name="l00203"></a>00203 <span class="comment"> //! Set the quantification level for this theorem</span>
<a name="l00204"></a>00204 <span class="comment"></span> <span class="keywordtype">void</span> setQuantLevel(<span class="keywordtype">unsigned</span> level);
<a name="l00205"></a>00205
<a name="l00206"></a>00206 <span class="comment">// hash</span>
<a name="l00207"></a>00207 <span class="keywordtype">size_t</span> <a class="code" href="structHash_1_1hash.html">hash</a>() <span class="keyword">const</span>;
<a name="l00208"></a>00208
<a name="l00209"></a>00209 <span class="comment">// Printing</span>
<a name="l00210"></a>00210 std::string toString() <span class="keyword">const</span>;
<a name="l00211"></a>00211
<a name="l00212"></a>00212 <span class="comment">// For debugging</span>
<a name="l00213"></a>00213 <span class="keywordtype">void</span> printx() <span class="keyword">const</span>;
<a name="l00214"></a>00214 <span class="keywordtype">void</span> printxnodag() <span class="keyword">const</span>;
<a name="l00215"></a>00215 <span class="keywordtype">void</span> pprintx() <span class="keyword">const</span>;
<a name="l00216"></a>00216 <span class="keywordtype">void</span> pprintxnodag() <span class="keyword">const</span>;
<a name="l00217"></a>00217
<a name="l00218"></a>00218 <span class="keywordtype">void</span> print() <span class="keyword">const</span>;
<a name="l00219"></a>00219 <span class="comment"></span>
<a name="l00220"></a>00220 <span class="comment"> /*! \name Methods for Theorem Attributes</span>
<a name="l00221"></a>00221 <span class="comment"> *</span>
<a name="l00222"></a>00222 <span class="comment"> * Several attributes used in conflict analysis and assumptions</span>
<a name="l00223"></a>00223 <span class="comment"> * graph traversals.</span>
<a name="l00224"></a>00224 <span class="comment"> * @{</span>
<a name="l00225"></a>00225 <span class="comment"> */</span><span class="comment"></span>
<a name="l00226"></a>00226 <span class="comment"> //! Check if the flag attribute is set</span>
<a name="l00227"></a>00227 <span class="comment"></span> <span class="keywordtype">bool</span> isFlagged() <span class="keyword">const</span>;<span class="comment"></span>
<a name="l00228"></a>00228 <span class="comment"> //! Clear the flag attribute in all the theorems</span>
<a name="l00229"></a>00229 <span class="comment"></span> <span class="keywordtype">void</span> clearAllFlags() <span class="keyword">const</span>;<span class="comment"></span>
<a name="l00230"></a>00230 <span class="comment"> //! Set the flag attribute</span>
<a name="l00231"></a>00231 <span class="comment"></span> <span class="keywordtype">void</span> setFlag() <span class="keyword">const</span>;
<a name="l00232"></a>00232 <span class="comment"></span>
<a name="l00233"></a>00233 <span class="comment"> //! Set flag stating that theorem is an instance of substitution</span>
<a name="l00234"></a>00234 <span class="comment"></span> <span class="keywordtype">void</span> setSubst() <span class="keyword">const</span>;<span class="comment"></span>
<a name="l00235"></a>00235 <span class="comment"> //! Is theorem an instance of substitution</span>
<a name="l00236"></a>00236 <span class="comment"></span> <span class="keywordtype">bool</span> isSubst() <span class="keyword">const</span>;<span class="comment"></span>
<a name="l00237"></a>00237 <span class="comment"> //! Set the "expand" attribute</span>
<a name="l00238"></a>00238 <span class="comment"></span> <span class="keywordtype">void</span> setExpandFlag(<span class="keywordtype">bool</span> val) <span class="keyword">const</span>;<span class="comment"></span>
<a name="l00239"></a>00239 <span class="comment"> //! Check the "expand" attribute</span>
<a name="l00240"></a>00240 <span class="comment"></span> <span class="keywordtype">bool</span> getExpandFlag() <span class="keyword">const</span>;<span class="comment"></span>
<a name="l00241"></a>00241 <span class="comment"> //! Set the "literal" attribute</span>
<a name="l00242"></a>00242 <span class="comment"></span><span class="comment"> /*! The expression of this theorem will be added as a conflict</span>
<a name="l00243"></a>00243 <span class="comment"> * clause literal */</span>
<a name="l00244"></a>00244 <span class="keywordtype">void</span> setLitFlag(<span class="keywordtype">bool</span> val) <span class="keyword">const</span>;<span class="comment"></span>
<a name="l00245"></a>00245 <span class="comment"> //! Check the "literal" attribute</span>
<a name="l00246"></a>00246 <span class="comment"></span><span class="comment"> /*! The expression of this theorem will be added as a conflict</span>
<a name="l00247"></a>00247 <span class="comment"> * clause literal */</span>
<a name="l00248"></a>00248 <span class="keywordtype">bool</span> getLitFlag() <span class="keyword">const</span>;<span class="comment"></span>
<a name="l00249"></a>00249 <span class="comment"> //! Check if the theorem is a literal</span>
<a name="l00250"></a>00250 <span class="comment"></span> <span class="keywordtype">bool</span> isAbsLiteral() <span class="keyword">const</span>;
<a name="l00251"></a>00251
<a name="l00252"></a><a class="code" href="classCVC3_1_1Theorem.html#a657f0037f907743988443bffdf2e505c">00252</a> <span class="keywordtype">bool</span> refutes(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e)<span class="keyword"> const</span>
<a name="l00253"></a>00253 <span class="keyword"> </span>{
<a name="l00254"></a>00254 <span class="keywordflow">return</span>
<a name="l00255"></a>00255 (e.<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>() && e[0] == getExpr()) ||
<a name="l00256"></a>00256 (getExpr().isNot() && getExpr()[0] == e);
<a name="l00257"></a>00257 }
<a name="l00258"></a>00258
<a name="l00259"></a><a class="code" href="classCVC3_1_1Theorem.html#afd8511ead1dfc424a75089f4b4afb95d">00259</a> <span class="keywordtype">bool</span> proves(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e)<span class="keyword"> const</span>
<a name="l00260"></a>00260 <span class="keyword"> </span>{
<a name="l00261"></a>00261 <span class="keywordflow">return</span> getExpr() == e;
<a name="l00262"></a>00262 }
<a name="l00263"></a>00263
<a name="l00264"></a><a class="code" href="classCVC3_1_1Theorem.html#a1d50e47a6c0a1dc6ac9328c5b8e63d1c">00264</a> <span class="keywordtype">bool</span> matches(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e)<span class="keyword"> const</span>
<a name="l00265"></a>00265 <span class="keyword"> </span>{
<a name="l00266"></a>00266 <span class="keywordflow">return</span> proves(e) || refutes(e);
<a name="l00267"></a>00267 }
<a name="l00268"></a>00268
<a name="l00269"></a>00269 <span class="keywordtype">void</span> setCachedValue(<span class="keywordtype">int</span> value) <span class="keyword">const</span>;
<a name="l00270"></a>00270 <span class="keywordtype">int</span> getCachedValue() <span class="keyword">const</span>;
<a name="l00271"></a>00271 <span class="comment"></span>
<a name="l00272"></a>00272 <span class="comment"> /*!@}*/</span> <span class="comment">// End of Attribute methods</span>
<a name="l00273"></a>00273 <span class="comment"></span>
<a name="l00274"></a>00274 <span class="comment"> //! Printing a theorem to a stream, calling it "name".</span>
<a name="l00275"></a>00275 <span class="comment"></span> std::ostream& print(std::ostream& os, <span class="keyword">const</span> std::string& name) <span class="keyword">const</span>;
<a name="l00276"></a>00276
<a name="l00277"></a><a class="code" href="classCVC3_1_1Theorem.html#afde7ac3dde23e989a6df667b6836ecfa">00277</a> <span class="keyword">friend</span> std::ostream& <a class="code" href="classCVC3_1_1Theorem.html#afde7ac3dde23e989a6df667b6836ecfa">operator<<</a>(std::ostream& os, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t) {
<a name="l00278"></a>00278 <span class="keywordflow">return</span> t.<a class="code" href="classCVC3_1_1Theorem.html#af412e1fca4a31f24a63c948f85c18358">print</a>(os, <span class="stringliteral">"Theorem"</span>);
<a name="l00279"></a>00279 }
<a name="l00280"></a>00280
<a name="l00281"></a><a class="code" href="classCVC3_1_1Theorem.html#aaf9a1a9a97d765b069eac3d3460545be">00281</a> <span class="keyword">static</span> <span class="keywordtype">bool</span> <a class="code" href="search__fast_8cpp.html#a262e92a64449205cbd952a704be68952">TheoremEq</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t2)
<a name="l00282"></a>00282 {
<a name="l00283"></a>00283 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!t1.<a class="code" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</a>() && !t2.<a class="code" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</a>(),
<a name="l00284"></a>00284 <span class="stringliteral">"AssumptionsValue() Null Theorem passed to constructor"</span>);
<a name="l00285"></a>00285 <span class="keywordflow">return</span> t1 == t2;
<a name="l00286"></a>00286 }
<a name="l00287"></a>00287 }; <span class="comment">// End of Theorem</span>
<a name="l00288"></a>00288
<a name="l00289"></a>00289 <span class="comment">/*****************************************************************************/</span><span class="comment"></span>
<a name="l00290"></a>00290 <span class="comment">/*!</span>
<a name="l00291"></a>00291 <span class="comment"> *\class Theorem3</span>
<a name="l00292"></a>00292 <span class="comment"> *\brief Theorem3</span>
<a name="l00293"></a>00293 <span class="comment"> *</span>
<a name="l00294"></a>00294 <span class="comment"> * Author: Sergey Berezin</span>
<a name="l00295"></a>00295 <span class="comment"> *</span>
<a name="l00296"></a>00296 <span class="comment"> * Created: Tue Nov 4 17:57:07 2003</span>
<a name="l00297"></a>00297 <span class="comment"> *</span>
<a name="l00298"></a>00298 <span class="comment"> * Implements the 3-valued theorem used for the user assertions and</span>
<a name="l00299"></a>00299 <span class="comment"> * the result of query. It is simply a wrapper around class Theorem,</span>
<a name="l00300"></a>00300 <span class="comment"> * but has a different semantic meaning: the formula may have partial</span>
<a name="l00301"></a>00301 <span class="comment"> * functions and has the Kleene's 3-valued interpretation. The fact</span>
<a name="l00302"></a>00302 <span class="comment"> * that a Theorem3 value is derived means that the TCCs for the</span>
<a name="l00303"></a>00303 <span class="comment"> * formula and all of its assumptions are valid in the current</span>
<a name="l00304"></a>00304 <span class="comment"> * context, and the proofs of TCCs contribute to the set of</span>
<a name="l00305"></a>00305 <span class="comment"> * assumptions.</span>
<a name="l00306"></a>00306 <span class="comment"> */</span>
<a name="l00307"></a>00307 <span class="comment">/*****************************************************************************/</span>
<a name="l00308"></a><a class="code" href="classCVC3_1_1Theorem3.html">00308</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1Theorem3.html" title="Theorem3.">Theorem3</a> {
<a name="l00309"></a>00309 <span class="keyword">private</span>:
<a name="l00310"></a>00310 <span class="comment">// Make a theorem producing class our friend. No definition is</span>
<a name="l00311"></a>00311 <span class="comment">// exposed here.</span>
<a name="l00312"></a><a class="code" href="classCVC3_1_1Theorem3.html#adb16a6e6bad96912c4150299576eaf9a">00312</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1TheoremProducer.html">TheoremProducer</a>;
<a name="l00313"></a>00313
<a name="l00314"></a><a class="code" href="classCVC3_1_1Theorem3.html#ab03f48bf3430eb93d82983dd2bc8a632">00314</a> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1Theorem3.html#ab03f48bf3430eb93d82983dd2bc8a632">d_thm</a>;
<a name="l00315"></a>00315
<a name="l00316"></a><a class="code" href="classCVC3_1_1Theorem3.html#a1d12c9cc45e21f2bef8b4065f23b1ecd">00316</a> <span class="keyword">friend</span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Theorem3.html#a1d12c9cc45e21f2bef8b4065f23b1ecd">operator==</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem3.html" title="Theorem3.">Theorem3</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem3.html" title="Theorem3.">Theorem3</a>& t2) {
<a name="l00317"></a>00317 <span class="keywordflow">return</span> t1.<a class="code" href="classCVC3_1_1Theorem3.html#ab03f48bf3430eb93d82983dd2bc8a632">d_thm</a> == t2.<a class="code" href="classCVC3_1_1Theorem3.html#ab03f48bf3430eb93d82983dd2bc8a632">d_thm</a>;
<a name="l00318"></a>00318 }
<a name="l00319"></a><a class="code" href="classCVC3_1_1Theorem3.html#a08914251eb8cbf0ced80d277a07b6827">00319</a> <span class="keyword">friend</span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Theorem3.html#a08914251eb8cbf0ced80d277a07b6827">operator!=</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem3.html" title="Theorem3.">Theorem3</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem3.html" title="Theorem3.">Theorem3</a>& t2) {
<a name="l00320"></a>00320 <span class="keywordflow">return</span> t1.<a class="code" href="classCVC3_1_1Theorem3.html#ab03f48bf3430eb93d82983dd2bc8a632">d_thm</a> != t2.<a class="code" href="classCVC3_1_1Theorem3.html#ab03f48bf3430eb93d82983dd2bc8a632">d_thm</a>;
<a name="l00321"></a>00321 }
<a name="l00322"></a>00322
<a name="l00323"></a>00323
<a name="l00324"></a>00324 <span class="comment">// Private constructors for a new theorem </span>
<a name="l00325"></a><a class="code" href="classCVC3_1_1Theorem3.html#a1986607c85de1a0550ebe7759bf5b6a4">00325</a> <a class="code" href="classCVC3_1_1Theorem3.html#ae64084287342d9fa9374a4db1981bbd5">Theorem3</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, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a>& assump,
<a name="l00326"></a>00326 <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_1Theorem3.html#aba6e80e63438ef74f027476ca085781a">isAssump</a> = <span class="keyword">false</span>, <span class="keywordtype">int</span> scope = -1)
<a name="l00327"></a>00327 : <a class="code" href="classCVC3_1_1Theorem3.html#ab03f48bf3430eb93d82983dd2bc8a632">d_thm</a>(tm, thm, assump, pf, <a class="code" href="classCVC3_1_1Theorem3.html#aba6e80e63438ef74f027476ca085781a">isAssump</a>, scope) { }
<a name="l00328"></a>00328
<a name="l00329"></a>00329 <span class="comment">// Constructors for rewrite theorems. These use a special efficient</span>
<a name="l00330"></a>00330 <span class="comment">// subclass of TheoremValue for theorems which represent rewrites:</span>
<a name="l00331"></a>00331 <span class="comment">// A |- t = t' or A |- phi iff phi'</span>
<a name="l00332"></a><a class="code" href="classCVC3_1_1Theorem3.html#a5495a662364c65492dceb1108a45d55c">00332</a> <a class="code" href="classCVC3_1_1Theorem3.html#ae64084287342d9fa9374a4db1981bbd5">Theorem3</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="l00333"></a>00333 <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)
<a name="l00334"></a>00334 : <a class="code" href="classCVC3_1_1Theorem3.html#ab03f48bf3430eb93d82983dd2bc8a632">d_thm</a>(tm, lhs, rhs, assump, pf) { }
<a name="l00335"></a>00335
<a name="l00336"></a>00336 <span class="keyword">public</span>:
<a name="l00337"></a>00337 <span class="comment">// recusive function to print theorems and all assumptions recursively</span>
<a name="l00338"></a>00338 <span class="comment">// important: this function will corrupt all flags!! so exercise </span>
<a name="l00339"></a>00339 <span class="comment">// caution when using in any graph traversals </span>
<a name="l00340"></a>00340 <span class="comment">// (probably more useful to call it only before a crash)</span>
<a name="l00341"></a><a class="code" href="classCVC3_1_1Theorem3.html#ab7984ea5eb9c9bdba751fc9ea9d6cc90">00341</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Theorem3.html#ab7984ea5eb9c9bdba751fc9ea9d6cc90">printDebug</a>()<span class="keyword"> const </span>{ <a class="code" href="classCVC3_1_1Theorem3.html#ab03f48bf3430eb93d82983dd2bc8a632">d_thm</a>.<a class="code" href="classCVC3_1_1Theorem.html#ad9da69b34ab2bab4192e5977e5c10498">printDebug</a>(); }
<a name="l00342"></a>00342
<a name="l00343"></a>00343 <span class="comment">// Default constructor creates Null theorem to allow untrusted</span>
<a name="l00344"></a>00344 <span class="comment">// code declare local vars without initialization (vector<Theorem></span>
<a name="l00345"></a>00345 <span class="comment">// may need that, for instance).</span>
<a name="l00346"></a><a class="code" href="classCVC3_1_1Theorem3.html#ae64084287342d9fa9374a4db1981bbd5">00346</a> <a class="code" href="classCVC3_1_1Theorem3.html#ae64084287342d9fa9374a4db1981bbd5">Theorem3</a>() { }
<a name="l00347"></a>00347
<a name="l00348"></a>00348 <span class="comment">// Destructor</span>
<a name="l00349"></a><a class="code" href="classCVC3_1_1Theorem3.html#a55e28790faec403ea8a9a0b5a718eab1">00349</a> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem3.html#a55e28790faec403ea8a9a0b5a718eab1">~Theorem3</a>() { }
<a name="l00350"></a>00350
<a name="l00351"></a><a class="code" href="classCVC3_1_1Theorem3.html#a1f2b0509853067114494079f955de741">00351</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Theorem3.html#a1f2b0509853067114494079f955de741">isNull</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Theorem3.html#ab03f48bf3430eb93d82983dd2bc8a632">d_thm</a>.<a class="code" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</a>(); }
<a name="l00352"></a>00352
<a name="l00353"></a>00353 <span class="comment">// True if theorem is of the form t=t' or phi iff phi'</span>
<a name="l00354"></a><a class="code" href="classCVC3_1_1Theorem3.html#ace6f5dda051da7db8a4adf74a723852c">00354</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Theorem3.html#ace6f5dda051da7db8a4adf74a723852c">isRewrite</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Theorem3.html#ab03f48bf3430eb93d82983dd2bc8a632">d_thm</a>.<a class="code" href="classCVC3_1_1Theorem.html#a362c1d70e03803d804bbe300e5f6dc87">isRewrite</a>(); }
<a name="l00355"></a><a class="code" href="classCVC3_1_1Theorem3.html#aba6e80e63438ef74f027476ca085781a">00355</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Theorem3.html#aba6e80e63438ef74f027476ca085781a">isAssump</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Theorem3.html#ab03f48bf3430eb93d82983dd2bc8a632">d_thm</a>.<a class="code" href="classCVC3_1_1Theorem.html#a05282db6832afb4f198d8c6b2b67aeb1">isAssump</a>(); }
<a name="l00356"></a>00356
<a name="l00357"></a>00357 <span class="comment">// Return the theorem value as an Expr</span>
<a name="l00358"></a><a class="code" href="classCVC3_1_1Theorem3.html#a744788782cc996d5b914533fe7304352">00358</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1Theorem3.html#a744788782cc996d5b914533fe7304352">getExpr</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Theorem3.html#ab03f48bf3430eb93d82983dd2bc8a632">d_thm</a>.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>(); }
<a name="l00359"></a><a class="code" href="classCVC3_1_1Theorem3.html#a86b1b2342e05df0b6c965df22ac6bdc5">00359</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_1Theorem3.html#a86b1b2342e05df0b6c965df22ac6bdc5">getLHS</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Theorem3.html#ab03f48bf3430eb93d82983dd2bc8a632">d_thm</a>.<a class="code" href="classCVC3_1_1Theorem.html#a206c04f39fbbcacef2337148675553f4">getLHS</a>(); }
<a name="l00360"></a><a class="code" href="classCVC3_1_1Theorem3.html#a1da681e13e1dd2bfefb0d21027e20eb6">00360</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_1Theorem3.html#a1da681e13e1dd2bfefb0d21027e20eb6">getRHS</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Theorem3.html#ab03f48bf3430eb93d82983dd2bc8a632">d_thm</a>.<a class="code" href="classCVC3_1_1Theorem.html#a97d957fcbf9094480851b1d2e5d3729f">getRHS</a>(); }
<a name="l00361"></a>00361
<a name="l00362"></a>00362 <span class="comment">// Return the assumptions.</span>
<a name="l00363"></a>00363 <span class="comment">// It's an error if called while running without assumptions.</span>
<a name="l00364"></a>00364 <span class="comment">// void getAssumptions(Assumptions& a) const { d_thm.getAssumptions(a); }</span>
<a name="l00365"></a><a class="code" href="classCVC3_1_1Theorem3.html#a3bf0a31a2adaabfd7a37d61e990fa9ea">00365</a> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a>& <a class="code" href="classCVC3_1_1Theorem3.html#a3bf0a31a2adaabfd7a37d61e990fa9ea">getAssumptionsRef</a>()<span class="keyword"> const </span>{
<a name="l00366"></a>00366 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Theorem3.html#ab03f48bf3430eb93d82983dd2bc8a632">d_thm</a>.<a class="code" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a>();
<a name="l00367"></a>00367 }
<a name="l00368"></a>00368 <span class="comment">// Return the proof of the theorem. If running without proofs,</span>
<a name="l00369"></a>00369 <span class="comment">// return the Null proof.</span>
<a name="l00370"></a><a class="code" href="classCVC3_1_1Theorem3.html#a05c74972ebc3932829fa32ca237880db">00370</a> <a class="code" href="classCVC3_1_1Proof.html">Proof</a> <a class="code" href="classCVC3_1_1Theorem3.html#a05c74972ebc3932829fa32ca237880db">getProof</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Theorem3.html#ab03f48bf3430eb93d82983dd2bc8a632">d_thm</a>.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>(); }
<a name="l00371"></a>00371
<a name="l00372"></a>00372 <span class="comment">// Return the lowest scope level at which this theorem is valid.</span>
<a name="l00373"></a>00373 <span class="comment">// Value -1 means no information is available.</span>
<a name="l00374"></a><a class="code" href="classCVC3_1_1Theorem3.html#a153b7d792f901a481d1eb4c91c885330">00374</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1Theorem3.html#a153b7d792f901a481d1eb4c91c885330">getScope</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Theorem3.html#ab03f48bf3430eb93d82983dd2bc8a632">d_thm</a>.<a class="code" href="classCVC3_1_1Theorem.html#a112466d9793abcf97015233ffdc4ec5e">getScope</a>(); }
<a name="l00375"></a>00375
<a name="l00376"></a>00376 <span class="comment">// Test if we are running in a proof production mode and with assumptions</span>
<a name="l00377"></a><a class="code" href="classCVC3_1_1Theorem3.html#a099ac3dc23ce274b26a25cd9e5059502">00377</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Theorem3.html#a099ac3dc23ce274b26a25cd9e5059502">withProof</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Theorem3.html#ab03f48bf3430eb93d82983dd2bc8a632">d_thm</a>.<a class="code" href="classCVC3_1_1Theorem.html#ad4573ca6be017cab3c83d28c2dbcebd8">withProof</a>(); }
<a name="l00378"></a><a class="code" href="classCVC3_1_1Theorem3.html#a49abf6d71c6190f1400b5146b61b0872">00378</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Theorem3.html#a49abf6d71c6190f1400b5146b61b0872">withAssumptions</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Theorem3.html#ab03f48bf3430eb93d82983dd2bc8a632">d_thm</a>.<a class="code" href="classCVC3_1_1Theorem.html#a90349125fe644e8a075e1a47a49872c7">withAssumptions</a>(); }
<a name="l00379"></a>00379
<a name="l00380"></a>00380 <span class="comment">// Printing</span>
<a name="l00381"></a>00381 std::string <a class="code" href="classCVC3_1_1Theorem3.html#a3712f50eb83d3b485aab55f660bed77a">toString</a>() <span class="keyword">const</span>;
<a name="l00382"></a>00382
<a name="l00383"></a>00383 <span class="comment">// For debugging</span>
<a name="l00384"></a><a class="code" href="classCVC3_1_1Theorem3.html#a4a2253b9fa2508aedd3dded623e283ad">00384</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Theorem3.html#a4a2253b9fa2508aedd3dded623e283ad">printx</a>()<span class="keyword"> const </span>{ <a class="code" href="classCVC3_1_1Theorem3.html#ab03f48bf3430eb93d82983dd2bc8a632">d_thm</a>.<a class="code" href="classCVC3_1_1Theorem.html#aeb41e125749338e05d680beca6df9ee4">printx</a>(); }
<a name="l00385"></a><a class="code" href="classCVC3_1_1Theorem3.html#ababd51a0131a57f96c0316f7f8f2a6c9">00385</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Theorem3.html#ababd51a0131a57f96c0316f7f8f2a6c9">print</a>()<span class="keyword"> const </span>{ <a class="code" href="classCVC3_1_1Theorem3.html#ab03f48bf3430eb93d82983dd2bc8a632">d_thm</a>.<a class="code" href="classCVC3_1_1Theorem.html#af412e1fca4a31f24a63c948f85c18358">print</a>(); }
<a name="l00386"></a>00386 <span class="comment"></span>
<a name="l00387"></a>00387 <span class="comment"> //! Check if the theorem is a literal</span>
<a name="l00388"></a><a class="code" href="classCVC3_1_1Theorem3.html#a31be5df9f946e3a6f2a75f673db863cb">00388</a> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Theorem3.html#a31be5df9f946e3a6f2a75f673db863cb" title="Check if the theorem is a literal.">isAbsLiteral</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Theorem3.html#ab03f48bf3430eb93d82983dd2bc8a632">d_thm</a>.<a class="code" href="classCVC3_1_1Theorem.html#aed1590a02166f6099e5538dbf681a60c" title="Check if the theorem is a literal.">isAbsLiteral</a>(); }
<a name="l00389"></a>00389
<a name="l00390"></a><a class="code" href="classCVC3_1_1Theorem3.html#af5109554e84f3a7b92eea93606cbc7bc">00390</a> <span class="keyword">friend</span> std::ostream& <a class="code" href="classCVC3_1_1Theorem3.html#af5109554e84f3a7b92eea93606cbc7bc">operator<<</a>(std::ostream& os, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem3.html" title="Theorem3.">Theorem3</a>& t) {
<a name="l00391"></a>00391 <span class="keywordflow">return</span> t.<a class="code" href="classCVC3_1_1Theorem3.html#ab03f48bf3430eb93d82983dd2bc8a632">d_thm</a>.<a class="code" href="classCVC3_1_1Theorem.html#af412e1fca4a31f24a63c948f85c18358">print</a>(os, <span class="stringliteral">"Theorem3"</span>);
<a name="l00392"></a>00392 }
<a name="l00393"></a>00393 }; <span class="comment">// End of Theorem3</span>
<a name="l00394"></a>00394 <span class="comment"></span>
<a name="l00395"></a>00395 <span class="comment"> //! "Less" comparator for theorems by TheoremValue pointers</span>
<a name="l00396"></a><a class="code" href="classCVC3_1_1TheoremLess.html">00396</a> <span class="comment"></span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1TheoremLess.html" title=""Less" comparator for theorems by TheoremValue pointers">TheoremLess</a> {
<a name="l00397"></a>00397 <span class="keyword">public</span>:
<a name="l00398"></a><a class="code" href="classCVC3_1_1TheoremLess.html#a2a853c2c34833645b058c4c07b21fcc2">00398</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoremLess.html#a2a853c2c34833645b058c4c07b21fcc2">operator()</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t2)<span class="keyword"> const </span>{
<a name="l00399"></a>00399 <span class="keywordflow">return</span> (<a class="code" href="namespaceCVC3.html#af87b5038044e2f5706e30e5ed6f7584e">compareByPtr</a>(t1, t2) < 0);
<a name="l00400"></a>00400 }
<a name="l00401"></a>00401 };
<a name="l00402"></a><a class="code" href="namespaceCVC3.html#ae8220d283ddfdaa8f4e0da0a03fa7ff4">00402</a> <span class="keyword">typedef</span> std::map<Theorem,bool, TheoremLess> <a class="code" href="namespaceCVC3.html#ae8220d283ddfdaa8f4e0da0a03fa7ff4">TheoremMap</a>;
<a name="l00403"></a>00403
<a name="l00404"></a><a class="code" href="classCVC3_1_1Theorem.html#ac4b1c9570ffb9cc901627ef2abb9ff77">00404</a> <span class="keyword">inline</span> std::string <a class="code" href="classCVC3_1_1Theorem.html#ac4b1c9570ffb9cc901627ef2abb9ff77">Theorem::toString</a>()<span class="keyword"> const </span>{
<a name="l00405"></a>00405 std::ostringstream ss;
<a name="l00406"></a>00406 ss << (*this);
<a name="l00407"></a>00407 <span class="keywordflow">return</span> ss.str();
<a name="l00408"></a>00408 }
<a name="l00409"></a>00409
<a name="l00410"></a><a class="code" href="classCVC3_1_1Theorem3.html#a3712f50eb83d3b485aab55f660bed77a">00410</a> <span class="keyword">inline</span> std::string <a class="code" href="classCVC3_1_1Theorem3.html#a3712f50eb83d3b485aab55f660bed77a">Theorem3::toString</a>()<span class="keyword"> const </span>{
<a name="l00411"></a>00411 std::ostringstream ss;
<a name="l00412"></a>00412 ss << (*this);
<a name="l00413"></a>00413 <span class="keywordflow">return</span> ss.str();
<a name="l00414"></a>00414 }
<a name="l00415"></a>00415
<a name="l00416"></a>00416 <span class="comment">// Merge assumptions from different theorems</span>
<a name="l00417"></a>00417 <span class="comment">// inline Assumptions merge(const Theorem& t1, const Theorem& t2) {</span>
<a name="l00418"></a>00418 <span class="comment">// return Assumptions(t1, t2);</span>
<a name="l00419"></a>00419 <span class="comment">// }</span>
<a name="l00420"></a>00420 <span class="comment">// inline void merge(Assumptions& a, const Theorem& t) {</span>
<a name="l00421"></a>00421 <span class="comment">// a.add(t);</span>
<a name="l00422"></a>00422 <span class="comment">// }</span>
<a name="l00423"></a>00423 <span class="comment">// inline Assumptions merge(const std::vector<Theorem>& t) {</span>
<a name="l00424"></a>00424 <span class="comment">// return Assumptions(t);</span>
<a name="l00425"></a>00425 <span class="comment">// }</span>
<a name="l00426"></a>00426
<a name="l00427"></a><a class="code" href="namespaceCVC3.html#a5d869d6f1c2d4780875deea3828247e1">00427</a> <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#ad3e3964a0b8cd9e2749de47b053b9d97">operator<</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t2)
<a name="l00428"></a>00428 { <span class="keywordflow">return</span> <a class="code" href="namespaceCVC3.html#ac06ac2fd4db699104b790f98b7abba71">compare</a>(t1, t2) < 0; }
<a name="l00429"></a><a class="code" href="namespaceCVC3.html#a3f7d84a4848e35fdefb0cf032716139c">00429</a> <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#abccc88aac4f7652def737f1081dc7a89">operator<=</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t2)
<a name="l00430"></a>00430 { <span class="keywordflow">return</span> <a class="code" href="namespaceCVC3.html#ac06ac2fd4db699104b790f98b7abba71">compare</a>(t1, t2) <= 0; }
<a name="l00431"></a><a class="code" href="namespaceCVC3.html#aafc08e614f90df8f0d23503c3fe13ef4">00431</a> <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#a0d82fd3eb68860cbd01ae86b2b9e3c66">operator></a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t2)
<a name="l00432"></a>00432 { <span class="keywordflow">return</span> <a class="code" href="namespaceCVC3.html#ac06ac2fd4db699104b790f98b7abba71">compare</a>(t1, t2) > 0; }
<a name="l00433"></a><a class="code" href="namespaceCVC3.html#a7d4b62b76a23fdc6b341f9f8c6a3aa4c">00433</a> <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#af997ba8407b661bf2ffe2cb6f52c3e3b">operator>=</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t2)
<a name="l00434"></a>00434 { <span class="keywordflow">return</span> <a class="code" href="namespaceCVC3.html#ac06ac2fd4db699104b790f98b7abba71">compare</a>(t1, t2) >= 0; }
<a name="l00435"></a>00435
<a name="l00436"></a>00436 } <span class="comment">// end of namespace CVC3</span>
<a name="l00437"></a>00437
<a name="l00438"></a>00438 <span class="preprocessor">#include "<a class="code" href="hash__fun_8h.html" title="hash functions">hash_fun.h</a>"</span>
<a name="l00439"></a>00439 <span class="keyword">namespace </span>Hash
<a name="l00440"></a>00440 {
<a name="l00441"></a>00441
<a name="l00442"></a><a class="code" href="structHash_1_1hash_3_01CVC3_1_1Theorem_01_4.html">00442</a> <span class="keyword">template</span><> <span class="keyword">struct </span><a class="code" href="structHash_1_1hash.html">hash</a><CVC3::Theorem>
<a name="l00443"></a>00443 {
<a name="l00444"></a><a class="code" href="structHash_1_1hash_3_01CVC3_1_1Theorem_01_4.html#a4bfe0bdb897f6190c56153b4bdf2f97e">00444</a> <span class="keywordtype">size_t</span> <a class="code" href="structHash_1_1hash_3_01CVC3_1_1Theorem_01_4.html#a4bfe0bdb897f6190c56153b4bdf2f97e">operator()</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a>& e)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> e.<a class="code" href="classCVC3_1_1Theorem.html#abe268eaf2b89ffdc4ccb291c0a2eaeb9">hash</a>(); }
<a name="l00445"></a>00445 };
<a name="l00446"></a>00446
<a name="l00447"></a>00447 }
<a name="l00448"></a>00448
<a name="l00449"></a>00449 <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>
