<!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_theorem_producer.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_0ed98c5bff61fa5a11795860655bf1d8.html">theorem</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="headertitle">
<div class="title">common_theorem_producer.h</div> </div>
</div><!--header-->
<div class="contents">
<a href="common__theorem__producer_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_theorem_producer.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: Feb 05 03:40:36 GMT 2003</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: CommonTheoremProducer</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: Implementation of the proof rules for ground</span></div>
<div class="line"><a name="l00025"></a><span class="lineno"> 25</span> <span class="comment">// equational logic (reflexivity, symmetry, transitivity, and</span></div>
<div class="line"><a name="l00026"></a><span class="lineno"> 26</span> <span class="comment">// substitutivity).</span></div>
<div class="line"><a name="l00027"></a><span class="lineno"> 27</span> <span class="comment">//</span><span class="comment"></span></div>
<div class="line"><a name="l00028"></a><span class="lineno"> 28</span> <span class="comment">///////////////////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00029"></a><span class="lineno"> 29</span> <span class="comment"></span></div>
<div class="line"><a name="l00030"></a><span class="lineno"> 30</span> <span class="preprocessor">#ifndef _cvc3__common_theorem_producer_h_</span></div>
<div class="line"><a name="l00031"></a><span class="lineno"> 31</span> <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__common_theorem_producer_h_</span></div>
<div class="line"><a name="l00032"></a><span class="lineno"> 32</span> <span class="preprocessor"></span></div>
<div class="line"><a name="l00033"></a><span class="lineno"> 33</span> <span class="preprocessor">#include "<a class="code" href="common__proof__rules_8h.html">common_proof_rules.h</a>"</span></div>
<div class="line"><a name="l00034"></a><span class="lineno"> 34</span> <span class="preprocessor">#include "<a class="code" href="theorem__producer_8h.html">theorem_producer.h</a>"</span></div>
<div class="line"><a name="l00035"></a><span class="lineno"> 35</span> <span class="preprocessor">#include "<a class="code" href="theorem_8h.html">theorem.h</a>"</span></div>
<div class="line"><a name="l00036"></a><span class="lineno"> 36</span> <span class="preprocessor">#include "<a class="code" href="cdmap_8h.html">cdmap.h</a>"</span></div>
<div class="line"><a name="l00037"></a><span class="lineno"> 37</span> </div>
<div class="line"><a name="l00038"></a><span class="lineno"> 38</span> <span class="keyword">namespace </span>CVC3 {</div>
<div class="line"><a name="l00039"></a><span class="lineno"> 39</span> </div>
<div class="line"><a name="l00040"></a><span class="lineno"><a class="code" href="classCVC3_1_1CommonTheoremProducer.html"> 40</a></span>  <span class="keyword">class </span><a class="code" href="classCVC3_1_1CommonTheoremProducer.html">CommonTheoremProducer</a>: <span class="keyword">public</span> <a class="code" href="classCVC3_1_1CommonProofRules.html">CommonProofRules</a>, <span class="keyword">public</span> <a class="code" href="classCVC3_1_1TheoremProducer.html">TheoremProducer</a> {</div>
<div class="line"><a name="l00041"></a><span class="lineno"> 41</span>  <span class="keyword">private</span>:</div>
<div class="line"><a name="l00042"></a><span class="lineno"> 42</span> </div>
<div class="line"><a name="l00043"></a><span class="lineno"> 43</span>  <span class="comment">// TODO: do we need to record skolem axioms? do we need context-dependence?</span></div>
<div class="line"><a name="l00044"></a><span class="lineno"> 44</span> </div>
<div class="line"><a name="l00045"></a><span class="lineno"> 45</span>  <span class="comment">// skolem axioms</span></div>
<div class="line"><a name="l00046"></a><span class="lineno"><a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a3ead097d78257116405995705a98a722"> 46</a></span>  std::vector<Theorem> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a3ead097d78257116405995705a98a722">d_skolem_axioms</a>;</div>
<div class="line"><a name="l00047"></a><span class="lineno"> 47</span> </div>
<div class="line"><a name="l00048"></a><span class="lineno"> 48</span>  <span class="comment">/* @brief Keep skolemization axioms so that they can be reused </span></div>
<div class="line"><a name="l00049"></a><span class="lineno"> 49</span> <span class="comment"> without being recreated each time */</span></div>
<div class="line"><a name="l00050"></a><span class="lineno"><a class="code" href="classCVC3_1_1CommonTheoremProducer.html#ab4d87623f3ff65970b5c015b39db5987"> 50</a></span>  <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, Theorem></a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#ab4d87623f3ff65970b5c015b39db5987">d_skolemized_thms</a>;</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"> //! Mapping of e to "|- e = v" for fresh Skolem vars v</span></div>
<div class="line"><a name="l00053"></a><span class="lineno"><a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a628cb0e578632642b6a2c8d48ddeb890"> 53</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, Theorem></a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a628cb0e578632642b6a2c8d48ddeb890" title="Mapping of e to "|- e = v" for fresh Skolem vars v.">d_skolemVars</a>;</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"> //! Helper function for liftOneITE</span></div>
<div class="line"><a name="l00056"></a><span class="lineno"> 56</span> <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a78038ee1c3cd8d3657a0261ce2f35eaf" title="Helper function for liftOneITE.">findITE</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 class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& condition, <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& thenpart, <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& elsepart);</div>
<div class="line"><a name="l00057"></a><span class="lineno"> 57</span> </div>
<div class="line"><a name="l00058"></a><span class="lineno"> 58</span>  <span class="keyword">public</span>:</div>
<div class="line"><a name="l00059"></a><span class="lineno"> 59</span>  <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a2ae31c06ed093e9b5b85f90af78641ae">CommonTheoremProducer</a>(<a class="code" href="classCVC3_1_1TheoremManager.html">TheoremManager</a>* tm);</div>
<div class="line"><a name="l00060"></a><span class="lineno"><a class="code" href="classCVC3_1_1CommonTheoremProducer.html#afed5498eb0373f7f482cc7fbf8eb857a"> 60</a></span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#afed5498eb0373f7f482cc7fbf8eb857a">~CommonTheoremProducer</a>() { }</div>
<div class="line"><a name="l00061"></a><span class="lineno"> 61</span> </div>
<div class="line"><a name="l00062"></a><span class="lineno"> 62</span>  <a class="code" href="classCVC3_1_1Theorem3.html" title="Theorem3.">Theorem3</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a685c913a4b6b80a546dcb9853a88e21a" 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);</div>
<div class="line"><a name="l00063"></a><span class="lineno"> 63</span>  <a class="code" href="classCVC3_1_1Theorem3.html" title="Theorem3.">Theorem3</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#abf904962af8344d8646c382747837af4" 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="l00064"></a><span class="lineno"> 64</span>  <span class="keyword">const</span> std::vector<Expr>& assump,</div>
<div class="line"><a name="l00065"></a><span class="lineno"> 65</span>  <span class="keyword">const</span> std::vector<Theorem>& tccs);</div>
<div class="line"><a name="l00066"></a><span class="lineno"> 66</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a28d225c0e86bf45df3441c14a11197be">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);</div>
<div class="line"><a name="l00067"></a><span class="lineno"> 67</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a306058f7ced3d7220b2d1a40892faae7">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);</div>
<div class="line"><a name="l00068"></a><span class="lineno"> 68</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a26b00cb395f45971ace24a4529189e1b" 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>& t);</div>
<div class="line"><a name="l00069"></a><span class="lineno"> 69</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#ab269d27c05584ade0b1f86f2ced0c46a" title=" (same for IFF)">symmetryRule</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="l00070"></a><span class="lineno"> 70</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#ac0813c68583ad6f0661d4c1affe3c6d8">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);</div>
<div class="line"><a name="l00071"></a><span class="lineno"> 71</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#ad5c0bc0fb82634039e5f2c8f9291de0e" 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="l00072"></a><span class="lineno"> 72</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& a2_eq_a3);</div>
<div class="line"><a name="l00073"></a><span class="lineno"> 73</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#aac39a4ae729b4218d4b70ed6a68bc53d" 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="l00074"></a><span class="lineno"> 74</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);</div>
<div class="line"><a name="l00075"></a><span class="lineno"> 75</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#aac39a4ae729b4218d4b70ed6a68bc53d" 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="l00076"></a><span class="lineno"> 76</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm1,</div>
<div class="line"><a name="l00077"></a><span class="lineno"> 77</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm2);</div>
<div class="line"><a name="l00078"></a><span class="lineno"> 78</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#aac39a4ae729b4218d4b70ed6a68bc53d" 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="l00079"></a><span class="lineno"> 79</span>  <span class="keyword">const</span> std::vector<Theorem>& thms);</div>
<div class="line"><a name="l00080"></a><span class="lineno"> 80</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#aac39a4ae729b4218d4b70ed6a68bc53d" 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="l00081"></a><span class="lineno"> 81</span>  <span class="keyword">const</span> std::vector<unsigned>& changed,</div>
<div class="line"><a name="l00082"></a><span class="lineno"> 82</span>  <span class="keyword">const</span> std::vector<Theorem>& thms);</div>
<div class="line"><a name="l00083"></a><span class="lineno"> 83</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#aac39a4ae729b4218d4b70ed6a68bc53d" 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="l00084"></a><span class="lineno"> 84</span>  <span class="keyword">const</span> <span class="keywordtype">int</span> changed,</div>
<div class="line"><a name="l00085"></a><span class="lineno"> 85</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);</div>
<div class="line"><a name="l00086"></a><span class="lineno"> 86</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#aaa58b8a459f5678aa2393fba6b50ff8d">contradictionRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& not_e);</div>
<div class="line"><a name="l00087"></a><span class="lineno"> 87</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#ad6ecd5f3d95b2f44d670ad1228a88f4a">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);</div>
<div class="line"><a name="l00088"></a><span class="lineno"> 88</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a37ed2850e80cd789f7ac712df6eacc63">iffTrue</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e);</div>
<div class="line"><a name="l00089"></a><span class="lineno"> 89</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a2b95f985a56f8d25b00145846406d70b">iffNotFalse</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e);</div>
<div class="line"><a name="l00090"></a><span class="lineno"> 90</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a40da8d343ef923020c472eaace6e8122">iffTrueElim</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e);</div>
<div class="line"><a name="l00091"></a><span class="lineno"> 91</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a4efade3a917467bf7287a19d2ee4ea2c">iffFalseElim</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e);</div>
<div class="line"><a name="l00092"></a><span class="lineno"> 92</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a3733173dbd8f639af979150059c4ec90" title="e1 <=> e2 ==> ~e1 <=> ~e2">iffContrapositive</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);</div>
<div class="line"><a name="l00093"></a><span class="lineno"> 93</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a59470692918d2f7c03c073a61daa3db5">notNotElim</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e);</div>
<div class="line"><a name="l00094"></a><span class="lineno"> 94</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a98f862538ac375b133079c336c539b22">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);</div>
<div class="line"><a name="l00095"></a><span class="lineno"> 95</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#ac7155849ce6bd4afe185fdb0e397fc58">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);</div>
<div class="line"><a name="l00096"></a><span class="lineno"> 96</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a23e3f96d1cc6da39d97f9b7a2e0ba723">andElim</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e, <span class="keywordtype">int</span> i);</div>
<div class="line"><a name="l00097"></a><span class="lineno"> 97</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a733e7c5fe7b46d1af284c7c30c94025a" title="e1, e2 ==> AND(e1, e2)">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);</div>
<div class="line"><a name="l00098"></a><span class="lineno"> 98</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a733e7c5fe7b46d1af284c7c30c94025a" title="e1, e2 ==> AND(e1, e2)">andIntro</a>(<span class="keyword">const</span> std::vector<Theorem>& es);</div>
<div class="line"><a name="l00099"></a><span class="lineno"> 99</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a414b98f6715044635975f8675f770c0b" title="Implication introduction rule: .">implIntro</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& phi, <span class="keyword">const</span> std::vector<Expr>& assump);</div>
<div class="line"><a name="l00100"></a><span class="lineno"> 100</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a38bb194aa15b10dd0959cfff5e33014b" title="e1 => e2 ==> ~e2 => ~e1">implContrapositive</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);</div>
<div class="line"><a name="l00101"></a><span class="lineno"> 101</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a2459a321ea5cdab974dc2cf029934a71" 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);</div>
<div class="line"><a name="l00102"></a><span class="lineno"> 102</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a1711198c758a0475449b1889815f1371" 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);</div>
<div class="line"><a name="l00103"></a><span class="lineno"> 103</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#aad60929c1c8c79287a16bc995cd9c51c" 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);</div>
<div class="line"><a name="l00104"></a><span class="lineno"> 104</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#ab9c0b6784e83fc0a4727a58c0a82b67a">notToIff</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& not_e);</div>
<div class="line"><a name="l00105"></a><span class="lineno"> 105</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a5b3a8e2d8bb3469935ecd1476778acaa">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);</div>
<div class="line"><a name="l00106"></a><span class="lineno"> 106</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#ab2233ef28defaf0af1b6a8cc4b887708" 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);</div>
<div class="line"><a name="l00107"></a><span class="lineno"> 107</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#ad74cb42b63d2f92b55c79281e84816c1" 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);</div>
<div class="line"><a name="l00108"></a><span class="lineno"> 108</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#aa0d6b0fbe3838ae22b4a90d92d1530e2" 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);</div>
<div class="line"><a name="l00109"></a><span class="lineno"> 109</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a49ce394a818d2ab83b2f97d44cd66f1b" 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);</div>
<div class="line"><a name="l00110"></a><span class="lineno"> 110</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#aace9193e3ff294ef6065178a55610e88" 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);</div>
<div class="line"><a name="l00111"></a><span class="lineno"> 111</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a84b83e300ddf9e67e427b2815ecff1e7" 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);</div>
<div class="line"><a name="l00112"></a><span class="lineno"> 112</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a6241bfc091691a667ed41a9d36d4cab6" 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);</div>
<div class="line"><a name="l00113"></a><span class="lineno"> 113</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a2535d1565f3f7b830063ad9ae3e1c4e7" 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);</div>
<div class="line"><a name="l00114"></a><span class="lineno"> 114</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#adcd56f1052668c269d59b5001a01191f">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);</div>
<div class="line"><a name="l00115"></a><span class="lineno"> 115</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a3bfb1ce883967f3822858b73156f99e9">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);</div>
<div class="line"><a name="l00116"></a><span class="lineno"> 116</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a5b97504309d324b509e18976b93a3c78" 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);</div>
<div class="line"><a name="l00117"></a><span class="lineno"> 117</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#ac003e84b85d4f51746628fd0f738b7e3" 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);</div>
<div class="line"><a name="l00118"></a><span class="lineno"> 118</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#adcd56f1052668c269d59b5001a01191f">skolemize</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);</div>
<div class="line"><a name="l00119"></a><span class="lineno"> 119</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a84f7da63e9d820ad781efa7e963733aa" 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);</div>
<div class="line"><a name="l00120"></a><span class="lineno"> 120</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a38a1b30499d07384066e9afca89f37c0" title="==> TRUE">trueTheorem</a>();</div>
<div class="line"><a name="l00121"></a><span class="lineno"> 121</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#ad74cb42b63d2f92b55c79281e84816c1" 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);</div>
<div class="line"><a name="l00122"></a><span class="lineno"> 122</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#aa0d6b0fbe3838ae22b4a90d92d1530e2" 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);</div>
<div class="line"><a name="l00123"></a><span class="lineno"> 123</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a752f5927047540cc10f67d3d5ed179a7">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);</div>
<div class="line"><a name="l00124"></a><span class="lineno"> 124</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a749d1c718f05307dad5dcc3f6d2296a2">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);</div>
<div class="line"><a name="l00125"></a><span class="lineno"> 125</span> </div>
<div class="line"><a name="l00126"></a><span class="lineno"><a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a8c83d415f39a7ac2f6a117972116c6b2"> 126</a></span>  std::vector<Theorem>& <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a8c83d415f39a7ac2f6a117972116c6b2">getSkolemAxioms</a>() { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a3ead097d78257116405995705a98a722">d_skolem_axioms</a>; }</div>
<div class="line"><a name="l00127"></a><span class="lineno"><a class="code" href="classCVC3_1_1CommonTheoremProducer.html#ad7dc685e6e46a90802f2602a70b9674a"> 127</a></span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#ad7dc685e6e46a90802f2602a70b9674a">clearSkolemAxioms</a>() { <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a3ead097d78257116405995705a98a722">d_skolem_axioms</a>.clear(); }</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">// end of class CommonTheoremProducer</span></div>
<div class="line"><a name="l00130"></a><span class="lineno"> 130</span> </div>
<div class="line"><a name="l00131"></a><span class="lineno"> 131</span> } <span class="comment">// end of namespace CVC3</span></div>
<div class="line"><a name="l00132"></a><span class="lineno"> 132</span> </div>
<div class="line"><a name="l00133"></a><span class="lineno"> 133</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>
