<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<title>CVC3: theory_bitvector.h Source File</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li><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 class="header">
<div class="headertitle">
<div class="title">theory_bitvector.h</div> </div>
</div>
<div class="contents">
<a href="theory__bitvector_8h.html">Go to the documentation of this file.</a><div class="fragment"><pre class="fragment"><a name="l00001"></a>00001 <span class="comment">/*****************************************************************************/</span><span class="comment"></span>
<a name="l00002"></a>00002 <span class="comment">/*!</span>
<a name="l00003"></a>00003 <span class="comment"> * \file theory_bitvector.h</span>
<a name="l00004"></a>00004 <span class="comment"> *</span>
<a name="l00005"></a>00005 <span class="comment"> * Author: Vijay Ganesh</span>
<a name="l00006"></a>00006 <span class="comment"> *</span>
<a name="l00007"></a>00007 <span class="comment"> * Created: Wed May 05 18:34:55 PDT 2004</span>
<a name="l00008"></a>00008 <span class="comment"> *</span>
<a name="l00009"></a>00009 <span class="comment"> * <hr></span>
<a name="l00010"></a>00010 <span class="comment"> *</span>
<a name="l00011"></a>00011 <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span>
<a name="l00012"></a>00012 <span class="comment"> * and its documentation for any purpose is hereby granted without</span>
<a name="l00013"></a>00013 <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span>
<a name="l00014"></a>00014 <span class="comment"> * LICENSE file provided with this distribution.</span>
<a name="l00015"></a>00015 <span class="comment"> *</span>
<a name="l00016"></a>00016 <span class="comment"> * <hr></span>
<a name="l00017"></a>00017 <span class="comment"> *</span>
<a name="l00018"></a>00018 <span class="comment"> */</span>
<a name="l00019"></a>00019 <span class="comment">/*****************************************************************************/</span>
<a name="l00020"></a>00020
<a name="l00021"></a>00021 <span class="preprocessor">#ifndef _cvc3__include__theory_bitvector_h_</span>
<a name="l00022"></a>00022 <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__include__theory_bitvector_h_</span>
<a name="l00023"></a>00023 <span class="preprocessor"></span>
<a name="l00024"></a>00024 <span class="preprocessor">#include "<a class="code" href="theory__core_8h.html">theory_core.h</a>"</span>
<a name="l00025"></a>00025 <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>
<a name="l00026"></a>00026
<a name="l00027"></a>00027 <span class="keyword">namespace </span>CVC3 {
<a name="l00028"></a>00028
<a name="l00029"></a>00029 <span class="keyword">class </span>VCL;
<a name="l00030"></a>00030 <span class="keyword">class </span>BitvectorProofRules;
<a name="l00031"></a>00031
<a name="l00032"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fc">00032</a> <span class="keyword">typedef</span> <span class="keyword">enum</span> { <span class="comment">//some new BV kinds</span>
<a name="l00033"></a>00033 <span class="comment">// New constants</span>
<a name="l00034"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcab517c07f8090ef28822598285c61506d">00034</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcab517c07f8090ef28822598285c61506d">BVCONST</a> = 80,
<a name="l00035"></a>00035
<a name="l00036"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca4099d4b4e4424d6ca22eb0b3fdc73bfa">00036</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca4099d4b4e4424d6ca22eb0b3fdc73bfa">BITVECTOR</a> = 8000,
<a name="l00037"></a>00037
<a name="l00038"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcac706ade993a8d075e5b0e05384f40da2">00038</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcac706ade993a8d075e5b0e05384f40da2">CONCAT</a>,
<a name="l00039"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca814f4580c72ef19f37aeac1b0dc7f7e9">00039</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca814f4580c72ef19f37aeac1b0dc7f7e9">EXTRACT</a>,
<a name="l00040"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcaf5f228243916a2ec50be7811b4333b35">00040</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcaf5f228243916a2ec50be7811b4333b35">BOOLEXTRACT</a>,
<a name="l00041"></a>00041
<a name="l00042"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca0b5ff0bbde7799993800f6c939ba49ef">00042</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca0b5ff0bbde7799993800f6c939ba49ef">LEFTSHIFT</a>,
<a name="l00043"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca39394266637ae52dc7232657e036af7a">00043</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca39394266637ae52dc7232657e036af7a">CONST_WIDTH_LEFTSHIFT</a>,
<a name="l00044"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcad66141e84453a3bae5d9d16f45d25d69">00044</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcad66141e84453a3bae5d9d16f45d25d69">RIGHTSHIFT</a>,
<a name="l00045"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca735ca3566cb9f10aa58f458889f4ddf4">00045</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca735ca3566cb9f10aa58f458889f4ddf4">BVSHL</a>,
<a name="l00046"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca7e306d4cb1a779347c5a2d69a56a5e71">00046</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca7e306d4cb1a779347c5a2d69a56a5e71">BVLSHR</a>,
<a name="l00047"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcac054f57234914470a3912e118222bbf5">00047</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcac054f57234914470a3912e118222bbf5">BVASHR</a>,
<a name="l00048"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca09caf9735c580d393b24bbcca2b60e12">00048</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca09caf9735c580d393b24bbcca2b60e12">SX</a>,
<a name="l00049"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca553ee15794ea4c75c21083a98f3abd9b">00049</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca553ee15794ea4c75c21083a98f3abd9b">BVREPEAT</a>,
<a name="l00050"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca393b289a4d8d97ba38fd9b0c82a64898">00050</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca393b289a4d8d97ba38fd9b0c82a64898">BVZEROEXTEND</a>,
<a name="l00051"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca180d8bac8397070ad5f0cab720858344">00051</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca180d8bac8397070ad5f0cab720858344">BVROTL</a>,
<a name="l00052"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca3bff45238e2f6e14081dd415d2bb409c">00052</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca3bff45238e2f6e14081dd415d2bb409c">BVROTR</a>,
<a name="l00053"></a>00053
<a name="l00054"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca033f8fb5d6777b4ca308522fe7c76abb">00054</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca033f8fb5d6777b4ca308522fe7c76abb">BVAND</a>,
<a name="l00055"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca0e7e1228034ad7003dc056893d4c683d">00055</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca0e7e1228034ad7003dc056893d4c683d">BVOR</a>,
<a name="l00056"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca13c4820e7aec8491475ebaca63c2ac0f">00056</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca13c4820e7aec8491475ebaca63c2ac0f">BVXOR</a>,
<a name="l00057"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcadca4a599a0fbc8bd38015e1714835fca">00057</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcadca4a599a0fbc8bd38015e1714835fca">BVXNOR</a>,
<a name="l00058"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcabe80cab40347b0ecf95be77d5bd7e8d9">00058</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcabe80cab40347b0ecf95be77d5bd7e8d9">BVNEG</a>,
<a name="l00059"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcab9d728d7dca301dd67d31ac302b2ed79">00059</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcab9d728d7dca301dd67d31ac302b2ed79">BVNAND</a>,
<a name="l00060"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcaf68c2ecf7cf6b63a8a50b468126550e3">00060</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcaf68c2ecf7cf6b63a8a50b468126550e3">BVNOR</a>,
<a name="l00061"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcaabff4c1f69d99fc6e230cc1d65aef18d">00061</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcaabff4c1f69d99fc6e230cc1d65aef18d">BVCOMP</a>,
<a name="l00062"></a>00062
<a name="l00063"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcafa8dfe3523dc0fd7eb200b12d9f8bb37">00063</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcafa8dfe3523dc0fd7eb200b12d9f8bb37">BVUMINUS</a>,
<a name="l00064"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcac41c4f67403afc67e2866787a6fc156e">00064</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcac41c4f67403afc67e2866787a6fc156e">BVPLUS</a>,
<a name="l00065"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca6a9467df1bf864d4d635322e43b497e8">00065</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca6a9467df1bf864d4d635322e43b497e8">BVSUB</a>,
<a name="l00066"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca3732a31c60803ee2918ba1999788ba39">00066</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca3732a31c60803ee2918ba1999788ba39">BVMULT</a>,
<a name="l00067"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca8a1bdb340fa2cb36921bf0ec284eb3fd">00067</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca8a1bdb340fa2cb36921bf0ec284eb3fd">BVUDIV</a>,
<a name="l00068"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca1938c4fc956ace5916c7b4bb462f0d6d">00068</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca1938c4fc956ace5916c7b4bb462f0d6d">BVSDIV</a>,
<a name="l00069"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca10b7e4b5dd07687faef4110b6dd7b069">00069</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca10b7e4b5dd07687faef4110b6dd7b069">BVUREM</a>,
<a name="l00070"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca31092d607cf44eb879d517e309e994e9">00070</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca31092d607cf44eb879d517e309e994e9">BVSREM</a>,
<a name="l00071"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcac53836c6cf69b0b07b11dde75dad1e71">00071</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcac53836c6cf69b0b07b11dde75dad1e71">BVSMOD</a>,
<a name="l00072"></a>00072
<a name="l00073"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca92c5ef9334e513d99b62c8d04c60ad20">00073</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca92c5ef9334e513d99b62c8d04c60ad20">BVLT</a>,
<a name="l00074"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca0c2b1488f08f5cd06a50c41e638c1620">00074</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca0c2b1488f08f5cd06a50c41e638c1620">BVLE</a>,
<a name="l00075"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca2474c46c07b6bbe632a473c5fe35666b">00075</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca2474c46c07b6bbe632a473c5fe35666b">BVGT</a>,
<a name="l00076"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca11ee3d8aed0361c47f9b330e89a9cacc">00076</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca11ee3d8aed0361c47f9b330e89a9cacc">BVGE</a>,
<a name="l00077"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca49ad286bf8b76cfbf1684e550536cd5a">00077</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca49ad286bf8b76cfbf1684e550536cd5a">BVSLT</a>,
<a name="l00078"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca0c78fcb723d5a706cfe6372e7c09b04c">00078</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca0c78fcb723d5a706cfe6372e7c09b04c">BVSLE</a>,
<a name="l00079"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca4e6a6d18a93b5e91a53de75a4787a014">00079</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca4e6a6d18a93b5e91a53de75a4787a014">BVSGT</a>,
<a name="l00080"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca01ff0bd050c25dea70aed8413846c2cb">00080</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca01ff0bd050c25dea70aed8413846c2cb">BVSGE</a>,
<a name="l00081"></a>00081
<a name="l00082"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca2c57965432c2e15e6c26475bf1328b51">00082</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca2c57965432c2e15e6c26475bf1328b51">INTTOBV</a>, <span class="comment">// Not implemented yet</span>
<a name="l00083"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca4c3b0b6c64b82b45ec2eb80770c37cf2">00083</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fca4c3b0b6c64b82b45ec2eb80770c37cf2">BVTOINT</a>, <span class="comment">// Not implemented yet</span>
<a name="l00084"></a>00084 <span class="comment">// A wrapper for delaying the construction of type predicates</span>
<a name="l00085"></a><a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcab15d7022f2ee4f2511256d8be02ea6b3">00085</a> <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fcab15d7022f2ee4f2511256d8be02ea6b3">BVTYPEPRED</a>
<a name="l00086"></a>00086 } <a class="code" href="namespaceCVC3.html#abab5915bdb6d99fb9960e1e5c037b9fc">BVKinds</a>;
<a name="l00087"></a>00087
<a name="l00088"></a>00088 <span class="comment">/*****************************************************************************/</span><span class="comment"></span>
<a name="l00089"></a>00089 <span class="comment">/*!</span>
<a name="l00090"></a>00090 <span class="comment"> *\class TheoryBitvector</span>
<a name="l00091"></a>00091 <span class="comment"> *\ingroup Theories</span>
<a name="l00092"></a>00092 <span class="comment"> *\brief Theory of bitvectors of known length \</span>
<a name="l00093"></a>00093 <span class="comment"> * (operations include: @,[i:j],[i],+,.,BVAND,BVNEG)</span>
<a name="l00094"></a>00094 <span class="comment"> *</span>
<a name="l00095"></a>00095 <span class="comment"> * Author: Vijay Ganesh</span>
<a name="l00096"></a>00096 <span class="comment"> *</span>
<a name="l00097"></a>00097 <span class="comment"> * Created:Wed May 5 15:35:07 PDT 2004</span>
<a name="l00098"></a>00098 <span class="comment"> */</span>
<a name="l00099"></a>00099 <span class="comment">/*****************************************************************************/</span>
<a name="l00100"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html">00100</a> <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> {
<a name="l00101"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#a36ce76cce9f4da02fe837fa6d99d6202">00101</a> <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>
<a name="l00102"></a>00102 <span class="comment"> //! MemoryManager index for BVConstExpr subclass</span>
<a name="l00103"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#aca1d99fa896f29efa540d8b83a4de848">00103</a> <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>;
<a name="l00104"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#a96840bd0a2349e2cd33345a709e84907">00104</a> <span class="keywordtype">size_t</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a96840bd0a2349e2cd33345a709e84907">d_bvPlusExprIndex</a>;
<a name="l00105"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#a6d5488901e86cf3db3fc473fc3770766">00105</a> <span class="keywordtype">size_t</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a6d5488901e86cf3db3fc473fc3770766">d_bvParameterExprIndex</a>;
<a name="l00106"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#ae58b98a947a495b8754413e336753518">00106</a> <span class="keywordtype">size_t</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#ae58b98a947a495b8754413e336753518">d_bvTypePredExprIndex</a>;
<a name="l00107"></a>00107 <span class="comment"></span>
<a name="l00108"></a>00108 <span class="comment"> //! counts delayed asserted equalities</span>
<a name="l00109"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#af183050f385d720871a298207a7790b1">00109</a> <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>
<a name="l00110"></a>00110 <span class="comment"> //! counts asserted equalities</span>
<a name="l00111"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#ae855792c718e64c8a46dab88ddd8b1b4">00111</a> <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>
<a name="l00112"></a>00112 <span class="comment"> //! counts delayed asserted disequalities</span>
<a name="l00113"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#a563bcc4483ffa3aee6a8e44e5ab07bcd">00113</a> <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>
<a name="l00114"></a>00114 <span class="comment"> //! counts asserted disequalities</span>
<a name="l00115"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#a071fce068ccf6223f20ba8a8d5b90b00">00115</a> <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>
<a name="l00116"></a>00116 <span class="comment"> //! counts type predicates</span>
<a name="l00117"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#aac1428f779c77033eb5c59b599629cb8">00117</a> <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>
<a name="l00118"></a>00118 <span class="comment"> //! counts delayed type predicates</span>
<a name="l00119"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#aefadf1146b79ded24d7f5a66adba069d">00119</a> <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>
<a name="l00120"></a>00120 <span class="comment"> //! counts bitblasted equalities</span>
<a name="l00121"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#aab7d49f889a88fd2373b722d33e21c31">00121</a> <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>
<a name="l00122"></a>00122 <span class="comment"> //! counts bitblasted disequalities</span>
<a name="l00123"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#a2f2ac7c248fe89fc483c3a1a43c459db">00123</a> <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>;
<a name="l00124"></a>00124 <span class="comment"></span>
<a name="l00125"></a>00125 <span class="comment"> //! boolean on the fly rewrite flag</span>
<a name="l00126"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#a20f9ef1d8f1666eeb16e9f2712320132">00126</a> <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>
<a name="l00127"></a>00127 <span class="comment"> //! bool extract cache flag</span>
<a name="l00128"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#aa96498fb323044a4ab77c9657ac8e614">00128</a> <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>
<a name="l00129"></a>00129 <span class="comment"> //! flag which indicates that all arithmetic is 32 bit with no overflow</span>
<a name="l00130"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#ac219e3d5a18642506f3def182a023989">00130</a> <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>;
<a name="l00131"></a>00131 <span class="comment"></span>
<a name="l00132"></a>00132 <span class="comment"> //! Cache for storing the results of the bitBlastTerm function</span>
<a name="l00133"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#a0f583ba86ce3c379097255ee97620652">00133</a> <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>;
<a name="l00134"></a>00134 <span class="comment"></span>
<a name="l00135"></a>00135 <span class="comment"> //! Cache for pushNegation(). it is ok that this is cache is</span>
<a name="l00136"></a>00136 <span class="comment"></span> <span class="comment">//ExprMap. it is cleared for each call of pushNegation. Does not add</span>
<a name="l00137"></a>00137 <span class="comment">//value across calls of pushNegation</span>
<a name="l00138"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#a2134631ced4e2db4bafac7755a4774f4">00138</a> <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>;
<a name="l00139"></a>00139 <span class="comment"></span>
<a name="l00140"></a>00140 <span class="comment"> //! Backtracking queue for equalities</span>
<a name="l00141"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#af8bcfa021f89dfbc8111eff923e48eab">00141</a> <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>
<a name="l00142"></a>00142 <span class="comment"> //! Backtracking queue for unsolved equalities</span>
<a name="l00143"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#a7c8dcbb9ba2c1c307c403966cd0b0c6d">00143</a> <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>
<a name="l00144"></a>00144 <span class="comment"> //! Index to current position in d_eqPending</span>
<a name="l00145"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#ac017443fdd0f931d9283bc9e2b52d831">00145</a> <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>
<a name="l00146"></a>00146 <span class="comment"> //! Backtracking queue for all other assertions</span>
<a name="l00147"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#ad133cd123c7cc462dbeca98a1d10f8e4">00147</a> <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>
<a name="l00148"></a>00148 <span class="comment"> //! Index to current position in d_bitblast</span>
<a name="l00149"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#ad9f83106573a125c219c3900a9aeceb3">00149</a> <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>
<a name="l00150"></a>00150 <span class="comment"> //! Backtracking database of subterms of shared terms</span>
<a name="l00151"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#aa899ef9e64b78453d199a84160f15444">00151</a> <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>
<a name="l00152"></a>00152 <span class="comment"> //! Backtracking database of subterms of shared terms</span>
<a name="l00153"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#a59850cd32a8031dff8e8918c1e9d31c7">00153</a> <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>;
<a name="l00154"></a>00154 <span class="comment"></span>
<a name="l00155"></a>00155 <span class="comment"> //! Constant 1-bit bit-vector 0bin0</span>
<a name="l00156"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#a8be187368c2a0f4e0b401bc1c7968d19">00156</a> <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>
<a name="l00157"></a>00157 <span class="comment"> //! Constant 1-bit bit-vector 0bin0</span>
<a name="l00158"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#aa4228ded9a53f6edcc7d06406f9c98c7">00158</a> <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>
<a name="l00159"></a>00159 <span class="comment"> //! Return cached constant 0bin0</span>
<a name="l00160"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#a2a6471d4278e92ffcaa981b39001fc8a">00160</a> <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>
<a name="l00161"></a>00161 <span class="comment"> //! Return cached constant 0bin1</span>
<a name="l00162"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#a3de9924e52bf35f61049f07f0d34529f">00162</a> <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>; }
<a name="l00163"></a>00163 <span class="comment"></span>
<a name="l00164"></a>00164 <span class="comment"> //! Max size of any bitvector we've seen</span>
<a name="l00165"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#a1559e63e86e26b348ad8bb618f29f202">00165</a> <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>;
<a name="l00166"></a>00166 <span class="comment"></span>
<a name="l00167"></a>00167 <span class="comment"> //! Used in checkSat</span>
<a name="l00168"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#a8990b759675928a62a4d75cf69fe8d72">00168</a> <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>;
<a name="l00169"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#a2316b51cfa9b54740298ec7d5e6630cb">00169</a> <a class="code" href="classCVC3_1_1CDO.html">CDO<unsigned></a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a2316b51cfa9b54740298ec7d5e6630cb">d_index2</a>;
<a name="l00170"></a>00170 <span class="comment"></span>
<a name="l00171"></a>00171 <span class="comment"> //! functions which implement the DP strategy for bitblasting</span>
<a name="l00172"></a>00172 <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>
<a name="l00173"></a>00173 <span class="comment"> //! bitblast disequation</span>
<a name="l00174"></a>00174 <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>
<a name="l00175"></a>00175 <span class="comment"> //! function which implements the DP strtagey to bitblast Inequations</span>
<a name="l00176"></a>00176 <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>
<a name="l00177"></a>00177 <span class="comment"> //! functions which implement the DP strategy for bitblasting</span>
<a name="l00178"></a>00178 <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);
<a name="l00179"></a>00179
<a name="l00180"></a>00180 <span class="comment">// //! strategy fucntions for BVPLUS NORMAL FORM</span>
<a name="l00181"></a>00181 <span class="comment">// Theorem padBVPlus(const Expr& e);</span>
<a name="l00182"></a>00182 <span class="comment">// //! strategy fucntions for BVPLUS NORMAL FORM</span>
<a name="l00183"></a>00183 <span class="comment">// Theorem flattenBVPlus(const Expr& e);</span>
<a name="l00184"></a>00184
<a name="l00185"></a>00185 <span class="comment">// //! Implementation of the concatenation normal form</span>
<a name="l00186"></a>00186 <span class="comment">// Theorem normalizeConcat(const Expr& e, bool useFind);</span>
<a name="l00187"></a>00187 <span class="comment">// //! Implementation of the n-bit arithmetic normal form</span>
<a name="l00188"></a>00188 <span class="comment">// Theorem normalizeBVArith(const Expr& e, bool useFind);</span>
<a name="l00189"></a>00189 <span class="comment">// //! Helper method for composing normalizations</span>
<a name="l00190"></a>00190 <span class="comment">// Theorem normalizeConcat(const Theorem& t, bool useFind) {</span>
<a name="l00191"></a>00191 <span class="comment">// return transitivityRule(t, normalizeConcat(t.getRHS(), useFind));</span>
<a name="l00192"></a>00192 <span class="comment">// }</span>
<a name="l00193"></a>00193 <span class="comment">// //! Helper method for composing normalizations</span>
<a name="l00194"></a>00194 <span class="comment">// Theorem normalizeBVArith(const Theorem& t, bool useFind) {</span>
<a name="l00195"></a>00195 <span class="comment">// return transitivityRule(t, normalizeBVArith(t.getRHS(), useFind));</span>
<a name="l00196"></a>00196 <span class="comment">// }</span>
<a name="l00197"></a>00197
<a name="l00198"></a>00198 <span class="comment">// Theorem signExtendBVLT(const Expr& e, int len, bool useFind);</span>
<a name="l00199"></a>00199
<a name="l00200"></a>00200 <span class="keyword">public</span>:
<a name="l00201"></a>00201 <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);
<a name="l00202"></a>00202 <span class="keyword">private</span>:
<a name="l00203"></a>00203 <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);
<a name="l00204"></a>00204 <span class="comment"></span>
<a name="l00205"></a>00205 <span class="comment"> //! Top down simplifier</span>
<a name="l00206"></a>00206 <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);
<a name="l00207"></a>00207 <span class="comment"></span>
<a name="l00208"></a>00208 <span class="comment"> //! Internal rewrite method for constants</span>
<a name="l00209"></a>00209 <span class="comment"></span> <span class="comment">// Theorem rewriteConst(const Expr& e);</span>
<a name="l00210"></a>00210 <span class="comment"></span>
<a name="l00211"></a>00211 <span class="comment"> //! Main rewrite method (implements the actual rewrites)</span>
<a name="l00212"></a>00212 <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);
<a name="l00213"></a>00213 <span class="comment"></span>
<a name="l00214"></a>00214 <span class="comment"> //! Rewrite children 'n' levels down (n==1 means "only the top level")</span>
<a name="l00215"></a>00215 <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);
<a name="l00216"></a>00216
<a name="l00217"></a>00217 <span class="comment">// Shortcuts for theorems</span>
<a name="l00218"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#ad9b702d3659fbaab47960bce473608c8">00218</a> <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) {
<a name="l00219"></a>00219 <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));
<a name="l00220"></a>00220 }
<a name="l00221"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#a84f5fc78f3f36e213ea70ff307db9db8">00221</a> <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) {
<a name="l00222"></a>00222 <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));
<a name="l00223"></a>00223 }
<a name="l00224"></a>00224 <span class="comment"></span>
<a name="l00225"></a>00225 <span class="comment"> //! rewrite input boolean expression e to a simpler form</span>
<a name="l00226"></a>00226 <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);
<a name="l00227"></a>00227
<a name="l00228"></a>00228 <span class="comment">/*Beginning of Lorenzo PLatania's methods*/</span>
<a name="l00229"></a>00229
<a name="l00230"></a>00230 <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);
<a name="l00231"></a>00231
<a name="l00232"></a>00232 <span class="comment">// extract the min value from a Rational list</span>
<a name="l00233"></a>00233 <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#ab4f87aca710aa31e6d438e91301beffc">min</a>(std::vector<Rational> list);
<a name="l00234"></a>00234
<a name="l00235"></a>00235 <span class="comment">// evaluates the gcd of two integer coefficients</span>
<a name="l00236"></a>00236 <span class="comment">// int gcd(int c1, int c2);</span>
<a name="l00237"></a>00237
<a name="l00238"></a>00238 <span class="comment">// converts a bv constant to an integer</span>
<a name="l00239"></a>00239 <span class="comment">// int bv2int(const Expr& e);</span>
<a name="l00240"></a>00240
<a name="l00241"></a>00241 <span class="comment">// return the odd coefficient of a leaf for which we can solve the</span>
<a name="l00242"></a>00242 <span class="comment">// equation, or zero if no one has been found</span>
<a name="l00243"></a>00243 <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 );
<a name="l00244"></a>00244
<a name="l00245"></a>00245
<a name="l00246"></a>00246
<a name="l00247"></a>00247 <span class="comment">// returns 1 if e is a linear term</span>
<a name="l00248"></a>00248 <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 );
<a name="l00249"></a>00249
<a name="l00250"></a>00250 <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);
<a name="l00251"></a>00251
<a name="l00252"></a>00252 <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 );
<a name="l00253"></a>00253
<a name="l00254"></a>00254 <span class="comment">// returns how many times "term" appears in "e"</span>
<a name="l00255"></a>00255 <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);
<a name="l00256"></a>00256
<a name="l00257"></a>00257 <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);
<a name="l00258"></a>00258 <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 );
<a name="l00259"></a>00259 <span class="comment">/*End of Lorenzo PLatania's methods*/</span>
<a name="l00260"></a>00260
<a name="l00261"></a>00261 <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);
<a name="l00262"></a>00262
<a name="l00263"></a>00263 <span class="keyword">public</span>:
<a name="l00264"></a>00264 <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);
<a name="l00265"></a>00265 <a class="code" href="classCVC3_1_1TheoryBitvector.html#a665042c64606705b935ac0ab15119266">~TheoryBitvector</a>();
<a name="l00266"></a>00266
<a name="l00267"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#a2508ac260570adfa5584847830806cb0">00267</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a2508ac260570adfa5584847830806cb0">d_bvPlusCarryCacheLeftBV</a>;
<a name="l00268"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#a9fcf8c7246955aa2a8aa6be2fd3d4f64">00268</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> <a class="code" href="classCVC3_1_1TheoryBitvector.html#a9fcf8c7246955aa2a8aa6be2fd3d4f64">d_bvPlusCarryCacheRightBV</a>;
<a name="l00269"></a>00269
<a name="l00270"></a>00270 <span class="comment">// Trusted method that creates the proof rules class (used in constructor).</span>
<a name="l00271"></a>00271 <span class="comment">// Implemented in bitvector_theorem_producer.cpp</span>
<a name="l00272"></a>00272 <a class="code" href="classCVC3_1_1BitvectorProofRules.html">BitvectorProofRules</a>* <a class="code" href="classCVC3_1_1TheoryBitvector.html#ae3141bc37e39e3379fa71d966c887426">createProofRules</a>();
<a name="l00273"></a>00273
<a name="l00274"></a>00274 <span class="comment">// Theory interface</span>
<a name="l00275"></a>00275 <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);
<a name="l00276"></a>00276 <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);
<a name="l00277"></a>00277 <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);
<a name="l00278"></a>00278 <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);
<a name="l00279"></a>00279 <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);
<a name="l00280"></a>00280 <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);
<a name="l00281"></a>00281 <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);
<a name="l00282"></a>00282 <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);
<a name="l00283"></a>00283 <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);
<a name="l00284"></a>00284 <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);
<a name="l00285"></a>00285 <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,
<a name="l00286"></a>00286 <span class="keywordtype">bool</span> enumerate, <span class="keywordtype">bool</span> computeSize);
<a name="l00287"></a>00287 <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);
<a name="l00288"></a>00288 <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);
<a name="l00289"></a>00289 <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);
<a name="l00290"></a>00290 <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);
<a name="l00291"></a>00291 <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);
<a name="l00292"></a>00292 <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);
<a name="l00293"></a>00293 <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);
<a name="l00294"></a>00294
<a name="l00295"></a>00295 <span class="comment">//helper functions</span>
<a name="l00296"></a>00296 <span class="comment"></span>
<a name="l00297"></a>00297 <span class="comment"> //! Return the number of bits in the bitvector expression</span>
<a name="l00298"></a>00298 <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);
<a name="l00299"></a>00299
<a name="l00300"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#ac88ba0954e217df731ebb362135ea107">00300</a> <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>
<a name="l00301"></a>00301 <span class="comment"> //!pads e to be of length len</span>
<a name="l00302"></a>00302 <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);
<a name="l00303"></a>00303
<a name="l00304"></a>00304 <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);
<a name="l00305"></a>00305
<a name="l00306"></a>00306 <span class="comment">//helper functions: functions to construct exprs</span>
<a name="l00307"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#a3d98cac1ae52614ee2adc3fbc407516e">00307</a> <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)
<a name="l00308"></a>00308 { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryBitvector.html#aef4eb029a55a6822baa7c381262154e5">newBitvectorTypeExpr</a>(i); }
<a name="l00309"></a>00309 <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);
<a name="l00310"></a>00310 <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);
<a name="l00311"></a>00311
<a name="l00312"></a>00312 <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);
<a name="l00313"></a>00313 <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);
<a name="l00314"></a>00314
<a name="l00315"></a>00315 <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);
<a name="l00316"></a>00316 <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);
<a name="l00317"></a>00317
<a name="l00318"></a>00318 <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);
<a name="l00319"></a>00319 <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);
<a name="l00320"></a>00320
<a name="l00321"></a>00321 <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);
<a name="l00322"></a>00322 <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);
<a name="l00323"></a>00323
<a name="l00324"></a>00324 <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);
<a name="l00325"></a>00325 <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);
<a name="l00326"></a>00326 <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);
<a name="l00327"></a>00327
<a name="l00328"></a>00328 <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);
<a name="l00329"></a>00329 <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);
<a name="l00330"></a>00330 <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);
<a name="l00331"></a>00331 <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);
<a name="l00332"></a>00332 <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);
<a name="l00333"></a>00333 <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);
<a name="l00334"></a>00334
<a name="l00335"></a>00335 <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);
<a name="l00336"></a>00336 <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);
<a name="l00337"></a>00337 <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);
<a name="l00338"></a>00338 <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);
<a name="l00339"></a>00339 <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);
<a name="l00340"></a>00340 <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);
<a name="l00341"></a>00341 <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);
<a name="l00342"></a>00342 <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);
<a name="l00343"></a>00343 <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);
<a name="l00344"></a>00344 <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);
<a name="l00345"></a>00345 <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);
<a name="l00346"></a>00346 <span class="comment">// Lorenzo's wrapper</span>
<a name="l00347"></a>00347 <span class="comment">// as computeBVConst can not give the BV expr of a negative rational,</span>
<a name="l00348"></a>00348 <span class="comment">// I use this wrapper to do that</span>
<a name="l00349"></a>00349 <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);
<a name="l00350"></a>00350 <span class="comment">// end of Lorenzo's wrapper</span>
<a name="l00351"></a>00351
<a name="l00352"></a>00352 <span class="comment">// Construct BVCONST of length 'len', or the min. needed length when len=0.</span>
<a name="l00353"></a>00353 <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);
<a name="l00354"></a>00354 <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);
<a name="l00355"></a>00355 <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>
<a name="l00356"></a>00356 <span class="comment"> //! hi and low are bit indices</span>
<a name="l00357"></a>00357 <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,
<a name="l00358"></a>00358 <span class="keywordtype">int</span> hi, <span class="keywordtype">int</span> low);
<a name="l00359"></a>00359 <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>
<a name="l00360"></a>00360 <span class="comment"> //! 'numbits' is the number of bits in the result</span>
<a name="l00361"></a>00361 <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>
<a name="l00362"></a>00362 <span class="comment"> //! 'numbits' is the number of bits in the result</span>
<a name="l00363"></a>00363 <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>
<a name="l00364"></a>00364 <span class="comment"> //! pads children and then builds plus expr</span>
<a name="l00365"></a>00365 <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);
<a name="l00366"></a>00366 <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,
<a name="l00367"></a>00367 <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);
<a name="l00368"></a>00368 <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);
<a name="l00369"></a>00369 <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,
<a name="l00370"></a>00370 <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);
<a name="l00371"></a>00371 <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);
<a name="l00372"></a>00372 <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);
<a name="l00373"></a>00373 <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);
<a name="l00374"></a>00374 <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);
<a name="l00375"></a>00375 <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);
<a name="l00376"></a>00376 <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);
<a name="l00377"></a>00377
<a name="l00378"></a>00378 <span class="comment">// Accessors for expression parameters</span>
<a name="l00379"></a>00379 <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);
<a name="l00380"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#a0d6c5357741846c314acfda3f93094a9">00380</a> <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)
<a name="l00381"></a>00381 { <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>()); }
<a name="l00382"></a>00382 <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);
<a name="l00383"></a>00383 <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);
<a name="l00384"></a>00384 <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);
<a name="l00385"></a>00385 <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);
<a name="l00386"></a>00386 <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);
<a name="l00387"></a>00387 <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);
<a name="l00388"></a>00388 <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);
<a name="l00389"></a>00389 <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);
<a name="l00390"></a>00390 <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);
<a name="l00391"></a>00391 <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);
<a name="l00392"></a>00392 <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);
<a name="l00393"></a>00393
<a name="l00394"></a>00394 <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);
<a name="l00395"></a>00395 <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>
<a name="l00396"></a>00396 <span class="comment"> //!computes the integer value of a bitvector constant</span>
<a name="l00397"></a>00397 <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>
<a name="l00398"></a>00398 <span class="comment"> //!computes the integer value of ~c+1 or BVUMINUS(c)</span>
<a name="l00399"></a>00399 <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);
<a name="l00400"></a>00400
<a name="l00401"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#af9b48795b632ce717e9f2149c99689fb">00401</a> <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>; }
<a name="l00402"></a>00402
<a name="l00403"></a>00403 <span class="comment">/*Beginning of Lorenzo PLatania's public methods*/</span>
<a name="l00404"></a>00404
<a name="l00405"></a>00405 <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 );
<a name="l00406"></a>00406 <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 );
<a name="l00407"></a>00407 <span class="comment">// checks whether e can be solved in term</span>
<a name="l00408"></a>00408 <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 );
<a name="l00409"></a>00409
<a name="l00410"></a>00410 <span class="comment">// evaluates the multipicative inverse</span>
<a name="l00411"></a>00411 <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);
<a name="l00412"></a>00412
<a name="l00413"></a>00413
<a name="l00414"></a>00414 <span class="comment">/*End of Lorenzo PLatania's public methods*/</span>
<a name="l00415"></a>00415
<a name="l00416"></a><a class="code" href="classCVC3_1_1TheoryBitvector.html#aa17e44a8047fc0f5220565f6cd5a203f">00416</a> std::vector<Theorem> <a class="code" href="classCVC3_1_1TheoryBitvector.html#aa17e44a8047fc0f5220565f6cd5a203f">additionalRewriteConstraints</a>;
<a name="l00417"></a>00417
<a name="l00418"></a>00418 }; <span class="comment">//end of class TheoryBitvector</span>
<a name="l00419"></a>00419
<a name="l00420"></a>00420
<a name="l00421"></a>00421 }<span class="comment">//end of namespace CVC3</span>
<a name="l00422"></a>00422 <span class="preprocessor">#endif</span>
</pre></div></div>
</div>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
