<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<meta http-equiv="X-UA-Compatible" content="IE=9"/>
<title>CVC3: CVC3::CommonProofRules Class Reference</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="jquery.js"></script>
<script type="text/javascript" src="dynsections.js"></script>
<link href="doxygen.css" rel="stylesheet" type="text/css" />
</head>
<body>
<div id="top"><!-- do not remove this div, it is closed by doxygen! -->
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3
</div>
</td>
</tr>
</tbody>
</table>
</div>
<!-- end header part -->
<!-- Generated by Doxygen 1.8.2 -->
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li 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="inherits.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_1CommonProofRules.html">CommonProofRules</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="summary">
<a href="#pub-methods">Public Member Functions</a> |
<a href="classCVC3_1_1CommonProofRules-members.html">List of all members</a> </div>
<div class="headertitle">
<div class="title">CVC3::CommonProofRules Class Reference<span class="mlabels"><span class="mlabel">abstract</span></span></div> </div>
</div><!--header-->
<div class="contents">
<p><code>#include <<a class="el" href="common__proof__rules_8h_source.html">common_proof_rules.h</a>></code></p>
<p>Inherited by <a class="el" href="classCVC3_1_1CommonTheoremProducer.html">CVC3::CommonTheoremProducer</a>.</p>
<div class="dynheader">
Collaboration diagram for CVC3::CommonProofRules:</div>
<div class="dyncontent">
<div class="center"><img src="classCVC3_1_1CommonProofRules__coll__graph.gif" border="0" usemap="#CVC3_1_1CommonProofRules_coll__map" alt="Collaboration graph"/></div>
<map name="CVC3_1_1CommonProofRules_coll__map" id="CVC3_1_1CommonProofRules_coll__map">
</map>
</div>
<table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pub-methods"></a>
Public Member Functions</h2></td></tr>
<tr class="memitem:a334ad50333e9323968df2bc286de7a8f"><td class="memItemLeft" align="right" valign="top">virtual </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a334ad50333e9323968df2bc286de7a8f">~CommonProofRules</a> ()</td></tr>
<tr class="memdesc:a334ad50333e9323968df2bc286de7a8f"><td class="mdescLeft"> </td><td class="mdescRight">Destructor. <a href="#a334ad50333e9323968df2bc286de7a8f"></a><br/></td></tr>
<tr class="separator:a334ad50333e9323968df2bc286de7a8f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a758fe978ff00099419c459914a0af5ba"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem3.html">Theorem3</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a758fe978ff00099419c459914a0af5ba">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)=0</td></tr>
<tr class="memdesc:a758fe978ff00099419c459914a0af5ba"><td class="mdescLeft"> </td><td class="mdescRight">Convert 2-valued formula to 3-valued by discharging its TCC ( <img class="formulaInl" alt="$D_\phi$" src="form_224.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_225.png"/>
</p>
<p>. <a href="#a758fe978ff00099419c459914a0af5ba"></a><br/></td></tr>
<tr class="separator:a758fe978ff00099419c459914a0af5ba"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:afe561cfd6d5ee752fbc1c3cafe9b68a5"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem3.html">Theorem3</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#afe561cfd6d5ee752fbc1c3cafe9b68a5">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)=0</td></tr>
<tr class="memdesc:afe561cfd6d5ee752fbc1c3cafe9b68a5"><td class="mdescLeft"> </td><td 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_226.png"/>
</p>
<a href="#afe561cfd6d5ee752fbc1c3cafe9b68a5"></a><br/></td></tr>
<tr class="separator:afe561cfd6d5ee752fbc1c3cafe9b68a5"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab4527c48e9f88d94d7ca076757a6f3ba"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#ab4527c48e9f88d94d7ca076757a6f3ba">assumpRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &a, int scope=-1)=0</td></tr>
<tr class="memdesc:ab4527c48e9f88d94d7ca076757a6f3ba"><td class="mdescLeft"> </td><td class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{}{a\vdash a}\]" src="form_229.png"/>
</p>
<a href="#ab4527c48e9f88d94d7ca076757a6f3ba"></a><br/></td></tr>
<tr class="separator:ab4527c48e9f88d94d7ca076757a6f3ba"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a61c1fe56b4ed9744006883a7784ddb71"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a61c1fe56b4ed9744006883a7784ddb71">reflexivityRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &a)=0</td></tr>
<tr class="memdesc:a61c1fe56b4ed9744006883a7784ddb71"><td class="mdescLeft"> </td><td class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{}{a = a}\quad or \quad\frac{}{a \Leftrightarrow a}\]" src="form_230.png"/>
</p>
<a href="#a61c1fe56b4ed9744006883a7784ddb71"></a><br/></td></tr>
<tr class="separator:a61c1fe56b4ed9744006883a7784ddb71"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad078b5d25129b200fe04b20c5962aa34"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#ad078b5d25129b200fe04b20c5962aa34">rewriteReflexivity</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &a_eq_a)=0</td></tr>
<tr class="memdesc:ad078b5d25129b200fe04b20c5962aa34"><td class="mdescLeft"> </td><td class="mdescRight">==> (a == a) IFF TRUE <a href="#ad078b5d25129b200fe04b20c5962aa34"></a><br/></td></tr>
<tr class="separator:ad078b5d25129b200fe04b20c5962aa34"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0a87e88508f49b73037e0024afa841bf"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a0a87e88508f49b73037e0024afa841bf">symmetryRule</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &a1_eq_a2)=0</td></tr>
<tr class="memdesc:a0a87e88508f49b73037e0024afa841bf"><td class="mdescLeft"> </td><td class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{a_1=a_2}{a_2=a_1}\]" src="form_231.png"/>
</p>
<p> (same for IFF) <a href="#a0a87e88508f49b73037e0024afa841bf"></a><br/></td></tr>
<tr class="separator:a0a87e88508f49b73037e0024afa841bf"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a338cafc978d9b6a447e8d58af42d7e5b"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a338cafc978d9b6a447e8d58af42d7e5b">rewriteUsingSymmetry</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &a1_eq_a2)=0</td></tr>
<tr class="memdesc:a338cafc978d9b6a447e8d58af42d7e5b"><td class="mdescLeft"> </td><td class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{}{(a_1=a_2)\Leftrightarrow (a_2=a_1)}\]" src="form_232.png"/>
</p>
<a href="#a338cafc978d9b6a447e8d58af42d7e5b"></a><br/></td></tr>
<tr class="separator:a338cafc978d9b6a447e8d58af42d7e5b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a4a4e90cd69ce24e83ba2c217907c277a"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a4a4e90cd69ce24e83ba2c217907c277a">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)=0</td></tr>
<tr class="memdesc:a4a4e90cd69ce24e83ba2c217907c277a"><td class="mdescLeft"> </td><td 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_233.png"/>
</p>
<p> (same for IFF) <a href="#a4a4e90cd69ce24e83ba2c217907c277a"></a><br/></td></tr>
<tr class="separator:a4a4e90cd69ce24e83ba2c217907c277a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a776c827bb6e3b889234429c49ae9ad6f"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a776c827bb6e3b889234429c49ae9ad6f">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)=0</td></tr>
<tr class="memdesc:a776c827bb6e3b889234429c49ae9ad6f"><td class="mdescLeft"> </td><td class="mdescRight">Optimized case for expr with one child. <a href="#a776c827bb6e3b889234429c49ae9ad6f"></a><br/></td></tr>
<tr class="separator:a776c827bb6e3b889234429c49ae9ad6f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:abd65b6e03c3c57174b94a955d12cf266"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#abd65b6e03c3c57174b94a955d12cf266">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)=0</td></tr>
<tr class="memdesc:abd65b6e03c3c57174b94a955d12cf266"><td class="mdescLeft"> </td><td class="mdescRight">Optimized case for expr with two children. <a href="#abd65b6e03c3c57174b94a955d12cf266"></a><br/></td></tr>
<tr class="separator:abd65b6e03c3c57174b94a955d12cf266"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa1d9df2568ac3efade63925834c752e6"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#aa1d9df2568ac3efade63925834c752e6">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)=0</td></tr>
<tr class="memdesc:aa1d9df2568ac3efade63925834c752e6"><td class="mdescLeft"> </td><td 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_234.png"/>
</p>
<a href="#aa1d9df2568ac3efade63925834c752e6"></a><br/></td></tr>
<tr class="separator:aa1d9df2568ac3efade63925834c752e6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a23a0251820f022d14376c6e825291fa2"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a23a0251820f022d14376c6e825291fa2">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)=0</td></tr>
<tr class="memdesc:a23a0251820f022d14376c6e825291fa2"><td class="mdescLeft"> </td><td 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_234.png"/>
</p>
<p> except that only those arguments are given that <img class="formulaInl" alt="$c_i\not=d_i$" src="form_235.png"/>. <a href="#a23a0251820f022d14376c6e825291fa2"></a><br/></td></tr>
<tr class="separator:a23a0251820f022d14376c6e825291fa2"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5f4e51842d28b0ef5def4eecb65ae99c"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a5f4e51842d28b0ef5def4eecb65ae99c">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)=0</td></tr>
<tr class="separator:a5f4e51842d28b0ef5def4eecb65ae99c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a1074822d52c22daacaa78b34ac0635ba"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a1074822d52c22daacaa78b34ac0635ba">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)=0</td></tr>
<tr class="memdesc:a1074822d52c22daacaa78b34ac0635ba"><td class="mdescLeft"> </td><td 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_238.png"/>
</p>
<a href="#a1074822d52c22daacaa78b34ac0635ba"></a><br/></td></tr>
<tr class="separator:a1074822d52c22daacaa78b34ac0635ba"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aec56ab0fbac82267ff202ae328fe801f"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#aec56ab0fbac82267ff202ae328fe801f">excludedMiddle</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:aec56ab0fbac82267ff202ae328fe801f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae5a0a67c59ba15d84e900fdccc7653ca"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#ae5a0a67c59ba15d84e900fdccc7653ca">iffTrue</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e)=0</td></tr>
<tr class="memdesc:ae5a0a67c59ba15d84e900fdccc7653ca"><td class="mdescLeft"> </td><td class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma\vdash e}{\Gamma\vdash e\Leftrightarrow\mathrm{TRUE}}\]" src="form_239.png"/>
</p>
<a href="#ae5a0a67c59ba15d84e900fdccc7653ca"></a><br/></td></tr>
<tr class="separator:ae5a0a67c59ba15d84e900fdccc7653ca"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5a56b6f9544841fe86255e5bc35e8449"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a5a56b6f9544841fe86255e5bc35e8449">iffNotFalse</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e)=0</td></tr>
<tr class="memdesc:a5a56b6f9544841fe86255e5bc35e8449"><td class="mdescLeft"> </td><td class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma\vdash e}{\Gamma\vdash\neg e\Leftrightarrow\mathrm{FALSE}}\]" src="form_240.png"/>
</p>
<a href="#a5a56b6f9544841fe86255e5bc35e8449"></a><br/></td></tr>
<tr class="separator:a5a56b6f9544841fe86255e5bc35e8449"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad2edb920405666bf6e9d21ae496ff6b3"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#ad2edb920405666bf6e9d21ae496ff6b3">iffTrueElim</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e)=0</td></tr>
<tr class="memdesc:ad2edb920405666bf6e9d21ae496ff6b3"><td class="mdescLeft"> </td><td class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma\vdash e\Leftrightarrow\mathrm{TRUE}}{\Gamma\vdash e}\]" src="form_241.png"/>
</p>
<a href="#ad2edb920405666bf6e9d21ae496ff6b3"></a><br/></td></tr>
<tr class="separator:ad2edb920405666bf6e9d21ae496ff6b3"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a11b56754024b56844336954cf789a63a"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a11b56754024b56844336954cf789a63a">iffFalseElim</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e)=0</td></tr>
<tr class="memdesc:a11b56754024b56844336954cf789a63a"><td class="mdescLeft"> </td><td class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma\vdash e\Leftrightarrow\mathrm{FALSE}}{\Gamma\vdash\neg e}\]" src="form_242.png"/>
</p>
<a href="#a11b56754024b56844336954cf789a63a"></a><br/></td></tr>
<tr class="separator:a11b56754024b56844336954cf789a63a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:af38f25446a561384c3de66392c4d3544"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#af38f25446a561384c3de66392c4d3544">iffContrapositive</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)=0</td></tr>
<tr class="memdesc:af38f25446a561384c3de66392c4d3544"><td class="mdescLeft"> </td><td class="mdescRight">e1 <=> e2 ==> ~e1 <=> ~e2 <a href="#af38f25446a561384c3de66392c4d3544"></a><br/></td></tr>
<tr class="separator:af38f25446a561384c3de66392c4d3544"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ace6786234994faf89bc1b0ac8575278a"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#ace6786234994faf89bc1b0ac8575278a">notNotElim</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &not_not_e)=0</td></tr>
<tr class="memdesc:ace6786234994faf89bc1b0ac8575278a"><td class="mdescLeft"> </td><td class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma\vdash\neg\neg e}{\Gamma\vdash e}\]" src="form_244.png"/>
</p>
<a href="#ace6786234994faf89bc1b0ac8575278a"></a><br/></td></tr>
<tr class="separator:ace6786234994faf89bc1b0ac8575278a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aebbcd4a194e4fdca0bcd16143fb03a75"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#aebbcd4a194e4fdca0bcd16143fb03a75">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)=0</td></tr>
<tr class="memdesc:aebbcd4a194e4fdca0bcd16143fb03a75"><td class="mdescLeft"> </td><td 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_245.png"/>
</p>
<a href="#aebbcd4a194e4fdca0bcd16143fb03a75"></a><br/></td></tr>
<tr class="separator:aebbcd4a194e4fdca0bcd16143fb03a75"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a86416b3ccec1ddf1ce534b53d6af1ec9"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a86416b3ccec1ddf1ce534b53d6af1ec9">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)=0</td></tr>
<tr class="memdesc:a86416b3ccec1ddf1ce534b53d6af1ec9"><td class="mdescLeft"> </td><td 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_246.png"/>
</p>
<a href="#a86416b3ccec1ddf1ce534b53d6af1ec9"></a><br/></td></tr>
<tr class="separator:a86416b3ccec1ddf1ce534b53d6af1ec9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a3f3592ac74d0aa0caa3b9224ea7e61f4"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a3f3592ac74d0aa0caa3b9224ea7e61f4">andElim</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e, int i)=0</td></tr>
<tr class="memdesc:a3f3592ac74d0aa0caa3b9224ea7e61f4"><td class="mdescLeft"> </td><td class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\vdash e_1\wedge\cdots\wedge e_n}{\vdash e_i}\]" src="form_247.png"/>
</p>
<a href="#a3f3592ac74d0aa0caa3b9224ea7e61f4"></a><br/></td></tr>
<tr class="separator:a3f3592ac74d0aa0caa3b9224ea7e61f4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a4aa193bfeb969c96b63db39a70470015"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a4aa193bfeb969c96b63db39a70470015">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)=0</td></tr>
<tr class="memdesc:a4aa193bfeb969c96b63db39a70470015"><td class="mdescLeft"> </td><td class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma_1\vdash e_1\quad \Gamma_2\vdash e_2} {\Gamma_1\cup\Gamma_2\vdash e_1\wedge e_2} \]" src="form_248.png"/>
</p>
<a href="#a4aa193bfeb969c96b63db39a70470015"></a><br/></td></tr>
<tr class="separator:a4aa193bfeb969c96b63db39a70470015"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a8fadf7698616e688d0db569b7db6e5fe"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a8fadf7698616e688d0db569b7db6e5fe">andIntro</a> (const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &es)=0</td></tr>
<tr class="memdesc:a8fadf7698616e688d0db569b7db6e5fe"><td class="mdescLeft"> </td><td 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_249.png"/>
</p>
<a href="#a8fadf7698616e688d0db569b7db6e5fe"></a><br/></td></tr>
<tr class="separator:a8fadf7698616e688d0db569b7db6e5fe"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a9292e13acd4b5ba2b215864022a22573"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a9292e13acd4b5ba2b215864022a22573">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)=0</td></tr>
<tr class="memdesc:a9292e13acd4b5ba2b215864022a22573"><td class="mdescLeft"> </td><td 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_250.png"/>
</p>
<p>. <a href="#a9292e13acd4b5ba2b215864022a22573"></a><br/></td></tr>
<tr class="separator:a9292e13acd4b5ba2b215864022a22573"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a69da48e244e1674f6b501ac4ef168feb"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a69da48e244e1674f6b501ac4ef168feb">implContrapositive</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)=0</td></tr>
<tr class="memdesc:a69da48e244e1674f6b501ac4ef168feb"><td class="mdescLeft"> </td><td class="mdescRight">e1 => e2 ==> ~e2 => ~e1 <a href="#a69da48e244e1674f6b501ac4ef168feb"></a><br/></td></tr>
<tr class="separator:a69da48e244e1674f6b501ac4ef168feb"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0e770e47e947275a69b4c9f225f8beb6"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a0e770e47e947275a69b4c9f225f8beb6">rewriteIteTrue</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a0e770e47e947275a69b4c9f225f8beb6"><td class="mdescLeft"> </td><td class="mdescRight">==> ITE(TRUE, e1, e2) == e1 <a href="#a0e770e47e947275a69b4c9f225f8beb6"></a><br/></td></tr>
<tr class="separator:a0e770e47e947275a69b4c9f225f8beb6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a95af3ce5ccd4212b15bac9b249004c48"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a95af3ce5ccd4212b15bac9b249004c48">rewriteIteFalse</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a95af3ce5ccd4212b15bac9b249004c48"><td class="mdescLeft"> </td><td class="mdescRight">==> ITE(FALSE, e1, e2) == e2 <a href="#a95af3ce5ccd4212b15bac9b249004c48"></a><br/></td></tr>
<tr class="separator:a95af3ce5ccd4212b15bac9b249004c48"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6cb02a9489ef5ed4e548f49bbd07439f"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a6cb02a9489ef5ed4e548f49bbd07439f">rewriteIteSame</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a6cb02a9489ef5ed4e548f49bbd07439f"><td class="mdescLeft"> </td><td class="mdescRight">==> ITE(c, e, e) == e <a href="#a6cb02a9489ef5ed4e548f49bbd07439f"></a><br/></td></tr>
<tr class="separator:a6cb02a9489ef5ed4e548f49bbd07439f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a34064eea86afa953b9229537b075a420"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a34064eea86afa953b9229537b075a420">notToIff</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &not_e)=0</td></tr>
<tr class="memdesc:a34064eea86afa953b9229537b075a420"><td class="mdescLeft"> </td><td class="mdescRight"><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\vdash\neg e}{\vdash e\Leftrightarrow\mathrm{FALSE}}\]" src="form_252.png"/>
</p>
<a href="#a34064eea86afa953b9229537b075a420"></a><br/></td></tr>
<tr class="separator:a34064eea86afa953b9229537b075a420"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae25f68b7cceeeb25b41b1d2bcb1df8f3"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#ae25f68b7cceeeb25b41b1d2bcb1df8f3">xorToIff</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:ae25f68b7cceeeb25b41b1d2bcb1df8f3"><td class="mdescLeft"> </td><td 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_253.png"/>
</p>
<a href="#ae25f68b7cceeeb25b41b1d2bcb1df8f3"></a><br/></td></tr>
<tr class="separator:ae25f68b7cceeeb25b41b1d2bcb1df8f3"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5c50bf251b95dfc47ccfc6e8b51426c1"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a5c50bf251b95dfc47ccfc6e8b51426c1">rewriteIff</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a5c50bf251b95dfc47ccfc6e8b51426c1"><td class="mdescLeft"> </td><td class="mdescRight">==> (e1 <=> e2) <=> [simplified expr] <a href="#a5c50bf251b95dfc47ccfc6e8b51426c1"></a><br/></td></tr>
<tr class="separator:a5c50bf251b95dfc47ccfc6e8b51426c1"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:afb2ae30738c04b088459281d259a6d3a"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#afb2ae30738c04b088459281d259a6d3a">rewriteAnd</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:afb2ae30738c04b088459281d259a6d3a"><td class="mdescLeft"> </td><td class="mdescRight">==> AND(e1,e2) IFF [simplified expr] <a href="#afb2ae30738c04b088459281d259a6d3a"></a><br/></td></tr>
<tr class="separator:afb2ae30738c04b088459281d259a6d3a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa3cfb7d47a6d6bc84c85c7fa6a3e1242"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#aa3cfb7d47a6d6bc84c85c7fa6a3e1242">rewriteOr</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:aa3cfb7d47a6d6bc84c85c7fa6a3e1242"><td class="mdescLeft"> </td><td class="mdescRight">==> OR(e1,...,en) IFF [simplified expr] <a href="#aa3cfb7d47a6d6bc84c85c7fa6a3e1242"></a><br/></td></tr>
<tr class="separator:aa3cfb7d47a6d6bc84c85c7fa6a3e1242"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad55b11590196fbd73d24daa1d0d6eeb1"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#ad55b11590196fbd73d24daa1d0d6eeb1">rewriteNotTrue</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:ad55b11590196fbd73d24daa1d0d6eeb1"><td class="mdescLeft"> </td><td class="mdescRight">==> NOT TRUE IFF FALSE <a href="#ad55b11590196fbd73d24daa1d0d6eeb1"></a><br/></td></tr>
<tr class="separator:ad55b11590196fbd73d24daa1d0d6eeb1"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a30fa79637f4308e8e733015624293775"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a30fa79637f4308e8e733015624293775">rewriteNotFalse</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a30fa79637f4308e8e733015624293775"><td class="mdescLeft"> </td><td class="mdescRight">==> NOT FALSE IFF TRUE <a href="#a30fa79637f4308e8e733015624293775"></a><br/></td></tr>
<tr class="separator:a30fa79637f4308e8e733015624293775"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a8a04ff29591a019d4d4cf073c0987316"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a8a04ff29591a019d4d4cf073c0987316">rewriteNotNot</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a8a04ff29591a019d4d4cf073c0987316"><td class="mdescLeft"> </td><td class="mdescRight">==> NOT NOT e IFF e, takes !!e <a href="#a8a04ff29591a019d4d4cf073c0987316"></a><br/></td></tr>
<tr class="separator:a8a04ff29591a019d4d4cf073c0987316"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad14f0ceb0d486ba3d78c2c3c6e47382a"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#ad14f0ceb0d486ba3d78c2c3c6e47382a">rewriteNotForall</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &forallExpr)=0</td></tr>
<tr class="memdesc:ad14f0ceb0d486ba3d78c2c3c6e47382a"><td class="mdescLeft"> </td><td class="mdescRight">==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e <a href="#ad14f0ceb0d486ba3d78c2c3c6e47382a"></a><br/></td></tr>
<tr class="separator:ad14f0ceb0d486ba3d78c2c3c6e47382a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a12d8ca9f5547fb3a3239d7dc6f53987c"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a12d8ca9f5547fb3a3239d7dc6f53987c">rewriteNotExists</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &existsExpr)=0</td></tr>
<tr class="memdesc:a12d8ca9f5547fb3a3239d7dc6f53987c"><td class="mdescLeft"> </td><td class="mdescRight">==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e <a href="#a12d8ca9f5547fb3a3239d7dc6f53987c"></a><br/></td></tr>
<tr class="separator:a12d8ca9f5547fb3a3239d7dc6f53987c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a015539886185195ba5d98c60cd7e8f66"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a015539886185195ba5d98c60cd7e8f66">skolemize</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:a015539886185195ba5d98c60cd7e8f66"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a8a2561e9e4763460c65dbebe10d2f281"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a8a2561e9e4763460c65dbebe10d2f281">skolemizeRewrite</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:a8a2561e9e4763460c65dbebe10d2f281"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a4013a795d82cebb8b60ed67c094a7cba"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a4013a795d82cebb8b60ed67c094a7cba">skolemizeRewriteVar</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a4013a795d82cebb8b60ed67c094a7cba"><td class="mdescLeft"> </td><td class="mdescRight">Special version of skolemizeRewrite for "EXISTS x. t = x". <a href="#a4013a795d82cebb8b60ed67c094a7cba"></a><br/></td></tr>
<tr class="separator:a4013a795d82cebb8b60ed67c094a7cba"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aab746efc9d013643bccc065affa82992"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#aab746efc9d013643bccc065affa82992">varIntroRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:aab746efc9d013643bccc065affa82992"><td class="mdescLeft"> </td><td class="mdescRight">|- EXISTS x. e = x <a href="#aab746efc9d013643bccc065affa82992"></a><br/></td></tr>
<tr class="separator:aab746efc9d013643bccc065affa82992"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aed771f6a74d1a336cc08bfcfaf8169da"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#aed771f6a74d1a336cc08bfcfaf8169da">skolemize</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)=0</td></tr>
<tr class="memdesc:aed771f6a74d1a336cc08bfcfaf8169da"><td class="mdescLeft"> </td><td 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="#aed771f6a74d1a336cc08bfcfaf8169da"></a><br/></td></tr>
<tr class="separator:aed771f6a74d1a336cc08bfcfaf8169da"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a10fa187373ec24079c10874d8e804ecb"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a10fa187373ec24079c10874d8e804ecb">varIntroSkolem</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a10fa187373ec24079c10874d8e804ecb"><td class="mdescLeft"> </td><td class="mdescRight">Retrun a theorem "|- e = v" for a new Skolem constant v. <a href="#a10fa187373ec24079c10874d8e804ecb"></a><br/></td></tr>
<tr class="separator:a10fa187373ec24079c10874d8e804ecb"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6e93694c76f7b567487bc8cae674ae5d"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a6e93694c76f7b567487bc8cae674ae5d">trueTheorem</a> ()=0</td></tr>
<tr class="memdesc:a6e93694c76f7b567487bc8cae674ae5d"><td class="mdescLeft"> </td><td class="mdescRight">==> TRUE <a href="#a6e93694c76f7b567487bc8cae674ae5d"></a><br/></td></tr>
<tr class="separator:a6e93694c76f7b567487bc8cae674ae5d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a1d546d9530a3c15cd627a141137a8616"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a1d546d9530a3c15cd627a141137a8616">rewriteAnd</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e)=0</td></tr>
<tr class="memdesc:a1d546d9530a3c15cd627a141137a8616"><td class="mdescLeft"> </td><td class="mdescRight">AND(e1,e2) ==> [simplified expr]. <a href="#a1d546d9530a3c15cd627a141137a8616"></a><br/></td></tr>
<tr class="separator:a1d546d9530a3c15cd627a141137a8616"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a44474beaa5761147eb816db48c795c4b"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a44474beaa5761147eb816db48c795c4b">rewriteOr</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e)=0</td></tr>
<tr class="memdesc:a44474beaa5761147eb816db48c795c4b"><td class="mdescLeft"> </td><td class="mdescRight">OR(e1,...,en) ==> [simplified expr]. <a href="#a44474beaa5761147eb816db48c795c4b"></a><br/></td></tr>
<tr class="separator:a44474beaa5761147eb816db48c795c4b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac773341edabcc5091ca25af74fcb7653"><td class="memItemLeft" align="right" valign="top">virtual std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#ac773341edabcc5091ca25af74fcb7653">getSkolemAxioms</a> ()=0</td></tr>
<tr class="separator:ac773341edabcc5091ca25af74fcb7653"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6f8068606f30fe7b2c405ddf5ce1a53b"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a6f8068606f30fe7b2c405ddf5ce1a53b">clearSkolemAxioms</a> ()=0</td></tr>
<tr class="separator:a6f8068606f30fe7b2c405ddf5ce1a53b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a484540b067da205d23b2fe263662cda2"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a484540b067da205d23b2fe263662cda2">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)=0</td></tr>
<tr class="separator:a484540b067da205d23b2fe263662cda2"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a893a258d9f7d49acb5c8a8b5b8ec39b0"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1CommonProofRules.html#a893a258d9f7d49acb5c8a8b5b8ec39b0">liftOneITE</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:a893a258d9f7d49acb5c8a8b5b8ec39b0"><td class="memSeparator" colspan="2"> </td></tr>
</table>
<a name="details" id="details"></a><h2 class="groupheader">Detailed Description</h2>
<div class="textblock">
<p>Definition at line <a class="el" href="common__proof__rules_8h_source.html#l00046">46</a> of file <a class="el" href="common__proof__rules_8h_source.html">common_proof_rules.h</a>.</p>
</div><h2 class="groupheader">Constructor & Destructor Documentation</h2>
<a class="anchor" id="a334ad50333e9323968df2bc286de7a8f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual CVC3::CommonProofRules::~CommonProofRules </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Destructor. </p>
<p>Definition at line <a class="el" href="common__proof__rules_8h_source.html#l00049">49</a> of file <a class="el" href="common__proof__rules_8h_source.html">common_proof_rules.h</a>.</p>
</div>
</div>
<h2 class="groupheader">Member Function Documentation</h2>
<a class="anchor" id="a758fe978ff00099419c459914a0af5ba"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem3.html">Theorem3</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </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_224.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_225.png"/>
</p>
<p>. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a685c913a4b6b80a546dcb9853a88e21a">CVC3::CommonTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="afe561cfd6d5ee752fbc1c3cafe9b68a5"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem3.html">Theorem3</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </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_226.png"/>
</p>
</p>
<dl class="params"><dt>Parameters</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_227.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_228.png"/> </td></tr>
</table>
</dd>
</dl>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#abf904962af8344d8646c382747837af4">CVC3::CommonTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ab4527c48e9f88d94d7ca076757a6f3ba"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{}{a\vdash a}\]" src="form_229.png"/>
</p>
</p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a28d225c0e86bf45df3441c14a11197be">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00170">CVC3::SearchImplBase::newIntAssumption()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00334">CVC3::ExprTransform::newPPrec()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00141">CVC3::SearchImplBase::newUserAssumption()</a>, <a class="el" href="search__sat_8cpp_source.html#l01064">CVC3::SearchSat::newUserAssumptionInt()</a>, and <a class="el" href="theory__quant_8cpp_source.html#l01731">CVC3::CompleteInstPreProcessor::simplifyQuant()</a>.</p>
</div>
</div>
<a class="anchor" id="a61c1fe56b4ed9744006883a7784ddb71"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </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_230.png"/>
</p>
</p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a306058f7ced3d7220b2d1a40892faae7">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="cnf__manager_8cpp_source.html#l00139">SAT::CNF_Manager::concreteThm()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00282">CVC3::ExprTransform::newPP()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00334">CVC3::ExprTransform::newPPrec()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00079">CVC3::ExprTransform::preprocess()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00127">CVC3::ExprTransform::pushNegation()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00239">CVC3::ExprTransform::pushNegation1()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00141">CVC3::ExprTransform::pushNegationRec()</a>, <a class="el" href="theory_8h_source.html#l00673">CVC3::Theory::reflexivityRule()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00804">CVC3::SearchImplBase::replaceITE()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00074">SAT::CNF_Manager::replaceITErec()</a>, <a class="el" href="theory__core_8cpp_source.html#l00968">CVC3::TheoryCore::rewrite()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00476">CVC3::ExprTransform::simplifyWithCare()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00296">CVC3::ExprTransform::specialSimplify()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00434">CVC3::ExprTransform::substitute()</a>, and <a class="el" href="cnf__manager_8cpp_source.html#l00147">SAT::CNF_Manager::translateExprRec()</a>.</p>
</div>
</div>
<a class="anchor" id="ad078b5d25129b200fe04b20c5962aa34"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>==> (a == a) IFF TRUE </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a26b00cb395f45971ace24a4529189e1b">CVC3::CommonTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a0a87e88508f49b73037e0024afa841bf"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </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_231.png"/>
</p>
<p> (same for IFF) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#ab269d27c05584ade0b1f86f2ced0c46a">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00563">CVC3::SearchImplBase::applyCNFRules()</a>, <a class="el" href="search__simple_8cpp_source.html#l00126">CVC3::SearchSimple::checkValidMain()</a>, <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00371">CVC3::SearchImplBase::enqueueCNFrec()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00074">SAT::CNF_Manager::replaceITErec()</a>, and <a class="el" href="theory_8h_source.html#l00677">CVC3::Theory::symmetryRule()</a>.</p>
</div>
</div>
<a class="anchor" id="a338cafc978d9b6a447e8d58af42d7e5b"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </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_232.png"/>
</p>
</p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#ac0813c68583ad6f0661d4c1affe3c6d8">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="theory__array_8cpp_source.html#l00368">CVC3::TheoryArray::rewrite()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02387">CVC3::TheoryArith3::rewrite()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03076">CVC3::TheoryArithOld::rewrite()</a>, and <a class="el" href="theory__core_8cpp_source.html#l01141">CVC3::TheoryCore::update()</a>.</p>
</div>
</div>
<a class="anchor" id="a4a4e90cd69ce24e83ba2c217907c277a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </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_233.png"/>
</p>
<p> (same for IFF) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#ad5c0bc0fb82634039e5f2c8f9291de0e">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00563">CVC3::SearchImplBase::applyCNFRules()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00371">CVC3::SearchImplBase::enqueueCNFrec()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00750">CVC3::SearchImplBase::findInCNFCache()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00334">CVC3::ExprTransform::newPPrec()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00079">CVC3::ExprTransform::preprocess()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00239">CVC3::ExprTransform::pushNegation1()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00225">CVC3::ExprTransform::pushNegationRec()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00804">CVC3::SearchImplBase::replaceITE()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00476">CVC3::ExprTransform::simplifyWithCare()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00434">CVC3::ExprTransform::substitute()</a>, and <a class="el" href="theory_8h_source.html#l00681">CVC3::Theory::transitivityRule()</a>.</p>
</div>
</div>
<a class="anchor" id="a776c827bb6e3b889234429c49ae9ad6f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Optimized case for expr with one child. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#aac39a4ae729b4218d4b70ed6a68bc53d">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00563">CVC3::SearchImplBase::applyCNFRules()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02020">CVC3::TheoryArith3::assertFact()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00371">CVC3::SearchImplBase::enqueueCNFrec()</a>, <a class="el" href="theory_8cpp_source.html#l00327">CVC3::Theory::findReduce()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00334">CVC3::ExprTransform::newPPrec()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00239">CVC3::ExprTransform::pushNegation1()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00141">CVC3::ExprTransform::pushNegationRec()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00074">SAT::CNF_Manager::replaceITErec()</a>, <a class="el" href="theory_8cpp_source.html#l00053">CVC3::Theory::simplifyOp()</a>, <a class="el" href="theory__core_8cpp_source.html#l01292">CVC3::TheoryCore::simplifyOp()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00296">CVC3::ExprTransform::specialSimplify()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00434">CVC3::ExprTransform::substitute()</a>, <a class="el" href="theory_8h_source.html#l00686">CVC3::Theory::substitutivityRule()</a>, <a class="el" href="theory__core_8cpp_source.html#l01141">CVC3::TheoryCore::update()</a>, and <a class="el" href="theory_8cpp_source.html#l00417">CVC3::Theory::updateHelper()</a>.</p>
</div>
</div>
<a class="anchor" id="abd65b6e03c3c57174b94a955d12cf266"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Optimized case for expr with two children. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a78ce0fe500f548d464b63e19211836f8">CVC3::CommonTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="aa1d9df2568ac3efade63925834c752e6"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </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_234.png"/>
</p>
</p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a3cbe9d25e0363d61a29179592561ddb9">CVC3::CommonTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a23a0251820f022d14376c6e825291fa2"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </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_234.png"/>
</p>
<p> except that only those arguments are given that <img class="formulaInl" alt="$c_i\not=d_i$" src="form_235.png"/>. </p>
<dl class="params"><dt>Parameters</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_236.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_237.png"/> for the changed kids. </td></tr>
</table>
</dd>
</dl>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a395cee7c667e641b2835748d0a8c4a9d">CVC3::CommonTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a5f4e51842d28b0ef5def4eecb65ae99c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#afeddaca97606b242861d6e05a97f62d7">CVC3::CommonTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a1074822d52c22daacaa78b34ac0635ba"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </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_238.png"/>
</p>
</p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#aaa58b8a459f5678aa2393fba6b50ff8d">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01530">CVC3::SearchEngineFast::addLiteralFact()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00549">CVC3::SearchEngineFast::recordFact()</a>.</p>
</div>
</div>
<a class="anchor" id="aec56ab0fbac82267ff202ae328fe801f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#ad6ecd5f3d95b2f44d670ad1228a88f4a">CVC3::CommonTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ae5a0a67c59ba15d84e900fdccc7653ca"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </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_239.png"/>
</p>
</p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a37ed2850e80cd789f7ac712df6eacc63">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="theory__arith3_8cpp_source.html#l02387">CVC3::TheoryArith3::rewrite()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03076">CVC3::TheoryArithOld::rewrite()</a>, and <a class="el" href="theory__core_8cpp_source.html#l01292">CVC3::TheoryCore::simplifyOp()</a>.</p>
</div>
</div>
<a class="anchor" id="a5a56b6f9544841fe86255e5bc35e8449"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </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_240.png"/>
</p>
</p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a2b95f985a56f8d25b00145846406d70b">CVC3::CommonTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ad2edb920405666bf6e9d21ae496ff6b3"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </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_241.png"/>
</p>
</p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a40da8d343ef923020c472eaace6e8122">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="theory__core_8cpp_source.html#l03541">CVC3::TheoryCore::registerAtom()</a>, <a class="el" href="search__fast_8cpp_source.html#l00254">CVC3::SearchEngineFast::split()</a>, <a class="el" href="theory__uf_8cpp_source.html#l00257">CVC3::TheoryUF::update()</a>, and <a class="el" href="theory__core_8cpp_source.html#l01141">CVC3::TheoryCore::update()</a>.</p>
</div>
</div>
<a class="anchor" id="a11b56754024b56844336954cf789a63a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </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_242.png"/>
</p>
</p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a4efade3a917467bf7287a19d2ee4ea2c">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="theory__core_8cpp_source.html#l03541">CVC3::TheoryCore::registerAtom()</a>, <a class="el" href="search__fast_8cpp_source.html#l00254">CVC3::SearchEngineFast::split()</a>, and <a class="el" href="theory__core_8cpp_source.html#l01141">CVC3::TheoryCore::update()</a>.</p>
</div>
</div>
<a class="anchor" id="af38f25446a561384c3de66392c4d3544"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </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_243.png"/>
</p>
<p> Where ~e is the <em>inverse</em> of e (that is, ~(!e') = e'). </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a3733173dbd8f639af979150059c4ec90">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00723">CVC3::SearchImplBase::addToCNFCache()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00563">CVC3::SearchImplBase::applyCNFRules()</a>, <a class="el" href="search__simple_8cpp_source.html#l00126">CVC3::SearchSimple::checkValidMain()</a>, <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00750">CVC3::SearchImplBase::findInCNFCache()</a>, and <a class="el" href="theory__core_8cpp_source.html#l04029">CVC3::TheoryCore::rewriteLiteral()</a>.</p>
</div>
</div>
<a class="anchor" id="ace6786234994faf89bc1b0ac8575278a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </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_244.png"/>
</p>
</p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a59470692918d2f7c03c073a61daa3db5">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00371">CVC3::SearchImplBase::enqueueCNFrec()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00254">CVC3::SearchEngineFast::split()</a>.</p>
</div>
</div>
<a class="anchor" id="aebbcd4a194e4fdca0bcd16143fb03a75"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </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_245.png"/>
</p>
</p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a98f862538ac375b133079c336c539b22">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="search__simple_8cpp_source.html#l00126">CVC3::SearchSimple::checkValidMain()</a>, <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00371">CVC3::SearchImplBase::enqueueCNFrec()</a>, <a class="el" href="search__fast_8cpp_source.html#l00939">CVC3::SearchEngineFast::fixConflict()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l03273">CVC3::TheoryArithNew::getVariableIntroThm()</a>, <a class="el" href="theory_8h_source.html#l00714">CVC3::Theory::iffMP()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00120">CVC3::ExprTransform::preprocess()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00804">CVC3::SearchImplBase::replaceITE()</a>, and <a class="el" href="cnf__manager_8cpp_source.html#l00074">SAT::CNF_Manager::replaceITErec()</a>.</p>
</div>
</div>
<a class="anchor" id="a86416b3ccec1ddf1ce534b53d6af1ec9"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </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_246.png"/>
</p>
</p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#ac7155849ce6bd4afe185fdb0e397fc58">CVC3::CommonTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a3f3592ac74d0aa0caa3b9224ea7e61f4"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </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_247.png"/>
</p>
</p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a23e3f96d1cc6da39d97f9b7a2e0ba723">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01445">CVC3::SearchEngineFast::addNonLiteralFact()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00563">CVC3::SearchImplBase::applyCNFRules()</a>, <a class="el" href="theory__core_8cpp_source.html#l04093">CVC3::TheoryCore::assertEqualities()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02643">CVC3::TheoryArith3::checkAssertEqInvariant()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03621">CVC3::TheoryArithOld::checkAssertEqInvariant()</a>, <a class="el" href="theory__core_8cpp_source.html#l01220">CVC3::TheoryCore::checkSolved()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00371">CVC3::SearchImplBase::enqueueCNFrec()</a>, <a class="el" href="search__sat_8cpp_source.html#l01042">CVC3::SearchSat::newUserAssumptionIntHelper()</a>, and <a class="el" href="theory__bitvector_8cpp_source.html#l02818">CVC3::TheoryBitvector::solve()</a>.</p>
</div>
</div>
<a class="anchor" id="a4aa193bfeb969c96b63db39a70470015"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </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_2} {\Gamma_1\cup\Gamma_2\vdash e_1\wedge e_2} \]" src="form_248.png"/>
</p>
</p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a733e7c5fe7b46d1af284c7c30c94025a">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="search__simple_8cpp_source.html#l00237">CVC3::SearchSimple::addNonLiteralFact()</a>.</p>
</div>
</div>
<a class="anchor" id="a8fadf7698616e688d0db569b7db6e5fe"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </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_249.png"/>
</p>
</p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a27ccedb2c4fb06b63f4019effb22feff">CVC3::CommonTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a9292e13acd4b5ba2b215864022a22573"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </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_250.png"/>
</p>
<p>. </p>
<dl class="params"><dt>Parameters</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_227.png"/> </td></tr>
</table>
</dd>
</dl>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a414b98f6715044635975f8675f770c0b">CVC3::CommonTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a69da48e244e1674f6b501ac4ef168feb"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </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_251.png"/>
</p>
<p> Where ~e is the <em>inverse</em> of e (that is, ~(!e') = e'). </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a38bb194aa15b10dd0959cfff5e33014b">CVC3::CommonTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a0e770e47e947275a69b4c9f225f8beb6"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>==> ITE(TRUE, e1, e2) == e1 </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a2459a321ea5cdab974dc2cf029934a71">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="theory_8cpp_source.html#l00923">CVC3::Theory::rewriteIte()</a>.</p>
</div>
</div>
<a class="anchor" id="a95af3ce5ccd4212b15bac9b249004c48"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>==> ITE(FALSE, e1, e2) == e2 </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a1711198c758a0475449b1889815f1371">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="theory_8cpp_source.html#l00923">CVC3::Theory::rewriteIte()</a>.</p>
</div>
</div>
<a class="anchor" id="a6cb02a9489ef5ed4e548f49bbd07439f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>==> ITE(c, e, e) == e </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#aad60929c1c8c79287a16bc995cd9c51c">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="theory_8cpp_source.html#l00923">CVC3::Theory::rewriteIte()</a>, and <a class="el" href="theory__core_8cpp_source.html#l01292">CVC3::TheoryCore::simplifyOp()</a>.</p>
</div>
</div>
<a class="anchor" id="a34064eea86afa953b9229537b075a420"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </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_252.png"/>
</p>
</p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#ab9c0b6784e83fc0a4727a58c0a82b67a">CVC3::CommonTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ae25f68b7cceeeb25b41b1d2bcb1df8f3"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </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_253.png"/>
</p>
</p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a5b3a8e2d8bb3469935ecd1476778acaa">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="theory__core_8cpp_source.html#l00968">CVC3::TheoryCore::rewrite()</a>.</p>
</div>
</div>
<a class="anchor" id="a5c50bf251b95dfc47ccfc6e8b51426c1"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </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>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#ab2233ef28defaf0af1b6a8cc4b887708">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="theory__core_8cpp_source.html#l00968">CVC3::TheoryCore::rewrite()</a>.</p>
</div>
</div>
<a class="anchor" id="afb2ae30738c04b088459281d259a6d3a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>==> AND(e1,e2) IFF [simplified expr] </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#ad74cb42b63d2f92b55c79281e84816c1">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="theory_8cpp_source.html#l00081">CVC3::Theory::computeTCC()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l05570">CVC3::TheoryBitvector::computeTCC()</a>, and <a class="el" href="theory_8h_source.html#l00719">CVC3::Theory::rewriteAnd()</a>.</p>
</div>
</div>
<a class="anchor" id="aa3cfb7d47a6d6bc84c85c7fa6a3e1242"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>==> OR(e1,...,en) IFF [simplified expr] </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#aa0d6b0fbe3838ae22b4a90d92d1530e2">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00939">CVC3::SearchEngineFast::fixConflict()</a>, and <a class="el" href="theory_8h_source.html#l00724">CVC3::Theory::rewriteOr()</a>.</p>
</div>
</div>
<a class="anchor" id="ad55b11590196fbd73d24daa1d0d6eeb1"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>==> NOT TRUE IFF FALSE </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a49ce394a818d2ab83b2f97d44cd66f1b">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="expr__transform_8cpp_source.html#l00239">CVC3::ExprTransform::pushNegation1()</a>, and <a class="el" href="expr__transform_8cpp_source.html#l00141">CVC3::ExprTransform::pushNegationRec()</a>.</p>
</div>
</div>
<a class="anchor" id="a30fa79637f4308e8e733015624293775"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>==> NOT FALSE IFF TRUE </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#aace9193e3ff294ef6065178a55610e88">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="expr__transform_8cpp_source.html#l00239">CVC3::ExprTransform::pushNegation1()</a>, and <a class="el" href="expr__transform_8cpp_source.html#l00141">CVC3::ExprTransform::pushNegationRec()</a>.</p>
</div>
</div>
<a class="anchor" id="a8a04ff29591a019d4d4cf073c0987316"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>==> NOT NOT e IFF e, takes !!e </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a84b83e300ddf9e67e427b2815ecff1e7">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00750">CVC3::SearchImplBase::findInCNFCache()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00239">CVC3::ExprTransform::pushNegation1()</a>, and <a class="el" href="expr__transform_8cpp_source.html#l00141">CVC3::ExprTransform::pushNegationRec()</a>.</p>
</div>
</div>
<a class="anchor" id="ad14f0ceb0d486ba3d78c2c3c6e47382a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a6241bfc091691a667ed41a9d36d4cab6">CVC3::CommonTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a12d8ca9f5547fb3a3239d7dc6f53987c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a2535d1565f3f7b830063ad9ae3e1c4e7">CVC3::CommonTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a015539886185195ba5d98c60cd7e8f66"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Expr.html">Expr</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#adcd56f1052668c269d59b5001a01191f">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00637">CVC3::SearchEngineFast::bcp()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01972">CVC3::CompleteInstPreProcessor::collectIndex()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01373">CVC3::CompleteInstPreProcessor::isMacro()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01693">CVC3::CompleteInstPreProcessor::recSkolemize()</a>, and <a class="el" href="theory__bitvector_8cpp_source.html#l02818">CVC3::TheoryBitvector::solve()</a>.</p>
</div>
</div>
<a class="anchor" id="a8a2561e9e4763460c65dbebe10d2f281"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </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>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a3bfb1ce883967f3822858b73156f99e9">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__new_8cpp_source.html#l03273">CVC3::TheoryArithNew::getVariableIntroThm()</a>.</p>
</div>
</div>
<a class="anchor" id="a4013a795d82cebb8b60ed67c094a7cba"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Special version of skolemizeRewrite for "EXISTS x. t = x". </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a5b97504309d324b509e18976b93a3c78">CVC3::CommonTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="aab746efc9d013643bccc065affa82992"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>|- EXISTS x. e = x </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#ac003e84b85d4f51746628fd0f738b7e3">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__new_8cpp_source.html#l03273">CVC3::TheoryArithNew::getVariableIntroThm()</a>.</p>
</div>
</div>
<a class="anchor" id="aed771f6a74d1a336cc08bfcfaf8169da"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </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 class="params"><dt>Parameters</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>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a9c3d8d07344147c33394ab68ca490c04">CVC3::CommonTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a10fa187373ec24079c10874d8e804ecb"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </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>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a84f7da63e9d820ad781efa7e963733aa">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00563">CVC3::SearchImplBase::applyCNFRules()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00371">CVC3::SearchImplBase::enqueueCNFrec()</a>, <a class="el" href="theory_8cpp_source.html#l00935">CVC3::Theory::renameExpr()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00804">CVC3::SearchImplBase::replaceITE()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00074">SAT::CNF_Manager::replaceITErec()</a>, and <a class="el" href="theory__arith__old_8cpp_source.html#l02227">CVC3::TheoryArithOld::TheoryArithOld()</a>.</p>
</div>
</div>
<a class="anchor" id="a6e93694c76f7b567487bc8cae674ae5d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::trueTheorem </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>==> TRUE </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a38a1b30499d07384066e9afca89f37c0">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="search__simple_8cpp_source.html#l00101">CVC3::SearchSimple::SearchSimple()</a>.</p>
</div>
</div>
<a class="anchor" id="a1d546d9530a3c15cd627a141137a8616"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>AND(e1,e2) ==> [simplified expr]. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a1f2d422ab4dd1297fbf6c4295a430f32">CVC3::CommonTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a44474beaa5761147eb816db48c795c4b"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>OR(e1,...,en) ==> [simplified expr]. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a9f135d57462754cd9903190d4fe4aec8">CVC3::CommonTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ac773341edabcc5091ca25af74fcb7653"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual std::vector<<a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>>& CVC3::CommonProofRules::getSkolemAxioms </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a8c83d415f39a7ac2f6a117972116c6b2">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00317">CVC3::SearchImplBase::processResult()</a>.</p>
</div>
</div>
<a class="anchor" id="a6f8068606f30fe7b2c405ddf5ce1a53b"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual void CVC3::CommonProofRules::clearSkolemAxioms </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#ad7dc685e6e46a90802f2602a70b9674a">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00344">CVC3::SearchImplBase::checkValid()</a>.</p>
</div>
</div>
<a class="anchor" id="a484540b067da205d23b2fe263662cda2"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a752f5927047540cc10f67d3d5ed179a7">CVC3::CommonTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a893a258d9f7d49acb5c8a8b5b8ec39b0"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CommonProofRules::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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a749d1c718f05307dad5dcc3f6d2296a2">CVC3::CommonTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="expr__transform_8cpp_source.html#l00334">CVC3::ExprTransform::newPPrec()</a>, and <a class="el" href="expr__transform_8cpp_source.html#l00476">CVC3::ExprTransform::simplifyWithCare()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following file:<ul>
<li><a class="el" href="common__proof__rules_8h_source.html">common_proof_rules.h</a></li>
</ul>
</div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:17 for CVC3 by  <a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/>
</a> 1.8.2
</small></address>
</body>
</html>
