<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<title>CVC3: Member List</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li class="current"><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="annotated.html"><span>Class List</span></a></li>
<li><a href="classes.html"><span>Class Index</span></a></li>
<li><a href="hierarchy.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="namespaceCVC3.html">CVC3</a> </li>
<li class="navelem"><a class="el" href="classCVC3_1_1BitvectorProofRules.html">BitvectorProofRules</a> </li>
</ul>
</div>
</div>
<div class="header">
<div class="headertitle">
<div class="title">CVC3::BitvectorProofRules Member List</div> </div>
</div>
<div class="contents">
This is the complete list of members for <a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a>, including all inherited members.<table>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a05dd94575cc5674452e2ff63106e2a40">bitblastBVMult</a>(const std::vector< Theorem > &a_bits, const std::vector< Theorem > &b_bits, const Expr &a_times_b, std::vector< Theorem > &output_bits)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a613cf0998893c8b66e40acf63b40a825">bitblastBVPlus</a>(const std::vector< Theorem > &a_bits, const std::vector< Theorem > &b_bits, const Expr &a_plus_b, std::vector< Theorem > &output_bits)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#aefb184e963398f43e9dd7a0799563350">bitBlastDisEqnRule</a>(const Theorem &e, const Expr &f)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a596c0779b2f39d41816ff658eef9203b">bitBlastEqnRule</a>(const Expr &e, const Expr &f)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ad63871213ec8c864a622bb3d2248b043">bitExtractAllToConstEq</a>(std::vector< Theorem > &thms)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a9f09c5a49fd132f26a01ec7d96168e42">bitExtractBitwise</a>(const Expr &x, int i, int kind)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a95f41581d03d993ec02541ec78fbd655">bitExtractBVASHR</a>(const Expr &x, int i)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#aebe59090c69f529aa1450a64f2d80538">bitExtractBVLSHR</a>(const Expr &x, int i)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ac473ab04bc4692de3ff7f19940d4a3a2">bitExtractBVMult</a>(const Expr &t, int i)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ab60522e7672d31bcf2957d1cbd118208">bitExtractBVPlus</a>(const std::vector< Theorem > &t1, const std::vector< Theorem > &t2, const Expr &bvPlusTerm, int i)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ab521ae872e2a877f5e30ec9f1b8ded8f">bitExtractBVPlusPreComputed</a>(const Theorem &t1_i, const Theorem &t2_i, const Expr &bvPlusTerm, int bitPos, int precomputed)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#afcd3c4de329e1b2912d83853be46130a">bitExtractBVSHL</a>(const Expr &x, int i)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a14d171b56b3318b1a070fc2c0798f038">bitExtractConcatenation</a>(const Expr &x, int i)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ace62b8eacaad88c90231099943a49090">bitExtractConstant</a>(const Expr &x, int i)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a14a48b5e0170be003c5a52585654fa6c">bitExtractConstBVMult</a>(const Expr &t, int i)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ae46b941cbb7c67aec7a96a45b33e73ab">bitExtractExtraction</a>(const Expr &x, int i)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a3c7217656c1f4bdd8ab08e415ef3dc7d">bitExtractFixedLeftShift</a>(const Expr &x, int i)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a8671b7ed4e5e09402cf5a732fb13a373">bitExtractFixedRightShift</a>(const Expr &x, int i)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a40fd98cf00aa03114e7bdf0e164abe69">bitExtractNot</a>(const Expr &x, int i)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a79a44f95f79735f733cd75f289887da9">bitExtractRewrite</a>(const Expr &x)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a0520e4a3cf5ce89aaa0cf24c1cf5dd9a">bitExtractSXRule</a>(const Expr &e, int i)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a77c82c6fccba740e2df14739edb40a02">bitExtractToExtract</a>(const Theorem &thm)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a6536981ca57bbf915b88a818ad56a1f3">bitvectorFalseRule</a>(const Theorem &thm)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a27a79309cbbf8554394d32c9773472cc">bitvectorTrueRule</a>(const Theorem &thm)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a29d3cce157edf35040c7c237570e37c9">bitwiseConcat</a>(const Expr &e, int kind)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#abc8792717d3f194aa05f279f63033ec1">bitwiseConst</a>(const Expr &e, const std::vector< int > &idxs, int kind)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ab67de0bd797585c3a5cfa3d80a4bfa42">bitwiseConstElim</a>(const Expr &e, int idx, int kind)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a78d58f8b598713266bad87dcfba0d93b">bitwiseFlatten</a>(const Expr &e, int kind)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a42639e0098377ce718308a2ae833430b">bvashrToConcat</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a3ce4fc360b44dec2f89d8d597244c305">bvConstIneqn</a>(const Expr &e, int kind)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a47645c759c4c43b1336d6aa8ea4bef24">bvConstMultAssocRule</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a994aa73b02c523cd2e9e76a4880a167b">bvlshrToConcat</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#aaeb132de41aad56b3bbb5a0c9fcede80">BVMult_order_subterms</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a06eb338d6dbad205f7ce886b94866e01">bvMultAssocRule</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a63c42dbedb2f04af9dd61d6b104c42f0">bvmultBVUminus</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ae0c8cdf3fade0ff0824c6112f4bdec0c">bvmultConst</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a0a00757ccf2b0b5115003629085752f5">bvMultDistRule</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a0836ea2282578bd221ade4a06d0abc2e">bvPlusAssociativityRule</a>(const Expr &bvPlusTerm)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a70ff8e2477ef2d049bd33d1a4bab482e">bvplusConst</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a425296e1ac48c9698802b9a7513745d5">bvplusZeroConcatRule</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a8737b8dee3cf693cba13dd073b132294">bvSDivRewrite</a>(const Expr &sDivExpr)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a52acdd1024ed2ab0737c7747102fa7fe">bvShiftZero</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ab3a7d61a6e1627433906f527f89e300b">bvshlSplit</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#aa665d97eb8067ae68741a6e25135e307">bvshlToConcat</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#af8734beba48ae58dd465efd808f73117">bvSModRewrite</a>(const Expr &sModExpr)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a41766b9dbe8dd7e8ebf5cf0349cf2e9e">bvSRemRewrite</a>(const Expr &sRemExpr)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a95920e0fd327bc9630d41784449bae0a">bvUDivConst</a>(const Expr &divExpr)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ab1b7fd737bbf85300e149a0ca1dce266">bvUDivTheorem</a>(const Expr &divExpr)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#afb6657218e31843d4f9fb55494133a51">bvuminusBVConst</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ae96c6008f1ded31a7d8985264594cbbc">bvuminusBVMult</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ac77eea8dcc7f833bb3f426fd3f021a93">bvuminusBVPlus</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a331e5974d6b4cf1458501aba9c4a2556">bvuminusBVUminus</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ab7d869044d0d907fb1066e706039ca68">bvuminusToBVPlus</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#aaa564090b043862b11ce47d777a9c959">bvuminusVar</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a3cf92f9619244e27a40a6b218887cad0">bvURemConst</a>(const Expr &remExpr)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a0e0a89d5b866cb77e50cc24c20f5d053">bvURemRewrite</a>(const Expr &divExpr)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a04f65b94c6a9ca2b84a6063aac0d082f">canonBVEQ</a>(const Expr &e, int maxEffort=3)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a74f5018affcab70b831029b390692552">canonBVMult</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a07f756438b45b15b493497341944bbb4">canonBVPlus</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#acb966a104436262e81299cea86bc21bb">canonBVUMinus</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a88dbf100f26bd80ac71b976513cf5ed0">combineLikeTermsRule</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a067fc47b8a688b6a08b94c5044d2faf5">concatConst</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a06461d9c64f09ce1dc9acf6cb0628977">concatFlatten</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#adec7f3c93376d5e5c0abb20fc3b44eb9">concatMergeExtract</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a30e4cf2ef646b5fbc1e0b2b6fb88115a">constEq</a>(const Expr &eq)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ac132cce6c99ee7626ee4696010e77aa6">constMultToPlus</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#aaf79659bd7a160d20c3d27d7746d9ca3">constWidthLeftShiftToConcat</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a11422aabc07aa0721cf17b2297a97b40">distributive_rule</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ad88adf2f899f5eab5c0de7c09892178f">eqConst</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a72537952b59dbed6451fe20803e565a6">eqToBits</a>(const Theorem &eq)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#acff4dd7561fb19a337f76edfa024c1aa">expandTypePred</a>(const Theorem &tp)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a9c8be2deedd7168a29b288737cd050a8">extractAnd</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a548cc7ab83b3d604226f09235d2097bf">extractBitwise</a>(const Expr &e, int kind, const std::string &name)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#aa3c6172968875b9189228eb7f8c50187">extractBVMult</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a144383710caebde013be9b2cefce5a4c">extractBVPlus</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a483af962d2b2c8390207e94bd2ae6dc1">extractConcat</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a56770462de38c0c8eed61d1f33c77d6c">extractConst</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a7fc72894f97ec709bf1558254e40903e">extractExtract</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ac258a650188de30470eae5c53116abfd">extractNeg</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a7cdfdc4ac2ed578d2c584549b8a374a7">extractOr</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ae9d9e1338cf24b20f8eb713fbd9b0219">extractWhole</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a5c1a3b38a87b8cdf2fe7674b0c50c8ed">flattenBVPlus</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ae17fc2f1a86046cc389e4f828ce6043c">flipBVMult</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a666ed19d6d57236061243c0951ee6228">generalIneqn</a>(const Expr &e, const Theorem &e0, const Theorem &e1, int kind)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#aef8e88512f778d081ade97e6304f1d18">isolate_var</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ae25244a21bbc10ad069c9c98ac49590e">iteBVnegRule</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#adabf3a32d5a2444ca64e2f66a414f185">iteExtractRule</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a2944e9810307f39e543f8fa6b973f0a8">leftShiftToConcat</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a4be7745b6e05010590d15b0ae9f87212">lhsEqRhsIneqn</a>(const Expr &e, int kind)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ad7df7b16e4ba8d0a84163dac7a3fd29d">lhsMinusRhsRule</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a17c15204dfec661af091bb07f44c4f51">liftConcatBVMult</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#affb1cdfd198f4140f1943f9296b1b97c">liftConcatBVPlus</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a02032b49999aa3913265a22cac129045">MarkNonSolvableEq</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a4fb78e904f25388d54eb0ba54ced536d">negBVand</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a5763889eb6cd07ab04d4c98686db01cf">negBVor</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#accade48c8a792079d97d49d92dc2abee">negBVxnor</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a2b4170a86c6978a77c338dbf832929ad">negBVxor</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a9c4a53c0c1961951e3d847394bfa1b20">negConcat</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a76151013db10b5faa12ba32ad2374fc6">negConst</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a13eeb7dac6de93650d885b61eb72e0ad">negElim</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ac6cbc581e757d482483d62366e84afb9">negNeg</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a7fdf91656d5a4d1b9278e8a974a2578e">notBVEQ1Rule</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a328733af3be6889566b4ab81c7dd4759">notBVLTRule</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a94e717097d7f4156e647893dd506b91d">oneBVAND</a>(const Expr &andEqOne)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a99efc60c900f6818e718eaa76634f82d">oneCoeffBVMult</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a5ca10099b3728f472fc70efbe03fce11">padBVLTRule</a>(const Expr &e, int len)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a185de05a96896134fb0c204bfa2b701f">padBVMult</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a534b8599309b8a1f04355f974450eb44">padBVPlus</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a9a4fef11fae7f9d9b281876569c3ecaf">padBVSLTRule</a>(const Expr &e, int len)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ac018d05ae792d761195fbcc9731017d0">processExtract</a>(const Theorem &e, bool &solvedForm)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#aed9f65e2eed1299d80b6ec63274568a4">repeatRule</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#acccc78337e0a0143b9635e1cd49ac657">rewriteBVCOMP</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a693f8801e36967bf64a0fef0290cad5a">rewriteBVSub</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a53c8279d20f7d229437790ce6c0da2da">rewriteNAND</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a8e2d34a4c387bd5eace8b7e6237bd936">rewriteNOR</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#af126175b4dbb92231ec44c14f32d8b21">rewriteXNOR</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ab2d4f1d9f2f71845d0e2efb2e9ab0f02">rightShiftToConcat</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a9a9c214170ee9595f2eb0b0552b6130f">rotlRule</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#aca310d258dd22e4e50b19274047c6528">rotrRule</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#af472ab5f550394b03c264675181ac1c9">signBVLTRule</a>(const Expr &e, const Theorem &topBit0, const Theorem &topBit1)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a06405edfaf820f9b2940ce7bf406615f">signExtendRule</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a4e491d1c488cb38d6e22ec21ac894f46">solveExtractOverlap</a>(const Expr &eq)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a3b3ae2372cab5026feec302b6bdaa7d6">solveExtractOverlapApplies</a>(const Expr &eq)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a2096bde76317290227a520452a3ab4c4">typePredBit</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a91229b0364c30d73cfdb5eba138ba712">zeroBVOR</a>(const Expr &orEqZero)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a0dacf60fcac4bbbcc45019a5c58d576c">zeroCoeffBVMult</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a0e4bd4a89095a5c275cc898b624b9346">zeroExtendRule</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a7536abc5b7725abfec2d93987cf86a6b">zeroLeq</a>(const Expr &e)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ae806df67b545215d677ccd81b68c9b16">zeroPaddingRule</a>(const Expr &e, int r)=0</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [pure virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a7b9613e9ffdee59c9f70bd06e1a6f29e">~BitvectorProofRules</a>()</td><td><a class="el" href="classCVC3_1_1BitvectorProofRules.html">CVC3::BitvectorProofRules</a></td><td><code> [inline, virtual]</code></td></tr>
</table></div>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
