<!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: Member List</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_1ArithTheoremProducer3.html">ArithTheoremProducer3</a> </li>
</ul>
</div>
</div>
<div class="header">
<div class="headertitle">
<div class="title">CVC3::ArithTheoremProducer3 Member List</div> </div>
</div>
<div class="contents">
This is the complete list of members for <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a>, including all inherited members.<table>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a301d62f207b9cfd50096417d1f5852df">addInequalities</a>(const Theorem &thm1, const Theorem &thm2)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aa2d099917106ead1062c72dde26a17a5">addInequalities</a>(const std::vector< Theorem > &thms)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a56fb5871062ffe12510c4cd4ba65b745">ArithTheoremProducer3</a>(TheoremManager *tm, TheoryArith3 *theoryArith)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#af61545eb36910fba4fa1b69e6febb354">canonCombineLikeTerms</a>(const std::vector< Expr > &sumExprs)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a245f64776d0b1fbd14d18bb145f717e4">canonComboLikeTerms</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#acfe4060947cb28e9fc9c4ea859df565c">canonDivide</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a3a2bf5e3b8c71543b1512f1606825a02">canonDivideConst</a>(const Expr &c, const Expr &d)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a39a2efadcc13383fd860340c6d76db54">canonDivideMult</a>(const Expr &cx, const Expr &d)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a897c950b6bb741189f1c33752159b587">canonDividePlus</a>(const Expr &e, const Expr &d)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a9fddb49ed54796e6a5487be554eb14f4">canonDivideVar</a>(const Expr &e1, const Expr &e2)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a5ec4889e730c0b1d4fb584d16af08a9d">canonFlattenSum</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a1a4b78b01763b1ca5a80c0211bc3ba4b">canonInvert</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#addd3884d42a6e4637e9bda79d4af6574">canonInvertConst</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a84b1ec96629fa2ae52792a582ba7a63a">canonInvertLeaf</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a94090722e5ab797e97cdb14458c40742">canonInvertMult</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a02b89064723281b69105ce11ecaf80c7">canonInvertPow</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a627a219305f83b200e36b28b1865729a">canonMult</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a4ea3884dff8c1606fd05e61eb78e379d">canonMultConstConst</a>(const Expr &c1, const Expr &c2)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ad49508debdf58df9d8333cd140c850a3">canonMultConstMult</a>(const Expr &c, const Expr &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a747b71c44a0bad76328039a2fc123363">canonMultConstPlus</a>(const Expr &e1, const Expr &e2)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a2765c1485aac81cc42ed3186f7a1f244">canonMultConstSum</a>(const Expr &c1, const Expr &sum)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a9e5b7c75f1f662071942150df1a4d69e">canonMultConstTerm</a>(const Expr &c1, const Expr &c2, const Expr &t)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ad9ff33794685a95c453d41bf1fd9d0aa">canonMultLeafLeaf</a>(const Expr &e1, const Expr &e2)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a9bf1d7c7d567deab2e5decc8c4e82fdc">canonMultLeafOrPowMult</a>(const Expr &e1, const Expr &e2)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ad5dec14920bc52be7b9fdfb458ba2e1b">canonMultLeafOrPowOrMultPlus</a>(const Expr &e1, const Expr &e2)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aa1ab000ca8a6a2605b2cb57f8b881d91">canonMultMtermMterm</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aed0a2d1337910f3027ac867e0f18b8de">canonMultOne</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ab327e6f313e952c0380fe7460bd7d36c">canonMultPlusPlus</a>(const Expr &e1, const Expr &e2)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a1765748e34d12d99b3bdf57f3ba49d49">canonMultPowLeaf</a>(const Expr &e1, const Expr &e2)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ae709408bffa6ff2016619a05febe63f5">canonMultPowPow</a>(const Expr &e1, const Expr &e2)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a294916be1e9ac30e3c824b0b8e4ff093">canonMultTerm1Term2</a>(const Expr &t1, const Expr &t2)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a401fca0c453a94c8c0053eb77e014af0">canonMultTermConst</a>(const Expr &c, const Expr &t)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a55fb07d5df2b4068bf5df327ae0d89d4">canonMultZero</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#acbd2c2b8d5a0728aa00dcf55c7c646f2">canonPlus</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a5347a8208d4d7aa05fad463bd6da8c41">canonPowConst</a>(const Expr &pow)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a9bf439248afb24bb63ea435193b68524">canonUMinusToDivide</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#af05299dbe2defe9679365201cd60c516">clashingBounds</a>(const Theorem &lowerBound, const Theorem &upperBound)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aac90a712f81d969d8aa0322b4d31de0b">compactNonLinearTerm</a>(const Expr &nonLinear)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a7a2a8059fa49da5a8877b28b1cfa445a">constPredicate</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#afa3e14a6cb004a107d915df0088ed16c">constRHSGrayShadow</a>(const Rational &c, const Rational &b, const Rational &a)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ab70323686fd8775952a2709a6c8c754b">create_t</a>(const Expr &eqn)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#adf974179ea62c2196a87fb9c2199f6cd">create_t2</a>(const Expr &lhs, const Expr &rhs, const Expr &t)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a6bad08f3833720448803251dfa234e36">create_t3</a>(const Expr &lhs, const Expr &rhs, const Expr &t)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a5411413ef39cb6029a8e85fc03908de3">cycleConflict</a>(const std::vector< Theorem > &inequalitites)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoremProducer.html#a8b023af23ac984c27c8eae1f79fb1e2d">d_checkProofs</a></td><td><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoremProducer.html#a1b706238281ad141a57363a6890f14a5">d_em</a></td><td><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoremProducer.html#aee4a05e25306885dbaa6f67fc92f119d">d_hole</a></td><td><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoremProducer.html#adcb2b6244c679d22b4a684fb39fd3558">d_pfOp</a></td><td><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a75321b2dd304a716364b64d21ebf3d07">d_theoryArith</a></td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoremProducer.html#a27015759e6bdfced928fc5a2d9877b7d">d_tm</a></td><td><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a2ad479414c401fb8a4ea9631cbdd95c0">darkGrayShadow2ab</a>(const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a8b2e8589d24fc69616ba431588c50b3e">darkGrayShadow2ba</a>(const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#afe495b6c58dd0c89c84b64c5194eeeaa">darkShadow</a>(const Expr &lhs, const Expr &rhs)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a20fdbcbe80fa06a175aae548af7d2519">diseqToIneq</a>(const Theorem &diseq)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a7bf31f4d4bd6e3f7ff7e37dd5236a792">divideEqnNonConst</a>(const Expr &x, const Expr &y, const Expr &z)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ae1e994559a2318ec45a758042371a71d">dummyTheorem</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ab29b63e40b7f2c624e6e4f11c4eff27e">elimPower</a>(const Expr &expr)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a942f9f0fc0ceff798b607e9fe032175a">elimPowerConst</a>(const Expr &expr, const Rational &root)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a1f5430f425efc533ca5881aaaeb42554">eqElimIntRule</a>(const Theorem &eqn, const Theorem &isIntx, const std::vector< Theorem > &isIntVars)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ad2f144d3a2ffe108e0d8e7df8e263832">eqToIneq</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#acb64cdcb59f042dd38a9bf9b70f043ad">equalLeaves1</a>(const Theorem &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ae97e571a8d541a31aef5c1c703190437">equalLeaves2</a>(const Theorem &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aba1a7d51f8b8291c30cc32c0f3ff5a4d">equalLeaves3</a>(const Theorem &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a5876760c9171eca18490c779cc2bbc73">equalLeaves4</a>(const Theorem &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#abe913a6cc9430faf8f0ac50ec51aa36c">evenPowerEqNegConst</a>(const Expr &expr)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a372efa694fb08c901deff55f5f108ffb">expandDarkShadow</a>(const Theorem &darkShadow)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ab9dd38464b6e02af6d7c570119c6aec3">expandGrayShadow</a>(const Theorem &grayShadow)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aacc831490c52da277133fe625522216f">expandGrayShadow0</a>(const Theorem &grayShadow)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a43d1cf15faefe439c344508bf60e5e96">expandGrayShadowConst</a>(const Theorem &grayShadow)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aa9b6fa1339b7e68cb730bdf2f63c0914">expandGrayShadowRewrite</a>(const Expr &theShadow)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a077f8d0dab986b01d390668f6af1afa2">f</a>(const Rational &i, const Rational &m)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aaba7798eb77a93ac0de8978507dca731">finiteInterval</a>(const Theorem &aLEt, const Theorem &tLEac, const Theorem &isInta, const Theorem &isIntt)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a216a950228aad3cdef0c5dd5213be4fb">flipInequality</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ab34039c1fcdbf7701cd0541dce2575c8">grayShadow</a>(const Expr &v, const Expr &e, const Rational &c1, const Rational &c2)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a0a5eb9028805dd1ee141713b7c70be77">grayShadowConst</a>(const Theorem &g)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a1923e590a205cefe9ef50d336e99c9e5">greaterthan</a>(const Expr &, const Expr &)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [static]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a9edd45196fbd8e61a4927134fde15e97">implyDiffLogicBothBounds</a>(const Expr &x, std::vector< Theorem > &c1_le_x, Rational c1, std::vector< Theorem > &x_le_c2, Rational c2)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a1efa679a45d71f60bf2be6f4f7a4430d">implyEqualities</a>(const std::vector< Theorem > &inequalities)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a1797b422d1100edc2464666121d7017b">implyNegatedInequality</a>(const Expr &expr1, const Expr &expr2)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a6ef98983cca8d3723f50fbea60c37cef">implyNegatedInequalityDiffLogic</a>(const std::vector< Theorem > &antecedentThms, const Expr &implied)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ae856ca9fab9699b655d7fd76cdf778d4">implyWeakerInequality</a>(const Expr &expr1, const Expr &expr2)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a8e90a0d0e2050a7f0eb1dde6df7f6842">implyWeakerInequalityDiffLogic</a>(const std::vector< Theorem > &antecedentThms, const Expr &implied)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ae25218af53e642382f30948adc991313">integerSplit</a>(const Expr &intVar, const Rational &intPoint)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a946832931094bb746277d8b95c471690">intEqIrrational</a>(const Expr &expr, const Theorem &isInt)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a84ec7197bec26c33753e98b6adf55dce">intEqualityRationalConstant</a>(const Theorem &isIntConstrThm, const Expr &constr)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a04f5df44759216fd1182bd745cfc6a82">intType</a>()</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a608b3a7da8f2824d3cc8188d7606396e">intVarEqnConst</a>(const Expr &eqn, const Theorem &isIntx)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a24216d1be10b57272b918ba416783b76">isIntConst</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ad2438a34ff1edb7268495d4105cb6c9c">IsIntegerElim</a>(const Theorem &isIntx)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aedad2be1c60515921f8c3761581afca5">leftMinusRight</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a91447c7423622c037a2956114fd549f4">lessThanToLE</a>(const Theorem &less, const Theorem &isIntLHS, const Theorem &isIntRHS, bool changeRight)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a55c056040dc960b598706a94650acccb">lessThanToLERewrite</a>(const Expr &ineq, const Theorem &isIntLHS, const Theorem &isIntRHS, bool changeRight)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ab0d610d377cc20e3ce16823713d25403">minusToPlus</a>(const Expr &x, const Expr &y)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ada3b48ce9720177b4a427237efe0453f">modEq</a>(const Rational &i, const Rational &m)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a5245a34c6f9e903db87e17df1d33c09d">monomialModM</a>(const Expr &e, const Rational &m, const Rational &divisor)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aea07da55e987ccd27d0f57e08558af01">monomialMulF</a>(const Expr &e, const Rational &m, const Rational &divisor)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aad289f36b55fe8be7f7af0f62aedaae8">moveSumConstantRight</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#afd7a6da45999fb3237cdbbbf9c5f19e8">multEqn</a>(const Expr &x, const Expr &y, const Expr &z)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a57eafe7c2a127ca4b4706437b777d610">multEqZero</a>(const Expr &expr)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a8af6455fe4a8889cfb7b0b8c865b847c">multIneqn</a>(const Expr &e, const Expr &z)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a27bb939c33616b21a83aabdb5d47a660">negatedInequality</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoremProducer.html#ae6f0d46a632906b24cca2d5f648ae329">newAssumption</a>(const Expr &thm, const Proof &pf, int scope=-1)</td><td><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td><code> [inline, protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoremProducer.html#af4bdd16428b49f295b3d21208dffc0cd">newLabel</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(const std::string &name)</td><td><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoremProducer.html#a4dc7589f2361108f86ba9a39584225c8">newPf</a>(const std::string &name, const Expr &e)</td><td><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoremProducer.html#a4318ccfdb9a7476428b6bec10218b704">newPf</a>(const std::string &name, const Proof &pf)</td><td><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoremProducer.html#afde487055921fadaa010a98fcfec3efc">newPf</a>(const std::string &name, const Expr &e1, const Expr &e2)</td><td><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoremProducer.html#ac8fe1de247e929400cdcf8abb05f51d8">newPf</a>(const std::string &name, const Expr &e, const Proof &pf)</td><td><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td></td></tr>
<tr class="memlist"><td><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><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td></td></tr>
<tr class="memlist"><td><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><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoremProducer.html#aea760a51b9c828ba13daabb8bb85a059">newPf</a>(const std::string &name, Expr::iterator begin, const Expr::iterator &end)</td><td><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td></td></tr>
<tr class="memlist"><td><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><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td></td></tr>
<tr class="memlist"><td><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><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoremProducer.html#afbc79087033fcd7a9c14faca4fee9d34">newPf</a>(const std::string &name, const std::vector< Expr > &args)</td><td><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td></td></tr>
<tr class="memlist"><td><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><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td></td></tr>
<tr class="memlist"><td><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><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td></td></tr>
<tr class="memlist"><td><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><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoremProducer.html#ac8ad8684a67b13b361a8569d825b2098">newPf</a>(const std::string &name, const std::vector< Proof > &pfs)</td><td><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td></td></tr>
<tr class="memlist"><td><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><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td></td></tr>
<tr class="memlist"><td><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><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoremProducer.html#a5703a2ebdbed3225aa886e4476c683ec">newPf</a>(const Proof &label, const Expr &frm, const Proof &pf)</td><td><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoremProducer.html#ab928d4883eab42df337ce09447c49702">newPf</a>(const Proof &label, const Proof &pf)</td><td><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td></td></tr>
<tr class="memlist"><td><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><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoremProducer.html#abe7fac97b88de3346898e955456adc75">newPf</a>(const std::vector< Proof > &labels, const Proof &pf)</td><td><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoremProducer.html#a0670b7f9cfb6e1420227b5df652d6e79">newReflTheorem</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td><code> [inline, protected]</code></td></tr>
<tr class="memlist"><td><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><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td><code> [inline, protected]</code></td></tr>
<tr class="memlist"><td><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><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td><code> [inline, protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89">newTheorem</a>(const Expr &thm, const Assumptions &assump, const Proof &pf)</td><td><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td><code> [inline, protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoremProducer.html#aec0760db9fcf381bf3886dbb1801662d">newTheorem3</a>(const Expr &thm, const Assumptions &assump, const Proof &pf)</td><td><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td><code> [inline, protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aaa91789edbf7fb936789379dd15a3a4f">nonLinearIneqSignSplit</a>(const Theorem &ineqThm)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a2caebbed8d00af9c80195413ed2cc568">oneElimination</a>(const Expr &x)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ab190e4d8fefb74f2a8117ca17ae49b48">plusPredicate</a>(const Expr &x, const Expr &y, const Expr &z, int kind)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#acbea7826fe54b91e8d4bc2c21f7137ae">powEqZero</a>(const Expr &expr)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#abf49b0eeb6087702dd1a8e9c03f7379a">powerOfOne</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a7638b18d73c05e7bedad7c4cdfeca809">rafineStrictInteger</a>(const Theorem &isIntConstrThm, const Expr &constr)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a4440979f29e7ec3519212ff1e23d758f">rat</a>(Rational r)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a6f08ce700f85f9ba2967ecee42e7a550">realShadow</a>(const Theorem &alphaLTt, const Theorem &tLTbeta)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a955e74558aee9ebc9de4c084819e93ac">realShadowEq</a>(const Theorem &alphaLEt, const Theorem &tLEalpha)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ad010c33575ebd1dc229c2a1526c229c5">realType</a>()</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a81d9ea1e5c2d42c2b60a893c879145bd">rewriteLeavesConst</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aca76a2dbee73d7ad9e2529ac8ce142a4">rightMinusLeft</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a6fe0e5ebaf81278f55759fff05c275c1">simpleIneqInt</a>(const Expr &ineq, const Theorem &isIntRHS)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aea589889127864f327d4d71800f096b7">simplifiedMultExpr</a>(std::vector< Expr > &mulKids)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><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><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ae609e58a7bee454d0f18dc1465cd2167">splitGrayShadow</a>(const Theorem &grayShadow)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aab0ccd490624628fa990b1dd473e7e8a">splitGrayShadowSmall</a>(const Theorem &grayShadow)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a3d0129d121975b0141d77ba6f458c182">substitute</a>(const Expr &term, ExprMap< Expr > &eMap)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aa21c4aa75f54e05bdc772b0e2d37b669">sumModM</a>(std::vector< Expr > &summands, const Expr &sum, const Rational &m, const Rational &divisor)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a36838065b24c16503ef6cf8164de44a8">sumMulF</a>(std::vector< Expr > &summands, const Expr &sum, const Rational &m, const Rational &divisor)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoremProducer.html#a5b69feb3bf1ce90107295b5731f847d7">TheoremProducer</a>(TheoremManager *tm)</td><td><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ad58ee7b299de278620860c9d67a2662b">trustedRewrite</a>(const Expr &expr1, const Expr &expr2)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a878e091ad5cfd2877ddce73d6f664e16">uMinusToMult</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a23340f90880cb869fdcfe6e69a7a2631">varToMult</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1ArithTheoremProducer3.html">CVC3::ArithTheoremProducer3</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoremProducer.html#a32afe6d99e661b5c70082036e40d48bc">withAssumptions</a>()</td><td><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a">withProof</a>()</td><td><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a410c697fc050feca9680a388397b0968">~ArithProofRules</a>()</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [inline, virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoremProducer.html#ae21722ca8449f4480e01566982cd4d61">~TheoremProducer</a>()</td><td><a class="el" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a></td><td><code> [inline, virtual]</code></td></tr>
</table></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>
