<!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_1TheoryBitvector.html">TheoryBitvector</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="headertitle">
<div class="title">CVC3::TheoryBitvector Member List</div> </div>
</div><!--header-->
<div class="contents">
<p>This is the complete list of members for <a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a>, including all inherited members.</p>
<table class="directory">
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a13ba9024a22362cc96760519a84f2316">addBoundVar</a>(const std::string &name, const Type &type)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#aa8f3f9fb084f9d5e385255baab5dc8f3">addBoundVar</a>(const std::string &name, const Type &type, const Expr &def)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a688cd0c0b669ab9719f8a99cb207ad2c">addGlobalLemma</a>(const Theorem &thm, int priority=0)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#aa17e44a8047fc0f5220565f6cd5a203f">additionalRewriteConstraints</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a3798dbe1339c1c376b35172fbbc6434b">addSharedTerm</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a605e960d2442b587046c562723b7f03a">addSplitter</a>(const Expr &e, int priority=0)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_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><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a70eefd32e475f3c04e195530145ae87f">assertFact</a>(const Theorem &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ac59b9ef8d3c7f68eee6a06ea17e3d104">assertTypePred</a>(const Expr &e, const Theorem &pred)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><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 class="even"><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><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#aa3c9c45c9989d45202d31dda4beb4386">bitBlastDisEqn</a>(const Theorem &notE)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a85512d4fcaee0050ee2b41dedd71c61c">bitBlastEqn</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a1381dbfdc07d3bdebe3a4b8f0172bb94">bitBlastIneqn</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a981e964dd8c6118cbcac5e0c2b307730">bitBlastTerm</a>(const Expr &t, int bitPosition)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><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_1TheoryBitvector.html#a3de9924e52bf35f61049f07f0d34529f">bvOne</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</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_1TheoryBitvector.html#adce40eaced94554fd76d2f660f5ba385">BVSize</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a2a6471d4278e92ffcaa981b39001fc8a">bvZero</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</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_1TheoryBitvector.html#a7d9bd17c1b561963bb05712071747090">canSolveFor</a>(const Expr &term, const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#aa1e382d50ad48fb6d222450d74dd9574">check_linear</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</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_1TheoryBitvector.html#a31df7eb073302681dd7aeedc57251d09">checkSat</a>(bool fullEffort)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a978cfa4add608e7f78c4e8b1d92e093f">checkType</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a1bf151ceda29668de133a3b005b9298b">comparebv</a>(const Expr &e1, const Expr &e2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></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="classCVC3_1_1TheoryBitvector.html#a08653884cd51197647ed006e5ae64332">computeBVConst</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a00182685c0c766dfdc560e3c5f00001b">computeModel</a>(const Expr &e, std::vector< Expr > &vars)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</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_1TheoryBitvector.html#a38b5fc9c8e39309a86634cc55ee116a0">computeModelTerm</a>(const Expr &e, std::vector< Expr > &v)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a9e49b77a0e80b7ba83bc77bb3a301c6b">computeNegBVConst</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a94d82875db6689ca7c986e24abf63a46">computeTCC</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#aad271001191bdd48d1b77d92d9558136">computeType</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a60d5dc6f4f252bbf62e9333134863da0">computeTypePred</a>(const Type &t, const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a79967704ae23c653a04a1ee3416a4d22">countTermIn</a>(const Expr &term, const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ae3141bc37e39e3379fa71d966c887426">createProofRules</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ad9f83106573a125c219c3900a9aeceb3">d_bb_index</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ad133cd123c7cc462dbeca98a1d10f8e4">d_bitblast</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a0f583ba86ce3c379097255ee97620652">d_bitvecCache</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a20f9ef1d8f1666eeb16e9f2712320132">d_booleanRWFlag</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#aa96498fb323044a4ab77c9657ac8e614">d_boolExtractCacheFlag</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ac219e3d5a18642506f3def182a023989">d_bv32Flag</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a071fce068ccf6223f20ba8a8d5b90b00">d_bvAssertDiseq</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ae855792c718e64c8a46dab88ddd8b1b4">d_bvAssertEq</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a2f2ac7c248fe89fc483c3a1a43c459db">d_bvBitBlastDiseq</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#aab7d49f889a88fd2373b722d33e21c31">d_bvBitBlastEq</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#aca1d99fa896f29efa540d8b83a4de848">d_bvConstExprIndex</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a563bcc4483ffa3aee6a8e44e5ab07bcd">d_bvDelayDiseq</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#af183050f385d720871a298207a7790b1">d_bvDelayEq</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#aefadf1146b79ded24d7f5a66adba069d">d_bvDelayTypePreds</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#aa4228ded9a53f6edcc7d06406f9c98c7">d_bvOne</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a6d5488901e86cf3db3fc473fc3770766">d_bvParameterExprIndex</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a2508ac260570adfa5584847830806cb0">d_bvPlusCarryCacheLeftBV</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a9fcf8c7246955aa2a8aa6be2fd3d4f64">d_bvPlusCarryCacheRightBV</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a96840bd0a2349e2cd33345a709e84907">d_bvPlusExprIndex</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ae58b98a947a495b8754413e336753518">d_bvTypePredExprIndex</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#aac1428f779c77033eb5c59b599629cb8">d_bvTypePreds</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a8be187368c2a0f4e0b401bc1c7968d19">d_bvZero</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#af8bcfa021f89dfbc8111eff923e48eab">d_eq</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ac017443fdd0f931d9283bc9e2b52d831">d_eq_index</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a7c8dcbb9ba2c1c307c403966cd0b0c6d">d_eqPending</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a8990b759675928a62a4d75cf69fe8d72">d_index1</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a2316b51cfa9b54740298ec7d5e6630cb">d_index2</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a1559e63e86e26b348ad8bb618f29f202">d_maxLength</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a2134631ced4e2db4bafac7755a4774f4">d_pushNegCache</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a36ce76cce9f4da02fe837fa6d99d6202">d_rules</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#aa899ef9e64b78453d199a84160f15444">d_sharedSubterms</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a59850cd32a8031dff8e8918c1e9d31c7">d_sharedSubtermsList</a></td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a262fdc338527489b376ec181ecc38ddc">d_theoryUsed</a></td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_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 class="even"><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><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a670ab645c15606c0653cd265c5378b52">extract_vars</a>(const Expr &e, std::vector< Expr > &vars)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></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_1TheoryBitvector.html#acc1ac9f10d2c91f9831057937fcba829">finiteTypeInfo</a>(Expr &e, Unsigned &n, bool enumerate, bool computeSize)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a0dedc2d6930e49cdf4d73c40da7a7bd8">generalBitBlast</a>(const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8">getBaseType</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a26afbc255a32b9fcff11d6b2625157ae">getBaseType</a>(const Type &tp)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a8e2bf7866c94979dfed7031a81c2e002">getBitvectorTypeParam</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a0d6c5357741846c314acfda3f93094a9">getBitvectorTypeParam</a>(const Type &t)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#aedf18fc1e6f9998ddaef98ab9273c2fb">getBoolExtractIndex</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a6d1c5d8e029a455d9bd058eb66c5cdc8">getBVConstSize</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a242600edbc48857be8abbab8e74ed3be">getBVConstValue</a>(const Expr &e, int i)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a2b61f3705b8789f652ea688ef331344f">getBVIndex</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a540b9b39838cb3c1b71925be3f5696fa">getBVMultParam</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a67259e3d5f08972e6a157f167aab7023">getBVPlusParam</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a50802b148e8192178cf790e6c45ddff3">getCommonRules</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e">getEM</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ad714ab7be58b17f2c120afa117abd1fb">getExtractHi</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#acbb820488811e04eed17d85199498ae9">getExtractLow</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#aafcc248e3361c69777cb1377a157db49">getFixedLeftShiftParam</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a801f0c6dd21ecfea0769abfcd7fd4b4e">getFixedRightShiftParam</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#af9b48795b632ce717e9f2149c99689fb">getMaxSize</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><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 class="even"><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><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 class="even"><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><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a7737e8531a34515a5d27afcb23bb314e">getSXIndex</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</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_1TheoryBitvector.html#a96385e1a741679ebbabe669b8ed4c5bf">getTypePredExpr</a>(const Expr &tp)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a697bd2ebc3d61f913039bf77bbdc3c51">getTypePredType</a>(const Expr &tp)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</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_1TheoryBitvector.html#afe606418dd434c720ec6cbec5dab3c1c">isLinearTerm</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a6739a946f5cdf86bd6597845b6f6df43">isTermIn</a>(const Expr &e1, const Expr &e2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</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#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_1TheoryBitvector.html#ab4f87aca710aa31e6d438e91301beffc">min</a>(std::vector< Rational > list)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a425367b8c2d69e637c93742ab1ed2134">multiplicative_inverse</a>(Rational r, int n_bits)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a265761c739bb7084fa9016e527499da5">multiply_coeff</a>(Rational mult_inv, const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a3d98cac1ae52614ee2adc3fbc407516e">newBitvectorType</a>(int i)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#aef4eb029a55a6822baa7c381262154e5">newBitvectorTypeExpr</a>(int i)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ad2f823cf9921323e80c510076dd20fa2">newBitvectorTypePred</a>(const Type &t, const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#aec57b42edc8ea39452039be2d93a26e7">newBoolExtractExpr</a>(const Expr &t1, int r)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ab22dd0ad8596f8fefce18f99b1791499">newBVAndExpr</a>(const Expr &t1, const Expr &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ac7cd7c2e0a03c30f3cec5ac5787d8d48">newBVAndExpr</a>(const std::vector< Expr > &kids)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a70d9bf0184ba1308434780a25439b402">newBVCompExpr</a>(const Expr &t1, const Expr &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a352c6547a3a7fba398cdd2b2ea391b22">newBVConstExpr</a>(const std::string &s, int base=2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a1aa46633fe05da5f22d43ee651229c93">newBVConstExpr</a>(const std::vector< bool > &bits)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ab5b4018be164d7f81fb9cdb1a3a1ca07">newBVConstExpr</a>(const Rational &r, int len=0)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a17a104b42804d41d9a11d15faf727166">newBVExtractExpr</a>(const Expr &e, int hi, int low)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a48a5a14c9e1efc9bc1d463d1be67fb1a">newBVIndexExpr</a>(int kind, const Expr &t1, int len)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ac6430938332eb644c11106ce5047825c">newBVLEExpr</a>(const Expr &t1, const Expr &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#aa849a2fd56e8a1e3a7742b00d043869a">newBVLTExpr</a>(const Expr &t1, const Expr &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ae601c7122d288358c50df9e27bd5a9df">newBVMultExpr</a>(int bvLength, const Expr &t1, const Expr &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ae53123881dda650f5722e10fdceb11d7">newBVMultExpr</a>(int bvLength, const std::vector< Expr > &kids)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ad27eceadd690e39ef8ad88881925ac0c">newBVMultPadExpr</a>(int bvLength, const Expr &t1, const Expr &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ac4a3e23b2c1039759f22316b4dc00df9">newBVMultPadExpr</a>(int bvLength, const std::vector< Expr > &kids)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a9a3678f2c6007c5b492017b0d9161a37">newBVNandExpr</a>(const Expr &t1, const Expr &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a4bc6d752b2ba293481468dcaaa821d3f">newBVNegExpr</a>(const Expr &t1)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ac7a7ef0271a8aa043ec09684e6a16e9b">newBVNorExpr</a>(const Expr &t1, const Expr &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a7e33736866d0752cdd551dd0059ca1bd">newBVOneString</a>(int r)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a7b93b348dffe055b771db6061446e9ea">newBVOrExpr</a>(const Expr &t1, const Expr &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a9efd00a5226558d90c2617f067c6a99a">newBVOrExpr</a>(const std::vector< Expr > &kids)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ac8e00bf8c66a041e12326e09c4d369ad">newBVPlusExpr</a>(int numbits, const Expr &k1, const Expr &k2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a7de12d92b8235b6b0675c65dd2b5f2dd">newBVPlusExpr</a>(int numbits, const std::vector< Expr > &k)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a284ff4a222be9ceaa97387661c76b147">newBVPlusPadExpr</a>(int bvLength, const std::vector< Expr > &k)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#aa17d7de309b676bac0454ae3dcecb38f">newBVSDivExpr</a>(const Expr &t1, const Expr &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a9b32f54063dda6c3424a63e1702cd277">newBVSLEExpr</a>(const Expr &t1, const Expr &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a2639e4a3d2b13f9e370daf41a833267c">newBVSLTExpr</a>(const Expr &t1, const Expr &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ac520790da34aa971a9ee4044b112ae82">newBVSModExpr</a>(const Expr &t1, const Expr &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a751ed4d2b46020c65ace988d96633142">newBVSRemExpr</a>(const Expr &t1, const Expr &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#af77dddbf974d441cf61294922be53739">newBVSubExpr</a>(const Expr &t1, const Expr &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a43b7fde20faf94ca0691c9c78f49983e">newBVUDivExpr</a>(const Expr &t1, const Expr &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a7113c95ecf45006003eed0d8d7dccda7">newBVUminusExpr</a>(const Expr &t1)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a32e681fc6dc959306710c880f83c95ba">newBVURemExpr</a>(const Expr &t1, const Expr &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ad25d43520383b198f379d573cf72d784">newBVXnorExpr</a>(const Expr &t1, const Expr &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ad5699f06db56401ba2e77bfc37f8344d">newBVXnorExpr</a>(const std::vector< Expr > &kids)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a003f69e1199d0a57102dadc83643fb18">newBVXorExpr</a>(const Expr &t1, const Expr &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a00b711043737f676675a99de32e93492">newBVXorExpr</a>(const std::vector< Expr > &kids)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#aedd220a3f14097d52b80576cdc7b73ec">newBVZeroString</a>(int r)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#aa34c7ab071175e4375822e6f1d47fe0d">newConcatExpr</a>(const Expr &t1, const Expr &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ad7d5b3725d0cae0109eaf01c7b45e2d6">newConcatExpr</a>(const Expr &t1, const Expr &t2, const Expr &t3)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a572efe0038efbeba9566895c58401fcb">newConcatExpr</a>(const std::vector< Expr > &kids)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a082d2161d7c59fcbac262e3d3ddc93a3">newFixedConstWidthLeftShiftExpr</a>(const Expr &t1, int r)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ae1559a54104ab7befb00c9a14b5ea95e">newFixedLeftShiftExpr</a>(const Expr &t1, int r)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a4cb4f4e7d854ca0c7d5883208de4355c">newFixedRightShiftExpr</a>(const Expr &t1, int r)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</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_1TheoryBitvector.html#aed210d6f5ea81db87debb15b422ded2c">newSXExpr</a>(const Expr &t1, int len)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#aadde006d0dea508fec039b8092b14ed6">newTypeExpr</a>(const std::string &name)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a7aadedb0affc98a4cd1741f5dcf42d3a">newTypeExpr</a>(const std::string &name, const Type &def)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a4f82b4903d68da2bd83afb104c2c62cc">newVar</a>(const std::string &name, const Type &type)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#aa7b6e0e6f53256fd0e5573ad51ae472b">newVar</a>(const std::string &name, const Type &type, const Expr &def)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="group__Theory__API.html#ga30a5750a0c38416c847e411c7400214a">notifyInconsistent</a>(const Theorem &thm)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a2e23b49398256989b0dea88a63717dee">Odd_coeff</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#aaa3c1d517c610706a066e7adfee9a6f6">pad</a>(int len, const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#abd5a64ee867dda0c216a04e9fc7fbd6c">parseExpr</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a8bf0677921ceebd416aa6208b56467eb">parseExprOp</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#aaa3c5b6fc08db3e297e811f4c9c18a17">print</a>(ExprStream &os, const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#abd70b8a3ad35dcf7299c87ab36a6f848">printSmtLibShared</a>(ExprStream &os, const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#aa7cb7ed38abf46e12d63c019b694c793">pushNegation</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a3f1ecbd3cea6637fe571cc8b614d3dd6">pushNegationRec</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ac88ba0954e217df731ebb362135ea107">rat</a>(const Rational &r)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</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#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_1TheoryBitvector.html#a82d63a41524830f12abe05b948eab4ca">rewrite</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</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="classCVC3_1_1TheoryBitvector.html#a55e7711ed3e5be41dd7aca955a9ecc7a">rewriteAtomic</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ac2ed14005bb197aaad28ead0cb537a72">rewriteBoolean</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a214442814e895d26ac43c42663741fbd">rewriteBV</a>(const Expr &e, ExprMap< Theorem > &cache, int n=1)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a9d96414ef3ff2c522e621ced84492f8f">rewriteBV</a>(const Expr &e, int n=1)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ad9b702d3659fbaab47960bce473608c8">rewriteBV</a>(const Theorem &t, ExprMap< Theorem > &cache, int n=1)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</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_1TheoryBitvector.html#a84f5fc78f3f36e213ea70ff307db9db8">rewriteBV</a>(const Theorem &t, int n=1)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</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#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_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_1TheoryBitvector.html#a1e7b1123d64a52db1e306942ff4576a3">setup</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</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_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 class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#ae2a5085da47f7b62ed4cb5a312bd9fb3">signed_newBVConstExpr</a>(Rational c, int bv_size)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></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_1TheoryBitvector.html#a5bd75507801c5b8b2595784ce53069aa">simplifyOp</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</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_1TheoryBitvector.html#a324d4171cfb81ff5e774cbc326aaa1d9">simplifyPendingEq</a>(const Theorem &thm, int maxEffort)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a2a6ec855d488ee1d662ac0d1268d2392">solve</a>(const Theorem &e)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</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#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_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_1TheoryBitvector.html#ac45c989f0c26d78a8de812f2123cd262">TheoryBitvector</a>(TheoryCore *core)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a90684d2a97738341c00f8f9c99af7b66">theoryCore</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a01fa8047ed1f649dc98831cb536187e4">theoryOf</a>(int kind)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#ad4fea3e52e80f6ea2fb1a1eaaa7163b8">theoryOf</a>(const Type &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a9ea78dba89246dda6c504c7af5201f1b">theoryOf</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="group__Theory__API.html#gab66d477fcc5c27075a25dbfec4988537">theoryPreprocess</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a5dad9fa356483782703a1ef1024d2a74">theoryUsed</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a76f6507116e36f46dab074781fb9bf2d">transitivityRule</a>(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#ab8835beee96db67f3c26a604d96f2fe8">trueExpr</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a090c2b079f3b90b4f5da3d8606b14d16">typePred</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#aafdee81857fde584632759c78ed821f5">unregisterKinds</a>(Theory *theory, std::vector< int > &kinds)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#a6bdcdfdf6d658b1b1b7c548ea4782e6e">unregisterTheory</a>(Theory *theory, std::vector< int > &kinds, bool hasSolver)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a57edac7a7e4ffd04e778f3858a000457">update</a>(const Theorem &e, const Expr &d)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</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_1TheoryBitvector.html#aa12fe04ae2312b60f15f5fc594d533f4">updateSubterms</a>(const Expr &d)</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theory.html#ac4527f940d280bca9ae279520fd1bc17">~Theory</a>(void)</td><td class="entry"><a class="el" href="classCVC3_1_1Theory.html">CVC3::Theory</a></td><td class="entry"><span class="mlabel">virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html#a665042c64606705b935ac0ab15119266">~TheoryBitvector</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1TheoryBitvector.html">CVC3::TheoryBitvector</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>
