<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<title>CVC3: Member List</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li class="current"><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="annotated.html"><span>Class List</span></a></li>
<li><a href="classes.html"><span>Class Index</span></a></li>
<li><a href="hierarchy.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="namespaceCVC3.html">CVC3</a> </li>
<li class="navelem"><a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> </li>
</ul>
</div>
</div>
<div class="header">
<div class="headertitle">
<div class="title">CVC3::TheoryCore Member List</div> </div>
</div>
<div class="contents">
This is the complete list of members for <a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a>, including all inherited members.<table>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a13ba9024a22362cc96760519a84f2316">addBoundVar</a>(const std::string &name, const Type &type)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#aa8f3f9fb084f9d5e385255baab5dc8f3">addBoundVar</a>(const std::string &name, const Type &type, const Expr &def)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#aecef2465eb761f7f112ddce77f93d081">addFact</a>(const Theorem &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a688cd0c0b669ab9719f8a99cb207ad2c">addGlobalLemma</a>(const Theorem &thm, int priority=0)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ac317be8457175b3cf458bff7f4cb6e27">addNotifyEq</a>(Theory *t, const Expr &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#aaf10cf53aae11fb855883f87c29e02e4">addSharedTerm</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [inline, virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a605e960d2442b587046c562723b7f03a">addSplitter</a>(const Expr &e, int priority=0)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ab810c8fdffa082334e4aa840d1249a39">addToVarDB</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#aaab0bd52237688848681cdb62c74f14c">assertEqualities</a>(const Theorem &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private, virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a36d46f0d53c3513ea56ee2eba60cd75a">assertFact</a>(const Theorem &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a3a897e60d6dd1dfd382870054e5ad777">assertFactCore</a>(const Theorem &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a1f662e7f045032350f2a3bccc63a71d6">assertFormula</a>(const Theorem &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="group__Theory__API.html#ga4ce2fe1baec76fcb6120bbd86623ecd2">assertTypePred</a>(const Expr &e, const Theorem &pred)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline, virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a584ebdaddb7e1a51b1740277a0b7098d">assignValue</a>(const Expr &t, const Expr &val)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a1a5505333dc3aea609553ab72f509205">assignValue</a>(const Theorem &thm)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a705d998884ec8a53c22220373472d868">boolType</a>()</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a6b5123c9d923a076385aa83a0fa37cf5">buildModel</a>(ExprMap< Expr > &m)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a5cce3a2fa78a9aa11b7d8e0668434f95">buildModel</a>(Theorem &thm)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a052424ef27a5042f6321db9a8d41bf82">callTheoryPreprocess</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="group__Theory__API.html#gacdab59f42f5124655275d2e08e7aa0e3">checkAssertEqInvariant</a>(const Theorem &e)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline, virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a0b0a73410836f7b3a0808a67647ba448">checkEquation</a>(const Theorem &thm)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a66cdb1662f1608dc95664b41ff90f1e4">checkSat</a>(bool fullEffort)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [inline, virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ae45217f71500d48ef1c4c5118011f254">checkSATCore</a>()</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a164ec255c41d187cc87f6996a8a5389a">checkSolved</a>(const Theorem &thm)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ada717b1e852018d77f154682a01f6731">checkType</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#aeeb68f961407ee80a9762a95e6998cf2">clearInPP</a>()</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a21441c74132e9fcfb53d2b33bd8c622a">collectBasicVars</a>()</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a48ba4c9731b4be8afdeafdf3eddeb919">collectModelValues</a>(const Expr &e, ExprMap< Expr > &m)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a624d8ed203fdd666ae97ec10f9859d26">computeBaseType</a>(const Type &t)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="group__Theory__API.html#ga4a5b9fff88df80582fc76fd3def55002">computeModel</a>(const Expr &e, std::vector< Expr > &vars)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline, virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a6edb2212446e43165666dcb7f319985a">computeModelBasic</a>(const std::vector< Expr > &v)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="group__Theory__API.html#ga37309ea20a161f2529cbb0ab79f9ed3f">computeModelTerm</a>(const Expr &e, std::vector< Expr > &v)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#acd533616106f9987039cfbd5988d50d5">computeTCC</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a4968c9a9514669bbd9c2e6774f17b743">computeType</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ab12924c15cb53753ba91d1766282a71e">computeTypePred</a>(const Type &t, const Expr &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a6b4c0f704ab77eddaaa6308ad6cf45cd">CoreNotifyObj</a> class</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [friend]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a5b386f16781365b7421e884baaebae41">createProofRules</a>(TheoremManager *tm)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ae0a477cb44ee4e9285008f0653b2f366">d_assignment</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#afbe156b32fe43d2b3e5519477df83110">d_basicModelVars</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#af1f09ebd45eebb8171943533fe49e677">d_boundVarMap</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a72592744e8f94ed7c832ad895791a72a">d_boundVarStack</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#aa803e0e65fec3e389c9c4d12d8d634a3">d_cm</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ae1618a8812ad74a6349ad585bb677354">d_coreSatAPI</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ae9e63b5ca2b5d745cb176ac3a528959b">d_currentRecursiveSimplifier</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a03b7c799d7ee3b3a4a10f14b2faacfbb">d_exprTrans</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#adf5b754e1e4732cb0e1946cf0f274885">d_flags</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a6ef875ba12849a2bfd367c4e1bc02e71">d_globals</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a7b531fbcb166cac53d82f74c812d42f6">d_impliedLiterals</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a496993a9e180ca584cff84ce9dbdff69">d_impliedLiteralsIdx</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#abf9ffc3f83f262e0acdece359d2d00bd">d_inAddFact</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#adc61197a61a4a024cdd614a281f8cf0c">d_inCheckSATCore</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ae81dae9c186efe8ead153d14e29985bf">d_incomplete</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ac44993c5095bc2fda1f6b931060223bf">d_inconsistent</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a1560124d30d8cda4a6cedca4c919f8aa">d_incThm</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#aac5050e644f0c475d104f4dd3a8ddf32">d_inPP</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a608590056910229da1a794d0dd5930c4">d_inRegisterAtom</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a966030ae5b96557c9ea5de874a9526ef">d_inUpdate</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a96ce7c2fe3b14e3b8b4661fbe19db290">d_notifyEq</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ae16ab39bb24e04e3928d693ac3a1bb1e">d_notifyObj</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#af8402b991e938282c87e01120dfd6b99">d_parseCache</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ac0523af18592d25050b45ca363e52332">d_parseCacheOther</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a22825b89097f0baa8348f268317db563">d_parseCacheTop</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a27f2f350452da6f7adca44c342a1f29d">d_predicates</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#aba88f17e048e24984f8637be9d31a74c">d_printer</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#af057513081cf61dc3780967f84ae58fe">d_queue</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a5253f49c096b1ce32579f7095c895ac4">d_queueSE</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a7040ce9b2fa8d567df0d84a5ceee84bf">d_resourceLimit</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#af28b98269dc8ef40a6fa97d58f414173">d_rules</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a28416be391c5f58a2bf7cbe301e81663">d_simplifiedModelVars</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ac02ca139143a150df1ecb7ec4d4247e7">d_simplifyInPlace</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#af15d1082296c5c7f610d832bfb3cc675">d_solver</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a053311bcc9681a402ab440bf90447632">d_statistics</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ab1f589f325461e2bb39f0035c2dfa4bb">d_tccCache</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a9ebcf505b2577cd3a3a29d70a4fd50ae">d_terms</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ab2fd8e3ebcc92df0276d6d0b4e8a88bf">d_termTheorems</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a067b4f792c7bcd9fa1d756efdc5d1e72">d_theories</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#af9395eb99819f9b78df0dcb24ffac785">d_theoryMap</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a262fdc338527489b376ec181ecc38ddc">d_theoryUsed</a></td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#aa2e429d75afaade7281ed2b370a50dcf">d_timeBase</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a4ad36b717dcce5ed5ad9a4514e39e66f">d_timeLimit</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a8b9c81920208ce15dac9eb3bb97b4a2b">d_tm</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#abe21ce53a179720cb3e94293fd6d771f">d_translator</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ae430167a0f9f0e2ba742436bcb04e9fb">d_typeComputer</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a9b774b862908ff097c6aed53bdfdbcd3">d_update_data</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a0813a81e68625ac93111f45a4e81b131">d_update_thms</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ad2689808e6b677e79151c5ae413a9170">d_varAssignments</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a74cb89f5b3e600cde8e0d7b961532a5e">d_varModelMap</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ae3ac2dba3022934af3ba4a61fc979be4">d_vars</a></td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a9563215d97859a27f661c1517614f6ce">EffortLevel</a> enum name</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a479141bc26a125b758a2acc6420274f9">enqueueFact</a>(const Theorem &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a09a7b1c4878f4ce9150fa89d304ca172">enqueueSE</a>(const Theorem &thm)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a0bbf7c5b6079fc99a0f759e5809fe6f5">falseExpr</a>()</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#ac59f888b3b3f973580e061ffd803b6bb">find</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a08412b310cb743536f7edd9fccd60e46">findExpr</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#ab46ce7e7b6c9425a42df38ccf56642b6">findReduce</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#ad0f5335bae1a358802ec5b958e77934e">findReduced</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a89a91d7480d5783fb0c0f67f2fdb7873">findRef</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#acf724e4b497f7ca829eaaca9007fbae6">finiteTypeInfo</a>(Expr &e, Unsigned &n, bool enumerate, bool computeSize)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a9563215d97859a27f661c1517614f6ceaf927a488bd3f95079d191debe7e93a06">FULL</a> enum value</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a3875119ce8336e4bb67a5cc6e771f779">getAssignment</a>()</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8">getBaseType</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a26afbc255a32b9fcff11d6b2625157ae">getBaseType</a>(const Type &tp)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a9377f423f4fd59fdac396794363733a6">getCM</a>() const </td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a50802b148e8192178cf790e6c45ddff3">getCommonRules</a>()</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a261880d3c6b9b852de5e1d146b9e1731">getCoreRules</a>() const </td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#aac8dbad8636607fa6424b0926c6c1c59">getCurQuantLevel</a>()</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e">getEM</a>()</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#acc963fd43994f06d3647394b731e835c">getExprTrans</a>() const </td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a46b2792a5c24f95ccfc3fbfc0456b09f">getFlags</a>() const </td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a464a49882cbd94a3c48428ed60d3a365">getImpliedLiteral</a>(void)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#adb97ff20d5c0d9a93d322b347b306f69">getImpliedLiteralByIndex</a>(unsigned index)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#ad8b27aeea37d99def7a3c0348ded3e66">getModelTerm</a>(const Expr &e, std::vector< Expr > &v)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ab360cca9e30af4434130557f6b45f627">getModelValue</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a4270eb556496ee10472b478b5792751c">getName</a>() const </td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#ab7c83d1e21c1553ff229447fe6d51530">getNumTheories</a>()</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a2c0a37ab972568b851d69292959eb915">getPredicates</a>()</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ae4e1f7bd995e6ef2bff499869d95c177">getQuantLevelForTerm</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a1558a9399314632d76c3d086f680d3b7">getResource</a>()</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ae5f8dd0508305fac921b9475376c4623">getResourceLimit</a>()</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a7f119c4fa5313b72feca7dd441e045f0">getStatistics</a>() const </td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#af38bdeb162a9ab9bd81ce40f598f608f">getTCC</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a605f2eee0d52005dba7450e14d36c002">getTerms</a>()</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ad072fbeed392b4b7ecb651609acfd9bd">getTheoremForTerm</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#af3077cff0601b8ae28e420ef5ce2ea37">getTM</a>() const </td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#af21dce6ee9ed152e132a4e77f10323e7">getTranslator</a>() const </td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a39539e895f8aade88ae5bc05bbcc9302">getTypePred</a>(const Type &t, const Expr &e)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a07e62d88f43bc14e3f0fe4805bd99356">getValue</a>(Expr e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a8dc9b3350f948ce5b6112a4812819696">hasTheory</a>(int kind)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#aeda4c57dfbe357a80a348da9ffa71072">iffMP</a>(const Theorem &e1, const Theorem &e1_iff_e2)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a36571dc56183d89cd36def27939430b0">incomplete</a>()</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a7725800ff83f210545f44c6eef346ee2">incomplete</a>(std::vector< std::string > &reasons)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a289340e4457a79f1101f37c3a07a49ed">inconsistent</a>()</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [inline, virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a5c7d2aa7db5db78829b8558d28560ddf">inconsistentThm</a>()</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ac5b53deab8186f2c2b48e9916f09801e">initTimeLimit</a>()</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a6b1c155465b0c24885213e7442dd0882">installID</a>(const std::string &name, const Expr &e)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ac3c2ee71df31487191401722ea1d235a">inUpdate</a>()</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ac79ad21d2aeee1d50ce53ab7f3a76eba">isBasicKind</a>(int kind)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a8d466120560b7b91dc279e657fe3c433">isLeaf</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#aa0ef53bc2009d92763e0916c38aaf692">isLeafIn</a>(const Expr &e1, const Expr &e2)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a8dd39cad11cf866afc6282475cfc81b7">leavesAreSimp</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a61a4a3159152e1ff93dea55a33441557">lookupFunction</a>(const std::string &name, Type *type)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a4e57c5fb189f51c6e5abeeb0bcb1baef">lookupTypeExpr</a>(const std::string &name)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a4b58aeebc3a62e41f0ce71ba01fa3961">lookupVar</a>(const std::string &name, Type *type)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a9563215d97859a27f661c1517614f6ceaa35ba8e293104fb62e9163b4c036386b">LOW</a> enum value</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a97642364c244b753d33b551fc8c3bb9a">newFunction</a>(const std::string &name, const Type &type, bool computeTransClosure)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#ac6c5f95bbc428cad8085b416cd40292a">newFunction</a>(const std::string &name, const Type &type, const Expr &def)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#af85a563480c411b1e8eb280de9f39bb2">newSubtypeExpr</a>(const Expr &pred, const Expr &witness)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#aadde006d0dea508fec039b8092b14ed6">newTypeExpr</a>(const std::string &name)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a7aadedb0affc98a4cd1741f5dcf42d3a">newTypeExpr</a>(const std::string &name, const Type &def)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a4f82b4903d68da2bd83afb104c2c62cc">newVar</a>(const std::string &name, const Type &type)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#aa7b6e0e6f53256fd0e5573ad51ae472b">newVar</a>(const std::string &name, const Type &type, const Expr &def)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a9563215d97859a27f661c1517614f6cea1c0ce47707a6729f337134fc3239ef07">NORMAL</a> enum value</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="group__Theory__API.html#ga30a5750a0c38416c847e411c7400214a">notifyInconsistent</a>(const Theorem &thm)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline, virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a2f6f4b38fe4582c8f979f35842284b4c">numImpliedLiterals</a>()</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a753057879f8565c504f162c13d0185a2">okToEnqueue</a>()</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#abf168c0ef6bed9274e49dc2c0576312e">outOfResources</a>()</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a6f367b1f413d7f1275e72381724ca148">parseExpr</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a0cf4d5c76db5be87a848d694adff4dfe">parseExprOp</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ac173889ba81d910884901b3fa32e600c">parseExprTop</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ab334f07590ad297ad6daa3383c61de5f">print</a>(ExprStream &os, const Expr &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a2856680de1938c077d7b25c865992de6">printSmtLibShared</a>(ExprStream &os, const Expr &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#aabb093a909384e36c8780e433453358a">processCond</a>(const Expr &e, int i)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a36cd038dd5644d4a2bd6ea56cec2212e">processFactQueue</a>(EffortLevel effort=NORMAL)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a728d9c7d448cc32f58292677e7b5aae2">processNotify</a>(const Theorem &e, NotifyList *L)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a846416a29d02c4f2615f4de65e042cac">processUpdates</a>()</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a6822c229c357d1afcda22bc073d45142">refineCounterExample</a>()</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a22920ae8b347ea919e53e6e009b13ce0">refineCounterExample</a>(Theorem &thm)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#af860f5d5e01423628c97c399606916ff">reflexivityRule</a>(const Expr &a)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ade1177fbf32e95b9433eb608c82857d7">registerAtom</a>(const Expr &e, const Theorem &thm)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="group__Theory__API.html#gaae6aca3030e9857d149b8ea26c44b535">CVC3::Theory::registerAtom</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline, virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#afb6629080bceb44023f1bb3a44f9136f">registerCoreSatAPI</a>(CoreSatAPI *coreSatAPI)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a41499be2b31d82e7bec5efc880126510">registerKinds</a>(Theory *theory, std::vector< int > &kinds)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a97a6f8e09f71513da969fa7847346c6f">registerTheory</a>(Theory *theory, std::vector< int > &kinds, bool hasSolver=false)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a07c2391015494b5f71def510c1fb6e26">renameExpr</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a07b326cd94b2bb8bafa39faf07caaec5">resolveID</a>(const std::string &name)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a54bce613a6b49a9a8a1a888ec36346d8">rewrite</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#aba1822f2d985b50f6405c290c3814c1a">rewriteAnd</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="group__Theory__API.html#gaacb9782eae3d1121c415cd4b7650025c">rewriteAtomic</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline, virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a2d91d71489b0c0a9822cef765326bc89">rewriteCC</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ad0643e3175b0c8fd270b044b02999de9">rewriteCore</a>(const Theorem &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a84a6096579ca77dda6b673da7f1fce7c">rewriteCore</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a0f2e0c6647ff6282ee2f65116a82e13b">rewriteIte</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a8ba8c93d75329369b8d91f37a463ef09">rewriteLitCore</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a586e77e855946fd0b5f541ec06f7decd">rewriteLiteral</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#ad58c336212c2669f3cf32c0915ee3788">rewriteOr</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a63e4ccd049c6191c675fe8ad4bf1979f">setFindLiteral</a>(const Theorem &thm)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a1589ba9f082079a4dce4c9125befcf06">setIncomplete</a>(const std::string &reason)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private, virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a4a87431f344c128dc58d5c2bd9206784">setInconsistent</a>(const Theorem &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a2e0118c395ece4dfcfae018628e3b08b">setInPP</a>()</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a02c9e1bf2f581de6b8f8a8da5cbb5318">setResourceLimit</a>(unsigned limit)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a18c6f732488f868d08fb2a0516c2ef33">setTimeLimit</a>(unsigned limit)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#af4468d5d65b78ac9dc4c89c71c7391f6">setup</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [inline, virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a29cc343040a52a299a4f20123edf4c75">setupCC</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#af29a30b97ecc26f0c4b3136531487caf">setupSubFormulas</a>(const Expr &s, const Expr &e, const Theorem &thm)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#afbd6dec08ab7f31031ddc2a97d779bd8">setupTerm</a>(const Expr &e, Theory *i, const Theorem &thm)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#adaea4aa951adbe1561f7b445517378b6">setUsed</a>()</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline, virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a8a66da5ca687474a3a725448a3be8c41">simplify</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a9d441225b287419426c80a0374d6c6cb">simplifyExpr</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a3aefb5e53e848ad18a5846d5be42d3d2">simplifyOp</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a2128e2419413e5c0455ca3011fa2b2db">solve</a>(const Theorem &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a92e2da5223d7fb620cce85b2813e047f">substitutivityRule</a>(const Op &op, const std::vector< Theorem > &thms)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a83a1a0b30a27f887cef4c394544b30b0">substitutivityRule</a>(const Expr &e, const Theorem &t)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#abddfe81d6d08a46f1d1b3aa80ac565d5">substitutivityRule</a>(const Expr &e, const Theorem &t1, const Theorem &t2)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><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><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a56f710c79a9b3464189e8bb4d9d8a8c2">substitutivityRule</a>(const Expr &e, int changed, const Theorem &thm)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a7440711981ac1bba2bed7476c0fa4e0b">symmetryRule</a>(const Theorem &a1_eq_a2)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a1a2ffa9c7365e9f0af36fbd83e2421ed">tccCache</a>()</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#abe20cc4b804d6951c09b92aec0085063">Theory</a> class</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [friend]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a8fa244df7dcd091e8a5c3381053cc394">CVC3::Theory::Theory</a>(TheoryCore *theoryCore, const std::string &name)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a90684d2a97738341c00f8f9c99af7b66">theoryCore</a>()</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#acd5196a42683a0f357560588d4e81817">TheoryCore</a>(ContextManager *cm, ExprManager *em, TheoremManager *tm, Translator *tr, const CLFlags &flags, Statistics &statistics)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a01fa8047ed1f649dc98831cb536187e4">theoryOf</a>(int kind)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#ad4fea3e52e80f6ea2fb1a1eaaa7163b8">theoryOf</a>(const Type &e)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a9ea78dba89246dda6c504c7af5201f1b">theoryOf</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="group__Theory__API.html#gab66d477fcc5c27075a25dbfec4988537">theoryPreprocess</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline, virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a5dad9fa356483782703a1ef1024d2a74">theoryUsed</a>()</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline, virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a226706d3c1ddda709f4b09ec2a4b55bb">timeLimitReached</a>()</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a76f6507116e36f46dab074781fb9bf2d">transitivityRule</a>(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#ab8835beee96db67f3c26a604d96f2fe8">trueExpr</a>()</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a69cd86a10c207d95ded425684c5527b9">typePred</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#aafdee81857fde584632759c78ed821f5">unregisterKinds</a>(Theory *theory, std::vector< int > &kinds)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a6bdcdfdf6d658b1b1b7c548ea4782e6e">unregisterTheory</a>(Theory *theory, std::vector< int > &kinds, bool hasSolver)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#a435e2305420c1ed5b2ff1e4758a50dc5">update</a>(const Theorem &e, const Expr &d)</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#a0b9e5a75b0e23a334563392f075df9e2">updateCC</a>(const Theorem &e, const Expr &d)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#ad6cb45844df7f1b08a53e41e40a362e3">updateHelper</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1Theory.html#ac4527f940d280bca9ae279520fd1bc17">~Theory</a>(void)</td><td><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1TheoryCore.html#ad91cca07e2f1e8cd9614a6e88d6dd232">~TheoryCore</a>()</td><td><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a></td><td></td></tr>
</table></div>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
