<!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: CVC3::CommonTheoremProducer Class Reference</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 class="current"><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="annotated.html"><span>Class List</span></a></li>
<li><a href="classes.html"><span>Class Index</span></a></li>
<li><a href="hierarchy.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="namespaceCVC3.html">CVC3</a> </li>
<li class="navelem"><a class="el" href="classCVC3_1_1CommonTheoremProducer.html">CommonTheoremProducer</a> </li>
</ul>
</div>
</div>
<div class="header">
<div class="summary">
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pri-methods">Private Member Functions</a> |
<a href="#pri-attribs">Private Attributes</a> </div>
<div class="headertitle">
<div class="title">CVC3::CommonTheoremProducer Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="CVC3::CommonTheoremProducer" --><!-- doxytag: inherits="CVC3::CommonProofRules,CVC3::TheoremProducer" -->
<p><code>#include <<a class="el" href="common__theorem__producer_8h_source.html">common_theorem_producer.h</a>></code></p>
<div class="dynheader">
Inheritance diagram for CVC3::CommonTheoremProducer:</div>
<div class="dyncontent">
<div class="center">
<img src="classCVC3_1_1CommonTheoremProducer.png" usemap="#CVC3::CommonTheoremProducer_map" alt=""/>
<map id="CVC3::CommonTheoremProducer_map" name="CVC3::CommonTheoremProducer_map">
<area href="classCVC3_1_1CommonProofRules.html" alt="CVC3::CommonProofRules" shape="rect" coords="0,0,202,24"/>
<area href="classCVC3_1_1TheoremProducer.html" alt="CVC3::TheoremProducer" shape="rect" coords="212,0,414,24"/>
</map>
</div></div>
<p><a href="classCVC3_1_1CommonTheoremProducer-members.html">List of all members.</a></p>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li><a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a2ae31c06ed093e9b5b85f90af78641ae">CommonTheoremProducer</a> (<a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a> *tm)
<li>virtual <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#afed5498eb0373f7f482cc7fbf8eb857a">~CommonTheoremProducer</a> ()
<li><a class="el" href="classCVC3_1_1Theorem3.html">Theorem3</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a685c913a4b6b80a546dcb9853a88e21a">queryTCC</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &phi, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &D_phi)
<dl class="el"><dd class="mdescRight">Convert 2-valued formula to 3-valued by discharging its TCC ( <img class="formulaInl" alt="$D_\phi$" src="form_232.png"/>): </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma_1\vdash_2 \phi\quad \Gamma_2\vdash_2 D_{\phi}} {\Gamma_1,\,\Gamma_2\vdash_3\phi}\]" src="form_233.png"/>
</p>
<p>. <a href="#a685c913a4b6b80a546dcb9853a88e21a"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem3.html">Theorem3</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#abf904962af8344d8646c382747837af4">implIntro3</a> (const <a class="el" href="classCVC3_1_1Theorem3.html">Theorem3</a> &phi, const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &assump, const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &tccs)
<dl class="el"><dd class="mdescRight">3-valued implication introduction rule: </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma_0,\,\alpha_1\,\ldots,\,\alpha_n\vdash_3\phi\quad (\Gamma_i\vdash D_{\alpha_i})_{i\in[1..n]}} {\Gamma_0,\,\Gamma_1, \ldots, \Gamma_n\vdash_3 (\bigwedge_{i=1}^n\alpha_i)\to\phi}\]" src="form_234.png"/>
</p>
<a href="#abf904962af8344d8646c382747837af4"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a28d225c0e86bf45df3441c14a11197be">assumpRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &a, int scope=-1)
<dl class="el"><dd class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{}{a\vdash a}\]" src="form_237.png"/>
</p>
<a href="#a28d225c0e86bf45df3441c14a11197be"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a306058f7ced3d7220b2d1a40892faae7">reflexivityRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &a)
<dl class="el"><dd class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{}{a = a}\quad or \quad\frac{}{a \Leftrightarrow a}\]" src="form_238.png"/>
</p>
<a href="#a306058f7ced3d7220b2d1a40892faae7"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a26b00cb395f45971ace24a4529189e1b">rewriteReflexivity</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &t)
<dl class="el"><dd class="mdescRight">==> (a == a) IFF TRUE <a href="#a26b00cb395f45971ace24a4529189e1b"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#ab269d27c05584ade0b1f86f2ced0c46a">symmetryRule</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &a1_eq_a2)
<dl class="el"><dd class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{a_1=a_2}{a_2=a_1}\]" src="form_239.png"/>
</p>
<p> (same for IFF) <a href="#ab269d27c05584ade0b1f86f2ced0c46a"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#ac0813c68583ad6f0661d4c1affe3c6d8">rewriteUsingSymmetry</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &a1_eq_a2)
<dl class="el"><dd class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{}{(a_1=a_2)\Leftrightarrow (a_2=a_1)}\]" src="form_240.png"/>
</p>
<a href="#ac0813c68583ad6f0661d4c1affe3c6d8"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#ad5c0bc0fb82634039e5f2c8f9291de0e">transitivityRule</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &a1_eq_a2, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &a2_eq_a3)
<dl class="el"><dd class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{a_1=a_2\quad a_2=a_3}{a_1=a_3}\]" src="form_241.png"/>
</p>
<p> (same for IFF) <a href="#ad5c0bc0fb82634039e5f2c8f9291de0e"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#aac39a4ae729b4218d4b70ed6a68bc53d">substitutivityRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)
<dl class="el"><dd class="mdescRight">Optimized case for expr with one child. <a href="#aac39a4ae729b4218d4b70ed6a68bc53d"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a78ce0fe500f548d464b63e19211836f8">substitutivityRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm1, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm2)
<dl class="el"><dd class="mdescRight">Optimized case for expr with two children. <a href="#a78ce0fe500f548d464b63e19211836f8"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a3cbe9d25e0363d61a29179592561ddb9">substitutivityRule</a> (const <a class="el" href="classCVC3_1_1Op.html">Op</a> &op, const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &thms)
<dl class="el"><dd class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{(c_1=d_1)\wedge\ldots\wedge(c_n=d_n)} {op(c_1,\ldots,c_n)=op(d_1,\ldots,d_n)}\]" src="form_242.png"/>
</p>
<a href="#a3cbe9d25e0363d61a29179592561ddb9"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a395cee7c667e641b2835748d0a8c4a9d">substitutivityRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, const std::vector< unsigned > &changed, const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &thms)
<dl class="el"><dd class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{(c_1=d_1)\wedge\ldots\wedge(c_n=d_n)} {op(c_1,\ldots,c_n)=op(d_1,\ldots,d_n)}\]" src="form_242.png"/>
</p>
<p> except that only those arguments are given that <img class="formulaInl" alt="$c_i\not=d_i$" src="form_243.png"/>. <a href="#a395cee7c667e641b2835748d0a8c4a9d"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#afeddaca97606b242861d6e05a97f62d7">substitutivityRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, const int changed, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)
<li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#aaa58b8a459f5678aa2393fba6b50ff8d">contradictionRule</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &not_e)
<dl class="el"><dd class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma_1\vdash e\quad\Gamma_2\vdash \neg e} {\Gamma_1\cup\Gamma_2\vdash \mathrm{FALSE}} \]" src="form_246.png"/>
</p>
<a href="#aaa58b8a459f5678aa2393fba6b50ff8d"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#ad6ecd5f3d95b2f44d670ad1228a88f4a">excludedMiddle</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a37ed2850e80cd789f7ac712df6eacc63">iffTrue</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e)
<dl class="el"><dd class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma\vdash e}{\Gamma\vdash e\Leftrightarrow\mathrm{TRUE}}\]" src="form_247.png"/>
</p>
<a href="#a37ed2850e80cd789f7ac712df6eacc63"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a2b95f985a56f8d25b00145846406d70b">iffNotFalse</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e)
<dl class="el"><dd class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma\vdash e}{\Gamma\vdash\neg e\Leftrightarrow\mathrm{FALSE}}\]" src="form_248.png"/>
</p>
<a href="#a2b95f985a56f8d25b00145846406d70b"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a40da8d343ef923020c472eaace6e8122">iffTrueElim</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e)
<dl class="el"><dd class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma\vdash e\Leftrightarrow\mathrm{TRUE}}{\Gamma\vdash e}\]" src="form_249.png"/>
</p>
<a href="#a40da8d343ef923020c472eaace6e8122"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a4efade3a917467bf7287a19d2ee4ea2c">iffFalseElim</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e)
<dl class="el"><dd class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma\vdash e\Leftrightarrow\mathrm{FALSE}}{\Gamma\vdash\neg e}\]" src="form_250.png"/>
</p>
<a href="#a4efade3a917467bf7287a19d2ee4ea2c"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a3733173dbd8f639af979150059c4ec90">iffContrapositive</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)
<dl class="el"><dd class="mdescRight">e1 <=> e2 ==> ~e1 <=> ~e2 <a href="#a3733173dbd8f639af979150059c4ec90"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a59470692918d2f7c03c073a61daa3db5">notNotElim</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e)
<dl class="el"><dd class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma\vdash\neg\neg e}{\Gamma\vdash e}\]" src="form_252.png"/>
</p>
<a href="#a59470692918d2f7c03c073a61daa3db5"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a98f862538ac375b133079c336c539b22">iffMP</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e1, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e1_iff_e2)
<dl class="el"><dd class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma_1\vdash e_1\quad \Gamma_2\vdash(e_1\Leftrightarrow e_2)} {\Gamma_1\cup\Gamma_2\vdash e_2} \]" src="form_253.png"/>
</p>
<a href="#a98f862538ac375b133079c336c539b22"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#ac7155849ce6bd4afe185fdb0e397fc58">implMP</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e1, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e1_impl_e2)
<dl class="el"><dd class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma_1\vdash e_1\quad \Gamma_2\vdash(e_1\Rightarrow e_2)} {\Gamma_1\cup\Gamma_2\vdash e_2} \]" src="form_254.png"/>
</p>
<a href="#ac7155849ce6bd4afe185fdb0e397fc58"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a23e3f96d1cc6da39d97f9b7a2e0ba723">andElim</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e, int i)
<dl class="el"><dd class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\vdash e_1\wedge\cdots\wedge e_n}{\vdash e_i}\]" src="form_255.png"/>
</p>
<a href="#a23e3f96d1cc6da39d97f9b7a2e0ba723"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a733e7c5fe7b46d1af284c7c30c94025a">andIntro</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e1, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e2)
<dl class="el"><dd class="mdescRight">e1, e2 ==> AND(e1, e2) <a href="#a733e7c5fe7b46d1af284c7c30c94025a"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a27ccedb2c4fb06b63f4019effb22feff">andIntro</a> (const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &es)
<dl class="el"><dd class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma_1\vdash e_1\quad \cdots \quad\Gamma_n\vdash e_n} {\bigcup_{i=1}^n\Gamma_i\vdash \bigwedge_{i=1}^n e_i} \]" src="form_257.png"/>
</p>
<a href="#a27ccedb2c4fb06b63f4019effb22feff"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a414b98f6715044635975f8675f770c0b">implIntro</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &phi, const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &assump)
<dl class="el"><dd class="mdescRight">Implication introduction rule: </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma,\,\alpha_1\,\ldots,\,\alpha_n\vdash\phi} {\Gamma\vdash(\bigwedge_{i=1}^n\alpha_i)\to\phi}\]" src="form_258.png"/>
</p>
<p>. <a href="#a414b98f6715044635975f8675f770c0b"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a38bb194aa15b10dd0959cfff5e33014b">implContrapositive</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)
<dl class="el"><dd class="mdescRight">e1 => e2 ==> ~e2 => ~e1 <a href="#a38bb194aa15b10dd0959cfff5e33014b"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a2459a321ea5cdab974dc2cf029934a71">rewriteIteTrue</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">==> ITE(TRUE, e1, e2) == e1 <a href="#a2459a321ea5cdab974dc2cf029934a71"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a1711198c758a0475449b1889815f1371">rewriteIteFalse</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">==> ITE(FALSE, e1, e2) == e2 <a href="#a1711198c758a0475449b1889815f1371"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#aad60929c1c8c79287a16bc995cd9c51c">rewriteIteSame</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">==> ITE(c, e, e) == e <a href="#aad60929c1c8c79287a16bc995cd9c51c"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#ab9c0b6784e83fc0a4727a58c0a82b67a">notToIff</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &not_e)
<dl class="el"><dd class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\vdash\neg e}{\vdash e\Leftrightarrow\mathrm{FALSE}}\]" src="form_260.png"/>
</p>
<a href="#ab9c0b6784e83fc0a4727a58c0a82b67a"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a5b3a8e2d8bb3469935ecd1476778acaa">xorToIff</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\vdash e_1 XOR e_2}{\vdash e_1\Leftrightarrow(\neg e_2)}\]" src="form_261.png"/>
</p>
<a href="#a5b3a8e2d8bb3469935ecd1476778acaa"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#ab2233ef28defaf0af1b6a8cc4b887708">rewriteIff</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">==> (e1 <=> e2) <=> [simplified expr] <a href="#ab2233ef28defaf0af1b6a8cc4b887708"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#ad74cb42b63d2f92b55c79281e84816c1">rewriteAnd</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">==> AND(e1,e2) IFF [simplified expr] <a href="#ad74cb42b63d2f92b55c79281e84816c1"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#aa0d6b0fbe3838ae22b4a90d92d1530e2">rewriteOr</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">==> OR(e1,...,en) IFF [simplified expr] <a href="#aa0d6b0fbe3838ae22b4a90d92d1530e2"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a49ce394a818d2ab83b2f97d44cd66f1b">rewriteNotTrue</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">==> NOT TRUE IFF FALSE <a href="#a49ce394a818d2ab83b2f97d44cd66f1b"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#aace9193e3ff294ef6065178a55610e88">rewriteNotFalse</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">==> NOT FALSE IFF TRUE <a href="#aace9193e3ff294ef6065178a55610e88"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a84b83e300ddf9e67e427b2815ecff1e7">rewriteNotNot</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">==> NOT NOT e IFF e, takes !!e <a href="#a84b83e300ddf9e67e427b2815ecff1e7"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a6241bfc091691a667ed41a9d36d4cab6">rewriteNotForall</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &forallExpr)
<dl class="el"><dd class="mdescRight">==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e <a href="#a6241bfc091691a667ed41a9d36d4cab6"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a2535d1565f3f7b830063ad9ae3e1c4e7">rewriteNotExists</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &existsExpr)
<dl class="el"><dd class="mdescRight">==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e <a href="#a2535d1565f3f7b830063ad9ae3e1c4e7"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#adcd56f1052668c269d59b5001a01191f">skolemize</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a3bfb1ce883967f3822858b73156f99e9">skolemizeRewrite</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a5b97504309d324b509e18976b93a3c78">skolemizeRewriteVar</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Special version of skolemizeRewrite for "EXISTS x. t = x". <a href="#a5b97504309d324b509e18976b93a3c78"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#ac003e84b85d4f51746628fd0f738b7e3">varIntroRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">|- EXISTS x. e = x <a href="#ac003e84b85d4f51746628fd0f738b7e3"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a9c3d8d07344147c33394ab68ca490c04">skolemize</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)
<dl class="el"><dd class="mdescRight">If thm is (EXISTS x: phi(x)), create the Skolemized version and add it to the database. Otherwise returns just thm. <a href="#a9c3d8d07344147c33394ab68ca490c04"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a84f7da63e9d820ad781efa7e963733aa">varIntroSkolem</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Retrun a theorem "|- e = v" for a new Skolem constant v. <a href="#a84f7da63e9d820ad781efa7e963733aa"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a38a1b30499d07384066e9afca89f37c0">trueTheorem</a> ()
<dl class="el"><dd class="mdescRight">==> TRUE <a href="#a38a1b30499d07384066e9afca89f37c0"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a1f2d422ab4dd1297fbf6c4295a430f32">rewriteAnd</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e)
<dl class="el"><dd class="mdescRight">AND(e1,e2) ==> [simplified expr]. <a href="#a1f2d422ab4dd1297fbf6c4295a430f32"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a9f135d57462754cd9903190d4fe4aec8">rewriteOr</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e)
<dl class="el"><dd class="mdescRight">OR(e1,...,en) ==> [simplified expr]. <a href="#a9f135d57462754cd9903190d4fe4aec8"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a752f5927047540cc10f67d3d5ed179a7">ackermann</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e1, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e2)
<li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a749d1c718f05307dad5dcc3f6d2296a2">liftOneITE</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<li>std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a8c83d415f39a7ac2f6a117972116c6b2">getSkolemAxioms</a> ()
<li>void <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#ad7dc685e6e46a90802f2602a70b9674a">clearSkolemAxioms</a> ()
</ul>
<h2><a name="pri-methods"></a>
Private Member Functions</h2>
<ul>
<li>void <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a78038ee1c3cd8d3657a0261ce2f35eaf">findITE</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &condition, <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &thenpart, <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &elsepart)
<dl class="el"><dd class="mdescRight">Helper function for liftOneITE. <a href="#a78038ee1c3cd8d3657a0261ce2f35eaf"></a><br/></dl></ul>
<h2><a name="pri-attribs"></a>
Private Attributes</h2>
<ul>
<li>std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a3ead097d78257116405995705a98a722">d_skolem_axioms</a>
<li><a class="el" href="classCVC3_1_1CDMap.html">CDMap</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#ab4d87623f3ff65970b5c015b39db5987">d_skolemized_thms</a>
<li><a class="el" href="classCVC3_1_1CDMap.html">CDMap</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a628cb0e578632642b6a2c8d48ddeb890">d_skolemVars</a>
<dl class="el"><dd class="mdescRight">Mapping of e to "|- e = v" for fresh Skolem vars v. <a href="#a628cb0e578632642b6a2c8d48ddeb890"></a><br/></dl></ul>
<hr/><a name="details" id="details"></a><h2>Detailed Description</h2>
<div class="textblock">
<p>Definition at line <a class="el" href="common__theorem__producer_8h_source.html#l00040">40</a> of file <a class="el" href="common__theorem__producer_8h_source.html">common_theorem_producer.h</a>.</p>
</div><hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="a2ae31c06ed093e9b5b85f90af78641ae"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::CommonTheoremProducer" ref="a2ae31c06ed093e9b5b85f90af78641ae" args="(TheoremManager *tm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CommonTheoremProducer::CommonTheoremProducer </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a> * </td>
<td class="paramname"><em>tm</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00040">40</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="afed5498eb0373f7f482cc7fbf8eb857a"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::~CommonTheoremProducer" ref="afed5498eb0373f7f482cc7fbf8eb857a" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual CVC3::CommonTheoremProducer::~CommonTheoremProducer </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="common__theorem__producer_8h_source.html#l00060">60</a> of file <a class="el" href="common__theorem__producer_8h_source.html">common_theorem_producer.h</a>.</p>
</div>
</div>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="a78038ee1c3cd8d3657a0261ce2f35eaf"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::findITE" ref="a78038ee1c3cd8d3657a0261ce2f35eaf" args="(const Expr &e, Expr &condition, Expr &thenpart, Expr &elsepart)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CommonTheoremProducer::findITE </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>condition</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>thenpart</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>elsepart</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Helper function for liftOneITE. </p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l01322">1322</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="expr_8cpp_source.html#l00525">CVC3::Expr::containsTermITE()</a>, <a class="el" href="expr_8h_source.html#l01183">CVC3::Expr::getOp()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, and <a class="el" href="expr_8h_source.html#l00423">CVC3::Expr::isITE()</a>.</p>
<p>Referenced by <a class="el" href="common__theorem__producer_8cpp_source.html#l01359">liftOneITE()</a>.</p>
</div>
</div>
<a class="anchor" id="a685c913a4b6b80a546dcb9853a88e21a"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::queryTCC" ref="a685c913a4b6b80a546dcb9853a88e21a" args="(const Theorem &phi, const Theorem &D_phi)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem3.html">Theorem3</a> CommonTheoremProducer::queryTCC </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>phi</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>D_phi</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Convert 2-valued formula to 3-valued by discharging its TCC ( <img class="formulaInl" alt="$D_\phi$" src="form_232.png"/>): </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma_1\vdash_2 \phi\quad \Gamma_2\vdash_2 D_{\phi}} {\Gamma_1,\,\Gamma_2\vdash_3\phi}\]" src="form_233.png"/>
</p>
<p>. </p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a758fe978ff00099419c459914a0af5ba">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00055">55</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="assumptions_8cpp_source.html#l00200">CVC3::Assumptions::add()</a>, <a class="el" href="theorem_8cpp_source.html#l00385">CVC3::Theorem::getAssumptionsRef()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00133">CVC3::TheoremProducer::newTheorem3()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="abf904962af8344d8646c382747837af4"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::implIntro3" ref="abf904962af8344d8646c382747837af4" args="(const Theorem3 &phi, const std::vector< Expr > &assump, const std::vector< Theorem > &tccs)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem3.html">Theorem3</a> CommonTheoremProducer::implIntro3 </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem3.html">Theorem3</a> & </td>
<td class="paramname"><em>phi</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>assump</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>tccs</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>3-valued implication introduction rule: </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma_0,\,\alpha_1\,\ldots,\,\alpha_n\vdash_3\phi\quad (\Gamma_i\vdash D_{\alpha_i})_{i\in[1..n]}} {\Gamma_0,\,\Gamma_1, \ldots, \Gamma_n\vdash_3 (\bigwedge_{i=1}^n\alpha_i)\to\phi}\]" src="form_234.png"/>
</p>
</p>
<dl><dt><b>Parameters:</b></dt><dd>
<table class="params">
<tr><td class="paramname">phi</td><td>is the formula <img class="formulaInl" alt="$\phi$" src="form_0.png"/> </td></tr>
<tr><td class="paramname">assump</td><td>is the vector of assumptions <img class="formulaInl" alt="$\alpha_1\ldots\alpha_n$" src="form_235.png"/> </td></tr>
<tr><td class="paramname">tccs</td><td>is the vector of TCCs for assumptions <img class="formulaInl" alt="$D_{\alpha_1}\ldots D_{\alpha_n}$" src="form_236.png"/> </td></tr>
</table>
</dd>
</dl>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#afe561cfd6d5ee752fbc1c3cafe9b68a5">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00085">85</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="assumptions_8cpp_source.html#l00200">CVC3::Assumptions::add()</a>, <a class="el" href="expr_8h_source.html#l00945">CVC3::andExpr()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem_8h_source.html#l00365">CVC3::Theorem3::getAssumptionsRef()</a>, <a class="el" href="theorem_8h_source.html#l00358">CVC3::Theorem3::getExpr()</a>, <a class="el" href="theorem_8h_source.html#l00370">CVC3::Theorem3::getProof()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="expr_8h_source.html#l00969">CVC3::Expr::impExpr()</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="theorem_8cpp_source.html#l00395">CVC3::Theorem::isAssump()</a>, <a class="el" href="theorem_8h_source.html#l00164">CVC3::Theorem::isNull()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00133">CVC3::TheoremProducer::newTheorem3()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, <a class="el" href="theorem__producer_8h_source.html#l00162">CVC3::TheoremProducer::withAssumptions()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a28d225c0e86bf45df3441c14a11197be"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::assumpRule" ref="a28d225c0e86bf45df3441c14a11197be" args="(const Expr &a, int scope=-1)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::assumpRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>a</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>scope</em> = <code>-1</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{}{a\vdash a}\]" src="form_237.png"/>
</p>
</p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#ab4527c48e9f88d94d7ca076757a6f3ba">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00154">154</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00129">CVC3::TheoremProducer::newAssumption()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00052">CVC3::TheoremProducer::newLabel()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a306058f7ced3d7220b2d1a40892faae7"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::reflexivityRule" ref="a306058f7ced3d7220b2d1a40892faae7" args="(const Expr &a)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::reflexivityRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>a</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{}{a = a}\quad or \quad\frac{}{a \Leftrightarrow a}\]" src="form_238.png"/>
</p>
</p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a61c1fe56b4ed9744006883a7784ddb71">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00162">162</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00125">CVC3::TheoremProducer::newReflTheorem()</a>.</p>
<p>Referenced by <a class="el" href="common__theorem__producer_8cpp_source.html#l00941">rewriteIff()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00221">rewriteUsingSymmetry()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00373">substitutivityRule()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00187">symmetryRule()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00245">transitivityRule()</a>, and <a class="el" href="common__theorem__producer_8cpp_source.html#l01280">trueTheorem()</a>.</p>
</div>
</div>
<a class="anchor" id="a26b00cb395f45971ace24a4529189e1b"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::rewriteReflexivity" ref="a26b00cb395f45971ace24a4529189e1b" args="(const Expr &t)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::rewriteReflexivity </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>a_eq_a</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> (a == a) IFF TRUE </p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#ad078b5d25129b200fe04b20c5962aa34">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00168">168</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem__producer_8h_source.html#l00095">CVC3::TheoremProducer::d_em</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l00419">CVC3::Expr::isEq()</a>, <a class="el" href="expr_8h_source.html#l00424">CVC3::Expr::isIff()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00118">CVC3::TheoremProducer::newRWTheorem()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, <a class="el" href="expr__manager_8h_source.html#l00280">CVC3::ExprManager::trueExpr()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
<p>Referenced by <a class="el" href="common__theorem__producer_8cpp_source.html#l00941">rewriteIff()</a>.</p>
</div>
</div>
<a class="anchor" id="ab269d27c05584ade0b1f86f2ced0c46a"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::symmetryRule" ref="ab269d27c05584ade0b1f86f2ced0c46a" args="(const Theorem &a1_eq_a2)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::symmetryRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>a1_eq_a2</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{a_1=a_2}{a_2=a_1}\]" src="form_239.png"/>
</p>
<p> (same for IFF) </p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a0a87e88508f49b73037e0024afa841bf">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00187">187</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00240">CVC3::Theorem::getLHS()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="theorem_8cpp_source.html#l00224">CVC3::Theorem::isRewrite()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00118">CVC3::TheoremProducer::newRWTheorem()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00162">reflexivityRule()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="ac0813c68583ad6f0661d4c1affe3c6d8"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::rewriteUsingSymmetry" ref="ac0813c68583ad6f0661d4c1affe3c6d8" args="(const Expr &a1_eq_a2)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::rewriteUsingSymmetry </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>a1_eq_a2</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{}{(a_1=a_2)\Leftrightarrow (a_2=a_1)}\]" src="form_240.png"/>
</p>
</p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a338cafc978d9b6a447e8d58af42d7e5b">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00221">221</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l00929">CVC3::Expr::eqExpr()</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="expr_8h_source.html#l00965">CVC3::Expr::iffExpr()</a>, <a class="el" href="expr_8h_source.html#l00419">CVC3::Expr::isEq()</a>, <a class="el" href="expr_8h_source.html#l00424">CVC3::Expr::isIff()</a>, <a class="el" href="type_8h_source.html#l00059">CVC3::Type::isNull()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00118">CVC3::TheoremProducer::newRWTheorem()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00162">reflexivityRule()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
<p>Referenced by <a class="el" href="common__theorem__producer_8cpp_source.html#l00941">rewriteIff()</a>.</p>
</div>
</div>
<a class="anchor" id="ad5c0bc0fb82634039e5f2c8f9291de0e"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::transitivityRule" ref="ad5c0bc0fb82634039e5f2c8f9291de0e" args="(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::transitivityRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>a1_eq_a2</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>a2_eq_a3</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{a_1=a_2\quad a_2=a_3}{a_1=a_3}\]" src="form_241.png"/>
</p>
<p> (same for IFF) </p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a4a4e90cd69ce24e83ba2c217907c277a">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00245">245</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00240">CVC3::Theorem::getLHS()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="type_8h_source.html#l00059">CVC3::Type::isNull()</a>, <a class="el" href="theorem_8h_source.html#l00164">CVC3::Theorem::isNull()</a>, <a class="el" href="theorem_8cpp_source.html#l00224">CVC3::Theorem::isRewrite()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00118">CVC3::TheoremProducer::newRWTheorem()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00162">reflexivityRule()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="aac39a4ae729b4218d4b70ed6a68bc53d"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::substitutivityRule" ref="aac39a4ae729b4218d4b70ed6a68bc53d" args="(const Expr &e, const Theorem &thm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::substitutivityRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Optimized case for expr with one child. </p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a776c827bb6e3b889234429c49ae9ad6f">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00302">302</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00240">CVC3::Theorem::getLHS()</a>, <a class="el" href="expr_8h_source.html#l01183">CVC3::Expr::getOp()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="theorem_8h_source.html#l00171">CVC3::Theorem::isRefl()</a>, <a class="el" href="theorem_8cpp_source.html#l00224">CVC3::Theorem::isRewrite()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00118">CVC3::TheoremProducer::newRWTheorem()</a>, <a class="el" href="theorem_8cpp_source.html#l00447">CVC3::Theorem::setSubst()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
<p>Referenced by <a class="el" href="common__theorem__producer_8cpp_source.html#l00424">substitutivityRule()</a>.</p>
</div>
</div>
<a class="anchor" id="a78ce0fe500f548d464b63e19211836f8"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::substitutivityRule" ref="a78ce0fe500f548d464b63e19211836f8" args="(const Expr &e, const Theorem &thm1, const Theorem &thm2)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::substitutivityRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm2</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Optimized case for expr with two children. </p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#abd65b6e03c3c57174b94a955d12cf266">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00332">332</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00240">CVC3::Theorem::getLHS()</a>, <a class="el" href="expr_8h_source.html#l01183">CVC3::Expr::getOp()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="theorem_8h_source.html#l00171">CVC3::Theorem::isRefl()</a>, <a class="el" href="theorem_8cpp_source.html#l00224">CVC3::Theorem::isRewrite()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00118">CVC3::TheoremProducer::newRWTheorem()</a>, <a class="el" href="theorem_8cpp_source.html#l00447">CVC3::Theorem::setSubst()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a3cbe9d25e0363d61a29179592561ddb9"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::substitutivityRule" ref="a3cbe9d25e0363d61a29179592561ddb9" args="(const Op &op, const std::vector< Theorem > &thms)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::substitutivityRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Op.html">Op</a> & </td>
<td class="paramname"><em>op</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>thms</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{(c_1=d_1)\wedge\ldots\wedge(c_n=d_n)} {op(c_1,\ldots,c_n)=op(d_1,\ldots,d_n)}\]" src="form_242.png"/>
</p>
</p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#aa1d9df2568ac3efade63925834c752e6">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00373">373</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem__producer_8h_source.html#l00094">CVC3::TheoremProducer::d_tm</a>, <a class="el" href="theorem__manager_8h_source.html#l00076">CVC3::TheoremManager::getEM()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="expr__manager_8h_source.html#l00454">CVC3::ExprManager::newLeafExpr()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00118">CVC3::TheoremProducer::newRWTheorem()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00162">reflexivityRule()</a>, <a class="el" href="theorem_8cpp_source.html#l00447">CVC3::Theorem::setSubst()</a>, <a class="el" href="expr__op_8cpp_source.html#l00038">CVC3::Op::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a395cee7c667e641b2835748d0a8c4a9d"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::substitutivityRule" ref="a395cee7c667e641b2835748d0a8c4a9d" args="(const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::substitutivityRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< unsigned > & </td>
<td class="paramname"><em>changed</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>thms</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{(c_1=d_1)\wedge\ldots\wedge(c_n=d_n)} {op(c_1,\ldots,c_n)=op(d_1,\ldots,d_n)}\]" src="form_242.png"/>
</p>
<p> except that only those arguments are given that <img class="formulaInl" alt="$c_i\not=d_i$" src="form_243.png"/>. </p>
<dl><dt><b>Parameters:</b></dt><dd>
<table class="params">
<tr><td class="paramname">e</td><td>is the original expression <img class="formulaInl" alt="$op(c_1,\ldots,c_n)$" src="form_244.png"/>. </td></tr>
<tr><td class="paramname">changed</td><td>is the vector of indices of changed kids </td></tr>
<tr><td class="paramname">thms</td><td>are the theorems <img class="formulaInl" alt="$c_i=d_i$" src="form_245.png"/> for the changed kids. </td></tr>
</table>
</dd>
</dl>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a23a0251820f022d14376c6e825291fa2">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00424">424</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr_8h_source.html#l01183">CVC3::Expr::getOp()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="theorem_8h_source.html#l00171">CVC3::Theorem::isRefl()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00118">CVC3::TheoremProducer::newRWTheorem()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00162">reflexivityRule()</a>, <a class="el" href="theorem_8cpp_source.html#l00447">CVC3::Theorem::setSubst()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00302">substitutivityRule()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="afeddaca97606b242861d6e05a97f62d7"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::substitutivityRule" ref="afeddaca97606b242861d6e05a97f62d7" args="(const Expr &e, const int changed, const Theorem &thm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::substitutivityRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const int </td>
<td class="paramname"><em>changed</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a5f4e51842d28b0ef5def4eecb65ae99c">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00509">509</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00240">CVC3::Theorem::getLHS()</a>, <a class="el" href="expr_8h_source.html#l01183">CVC3::Expr::getOp()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="theorem_8cpp_source.html#l00224">CVC3::Theorem::isRewrite()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00118">CVC3::TheoremProducer::newRWTheorem()</a>, <a class="el" href="theorem_8cpp_source.html#l00447">CVC3::Theorem::setSubst()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="aaa58b8a459f5678aa2393fba6b50ff8d"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::contradictionRule" ref="aaa58b8a459f5678aa2393fba6b50ff8d" args="(const Theorem &e, const Theorem &not_e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::contradictionRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>not_e</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma_1\vdash e\quad\Gamma_2\vdash \neg e} {\Gamma_1\cup\Gamma_2\vdash \mathrm{FALSE}} \]" src="form_246.png"/>
</p>
</p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a1074822d52c22daacaa78b34ac0635ba">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00561">561</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem__producer_8h_source.html#l00095">CVC3::TheoremProducer::d_em</a>, <a class="el" href="expr__manager_8h_source.html#l00278">CVC3::ExprManager::falseExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="theorem_8h_source.html#l00404">CVC3::Theorem::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="ad6ecd5f3d95b2f44d670ad1228a88f4a"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::excludedMiddle" ref="ad6ecd5f3d95b2f44d670ad1228a88f4a" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::excludedMiddle </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#aec56ab0fbac82267ff202ae328fe801f">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00580">580</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="expr_8h_source.html#l00951">CVC3::Expr::orExpr()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a37ed2850e80cd789f7ac712df6eacc63"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::iffTrue" ref="a37ed2850e80cd789f7ac712df6eacc63" args="(const Theorem &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::iffTrue </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma\vdash e}{\Gamma\vdash e\Leftrightarrow\mathrm{TRUE}}\]" src="form_247.png"/>
</p>
</p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#ae5a0a67c59ba15d84e900fdccc7653ca">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00591">591</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00095">CVC3::TheoremProducer::d_em</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00118">CVC3::TheoremProducer::newRWTheorem()</a>, <a class="el" href="expr__manager_8h_source.html#l00280">CVC3::ExprManager::trueExpr()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a2b95f985a56f8d25b00145846406d70b"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::iffNotFalse" ref="a2b95f985a56f8d25b00145846406d70b" args="(const Theorem &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::iffNotFalse </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma\vdash e}{\Gamma\vdash\neg e\Leftrightarrow\mathrm{FALSE}}\]" src="form_248.png"/>
</p>
</p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a5a56b6f9544841fe86255e5bc35e8449">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00602">602</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00095">CVC3::TheoremProducer::d_em</a>, <a class="el" href="expr__manager_8h_source.html#l00278">CVC3::ExprManager::falseExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00118">CVC3::TheoremProducer::newRWTheorem()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a40da8d343ef923020c472eaace6e8122"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::iffTrueElim" ref="a40da8d343ef923020c472eaace6e8122" args="(const Theorem &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::iffTrueElim </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma\vdash e\Leftrightarrow\mathrm{TRUE}}{\Gamma\vdash e}\]" src="form_249.png"/>
</p>
</p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#ad2edb920405666bf6e9d21ae496ff6b3">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00612">612</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem_8cpp_source.html#l00240">CVC3::Theorem::getLHS()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="theorem_8cpp_source.html#l00224">CVC3::Theorem::isRewrite()</a>, <a class="el" href="expr_8h_source.html#l00356">CVC3::Expr::isTrue()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="theorem_8h_source.html#l00404">CVC3::Theorem::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
<p>Referenced by <a class="el" href="common__theorem__producer_8cpp_source.html#l01280">trueTheorem()</a>.</p>
</div>
</div>
<a class="anchor" id="a4efade3a917467bf7287a19d2ee4ea2c"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::iffFalseElim" ref="a4efade3a917467bf7287a19d2ee4ea2c" args="(const Theorem &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::iffFalseElim </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma\vdash e\Leftrightarrow\mathrm{FALSE}}{\Gamma\vdash\neg e}\]" src="form_250.png"/>
</p>
</p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a11b56754024b56844336954cf789a63a">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00626">626</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem_8cpp_source.html#l00240">CVC3::Theorem::getLHS()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="expr_8h_source.html#l00355">CVC3::Expr::isFalse()</a>, <a class="el" href="theorem_8cpp_source.html#l00224">CVC3::Theorem::isRewrite()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="theorem_8h_source.html#l00404">CVC3::Theorem::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a3733173dbd8f639af979150059c4ec90"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::iffContrapositive" ref="a3733173dbd8f639af979150059c4ec90" args="(const Theorem &thm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::iffContrapositive </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>e1 <=> e2 ==> ~e1 <=> ~e2 </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma\vdash e_1\Leftrightarrow e_2} {\Gamma\vdash\sim e_1\Leftrightarrow\sim e_2}\]" src="form_251.png"/>
</p>
<p> Where ~e is the <em>inverse</em> of e (that is, ~(!e') = e'). </p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#af38f25446a561384c3de66392c4d3544">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00641">641</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00240">CVC3::Theorem::getLHS()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="theorem_8cpp_source.html#l00224">CVC3::Theorem::isRewrite()</a>, <a class="el" href="expr_8h_source.html#l00937">CVC3::Expr::negate()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00118">CVC3::TheoremProducer::newRWTheorem()</a>, <a class="el" href="theorem_8h_source.html#l00404">CVC3::Theorem::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a59470692918d2f7c03c073a61daa3db5"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::notNotElim" ref="a59470692918d2f7c03c073a61daa3db5" args="(const Theorem &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::notNotElim </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>not_not_e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma\vdash\neg\neg e}{\Gamma\vdash e}\]" src="form_252.png"/>
</p>
</p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#ace6786234994faf89bc1b0ac8575278a">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00655">655</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="theorem_8h_source.html#l00404">CVC3::Theorem::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a98f862538ac375b133079c336c539b22"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::iffMP" ref="a98f862538ac375b133079c336c539b22" args="(const Theorem &e1, const Theorem &e1_iff_e2)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::iffMP </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>e1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>e1_iff_e2</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma_1\vdash e_1\quad \Gamma_2\vdash(e_1\Leftrightarrow e_2)} {\Gamma_1\cup\Gamma_2\vdash e_2} \]" src="form_253.png"/>
</p>
</p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#aebbcd4a194e4fdca0bcd16143fb03a75">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00667">667</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00240">CVC3::Theorem::getLHS()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="theorem_8cpp_source.html#l00224">CVC3::Theorem::isRewrite()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="theorem_8h_source.html#l00404">CVC3::Theorem::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
<p>Referenced by <a class="el" href="common__theorem__producer_8cpp_source.html#l01286">rewriteAnd()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l01292">rewriteOr()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l01223">skolemize()</a>, and <a class="el" href="common__theorem__producer_8cpp_source.html#l01250">varIntroSkolem()</a>.</p>
</div>
</div>
<a class="anchor" id="ac7155849ce6bd4afe185fdb0e397fc58"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::implMP" ref="ac7155849ce6bd4afe185fdb0e397fc58" args="(const Theorem &e1, const Theorem &e1_impl_e2)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::implMP </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>e1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>e1_impl_e2</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma_1\vdash e_1\quad \Gamma_2\vdash(e_1\Rightarrow e_2)} {\Gamma_1\cup\Gamma_2\vdash e_2} \]" src="form_254.png"/>
</p>
</p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a86416b3ccec1ddf1ce534b53d6af1ec9">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00692">692</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="expr_8h_source.html#l00425">CVC3::Expr::isImpl()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="theorem_8h_source.html#l00404">CVC3::Theorem::toString()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a23e3f96d1cc6da39d97f9b7a2e0ba723"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::andElim" ref="a23e3f96d1cc6da39d97f9b7a2e0ba723" args="(const Theorem &e, int i)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::andElim </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\vdash e_1\wedge\cdots\wedge e_n}{\vdash e_i}\]" src="form_255.png"/>
</p>
</p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a3f3592ac74d0aa0caa3b9224ea7e61f4">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00718">718</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem__producer_8h_source.html#l00095">CVC3::TheoremProducer::d_em</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="expr_8h_source.html#l00421">CVC3::Expr::isAnd()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="expr__manager_8h_source.html#l00471">CVC3::ExprManager::newRatExpr()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="theorem_8h_source.html#l00404">CVC3::Theorem::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a733e7c5fe7b46d1af284c7c30c94025a"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::andIntro" ref="a733e7c5fe7b46d1af284c7c30c94025a" args="(const Theorem &e1, const Theorem &e2)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::andIntro </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>e1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>e2</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>e1, e2 ==> AND(e1, e2) </p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a4aa193bfeb969c96b63db39a70470015">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00733">733</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="a27ccedb2c4fb06b63f4019effb22feff"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::andIntro" ref="a27ccedb2c4fb06b63f4019effb22feff" args="(const std::vector< Theorem > &es)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::andIntro </td>
<td>(</td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>es</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma_1\vdash e_1\quad \cdots \quad\Gamma_n\vdash e_n} {\bigcup_{i=1}^n\Gamma_i\vdash \bigwedge_{i=1}^n e_i} \]" src="form_257.png"/>
</p>
</p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a8fadf7698616e688d0db569b7db6e5fe">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00741">741</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l00945">CVC3::andExpr()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a414b98f6715044635975f8675f770c0b"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::implIntro" ref="a414b98f6715044635975f8675f770c0b" args="(const Theorem &phi, const std::vector< Expr > &assump)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::implIntro </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>phi</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>assump</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implication introduction rule: </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma,\,\alpha_1\,\ldots,\,\alpha_n\vdash\phi} {\Gamma\vdash(\bigwedge_{i=1}^n\alpha_i)\to\phi}\]" src="form_258.png"/>
</p>
<p>. </p>
<dl><dt><b>Parameters:</b></dt><dd>
<table class="params">
<tr><td class="paramname">phi</td><td>is the formula <img class="formulaInl" alt="$\phi$" src="form_0.png"/> </td></tr>
<tr><td class="paramname">assump</td><td>is the vector of assumptions <img class="formulaInl" alt="$\alpha_1\ldots\alpha_n$" src="form_235.png"/> </td></tr>
</table>
</dd>
</dl>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a9292e13acd4b5ba2b215864022a22573">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00775">775</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l00945">CVC3::andExpr()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem_8cpp_source.html#l00385">CVC3::Theorem::getAssumptionsRef()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="expr_8h_source.html#l00969">CVC3::Expr::impExpr()</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="theorem_8cpp_source.html#l00395">CVC3::Theorem::isAssump()</a>, <a class="el" href="theorem_8h_source.html#l00164">CVC3::Theorem::isNull()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, <a class="el" href="theorem__producer_8h_source.html#l00162">CVC3::TheoremProducer::withAssumptions()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a38bb194aa15b10dd0959cfff5e33014b"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::implContrapositive" ref="a38bb194aa15b10dd0959cfff5e33014b" args="(const Theorem &thm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::implContrapositive </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>e1 => e2 ==> ~e2 => ~e1 </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma\vdash e_1\Rightarrow e_2} {\Gamma\vdash\sim e_2\Rightarrow\sim e_1}\]" src="form_259.png"/>
</p>
<p> Where ~e is the <em>inverse</em> of e (that is, ~(!e') = e'). </p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a69da48e244e1674f6b501ac4ef168feb">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00825">825</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="expr_8h_source.html#l00425">CVC3::Expr::isImpl()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a2459a321ea5cdab974dc2cf029934a71"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::rewriteIteTrue" ref="a2459a321ea5cdab974dc2cf029934a71" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::rewriteIteTrue </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> ITE(TRUE, e1, e2) == e1 </p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a0e770e47e947275a69b4c9f225f8beb6">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00841">841</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="expr_8h_source.html#l00423">CVC3::Expr::isITE()</a>, <a class="el" href="type_8h_source.html#l00059">CVC3::Type::isNull()</a>, <a class="el" href="expr_8h_source.html#l00356">CVC3::Expr::isTrue()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00118">CVC3::TheoremProducer::newRWTheorem()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a1711198c758a0475449b1889815f1371"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::rewriteIteFalse" ref="a1711198c758a0475449b1889815f1371" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::rewriteIteFalse </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> ITE(FALSE, e1, e2) == e2 </p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a95af3ce5ccd4212b15bac9b249004c48">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00863">863</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="expr_8h_source.html#l00355">CVC3::Expr::isFalse()</a>, <a class="el" href="expr_8h_source.html#l00423">CVC3::Expr::isITE()</a>, <a class="el" href="type_8h_source.html#l00059">CVC3::Type::isNull()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00118">CVC3::TheoremProducer::newRWTheorem()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="aad60929c1c8c79287a16bc995cd9c51c"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::rewriteIteSame" ref="aad60929c1c8c79287a16bc995cd9c51c" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::rewriteIteSame </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> ITE(c, e, e) == e </p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a6cb02a9489ef5ed4e548f49bbd07439f">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00885">885</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="expr_8h_source.html#l00423">CVC3::Expr::isITE()</a>, <a class="el" href="type_8h_source.html#l00059">CVC3::Type::isNull()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00118">CVC3::TheoremProducer::newRWTheorem()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="ab9c0b6784e83fc0a4727a58c0a82b67a"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::notToIff" ref="ab9c0b6784e83fc0a4727a58c0a82b67a" args="(const Theorem &not_e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::notToIff </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>not_e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\vdash\neg e}{\vdash e\Leftrightarrow\mathrm{FALSE}}\]" src="form_260.png"/>
</p>
</p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a34064eea86afa953b9229537b075a420">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00906">906</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem__producer_8h_source.html#l00095">CVC3::TheoremProducer::d_em</a>, <a class="el" href="expr__manager_8h_source.html#l00278">CVC3::ExprManager::falseExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00118">CVC3::TheoremProducer::newRWTheorem()</a>, <a class="el" href="theorem_8h_source.html#l00404">CVC3::Theorem::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a5b3a8e2d8bb3469935ecd1476778acaa"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::xorToIff" ref="a5b3a8e2d8bb3469935ecd1476778acaa" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::xorToIff </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\vdash e_1 XOR e_2}{\vdash e_1\Leftrightarrow(\neg e_2)}\]" src="form_261.png"/>
</p>
</p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#ae25f68b7cceeeb25b41b1d2bcb1df8f3">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00922">922</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l00426">CVC3::Expr::isXor()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00118">CVC3::TheoremProducer::newRWTheorem()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="ab2233ef28defaf0af1b6a8cc4b887708"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::rewriteIff" ref="ab2233ef28defaf0af1b6a8cc4b887708" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::rewriteIff </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> (e1 <=> e2) <=> [simplified expr] </p>
<p>Rewrite formulas like FALSE/TRUE <=> e, e <=> NOT e, etc. </p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a5c50bf251b95dfc47ccfc6e8b51426c1">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00941">941</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem__producer_8h_source.html#l00095">CVC3::TheoremProducer::d_em</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="kinds_8h_source.html#l00036">FALSE_EXPR</a>, <a class="el" href="expr__manager_8h_source.html#l00278">CVC3::ExprManager::falseExpr()</a>, <a class="el" href="expr_8h_source.html#l00424">CVC3::Expr::isIff()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00118">CVC3::TheoremProducer::newRWTheorem()</a>, <a class="el" href="kinds_8h_source.html#l00066">NOT</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00162">reflexivityRule()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00168">rewriteReflexivity()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00221">rewriteUsingSymmetry()</a>, <a class="el" href="kinds_8h_source.html#l00035">TRUE_EXPR</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="ad74cb42b63d2f92b55c79281e84816c1"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::rewriteAnd" ref="ad74cb42b63d2f92b55c79281e84816c1" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::rewriteAnd </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> AND(e1,e2) IFF [simplified expr] </p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#afb2ae30738c04b088459281d259a6d3a">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00989">989</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l00945">CVC3::andExpr()</a>, <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr__map_8h_source.html#l00190">CVC3::ExprMap< Data >::begin()</a>, <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="expr__map_8h_source.html#l00173">CVC3::ExprMap< Data >::count()</a>, <a class="el" href="theorem__producer_8h_source.html#l00095">CVC3::TheoremProducer::d_em</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="expr__manager_8h_source.html#l00278">CVC3::ExprManager::falseExpr()</a>, <a class="el" href="expr_8h_source.html#l00421">CVC3::Expr::isAnd()</a>, <a class="el" href="expr_8h_source.html#l00355">CVC3::Expr::isFalse()</a>, <a class="el" href="expr_8h_source.html#l00356">CVC3::Expr::isTrue()</a>, <a class="el" href="expr_8h_source.html#l00937">CVC3::Expr::negate()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00118">CVC3::TheoremProducer::newRWTheorem()</a>, <a class="el" href="expr__map_8h_source.html#l00171">CVC3::ExprMap< Data >::size()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, <a class="el" href="expr__manager_8h_source.html#l00280">CVC3::ExprManager::trueExpr()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
<p>Referenced by <a class="el" href="common__theorem__producer_8cpp_source.html#l01286">rewriteAnd()</a>.</p>
</div>
</div>
<a class="anchor" id="aa0d6b0fbe3838ae22b4a90d92d1530e2"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::rewriteOr" ref="aa0d6b0fbe3838ae22b4a90d92d1530e2" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::rewriteOr </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> OR(e1,...,en) IFF [simplified expr] </p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#aa3cfb7d47a6d6bc84c85c7fa6a3e1242">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l01028">1028</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr__map_8h_source.html#l00190">CVC3::ExprMap< Data >::begin()</a>, <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="expr__map_8h_source.html#l00173">CVC3::ExprMap< Data >::count()</a>, <a class="el" href="theorem__producer_8h_source.html#l00095">CVC3::TheoremProducer::d_em</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="expr__manager_8h_source.html#l00278">CVC3::ExprManager::falseExpr()</a>, <a class="el" href="expr_8h_source.html#l00355">CVC3::Expr::isFalse()</a>, <a class="el" href="expr_8h_source.html#l00422">CVC3::Expr::isOr()</a>, <a class="el" href="expr_8h_source.html#l00356">CVC3::Expr::isTrue()</a>, <a class="el" href="expr_8h_source.html#l00937">CVC3::Expr::negate()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00118">CVC3::TheoremProducer::newRWTheorem()</a>, <a class="el" href="expr_8h_source.html#l00955">CVC3::orExpr()</a>, <a class="el" href="expr__map_8h_source.html#l00171">CVC3::ExprMap< Data >::size()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, <a class="el" href="expr__manager_8h_source.html#l00280">CVC3::ExprManager::trueExpr()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
<p>Referenced by <a class="el" href="common__theorem__producer_8cpp_source.html#l01292">rewriteOr()</a>.</p>
</div>
</div>
<a class="anchor" id="a49ce394a818d2ab83b2f97d44cd66f1b"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::rewriteNotTrue" ref="a49ce394a818d2ab83b2f97d44cd66f1b" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::rewriteNotTrue </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> NOT TRUE IFF FALSE </p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#ad55b11590196fbd73d24daa1d0d6eeb1">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l01066">1066</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem__producer_8h_source.html#l00095">CVC3::TheoremProducer::d_em</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr__manager_8h_source.html#l00278">CVC3::ExprManager::falseExpr()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="expr_8h_source.html#l00356">CVC3::Expr::isTrue()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00118">CVC3::TheoremProducer::newRWTheorem()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="aace9193e3ff294ef6065178a55610e88"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::rewriteNotFalse" ref="aace9193e3ff294ef6065178a55610e88" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::rewriteNotFalse </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> NOT FALSE IFF TRUE </p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a30fa79637f4308e8e733015624293775">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l01078">1078</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem__producer_8h_source.html#l00095">CVC3::TheoremProducer::d_em</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l00355">CVC3::Expr::isFalse()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00118">CVC3::TheoremProducer::newRWTheorem()</a>, <a class="el" href="expr__manager_8h_source.html#l00280">CVC3::ExprManager::trueExpr()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a84b83e300ddf9e67e427b2815ecff1e7"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::rewriteNotNot" ref="a84b83e300ddf9e67e427b2815ecff1e7" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::rewriteNotNot </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> NOT NOT e IFF e, takes !!e </p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a8a04ff29591a019d4d4cf073c0987316">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l01090">1090</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00118">CVC3::TheoremProducer::newRWTheorem()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a6241bfc091691a667ed41a9d36d4cab6"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::rewriteNotForall" ref="a6241bfc091691a667ed41a9d36d4cab6" args="(const Expr &forallExpr)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::rewriteNotForall </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>forallExpr</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e </p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#ad14f0ceb0d486ba3d78c2c3c6e47382a">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l01102">1102</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem__producer_8h_source.html#l00095">CVC3::TheoremProducer::d_em</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="kinds_8h_source.html#l00085">EXISTS</a>, <a class="el" href="expr_8h_source.html#l01069">CVC3::Expr::getBody()</a>, <a class="el" href="expr_8h_source.html#l01062">CVC3::Expr::getVars()</a>, <a class="el" href="expr_8h_source.html#l00428">CVC3::Expr::isForall()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="expr__manager_8h_source.html#l00506">CVC3::ExprManager::newClosureExpr()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00118">CVC3::TheoremProducer::newRWTheorem()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a2535d1565f3f7b830063ad9ae3e1c4e7"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::rewriteNotExists" ref="a2535d1565f3f7b830063ad9ae3e1c4e7" args="(const Expr &existsExpr)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::rewriteNotExists </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>existsExpr</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e </p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a12d8ca9f5547fb3a3239d7dc6f53987c">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l01117">1117</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem__producer_8h_source.html#l00095">CVC3::TheoremProducer::d_em</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="kinds_8h_source.html#l00084">FORALL</a>, <a class="el" href="expr_8h_source.html#l01069">CVC3::Expr::getBody()</a>, <a class="el" href="expr_8h_source.html#l01062">CVC3::Expr::getVars()</a>, <a class="el" href="expr_8h_source.html#l00429">CVC3::Expr::isExists()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="expr__manager_8h_source.html#l00506">CVC3::ExprManager::newClosureExpr()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00118">CVC3::TheoremProducer::newRWTheorem()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="adcd56f1052668c269d59b5001a01191f"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::skolemize" ref="adcd56f1052668c269d59b5001a01191f" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> CommonTheoremProducer::skolemize </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a015539886185195ba5d98c60cd7e8f66">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l01131">1131</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01069">CVC3::Expr::getBody()</a>, <a class="el" href="expr_8h_source.html#l01062">CVC3::Expr::getVars()</a>, <a class="el" href="expr_8h_source.html#l00977">CVC3::Expr::skolemExpr()</a>, and <a class="el" href="expr_8cpp_source.html#l00178">CVC3::Expr::substExpr()</a>.</p>
<p>Referenced by <a class="el" href="common__theorem__producer_8cpp_source.html#l01145">skolemizeRewrite()</a>.</p>
</div>
</div>
<a class="anchor" id="a3bfb1ce883967f3822858b73156f99e9"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::skolemizeRewrite" ref="a3bfb1ce883967f3822858b73156f99e9" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::skolemizeRewrite </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>skolem rewrite rule: Introduces axiom |- Exists(x) phi(x) <=> phi(c) where c is a constant defined by the expression Exists(x) phi(x) </p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a8a2561e9e4763460c65dbebe10d2f281">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l01145">1145</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l00965">CVC3::Expr::iffExpr()</a>, <a class="el" href="expr_8h_source.html#l00429">CVC3::Expr::isExists()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00052">CVC3::TheoremProducer::newLabel()</a>, <a class="el" href="theorem__producer_8h_source.html#l00118">CVC3::TheoremProducer::newRWTheorem()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l01131">skolemize()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
<p>Referenced by <a class="el" href="common__theorem__producer_8cpp_source.html#l01223">skolemize()</a>.</p>
</div>
</div>
<a class="anchor" id="a5b97504309d324b509e18976b93a3c78"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::skolemizeRewriteVar" ref="a5b97504309d324b509e18976b93a3c78" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::skolemizeRewriteVar </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Special version of skolemizeRewrite for "EXISTS x. t = x". </p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a4013a795d82cebb8b60ed67c094a7cba">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l01165">1165</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l01069">CVC3::Expr::getBody()</a>, <a class="el" href="expr_8h_source.html#l01183">CVC3::Expr::getOp()</a>, <a class="el" href="expr_8h_source.html#l01062">CVC3::Expr::getVars()</a>, <a class="el" href="expr_8h_source.html#l00965">CVC3::Expr::iffExpr()</a>, <a class="el" href="expr_8h_source.html#l00419">CVC3::Expr::isEq()</a>, <a class="el" href="expr_8h_source.html#l00429">CVC3::Expr::isExists()</a>, <a class="el" href="expr_8h_source.html#l00424">CVC3::Expr::isIff()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00052">CVC3::TheoremProducer::newLabel()</a>, <a class="el" href="theorem__producer_8h_source.html#l00118">CVC3::TheoremProducer::newRWTheorem()</a>, <a class="el" href="expr_8h_source.html#l00977">CVC3::Expr::skolemExpr()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
<p>Referenced by <a class="el" href="common__theorem__producer_8cpp_source.html#l01250">varIntroSkolem()</a>.</p>
</div>
</div>
<a class="anchor" id="ac003e84b85d4f51746628fd0f738b7e3"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::varIntroRule" ref="ac003e84b85d4f51746628fd0f738b7e3" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::varIntroRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>|- EXISTS x. e = x </p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#aab746efc9d013643bccc065affa82992">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l01202">1202</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00095">CVC3::TheoremProducer::d_em</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l00929">CVC3::Expr::eqExpr()</a>, <a class="el" href="kinds_8h_source.html#l00085">EXISTS</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="expr_8h_source.html#l00965">CVC3::Expr::iffExpr()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="expr__manager_8h_source.html#l00484">CVC3::ExprManager::newBoundVarExpr()</a>, <a class="el" href="expr__manager_8h_source.html#l00506">CVC3::ExprManager::newClosureExpr()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
<p>Referenced by <a class="el" href="common__theorem__producer_8cpp_source.html#l01250">varIntroSkolem()</a>.</p>
</div>
</div>
<a class="anchor" id="a9c3d8d07344147c33394ab68ca490c04"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::skolemize" ref="a9c3d8d07344147c33394ab68ca490c04" args="(const Theorem &thm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::skolemize </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>If thm is (EXISTS x: phi(x)), create the Skolemized version and add it to the database. Otherwise returns just thm. </p>
<dl><dt><b>Parameters:</b></dt><dd>
<table class="params">
<tr><td class="paramname">thm</td><td>is the <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>(EXISTS x: phi(x)) </td></tr>
</table>
</dd>
</dl>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#aed771f6a74d1a336cc08bfcfaf8169da">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l01223">1223</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="common__theorem__producer_8h_source.html#l00046">d_skolem_axioms</a>, <a class="el" href="common__theorem__producer_8h_source.html#l00050">d_skolemized_thms</a>, <a class="el" href="cdmap_8h_source.html#l00258">CVC3::CDMap< Key, Data, HashFcn >::end()</a>, <a class="el" href="cdmap_8h_source.html#l00303">CVC3::CDMap< Key, Data, HashFcn >::find()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="expr_8h_source.html#l01062">CVC3::Expr::getVars()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00667">iffMP()</a>, <a class="el" href="cdmap_8h_source.html#l00190">CVC3::CDMap< Key, Data, HashFcn >::insert()</a>, <a class="el" href="expr_8h_source.html#l00429">CVC3::Expr::isExists()</a>, <a class="el" href="expr_8h_source.html#l00977">CVC3::Expr::skolemExpr()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l01145">skolemizeRewrite()</a>, and <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>.</p>
</div>
</div>
<a class="anchor" id="a84f7da63e9d820ad781efa7e963733aa"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::varIntroSkolem" ref="a84f7da63e9d820ad781efa7e963733aa" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::varIntroSkolem </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Retrun a theorem "|- e = v" for a new Skolem constant v. </p>
<p>This is equivalent to skolemize(d_core->varIntroRule(e)), only more efficient. </p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a10fa187373ec24079c10874d8e804ecb">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l01250">1250</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="common__theorem__producer_8h_source.html#l00046">d_skolem_axioms</a>, <a class="el" href="common__theorem__producer_8h_source.html#l00050">d_skolemized_thms</a>, <a class="el" href="common__theorem__producer_8h_source.html#l00053">d_skolemVars</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="cdmap_8h_source.html#l00258">CVC3::CDMap< Key, Data, HashFcn >::end()</a>, <a class="el" href="cdmap_8h_source.html#l00303">CVC3::CDMap< Key, Data, HashFcn >::find()</a>, <a class="el" href="expr_8h_source.html#l01062">CVC3::Expr::getVars()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00667">iffMP()</a>, <a class="el" href="cdmap_8h_source.html#l00190">CVC3::CDMap< Key, Data, HashFcn >::insert()</a>, <a class="el" href="expr_8h_source.html#l00429">CVC3::Expr::isExists()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l01165">skolemizeRewriteVar()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="common__theorem__producer_8cpp_source.html#l01202">varIntroRule()</a>.</p>
</div>
</div>
<a class="anchor" id="a38a1b30499d07384066e9afca89f37c0"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::trueTheorem" ref="a38a1b30499d07384066e9afca89f37c0" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::trueTheorem </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> TRUE </p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a6e93694c76f7b567487bc8cae674ae5d">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l01280">1280</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00095">CVC3::TheoremProducer::d_em</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00612">iffTrueElim()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00162">reflexivityRule()</a>, and <a class="el" href="expr__manager_8h_source.html#l00280">CVC3::ExprManager::trueExpr()</a>.</p>
</div>
</div>
<a class="anchor" id="a1f2d422ab4dd1297fbf6c4295a430f32"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::rewriteAnd" ref="a1f2d422ab4dd1297fbf6c4295a430f32" args="(const Theorem &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::rewriteAnd </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>AND(e1,e2) ==> [simplified expr]. </p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a1d546d9530a3c15cd627a141137a8616">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l01286">1286</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00667">iffMP()</a>, and <a class="el" href="common__theorem__producer_8cpp_source.html#l00989">rewriteAnd()</a>.</p>
</div>
</div>
<a class="anchor" id="a9f135d57462754cd9903190d4fe4aec8"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::rewriteOr" ref="a9f135d57462754cd9903190d4fe4aec8" args="(const Theorem &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::rewriteOr </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>OR(e1,...,en) ==> [simplified expr]. </p>
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a44474beaa5761147eb816db48c795c4b">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l01292">1292</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00667">iffMP()</a>, and <a class="el" href="common__theorem__producer_8cpp_source.html#l01028">rewriteOr()</a>.</p>
</div>
</div>
<a class="anchor" id="a752f5927047540cc10f67d3d5ed179a7"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::ackermann" ref="a752f5927047540cc10f67d3d5ed179a7" args="(const Expr &e1, const Expr &e2)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::ackermann </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e2</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a484540b067da205d23b2fe263662cda2">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l01298">1298</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00067">AND</a>, <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l00929">CVC3::Expr::eqExpr()</a>, <a class="el" href="expr_8h_source.html#l01183">CVC3::Expr::getOp()</a>, <a class="el" href="expr_8h_source.html#l01014">CVC3::Expr::isApply()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a749d1c718f05307dad5dcc3f6d2296a2"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::liftOneITE" ref="a749d1c718f05307dad5dcc3f6d2296a2" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CommonTheoremProducer::liftOneITE </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a893a258d9f7d49acb5c8a8b5b8ec39b0">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l01359">1359</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="expr_8cpp_source.html#l00525">CVC3::Expr::containsTermITE()</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l01322">findITE()</a>, <a class="el" href="expr_8h_source.html#l00961">CVC3::Expr::iteExpr()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00118">CVC3::TheoremProducer::newRWTheorem()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a8c83d415f39a7ac2f6a117972116c6b2"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::getSkolemAxioms" ref="a8c83d415f39a7ac2f6a117972116c6b2" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<<a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>>& CVC3::CommonTheoremProducer::getSkolemAxioms </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#ac773341edabcc5091ca25af74fcb7653">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8h_source.html#l00126">126</a> of file <a class="el" href="common__theorem__producer_8h_source.html">common_theorem_producer.h</a>.</p>
<p>References <a class="el" href="common__theorem__producer_8h_source.html#l00046">d_skolem_axioms</a>.</p>
</div>
</div>
<a class="anchor" id="ad7dc685e6e46a90802f2602a70b9674a"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::clearSkolemAxioms" ref="ad7dc685e6e46a90802f2602a70b9674a" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::CommonTheoremProducer::clearSkolemAxioms </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classCVC3_1_1CommonProofRules.html#a6f8068606f30fe7b2c405ddf5ce1a53b">CVC3::CommonProofRules</a>.</p>
<p>Definition at line <a class="el" href="common__theorem__producer_8h_source.html#l00127">127</a> of file <a class="el" href="common__theorem__producer_8h_source.html">common_theorem_producer.h</a>.</p>
<p>References <a class="el" href="common__theorem__producer_8h_source.html#l00046">d_skolem_axioms</a>.</p>
</div>
</div>
<hr/><h2>Member Data Documentation</h2>
<a class="anchor" id="a3ead097d78257116405995705a98a722"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::d_skolem_axioms" ref="a3ead097d78257116405995705a98a722" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<<a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a3ead097d78257116405995705a98a722">CVC3::CommonTheoremProducer::d_skolem_axioms</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="common__theorem__producer_8h_source.html#l00046">46</a> of file <a class="el" href="common__theorem__producer_8h_source.html">common_theorem_producer.h</a>.</p>
<p>Referenced by <a class="el" href="common__theorem__producer_8h_source.html#l00127">clearSkolemAxioms()</a>, <a class="el" href="common__theorem__producer_8h_source.html#l00126">getSkolemAxioms()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l01223">skolemize()</a>, and <a class="el" href="common__theorem__producer_8cpp_source.html#l01250">varIntroSkolem()</a>.</p>
</div>
</div>
<a class="anchor" id="ab4d87623f3ff65970b5c015b39db5987"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::d_skolemized_thms" ref="ab4d87623f3ff65970b5c015b39db5987" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDMap.html">CDMap</a><<a class="el" href="classCVC3_1_1Expr.html">Expr</a>, <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#ab4d87623f3ff65970b5c015b39db5987">CVC3::CommonTheoremProducer::d_skolemized_thms</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="common__theorem__producer_8h_source.html#l00050">50</a> of file <a class="el" href="common__theorem__producer_8h_source.html">common_theorem_producer.h</a>.</p>
<p>Referenced by <a class="el" href="common__theorem__producer_8cpp_source.html#l01223">skolemize()</a>, and <a class="el" href="common__theorem__producer_8cpp_source.html#l01250">varIntroSkolem()</a>.</p>
</div>
</div>
<a class="anchor" id="a628cb0e578632642b6a2c8d48ddeb890"></a><!-- doxytag: member="CVC3::CommonTheoremProducer::d_skolemVars" ref="a628cb0e578632642b6a2c8d48ddeb890" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDMap.html">CDMap</a><<a class="el" href="classCVC3_1_1Expr.html">Expr</a>, <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>> <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a628cb0e578632642b6a2c8d48ddeb890">CVC3::CommonTheoremProducer::d_skolemVars</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Mapping of e to "|- e = v" for fresh Skolem vars v. </p>
<p>Definition at line <a class="el" href="common__theorem__producer_8h_source.html#l00053">53</a> of file <a class="el" href="common__theorem__producer_8h_source.html">common_theorem_producer.h</a>.</p>
<p>Referenced by <a class="el" href="common__theorem__producer_8cpp_source.html#l01250">varIntroSkolem()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="common__theorem__producer_8h_source.html">common_theorem_producer.h</a></li>
<li><a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a></li>
</ul>
</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>
