<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<title>CVC3: CVC3::CoreTheoremProducer Class Reference</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li class="current"><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="annotated.html"><span>Class List</span></a></li>
<li><a href="classes.html"><span>Class Index</span></a></li>
<li><a href="hierarchy.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="namespaceCVC3.html">CVC3</a> </li>
<li class="navelem"><a class="el" href="classCVC3_1_1CoreTheoremProducer.html">CoreTheoremProducer</a> </li>
</ul>
</div>
</div>
<div class="header">
<div class="summary">
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pri-attribs">Private Attributes</a> </div>
<div class="headertitle">
<div class="title">CVC3::CoreTheoremProducer Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="CVC3::CoreTheoremProducer" --><!-- doxytag: inherits="CVC3::CoreProofRules,CVC3::TheoremProducer" -->
<p><code>#include <<a class="el" href="core__theorem__producer_8h_source.html">core_theorem_producer.h</a>></code></p>
<div class="dynheader">
Inheritance diagram for CVC3::CoreTheoremProducer:</div>
<div class="dyncontent">
<div class="center">
<img src="classCVC3_1_1CoreTheoremProducer.png" usemap="#CVC3::CoreTheoremProducer_map" alt=""/>
<map id="CVC3::CoreTheoremProducer_map" name="CVC3::CoreTheoremProducer_map">
<area href="classCVC3_1_1CoreProofRules.html" alt="CVC3::CoreProofRules" shape="rect" coords="0,0,182,24"/>
<area href="classCVC3_1_1TheoremProducer.html" alt="CVC3::TheoremProducer" shape="rect" coords="192,0,374,24"/>
</map>
</div></div>
<p><a href="classCVC3_1_1CoreTheoremProducer-members.html">List of all members.</a></p>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li><a class="el" href="classCVC3_1_1CoreTheoremProducer.html#ade8689298e574b416d296d03ed44c051">CoreTheoremProducer</a> (<a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a> *tm, <a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> *core)
<li>virtual <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a31ee45df90c9144296b9312c9b5c4a97">~CoreTheoremProducer</a> ()
<li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a0b6d312ded517ab466308ec5981d250e">typePred</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">e: T ==> |- typePred_T(e) [deriving the type predicate of e] <a href="#a0b6d312ded517ab466308ec5981d250e"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a222db72dc6f637e582dfb9b8dd4e362c">rewriteLetDecl</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Replace LETDECL with its definition. <a href="#a222db72dc6f637e582dfb9b8dd4e362c"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a66f5d185eca0ccf417b4bf5ed4448f72">rewriteNotAnd</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">==> NOT (AND e1 ... en) IFF (OR !e1 ... !en), takes (AND ...) <a href="#a66f5d185eca0ccf417b4bf5ed4448f72"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a5ce6abeb6a346d20f5d5860a30a33e28">rewriteNotOr</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">==> NOT (OR e1 ... en) IFF (AND !e1 ... !en), takes (OR ...) <a href="#a5ce6abeb6a346d20f5d5860a30a33e28"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a7da16f5874fbc0870f57a9deeeec80b8">rewriteNotIff</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">==> NOT IFF(e1,e2) IFF IFF(e1,NOT e2) <a href="#a7da16f5874fbc0870f57a9deeeec80b8"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#accd799779aa02c5d84352cc48e975b3d">rewriteNotIte</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">==> NOT ITE(a,b,c) IFF ITE(a,NOT b,NOT c) <a href="#accd799779aa02c5d84352cc48e975b3d"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a490808acd89e0732678d570599c93165">rewriteIteThen</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thenThm)
<dl class="el"><dd class="mdescRight">a |- b == d ==> ITE(a, b, c) == ITE(a, d, c) <a href="#a490808acd89e0732678d570599c93165"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#ae1092dc92aef4300caf926b48ac2ec65">rewriteIteElse</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &elseThm)
<dl class="el"><dd class="mdescRight">!a |- c == d ==> ITE(a, b, c) == ITE(a, b, d) <a href="#ae1092dc92aef4300caf926b48ac2ec65"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#ac888377c574a056b251446902c010352">rewriteIteBool</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &c, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e1, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e2)
<dl class="el"><dd class="mdescRight">==> ITE(c, e1, e2) <=> (c => e1) AND (!c => e2) <a href="#ac888377c574a056b251446902c010352"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a84abfb7cac1d339c43b322b097aa574c">orDistributivityRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">|= (A & B1) | (A & B2) | ... | (A & bn) <=> A & (B1 | B2 | ...| Bn) <a href="#a84abfb7cac1d339c43b322b097aa574c"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#af5e5fb97e5fe6197e42c2c44e1757bb3">andDistributivityRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">|= (A | B1) & (A | B2) & ... & (A | bn) <=> A | (B1 & B2 & ...& Bn) <a href="#af5e5fb97e5fe6197e42c2c44e1757bb3"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#ac88efa4d7c591f187d3212c7162ef9a5">rewriteImplies</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">==> IMPLIES(e1,e2) IFF OR(!e1, e2) <a href="#ac88efa4d7c591f187d3212c7162ef9a5"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a17536e7c7ffa8d9a34981458a20f21ff">rewriteDistinct</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">==> DISTINCT(e1,...,en) IFF AND 1 <= i < j <= n (e[i] /= e[j]) <a href="#a17536e7c7ffa8d9a34981458a20f21ff"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a287bd6f15c149c66f1aea020cd144571">NotToIte</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &not_e)
<dl class="el"><dd class="mdescRight">==> NOT(e) == ITE(e, FALSE, TRUE) <a href="#a287bd6f15c149c66f1aea020cd144571"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a23a4580e5eb68d197db655776c5e8b0a">OrToIte</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">==> Or(e) == ITE(e[1], TRUE, e[0]) <a href="#a23a4580e5eb68d197db655776c5e8b0a"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#aaa435d07458188d1380e42d51c70b419">AndToIte</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">==> And(e) == ITE(e[1], e[0], FALSE) <a href="#aaa435d07458188d1380e42d51c70b419"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#af0a98459d73dbd5b89582d803f304aac">IffToIte</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">==> IFF(a,b) == ITE(a, b, !b) <a href="#af0a98459d73dbd5b89582d803f304aac"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#aa5abdd3bfe669a3a0b28a92d28e8958a">ImpToIte</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">==> IMPLIES(a,b) == ITE(a, b, TRUE) <a href="#aa5abdd3bfe669a3a0b28a92d28e8958a"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a27d39117a5ede71d9c460b0232bdd469">rewriteIteToNot</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">==> ITE(e, FALSE, TRUE) IFF NOT(e) <a href="#a27d39117a5ede71d9c460b0232bdd469"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a2db95a382b0141d9a5098e9ca9ddd0f7">rewriteIteToOr</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">==> ITE(a, TRUE, b) IFF OR(a, b) <a href="#a2db95a382b0141d9a5098e9ca9ddd0f7"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#ae681f89828ece60f9725c5696204cd72">rewriteIteToAnd</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">==> ITE(a, b, FALSE) IFF AND(a, b) <a href="#ae681f89828ece60f9725c5696204cd72"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#abba61fa631a3e3fd6ae8761754f01c72">rewriteIteToIff</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">==> ITE(a, b, !b) IFF IFF(a, b) <a href="#abba61fa631a3e3fd6ae8761754f01c72"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#af0468c432ee5bfc5f82675f4b50e2002">rewriteIteToImp</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">==> ITE(a, b, TRUE) IFF IMPLIES(a, b) <a href="#af0468c432ee5bfc5f82675f4b50e2002"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#acc27c290c53fdaab6977d43d765b10e3">rewriteIteCond</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">==> ITE(a, b(a), c(a)) IFF ITE(a, b(TRUE), c(FALSE)) <a href="#acc27c290c53fdaab6977d43d765b10e3"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#ac4ef57871856386e38e514d65e3b2c5e">ifLiftUnaryRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">|- op(ITE(cond,a,b)) =/<=> ITE(cond,op(a),op(b)) <a href="#ac4ef57871856386e38e514d65e3b2c5e"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a93299fd86567941880c6566e1d3af6b8">iffOrDistrib</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &iff)
<dl class="el"><dd class="mdescRight">((a|b)<=>(a|c))<=>(a|(b<=>c)); takes ((a|b)<=>(a|c)) as 'iff' <a href="#a93299fd86567941880c6566e1d3af6b8"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#aecd467f33f9bcb736eadfa77f1a517aa">iffAndDistrib</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &iff)
<dl class="el"><dd class="mdescRight">((a&b)<=>(a&c))<=>(!a|(b<=>c)); takes ((a&b)<=>(a&c)) as 'iff' <a href="#aecd467f33f9bcb736eadfa77f1a517aa"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a8c67942a0f72ee11abe27c992e0833c1">rewriteAndSubterms</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, int idx)
<dl class="el"><dd class="mdescRight">(a & b) <=> a & b[a/true]; takes the index of a <a href="#a8c67942a0f72ee11abe27c992e0833c1"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#ae6b1fd56b11dbe24218cd2f5c74518c9">rewriteOrSubterms</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, int idx)
<dl class="el"><dd class="mdescRight">(a | b) <=> a | b[a/false]; takes the index of a <a href="#ae6b1fd56b11dbe24218cd2f5c74518c9"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a1990709421517a01d824217eed8d1021">dummyTheorem</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Temporary cheat for building theorems. <a href="#a1990709421517a01d824217eed8d1021"></a><br/></dl></ul>
<h2><a name="pri-attribs"></a>
Private Attributes</h2>
<ul>
<li><a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> * <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a800f23429437fab5c80e9243de6c5c11">d_core</a>
<dl class="el"><dd class="mdescRight">pointer to theory core <a href="#a800f23429437fab5c80e9243de6c5c11"></a><br/></dl></ul>
<hr/><a name="details" id="details"></a><h2>Detailed Description</h2>
<div class="textblock">
<p>Definition at line <a class="el" href="core__theorem__producer_8h_source.html#l00040">40</a> of file <a class="el" href="core__theorem__producer_8h_source.html">core_theorem_producer.h</a>.</p>
</div><hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="ade8689298e574b416d296d03ed44c051"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::CoreTheoremProducer" ref="ade8689298e574b416d296d03ed44c051" args="(TheoremManager *tm, TheoryCore *core)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVC3::CoreTheoremProducer::CoreTheoremProducer </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a> * </td>
<td class="paramname"><em>tm</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> * </td>
<td class="paramname"><em>core</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="core__theorem__producer_8h_source.html#l00046">46</a> of file <a class="el" href="core__theorem__producer_8h_source.html">core_theorem_producer.h</a>.</p>
</div>
</div>
<a class="anchor" id="a31ee45df90c9144296b9312c9b5c4a97"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::~CoreTheoremProducer" ref="a31ee45df90c9144296b9312c9b5c4a97" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual CVC3::CoreTheoremProducer::~CoreTheoremProducer </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="core__theorem__producer_8h_source.html#l00048">48</a> of file <a class="el" href="core__theorem__producer_8h_source.html">core_theorem_producer.h</a>.</p>
</div>
</div>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="a0b6d312ded517ab466308ec5981d250e"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::typePred" ref="a0b6d312ded517ab466308ec5981d250e" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::typePred </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>e: T ==> |- typePred_T(e) [deriving the type predicate of e] </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#ae4fcd08f795189bb93d76144f77a3862">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00052">52</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, and <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>.</p>
</div>
</div>
<a class="anchor" id="a222db72dc6f637e582dfb9b8dd4e362c"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::rewriteLetDecl" ref="a222db72dc6f637e582dfb9b8dd4e362c" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::rewriteLetDecl </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Replace LETDECL with its definition. </p>
<p>Used only in <a class="el" href="classCVC3_1_1TheoryCore.html" title="This theory handles the built-in logical connectives plus equality. It also handles the registration ...">TheoryCore</a> </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#acad687c3e6faa5709961210637c260da">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00064">64</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="kinds_8h_source.html#l00227">LETDECL</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="a66f5d185eca0ccf417b4bf5ed4448f72"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::rewriteNotAnd" ref="a66f5d185eca0ccf417b4bf5ed4448f72" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::rewriteNotAnd </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> NOT (AND e1 ... en) IFF (OR !e1 ... !en), takes (AND ...) </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#ade3007866410b6565ee0ea1ff4c49a99">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00075">75</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="expr_8h_source.html#l00421">CVC3::Expr::isAnd()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="expr_8h_source.html#l00955">CVC3::orExpr()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="a5ce6abeb6a346d20f5d5860a30a33e28"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::rewriteNotOr" ref="a5ce6abeb6a346d20f5d5860a30a33e28" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::rewriteNotOr </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> NOT (OR e1 ... en) IFF (AND !e1 ... !en), takes (OR ...) </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#aea875ee7355ae6aab01b84c176dbccf6">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00093">93</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l00945">CVC3::andExpr()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="expr_8h_source.html#l00422">CVC3::Expr::isOr()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="a7da16f5874fbc0870f57a9deeeec80b8"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::rewriteNotIff" ref="a7da16f5874fbc0870f57a9deeeec80b8" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::rewriteNotIff </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> NOT IFF(e1,e2) IFF IFF(e1,NOT e2) </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#ae480ca62cb7a8656f01ea3f938fb97d8">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00110">110</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l00424">CVC3::Expr::isIff()</a>, and <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>.</p>
</div>
</div>
<a class="anchor" id="accd799779aa02c5d84352cc48e975b3d"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::rewriteNotIte" ref="accd799779aa02c5d84352cc48e975b3d" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::rewriteNotIte </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> NOT ITE(a,b,c) IFF ITE(a,NOT b,NOT c) </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#ac68942cf0c21011f9429042e279b4a54">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00123">123</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l00423">CVC3::Expr::isITE()</a>, and <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>.</p>
</div>
</div>
<a class="anchor" id="a490808acd89e0732678d570599c93165"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::rewriteIteThen" ref="a490808acd89e0732678d570599c93165" args="(const Expr &e, const Theorem &thenThm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::rewriteIteThen </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>thenThm</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>a |- b == d ==> ITE(a, b, c) == ITE(a, d, c) </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#a8117a95eed02c35936f988d1c9c2bdab">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00136">136</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem_8cpp_source.html#l00385">CVC3::Theorem::getAssumptionsRef()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00240">CVC3::Theorem::getLHS()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="expr_8h_source.html#l00423">CVC3::Expr::isITE()</a>, <a class="el" href="type_8h_source.html#l00059">CVC3::Type::isNull()</a>, <a class="el" href="theorem_8cpp_source.html#l00224">CVC3::Theorem::isRewrite()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="ae1092dc92aef4300caf926b48ac2ec65"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::rewriteIteElse" ref="ae1092dc92aef4300caf926b48ac2ec65" args="(const Expr &e, const Theorem &elseThm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::rewriteIteElse </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>elseThm</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>!a |- c == d ==> ITE(a, b, c) == ITE(a, b, d) </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#a7912f66f5be7e05b0c85f15596747be4">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00161">161</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem_8cpp_source.html#l00385">CVC3::Theorem::getAssumptionsRef()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00240">CVC3::Theorem::getLHS()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="expr_8h_source.html#l00423">CVC3::Expr::isITE()</a>, <a class="el" href="type_8h_source.html#l00059">CVC3::Type::isNull()</a>, <a class="el" href="theorem_8cpp_source.html#l00224">CVC3::Theorem::isRewrite()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="ac888377c574a056b251446902c010352"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::rewriteIteBool" ref="ac888377c574a056b251446902c010352" args="(const Expr &c, const Expr &e1, const Expr &e2)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::rewriteIteBool </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>c</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>e1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e2</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> ITE(c, e1, e2) <=> (c => e1) AND (!c => e2) </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#aa66c668de7d5a026297a6bc901a1f7c3">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00186">186</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l00941">CVC3::Expr::andExpr()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="expr_8h_source.html#l00961">CVC3::Expr::iteExpr()</a>, <a class="el" href="expr_8h_source.html#l00951">CVC3::Expr::orExpr()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="a84abfb7cac1d339c43b322b097aa574c"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::orDistributivityRule" ref="a84abfb7cac1d339c43b322b097aa574c" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::orDistributivityRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>|= (A & B1) | (A & B2) | ... | (A & bn) <=> A & (B1 | B2 | ...| Bn) </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#ac86206cae475f12c9512e436c64656f0">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00202">202</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l00941">CVC3::Expr::andExpr()</a>, <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="expr_8h_source.html#l00421">CVC3::Expr::isAnd()</a>, <a class="el" href="expr_8h_source.html#l00422">CVC3::Expr::isOr()</a>, <a class="el" href="expr_8h_source.html#l00955">CVC3::orExpr()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="af5e5fb97e5fe6197e42c2c44e1757bb3"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::andDistributivityRule" ref="af5e5fb97e5fe6197e42c2c44e1757bb3" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::andDistributivityRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>|= (A | B1) & (A | B2) & ... & (A | bn) <=> A | (B1 & B2 & ...& Bn) </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#aa3091e00758d1cb9e91f1cd3fca1e696">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00245">245</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l00945">CVC3::andExpr()</a>, <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="expr_8h_source.html#l00421">CVC3::Expr::isAnd()</a>, <a class="el" href="expr_8h_source.html#l00422">CVC3::Expr::isOr()</a>, <a class="el" href="expr_8h_source.html#l00951">CVC3::Expr::orExpr()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="ac88efa4d7c591f187d3212c7162ef9a5"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::rewriteImplies" ref="ac88efa4d7c591f187d3212c7162ef9a5" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::rewriteImplies </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> IMPLIES(e1,e2) IFF OR(!e1, e2) </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#a3389cd795acc4cee4b591c1488293963">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00285">285</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, and <a class="el" href="expr_8h_source.html#l00425">CVC3::Expr::isImpl()</a>.</p>
</div>
</div>
<a class="anchor" id="a17536e7c7ffa8d9a34981458a20f21ff"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::rewriteDistinct" ref="a17536e7c7ffa8d9a34981458a20f21ff" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::rewriteDistinct </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> DISTINCT(e1,...,en) IFF AND 1 <= i < j <= n (e[i] /= e[j]) </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#ae429bb5ede0ce74b02cb85f8d0a372dd">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00297">297</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00067">AND</a>, <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="kinds_8h_source.html#l00063">DISTINCT</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l00929">CVC3::Expr::eqExpr()</a>, <a class="el" href="expr_8h_source.html#l01156">CVC3::Expr::getEM()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, and <a class="el" href="expr__manager_8h_source.html#l00280">CVC3::ExprManager::trueExpr()</a>.</p>
</div>
</div>
<a class="anchor" id="a287bd6f15c149c66f1aea020cd144571"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::NotToIte" ref="a287bd6f15c149c66f1aea020cd144571" args="(const Expr &not_e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::NotToIte </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>not_e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> NOT(e) == ITE(e, FALSE, TRUE) </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#aa801f2fa243080def2ef1bff48fba3a9">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00328">328</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, and <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>.</p>
</div>
</div>
<a class="anchor" id="a23a4580e5eb68d197db655776c5e8b0a"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::OrToIte" ref="a23a4580e5eb68d197db655776c5e8b0a" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::OrToIte </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> Or(e) == ITE(e[1], TRUE, e[0]) </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#a07be24cd846d62320aca4fb69645a1db">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00345">345</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l01162">CVC3::Expr::getKids()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="type_8h_source.html#l00059">CVC3::Type::isNull()</a>, <a class="el" href="expr_8h_source.html#l00422">CVC3::Expr::isOr()</a>, <a class="el" href="expr_8h_source.html#l00961">CVC3::Expr::iteExpr()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="aaa435d07458188d1380e42d51c70b419"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::AndToIte" ref="aaa435d07458188d1380e42d51c70b419" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::AndToIte </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> And(e) == ITE(e[1], e[0], FALSE) </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#a332e730ff085f109382a680847189a0d">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00383">383</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l01162">CVC3::Expr::getKids()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="expr_8h_source.html#l00421">CVC3::Expr::isAnd()</a>, <a class="el" href="type_8h_source.html#l00059">CVC3::Type::isNull()</a>, <a class="el" href="expr_8h_source.html#l00961">CVC3::Expr::iteExpr()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="af0a98459d73dbd5b89582d803f304aac"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::IffToIte" ref="af0a98459d73dbd5b89582d803f304aac" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::IffToIte </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> IFF(a,b) == ITE(a, b, !b) </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#ac0bd85a42727e1f5d41c7f4fb5366acf">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00423">423</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="expr_8h_source.html#l00424">CVC3::Expr::isIff()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="aa5abdd3bfe669a3a0b28a92d28e8958a"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::ImpToIte" ref="aa5abdd3bfe669a3a0b28a92d28e8958a" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::ImpToIte </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> IMPLIES(a,b) == ITE(a, b, TRUE) </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#a6639598cf87b9c51bc097bad578b0ac4">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00439">439</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="expr_8h_source.html#l00425">CVC3::Expr::isImpl()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="a27d39117a5ede71d9c460b0232bdd469"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::rewriteIteToNot" ref="a27d39117a5ede71d9c460b0232bdd469" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::rewriteIteToNot </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> ITE(e, FALSE, TRUE) IFF NOT(e) </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#a71c2aa506efd447f6c411159f44d5af0">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00455">455</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l00355">CVC3::Expr::isFalse()</a>, <a class="el" href="expr_8h_source.html#l00423">CVC3::Expr::isITE()</a>, <a class="el" href="expr_8h_source.html#l00356">CVC3::Expr::isTrue()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="a2db95a382b0141d9a5098e9ca9ddd0f7"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::rewriteIteToOr" ref="a2db95a382b0141d9a5098e9ca9ddd0f7" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::rewriteIteToOr </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> ITE(a, TRUE, b) IFF OR(a, b) </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#ab23828c9cc70a3805a0be7632e03163b">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00467">467</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l00423">CVC3::Expr::isITE()</a>, <a class="el" href="expr_8h_source.html#l00356">CVC3::Expr::isTrue()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="ae681f89828ece60f9725c5696204cd72"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::rewriteIteToAnd" ref="ae681f89828ece60f9725c5696204cd72" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::rewriteIteToAnd </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> ITE(a, b, FALSE) IFF AND(a, b) </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#a3eb08bdf90ac80d5c372e4791120d894">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00479">479</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l00355">CVC3::Expr::isFalse()</a>, <a class="el" href="expr_8h_source.html#l00423">CVC3::Expr::isITE()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="abba61fa631a3e3fd6ae8761754f01c72"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::rewriteIteToIff" ref="abba61fa631a3e3fd6ae8761754f01c72" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::rewriteIteToIff </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> ITE(a, b, !b) IFF IFF(a, b) </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#a8a98457f410ab11e4b66adad150e1b67">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00491">491</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l00423">CVC3::Expr::isITE()</a>, <a class="el" href="expr_8h_source.html#l00937">CVC3::Expr::negate()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="af0468c432ee5bfc5f82675f4b50e2002"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::rewriteIteToImp" ref="af0468c432ee5bfc5f82675f4b50e2002" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::rewriteIteToImp </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> ITE(a, b, TRUE) IFF IMPLIES(a, b) </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#a1d30881c6f1a902575da033dbbeb2aa9">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00503">503</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l00423">CVC3::Expr::isITE()</a>, <a class="el" href="expr_8h_source.html#l00356">CVC3::Expr::isTrue()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="acc27c290c53fdaab6977d43d765b10e3"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::rewriteIteCond" ref="acc27c290c53fdaab6977d43d765b10e3" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::rewriteIteCond </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> ITE(a, b(a), c(a)) IFF ITE(a, b(TRUE), c(FALSE)) </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#a03f8a74b8b1b6d90ff23a0a6150c49d6">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00516">516</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l00423">CVC3::Expr::isITE()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="ac4ef57871856386e38e514d65e3b2c5e"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::ifLiftUnaryRule" ref="ac4ef57871856386e38e514d65e3b2c5e" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::ifLiftUnaryRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>|- op(ITE(cond,a,b)) =/<=> ITE(cond,op(a),op(b)) </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#abbf1d27a8dba7669aac602a4a95f0b3f">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00588">588</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l01183">CVC3::Expr::getOp()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="expr_8h_source.html#l00423">CVC3::Expr::isITE()</a>, <a class="el" href="expr_8h_source.html#l00961">CVC3::Expr::iteExpr()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="a93299fd86567941880c6566e1d3af6b8"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::iffOrDistrib" ref="a93299fd86567941880c6566e1d3af6b8" args="(const Expr &iff)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::iffOrDistrib </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>iff</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>((a|b)<=>(a|c))<=>(a|(b<=>c)); takes ((a|b)<=>(a|c)) as 'iff' </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#a8fc33a9fbd44abba98547acf63322fc8">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00543">543</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l00965">CVC3::Expr::iffExpr()</a>, <a class="el" href="expr_8h_source.html#l00424">CVC3::Expr::isIff()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="aecd467f33f9bcb736eadfa77f1a517aa"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::iffAndDistrib" ref="aecd467f33f9bcb736eadfa77f1a517aa" args="(const Expr &iff)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::iffAndDistrib </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>iff</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>((a&b)<=>(a&c))<=>(!a|(b<=>c)); takes ((a&b)<=>(a&c)) as 'iff' </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#a0648f60b8e9b11dee35544c83512fa30">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00565">565</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l00965">CVC3::Expr::iffExpr()</a>, <a class="el" href="expr_8h_source.html#l00424">CVC3::Expr::isIff()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="a8c67942a0f72ee11abe27c992e0833c1"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::rewriteAndSubterms" ref="a8c67942a0f72ee11abe27c992e0833c1" args="(const Expr &e, int idx)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::rewriteAndSubterms </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">int </td>
<td class="paramname"><em>idx</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>(a & b) <=> a & b[a/true]; takes the index of a </p>
<p>and rewrites all the other conjuncts. </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#a07d66271324bda72a66505bb427df156">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00621">621</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l01183">CVC3::Expr::getOp()</a>, <a class="el" href="expr__map_8h_source.html#l00312">CVC3::ExprHashMap< Data >::insert()</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="expr_8h_source.html#l00421">CVC3::Expr::isAnd()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="ae6b1fd56b11dbe24218cd2f5c74518c9"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::rewriteOrSubterms" ref="ae6b1fd56b11dbe24218cd2f5c74518c9" args="(const Expr &e, int idx)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::rewriteOrSubterms </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">int </td>
<td class="paramname"><em>idx</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>(a | b) <=> a | b[a/false]; takes the index of a </p>
<p>and rewrites all the other disjuncts. </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#a0d589028239025d0e43c92c04b5d586a">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00647">647</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr_8h_source.html#l01183">CVC3::Expr::getOp()</a>, <a class="el" href="expr__map_8h_source.html#l00312">CVC3::ExprHashMap< Data >::insert()</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="expr_8h_source.html#l00422">CVC3::Expr::isOr()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="a1990709421517a01d824217eed8d1021"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::dummyTheorem" ref="a1990709421517a01d824217eed8d1021" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CoreTheoremProducer::dummyTheorem </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Temporary cheat for building theorems. </p>
<p>Implements <a class="el" href="classCVC3_1_1CoreProofRules.html#a9592705bbf82393b7f6500fa33ead252">CVC3::CoreProofRules</a>.</p>
<p>Definition at line <a class="el" href="core__theorem__producer_8cpp_source.html#l00670">670</a> of file <a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>.</p>
</div>
</div>
<hr/><h2>Member Data Documentation</h2>
<a class="anchor" id="a800f23429437fab5c80e9243de6c5c11"></a><!-- doxytag: member="CVC3::CoreTheoremProducer::d_core" ref="a800f23429437fab5c80e9243de6c5c11" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a>* <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a800f23429437fab5c80e9243de6c5c11">CVC3::CoreTheoremProducer::d_core</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>pointer to theory core </p>
<p>Definition at line <a class="el" href="core__theorem__producer_8h_source.html#l00043">43</a> of file <a class="el" href="core__theorem__producer_8h_source.html">core_theorem_producer.h</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="core__theorem__producer_8h_source.html">core_theorem_producer.h</a></li>
<li><a class="el" href="core__theorem__producer_8cpp_source.html">core_theorem_producer.cpp</a></li>
</ul>
</div>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
