<!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_1TheoryArithOld.html">TheoryArithOld</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="headertitle">
<div class="title">CVC3::TheoryArithOld Member List</div> </div>
</div><!--header-->
<div class="contents">
<p>This is the complete list of members for <a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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_1TheoryArithOld.html#a0f6143643b36835a5383acfa65252f3e">addMultiplicativeSignSplit</a>(const Theorem &case_split_thm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a7cc81a1017de4d7e2c7278dfc01a4e60">addPairToArithOrder</a>(const Expr &smaller, const Expr &bigger)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a1503d539a5f25dfdb5fcfe486405b658">addSharedTerm</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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#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><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a473d3204340c03e97f8eae1975b752cb">addToBuffer</a>(const Theorem &thm, bool priority=false)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a079cb45bf44fab2325badc15ec92c4e4">alreadyProjected</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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_1TheoryArithOld.html#a998f71fde188c547c464a912058dd64d">assertFact</a>(const Theorem &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><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 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_1TheoryArithOld.html#a515b32506fecca7cd6425d62b9ef5077">assignVariables</a>(std::vector< Expr > &v)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a46d5c29d89249608a80159a17ef5c794">AtomsMap</a> typedef</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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_1TheoryArithOld.html#a26c172f0fb2468ba2255c3d5a2c46811">BoundsQueryType</a> enum name</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#ad1514cc33619de965117a48c4e3ea342">bufferedInequalities</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a657b7b3914e46113e28b2e1fff310c26">canon</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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_1TheoryArithOld.html#a43f9a32880731caf7956db77adf633c8">canonConjunctionEquiv</a>(const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a3190adc8a44721ed37dfa34333462a0c">canonPred</a>(const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a4933900b82159f8380754b386a895f84">canonPredEquiv</a>(const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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_1TheoryArithOld.html#a1c6bb68d18ada95c8780bdce6e6cb5e5">canonSimplify</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a04fff631d56ee39c895818f6bb2014b6">canonSimplify</a>(const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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_1TheoryArithOld.html#aaa7f3188301a696b421577f2c8059a46">canPickEqMonomial</a>(const Expr &right)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a331a6d4320eee82cbb093fd587c96bb8">checkAssertEqInvariant</a>(const Theorem &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a1b75e191eff379114ec4ad4e73c73610">checkIntegerEquality</a>(const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a966afeabb8016841de17f5c51fe165a0">checkSat</a>(bool fullEffort)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#ad3e9ede8154ffafbbfdefef3c79d5f78">checkType</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#aa3aac05d983610669f500fb761615fa0">collectVars</a>(const Expr &e, std::vector< Expr > &vars, std::set< Expr > &cache)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#adaecdd481476e8db3e400a1bcecf25f3">computeBaseType</a>(const Type &t)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#ab89a3988c04c44852823fa598358ab67">computeModel</a>(const Expr &e, std::vector< Expr > &vars)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#ab0be6755fcb152cd582d064663e2d53f">computeModelBasic</a>(const std::vector< Expr > &v)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a30991bcd4bbcf65cd1c6215725af9899">computeModelTerm</a>(const Expr &e, std::vector< Expr > &v)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a1b9f6be5cba7ac4ae67800f5b002ef09">computeNormalFactor</a>(const Expr &rhs, bool normalizeConstants)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a6f507fbe5ded9976e290274059611808">computeTCC</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a0a9d00e2c2f734aec6d76a52cf301bc4">computeTermBounds</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#ae15e9cc1e826299a857a232c341402c1">computeType</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a5c1f93e8fcd10c7943895532cf0aa6f6">computeTypePred</a>(const Type &t, const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a80f0e73dede7d5072cf7941a39a8deb4">createProofRulesOld</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a44ca4928fb45298b5d5586c8b509fba3">currentMaxCoefficient</a>(Expr var)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a4d49144bb8b5ce32137c7ed8ccf27b32">d_buffer_0</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#abc136583724a477c0d748096580fe0b9">d_buffer_1</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a435fac35fb032c091e227398972ad55e">d_buffer_2</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a4e33f5321cb15e4f7252772c58600bce">d_buffer_3</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#aa2f920e8cc39034f24cbe52a7edb7754">d_bufferIdx_0</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a06582edc6ff3081f420bccb4a35b33e3">d_bufferIdx_1</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a31b271732e81b39fa2d228af1dff9a68">d_bufferIdx_2</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#aba34300626e64486129e1afa96da9837">d_bufferIdx_3</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a53b15103320c4dcce490238f380851ff">d_bufferThres</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a69bd49fe441cf96f2c665deb97ab6859">d_countLeft</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#ae642c380af492cdc4581a9182514c20c">d_countRight</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a475767dfdb12442c31b65bd944b00b10">d_diseq</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a2a0a551f54d4d406e672526fc863e982">d_diseqIdx</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#abf3123ffb3e08ece66d6982e9a4b6c2e">d_freeConstDB</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a3f242375ca87172a68b30c5a49a0cf2e">d_graph</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#af606dcd2ddc8be8ad3f0bb6fea6eb4db">d_grayShadowThres</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#ad4df2ed12abb38f060e8c82515b8608c">d_inequalitiesLeftDB</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#af89e9fc76620b5d170850e769cc0c785">d_inequalitiesRightDB</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a40829e395fe9f98d5b1a043df470c50c">d_inModelCreation</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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_1TheoryArithOld.html#a1f700d0b7e2e30c96ed9d9640d988860">d_rules</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a5c8d1f10ab619b668988eb866a5b8e45">d_sharedTerms</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#abd3bec60e2dbe8e0c427d91227733dd2">d_sharedTermsList</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a84b39d6978a6942723f608da58d54e51">d_sharedVars</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a7cee71daa7f8f8bbd33d0b6a333f61aa">d_splitSign</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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_1TheoryArithOld.html#acb4e673f7c27347289317a35a376f82d">d_varConstrainedMinus</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a1dbba6d20d053083679893b4f79998a8">d_varConstrainedPlus</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</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_1TheoryArithOld.html#ae176998a4531d73a2723680c45ef618c">diff_logic_size</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a1dda0fccac36ffbebc06beb58e404619">diffLogicGraph</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#affd5f1260775159e8b6b01783f3cfb9b">diffLogicOnly</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#aa9f5d8de688f66aecd61f2c079b0e4e8">diseqSplitAlready</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a939e94398d23870f3a43fc0d7067b581">dontBuffer</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a7026fb3070c66f3e3001ca94c3153434">doSolve</a>(const Theorem &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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_1TheoryArithOld.html#a3244505fc75c1ef822b445c266da5bb5">extractTermsFromInequality</a>(const Expr &inequality, Rational &c1, Expr &t1, Rational &c2, Expr &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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_1TheoryArithOld.html#a8dfcde6ee0edf0f14959b1b582575261">findBounds</a>(const Expr &e, Rational &lub, Rational &glb)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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#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><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#ab26f578642a85785f9323fcabef94797">findRationalBound</a>(const Expr &varSide, const Expr &ratSide, const Expr &var, Rational &r)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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#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><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 class="even"><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><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#ae22b1b370ee8be1c54ef4a1c3f527d5f">finiteTypeInfo</a>(Expr &e, Unsigned &n, bool enumerate, bool computeSize)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a7bb41aa46d0caeecb89a534fc9c359af">fixCurrentMaxCoefficient</a>(Expr variable, Rational max)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#afc337545f540e2e3301cfaa0ff240c29">fixedMaxCoefficient</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#af353ec3abe3d512a90dc8b83a28ccfb5">formulaAtomLowerBound</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a1c52c54bc6c46167e0526723128c0e72">formulaAtoms</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#af6089a946fd9248a222bd3a83d2e4478">formulaAtomUpperBound</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a5adbc1a0946700ed1c6258fd29e044be">freeConstIneq</a>(const Expr &ineq, bool varOnRHS)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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_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><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 class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a1bd6e1f367ec9b69c2f511716c4d4b59">getFactors</a>(const Expr &e, std::set< Expr > &factors)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a1582b7d8a6cfa35a2eb1372408e1d9d1">getLowerBound</a>(const Expr &t, BoundsQueryType queryType=QueryWithCacheLeaves)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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#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_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><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 class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a92ebe6beaf47d0b9567b4552e9aabf94">getUpperBound</a>(const Expr &t, BoundsQueryType queryType=QueryWithCacheLeaves)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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_1TheoryArithOld.html#aa3b6cea5b43872330fab4c92d55a71d0">hasLowerBound</a>(const Expr &t, BoundsQueryType queryType=QueryWithCacheLeaves)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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_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 class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a7ec3bcab775ad3248c29c09c4a109a11">hasUpperBound</a>(const Expr &t, BoundsQueryType queryType=QueryWithCacheLeaves)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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_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_1TheoryArithOld.html#a83f995b3176a7faffae2a5fcd5c2386f">inequalityToFind</a>(const Theorem &inequalityThm, bool normalizeRHS)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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#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><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_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><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 class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#ad2133967c6b85ec7b144f023b7428afd">isBounded</a>(const Expr &t, BoundsQueryType queryType=QueryWithCacheLeaves)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a39d64f6ffb9232db82c4fea6ad6407b3">isConstrained</a>(const Expr &t, bool intOnly=true, BoundsQueryType queryType=QueryWithCacheLeaves)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a31e4ddb10498727798fb49d7dae42312">isConstrainedAbove</a>(const Expr &t, BoundsQueryType queryType=QueryWithCacheLeaves)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a9c85d0cd35937c0ae9d343490b470e22">isConstrainedBelow</a>(const Expr &t, BoundsQueryType queryType=QueryWithCacheLeaves)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a849e9094d3af74ee70e45112b353136c">isInteger</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a6e0c686fb1eedbe704466bceb531dab7">isIntegerDerive</a>(const Expr &isIntE, const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a616b3e984904813383d6bc716496ef06">isIntegerThm</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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_1TheoryArithOld.html#ab8686f11885fd196e2d0e592f767ba76">isNonlinearEq</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#aadfdf8251af6c3a07baa5e8ee0828146">isNonlinearSumTerm</a>(const Expr &term)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a3bef421de6f4579b54b76666d015ecb4">isolateVariable</a>(const Theorem &inputThm, bool &e1)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#af99992fce594e9940305e0121eb0b45c">isPowerEquality</a>(const Expr &nonlinearEq, Rational &constant, Expr &power1)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a3eebb5aa899590483a0e9f8223599051">isPowersEquality</a>(const Expr &nonlinearEq, Expr &power1, Expr &power2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#ac623d777315532c14558cff5b16cd085">isStale</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a65e5d28ea620e399d0d11e4580379394">isStale</a>(const Ineq &ineq)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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_1TheoryArithOld.html#a820f1ace7a5dd9e962b2453ceb1bcaf1">isUnconstrained</a>(const Expr &t)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a787aa195e77ab9fd007352d5ad74cc7f">kidsCanonical</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><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 class="even"><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><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a7aaeb2f1987ed2be618088b8149dd329">lessThanVar</a>(const Expr &isolatedVar, const Expr &var2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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#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><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 class="even"><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><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a9600791c28f5e0d0cfd79c8eb025f5e3">maxCoefficientLeft</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a667bd1e22b3275a0c8544e29bd8fe613">maxCoefficientRight</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#ab9e74bfc121f8d683449540b3f47648d">multiplicativeSignSplits</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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#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><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 class="even"><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><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 class="even"><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><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 class="even"><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><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a372a7ff635b9de24607daa04d3a63d02">nonlinearSignSplit</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a19b5fc9e624049923d3bf7d561cf83a8">normalize</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#ad28af4388c0e1a5548faddbc00662040">normalize</a>(const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a6998209aa1c4e1ed10a2be7b7303d89c">normalizeProjectIneqs</a>(const Theorem &ineqThm1, const Theorem &ineqThm2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><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 class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a24b0687e8f0fa36a6d5bacc8155517e2">operator<<</a>(std::ostream &os, const FreeConst &fc)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a588ea1b8e9435f2a0fa0fbfe028fbd28">operator<<</a>(std::ostream &os, const Ineq &ineq)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
<tr class="even"><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><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#ae4d0208af0078ee314c94f199f8b50db">parseExprOp</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a1c9bcf5e29f48498065f1d32a8c3f4b7">pickIntEqMonomial</a>(const Expr &right, Expr &isolated, bool &nonlin)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a12afa30f9322b35f5c79107522aa3d40">pickMonomial</a>(const Expr &right)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a887b53a4c32e7daab34048bdfe2a31c4">print</a>(ExprStream &os, const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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_1TheoryArithOld.html#ad6d1693a1a81c87e64d51abb3596f21b">processBuffer</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#abc79fe4a559ac4d6e9b75a2cab81d2b0">processFiniteInterval</a>(const Theorem &alphaLEax, const Theorem &bxLEbeta)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a9dc4aaaa3c9bf4cc53ed6e699b5cb67d">processFiniteIntervals</a>(const Expr &x)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a4f8a6f8aa73817d4696a4035713c1eaa">processIntEq</a>(const Theorem &eqn)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a8eee6ca3ee410677dea1209a8cbef65f">processRealEq</a>(const Theorem &eqn)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a8b94e299e5947b05b3e29757ff621b56">processSimpleIntEq</a>(const Theorem &eqn)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a03cf8b3d693cd9bc3237f9e1e1cacaf1">projectInequalities</a>(const Theorem &theInequality, bool isolatedVarOnRHS)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a26c172f0fb2468ba2255c3d5a2c46811a3a2069125b24eeea4fcd590525d935bc">QueryWithCacheAll</a> enum value</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a26c172f0fb2468ba2255c3d5a2c46811acaf2c948bff23c8f1d04da41f12fe574">QueryWithCacheLeaves</a> enum value</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a26c172f0fb2468ba2255c3d5a2c46811a24a2b363efc7f74b482ce52d1957b3bf">QueryWithCacheLeavesAndConstrainedComputation</a> enum value</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#aea59b6a8576bd484d6bcede8363e4076">rafineInequalityToInteger</a>(const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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_1TheoryArithOld.html#aa4dc2c586e3bf401a1940a2057508d9f">refineCounterExample</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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_1TheoryArithOld.html#ad4d5973db0c0b0d26e358450b0c0a4a1">registerAtom</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span><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_1TheoryArithOld.html#a17c6d2694c44f77da17d5b32620b0761">rewrite</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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_1TheoryArithOld.html#a86f96d920118d4b8c7b6bf78bb6ee740">selectSmallestByCoefficient</a>(const std::vector< Expr > &input, std::vector< Expr > &output)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a7cf2bbefa118b69a416778e98cda8408">separateMonomial</a>(const Expr &e, Expr &c, Expr &var)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><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 class="even"><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><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#af876aaea3321dd03faebd5f4b3f06ddd">setup</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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_1TheoryArithOld.html#ac240d8f8712b716744824921cf46deb0">setupRec</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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_1TheoryArithOld.html#adecf2614be23bfd1347e1992081e7848">shared_index_1</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a4a63d7abe48efcd5262bdec8d2a48ebf">shared_index_2</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</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_1TheoryArithOld.html#a9488a6be1041e63a9519482ac7e854c8">solve</a>(const Theorem &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a02f7b174fc1989343a087bb495cb7e75">solvedForm</a>(const std::vector< Theorem > &solvedEqs)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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_1TheoryArithOld.html#a315acb4c55cf413c47c013853a534112">substAndCanonize</a>(const Expr &t, ExprMap< Theorem > &subst)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a6d57d63930df3fd7cd61ffb4603f012d">substAndCanonize</a>(const Theorem &eq, ExprMap< Theorem > &subst)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><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 class="even"><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><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 class="even"><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><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 class="even"><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><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a8c0a52d514303b34e73fc36803331419">termConstrainedAbove</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#afd5889bc69bdde0f39137619db945c80">termConstrainedBelow</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a878f9a4ecf6d87a79f37e9e916750d4c">termDegree</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a14047821f94566b7a46950d1f6529332">termLowerBound</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#aa3cbd03caf1f931c74829f2502d75553">termLowerBounded</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#ab6d69b6422585056ed9ce55777d04590">termLowerBoundThm</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a45ed4c2833167e036dbf682c8bd06e72">termUpperBound</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#ae3f7689542dd29298e68dcc16e5976e6">termUpperBounded</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a21dd22e840f352a67dc6be3472a2bb5a">termUpperBoundThm</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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#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><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 class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a421bf72419f51b1a7e95363da00f4177">TheoryArithOld</a>(TheoryCore *core)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"></td></tr>
<tr><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 class="even"><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><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 class="even"><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><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 class="even"><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><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 class="even"><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><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#af26f1b31629fe94f3678e4d051b17afa">tryPropagate</a>(const Expr &x, const Expr &y, const DifferenceLogicGraph::EdgeInfo &x_y_edge, int kind)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"></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_1TheoryArithOld.html#a314a1422f7fb05eb90d94cd88625fd0c">update</a>(const Theorem &e, const Expr &d)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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#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><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#abc26aaf78f6b9a25b3c5f3923719ddb7">updateConstrained</a>(const Expr &t)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"></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_1TheoryArithOld.html#aeda9acb0bae07ff39ce79f8b0e2e83f7">updateStats</a>(const Rational &c, const Expr &var)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#aeb19474dc85d27601add9f7956bb2768">updateStats</a>(const Expr &monomial)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a1a20be9ae34b5301092b70364d8b4bb1">updateSubsumptionDB</a>(const Expr &ineq, bool varOnRHS, bool &subsumed)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html#a5aef4b094054e928a145c5b9ee5703d1">zero</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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_1TheoryArithOld.html#a72870e1afaa3d74f5de058116211b4a9">~TheoryArithOld</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryArithOld.html">CVC3::TheoryArithOld</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>
