<!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"/>
<meta http-equiv="X-UA-Compatible" content="IE=9"/>
<title>CVC3: common_proof_rules.h Source File</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="jquery.js"></script>
<script type="text/javascript" src="dynsections.js"></script>
<link href="doxygen.css" rel="stylesheet" type="text/css" />
</head>
<body>
<div id="top"><!-- do not remove this div, it is closed by doxygen! -->
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3
</div>
</td>
</tr>
</tbody>
</table>
</div>
<!-- end header part -->
<!-- Generated by Doxygen 1.8.2 -->
<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 id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="dir_68267d1309a1af8e8297ef4c3efbcdba.html">src</a></li><li class="navelem"><a class="el" href="dir_b0856f6b0d80ccb263b2f415c91f9e17.html">include</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="headertitle">
<div class="title">common_proof_rules.h</div> </div>
</div><!--header-->
<div class="contents">
<a href="common__proof__rules_8h.html">Go to the documentation of this file.</a><div class="fragment"><div class="line"><a name="l00001"></a><span class="lineno"> 1</span> <span class="comment">/*****************************************************************************/</span><span class="comment"></span></div>
<div class="line"><a name="l00002"></a><span class="lineno"> 2</span> <span class="comment">/*!</span></div>
<div class="line"><a name="l00003"></a><span class="lineno"> 3</span> <span class="comment"> * \file common_proof_rules.h</span></div>
<div class="line"><a name="l00004"></a><span class="lineno"> 4</span> <span class="comment"> * </span></div>
<div class="line"><a name="l00005"></a><span class="lineno"> 5</span> <span class="comment"> * Author: Sergey Berezin</span></div>
<div class="line"><a name="l00006"></a><span class="lineno"> 6</span> <span class="comment"> * </span></div>
<div class="line"><a name="l00007"></a><span class="lineno"> 7</span> <span class="comment"> * Created: Dec 11 18:15:37 GMT 2002</span></div>
<div class="line"><a name="l00008"></a><span class="lineno"> 8</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00009"></a><span class="lineno"> 9</span> <span class="comment"> * <hr></span></div>
<div class="line"><a name="l00010"></a><span class="lineno"> 10</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00011"></a><span class="lineno"> 11</span> <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span></div>
<div class="line"><a name="l00012"></a><span class="lineno"> 12</span> <span class="comment"> * and its documentation for any purpose is hereby granted without</span></div>
<div class="line"><a name="l00013"></a><span class="lineno"> 13</span> <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span></div>
<div class="line"><a name="l00014"></a><span class="lineno"> 14</span> <span class="comment"> * LICENSE file provided with this distribution.</span></div>
<div class="line"><a name="l00015"></a><span class="lineno"> 15</span> <span class="comment"> * </span></div>
<div class="line"><a name="l00016"></a><span class="lineno"> 16</span> <span class="comment"> * <hr></span></div>
<div class="line"><a name="l00017"></a><span class="lineno"> 17</span> <span class="comment"> * </span></div>
<div class="line"><a name="l00018"></a><span class="lineno"> 18</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00019"></a><span class="lineno"> 19</span> <span class="comment">/*****************************************************************************/</span></div>
<div class="line"><a name="l00020"></a><span class="lineno"> 20</span> <span class="comment">// CLASS: CommonProofRules</span></div>
<div class="line"><a name="l00021"></a><span class="lineno"> 21</span> <span class="comment">//</span></div>
<div class="line"><a name="l00022"></a><span class="lineno"> 22</span> <span class="comment">// AUTHOR: Sergey Berezin, 12/09/2002</span></div>
<div class="line"><a name="l00023"></a><span class="lineno"> 23</span> <span class="comment">//</span></div>
<div class="line"><a name="l00024"></a><span class="lineno"> 24</span> <span class="comment">// Description: Commonly used proof rules (reflexivity, symmetry,</span></div>
<div class="line"><a name="l00025"></a><span class="lineno"> 25</span> <span class="comment">// transitivity, substitutivity, etc.).</span></div>
<div class="line"><a name="l00026"></a><span class="lineno"> 26</span> <span class="comment">//</span></div>
<div class="line"><a name="l00027"></a><span class="lineno"> 27</span> <span class="comment">// Normally, proof rule interfaces belong to their decision</span></div>
<div class="line"><a name="l00028"></a><span class="lineno"> 28</span> <span class="comment">// procedures. However, in the case of equational logic, the rules</span></div>
<div class="line"><a name="l00029"></a><span class="lineno"> 29</span> <span class="comment">// are so useful, that even some basic classes like Transformer use</span></div>
<div class="line"><a name="l00030"></a><span class="lineno"> 30</span> <span class="comment">// these rules under the hood. Therefore, it is made public, and its</span></div>
<div class="line"><a name="l00031"></a><span class="lineno"> 31</span> <span class="comment">// implementation is provided by the 'theorem' module.</span><span class="comment"></span></div>
<div class="line"><a name="l00032"></a><span class="lineno"> 32</span> <span class="comment">///////////////////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00033"></a><span class="lineno"> 33</span> <span class="comment"></span></div>
<div class="line"><a name="l00034"></a><span class="lineno"> 34</span> <span class="preprocessor">#ifndef _cvc3__common_proof_rules_h_</span></div>
<div class="line"><a name="l00035"></a><span class="lineno"> 35</span> <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__common_proof_rules_h_</span></div>
<div class="line"><a name="l00036"></a><span class="lineno"> 36</span> <span class="preprocessor"></span></div>
<div class="line"><a name="l00037"></a><span class="lineno"> 37</span> <span class="preprocessor">#include <vector></span></div>
<div class="line"><a name="l00038"></a><span class="lineno"> 38</span> </div>
<div class="line"><a name="l00039"></a><span class="lineno"> 39</span> <span class="keyword">namespace </span>CVC3 {</div>
<div class="line"><a name="l00040"></a><span class="lineno"> 40</span> </div>
<div class="line"><a name="l00041"></a><span class="lineno"> 41</span>  <span class="keyword">class </span>Theorem;</div>
<div class="line"><a name="l00042"></a><span class="lineno"> 42</span>  <span class="keyword">class </span>Theorem3;</div>
<div class="line"><a name="l00043"></a><span class="lineno"> 43</span>  <span class="keyword">class </span>Expr;</div>
<div class="line"><a name="l00044"></a><span class="lineno"> 44</span>  <span class="keyword">class </span>Op;</div>
<div class="line"><a name="l00045"></a><span class="lineno"> 45</span> </div>
<div class="line"><a name="l00046"></a><span class="lineno"><a class="code" href="classCVC3_1_1CommonProofRules.html"> 46</a></span>  <span class="keyword">class </span><a class="code" href="classCVC3_1_1CommonProofRules.html">CommonProofRules</a> {</div>
<div class="line"><a name="l00047"></a><span class="lineno"> 47</span>  <span class="keyword">public</span>:<span class="comment"></span></div>
<div class="line"><a name="l00048"></a><span class="lineno"> 48</span> <span class="comment"> //! Destructor</span></div>
<div class="line"><a name="l00049"></a><span class="lineno"><a class="code" href="classCVC3_1_1CommonProofRules.html#a334ad50333e9323968df2bc286de7a8f"> 49</a></span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1CommonProofRules.html#a334ad50333e9323968df2bc286de7a8f" title="Destructor.">~CommonProofRules</a>() { }</div>
<div class="line"><a name="l00050"></a><span class="lineno"> 50</span> <span class="comment"></span></div>
<div class="line"><a name="l00051"></a><span class="lineno"> 51</span> <span class="comment"> ////////////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00052"></a><span class="lineno"> 52</span> <span class="comment"></span> <span class="comment">// TCC rules (3-valued logic)</span><span class="comment"></span></div>
<div class="line"><a name="l00053"></a><span class="lineno"> 53</span> <span class="comment"> ////////////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00054"></a><span class="lineno"> 54</span> <span class="comment"></span></div>
<div class="line"><a name="l00055"></a><span class="lineno"> 55</span>  <span class="comment">// G1 |- phi G2 |- D_phi</span></div>
<div class="line"><a name="l00056"></a><span class="lineno"> 56</span>  <span class="comment">// -------------------------</span></div>
<div class="line"><a name="l00057"></a><span class="lineno"> 57</span>  <span class="comment">// G1,G2 |-_3 phi</span><span class="comment"></span></div>
<div class="line"><a name="l00058"></a><span class="lineno"> 58</span> <span class="comment"> /*!</span></div>
<div class="line"><a name="l00059"></a><span class="lineno"> 59</span> <span class="comment"> * @brief Convert 2-valued formula to 3-valued by discharging its</span></div>
<div class="line"><a name="l00060"></a><span class="lineno"> 60</span> <span class="comment"> * TCC (\f$D_\phi\f$):</span></div>
<div class="line"><a name="l00061"></a><span class="lineno"> 61</span> <span class="comment"> * \f[\frac{\Gamma_1\vdash_2 \phi\quad \Gamma_2\vdash_2 D_{\phi}}</span></div>
<div class="line"><a name="l00062"></a><span class="lineno"> 62</span> <span class="comment"> * {\Gamma_1,\,\Gamma_2\vdash_3\phi}\f]</span></div>
<div class="line"><a name="l00063"></a><span class="lineno"> 63</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00064"></a><span class="lineno"> 64</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem3.html" title="Theorem3.">Theorem3</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a758fe978ff00099419c459914a0af5ba" title="Convert 2-valued formula to 3-valued by discharging its TCC ( ): .">queryTCC</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& phi, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& D_phi) = 0;</div>
<div class="line"><a name="l00065"></a><span class="lineno"> 65</span> </div>
<div class="line"><a name="l00066"></a><span class="lineno"> 66</span>  <span class="comment">// G0,a1,...,an |-_3 phi G1 |- D_a1 ... Gn |- D_an</span></div>
<div class="line"><a name="l00067"></a><span class="lineno"> 67</span>  <span class="comment">// -------------------------------------------------</span></div>
<div class="line"><a name="l00068"></a><span class="lineno"> 68</span>  <span class="comment">// G0,G1,...,Gn |-_3 (a1 & ... & an) -> phi</span><span class="comment"></span></div>
<div class="line"><a name="l00069"></a><span class="lineno"> 69</span> <span class="comment"> /*!</span></div>
<div class="line"><a name="l00070"></a><span class="lineno"> 70</span> <span class="comment"> * @brief 3-valued implication introduction rule:</span></div>
<div class="line"><a name="l00071"></a><span class="lineno"> 71</span> <span class="comment"> * \f[\frac{\Gamma_0,\,\alpha_1\,\ldots,\,\alpha_n\vdash_3\phi\quad</span></div>
<div class="line"><a name="l00072"></a><span class="lineno"> 72</span> <span class="comment"> * (\Gamma_i\vdash D_{\alpha_i})_{i\in[1..n]}}</span></div>
<div class="line"><a name="l00073"></a><span class="lineno"> 73</span> <span class="comment"> * {\Gamma_0,\,\Gamma_1, \ldots, \Gamma_n\vdash_3</span></div>
<div class="line"><a name="l00074"></a><span class="lineno"> 74</span> <span class="comment"> * (\bigwedge_{i=1}^n\alpha_i)\to\phi}\f]</span></div>
<div class="line"><a name="l00075"></a><span class="lineno"> 75</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00076"></a><span class="lineno"> 76</span> <span class="comment"> * \param phi is the formula \f$\phi\f$</span></div>
<div class="line"><a name="l00077"></a><span class="lineno"> 77</span> <span class="comment"> * \param assump is the vector of assumptions \f$\alpha_1\ldots\alpha_n\f$</span></div>
<div class="line"><a name="l00078"></a><span class="lineno"> 78</span> <span class="comment"> * \param tccs is the vector of TCCs for assumptions</span></div>
<div class="line"><a name="l00079"></a><span class="lineno"> 79</span> <span class="comment"> * \f$D_{\alpha_1}\ldots D_{\alpha_n}\f$</span></div>
<div class="line"><a name="l00080"></a><span class="lineno"> 80</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00081"></a><span class="lineno"> 81</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem3.html" title="Theorem3.">Theorem3</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#afe561cfd6d5ee752fbc1c3cafe9b68a5" title="3-valued implication introduction rule: ">implIntro3</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem3.html" title="Theorem3.">Theorem3</a>& phi,</div>
<div class="line"><a name="l00082"></a><span class="lineno"> 82</span>  <span class="keyword">const</span> std::vector<Expr>& assump,</div>
<div class="line"><a name="l00083"></a><span class="lineno"> 83</span>  <span class="keyword">const</span> std::vector<Theorem>& tccs) = 0;</div>
<div class="line"><a name="l00084"></a><span class="lineno"> 84</span> <span class="comment"></span></div>
<div class="line"><a name="l00085"></a><span class="lineno"> 85</span> <span class="comment"> ////////////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00086"></a><span class="lineno"> 86</span> <span class="comment"></span> <span class="comment">// Common rules</span><span class="comment"></span></div>
<div class="line"><a name="l00087"></a><span class="lineno"> 87</span> <span class="comment"> ////////////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00088"></a><span class="lineno"> 88</span> <span class="comment"></span></div>
<div class="line"><a name="l00089"></a><span class="lineno"> 89</span>  <span class="comment">// ==> u:a |- a</span><span class="comment"></span></div>
<div class="line"><a name="l00090"></a><span class="lineno"> 90</span> <span class="comment"> //! \f[\frac{}{a\vdash a}\f]</span></div>
<div class="line"><a name="l00091"></a><span class="lineno"> 91</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#ab4527c48e9f88d94d7ca076757a6f3ba">assumpRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& a, <span class="keywordtype">int</span> scope = -1) = 0;</div>
<div class="line"><a name="l00092"></a><span class="lineno"> 92</span> </div>
<div class="line"><a name="l00093"></a><span class="lineno"> 93</span>  <span class="comment">// ==> a == a or ==> a IFF a</span><span class="comment"></span></div>
<div class="line"><a name="l00094"></a><span class="lineno"> 94</span> <span class="comment"> //! \f[\frac{}{a = a}\quad or \quad\frac{}{a \Leftrightarrow a}\f]</span></div>
<div class="line"><a name="l00095"></a><span class="lineno"> 95</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a61c1fe56b4ed9744006883a7784ddb71">reflexivityRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& a) = 0;</div>
<div class="line"><a name="l00096"></a><span class="lineno"> 96</span> <span class="comment"></span></div>
<div class="line"><a name="l00097"></a><span class="lineno"> 97</span> <span class="comment"> //! ==> (a == a) IFF TRUE</span></div>
<div class="line"><a name="l00098"></a><span class="lineno"> 98</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#ad078b5d25129b200fe04b20c5962aa34" title="==> (a == a) IFF TRUE">rewriteReflexivity</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& a_eq_a) = 0;</div>
<div class="line"><a name="l00099"></a><span class="lineno"> 99</span> </div>
<div class="line"><a name="l00100"></a><span class="lineno"> 100</span>  <span class="comment">// a1 == a2 ==> a2 == a1 (same for IFF)</span><span class="comment"></span></div>
<div class="line"><a name="l00101"></a><span class="lineno"> 101</span> <span class="comment"> //! \f[\frac{a_1=a_2}{a_2=a_1}\f] (same for IFF)</span></div>
<div class="line"><a name="l00102"></a><span class="lineno"> 102</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a0a87e88508f49b73037e0024afa841bf" title=" (same for IFF)">symmetryRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& a1_eq_a2) = 0;</div>
<div class="line"><a name="l00103"></a><span class="lineno"> 103</span> </div>
<div class="line"><a name="l00104"></a><span class="lineno"> 104</span>  <span class="comment">// ==> (a1 == a2) IFF (a2 == a1)</span><span class="comment"></span></div>
<div class="line"><a name="l00105"></a><span class="lineno"> 105</span> <span class="comment"> //! \f[\frac{}{(a_1=a_2)\Leftrightarrow (a_2=a_1)}\f]</span></div>
<div class="line"><a name="l00106"></a><span class="lineno"> 106</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a338cafc978d9b6a447e8d58af42d7e5b">rewriteUsingSymmetry</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& a1_eq_a2) = 0;</div>
<div class="line"><a name="l00107"></a><span class="lineno"> 107</span> </div>
<div class="line"><a name="l00108"></a><span class="lineno"> 108</span>  <span class="comment">// (a1 == a2) & (a2 == a3) ==> (a1 == a3) [same for IFF]</span><span class="comment"></span></div>
<div class="line"><a name="l00109"></a><span class="lineno"> 109</span> <span class="comment"> //! \f[\frac{a_1=a_2\quad a_2=a_3}{a_1=a_3}\f] (same for IFF)</span></div>
<div class="line"><a name="l00110"></a><span class="lineno"> 110</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a4a4e90cd69ce24e83ba2c217907c277a" title=" (same for IFF)">transitivityRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& a1_eq_a2,</div>
<div class="line"><a name="l00111"></a><span class="lineno"> 111</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& a2_eq_a3) = 0;</div>
<div class="line"><a name="l00112"></a><span class="lineno"> 112</span> <span class="comment"></span></div>
<div class="line"><a name="l00113"></a><span class="lineno"> 113</span> <span class="comment"> //! Optimized case for expr with one child</span></div>
<div class="line"><a name="l00114"></a><span class="lineno"> 114</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a776c827bb6e3b889234429c49ae9ad6f" title="Optimized case for expr with one child.">substitutivityRule</a>(<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 class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm) = 0;</div>
<div class="line"><a name="l00115"></a><span class="lineno"> 115</span> <span class="comment"></span></div>
<div class="line"><a name="l00116"></a><span class="lineno"> 116</span> <span class="comment"> //! Optimized case for expr with two children</span></div>
<div class="line"><a name="l00117"></a><span class="lineno"> 117</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a776c827bb6e3b889234429c49ae9ad6f" title="Optimized case for expr with one child.">substitutivityRule</a>(<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 class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm1,</div>
<div class="line"><a name="l00118"></a><span class="lineno"> 118</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm2) = 0;</div>
<div class="line"><a name="l00119"></a><span class="lineno"> 119</span> </div>
<div class="line"><a name="l00120"></a><span class="lineno"> 120</span>  <span class="comment">// (c_1 == d_1) & ... & (c_n == d_n)</span></div>
<div class="line"><a name="l00121"></a><span class="lineno"> 121</span>  <span class="comment">// ==> op(c_1,...,c_n) == op(d_1,...,d_n)</span><span class="comment"></span></div>
<div class="line"><a name="l00122"></a><span class="lineno"> 122</span> <span class="comment"> /*! @brief </span></div>
<div class="line"><a name="l00123"></a><span class="lineno"> 123</span> <span class="comment"> \f[\frac{(c_1=d_1)\wedge\ldots\wedge(c_n=d_n)}</span></div>
<div class="line"><a name="l00124"></a><span class="lineno"> 124</span> <span class="comment"> {op(c_1,\ldots,c_n)=op(d_1,\ldots,d_n)}\f]</span></div>
<div class="line"><a name="l00125"></a><span class="lineno"> 125</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00126"></a><span class="lineno"> 126</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a776c827bb6e3b889234429c49ae9ad6f" title="Optimized case for expr with one child.">substitutivityRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Op.html">Op</a>& op,</div>
<div class="line"><a name="l00127"></a><span class="lineno"> 127</span>  <span class="keyword">const</span> std::vector<Theorem>& thms) = 0;</div>
<div class="line"><a name="l00128"></a><span class="lineno"> 128</span> </div>
<div class="line"><a name="l00129"></a><span class="lineno"> 129</span>  <span class="comment">// (c_1 == d_1) & ... & (c_n == d_n)</span></div>
<div class="line"><a name="l00130"></a><span class="lineno"> 130</span>  <span class="comment">// ==> op(c_1,...,c_n) == op(d_1,...,d_n)</span><span class="comment"></span></div>
<div class="line"><a name="l00131"></a><span class="lineno"> 131</span> <span class="comment"> /*! @brief </span></div>
<div class="line"><a name="l00132"></a><span class="lineno"> 132</span> <span class="comment"> \f[\frac{(c_1=d_1)\wedge\ldots\wedge(c_n=d_n)}</span></div>
<div class="line"><a name="l00133"></a><span class="lineno"> 133</span> <span class="comment"> {op(c_1,\ldots,c_n)=op(d_1,\ldots,d_n)}\f]</span></div>
<div class="line"><a name="l00134"></a><span class="lineno"> 134</span> <span class="comment"> except that only those arguments are given that \f$c_i\not=d_i\f$.</span></div>
<div class="line"><a name="l00135"></a><span class="lineno"> 135</span> <span class="comment"> \param e is the original expression \f$op(c_1,\ldots,c_n)\f$.</span></div>
<div class="line"><a name="l00136"></a><span class="lineno"> 136</span> <span class="comment"> \param changed is the vector of indices of changed kids</span></div>
<div class="line"><a name="l00137"></a><span class="lineno"> 137</span> <span class="comment"> \param thms are the theorems \f$c_i=d_i\f$ for the changed kids.</span></div>
<div class="line"><a name="l00138"></a><span class="lineno"> 138</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00139"></a><span class="lineno"> 139</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a776c827bb6e3b889234429c49ae9ad6f" title="Optimized case for expr with one child.">substitutivityRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e,</div>
<div class="line"><a name="l00140"></a><span class="lineno"> 140</span>  <span class="keyword">const</span> std::vector<unsigned>& changed,</div>
<div class="line"><a name="l00141"></a><span class="lineno"> 141</span>  <span class="keyword">const</span> std::vector<Theorem>& thms) = 0;</div>
<div class="line"><a name="l00142"></a><span class="lineno"> 142</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a776c827bb6e3b889234429c49ae9ad6f" title="Optimized case for expr with one child.">substitutivityRule</a>(<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> <span class="keywordtype">int</span> changed, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm) = 0;</div>
<div class="line"><a name="l00143"></a><span class="lineno"> 143</span> </div>
<div class="line"><a name="l00144"></a><span class="lineno"> 144</span>  <span class="comment">// |- e, |- !e ==> |- FALSE</span><span class="comment"></span></div>
<div class="line"><a name="l00145"></a><span class="lineno"> 145</span> <span class="comment"> /*! @brief</span></div>
<div class="line"><a name="l00146"></a><span class="lineno"> 146</span> <span class="comment"> \f[\frac{\Gamma_1\vdash e\quad\Gamma_2\vdash \neg e}</span></div>
<div class="line"><a name="l00147"></a><span class="lineno"> 147</span> <span class="comment"> {\Gamma_1\cup\Gamma_2\vdash \mathrm{FALSE}}</span></div>
<div class="line"><a name="l00148"></a><span class="lineno"> 148</span> <span class="comment"> \f]</span></div>
<div class="line"><a name="l00149"></a><span class="lineno"> 149</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00150"></a><span class="lineno"> 150</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a1074822d52c22daacaa78b34ac0635ba">contradictionRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e,</div>
<div class="line"><a name="l00151"></a><span class="lineno"> 151</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& not_e) = 0;</div>
<div class="line"><a name="l00152"></a><span class="lineno"> 152</span> </div>
<div class="line"><a name="l00153"></a><span class="lineno"> 153</span>  <span class="comment">// |- e OR !e</span></div>
<div class="line"><a name="l00154"></a><span class="lineno"> 154</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#aec56ab0fbac82267ff202ae328fe801f">excludedMiddle</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) = 0;</div>
<div class="line"><a name="l00155"></a><span class="lineno"> 155</span> </div>
<div class="line"><a name="l00156"></a><span class="lineno"> 156</span>  <span class="comment">// e ==> e IFF TRUE</span><span class="comment"></span></div>
<div class="line"><a name="l00157"></a><span class="lineno"> 157</span> <span class="comment"> //! \f[\frac{\Gamma\vdash e}{\Gamma\vdash e\Leftrightarrow\mathrm{TRUE}}\f]</span></div>
<div class="line"><a name="l00158"></a><span class="lineno"> 158</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#ae5a0a67c59ba15d84e900fdccc7653ca">iffTrue</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e) = 0;</div>
<div class="line"><a name="l00159"></a><span class="lineno"> 159</span> </div>
<div class="line"><a name="l00160"></a><span class="lineno"> 160</span>  <span class="comment">// e ==> !e IFF FALSE</span><span class="comment"></span></div>
<div class="line"><a name="l00161"></a><span class="lineno"> 161</span> <span class="comment"> //! \f[\frac{\Gamma\vdash e}{\Gamma\vdash\neg e\Leftrightarrow\mathrm{FALSE}}\f]</span></div>
<div class="line"><a name="l00162"></a><span class="lineno"> 162</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a5a56b6f9544841fe86255e5bc35e8449">iffNotFalse</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e) = 0;</div>
<div class="line"><a name="l00163"></a><span class="lineno"> 163</span> </div>
<div class="line"><a name="l00164"></a><span class="lineno"> 164</span>  <span class="comment">// e IFF TRUE ==> e</span><span class="comment"></span></div>
<div class="line"><a name="l00165"></a><span class="lineno"> 165</span> <span class="comment"> //! \f[\frac{\Gamma\vdash e\Leftrightarrow\mathrm{TRUE}}{\Gamma\vdash e}\f]</span></div>
<div class="line"><a name="l00166"></a><span class="lineno"> 166</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#ad2edb920405666bf6e9d21ae496ff6b3">iffTrueElim</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e) = 0;</div>
<div class="line"><a name="l00167"></a><span class="lineno"> 167</span> </div>
<div class="line"><a name="l00168"></a><span class="lineno"> 168</span>  <span class="comment">// e IFF FALSE ==> !e</span><span class="comment"></span></div>
<div class="line"><a name="l00169"></a><span class="lineno"> 169</span> <span class="comment"> //! \f[\frac{\Gamma\vdash e\Leftrightarrow\mathrm{FALSE}}{\Gamma\vdash\neg e}\f]</span></div>
<div class="line"><a name="l00170"></a><span class="lineno"> 170</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a11b56754024b56844336954cf789a63a">iffFalseElim</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e) = 0;</div>
<div class="line"><a name="l00171"></a><span class="lineno"> 171</span> <span class="comment"></span></div>
<div class="line"><a name="l00172"></a><span class="lineno"> 172</span> <span class="comment"> //! e1 <=> e2 ==> ~e1 <=> ~e2</span></div>
<div class="line"><a name="l00173"></a><span class="lineno"> 173</span> <span class="comment"></span><span class="comment"> /*! \f[\frac{\Gamma\vdash e_1\Leftrightarrow e_2}</span></div>
<div class="line"><a name="l00174"></a><span class="lineno"> 174</span> <span class="comment"> * {\Gamma\vdash\sim e_1\Leftrightarrow\sim e_2}\f]</span></div>
<div class="line"><a name="l00175"></a><span class="lineno"> 175</span> <span class="comment"> * Where ~e is the <em>inverse</em> of e (that is, ~(!e') = e').</span></div>
<div class="line"><a name="l00176"></a><span class="lineno"> 176</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00177"></a><span class="lineno"> 177</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#af38f25446a561384c3de66392c4d3544" title="e1 <=> e2 ==> ~e1 <=> ~e2">iffContrapositive</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm) = 0;</div>
<div class="line"><a name="l00178"></a><span class="lineno"> 178</span> </div>
<div class="line"><a name="l00179"></a><span class="lineno"> 179</span>  <span class="comment">// !!e ==> e</span><span class="comment"></span></div>
<div class="line"><a name="l00180"></a><span class="lineno"> 180</span> <span class="comment"> //! \f[\frac{\Gamma\vdash\neg\neg e}{\Gamma\vdash e}\f]</span></div>
<div class="line"><a name="l00181"></a><span class="lineno"> 181</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#ace6786234994faf89bc1b0ac8575278a">notNotElim</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& not_not_e) = 0;</div>
<div class="line"><a name="l00182"></a><span class="lineno"> 182</span> </div>
<div class="line"><a name="l00183"></a><span class="lineno"> 183</span>  <span class="comment">// e1 AND (e1 IFF e2) ==> e2</span><span class="comment"></span></div>
<div class="line"><a name="l00184"></a><span class="lineno"> 184</span> <span class="comment"> /*! @brief</span></div>
<div class="line"><a name="l00185"></a><span class="lineno"> 185</span> <span class="comment"> \f[\frac{\Gamma_1\vdash e_1\quad \Gamma_2\vdash(e_1\Leftrightarrow e_2)}</span></div>
<div class="line"><a name="l00186"></a><span class="lineno"> 186</span> <span class="comment"> {\Gamma_1\cup\Gamma_2\vdash e_2}</span></div>
<div class="line"><a name="l00187"></a><span class="lineno"> 187</span> <span class="comment"> \f]</span></div>
<div class="line"><a name="l00188"></a><span class="lineno"> 188</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00189"></a><span class="lineno"> 189</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#aebbcd4a194e4fdca0bcd16143fb03a75">iffMP</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e1_iff_e2) = 0;</div>
<div class="line"><a name="l00190"></a><span class="lineno"> 190</span> </div>
<div class="line"><a name="l00191"></a><span class="lineno"> 191</span>  <span class="comment">// e1 AND (e1 IMPLIES e2) ==> e2</span><span class="comment"></span></div>
<div class="line"><a name="l00192"></a><span class="lineno"> 192</span> <span class="comment"> /*! @brief</span></div>
<div class="line"><a name="l00193"></a><span class="lineno"> 193</span> <span class="comment"> \f[\frac{\Gamma_1\vdash e_1\quad \Gamma_2\vdash(e_1\Rightarrow e_2)}</span></div>
<div class="line"><a name="l00194"></a><span class="lineno"> 194</span> <span class="comment"> {\Gamma_1\cup\Gamma_2\vdash e_2}</span></div>
<div class="line"><a name="l00195"></a><span class="lineno"> 195</span> <span class="comment"> \f]</span></div>
<div class="line"><a name="l00196"></a><span class="lineno"> 196</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00197"></a><span class="lineno"> 197</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a86416b3ccec1ddf1ce534b53d6af1ec9">implMP</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e1_impl_e2) = 0;</div>
<div class="line"><a name="l00198"></a><span class="lineno"> 198</span> </div>
<div class="line"><a name="l00199"></a><span class="lineno"> 199</span>  <span class="comment">// AND(e_1,...e_n) ==> e_i</span><span class="comment"></span></div>
<div class="line"><a name="l00200"></a><span class="lineno"> 200</span> <span class="comment"> //! \f[\frac{\vdash e_1\wedge\cdots\wedge e_n}{\vdash e_i}\f]</span></div>
<div class="line"><a name="l00201"></a><span class="lineno"> 201</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a3f3592ac74d0aa0caa3b9224ea7e61f4">andElim</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e, <span class="keywordtype">int</span> i) = 0;</div>
<div class="line"><a name="l00202"></a><span class="lineno"> 202</span> </div>
<div class="line"><a name="l00203"></a><span class="lineno"> 203</span>  <span class="comment">// e1, e2 ==> AND(e1, e2)</span><span class="comment"></span></div>
<div class="line"><a name="l00204"></a><span class="lineno"> 204</span> <span class="comment"> /*! @brief</span></div>
<div class="line"><a name="l00205"></a><span class="lineno"> 205</span> <span class="comment"> \f[\frac{\Gamma_1\vdash e_1\quad \Gamma_2\vdash e_2}</span></div>
<div class="line"><a name="l00206"></a><span class="lineno"> 206</span> <span class="comment"> {\Gamma_1\cup\Gamma_2\vdash e_1\wedge e_2}</span></div>
<div class="line"><a name="l00207"></a><span class="lineno"> 207</span> <span class="comment"> \f]</span></div>
<div class="line"><a name="l00208"></a><span class="lineno"> 208</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00209"></a><span class="lineno"> 209</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a4aa193bfeb969c96b63db39a70470015">andIntro</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e2) = 0;</div>
<div class="line"><a name="l00210"></a><span class="lineno"> 210</span> </div>
<div class="line"><a name="l00211"></a><span class="lineno"> 211</span>  <span class="comment">// e1, ..., en ==> AND(e1, ..., en)</span><span class="comment"></span></div>
<div class="line"><a name="l00212"></a><span class="lineno"> 212</span> <span class="comment"> /*! @brief</span></div>
<div class="line"><a name="l00213"></a><span class="lineno"> 213</span> <span class="comment"> \f[\frac{\Gamma_1\vdash e_1\quad \cdots \quad\Gamma_n\vdash e_n}</span></div>
<div class="line"><a name="l00214"></a><span class="lineno"> 214</span> <span class="comment"> {\bigcup_{i=1}^n\Gamma_i\vdash \bigwedge_{i=1}^n e_i}</span></div>
<div class="line"><a name="l00215"></a><span class="lineno"> 215</span> <span class="comment"> \f]</span></div>
<div class="line"><a name="l00216"></a><span class="lineno"> 216</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00217"></a><span class="lineno"> 217</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a4aa193bfeb969c96b63db39a70470015">andIntro</a>(<span class="keyword">const</span> std::vector<Theorem>& es) = 0;</div>
<div class="line"><a name="l00218"></a><span class="lineno"> 218</span> </div>
<div class="line"><a name="l00219"></a><span class="lineno"> 219</span>  <span class="comment">// G,a1,...,an |- phi</span></div>
<div class="line"><a name="l00220"></a><span class="lineno"> 220</span>  <span class="comment">// -------------------------------------------------</span></div>
<div class="line"><a name="l00221"></a><span class="lineno"> 221</span>  <span class="comment">// G |- (a1 & ... & an) -> phi</span><span class="comment"></span></div>
<div class="line"><a name="l00222"></a><span class="lineno"> 222</span> <span class="comment"> /*!</span></div>
<div class="line"><a name="l00223"></a><span class="lineno"> 223</span> <span class="comment"> * @brief Implication introduction rule:</span></div>
<div class="line"><a name="l00224"></a><span class="lineno"> 224</span> <span class="comment"> * \f[\frac{\Gamma,\,\alpha_1\,\ldots,\,\alpha_n\vdash\phi}</span></div>
<div class="line"><a name="l00225"></a><span class="lineno"> 225</span> <span class="comment"> * {\Gamma\vdash(\bigwedge_{i=1}^n\alpha_i)\to\phi}\f]</span></div>
<div class="line"><a name="l00226"></a><span class="lineno"> 226</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00227"></a><span class="lineno"> 227</span> <span class="comment"> * \param phi is the formula \f$\phi\f$</span></div>
<div class="line"><a name="l00228"></a><span class="lineno"> 228</span> <span class="comment"> * \param assump is the vector of assumptions \f$\alpha_1\ldots\alpha_n\f$</span></div>
<div class="line"><a name="l00229"></a><span class="lineno"> 229</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00230"></a><span class="lineno"> 230</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a9292e13acd4b5ba2b215864022a22573" title="Implication introduction rule: .">implIntro</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& phi,</div>
<div class="line"><a name="l00231"></a><span class="lineno"> 231</span>  <span class="keyword">const</span> std::vector<Expr>& assump) = 0;</div>
<div class="line"><a name="l00232"></a><span class="lineno"> 232</span> <span class="comment"></span></div>
<div class="line"><a name="l00233"></a><span class="lineno"> 233</span> <span class="comment"> //! e1 => e2 ==> ~e2 => ~e1</span></div>
<div class="line"><a name="l00234"></a><span class="lineno"> 234</span> <span class="comment"></span><span class="comment"> /*! \f[\frac{\Gamma\vdash e_1\Rightarrow e_2}</span></div>
<div class="line"><a name="l00235"></a><span class="lineno"> 235</span> <span class="comment"> * {\Gamma\vdash\sim e_2\Rightarrow\sim e_1}\f]</span></div>
<div class="line"><a name="l00236"></a><span class="lineno"> 236</span> <span class="comment"> * Where ~e is the <em>inverse</em> of e (that is, ~(!e') = e').</span></div>
<div class="line"><a name="l00237"></a><span class="lineno"> 237</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00238"></a><span class="lineno"> 238</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a69da48e244e1674f6b501ac4ef168feb" title="e1 => e2 ==> ~e2 => ~e1">implContrapositive</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm) = 0;</div>
<div class="line"><a name="l00239"></a><span class="lineno"> 239</span> <span class="comment"></span></div>
<div class="line"><a name="l00240"></a><span class="lineno"> 240</span> <span class="comment"> //! ==> ITE(TRUE, e1, e2) == e1</span></div>
<div class="line"><a name="l00241"></a><span class="lineno"> 241</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a0e770e47e947275a69b4c9f225f8beb6" title="==> ITE(TRUE, e1, e2) == e1">rewriteIteTrue</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) = 0;<span class="comment"></span></div>
<div class="line"><a name="l00242"></a><span class="lineno"> 242</span> <span class="comment"> //! ==> ITE(FALSE, e1, e2) == e2</span></div>
<div class="line"><a name="l00243"></a><span class="lineno"> 243</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a95af3ce5ccd4212b15bac9b249004c48" title="==> ITE(FALSE, e1, e2) == e2">rewriteIteFalse</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) = 0;<span class="comment"></span></div>
<div class="line"><a name="l00244"></a><span class="lineno"> 244</span> <span class="comment"> //! ==> ITE(c, e, e) == e</span></div>
<div class="line"><a name="l00245"></a><span class="lineno"> 245</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a6cb02a9489ef5ed4e548f49bbd07439f" title="==> ITE(c, e, e) == e">rewriteIteSame</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) = 0;</div>
<div class="line"><a name="l00246"></a><span class="lineno"> 246</span> </div>
<div class="line"><a name="l00247"></a><span class="lineno"> 247</span>  <span class="comment">// NOT e ==> e IFF FALSE</span><span class="comment"></span></div>
<div class="line"><a name="l00248"></a><span class="lineno"> 248</span> <span class="comment"> //! \f[\frac{\vdash\neg e}{\vdash e\Leftrightarrow\mathrm{FALSE}}\f]</span></div>
<div class="line"><a name="l00249"></a><span class="lineno"> 249</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a34064eea86afa953b9229537b075a420">notToIff</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& not_e) = 0;</div>
<div class="line"><a name="l00250"></a><span class="lineno"> 250</span> </div>
<div class="line"><a name="l00251"></a><span class="lineno"> 251</span>  <span class="comment">// e1 XOR e2 ==> e1 IFF (NOT e2)</span><span class="comment"></span></div>
<div class="line"><a name="l00252"></a><span class="lineno"> 252</span> <span class="comment"> //! \f[\frac{\vdash e_1 XOR e_2}{\vdash e_1\Leftrightarrow(\neg e_2)}\f]</span></div>
<div class="line"><a name="l00253"></a><span class="lineno"> 253</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#ae25f68b7cceeeb25b41b1d2bcb1df8f3">xorToIff</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) = 0;</div>
<div class="line"><a name="l00254"></a><span class="lineno"> 254</span> <span class="comment"></span></div>
<div class="line"><a name="l00255"></a><span class="lineno"> 255</span> <span class="comment"> //! ==> (e1 <=> e2) <=> [simplified expr]</span></div>
<div class="line"><a name="l00256"></a><span class="lineno"> 256</span> <span class="comment"></span><span class="comment"> /*! Rewrite formulas like FALSE/TRUE <=> e, e <=> NOT e, etc. */</span></div>
<div class="line"><a name="l00257"></a><span class="lineno"> 257</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a5c50bf251b95dfc47ccfc6e8b51426c1" title="==> (e1 <=> e2) <=> [simplified expr]">rewriteIff</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) = 0;</div>
<div class="line"><a name="l00258"></a><span class="lineno"> 258</span> </div>
<div class="line"><a name="l00259"></a><span class="lineno"> 259</span>  <span class="comment">// AND and OR rewrites check for TRUE and FALSE arguments and</span></div>
<div class="line"><a name="l00260"></a><span class="lineno"> 260</span>  <span class="comment">// remove them or collapse the entire expression to TRUE and FALSE</span></div>
<div class="line"><a name="l00261"></a><span class="lineno"> 261</span>  <span class="comment">// appropriately</span></div>
<div class="line"><a name="l00262"></a><span class="lineno"> 262</span> <span class="comment"></span></div>
<div class="line"><a name="l00263"></a><span class="lineno"> 263</span> <span class="comment"> //! ==> AND(e1,e2) IFF [simplified expr]</span></div>
<div class="line"><a name="l00264"></a><span class="lineno"> 264</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#afb2ae30738c04b088459281d259a6d3a" title="==> AND(e1,e2) IFF [simplified expr]">rewriteAnd</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) = 0;</div>
<div class="line"><a name="l00265"></a><span class="lineno"> 265</span> <span class="comment"></span></div>
<div class="line"><a name="l00266"></a><span class="lineno"> 266</span> <span class="comment"> //! ==> OR(e1,...,en) IFF [simplified expr]</span></div>
<div class="line"><a name="l00267"></a><span class="lineno"> 267</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#aa3cfb7d47a6d6bc84c85c7fa6a3e1242" title="==> OR(e1,...,en) IFF [simplified expr]">rewriteOr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) = 0;</div>
<div class="line"><a name="l00268"></a><span class="lineno"> 268</span> <span class="comment"></span></div>
<div class="line"><a name="l00269"></a><span class="lineno"> 269</span> <span class="comment"> //! ==> NOT TRUE IFF FALSE</span></div>
<div class="line"><a name="l00270"></a><span class="lineno"> 270</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#ad55b11590196fbd73d24daa1d0d6eeb1" title="==> NOT TRUE IFF FALSE">rewriteNotTrue</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) = 0;</div>
<div class="line"><a name="l00271"></a><span class="lineno"> 271</span> <span class="comment"></span></div>
<div class="line"><a name="l00272"></a><span class="lineno"> 272</span> <span class="comment"> //! ==> NOT FALSE IFF TRUE</span></div>
<div class="line"><a name="l00273"></a><span class="lineno"> 273</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a30fa79637f4308e8e733015624293775" title="==> NOT FALSE IFF TRUE">rewriteNotFalse</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) = 0;</div>
<div class="line"><a name="l00274"></a><span class="lineno"> 274</span> <span class="comment"></span></div>
<div class="line"><a name="l00275"></a><span class="lineno"> 275</span> <span class="comment"> //! ==> NOT NOT e IFF e, takes !!e</span></div>
<div class="line"><a name="l00276"></a><span class="lineno"> 276</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a8a04ff29591a019d4d4cf073c0987316" title="==> NOT NOT e IFF e, takes !!e">rewriteNotNot</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) = 0;</div>
<div class="line"><a name="l00277"></a><span class="lineno"> 277</span> <span class="comment"></span></div>
<div class="line"><a name="l00278"></a><span class="lineno"> 278</span> <span class="comment"> //! ==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e</span></div>
<div class="line"><a name="l00279"></a><span class="lineno"> 279</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#ad14f0ceb0d486ba3d78c2c3c6e47382a" title="==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e">rewriteNotForall</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& forallExpr) = 0;</div>
<div class="line"><a name="l00280"></a><span class="lineno"> 280</span> <span class="comment"></span></div>
<div class="line"><a name="l00281"></a><span class="lineno"> 281</span> <span class="comment"> //! ==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e</span></div>
<div class="line"><a name="l00282"></a><span class="lineno"> 282</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a12d8ca9f5547fb3a3239d7dc6f53987c" title="==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e">rewriteNotExists</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& existsExpr) = 0;</div>
<div class="line"><a name="l00283"></a><span class="lineno"> 283</span> </div>
<div class="line"><a name="l00284"></a><span class="lineno"> 284</span>  <span class="comment">//From expr EXISTS(x1: t1, ..., xn: tn) phi(x1,...,cn)</span></div>
<div class="line"><a name="l00285"></a><span class="lineno"> 285</span>  <span class="comment">//we create phi(c1,...,cn) where ci is a skolem constant</span></div>
<div class="line"><a name="l00286"></a><span class="lineno"> 286</span>  <span class="comment">//defined by the original expression and the index i.</span></div>
<div class="line"><a name="l00287"></a><span class="lineno"> 287</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a015539886185195ba5d98c60cd7e8f66">skolemize</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) = 0;</div>
<div class="line"><a name="l00288"></a><span class="lineno"> 288</span> <span class="comment"></span></div>
<div class="line"><a name="l00289"></a><span class="lineno"> 289</span> <span class="comment"> /*! skolem rewrite rule: Introduces axiom |- Exists(x) phi(x) <=> phi(c)</span></div>
<div class="line"><a name="l00290"></a><span class="lineno"> 290</span> <span class="comment"> * where c is a constant defined by the expression Exists(x) phi(x)</span></div>
<div class="line"><a name="l00291"></a><span class="lineno"> 291</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00292"></a><span class="lineno"> 292</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a8a2561e9e4763460c65dbebe10d2f281">skolemizeRewrite</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) = 0;</div>
<div class="line"><a name="l00293"></a><span class="lineno"> 293</span> <span class="comment"></span></div>
<div class="line"><a name="l00294"></a><span class="lineno"> 294</span> <span class="comment"> //! Special version of skolemizeRewrite for "EXISTS x. t = x"</span></div>
<div class="line"><a name="l00295"></a><span class="lineno"> 295</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a4013a795d82cebb8b60ed67c094a7cba" title="Special version of skolemizeRewrite for "EXISTS x. t = x".">skolemizeRewriteVar</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) = 0;</div>
<div class="line"><a name="l00296"></a><span class="lineno"> 296</span> <span class="comment"></span></div>
<div class="line"><a name="l00297"></a><span class="lineno"> 297</span> <span class="comment"> //! |- EXISTS x. e = x</span></div>
<div class="line"><a name="l00298"></a><span class="lineno"> 298</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#aab746efc9d013643bccc065affa82992" title="|- EXISTS x. e = x">varIntroRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) = 0;</div>
<div class="line"><a name="l00299"></a><span class="lineno"> 299</span> <span class="comment"></span></div>
<div class="line"><a name="l00300"></a><span class="lineno"> 300</span> <span class="comment"> /*! @brief If thm is (EXISTS x: phi(x)), create the Skolemized version</span></div>
<div class="line"><a name="l00301"></a><span class="lineno"> 301</span> <span class="comment"> and add it to the database. Otherwise returns just thm. */</span><span class="comment"></span></div>
<div class="line"><a name="l00302"></a><span class="lineno"> 302</span> <span class="comment"> /*!</span></div>
<div class="line"><a name="l00303"></a><span class="lineno"> 303</span> <span class="comment"> * \param thm is the Theorem(EXISTS x: phi(x))</span></div>
<div class="line"><a name="l00304"></a><span class="lineno"> 304</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00305"></a><span class="lineno"> 305</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a015539886185195ba5d98c60cd7e8f66">skolemize</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm) = 0;</div>
<div class="line"><a name="l00306"></a><span class="lineno"> 306</span> <span class="comment"></span></div>
<div class="line"><a name="l00307"></a><span class="lineno"> 307</span> <span class="comment"> //! Retrun a theorem "|- e = v" for a new Skolem constant v</span></div>
<div class="line"><a name="l00308"></a><span class="lineno"> 308</span> <span class="comment"></span><span class="comment"> /*!</span></div>
<div class="line"><a name="l00309"></a><span class="lineno"> 309</span> <span class="comment"> * This is equivalent to skolemize(d_core->varIntroRule(e)), only more</span></div>
<div class="line"><a name="l00310"></a><span class="lineno"> 310</span> <span class="comment"> * efficient.</span></div>
<div class="line"><a name="l00311"></a><span class="lineno"> 311</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00312"></a><span class="lineno"> 312</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a10fa187373ec24079c10874d8e804ecb" title="Retrun a theorem "|- e = v" for a new Skolem constant v.">varIntroSkolem</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) = 0;</div>
<div class="line"><a name="l00313"></a><span class="lineno"> 313</span> </div>
<div class="line"><a name="l00314"></a><span class="lineno"> 314</span>  <span class="comment">// Derived rules</span></div>
<div class="line"><a name="l00315"></a><span class="lineno"> 315</span> <span class="comment"></span></div>
<div class="line"><a name="l00316"></a><span class="lineno"> 316</span> <span class="comment"> //! ==> TRUE</span></div>
<div class="line"><a name="l00317"></a><span class="lineno"> 317</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a6e93694c76f7b567487bc8cae674ae5d" title="==> TRUE">trueTheorem</a>() = 0;</div>
<div class="line"><a name="l00318"></a><span class="lineno"> 318</span> <span class="comment"></span></div>
<div class="line"><a name="l00319"></a><span class="lineno"> 319</span> <span class="comment"> //! AND(e1,e2) ==> [simplified expr]</span></div>
<div class="line"><a name="l00320"></a><span class="lineno"> 320</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#afb2ae30738c04b088459281d259a6d3a" title="==> AND(e1,e2) IFF [simplified expr]">rewriteAnd</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e) = 0;</div>
<div class="line"><a name="l00321"></a><span class="lineno"> 321</span> <span class="comment"></span></div>
<div class="line"><a name="l00322"></a><span class="lineno"> 322</span> <span class="comment"> //! OR(e1,...,en) ==> [simplified expr]</span></div>
<div class="line"><a name="l00323"></a><span class="lineno"> 323</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#aa3cfb7d47a6d6bc84c85c7fa6a3e1242" title="==> OR(e1,...,en) IFF [simplified expr]">rewriteOr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e) = 0;</div>
<div class="line"><a name="l00324"></a><span class="lineno"> 324</span> </div>
<div class="line"><a name="l00325"></a><span class="lineno"> 325</span>  <span class="comment">// TODO: do we really need this?</span></div>
<div class="line"><a name="l00326"></a><span class="lineno"> 326</span>  <span class="keyword">virtual</span> std::vector<Theorem>& <a class="code" href="classCVC3_1_1CommonProofRules.html#ac773341edabcc5091ca25af74fcb7653">getSkolemAxioms</a>() = 0;</div>
<div class="line"><a name="l00327"></a><span class="lineno"> 327</span> </div>
<div class="line"><a name="l00328"></a><span class="lineno"> 328</span>  <span class="comment">//TODO: do we need this?</span></div>
<div class="line"><a name="l00329"></a><span class="lineno"> 329</span>  <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1CommonProofRules.html#a6f8068606f30fe7b2c405ddf5ce1a53b">clearSkolemAxioms</a>() = 0;</div>
<div class="line"><a name="l00330"></a><span class="lineno"> 330</span> </div>
<div class="line"><a name="l00331"></a><span class="lineno"> 331</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a484540b067da205d23b2fe263662cda2">ackermann</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e2) = 0;</div>
<div class="line"><a name="l00332"></a><span class="lineno"> 332</span> </div>
<div class="line"><a name="l00333"></a><span class="lineno"> 333</span>  <span class="comment">// Given a propositional atom containing embedded ite's, lifts first ite condition</span></div>
<div class="line"><a name="l00334"></a><span class="lineno"> 334</span>  <span class="comment">// to form a Boolean ITE</span></div>
<div class="line"><a name="l00335"></a><span class="lineno"> 335</span>  <span class="comment">// |- P(...ite(a,b,c)...) <=> ite(a,P(...b...),P(...c...))</span></div>
<div class="line"><a name="l00336"></a><span class="lineno"> 336</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonProofRules.html#a893a258d9f7d49acb5c8a8b5b8ec39b0">liftOneITE</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) = 0;</div>
<div class="line"><a name="l00337"></a><span class="lineno"> 337</span> </div>
<div class="line"><a name="l00338"></a><span class="lineno"> 338</span>  }; <span class="comment">// end of class CommonProofRules</span></div>
<div class="line"><a name="l00339"></a><span class="lineno"> 339</span> </div>
<div class="line"><a name="l00340"></a><span class="lineno"> 340</span> } <span class="comment">// end of namespace CVC3</span></div>
<div class="line"><a name="l00341"></a><span class="lineno"> 341</span> </div>
<div class="line"><a name="l00342"></a><span class="lineno"> 342</span> <span class="preprocessor">#endif</span></div>
</div><!-- fragment --></div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:13 for CVC3 by  <a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/>
</a> 1.8.2
</small></address>
</body>
</html>
