<!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: bitvector_theorem_producer.h Source File</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><a href="annotated.html"><span>Classes</span></a></li>
<li class="current"><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="files.html"><span>File List</span></a></li>
<li><a href="globals.html"><span>File Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="dir_68267d1309a1af8e8297ef4c3efbcdba.html">src</a></li><li class="navelem"><a class="el" href="dir_e4adeda04d5be4768968997038f0705c.html">theory_bitvector</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="headertitle">
<div class="title">bitvector_theorem_producer.h</div> </div>
</div><!--header-->
<div class="contents">
<a href="bitvector__theorem__producer_8h.html">Go to the documentation of this file.</a><div class="fragment"><div class="line"><a name="l00001"></a><span class="lineno"> 1</span> <span class="comment">/*****************************************************************************/</span><span class="comment"></span></div>
<div class="line"><a name="l00002"></a><span class="lineno"> 2</span> <span class="comment">/*!</span></div>
<div class="line"><a name="l00003"></a><span class="lineno"> 3</span> <span class="comment"> * \file bitvector_theorem_producer.h</span></div>
<div class="line"><a name="l00004"></a><span class="lineno"> 4</span> <span class="comment"> * \brief TRUSTED implementation of bitvector proof rules</span></div>
<div class="line"><a name="l00005"></a><span class="lineno"> 5</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00006"></a><span class="lineno"> 6</span> <span class="comment"> * Author: Vijay Ganesh</span></div>
<div class="line"><a name="l00007"></a><span class="lineno"> 7</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00008"></a><span class="lineno"> 8</span> <span class="comment"> * Created: Wed May 5 16:10:28 PST 2004</span></div>
<div class="line"><a name="l00009"></a><span class="lineno"> 9</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00010"></a><span class="lineno"> 10</span> <span class="comment"> * <hr></span></div>
<div class="line"><a name="l00011"></a><span class="lineno"> 11</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00012"></a><span class="lineno"> 12</span> <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span></div>
<div class="line"><a name="l00013"></a><span class="lineno"> 13</span> <span class="comment"> * and its documentation for any purpose is hereby granted without</span></div>
<div class="line"><a name="l00014"></a><span class="lineno"> 14</span> <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span></div>
<div class="line"><a name="l00015"></a><span class="lineno"> 15</span> <span class="comment"> * LICENSE file provided with this distribution.</span></div>
<div class="line"><a name="l00016"></a><span class="lineno"> 16</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00017"></a><span class="lineno"> 17</span> <span class="comment"> * <hr></span></div>
<div class="line"><a name="l00018"></a><span class="lineno"> 18</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00019"></a><span class="lineno"> 19</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00020"></a><span class="lineno"> 20</span> <span class="comment">/*****************************************************************************/</span></div>
<div class="line"><a name="l00021"></a><span class="lineno"> 21</span> </div>
<div class="line"><a name="l00022"></a><span class="lineno"> 22</span> <span class="preprocessor">#ifndef _cvc3__bitvector_theorem_producer_h_</span></div>
<div class="line"><a name="l00023"></a><span class="lineno"> 23</span> <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__bitvector_theorem_producer_h_</span></div>
<div class="line"><a name="l00024"></a><span class="lineno"> 24</span> <span class="preprocessor"></span></div>
<div class="line"><a name="l00025"></a><span class="lineno"> 25</span> <span class="preprocessor">#include "<a class="code" href="bitvector__proof__rules_8h.html" title="Arithmetic proof rules.">bitvector_proof_rules.h</a>"</span></div>
<div class="line"><a name="l00026"></a><span class="lineno"> 26</span> <span class="preprocessor">#include "<a class="code" href="theorem__producer_8h.html">theorem_producer.h</a>"</span></div>
<div class="line"><a name="l00027"></a><span class="lineno"> 27</span> </div>
<div class="line"><a name="l00028"></a><span class="lineno"> 28</span> <span class="keyword">namespace </span>CVC3 {</div>
<div class="line"><a name="l00029"></a><span class="lineno"> 29</span> </div>
<div class="line"><a name="l00030"></a><span class="lineno"> 30</span>  <span class="keyword">class </span>TheoryBitvector;</div>
<div class="line"><a name="l00031"></a><span class="lineno"> 31</span> <span class="comment"></span></div>
<div class="line"><a name="l00032"></a><span class="lineno"> 32</span> <span class="comment"> /*! @brief This class implements proof rules for bitvector</span></div>
<div class="line"><a name="l00033"></a><span class="lineno"> 33</span> <span class="comment"> * normalizers (concatenation normal form, bvplus normal form),</span></div>
<div class="line"><a name="l00034"></a><span class="lineno"> 34</span> <span class="comment"> * bitblaster rules, other relevant rewrite rules for bv arithmetic</span></div>
<div class="line"><a name="l00035"></a><span class="lineno"> 35</span> <span class="comment"> * and word-level operators</span></div>
<div class="line"><a name="l00036"></a><span class="lineno"> 36</span> <span class="comment"> */</span><span class="comment"></span></div>
<div class="line"><a name="l00037"></a><span class="lineno"> 37</span> <span class="comment"> /*!</span></div>
<div class="line"><a name="l00038"></a><span class="lineno"> 38</span> <span class="comment"> Author: Vijay Ganesh, May-August, 2004</span></div>
<div class="line"><a name="l00039"></a><span class="lineno"> 39</span> <span class="comment"></span></div>
<div class="line"><a name="l00040"></a><span class="lineno"> 40</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00041"></a><span class="lineno"><a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html"> 41</a></span>  <span class="keyword">class </span><a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html" title="This class implements proof rules for bitvector normalizers (concatenation normal form...">BitvectorTheoremProducer</a>:</div>
<div class="line"><a name="l00042"></a><span class="lineno"> 42</span>  <span class="keyword">public</span> <a class="code" href="classCVC3_1_1BitvectorProofRules.html">BitvectorProofRules</a>, <span class="keyword">public</span> <a class="code" href="classCVC3_1_1TheoremProducer.html">TheoremProducer</a> {</div>
<div class="line"><a name="l00043"></a><span class="lineno"> 43</span>  <span class="keyword">private</span>:</div>
<div class="line"><a name="l00044"></a><span class="lineno"><a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#adac6d564649b68cf95c22a82cefbbe72"> 44</a></span>  <a class="code" href="classCVC3_1_1TheoryBitvector.html" title="Theory of bitvectors of known length \ (operations include: @,[i:j],[i],+,.,BVAND,BVNEG)">TheoryBitvector</a>* <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#adac6d564649b68cf95c22a82cefbbe72">d_theoryBitvector</a>; <span class="comment">//! instance of bitvector DP</span></div>
<div class="line"><a name="l00045"></a><span class="lineno"> 45</span> <span class="comment"></span><span class="comment"> //! Constant 1-bit bit-vector 0bin0</span></div>
<div class="line"><a name="l00046"></a><span class="lineno"><a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#ae3c2817336952a9c84ca8a44db3896e1"> 46</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#ae3c2817336952a9c84ca8a44db3896e1" title="Constant 1-bit bit-vector 0bin0.">d_bvZero</a>;<span class="comment"></span></div>
<div class="line"><a name="l00047"></a><span class="lineno"> 47</span> <span class="comment"> //! Constant 1-bit bit-vector 0bin1</span></div>
<div class="line"><a name="l00048"></a><span class="lineno"><a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#aed61523f51f9daff35bf4823e9c4c06e"> 48</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#aed61523f51f9daff35bf4823e9c4c06e" title="Constant 1-bit bit-vector 0bin1.">d_bvOne</a>;<span class="comment"></span></div>
<div class="line"><a name="l00049"></a><span class="lineno"> 49</span> <span class="comment"> //! Return cached constant 0bin0</span></div>
<div class="line"><a name="l00050"></a><span class="lineno"><a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#aaf9905051ca381e18683a41651404b69"> 50</a></span> <span class="comment"></span> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#aaf9905051ca381e18683a41651404b69" title="Return cached constant 0bin0.">bvZero</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#ae3c2817336952a9c84ca8a44db3896e1" title="Constant 1-bit bit-vector 0bin0.">d_bvZero</a>; }<span class="comment"></span></div>
<div class="line"><a name="l00051"></a><span class="lineno"> 51</span> <span class="comment"> //! Return cached constant 0bin1</span></div>
<div class="line"><a name="l00052"></a><span class="lineno"><a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a53f5be1f87db3613052a22fcf8a7e5d0"> 52</a></span> <span class="comment"></span> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a53f5be1f87db3613052a22fcf8a7e5d0" title="Return cached constant 0bin1.">bvOne</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#aed61523f51f9daff35bf4823e9c4c06e" title="Constant 1-bit bit-vector 0bin1.">d_bvOne</a>; }</div>
<div class="line"><a name="l00053"></a><span class="lineno"> 53</span> <span class="comment"></span></div>
<div class="line"><a name="l00054"></a><span class="lineno"> 54</span> <span class="comment"> //! Collect all of: a*x1+b*x1 + c*x2-x2 + d*x3 + ~x3 + ~x4 +e into</span></div>
<div class="line"><a name="l00055"></a><span class="lineno"> 55</span> <span class="comment"> //! (a+b, x1) , (c-1 , x2), (d-1, x3), (-1, x4) and the constant e-2.</span></div>
<div class="line"><a name="l00056"></a><span class="lineno"> 56</span> <span class="comment"> //! The constant is calculated from the formula -x = ~x+1 (or -x-1=~x).</span></div>
<div class="line"><a name="l00057"></a><span class="lineno"> 57</span> <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#ab46305e9bee9f911362cdb54a3037703">collectLikeTermsOfPlus</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e,</div>
<div class="line"><a name="l00058"></a><span class="lineno"> 58</span>  <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Rational></a> & likeTerms,</div>
<div class="line"><a name="l00059"></a><span class="lineno"> 59</span>  <a class="code" href="classCVC3_1_1Rational.html">Rational</a> & plusConstant);</div>
<div class="line"><a name="l00060"></a><span class="lineno"> 60</span> <span class="comment"></span></div>
<div class="line"><a name="l00061"></a><span class="lineno"> 61</span> <span class="comment"> //! Collect a single coefficient*var pair into likeTerms.</span></div>
<div class="line"><a name="l00062"></a><span class="lineno"> 62</span> <span class="comment"> //! Update the counter of likeTerms[var] += coefficient.</span></div>
<div class="line"><a name="l00063"></a><span class="lineno"> 63</span> <span class="comment"> //! Potentially update the constant additive plusConstant.</span></div>
<div class="line"><a name="l00064"></a><span class="lineno"> 64</span> <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a6596cca8e249d3ef6632429bd114a98a">collectOneTermOfPlus</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Rational.html">Rational</a> & coefficient,</div>
<div class="line"><a name="l00065"></a><span class="lineno"> 65</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& var,</div>
<div class="line"><a name="l00066"></a><span class="lineno"> 66</span>  <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Rational></a> & likeTerms,</div>
<div class="line"><a name="l00067"></a><span class="lineno"> 67</span>  <a class="code" href="classCVC3_1_1Rational.html">Rational</a> & plusConstant);</div>
<div class="line"><a name="l00068"></a><span class="lineno"> 68</span> <span class="comment"></span></div>
<div class="line"><a name="l00069"></a><span class="lineno"> 69</span> <span class="comment"> //! Create a vector which will form the next PVPLUS.</span></div>
<div class="line"><a name="l00070"></a><span class="lineno"> 70</span> <span class="comment"> //! Use the colleciton of likeTerms, and the constant additive plusConstant</span></div>
<div class="line"><a name="l00071"></a><span class="lineno"> 71</span> <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a0c47ccc89b98254df839ea35b1a0720d">createNewPlusCollection</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> & e,</div>
<div class="line"><a name="l00072"></a><span class="lineno"> 72</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Rational></a> & likeTerms,</div>
<div class="line"><a name="l00073"></a><span class="lineno"> 73</span>  <a class="code" href="classCVC3_1_1Rational.html">Rational</a> & plusConstant,</div>
<div class="line"><a name="l00074"></a><span class="lineno"> 74</span>  std::vector<Expr> & result);</div>
<div class="line"><a name="l00075"></a><span class="lineno"> 75</span> <span class="comment"></span></div>
<div class="line"><a name="l00076"></a><span class="lineno"> 76</span> <span class="comment"> //! Create expression by applying plus to all elements.</span></div>
<div class="line"><a name="l00077"></a><span class="lineno"> 77</span> <span class="comment"> //! All elements should be normalized and ready.</span></div>
<div class="line"><a name="l00078"></a><span class="lineno"> 78</span> <span class="comment"> //! If there are too few elements, a non BVPLUS expression will be created.</span></div>
<div class="line"><a name="l00079"></a><span class="lineno"> 79</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a24fff4a463643869b7a3b604884437b9">sumNormalizedElements</a>(<span class="keywordtype">int</span> bvplusLength,</div>
<div class="line"><a name="l00080"></a><span class="lineno"> 80</span>  <span class="keyword">const</span> std::vector<Expr>& elements);</div>
<div class="line"><a name="l00081"></a><span class="lineno"> 81</span> </div>
<div class="line"><a name="l00082"></a><span class="lineno"> 82</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a2a396fdaba828777b1c5277aee4fc69a">getPlusTerms</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <a class="code" href="classCVC3_1_1Rational.html">Rational</a>& known_term, <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Rational></a>& sumHashMap);</div>
<div class="line"><a name="l00083"></a><span class="lineno"> 83</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#af6d2296102e85962df7567ed2c09d0b6">buildPlusTerm</a>(<span class="keywordtype">int</span> bv_size, <a class="code" href="classCVC3_1_1Rational.html">Rational</a>& known_term, <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Rational></a>& sumHashMap);</div>
<div class="line"><a name="l00084"></a><span class="lineno"> 84</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#ab6cc1b10eb60cdf44eabb5a45013477f">chopConcat</a>(<span class="keywordtype">int</span> bv_size, <a class="code" href="classCVC3_1_1Rational.html">Rational</a> c, std::vector<Expr>& concatKids);</div>
<div class="line"><a name="l00085"></a><span class="lineno"> 85</span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#afd8d2a7f441db7d8a8cf41b83dcc9d0a">okToSplit</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00086"></a><span class="lineno"> 86</span> </div>
<div class="line"><a name="l00087"></a><span class="lineno"> 87</span>  <span class="keyword">public</span>:<span class="comment"></span></div>
<div class="line"><a name="l00088"></a><span class="lineno"> 88</span> <span class="comment"> //! Constructor: constructs an instance of bitvector DP</span></div>
<div class="line"><a name="l00089"></a><span class="lineno"> 89</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#ab0dec14e43b28a75df52cbef0f767a23" title="Constructor: constructs an instance of bitvector DP.">BitvectorTheoremProducer</a>(<a class="code" href="classCVC3_1_1TheoryBitvector.html" title="Theory of bitvectors of known length \ (operations include: @,[i:j],[i],+,.,BVAND,BVNEG)">TheoryBitvector</a>* theoryBitvector);</div>
<div class="line"><a name="l00090"></a><span class="lineno"><a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a8be04256f3b26c7932f2c0272ad3f6d1"> 90</a></span>  <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a8be04256f3b26c7932f2c0272ad3f6d1">~BitvectorTheoremProducer</a>() {}</div>
<div class="line"><a name="l00091"></a><span class="lineno"> 91</span> </div>
<div class="line"><a name="l00092"></a><span class="lineno"> 92</span>  <span class="comment">//ExprMap<Expr> d_bvPlusCarryCacheLeftBV;</span></div>
<div class="line"><a name="l00093"></a><span class="lineno"> 93</span>  <span class="comment">//ExprMap<Expr> d_bvPlusCarryCacheRightBV;</span></div>
<div class="line"><a name="l00094"></a><span class="lineno"> 94</span> <span class="comment"></span></div>
<div class="line"><a name="l00095"></a><span class="lineno"> 95</span> <span class="comment"> ////////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00096"></a><span class="lineno"> 96</span> <span class="comment"></span> <span class="comment">// Partial Canonization rules</span><span class="comment"></span></div>
<div class="line"><a name="l00097"></a><span class="lineno"> 97</span> <span class="comment"> ////////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00098"></a><span class="lineno"> 98</span> <span class="comment"></span><span class="comment"></span></div>
<div class="line"><a name="l00099"></a><span class="lineno"> 99</span> <span class="comment"> ////////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00100"></a><span class="lineno"> 100</span> <span class="comment"></span> <span class="comment">// Bitblasting rules for equations</span><span class="comment"></span></div>
<div class="line"><a name="l00101"></a><span class="lineno"> 101</span> <span class="comment"> ////////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00102"></a><span class="lineno"> 102</span> <span class="comment"></span><span class="comment"></span></div>
<div class="line"><a name="l00103"></a><span class="lineno"> 103</span> <span class="comment"> /*! \param thm input theorem: (e1[i]<=>e2[i])<=>false</span></div>
<div class="line"><a name="l00104"></a><span class="lineno"> 104</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00105"></a><span class="lineno"> 105</span> <span class="comment"> * \result (e1=e2)<=>false</span></div>
<div class="line"><a name="l00106"></a><span class="lineno"> 106</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00107"></a><span class="lineno"> 107</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a335f389e282bdb6529f86b2101b330e0">bitvectorFalseRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);</div>
<div class="line"><a name="l00108"></a><span class="lineno"> 108</span> <span class="comment"></span></div>
<div class="line"><a name="l00109"></a><span class="lineno"> 109</span> <span class="comment"> /*! \param thm input theorem: (~e1[i]<=>e2[i])<=>true</span></div>
<div class="line"><a name="l00110"></a><span class="lineno"> 110</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00111"></a><span class="lineno"> 111</span> <span class="comment"> * \result (e1!=e2)<=>true</span></div>
<div class="line"><a name="l00112"></a><span class="lineno"> 112</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00113"></a><span class="lineno"> 113</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#aafe3a19c755d3559e4c419be7c66d7c5">bitvectorTrueRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);</div>
<div class="line"><a name="l00114"></a><span class="lineno"> 114</span> <span class="comment"></span></div>
<div class="line"><a name="l00115"></a><span class="lineno"> 115</span> <span class="comment"> /*! \param e input equation: e1=e2 over bitvector terms</span></div>
<div class="line"><a name="l00116"></a><span class="lineno"> 116</span> <span class="comment"> * \param f formula over the bits of bitvector variables in e:</span></div>
<div class="line"><a name="l00117"></a><span class="lineno"> 117</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00118"></a><span class="lineno"> 118</span> <span class="comment"> * \result \f[\frac{e_1 = e_2}{\bigwedge_{i=1}^n (e_{1}[i]</span></div>
<div class="line"><a name="l00119"></a><span class="lineno"> 119</span> <span class="comment"> * \iff e_{2}[i]) } \f] where each of \f[ e_{1}[i], e{2}[i] \f] denotes a</span></div>
<div class="line"><a name="l00120"></a><span class="lineno"> 120</span> <span class="comment"> * formula over variables in \f[ e_{1}, e_{2} \f] respectively</span></div>
<div class="line"><a name="l00121"></a><span class="lineno"> 121</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00122"></a><span class="lineno"> 122</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#adc756096f301c80bb2bf73266c200aff">bitBlastEqnRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& f);</div>
<div class="line"><a name="l00123"></a><span class="lineno"> 123</span> <span class="comment"></span></div>
<div class="line"><a name="l00124"></a><span class="lineno"> 124</span> <span class="comment"> /*! \param e : input disequality: e1 != e2 over bitvector terms</span></div>
<div class="line"><a name="l00125"></a><span class="lineno"> 125</span> <span class="comment"> * \param f : formula over the bits of bitvector variables in e:</span></div>
<div class="line"><a name="l00126"></a><span class="lineno"> 126</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00127"></a><span class="lineno"> 127</span> <span class="comment"> * \result \f[\frac{e_1 \not = e_2}{\bigwedge_{i=1}^n ((\neg e_{1}[i])</span></div>
<div class="line"><a name="l00128"></a><span class="lineno"> 128</span> <span class="comment"> * \iff e_{2}[i]) } \f] where each of \f[ e_{1}[i], e{2}[i] \f] denotes a</span></div>
<div class="line"><a name="l00129"></a><span class="lineno"> 129</span> <span class="comment"> * formula over variables in \f[ e_{1}, e_{2} \f] respectively</span></div>
<div class="line"><a name="l00130"></a><span class="lineno"> 130</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00131"></a><span class="lineno"> 131</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a9839f27db5f349fe6fb6b21575cde24c">bitBlastDisEqnRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& f);</div>
<div class="line"><a name="l00132"></a><span class="lineno"> 132</span> </div>
<div class="line"><a name="l00133"></a><span class="lineno"> 133</span> <span class="comment"></span></div>
<div class="line"><a name="l00134"></a><span class="lineno"> 134</span> <span class="comment"> ////////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00135"></a><span class="lineno"> 135</span> <span class="comment"></span> <span class="comment">// Bitblasting and rewrite rules for Inequations</span><span class="comment"></span></div>
<div class="line"><a name="l00136"></a><span class="lineno"> 136</span> <span class="comment"> ////////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00137"></a><span class="lineno"> 137</span> <span class="comment"></span><span class="comment"></span></div>
<div class="line"><a name="l00138"></a><span class="lineno"> 138</span> <span class="comment"> //! sign extend the input SX(e) appropriately</span></div>
<div class="line"><a name="l00139"></a><span class="lineno"> 139</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#ae676208401e0d94c96d258f2dd652a68" title="sign extend the input SX(e) appropriately">signExtendRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00140"></a><span class="lineno"> 140</span> <span class="comment"></span></div>
<div class="line"><a name="l00141"></a><span class="lineno"> 141</span> <span class="comment"> //! Pad the kids of BVLT/BVLE to make their length equal</span></div>
<div class="line"><a name="l00142"></a><span class="lineno"> 142</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#ac83f1aeaf2b0dd78c5aec3d4dd605b21" title="Pad the kids of BVLT/BVLE to make their length equal.">padBVLTRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <span class="keywordtype">int</span> len);</div>
<div class="line"><a name="l00143"></a><span class="lineno"> 143</span> <span class="comment"></span></div>
<div class="line"><a name="l00144"></a><span class="lineno"> 144</span> <span class="comment"> //! Sign Extend the kids of BVSLT/BVSLE to make their length equal</span></div>
<div class="line"><a name="l00145"></a><span class="lineno"> 145</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#ab1f7b6923eb8053bbc567f7610458685" title="Sign Extend the kids of BVSLT/BVSLE to make their length equal.">padBVSLTRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <span class="keywordtype">int</span> len);</div>
<div class="line"><a name="l00146"></a><span class="lineno"> 146</span> <span class="comment"></span></div>
<div class="line"><a name="l00147"></a><span class="lineno"> 147</span> <span class="comment"> /*! input: e0 <=(s) e1. output depends on whether the topbits(MSB) of</span></div>
<div class="line"><a name="l00148"></a><span class="lineno"> 148</span> <span class="comment"> * e0 and e1 are constants. If they are constants then optimizations</span></div>
<div class="line"><a name="l00149"></a><span class="lineno"> 149</span> <span class="comment"> * are done, otherwise the following rule is implemented.</span></div>
<div class="line"><a name="l00150"></a><span class="lineno"> 150</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00151"></a><span class="lineno"> 151</span> <span class="comment"> * e0 <=(s) e1 <==> (e0[n-1] AND NOT e1[n-1]) OR</span></div>
<div class="line"><a name="l00152"></a><span class="lineno"> 152</span> <span class="comment"> * (e0[n-1] AND e1[n-1] AND e1[n-2:0] <= e0[n-2:0]) OR</span></div>
<div class="line"><a name="l00153"></a><span class="lineno"> 153</span> <span class="comment"> * (NOT e0[n-1] AND NOT e1[n-1] AND e0[n-2:0] <= e1[n-2:0])</span></div>
<div class="line"><a name="l00154"></a><span class="lineno"> 154</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00155"></a><span class="lineno"> 155</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a1798c9272bc8f7f78100a4fb839fb907">signBVLTRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e,</div>
<div class="line"><a name="l00156"></a><span class="lineno"> 156</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& topBit0,</div>
<div class="line"><a name="l00157"></a><span class="lineno"> 157</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& topBit1);</div>
<div class="line"><a name="l00158"></a><span class="lineno"> 158</span> <span class="comment"></span></div>
<div class="line"><a name="l00159"></a><span class="lineno"> 159</span> <span class="comment"> /*! NOT(e[0][0] = e[0][1]) <==> e[0][0] = ~e[0][1]</span></div>
<div class="line"><a name="l00160"></a><span class="lineno"> 160</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00161"></a><span class="lineno"> 161</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#aff7d8a5558884d2b24e83dc55dc0a59e">notBVEQ1Rule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00162"></a><span class="lineno"> 162</span> <span class="comment"></span></div>
<div class="line"><a name="l00163"></a><span class="lineno"> 163</span> <span class="comment"> /*! NOT(e[0][0] < e[0][1]) <==> (e[0][1] <= e[0][0]),</span></div>
<div class="line"><a name="l00164"></a><span class="lineno"> 164</span> <span class="comment"> * NOT(e[0][0] <= e[0][1]) <==> (e[0][1] < e[0][0])</span></div>
<div class="line"><a name="l00165"></a><span class="lineno"> 165</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00166"></a><span class="lineno"> 166</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a15d14a25e4805c5aceff3521f7dbebd0">notBVLTRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00167"></a><span class="lineno"> 167</span> <span class="comment"></span></div>
<div class="line"><a name="l00168"></a><span class="lineno"> 168</span> <span class="comment"> //! if(lhs==rhs) then we have (lhs < rhs <==> false),(lhs <= rhs <==> true)</span></div>
<div class="line"><a name="l00169"></a><span class="lineno"> 169</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#aa9b8579a600e0c95fbc51a599b03a182" title="if(lhs==rhs) then we have (lhs < rhs <==> false),(lhs <= rhs <==> true)">lhsEqRhsIneqn</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <span class="keywordtype">int</span> kind);</div>
<div class="line"><a name="l00170"></a><span class="lineno"> 170</span> </div>
<div class="line"><a name="l00171"></a><span class="lineno"> 171</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#ac141b7dc72e52b9b18fd2258db17a952" title="|= 0 <= foo <-> TRUE">zeroLeq</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00172"></a><span class="lineno"> 172</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a00a6af751fe6354bfd282f5a8f25456a" title="if indeed e[0] < e[1] then (e<==>true) else (e<==>false)">bvConstIneqn</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <span class="keywordtype">int</span> kind);</div>
<div class="line"><a name="l00173"></a><span class="lineno"> 173</span> </div>
<div class="line"><a name="l00174"></a><span class="lineno"> 174</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a9e41265f17a1d607e9559bb718963f0a">generalIneqn</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e,</div>
<div class="line"><a name="l00175"></a><span class="lineno"> 175</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& lhs_i,</div>
<div class="line"><a name="l00176"></a><span class="lineno"> 176</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& rhs_i, <span class="keywordtype">int</span> kind);</div>
<div class="line"><a name="l00177"></a><span class="lineno"> 177</span> <span class="comment"></span></div>
<div class="line"><a name="l00178"></a><span class="lineno"> 178</span> <span class="comment"> ////////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00179"></a><span class="lineno"> 179</span> <span class="comment"></span> <span class="comment">// Bitblasting rules for terms</span><span class="comment"></span></div>
<div class="line"><a name="l00180"></a><span class="lineno"> 180</span> <span class="comment"> ////////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00181"></a><span class="lineno"> 181</span> <span class="comment"></span></div>
<div class="line"><a name="l00182"></a><span class="lineno"> 182</span>  <span class="comment">// Input: |- BOOLEXTRACT(a,0) <=> bc_0, ... BOOLEXTRACT(a,n-1) <=> bc_(n-1)</span></div>
<div class="line"><a name="l00183"></a><span class="lineno"> 183</span>  <span class="comment">// where each bc_0 is TRUE or FALSE</span></div>
<div class="line"><a name="l00184"></a><span class="lineno"> 184</span>  <span class="comment">// Output: |- a = c</span></div>
<div class="line"><a name="l00185"></a><span class="lineno"> 185</span>  <span class="comment">// where c is an n-bit constant made from the values bc_0..bc_(n-1)</span></div>
<div class="line"><a name="l00186"></a><span class="lineno"> 186</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a70fb1053bd8518120c0d69dca9069062">bitExtractAllToConstEq</a>(std::vector<Theorem>& thms);<span class="comment"></span></div>
<div class="line"><a name="l00187"></a><span class="lineno"> 187</span> <span class="comment"> //! t[i] ==> t[i:i] = 0bin1 or NOT t[i] ==> t[i:i] = 0bin0</span></div>
<div class="line"><a name="l00188"></a><span class="lineno"> 188</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#ae7cdd320c7fb8e16f943626d07d9f63b" title="t[i] ==> t[i:i] = 0bin1 or NOT t[i] ==> t[i:i] = 0bin0">bitExtractToExtract</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);<span class="comment"></span></div>
<div class="line"><a name="l00189"></a><span class="lineno"> 189</span> <span class="comment"> //! t[i] <=> t[i:i][0] (to use rewriter for simplifying t[i:i])</span></div>
<div class="line"><a name="l00190"></a><span class="lineno"> 190</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a8dab3dc6ffdf47a18f6097ad0185b4de" title="t[i] <=> t[i:i][0] (to use rewriter for simplifying t[i:i])">bitExtractRewrite</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& x);</div>
<div class="line"><a name="l00191"></a><span class="lineno"> 191</span> <span class="comment"></span></div>
<div class="line"><a name="l00192"></a><span class="lineno"> 192</span> <span class="comment"> /*! \param x : input1 is bitvector constant</span></div>
<div class="line"><a name="l00193"></a><span class="lineno"> 193</span> <span class="comment"> * \param i : input2 is extracted bitposition</span></div>
<div class="line"><a name="l00194"></a><span class="lineno"> 194</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00195"></a><span class="lineno"> 195</span> <span class="comment"> * \result \f[ \frac{}{\mathrm{BOOLEXTRACT(x,i)} \iff</span></div>
<div class="line"><a name="l00196"></a><span class="lineno"> 196</span> <span class="comment"> * \mathrm{TRUE}} \f], if bitposition has a 1; \f[</span></div>
<div class="line"><a name="l00197"></a><span class="lineno"> 197</span> <span class="comment"> * \frac{}{\mathrm{BOOLEXTRACT(x,i)} \iff \mathrm{FALSE}} \f], if</span></div>
<div class="line"><a name="l00198"></a><span class="lineno"> 198</span> <span class="comment"> * the bitposition has a 0</span></div>
<div class="line"><a name="l00199"></a><span class="lineno"> 199</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00200"></a><span class="lineno"> 200</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#ad14158d7d8b6a1ccf2b6c47991d498d7">bitExtractConstant</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> & x, <span class="keywordtype">int</span> i);</div>
<div class="line"><a name="l00201"></a><span class="lineno"> 201</span> <span class="comment"></span></div>
<div class="line"><a name="l00202"></a><span class="lineno"> 202</span> <span class="comment"> /*! \param x : input1 is bitvector binary concatenation</span></div>
<div class="line"><a name="l00203"></a><span class="lineno"> 203</span> <span class="comment"> * \param i : input2 is extracted bitposition</span></div>
<div class="line"><a name="l00204"></a><span class="lineno"> 204</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00205"></a><span class="lineno"> 205</span> <span class="comment"> * \result \f[ \frac{}{(t_{[m]}@q_{[n]})[i] \iff (q_{[n]})[i]}</span></div>
<div class="line"><a name="l00206"></a><span class="lineno"> 206</span> <span class="comment"> * \f], where \f[ 0 \geq i \geq n-1 \f], another case of</span></div>
<div class="line"><a name="l00207"></a><span class="lineno"> 207</span> <span class="comment"> * boolextract over concatenation is:</span></div>
<div class="line"><a name="l00208"></a><span class="lineno"> 208</span> <span class="comment"> * \f[\frac{}{(t_{[m]}@q_{[n]})[i] \iff (t_{[m]})[i-n]} \f],</span></div>
<div class="line"><a name="l00209"></a><span class="lineno"> 209</span> <span class="comment"> * where \f[ n \geq i \geq m+n-1 \f]</span></div>
<div class="line"><a name="l00210"></a><span class="lineno"> 210</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00211"></a><span class="lineno"> 211</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a571db5dc21ec0b24e1d861c137892f9c">bitExtractConcatenation</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> & x, <span class="keywordtype">int</span> i);</div>
<div class="line"><a name="l00212"></a><span class="lineno"> 212</span> <span class="comment"></span></div>
<div class="line"><a name="l00213"></a><span class="lineno"> 213</span> <span class="comment"> /*! \param t : input1 is bitvector binary BVMULT. x[0] must be BVCONST</span></div>
<div class="line"><a name="l00214"></a><span class="lineno"> 214</span> <span class="comment"> * \param i : input2 is extracted bitposition</span></div>
<div class="line"><a name="l00215"></a><span class="lineno"> 215</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00216"></a><span class="lineno"> 216</span> <span class="comment"> * \result bitblast of BVMULT</span></div>
<div class="line"><a name="l00217"></a><span class="lineno"> 217</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00218"></a><span class="lineno"> 218</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#abf6f1ff706f6cefe196b1cbe7d5f85c1">bitExtractConstBVMult</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t, <span class="keywordtype">int</span> i);</div>
<div class="line"><a name="l00219"></a><span class="lineno"> 219</span> <span class="comment"></span></div>
<div class="line"><a name="l00220"></a><span class="lineno"> 220</span> <span class="comment"> /*! \param t : input1 is bitvector binary BVMULT. t[0] must not be BVCONST</span></div>
<div class="line"><a name="l00221"></a><span class="lineno"> 221</span> <span class="comment"> * \param i : input2 is extracted bitposition</span></div>
<div class="line"><a name="l00222"></a><span class="lineno"> 222</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00223"></a><span class="lineno"> 223</span> <span class="comment"> * \result bitblast of BVMULT</span></div>
<div class="line"><a name="l00224"></a><span class="lineno"> 224</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00225"></a><span class="lineno"> 225</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a0425488c3b01eb65554867483e3cac02">bitExtractBVMult</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t, <span class="keywordtype">int</span> i);</div>
<div class="line"><a name="l00226"></a><span class="lineno"> 226</span> <span class="comment"></span></div>
<div class="line"><a name="l00227"></a><span class="lineno"> 227</span> <span class="comment"> /*! \param x : input1 is bitvector extraction [k:j]</span></div>
<div class="line"><a name="l00228"></a><span class="lineno"> 228</span> <span class="comment"> * \param i : input2 is extracted bitposition</span></div>
<div class="line"><a name="l00229"></a><span class="lineno"> 229</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00230"></a><span class="lineno"> 230</span> <span class="comment"> * \result \f[ \frac{}{(t_{[n]}[k:j])[i] \iff (t_{[n]})[i+j]}</span></div>
<div class="line"><a name="l00231"></a><span class="lineno"> 231</span> <span class="comment"> * \f], where \f[ 0 \geq j \geq k < n, 0 \geq i < k-j \f]</span></div>
<div class="line"><a name="l00232"></a><span class="lineno"> 232</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00233"></a><span class="lineno"> 233</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a8efcf949614eab1089f00519f1db57bb">bitExtractExtraction</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> & x, <span class="keywordtype">int</span> i);</div>
<div class="line"><a name="l00234"></a><span class="lineno"> 234</span> <span class="comment"></span></div>
<div class="line"><a name="l00235"></a><span class="lineno"> 235</span> <span class="comment"> /*! \param t1 : input1 is vector of bitblasts of t, from bit i-1 to 0</span></div>
<div class="line"><a name="l00236"></a><span class="lineno"> 236</span> <span class="comment"> * \param t2 : input2 is vector of bitblasts of q, from bit i-1 to 0</span></div>
<div class="line"><a name="l00237"></a><span class="lineno"> 237</span> <span class="comment"> * \param bvPlusTerm : input3 is BVPLUS term: BVPLUS(n,t,q)</span></div>
<div class="line"><a name="l00238"></a><span class="lineno"> 238</span> <span class="comment"> * \param i : input4 is extracted bitposition</span></div>
<div class="line"><a name="l00239"></a><span class="lineno"> 239</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00240"></a><span class="lineno"> 240</span> <span class="comment"> * \result The base case is: \f[</span></div>
<div class="line"><a name="l00241"></a><span class="lineno"> 241</span> <span class="comment"> * \frac{}{(\mathrm{BVPLUS}(n,t,q))[0] \iff t[0] \oplus q[0]}</span></div>
<div class="line"><a name="l00242"></a><span class="lineno"> 242</span> <span class="comment"> * \f], when \f[ 0 < i \leq n-1 \f], we have \f[</span></div>
<div class="line"><a name="l00243"></a><span class="lineno"> 243</span> <span class="comment"> * \frac{}{(\mathrm{BVPLUS}(n,t,q))[i] \iff t[i] \oplus q[i]</span></div>
<div class="line"><a name="l00244"></a><span class="lineno"> 244</span> <span class="comment"> * \oplus c(t,q,i)} \f], where c(t,q,i) is the carry generated</span></div>
<div class="line"><a name="l00245"></a><span class="lineno"> 245</span> <span class="comment"> * by the addition of bits from 0 to i-1</span></div>
<div class="line"><a name="l00246"></a><span class="lineno"> 246</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00247"></a><span class="lineno"> 247</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a6c02b66248026d3ffb357e980de37ed7">bitExtractBVPlus</a>(<span class="keyword">const</span> std::vector<Theorem>& t1,</div>
<div class="line"><a name="l00248"></a><span class="lineno"> 248</span>  <span class="keyword">const</span> std::vector<Theorem>& t2,</div>
<div class="line"><a name="l00249"></a><span class="lineno"> 249</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& bvPlusTerm, <span class="keywordtype">int</span> i);</div>
<div class="line"><a name="l00250"></a><span class="lineno"> 250</span> </div>
<div class="line"><a name="l00251"></a><span class="lineno"> 251</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#aaf4999f69872e881257cd1e127732ec8">bitExtractBVPlusPreComputed</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t1_i,</div>
<div class="line"><a name="l00252"></a><span class="lineno"> 252</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t2_i,</div>
<div class="line"><a name="l00253"></a><span class="lineno"> 253</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& bvPlusTerm,</div>
<div class="line"><a name="l00254"></a><span class="lineno"> 254</span>  <span class="keywordtype">int</span> bitPos,</div>
<div class="line"><a name="l00255"></a><span class="lineno"> 255</span>  <span class="keywordtype">int</span> precomputed);</div>
<div class="line"><a name="l00256"></a><span class="lineno"> 256</span> <span class="comment"></span></div>
<div class="line"><a name="l00257"></a><span class="lineno"> 257</span> <span class="comment"> /*! \param bvPlusTerm : input1 is bvPlusTerm, a BVPLUS term with</span></div>
<div class="line"><a name="l00258"></a><span class="lineno"> 258</span> <span class="comment"> * arity > 2</span></div>
<div class="line"><a name="l00259"></a><span class="lineno"> 259</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00260"></a><span class="lineno"> 260</span> <span class="comment"> * \result : output is iff-Theorem: bvPlusTerm <==> outputTerm,</span></div>
<div class="line"><a name="l00261"></a><span class="lineno"> 261</span> <span class="comment"> * where outputTerm is an equivalent BINARY bvplus.</span></div>
<div class="line"><a name="l00262"></a><span class="lineno"> 262</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00263"></a><span class="lineno"> 263</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a415c16ecc3bbdd0942801028526d641f">bvPlusAssociativityRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& bvPlusTerm);</div>
<div class="line"><a name="l00264"></a><span class="lineno"> 264</span> <span class="comment"></span></div>
<div class="line"><a name="l00265"></a><span class="lineno"> 265</span> <span class="comment"> /*! \param x : input1 is bitwise NEGATION</span></div>
<div class="line"><a name="l00266"></a><span class="lineno"> 266</span> <span class="comment"> * \param i : input2 is extracted bitposition</span></div>
<div class="line"><a name="l00267"></a><span class="lineno"> 267</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00268"></a><span class="lineno"> 268</span> <span class="comment"> * \result \f[ \frac{}{(\sim t_{[n]})[i] \iff \neg (t_{[n]}[i])}</span></div>
<div class="line"><a name="l00269"></a><span class="lineno"> 269</span> <span class="comment"> * \f]</span></div>
<div class="line"><a name="l00270"></a><span class="lineno"> 270</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00271"></a><span class="lineno"> 271</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a43201ddd283a81a44095658241ca2a5e">bitExtractNot</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> & x, <span class="keywordtype">int</span> i);</div>
<div class="line"><a name="l00272"></a><span class="lineno"> 272</span> <span class="comment"></span></div>
<div class="line"><a name="l00273"></a><span class="lineno"> 273</span> <span class="comment"> //! Extract from bitwise AND, OR, or XOR</span></div>
<div class="line"><a name="l00274"></a><span class="lineno"> 274</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#acd7ddad997b468fbb64373913e03b5e9" title="Extract from bitwise AND, OR, or XOR.">bitExtractBitwise</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& x, <span class="keywordtype">int</span> i, <span class="keywordtype">int</span> kind);</div>
<div class="line"><a name="l00275"></a><span class="lineno"> 275</span> <span class="comment"></span></div>
<div class="line"><a name="l00276"></a><span class="lineno"> 276</span> <span class="comment"> /*! \param x : input1 is bitvector FIXED SHIFT \f[ e_{[n]} \ll k \f]</span></div>
<div class="line"><a name="l00277"></a><span class="lineno"> 277</span> <span class="comment"> * \param i : input2 is extracted bitposition</span></div>
<div class="line"><a name="l00278"></a><span class="lineno"> 278</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00279"></a><span class="lineno"> 279</span> <span class="comment"> * \result \f[\frac{}{(e_{[n]} \ll k)[i] \iff \mathrm{FALSE}}</span></div>
<div class="line"><a name="l00280"></a><span class="lineno"> 280</span> <span class="comment"> * \f], if 0 <= i < k. however, if k <= i < n then, result is</span></div>
<div class="line"><a name="l00281"></a><span class="lineno"> 281</span> <span class="comment"> * \f[\frac{}{(e_{[n]} \ll k)[i] \iff e_{[n]}[i]} \f]</span></div>
<div class="line"><a name="l00282"></a><span class="lineno"> 282</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00283"></a><span class="lineno"> 283</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a4153b23dadd58aea7bde7f71001aad91">bitExtractFixedLeftShift</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> & x, <span class="keywordtype">int</span> i);</div>
<div class="line"><a name="l00284"></a><span class="lineno"> 284</span> </div>
<div class="line"><a name="l00285"></a><span class="lineno"> 285</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a2db4c3bb12bae8276f7c542936989d83">bitExtractFixedRightShift</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> & x, <span class="keywordtype">int</span> i);</div>
<div class="line"><a name="l00286"></a><span class="lineno"> 286</span> </div>
<div class="line"><a name="l00287"></a><span class="lineno"> 287</span>  <span class="comment">// BOOLEXTRACT(bvshl(t,s),i) <=> ((s = 0) AND BOOLEXTRACT(t,i)) OR</span></div>
<div class="line"><a name="l00288"></a><span class="lineno"> 288</span>  <span class="comment">// ((s = 1) AND BOOLEXTRACT(t,i-1)) OR ...</span></div>
<div class="line"><a name="l00289"></a><span class="lineno"> 289</span>  <span class="comment">// ((s = i) AND BOOLEXTRACT(t,0))</span></div>
<div class="line"><a name="l00290"></a><span class="lineno"> 290</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a2b273a0a3bb7a39646f0fb065e954ccc">bitExtractBVSHL</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> & x, <span class="keywordtype">int</span> i);</div>
<div class="line"><a name="l00291"></a><span class="lineno"> 291</span> </div>
<div class="line"><a name="l00292"></a><span class="lineno"> 292</span>  <span class="comment">// BOOLEXTRACT(bvlshr(t,s),i) <=> ((s = 0) AND BOOLEXTRACT(t,i)) OR</span></div>
<div class="line"><a name="l00293"></a><span class="lineno"> 293</span>  <span class="comment">// ((s = 1) AND BOOLEXTRACT(t,i+1)) OR ...</span></div>
<div class="line"><a name="l00294"></a><span class="lineno"> 294</span>  <span class="comment">// ((s = n-1-i) AND BOOLEXTRACT(t,n-1))</span></div>
<div class="line"><a name="l00295"></a><span class="lineno"> 295</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#afc17991261fb1f240861496d391c452a">bitExtractBVLSHR</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> & x, <span class="keywordtype">int</span> i);</div>
<div class="line"><a name="l00296"></a><span class="lineno"> 296</span> </div>
<div class="line"><a name="l00297"></a><span class="lineno"> 297</span>  <span class="comment">// BOOLEXTRACT(bvashr(t,s),i) <=> ((s = 0) AND BOOLEXTRACT(t,i)) OR</span></div>
<div class="line"><a name="l00298"></a><span class="lineno"> 298</span>  <span class="comment">// ((s = 1) AND BOOLEXTRACT(t,i+1)) OR ...</span></div>
<div class="line"><a name="l00299"></a><span class="lineno"> 299</span>  <span class="comment">// ((s >= n-1-i) AND BOOLEXTRACT(t,n-1))</span></div>
<div class="line"><a name="l00300"></a><span class="lineno"> 300</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#ad9256452fce83e6505d94f2a11b2a463">bitExtractBVASHR</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> & x, <span class="keywordtype">int</span> i);</div>
<div class="line"><a name="l00301"></a><span class="lineno"> 301</span> <span class="comment"></span></div>
<div class="line"><a name="l00302"></a><span class="lineno"> 302</span> <span class="comment"> /*! \param e : input1 is bitvector term</span></div>
<div class="line"><a name="l00303"></a><span class="lineno"> 303</span> <span class="comment"> * \param r : input2 is extracted bitposition</span></div>
<div class="line"><a name="l00304"></a><span class="lineno"> 304</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00305"></a><span class="lineno"> 305</span> <span class="comment"> * \result we check if r > bvlength(e). if yes, then return</span></div>
<div class="line"><a name="l00306"></a><span class="lineno"> 306</span> <span class="comment"> * BOOLEXTRACT(e,r) <==> FALSE; else raise soundness</span></div>
<div class="line"><a name="l00307"></a><span class="lineno"> 307</span> <span class="comment"> * exception. (Note: this rule is used in BVPLUS bitblast</span></div>
<div class="line"><a name="l00308"></a><span class="lineno"> 308</span> <span class="comment"> * function)</span></div>
<div class="line"><a name="l00309"></a><span class="lineno"> 309</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00310"></a><span class="lineno"> 310</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a6c59521b4540e2acd1fe954272bf3e09">zeroPaddingRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <span class="keywordtype">int</span> r);</div>
<div class="line"><a name="l00311"></a><span class="lineno"> 311</span> </div>
<div class="line"><a name="l00312"></a><span class="lineno"> 312</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a1d749524ddb67fa00fc4da46df1156c9" title="bitExtractSXRule">bitExtractSXRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <span class="keywordtype">int</span> i);</div>
<div class="line"><a name="l00313"></a><span class="lineno"> 313</span> <span class="comment"></span></div>
<div class="line"><a name="l00314"></a><span class="lineno"> 314</span> <span class="comment"> //! c1=c2 <=> TRUE/FALSE (equality of constant bitvectors)</span></div>
<div class="line"><a name="l00315"></a><span class="lineno"> 315</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#aaa38beb3d8990340aa5867f09900f14e" title="c1=c2 <=> TRUE/FALSE (equality of constant bitvectors)">eqConst</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00316"></a><span class="lineno"> 316</span> <span class="comment"> //! |- c1=c2 ==> |- AND(c1[i:i] = c2[i:i]) - expanding equalities into bits</span></div>
<div class="line"><a name="l00317"></a><span class="lineno"> 317</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a58ce4c07a8d005fa6d9820abc5fac028" title="|- c1=c2 ==> |- AND(c1[i:i] = c2[i:i]) - expanding equalities into bits">eqToBits</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& eq);<span class="comment"></span></div>
<div class="line"><a name="l00318"></a><span class="lineno"> 318</span> <span class="comment"> //! t<<n = c @ 0bin00...00, takes e == (t<<n)</span></div>
<div class="line"><a name="l00319"></a><span class="lineno"> 319</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a68fd84ca46b0e62103314c45dee495bd" title="t<<n = c @ 0bin00...00, takes e == (t<<n)">leftShiftToConcat</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00320"></a><span class="lineno"> 320</span> <span class="comment"> //! t<<n = c @ 0bin00...00, takes e == (t<<n)</span></div>
<div class="line"><a name="l00321"></a><span class="lineno"> 321</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#aabb5f8d91314adc4688e5970b986edf0" title="t<<n = c @ 0bin00...00, takes e == (t<<n)">constWidthLeftShiftToConcat</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00322"></a><span class="lineno"> 322</span> <span class="comment"> //! t>>m = 0bin00...00 @ t[bvlength-1:m], takes e == (t>>n)</span></div>
<div class="line"><a name="l00323"></a><span class="lineno"> 323</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a7d91d285e929d00572f3da4da772f505" title="t>>m = 0bin00...00 @ t[bvlength-1:m], takes e == (t>>n)">rightShiftToConcat</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00324"></a><span class="lineno"> 324</span> <span class="comment"> //! BVSHL(t,c) = t[n-c,0] @ 0bin00...00</span></div>
<div class="line"><a name="l00325"></a><span class="lineno"> 325</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#ae47b2ec2a40c3376071ed60c16d457b6" title="BVSHL(t,c) = t[n-c,0] @ 0bin00...00.">bvshlToConcat</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00326"></a><span class="lineno"> 326</span> <span class="comment"> //! BVSHL(t,c) = IF (c = 0) THEN t ELSE IF (c = 1) ...</span></div>
<div class="line"><a name="l00327"></a><span class="lineno"> 327</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a431507c9e35ad328509072cea05f2d8e" title="BVSHL(t,c) = IF (c = 0) THEN t ELSE IF (c = 1) ...">bvshlSplit</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00328"></a><span class="lineno"> 328</span> <span class="comment"> //! BVLSHR(t,c) = 0bin00...00 @ t[n-1,c]</span></div>
<div class="line"><a name="l00329"></a><span class="lineno"> 329</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a5f99ee62c0847affeb44264840764b43" title="BVLSHR(t,c) = 0bin00...00 @ t[n-1,c].">bvlshrToConcat</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00330"></a><span class="lineno"> 330</span> <span class="comment"> //! All shifts over a 0 constant = 0</span></div>
<div class="line"><a name="l00331"></a><span class="lineno"> 331</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a61b2ded76e35d870b15502ab0641010d" title="All shifts over a 0 constant = 0.">bvShiftZero</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00332"></a><span class="lineno"> 332</span> <span class="comment"> //! BVASHR(t,c) = SX(t[n-1,c], n-1)</span></div>
<div class="line"><a name="l00333"></a><span class="lineno"> 333</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a3c3a4d49d47a08a3eb7599327f30f324" title="BVASHR(t,c) = SX(t[n-1,c], n-1)">bvashrToConcat</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00334"></a><span class="lineno"> 334</span> <span class="comment"> //! a XNOR b <=> (~a & ~b) | (a & b)</span></div>
<div class="line"><a name="l00335"></a><span class="lineno"> 335</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a70ad43279f8061f7be4e35c49205ab69" title="a XNOR b <=> (~a & ~b) | (a & b)">rewriteXNOR</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00336"></a><span class="lineno"> 336</span> <span class="comment"> //! a NAND b <=> ~(a & b)</span></div>
<div class="line"><a name="l00337"></a><span class="lineno"> 337</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a2d49a06be7aae5f5675977fdc1b6457e" title="a NAND b <=> ~(a & b)">rewriteNAND</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00338"></a><span class="lineno"> 338</span> <span class="comment"> //! a NOR b <=> ~(a | b)</span></div>
<div class="line"><a name="l00339"></a><span class="lineno"> 339</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a372c699b42bb9ab8b64e2a836bedcffd" title="a NOR b <=> ~(a | b)">rewriteNOR</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00340"></a><span class="lineno"> 340</span> <span class="comment"> //! BVCOMP(a,b) <=> ITE(a=b,0bin1,0bin0)</span></div>
<div class="line"><a name="l00341"></a><span class="lineno"> 341</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#ab314017086d977ee1f4facb23208864c" title="BVCOMP(a,b) <=> ITE(a=b,0bin1,0bin0)">rewriteBVCOMP</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00342"></a><span class="lineno"> 342</span> <span class="comment"> //! a - b <=> a + (-b)</span></div>
<div class="line"><a name="l00343"></a><span class="lineno"> 343</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a1a040de059cc4fedf5cdd00cec37fc9c" title="a - b <=> a + (-b)">rewriteBVSub</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00344"></a><span class="lineno"> 344</span> <span class="comment"> //! k*t = BVPLUS(n, <sum of shifts of t>) -- translation of k*t to BVPLUS</span></div>
<div class="line"><a name="l00345"></a><span class="lineno"> 345</span> <span class="comment"></span><span class="comment"> /*! If k = 2^m, return k*t = t\@0...0 */</span></div>
<div class="line"><a name="l00346"></a><span class="lineno"> 346</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a560ad9ec684e523f941c2d12fa833cd1" title="k*t = BVPLUS(n, <sum of shifts of t>) – translation of k*t to BVPLUS">constMultToPlus</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00347"></a><span class="lineno"> 347</span> <span class="comment"> //! 0bin0...0 @ BVPLUS(n, args) = BVPLUS(n+k, args)</span></div>
<div class="line"><a name="l00348"></a><span class="lineno"> 348</span> <span class="comment"></span><span class="comment"> /*! where k is the size of the 0bin0...0 */</span></div>
<div class="line"><a name="l00349"></a><span class="lineno"> 349</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#af734405e15de47e28f4112e07bfc9dba" title="0bin0...0 @ BVPLUS(n, args) = BVPLUS(n+k, args)">bvplusZeroConcatRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00350"></a><span class="lineno"> 350</span> </div>
<div class="line"><a name="l00351"></a><span class="lineno"> 351</span> <span class="comment"></span></div>
<div class="line"><a name="l00352"></a><span class="lineno"> 352</span> <span class="comment"> ///////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00353"></a><span class="lineno"> 353</span> <span class="comment"> ///// Bvplus Normal Form rules</span></div>
<div class="line"><a name="l00354"></a><span class="lineno"> 354</span> <span class="comment"> ///////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00355"></a><span class="lineno"> 355</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a6d773885e3e78a736cd22dd79835b9e3">zeroCoeffBVMult</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00356"></a><span class="lineno"> 356</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a916fcffc7cb40f2159b00a710c26f669">oneCoeffBVMult</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00357"></a><span class="lineno"> 357</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a9ed93437abb38597bbf7d153184c70e5" title="t1*a <==> a*t1">flipBVMult</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00358"></a><span class="lineno"> 358</span> <span class="comment"> //! converts e to a bitvector of length rat</span></div>
<div class="line"><a name="l00359"></a><span class="lineno"> 359</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a99694606f15f144080a21f142b8a098f" title="converts e to a bitvector of length rat">pad</a>(<span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#ae03f092d2050783885e338b5880b2645">rat</a>, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00360"></a><span class="lineno"> 360</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#aa3d3d7bff1a088fa66a19076c471571a" title="Pad the kids of BVMULT to make their bvLength = # of output-bits.">padBVPlus</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00361"></a><span class="lineno"> 361</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#ac8509af4659a1391e983939d825f0e85" title="Pad the kids of BVMULT to make their bvLength = # of output-bits.">padBVMult</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00362"></a><span class="lineno"> 362</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a67921f96646d6b01d62d8a1cd116ddb3" title="a*(b*t) <==> (a*b)*t, where a,b,t have same bvLength">bvConstMultAssocRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00363"></a><span class="lineno"> 363</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#afa7daebdee6dafd361980583b6d3ffe1" title="(t1*t2)*t3 <==> t1*(t2*t3), where t1<t2<t3">bvMultAssocRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00364"></a><span class="lineno"> 364</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a44e37a65f45da9fb8469a0003a140836" title="a*(t1+...+tn) <==> (a*t1+...+a*tn), where all kids are equibvLength">bvMultDistRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00365"></a><span class="lineno"> 365</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a2a66e5fbe24e038a79ac07290900fdd4" title="input BVPLUS expression e.output e <==> e', where e' has no BVPLUS">flattenBVPlus</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00366"></a><span class="lineno"> 366</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a2a6308a817bfe26b843612fd02ba5441">combineLikeTermsRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00367"></a><span class="lineno"> 367</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a85f807faae622c7c6cb9d85cad0c5fc3">lhsMinusRhsRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00368"></a><span class="lineno"> 368</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a5df17d5d90f8a7389808a870a90ae863" title="(x *[n] y)[m:k] = (x *[m+1] y)[m:k], where m < n">extractBVMult</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00369"></a><span class="lineno"> 369</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#aabeacfb4b8a65744ac53f2cfe5dadc74" title="(x +[n] y)[m:k] = (x +[m+1] y)[m:k], where m < n">extractBVPlus</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00370"></a><span class="lineno"> 370</span> <span class="comment"> //! ite(c,t1,t2)[i:j] <=> ite(c,t1[i:j],t2[i:j])</span></div>
<div class="line"><a name="l00371"></a><span class="lineno"> 371</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a35d8c914e411c866485e17febed62c00" title="ite(c,t1,t2)[i:j] <=> ite(c,t1[i:j],t2[i:j])">iteExtractRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00372"></a><span class="lineno"> 372</span> <span class="comment"> //! ~ite(c,t1,t2) <=> ite(c,~t1,~t2)</span></div>
<div class="line"><a name="l00373"></a><span class="lineno"> 373</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a5bd890187bf9297b3b1092c623c1d922" title="~ite(c,t1,t2) <=> ite(c,~t1,~t2)">iteBVnegRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00374"></a><span class="lineno"> 374</span> </div>
<div class="line"><a name="l00375"></a><span class="lineno"> 375</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#ac0f04eeb2cf6b89dbbcf8849bea4e40b" title="-0 <==> 0, -c <==> ~c+1">bvuminusBVConst</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00376"></a><span class="lineno"> 376</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a84fcae86e983ecd86c77705c8a749576" title="-(c*t)<=>(-c)*t; if -c==0 return e<=>0. if(-c==1) return e<=>t">bvuminusBVMult</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00377"></a><span class="lineno"> 377</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a256b7d97aae2e5933ac4a9161c2da211" title="-(-e) <==> e">bvuminusBVUminus</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00378"></a><span class="lineno"> 378</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a6c8e614b400899e9f7e28cbfb6129a2a" title="-v <==> -1*v">bvuminusVar</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00379"></a><span class="lineno"> 379</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a4b76e0978912f6211ce0549cb9dd8550" title="c*(-t) <==> (-c)*t">bvmultBVUminus</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00380"></a><span class="lineno"> 380</span> <span class="comment"> //! -t <==> ~t+1</span></div>
<div class="line"><a name="l00381"></a><span class="lineno"> 381</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a4ede1f1385025a1621114addc25569c1" title="-t <==> ~t+1">bvuminusToBVPlus</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00382"></a><span class="lineno"> 382</span> <span class="comment"> //! -(c1*t1+...+cn*tn) <==> (-(c1*t1)+...+-(cn*tn))</span></div>
<div class="line"><a name="l00383"></a><span class="lineno"> 383</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a126c38f580c510745dacd0dea2cb5c15" title="-(c1*t1+...+cn*tn) <==> (-(c1*t1)+...+-(cn*tn))">bvuminusBVPlus</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00384"></a><span class="lineno"> 384</span> </div>
<div class="line"><a name="l00385"></a><span class="lineno"> 385</span> <span class="comment"></span></div>
<div class="line"><a name="l00386"></a><span class="lineno"> 386</span> <span class="comment"> ///////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00387"></a><span class="lineno"> 387</span> <span class="comment"> ///// Concatenation Normal Form rules</span></div>
<div class="line"><a name="l00388"></a><span class="lineno"> 388</span> <span class="comment"> ///////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00389"></a><span class="lineno"> 389</span> <span class="comment"></span></div>
<div class="line"><a name="l00390"></a><span class="lineno"> 390</span>  <span class="comment">// Extraction rules</span></div>
<div class="line"><a name="l00391"></a><span class="lineno"> 391</span> <span class="comment"></span></div>
<div class="line"><a name="l00392"></a><span class="lineno"> 392</span> <span class="comment"> //! c1[i:j] = c (extraction from a constant bitvector)</span></div>
<div class="line"><a name="l00393"></a><span class="lineno"> 393</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a8c0923ca7a786c2a7ee60cc7b456a9e0" title="c1[i:j] = c (extraction from a constant bitvector)">extractConst</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00394"></a><span class="lineno"> 394</span> <span class="comment"> //! t[n-1:0] = t for n-bit t</span></div>
<div class="line"><a name="l00395"></a><span class="lineno"> 395</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a8f8cd95c4037ee94e91ba93fe7d869c0" title="t[n-1:0] = t for n-bit t">extractWhole</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00396"></a><span class="lineno"> 396</span> <span class="comment"> //! t[i:j][k:l] = t[k+j:l+j] (eliminate double extraction)</span></div>
<div class="line"><a name="l00397"></a><span class="lineno"> 397</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a5c7969edaba735a5f73258b57ea42184" title="t[i:j][k:l] = t[k+j:l+j] (eliminate double extraction)">extractExtract</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00398"></a><span class="lineno"> 398</span> <span class="comment"> //! (t1 @ t2)[i:j] = t1[...] @ t2[...] (push extraction through concat)</span></div>
<div class="line"><a name="l00399"></a><span class="lineno"> 399</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#ad3f6288f648cee583f8dfee29fc97112" title="(t1 @ t2)[i:j] = t1[...] @ t2[...] (push extraction through concat)">extractConcat</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00400"></a><span class="lineno"> 400</span> <span class="comment"></span></div>
<div class="line"><a name="l00401"></a><span class="lineno"> 401</span> <span class="comment"> //! Auxiliary function: (t1 op t2)[i:j] = t1[i:j] op t2[i:j]</span></div>
<div class="line"><a name="l00402"></a><span class="lineno"> 402</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a222240751acfa38ed43f717c803aca34" title="Auxiliary function: (t1 op t2)[i:j] = t1[i:j] op t2[i:j].">extractBitwise</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <span class="keywordtype">int</span> kind, <span class="keyword">const</span> std::string& name);<span class="comment"></span></div>
<div class="line"><a name="l00403"></a><span class="lineno"> 403</span> <span class="comment"> //! (t1 & t2)[i:j] = t1[i:j] & t2[i:j] (push extraction through OR)</span></div>
<div class="line"><a name="l00404"></a><span class="lineno"> 404</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a0b3d60749f5bc14f524e0f5234bb1cf3" title="(t1 & t2)[i:j] = t1[i:j] & t2[i:j] (push extraction through OR)">extractAnd</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00405"></a><span class="lineno"> 405</span> <span class="comment"> //! (t1 | t2)[i:j] = t1[i:j] | t2[i:j] (push extraction through AND)</span></div>
<div class="line"><a name="l00406"></a><span class="lineno"> 406</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a7a8f90ee8e8450bcb4bfe3e1f231c4b0" title="(t1 | t2)[i:j] = t1[i:j] | t2[i:j] (push extraction through AND)">extractOr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00407"></a><span class="lineno"> 407</span> <span class="comment"> //! (~t)[i:j] = ~(t[i:j]) (push extraction through NEG)</span></div>
<div class="line"><a name="l00408"></a><span class="lineno"> 408</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a8014d2c21597d514e39a4fba8a060952" title="(~t)[i:j] = ~(t[i:j]) (push extraction through NEG)">extractNeg</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00409"></a><span class="lineno"> 409</span> </div>
<div class="line"><a name="l00410"></a><span class="lineno"> 410</span>  <span class="comment">// Negation rules</span></div>
<div class="line"><a name="l00411"></a><span class="lineno"> 411</span> <span class="comment"></span></div>
<div class="line"><a name="l00412"></a><span class="lineno"> 412</span> <span class="comment"> //! ~c1 = c (bit-wise negation of a constant bitvector)</span></div>
<div class="line"><a name="l00413"></a><span class="lineno"> 413</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a28038efe4f40407c727f91d856234d49" title="~c1 = c (bit-wise negation of a constant bitvector)">negConst</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00414"></a><span class="lineno"> 414</span> <span class="comment"> //! ~(t1\@...\@tn) = (~t1)\@...\@(~tn) -- push negation through concat</span></div>
<div class="line"><a name="l00415"></a><span class="lineno"> 415</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a8e1501e7e12f93e385f77c75a931b970" title="~(t1@...@tn) = (~t1)@...@(~tn) – push negation through concat">negConcat</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00416"></a><span class="lineno"> 416</span> <span class="comment"> //! ~(~t) = t -- eliminate double negation</span></div>
<div class="line"><a name="l00417"></a><span class="lineno"> 417</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#ae2ec10b9faef513781d02bb81cc3e88b" title="~(~t) = t – eliminate double negation">negNeg</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00418"></a><span class="lineno"> 418</span> <span class="comment"> //! ~t = -1*t + 1 -- eliminate negation</span></div>
<div class="line"><a name="l00419"></a><span class="lineno"> 419</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a8e6947b16b14750e13812e43b9f5080c" title="~t = -1*t + 1 – eliminate negation">negElim</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00420"></a><span class="lineno"> 420</span> <span class="comment"> //! ~(t1 & t2) <=> ~t1 | ~t2 -- DeMorgan's Laws</span></div>
<div class="line"><a name="l00421"></a><span class="lineno"> 421</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#abc285ae73d2259fe1efea8cb46b2698a" title="~(t1 & t2) <=> ~t1 | ~t2 – DeMorgan's Laws">negBVand</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00422"></a><span class="lineno"> 422</span> <span class="comment"> //! ~(t1 | t2) <=> ~t1 & ~t2 -- DeMorgan's Laws</span></div>
<div class="line"><a name="l00423"></a><span class="lineno"> 423</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#abf45c19e2d11f75d68785cc88f7ccf32" title="~(t1 | t2) <=> ~t1 & ~t2 – DeMorgan's Laws">negBVor</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00424"></a><span class="lineno"> 424</span> <span class="comment"> //! ~(t1 xor t2) = ~t1 xor t2</span></div>
<div class="line"><a name="l00425"></a><span class="lineno"> 425</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a815029f46058047bfe8a5e0dbc85ddc6" title="~(t1 xor t2) = ~t1 xor t2">negBVxor</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00426"></a><span class="lineno"> 426</span> <span class="comment"> //! ~(t1 xnor t2) = t1 xor t2</span></div>
<div class="line"><a name="l00427"></a><span class="lineno"> 427</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a2388a9d25fafcd0711a286d4666ee960" title="~(t1 xnor t2) = t1 xor t2">negBVxnor</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00428"></a><span class="lineno"> 428</span> </div>
<div class="line"><a name="l00429"></a><span class="lineno"> 429</span>  <span class="comment">// Bit-wise rules</span><span class="comment"></span></div>
<div class="line"><a name="l00430"></a><span class="lineno"> 430</span> <span class="comment"> //! Combine constants in bitwise AND, OR, XOR</span></div>
<div class="line"><a name="l00431"></a><span class="lineno"> 431</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#af3928b2385a298cc085134ac1e8222e4" title="Combine constants in bitwise AND, OR, XOR.">bitwiseConst</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <span class="keyword">const</span> std::vector<int>& idxs,</div>
<div class="line"><a name="l00432"></a><span class="lineno"> 432</span>  <span class="keywordtype">int</span> kind);<span class="comment"></span></div>
<div class="line"><a name="l00433"></a><span class="lineno"> 433</span> <span class="comment"> //! Lifts concatenation above bitwise operators.</span></div>
<div class="line"><a name="l00434"></a><span class="lineno"> 434</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a731d832fce739c8b6d7b5ccf9932a94a" title="Lifts concatenation above bitwise operators.">bitwiseConcat</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <span class="keywordtype">int</span> kind);<span class="comment"></span></div>
<div class="line"><a name="l00435"></a><span class="lineno"> 435</span> <span class="comment"> //! Flatten bitwise operation</span></div>
<div class="line"><a name="l00436"></a><span class="lineno"> 436</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#ac6e8075bfc61e657a37648ba78003f36" title="Flatten bitwise operation.">bitwiseFlatten</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <span class="keywordtype">int</span> kind);<span class="comment"></span></div>
<div class="line"><a name="l00437"></a><span class="lineno"> 437</span> <span class="comment"> //! Simplify bitwise operator containing a constant child</span></div>
<div class="line"><a name="l00438"></a><span class="lineno"> 438</span> <span class="comment"></span><span class="comment"> /*! \param e is the bit-wise expr</span></div>
<div class="line"><a name="l00439"></a><span class="lineno"> 439</span> <span class="comment"> * \param idx is the index of the constant bitvector</span></div>
<div class="line"><a name="l00440"></a><span class="lineno"> 440</span> <span class="comment"> * \param kind is the kind of e</span></div>
<div class="line"><a name="l00441"></a><span class="lineno"> 441</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00442"></a><span class="lineno"> 442</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#aac798843b8390b423f901f9cc1cb14dd" title="Simplify bitwise operator containing a constant child.">bitwiseConstElim</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <span class="keywordtype">int</span> idx, <span class="keywordtype">int</span> kind);</div>
<div class="line"><a name="l00443"></a><span class="lineno"> 443</span> <span class="comment"></span></div>
<div class="line"><a name="l00444"></a><span class="lineno"> 444</span> <span class="comment"> /*! checks if e is already present in likeTerms without conflicts.</span></div>
<div class="line"><a name="l00445"></a><span class="lineno"> 445</span> <span class="comment"> * if yes return 1, else{ if conflict return -1 else return 0 }</span></div>
<div class="line"><a name="l00446"></a><span class="lineno"> 446</span> <span class="comment"> * we have conflict if</span></div>
<div class="line"><a name="l00447"></a><span class="lineno"> 447</span> <span class="comment"> * 1. the kind of e is BVNEG,</span></div>
<div class="line"><a name="l00448"></a><span class="lineno"> 448</span> <span class="comment"> * and e[0] is already present in likeTerms</span></div>
<div class="line"><a name="l00449"></a><span class="lineno"> 449</span> <span class="comment"> * 2. ~e is present in likeTerms already</span></div>
<div class="line"><a name="l00450"></a><span class="lineno"> 450</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00451"></a><span class="lineno"> 451</span>  <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#ae51599976453a95306a7b5a0b2e15029">sameKidCheck</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<int></a>& likeTerms);</div>
<div class="line"><a name="l00452"></a><span class="lineno"> 452</span> </div>
<div class="line"><a name="l00453"></a><span class="lineno"> 453</span>  <span class="comment">// Concatenation rules</span></div>
<div class="line"><a name="l00454"></a><span class="lineno"> 454</span> <span class="comment"></span></div>
<div class="line"><a name="l00455"></a><span class="lineno"> 455</span> <span class="comment"> //! c1\@c2\@...\@cn = c (concatenation of constant bitvectors)</span></div>
<div class="line"><a name="l00456"></a><span class="lineno"> 456</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#abee7fa8ab42b1addc72b7463b4a60975" title="c1@c2@...@cn = c (concatenation of constant bitvectors)">concatConst</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00457"></a><span class="lineno"> 457</span> <span class="comment"> //! Flatten one level of nested concatenation, e.g.: x\@(y\@z)\@w = x\@y\@z\@w</span></div>
<div class="line"><a name="l00458"></a><span class="lineno"> 458</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#adba6266c081af892dadf257a001ae920" title="Flatten one level of nested concatenation, e.g.: x@(y@z)@w = x@y@z@w.">concatFlatten</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00459"></a><span class="lineno"> 459</span> <span class="comment"> //! Merge n-ary concat. of adjacent extractions: x[15:8]\@x[7:0] = x[15:0]</span></div>
<div class="line"><a name="l00460"></a><span class="lineno"> 460</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#af8c35b9567c60d128480b278de348842" title="Merge n-ary concat. of adjacent extractions: x[15:8]@x[7:0] = x[15:0].">concatMergeExtract</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00461"></a><span class="lineno"> 461</span> <span class="comment"></span></div>
<div class="line"><a name="l00462"></a><span class="lineno"> 462</span> <span class="comment"> ///////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00463"></a><span class="lineno"> 463</span> <span class="comment"> ///// Modulo arithmetic rules</span></div>
<div class="line"><a name="l00464"></a><span class="lineno"> 464</span> <span class="comment"> ///////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00465"></a><span class="lineno"> 465</span> <span class="comment"></span><span class="comment"></span></div>
<div class="line"><a name="l00466"></a><span class="lineno"> 466</span> <span class="comment"> //! BVPLUS(n, c1,c2,...,cn) = c (bit-vector plus of constant bitvectors)</span></div>
<div class="line"><a name="l00467"></a><span class="lineno"> 467</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a8475377c17d5c4241e1a134ce5b28eba" title="BVPLUS(n, c1,c2,...,cn) = c (bit-vector plus of constant bitvectors)">bvplusConst</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span></div>
<div class="line"><a name="l00468"></a><span class="lineno"> 468</span> <span class="comment"> /*! @brief n*c1 = c, where n >= 0 (multiplication of a constant</span></div>
<div class="line"><a name="l00469"></a><span class="lineno"> 469</span> <span class="comment"> * bitvector by a non-negative constant) */</span></div>
<div class="line"><a name="l00470"></a><span class="lineno"> 470</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a05e4123ccbc5000dbf9615d89e13067d" title="n*c1 = c, where n >= 0 (multiplication of a constant bitvector by a non-negative constant)">bvmultConst</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00471"></a><span class="lineno"> 471</span> <span class="comment"></span></div>
<div class="line"><a name="l00472"></a><span class="lineno"> 472</span> <span class="comment"> ///////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00473"></a><span class="lineno"> 473</span> <span class="comment"> ///// Type predicate rules</span></div>
<div class="line"><a name="l00474"></a><span class="lineno"> 474</span> <span class="comment"> ///////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00475"></a><span class="lineno"> 475</span> <span class="comment"></span><span class="comment"></span></div>
<div class="line"><a name="l00476"></a><span class="lineno"> 476</span> <span class="comment"> //! |- t=0 OR t=1 for any 1-bit bitvector t</span></div>
<div class="line"><a name="l00477"></a><span class="lineno"> 477</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#aea2fb217bff7c7b46f996eacd051461b" title="|- t=0 OR t=1 for any 1-bit bitvector t">typePredBit</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00478"></a><span class="lineno"> 478</span> <span class="comment"></span></div>
<div class="line"><a name="l00479"></a><span class="lineno"> 479</span> <span class="comment"> //! Expand the type predicate wrapper (compute the actual type predicate)</span></div>
<div class="line"><a name="l00480"></a><span class="lineno"> 480</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a7d8030814a36206774951e3ae8968848" title="Expand the type predicate wrapper (compute the actual type predicate)">expandTypePred</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& tp);</div>
<div class="line"><a name="l00481"></a><span class="lineno"> 481</span> <span class="comment"></span></div>
<div class="line"><a name="l00482"></a><span class="lineno"> 482</span> <span class="comment"> ////////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00483"></a><span class="lineno"> 483</span> <span class="comment"></span> <span class="comment">// Helper functions</span><span class="comment"></span></div>
<div class="line"><a name="l00484"></a><span class="lineno"> 484</span> <span class="comment"> ////////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00485"></a><span class="lineno"> 485</span> <span class="comment"> //! Create Expr from Rational (for convenience)</span></div>
<div class="line"><a name="l00486"></a><span class="lineno"><a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#ae03f092d2050783885e338b5880b2645"> 486</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#ae03f092d2050783885e338b5880b2645">rat</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Rational.html">Rational</a>& r) { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremProducer.html#a1b706238281ad141a57363a6890f14a5">d_em</a>-><a class="code" href="group__EM__Priv.html#ga18423a42ce6557dc33287d3979ccc3c6">newRatExpr</a>(r); }<span class="comment"></span></div>
<div class="line"><a name="l00487"></a><span class="lineno"> 487</span> <span class="comment"> /*! \param t1BitExtractThms : input1 is vector of bitblasts of t1,</span></div>
<div class="line"><a name="l00488"></a><span class="lineno"> 488</span> <span class="comment"> * from bit i-1 to 0</span></div>
<div class="line"><a name="l00489"></a><span class="lineno"> 489</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00490"></a><span class="lineno"> 490</span> <span class="comment"> * \param t2BitExtractThms : input2 is vector of bitblasts of t2,</span></div>
<div class="line"><a name="l00491"></a><span class="lineno"> 491</span> <span class="comment"> * from bit i-1 to 0</span></div>
<div class="line"><a name="l00492"></a><span class="lineno"> 492</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00493"></a><span class="lineno"> 493</span> <span class="comment"> * \param bitPos : input3 is extracted * bitposition</span></div>
<div class="line"><a name="l00494"></a><span class="lineno"> 494</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00495"></a><span class="lineno"> 495</span> <span class="comment"> * \result is the expression \f$t1[0] \wedge t2[0]\f$ if</span></div>
<div class="line"><a name="l00496"></a><span class="lineno"> 496</span> <span class="comment"> * bitPos=0. this function is recursive; if bitPos > 0 then the</span></div>
<div class="line"><a name="l00497"></a><span class="lineno"> 497</span> <span class="comment"> * output expression is</span></div>
<div class="line"><a name="l00498"></a><span class="lineno"> 498</span> <span class="comment"> * \f[ (t1[i-1] \wedge t2[i-1])</span></div>
<div class="line"><a name="l00499"></a><span class="lineno"> 499</span> <span class="comment"> * \vee (t1[i-1] \wedge computeCarry(t1,t2,i-1))</span></div>
<div class="line"><a name="l00500"></a><span class="lineno"> 500</span> <span class="comment"> * \vee (t2[i-1] \wedge computeCarry(t1,t2,i-1))</span></div>
<div class="line"><a name="l00501"></a><span class="lineno"> 501</span> <span class="comment"> * \f]</span></div>
<div class="line"><a name="l00502"></a><span class="lineno"> 502</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00503"></a><span class="lineno"> 503</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a433503188cd190201bbea389cbc43478">computeCarry</a>(<span class="keyword">const</span> std::vector<Theorem>& t1BitExtractThms,</div>
<div class="line"><a name="l00504"></a><span class="lineno"> 504</span>  <span class="keyword">const</span> std::vector<Theorem>& t2BitExtractThms,</div>
<div class="line"><a name="l00505"></a><span class="lineno"> 505</span>  <span class="keywordtype">int</span> bitPos);</div>
<div class="line"><a name="l00506"></a><span class="lineno"> 506</span> </div>
<div class="line"><a name="l00507"></a><span class="lineno"> 507</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#afdb4f9bf82d3ab61d6ac486b7807aa71" title="compute carryout of the current bits and cache them, and return">computeCarryPreComputed</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t1_i,</div>
<div class="line"><a name="l00508"></a><span class="lineno"> 508</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t2_i,</div>
<div class="line"><a name="l00509"></a><span class="lineno"> 509</span>  <span class="keywordtype">int</span> bitPos,</div>
<div class="line"><a name="l00510"></a><span class="lineno"> 510</span>  <span class="keywordtype">int</span> precomputedFlag);</div>
<div class="line"><a name="l00511"></a><span class="lineno"> 511</span> </div>
<div class="line"><a name="l00512"></a><span class="lineno"> 512</span>  <span class="comment">/*Beginning of Lorenzo PLatania's methods*/</span></div>
<div class="line"><a name="l00513"></a><span class="lineno"> 513</span> </div>
<div class="line"><a name="l00514"></a><span class="lineno"> 514</span>  <span class="comment">// virtual Theorem multiply_coeff( Rational mult_inv, const Expr& e);</span><span class="comment"></span></div>
<div class="line"><a name="l00515"></a><span class="lineno"> 515</span> <span class="comment"> //! isolate a variable with coefficient = 1 on the Lhs of an</span></div>
<div class="line"><a name="l00516"></a><span class="lineno"> 516</span> <span class="comment"></span> <span class="comment">//equality expression</span></div>
<div class="line"><a name="l00517"></a><span class="lineno"> 517</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a54d8f6979007cfc5e0da1ebf7f73f51d" title="isolate a variable with coefficient = 1 on the Lhs of an">isolate_var</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00518"></a><span class="lineno"> 518</span> </div>
<div class="line"><a name="l00519"></a><span class="lineno"> 519</span>  <span class="comment">// BVPLUS(N, a@b, y) = BVPLUS(N-n,a,BVPLUS(N,b,y)[N-1:n])@BVPLUS(n,b,y)</span></div>
<div class="line"><a name="l00520"></a><span class="lineno"> 520</span>  <span class="comment">// where n = BVSize(b), a != 0</span></div>
<div class="line"><a name="l00521"></a><span class="lineno"> 521</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a91a4bd06c22c93729e954302840877ad">liftConcatBVMult</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00522"></a><span class="lineno"> 522</span> <span class="comment"></span></div>
<div class="line"><a name="l00523"></a><span class="lineno"> 523</span> <span class="comment"> //! canonize BVMult expressions in order to get one coefficient</span></div>
<div class="line"><a name="l00524"></a><span class="lineno"> 524</span> <span class="comment"></span> <span class="comment">//multiplying the variable(s) in the expression</span></div>
<div class="line"><a name="l00525"></a><span class="lineno"> 525</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#aa5acae5a384220d4dca181b8675831b3" title="canonize BVMult expressions in order to get one coefficient">canonBVMult</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e );</div>
<div class="line"><a name="l00526"></a><span class="lineno"> 526</span> </div>
<div class="line"><a name="l00527"></a><span class="lineno"> 527</span>  <span class="comment">// BVPLUS(N, a@b, y) = BVPLUS(N-n,a,BVPLUS(N,b,y)[N-1:n])@BVPLUS(n,b,y)</span></div>
<div class="line"><a name="l00528"></a><span class="lineno"> 528</span>  <span class="comment">// where n = BVSize(b)</span></div>
<div class="line"><a name="l00529"></a><span class="lineno"> 529</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a5fb475feef8b6740cc8c2f5f2104f07d">liftConcatBVPlus</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00530"></a><span class="lineno"> 530</span> <span class="comment"></span></div>
<div class="line"><a name="l00531"></a><span class="lineno"> 531</span> <span class="comment"> //! canonize BVPlus expressions in order to get just one</span></div>
<div class="line"><a name="l00532"></a><span class="lineno"> 532</span> <span class="comment"></span> <span class="comment">//coefficient multiplying each variable in the expression</span></div>
<div class="line"><a name="l00533"></a><span class="lineno"> 533</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a31b9e200eff6852b66a8d8ac19ec2db3" title="canonize BVPlus expressions in order to get just one">canonBVPlus</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e );</div>
<div class="line"><a name="l00534"></a><span class="lineno"> 534</span> <span class="comment"></span></div>
<div class="line"><a name="l00535"></a><span class="lineno"> 535</span> <span class="comment"> //! canonize BVMinus expressions: push the minus to the leafs in</span></div>
<div class="line"><a name="l00536"></a><span class="lineno"> 536</span> <span class="comment"></span> <span class="comment">//BVPLUS expr; simplify minus in BVMULT and BVMINUS expr</span></div>
<div class="line"><a name="l00537"></a><span class="lineno"> 537</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#af3fc29529753dc8161360688bcaaf12b" title="canonize BVMinus expressions: push the minus to the leafs in">canonBVUMinus</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e );</div>
<div class="line"><a name="l00538"></a><span class="lineno"> 538</span> </div>
<div class="line"><a name="l00539"></a><span class="lineno"> 539</span>  <span class="comment">// Input: t[hi:lo] = rhs</span></div>
<div class="line"><a name="l00540"></a><span class="lineno"> 540</span>  <span class="comment">// if t appears as leaf in rhs, then:</span></div>
<div class="line"><a name="l00541"></a><span class="lineno"> 541</span>  <span class="comment">// t[hi:lo] = rhs |- Exists x,y,z. (t = x @ y @ z AND y = rhs), solvedForm = false</span></div>
<div class="line"><a name="l00542"></a><span class="lineno"> 542</span>  <span class="comment">// else</span></div>
<div class="line"><a name="l00543"></a><span class="lineno"> 543</span>  <span class="comment">// t[hi:lo] = rhs |- Exists x,y,z. (t = x @ rhs @ z AND y = rhs), solvedForm = true</span></div>
<div class="line"><a name="l00544"></a><span class="lineno"> 544</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a8475d9fad4a99ea877f69e154f1d67d6">processExtract</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e, <span class="keywordtype">bool</span>& solvedForm);</div>
<div class="line"><a name="l00545"></a><span class="lineno"> 545</span> </div>
<div class="line"><a name="l00546"></a><span class="lineno"> 546</span>  <span class="comment">// normalizes equation</span></div>
<div class="line"><a name="l00547"></a><span class="lineno"> 547</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#ac946768d5a1aae35472b63b53b457264">canonBVEQ</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <span class="keywordtype">int</span> maxEffort = 3 );</div>
<div class="line"><a name="l00548"></a><span class="lineno"> 548</span> <span class="comment"></span></div>
<div class="line"><a name="l00549"></a><span class="lineno"> 549</span> <span class="comment"> //! apply the distributive rule on the BVMULT expression e</span></div>
<div class="line"><a name="l00550"></a><span class="lineno"> 550</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a9fe7ec7e369ee92339471e805a1dd7c3" title="apply the distributive rule on the BVMULT expression e">distributive_rule</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e );</div>
<div class="line"><a name="l00551"></a><span class="lineno"> 551</span>  <span class="comment">// virtual Theorem BVMultConstTerm( const Expr& e1, const Expr& e2);</span></div>
<div class="line"><a name="l00552"></a><span class="lineno"> 552</span>  <span class="comment">// recursively reorder subterms in a BVMULT term</span></div>
<div class="line"><a name="l00553"></a><span class="lineno"> 553</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a87288805014f1d0e935c052364142d6b">BVMult_order_subterms</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00554"></a><span class="lineno"> 554</span> </div>
<div class="line"><a name="l00555"></a><span class="lineno"> 555</span>  <span class="comment">// rewrites the equation in the form 0 = Expr</span></div>
<div class="line"><a name="l00556"></a><span class="lineno"> 556</span>  <span class="comment">// this is needed for TheoryBitvector::solve</span></div>
<div class="line"><a name="l00557"></a><span class="lineno"> 557</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a0f02e48875ccb661cae7cc7a2489dce1">MarkNonSolvableEq</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00558"></a><span class="lineno"> 558</span>  <span class="comment">/*End of Lorenzo PLatania's methods*/</span></div>
<div class="line"><a name="l00559"></a><span class="lineno"> 559</span> </div>
<div class="line"><a name="l00560"></a><span class="lineno"> 560</span>  <span class="comment">// rewrite BVZEROEXTEND into CONCAT</span></div>
<div class="line"><a name="l00561"></a><span class="lineno"> 561</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a8295f4644a077f3c8af0db53be7b458b" title="BVZEROEXTEND(e, i) = zeroString @ e.">zeroExtendRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00562"></a><span class="lineno"> 562</span> </div>
<div class="line"><a name="l00563"></a><span class="lineno"> 563</span>  <span class="comment">// rewrite BVREPEAT into CONCAT</span></div>
<div class="line"><a name="l00564"></a><span class="lineno"> 564</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a9b9a128c7c863d01c804bfec956ffb6c" title="BVREPEAT(e, i) = e @ e @ ... @ e.">repeatRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00565"></a><span class="lineno"> 565</span> </div>
<div class="line"><a name="l00566"></a><span class="lineno"> 566</span>  <span class="comment">// rewrite BVROTL into CONCAT</span></div>
<div class="line"><a name="l00567"></a><span class="lineno"> 567</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#afdc5b05255d1d217c26d5e3660957fde" title="BVROTL(e, i) = a[n-i-1:0] @ a[n-1:n-i].">rotlRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00568"></a><span class="lineno"> 568</span>  <span class="comment">// rewrite BVROTR into CONCAT</span></div>
<div class="line"><a name="l00569"></a><span class="lineno"> 569</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a6495867fe7ef34a838e83315dd8b02e4" title="BVROTR(e, i) = a[i-1:0] @ a[n-1:i].">rotrRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00570"></a><span class="lineno"> 570</span> </div>
<div class="line"><a name="l00571"></a><span class="lineno"> 571</span>  <span class="comment">// Dejan: Division rewrites</span></div>
<div class="line"><a name="l00572"></a><span class="lineno"> 572</span> <span class="comment"></span></div>
<div class="line"><a name="l00573"></a><span class="lineno"> 573</span> <span class="comment"> /**</span></div>
<div class="line"><a name="l00574"></a><span class="lineno"> 574</span> <span class="comment"> * Divide a with b unsigned and return the bit-vector constant result</span></div>
<div class="line"><a name="l00575"></a><span class="lineno"> 575</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00576"></a><span class="lineno"> 576</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#acc221d6c256b7d550090627e6fee9643">bvUDivConst</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& divExpr);</div>
<div class="line"><a name="l00577"></a><span class="lineno"> 577</span> <span class="comment"></span></div>
<div class="line"><a name="l00578"></a><span class="lineno"> 578</span> <span class="comment"> /**</span></div>
<div class="line"><a name="l00579"></a><span class="lineno"> 579</span> <span class="comment"> * Rewrite x/y to</span></div>
<div class="line"><a name="l00580"></a><span class="lineno"> 580</span> <span class="comment"> * \f[\exists s: s = x/y \wedge (y \neq 0 \implies x = y * s + m \wedge 0 <= m < y)\f]</span></div>
<div class="line"><a name="l00581"></a><span class="lineno"> 581</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00582"></a><span class="lineno"> 582</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a330fc1ea75378bfe0fec034132af7400">bvUDivTheorem</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& divExpr);</div>
<div class="line"><a name="l00583"></a><span class="lineno"> 583</span> <span class="comment"></span></div>
<div class="line"><a name="l00584"></a><span class="lineno"> 584</span> <span class="comment"> /**</span></div>
<div class="line"><a name="l00585"></a><span class="lineno"> 585</span> <span class="comment"> * Compute the remainder</span></div>
<div class="line"><a name="l00586"></a><span class="lineno"> 586</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00587"></a><span class="lineno"> 587</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#af8bafa1141beb24e3742bce376697e8f">bvURemConst</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& remExpr);</div>
<div class="line"><a name="l00588"></a><span class="lineno"> 588</span> <span class="comment"></span></div>
<div class="line"><a name="l00589"></a><span class="lineno"> 589</span> <span class="comment"> /**</span></div>
<div class="line"><a name="l00590"></a><span class="lineno"> 590</span> <span class="comment"> * Rewrite a%b in terms of a/b, i.e. a - a/b</span></div>
<div class="line"><a name="l00591"></a><span class="lineno"> 591</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00592"></a><span class="lineno"> 592</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#aa6941790eb888168ffdc5531b129b466">bvURemRewrite</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& remExpr);</div>
<div class="line"><a name="l00593"></a><span class="lineno"> 593</span> <span class="comment"></span></div>
<div class="line"><a name="l00594"></a><span class="lineno"> 594</span> <span class="comment"> /**</span></div>
<div class="line"><a name="l00595"></a><span class="lineno"> 595</span> <span class="comment"> * Bit-blast the multiplication a_times_b given the bits in a_bits and b_bits.</span></div>
<div class="line"><a name="l00596"></a><span class="lineno"> 596</span> <span class="comment"> * The resulting output bits will be in the vector output_bits. The return value</span></div>
<div class="line"><a name="l00597"></a><span class="lineno"> 597</span> <span class="comment"> * is a theorem saying there is no overflow for this multiplication. (TODO, it's</span></div>
<div class="line"><a name="l00598"></a><span class="lineno"> 598</span> <span class="comment"> * just an empty theorem for now).</span></div>
<div class="line"><a name="l00599"></a><span class="lineno"> 599</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00600"></a><span class="lineno"> 600</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a714a402f525e0d0c222846379366edc5">bitblastBVMult</a>(<span class="keyword">const</span> std::vector<Theorem>& a_bits,</div>
<div class="line"><a name="l00601"></a><span class="lineno"> 601</span>  <span class="keyword">const</span> std::vector<Theorem>& b_bits,</div>
<div class="line"><a name="l00602"></a><span class="lineno"> 602</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& a_times_b,</div>
<div class="line"><a name="l00603"></a><span class="lineno"> 603</span>  std::vector<Theorem>& output_bits);</div>
<div class="line"><a name="l00604"></a><span class="lineno"> 604</span> <span class="comment"></span></div>
<div class="line"><a name="l00605"></a><span class="lineno"> 605</span> <span class="comment"> /**</span></div>
<div class="line"><a name="l00606"></a><span class="lineno"> 606</span> <span class="comment"> * Bit-blast the sum a_plus_b given the bits in a_bits and b_bits.</span></div>
<div class="line"><a name="l00607"></a><span class="lineno"> 607</span> <span class="comment"> * The resulting output bits will be in the vector output_bits. The return value</span></div>
<div class="line"><a name="l00608"></a><span class="lineno"> 608</span> <span class="comment"> * is a theorem saying there is no overflow for this sum. (TODO, it's</span></div>
<div class="line"><a name="l00609"></a><span class="lineno"> 609</span> <span class="comment"> * just an empty theorem for now).</span></div>
<div class="line"><a name="l00610"></a><span class="lineno"> 610</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00611"></a><span class="lineno"> 611</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#aef3181ea41680c3f7b1b4ec724e8b68d">bitblastBVPlus</a>(<span class="keyword">const</span> std::vector<Theorem>& a_bits,</div>
<div class="line"><a name="l00612"></a><span class="lineno"> 612</span>  <span class="keyword">const</span> std::vector<Theorem>& b_bits,</div>
<div class="line"><a name="l00613"></a><span class="lineno"> 613</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& a_plus_b,</div>
<div class="line"><a name="l00614"></a><span class="lineno"> 614</span>  std::vector<Theorem>& output_bits);</div>
<div class="line"><a name="l00615"></a><span class="lineno"> 615</span> <span class="comment"></span></div>
<div class="line"><a name="l00616"></a><span class="lineno"> 616</span> <span class="comment"> /**</span></div>
<div class="line"><a name="l00617"></a><span class="lineno"> 617</span> <span class="comment"> * Rewrite the signed divide in terms of the unsigned one.</span></div>
<div class="line"><a name="l00618"></a><span class="lineno"> 618</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00619"></a><span class="lineno"> 619</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#ad3bdebd3ad40f70a1592fda3fae82e71">bvSDivRewrite</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& sDivExpr);</div>
<div class="line"><a name="l00620"></a><span class="lineno"> 620</span> <span class="comment"></span></div>
<div class="line"><a name="l00621"></a><span class="lineno"> 621</span> <span class="comment"> /**</span></div>
<div class="line"><a name="l00622"></a><span class="lineno"> 622</span> <span class="comment"> * Rewrite the signed remainder in terms of the unsigned one.</span></div>
<div class="line"><a name="l00623"></a><span class="lineno"> 623</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00624"></a><span class="lineno"> 624</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a73632313f926e7b93104538c465bbcfb">bvSRemRewrite</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& sRemExpr);</div>
<div class="line"><a name="l00625"></a><span class="lineno"> 625</span> <span class="comment"></span></div>
<div class="line"><a name="l00626"></a><span class="lineno"> 626</span> <span class="comment"> /**</span></div>
<div class="line"><a name="l00627"></a><span class="lineno"> 627</span> <span class="comment"> * Rewrite the signed mod in terms of the unsigned one.</span></div>
<div class="line"><a name="l00628"></a><span class="lineno"> 628</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00629"></a><span class="lineno"> 629</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a8d5827e983be4b7ed387314332ac4613">bvSModRewrite</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& sModExpr);</div>
<div class="line"><a name="l00630"></a><span class="lineno"> 630</span> <span class="comment"></span></div>
<div class="line"><a name="l00631"></a><span class="lineno"> 631</span> <span class="comment"> /**</span></div>
<div class="line"><a name="l00632"></a><span class="lineno"> 632</span> <span class="comment"> * Rewrite \f[x_1 \vee x_2 \vee \ldots \vee x_n = 0\f] into</span></div>
<div class="line"><a name="l00633"></a><span class="lineno"> 633</span> <span class="comment"> * \f[x_1 = 0 \wedge x_2 = 0 \wedge \ldots \wedge x_n = 0\f].</span></div>
<div class="line"><a name="l00634"></a><span class="lineno"> 634</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00635"></a><span class="lineno"> 635</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a9200f74bce7930bb77d5e2a00b81a1d4">zeroBVOR</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& orEqZero);</div>
<div class="line"><a name="l00636"></a><span class="lineno"> 636</span> <span class="comment"></span></div>
<div class="line"><a name="l00637"></a><span class="lineno"> 637</span> <span class="comment"> /**</span></div>
<div class="line"><a name="l00638"></a><span class="lineno"> 638</span> <span class="comment"> * Rewrite \f[x_1 \wedge x_2 \wedge \ldots \wedge x_n = 1^n\f] into</span></div>
<div class="line"><a name="l00639"></a><span class="lineno"> 639</span> <span class="comment"> * \f[x_1 = 1^n \wedge x_2 = 1^n \wedge \ldots \wedge x_n = 1^n\f].</span></div>
<div class="line"><a name="l00640"></a><span class="lineno"> 640</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00641"></a><span class="lineno"> 641</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a1d422c14bfbcac9e91c53260b856b93e">oneBVAND</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& andEqOne);</div>
<div class="line"><a name="l00642"></a><span class="lineno"> 642</span> <span class="comment"></span></div>
<div class="line"><a name="l00643"></a><span class="lineno"> 643</span> <span class="comment"> /**</span></div>
<div class="line"><a name="l00644"></a><span class="lineno"> 644</span> <span class="comment"> * Equalities over constants go to true/false.</span></div>
<div class="line"><a name="l00645"></a><span class="lineno"> 645</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00646"></a><span class="lineno"> 646</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a9c0a8eae91823c04c12dbedbbbbd417f">constEq</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& eq);</div>
<div class="line"><a name="l00647"></a><span class="lineno"> 647</span> <span class="comment"></span></div>
<div class="line"><a name="l00648"></a><span class="lineno"> 648</span> <span class="comment"> /**</span></div>
<div class="line"><a name="l00649"></a><span class="lineno"> 649</span> <span class="comment"> * Returns true if equation is of the form x[i:j] = x[k:l], where the</span></div>
<div class="line"><a name="l00650"></a><span class="lineno"> 650</span> <span class="comment"> * extracted segments overlap, i.e. i > j >= k > l or k > i >= l > j.</span></div>
<div class="line"><a name="l00651"></a><span class="lineno"> 651</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00652"></a><span class="lineno"> 652</span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#adf540a2323b9f9ba281d2d67826cdae7">solveExtractOverlapApplies</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& eq);</div>
<div class="line"><a name="l00653"></a><span class="lineno"> 653</span> <span class="comment"></span></div>
<div class="line"><a name="l00654"></a><span class="lineno"> 654</span> <span class="comment"> /**</span></div>
<div class="line"><a name="l00655"></a><span class="lineno"> 655</span> <span class="comment"> * Returns the theorem that simplifies the equality of two overlapping</span></div>
<div class="line"><a name="l00656"></a><span class="lineno"> 656</span> <span class="comment"> * extracts over the same term.</span></div>
<div class="line"><a name="l00657"></a><span class="lineno"> 657</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00658"></a><span class="lineno"> 658</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1BitvectorTheoremProducer.html#a79998a92001fa8625a471bf7011b9cd3">solveExtractOverlap</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& eq);</div>
<div class="line"><a name="l00659"></a><span class="lineno"> 659</span> </div>
<div class="line"><a name="l00660"></a><span class="lineno"> 660</span> </div>
<div class="line"><a name="l00661"></a><span class="lineno"> 661</span> }; <span class="comment">// end of class BitvectorTheoremProducer</span></div>
<div class="line"><a name="l00662"></a><span class="lineno"> 662</span> } <span class="comment">// end of name-space CVC3</span></div>
<div class="line"><a name="l00663"></a><span class="lineno"> 663</span> </div>
<div class="line"><a name="l00664"></a><span class="lineno"> 664</span> </div>
<div class="line"><a name="l00665"></a><span class="lineno"> 665</span> <span class="preprocessor">#endif</span></div>
<div class="line"><a name="l00666"></a><span class="lineno"> 666</span> <span class="preprocessor"></span></div>
</div><!-- fragment --></div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:13 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>
