<!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_1TheoryQuant.html">TheoryQuant</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="headertitle">
<div class="title">CVC3::TheoryQuant Member List</div> </div>
</div><!--header-->
<div class="contents">
<p>This is the complete list of members for <a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a>, including all inherited members.</p>
<table class="directory">
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#af1a7155ec3ea39cc6416e5889a6b06dc">add_parent</a>(const Expr &parent)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</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#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 class="even"><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><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 class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ac91bfb78e30e5f81d1d11a25a47f33b1">addNotify</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#aae3f95b1c6505b090105271bbccd7408">addSharedTerm</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</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#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_1TheoryQuant.html#a99d04925b72f6f7219bb759ef05a88e6">arrayHeuristic</a>(const Trigger &trig, size_t univid)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#acad8f385272425eabffcc518eacefbb4">arrayIndexName</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</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_1TheoryQuant.html#a98ceeca1859a3d4b0c01fc85a3f610ea">assertFact</a>(const Theorem &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</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_1TheoryQuant.html#ac4aaca08cc3081e899b3f771a8a37a37">backList</a>(const Expr &ex)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</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#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 class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#aaab4c2084e0104f66d12fd9d08b9823b">cacheHead</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a8cfa16216ec725f8b63ce5071c311b37">canMatch</a>(const Expr &t1, const Expr &t2, ExprMap< Expr > &env)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="group__Theory__API.html#gacdab59f42f5124655275d2e08e7aa0e3">checkAssertEqInvariant</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">inline</span><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#af8346007d3494f2c89687e8b14dc86a3">checkSat</a>(bool fullEffort)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="group__Theory__API.html#gac22e5fff02a4681c3972e3637bd15748">checkType</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_1TheoryQuant.html#afd3873e6105a187cba1e1c364c6b06d1">collectChangedTerms</a>(CDList< Expr > &changed_terms)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a211c3255d97a25eb0041ec8738d78a53">combineOldNewTrigs</a>(ExprMap< ExprMap< std::vector< dynTrig > * > * > &new_trigs)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="group__Theory__API.html#gaa29925192ee19a6d1f0644174cfd07af">computeBaseType</a>(const Type &tp)</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="group__Theory__API.html#ga4a5b9fff88df80582fc76fd3def55002">computeModel</a>(const Expr &e, std::vector< Expr > &vars)</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="group__Theory__API.html#ga6a6bc2982a8c71475cd9f1b6a4aa388e">computeModelBasic</a>(const std::vector< Expr > &v)</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="group__Theory__API.html#ga37309ea20a161f2529cbb0ab79f9ed3f">computeModelTerm</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"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ac702ce1fbdd3fee29f4b1c8868579276">computeTCC</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#aa48359564f5cfda755d46d1aed992dc8">computeType</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="group__Theory__API.html#ga19d53b411ccc48276f6666183b3c5887">computeTypePred</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"><span class="mlabel">inline</span><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a493eb80061815c95bab507f41343b260">createProofRules</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#aa6905effa7a717856118ed19f818e7f3">d_abInstCount</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a5ba728c791a6e156c1e1252698656154">d_all_multTrigsInfo</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ad705af0d0dad0e43422b8f2b6c7f6885">d_allInstCount</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ab35f04d2883c028bd5a5abe0d7004e06">d_allInstCount2</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a257fa05e1227011338ff18b07bbd8ea7">d_allInsts</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ac1dc98cab588b291d74859884fc25f5e">d_allmap_trigs</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a6c0bfa341c282227a4a94e27d997bf01">d_allout</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a0dd41bdd27bbd7c71fc45749fb80ff96">d_alltrig_list</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a42bf4d8a8865547e765374f47c89a42d">d_arrayIndic</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a6ed4dff6a76e12a20c1b11cf2080106f">d_arrayTrigs</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a7e78eaa04046525a5655c6b012948357">d_bindGlobalHistory</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a7e9807fc95db1efef6f3ac955a034f85">d_bindGlobalThmHistory</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ad8356f54f8d013951ebfd9480e940867">d_bindHistory</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a4f00e0765ee64e22e984587a4579bde6">d_cacheTheorem</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a65a292cd648bd4af31f19ff9c7532ea4">d_cacheThmPos</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a0615dcf3f868ddbd02984a29e482427e">d_callThisRound</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ab4a7ed7a25824178d2a60fb9d2645632">d_contextCache</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a9f6efeac1026260673ddbf7f083504da">d_contextMap</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#aa859e8e5d08c4c4a64c110f956209b72">d_contextTerms</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a0353fa5170be84ed1feffc0adaea61b6">d_curMaxExprScore</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a0a9d848eb97d33e8c555015cb126c39b">d_eq_list</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#acc57bb5cdcafa8c1fbdf85c030e35d00">d_eq_pos</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a66b5c3d369b6e969015c566d86014e46">d_eqs</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#aecebd6c0ff45e853d495b3a940a34a65">d_eqs_pos</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#afeebec46ae80ed697b00a5da3e043576">d_eqsUpdate</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ad9e2ac11111d8068cd47101e914400ec">d_exprLastUpdatedPos</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a590efa99276b0b530def7c750931f0e0">d_fullTrigs</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a7f68f552fa0794f221bbceeb7918c167">d_gBindQueue</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a343bd1867fbb824c16f2bc376d031234">d_gfactLimit</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#adced7c9130c7f24e53f2553eae73246c">d_gUnivQueue</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a149311d8fb4973ba78aaef0b49fcdeb3">d_hasMoreBVs</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#aa0f0f35f81aad33349edb9a4ae1f50c2">d_hasTriggers</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a712b1f8b6128c2f5290b02b16285fac4">d_indexExpr</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a8acfdb59fc63cde21b7d9ec22796756d">d_indexScore</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a97c18d8746ce2afdd83a9e12c84cdd24">d_inEnd</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a7e5a0fbbbe03ac62ae2fe52ea6768988">d_initMaxScore</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a9bc78df3616eacf20e564a08c8a9896f">d_instCount</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#aabd606d2811108af2cd562c63d9cfbdd">d_instHistory</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a66b101a27d3ee2d8494a6cb268e1ef8c">d_instHistoryGlobal</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#afbc66a1d0e321ce140c1db73d22d2551">d_insts</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a42b268e32a020cedcca5c58efd84c114">d_instThisRound</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a8182fa76e03957abb77e540861c4db40">d_lastArrayPos</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a5d4d5c909890619d446f8e1563d86e60">d_lastEqsUpdatePos</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#adb2db1fc47d328213e2f8bef1de71b88">d_lastPartLevel</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ac84aea59c42a90500d10f8604e7eb822">d_lastPartPredsPos</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a9141a0d67cecc9180e1838b1e03f2062">d_lastPartTermsPos</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ad1c890b18078d4c9ce5ef49517f539c4">d_lastPredsPos</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ada0a9362e554f531636059ba0f128ac9">d_lastTermsPos</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a949092aaf1aba7329ab512031f8399cc">d_lastUsefulGtermsPos</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#aa223ccaf4a6297fbe9243905f2fa1cd3">d_maxIL</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a5c321d21dbbf2e23a772dec478dd6ade">d_maxILReached</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a5f3ae02fd56df2f401da18b10ffc068b">d_maxInst</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ac5ecfdb795d8741da3942e7e4ec19928">d_maxNaiveCall</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#aad0370d3aabc256eb298dfcc27229e72">d_maxQuantInst</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ab36ea36a9cc54b697a0d188f725558c1">d_mtrigs_bvorder</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a0026da40c823471fb89c809d5429213f">d_mtrigs_inst</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#abe536d22495efd45fcb3c35cadc3f417">d_multitrigs_maps</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ac1f7a57f263b0bbc3d2bd87e7a931598">d_multTriggers</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ab3d76fe9a84814d0493dc47928450be1">d_multTrigs</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#af51bfd58e92b284832770c68c1685ab6">d_mybvs</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#adb5ce0ce6808f4d60284a2658256a772">d_offset_multi_trig</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a33efe13ffba90a746bea195b8892a437">d_parent_list</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a777ab16b886b05ea63180e44bd62fe43">d_partCalled</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ab00d303da385069d53e20c8fe52248b0">d_partTriggers</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a9b64987d5098fd227f10b45e0365da63">d_partTrigs</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a98562e5cbaac2c2abec9a0814726e990">d_rawUnivs</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a54e9b1c666a443f2fd4b8abf48077f5b">d_rawUnivsSavedPos</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a402f8b86c479687a21ff3e71581e9cd4">d_rules</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ab211a218c1b6d7f99ce2310730b27bbb">d_same_head_expr</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a2090a926ff4120c1f417693974afd49e">d_savedCache</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a151130d7ab3011be448ea16b0eb96156">d_savedMap</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ab8eafb65bdcded93b43a311e65d80051">d_savedTerms</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a12325d3d4d8cd79170c4cf3ec61a511f">d_savedTermsPos</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a20237cf6afe027d65533f121fa9baa8d">d_simplifiedThmQueue</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#aa05d5ab159323722c0c86f7bbbd4fa73">d_subTermsMap</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#afa26420c222cf2a7f47c09842b164307">d_tempBinds</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><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 class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#acb9e190ab07b49b4d1e62c4edbf75ca5">d_thmCount</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a96b6c0364f1b8e2aa6f5156eb7bfe469">d_totalInstCount</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a3e97f6a9759fca392443aee3d9ef0c0d">d_totalThmCount</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a1c1cea4c4d5aa9cd0e85233daf082a14">d_trans2_found</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a21177e07fa85adab68a40245f7b56dc7">d_trans2_num</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a5988b551d392a2675afe20061c374387">d_trans_back</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a09130b8c278fc53d6b978144fc060b88">d_trans_forw</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a40d9d2a6ac497d8925d85b1534f927fe">d_trans_found</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a32a16dc1f3abd4bb2923512863dad2e3">d_trans_num</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#affe271f96919ed4bb74e331159573d03">d_translate</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ab4cd6dafd73a1cdb2ce8d0bfa68975f5">d_transThm</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ab3e1ed0e8cc74fac887ded9f56a17f78">d_trueInstCount</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a99ff15c8d97f8c5539d744d077679bbd">d_typeExprMap</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a8c837bb9045c09ceb44d135e13f1788a">d_univs</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a0388d31f826f4786e14d252726c8c26a">d_univsContextPos</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a49b552d6d70733a9c6dd60eee5a2a646">d_univsPartSavedPos</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a8b5e246c61121a22421d550d4376d3f0">d_univsPosFull</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a216345a29be8f6c9e135b656e16fd4ca">d_univsQueue</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a78e66cea83a0bd258f7c7064bac4808c">d_univsSavedPos</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a307d487df3c5ba9770f4f2c99a1ce912">d_useCompleteInst</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ab6987761a0573b5a1f96be74f5be6594">d_useEqu</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a8f7f76c25794e58a8bbd35bbb37e3aed">d_useExprScore</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ae2aa24cf865298deb21463f1c64cefed">d_usefulGterms</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ae765160d5df0404da2d869a19ce3392d">d_useFullTrig</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a2dc4c4cd98dd966b17a705399db80bd4">d_useGFact</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a1caf0d9c2c9ff8ac77123921158e781c">d_useInstAll</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#aed3aa4f475cb2d920dcc137009aa208c">d_useInstGCache</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ae18bcd5e6dd77c740c08a37a90face8d">d_useInstLCache</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a0cb98a0e60550b47b6cf62d58ef7526c">d_useInstThmCache</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a26af226b922851112e91577ca7e3b452">d_useInstTrue</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a71f7265b98a79dff4f924fa84c6720d5">d_useLazyInst</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a2a8534b65e4c74e2c28c98f297b931e0">d_useManTrig</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ad0bf093cc6fe61456b2d186333fa1476">d_useMult</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a94cdc6b5d40ea0d468176829f3b7cc7f">d_useMultTrig</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ae3655c358b7c2b206c7a467eb7cc4880">d_useNaiveInst</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a941345e490bc23ed9454bc98513fafb2">d_useNew</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ad7cb228fd0c997d6d0cb92ebdf36f0d4">d_useNewEqu</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#aa6c894d36bb697a93713950312593e53">d_usePart</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a43d925d46b17106af6676a693bb3e81c">d_usePartTrig</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a7285a10b61c56f1abd386d15da664341">d_usePolarity</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a40f07b217c6934bba4480207f798eea2">d_usePullVar</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a6849ba1ee187928b1c254722525f8c5e">d_useSemMatch</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a6bde73c972d4bfc46683279e6c18b7df">d_useTrans</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a596216803168d232d335c3a2e7b35a02">d_useTrans2</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a1f1f4c18fe0c68dfb7eea0d3bd0220db">d_useTrigLoop</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a915c35bc6dedbc7827f8800fa9d2ac44">debug</a>(int i)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a7ee722984f64a327d4afd1d44915c94c">defaultDivideExpr</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#adaebb75807818796d34d2ff776755528">defaultMinusExpr</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a52e766e9bd39c2061de7c46368fd28e0">defaultMultExpr</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ae722d51a41c8bbfb71262033b5366267">defaultPlusExpr</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ab47f89174cf6213f2379e9df4eef8bec">defaultPowExpr</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ac3c6c90503e2a63b01cb71aec8e67959">defaultReadExpr</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a8c198e6cf92b67913a4c2eeba3049591">defaultWriteExpr</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a7cefd1998194a1bfb4025c51202f3a33">delNewTrigs</a>(ExprMap< ExprMap< std::vector< dynTrig > * > * > &new_trigs)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</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_1TheoryQuant.html#a9c0b1e3cb9cdd4a69f70cc912c14d438">enqueueInst</a>(const Theorem, const Theorem)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a7ced42bc689f825bb5dfccd859b0132f">enqueueInst</a>(const Theorem &univ, const std::vector< Expr > &bind, const Expr &gterm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#aa4aeaa406635cd716a4662cb856959ce">enqueueInst</a>(size_t univ_id, const std::vector< Expr > &bind, const Expr &gterm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ad43fa5b4cb57284f026897681af4ec3f">enqueueInst</a>(const Theorem &univ, Trigger &trig, const std::vector< Expr > &binds, const Expr &gterm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</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_1TheoryQuant.html#a8592168894e51ae87e4c765ba64f5d4c">exprMap2string</a>(const ExprMap< Expr > &vec)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#adf21f465d1b5579bd540535993f0fb3e">exprMap2stringSig</a>(const ExprMap< Expr > &vec)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a08ba0747b982df3234846c79e2c184a9">exprMap2stringSimplify</a>(const ExprMap< Expr > &vec)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</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_1Theory.html#a08412b310cb743536f7edd9fccd60e46">findExpr</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a652fbf4d1d2a11fc048e0cedcb8d69e1">findInstAssumptions</a>(const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#ab46ce7e7b6c9425a42df38ccf56642b6">findReduce</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#ad0f5335bae1a358802ec5b958e77934e">findReduced</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a89a91d7480d5783fb0c0f67f2fdb7873">findRef</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="group__Theory__API.html#ga166b2a0c7ec3b09e079c2f84bb6087bc">finiteTypeInfo</a>(Expr &e, Unsigned &n, bool enumerate, bool computeSize)</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_1TheoryQuant.html#a009ef12073c14fb4f18c0d05fd166c11">forwList</a>(const Expr &ex)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a14f9823bc4dbe53b96c895bafa71df1a">generalTrig</a>(const Expr &trig, ExprMap< Expr > &bvs)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><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 class="even"><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><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a50802b148e8192178cf790e6c45ddff3">getCommonRules</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e">getEM</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a8e31abf45d65f6893471be5611aa9f2e">getExprScore</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a26d25a02f8647a37593d84c75e23d78c">getHead</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a1de92cf7646580a4c25596cd91a0ece4">getHeadExpr</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</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_1TheoryQuant.html#aa1e8210488cd01cfc4b36c105b0f8484">getSubTerms</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#af38bdeb162a9ab9bd81ce40f598f608f">getTCC</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a39539e895f8aade88ae5bc05bbcc9302">getTypePred</a>(const Type &t, const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a068a9d83c75c80f1cb92104570bb1bac">goodSynMatch</a>(const Expr &e, const std::vector< Expr > &boundVars, std::vector< std::vector< Expr > > &instBindsTerm, std::vector< Expr > &instGterm, const CDList< Expr > &allterms, size_t tBegin)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a9efbf461e32e3c55fb05c8828f1ccac7">goodSynMatchNewTrig</a>(const Trigger &trig, const std::vector< Expr > &boundVars, std::vector< std::vector< Expr > > &instBinds, std::vector< Expr > &instGterms, const CDList< Expr > &allterms, size_t tBegin)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a2f46eef5c7af44f3880ccf179e3eb528">goodSynMatchNewTrig</a>(const Trigger &trig, const std::vector< Expr > &boundVars, std::vector< std::vector< Expr > > &instBinds, std::vector< Expr > &instGterms, const Expr &gterm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#acd5769f981e6fbefb01c35459836682f">hasGoodSemInst</a>(const Expr &e, std::vector< Expr > &bVars, std::set< std::vector< Expr > > &instSet, size_t tBegin)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a32914adfab6f1127e54e77789507f7e2">hasGoodSynInstNewTrig</a>(Trigger &trig, const std::vector< Expr > &boundVars, std::vector< std::vector< Expr > > &instBinds, std::vector< Expr > &instGterms, const CDList< Expr > &allterms, size_t tBegin)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a0529a0896f101fc28d0bda6a06a30017">hasGoodSynInstNewTrigOld</a>(Trigger &trig, std::vector< Expr > &boundVars, std::vector< std::vector< Expr > > &instBinds, std::vector< Expr > &instGterms, const CDList< Expr > &allterms, size_t tBegin)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a133000dab6d34bc6686aa55b67a7820a">hasGoodSynMultiInst</a>(const Expr &e, std::vector< Expr > &bVars, std::vector< std::vector< Expr > > &instSet, const CDList< Expr > &allterms, size_t tBegin)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</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#a8dc9b3350f948ce5b6112a4812819696">hasTheory</a>(int kind)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#aa3dcc4288e4738de508875ecccbe32eb">help</a>(int i)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"></td></tr>
<tr class="even"><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><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 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_1TheoryQuant.html#a501db08125b03768f4f270c3d4a251e0">instantiate</a>(Theorem univ, bool all, bool savedMap, size_t newIndex)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a02124fe37089a15098eddb145fef3541">insted</a>(const Theorem &univ, const std::vector< Expr > &binds)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</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_1TheoryQuant.html#aa837ec5c9ce0d4363fbb47eade316008">isTrans2Like</a>(const std::vector< Expr > &all_terms, const Expr &tr2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a243490ead7aaf5a0a311076661f783d1">isTransLike</a>(const std::vector< Expr > &cur_trig)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a2b83e2b6ed406fab48b51aad5bed441b">iterBKList</a>(const Expr &sr, const Expr &dt, size_t univ_id, const Expr &gterm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#aa695cc36069a55cb32ed84963093bd9d">iterFWList</a>(const Expr &sr, const Expr &dt, size_t univ_id, const Expr &gterm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</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#a8dd39cad11cf866afc6282475cfc81b7">leavesAreSimp</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a40cb1864bfcfedf2f6b20db57ba662ed">loc_gterm</a>(const std::vector< Expr > &border, const Expr &gterm, int pos)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a61a4a3159152e1ff93dea55a33441557">lookupFunction</a>(const std::string &name, Type *type)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a4e57c5fb189f51c6e5abeeb0bcb1baef">lookupTypeExpr</a>(const std::string &name)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a4b58aeebc3a62e41f0ce71ba01fa3961">lookupVar</a>(const std::string &name, Type *type)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a151e98ce89abebbe306580f7fcd06704">mapTermsByType</a>(const CDList< Expr > &terms)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a8631dcdf3e42b922ea500115b2f70629">matchListNew</a>(ExprMap< ExprMap< std::vector< dynTrig > * > * > &new_trigs, const CDList< Expr > &list, size_t gbegin, size_t gend)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a7aa91c8e11e7d0058082d1be9e5cb851">matchListOld</a>(const CDList< Expr > &list, size_t gbegin, size_t gend)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#aa7c01b86ccf4a315711e7d09c47c71cd">MAX_TRIG_BVS</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span><span class="mlabel">static</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#addac94f519d0c54d739281e72989a669">multMatchChild</a>(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, bool top=false)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</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_1TheoryQuant.html#a036828f1d240572e4a37e22af4d79d06">multMatchTop</a>(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a8ccfdf955d67688e51dc9bcbb3911a2d">naiveCheckSat</a>(bool)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a97642364c244b753d33b551fc8c3bb9a">newFunction</a>(const std::string &name, const Type &type, bool computeTransClosure)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#ac6c5f95bbc428cad8085b416cd40292a">newFunction</a>(const std::string &name, const Type &type, const Expr &def)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#af85a563480c411b1e8eb280de9f39bb2">newSubtypeExpr</a>(const Expr &pred, const Expr &witness)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a9f44d577beb7d01fa993ec72c8e144b9">newTopMatch</a>(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, const Trigger &trig)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#adbebf5bb207253848504a3711ddab1c9">newTopMatchBackupOnly</a>(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, const Trigger &trig)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a663ab694805834cbb8af2e3e1c0a07b0">newTopMatchNoSig</a>(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, const Trigger &trig)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#abf931ce810d553219994f72b7098a5d0">newTopMatchSig</a>(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, const Trigger &trig)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</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#aadde006d0dea508fec039b8092b14ed6">newTypeExpr</a>(const std::string &name)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a7aadedb0affc98a4cd1741f5dcf42d3a">newTypeExpr</a>(const std::string &name, const Type &def)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a4f82b4903d68da2bd83afb104c2c62cc">newVar</a>(const std::string &name, const Type &type)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#aa7b6e0e6f53256fd0e5573ad51ae472b">newVar</a>(const std::string &name, const Type &type, const Expr &def)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#acfc01954af4379d6ee3917afbdb73612">notifyInconsistent</a>(const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a48b9c68f68437b817726cedaf097a531">null_cdlist</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</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#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_1TheoryQuant.html#a4ddfed955f288872e94794075f019c9f">parseExprOp</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#aa60a22e8795e5046cd17d016d40705b2">partial_called</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#aa0c1c26775ebf349dbaa34e7a0dfc268">print</a>(ExprStream &os, const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a641298c9d293b81af61f5de825b3324a">pushBackList</a>(const Expr &node, Expr ex)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</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_1TheoryQuant.html#a88227f7c82c03ffd8ad44a959cc47554">pushForwList</a>(const Expr &node, Expr ex)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a6177e4b547322f04e6ff282521120a37">recGeneralTrig</a>(const Expr &trig, ExprMap< Expr > &bvs, size_t &mybvs_count)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a8e4d77afeb2cf976688bc923b3c7b3d4">recGoodSemMatch</a>(const Expr &e, const std::vector< Expr > &bVars, std::vector< Expr > &newInst, std::set< std::vector< Expr > > &instSet)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a9e3bb4497a71d84322a8f97a86d2b11c">recInstantiate</a>(Theorem &univ, bool all, bool savedMap, size_t newIndex, std::vector< Expr > &varReplacements)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#aede3f8a2e1b235a5cafde5f62a3356cf">recMultMatch</a>(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a6105760e18793163cafd935f92214b57">recMultMatchDebug</a>(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a017c02318b460823b9e5e63b8b72a14f">recMultMatchNewWay</a>(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a22391b53ffa8331b754fb7ad85b58ec0">recMultMatchOldWay</a>(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a21e6b9a3115caa0b22322bd75d883347">recSearchCover</a>(const std::vector< Expr > &border, const std::vector< Expr > &mtrigs, int cur_depth, std::vector< std::vector< Expr > > &instSet, std::vector< Expr > &cur_inst)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a33dfaf67440a78f618a6c379fd884330">recSynMatch</a>(const Expr &gterm, const Expr &vterm, ExprMap< Expr > &env)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ad2e8ad874c79cb5300302d30b6475b7b">recSynMatchBackupOnly</a>(const Expr &gterm, const Expr &vterm, ExprMap< Expr > &env)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a184ff0daa00e9777c766aec5e1fc3015">recursiveMap</a>(const Expr &term)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="group__Theory__API.html#gab23238889b7f68caa0715e6ab5d31775">refineCounterExample</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#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><td class="entry"><a class="el" href="group__Theory__API.html#gafb1431aa8258f6663ad948ebb08e5330">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="group__Theory__API.html#gaae6aca3030e9857d149b8ea26c44b535">registerAtom</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#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 class="even"><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><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ad7f534d41a6c648eb5fbad4bbc1c92a1">registerTrig</a>(ExprMap< ExprMap< std::vector< dynTrig > * > * > &cur_trig_map, Trigger trig, const std::vector< Expr > thmBVs, size_t univ_id)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ad9323b081878d5b80294cd48b68dd8a1">registerTrigReal</a>(Trigger trig, const std::vector< Expr >, size_t univ_id)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><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 class="even"><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><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#aaed061533566d5aa74f4195a6eece020">rewrite</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</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_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><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 class="even"><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><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 class="even"><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><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a3417f85c140e902187726b52a4628966">saveContext</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a681dfda538563ad8b07372fde28947e9">searchCover</a>(const Expr &thm, const std::vector< Expr > &border, std::vector< std::vector< Expr > > &instSet)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#afe19c7bd637cb0c5fad7ab0494135010">semCheckSat</a>(bool)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a4d6102e7b0c820e32c1488da4b19e140">semInst</a>(const Theorem &univ, size_t tBegin)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a66e269df47eb8d5827b10c15937c6432">sendInstNew</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a108c813a9b45447451b2230e9ad26801">setGround</a>(const Expr &gterm, const Expr &trig, const Theorem &univ, const std::vector< Expr > &subTerms)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</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_1TheoryQuant.html#a9ed056909d84ff32d1768bce20ba3480">setTrans2Found</a>(const Expr &comb)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a2839204961cc646d22f8dfd3c1c53575">setTransFound</a>(const Expr &comb)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</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_1TheoryQuant.html#a8669c171bcd467dc782f4268093cab11">setup</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</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_1TheoryQuant.html#a892fb1c6479c80fe7cab50a156d04b97">setupTriggers</a>(ExprMap< ExprMap< std::vector< dynTrig > * > * > &trig_maps, const Theorem &thm, size_t univs_id)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#adaea4aa951adbe1561f7b445517378b6">setUsed</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a52158688456f8605b064fbbf7a46039c">simplify</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a9d441225b287419426c80a0374d6c6cb">simplifyExpr</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a1422df86ad2222a61bfd19e71bb36d37">simplifyExprMap</a>(ExprMap< Expr > &orgExprMap)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="group__Theory__API.html#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><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a510dde7cfaa1f736d1507efb0f630622">simplifyVectorExprMap</a>(std::vector< ExprMap< Expr > > &orgVectorExprMap)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ad3380307e5e4a152e9cbd4595931dc3a">simpRAWList</a>(const Expr &org)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="group__Theory__API.html#ga3908ecb66d7ba9830e7cf5d1a8ab91c3">solve</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">inline</span><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a92e2da5223d7fb620cce85b2813e047f">substitutivityRule</a>(const Op &op, const std::vector< Theorem > &thms)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a83a1a0b30a27f887cef4c394544b30b0">substitutivityRule</a>(const Expr &e, const Theorem &t)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#abddfe81d6d08a46f1d1b3aa80ac565d5">substitutivityRule</a>(const Expr &e, const Theorem &t1, const Theorem &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a8ab61a1574ac8c29db7ddb5b0d45235b">substitutivityRule</a>(const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a56f710c79a9b3464189e8bb4d9d8a8c2">substitutivityRule</a>(const Expr &e, int changed, const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a7440711981ac1bba2bed7476c0fa4e0b">symmetryRule</a>(const Theorem &a1_eq_a2)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a52ca7d3454b8359a1aee518b57f9720a">synCheckSat</a>(ExprMap< ExprMap< std::vector< dynTrig > * > * > &, bool)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a230e85344be8da88669b0c7a3f6664c3">synCheckSat</a>(bool)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a7db6cfe00994c2a42281569e9adb464a">synFullInst</a>(const Theorem &univ, const CDList< Expr > &allterms, size_t tBegin)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a1e1906aefb76bb94539706422769ca56">synInst</a>(const Theorem &univ, const CDList< Expr > &allterms, size_t tBegin)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#abe90a3995031ac7ab9e020be4bf828a2">synMatchTopPred</a>(const Expr &gterm, const Trigger trig, ExprMap< Expr > &env)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a49dcf36058067da8bb3746c6c675e586">synMultInst</a>(const Theorem &univ, const CDList< Expr > &allterms, size_t tBegin)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#ae568ecab36a477db5114c8f7a53e3755">synNewInst</a>(size_t univ_id, const std::vector< Expr > &binds, const Expr &gterm, const Trigger &trig)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a98757263b2fee18abdf1455940ac591a">synPartInst</a>(const Theorem &univ, const CDList< Expr > &allterms, size_t tBegin)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</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_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="classCVC3_1_1TheoryQuant.html#a2d5e93e866382db19e0675f693d14c32">theoryPreprocess</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</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_1TheoryQuant.html#aa78a307b46795fba7cd31d7459f5af4e">TheoryQuant</a>(TheoryCore *core)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a5dad9fa356483782703a1ef1024d2a74">theoryUsed</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a2c9aee5ef245bdf1536f58c17414f4f0">trans2Found</a>(const Expr &comb)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</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_1TheoryQuant.html#a192cb414dac910cbd803f82ad39df82e">transFound</a>(const Expr &comb)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a76f6507116e36f46dab074781fb9bf2d">transitivityRule</a>(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#ab8835beee96db67f3c26a604d96f2fe8">trueExpr</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a9530e1a16572ad8b35d7c3bd08c9803a">typeMap</a> typedef</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><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 class="even"><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><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 class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html#a03756dc7d7ff3b399cae1c98140eccb8">update</a>(const Theorem &e, const Expr &d)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a0b9e5a75b0e23a334563392f075df9e2">updateCC</a>(const Theorem &e, const Expr &d)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_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_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_1TheoryQuant.html#a653f0e36db9a5c07024565e77d01abb0">~TheoryQuant</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryQuant.html">CVC3::TheoryQuant</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>
