<!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: theory_bitvector.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_b0856f6b0d80ccb263b2f415c91f9e17.html">include</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="headertitle">
<div class="title">theory_bitvector.h</div> </div>
</div><!--header-->
<div class="contents">
<a href="theory__bitvector_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 theory_bitvector.h</span></div>
<div class="line"><a name="l00004"></a><span class="lineno"> 4</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00005"></a><span class="lineno"> 5</span> <span class="comment"> * Author: Vijay Ganesh</span></div>
<div class="line"><a name="l00006"></a><span class="lineno"> 6</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00007"></a><span class="lineno"> 7</span> <span class="comment"> * Created: Wed May 05 18:34:55 PDT 2004</span></div>
<div class="line"><a name="l00008"></a><span class="lineno"> 8</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00009"></a><span class="lineno"> 9</span> <span class="comment"> * <hr></span></div>
<div class="line"><a name="l00010"></a><span class="lineno"> 10</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00011"></a><span class="lineno"> 11</span> <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span></div>
<div class="line"><a name="l00012"></a><span class="lineno"> 12</span> <span class="comment"> * and its documentation for any purpose is hereby granted without</span></div>
<div class="line"><a name="l00013"></a><span class="lineno"> 13</span> <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span></div>
<div class="line"><a name="l00014"></a><span class="lineno"> 14</span> <span class="comment"> * LICENSE file provided with this distribution.</span></div>
<div class="line"><a name="l00015"></a><span class="lineno"> 15</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00016"></a><span class="lineno"> 16</span> <span class="comment"> * <hr></span></div>
<div class="line"><a name="l00017"></a><span class="lineno"> 17</span> <span class="comment"> *</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> </div>
<div class="line"><a name="l00021"></a><span class="lineno"> 21</span> <span class="preprocessor">#ifndef _cvc3__include__theory_bitvector_h_</span></div>
<div class="line"><a name="l00022"></a><span class="lineno"> 22</span> <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__include__theory_bitvector_h_</span></div>
<div class="line"><a name="l00023"></a><span class="lineno"> 23</span> <span class="preprocessor"></span></div>
<div class="line"><a name="l00024"></a><span class="lineno"> 24</span> <span class="preprocessor">#include "<a class="code" href="theory__core_8h.html">theory_core.h</a>"</span></div>
<div class="line"><a name="l00025"></a><span class="lineno"> 25</span> <span class="preprocessor">#include "<a class="code" href="statistics_8h.html" title="Description: Counters and flags for collecting run-time statistics.">statistics.h</a>"</span></div>
<div class="line"><a name="l00026"></a><span class="lineno"> 26</span> </div>
<div class="line"><a name="l00027"></a><span class="lineno"> 27</span> <span class="keyword">namespace </span>CVC3 {</div>
<div class="line"><a name="l00028"></a><span class="lineno"> 28</span> </div>
<div class="line"><a name="l00029"></a><span class="lineno"> 29</span>  <span class="keyword">class </span>VCL;</div>
<div class="line"><a name="l00030"></a><span class="lineno"> 30</span>  <span class="keyword">class </span>BitvectorProofRules;</div>
<div class="line"><a name="l00031"></a><span class="lineno"> 31</span> </div>
<div class="line"><a name="l00032"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fc"> 32</a></span>  <span class="keyword">typedef</span> <span class="keyword">enum</span> { <span class="comment">//some new BV kinds</span></div>
<div class="line"><a name="l00033"></a><span class="lineno"> 33</span>  <span class="comment">// New constants</span></div>
<div class="line"><a name="l00034"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcab517c07f8090ef28822598285c61506d"> 34</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcab517c07f8090ef28822598285c61506d">BVCONST</a> = 80,</div>
<div class="line"><a name="l00035"></a><span class="lineno"> 35</span> </div>
<div class="line"><a name="l00036"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca4099d4b4e4424d6ca22eb0b3fdc73bfa"> 36</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca4099d4b4e4424d6ca22eb0b3fdc73bfa">BITVECTOR</a> = 8000,</div>
<div class="line"><a name="l00037"></a><span class="lineno"> 37</span> </div>
<div class="line"><a name="l00038"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcac706ade993a8d075e5b0e05384f40da2"> 38</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcac706ade993a8d075e5b0e05384f40da2">CONCAT</a>,</div>
<div class="line"><a name="l00039"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca814f4580c72ef19f37aeac1b0dc7f7e9"> 39</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca814f4580c72ef19f37aeac1b0dc7f7e9">EXTRACT</a>,</div>
<div class="line"><a name="l00040"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcaf5f228243916a2ec50be7811b4333b35"> 40</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcaf5f228243916a2ec50be7811b4333b35">BOOLEXTRACT</a>,</div>
<div class="line"><a name="l00041"></a><span class="lineno"> 41</span> </div>
<div class="line"><a name="l00042"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca0b5ff0bbde7799993800f6c939ba49ef"> 42</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca0b5ff0bbde7799993800f6c939ba49ef">LEFTSHIFT</a>,</div>
<div class="line"><a name="l00043"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca39394266637ae52dc7232657e036af7a"> 43</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca39394266637ae52dc7232657e036af7a">CONST_WIDTH_LEFTSHIFT</a>,</div>
<div class="line"><a name="l00044"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcad66141e84453a3bae5d9d16f45d25d69"> 44</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcad66141e84453a3bae5d9d16f45d25d69">RIGHTSHIFT</a>,</div>
<div class="line"><a name="l00045"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca735ca3566cb9f10aa58f458889f4ddf4"> 45</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca735ca3566cb9f10aa58f458889f4ddf4">BVSHL</a>,</div>
<div class="line"><a name="l00046"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca7e306d4cb1a779347c5a2d69a56a5e71"> 46</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca7e306d4cb1a779347c5a2d69a56a5e71">BVLSHR</a>,</div>
<div class="line"><a name="l00047"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcac054f57234914470a3912e118222bbf5"> 47</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcac054f57234914470a3912e118222bbf5">BVASHR</a>,</div>
<div class="line"><a name="l00048"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca09caf9735c580d393b24bbcca2b60e12"> 48</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca09caf9735c580d393b24bbcca2b60e12">SX</a>,</div>
<div class="line"><a name="l00049"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca553ee15794ea4c75c21083a98f3abd9b"> 49</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca553ee15794ea4c75c21083a98f3abd9b">BVREPEAT</a>,</div>
<div class="line"><a name="l00050"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca393b289a4d8d97ba38fd9b0c82a64898"> 50</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca393b289a4d8d97ba38fd9b0c82a64898">BVZEROEXTEND</a>,</div>
<div class="line"><a name="l00051"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca180d8bac8397070ad5f0cab720858344"> 51</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca180d8bac8397070ad5f0cab720858344">BVROTL</a>,</div>
<div class="line"><a name="l00052"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca3bff45238e2f6e14081dd415d2bb409c"> 52</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca3bff45238e2f6e14081dd415d2bb409c">BVROTR</a>,</div>
<div class="line"><a name="l00053"></a><span class="lineno"> 53</span> </div>
<div class="line"><a name="l00054"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca033f8fb5d6777b4ca308522fe7c76abb"> 54</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca033f8fb5d6777b4ca308522fe7c76abb">BVAND</a>,</div>
<div class="line"><a name="l00055"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca0e7e1228034ad7003dc056893d4c683d"> 55</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca0e7e1228034ad7003dc056893d4c683d">BVOR</a>,</div>
<div class="line"><a name="l00056"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca13c4820e7aec8491475ebaca63c2ac0f"> 56</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca13c4820e7aec8491475ebaca63c2ac0f">BVXOR</a>,</div>
<div class="line"><a name="l00057"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcadca4a599a0fbc8bd38015e1714835fca"> 57</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcadca4a599a0fbc8bd38015e1714835fca">BVXNOR</a>,</div>
<div class="line"><a name="l00058"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcabe80cab40347b0ecf95be77d5bd7e8d9"> 58</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcabe80cab40347b0ecf95be77d5bd7e8d9">BVNEG</a>,</div>
<div class="line"><a name="l00059"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcab9d728d7dca301dd67d31ac302b2ed79"> 59</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcab9d728d7dca301dd67d31ac302b2ed79">BVNAND</a>,</div>
<div class="line"><a name="l00060"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcaf68c2ecf7cf6b63a8a50b468126550e3"> 60</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcaf68c2ecf7cf6b63a8a50b468126550e3">BVNOR</a>,</div>
<div class="line"><a name="l00061"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcaabff4c1f69d99fc6e230cc1d65aef18d"> 61</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcaabff4c1f69d99fc6e230cc1d65aef18d">BVCOMP</a>,</div>
<div class="line"><a name="l00062"></a><span class="lineno"> 62</span> </div>
<div class="line"><a name="l00063"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcafa8dfe3523dc0fd7eb200b12d9f8bb37"> 63</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcafa8dfe3523dc0fd7eb200b12d9f8bb37">BVUMINUS</a>,</div>
<div class="line"><a name="l00064"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcac41c4f67403afc67e2866787a6fc156e"> 64</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcac41c4f67403afc67e2866787a6fc156e">BVPLUS</a>,</div>
<div class="line"><a name="l00065"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca6a9467df1bf864d4d635322e43b497e8"> 65</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca6a9467df1bf864d4d635322e43b497e8">BVSUB</a>,</div>
<div class="line"><a name="l00066"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca3732a31c60803ee2918ba1999788ba39"> 66</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca3732a31c60803ee2918ba1999788ba39">BVMULT</a>,</div>
<div class="line"><a name="l00067"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca8a1bdb340fa2cb36921bf0ec284eb3fd"> 67</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca8a1bdb340fa2cb36921bf0ec284eb3fd">BVUDIV</a>,</div>
<div class="line"><a name="l00068"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca1938c4fc956ace5916c7b4bb462f0d6d"> 68</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca1938c4fc956ace5916c7b4bb462f0d6d">BVSDIV</a>,</div>
<div class="line"><a name="l00069"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca10b7e4b5dd07687faef4110b6dd7b069"> 69</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca10b7e4b5dd07687faef4110b6dd7b069">BVUREM</a>,</div>
<div class="line"><a name="l00070"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca31092d607cf44eb879d517e309e994e9"> 70</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca31092d607cf44eb879d517e309e994e9">BVSREM</a>,</div>
<div class="line"><a name="l00071"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcac53836c6cf69b0b07b11dde75dad1e71"> 71</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcac53836c6cf69b0b07b11dde75dad1e71">BVSMOD</a>,</div>
<div class="line"><a name="l00072"></a><span class="lineno"> 72</span> </div>
<div class="line"><a name="l00073"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca92c5ef9334e513d99b62c8d04c60ad20"> 73</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca92c5ef9334e513d99b62c8d04c60ad20">BVLT</a>,</div>
<div class="line"><a name="l00074"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca0c2b1488f08f5cd06a50c41e638c1620"> 74</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca0c2b1488f08f5cd06a50c41e638c1620">BVLE</a>,</div>
<div class="line"><a name="l00075"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca2474c46c07b6bbe632a473c5fe35666b"> 75</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca2474c46c07b6bbe632a473c5fe35666b">BVGT</a>,</div>
<div class="line"><a name="l00076"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca11ee3d8aed0361c47f9b330e89a9cacc"> 76</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca11ee3d8aed0361c47f9b330e89a9cacc">BVGE</a>,</div>
<div class="line"><a name="l00077"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca49ad286bf8b76cfbf1684e550536cd5a"> 77</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca49ad286bf8b76cfbf1684e550536cd5a">BVSLT</a>,</div>
<div class="line"><a name="l00078"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca0c78fcb723d5a706cfe6372e7c09b04c"> 78</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca0c78fcb723d5a706cfe6372e7c09b04c">BVSLE</a>,</div>
<div class="line"><a name="l00079"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca4e6a6d18a93b5e91a53de75a4787a014"> 79</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca4e6a6d18a93b5e91a53de75a4787a014">BVSGT</a>,</div>
<div class="line"><a name="l00080"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca01ff0bd050c25dea70aed8413846c2cb"> 80</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca01ff0bd050c25dea70aed8413846c2cb">BVSGE</a>,</div>
<div class="line"><a name="l00081"></a><span class="lineno"> 81</span> </div>
<div class="line"><a name="l00082"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca2c57965432c2e15e6c26475bf1328b51"> 82</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca2c57965432c2e15e6c26475bf1328b51">INTTOBV</a>, <span class="comment">// Not implemented yet</span></div>
<div class="line"><a name="l00083"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca4c3b0b6c64b82b45ec2eb80770c37cf2"> 83</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca4c3b0b6c64b82b45ec2eb80770c37cf2">BVTOINT</a>, <span class="comment">// Not implemented yet</span></div>
<div class="line"><a name="l00084"></a><span class="lineno"> 84</span>  <span class="comment">// A wrapper for delaying the construction of type predicates</span></div>
<div class="line"><a name="l00085"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcab15d7022f2ee4f2511256d8be02ea6b3"> 85</a></span>  <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcab15d7022f2ee4f2511256d8be02ea6b3">BVTYPEPRED</a></div>
<div class="line"><a name="l00086"></a><span class="lineno"> 86</span>  } <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fc">BVKinds</a>;</div>
<div class="line"><a name="l00087"></a><span class="lineno"> 87</span> </div>
<div class="line"><a name="l00088"></a><span class="lineno"> 88</span> <span class="comment">/*****************************************************************************/</span><span class="comment"></span></div>
<div class="line"><a name="l00089"></a><span class="lineno"> 89</span> <span class="comment">/*!</span></div>
<div class="line"><a name="l00090"></a><span class="lineno"> 90</span> <span class="comment"> *\class TheoryBitvector</span></div>
<div class="line"><a name="l00091"></a><span class="lineno"> 91</span> <span class="comment"> *\ingroup Theories</span></div>
<div class="line"><a name="l00092"></a><span class="lineno"> 92</span> <span class="comment"> *\brief Theory of bitvectors of known length \</span></div>
<div class="line"><a name="l00093"></a><span class="lineno"> 93</span> <span class="comment"> * (operations include: @,[i:j],[i],+,.,BVAND,BVNEG)</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"> * Author: Vijay Ganesh</span></div>
<div class="line"><a name="l00096"></a><span class="lineno"> 96</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00097"></a><span class="lineno"> 97</span> <span class="comment"> * Created:Wed May 5 15:35:07 PDT 2004</span></div>
<div class="line"><a name="l00098"></a><span class="lineno"> 98</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"><a class="code" href="classCVC3_1_1TheoryBitvector.html"> 100</a></span> <span class="keyword">class </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> :<span class="keyword">public</span> <a class="code" href="classCVC3_1_1Theory.html" title="Base class for theories.">Theory</a> {</div>
<div class="line"><a name="l00101"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#a36ce76cce9f4da02fe837fa6d99d6202"> 101</a></span>  <a class="code" href="classCVC3_1_1BitvectorProofRules.html">BitvectorProofRules</a>* <a class="code" href="classCVC3_1_1TheoryBitvector.html#a36ce76cce9f4da02fe837fa6d99d6202">d_rules</a>;<span class="comment"></span></div>
<div class="line"><a name="l00102"></a><span class="lineno"> 102</span> <span class="comment"> //! MemoryManager index for BVConstExpr subclass</span></div>
<div class="line"><a name="l00103"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#aca1d99fa896f29efa540d8b83a4de848"> 103</a></span> <span class="comment"></span> <span class="keywordtype">size_t</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#aca1d99fa896f29efa540d8b83a4de848" title="MemoryManager index for BVConstExpr subclass.">d_bvConstExprIndex</a>;</div>
<div class="line"><a name="l00104"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#a96840bd0a2349e2cd33345a709e84907"> 104</a></span>  <span class="keywordtype">size_t</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a96840bd0a2349e2cd33345a709e84907">d_bvPlusExprIndex</a>;</div>
<div class="line"><a name="l00105"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#a6d5488901e86cf3db3fc473fc3770766"> 105</a></span>  <span class="keywordtype">size_t</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a6d5488901e86cf3db3fc473fc3770766">d_bvParameterExprIndex</a>;</div>
<div class="line"><a name="l00106"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#ae58b98a947a495b8754413e336753518"> 106</a></span>  <span class="keywordtype">size_t</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#ae58b98a947a495b8754413e336753518">d_bvTypePredExprIndex</a>;</div>
<div class="line"><a name="l00107"></a><span class="lineno"> 107</span> <span class="comment"></span></div>
<div class="line"><a name="l00108"></a><span class="lineno"> 108</span> <span class="comment"> //! counts delayed asserted equalities</span></div>
<div class="line"><a name="l00109"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#af183050f385d720871a298207a7790b1"> 109</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1StatCounter.html">StatCounter</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#af183050f385d720871a298207a7790b1" title="counts delayed asserted equalities">d_bvDelayEq</a>;<span class="comment"></span></div>
<div class="line"><a name="l00110"></a><span class="lineno"> 110</span> <span class="comment"> //! counts asserted equalities</span></div>
<div class="line"><a name="l00111"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#ae855792c718e64c8a46dab88ddd8b1b4"> 111</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1StatCounter.html">StatCounter</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#ae855792c718e64c8a46dab88ddd8b1b4" title="counts asserted equalities">d_bvAssertEq</a>;<span class="comment"></span></div>
<div class="line"><a name="l00112"></a><span class="lineno"> 112</span> <span class="comment"> //! counts delayed asserted disequalities</span></div>
<div class="line"><a name="l00113"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#a563bcc4483ffa3aee6a8e44e5ab07bcd"> 113</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1StatCounter.html">StatCounter</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a563bcc4483ffa3aee6a8e44e5ab07bcd" title="counts delayed asserted disequalities">d_bvDelayDiseq</a>;<span class="comment"></span></div>
<div class="line"><a name="l00114"></a><span class="lineno"> 114</span> <span class="comment"> //! counts asserted disequalities</span></div>
<div class="line"><a name="l00115"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#a071fce068ccf6223f20ba8a8d5b90b00"> 115</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1StatCounter.html">StatCounter</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a071fce068ccf6223f20ba8a8d5b90b00" title="counts asserted disequalities">d_bvAssertDiseq</a>;<span class="comment"></span></div>
<div class="line"><a name="l00116"></a><span class="lineno"> 116</span> <span class="comment"> //! counts type predicates</span></div>
<div class="line"><a name="l00117"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#aac1428f779c77033eb5c59b599629cb8"> 117</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1StatCounter.html">StatCounter</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#aac1428f779c77033eb5c59b599629cb8" title="counts type predicates">d_bvTypePreds</a>;<span class="comment"></span></div>
<div class="line"><a name="l00118"></a><span class="lineno"> 118</span> <span class="comment"> //! counts delayed type predicates</span></div>
<div class="line"><a name="l00119"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#aefadf1146b79ded24d7f5a66adba069d"> 119</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1StatCounter.html">StatCounter</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#aefadf1146b79ded24d7f5a66adba069d" title="counts delayed type predicates">d_bvDelayTypePreds</a>;<span class="comment"></span></div>
<div class="line"><a name="l00120"></a><span class="lineno"> 120</span> <span class="comment"> //! counts bitblasted equalities</span></div>
<div class="line"><a name="l00121"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#aab7d49f889a88fd2373b722d33e21c31"> 121</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1StatCounter.html">StatCounter</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#aab7d49f889a88fd2373b722d33e21c31" title="counts bitblasted equalities">d_bvBitBlastEq</a>;<span class="comment"></span></div>
<div class="line"><a name="l00122"></a><span class="lineno"> 122</span> <span class="comment"> //! counts bitblasted disequalities</span></div>
<div class="line"><a name="l00123"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#a2f2ac7c248fe89fc483c3a1a43c459db"> 123</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1StatCounter.html">StatCounter</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a2f2ac7c248fe89fc483c3a1a43c459db" title="counts bitblasted disequalities">d_bvBitBlastDiseq</a>;</div>
<div class="line"><a name="l00124"></a><span class="lineno"> 124</span> <span class="comment"></span></div>
<div class="line"><a name="l00125"></a><span class="lineno"> 125</span> <span class="comment"> //! boolean on the fly rewrite flag</span></div>
<div class="line"><a name="l00126"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#a20f9ef1d8f1666eeb16e9f2712320132"> 126</a></span> <span class="comment"></span> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryBitvector.html#a20f9ef1d8f1666eeb16e9f2712320132" title="boolean on the fly rewrite flag">d_booleanRWFlag</a>;<span class="comment"></span></div>
<div class="line"><a name="l00127"></a><span class="lineno"> 127</span> <span class="comment"> //! bool extract cache flag</span></div>
<div class="line"><a name="l00128"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#aa96498fb323044a4ab77c9657ac8e614"> 128</a></span> <span class="comment"></span> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryBitvector.html#aa96498fb323044a4ab77c9657ac8e614" title="bool extract cache flag">d_boolExtractCacheFlag</a>;<span class="comment"></span></div>
<div class="line"><a name="l00129"></a><span class="lineno"> 129</span> <span class="comment"> //! flag which indicates that all arithmetic is 32 bit with no overflow</span></div>
<div class="line"><a name="l00130"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#ac219e3d5a18642506f3def182a023989"> 130</a></span> <span class="comment"></span> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryBitvector.html#ac219e3d5a18642506f3def182a023989" title="flag which indicates that all arithmetic is 32 bit with no overflow">d_bv32Flag</a>;</div>
<div class="line"><a name="l00131"></a><span class="lineno"> 131</span> <span class="comment"></span></div>
<div class="line"><a name="l00132"></a><span class="lineno"> 132</span> <span class="comment"> //! Cache for storing the results of the bitBlastTerm function</span></div>
<div class="line"><a name="l00133"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#a0f583ba86ce3c379097255ee97620652"> 133</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr,Theorem></a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a0f583ba86ce3c379097255ee97620652" title="Cache for storing the results of the bitBlastTerm function.">d_bitvecCache</a>;</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"> //! Cache for pushNegation(). it is ok that this is cache is</span></div>
<div class="line"><a name="l00136"></a><span class="lineno"> 136</span> <span class="comment"></span> <span class="comment">//ExprMap. it is cleared for each call of pushNegation. Does not add</span></div>
<div class="line"><a name="l00137"></a><span class="lineno"> 137</span>  <span class="comment">//value across calls of pushNegation</span></div>
<div class="line"><a name="l00138"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#a2134631ced4e2db4bafac7755a4774f4"> 138</a></span>  <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Theorem></a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a2134631ced4e2db4bafac7755a4774f4" title="Cache for pushNegation(). it is ok that this is cache is.">d_pushNegCache</a>;</div>
<div class="line"><a name="l00139"></a><span class="lineno"> 139</span> <span class="comment"></span></div>
<div class="line"><a name="l00140"></a><span class="lineno"> 140</span> <span class="comment"> //! Backtracking queue for equalities</span></div>
<div class="line"><a name="l00141"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#af8bcfa021f89dfbc8111eff923e48eab"> 141</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Theorem></a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#af8bcfa021f89dfbc8111eff923e48eab" title="Backtracking queue for equalities.">d_eq</a>;<span class="comment"></span></div>
<div class="line"><a name="l00142"></a><span class="lineno"> 142</span> <span class="comment"> //! Backtracking queue for unsolved equalities</span></div>
<div class="line"><a name="l00143"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#a7c8dcbb9ba2c1c307c403966cd0b0c6d"> 143</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Theorem></a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a7c8dcbb9ba2c1c307c403966cd0b0c6d" title="Backtracking queue for unsolved equalities.">d_eqPending</a>;<span class="comment"></span></div>
<div class="line"><a name="l00144"></a><span class="lineno"> 144</span> <span class="comment"> //! Index to current position in d_eqPending</span></div>
<div class="line"><a name="l00145"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#ac017443fdd0f931d9283bc9e2b52d831"> 145</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<unsigned int></a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#ac017443fdd0f931d9283bc9e2b52d831" title="Index to current position in d_eqPending.">d_eq_index</a>;<span class="comment"></span></div>
<div class="line"><a name="l00146"></a><span class="lineno"> 146</span> <span class="comment"> //! Backtracking queue for all other assertions</span></div>
<div class="line"><a name="l00147"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#ad133cd123c7cc462dbeca98a1d10f8e4"> 147</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Theorem></a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#ad133cd123c7cc462dbeca98a1d10f8e4" title="Backtracking queue for all other assertions.">d_bitblast</a>;<span class="comment"></span></div>
<div class="line"><a name="l00148"></a><span class="lineno"> 148</span> <span class="comment"> //! Index to current position in d_bitblast</span></div>
<div class="line"><a name="l00149"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#ad9f83106573a125c219c3900a9aeceb3"> 149</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<unsigned int></a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#ad9f83106573a125c219c3900a9aeceb3" title="Index to current position in d_bitblast.">d_bb_index</a>;<span class="comment"></span></div>
<div class="line"><a name="l00150"></a><span class="lineno"> 150</span> <span class="comment"> //! Backtracking database of subterms of shared terms</span></div>
<div class="line"><a name="l00151"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#aa899ef9e64b78453d199a84160f15444"> 151</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr,Expr></a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#aa899ef9e64b78453d199a84160f15444" title="Backtracking database of subterms of shared terms.">d_sharedSubterms</a>;<span class="comment"></span></div>
<div class="line"><a name="l00152"></a><span class="lineno"> 152</span> <span class="comment"> //! Backtracking database of subterms of shared terms</span></div>
<div class="line"><a name="l00153"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#a59850cd32a8031dff8e8918c1e9d31c7"> 153</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a59850cd32a8031dff8e8918c1e9d31c7" title="Backtracking database of subterms of shared terms.">d_sharedSubtermsList</a>;</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> <span class="comment"> //! Constant 1-bit bit-vector 0bin0</span></div>
<div class="line"><a name="l00156"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#a8be187368c2a0f4e0b401bc1c7968d19"> 156</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_1TheoryBitvector.html#a8be187368c2a0f4e0b401bc1c7968d19" title="Constant 1-bit bit-vector 0bin0.">d_bvZero</a>;<span class="comment"></span></div>
<div class="line"><a name="l00157"></a><span class="lineno"> 157</span> <span class="comment"> //! Constant 1-bit bit-vector 0bin0</span></div>
<div class="line"><a name="l00158"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#aa4228ded9a53f6edcc7d06406f9c98c7"> 158</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_1TheoryBitvector.html#aa4228ded9a53f6edcc7d06406f9c98c7" title="Constant 1-bit bit-vector 0bin0.">d_bvOne</a>;<span class="comment"></span></div>
<div class="line"><a name="l00159"></a><span class="lineno"> 159</span> <span class="comment"> //! Return cached constant 0bin0</span></div>
<div class="line"><a name="l00160"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#a2a6471d4278e92ffcaa981b39001fc8a"> 160</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_1TheoryBitvector.html#a2a6471d4278e92ffcaa981b39001fc8a" title="Return cached constant 0bin0.">bvZero</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a8be187368c2a0f4e0b401bc1c7968d19" title="Constant 1-bit bit-vector 0bin0.">d_bvZero</a>; }<span class="comment"></span></div>
<div class="line"><a name="l00161"></a><span class="lineno"> 161</span> <span class="comment"> //! Return cached constant 0bin1</span></div>
<div class="line"><a name="l00162"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#a3de9924e52bf35f61049f07f0d34529f"> 162</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_1TheoryBitvector.html#a3de9924e52bf35f61049f07f0d34529f" title="Return cached constant 0bin1.">bvOne</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#aa4228ded9a53f6edcc7d06406f9c98c7" title="Constant 1-bit bit-vector 0bin0.">d_bvOne</a>; }</div>
<div class="line"><a name="l00163"></a><span class="lineno"> 163</span> <span class="comment"></span></div>
<div class="line"><a name="l00164"></a><span class="lineno"> 164</span> <span class="comment"> //! Max size of any bitvector we've seen</span></div>
<div class="line"><a name="l00165"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#a1559e63e86e26b348ad8bb618f29f202"> 165</a></span> <span class="comment"></span> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a1559e63e86e26b348ad8bb618f29f202" title="Max size of any bitvector we've seen.">d_maxLength</a>;</div>
<div class="line"><a name="l00166"></a><span class="lineno"> 166</span> <span class="comment"></span></div>
<div class="line"><a name="l00167"></a><span class="lineno"> 167</span> <span class="comment"> //! Used in checkSat</span></div>
<div class="line"><a name="l00168"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#a8990b759675928a62a4d75cf69fe8d72"> 168</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<unsigned></a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a8990b759675928a62a4d75cf69fe8d72" title="Used in checkSat.">d_index1</a>;</div>
<div class="line"><a name="l00169"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#a2316b51cfa9b54740298ec7d5e6630cb"> 169</a></span>  <a class="code" href="classCVC3_1_1CDO.html">CDO<unsigned></a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a2316b51cfa9b54740298ec7d5e6630cb">d_index2</a>;</div>
<div class="line"><a name="l00170"></a><span class="lineno"> 170</span> <span class="comment"></span></div>
<div class="line"><a name="l00171"></a><span class="lineno"> 171</span> <span class="comment"> //! functions which implement the DP strategy for bitblasting</span></div>
<div class="line"><a name="l00172"></a><span class="lineno"> 172</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a85512d4fcaee0050ee2b41dedd71c61c" title="functions which implement the DP strategy for bitblasting">bitBlastEqn</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="l00173"></a><span class="lineno"> 173</span> <span class="comment"> //! bitblast disequation</span></div>
<div class="line"><a name="l00174"></a><span class="lineno"> 174</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#aa3c9c45c9989d45202d31dda4beb4386" title="bitblast disequation">bitBlastDisEqn</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& notE);<span class="comment"></span></div>
<div class="line"><a name="l00175"></a><span class="lineno"> 175</span> <span class="comment"> //! function which implements the DP strtagey to bitblast Inequations</span></div>
<div class="line"><a name="l00176"></a><span class="lineno"> 176</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a1381dbfdc07d3bdebe3a4b8f0172bb94" title="function which implements the DP strtagey to bitblast Inequations">bitBlastIneqn</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="l00177"></a><span class="lineno"> 177</span> <span class="comment"> //! functions which implement the DP strategy for bitblasting</span></div>
<div class="line"><a name="l00178"></a><span class="lineno"> 178</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a981e964dd8c6118cbcac5e0c2b307730" title="functions which implement the DP strategy for bitblasting">bitBlastTerm</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> bitPosition);</div>
<div class="line"><a name="l00179"></a><span class="lineno"> 179</span> </div>
<div class="line"><a name="l00180"></a><span class="lineno"> 180</span> <span class="comment">// //! strategy fucntions for BVPLUS NORMAL FORM</span></div>
<div class="line"><a name="l00181"></a><span class="lineno"> 181</span> <span class="comment">// Theorem padBVPlus(const Expr& e);</span></div>
<div class="line"><a name="l00182"></a><span class="lineno"> 182</span> <span class="comment">// //! strategy fucntions for BVPLUS NORMAL FORM</span></div>
<div class="line"><a name="l00183"></a><span class="lineno"> 183</span> <span class="comment">// Theorem flattenBVPlus(const Expr& e);</span></div>
<div class="line"><a name="l00184"></a><span class="lineno"> 184</span> </div>
<div class="line"><a name="l00185"></a><span class="lineno"> 185</span> <span class="comment">// //! Implementation of the concatenation normal form</span></div>
<div class="line"><a name="l00186"></a><span class="lineno"> 186</span> <span class="comment">// Theorem normalizeConcat(const Expr& e, bool useFind);</span></div>
<div class="line"><a name="l00187"></a><span class="lineno"> 187</span> <span class="comment">// //! Implementation of the n-bit arithmetic normal form</span></div>
<div class="line"><a name="l00188"></a><span class="lineno"> 188</span> <span class="comment">// Theorem normalizeBVArith(const Expr& e, bool useFind);</span></div>
<div class="line"><a name="l00189"></a><span class="lineno"> 189</span> <span class="comment">// //! Helper method for composing normalizations</span></div>
<div class="line"><a name="l00190"></a><span class="lineno"> 190</span> <span class="comment">// Theorem normalizeConcat(const Theorem& t, bool useFind) {</span></div>
<div class="line"><a name="l00191"></a><span class="lineno"> 191</span> <span class="comment">// return transitivityRule(t, normalizeConcat(t.getRHS(), useFind));</span></div>
<div class="line"><a name="l00192"></a><span class="lineno"> 192</span> <span class="comment">// }</span></div>
<div class="line"><a name="l00193"></a><span class="lineno"> 193</span> <span class="comment">// //! Helper method for composing normalizations</span></div>
<div class="line"><a name="l00194"></a><span class="lineno"> 194</span> <span class="comment">// Theorem normalizeBVArith(const Theorem& t, bool useFind) {</span></div>
<div class="line"><a name="l00195"></a><span class="lineno"> 195</span> <span class="comment">// return transitivityRule(t, normalizeBVArith(t.getRHS(), useFind));</span></div>
<div class="line"><a name="l00196"></a><span class="lineno"> 196</span> <span class="comment">// }</span></div>
<div class="line"><a name="l00197"></a><span class="lineno"> 197</span> </div>
<div class="line"><a name="l00198"></a><span class="lineno"> 198</span> <span class="comment">// Theorem signExtendBVLT(const Expr& e, int len, bool useFind);</span></div>
<div class="line"><a name="l00199"></a><span class="lineno"> 199</span> </div>
<div class="line"><a name="l00200"></a><span class="lineno"> 200</span>  <span class="keyword">public</span>:</div>
<div class="line"><a name="l00201"></a><span class="lineno"> 201</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a3f1ecbd3cea6637fe571cc8b614d3dd6">pushNegationRec</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="l00202"></a><span class="lineno"> 202</span>  <span class="keyword">private</span>:</div>
<div class="line"><a name="l00203"></a><span class="lineno"> 203</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#aa7cb7ed38abf46e12d63c019b694c793">pushNegation</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="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"> //! Top down simplifier</span></div>
<div class="line"><a name="l00206"></a><span class="lineno"> 206</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_1TheoryBitvector.html#a5bd75507801c5b8b2595784ce53069aa" title="Top down simplifier.">simplifyOp</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="l00207"></a><span class="lineno"> 207</span> <span class="comment"></span></div>
<div class="line"><a name="l00208"></a><span class="lineno"> 208</span> <span class="comment"> //! Internal rewrite method for constants</span></div>
<div class="line"><a name="l00209"></a><span class="lineno"> 209</span> <span class="comment"></span> <span class="comment">// Theorem rewriteConst(const Expr& e);</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> <span class="comment"> //! Main rewrite method (implements the actual rewrites)</span></div>
<div class="line"><a name="l00212"></a><span class="lineno"> 212</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a214442814e895d26ac43c42663741fbd" title="Internal rewrite method for constants.">rewriteBV</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<Theorem></a>& cache, <span class="keywordtype">int</span> n = 1);</div>
<div class="line"><a name="l00213"></a><span class="lineno"> 213</span> <span class="comment"></span></div>
<div class="line"><a name="l00214"></a><span class="lineno"> 214</span> <span class="comment"> //! Rewrite children 'n' levels down (n==1 means "only the top level")</span></div>
<div class="line"><a name="l00215"></a><span class="lineno"> 215</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a214442814e895d26ac43c42663741fbd" title="Internal rewrite method for constants.">rewriteBV</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> n = 1);</div>
<div class="line"><a name="l00216"></a><span class="lineno"> 216</span> </div>
<div class="line"><a name="l00217"></a><span class="lineno"> 217</span>  <span class="comment">// Shortcuts for theorems</span></div>
<div class="line"><a name="l00218"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#ad9b702d3659fbaab47960bce473608c8"> 218</a></span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#ad9b702d3659fbaab47960bce473608c8">rewriteBV</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t, <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Theorem></a>& cache, <span class="keywordtype">int</span> n = 1) {</div>
<div class="line"><a name="l00219"></a><span class="lineno"> 219</span>  <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Theory.html#a76f6507116e36f46dab074781fb9bf2d" title="(a1 == a2) & (a2 == a3) ==> (a1 == a3)">transitivityRule</a>(t, <a class="code" href="classCVC3_1_1TheoryBitvector.html#a214442814e895d26ac43c42663741fbd" title="Internal rewrite method for constants.">rewriteBV</a>(t.<a class="code" href="classCVC3_1_1Theorem.html#a97d957fcbf9094480851b1d2e5d3729f">getRHS</a>(), cache, n));</div>
<div class="line"><a name="l00220"></a><span class="lineno"> 220</span>  }</div>
<div class="line"><a name="l00221"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#a84f5fc78f3f36e213ea70ff307db9db8"> 221</a></span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a84f5fc78f3f36e213ea70ff307db9db8">rewriteBV</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t, <span class="keywordtype">int</span> n = 1) {</div>
<div class="line"><a name="l00222"></a><span class="lineno"> 222</span>  <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Theory.html#a76f6507116e36f46dab074781fb9bf2d" title="(a1 == a2) & (a2 == a3) ==> (a1 == a3)">transitivityRule</a>(t, <a class="code" href="classCVC3_1_1TheoryBitvector.html#a214442814e895d26ac43c42663741fbd" title="Internal rewrite method for constants.">rewriteBV</a>(t.<a class="code" href="classCVC3_1_1Theorem.html#a97d957fcbf9094480851b1d2e5d3729f">getRHS</a>(), n));</div>
<div class="line"><a name="l00223"></a><span class="lineno"> 223</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> <span class="comment"> //! rewrite input boolean expression e to a simpler form</span></div>
<div class="line"><a name="l00226"></a><span class="lineno"> 226</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#ac2ed14005bb197aaad28ead0cb537a72" title="rewrite input boolean expression e to a simpler form">rewriteBoolean</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="l00227"></a><span class="lineno"> 227</span> </div>
<div class="line"><a name="l00228"></a><span class="lineno"> 228</span> <span class="comment">/*Beginning of Lorenzo PLatania's methods*/</span></div>
<div class="line"><a name="l00229"></a><span class="lineno"> 229</span> </div>
<div class="line"><a name="l00230"></a><span class="lineno"> 230</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a265761c739bb7084fa9016e527499da5">multiply_coeff</a>( <a class="code" href="classCVC3_1_1Rational.html">Rational</a> mult_inv, <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="l00231"></a><span class="lineno"> 231</span> </div>
<div class="line"><a name="l00232"></a><span class="lineno"> 232</span>  <span class="comment">// extract the min value from a Rational list</span></div>
<div class="line"><a name="l00233"></a><span class="lineno"> 233</span>  <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#ab4f87aca710aa31e6d438e91301beffc">min</a>(std::vector<Rational> list);</div>
<div class="line"><a name="l00234"></a><span class="lineno"> 234</span> </div>
<div class="line"><a name="l00235"></a><span class="lineno"> 235</span>  <span class="comment">// evaluates the gcd of two integer coefficients</span></div>
<div class="line"><a name="l00236"></a><span class="lineno"> 236</span>  <span class="comment">// int gcd(int c1, int c2);</span></div>
<div class="line"><a name="l00237"></a><span class="lineno"> 237</span> </div>
<div class="line"><a name="l00238"></a><span class="lineno"> 238</span>  <span class="comment">// converts a bv constant to an integer</span></div>
<div class="line"><a name="l00239"></a><span class="lineno"> 239</span>  <span class="comment">// int bv2int(const Expr& e);</span></div>
<div class="line"><a name="l00240"></a><span class="lineno"> 240</span> </div>
<div class="line"><a name="l00241"></a><span class="lineno"> 241</span>  <span class="comment">// return the odd coefficient of a leaf for which we can solve the</span></div>
<div class="line"><a name="l00242"></a><span class="lineno"> 242</span>  <span class="comment">// equation, or zero if no one has been found</span></div>
<div class="line"><a name="l00243"></a><span class="lineno"> 243</span>  <a class="code" href="classCVC3_1_1Rational.html">Rational</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a2e23b49398256989b0dea88a63717dee">Odd_coeff</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="l00244"></a><span class="lineno"> 244</span> </div>
<div class="line"><a name="l00245"></a><span class="lineno"> 245</span> </div>
<div class="line"><a name="l00246"></a><span class="lineno"> 246</span> </div>
<div class="line"><a name="l00247"></a><span class="lineno"> 247</span>  <span class="comment">// returns 1 if e is a linear term</span></div>
<div class="line"><a name="l00248"></a><span class="lineno"> 248</span>  <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#aa1e382d50ad48fb6d222450d74dd9574">check_linear</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="l00249"></a><span class="lineno"> 249</span> </div>
<div class="line"><a name="l00250"></a><span class="lineno"> 250</span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a6739a946f5cdf86bd6597845b6f6df43">isTermIn</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e2);</div>
<div class="line"><a name="l00251"></a><span class="lineno"> 251</span> </div>
<div class="line"><a name="l00252"></a><span class="lineno"> 252</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#aa12fe04ae2312b60f15f5fc594d533f4">updateSubterms</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& d );</div>
<div class="line"><a name="l00253"></a><span class="lineno"> 253</span> </div>
<div class="line"><a name="l00254"></a><span class="lineno"> 254</span>  <span class="comment">// returns how many times "term" appears in "e"</span></div>
<div class="line"><a name="l00255"></a><span class="lineno"> 255</span>  <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a79967704ae23c653a04a1ee3416a4d22">countTermIn</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& term, <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="l00256"></a><span class="lineno"> 256</span> </div>
<div class="line"><a name="l00257"></a><span class="lineno"> 257</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a324d4171cfb81ff5e774cbc326aaa1d9">simplifyPendingEq</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm, <span class="keywordtype">int</span> maxEffort);</div>
<div class="line"><a name="l00258"></a><span class="lineno"> 258</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a0dedc2d6930e49cdf4d73c40da7a7bd8">generalBitBlast</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm );</div>
<div class="line"><a name="l00259"></a><span class="lineno"> 259</span> <span class="comment">/*End of Lorenzo PLatania's methods*/</span></div>
<div class="line"><a name="l00260"></a><span class="lineno"> 260</span> </div>
<div class="line"><a name="l00261"></a><span class="lineno"> 261</span>  <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& <a class="code" href="classCVC3_1_1TheoryBitvector.html#abd70b8a3ad35dcf7299c87ab36a6f848">printSmtLibShared</a>(<a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& os, <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="l00262"></a><span class="lineno"> 262</span> </div>
<div class="line"><a name="l00263"></a><span class="lineno"> 263</span> <span class="keyword">public</span>:</div>
<div class="line"><a name="l00264"></a><span class="lineno"> 264</span>  <a class="code" href="classCVC3_1_1TheoryBitvector.html#ac45c989f0c26d78a8de812f2123cd262">TheoryBitvector</a>(<a class="code" href="classCVC3_1_1TheoryCore.html" title="This theory handles the built-in logical connectives plus equality. It also handles the registration ...">TheoryCore</a>* core);</div>
<div class="line"><a name="l00265"></a><span class="lineno"> 265</span>  <a class="code" href="classCVC3_1_1TheoryBitvector.html#a665042c64606705b935ac0ab15119266">~TheoryBitvector</a>();</div>
<div class="line"><a name="l00266"></a><span class="lineno"> 266</span> </div>
<div class="line"><a name="l00267"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#a2508ac260570adfa5584847830806cb0"> 267</a></span>  <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a2508ac260570adfa5584847830806cb0">d_bvPlusCarryCacheLeftBV</a>;</div>
<div class="line"><a name="l00268"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#a9fcf8c7246955aa2a8aa6be2fd3d4f64"> 268</a></span>  <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a9fcf8c7246955aa2a8aa6be2fd3d4f64">d_bvPlusCarryCacheRightBV</a>;</div>
<div class="line"><a name="l00269"></a><span class="lineno"> 269</span> </div>
<div class="line"><a name="l00270"></a><span class="lineno"> 270</span>  <span class="comment">// Trusted method that creates the proof rules class (used in constructor).</span></div>
<div class="line"><a name="l00271"></a><span class="lineno"> 271</span>  <span class="comment">// Implemented in bitvector_theorem_producer.cpp</span></div>
<div class="line"><a name="l00272"></a><span class="lineno"> 272</span>  <a class="code" href="classCVC3_1_1BitvectorProofRules.html">BitvectorProofRules</a>* <a class="code" href="classCVC3_1_1TheoryBitvector.html#ae3141bc37e39e3379fa71d966c887426">createProofRules</a>();</div>
<div class="line"><a name="l00273"></a><span class="lineno"> 273</span> </div>
<div class="line"><a name="l00274"></a><span class="lineno"> 274</span>  <span class="comment">// Theory interface</span></div>
<div class="line"><a name="l00275"></a><span class="lineno"> 275</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a3798dbe1339c1c376b35172fbbc6434b" title="Notify theory of a new shared term.">addSharedTerm</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="l00276"></a><span class="lineno"> 276</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a70eefd32e475f3c04e195530145ae87f" title="Assert a new fact to the decision procedure.">assertFact</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e);</div>
<div class="line"><a name="l00277"></a><span class="lineno"> 277</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#ac59b9ef8d3c7f68eee6a06ea17e3d104" title="Receives all the type predicates for the types of the given theory.">assertTypePred</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_1Theorem.html">Theorem</a>& pred);</div>
<div class="line"><a name="l00278"></a><span class="lineno"> 278</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a31df7eb073302681dd7aeedc57251d09" title="Check for satisfiability in the theory.">checkSat</a>(<span class="keywordtype">bool</span> fullEffort);</div>
<div class="line"><a name="l00279"></a><span class="lineno"> 279</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a82d63a41524830f12abe05b948eab4ca" title="Theory-specific rewrite rules.">rewrite</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="l00280"></a><span class="lineno"> 280</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a55e7711ed3e5be41dd7aca955a9ecc7a" title="Theory-specific rewrites for atomic formulas.">rewriteAtomic</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="l00281"></a><span class="lineno"> 281</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a1e7b1123d64a52db1e306942ff4576a3" title="Set up the term e for call-backs when e or its children change.">setup</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="l00282"></a><span class="lineno"> 282</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a57edac7a7e4ffd04e778f3858a000457" title="Notify a theory of a new equality.">update</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>& d);</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_1TheoryBitvector.html#a2a6ec855d488ee1d662ac0d1268d2392" title="An optional solver.">solve</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e);</div>
<div class="line"><a name="l00284"></a><span class="lineno"> 284</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a978cfa4add608e7f78c4e8b1d92e093f" title="Check that e is a valid Type expr.">checkType</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="l00285"></a><span class="lineno"> 285</span>  <a class="code" href="namespaceCVC3.html#af969e724f8b7016909f5804e8cea3e54" title="Enum for cardinality of types.">Cardinality</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#acc1ac9f10d2c91f9831057937fcba829" title="Compute information related to finiteness of types.">finiteTypeInfo</a>(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a>& n,</div>
<div class="line"><a name="l00286"></a><span class="lineno"> 286</span>  <span class="keywordtype">bool</span> enumerate, <span class="keywordtype">bool</span> computeSize);</div>
<div class="line"><a name="l00287"></a><span class="lineno"> 287</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#aad271001191bdd48d1b77d92d9558136" title="Compute and store the type of e.">computeType</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="l00288"></a><span class="lineno"> 288</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a38b5fc9c8e39309a86634cc55ee116a0" title="Add variables from 'e' to 'v' for constructing a concrete model.">computeModelTerm</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, std::vector<Expr>& v);</div>
<div class="line"><a name="l00289"></a><span class="lineno"> 289</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a00182685c0c766dfdc560e3c5f00001b" title="Compute the value of a compound variable from the more primitive ones.">computeModel</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, std::vector<Expr>& vars);</div>
<div class="line"><a name="l00290"></a><span class="lineno"> 290</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a60d5dc6f4f252bbf62e9333134863da0" title="Theory specific computation of the subtyping predicate for type t applied to the expression e...">computeTypePred</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& t, <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="l00291"></a><span class="lineno"> 291</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a94d82875db6689ca7c986e24abf63a46" title="Compute and cache the TCC of e.">computeTCC</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="l00292"></a><span class="lineno"> 292</span>  <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& <a class="code" href="classCVC3_1_1TheoryBitvector.html#aaa3c5b6fc08db3e297e811f4c9c18a17" title="Theory-specific pretty-printing.">print</a>(<a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& os, <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="l00293"></a><span class="lineno"> 293</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a8bf0677921ceebd416aa6208b56467eb" title="Theory-specific parsing implemented by the DP.">parseExprOp</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="l00294"></a><span class="lineno"> 294</span> </div>
<div class="line"><a name="l00295"></a><span class="lineno"> 295</span>  <span class="comment">//helper functions</span></div>
<div class="line"><a name="l00296"></a><span class="lineno"> 296</span> <span class="comment"></span></div>
<div class="line"><a name="l00297"></a><span class="lineno"> 297</span> <span class="comment"> //! Return the number of bits in the bitvector expression</span></div>
<div class="line"><a name="l00298"></a><span class="lineno"> 298</span> <span class="comment"></span> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#adce40eaced94554fd76d2f660f5ba385" title="Return the number of bits in the bitvector expression.">BVSize</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="l00299"></a><span class="lineno"> 299</span> </div>
<div class="line"><a name="l00300"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#ac88ba0954e217df731ebb362135ea107"> 300</a></span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#ac88ba0954e217df731ebb362135ea107">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_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e" title="Access to ExprManager.">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga18423a42ce6557dc33287d3979ccc3c6">newRatExpr</a>(r); }<span class="comment"></span></div>
<div class="line"><a name="l00301"></a><span class="lineno"> 301</span> <span class="comment"> //!pads e to be of length len</span></div>
<div class="line"><a name="l00302"></a><span class="lineno"> 302</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_1TheoryBitvector.html#aaa3c1d517c610706a066e7adfee9a6f6" title="pads e to be of length len">pad</a>(<span class="keywordtype">int</span> len, <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="l00303"></a><span class="lineno"> 303</span> </div>
<div class="line"><a name="l00304"></a><span class="lineno"> 304</span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a1bf151ceda29668de133a3b005b9298b">comparebv</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e2);</div>
<div class="line"><a name="l00305"></a><span class="lineno"> 305</span> </div>
<div class="line"><a name="l00306"></a><span class="lineno"> 306</span>  <span class="comment">//helper functions: functions to construct exprs</span></div>
<div class="line"><a name="l00307"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#a3d98cac1ae52614ee2adc3fbc407516e"> 307</a></span>  <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a3d98cac1ae52614ee2adc3fbc407516e">newBitvectorType</a>(<span class="keywordtype">int</span> i)</div>
<div class="line"><a name="l00308"></a><span class="lineno"> 308</span>  { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#aef4eb029a55a6822baa7c381262154e5">newBitvectorTypeExpr</a>(i); }</div>
<div class="line"><a name="l00309"></a><span class="lineno"> 309</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#ad2f823cf9921323e80c510076dd20fa2">newBitvectorTypePred</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& t, <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="l00310"></a><span class="lineno"> 310</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#aef4eb029a55a6822baa7c381262154e5">newBitvectorTypeExpr</a>(<span class="keywordtype">int</span> i);</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_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#ab22dd0ad8596f8fefce18f99b1791499">newBVAndExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);</div>
<div class="line"><a name="l00313"></a><span class="lineno"> 313</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#ab22dd0ad8596f8fefce18f99b1791499">newBVAndExpr</a>(<span class="keyword">const</span> std::vector<Expr>& kids);</div>
<div class="line"><a name="l00314"></a><span class="lineno"> 314</span> </div>
<div class="line"><a name="l00315"></a><span class="lineno"> 315</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a7b93b348dffe055b771db6061446e9ea">newBVOrExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);</div>
<div class="line"><a name="l00316"></a><span class="lineno"> 316</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a7b93b348dffe055b771db6061446e9ea">newBVOrExpr</a>(<span class="keyword">const</span> std::vector<Expr>& kids);</div>
<div class="line"><a name="l00317"></a><span class="lineno"> 317</span> </div>
<div class="line"><a name="l00318"></a><span class="lineno"> 318</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a003f69e1199d0a57102dadc83643fb18">newBVXorExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);</div>
<div class="line"><a name="l00319"></a><span class="lineno"> 319</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a003f69e1199d0a57102dadc83643fb18">newBVXorExpr</a>(<span class="keyword">const</span> std::vector<Expr>& kids);</div>
<div class="line"><a name="l00320"></a><span class="lineno"> 320</span> </div>
<div class="line"><a name="l00321"></a><span class="lineno"> 321</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#ad25d43520383b198f379d573cf72d784">newBVXnorExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);</div>
<div class="line"><a name="l00322"></a><span class="lineno"> 322</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#ad25d43520383b198f379d573cf72d784">newBVXnorExpr</a>(<span class="keyword">const</span> std::vector<Expr>& kids);</div>
<div class="line"><a name="l00323"></a><span class="lineno"> 323</span> </div>
<div class="line"><a name="l00324"></a><span class="lineno"> 324</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a9a3678f2c6007c5b492017b0d9161a37">newBVNandExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);</div>
<div class="line"><a name="l00325"></a><span class="lineno"> 325</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#ac7a7ef0271a8aa043ec09684e6a16e9b">newBVNorExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);</div>
<div class="line"><a name="l00326"></a><span class="lineno"> 326</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a70d9bf0184ba1308434780a25439b402">newBVCompExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);</div>
<div class="line"><a name="l00327"></a><span class="lineno"> 327</span> </div>
<div class="line"><a name="l00328"></a><span class="lineno"> 328</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#aa849a2fd56e8a1e3a7742b00d043869a">newBVLTExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);</div>
<div class="line"><a name="l00329"></a><span class="lineno"> 329</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#ac6430938332eb644c11106ce5047825c">newBVLEExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);</div>
<div class="line"><a name="l00330"></a><span class="lineno"> 330</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#aed210d6f5ea81db87debb15b422ded2c">newSXExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keywordtype">int</span> len);</div>
<div class="line"><a name="l00331"></a><span class="lineno"> 331</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a48a5a14c9e1efc9bc1d463d1be67fb1a">newBVIndexExpr</a>(<span class="keywordtype">int</span> kind, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keywordtype">int</span> len);</div>
<div class="line"><a name="l00332"></a><span class="lineno"> 332</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a2639e4a3d2b13f9e370daf41a833267c">newBVSLTExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);</div>
<div class="line"><a name="l00333"></a><span class="lineno"> 333</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a9b32f54063dda6c3424a63e1702cd277">newBVSLEExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);</div>
<div class="line"><a name="l00334"></a><span class="lineno"> 334</span> </div>
<div class="line"><a name="l00335"></a><span class="lineno"> 335</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a4bc6d752b2ba293481468dcaaa821d3f">newBVNegExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1);</div>
<div class="line"><a name="l00336"></a><span class="lineno"> 336</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a7113c95ecf45006003eed0d8d7dccda7">newBVUminusExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1);</div>
<div class="line"><a name="l00337"></a><span class="lineno"> 337</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#aec57b42edc8ea39452039be2d93a26e7">newBoolExtractExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keywordtype">int</span> r);</div>
<div class="line"><a name="l00338"></a><span class="lineno"> 338</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#ae1559a54104ab7befb00c9a14b5ea95e">newFixedLeftShiftExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keywordtype">int</span> r);</div>
<div class="line"><a name="l00339"></a><span class="lineno"> 339</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a082d2161d7c59fcbac262e3d3ddc93a3">newFixedConstWidthLeftShiftExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keywordtype">int</span> r);</div>
<div class="line"><a name="l00340"></a><span class="lineno"> 340</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a4cb4f4e7d854ca0c7d5883208de4355c">newFixedRightShiftExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keywordtype">int</span> r);</div>
<div class="line"><a name="l00341"></a><span class="lineno"> 341</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#aa34c7ab071175e4375822e6f1d47fe0d">newConcatExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);</div>
<div class="line"><a name="l00342"></a><span class="lineno"> 342</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#aa34c7ab071175e4375822e6f1d47fe0d">newConcatExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t3);</div>
<div class="line"><a name="l00343"></a><span class="lineno"> 343</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#aa34c7ab071175e4375822e6f1d47fe0d">newConcatExpr</a>(<span class="keyword">const</span> std::vector<Expr>& kids);</div>
<div class="line"><a name="l00344"></a><span class="lineno"> 344</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a352c6547a3a7fba398cdd2b2ea391b22">newBVConstExpr</a>(<span class="keyword">const</span> std::string& s, <span class="keywordtype">int</span> base = 2);</div>
<div class="line"><a name="l00345"></a><span class="lineno"> 345</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a352c6547a3a7fba398cdd2b2ea391b22">newBVConstExpr</a>(<span class="keyword">const</span> std::vector<bool>& bits);</div>
<div class="line"><a name="l00346"></a><span class="lineno"> 346</span>  <span class="comment">// Lorenzo's wrapper</span></div>
<div class="line"><a name="l00347"></a><span class="lineno"> 347</span>  <span class="comment">// as computeBVConst can not give the BV expr of a negative rational,</span></div>
<div class="line"><a name="l00348"></a><span class="lineno"> 348</span>  <span class="comment">// I use this wrapper to do that</span></div>
<div class="line"><a name="l00349"></a><span class="lineno"> 349</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#ae2a5085da47f7b62ed4cb5a312bd9fb3">signed_newBVConstExpr</a>( <a class="code" href="classCVC3_1_1Rational.html">Rational</a> c, <span class="keywordtype">int</span> bv_size);</div>
<div class="line"><a name="l00350"></a><span class="lineno"> 350</span>  <span class="comment">// end of Lorenzo's wrapper</span></div>
<div class="line"><a name="l00351"></a><span class="lineno"> 351</span> </div>
<div class="line"><a name="l00352"></a><span class="lineno"> 352</span>  <span class="comment">// Construct BVCONST of length 'len', or the min. needed length when len=0.</span></div>
<div class="line"><a name="l00353"></a><span class="lineno"> 353</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a352c6547a3a7fba398cdd2b2ea391b22">newBVConstExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Rational.html">Rational</a>& r, <span class="keywordtype">int</span> len = 0);</div>
<div class="line"><a name="l00354"></a><span class="lineno"> 354</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#aedd220a3f14097d52b80576cdc7b73ec" title="produces a string of 0's of length bvLength">newBVZeroString</a>(<span class="keywordtype">int</span> r);</div>
<div class="line"><a name="l00355"></a><span class="lineno"> 355</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a7e33736866d0752cdd551dd0059ca1bd" title="produces a string of 1's of length bvLength">newBVOneString</a>(<span class="keywordtype">int</span> r);<span class="comment"></span></div>
<div class="line"><a name="l00356"></a><span class="lineno"> 356</span> <span class="comment"> //! hi and low are bit indices</span></div>
<div class="line"><a name="l00357"></a><span class="lineno"> 357</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_1TheoryBitvector.html#a17a104b42804d41d9a11d15faf727166" title="hi and low are bit indices">newBVExtractExpr</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="l00358"></a><span class="lineno"> 358</span>  <span class="keywordtype">int</span> hi, <span class="keywordtype">int</span> low);</div>
<div class="line"><a name="l00359"></a><span class="lineno"> 359</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#af77dddbf974d441cf61294922be53739">newBVSubExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);<span class="comment"></span></div>
<div class="line"><a name="l00360"></a><span class="lineno"> 360</span> <span class="comment"> //! 'numbits' is the number of bits in the result</span></div>
<div class="line"><a name="l00361"></a><span class="lineno"> 361</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_1TheoryBitvector.html#ac8e00bf8c66a041e12326e09c4d369ad" title="'numbits' is the number of bits in the result">newBVPlusExpr</a>(<span class="keywordtype">int</span> numbits, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& k1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& k2);<span class="comment"></span></div>
<div class="line"><a name="l00362"></a><span class="lineno"> 362</span> <span class="comment"> //! 'numbits' is the number of bits in the result</span></div>
<div class="line"><a name="l00363"></a><span class="lineno"> 363</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_1TheoryBitvector.html#ac8e00bf8c66a041e12326e09c4d369ad" title="'numbits' is the number of bits in the result">newBVPlusExpr</a>(<span class="keywordtype">int</span> numbits, <span class="keyword">const</span> std::vector<Expr>& k);<span class="comment"></span></div>
<div class="line"><a name="l00364"></a><span class="lineno"> 364</span> <span class="comment"> //! pads children and then builds plus expr</span></div>
<div class="line"><a name="l00365"></a><span class="lineno"> 365</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_1TheoryBitvector.html#a284ff4a222be9ceaa97387661c76b147" title="pads children and then builds plus expr">newBVPlusPadExpr</a>(<span class="keywordtype">int</span> bvLength, <span class="keyword">const</span> std::vector<Expr>& k);</div>
<div class="line"><a name="l00366"></a><span class="lineno"> 366</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#ae601c7122d288358c50df9e27bd5a9df">newBVMultExpr</a>(<span class="keywordtype">int</span> bvLength,</div>
<div class="line"><a name="l00367"></a><span class="lineno"> 367</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);</div>
<div class="line"><a name="l00368"></a><span class="lineno"> 368</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#ae601c7122d288358c50df9e27bd5a9df">newBVMultExpr</a>(<span class="keywordtype">int</span> bvLength, <span class="keyword">const</span> std::vector<Expr>& kids);</div>
<div class="line"><a name="l00369"></a><span class="lineno"> 369</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#ad27eceadd690e39ef8ad88881925ac0c">newBVMultPadExpr</a>(<span class="keywordtype">int</span> bvLength,</div>
<div class="line"><a name="l00370"></a><span class="lineno"> 370</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);</div>
<div class="line"><a name="l00371"></a><span class="lineno"> 371</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#ad27eceadd690e39ef8ad88881925ac0c">newBVMultPadExpr</a>(<span class="keywordtype">int</span> bvLength, <span class="keyword">const</span> std::vector<Expr>& kids);</div>
<div class="line"><a name="l00372"></a><span class="lineno"> 372</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a43b7fde20faf94ca0691c9c78f49983e">newBVUDivExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);</div>
<div class="line"><a name="l00373"></a><span class="lineno"> 373</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a32e681fc6dc959306710c880f83c95ba">newBVURemExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);</div>
<div class="line"><a name="l00374"></a><span class="lineno"> 374</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#aa17d7de309b676bac0454ae3dcecb38f">newBVSDivExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);</div>
<div class="line"><a name="l00375"></a><span class="lineno"> 375</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a751ed4d2b46020c65ace988d96633142">newBVSRemExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);</div>
<div class="line"><a name="l00376"></a><span class="lineno"> 376</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#ac520790da34aa971a9ee4044b112ae82">newBVSModExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);</div>
<div class="line"><a name="l00377"></a><span class="lineno"> 377</span> </div>
<div class="line"><a name="l00378"></a><span class="lineno"> 378</span>  <span class="comment">// Accessors for expression parameters</span></div>
<div class="line"><a name="l00379"></a><span class="lineno"> 379</span>  <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a8e2bf7866c94979dfed7031a81c2e002">getBitvectorTypeParam</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="l00380"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#a0d6c5357741846c314acfda3f93094a9"> 380</a></span>  <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a8e2bf7866c94979dfed7031a81c2e002">getBitvectorTypeParam</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& t)</div>
<div class="line"><a name="l00381"></a><span class="lineno"> 381</span>  { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a0d6c5357741846c314acfda3f93094a9">getBitvectorTypeParam</a>(t.<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>()); }</div>
<div class="line"><a name="l00382"></a><span class="lineno"> 382</span>  <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a697bd2ebc3d61f913039bf77bbdc3c51">getTypePredType</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& tp);</div>
<div class="line"><a name="l00383"></a><span class="lineno"> 383</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_1TheoryBitvector.html#a96385e1a741679ebbabe669b8ed4c5bf">getTypePredExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& tp);</div>
<div class="line"><a name="l00384"></a><span class="lineno"> 384</span>  <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a7737e8531a34515a5d27afcb23bb314e">getSXIndex</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="l00385"></a><span class="lineno"> 385</span>  <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a2b61f3705b8789f652ea688ef331344f">getBVIndex</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="l00386"></a><span class="lineno"> 386</span>  <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#aedf18fc1e6f9998ddaef98ab9273c2fb">getBoolExtractIndex</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="l00387"></a><span class="lineno"> 387</span>  <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#aafcc248e3361c69777cb1377a157db49">getFixedLeftShiftParam</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="l00388"></a><span class="lineno"> 388</span>  <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a801f0c6dd21ecfea0769abfcd7fd4b4e">getFixedRightShiftParam</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="l00389"></a><span class="lineno"> 389</span>  <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#ad714ab7be58b17f2c120afa117abd1fb">getExtractHi</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="l00390"></a><span class="lineno"> 390</span>  <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#acbb820488811e04eed17d85199498ae9">getExtractLow</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="l00391"></a><span class="lineno"> 391</span>  <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a67259e3d5f08972e6a157f167aab7023">getBVPlusParam</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="l00392"></a><span class="lineno"> 392</span>  <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a540b9b39838cb3c1b71925be3f5696fa">getBVMultParam</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="l00393"></a><span class="lineno"> 393</span> </div>
<div class="line"><a name="l00394"></a><span class="lineno"> 394</span>  <span class="keywordtype">unsigned</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a6d1c5d8e029a455d9bd058eb66c5cdc8">getBVConstSize</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="l00395"></a><span class="lineno"> 395</span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a242600edbc48857be8abbab8e74ed3be">getBVConstValue</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);<span class="comment"></span></div>
<div class="line"><a name="l00396"></a><span class="lineno"> 396</span> <span class="comment"> //!computes the integer value of a bitvector constant</span></div>
<div class="line"><a name="l00397"></a><span class="lineno"> 397</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Rational.html">Rational</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a08653884cd51197647ed006e5ae64332" title="computes the integer value of a bitvector constant">computeBVConst</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"> //!computes the integer value of ~c+1 or BVUMINUS(c)</span></div>
<div class="line"><a name="l00399"></a><span class="lineno"> 399</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Rational.html">Rational</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a9e49b77a0e80b7ba83bc77bb3a301c6b" title="computes the integer value of ~c+1 or BVUMINUS(c)">computeNegBVConst</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> </div>
<div class="line"><a name="l00401"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#af9b48795b632ce717e9f2149c99689fb"> 401</a></span>  <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#af9b48795b632ce717e9f2149c99689fb">getMaxSize</a>() { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a1559e63e86e26b348ad8bb618f29f202" title="Max size of any bitvector we've seen.">d_maxLength</a>; }</div>
<div class="line"><a name="l00402"></a><span class="lineno"> 402</span> </div>
<div class="line"><a name="l00403"></a><span class="lineno"> 403</span> <span class="comment">/*Beginning of Lorenzo PLatania's public methods*/</span></div>
<div class="line"><a name="l00404"></a><span class="lineno"> 404</span> </div>
<div class="line"><a name="l00405"></a><span class="lineno"> 405</span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#afe606418dd434c720ec6cbec5dab3c1c">isLinearTerm</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="l00406"></a><span class="lineno"> 406</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a670ab645c15606c0653cd265c5378b52">extract_vars</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, std::vector<Expr>& vars );</div>
<div class="line"><a name="l00407"></a><span class="lineno"> 407</span>  <span class="comment">// checks whether e can be solved in term</span></div>
<div class="line"><a name="l00408"></a><span class="lineno"> 408</span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a7d9bd17c1b561963bb05712071747090">canSolveFor</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& term, <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">// evaluates the multipicative inverse</span></div>
<div class="line"><a name="l00411"></a><span class="lineno"> 411</span>  <a class="code" href="classCVC3_1_1Rational.html">Rational</a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a425367b8c2d69e637c93742ab1ed2134">multiplicative_inverse</a>(<a class="code" href="classCVC3_1_1Rational.html">Rational</a> r, <span class="keywordtype">int</span> n_bits);</div>
<div class="line"><a name="l00412"></a><span class="lineno"> 412</span> </div>
<div class="line"><a name="l00413"></a><span class="lineno"> 413</span> </div>
<div class="line"><a name="l00414"></a><span class="lineno"> 414</span>  <span class="comment">/*End of Lorenzo PLatania's public methods*/</span></div>
<div class="line"><a name="l00415"></a><span class="lineno"> 415</span> </div>
<div class="line"><a name="l00416"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryBitvector.html#aa17e44a8047fc0f5220565f6cd5a203f"> 416</a></span>  std::vector<Theorem> <a class="code" href="classCVC3_1_1TheoryBitvector.html#aa17e44a8047fc0f5220565f6cd5a203f">additionalRewriteConstraints</a>;</div>
<div class="line"><a name="l00417"></a><span class="lineno"> 417</span> </div>
<div class="line"><a name="l00418"></a><span class="lineno"> 418</span> }; <span class="comment">//end of class TheoryBitvector</span></div>
<div class="line"><a name="l00419"></a><span class="lineno"> 419</span> </div>
<div class="line"><a name="l00420"></a><span class="lineno"> 420</span> </div>
<div class="line"><a name="l00421"></a><span class="lineno"> 421</span> }<span class="comment">//end of namespace CVC3</span></div>
<div class="line"><a name="l00422"></a><span class="lineno"> 422</span> <span class="preprocessor">#endif</span></div>
</div><!-- fragment --></div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:15 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>
