<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<title>CVC3: common_theorem_producer.h Source File</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li><a href="annotated.html"><span>Classes</span></a></li>
<li class="current"><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="files.html"><span>File List</span></a></li>
<li><a href="globals.html"><span>File Members</span></a></li>
</ul>
</div>
<div class="header">
<div class="headertitle">
<div class="title">common_theorem_producer.h</div> </div>
</div>
<div class="contents">
<a href="common__theorem__producer_8h.html">Go to the documentation of this file.</a><div class="fragment"><pre class="fragment"><a name="l00001"></a>00001 <span class="comment">/*****************************************************************************/</span><span class="comment"></span>
<a name="l00002"></a>00002 <span class="comment">/*!</span>
<a name="l00003"></a>00003 <span class="comment"> * \file common_theorem_producer.h</span>
<a name="l00004"></a>00004 <span class="comment"> * </span>
<a name="l00005"></a>00005 <span class="comment"> * Author: Sergey Berezin</span>
<a name="l00006"></a>00006 <span class="comment"> * </span>
<a name="l00007"></a>00007 <span class="comment"> * Created: Feb 05 03:40:36 GMT 2003</span>
<a name="l00008"></a>00008 <span class="comment"> *</span>
<a name="l00009"></a>00009 <span class="comment"> * <hr></span>
<a name="l00010"></a>00010 <span class="comment"> *</span>
<a name="l00011"></a>00011 <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span>
<a name="l00012"></a>00012 <span class="comment"> * and its documentation for any purpose is hereby granted without</span>
<a name="l00013"></a>00013 <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span>
<a name="l00014"></a>00014 <span class="comment"> * LICENSE file provided with this distribution.</span>
<a name="l00015"></a>00015 <span class="comment"> * </span>
<a name="l00016"></a>00016 <span class="comment"> * <hr></span>
<a name="l00017"></a>00017 <span class="comment"> * </span>
<a name="l00018"></a>00018 <span class="comment"> */</span>
<a name="l00019"></a>00019 <span class="comment">/*****************************************************************************/</span>
<a name="l00020"></a>00020 <span class="comment">// CLASS: CommonTheoremProducer</span>
<a name="l00021"></a>00021 <span class="comment">//</span>
<a name="l00022"></a>00022 <span class="comment">// AUTHOR: Sergey Berezin, 12/09/2002</span>
<a name="l00023"></a>00023 <span class="comment">//</span>
<a name="l00024"></a>00024 <span class="comment">// Description: Implementation of the proof rules for ground</span>
<a name="l00025"></a>00025 <span class="comment">// equational logic (reflexivity, symmetry, transitivity, and</span>
<a name="l00026"></a>00026 <span class="comment">// substitutivity).</span>
<a name="l00027"></a>00027 <span class="comment">//</span><span class="comment"></span>
<a name="l00028"></a>00028 <span class="comment">///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00029"></a>00029 <span class="comment"></span>
<a name="l00030"></a>00030 <span class="preprocessor">#ifndef _cvc3__common_theorem_producer_h_</span>
<a name="l00031"></a>00031 <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__common_theorem_producer_h_</span>
<a name="l00032"></a>00032 <span class="preprocessor"></span>
<a name="l00033"></a>00033 <span class="preprocessor">#include "<a class="code" href="common__proof__rules_8h.html">common_proof_rules.h</a>"</span>
<a name="l00034"></a>00034 <span class="preprocessor">#include "<a class="code" href="theorem__producer_8h.html">theorem_producer.h</a>"</span>
<a name="l00035"></a>00035 <span class="preprocessor">#include "<a class="code" href="theorem_8h.html">theorem.h</a>"</span>
<a name="l00036"></a>00036 <span class="preprocessor">#include "<a class="code" href="cdmap_8h.html">cdmap.h</a>"</span>
<a name="l00037"></a>00037
<a name="l00038"></a>00038 <span class="keyword">namespace </span>CVC3 {
<a name="l00039"></a>00039
<a name="l00040"></a><a class="code" href="classCVC3_1_1CommonTheoremProducer.html">00040</a> <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> {
<a name="l00041"></a>00041 <span class="keyword">private</span>:
<a name="l00042"></a>00042
<a name="l00043"></a>00043 <span class="comment">// TODO: do we need to record skolem axioms? do we need context-dependence?</span>
<a name="l00044"></a>00044
<a name="l00045"></a>00045 <span class="comment">// skolem axioms</span>
<a name="l00046"></a><a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a3ead097d78257116405995705a98a722">00046</a> std::vector<Theorem> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a3ead097d78257116405995705a98a722">d_skolem_axioms</a>;
<a name="l00047"></a>00047
<a name="l00048"></a>00048 <span class="comment">/* @brief Keep skolemization axioms so that they can be reused </span>
<a name="l00049"></a>00049 <span class="comment"> without being recreated each time */</span>
<a name="l00050"></a><a class="code" href="classCVC3_1_1CommonTheoremProducer.html#ab4d87623f3ff65970b5c015b39db5987">00050</a> <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>;
<a name="l00051"></a>00051 <span class="comment"></span>
<a name="l00052"></a>00052 <span class="comment"> //! Mapping of e to "|- e = v" for fresh Skolem vars v</span>
<a name="l00053"></a><a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a628cb0e578632642b6a2c8d48ddeb890">00053</a> <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>;
<a name="l00054"></a>00054 <span class="comment"></span>
<a name="l00055"></a>00055 <span class="comment"> //! Helper function for liftOneITE</span>
<a name="l00056"></a>00056 <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);
<a name="l00057"></a>00057
<a name="l00058"></a>00058 <span class="keyword">public</span>:
<a name="l00059"></a>00059 <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a2ae31c06ed093e9b5b85f90af78641ae">CommonTheoremProducer</a>(<a class="code" href="classCVC3_1_1TheoremManager.html">TheoremManager</a>* tm);
<a name="l00060"></a><a class="code" href="classCVC3_1_1CommonTheoremProducer.html#afed5498eb0373f7f482cc7fbf8eb857a">00060</a> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#afed5498eb0373f7f482cc7fbf8eb857a">~CommonTheoremProducer</a>() { }
<a name="l00061"></a>00061
<a name="l00062"></a>00062 <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);
<a name="l00063"></a>00063 <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,
<a name="l00064"></a>00064 <span class="keyword">const</span> std::vector<Expr>& assump,
<a name="l00065"></a>00065 <span class="keyword">const</span> std::vector<Theorem>& tccs);
<a name="l00066"></a>00066 <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);
<a name="l00067"></a>00067 <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);
<a name="l00068"></a>00068 <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);
<a name="l00069"></a>00069 <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);
<a name="l00070"></a>00070 <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);
<a name="l00071"></a>00071 <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,
<a name="l00072"></a>00072 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& a2_eq_a3);
<a name="l00073"></a>00073 <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,
<a name="l00074"></a>00074 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);
<a name="l00075"></a>00075 <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,
<a name="l00076"></a>00076 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm1,
<a name="l00077"></a>00077 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm2);
<a name="l00078"></a>00078 <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,
<a name="l00079"></a>00079 <span class="keyword">const</span> std::vector<Theorem>& thms);
<a name="l00080"></a>00080 <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,
<a name="l00081"></a>00081 <span class="keyword">const</span> std::vector<unsigned>& changed,
<a name="l00082"></a>00082 <span class="keyword">const</span> std::vector<Theorem>& thms);
<a name="l00083"></a>00083 <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,
<a name="l00084"></a>00084 <span class="keyword">const</span> <span class="keywordtype">int</span> changed,
<a name="l00085"></a>00085 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);
<a name="l00086"></a>00086 <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);
<a name="l00087"></a>00087 <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);
<a name="l00088"></a>00088 <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);
<a name="l00089"></a>00089 <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);
<a name="l00090"></a>00090 <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);
<a name="l00091"></a>00091 <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);
<a name="l00092"></a>00092 <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);
<a name="l00093"></a>00093 <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);
<a name="l00094"></a>00094 <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);
<a name="l00095"></a>00095 <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);
<a name="l00096"></a>00096 <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);
<a name="l00097"></a>00097 <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);
<a name="l00098"></a>00098 <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);
<a name="l00099"></a>00099 <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);
<a name="l00100"></a>00100 <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);
<a name="l00101"></a>00101 <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);
<a name="l00102"></a>00102 <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);
<a name="l00103"></a>00103 <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);
<a name="l00104"></a>00104 <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);
<a name="l00105"></a>00105 <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);
<a name="l00106"></a>00106 <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);
<a name="l00107"></a>00107 <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);
<a name="l00108"></a>00108 <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);
<a name="l00109"></a>00109 <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);
<a name="l00110"></a>00110 <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);
<a name="l00111"></a>00111 <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);
<a name="l00112"></a>00112 <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);
<a name="l00113"></a>00113 <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);
<a name="l00114"></a>00114 <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);
<a name="l00115"></a>00115 <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);
<a name="l00116"></a>00116 <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);
<a name="l00117"></a>00117 <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);
<a name="l00118"></a>00118 <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);
<a name="l00119"></a>00119 <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);
<a name="l00120"></a>00120 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a38a1b30499d07384066e9afca89f37c0" title="==> TRUE">trueTheorem</a>();
<a name="l00121"></a>00121 <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);
<a name="l00122"></a>00122 <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);
<a name="l00123"></a>00123 <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);
<a name="l00124"></a>00124 <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);
<a name="l00125"></a>00125
<a name="l00126"></a><a class="code" href="classCVC3_1_1CommonTheoremProducer.html#a8c83d415f39a7ac2f6a117972116c6b2">00126</a> 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>; }
<a name="l00127"></a><a class="code" href="classCVC3_1_1CommonTheoremProducer.html#ad7dc685e6e46a90802f2602a70b9674a">00127</a> <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(); }
<a name="l00128"></a>00128
<a name="l00129"></a>00129 }; <span class="comment">// end of class CommonTheoremProducer</span>
<a name="l00130"></a>00130
<a name="l00131"></a>00131 } <span class="comment">// end of namespace CVC3</span>
<a name="l00132"></a>00132
<a name="l00133"></a>00133 <span class="preprocessor">#endif</span>
</pre></div></div>
</div>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
