<!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_1TheoryArithNew.html">TheoryArithNew</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="headertitle">
<div class="title">CVC3::TheoryArithNew Member List</div> </div>
</div><!--header-->
<div class="contents">
<p>This is the complete list of members for <a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a>, including all inherited members.</p>
<table class="directory">
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a13ba9024a22362cc96760519a84f2316">addBoundVar</a>(const std::string &name, const Type &type)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#aa8f3f9fb084f9d5e385255baab5dc8f3">addBoundVar</a>(const std::string &name, const Type &type, const Expr &def)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a688cd0c0b669ab9719f8a99cb207ad2c">addGlobalLemma</a>(const Theorem &thm, int priority=0)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a5402887425b9a029f2ae0718c5012cb2">addInequalities</a>(const Theorem &le_1, const Theorem &le_2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html#a7491e5568f08eb89f9e801fccbd94b3e">addMultiplicativeSignSplit</a>(const Theorem &case_split_thm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html">CVC3::TheoryArith</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html#a9c7006698172a267cd3b138baf5ad5a9">addPairToArithOrder</a>(const Expr &smaller, const Expr &bigger)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html">CVC3::TheoryArith</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_1TheoryArithNew.html#a73bfa7842e5dfb1bbcf540b6a0ce49c8">addSharedTerm</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a605e960d2442b587046c562723b7f03a">addSplitter</a>(const Expr &e, int priority=0)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a4aa91ab5d33db7fbcaf1eb5e327f64f9">addToBuffer</a>(const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ae72d6b44b420d4acb2935c00d0b01fec">allBounds</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a7ff415cf3c90ddb60ff436d4b0b4c04b">assertedExpr</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a74dc050dee06beacca0e7e32b4585ec0">assertedExprCount</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ace140a37ea260f769f4aa2756e5f22f0">assertEqual</a>(const Expr &x_i, const EpsRational &c, const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a135cfab97004ee025a7840d72b6c4e1d">assertEqualities</a>(const Theorem &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ad083c5101196d8ea5aecf48dc00a9341">assertFact</a>(const Theorem &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#aa17423f3ce290e28544a356f0977f6f8">assertLower</a>(const Expr &x_i, const EpsRational &c, const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="group__Theory__API.html#ga4ce2fe1baec76fcb6120bbd86623ecd2">assertTypePred</a>(const Expr &e, const Theorem &pred)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a344feb254ed4f336fc0dc41a66cf232c">assertUpper</a>(const Expr &x_i, const EpsRational &c, const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a917b117d28514f486b296568fcd1cfd1">assignValue</a>(const Expr &t, const Expr &val)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a4a9cda0b7c7b2fd0874e7d7b9819a68f">assignValue</a>(const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ac327959d7f9b67467862643c33ff89c1">assignVariables</a>(std::vector< Expr > &v)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ab75b8a7b5960850c91a39c7713fb2477">beta</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a705d998884ec8a53c22220373472d868">boolType</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a2a34551a41e235972300cd849314c472">BoundInfoSet</a> typedef</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#acbfcb4d92182bdf9e185661ec0fc61e0">boundsAsString</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a453194ac83f105514a4d95fca44bd08e">canon</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a1e1a47d2be625ad62ac79da63678dc26">canonConjunctionEquiv</a>(const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a48756ab6f45691b827fc4e5545651778">canonPred</a>(const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a18e20adf514c858e9cfeb535e545fb06">canonPredEquiv</a>(const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html#a646f9972679d4465ba9ff7430cda9268">canonRec</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html">CVC3::TheoryArith</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html#ac34712c1935e1c1f465f3132c622d1aa">canonSimp</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html">CVC3::TheoryArith</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#aeb8051f2049c78b1b007e274288fcc3b">canonSimplify</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a2a7779383e5e73671e5b29978f106c0d">canonSimplify</a>(const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html#ad758f1c786e6c2631f0b74f0ef135353">canonThm</a>(const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html">CVC3::TheoryArith</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ae4ed8b9b3074828d356a35192288b397">checkAssertEqInvariant</a>(const Theorem &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#af7b2bbb0c854bab9488a19b1d3072cb5">checkSat</a>(bool fullEffort)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a7b516a72d54789b1403b8854b83aeb29">checkSatInteger</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ab67b64c7fd085bd9881aa7cef33217de">checkSatSimplex</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a272700cefa9c3f96bde0b61cc1d0b69e">checkType</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a437f70ccbf4e58ba40b4b9a067b224f1">collectVars</a>(const Expr &e, std::vector< Expr > &vars, std::set< Expr > &cache)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a84a67c02055bd8d4e4eb3d7c60ddf495">computeBaseType</a>(const Type &t)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a5c9f6212127845ff56f5c88aff72d49a">computeModel</a>(const Expr &e, std::vector< Expr > &vars)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a7d73feef91b15cb086f6d1b7a7bd19c2">computeModelBasic</a>(const std::vector< Expr > &v)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#adb72936111e69a1ab0e032cc017ee2db">computeModelTerm</a>(const Expr &e, std::vector< Expr > &v)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a48d4a6a488973f4fc79fc8d0c4d1470c">computeNormalFactor</a>(const Expr &rhs, NormalizationType type=NORMALIZE_GCD)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#aa618dbba5196953efee6954efe321ef8">computeTCC</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a86fdcfbc819885dac3640dcf68472554">computeType</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a46272039047747962cdfbb34d6e54476">computeTypePred</a>(const Type &t, const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a5d837dd76fd8ae099ace4c1e6492301d">consistent</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ac92f7d2a8db02ccf23fe15302dee278d">createProofRules</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a2f0dca2d2952728c2556f8d255cfb008">d_buffer</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a9a394c94c0607e645c355489631ed690">d_bufferIdx</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a2f0bafe4d3eddd28d9d9484318c17e45">d_bufferThres</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#add35a93fae75084ae5b77f1995477c77">d_countLeft</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ad568a72b85a6bc0c70dfe14d279c9360">d_countRight</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a7f402d265d6f783bbc4139ba3dddd9db">d_diseq</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a40a1d8f8e7d2faf4ddffe3ca14a90e88">d_diseqIdx</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ab5a2165c11bc6867c349627682291fcf">d_freeConstDB</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#aed79ec63593f899733e76790d28d4a62">d_graph</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a74167d750ba8d8cc8b0ec520e8a41894">d_inequalitiesLeftDB</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#acb102f87cd4bcdba4d404a6951eac0aa">d_inequalitiesRightDB</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ae29425ad828a82acb991db1ab50e8dd7">d_inModelCreation</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html#a8ae42bae19cdfd95be038365c55ca1ab">d_intType</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html">CVC3::TheoryArith</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html#a96bd09b1e8c9d9044d186197fa3aa924">d_kinds</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html">CVC3::TheoryArith</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html#a447eac07a3b8a1f439e9379466be2a10">d_realType</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html">CVC3::TheoryArith</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a1fb30358f2875620fef664227f0d3d5e">d_rules</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a6d0b6ef62c9feb4df9c71f2c11912b54">d_sharedTerms</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a7ae009f0e7ba96e071f45d9e1094c522">d_sharedVars</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a262fdc338527489b376ec181ecc38ddc">d_theoryUsed</a></td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html#abee62d97b0c60a1a44b7ede3c60b11b6">darkShadow</a>(const Expr &lhs, const Expr &rhs)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html">CVC3::TheoryArith</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a3353b432dcd79f2168bfcefc072edb67">DependenciesMap</a> typedef</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a5fd6d2cc2d018a67da124ef194f178ab">dependenciesMap</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#aeee481c90c90340e900a847fc0c8b82e">deriveGomoryCut</a>(const Expr &x_i)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ab43a4690bbc1cbe62a368efa7816de4a">doSolve</a>(const Theorem &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a93856c9af82b2c25c51b3c36bafb71f4">enqueueFact</a>(const Theorem &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#af833743a1332ba2b84bdc4118a05300f">enqueueSE</a>(const Theorem &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a26d56a1b473c8e770caba9f3eb85f79a">explanation</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a0bbf7c5b6079fc99a0f759e5809fe6f5">falseExpr</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#ac59f888b3b3f973580e061ffd803b6bb">find</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ad2690ef89c8acd959a9238c4f0bc0a57">findBounds</a>(const Expr &e, Rational &lub, Rational &glb)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a5fcebedad96665573ab5eafb7d70b2e0">findCoefficient</a>(const Expr &var, const Expr &expr)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a08412b310cb743536f7edd9fccd60e46">findExpr</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#abb05a7ed953b9b3ac71497c44826c743">findRationalBound</a>(const Expr &varSide, const Expr &ratSide, const Expr &var, Rational &r)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#ab46ce7e7b6c9425a42df38ccf56642b6">findReduce</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#ad0f5335bae1a358802ec5b958e77934e">findReduced</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a89a91d7480d5783fb0c0f67f2fdb7873">findRef</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a1070c24b2f7c993390dc1e3f00282f94">finiteTypeInfo</a>(Expr &e, Unsigned &n, bool enumerate, bool computeSize)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ac7d4a8110239f9c2d6f17c7a46a69d6e">freshVariables</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8">getBaseType</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a26afbc255a32b9fcff11d6b2625157ae">getBaseType</a>(const Type &tp)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a41dbe160161458e73fa669fe891ec529">getBeta</a>(const Expr &x)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a50802b148e8192178cf790e6c45ddff3">getCommonRules</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e">getEM</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ad4e8b908bccb2d534552f968bd27979c">getLowerBound</a>(const Expr &x) const </td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a843498f8c1a569a296822e8f1f92d675">getLowerBoundExplanation</a>(const TebleauxMap::iterator &var_it)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ab27c747e527f4e6a9f0bc39692a706af">getLowerBoundThm</a>(const Expr &x) const </td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#ad8b27aeea37d99def7a3c0348ded3e66">getModelTerm</a>(const Expr &e, std::vector< Expr > &v)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a4867f332c809f6efe8f01ffa45c32db3">getModelValue</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a4270eb556496ee10472b478b5792751c">getName</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#ab7c83d1e21c1553ff229447fe6d51530">getNumTheories</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a4ed9c0c6e1bfa32ead951cb6c1221f0e">getTableauxEntry</a>(const Expr &x_i, const Expr &x_j)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#af38bdeb162a9ab9bd81ce40f598f608f">getTCC</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a39539e895f8aade88ae5bc05bbcc9302">getTypePred</a>(const Type &t, const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a7fcc9a229fd6125188d69f4bc282cdfb">getUpperBound</a>(const Expr &x) const </td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a6bbd3291d090682e1c8a2cadb0d8380d">getUpperBoundExplanation</a>(const TebleauxMap::iterator &var_it)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ab41d31e40d053398a37f77a7a797c7a7">getUpperBoundThm</a>(const Expr &x) const </td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ad6fc5bdbe7ed6bcd4df8543e96b2b079">getVariableIntroThm</a>(const Expr &leftSide)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html#ae7d59b8b9bff1ae3cbb1b67a0baa3463">grayShadow</a>(const Expr &v, const Expr &e, const Rational &c1, const Rational &c2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html">CVC3::TheoryArith</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a8dc9b3350f948ce5b6112a4812819696">hasTheory</a>(int kind)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#aeda4c57dfbe357a80a348da9ffa71072">iffMP</a>(const Theorem &e1, const Theorem &e1_iff_e2)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#ab85541a91803599b7495f709c72c28c5">inconsistent</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a6b1c155465b0c24885213e7442dd0882">installID</a>(const std::string &name, const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a17aa12461bb0531b62670e37499b38a0">integer_lemma</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html#ad3e47bba6c50745ad194cf273aa1d146">intType</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html">CVC3::TheoryArith</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ae79693c72c0c7236d6d76cab2a4dcc0b">intVariables</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html#a8a309c3cad104aeb4a0b94b64dff22d7">isAtomicArithFormula</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html">CVC3::TheoryArith</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html#a432e12ff64bf229a3572e36d49aec683">isAtomicArithTerm</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html">CVC3::TheoryArith</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#af4eaf347e86ee4616a52676801213711">isBasic</a>(const Expr &x) const </td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a8e6e4c763da5203506a4ccc89d884655">isInteger</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#aedd0b63568ada4ac3ddbc515e882a617">isIntegerDerive</a>(const Expr &isIntE, const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a1f78d51287d2a25282a94b7bb09d7932">isIntegerThm</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a8d466120560b7b91dc279e657fe3c433">isLeaf</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#aa0ef53bc2009d92763e0916c38aaf692">isLeafIn</a>(const Expr &e1, const Expr &e2)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a210dc18f7e0df0a95ff00292e9dacdbc">isolateVariable</a>(const Theorem &inputThm, bool &e1)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a2597ed8fe8f3cae03240a2064d516c88">isStale</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a6c182b83ba6d8d60557dfa19446fb9da">isStale</a>(const Ineq &ineq)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html#a4df272c28af590572a6ed1b1df8316b0">isSyntacticRational</a>(const Expr &e, Rational &r)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html">CVC3::TheoryArith</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a89696e5cdd27e0e15711a7b9a027c205">kidsCanonical</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html#adcdf01dd1e0f78760fefc2a82b604098">leavesAreNumConst</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html">CVC3::TheoryArith</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a8dd39cad11cf866afc6282475cfc81b7">leavesAreSimp</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ad34845d9afc0b2091a4e07d6ee805066">lessThanVar</a>(const Expr &isolatedVar, const Expr &var2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a61a4a3159152e1ff93dea55a33441557">lookupFunction</a>(const std::string &name, Type *type)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a4e57c5fb189f51c6e5abeeb0bcb1baef">lookupTypeExpr</a>(const std::string &name)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a4b58aeebc3a62e41f0ce71ba01fa3961">lookupVar</a>(const std::string &name, Type *type)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a9fd0d5eca20607172cb8260a02296e74">lowerBound</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a97642364c244b753d33b551fc8c3bb9a">newFunction</a>(const std::string &name, const Type &type, bool computeTransClosure)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#ac6c5f95bbc428cad8085b416cd40292a">newFunction</a>(const std::string &name, const Type &type, const Expr &def)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#af85a563480c411b1e8eb280de9f39bb2">newSubtypeExpr</a>(const Expr &pred, const Expr &witness)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#aadde006d0dea508fec039b8092b14ed6">newTypeExpr</a>(const std::string &name)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a7aadedb0affc98a4cd1741f5dcf42d3a">newTypeExpr</a>(const std::string &name, const Type &def)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a4f82b4903d68da2bd83afb104c2c62cc">newVar</a>(const std::string &name, const Type &type)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#aa7b6e0e6f53256fd0e5573ad51ae472b">newVar</a>(const std::string &name, const Type &type, const Expr &def)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a9707c04f2d2af4812b8c18029f0368f4">NormalizationType</a> enum name</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a243f5665943792345df52be2a94eb648">normalize</a>(const Expr &e, NormalizationType type=NORMALIZE_GCD)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a51f12b9264f77ec8a82f58cce68780c8">normalize</a>(const Theorem &thm, NormalizationType type=NORMALIZE_GCD)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a9707c04f2d2af4812b8c18029f0368f4a5df10a1338d39c91f6886d5b09a2751d">NORMALIZE_GCD</a> enum value</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a9707c04f2d2af4812b8c18029f0368f4a382fccac5af0c0091adfac3b4048c2ba">NORMALIZE_UNIT</a> enum value</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a9c096e8707864d1a0ecde75bd58cf424">normalizeProjectIneqs</a>(const Theorem &ineqThm1, const Theorem &ineqThm2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="group__Theory__API.html#ga30a5750a0c38416c847e411c7400214a">notifyInconsistent</a>(const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a24b0687e8f0fa36a6d5bacc8155517e2">operator<<</a>(std::ostream &os, const FreeConst &fc)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a588ea1b8e9435f2a0fa0fbfe028fbd28">operator<<</a>(std::ostream &os, const Ineq &ineq)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#abd5a64ee867dda0c216a04e9fc7fbd6c">parseExpr</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ae909a0b86693e59e95c69de37e6adf08">parseExprOp</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a7e1ffe57de5017f1a3bc83aa3a6163a7">pickIntEqMonomial</a>(const Expr &right)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a5d94da8150af4d31977b695bfeac4801">pickMonomial</a>(const Expr &right)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ab19840152f3116c50edb0b6c0cc673f7">pivot</a>(const Expr &x_r, const Expr &x_s)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ae9e0aad1b930137d011dbab8bf4b0874">pivotAndUpdate</a>(const Expr &x_i, const Expr &x_j, const EpsRational &v)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#abebb5cee14c85657ea68c873372b14d9">pivotRule</a>(const Theorem &eq, const Expr &var)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a01afc8056a17c0412af99b3c33bace20">print</a>(ExprStream &os, const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html#aa2e49ab9e41d425df9398b27c7a95251">printRational</a>(ExprStream &os, const Rational &r, bool printAsReal=false)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html">CVC3::TheoryArith</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a2f6e83fb2d863d7625c94d90bf5db856">processFiniteInterval</a>(const Theorem &alphaLEax, const Theorem &bxLEbeta)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#aa2a249c2877aa16d3517a6cca9992216">processFiniteIntervals</a>(const Expr &x)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#afdcb8dc50f957161f878c563f09a48b3">processIntEq</a>(const Theorem &eqn)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a5cc134d71df3e702dc3785072f4d5bb3">processRealEq</a>(const Theorem &eqn)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a25d8be2e57c83d2e810ee815fae992d7">processSimpleIntEq</a>(const Theorem &eqn)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ab4e8d03929cc1b660d29d94c3adf3fcc">projectInequalities</a>(const Theorem &theInequality, bool isolatedVarOnRHS)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ace61ed893b9e6d4b5e8ff19f40e9152a">propagate</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ac6fc7d06f3933010435be7f77b0022bc">propagateTheory</a>(const Expr &assertExpr, const EpsRational &bound, const EpsRational &oldBound)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a68884e312bf69a858ed5a45979571d1a">rafineIntegerConstraints</a>(const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html#a11b44bafcad3c0875372d6c90a041e2d">rat</a>(Rational r)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html">CVC3::TheoryArith</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html#a03fa81194322b92c488033695bec7204">realType</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html">CVC3::TheoryArith</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html#adea0b08bcb123d6dca2b4742326b87c1">recursiveCanonSimpCheck</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html">CVC3::TheoryArith</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a3dafcfa8f6451023a83ce69c53fac641">refineCounterExample</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#af860f5d5e01423628c97c399606916ff">reflexivityRule</a>(const Expr &a)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#acf71ca1da6261f1fb8f14522613de497">registerAtom</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="group__Theory__API.html#gafb1431aa8258f6663ad948ebb08e5330">CVC3::TheoryArith::registerAtom</a>(const Expr &e, const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a41499be2b31d82e7bec5efc880126510">registerKinds</a>(Theory *theory, std::vector< int > &kinds)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a97a6f8e09f71513da969fa7847346c6f">registerTheory</a>(Theory *theory, std::vector< int > &kinds, bool hasSolver=false)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a07c2391015494b5f71def510c1fb6e26">renameExpr</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a07b326cd94b2bb8bafa39faf07caaec5">resolveID</a>(const std::string &name)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#adf76a677d3133da1fb3e8cf33ba26cc9">rewrite</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#aba1822f2d985b50f6405c290c3814c1a">rewriteAnd</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="group__Theory__API.html#gaacb9782eae3d1121c415cd4b7650025c">rewriteAtomic</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a2d91d71489b0c0a9822cef765326bc89">rewriteCC</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a0f2e0c6647ff6282ee2f65116a82e13b">rewriteIte</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#ad58c336212c2669f3cf32c0915ee3788">rewriteOr</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html#a5fcd4d9b9075f8d00096eea469b81abc">rewriteToDiff</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html">CVC3::TheoryArith</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a420591a664c53906e735b528f7dc2c94">separateMonomial</a>(const Expr &e, Expr &c, Expr &var)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a08cc815e21d2972f54f8c1e70ce8ab51">setIncomplete</a>(const std::string &reason)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a89f8e1e02e22ef524c286ce8b87bdea4">setInconsistent</a>(const Theorem &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a57d34162d4006753f6202c531e2a9d9a">SetOfVariables</a> typedef</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a36a8c831cfe356a9e779988cae3e101c">setup</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a29cc343040a52a299a4f20123edf4c75">setupCC</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a251086c30f2a7939e6d624d4a4cd8db4">setupRec</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#adaea4aa951adbe1561f7b445517378b6">setUsed</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a52158688456f8605b064fbbf7a46039c">simplify</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a9d441225b287419426c80a0374d6c6cb">simplifyExpr</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="group__Theory__API.html#ga55b82868b8e9e60906756e797da9355a">simplifyOp</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a35ee82710c965d845aecbe6320f2ae38">solve</a>(const Theorem &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a6a01623e613f46e0d8f2de1a05262ec2">solvedForm</a>(const std::vector< Theorem > &solvedEqs)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html#a3ddbc092260178d9042bba1c175cb9a6">subrangeType</a>(const Expr &l, const Expr &r)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html">CVC3::TheoryArith</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#aeeb80a89d9eb5c4fc2515d2108e197d8">substAndCanonize</a>(const Expr &t, ExprMap< Theorem > &subst)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#af2775def72b9055dc878963bcfb9b947">substAndCanonize</a>(const Theorem &eq, ExprMap< Theorem > &subst)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a349c59e5b2eb5c2a9154f5bdeff43fde">substAndCanonizeModTableaux</a>(const Theorem &eq)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#afc88d03ab0e42f2e4e53f8c5800313ad">substAndCanonizeModTableaux</a>(const Expr &sum)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ad7d64d8e7110a9992654154b3e3613b0">substAndCanonizeTableaux</a>(const Theorem &eq)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a92e2da5223d7fb620cce85b2813e047f">substitutivityRule</a>(const Op &op, const std::vector< Theorem > &thms)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a83a1a0b30a27f887cef4c394544b30b0">substitutivityRule</a>(const Expr &e, const Theorem &t)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#abddfe81d6d08a46f1d1b3aa80ac565d5">substitutivityRule</a>(const Expr &e, const Theorem &t1, const Theorem &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a8ab61a1574ac8c29db7ddb5b0d45235b">substitutivityRule</a>(const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a56f710c79a9b3464189e8bb4d9d8a8c2">substitutivityRule</a>(const Expr &e, int changed, const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a7440711981ac1bba2bed7476c0fa4e0b">symmetryRule</a>(const Theorem &a1_eq_a2)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ad96e0ca1cad09988822b88f82ebdc016">tableaux</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#af2a4bc0a133edf66fe040d72c4e7ea01">tableauxAsString</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a159af481e211c2e18dd9280a17ae17a3">TebleauxMap</a> typedef</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a8fa244df7dcd091e8a5c3381053cc394">Theory</a>(TheoryCore *theoryCore, const std::string &name)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html#a6a2211c8a2f43f881c2d9cf31deb6f08">TheoryArith</a>(TheoryCore *core, const std::string &name)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html">CVC3::TheoryArith</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ab4411e3c522623b9041aa52ce7d857f7">TheoryArithNew</a>(TheoryCore *core)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a90684d2a97738341c00f8f9c99af7b66">theoryCore</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a01fa8047ed1f649dc98831cb536187e4">theoryOf</a>(int kind)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#ad4fea3e52e80f6ea2fb1a1eaaa7163b8">theoryOf</a>(const Type &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a9ea78dba89246dda6c504c7af5201f1b">theoryOf</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="group__Theory__API.html#gab66d477fcc5c27075a25dbfec4988537">theoryPreprocess</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a5dad9fa356483782703a1ef1024d2a74">theoryUsed</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</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_1Theory.html#a76f6507116e36f46dab074781fb9bf2d">transitivityRule</a>(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#ab8835beee96db67f3c26a604d96f2fe8">trueExpr</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a090c2b079f3b90b4f5da3d8606b14d16">typePred</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#aafdee81857fde584632759c78ed821f5">unregisterKinds</a>(Theory *theory, std::vector< int > &kinds)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a6bdcdfdf6d658b1b1b7c548ea4782e6e">unregisterTheory</a>(Theory *theory, std::vector< int > &kinds, bool hasSolver)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#afbbf8a22ba662eaea65afbbcb135ff83">unsatAsString</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a3accb9cf21e2168036e7b365649820fa">unsatBasicVariables</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a3790410296752fded1074ce1b808598b">update</a>(const Theorem &e, const Expr &d)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#abd8ac3d26ddd910cc52da9bde210e50a">update</a>(const Expr &x_i, const EpsRational &v)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a0b9e5a75b0e23a334563392f075df9e2">updateCC</a>(const Theorem &e, const Expr &d)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a85da313a2d543ca7343191a4cc20fa0d">updateDependencies</a>(const Expr &oldExpr, const Expr &newExpr, const Expr &var, const Expr &skipVar)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a59752d5aa73e48dd1a6c133a41a3c5d4">updateDependenciesAdd</a>(const Expr &var, const Expr &sum)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#aa21dc626bcc3110d6f90cddfa66e7729">updateDependenciesRemove</a>(const Expr &var, const Expr &sum)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a16a43c368ec23e06c847ae9684a98381">updateFreshVariables</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#ad6cb45844df7f1b08a53e41e40a362e3">updateHelper</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#af80703576d25418c16a5a187e8bcd0ef">updateStats</a>(const Rational &c, const Expr &var)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a8105c616e2a7410133e6f4c908d35def">updateStats</a>(const Expr &monomial)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ad22fa5522add29991c72dab60da2e922">updateValue</a>(const Expr &var, const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#a485637b86fce6c4a8d53d54e286d2eb8">upperBound</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#ac4527f940d280bca9ae279520fd1bc17">~Theory</a>(void)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html#a23882e28175f07c2f0636f5ffe423595">~TheoryArith</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArith.html">CVC3::TheoryArith</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html#ad1803172bb5078cdfc962febe9b080dc">~TheoryArithNew</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithNew.html">CVC3::TheoryArithNew</a></td><td class="entry"></td></tr>
</table></div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:18 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>
