<!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_1ArithProofRules.html">ArithProofRules</a> </li>
</ul>
</div>
</div>
<div class="header">
<div class="headertitle">
<div class="title">CVC3::ArithProofRules Member List</div> </div>
</div>
<div class="contents">
This is the complete list of members for <a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a>, including all inherited members.<table>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#ac06dd83948d0f3e474f073ecac592343">addInequalities</a>(const Theorem &thm1, const Theorem &thm2)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#ab87b1e3a09aa830063d51c24a2147095">addInequalities</a>(const std::vector< Theorem > &thms)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a1da0c47c02ff2392ca3e0b6493ac4823">canonComboLikeTerms</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a198b0b44145b8e33555ffd212f43b7b3">canonDivide</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a79c759f2bb7dc41ed98c5962febef804">canonDivideConst</a>(const Expr &c, const Expr &d)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#aee487a2a1e8ce4c34075568eb70ea874">canonDivideMult</a>(const Expr &cx, const Expr &d)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a92846ee0cdab98d1759a13ff7e8d710d">canonDividePlus</a>(const Expr &e, const Expr &d)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a4ab0351b340ecb82d6ced530e4f30510">canonDivideVar</a>(const Expr &e, const Expr &d)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#af0f4877d7326a53faec76bef54a3d400">canonFlattenSum</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a9a806d487932bbfa9a019d4d1eed1cea">canonInvert</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#aca910e6ff44389aac100b14b486c1942">canonMult</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a71be38a9fa2d89e147ac4fde35c49e21">canonMultConstConst</a>(const Expr &c1, const Expr &c2)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a978068749de266dbbba2000d9e0c3d39">canonMultConstSum</a>(const Expr &c1, const Expr &sum)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a96b1cb83272cf80c2de663de429e6a15">canonMultConstTerm</a>(const Expr &c1, const Expr &c2, const Expr &t)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#aa38d5c06ebe0b672570641fe933cfedb">canonMultMtermMterm</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a87f9a39ecb1bec46adff5187bc899726">canonMultOne</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a8b9abf99f0b013714eaaa49e81a618b9">canonMultTerm1Term2</a>(const Expr &t1, const Expr &t2)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a11870b90dbfcc61d2b9a2820df7f6057">canonMultTermConst</a>(const Expr &c, const Expr &t)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#aae559b4d1558fecba5621c9ba27daa88">canonMultZero</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a225fe511e6f654f313048e86c1550510">canonPlus</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a999f13a6fa4a6d8cbe97f02f93fc9ed3">canonPowConst</a>(const Expr &pow)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a0053398d4a8fc49d9a2f8ede6949fc70">canonUMinusToDivide</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#ad0b23fb01a7adea349c8958059b9f7fd">clashingBounds</a>(const Theorem &lowerBound, const Theorem &upperBound)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a98020e790bcb60c9c2cc5a7e406f500f">compactNonLinearTerm</a>(const Expr &nonLinear)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a8dd6bb6fed9a4745469b0cad5ed4a139">constPredicate</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a5a544980652c3f6793057b16cbc43cf9">cycleConflict</a>(const std::vector< Theorem > &inequalitites)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a37835b10dd0f73b5c4cf36c1eebf0d1f">darkGrayShadow2ab</a>(const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#ab17282c2e4de9965586f4821f17bf60d">darkGrayShadow2ba</a>(const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#af180898d9f1d255ef3a2f528ecd8ac65">diseqToIneq</a>(const Theorem &diseq)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a419dd84177b5ca1fda7a23f3052b6132">divideEqnNonConst</a>(const Expr &x, const Expr &y, const Expr &z)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a24ea340651805e648d7180debad17225">dummyTheorem</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a0e6f19ba5333f667efa3a0e3d8787775">elimPower</a>(const Expr &expr)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a0e240fba4eac33522b24be6581d98346">elimPowerConst</a>(const Expr &expr, const Rational &root)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a08b14a730bbc6b4ca28bb808e6f6dc85">eqElimIntRule</a>(const Theorem &eqn, const Theorem &isIntx, const std::vector< Theorem > &isIntVars)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a646e312e12d5d23dca0c4db39d2c9fb9">eqToIneq</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#ac05fd3606540a5222ebaa68f9091345b">equalLeaves1</a>(const Theorem &thm)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a5052c783af25243987424ef66e2bf5fc">equalLeaves2</a>(const Theorem &thm)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a893c86f0404789d229540f7a0a00df89">equalLeaves3</a>(const Theorem &thm)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#aa9018c4d16d3d0a2d8f1614f8e7cae23">equalLeaves4</a>(const Theorem &thm)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a80f948f405f0b1a88283c97b70aab43e">evenPowerEqNegConst</a>(const Expr &expr)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a94ffe313b29aa63c32d5c3facb3bc917">expandDarkShadow</a>(const Theorem &darkShadow)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#af936b764ef75b0a6f63043d01a819044">expandGrayShadow</a>(const Theorem &g)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a32df170ed2ec7fb3d1c7541e6f3dda77">expandGrayShadow0</a>(const Theorem &g)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a3083a3c5893123f2a3ec54ce31718e09">expandGrayShadowConst</a>(const Theorem &g)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#ac48d6f8b2ad8e8f8fefac775d33825b5">expandGrayShadowRewrite</a>(const Expr &theShadow)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a5d419e48b93820624e356ba33efef27c">finiteInterval</a>(const Theorem &aLEt, const Theorem &tLEac, const Theorem &isInta, const Theorem &isIntt)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#aff4a01da77770b0b60089444c83c9cef">flipInequality</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a597adbe8879c33bffefae537a5bca7c0">grayShadowConst</a>(const Theorem &g)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#af80ad28bb01d8a37e32f29c746d22dbc">implyDiffLogicBothBounds</a>(const Expr &x, std::vector< Theorem > &c1_le_x, Rational c1, std::vector< Theorem > &x_le_c2, Rational c2)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a5b475214a53d70298e55f4ac5f3db71f">implyEqualities</a>(const std::vector< Theorem > &inequalities)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a5eaf4d106f7ce86227ab1d96ffc66b55">implyNegatedInequality</a>(const Expr &expr1, const Expr &expr2)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a61ecf1cfc7219c010519cd90cb31d465">implyNegatedInequalityDiffLogic</a>(const std::vector< Theorem > &antecedentThms, const Expr &implied)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a9abe85f95b61d94fa308a0b15f2b2ef8">implyWeakerInequality</a>(const Expr &expr1, const Expr &expr2)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#aafc12b4bdf180f3475ecf4eaa40648d9">implyWeakerInequalityDiffLogic</a>(const std::vector< Theorem > &antecedentThms, const Expr &implied)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a0090e0d4065efbf936ec92f0e99935e9">integerSplit</a>(const Expr &intVar, const Rational &intPoint)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#aff57d78a7d743fffd21de7d4415df3e4">intEqIrrational</a>(const Expr &expr, const Theorem &isInt)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a93489420e882a93eb308c7d99c27dc1e">intEqualityRationalConstant</a>(const Theorem &isIntConstrThm, const Expr &constr)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a62d76b2ccca8af5e1f28c5104ea2e313">intVarEqnConst</a>(const Expr &eqn, const Theorem &isIntx)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a5e9bccd77000156ab34b0b42d3e3bb18">isIntConst</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a8c3d5fdc2b0c9c11291d41c3c20067e4">IsIntegerElim</a>(const Theorem &isIntx)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a0201544f06baaba23df9946f5da47978">leftMinusRight</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a7a0dad5cb9c2815421457dabc25bc537">lessThanToLE</a>(const Theorem &less, const Theorem &isIntLHS, const Theorem &isIntRHS, bool changeRight)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#af5cfb693ee5ee6f3463e83f01196b31e">lessThanToLERewrite</a>(const Expr &ineq, const Theorem &isIntLHS, const Theorem &isIntRHS, bool changeRight)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a4319c532082c0f43794b34a2fb9df73f">minusToPlus</a>(const Expr &x, const Expr &y)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a18e5970bc4f670a63ca5775750f099ab">moveSumConstantRight</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#ad62d795eb10e67c655c608774881bde3">multEqn</a>(const Expr &x, const Expr &y, const Expr &z)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#af8f4f59bd12fdd8f93d1fd49ae41279e">multEqZero</a>(const Expr &expr)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a70e83cfbc207a5d15fedd4adde7e9e76">multIneqn</a>(const Expr &e, const Expr &z)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#aee47bda46999143ea29d7d4ff0be89d4">negatedInequality</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#aa6874fa9f5b02db0adb8149af9664b05">nonLinearIneqSignSplit</a>(const Theorem &ineqThm)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a1ebae10d65430ab1a3a14c866af93de6">oneElimination</a>(const Expr &x)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a0fa920a2a5cfa4419dbde10b1d913687">plusPredicate</a>(const Expr &x, const Expr &y, const Expr &z, int kind)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#af17a5dbf4ebbe9d7e46d63ad1284ddaf">powEqZero</a>(const Expr &expr)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#ad3dee93f4078a4fc79ccacef33f05119">powerOfOne</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a4b61e3ea9d5ac911806de95241cf35de">rafineStrictInteger</a>(const Theorem &isIntConstrThm, const Expr &constr)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a203c7079289189cd4bf4f604c10645e5">realShadow</a>(const Theorem &alphaLTt, const Theorem &tLTbeta)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a08dfccc28787af2a4141ed0f5a66bc9d">realShadowEq</a>(const Theorem &alphaLEt, const Theorem &tLEalpha)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</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_1ArithProofRules.html#acde77bf4aa73ff6b9a079b372ed7cc51">rightMinusLeft</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a95bc88d9e126e6b9c938691ce92985aa">simpleIneqInt</a>(const Expr &ineq, const Theorem &isIntRHS)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a4b6ef5b29b05bada6ea2df72873abea6">splitGrayShadow</a>(const Theorem &g)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#aa33975feef2a9cdd513e5d641f14dc7a">splitGrayShadowSmall</a>(const Theorem &g)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a11976de555ee2e88236575893f2ed766">trustedRewrite</a>(const Expr &expr1, const Expr &expr2)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#aa95faca93e7b4a1cf21667ff88d390e4">uMinusToMult</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ArithProofRules.html#a8b8db5ad0a8d4968f429e98964db93c1">varToMult</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1ArithProofRules.html">CVC3::ArithProofRules</a></td><td><code> [pure virtual]</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>
</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>
