<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<meta http-equiv="X-UA-Compatible" content="IE=9"/>
<title>CVC3: Member List</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="jquery.js"></script>
<script type="text/javascript" src="dynsections.js"></script>
<link href="doxygen.css" rel="stylesheet" type="text/css" />
</head>
<body>
<div id="top"><!-- do not remove this div, it is closed by doxygen! -->
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3
</div>
</td>
</tr>
</tbody>
</table>
</div>
<!-- end header part -->
<!-- Generated by Doxygen 1.8.2 -->
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li class="current"><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="annotated.html"><span>Class List</span></a></li>
<li><a href="classes.html"><span>Class Index</span></a></li>
<li><a href="inherits.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="namespaceCVC3.html">CVC3</a></li><li class="navelem"><a class="el" href="classCVC3_1_1CoreProofRules.html">CoreProofRules</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="headertitle">
<div class="title">CVC3::CoreProofRules Member List</div> </div>
</div><!--header-->
<div class="contents">
<p>This is the complete list of members for <a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a>, including all inherited members.</p>
<table class="directory">
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#aa3091e00758d1cb9e91f1cd3fca1e696">andDistributivityRule</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#a332e730ff085f109382a680847189a0d">AndToIte</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#a9592705bbf82393b7f6500fa33ead252">dummyTheorem</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#a0648f60b8e9b11dee35544c83512fa30">iffAndDistrib</a>(const Expr &iff)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#a8fc33a9fbd44abba98547acf63322fc8">iffOrDistrib</a>(const Expr &iff)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#ac0bd85a42727e1f5d41c7f4fb5366acf">IffToIte</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#abbf1d27a8dba7669aac602a4a95f0b3f">ifLiftUnaryRule</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#a6639598cf87b9c51bc097bad578b0ac4">ImpToIte</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#aa801f2fa243080def2ef1bff48fba3a9">NotToIte</a>(const Expr &not_e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#ac86206cae475f12c9512e436c64656f0">orDistributivityRule</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#a07be24cd846d62320aca4fb69645a1db">OrToIte</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#a07d66271324bda72a66505bb427df156">rewriteAndSubterms</a>(const Expr &e, int idx)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#ae429bb5ede0ce74b02cb85f8d0a372dd">rewriteDistinct</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#a3389cd795acc4cee4b591c1488293963">rewriteImplies</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#aa66c668de7d5a026297a6bc901a1f7c3">rewriteIteBool</a>(const Expr &c, const Expr &e1, const Expr &e2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#a03f8a74b8b1b6d90ff23a0a6150c49d6">rewriteIteCond</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#a7912f66f5be7e05b0c85f15596747be4">rewriteIteElse</a>(const Expr &e, const Theorem &elseThm)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#a8117a95eed02c35936f988d1c9c2bdab">rewriteIteThen</a>(const Expr &e, const Theorem &thenThm)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#a3eb08bdf90ac80d5c372e4791120d894">rewriteIteToAnd</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#a8a98457f410ab11e4b66adad150e1b67">rewriteIteToIff</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#a1d30881c6f1a902575da033dbbeb2aa9">rewriteIteToImp</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#a71c2aa506efd447f6c411159f44d5af0">rewriteIteToNot</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#ab23828c9cc70a3805a0be7632e03163b">rewriteIteToOr</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#acad687c3e6faa5709961210637c260da">rewriteLetDecl</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#ade3007866410b6565ee0ea1ff4c49a99">rewriteNotAnd</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#ae480ca62cb7a8656f01ea3f938fb97d8">rewriteNotIff</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#ac68942cf0c21011f9429042e279b4a54">rewriteNotIte</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#aea875ee7355ae6aab01b84c176dbccf6">rewriteNotOr</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#a0d589028239025d0e43c92c04b5d586a">rewriteOrSubterms</a>(const Expr &e, int idx)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#ae4fcd08f795189bb93d76144f77a3862">typePred</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html#a04af291caa087f8dc1c2c8d346e4dffe">~CoreProofRules</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1CoreProofRules.html">CVC3::CoreProofRules</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">virtual</span></td></tr>
</table></div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:19 for CVC3 by  <a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/>
</a> 1.8.2
</small></address>
</body>
</html>
