<!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_1ArithTheoremProducer.html">ArithTheoremProducer</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="headertitle">
<div class="title">CVC3::ArithTheoremProducer Member List</div> </div>
</div><!--header-->
<div class="contents">
<p>This is the complete list of members for <a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a>, including all inherited members.</p>
<table class="directory">
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a3b2bea72cd9163daa7c41388037bca29">addInequalities</a>(const Theorem &thm1, const Theorem &thm2)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a0eb949bb19e618a8318f236b249fadd5">addInequalities</a>(const std::vector< Theorem > &thms)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a8216db52c44de1ba9a50ca6dfea24720">ArithTheoremProducer</a>(TheoremManager *tm, TheoryArithNew *theoryArith)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a9548361051bb6febc314faa107d2c2f5">canonCombineLikeTerms</a>(const std::vector< Expr > &sumExprs)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ac9ee451992ab00f200ee8aee26e99e0c">canonComboLikeTerms</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a92540cc58f6203c2904fc2bd197190da">canonDivide</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a515e5d076ed135a6d943c2f5d5e34188">canonDivideConst</a>(const Expr &c, const Expr &d)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a4d2d8da9de6d6faaa07758c01e3a9fe8">canonDivideMult</a>(const Expr &cx, const Expr &d)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a4338b85f1dd0fca0cc58e6b7259a20b4">canonDividePlus</a>(const Expr &e, const Expr &d)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#aa651eb7a4d20a77135efa2d3e984c355">canonDivideVar</a>(const Expr &e1, const Expr &e2)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a19964269c705bafbe69cb1052fe7bec8">canonFlattenSum</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a7c7c860b193ec63a776dd13613aeca25">canonInvert</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a7b07ab799dbdf80254df3ec7fc35d36d">canonInvertConst</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#afb0c2a89f3373dcb26cd516714d0e49a">canonInvertLeaf</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a70a381c22184655fb6d4f3b621bf216b">canonInvertMult</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a6a829cb16f960f9e7c2f25ea4906eaba">canonInvertPow</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a9bd77385dd0cbaac271aaab4b6c6ec09">canonMult</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#affbdf02016310d8cd6a9037fdd9eddc6">canonMultConstConst</a>(const Expr &c1, const Expr &c2)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a10ebfab26aa4ee1a147f08d8f6b94c45">canonMultConstMult</a>(const Expr &c, const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a48b21552a97a3a75ae469fb48c155e51">canonMultConstPlus</a>(const Expr &e1, const Expr &e2)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ab0e0e14c71501a9f8208963c54010fe4">canonMultConstSum</a>(const Expr &c1, const Expr &sum)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ad51f0d5c3232b6c247939a10e253f53d">canonMultConstTerm</a>(const Expr &c1, const Expr &c2, const Expr &t)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#aae1bc41d54f8b148ce5cf9425ac688af">canonMultLeafLeaf</a>(const Expr &e1, const Expr &e2)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a05b2608fd280890cb49bf4534a54e304">canonMultLeafOrPowMult</a>(const Expr &e1, const Expr &e2)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a0b344f367f01d240d997df7edfe1a12c">canonMultLeafOrPowOrMultPlus</a>(const Expr &e1, const Expr &e2)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ab5166b206f49897a6a49ba0014c0b808">canonMultMtermMterm</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ae5a6e1b2c7b9239b7e53027c51a2dc7e">canonMultOne</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ac0363ff2f51ad1173ed1e46046b0654a">canonMultPlusPlus</a>(const Expr &e1, const Expr &e2)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#aabc24cdaf5d3a390f9880937bac17311">canonMultPowLeaf</a>(const Expr &e1, const Expr &e2)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#aebf0a0b539104e2190b53351efc6116b">canonMultPowPow</a>(const Expr &e1, const Expr &e2)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a529fe89fea243d932879a1a74e9d36a7">canonMultTerm1Term2</a>(const Expr &t1, const Expr &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#af6ba91fa47c4c9139c4d93fe3de0112f">canonMultTermConst</a>(const Expr &c, const Expr &t)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a55ec89d6cf310694e9f4b1013a795ce2">canonMultZero</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a41f7000c783a82e9a86cad823b06bff4">canonPlus</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#af673275ae1c3dc606b29979b60df35c5">canonPowConst</a>(const Expr &pow)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a4671174ae8ff61c52f16ddd53a3cdd27">canonUMinusToDivide</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ad4513630a9eec6c841b527222a79ea1d">clashingBounds</a>(const Theorem &lowerBound, const Theorem &upperBound)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ae43400e7e4c9e3695a75da3bd5718eda">compactNonLinearTerm</a>(const Expr &nonLinear)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a621015d4894231ecd9ab465494e9c9c8">constPredicate</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a529e92e59e9009e3330a8592c9cb56fe">constRHSGrayShadow</a>(const Rational &c, const Rational &b, const Rational &a)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a47a517c15b57ba19b7759a4ba925e306">create_t</a>(const Expr &eqn)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ab20380e74e431d9956c588d45d5121a4">create_t2</a>(const Expr &lhs, const Expr &rhs, const Expr &t)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a77e9c5681a02ab61f1311628e843d3db">create_t3</a>(const Expr &lhs, const Expr &rhs, const Expr &t)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a0111aa5645658dbd6a4bc030178edb94">cycleConflict</a>(const std::vector< Theorem > &inequalitites)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#a8b023af23ac984c27c8eae1f79fb1e2d">d_checkProofs</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#a1b706238281ad141a57363a6890f14a5">d_em</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#aee4a05e25306885dbaa6f67fc92f119d">d_hole</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#adcb2b6244c679d22b4a684fb39fd3558">d_pfOp</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ad2c70acba668e2582f0ebd9533646338">d_theoryArith</a></td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#a27015759e6bdfced928fc5a2d9877b7d">d_tm</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#aef6fd1261bea182d4554d0423803b05e">darkGrayShadow2ab</a>(const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#aaf64935bb620ab79fd7383f1913bd8b8">darkGrayShadow2ba</a>(const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a9dfab0a471e7a705264be04007ac61e5">darkShadow</a>(const Expr &lhs, const Expr &rhs)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a3d6e1d8668360c20b5a6a47e3fcc4612">diseqToIneq</a>(const Theorem &diseq)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#aa371616db9ac1a4a9c7a4b1ce0f2a05c">divideEqnNonConst</a>(const Expr &x, const Expr &y, const Expr &z)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a753c339b31e38915ae6f06e0fe6e48da">dummyTheorem</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a3c454b863142345e1093663fbb89d306">elimPower</a>(const Expr &expr)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a21456f49d3a6711f21e3c13fb3c0d34a">elimPowerConst</a>(const Expr &expr, const Rational &root)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a49d6559f50d51cde3c2e723c2a254cff">eqElimIntRule</a>(const Theorem &eqn, const Theorem &isIntx, const std::vector< Theorem > &isIntVars)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a517d45514aefcab0dc6aabb400f149fd">eqToIneq</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a512f22a4a025477ced8c27f3d62809d7">equalLeaves1</a>(const Theorem &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a77ae567431bf98e20cc08903deb2ec99">equalLeaves2</a>(const Theorem &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a8de6b6b44c60cf495b455b980a7c681b">equalLeaves3</a>(const Theorem &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a97768870957319cdc68eb94694a37dc5">equalLeaves4</a>(const Theorem &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#afbf059903de8b1e87aef9a4a75340d6c">evenPowerEqNegConst</a>(const Expr &expr)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#aafadfc6ae6013ab18a7b4ee570cce16a">expandDarkShadow</a>(const Theorem &darkShadow)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ac6714d4922aea3413f9aeed742bc645e">expandGrayShadow</a>(const Theorem &grayShadow)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ac8a2c0a97ace8f17153ad784c87ba5a2">expandGrayShadow0</a>(const Theorem &grayShadow)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#af091e13254c983370c46707a03b1ad30">expandGrayShadowConst</a>(const Theorem &grayShadow)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a84a9652acc5908e5d1ead5c54c1f2d90">expandGrayShadowRewrite</a>(const Expr &theShadow)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ad727620082aea32b487863ac5888eb1b">f</a>(const Rational &i, const Rational &m)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a7f4c82e18e7a3ed3b5b22a6ce7d7cf27">finiteInterval</a>(const Theorem &aLEt, const Theorem &tLEac, const Theorem &isInta, const Theorem &isIntt)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#af069fc1b320c0455ec7cde192668884b">flipInequality</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a1684298bef4bf1efdccb7078f5a6c96f">grayShadow</a>(const Expr &v, const Expr &e, const Rational &c1, const Rational &c2)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#af0070c5da95d33029e54b1d669d5b1f0">grayShadowConst</a>(const Theorem &g)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a23faa6b30e4b01d7540ac1e22e6e06ce">greaterthan</a>(const Expr &, const Expr &)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">static</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a45d8f89bdb0e57ddbaec273a24bf34b4">implyDiffLogicBothBounds</a>(const Expr &x, std::vector< Theorem > &c1_le_x, Rational c1, std::vector< Theorem > &x_le_c2, Rational c2)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#abb8aff055ea56ad8de2b66fd9a7aeba9">implyEqualities</a>(const std::vector< Theorem > &inequalities)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a1bf4d45330b587882e726daa9117cdfb">implyNegatedInequality</a>(const Expr &expr1, const Expr &expr2)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ab794c1f9d6e971ac56e0063f409b4774">implyNegatedInequalityDiffLogic</a>(const std::vector< Theorem > &antecedentThms, const Expr &implied)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a364ef37224bae3afb4f62a5c0f75d02c">implyWeakerInequality</a>(const Expr &expr1, const Expr &expr2)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ae3a7aa0ebe8e84b806efaa59278ea75e">implyWeakerInequalityDiffLogic</a>(const std::vector< Theorem > &antecedentThms, const Expr &implied)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ab9395a2ee958d70c780df2514e517320">integerSplit</a>(const Expr &intVar, const Rational &intPoint)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#aa3838fe1c003a9f47f3ec8344d192dea">intEqIrrational</a>(const Expr &expr, const Theorem &isInt)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ad5f121b6b7d6b8ae951dfb4cce064575">intEqualityRationalConstant</a>(const Theorem &isIntConstrThm, const Expr &constr)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a8b33391347e9741339b674abd5c4fbf2">intType</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a92936e3de514c430659486b00e84b0a9">intVarEqnConst</a>(const Expr &eqn, const Theorem &isIntx)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#af1baf70d6108dc52cbb9704e2a8889ec">isIntConst</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a85e9c7d93d6d1433fea606b0c3878e25">IsIntegerElim</a>(const Theorem &isIntx)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a8196042ba713a7c782ee4b5eb4c69ccc">leftMinusRight</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ac5d4056f00cee80d73b5b46f63bd5b3d">lessThanToLE</a>(const Theorem &less, const Theorem &isIntLHS, const Theorem &isIntRHS, bool changeRight)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#af55c5d0a2626f955b0843381ca8b50f3">lessThanToLERewrite</a>(const Expr &ineq, const Theorem &isIntLHS, const Theorem &isIntRHS, bool changeRight)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ab369e518fc2ee411503253fa0b1515d6">minusToPlus</a>(const Expr &x, const Expr &y)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a3cb8580c7627250ffe999de9a1b2c8c3">modEq</a>(const Rational &i, const Rational &m)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a69adf7d70a6a71e5c0e3489535a18108">monomialModM</a>(const Expr &e, const Rational &m, const Rational &divisor)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a41da83b4624daa43a84bc049b5b7d836">monomialMulF</a>(const Expr &e, const Rational &m, const Rational &divisor)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a77b99e94956d407e5cd20701e6771120">moveSumConstantRight</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ae66ddbc1457e3c032ea9059625059992">multEqn</a>(const Expr &x, const Expr &y, const Expr &z)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a0040d5d848f7040df940b92d95a75930">multEqZero</a>(const Expr &expr)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a3d245f36a2e42684ec2fd9356d89111f">multIneqn</a>(const Expr &e, const Expr &z)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a07368f8a2e12b5c189645a99bc934102">negatedInequality</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#ae6f0d46a632906b24cca2d5f648ae329">newAssumption</a>(const Expr &thm, const Proof &pf, int scope=-1)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#af4bdd16428b49f295b3d21208dffc0cd">newLabel</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(const std::string &name)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#a4dc7589f2361108f86ba9a39584225c8">newPf</a>(const std::string &name, const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#a4318ccfdb9a7476428b6bec10218b704">newPf</a>(const std::string &name, const Proof &pf)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#afde487055921fadaa010a98fcfec3efc">newPf</a>(const std::string &name, const Expr &e1, const Expr &e2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#ac8fe1de247e929400cdcf8abb05f51d8">newPf</a>(const std::string &name, const Expr &e, const Proof &pf)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#a4442d3e5b304a0d0c26a70f398605c2f">newPf</a>(const std::string &name, const Expr &e1, const Expr &e2, const Expr &e3)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#a9635508015efe3b1eee16c42c095d664">newPf</a>(const std::string &name, const Expr &e1, const Expr &e2, const Proof &pf)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#aea760a51b9c828ba13daabb8bb85a059">newPf</a>(const std::string &name, Expr::iterator begin, const Expr::iterator &end)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#a64af41f02b0a09e641ddfee381dec928">newPf</a>(const std::string &name, const Expr &e, Expr::iterator begin, const Expr::iterator &end)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#a19abffed968792730fc45001a78e2f29">newPf</a>(const std::string &name, Expr::iterator begin, const Expr::iterator &end, const std::vector< Proof > &pfs)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#afbc79087033fcd7a9c14faca4fee9d34">newPf</a>(const std::string &name, const std::vector< Expr > &args)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#a8748ea26e91b5d0046ba28ffaa085935">newPf</a>(const std::string &name, const Expr &e, const std::vector< Expr > &args)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#a9620645731b7d636c5988319d2b02513">newPf</a>(const std::string &name, const Expr &e, const std::vector< Proof > &pfs)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#a9dd3b2ab2d8230f47795e65d2c48fb04">newPf</a>(const std::string &name, const Expr &e1, const Expr &e2, const std::vector< Proof > &pfs)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#ac8ad8684a67b13b361a8569d825b2098">newPf</a>(const std::string &name, const std::vector< Proof > &pfs)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#a241ecbd26413d976be8cc1d34f7f93e2">newPf</a>(const std::string &name, const std::vector< Expr > &args, const Proof &pf)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#ac903fe293131f805c477a7830956de9a">newPf</a>(const std::string &name, const std::vector< Expr > &args, const std::vector< Proof > &pfs)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#a5703a2ebdbed3225aa886e4476c683ec">newPf</a>(const Proof &label, const Expr &frm, const Proof &pf)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#ab928d4883eab42df337ce09447c49702">newPf</a>(const Proof &label, const Proof &pf)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#aad2d702b1e1a7e024d1068cbde1b8d77">newPf</a>(const std::vector< Proof > &labels, const std::vector< Expr > &frms, const Proof &pf)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#abe7fac97b88de3346898e955456adc75">newPf</a>(const std::vector< Proof > &labels, const Proof &pf)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#a0670b7f9cfb6e1420227b5df652d6e79">newReflTheorem</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#a1b12639479f7d06736c643d43d714e90">newRWTheorem</a>(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#aaaca425811ff3137c21a040a8ce1b69e">newRWTheorem3</a>(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89">newTheorem</a>(const Expr &thm, const Assumptions &assump, const Proof &pf)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#aec0760db9fcf381bf3886dbb1801662d">newTheorem3</a>(const Expr &thm, const Assumptions &assump, const Proof &pf)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a9edd8b9ee6a8b4d14e9a2f967b78d52f">nonLinearIneqSignSplit</a>(const Theorem &ineqThm)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a23051d23d509f9cda35c64d4a5ff1dbf">oneElimination</a>(const Expr &x)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a3c3041eb3b0144e21d72ffe6999953e2">plusPredicate</a>(const Expr &x, const Expr &y, const Expr &z, int kind)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a9cd618abf322c0389f1fc40f274059c2">powEqZero</a>(const Expr &expr)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a0433b1ba53a33275015c26450acb09d0">powerOfOne</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a4b28aa17702ca3f9703e61ca012ca236">rafineStrictInteger</a>(const Theorem &isIntConstrThm, const Expr &constr)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ae0d46b17ef012eabbbe62cac026bfab9">rat</a>(Rational r)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a8092c96a87d952fc1e572bb9237ff994">realShadow</a>(const Theorem &alphaLTt, const Theorem &tLTbeta)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a6e14251c516153e14539a34598daca04">realShadowEq</a>(const Theorem &alphaLEt, const Theorem &tLEalpha)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a4606a94098ae94cdae1b924dc7f7b4ae">realType</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithProofRules.html#a81d9ea1e5c2d42c2b60a893c879145bd">rewriteLeavesConst</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a3eb1309c184247837239c098d9c9100a">rightMinusLeft</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#afd5bca9b136254b904b931680180ac83">simpleIneqInt</a>(const Expr &ineq, const Theorem &isIntRHS)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#af24b2bc3bc03bc320707362f2460dd0e">simplifiedMultExpr</a>(std::vector< Expr > &mulKids)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#a8f74c8badd61cf70ebeb05183c00d608">soundError</a>(const std::string &file, int line, const std::string &cond, const std::string &msg)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a14af8b5ecbfaaee4600453bd9d681838">splitGrayShadow</a>(const Theorem &grayShadow)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#acaa835c8569f6667fa26bfedb0502cf1">splitGrayShadowSmall</a>(const Theorem &grayShadow)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a073ec1476668043be44ae96519eae36d">substitute</a>(const Expr &term, ExprMap< Expr > &eMap)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a10c569edc893a67b42af659633b3f20d">sumModM</a>(std::vector< Expr > &summands, const Expr &sum, const Rational &m, const Rational &divisor)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a32e61136df79a76fe1ed853ee6b8dc2e">sumMulF</a>(std::vector< Expr > &summands, const Expr &sum, const Rational &m, const Rational &divisor)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#a5b69feb3bf1ce90107295b5731f847d7">TheoremProducer</a>(TheoremManager *tm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a43fa5f7c8c3ad3915de7f068ac8cefbd">trustedRewrite</a>(const Expr &expr1, const Expr &expr2)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#aaafdbe9dcc49728cc2bf16b43045c193">uMinusToMult</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a7568925b6c26f1c7ba882893f596d214">varToMult</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1ArithTheoremProducer.html">CVC3::ArithTheoremProducer</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#a32afe6d99e661b5c70082036e40d48bc">withAssumptions</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a">withProof</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ArithProofRules.html#a410c697fc050feca9680a388397b0968">~ArithProofRules</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html#ae21722ca8449f4480e01566982cd4d61">~TheoremProducer</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</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>
