<!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: CVC3::BitvectorProofRules Class Reference</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_1BitvectorProofRules.html">BitvectorProofRules</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="summary">
<a href="#pub-methods">Public Member Functions</a> |
<a href="classCVC3_1_1BitvectorProofRules-members.html">List of all members</a> </div>
<div class="headertitle">
<div class="title">CVC3::BitvectorProofRules Class Reference<span class="mlabels"><span class="mlabel">abstract</span></span></div> </div>
</div><!--header-->
<div class="contents">
<p><code>#include <<a class="el" href="bitvector__proof__rules_8h_source.html">bitvector_proof_rules.h</a>></code></p>
<p>Inherited by <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html">CVC3::BitvectorTheoremProducer</a>.</p>
<div class="dynheader">
Collaboration diagram for CVC3::BitvectorProofRules:</div>
<div class="dyncontent">
<div class="center"><img src="classCVC3_1_1BitvectorProofRules__coll__graph.gif" border="0" usemap="#CVC3_1_1BitvectorProofRules_coll__map" alt="Collaboration graph"/></div>
<map name="CVC3_1_1BitvectorProofRules_coll__map" id="CVC3_1_1BitvectorProofRules_coll__map">
</map>
</div>
<table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pub-methods"></a>
Public Member Functions</h2></td></tr>
<tr class="memitem:a7b9613e9ffdee59c9f70bd06e1a6f29e"><td class="memItemLeft" align="right" valign="top">virtual </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a7b9613e9ffdee59c9f70bd06e1a6f29e">~BitvectorProofRules</a> ()</td></tr>
<tr class="separator:a7b9613e9ffdee59c9f70bd06e1a6f29e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6536981ca57bbf915b88a818ad56a1f3"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a6536981ca57bbf915b88a818ad56a1f3">bitvectorFalseRule</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)=0</td></tr>
<tr class="separator:a6536981ca57bbf915b88a818ad56a1f3"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a27a79309cbbf8554394d32c9773472cc"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a27a79309cbbf8554394d32c9773472cc">bitvectorTrueRule</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)=0</td></tr>
<tr class="separator:a27a79309cbbf8554394d32c9773472cc"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a596c0779b2f39d41816ff658eef9203b"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a596c0779b2f39d41816ff658eef9203b">bitBlastEqnRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &f)=0</td></tr>
<tr class="memdesc:a596c0779b2f39d41816ff658eef9203b"><td class="mdescLeft"> </td><td class="mdescRight">t1=t2 ==> AND_i(t1[i:i] = t2[i:i]) <a href="#a596c0779b2f39d41816ff658eef9203b"></a><br/></td></tr>
<tr class="separator:a596c0779b2f39d41816ff658eef9203b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aefb184e963398f43e9dd7a0799563350"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#aefb184e963398f43e9dd7a0799563350">bitBlastDisEqnRule</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &f)=0</td></tr>
<tr class="memdesc:aefb184e963398f43e9dd7a0799563350"><td class="mdescLeft"> </td><td class="mdescRight">t1/=t2 ==> OR_i(NOT t1[i]<=>t2[i]) <a href="#aefb184e963398f43e9dd7a0799563350"></a><br/></td></tr>
<tr class="separator:aefb184e963398f43e9dd7a0799563350"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a06405edfaf820f9b2940ce7bf406615f"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a06405edfaf820f9b2940ce7bf406615f">signExtendRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a06405edfaf820f9b2940ce7bf406615f"><td class="mdescLeft"> </td><td class="mdescRight">sign extend the input SX(e) appropriately <a href="#a06405edfaf820f9b2940ce7bf406615f"></a><br/></td></tr>
<tr class="separator:a06405edfaf820f9b2940ce7bf406615f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5ca10099b3728f472fc70efbe03fce11"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a5ca10099b3728f472fc70efbe03fce11">padBVLTRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, int len)=0</td></tr>
<tr class="memdesc:a5ca10099b3728f472fc70efbe03fce11"><td class="mdescLeft"> </td><td class="mdescRight">Pad the kids of BVLT/BVLE to make their length equal. <a href="#a5ca10099b3728f472fc70efbe03fce11"></a><br/></td></tr>
<tr class="separator:a5ca10099b3728f472fc70efbe03fce11"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a9a4fef11fae7f9d9b281876569c3ecaf"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a9a4fef11fae7f9d9b281876569c3ecaf">padBVSLTRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, int len)=0</td></tr>
<tr class="memdesc:a9a4fef11fae7f9d9b281876569c3ecaf"><td class="mdescLeft"> </td><td class="mdescRight">Sign Extend the kids of BVSLT/BVSLE to make their length equal. <a href="#a9a4fef11fae7f9d9b281876569c3ecaf"></a><br/></td></tr>
<tr class="separator:a9a4fef11fae7f9d9b281876569c3ecaf"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:af472ab5f550394b03c264675181ac1c9"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#af472ab5f550394b03c264675181ac1c9">signBVLTRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &topBit0, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &topBit1)=0</td></tr>
<tr class="separator:af472ab5f550394b03c264675181ac1c9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a7fdf91656d5a4d1b9278e8a974a2578e"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a7fdf91656d5a4d1b9278e8a974a2578e">notBVEQ1Rule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:a7fdf91656d5a4d1b9278e8a974a2578e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a328733af3be6889566b4ab81c7dd4759"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a328733af3be6889566b4ab81c7dd4759">notBVLTRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:a328733af3be6889566b4ab81c7dd4759"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a4be7745b6e05010590d15b0ae9f87212"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a4be7745b6e05010590d15b0ae9f87212">lhsEqRhsIneqn</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, int kind)=0</td></tr>
<tr class="memdesc:a4be7745b6e05010590d15b0ae9f87212"><td class="mdescLeft"> </td><td class="mdescRight">if(lhs==rhs) then we have (lhs < rhs <==> false),(lhs <= rhs <==> true) <a href="#a4be7745b6e05010590d15b0ae9f87212"></a><br/></td></tr>
<tr class="separator:a4be7745b6e05010590d15b0ae9f87212"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a7536abc5b7725abfec2d93987cf86a6b"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a7536abc5b7725abfec2d93987cf86a6b">zeroLeq</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:a7536abc5b7725abfec2d93987cf86a6b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a3ce4fc360b44dec2f89d8d597244c305"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a3ce4fc360b44dec2f89d8d597244c305">bvConstIneqn</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, int kind)=0</td></tr>
<tr class="separator:a3ce4fc360b44dec2f89d8d597244c305"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a666ed19d6d57236061243c0951ee6228"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a666ed19d6d57236061243c0951ee6228">generalIneqn</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e0, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e1, int kind)=0</td></tr>
<tr class="separator:a666ed19d6d57236061243c0951ee6228"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad63871213ec8c864a622bb3d2248b043"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ad63871213ec8c864a622bb3d2248b043">bitExtractAllToConstEq</a> (std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &thms)=0</td></tr>
<tr class="separator:ad63871213ec8c864a622bb3d2248b043"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a77c82c6fccba740e2df14739edb40a02"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a77c82c6fccba740e2df14739edb40a02">bitExtractToExtract</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)=0</td></tr>
<tr class="memdesc:a77c82c6fccba740e2df14739edb40a02"><td class="mdescLeft"> </td><td class="mdescRight">t[i] ==> t[i:i] = 0bin1 or NOT t[i] ==> t[i:i] = 0bin0 <a href="#a77c82c6fccba740e2df14739edb40a02"></a><br/></td></tr>
<tr class="separator:a77c82c6fccba740e2df14739edb40a02"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a79a44f95f79735f733cd75f289887da9"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a79a44f95f79735f733cd75f289887da9">bitExtractRewrite</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &x)=0</td></tr>
<tr class="memdesc:a79a44f95f79735f733cd75f289887da9"><td class="mdescLeft"> </td><td class="mdescRight">t[i] <=> t[i:i][0] (to use rewriter for simplifying t[i:i]) <a href="#a79a44f95f79735f733cd75f289887da9"></a><br/></td></tr>
<tr class="separator:a79a44f95f79735f733cd75f289887da9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ace62b8eacaad88c90231099943a49090"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ace62b8eacaad88c90231099943a49090">bitExtractConstant</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &x, int i)=0</td></tr>
<tr class="separator:ace62b8eacaad88c90231099943a49090"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a14d171b56b3318b1a070fc2c0798f038"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a14d171b56b3318b1a070fc2c0798f038">bitExtractConcatenation</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &x, int i)=0</td></tr>
<tr class="separator:a14d171b56b3318b1a070fc2c0798f038"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a14a48b5e0170be003c5a52585654fa6c"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a14a48b5e0170be003c5a52585654fa6c">bitExtractConstBVMult</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &t, int i)=0</td></tr>
<tr class="separator:a14a48b5e0170be003c5a52585654fa6c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac473ab04bc4692de3ff7f19940d4a3a2"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ac473ab04bc4692de3ff7f19940d4a3a2">bitExtractBVMult</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &t, int i)=0</td></tr>
<tr class="separator:ac473ab04bc4692de3ff7f19940d4a3a2"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae46b941cbb7c67aec7a96a45b33e73ab"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ae46b941cbb7c67aec7a96a45b33e73ab">bitExtractExtraction</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &x, int i)=0</td></tr>
<tr class="separator:ae46b941cbb7c67aec7a96a45b33e73ab"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab60522e7672d31bcf2957d1cbd118208"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ab60522e7672d31bcf2957d1cbd118208">bitExtractBVPlus</a> (const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &t1, const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &t2, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &bvPlusTerm, int i)=0</td></tr>
<tr class="separator:ab60522e7672d31bcf2957d1cbd118208"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab521ae872e2a877f5e30ec9f1b8ded8f"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ab521ae872e2a877f5e30ec9f1b8ded8f">bitExtractBVPlusPreComputed</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &t1_i, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &t2_i, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &bvPlusTerm, int bitPos, int precomputed)=0</td></tr>
<tr class="separator:ab521ae872e2a877f5e30ec9f1b8ded8f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0836ea2282578bd221ade4a06d0abc2e"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a0836ea2282578bd221ade4a06d0abc2e">bvPlusAssociativityRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &bvPlusTerm)=0</td></tr>
<tr class="separator:a0836ea2282578bd221ade4a06d0abc2e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a40fd98cf00aa03114e7bdf0e164abe69"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a40fd98cf00aa03114e7bdf0e164abe69">bitExtractNot</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &x, int i)=0</td></tr>
<tr class="separator:a40fd98cf00aa03114e7bdf0e164abe69"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a9f09c5a49fd132f26a01ec7d96168e42"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a9f09c5a49fd132f26a01ec7d96168e42">bitExtractBitwise</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &x, int i, int kind)=0</td></tr>
<tr class="memdesc:a9f09c5a49fd132f26a01ec7d96168e42"><td class="mdescLeft"> </td><td class="mdescRight">Extract from bitwise AND, OR, or XOR. <a href="#a9f09c5a49fd132f26a01ec7d96168e42"></a><br/></td></tr>
<tr class="separator:a9f09c5a49fd132f26a01ec7d96168e42"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a3c7217656c1f4bdd8ab08e415ef3dc7d"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a3c7217656c1f4bdd8ab08e415ef3dc7d">bitExtractFixedLeftShift</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &x, int i)=0</td></tr>
<tr class="separator:a3c7217656c1f4bdd8ab08e415ef3dc7d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a8671b7ed4e5e09402cf5a732fb13a373"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a8671b7ed4e5e09402cf5a732fb13a373">bitExtractFixedRightShift</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &x, int i)=0</td></tr>
<tr class="separator:a8671b7ed4e5e09402cf5a732fb13a373"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:afcd3c4de329e1b2912d83853be46130a"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#afcd3c4de329e1b2912d83853be46130a">bitExtractBVSHL</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &x, int i)=0</td></tr>
<tr class="separator:afcd3c4de329e1b2912d83853be46130a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aebe59090c69f529aa1450a64f2d80538"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#aebe59090c69f529aa1450a64f2d80538">bitExtractBVLSHR</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &x, int i)=0</td></tr>
<tr class="separator:aebe59090c69f529aa1450a64f2d80538"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a95f41581d03d993ec02541ec78fbd655"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a95f41581d03d993ec02541ec78fbd655">bitExtractBVASHR</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &x, int i)=0</td></tr>
<tr class="separator:a95f41581d03d993ec02541ec78fbd655"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae806df67b545215d677ccd81b68c9b16"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ae806df67b545215d677ccd81b68c9b16">zeroPaddingRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, int r)=0</td></tr>
<tr class="separator:ae806df67b545215d677ccd81b68c9b16"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0520e4a3cf5ce89aaa0cf24c1cf5dd9a"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a0520e4a3cf5ce89aaa0cf24c1cf5dd9a">bitExtractSXRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, int i)=0</td></tr>
<tr class="separator:a0520e4a3cf5ce89aaa0cf24c1cf5dd9a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad88adf2f899f5eab5c0de7c09892178f"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ad88adf2f899f5eab5c0de7c09892178f">eqConst</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:ad88adf2f899f5eab5c0de7c09892178f"><td class="mdescLeft"> </td><td class="mdescRight">c1=c2 <=> TRUE/FALSE (equality of constant bitvectors) <a href="#ad88adf2f899f5eab5c0de7c09892178f"></a><br/></td></tr>
<tr class="separator:ad88adf2f899f5eab5c0de7c09892178f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a72537952b59dbed6451fe20803e565a6"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a72537952b59dbed6451fe20803e565a6">eqToBits</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &eq)=0</td></tr>
<tr class="memdesc:a72537952b59dbed6451fe20803e565a6"><td class="mdescLeft"> </td><td class="mdescRight">|- c1=c2 ==> |- AND(c1[i:i] = c2[i:i]) - expanding equalities into bits <a href="#a72537952b59dbed6451fe20803e565a6"></a><br/></td></tr>
<tr class="separator:a72537952b59dbed6451fe20803e565a6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a2944e9810307f39e543f8fa6b973f0a8"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a2944e9810307f39e543f8fa6b973f0a8">leftShiftToConcat</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a2944e9810307f39e543f8fa6b973f0a8"><td class="mdescLeft"> </td><td class="mdescRight">t<<n = c @ 0bin00...00, takes e == (t<<n) <a href="#a2944e9810307f39e543f8fa6b973f0a8"></a><br/></td></tr>
<tr class="separator:a2944e9810307f39e543f8fa6b973f0a8"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aaf79659bd7a160d20c3d27d7746d9ca3"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#aaf79659bd7a160d20c3d27d7746d9ca3">constWidthLeftShiftToConcat</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:aaf79659bd7a160d20c3d27d7746d9ca3"><td class="mdescLeft"> </td><td class="mdescRight">t<<n = c @ 0bin00...00, takes e == (t<<n) <a href="#aaf79659bd7a160d20c3d27d7746d9ca3"></a><br/></td></tr>
<tr class="separator:aaf79659bd7a160d20c3d27d7746d9ca3"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab2d4f1d9f2f71845d0e2efb2e9ab0f02"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ab2d4f1d9f2f71845d0e2efb2e9ab0f02">rightShiftToConcat</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:ab2d4f1d9f2f71845d0e2efb2e9ab0f02"><td class="mdescLeft"> </td><td class="mdescRight">t>>m = 0bin00...00 @ t[bvlength-1:m], takes e == (t>>n) <a href="#ab2d4f1d9f2f71845d0e2efb2e9ab0f02"></a><br/></td></tr>
<tr class="separator:ab2d4f1d9f2f71845d0e2efb2e9ab0f02"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa665d97eb8067ae68741a6e25135e307"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#aa665d97eb8067ae68741a6e25135e307">bvshlToConcat</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:aa665d97eb8067ae68741a6e25135e307"><td class="mdescLeft"> </td><td class="mdescRight">BVSHL(t,c) = t[n-c,0] @ 0bin00...00. <a href="#aa665d97eb8067ae68741a6e25135e307"></a><br/></td></tr>
<tr class="separator:aa665d97eb8067ae68741a6e25135e307"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab3a7d61a6e1627433906f527f89e300b"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ab3a7d61a6e1627433906f527f89e300b">bvshlSplit</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:ab3a7d61a6e1627433906f527f89e300b"><td class="mdescLeft"> </td><td class="mdescRight">BVSHL(t,c) = IF (c = 0) THEN t ELSE IF (c = 1) ... <a href="#ab3a7d61a6e1627433906f527f89e300b"></a><br/></td></tr>
<tr class="separator:ab3a7d61a6e1627433906f527f89e300b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a994aa73b02c523cd2e9e76a4880a167b"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a994aa73b02c523cd2e9e76a4880a167b">bvlshrToConcat</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a994aa73b02c523cd2e9e76a4880a167b"><td class="mdescLeft"> </td><td class="mdescRight">BVLSHR(t,c) = 0bin00...00 @ t[n-1,c]. <a href="#a994aa73b02c523cd2e9e76a4880a167b"></a><br/></td></tr>
<tr class="separator:a994aa73b02c523cd2e9e76a4880a167b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a52acdd1024ed2ab0737c7747102fa7fe"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a52acdd1024ed2ab0737c7747102fa7fe">bvShiftZero</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a52acdd1024ed2ab0737c7747102fa7fe"><td class="mdescLeft"> </td><td class="mdescRight">Any shift over a zero = 0. <a href="#a52acdd1024ed2ab0737c7747102fa7fe"></a><br/></td></tr>
<tr class="separator:a52acdd1024ed2ab0737c7747102fa7fe"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a42639e0098377ce718308a2ae833430b"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a42639e0098377ce718308a2ae833430b">bvashrToConcat</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a42639e0098377ce718308a2ae833430b"><td class="mdescLeft"> </td><td class="mdescRight">BVASHR(t,c) = SX(t[n-1,c], n-1) <a href="#a42639e0098377ce718308a2ae833430b"></a><br/></td></tr>
<tr class="separator:a42639e0098377ce718308a2ae833430b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:af126175b4dbb92231ec44c14f32d8b21"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#af126175b4dbb92231ec44c14f32d8b21">rewriteXNOR</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:af126175b4dbb92231ec44c14f32d8b21"><td class="mdescLeft"> </td><td class="mdescRight">a XNOR b <=> (~a & ~b) | (a & b) <a href="#af126175b4dbb92231ec44c14f32d8b21"></a><br/></td></tr>
<tr class="separator:af126175b4dbb92231ec44c14f32d8b21"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a53c8279d20f7d229437790ce6c0da2da"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a53c8279d20f7d229437790ce6c0da2da">rewriteNAND</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a53c8279d20f7d229437790ce6c0da2da"><td class="mdescLeft"> </td><td class="mdescRight">a NAND b <=> ~(a & b) <a href="#a53c8279d20f7d229437790ce6c0da2da"></a><br/></td></tr>
<tr class="separator:a53c8279d20f7d229437790ce6c0da2da"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a8e2d34a4c387bd5eace8b7e6237bd936"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a8e2d34a4c387bd5eace8b7e6237bd936">rewriteNOR</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a8e2d34a4c387bd5eace8b7e6237bd936"><td class="mdescLeft"> </td><td class="mdescRight">a NOR b <=> ~(a | b) <a href="#a8e2d34a4c387bd5eace8b7e6237bd936"></a><br/></td></tr>
<tr class="separator:a8e2d34a4c387bd5eace8b7e6237bd936"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:acccc78337e0a0143b9635e1cd49ac657"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#acccc78337e0a0143b9635e1cd49ac657">rewriteBVCOMP</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:acccc78337e0a0143b9635e1cd49ac657"><td class="mdescLeft"> </td><td class="mdescRight">BVCOMP(a,b) <=> ITE(a=b,0bin1,0bin0) <a href="#acccc78337e0a0143b9635e1cd49ac657"></a><br/></td></tr>
<tr class="separator:acccc78337e0a0143b9635e1cd49ac657"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a693f8801e36967bf64a0fef0290cad5a"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a693f8801e36967bf64a0fef0290cad5a">rewriteBVSub</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a693f8801e36967bf64a0fef0290cad5a"><td class="mdescLeft"> </td><td class="mdescRight">a - b <=> a + (-b) <a href="#a693f8801e36967bf64a0fef0290cad5a"></a><br/></td></tr>
<tr class="separator:a693f8801e36967bf64a0fef0290cad5a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac132cce6c99ee7626ee4696010e77aa6"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ac132cce6c99ee7626ee4696010e77aa6">constMultToPlus</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:ac132cce6c99ee7626ee4696010e77aa6"><td class="mdescLeft"> </td><td class="mdescRight">k*t = BVPLUS(n, <sum of shifts of t>) – translation of k*t to BVPLUS <a href="#ac132cce6c99ee7626ee4696010e77aa6"></a><br/></td></tr>
<tr class="separator:ac132cce6c99ee7626ee4696010e77aa6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a425296e1ac48c9698802b9a7513745d5"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a425296e1ac48c9698802b9a7513745d5">bvplusZeroConcatRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a425296e1ac48c9698802b9a7513745d5"><td class="mdescLeft"> </td><td class="mdescRight">0bin0...0 @ BVPLUS(n, args) = BVPLUS(n+k, args) <a href="#a425296e1ac48c9698802b9a7513745d5"></a><br/></td></tr>
<tr class="separator:a425296e1ac48c9698802b9a7513745d5"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0dacf60fcac4bbbcc45019a5c58d576c"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a0dacf60fcac4bbbcc45019a5c58d576c">zeroCoeffBVMult</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:a0dacf60fcac4bbbcc45019a5c58d576c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a99efc60c900f6818e718eaa76634f82d"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a99efc60c900f6818e718eaa76634f82d">oneCoeffBVMult</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:a99efc60c900f6818e718eaa76634f82d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae17fc2f1a86046cc389e4f828ce6043c"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ae17fc2f1a86046cc389e4f828ce6043c">flipBVMult</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:ae17fc2f1a86046cc389e4f828ce6043c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a534b8599309b8a1f04355f974450eb44"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a534b8599309b8a1f04355f974450eb44">padBVPlus</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a534b8599309b8a1f04355f974450eb44"><td class="mdescLeft"> </td><td class="mdescRight">Make args the same length as the result (zero-extend) <a href="#a534b8599309b8a1f04355f974450eb44"></a><br/></td></tr>
<tr class="separator:a534b8599309b8a1f04355f974450eb44"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a185de05a96896134fb0c204bfa2b701f"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a185de05a96896134fb0c204bfa2b701f">padBVMult</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a185de05a96896134fb0c204bfa2b701f"><td class="mdescLeft"> </td><td class="mdescRight">Make args the same length as the result (zero-extend) <a href="#a185de05a96896134fb0c204bfa2b701f"></a><br/></td></tr>
<tr class="separator:a185de05a96896134fb0c204bfa2b701f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a47645c759c4c43b1336d6aa8ea4bef24"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a47645c759c4c43b1336d6aa8ea4bef24">bvConstMultAssocRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:a47645c759c4c43b1336d6aa8ea4bef24"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a06eb338d6dbad205f7ce886b94866e01"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a06eb338d6dbad205f7ce886b94866e01">bvMultAssocRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:a06eb338d6dbad205f7ce886b94866e01"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0a00757ccf2b0b5115003629085752f5"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a0a00757ccf2b0b5115003629085752f5">bvMultDistRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:a0a00757ccf2b0b5115003629085752f5"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5c1a3b38a87b8cdf2fe7674b0c50c8ed"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a5c1a3b38a87b8cdf2fe7674b0c50c8ed">flattenBVPlus</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:a5c1a3b38a87b8cdf2fe7674b0c50c8ed"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a88dbf100f26bd80ac71b976513cf5ed0"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a88dbf100f26bd80ac71b976513cf5ed0">combineLikeTermsRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:a88dbf100f26bd80ac71b976513cf5ed0"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad7df7b16e4ba8d0a84163dac7a3fd29d"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ad7df7b16e4ba8d0a84163dac7a3fd29d">lhsMinusRhsRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:ad7df7b16e4ba8d0a84163dac7a3fd29d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa3c6172968875b9189228eb7f8c50187"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#aa3c6172968875b9189228eb7f8c50187">extractBVMult</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:aa3c6172968875b9189228eb7f8c50187"><td class="mdescLeft"> </td><td class="mdescRight">(x *[n] y)[m:k] = (x *[m+1] y)[m:k], where m < n <a href="#aa3c6172968875b9189228eb7f8c50187"></a><br/></td></tr>
<tr class="separator:aa3c6172968875b9189228eb7f8c50187"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a144383710caebde013be9b2cefce5a4c"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a144383710caebde013be9b2cefce5a4c">extractBVPlus</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a144383710caebde013be9b2cefce5a4c"><td class="mdescLeft"> </td><td class="mdescRight">(x +[n] y)[m:k] = (x +[m+1] y)[m:k], where m < n <a href="#a144383710caebde013be9b2cefce5a4c"></a><br/></td></tr>
<tr class="separator:a144383710caebde013be9b2cefce5a4c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:adabf3a32d5a2444ca64e2f66a414f185"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#adabf3a32d5a2444ca64e2f66a414f185">iteExtractRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:adabf3a32d5a2444ca64e2f66a414f185"><td class="mdescLeft"> </td><td class="mdescRight">ite(c,t1,t2)[i:j] <=> ite(c,t1[i:j],t2[i:j]) <a href="#adabf3a32d5a2444ca64e2f66a414f185"></a><br/></td></tr>
<tr class="separator:adabf3a32d5a2444ca64e2f66a414f185"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae25244a21bbc10ad069c9c98ac49590e"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ae25244a21bbc10ad069c9c98ac49590e">iteBVnegRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:ae25244a21bbc10ad069c9c98ac49590e"><td class="mdescLeft"> </td><td class="mdescRight">~ite(c,t1,t2) <=> ite(c,~t1,~t2) <a href="#ae25244a21bbc10ad069c9c98ac49590e"></a><br/></td></tr>
<tr class="separator:ae25244a21bbc10ad069c9c98ac49590e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:afb6657218e31843d4f9fb55494133a51"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#afb6657218e31843d4f9fb55494133a51">bvuminusBVConst</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:afb6657218e31843d4f9fb55494133a51"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae96c6008f1ded31a7d8985264594cbbc"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ae96c6008f1ded31a7d8985264594cbbc">bvuminusBVMult</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:ae96c6008f1ded31a7d8985264594cbbc"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a331e5974d6b4cf1458501aba9c4a2556"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a331e5974d6b4cf1458501aba9c4a2556">bvuminusBVUminus</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:a331e5974d6b4cf1458501aba9c4a2556"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aaa564090b043862b11ce47d777a9c959"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#aaa564090b043862b11ce47d777a9c959">bvuminusVar</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:aaa564090b043862b11ce47d777a9c959"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a63c42dbedb2f04af9dd61d6b104c42f0"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a63c42dbedb2f04af9dd61d6b104c42f0">bvmultBVUminus</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:a63c42dbedb2f04af9dd61d6b104c42f0"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab7d869044d0d907fb1066e706039ca68"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ab7d869044d0d907fb1066e706039ca68">bvuminusToBVPlus</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:ab7d869044d0d907fb1066e706039ca68"><td class="mdescLeft"> </td><td class="mdescRight">-t <==> ~t+1 <a href="#ab7d869044d0d907fb1066e706039ca68"></a><br/></td></tr>
<tr class="separator:ab7d869044d0d907fb1066e706039ca68"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac77eea8dcc7f833bb3f426fd3f021a93"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ac77eea8dcc7f833bb3f426fd3f021a93">bvuminusBVPlus</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:ac77eea8dcc7f833bb3f426fd3f021a93"><td class="mdescLeft"> </td><td class="mdescRight">-(c1*t1+...+cn*tn) <==> (-(c1*t1)+...+-(cn*tn)) <a href="#ac77eea8dcc7f833bb3f426fd3f021a93"></a><br/></td></tr>
<tr class="separator:ac77eea8dcc7f833bb3f426fd3f021a93"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a56770462de38c0c8eed61d1f33c77d6c"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a56770462de38c0c8eed61d1f33c77d6c">extractConst</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a56770462de38c0c8eed61d1f33c77d6c"><td class="mdescLeft"> </td><td class="mdescRight">c1[i:j] = c (extraction from a constant bitvector) <a href="#a56770462de38c0c8eed61d1f33c77d6c"></a><br/></td></tr>
<tr class="separator:a56770462de38c0c8eed61d1f33c77d6c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae9d9e1338cf24b20f8eb713fbd9b0219"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ae9d9e1338cf24b20f8eb713fbd9b0219">extractWhole</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:ae9d9e1338cf24b20f8eb713fbd9b0219"><td class="mdescLeft"> </td><td class="mdescRight">t[n-1:0] = t for n-bit t <a href="#ae9d9e1338cf24b20f8eb713fbd9b0219"></a><br/></td></tr>
<tr class="separator:ae9d9e1338cf24b20f8eb713fbd9b0219"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a7fc72894f97ec709bf1558254e40903e"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a7fc72894f97ec709bf1558254e40903e">extractExtract</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a7fc72894f97ec709bf1558254e40903e"><td class="mdescLeft"> </td><td class="mdescRight">t[i:j][k:l] = t[k+j:l+j] (eliminate double extraction) <a href="#a7fc72894f97ec709bf1558254e40903e"></a><br/></td></tr>
<tr class="separator:a7fc72894f97ec709bf1558254e40903e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a483af962d2b2c8390207e94bd2ae6dc1"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a483af962d2b2c8390207e94bd2ae6dc1">extractConcat</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a483af962d2b2c8390207e94bd2ae6dc1"><td class="mdescLeft"> </td><td class="mdescRight">(t1 @ t2)[i:j] = t1[...] @ t2[...] (push extraction through concat) <a href="#a483af962d2b2c8390207e94bd2ae6dc1"></a><br/></td></tr>
<tr class="separator:a483af962d2b2c8390207e94bd2ae6dc1"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a9c8be2deedd7168a29b288737cd050a8"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a9c8be2deedd7168a29b288737cd050a8">extractAnd</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a9c8be2deedd7168a29b288737cd050a8"><td class="mdescLeft"> </td><td class="mdescRight">(t1 & t2)[i:j] = t1[i:j] & t2[i:j] (push extraction through OR) <a href="#a9c8be2deedd7168a29b288737cd050a8"></a><br/></td></tr>
<tr class="separator:a9c8be2deedd7168a29b288737cd050a8"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a7cdfdc4ac2ed578d2c584549b8a374a7"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a7cdfdc4ac2ed578d2c584549b8a374a7">extractOr</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a7cdfdc4ac2ed578d2c584549b8a374a7"><td class="mdescLeft"> </td><td class="mdescRight">(t1 | t2)[i:j] = t1[i:j] | t2[i:j] (push extraction through AND) <a href="#a7cdfdc4ac2ed578d2c584549b8a374a7"></a><br/></td></tr>
<tr class="separator:a7cdfdc4ac2ed578d2c584549b8a374a7"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac258a650188de30470eae5c53116abfd"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ac258a650188de30470eae5c53116abfd">extractNeg</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:ac258a650188de30470eae5c53116abfd"><td class="mdescLeft"> </td><td class="mdescRight">(~t)[i:j] = ~(t[i:j]) (push extraction through NEG) <a href="#ac258a650188de30470eae5c53116abfd"></a><br/></td></tr>
<tr class="separator:ac258a650188de30470eae5c53116abfd"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a548cc7ab83b3d604226f09235d2097bf"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a548cc7ab83b3d604226f09235d2097bf">extractBitwise</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, int kind, const std::string &name)=0</td></tr>
<tr class="memdesc:a548cc7ab83b3d604226f09235d2097bf"><td class="mdescLeft"> </td><td class="mdescRight">Auxiliary function: (t1 op t2)[i:j] = t1[i:j] op t2[i:j]. <a href="#a548cc7ab83b3d604226f09235d2097bf"></a><br/></td></tr>
<tr class="separator:a548cc7ab83b3d604226f09235d2097bf"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a76151013db10b5faa12ba32ad2374fc6"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a76151013db10b5faa12ba32ad2374fc6">negConst</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a76151013db10b5faa12ba32ad2374fc6"><td class="mdescLeft"> </td><td class="mdescRight">~c1 = c (bit-wise negation of a constant bitvector) <a href="#a76151013db10b5faa12ba32ad2374fc6"></a><br/></td></tr>
<tr class="separator:a76151013db10b5faa12ba32ad2374fc6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a9c4a53c0c1961951e3d847394bfa1b20"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a9c4a53c0c1961951e3d847394bfa1b20">negConcat</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a9c4a53c0c1961951e3d847394bfa1b20"><td class="mdescLeft"> </td><td class="mdescRight">~(t1@...@tn) = (~t1)@...@(~tn) – push negation through concat <a href="#a9c4a53c0c1961951e3d847394bfa1b20"></a><br/></td></tr>
<tr class="separator:a9c4a53c0c1961951e3d847394bfa1b20"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac6cbc581e757d482483d62366e84afb9"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ac6cbc581e757d482483d62366e84afb9">negNeg</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:ac6cbc581e757d482483d62366e84afb9"><td class="mdescLeft"> </td><td class="mdescRight">~(~t) = t – eliminate double negation <a href="#ac6cbc581e757d482483d62366e84afb9"></a><br/></td></tr>
<tr class="separator:ac6cbc581e757d482483d62366e84afb9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a13eeb7dac6de93650d885b61eb72e0ad"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a13eeb7dac6de93650d885b61eb72e0ad">negElim</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a13eeb7dac6de93650d885b61eb72e0ad"><td class="mdescLeft"> </td><td class="mdescRight">~t = -1*t + 1 – eliminate negation <a href="#a13eeb7dac6de93650d885b61eb72e0ad"></a><br/></td></tr>
<tr class="separator:a13eeb7dac6de93650d885b61eb72e0ad"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a4fb78e904f25388d54eb0ba54ced536d"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a4fb78e904f25388d54eb0ba54ced536d">negBVand</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a4fb78e904f25388d54eb0ba54ced536d"><td class="mdescLeft"> </td><td class="mdescRight">~(t1 & t2) <=> ~t1 | ~t2 – DeMorgan's Laws <a href="#a4fb78e904f25388d54eb0ba54ced536d"></a><br/></td></tr>
<tr class="separator:a4fb78e904f25388d54eb0ba54ced536d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5763889eb6cd07ab04d4c98686db01cf"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a5763889eb6cd07ab04d4c98686db01cf">negBVor</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a5763889eb6cd07ab04d4c98686db01cf"><td class="mdescLeft"> </td><td class="mdescRight">~(t1 | t2) <=> ~t1 & ~t2 – DeMorgan's Laws <a href="#a5763889eb6cd07ab04d4c98686db01cf"></a><br/></td></tr>
<tr class="separator:a5763889eb6cd07ab04d4c98686db01cf"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a2b4170a86c6978a77c338dbf832929ad"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a2b4170a86c6978a77c338dbf832929ad">negBVxor</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a2b4170a86c6978a77c338dbf832929ad"><td class="mdescLeft"> </td><td class="mdescRight">~(t1 xor t2) = ~t1 xor t2 <a href="#a2b4170a86c6978a77c338dbf832929ad"></a><br/></td></tr>
<tr class="separator:a2b4170a86c6978a77c338dbf832929ad"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:accade48c8a792079d97d49d92dc2abee"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#accade48c8a792079d97d49d92dc2abee">negBVxnor</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:accade48c8a792079d97d49d92dc2abee"><td class="mdescLeft"> </td><td class="mdescRight">~(t1 xnor t2) = t1 xor t2 <a href="#accade48c8a792079d97d49d92dc2abee"></a><br/></td></tr>
<tr class="separator:accade48c8a792079d97d49d92dc2abee"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:abc8792717d3f194aa05f279f63033ec1"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#abc8792717d3f194aa05f279f63033ec1">bitwiseConst</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, const std::vector< int > &idxs, int kind)=0</td></tr>
<tr class="memdesc:abc8792717d3f194aa05f279f63033ec1"><td class="mdescLeft"> </td><td class="mdescRight">Combine constants in bitwise AND, OR, XOR. <a href="#abc8792717d3f194aa05f279f63033ec1"></a><br/></td></tr>
<tr class="separator:abc8792717d3f194aa05f279f63033ec1"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a29d3cce157edf35040c7c237570e37c9"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a29d3cce157edf35040c7c237570e37c9">bitwiseConcat</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, int kind)=0</td></tr>
<tr class="memdesc:a29d3cce157edf35040c7c237570e37c9"><td class="mdescLeft"> </td><td class="mdescRight">Lifts concatenation above bitwise operators. <a href="#a29d3cce157edf35040c7c237570e37c9"></a><br/></td></tr>
<tr class="separator:a29d3cce157edf35040c7c237570e37c9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a78d58f8b598713266bad87dcfba0d93b"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a78d58f8b598713266bad87dcfba0d93b">bitwiseFlatten</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, int kind)=0</td></tr>
<tr class="memdesc:a78d58f8b598713266bad87dcfba0d93b"><td class="mdescLeft"> </td><td class="mdescRight">Flatten bitwise operation. <a href="#a78d58f8b598713266bad87dcfba0d93b"></a><br/></td></tr>
<tr class="separator:a78d58f8b598713266bad87dcfba0d93b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab67de0bd797585c3a5cfa3d80a4bfa42"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ab67de0bd797585c3a5cfa3d80a4bfa42">bitwiseConstElim</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, int idx, int kind)=0</td></tr>
<tr class="memdesc:ab67de0bd797585c3a5cfa3d80a4bfa42"><td class="mdescLeft"> </td><td class="mdescRight">Simplify bitwise operator containing a constant child. <a href="#ab67de0bd797585c3a5cfa3d80a4bfa42"></a><br/></td></tr>
<tr class="separator:ab67de0bd797585c3a5cfa3d80a4bfa42"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a067fc47b8a688b6a08b94c5044d2faf5"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a067fc47b8a688b6a08b94c5044d2faf5">concatConst</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a067fc47b8a688b6a08b94c5044d2faf5"><td class="mdescLeft"> </td><td class="mdescRight">c1@c2@...@cn = c (concatenation of constant bitvectors) <a href="#a067fc47b8a688b6a08b94c5044d2faf5"></a><br/></td></tr>
<tr class="separator:a067fc47b8a688b6a08b94c5044d2faf5"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a06461d9c64f09ce1dc9acf6cb0628977"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a06461d9c64f09ce1dc9acf6cb0628977">concatFlatten</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a06461d9c64f09ce1dc9acf6cb0628977"><td class="mdescLeft"> </td><td class="mdescRight">Flatten one level of nested concatenation, e.g.: x@(y@z)@w = x@y@z@w. <a href="#a06461d9c64f09ce1dc9acf6cb0628977"></a><br/></td></tr>
<tr class="separator:a06461d9c64f09ce1dc9acf6cb0628977"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:adec7f3c93376d5e5c0abb20fc3b44eb9"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#adec7f3c93376d5e5c0abb20fc3b44eb9">concatMergeExtract</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:adec7f3c93376d5e5c0abb20fc3b44eb9"><td class="mdescLeft"> </td><td class="mdescRight">Merge n-ary concat. of adjacent extractions: x[15:8]@x[7:0] = x[15:0]. <a href="#adec7f3c93376d5e5c0abb20fc3b44eb9"></a><br/></td></tr>
<tr class="separator:adec7f3c93376d5e5c0abb20fc3b44eb9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a70ff8e2477ef2d049bd33d1a4bab482e"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a70ff8e2477ef2d049bd33d1a4bab482e">bvplusConst</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a70ff8e2477ef2d049bd33d1a4bab482e"><td class="mdescLeft"> </td><td class="mdescRight">BVPLUS(n, c1,c2,...,cn) = c (bit-vector plus of constant bitvectors) <a href="#a70ff8e2477ef2d049bd33d1a4bab482e"></a><br/></td></tr>
<tr class="separator:a70ff8e2477ef2d049bd33d1a4bab482e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae0c8cdf3fade0ff0824c6112f4bdec0c"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ae0c8cdf3fade0ff0824c6112f4bdec0c">bvmultConst</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:ae0c8cdf3fade0ff0824c6112f4bdec0c"><td class="mdescLeft"> </td><td class="mdescRight">n*c1 = c, where n >= 0 (multiplication of a constant bitvector by a non-negative constant) <a href="#ae0c8cdf3fade0ff0824c6112f4bdec0c"></a><br/></td></tr>
<tr class="separator:ae0c8cdf3fade0ff0824c6112f4bdec0c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a2096bde76317290227a520452a3ab4c4"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a2096bde76317290227a520452a3ab4c4">typePredBit</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a2096bde76317290227a520452a3ab4c4"><td class="mdescLeft"> </td><td class="mdescRight">|- t=0 OR t=1 for any 1-bit bitvector t <a href="#a2096bde76317290227a520452a3ab4c4"></a><br/></td></tr>
<tr class="separator:a2096bde76317290227a520452a3ab4c4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:acff4dd7561fb19a337f76edfa024c1aa"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#acff4dd7561fb19a337f76edfa024c1aa">expandTypePred</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &tp)=0</td></tr>
<tr class="memdesc:acff4dd7561fb19a337f76edfa024c1aa"><td class="mdescLeft"> </td><td class="mdescRight">Expand the type predicate wrapper (compute the actual type predicate) <a href="#acff4dd7561fb19a337f76edfa024c1aa"></a><br/></td></tr>
<tr class="separator:acff4dd7561fb19a337f76edfa024c1aa"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aef8e88512f778d081ade97e6304f1d18"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#aef8e88512f778d081ade97e6304f1d18">isolate_var</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:aef8e88512f778d081ade97e6304f1d18"><td class="mdescLeft"> </td><td class="mdescRight">isolate a variable with coefficient = 1 on the Lhs of an <a href="#aef8e88512f778d081ade97e6304f1d18"></a><br/></td></tr>
<tr class="separator:aef8e88512f778d081ade97e6304f1d18"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a17c15204dfec661af091bb07f44c4f51"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a17c15204dfec661af091bb07f44c4f51">liftConcatBVMult</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:a17c15204dfec661af091bb07f44c4f51"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a74f5018affcab70b831029b390692552"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a74f5018affcab70b831029b390692552">canonBVMult</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a74f5018affcab70b831029b390692552"><td class="mdescLeft"> </td><td class="mdescRight">canonize BVMult expressions in order to get one coefficient <a href="#a74f5018affcab70b831029b390692552"></a><br/></td></tr>
<tr class="separator:a74f5018affcab70b831029b390692552"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:affb1cdfd198f4140f1943f9296b1b97c"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#affb1cdfd198f4140f1943f9296b1b97c">liftConcatBVPlus</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:affb1cdfd198f4140f1943f9296b1b97c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a07f756438b45b15b493497341944bbb4"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a07f756438b45b15b493497341944bbb4">canonBVPlus</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a07f756438b45b15b493497341944bbb4"><td class="mdescLeft"> </td><td class="mdescRight">canonize BVPlus expressions in order to get just one <a href="#a07f756438b45b15b493497341944bbb4"></a><br/></td></tr>
<tr class="separator:a07f756438b45b15b493497341944bbb4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:acb966a104436262e81299cea86bc21bb"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#acb966a104436262e81299cea86bc21bb">canonBVUMinus</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:acb966a104436262e81299cea86bc21bb"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac018d05ae792d761195fbcc9731017d0"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ac018d05ae792d761195fbcc9731017d0">processExtract</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e, bool &solvedForm)=0</td></tr>
<tr class="separator:ac018d05ae792d761195fbcc9731017d0"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a04f65b94c6a9ca2b84a6063aac0d082f"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a04f65b94c6a9ca2b84a6063aac0d082f">canonBVEQ</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, int maxEffort=3)=0</td></tr>
<tr class="separator:a04f65b94c6a9ca2b84a6063aac0d082f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a11422aabc07aa0721cf17b2297a97b40"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a11422aabc07aa0721cf17b2297a97b40">distributive_rule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="memdesc:a11422aabc07aa0721cf17b2297a97b40"><td class="mdescLeft"> </td><td class="mdescRight">apply the distributive rule on the BVMULT expression e <a href="#a11422aabc07aa0721cf17b2297a97b40"></a><br/></td></tr>
<tr class="separator:a11422aabc07aa0721cf17b2297a97b40"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aaeb132de41aad56b3bbb5a0c9fcede80"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#aaeb132de41aad56b3bbb5a0c9fcede80">BVMult_order_subterms</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:aaeb132de41aad56b3bbb5a0c9fcede80"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a02032b49999aa3913265a22cac129045"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a02032b49999aa3913265a22cac129045">MarkNonSolvableEq</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:a02032b49999aa3913265a22cac129045"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0e4bd4a89095a5c275cc898b624b9346"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a0e4bd4a89095a5c275cc898b624b9346">zeroExtendRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:a0e4bd4a89095a5c275cc898b624b9346"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aed9f65e2eed1299d80b6ec63274568a4"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#aed9f65e2eed1299d80b6ec63274568a4">repeatRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:aed9f65e2eed1299d80b6ec63274568a4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a9a9c214170ee9595f2eb0b0552b6130f"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a9a9c214170ee9595f2eb0b0552b6130f">rotlRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:a9a9c214170ee9595f2eb0b0552b6130f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aca310d258dd22e4e50b19274047c6528"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#aca310d258dd22e4e50b19274047c6528">rotrRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0</td></tr>
<tr class="separator:aca310d258dd22e4e50b19274047c6528"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a95920e0fd327bc9630d41784449bae0a"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a95920e0fd327bc9630d41784449bae0a">bvUDivConst</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &divExpr)=0</td></tr>
<tr class="separator:a95920e0fd327bc9630d41784449bae0a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab1b7fd737bbf85300e149a0ca1dce266"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#ab1b7fd737bbf85300e149a0ca1dce266">bvUDivTheorem</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &divExpr)=0</td></tr>
<tr class="separator:ab1b7fd737bbf85300e149a0ca1dce266"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a3cf92f9619244e27a40a6b218887cad0"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a3cf92f9619244e27a40a6b218887cad0">bvURemConst</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &remExpr)=0</td></tr>
<tr class="separator:a3cf92f9619244e27a40a6b218887cad0"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0e0a89d5b866cb77e50cc24c20f5d053"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a0e0a89d5b866cb77e50cc24c20f5d053">bvURemRewrite</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &divExpr)=0</td></tr>
<tr class="separator:a0e0a89d5b866cb77e50cc24c20f5d053"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a8737b8dee3cf693cba13dd073b132294"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a8737b8dee3cf693cba13dd073b132294">bvSDivRewrite</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &sDivExpr)=0</td></tr>
<tr class="separator:a8737b8dee3cf693cba13dd073b132294"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a41766b9dbe8dd7e8ebf5cf0349cf2e9e"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a41766b9dbe8dd7e8ebf5cf0349cf2e9e">bvSRemRewrite</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &sRemExpr)=0</td></tr>
<tr class="separator:a41766b9dbe8dd7e8ebf5cf0349cf2e9e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:af8734beba48ae58dd465efd808f73117"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#af8734beba48ae58dd465efd808f73117">bvSModRewrite</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &sModExpr)=0</td></tr>
<tr class="separator:af8734beba48ae58dd465efd808f73117"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a05dd94575cc5674452e2ff63106e2a40"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a05dd94575cc5674452e2ff63106e2a40">bitblastBVMult</a> (const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &a_bits, const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &b_bits, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &a_times_b, std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &output_bits)=0</td></tr>
<tr class="separator:a05dd94575cc5674452e2ff63106e2a40"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a613cf0998893c8b66e40acf63b40a825"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a613cf0998893c8b66e40acf63b40a825">bitblastBVPlus</a> (const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &a_bits, const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &b_bits, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &a_plus_b, std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &output_bits)=0</td></tr>
<tr class="separator:a613cf0998893c8b66e40acf63b40a825"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a91229b0364c30d73cfdb5eba138ba712"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a91229b0364c30d73cfdb5eba138ba712">zeroBVOR</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &orEqZero)=0</td></tr>
<tr class="separator:a91229b0364c30d73cfdb5eba138ba712"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a94e717097d7f4156e647893dd506b91d"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a94e717097d7f4156e647893dd506b91d">oneBVAND</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &andEqOne)=0</td></tr>
<tr class="separator:a94e717097d7f4156e647893dd506b91d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a30e4cf2ef646b5fbc1e0b2b6fb88115a"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a30e4cf2ef646b5fbc1e0b2b6fb88115a">constEq</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &eq)=0</td></tr>
<tr class="separator:a30e4cf2ef646b5fbc1e0b2b6fb88115a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a3b3ae2372cab5026feec302b6bdaa7d6"><td class="memItemLeft" align="right" valign="top">virtual bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a3b3ae2372cab5026feec302b6bdaa7d6">solveExtractOverlapApplies</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &eq)=0</td></tr>
<tr class="separator:a3b3ae2372cab5026feec302b6bdaa7d6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a4e491d1c488cb38d6e22ec21ac894f46"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1BitvectorProofRules.html#a4e491d1c488cb38d6e22ec21ac894f46">solveExtractOverlap</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &eq)=0</td></tr>
<tr class="separator:a4e491d1c488cb38d6e22ec21ac894f46"><td class="memSeparator" colspan="2"> </td></tr>
</table>
<a name="details" id="details"></a><h2 class="groupheader">Detailed Description</h2>
<div class="textblock">
<p>Definition at line <a class="el" href="bitvector__proof__rules_8h_source.html#l00033">33</a> of file <a class="el" href="bitvector__proof__rules_8h_source.html">bitvector_proof_rules.h</a>.</p>
</div><h2 class="groupheader">Constructor & Destructor Documentation</h2>
<a class="anchor" id="a7b9613e9ffdee59c9f70bd06e1a6f29e"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual CVC3::BitvectorProofRules::~BitvectorProofRules </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="bitvector__proof__rules_8h_source.html#l00036">36</a> of file <a class="el" href="bitvector__proof__rules_8h_source.html">bitvector_proof_rules.h</a>.</p>
</div>
</div>
<h2 class="groupheader">Member Function Documentation</h2>
<a class="anchor" id="a6536981ca57bbf915b88a818ad56a1f3"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bitvectorFalseRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">thm</td><td>input theorem: (e1[i]<=>e2[i])<=>false <pre class="fragment"> \result (e1=e2)<=>false</pre> </td></tr>
</table>
</dd>
</dl>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a335f389e282bdb6529f86b2101b330e0">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a27a79309cbbf8554394d32c9773472cc"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bitvectorTrueRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">thm</td><td>input theorem: (~e1[i]<=>e2[i])<=>true <pre class="fragment"> \result (e1!=e2)<=>true</pre> </td></tr>
</table>
</dd>
</dl>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#aafe3a19c755d3559e4c419be7c66d7c5">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a596c0779b2f39d41816ff658eef9203b"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bitBlastEqnRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>f</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>t1=t2 ==> AND_i(t1[i:i] = t2[i:i]) </p>
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">e</td><td>is a <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(t1=t2)</td></tr>
<tr><td class="paramname">f</td><td>is the resulting expression AND_i(t1[i:i] = t2[i:i]) is passed to the rule for efficiency. </td></tr>
</table>
</dd>
</dl>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#adc756096f301c80bb2bf73266c200aff">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="aefb184e963398f43e9dd7a0799563350"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bitBlastDisEqnRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>f</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>t1/=t2 ==> OR_i(NOT t1[i]<=>t2[i]) </p>
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">e</td><td>is a <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>(t1/=t2)</td></tr>
<tr><td class="paramname">f</td><td>is the resulting expression OR_i(NOT t1[i]<=>t2[i]), passed to the rule for efficiency. </td></tr>
</table>
</dd>
</dl>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a9839f27db5f349fe6fb6b21575cde24c">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a06405edfaf820f9b2940ce7bf406615f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::signExtendRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>sign extend the input SX(e) appropriately </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#ae676208401e0d94c96d258f2dd652a68">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a5ca10099b3728f472fc70efbe03fce11"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::padBVLTRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>len</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Pad the kids of BVLT/BVLE to make their length equal. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#ac83f1aeaf2b0dd78c5aec3d4dd605b21">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a9a4fef11fae7f9d9b281876569c3ecaf"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::padBVSLTRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>len</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Sign Extend the kids of BVSLT/BVSLE to make their length equal. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#ab1f7b6923eb8053bbc567f7610458685">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="af472ab5f550394b03c264675181ac1c9"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::signBVLTRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>topBit0</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>topBit1</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>input: e0 <=(s) e1. output depends on whether the topbits(MSB) of e0 and e1 are constants. If they are constants then optimizations are done, otherwise the following rule is implemented.</p>
<p>e0 <=(s) e1 <==> (e0[n-1] AND NOT e1[n-1]) OR (e0[n-1] AND e1[n-1] AND e1[n-2:0] <= e0[n-2:0]) OR (NOT e0[n-1] AND NOT e1[n-1] AND e0[n-2:0] <= e1[n-2:0]) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a1798c9272bc8f7f78100a4fb839fb907">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a7fdf91656d5a4d1b9278e8a974a2578e"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::notBVEQ1Rule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>NOT(e[0][0] = e[0][1]) <==> e[0][0] = ~e[0][1] </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#aff7d8a5558884d2b24e83dc55dc0a59e">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a328733af3be6889566b4ab81c7dd4759"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::notBVLTRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>NOT(e[0][0] < e[0][1]) <==> (e[0][1] <= e[0][0]), NOT(e[0][0] <= e[0][1]) <==> (e[0][1] < e[0][0]) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a15d14a25e4805c5aceff3521f7dbebd0">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a4be7745b6e05010590d15b0ae9f87212"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::lhsEqRhsIneqn </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>kind</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>if(lhs==rhs) then we have (lhs < rhs <==> false),(lhs <= rhs <==> true) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#aa9b8579a600e0c95fbc51a599b03a182">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a7536abc5b7725abfec2d93987cf86a6b"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::zeroLeq </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#ac141b7dc72e52b9b18fd2258db17a952">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a3ce4fc360b44dec2f89d8d597244c305"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bvConstIneqn </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>kind</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a00a6af751fe6354bfd282f5a8f25456a">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a666ed19d6d57236061243c0951ee6228"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::generalIneqn </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>e0</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>e1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>kind</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a9e41265f17a1d607e9559bb718963f0a">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ad63871213ec8c864a622bb3d2248b043"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bitExtractAllToConstEq </td>
<td>(</td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>thms</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a70fb1053bd8518120c0d69dca9069062">CVC3::BitvectorTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="theory__bitvector_8cpp_source.html#l02512">CVC3::TheoryBitvector::comparebv()</a>.</p>
</div>
</div>
<a class="anchor" id="a77c82c6fccba740e2df14739edb40a02"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bitExtractToExtract </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>t[i] ==> t[i:i] = 0bin1 or NOT t[i] ==> t[i:i] = 0bin0 </p>
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">thm</td><td>is a Theorem(t[i]) or Theorem(NOT t[i]), where t[i] is BOOLEXTRACT(t, i). </td></tr>
</table>
</dd>
</dl>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#ae7cdd320c7fb8e16f943626d07d9f63b">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a79a44f95f79735f733cd75f289887da9"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bitExtractRewrite </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>x</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>t[i] <=> t[i:i][0] (to use rewriter for simplifying t[i:i]) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a8dab3dc6ffdf47a18f6097ad0185b4de">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ace62b8eacaad88c90231099943a49090"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bitExtractConstant </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>x</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">x</td><td>is bitvector constant </td></tr>
<tr><td class="paramname">i</td><td>is extracted bitposition</td></tr>
</table>
</dd>
</dl>
<dl class="section return"><dt>Returns</dt><dd><p class="formulaDsp">
<img class="formulaDsp" alt="\[ \frac{}{\mathrm{BOOLEXTRACT(x,i)} \iff \mathrm{TRUE}} \]" src="form_308.png"/>
</p>
, if bitposition has a 1; <p class="formulaDsp">
<img class="formulaDsp" alt="\[ \frac{}{\mathrm{BOOLEXTRACT(x,i)} \iff \mathrm{FALSE}} \]" src="form_309.png"/>
</p>
, if the bitposition has a 0 </dd></dl>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#ad14158d7d8b6a1ccf2b6c47991d498d7">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a14d171b56b3318b1a070fc2c0798f038"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bitExtractConcatenation </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>x</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">x</td><td>is bitvector binary concatenation </td></tr>
<tr><td class="paramname">i</td><td>is extracted bitposition</td></tr>
</table>
</dd>
</dl>
<dl class="section return"><dt>Returns</dt><dd><p class="formulaDsp">
<img class="formulaDsp" alt="\[ \frac{}{(t_{[m]}@q_{[n]})[i] \iff (q_{[n]})[i]} \]" src="form_310.png"/>
</p>
, where <p class="formulaDsp">
<img class="formulaDsp" alt="\[ 0 \geq i \geq n-1 \]" src="form_311.png"/>
</p>
, another case of boolextract over concatenation is: <p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{}{(t_{[m]}@q_{[n]})[i] \iff (t_{[m]})[i-n]} \]" src="form_312.png"/>
</p>
, where <p class="formulaDsp">
<img class="formulaDsp" alt="\[ n \geq i \geq m+n-1 \]" src="form_313.png"/>
</p>
</dd></dl>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a571db5dc21ec0b24e1d861c137892f9c">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a14a48b5e0170be003c5a52585654fa6c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bitExtractConstBVMult </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>t</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">t</td><td>is bitvector binary BVMULT. x[0] must be BVCONST </td></tr>
<tr><td class="paramname">i</td><td>is extracted bitposition</td></tr>
</table>
</dd>
</dl>
<dl class="section return"><dt>Returns</dt><dd>bitblast of BVMULT </dd></dl>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#abf6f1ff706f6cefe196b1cbe7d5f85c1">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ac473ab04bc4692de3ff7f19940d4a3a2"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bitExtractBVMult </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>t</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">t</td><td>: input1 is bitvector binary BVMULT. t[0] must not be BVCONST </td></tr>
<tr><td class="paramname">i</td><td>: input2 is extracted bitposition</td></tr>
</table>
</dd>
</dl>
<dl class="section return"><dt>Returns</dt><dd>bitblast of BVMULT </dd></dl>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a0425488c3b01eb65554867483e3cac02">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ae46b941cbb7c67aec7a96a45b33e73ab"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bitExtractExtraction </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>x</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">x</td><td>is bitvector extraction e[k:j] </td></tr>
<tr><td class="paramname">i</td><td>is extracted bitposition</td></tr>
</table>
</dd>
</dl>
<dl class="section return"><dt>Returns</dt><dd><p class="formulaDsp">
<img class="formulaDsp" alt="\[ \frac{}{(t_{[n]}[k:j])[i] \iff (t_{[n]})[i+j]} \]" src="form_314.png"/>
</p>
, where <p class="formulaDsp">
<img class="formulaDsp" alt="\[ 0 \geq j \geq k < n, 0 \geq i < k-j \]" src="form_315.png"/>
</p>
</dd></dl>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a8efcf949614eab1089f00519f1db57bb">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ab60522e7672d31bcf2957d1cbd118208"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bitExtractBVPlus </td>
<td>(</td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>t1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>t2</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>bvPlusTerm</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">t1</td><td>is vector of bitblasts of t, from bit i-1 to 0 </td></tr>
<tr><td class="paramname">t2</td><td>is vector of bitblasts of q, from bit i-1 to 0 </td></tr>
<tr><td class="paramname">bvPlusTerm</td><td>is BVPLUS term: BVPLUS(n,t,q) </td></tr>
<tr><td class="paramname">i</td><td>is extracted bitposition</td></tr>
</table>
</dd>
</dl>
<dl class="section return"><dt>Returns</dt><dd>The base case is: <p class="formulaDsp">
<img class="formulaDsp" alt="\[ \frac{}{(\mathrm{BVPLUS}(n,t,q))[0] \iff t[0] \oplus q[0]} \]" src="form_316.png"/>
</p>
, when <p class="formulaDsp">
<img class="formulaDsp" alt="\[ 0 < i \leq n-1 \]" src="form_317.png"/>
</p>
, we have <p class="formulaDsp">
<img class="formulaDsp" alt="\[ \frac{}{(\mathrm{BVPLUS}(n,t,q))[i] \iff t[i] \oplus q[i] \oplus c(t,q,i)} \]" src="form_318.png"/>
</p>
, where c(t,q,i) is the carry generated by the addition of bits from 0 to i-1 </dd></dl>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a6c02b66248026d3ffb357e980de37ed7">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ab521ae872e2a877f5e30ec9f1b8ded8f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bitExtractBVPlusPreComputed </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>t1_i</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>t2_i</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>bvPlusTerm</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>bitPos</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>precomputed</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#aaf4999f69872e881257cd1e127732ec8">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a0836ea2282578bd221ade4a06d0abc2e"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bvPlusAssociativityRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>bvPlusTerm</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">bvPlusTerm</td><td>: input1 is bvPlusTerm, a BVPLUS term with arity > 2</td></tr>
</table>
</dd>
</dl>
<dl class="section return"><dt>Returns</dt><dd>: output is iff-Theorem: bvPlusTerm <==> outputTerm, where outputTerm is an equivalent BINARY bvplus. </dd></dl>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a415c16ecc3bbdd0942801028526d641f">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a40fd98cf00aa03114e7bdf0e164abe69"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bitExtractNot </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>x</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">x</td><td>: input1 is bitwise NEGATION </td></tr>
<tr><td class="paramname">i</td><td>: input2 is extracted bitposition</td></tr>
</table>
</dd>
</dl>
<dl class="section return"><dt>Returns</dt><dd><p class="formulaDsp">
<img class="formulaDsp" alt="\[ \frac{}{(\sim t_{[n]})[i] \iff \neg (t_{[n]}[i])} \]" src="form_319.png"/>
</p>
</dd></dl>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a43201ddd283a81a44095658241ca2a5e">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a9f09c5a49fd132f26a01ec7d96168e42"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bitExtractBitwise </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>x</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>kind</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Extract from bitwise AND, OR, or XOR. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#acd7ddad997b468fbb64373913e03b5e9">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a3c7217656c1f4bdd8ab08e415ef3dc7d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bitExtractFixedLeftShift </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>x</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">x</td><td>: input1 is bitvector FIXED SHIFT <p class="formulaDsp">
<img class="formulaDsp" alt="\[ e_{[n]} \ll k \]" src="form_320.png"/>
</p>
</td></tr>
<tr><td class="paramname">i</td><td>: input2 is extracted bitposition</td></tr>
</table>
</dd>
</dl>
<dl class="section return"><dt>Returns</dt><dd><p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{}{(e_{[n]} \ll k)[i] \iff \mathrm{FALSE}} \]" src="form_321.png"/>
</p>
, if 0 <= i < k. however, if k <= i < n then, result is <p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{}{(e_{[n]} \ll k)[i] \iff e_{[n]}[i]} \]" src="form_322.png"/>
</p>
</dd></dl>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a4153b23dadd58aea7bde7f71001aad91">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a8671b7ed4e5e09402cf5a732fb13a373"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bitExtractFixedRightShift </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>x</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a2db4c3bb12bae8276f7c542936989d83">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="afcd3c4de329e1b2912d83853be46130a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bitExtractBVSHL </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>x</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a2b273a0a3bb7a39646f0fb065e954ccc">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="aebe59090c69f529aa1450a64f2d80538"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bitExtractBVLSHR </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>x</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#afc17991261fb1f240861496d391c452a">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a95f41581d03d993ec02541ec78fbd655"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bitExtractBVASHR </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>x</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#ad9256452fce83e6505d94f2a11b2a463">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ae806df67b545215d677ccd81b68c9b16"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::zeroPaddingRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>r</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">e</td><td>: input1 is bitvector term </td></tr>
<tr><td class="paramname">r</td><td>: input2 is extracted bitposition</td></tr>
</table>
</dd>
</dl>
<dl class="section return"><dt>Returns</dt><dd>we check if r > bvlength(e). if yes, then return BOOLEXTRACT(e,r) <==> FALSE; else raise soundness exception. (Note: this rule is used in BVPLUS bitblast function) </dd></dl>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a6c59521b4540e2acd1fe954272bf3e09">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a0520e4a3cf5ce89aaa0cf24c1cf5dd9a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bitExtractSXRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a1d749524ddb67fa00fc4da46df1156c9">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ad88adf2f899f5eab5c0de7c09892178f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::eqConst </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>c1=c2 <=> TRUE/FALSE (equality of constant bitvectors) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#aaa38beb3d8990340aa5867f09900f14e">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a72537952b59dbed6451fe20803e565a6"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::eqToBits </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>eq</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>|- c1=c2 ==> |- AND(c1[i:i] = c2[i:i]) - expanding equalities into bits </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a58ce4c07a8d005fa6d9820abc5fac028">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a2944e9810307f39e543f8fa6b973f0a8"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::leftShiftToConcat </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>t<<n = c @ 0bin00...00, takes e == (t<<n) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a68fd84ca46b0e62103314c45dee495bd">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="aaf79659bd7a160d20c3d27d7746d9ca3"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::constWidthLeftShiftToConcat </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>t<<n = c @ 0bin00...00, takes e == (t<<n) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#aabb5f8d91314adc4688e5970b986edf0">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ab2d4f1d9f2f71845d0e2efb2e9ab0f02"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::rightShiftToConcat </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>t>>m = 0bin00...00 @ t[bvlength-1:m], takes e == (t>>n) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a7d91d285e929d00572f3da4da772f505">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="aa665d97eb8067ae68741a6e25135e307"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bvshlToConcat </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>BVSHL(t,c) = t[n-c,0] @ 0bin00...00. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#ae47b2ec2a40c3376071ed60c16d457b6">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ab3a7d61a6e1627433906f527f89e300b"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bvshlSplit </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>BVSHL(t,c) = IF (c = 0) THEN t ELSE IF (c = 1) ... </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a431507c9e35ad328509072cea05f2d8e">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a994aa73b02c523cd2e9e76a4880a167b"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bvlshrToConcat </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>BVLSHR(t,c) = 0bin00...00 @ t[n-1,c]. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a5f99ee62c0847affeb44264840764b43">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a52acdd1024ed2ab0737c7747102fa7fe"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bvShiftZero </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Any shift over a zero = 0. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a61b2ded76e35d870b15502ab0641010d">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a42639e0098377ce718308a2ae833430b"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bvashrToConcat </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>BVASHR(t,c) = SX(t[n-1,c], n-1) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a3c3a4d49d47a08a3eb7599327f30f324">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="af126175b4dbb92231ec44c14f32d8b21"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::rewriteXNOR </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>a XNOR b <=> (~a & ~b) | (a & b) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a70ad43279f8061f7be4e35c49205ab69">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a53c8279d20f7d229437790ce6c0da2da"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::rewriteNAND </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>a NAND b <=> ~(a & b) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a2d49a06be7aae5f5675977fdc1b6457e">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a8e2d34a4c387bd5eace8b7e6237bd936"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::rewriteNOR </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>a NOR b <=> ~(a | b) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a372c699b42bb9ab8b64e2a836bedcffd">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="acccc78337e0a0143b9635e1cd49ac657"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::rewriteBVCOMP </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>BVCOMP(a,b) <=> ITE(a=b,0bin1,0bin0) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#ab314017086d977ee1f4facb23208864c">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a693f8801e36967bf64a0fef0290cad5a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::rewriteBVSub </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>a - b <=> a + (-b) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a1a040de059cc4fedf5cdd00cec37fc9c">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ac132cce6c99ee7626ee4696010e77aa6"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::constMultToPlus </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>k*t = BVPLUS(n, <sum of shifts of t>) – translation of k*t to BVPLUS </p>
<p>If k = 2^m, return k*t = t@0...0 </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a560ad9ec684e523f941c2d12fa833cd1">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a425296e1ac48c9698802b9a7513745d5"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bvplusZeroConcatRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>0bin0...0 @ BVPLUS(n, args) = BVPLUS(n+k, args) </p>
<p>provided that m+ceil(log2(l)) <= n, where k is the size of the 0bin0...0, m is the max. length of each argument, and l is the number of arguments. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#af734405e15de47e28f4112e07bfc9dba">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a0dacf60fcac4bbbcc45019a5c58d576c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::zeroCoeffBVMult </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a6d773885e3e78a736cd22dd79835b9e3">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a99efc60c900f6818e718eaa76634f82d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::oneCoeffBVMult </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a916fcffc7cb40f2159b00a710c26f669">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ae17fc2f1a86046cc389e4f828ce6043c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::flipBVMult </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a9ed93437abb38597bbf7d153184c70e5">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a534b8599309b8a1f04355f974450eb44"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::padBVPlus </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Make args the same length as the result (zero-extend) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#aa3d3d7bff1a088fa66a19076c471571a">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a185de05a96896134fb0c204bfa2b701f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::padBVMult </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Make args the same length as the result (zero-extend) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#ac8509af4659a1391e983939d825f0e85">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a47645c759c4c43b1336d6aa8ea4bef24"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bvConstMultAssocRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a67921f96646d6b01d62d8a1cd116ddb3">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a06eb338d6dbad205f7ce886b94866e01"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bvMultAssocRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#afa7daebdee6dafd361980583b6d3ffe1">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a0a00757ccf2b0b5115003629085752f5"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bvMultDistRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a44e37a65f45da9fb8469a0003a140836">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a5c1a3b38a87b8cdf2fe7674b0c50c8ed"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::flattenBVPlus </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a2a66e5fbe24e038a79ac07290900fdd4">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a88dbf100f26bd80ac71b976513cf5ed0"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::combineLikeTermsRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a2a6308a817bfe26b843612fd02ba5441">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ad7df7b16e4ba8d0a84163dac7a3fd29d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::lhsMinusRhsRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a85f807faae622c7c6cb9d85cad0c5fc3">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="aa3c6172968875b9189228eb7f8c50187"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::extractBVMult </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>(x *[n] y)[m:k] = (x *[m+1] y)[m:k], where m < n </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a5df17d5d90f8a7389808a870a90ae863">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a144383710caebde013be9b2cefce5a4c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::extractBVPlus </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>(x +[n] y)[m:k] = (x +[m+1] y)[m:k], where m < n </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#aabeacfb4b8a65744ac53f2cfe5dadc74">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="adabf3a32d5a2444ca64e2f66a414f185"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::iteExtractRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>ite(c,t1,t2)[i:j] <=> ite(c,t1[i:j],t2[i:j]) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a35d8c914e411c866485e17febed62c00">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ae25244a21bbc10ad069c9c98ac49590e"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::iteBVnegRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>~ite(c,t1,t2) <=> ite(c,~t1,~t2) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a5bd890187bf9297b3b1092c623c1d922">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="afb6657218e31843d4f9fb55494133a51"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bvuminusBVConst </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#ac0f04eeb2cf6b89dbbcf8849bea4e40b">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ae96c6008f1ded31a7d8985264594cbbc"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bvuminusBVMult </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a84fcae86e983ecd86c77705c8a749576">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a331e5974d6b4cf1458501aba9c4a2556"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bvuminusBVUminus </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a256b7d97aae2e5933ac4a9161c2da211">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="aaa564090b043862b11ce47d777a9c959"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bvuminusVar </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a6c8e614b400899e9f7e28cbfb6129a2a">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a63c42dbedb2f04af9dd61d6b104c42f0"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bvmultBVUminus </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a4b76e0978912f6211ce0549cb9dd8550">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ab7d869044d0d907fb1066e706039ca68"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bvuminusToBVPlus </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>-t <==> ~t+1 </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a4ede1f1385025a1621114addc25569c1">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ac77eea8dcc7f833bb3f426fd3f021a93"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bvuminusBVPlus </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>-(c1*t1+...+cn*tn) <==> (-(c1*t1)+...+-(cn*tn)) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a126c38f580c510745dacd0dea2cb5c15">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a56770462de38c0c8eed61d1f33c77d6c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::extractConst </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>c1[i:j] = c (extraction from a constant bitvector) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a8c0923ca7a786c2a7ee60cc7b456a9e0">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ae9d9e1338cf24b20f8eb713fbd9b0219"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::extractWhole </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>t[n-1:0] = t for n-bit t </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a8f8cd95c4037ee94e91ba93fe7d869c0">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a7fc72894f97ec709bf1558254e40903e"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::extractExtract </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>t[i:j][k:l] = t[k+j:l+j] (eliminate double extraction) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a5c7969edaba735a5f73258b57ea42184">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a483af962d2b2c8390207e94bd2ae6dc1"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::extractConcat </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>(t1 @ t2)[i:j] = t1[...] @ t2[...] (push extraction through concat) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#ad3f6288f648cee583f8dfee29fc97112">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a9c8be2deedd7168a29b288737cd050a8"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::extractAnd </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>(t1 & t2)[i:j] = t1[i:j] & t2[i:j] (push extraction through OR) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a0b3d60749f5bc14f524e0f5234bb1cf3">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a7cdfdc4ac2ed578d2c584549b8a374a7"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::extractOr </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>(t1 | t2)[i:j] = t1[i:j] | t2[i:j] (push extraction through AND) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a7a8f90ee8e8450bcb4bfe3e1f231c4b0">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ac258a650188de30470eae5c53116abfd"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::extractNeg </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>(~t)[i:j] = ~(t[i:j]) (push extraction through NEG) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a8014d2c21597d514e39a4fba8a060952">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a548cc7ab83b3d604226f09235d2097bf"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::extractBitwise </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>kind</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>name</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Auxiliary function: (t1 op t2)[i:j] = t1[i:j] op t2[i:j]. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a222240751acfa38ed43f717c803aca34">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a76151013db10b5faa12ba32ad2374fc6"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::negConst </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>~c1 = c (bit-wise negation of a constant bitvector) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a28038efe4f40407c727f91d856234d49">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a9c4a53c0c1961951e3d847394bfa1b20"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::negConcat </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>~(t1@...@tn) = (~t1)@...@(~tn) – push negation through concat </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a8e1501e7e12f93e385f77c75a931b970">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ac6cbc581e757d482483d62366e84afb9"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::negNeg </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>~(~t) = t – eliminate double negation </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#ae2ec10b9faef513781d02bb81cc3e88b">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a13eeb7dac6de93650d885b61eb72e0ad"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::negElim </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>~t = -1*t + 1 – eliminate negation </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a8e6947b16b14750e13812e43b9f5080c">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a4fb78e904f25388d54eb0ba54ced536d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::negBVand </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>~(t1 & t2) <=> ~t1 | ~t2 – DeMorgan's Laws </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#abc285ae73d2259fe1efea8cb46b2698a">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a5763889eb6cd07ab04d4c98686db01cf"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::negBVor </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>~(t1 | t2) <=> ~t1 & ~t2 – DeMorgan's Laws </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#abf45c19e2d11f75d68785cc88f7ccf32">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a2b4170a86c6978a77c338dbf832929ad"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::negBVxor </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>~(t1 xor t2) = ~t1 xor t2 </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a815029f46058047bfe8a5e0dbc85ddc6">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="accade48c8a792079d97d49d92dc2abee"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::negBVxnor </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>~(t1 xnor t2) = t1 xor t2 </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a2388a9d25fafcd0711a286d4666ee960">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="abc8792717d3f194aa05f279f63033ec1"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bitwiseConst </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< int > & </td>
<td class="paramname"><em>idxs</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>kind</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Combine constants in bitwise AND, OR, XOR. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#af3928b2385a298cc085134ac1e8222e4">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a29d3cce157edf35040c7c237570e37c9"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bitwiseConcat </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>kind</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Lifts concatenation above bitwise operators. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a731d832fce739c8b6d7b5ccf9932a94a">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a78d58f8b598713266bad87dcfba0d93b"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bitwiseFlatten </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>kind</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Flatten bitwise operation. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#ac6e8075bfc61e657a37648ba78003f36">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ab67de0bd797585c3a5cfa3d80a4bfa42"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bitwiseConstElim </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>idx</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>kind</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Simplify bitwise operator containing a constant child. </p>
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">e</td><td>is the bit-wise expr </td></tr>
<tr><td class="paramname">idx</td><td>is the index of the constant bitvector </td></tr>
<tr><td class="paramname">kind</td><td>is the kind of e </td></tr>
</table>
</dd>
</dl>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#aac798843b8390b423f901f9cc1cb14dd">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a067fc47b8a688b6a08b94c5044d2faf5"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::concatConst </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>c1@c2@...@cn = c (concatenation of constant bitvectors) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#abee7fa8ab42b1addc72b7463b4a60975">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a06461d9c64f09ce1dc9acf6cb0628977"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::concatFlatten </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Flatten one level of nested concatenation, e.g.: x@(y@z)@w = x@y@z@w. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#adba6266c081af892dadf257a001ae920">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="adec7f3c93376d5e5c0abb20fc3b44eb9"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::concatMergeExtract </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Merge n-ary concat. of adjacent extractions: x[15:8]@x[7:0] = x[15:0]. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#af8c35b9567c60d128480b278de348842">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a70ff8e2477ef2d049bd33d1a4bab482e"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bvplusConst </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>BVPLUS(n, c1,c2,...,cn) = c (bit-vector plus of constant bitvectors) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a8475377c17d5c4241e1a134ce5b28eba">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ae0c8cdf3fade0ff0824c6112f4bdec0c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bvmultConst </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>n*c1 = c, where n >= 0 (multiplication of a constant bitvector by a non-negative constant) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a05e4123ccbc5000dbf9615d89e13067d">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a2096bde76317290227a520452a3ab4c4"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::typePredBit </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>|- t=0 OR t=1 for any 1-bit bitvector t </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#aea2fb217bff7c7b46f996eacd051461b">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="acff4dd7561fb19a337f76edfa024c1aa"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::expandTypePred </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>tp</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Expand the type predicate wrapper (compute the actual type predicate) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a7d8030814a36206774951e3ae8968848">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="aef8e88512f778d081ade97e6304f1d18"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::isolate_var </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>isolate a variable with coefficient = 1 on the Lhs of an </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a54d8f6979007cfc5e0da1ebf7f73f51d">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a17c15204dfec661af091bb07f44c4f51"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::liftConcatBVMult </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a91a4bd06c22c93729e954302840877ad">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a74f5018affcab70b831029b390692552"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::canonBVMult </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>canonize BVMult expressions in order to get one coefficient </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#aa5acae5a384220d4dca181b8675831b3">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="affb1cdfd198f4140f1943f9296b1b97c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::liftConcatBVPlus </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a5fb475feef8b6740cc8c2f5f2104f07d">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a07f756438b45b15b493497341944bbb4"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::canonBVPlus </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>canonize BVPlus expressions in order to get just one </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a31b9e200eff6852b66a8d8ac19ec2db3">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="acb966a104436262e81299cea86bc21bb"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::canonBVUMinus </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#af3fc29529753dc8161360688bcaaf12b">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ac018d05ae792d761195fbcc9731017d0"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::processExtract </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool & </td>
<td class="paramname"><em>solvedForm</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a8475d9fad4a99ea877f69e154f1d67d6">CVC3::BitvectorTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="theory__bitvector_8cpp_source.html#l02818">CVC3::TheoryBitvector::solve()</a>.</p>
</div>
</div>
<a class="anchor" id="a04f65b94c6a9ca2b84a6063aac0d082f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::canonBVEQ </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>maxEffort</em> = <code>3</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#ac946768d5a1aae35472b63b53b457264">CVC3::BitvectorTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="theory__bitvector_8cpp_source.html#l02409">CVC3::TheoryBitvector::generalBitBlast()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l02366">CVC3::TheoryBitvector::simplifyPendingEq()</a>, and <a class="el" href="theory__bitvector_8cpp_source.html#l02818">CVC3::TheoryBitvector::solve()</a>.</p>
</div>
</div>
<a class="anchor" id="a11422aabc07aa0721cf17b2297a97b40"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::distributive_rule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>apply the distributive rule on the BVMULT expression e </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a9fe7ec7e369ee92339471e805a1dd7c3">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="aaeb132de41aad56b3bbb5a0c9fcede80"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::BVMult_order_subterms </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a87288805014f1d0e935c052364142d6b">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a02032b49999aa3913265a22cac129045"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::MarkNonSolvableEq </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a0f02e48875ccb661cae7cc7a2489dce1">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a0e4bd4a89095a5c275cc898b624b9346"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::zeroExtendRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a8295f4644a077f3c8af0db53be7b458b">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="aed9f65e2eed1299d80b6ec63274568a4"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::repeatRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a9b9a128c7c863d01c804bfec956ffb6c">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a9a9c214170ee9595f2eb0b0552b6130f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::rotlRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#afdc5b05255d1d217c26d5e3660957fde">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="aca310d258dd22e4e50b19274047c6528"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::rotrRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a6495867fe7ef34a838e83315dd8b02e4">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a95920e0fd327bc9630d41784449bae0a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bvUDivConst </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>divExpr</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Divide a with b unsigned and return the bit-vector constant result </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#acc221d6c256b7d550090627e6fee9643">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="ab1b7fd737bbf85300e149a0ca1dce266"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bvUDivTheorem </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>divExpr</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Rewrite a/b with a fresh variable d and add the constraints to make it be a divider. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a330fc1ea75378bfe0fec034132af7400">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a3cf92f9619244e27a40a6b218887cad0"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bvURemConst </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>remExpr</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Divide a with b unsigned and return the bit-vector constant result </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#af8bafa1141beb24e3742bce376697e8f">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a0e0a89d5b866cb77e50cc24c20f5d053"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bvURemRewrite </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>divExpr</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Rewrite ab in terms of a/b, i.e. a - a/b </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#aa6941790eb888168ffdc5531b129b466">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a8737b8dee3cf693cba13dd073b132294"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bvSDivRewrite </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>sDivExpr</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Rewrite the signed divide in terms of the unsigned one. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#ad3bdebd3ad40f70a1592fda3fae82e71">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a41766b9dbe8dd7e8ebf5cf0349cf2e9e"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bvSRemRewrite </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>sRemExpr</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Rewrite the signed remainder in terms of the unsigned one. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a73632313f926e7b93104538c465bbcfb">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="af8734beba48ae58dd465efd808f73117"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bvSModRewrite </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>sModExpr</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Rewrite the signed mod in terms of the unsigned one. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a8d5827e983be4b7ed387314332ac4613">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a05dd94575cc5674452e2ff63106e2a40"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bitblastBVMult </td>
<td>(</td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>a_bits</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>b_bits</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>a_times_b</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>output_bits</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Bit-blast the multiplication a_times_b given the bits in a_bits and b_bits. The resulting output bits will be in the vector output_bits. The return value is a theorem saying there is no overflow for this multiplication. (TODO, it's just an empty theorem for now). </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a714a402f525e0d0c222846379366edc5">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a613cf0998893c8b66e40acf63b40a825"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::bitblastBVPlus </td>
<td>(</td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>a_bits</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>b_bits</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>a_plus_b</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>output_bits</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Bit-blast the sum a_times_b given the bits in a_bits and b_bits. The resulting output bits will be in the vector output_bits. The return value is a theorem saying there is no overflow for this sum. (TODO, it's just an empty theorem for now). </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#aef3181ea41680c3f7b1b4ec724e8b68d">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a91229b0364c30d73cfdb5eba138ba712"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::zeroBVOR </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>orEqZero</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Rewrite </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[x_1 \vee x_2 \vee \ldots \vee x_n = 0\]" src="form_323.png"/>
</p>
<p> into </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[x_1 = 0 \wedge x_2 = 0 \wedge \ldots \wedge x_n = 0\]" src="form_324.png"/>
</p>
<p>. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a9200f74bce7930bb77d5e2a00b81a1d4">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a94e717097d7f4156e647893dd506b91d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::oneBVAND </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>andEqOne</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Rewrite </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[x_1 \wedge x_2 \wedge \ldots \wedge x_n = 1^n\]" src="form_325.png"/>
</p>
<p> into </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[x_1 = 1^n \wedge x_2 = 1^n \wedge \ldots \wedge x_n = 1^n\]" src="form_326.png"/>
</p>
<p>. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a1d422c14bfbcac9e91c53260b856b93e">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a30e4cf2ef646b5fbc1e0b2b6fb88115a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::constEq </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>eq</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Equalities over constants go to true/false. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a9c0a8eae91823c04c12dbedbbbbd417f">CVC3::BitvectorTheoremProducer</a>.</p>
</div>
</div>
<a class="anchor" id="a3b3ae2372cab5026feec302b6bdaa7d6"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual bool CVC3::BitvectorProofRules::solveExtractOverlapApplies </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>eq</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Returns true if equation is of the form x[i:j] = x[k:l], where the extracted segments overlap, i.e. i > j >= k > l or k > i >= l > j. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#adf540a2323b9f9ba281d2d67826cdae7">CVC3::BitvectorTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="theory__bitvector_8cpp_source.html#l02818">CVC3::TheoryBitvector::solve()</a>.</p>
</div>
</div>
<a class="anchor" id="a4e491d1c488cb38d6e22ec21ac894f46"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::BitvectorProofRules::solveExtractOverlap </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>eq</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Returns the theorem that simplifies the equality of two overlapping extracts over the same term. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a79998a92001fa8625a471bf7011b9cd3">CVC3::BitvectorTheoremProducer</a>.</p>
<p>Referenced by <a class="el" href="theory__bitvector_8cpp_source.html#l02818">CVC3::TheoryBitvector::solve()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following file:<ul>
<li><a class="el" href="bitvector__proof__rules_8h_source.html">bitvector_proof_rules.h</a></li>
</ul>
</div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:19 for CVC3 by  <a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/>
</a> 1.8.2
</small></address>
</body>
</html>
