<!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_1TheoryRecords.html">TheoryRecords</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="headertitle">
<div class="title">CVC3::TheoryRecords Member List</div> </div>
</div><!--header-->
<div class="contents">
<p>This is the complete list of members for <a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a>, including all inherited members.</p>
<table class="directory">
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a13ba9024a22362cc96760519a84f2316">addBoundVar</a>(const std::string &name, const Type &type)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#aa8f3f9fb084f9d5e385255baab5dc8f3">addBoundVar</a>(const std::string &name, const Type &type, const Expr &def)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a688cd0c0b669ab9719f8a99cb207ad2c">addGlobalLemma</a>(const Theorem &thm, int priority=0)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="group__Theory__API.html#ga664e787b0eb7e5e6fdb03efeb409d38a">addSharedTerm</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#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_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_1TheoryRecords.html#ad7fd739c906e86c0b5a135374cc10dc0">assertFact</a>(const Theorem &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</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_1Theory.html#a705d998884ec8a53c22220373472d868">boolType</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="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 class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a4780c4692ecdb6fc82f181b86cebeb68">checkSat</a>(bool fullEffort)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</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_1TheoryRecords.html#a0fd20bc4ca8c7701c189ce465cd3641c">checkType</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a0cdc07a00c674c1190f721908a77c0ca">computeBaseType</a>(const Type &t)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a43f8bb4aeae98801e974b7f3fa0ed068">computeModel</a>(const Expr &e, std::vector< Expr > &vars)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</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#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><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a77c8993b2ad9daca3803c78991589351">computeModelTerm</a>(const Expr &e, std::vector< Expr > &v)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a2ae67fcdda4a2c2f55238adea0b8eabc">computeTCC</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a59dd99a5c7c1540d6517dc69dc157cfb">computeType</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a62ea35463c9093da92601e33698f905b">computeTypePred</a>(const Type &t, const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#acefe38731a5693d2c2b7d630088ee708">createProofRules</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a6bb9f23a660b77ee034a407bc46774dd">d_rules</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</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_1Theory.html#a93856c9af82b2c25c51b3c36bafb71f4">enqueueFact</a>(const Theorem &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#af833743a1332ba2b84bdc4118a05300f">enqueueSE</a>(const Theorem &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_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><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 class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a08412b310cb743536f7edd9fccd60e46">findExpr</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#ab46ce7e7b6c9425a42df38ccf56642b6">findReduce</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#ad0f5335bae1a358802ec5b958e77934e">findReduced</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a89a91d7480d5783fb0c0f67f2fdb7873">findRef</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#ac58f7129ed3e62d2d183922cb70428ac">finiteTypeInfo</a>(Expr &e, Unsigned &n, bool enumerate, bool computeSize)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"><span class="mlabel">virtual</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_1TheoryRecords.html#ac45307e001d2f373bdf4116416c84b77">getField</a>(const Expr &e, int i)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#ac64247bde64f8819221125be780f3a1d">getField</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a8b8cf0a921555538ec1b91c08600e721">getFieldIndex</a>(const Expr &e, const std::string &field)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#aaf09fd297eafe6e114863581c558f163">getFields</a>(const Expr &r)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#ab228944f5113535c5859cbaa2de0d811">getIndex</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#ad8b27aeea37d99def7a3c0348ded3e66">getModelTerm</a>(const Expr &e, std::vector< Expr > &v)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a4867f332c809f6efe8f01ffa45c32db3">getModelValue</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a4270eb556496ee10472b478b5792751c">getName</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#ab7c83d1e21c1553ff229447fe6d51530">getNumTheories</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#af38bdeb162a9ab9bd81ce40f598f608f">getTCC</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a39539e895f8aade88ae5bc05bbcc9302">getTypePred</a>(const Type &t, const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a8dc9b3350f948ce5b6112a4812819696">hasTheory</a>(int kind)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#aeda4c57dfbe357a80a348da9ffa71072">iffMP</a>(const Theorem &e1, const Theorem &e1_iff_e2)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#ab85541a91803599b7495f709c72c28c5">inconsistent</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a6b1c155465b0c24885213e7442dd0882">installID</a>(const std::string &name, const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_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><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 class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a5aee76070091906e4b5a710d2c1e2d5b">isRecord</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a09dac099c2d70610b91e30cd21e00fe1">isRecordAccess</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a71dfd95cef55ec88b9c2a29297542ab0">isRecordType</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a9944c0e052d60784eaffb8329db47a5f">isRecordType</a>(const Type &t)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a30d3306dd140e2ff2dbf3b145bb476cf">isTuple</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a8524c2c102a95e757b3c990b44e9576d">isTupleAccess</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a6c178cfcd9fd7e13a0c28ff28ce60f4d">isTupleType</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#af039aad415a0cc2be21c354d40c8f9aa">isTupleType</a>(const Type &tp)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</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#a8dd39cad11cf866afc6282475cfc81b7">leavesAreSimp</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_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_1Theory.html#a97642364c244b753d33b551fc8c3bb9a">newFunction</a>(const std::string &name, const Type &type, bool computeTransClosure)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#ac6c5f95bbc428cad8085b416cd40292a">newFunction</a>(const std::string &name, const Type &type, const Expr &def)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#af85a563480c411b1e8eb280de9f39bb2">newSubtypeExpr</a>(const Expr &pred, const Expr &witness)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#aadde006d0dea508fec039b8092b14ed6">newTypeExpr</a>(const std::string &name)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a7aadedb0affc98a4cd1741f5dcf42d3a">newTypeExpr</a>(const std::string &name, const Type &def)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a4f82b4903d68da2bd83afb104c2c62cc">newVar</a>(const std::string &name, const Type &type)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#aa7b6e0e6f53256fd0e5573ad51ae472b">newVar</a>(const std::string &name, const Type &type, const Expr &def)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="group__Theory__API.html#ga30a5750a0c38416c847e411c7400214a">notifyInconsistent</a>(const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_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_1TheoryRecords.html#a72f4af007baf95a36b21246433266319">parseExprOp</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#aad0935f7bc94c98934c0e1690b2ec850">print</a>(ExprStream &os, const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#aa5a9cbcd30ed23792c030d70181483d3">recordExpr</a>(const std::vector< std::string > &fields, const std::vector< Expr > &kids)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a179c7224344f4316c25ceb4626a6f2f0">recordExpr</a>(const std::vector< Expr > &fields, const std::vector< Expr > &kids)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a6123e229d2eac24364f4cf1b30927f0c">recordSelect</a>(const Expr &r, const std::string &field)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a4b298f0e7a25449c945480544996d105">recordType</a>(const std::vector< std::string > &fields, const std::vector< Type > &types)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a9a918c3cb8e49f04b4a8331eaf696c7c">recordType</a>(const std::vector< std::string > &fields, const std::vector< Expr > &types)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a4c7522da56902a7f3bd8a7b530a77dc5">recordType</a>(const std::vector< Expr > &fields, const std::vector< Expr > &types)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#ad6d5734bb5b21cada7e7958c6840e2c4">recordUpdate</a>(const Expr &r, const std::string &field, const Expr &val)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"></td></tr>
<tr class="even"><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><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#af860f5d5e01423628c97c399606916ff">reflexivityRule</a>(const Expr &a)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="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><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 class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a41499be2b31d82e7bec5efc880126510">registerKinds</a>(Theory *theory, std::vector< int > &kinds)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a97a6f8e09f71513da969fa7847346c6f">registerTheory</a>(Theory *theory, std::vector< int > &kinds, bool hasSolver=false)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a07c2391015494b5f71def510c1fb6e26">renameExpr</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a07b326cd94b2bb8bafa39faf07caaec5">resolveID</a>(const std::string &name)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a56d1048536807a3bb9d746c833b75c47">rewrite</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#aba1822f2d985b50f6405c290c3814c1a">rewriteAnd</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="group__Theory__API.html#gaacb9782eae3d1121c415cd4b7650025c">rewriteAtomic</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a243eef0e23027e100aede3646eca3617">rewriteAux</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a89f926d66c9b7b414160bb12f42f4485">rewriteAux</a>(const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a2d91d71489b0c0a9822cef765326bc89">rewriteCC</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a0f2e0c6647ff6282ee2f65116a82e13b">rewriteIte</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#ad58c336212c2669f3cf32c0915ee3788">rewriteOr</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a08cc815e21d2972f54f8c1e70ce8ab51">setIncomplete</a>(const std::string &reason)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a89f8e1e02e22ef524c286ce8b87bdea4">setInconsistent</a>(const Theorem &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a707f98454898e685084f75a006cdd100">setup</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><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 class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#adaea4aa951adbe1561f7b445517378b6">setUsed</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a52158688456f8605b064fbbf7a46039c">simplify</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a9d441225b287419426c80a0374d6c6cb">simplifyExpr</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="group__Theory__API.html#ga55b82868b8e9e60906756e797da9355a">simplifyOp</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="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><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a92e2da5223d7fb620cce85b2813e047f">substitutivityRule</a>(const Op &op, const std::vector< Theorem > &thms)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a83a1a0b30a27f887cef4c394544b30b0">substitutivityRule</a>(const Expr &e, const Theorem &t)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#abddfe81d6d08a46f1d1b3aa80ac565d5">substitutivityRule</a>(const Expr &e, const Theorem &t1, const Theorem &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a8ab61a1574ac8c29db7ddb5b0d45235b">substitutivityRule</a>(const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a56f710c79a9b3464189e8bb4d9d8a8c2">substitutivityRule</a>(const Expr &e, int changed, const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a7440711981ac1bba2bed7476c0fa4e0b">symmetryRule</a>(const Theorem &a1_eq_a2)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a8fa244df7dcd091e8a5c3381053cc394">Theory</a>(TheoryCore *theoryCore, const std::string &name)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a90684d2a97738341c00f8f9c99af7b66">theoryCore</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a01fa8047ed1f649dc98831cb536187e4">theoryOf</a>(int kind)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#ad4fea3e52e80f6ea2fb1a1eaaa7163b8">theoryOf</a>(const Type &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a9ea78dba89246dda6c504c7af5201f1b">theoryOf</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="group__Theory__API.html#gab66d477fcc5c27075a25dbfec4988537">theoryPreprocess</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a7f3fc16c1167afe2d6ff3da0a59c06fd">TheoryRecords</a>(TheoryCore *core)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a5dad9fa356483782703a1ef1024d2a74">theoryUsed</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a76f6507116e36f46dab074781fb9bf2d">transitivityRule</a>(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#ab8835beee96db67f3c26a604d96f2fe8">trueExpr</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a6633d0d5b34ebfaf5d6a42f72c8d4818">tupleExpr</a>(const std::vector< Expr > &kids)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#ada5d6a109788e70405af2adee937c379">tupleSelect</a>(const Expr &tup, int i)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a4ab484efb75ef41b5a29d5e598ab91a1">tupleType</a>(const std::vector< Type > &types)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#aaf96b1c14ffa1741f3dfadcca8bfa212">tupleType</a>(const std::vector< Expr > &types)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a7ca579aacef4b87f4b2235da4ef1ec47">tupleUpdate</a>(const Expr &tup, int i, const Expr &val)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a090c2b079f3b90b4f5da3d8606b14d16">typePred</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#aafdee81857fde584632759c78ed821f5">unregisterKinds</a>(Theory *theory, std::vector< int > &kinds)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a6bdcdfdf6d658b1b1b7c548ea4782e6e">unregisterTheory</a>(Theory *theory, std::vector< int > &kinds, bool hasSolver)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a070b5644bc6e362999305ee8bb3774ff">update</a>(const Theorem &e, const Expr &d)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a0b9e5a75b0e23a334563392f075df9e2">updateCC</a>(const Theorem &e, const Expr &d)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_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 class="even"><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><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html#a7e0ac2c2be6942fc04ce9c21951fe7a7">~TheoryRecords</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryRecords.html">CVC3::TheoryRecords</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:19 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>
