<!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::CoreProofRules 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_1CoreProofRules.html">CoreProofRules</a> </li>
</ul>
</div>
</div>
<div class="header">
<div class="summary">
<a href="#pub-methods">Public Member Functions</a> </div>
<div class="headertitle">
<div class="title">CVC3::CoreProofRules Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="CVC3::CoreProofRules" -->
<p><code>#include <<a class="el" href="core__proof__rules_8h_source.html">core_proof_rules.h</a>></code></p>
<div class="dynheader">
Inheritance diagram for CVC3::CoreProofRules:</div>
<div class="dyncontent">
<div class="center">
<img src="classCVC3_1_1CoreProofRules.png" usemap="#CVC3::CoreProofRules_map" alt=""/>
<map id="CVC3::CoreProofRules_map" name="CVC3::CoreProofRules_map">
<area href="classCVC3_1_1CoreTheoremProducer.html" alt="CVC3::CoreTheoremProducer" shape="rect" coords="0,56,182,80"/>
</map>
</div></div>
<p><a href="classCVC3_1_1CoreProofRules-members.html">List of all members.</a></p>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li>virtual <a class="el" href="classCVC3_1_1CoreProofRules.html#a04af291caa087f8dc1c2c8d346e4dffe">~CoreProofRules</a> ()
<dl class="el"><dd class="mdescRight">Destructor. <a href="#a04af291caa087f8dc1c2c8d346e4dffe"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#ae4fcd08f795189bb93d76144f77a3862">typePred</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">e: T ==> |- typePred_T(e) [deriving the type predicate of e] <a href="#ae4fcd08f795189bb93d76144f77a3862"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#acad687c3e6faa5709961210637c260da">rewriteLetDecl</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">Replace LETDECL with its definition. <a href="#acad687c3e6faa5709961210637c260da"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#ade3007866410b6565ee0ea1ff4c49a99">rewriteNotAnd</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">==> NOT (AND e1 ... en) IFF (OR !e1 ... !en), takes (AND ...) <a href="#ade3007866410b6565ee0ea1ff4c49a99"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#aea875ee7355ae6aab01b84c176dbccf6">rewriteNotOr</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">==> NOT (OR e1 ... en) IFF (AND !e1 ... !en), takes (OR ...) <a href="#aea875ee7355ae6aab01b84c176dbccf6"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#ae480ca62cb7a8656f01ea3f938fb97d8">rewriteNotIff</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">==> NOT IFF(e1,e2) IFF IFF(e1,NOT e2) <a href="#ae480ca62cb7a8656f01ea3f938fb97d8"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#ac68942cf0c21011f9429042e279b4a54">rewriteNotIte</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">==> NOT ITE(a,b,c) IFF ITE(a,NOT b,NOT c) <a href="#ac68942cf0c21011f9429042e279b4a54"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#a8117a95eed02c35936f988d1c9c2bdab">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)=0
<dl class="el"><dd class="mdescRight">a |- b == d ==> ITE(a, b, c) == ITE(a, d, c) <a href="#a8117a95eed02c35936f988d1c9c2bdab"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#a7912f66f5be7e05b0c85f15596747be4">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)=0
<dl class="el"><dd class="mdescRight">!a |- c == d ==> ITE(a, b, c) == ITE(a, b, d) <a href="#a7912f66f5be7e05b0c85f15596747be4"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#aa66c668de7d5a026297a6bc901a1f7c3">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)=0
<dl class="el"><dd class="mdescRight">==> ITE(c, e1, e2) <=> (c => e1) AND (!c => e2) <a href="#aa66c668de7d5a026297a6bc901a1f7c3"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#ac86206cae475f12c9512e436c64656f0">orDistributivityRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">|= (A & B1) | (A & B2) | ... | (A & bn) <=> A & (B1 | B2 | ...| Bn) <a href="#ac86206cae475f12c9512e436c64656f0"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#aa3091e00758d1cb9e91f1cd3fca1e696">andDistributivityRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">|= (A | B1) & (A | B2) & ... & (A | bn) <=> A | (B1 & B2 & ...& Bn) <a href="#aa3091e00758d1cb9e91f1cd3fca1e696"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#a3389cd795acc4cee4b591c1488293963">rewriteImplies</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">==> IMPLIES(e1,e2) IFF OR(!e1, e2) <a href="#a3389cd795acc4cee4b591c1488293963"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#ae429bb5ede0ce74b02cb85f8d0a372dd">rewriteDistinct</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">==> DISTINCT(e1,...,en) IFF AND 1 <= i < j <= n (e[i] /= e[j]) <a href="#ae429bb5ede0ce74b02cb85f8d0a372dd"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#aa801f2fa243080def2ef1bff48fba3a9">NotToIte</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &not_e)=0
<dl class="el"><dd class="mdescRight">==> NOT(e) == ITE(e, FALSE, TRUE) <a href="#aa801f2fa243080def2ef1bff48fba3a9"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#a07be24cd846d62320aca4fb69645a1db">OrToIte</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">==> Or(e) == ITE(e[1], TRUE, e[0]) <a href="#a07be24cd846d62320aca4fb69645a1db"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#a332e730ff085f109382a680847189a0d">AndToIte</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">==> And(e) == ITE(e[1], e[0], FALSE) <a href="#a332e730ff085f109382a680847189a0d"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#ac0bd85a42727e1f5d41c7f4fb5366acf">IffToIte</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">==> IFF(a,b) == ITE(a, b, !b) <a href="#ac0bd85a42727e1f5d41c7f4fb5366acf"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#a6639598cf87b9c51bc097bad578b0ac4">ImpToIte</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">==> IMPLIES(a,b) == ITE(a, b, TRUE) <a href="#a6639598cf87b9c51bc097bad578b0ac4"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#a71c2aa506efd447f6c411159f44d5af0">rewriteIteToNot</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">==> ITE(e, FALSE, TRUE) IFF NOT(e) <a href="#a71c2aa506efd447f6c411159f44d5af0"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#ab23828c9cc70a3805a0be7632e03163b">rewriteIteToOr</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">==> ITE(a, TRUE, b) IFF OR(a, b) <a href="#ab23828c9cc70a3805a0be7632e03163b"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#a3eb08bdf90ac80d5c372e4791120d894">rewriteIteToAnd</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">==> ITE(a, b, FALSE) IFF AND(a, b) <a href="#a3eb08bdf90ac80d5c372e4791120d894"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#a8a98457f410ab11e4b66adad150e1b67">rewriteIteToIff</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">==> ITE(a, b, !b) IFF IFF(a, b) <a href="#a8a98457f410ab11e4b66adad150e1b67"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#a1d30881c6f1a902575da033dbbeb2aa9">rewriteIteToImp</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">==> ITE(a, b, TRUE) IFF IMPLIES(a, b) <a href="#a1d30881c6f1a902575da033dbbeb2aa9"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#a03f8a74b8b1b6d90ff23a0a6150c49d6">rewriteIteCond</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">==> ITE(a, b(a), c(a)) IFF ITE(a, b(TRUE), c(FALSE)) <a href="#a03f8a74b8b1b6d90ff23a0a6150c49d6"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#abbf1d27a8dba7669aac602a4a95f0b3f">ifLiftUnaryRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">|- op(ITE(cond,a,b)) =/<=> ITE(cond,op(a),op(b)) <a href="#abbf1d27a8dba7669aac602a4a95f0b3f"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#a8fc33a9fbd44abba98547acf63322fc8">iffOrDistrib</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &iff)=0
<dl class="el"><dd class="mdescRight">((a|b)<=>(a|c))<=>(a|(b<=>c)); takes ((a|b)<=>(a|c)) as 'iff' <a href="#a8fc33a9fbd44abba98547acf63322fc8"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#a0648f60b8e9b11dee35544c83512fa30">iffAndDistrib</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &iff)=0
<dl class="el"><dd class="mdescRight">((a&b)<=>(a&c))<=>(!a|(b<=>c)); takes ((a&b)<=>(a&c)) as 'iff' <a href="#a0648f60b8e9b11dee35544c83512fa30"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#a07d66271324bda72a66505bb427df156">rewriteAndSubterms</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, int idx)=0
<dl class="el"><dd class="mdescRight">(a & b) <=> a & b[a/true]; takes the index of a <a href="#a07d66271324bda72a66505bb427df156"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#a0d589028239025d0e43c92c04b5d586a">rewriteOrSubterms</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, int idx)=0
<dl class="el"><dd class="mdescRight">(a | b) <=> a | b[a/false]; takes the index of a <a href="#a0d589028239025d0e43c92c04b5d586a"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1CoreProofRules.html#a9592705bbf82393b7f6500fa33ead252">dummyTheorem</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">Temporary cheat for building theorems. <a href="#a9592705bbf82393b7f6500fa33ead252"></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__proof__rules_8h_source.html#l00034">34</a> of file <a class="el" href="core__proof__rules_8h_source.html">core_proof_rules.h</a>.</p>
</div><hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="a04af291caa087f8dc1c2c8d346e4dffe"></a><!-- doxytag: member="CVC3::CoreProofRules::~CoreProofRules" ref="a04af291caa087f8dc1c2c8d346e4dffe" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual CVC3::CoreProofRules::~CoreProofRules </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Destructor. </p>
<p>Definition at line <a class="el" href="core__proof__rules_8h_source.html#l00037">37</a> of file <a class="el" href="core__proof__rules_8h_source.html">core_proof_rules.h</a>.</p>
</div>
</div>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="ae4fcd08f795189bb93d76144f77a3862"></a><!-- doxytag: member="CVC3::CoreProofRules::typePred" ref="ae4fcd08f795189bb93d76144f77a3862" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>e: T ==> |- typePred_T(e) [deriving the type predicate of e] </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a0b6d312ded517ab466308ec5981d250e">CVC3::CoreTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="theory__core_8cpp_source.html#l04260">CVC3::TheoryCore::setupTerm()</a>, and <a class="el" href="theory__core_8cpp_source.html#l04186">CVC3::TheoryCore::typePred()</a>.</p>
</div>
</div>
<a class="anchor" id="acad687c3e6faa5709961210637c260da"></a><!-- doxytag: member="CVC3::CoreProofRules::rewriteLetDecl" ref="acad687c3e6faa5709961210637c260da" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure 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>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a222db72dc6f637e582dfb9b8dd4e362c">CVC3::CoreTheoremProducer</a>.</p>
<p>Referenced by <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>, and <a class="el" href="theory__core_8cpp_source.html#l00968">CVC3::TheoryCore::rewrite()</a>.</p>
</div>
</div>
<a class="anchor" id="ade3007866410b6565ee0ea1ff4c49a99"></a><!-- doxytag: member="CVC3::CoreProofRules::rewriteNotAnd" ref="ade3007866410b6565ee0ea1ff4c49a99" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> NOT (AND e1 ... en) IFF (OR !e1 ... !en), takes (AND ...) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a66f5d185eca0ccf417b4bf5ed4448f72">CVC3::CoreTheoremProducer</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="aea875ee7355ae6aab01b84c176dbccf6"></a><!-- doxytag: member="CVC3::CoreProofRules::rewriteNotOr" ref="aea875ee7355ae6aab01b84c176dbccf6" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> NOT (OR e1 ... en) IFF (AND !e1 ... !en), takes (OR ...) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a5ce6abeb6a346d20f5d5860a30a33e28">CVC3::CoreTheoremProducer</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="ae480ca62cb7a8656f01ea3f938fb97d8"></a><!-- doxytag: member="CVC3::CoreProofRules::rewriteNotIff" ref="ae480ca62cb7a8656f01ea3f938fb97d8" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> NOT IFF(e1,e2) IFF IFF(e1,NOT e2) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a7da16f5874fbc0870f57a9deeeec80b8">CVC3::CoreTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ac68942cf0c21011f9429042e279b4a54"></a><!-- doxytag: member="CVC3::CoreProofRules::rewriteNotIte" ref="ac68942cf0c21011f9429042e279b4a54" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> NOT ITE(a,b,c) IFF ITE(a,NOT b,NOT c) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#accd799779aa02c5d84352cc48e975b3d">CVC3::CoreTheoremProducer</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="a8117a95eed02c35936f988d1c9c2bdab"></a><!-- doxytag: member="CVC3::CoreProofRules::rewriteIteThen" ref="a8117a95eed02c35936f988d1c9c2bdab" args="(const Expr &e, const Theorem &thenThm)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>a |- b == d ==> ITE(a, b, c) == ITE(a, d, c) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a490808acd89e0732678d570599c93165">CVC3::CoreTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="expr__transform_8cpp_source.html#l00334">CVC3::ExprTransform::newPPrec()</a>.</p>
</div>
</div>
<a class="anchor" id="a7912f66f5be7e05b0c85f15596747be4"></a><!-- doxytag: member="CVC3::CoreProofRules::rewriteIteElse" ref="a7912f66f5be7e05b0c85f15596747be4" args="(const Expr &e, const Theorem &elseThm)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>!a |- c == d ==> ITE(a, b, c) == ITE(a, b, d) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#ae1092dc92aef4300caf926b48ac2ec65">CVC3::CoreTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="expr__transform_8cpp_source.html#l00334">CVC3::ExprTransform::newPPrec()</a>.</p>
</div>
</div>
<a class="anchor" id="aa66c668de7d5a026297a6bc901a1f7c3"></a><!-- doxytag: member="CVC3::CoreProofRules::rewriteIteBool" ref="aa66c668de7d5a026297a6bc901a1f7c3" args="(const Expr &c, const Expr &e1, const Expr &e2)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> ITE(c, e1, e2) <=> (c => e1) AND (!c => e2) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#ac888377c574a056b251446902c010352">CVC3::CoreTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ac86206cae475f12c9512e436c64656f0"></a><!-- doxytag: member="CVC3::CoreProofRules::orDistributivityRule" ref="ac86206cae475f12c9512e436c64656f0" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>|= (A & B1) | (A & B2) | ... | (A & bn) <=> A & (B1 | B2 | ...| Bn) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a84abfb7cac1d339c43b322b097aa574c">CVC3::CoreTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="aa3091e00758d1cb9e91f1cd3fca1e696"></a><!-- doxytag: member="CVC3::CoreProofRules::andDistributivityRule" ref="aa3091e00758d1cb9e91f1cd3fca1e696" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>|= (A | B1) & (A | B2) & ... & (A | bn) <=> A | (B1 & B2 & ...& Bn) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#af5e5fb97e5fe6197e42c2c44e1757bb3">CVC3::CoreTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a3389cd795acc4cee4b591c1488293963"></a><!-- doxytag: member="CVC3::CoreProofRules::rewriteImplies" ref="a3389cd795acc4cee4b591c1488293963" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> IMPLIES(e1,e2) IFF OR(!e1, e2) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#ac88efa4d7c591f187d3212c7162ef9a5">CVC3::CoreTheoremProducer</a>.</p>
<p>Referenced by <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__core_8cpp_source.html#l00968">CVC3::TheoryCore::rewrite()</a>, and <a class="el" href="theory__core_8cpp_source.html#l01292">CVC3::TheoryCore::simplifyOp()</a>.</p>
</div>
</div>
<a class="anchor" id="ae429bb5ede0ce74b02cb85f8d0a372dd"></a><!-- doxytag: member="CVC3::CoreProofRules::rewriteDistinct" ref="ae429bb5ede0ce74b02cb85f8d0a372dd" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure 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>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a17536e7c7ffa8d9a34981458a20f21ff">CVC3::CoreTheoremProducer</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="aa801f2fa243080def2ef1bff48fba3a9"></a><!-- doxytag: member="CVC3::CoreProofRules::NotToIte" ref="aa801f2fa243080def2ef1bff48fba3a9" args="(const Expr &not_e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> NOT(e) == ITE(e, FALSE, TRUE) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a287bd6f15c149c66f1aea020cd144571">CVC3::CoreTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a07be24cd846d62320aca4fb69645a1db"></a><!-- doxytag: member="CVC3::CoreProofRules::OrToIte" ref="a07be24cd846d62320aca4fb69645a1db" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> Or(e) == ITE(e[1], TRUE, e[0]) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a23a4580e5eb68d197db655776c5e8b0a">CVC3::CoreTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a332e730ff085f109382a680847189a0d"></a><!-- doxytag: member="CVC3::CoreProofRules::AndToIte" ref="a332e730ff085f109382a680847189a0d" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> And(e) == ITE(e[1], e[0], FALSE) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#aaa435d07458188d1380e42d51c70b419">CVC3::CoreTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ac0bd85a42727e1f5d41c7f4fb5366acf"></a><!-- doxytag: member="CVC3::CoreProofRules::IffToIte" ref="ac0bd85a42727e1f5d41c7f4fb5366acf" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> IFF(a,b) == ITE(a, b, !b) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#af0a98459d73dbd5b89582d803f304aac">CVC3::CoreTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a6639598cf87b9c51bc097bad578b0ac4"></a><!-- doxytag: member="CVC3::CoreProofRules::ImpToIte" ref="a6639598cf87b9c51bc097bad578b0ac4" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> IMPLIES(a,b) == ITE(a, b, TRUE) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#aa5abdd3bfe669a3a0b28a92d28e8958a">CVC3::CoreTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a71c2aa506efd447f6c411159f44d5af0"></a><!-- doxytag: member="CVC3::CoreProofRules::rewriteIteToNot" ref="a71c2aa506efd447f6c411159f44d5af0" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> ITE(e, FALSE, TRUE) IFF NOT(e) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a27d39117a5ede71d9c460b0232bdd469">CVC3::CoreTheoremProducer</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="ab23828c9cc70a3805a0be7632e03163b"></a><!-- doxytag: member="CVC3::CoreProofRules::rewriteIteToOr" ref="ab23828c9cc70a3805a0be7632e03163b" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> ITE(a, TRUE, b) IFF OR(a, b) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a2db95a382b0141d9a5098e9ca9ddd0f7">CVC3::CoreTheoremProducer</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="a3eb08bdf90ac80d5c372e4791120d894"></a><!-- doxytag: member="CVC3::CoreProofRules::rewriteIteToAnd" ref="a3eb08bdf90ac80d5c372e4791120d894" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> ITE(a, b, FALSE) IFF AND(a, b) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#ae681f89828ece60f9725c5696204cd72">CVC3::CoreTheoremProducer</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="a8a98457f410ab11e4b66adad150e1b67"></a><!-- doxytag: member="CVC3::CoreProofRules::rewriteIteToIff" ref="a8a98457f410ab11e4b66adad150e1b67" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> ITE(a, b, !b) IFF IFF(a, b) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#abba61fa631a3e3fd6ae8761754f01c72">CVC3::CoreTheoremProducer</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="a1d30881c6f1a902575da033dbbeb2aa9"></a><!-- doxytag: member="CVC3::CoreProofRules::rewriteIteToImp" ref="a1d30881c6f1a902575da033dbbeb2aa9" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> ITE(a, b, TRUE) IFF IMPLIES(a, b) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#af0468c432ee5bfc5f82675f4b50e2002">CVC3::CoreTheoremProducer</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="a03f8a74b8b1b6d90ff23a0a6150c49d6"></a><!-- doxytag: member="CVC3::CoreProofRules::rewriteIteCond" ref="a03f8a74b8b1b6d90ff23a0a6150c49d6" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure 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>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#acc27c290c53fdaab6977d43d765b10e3">CVC3::CoreTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="theory__core_8cpp_source.html#l00968">CVC3::TheoryCore::rewrite()</a>, and <a class="el" href="expr__transform_8cpp_source.html#l00476">CVC3::ExprTransform::simplifyWithCare()</a>.</p>
</div>
</div>
<a class="anchor" id="abbf1d27a8dba7669aac602a4a95f0b3f"></a><!-- doxytag: member="CVC3::CoreProofRules::ifLiftUnaryRule" ref="abbf1d27a8dba7669aac602a4a95f0b3f" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>|- op(ITE(cond,a,b)) =/<=> ITE(cond,op(a),op(b)) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#ac4ef57871856386e38e514d65e3b2c5e">CVC3::CoreTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a8fc33a9fbd44abba98547acf63322fc8"></a><!-- doxytag: member="CVC3::CoreProofRules::iffOrDistrib" ref="a8fc33a9fbd44abba98547acf63322fc8" args="(const Expr &iff)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure 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>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a93299fd86567941880c6566e1d3af6b8">CVC3::CoreTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a0648f60b8e9b11dee35544c83512fa30"></a><!-- doxytag: member="CVC3::CoreProofRules::iffAndDistrib" ref="a0648f60b8e9b11dee35544c83512fa30" args="(const Expr &iff)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure 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>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#aecd467f33f9bcb736eadfa77f1a517aa">CVC3::CoreTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a07d66271324bda72a66505bb427df156"></a><!-- doxytag: member="CVC3::CoreProofRules::rewriteAndSubterms" ref="a07d66271324bda72a66505bb427df156" args="(const Expr &e, int idx)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure 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>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a8c67942a0f72ee11abe27c992e0833c1">CVC3::CoreTheoremProducer</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="a0d589028239025d0e43c92c04b5d586a"></a><!-- doxytag: member="CVC3::CoreProofRules::rewriteOrSubterms" ref="a0d589028239025d0e43c92c04b5d586a" args="(const Expr &e, int idx)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure 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>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#ae6b1fd56b11dbe24218cd2f5c74518c9">CVC3::CoreTheoremProducer</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="a9592705bbf82393b7f6500fa33ead252"></a><!-- doxytag: member="CVC3::CoreProofRules::dummyTheorem" ref="a9592705bbf82393b7f6500fa33ead252" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::CoreProofRules::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> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Temporary cheat for building theorems. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a1990709421517a01d824217eed8d1021">CVC3::CoreTheoremProducer</a>.</p>
<p>Referenced by <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="core__proof__rules_8h_source.html">core_proof_rules.h</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>
