<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<meta http-equiv="X-UA-Compatible" content="IE=9"/>
<title>CVC3: theory_arith3.h Source File</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="jquery.js"></script>
<script type="text/javascript" src="dynsections.js"></script>
<link href="doxygen.css" rel="stylesheet" type="text/css" />
</head>
<body>
<div id="top"><!-- do not remove this div, it is closed by doxygen! -->
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3
</div>
</td>
</tr>
</tbody>
</table>
</div>
<!-- end header part -->
<!-- Generated by Doxygen 1.8.2 -->
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li><a href="annotated.html"><span>Classes</span></a></li>
<li class="current"><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="files.html"><span>File List</span></a></li>
<li><a href="globals.html"><span>File Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="dir_68267d1309a1af8e8297ef4c3efbcdba.html">src</a></li><li class="navelem"><a class="el" href="dir_b0856f6b0d80ccb263b2f415c91f9e17.html">include</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="headertitle">
<div class="title">theory_arith3.h</div> </div>
</div><!--header-->
<div class="contents">
<a href="theory__arith3_8h.html">Go to the documentation of this file.</a><div class="fragment"><div class="line"><a name="l00001"></a><span class="lineno"> 1</span> <span class="comment">/*****************************************************************************/</span><span class="comment"></span></div>
<div class="line"><a name="l00002"></a><span class="lineno"> 2</span> <span class="comment">/*!</span></div>
<div class="line"><a name="l00003"></a><span class="lineno"> 3</span> <span class="comment"> * \file theory_arith3.h</span></div>
<div class="line"><a name="l00004"></a><span class="lineno"> 4</span> <span class="comment"> * </span></div>
<div class="line"><a name="l00005"></a><span class="lineno"> 5</span> <span class="comment"> * Author: Clark Barrett</span></div>
<div class="line"><a name="l00006"></a><span class="lineno"> 6</span> <span class="comment"> * </span></div>
<div class="line"><a name="l00007"></a><span class="lineno"> 7</span> <span class="comment"> * Created: Thu Jun 14 13:22:11 2007</span></div>
<div class="line"><a name="l00008"></a><span class="lineno"> 8</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00009"></a><span class="lineno"> 9</span> <span class="comment"> * <hr></span></div>
<div class="line"><a name="l00010"></a><span class="lineno"> 10</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00011"></a><span class="lineno"> 11</span> <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span></div>
<div class="line"><a name="l00012"></a><span class="lineno"> 12</span> <span class="comment"> * and its documentation for any purpose is hereby granted without</span></div>
<div class="line"><a name="l00013"></a><span class="lineno"> 13</span> <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span></div>
<div class="line"><a name="l00014"></a><span class="lineno"> 14</span> <span class="comment"> * LICENSE file provided with this distribution.</span></div>
<div class="line"><a name="l00015"></a><span class="lineno"> 15</span> <span class="comment"> * </span></div>
<div class="line"><a name="l00016"></a><span class="lineno"> 16</span> <span class="comment"> * <hr></span></div>
<div class="line"><a name="l00017"></a><span class="lineno"> 17</span> <span class="comment"> * </span></div>
<div class="line"><a name="l00018"></a><span class="lineno"> 18</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00019"></a><span class="lineno"> 19</span> <span class="comment">/*****************************************************************************/</span></div>
<div class="line"><a name="l00020"></a><span class="lineno"> 20</span> </div>
<div class="line"><a name="l00021"></a><span class="lineno"> 21</span> <span class="preprocessor">#ifndef _cvc3__include__theory_arith3_h_</span></div>
<div class="line"><a name="l00022"></a><span class="lineno"> 22</span> <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__include__theory_arith3_h_</span></div>
<div class="line"><a name="l00023"></a><span class="lineno"> 23</span> <span class="preprocessor"></span></div>
<div class="line"><a name="l00024"></a><span class="lineno"> 24</span> <span class="preprocessor">#include "<a class="code" href="theory__arith_8h.html">theory_arith.h</a>"</span></div>
<div class="line"><a name="l00025"></a><span class="lineno"> 25</span> </div>
<div class="line"><a name="l00026"></a><span class="lineno"> 26</span> <span class="keyword">namespace </span>CVC3 {</div>
<div class="line"><a name="l00027"></a><span class="lineno"> 27</span> </div>
<div class="line"><a name="l00028"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3.html"> 28</a></span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1TheoryArith3.html">TheoryArith3</a> :<span class="keyword">public</span> <a class="code" href="classCVC3_1_1TheoryArith.html" title="This theory handles basic linear arithmetic.">TheoryArith</a> {</div>
<div class="line"><a name="l00029"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3.html#a27d63b744292174502cd871610cd3d1f"> 29</a></span>  <a class="code" href="classCVC3_1_1CDList.html">CDList<Theorem></a> <a class="code" href="classCVC3_1_1TheoryArith3.html#a27d63b744292174502cd871610cd3d1f">d_diseq</a>; <span class="comment">// For concrete model generation</span></div>
<div class="line"><a name="l00030"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3.html#a8f6255ef2bae62211980a687a178a923"> 30</a></span>  <a class="code" href="classCVC3_1_1CDO.html">CDO<size_t></a> <a class="code" href="classCVC3_1_1TheoryArith3.html#a8f6255ef2bae62211980a687a178a923">d_diseqIdx</a>; <span class="comment">// Index to the next unprocessed disequality</span></div>
<div class="line"><a name="l00031"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3.html#ad36b56d2d11b3c5398c4d9f554bae18e"> 31</a></span>  <a class="code" href="classCVC3_1_1ArithProofRules.html">ArithProofRules</a>* <a class="code" href="classCVC3_1_1TheoryArith3.html#ad36b56d2d11b3c5398c4d9f554bae18e">d_rules</a>;</div>
<div class="line"><a name="l00032"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3.html#ab6ea7bdf248ad9f15dbbb2a25c70d53d"> 32</a></span>  <a class="code" href="classCVC3_1_1CDO.html">CDO<bool></a> <a class="code" href="classCVC3_1_1TheoryArith3.html#ab6ea7bdf248ad9f15dbbb2a25c70d53d">d_inModelCreation</a>;</div>
<div class="line"><a name="l00033"></a><span class="lineno"> 33</span> <span class="comment"></span></div>
<div class="line"><a name="l00034"></a><span class="lineno"> 34</span> <span class="comment"> //! Data class for the strongest free constant in separation inqualities</span></div>
<div class="line"><a name="l00035"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html"> 35</a></span> <span class="comment"></span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html" title="Data class for the strongest free constant in separation inqualities.">FreeConst</a> {</div>
<div class="line"><a name="l00036"></a><span class="lineno"> 36</span>  <span class="keyword">private</span>:</div>
<div class="line"><a name="l00037"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html#a21b19900b574aa5811f8ff509f462adc"> 37</a></span>  <a class="code" href="classCVC3_1_1Rational.html">Rational</a> <a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html#a21b19900b574aa5811f8ff509f462adc">d_r</a>;</div>
<div class="line"><a name="l00038"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html#abb9b46f53c831589cbd1a43fa8a454ed"> 38</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html#abb9b46f53c831589cbd1a43fa8a454ed">d_strict</a>;</div>
<div class="line"><a name="l00039"></a><span class="lineno"> 39</span>  <span class="keyword">public</span>:</div>
<div class="line"><a name="l00040"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html#ac351ae05917b9c1cf518def6ebc60931"> 40</a></span>  <a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html#ac351ae05917b9c1cf518def6ebc60931">FreeConst</a>() { }</div>
<div class="line"><a name="l00041"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html#ab6f3c524cdb2b2cb8e690299f347510e"> 41</a></span>  <a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html#ab6f3c524cdb2b2cb8e690299f347510e">FreeConst</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Rational.html">Rational</a>& r, <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html#a81887e267dfe84df58a876474011601a">strict</a>): <a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html#a21b19900b574aa5811f8ff509f462adc">d_r</a>(r), <a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html#abb9b46f53c831589cbd1a43fa8a454ed">d_strict</a>(strict) { }</div>
<div class="line"><a name="l00042"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html#a0c5f7aef8c5d3c3e2dbca9a80711a523"> 42</a></span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Rational.html">Rational</a>& <a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html#a0c5f7aef8c5d3c3e2dbca9a80711a523">getConst</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html#a21b19900b574aa5811f8ff509f462adc">d_r</a>; }</div>
<div class="line"><a name="l00043"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html#a81887e267dfe84df58a876474011601a"> 43</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html#a81887e267dfe84df58a876474011601a">strict</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html#abb9b46f53c831589cbd1a43fa8a454ed">d_strict</a>; }</div>
<div class="line"><a name="l00044"></a><span class="lineno"> 44</span>  };<span class="comment"></span></div>
<div class="line"><a name="l00045"></a><span class="lineno"> 45</span> <span class="comment"> //! Printing</span></div>
<div class="line"><a name="l00046"></a><span class="lineno"> 46</span> <span class="comment"></span> <span class="keyword">friend</span> std::ostream& <a class="code" href="classCVC3_1_1TheoryArith3.html#a24b0687e8f0fa36a6d5bacc8155517e2" title="Printing.">operator<<</a>(std::ostream& os, <span class="keyword">const</span> FreeConst& fc);</div>
<div class="line"><a name="l00047"></a><span class="lineno"> 47</span> <span class="comment"></span></div>
<div class="line"><a name="l00048"></a><span class="lineno"> 48</span> <span class="comment"> //! Private class for an inequality in the Fourier-Motzkin database</span></div>
<div class="line"><a name="l00049"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html"> 49</a></span> <span class="comment"></span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html" title="Private class for an inequality in the Fourier-Motzkin database.">Ineq</a> {</div>
<div class="line"><a name="l00050"></a><span class="lineno"> 50</span>  <span class="keyword">private</span>:</div>
<div class="line"><a name="l00051"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a1f60f98a9ea7af2ab7d88938a75adc9a"> 51</a></span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a1f60f98a9ea7af2ab7d88938a75adc9a" title="The inequality.">d_ineq</a>; <span class="comment">//!< The inequality</span></div>
<div class="line"><a name="l00052"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a7771529070ba56e5372268cd6bbf933b"> 52</a></span> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a7771529070ba56e5372268cd6bbf933b" title="Var is isolated on the RHS.">d_rhs</a>; <span class="comment">//!< Var is isolated on the RHS</span></div>
<div class="line"><a name="l00053"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a74cc096f9bd6c60e0eb03dfd6111eb72"> 53</a></span> <span class="comment"></span> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html" title="Data class for the strongest free constant in separation inqualities.">FreeConst</a>* <a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a74cc096f9bd6c60e0eb03dfd6111eb72">d_const</a>; <span class="comment">//!< The max/min const for subsumption check</span></div>
<div class="line"><a name="l00054"></a><span class="lineno"> 54</span> <span class="comment"></span><span class="comment"> //! Default constructor is disabled</span></div>
<div class="line"><a name="l00055"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a8abbe09b51cd4577f581259521fcd648"> 55</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a8abbe09b51cd4577f581259521fcd648" title="Default constructor is disabled.">Ineq</a>() { }</div>
<div class="line"><a name="l00056"></a><span class="lineno"> 56</span>  <span class="keyword">public</span>:<span class="comment"></span></div>
<div class="line"><a name="l00057"></a><span class="lineno"> 57</span> <span class="comment"> //! Initial constructor. 'r' is taken from the subsumption database.</span></div>
<div class="line"><a name="l00058"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a805b109e6c6e114c224bd948a452fa90"> 58</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a8abbe09b51cd4577f581259521fcd648" title="Default constructor is disabled.">Ineq</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& <a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#ae56ae01b38b372401bd3a8f407093558" title="Get the inequality.">ineq</a>, <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a7f588540905cfdd00b515ea59c8c0482" title="Flag whether var is isolated on the RHS.">varOnRHS</a>, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html" title="Data class for the strongest free constant in separation inqualities.">FreeConst</a>& c):</div>
<div class="line"><a name="l00059"></a><span class="lineno"> 59</span>  <a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a1f60f98a9ea7af2ab7d88938a75adc9a" title="The inequality.">d_ineq</a>(ineq), <a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a7771529070ba56e5372268cd6bbf933b" title="Var is isolated on the RHS.">d_rhs</a>(varOnRHS), <a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a74cc096f9bd6c60e0eb03dfd6111eb72">d_const</a>(&c) { }<span class="comment"></span></div>
<div class="line"><a name="l00060"></a><span class="lineno"> 60</span> <span class="comment"> //! Get the inequality</span></div>
<div class="line"><a name="l00061"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#ae56ae01b38b372401bd3a8f407093558"> 61</a></span> <span class="comment"></span> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& <a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#ae56ae01b38b372401bd3a8f407093558" title="Get the inequality.">ineq</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a1f60f98a9ea7af2ab7d88938a75adc9a" title="The inequality.">d_ineq</a>; }<span class="comment"></span></div>
<div class="line"><a name="l00062"></a><span class="lineno"> 62</span> <span class="comment"> //! Get the max/min constant</span></div>
<div class="line"><a name="l00063"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a9207644df8d21b4db1c5e3a88fb2cdfb"> 63</a></span> <span class="comment"></span> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html" title="Data class for the strongest free constant in separation inqualities.">FreeConst</a>& <a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a9207644df8d21b4db1c5e3a88fb2cdfb" title="Get the max/min constant.">getConst</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> *<a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a74cc096f9bd6c60e0eb03dfd6111eb72">d_const</a>; }<span class="comment"></span></div>
<div class="line"><a name="l00064"></a><span class="lineno"> 64</span> <span class="comment"> //! Flag whether var is isolated on the RHS</span></div>
<div class="line"><a name="l00065"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a7f588540905cfdd00b515ea59c8c0482"> 65</a></span> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a7f588540905cfdd00b515ea59c8c0482" title="Flag whether var is isolated on the RHS.">varOnRHS</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a7771529070ba56e5372268cd6bbf933b" title="Var is isolated on the RHS.">d_rhs</a>; }<span class="comment"></span></div>
<div class="line"><a name="l00066"></a><span class="lineno"> 66</span> <span class="comment"> //! Flag whether var is isolated on the LHS</span></div>
<div class="line"><a name="l00067"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a3f5d837020af57b45fbaa704727a7e11"> 67</a></span> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a3f5d837020af57b45fbaa704727a7e11" title="Flag whether var is isolated on the LHS.">varOnLHS</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> !<a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a7771529070ba56e5372268cd6bbf933b" title="Var is isolated on the RHS.">d_rhs</a>; }<span class="comment"></span></div>
<div class="line"><a name="l00068"></a><span class="lineno"> 68</span> <span class="comment"> //! Auto-cast to Theorem</span></div>
<div class="line"><a name="l00069"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#ae9fce2eb529ed3a936ae93ef87273b0b"> 69</a></span> <span class="comment"></span> <span class="keyword">operator</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a1f60f98a9ea7af2ab7d88938a75adc9a" title="The inequality.">d_ineq</a>; }</div>
<div class="line"><a name="l00070"></a><span class="lineno"> 70</span>  };<span class="comment"></span></div>
<div class="line"><a name="l00071"></a><span class="lineno"> 71</span> <span class="comment"> //! Printing</span></div>
<div class="line"><a name="l00072"></a><span class="lineno"> 72</span> <span class="comment"></span> <span class="keyword">friend</span> std::ostream& <a class="code" href="classCVC3_1_1TheoryArith3.html#a24b0687e8f0fa36a6d5bacc8155517e2" title="Printing.">operator<<</a>(std::ostream& os, <span class="keyword">const</span> Ineq& ineq);</div>
<div class="line"><a name="l00073"></a><span class="lineno"> 73</span> <span class="comment"></span></div>
<div class="line"><a name="l00074"></a><span class="lineno"> 74</span> <span class="comment"> //! Database of inequalities with a variable isolated on the right</span></div>
<div class="line"><a name="l00075"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3.html#ae907bba6bfb622671693d64fd4f7651b"> 75</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<CDList<Ineq></a> *> <a class="code" href="classCVC3_1_1TheoryArith3.html#ae907bba6bfb622671693d64fd4f7651b" title="Database of inequalities with a variable isolated on the right.">d_inequalitiesRightDB</a>;</div>
<div class="line"><a name="l00076"></a><span class="lineno"> 76</span> <span class="comment"></span></div>
<div class="line"><a name="l00077"></a><span class="lineno"> 77</span> <span class="comment"> //! Database of inequalities with a variable isolated on the left</span></div>
<div class="line"><a name="l00078"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3.html#adef4166f884bc9d39c9649de29ba6223"> 78</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<CDList<Ineq></a> *> <a class="code" href="classCVC3_1_1TheoryArith3.html#adef4166f884bc9d39c9649de29ba6223" title="Database of inequalities with a variable isolated on the left.">d_inequalitiesLeftDB</a>;</div>
<div class="line"><a name="l00079"></a><span class="lineno"> 79</span> <span class="comment"></span></div>
<div class="line"><a name="l00080"></a><span class="lineno"> 80</span> <span class="comment"> //! Mapping of inequalities to the largest/smallest free constant</span></div>
<div class="line"><a name="l00081"></a><span class="lineno"> 81</span> <span class="comment"></span><span class="comment"> /*! The Expr is the original inequality with the free constant</span></div>
<div class="line"><a name="l00082"></a><span class="lineno"> 82</span> <span class="comment"> * removed and inequality converted to non-strict (for indexing</span></div>
<div class="line"><a name="l00083"></a><span class="lineno"> 83</span> <span class="comment"> * purposes). I.e. ax<c+t becomes ax<=t. This inequality is mapped</span></div>
<div class="line"><a name="l00084"></a><span class="lineno"> 84</span> <span class="comment"> * to a pair<c,strict>, the smallest (largest for c+t<ax) constant</span></div>
<div class="line"><a name="l00085"></a><span class="lineno"> 85</span> <span class="comment"> * among inequalities with the same 'a', 'x', and 't', and a boolean</span></div>
<div class="line"><a name="l00086"></a><span class="lineno"> 86</span> <span class="comment"> * flag indicating whether the strongest inequality is strict.</span></div>
<div class="line"><a name="l00087"></a><span class="lineno"> 87</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00088"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3.html#abe31caa3bc2ac4ee941a83870b802ab4"> 88</a></span>  <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, FreeConst></a> <a class="code" href="classCVC3_1_1TheoryArith3.html#abe31caa3bc2ac4ee941a83870b802ab4" title="Mapping of inequalities to the largest/smallest free constant.">d_freeConstDB</a>;</div>
<div class="line"><a name="l00089"></a><span class="lineno"> 89</span> </div>
<div class="line"><a name="l00090"></a><span class="lineno"> 90</span>  <span class="comment">// Input buffer to store the incoming inequalities</span></div>
<div class="line"><a name="l00091"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3.html#a3875f5f084ebf03733c8f94a4774c536"> 91</a></span>  <a class="code" href="classCVC3_1_1CDList.html">CDList<Theorem></a> <a class="code" href="classCVC3_1_1TheoryArith3.html#a3875f5f084ebf03733c8f94a4774c536" title="Buffer of input inequalities.">d_buffer</a>; <span class="comment">//!< Buffer of input inequalities</span></div>
<div class="line"><a name="l00092"></a><span class="lineno"> 92</span> <span class="comment"></span></div>
<div class="line"><a name="l00093"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3.html#a1e095f1d7e371b227dc08f3b8635c004"> 93</a></span>  <a class="code" href="classCVC3_1_1CDO.html">CDO<size_t></a> <a class="code" href="classCVC3_1_1TheoryArith3.html#a1e095f1d7e371b227dc08f3b8635c004" title="Buffer index of the next unprocessed inequality.">d_bufferIdx</a>; <span class="comment">//!< Buffer index of the next unprocessed inequality</span></div>
<div class="line"><a name="l00094"></a><span class="lineno"> 94</span> <span class="comment"></span></div>
<div class="line"><a name="l00095"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3.html#aa1aa058a244693fbfadaa8326d9573a2"> 95</a></span>  <span class="keyword">const</span> <span class="keywordtype">int</span>* <a class="code" href="classCVC3_1_1TheoryArith3.html#aa1aa058a244693fbfadaa8326d9573a2" title="Threshold when the buffer must be processed.">d_bufferThres</a>; <span class="comment">//!< Threshold when the buffer must be processed</span></div>
<div class="line"><a name="l00096"></a><span class="lineno"> 96</span> <span class="comment"></span></div>
<div class="line"><a name="l00097"></a><span class="lineno"> 97</span>  <span class="comment">// Statistics for the variables</span></div>
<div class="line"><a name="l00098"></a><span class="lineno"> 98</span> <span class="comment"></span></div>
<div class="line"><a name="l00099"></a><span class="lineno"> 99</span> <span class="comment"> /*! @brief Mapping of a variable to the number of inequalities where</span></div>
<div class="line"><a name="l00100"></a><span class="lineno"> 100</span> <span class="comment"> the variable would be isolated on the right */</span></div>
<div class="line"><a name="l00101"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3.html#a6d0840e19aef8d9e2e3eefad3cb5a279"> 101</a></span>  <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, int></a> <a class="code" href="classCVC3_1_1TheoryArith3.html#a6d0840e19aef8d9e2e3eefad3cb5a279" title="Mapping of a variable to the number of inequalities where the variable would be isolated on the right...">d_countRight</a>;</div>
<div class="line"><a name="l00102"></a><span class="lineno"> 102</span> <span class="comment"></span></div>
<div class="line"><a name="l00103"></a><span class="lineno"> 103</span> <span class="comment"> /*! @brief Mapping of a variable to the number of inequalities where</span></div>
<div class="line"><a name="l00104"></a><span class="lineno"> 104</span> <span class="comment"> the variable would be isolated on the left */</span></div>
<div class="line"><a name="l00105"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3.html#a45bee8f005bbd76195fd207f6e14b530"> 105</a></span>  <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, int></a> <a class="code" href="classCVC3_1_1TheoryArith3.html#a45bee8f005bbd76195fd207f6e14b530" title="Mapping of a variable to the number of inequalities where the variable would be isolated on the left...">d_countLeft</a>;</div>
<div class="line"><a name="l00106"></a><span class="lineno"> 106</span> <span class="comment"></span></div>
<div class="line"><a name="l00107"></a><span class="lineno"> 107</span> <span class="comment"> //! Set of shared terms (for counterexample generation)</span></div>
<div class="line"><a name="l00108"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3.html#a4e74ec27493ce714497a40de4743a706"> 108</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, bool></a> <a class="code" href="classCVC3_1_1TheoryArith3.html#a4e74ec27493ce714497a40de4743a706" title="Set of shared terms (for counterexample generation)">d_sharedTerms</a>;</div>
<div class="line"><a name="l00109"></a><span class="lineno"> 109</span> <span class="comment"></span></div>
<div class="line"><a name="l00110"></a><span class="lineno"> 110</span> <span class="comment"> //! Set of shared integer variables (i-leaves)</span></div>
<div class="line"><a name="l00111"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3.html#a333b1082c80655c02182b44a0c4a8dda"> 111</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, bool></a> <a class="code" href="classCVC3_1_1TheoryArith3.html#a333b1082c80655c02182b44a0c4a8dda" title="Set of shared integer variables (i-leaves)">d_sharedVars</a>;</div>
<div class="line"><a name="l00112"></a><span class="lineno"> 112</span> </div>
<div class="line"><a name="l00113"></a><span class="lineno"> 113</span>  <span class="comment">//Directed Acyclic Graph representing partial variable ordering for</span></div>
<div class="line"><a name="l00114"></a><span class="lineno"> 114</span>  <span class="comment">//variable projection over inequalities.</span></div>
<div class="line"><a name="l00115"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3_1_1VarOrderGraph.html"> 115</a></span>  <span class="keyword">class </span><a class="code" href="classCVC3_1_1TheoryArith3_1_1VarOrderGraph.html">VarOrderGraph</a> {</div>
<div class="line"><a name="l00116"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3_1_1VarOrderGraph.html#addddfffbec3000a4203e471639b6bfab"> 116</a></span>  <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<std::vector<Expr></a> > <a class="code" href="classCVC3_1_1TheoryArith3_1_1VarOrderGraph.html#addddfffbec3000a4203e471639b6bfab">d_edges</a>;</div>
<div class="line"><a name="l00117"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3_1_1VarOrderGraph.html#a16d50d02f53c31cfa278e25f3f6db518"> 117</a></span>  <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<bool></a> <a class="code" href="classCVC3_1_1TheoryArith3_1_1VarOrderGraph.html#a16d50d02f53c31cfa278e25f3f6db518">d_cache</a>;</div>
<div class="line"><a name="l00118"></a><span class="lineno"> 118</span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArith3_1_1VarOrderGraph.html#a6ac9265a0a7221011c0411bf17288ec9">dfs</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e2);</div>
<div class="line"><a name="l00119"></a><span class="lineno"> 119</span>  <span class="keyword">public</span>:</div>
<div class="line"><a name="l00120"></a><span class="lineno"> 120</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3_1_1VarOrderGraph.html#a51dbff9f12b47c8ad5e0724a12dacc51">addEdge</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e2);</div>
<div class="line"><a name="l00121"></a><span class="lineno"> 121</span>  <span class="comment">//returns true if e1 < e2, false otherwise.</span></div>
<div class="line"><a name="l00122"></a><span class="lineno"> 122</span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArith3_1_1VarOrderGraph.html#acaacdf139637b2d7a2a47a341c8be640">lessThan</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e2);</div>
<div class="line"><a name="l00123"></a><span class="lineno"> 123</span>  <span class="comment">//selects those variables which are largest and incomparable among</span></div>
<div class="line"><a name="l00124"></a><span class="lineno"> 124</span>  <span class="comment">//v1 and puts it into v2</span></div>
<div class="line"><a name="l00125"></a><span class="lineno"> 125</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3_1_1VarOrderGraph.html#a0a69fb1270ba25e41ed948f1eb0417d9">selectLargest</a>(<span class="keyword">const</span> std::vector<Expr>& v1, std::vector<Expr>& v2);</div>
<div class="line"><a name="l00126"></a><span class="lineno"> 126</span>  <span class="comment">//selects those variables which are smallest and incomparable among</span></div>
<div class="line"><a name="l00127"></a><span class="lineno"> 127</span>  <span class="comment">//v1, removes them from v1 and puts them into v2. </span></div>
<div class="line"><a name="l00128"></a><span class="lineno"> 128</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3_1_1VarOrderGraph.html#aab3e30fe8063d2feeddac9f4226a2f60">selectSmallest</a>( std::vector<Expr>& v1, std::vector<Expr>& v2);</div>
<div class="line"><a name="l00129"></a><span class="lineno"> 129</span>  };</div>
<div class="line"><a name="l00130"></a><span class="lineno"> 130</span>  </div>
<div class="line"><a name="l00131"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3.html#a7b9b0448e5f0149ea33709b1ba392c1e"> 131</a></span>  <a class="code" href="classCVC3_1_1TheoryArith3_1_1VarOrderGraph.html">VarOrderGraph</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#a7b9b0448e5f0149ea33709b1ba392c1e">d_graph</a>;</div>
<div class="line"><a name="l00132"></a><span class="lineno"> 132</span> </div>
<div class="line"><a name="l00133"></a><span class="lineno"> 133</span>  <span class="comment">// Private methods</span></div>
<div class="line"><a name="l00134"></a><span class="lineno"> 134</span> <span class="comment"></span></div>
<div class="line"><a name="l00135"></a><span class="lineno"> 135</span> <span class="comment"> //! Check the term t for integrality. </span></div>
<div class="line"><a name="l00136"></a><span class="lineno"> 136</span> <span class="comment"></span><span class="comment"> /*! \return a theorem of IS_INTEGER(t) or Null. */</span></div>
<div class="line"><a name="l00137"></a><span class="lineno"> 137</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#ac053c3120ee5ede28ff6097b2faea155" title="Check the term t for integrality.">isIntegerThm</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00138"></a><span class="lineno"> 138</span> <span class="comment"></span></div>
<div class="line"><a name="l00139"></a><span class="lineno"> 139</span> <span class="comment"> //! A helper method for isIntegerThm()</span></div>
<div class="line"><a name="l00140"></a><span class="lineno"> 140</span> <span class="comment"></span><span class="comment"> /*! Check if IS_INTEGER(e) is easily derivable from the given 'thm' */</span></div>
<div class="line"><a name="l00141"></a><span class="lineno"> 141</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#ae5339522241766bfc991ca476f94b6d8" title="A helper method for isIntegerThm()">isIntegerDerive</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& isIntE, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);</div>
<div class="line"><a name="l00142"></a><span class="lineno"> 142</span> <span class="comment"></span></div>
<div class="line"><a name="l00143"></a><span class="lineno"> 143</span> <span class="comment"> //! Extract the free constant from an inequality</span></div>
<div class="line"><a name="l00144"></a><span class="lineno"> 144</span> <span class="comment"></span> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Rational.html">Rational</a>& <a class="code" href="classCVC3_1_1TheoryArith3.html#a472ba8372206ffe82fc42f33f032784a" title="Extract the free constant from an inequality.">freeConstIneq</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& ineq, <span class="keywordtype">bool</span> varOnRHS);</div>
<div class="line"><a name="l00145"></a><span class="lineno"> 145</span> <span class="comment"></span></div>
<div class="line"><a name="l00146"></a><span class="lineno"> 146</span> <span class="comment"> //! Update the free constant subsumption database with new inequality</span></div>
<div class="line"><a name="l00147"></a><span class="lineno"> 147</span> <span class="comment"></span><span class="comment"> /*! \return a reference to the max/min constant.</span></div>
<div class="line"><a name="l00148"></a><span class="lineno"> 148</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00149"></a><span class="lineno"> 149</span> <span class="comment"> * Also, sets 'subsumed' argument to true if the inequality is</span></div>
<div class="line"><a name="l00150"></a><span class="lineno"> 150</span> <span class="comment"> * subsumed by an existing inequality.</span></div>
<div class="line"><a name="l00151"></a><span class="lineno"> 151</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00152"></a><span class="lineno"> 152</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html" title="Data class for the strongest free constant in separation inqualities.">FreeConst</a>& <a class="code" href="classCVC3_1_1TheoryArith3.html#ae4e1a30b7247216751f1eaea91362cc0" title="Update the free constant subsumption database with new inequality.">updateSubsumptionDB</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& ineq, <span class="keywordtype">bool</span> varOnRHS,</div>
<div class="line"><a name="l00153"></a><span class="lineno"> 153</span>  <span class="keywordtype">bool</span>& subsumed);<span class="comment"></span></div>
<div class="line"><a name="l00154"></a><span class="lineno"> 154</span> <span class="comment"> //! Check if the kids of e are fully simplified and canonized (for debugging)</span></div>
<div class="line"><a name="l00155"></a><span class="lineno"> 155</span> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#a9f75f31dff3486528563454fce4381a6" title="Check if the kids of e are fully simplified and canonized (for debugging)">kidsCanonical</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00156"></a><span class="lineno"> 156</span> <span class="comment"></span></div>
<div class="line"><a name="l00157"></a><span class="lineno"> 157</span> <span class="comment"> //! Canonize the expression e, assuming all children are canonical</span></div>
<div class="line"><a name="l00158"></a><span class="lineno"> 158</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#a4fecdcaa672c9263e1f823c6650d1725" title="Canonize the expression e, assuming all children are canonical.">canon</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00159"></a><span class="lineno"> 159</span> <span class="comment"></span></div>
<div class="line"><a name="l00160"></a><span class="lineno"> 160</span> <span class="comment"> /*! @brief Canonize and reduce e w.r.t. union-find database; assume</span></div>
<div class="line"><a name="l00161"></a><span class="lineno"> 161</span> <span class="comment"> * all children are canonical */</span></div>
<div class="line"><a name="l00162"></a><span class="lineno"> 162</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#a486c66ef1f738b8ec48ac580d16b0d60" title="Canonize and reduce e w.r.t. union-find database; assume all children are canonical.">canonSimplify</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00163"></a><span class="lineno"> 163</span> <span class="comment"></span></div>
<div class="line"><a name="l00164"></a><span class="lineno"> 164</span> <span class="comment"> /*! @brief Composition of canonSimplify(const Expr&) by</span></div>
<div class="line"><a name="l00165"></a><span class="lineno"> 165</span> <span class="comment"> * transitivity: take e0 = e1, canonize and simplify e1 to e2,</span></div>
<div class="line"><a name="l00166"></a><span class="lineno"> 166</span> <span class="comment"> * return e0 = e2. */</span></div>
<div class="line"><a name="l00167"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3.html#aaef92a86079cf95107c7c4552fe77a34"> 167</a></span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#aaef92a86079cf95107c7c4552fe77a34" title="Composition of canonSimplify(const Expr&) by transitivity: take e0 = e1, canonize and simplify e1 to ...">canonSimplify</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm) {</div>
<div class="line"><a name="l00168"></a><span class="lineno"> 168</span>  <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Theory.html#a76f6507116e36f46dab074781fb9bf2d" title="(a1 == a2) & (a2 == a3) ==> (a1 == a3)">transitivityRule</a>(thm, <a class="code" href="classCVC3_1_1TheoryArith3.html#a486c66ef1f738b8ec48ac580d16b0d60" title="Canonize and reduce e w.r.t. union-find database; assume all children are canonical.">canonSimplify</a>(thm.<a class="code" href="classCVC3_1_1Theorem.html#a97d957fcbf9094480851b1d2e5d3729f">getRHS</a>()));</div>
<div class="line"><a name="l00169"></a><span class="lineno"> 169</span>  }</div>
<div class="line"><a name="l00170"></a><span class="lineno"> 170</span> <span class="comment"></span></div>
<div class="line"><a name="l00171"></a><span class="lineno"> 171</span> <span class="comment"> //! Canonize predicate (x = y, x < y, etc.)</span></div>
<div class="line"><a name="l00172"></a><span class="lineno"> 172</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#a785848c0f072e06ca036ed4ce1f8c16b" title="Canonize predicate (x = y, x < y, etc.)">canonPred</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);</div>
<div class="line"><a name="l00173"></a><span class="lineno"> 173</span> <span class="comment"></span></div>
<div class="line"><a name="l00174"></a><span class="lineno"> 174</span> <span class="comment"> //! Canonize predicate like canonPred except that the input theorem</span></div>
<div class="line"><a name="l00175"></a><span class="lineno"> 175</span> <span class="comment"> //! is an equivalent transformation.</span></div>
<div class="line"><a name="l00176"></a><span class="lineno"> 176</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#ac0c4f725256399640c17b0783fec9f13">canonPredEquiv</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);</div>
<div class="line"><a name="l00177"></a><span class="lineno"> 177</span> <span class="comment"></span></div>
<div class="line"><a name="l00178"></a><span class="lineno"> 178</span> <span class="comment"> //! Solve an equation and return an equivalent Theorem in the solved form</span></div>
<div class="line"><a name="l00179"></a><span class="lineno"> 179</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#ac686439c56c6043030c7f54054fb679a" title="Solve an equation and return an equivalent Theorem in the solved form.">doSolve</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e);</div>
<div class="line"><a name="l00180"></a><span class="lineno"> 180</span> <span class="comment"></span></div>
<div class="line"><a name="l00181"></a><span class="lineno"> 181</span> <span class="comment"> //! takes in a conjunction equivalence Thm and canonizes it.</span></div>
<div class="line"><a name="l00182"></a><span class="lineno"> 182</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#af806119e538c39891145ef30f906e9af" title="takes in a conjunction equivalence Thm and canonizes it.">canonConjunctionEquiv</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);</div>
<div class="line"><a name="l00183"></a><span class="lineno"> 183</span> <span class="comment"></span></div>
<div class="line"><a name="l00184"></a><span class="lineno"> 184</span> <span class="comment"> //! picks the monomial with the smallest abs(coeff) from the input</span></div>
<div class="line"><a name="l00185"></a><span class="lineno"> 185</span> <span class="comment"></span> <span class="comment">//integer equation.</span></div>
<div class="line"><a name="l00186"></a><span class="lineno"> 186</span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#a353478e5b8c453a2e8d774f5e6131cd3" title="picks the monomial with the smallest abs(coeff) from the input">pickIntEqMonomial</a>(<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="namespaceMiniSat.html#a82558b7a36c52f5d3211d5d14bed99d4">right</a>, <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& isolated, <span class="keywordtype">bool</span>& nonlin);</div>
<div class="line"><a name="l00187"></a><span class="lineno"> 187</span> <span class="comment"></span></div>
<div class="line"><a name="l00188"></a><span class="lineno"> 188</span> <span class="comment"> //! processes equalities with 1 or more vars of type REAL</span></div>
<div class="line"><a name="l00189"></a><span class="lineno"> 189</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#aa7ff101a4a69c0234af6c0a53ba29764" title="processes equalities with 1 or more vars of type REAL">processRealEq</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& eqn);</div>
<div class="line"><a name="l00190"></a><span class="lineno"> 190</span> <span class="comment"></span></div>
<div class="line"><a name="l00191"></a><span class="lineno"> 191</span> <span class="comment"> //! processes equalities whose vars are all of type INT</span></div>
<div class="line"><a name="l00192"></a><span class="lineno"> 192</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#a040075d9eae3b054cc65a994d311c70a" title="processes equalities whose vars are all of type INT">processIntEq</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& eqn);</div>
<div class="line"><a name="l00193"></a><span class="lineno"> 193</span> <span class="comment"></span></div>
<div class="line"><a name="l00194"></a><span class="lineno"> 194</span> <span class="comment"> //! One step of INT equality processing (aux. method for processIntEq())</span></div>
<div class="line"><a name="l00195"></a><span class="lineno"> 195</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#ae3a3a08b59de54cff2cca3da66b89ca3" title="One step of INT equality processing (aux. method for processIntEq())">processSimpleIntEq</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& eqn);</div>
<div class="line"><a name="l00196"></a><span class="lineno"> 196</span> <span class="comment"></span></div>
<div class="line"><a name="l00197"></a><span class="lineno"> 197</span> <span class="comment"> //! Process inequalities in the buffer</span></div>
<div class="line"><a name="l00198"></a><span class="lineno"> 198</span> <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#a3a28af3eaef560d01cc9755f29f1dcd1" title="Process inequalities in the buffer.">processBuffer</a>();</div>
<div class="line"><a name="l00199"></a><span class="lineno"> 199</span> <span class="comment"></span></div>
<div class="line"><a name="l00200"></a><span class="lineno"> 200</span> <span class="comment"> //! Take an inequality and isolate a variable</span></div>
<div class="line"><a name="l00201"></a><span class="lineno"> 201</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#a46aa67085cf8a1c691cbe5846e740765" title="Take an inequality and isolate a variable.">isolateVariable</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& inputThm, <span class="keywordtype">bool</span>& e1);</div>
<div class="line"><a name="l00202"></a><span class="lineno"> 202</span> <span class="comment"></span></div>
<div class="line"><a name="l00203"></a><span class="lineno"> 203</span> <span class="comment"> //! Update the statistics counters for the variable with a coeff. c</span></div>
<div class="line"><a name="l00204"></a><span class="lineno"> 204</span> <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#a6dffd309689d82e967c9bbe05d2ba982" title="Update the statistics counters for the variable with a coeff. c.">updateStats</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Rational.html">Rational</a>& c, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& var);</div>
<div class="line"><a name="l00205"></a><span class="lineno"> 205</span> <span class="comment"></span></div>
<div class="line"><a name="l00206"></a><span class="lineno"> 206</span> <span class="comment"> //! Update the statistics counters for the monomial</span></div>
<div class="line"><a name="l00207"></a><span class="lineno"> 207</span> <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#a6dffd309689d82e967c9bbe05d2ba982" title="Update the statistics counters for the variable with a coeff. c.">updateStats</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& monomial);</div>
<div class="line"><a name="l00208"></a><span class="lineno"> 208</span> <span class="comment"></span></div>
<div class="line"><a name="l00209"></a><span class="lineno"> 209</span> <span class="comment"> //! Add an inequality to the input buffer. See also d_buffer</span></div>
<div class="line"><a name="l00210"></a><span class="lineno"> 210</span> <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#a504bf0d2dd4a3b5e3346db7ffd105d63" title="Add an inequality to the input buffer. See also d_buffer.">addToBuffer</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);</div>
<div class="line"><a name="l00211"></a><span class="lineno"> 211</span> <span class="comment"></span></div>
<div class="line"><a name="l00212"></a><span class="lineno"> 212</span> <span class="comment"> /*! @brief Given a canonized term, compute a factor to make all</span></div>
<div class="line"><a name="l00213"></a><span class="lineno"> 213</span> <span class="comment"> coefficients integer and relatively prime */</span></div>
<div class="line"><a name="l00214"></a><span class="lineno"> 214</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#a2eeb16c35c6b47810a8163f556fdafc5" title="Given a canonized term, compute a factor to make all coefficients integer and relatively prime...">computeNormalFactor</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& rhs);</div>
<div class="line"><a name="l00215"></a><span class="lineno"> 215</span> <span class="comment"></span></div>
<div class="line"><a name="l00216"></a><span class="lineno"> 216</span> <span class="comment"> //! Normalize an equation (make all coefficients rel. prime integers)</span></div>
<div class="line"><a name="l00217"></a><span class="lineno"> 217</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#ac92c123cb9146a4a0f3f45e37b3306ed" title="Normalize an equation (make all coefficients rel. prime integers)">normalize</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00218"></a><span class="lineno"> 218</span> <span class="comment"></span></div>
<div class="line"><a name="l00219"></a><span class="lineno"> 219</span> <span class="comment"> //! Normalize an equation (make all coefficients rel. prime integers)</span></div>
<div class="line"><a name="l00220"></a><span class="lineno"> 220</span> <span class="comment"></span><span class="comment"> /*! accepts a rewrite theorem over eqn|ineqn and normalizes it</span></div>
<div class="line"><a name="l00221"></a><span class="lineno"> 221</span> <span class="comment"> * and returns a theorem to that effect.</span></div>
<div class="line"><a name="l00222"></a><span class="lineno"> 222</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00223"></a><span class="lineno"> 223</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#ac92c123cb9146a4a0f3f45e37b3306ed" title="Normalize an equation (make all coefficients rel. prime integers)">normalize</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);</div>
<div class="line"><a name="l00224"></a><span class="lineno"> 224</span> </div>
<div class="line"><a name="l00225"></a><span class="lineno"> 225</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#a5e2c1bdff3d602f37c1cc89dd4fd1574">pickMonomial</a>(<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="namespaceMiniSat.html#a82558b7a36c52f5d3211d5d14bed99d4">right</a>);</div>
<div class="line"><a name="l00226"></a><span class="lineno"> 226</span> </div>
<div class="line"><a name="l00227"></a><span class="lineno"> 227</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#a6ca53edda892c56d40b65b2f9cad610c">getFactors</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::set<Expr>& factors);</div>
<div class="line"><a name="l00228"></a><span class="lineno"> 228</span> </div>
<div class="line"><a name="l00229"></a><span class="lineno"> 229</span>  <span class="keyword">public</span>: <span class="comment">// ArithTheoremProducer needs this function, so make it public</span><span class="comment"></span></div>
<div class="line"><a name="l00230"></a><span class="lineno"> 230</span> <span class="comment"> //! Separate monomial e = c*p1*...*pn into c and 1*p1*...*pn</span></div>
<div class="line"><a name="l00231"></a><span class="lineno"> 231</span> <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#a70491110f5b66fb6fd62c109b6dffc09" title="Separate monomial e = c*p1*...*pn into c and 1*p1*...*pn.">separateMonomial</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_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& c, <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& var);<span class="comment"></span></div>
<div class="line"><a name="l00232"></a><span class="lineno"> 232</span> <span class="comment"> //! Check the term t for integrality (return bool)</span></div>
<div class="line"><a name="l00233"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3.html#addd34c5d0ee1bdab0ecbbc92ebd0f175"> 233</a></span> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#addd34c5d0ee1bdab0ecbbc92ebd0f175" title="Check the term t for integrality (return bool)">isInteger</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="keywordflow">return</span> !(<a class="code" href="classCVC3_1_1TheoryArith3.html#ac053c3120ee5ede28ff6097b2faea155" title="Check the term t for integrality.">isIntegerThm</a>(e).<a class="code" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</a>()); }</div>
<div class="line"><a name="l00234"></a><span class="lineno"> 234</span> </div>
<div class="line"><a name="l00235"></a><span class="lineno"> 235</span> </div>
<div class="line"><a name="l00236"></a><span class="lineno"> 236</span>  <span class="keyword">private</span>:</div>
<div class="line"><a name="l00237"></a><span class="lineno"> 237</span> </div>
<div class="line"><a name="l00238"></a><span class="lineno"> 238</span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#a957c9fd7f07ee82288a20effb505ca06">lessThanVar</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& isolatedVar, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& var2);</div>
<div class="line"><a name="l00239"></a><span class="lineno"> 239</span> <span class="comment"></span></div>
<div class="line"><a name="l00240"></a><span class="lineno"> 240</span> <span class="comment"> //! Check if the term expression is "stale"</span></div>
<div class="line"><a name="l00241"></a><span class="lineno"> 241</span> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#a17195fe93c0fe689e6a1d08c1459bd82" title="Check if the term expression is "stale".">isStale</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00242"></a><span class="lineno"> 242</span> <span class="comment"></span></div>
<div class="line"><a name="l00243"></a><span class="lineno"> 243</span> <span class="comment"> //! Check if the inequality is "stale" or subsumed</span></div>
<div class="line"><a name="l00244"></a><span class="lineno"> 244</span> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#a17195fe93c0fe689e6a1d08c1459bd82" title="Check if the term expression is "stale".">isStale</a>(<span class="keyword">const</span> Ineq& ineq);</div>
<div class="line"><a name="l00245"></a><span class="lineno"> 245</span> </div>
<div class="line"><a name="l00246"></a><span class="lineno"> 246</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#a2896ed5876f029204b26eca916c6cdbd">projectInequalities</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& theInequality,<span class="keywordtype">bool</span> isolatedVarOnRHS);</div>
<div class="line"><a name="l00247"></a><span class="lineno"> 247</span> </div>
<div class="line"><a name="l00248"></a><span class="lineno"> 248</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#ab88556951a1e36e72efb357ed5ff8231">assignVariables</a>(std::vector<Expr>&v);</div>
<div class="line"><a name="l00249"></a><span class="lineno"> 249</span> </div>
<div class="line"><a name="l00250"></a><span class="lineno"> 250</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#af02fbf9a3193abb569fcb27e5f1d2db7">findRationalBound</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& varSide, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& ratSide, </div>
<div class="line"><a name="l00251"></a><span class="lineno"> 251</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& var,</div>
<div class="line"><a name="l00252"></a><span class="lineno"> 252</span>  <a class="code" href="classCVC3_1_1Rational.html">Rational</a> &r);</div>
<div class="line"><a name="l00253"></a><span class="lineno"> 253</span> </div>
<div class="line"><a name="l00254"></a><span class="lineno"> 254</span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#aa26c0384f5e6b14af63cba1bda052445">findBounds</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <a class="code" href="classCVC3_1_1Rational.html">Rational</a>& lub, <a class="code" href="classCVC3_1_1Rational.html">Rational</a>& glb);</div>
<div class="line"><a name="l00255"></a><span class="lineno"> 255</span> </div>
<div class="line"><a name="l00256"></a><span class="lineno"> 256</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#aff09d333af28a78565540409f88024fa">normalizeProjectIneqs</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& ineqThm1,</div>
<div class="line"><a name="l00257"></a><span class="lineno"> 257</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& ineqThm2);</div>
<div class="line"><a name="l00258"></a><span class="lineno"> 258</span> <span class="comment"></span></div>
<div class="line"><a name="l00259"></a><span class="lineno"> 259</span> <span class="comment"> //! Take a system of equations and turn it into a solved form</span></div>
<div class="line"><a name="l00260"></a><span class="lineno"> 260</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#a1660f18e07c37dcda3be7afa645722a5" title="Take a system of equations and turn it into a solved form.">solvedForm</a>(<span class="keyword">const</span> std::vector<Theorem>& solvedEqs);</div>
<div class="line"><a name="l00261"></a><span class="lineno"> 261</span> <span class="comment"></span></div>
<div class="line"><a name="l00262"></a><span class="lineno"> 262</span> <span class="comment"> /*! @brief Substitute all vars in term 't' according to the</span></div>
<div class="line"><a name="l00263"></a><span class="lineno"> 263</span> <span class="comment"> * substitution 'subst' and canonize the result.</span></div>
<div class="line"><a name="l00264"></a><span class="lineno"> 264</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00265"></a><span class="lineno"> 265</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#ac2fcec4f5baacf96ca2383e073d44228" title="Substitute all vars in term 't' according to the substitution 'subst' and canonize the result...">substAndCanonize</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t, <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Theorem></a>& subst);</div>
<div class="line"><a name="l00266"></a><span class="lineno"> 266</span> <span class="comment"></span></div>
<div class="line"><a name="l00267"></a><span class="lineno"> 267</span> <span class="comment"> /*! @brief Substitute all vars in the RHS of the equation 'eq' of</span></div>
<div class="line"><a name="l00268"></a><span class="lineno"> 268</span> <span class="comment"> * the form (x = t) according to the substitution 'subst', and</span></div>
<div class="line"><a name="l00269"></a><span class="lineno"> 269</span> <span class="comment"> * canonize the result.</span></div>
<div class="line"><a name="l00270"></a><span class="lineno"> 270</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00271"></a><span class="lineno"> 271</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#ac2fcec4f5baacf96ca2383e073d44228" title="Substitute all vars in term 't' according to the substitution 'subst' and canonize the result...">substAndCanonize</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& eq, <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Theorem></a>& subst);</div>
<div class="line"><a name="l00272"></a><span class="lineno"> 272</span> <span class="comment"></span></div>
<div class="line"><a name="l00273"></a><span class="lineno"> 273</span> <span class="comment"> //! Traverse 'e' and push all the i-leaves into 'vars' vector</span></div>
<div class="line"><a name="l00274"></a><span class="lineno"> 274</span> <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#a9dce9b9f5badc37fb3bcadcf8ef78583" title="Traverse 'e' and push all the i-leaves into 'vars' vector.">collectVars</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, std::vector<Expr>& vars,</div>
<div class="line"><a name="l00275"></a><span class="lineno"> 275</span>  std::set<Expr>& cache);</div>
<div class="line"><a name="l00276"></a><span class="lineno"> 276</span> <span class="comment"></span></div>
<div class="line"><a name="l00277"></a><span class="lineno"> 277</span> <span class="comment"> /*! @brief Check if alpha <= ax & bx <= beta is a finite interval</span></div>
<div class="line"><a name="l00278"></a><span class="lineno"> 278</span> <span class="comment"> * for integer var 'x', and assert the corresponding constraint</span></div>
<div class="line"><a name="l00279"></a><span class="lineno"> 279</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00280"></a><span class="lineno"> 280</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#aee8cdf4bc28c2aa427a49bb8e221b88d" title="Check if alpha <= ax & bx <= beta is a finite interval for integer var 'x', and assert the correspondin...">processFiniteInterval</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& alphaLEax,</div>
<div class="line"><a name="l00281"></a><span class="lineno"> 281</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& bxLEbeta);</div>
<div class="line"><a name="l00282"></a><span class="lineno"> 282</span> <span class="comment"></span></div>
<div class="line"><a name="l00283"></a><span class="lineno"> 283</span> <span class="comment"> //! For an integer var 'x', find and process all constraints A <= ax <= A+c </span></div>
<div class="line"><a name="l00284"></a><span class="lineno"> 284</span> <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#a6cea6a92562860617a56fd0c4181245e" title="For an integer var 'x', find and process all constraints A <= ax <= A+c.">processFiniteIntervals</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& x);</div>
<div class="line"><a name="l00285"></a><span class="lineno"> 285</span> <span class="comment"></span></div>
<div class="line"><a name="l00286"></a><span class="lineno"> 286</span> <span class="comment"> //! Recursive setup for isolated inequalities (and other new expressions)</span></div>
<div class="line"><a name="l00287"></a><span class="lineno"> 287</span> <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#a981a077978ed5779f8ac4b739d32c084" title="Recursive setup for isolated inequalities (and other new expressions)">setupRec</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00288"></a><span class="lineno"> 288</span> </div>
<div class="line"><a name="l00289"></a><span class="lineno"> 289</span> <span class="keyword">public</span>:</div>
<div class="line"><a name="l00290"></a><span class="lineno"> 290</span>  <a class="code" href="classCVC3_1_1TheoryArith3.html#a788719650296495e2ab22966e462b3ac">TheoryArith3</a>(<a class="code" href="classCVC3_1_1TheoryCore.html" title="This theory handles the built-in logical connectives plus equality. It also handles the registration ...">TheoryCore</a>* core);</div>
<div class="line"><a name="l00291"></a><span class="lineno"> 291</span>  <a class="code" href="classCVC3_1_1TheoryArith3.html#a6ce33109bdf13407e2c36a6e608132cd">~TheoryArith3</a>();</div>
<div class="line"><a name="l00292"></a><span class="lineno"> 292</span> </div>
<div class="line"><a name="l00293"></a><span class="lineno"> 293</span>  <span class="comment">// Trusted method that creates the proof rules class (used in constructor).</span></div>
<div class="line"><a name="l00294"></a><span class="lineno"> 294</span>  <span class="comment">// Implemented in arith_theorem_producer.cpp</span></div>
<div class="line"><a name="l00295"></a><span class="lineno"> 295</span>  <a class="code" href="classCVC3_1_1ArithProofRules.html">ArithProofRules</a>* <a class="code" href="classCVC3_1_1TheoryArith3.html#af8a9ccde61831efd7b0e9093ed1d9770">createProofRules3</a>();</div>
<div class="line"><a name="l00296"></a><span class="lineno"> 296</span> </div>
<div class="line"><a name="l00297"></a><span class="lineno"> 297</span>  <span class="comment">// Theory interface</span></div>
<div class="line"><a name="l00298"></a><span class="lineno"> 298</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#a1f122f4d960ac5df603cf7759681c95b" title="Notify theory of a new shared term.">addSharedTerm</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00299"></a><span class="lineno"> 299</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#a0b160ba7b04b17aba1d9f07c6d776b0e" title="Assert a new fact to the decision procedure.">assertFact</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e);</div>
<div class="line"><a name="l00300"></a><span class="lineno"> 300</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#ae44a95809991c134c6ed6a8c795a06bc" title="Process disequalities from the arrangement for model generation.">refineCounterExample</a>();</div>
<div class="line"><a name="l00301"></a><span class="lineno"> 301</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#a6e35b7340b2370e2ac9ea6b6892ec479" title="Assign concrete values to basic-type variables in v.">computeModelBasic</a>(<span class="keyword">const</span> std::vector<Expr>& v);</div>
<div class="line"><a name="l00302"></a><span class="lineno"> 302</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#ad9f6d84e930741b9b6675dec46ba9b26" title="Compute the value of a compound variable from the more primitive ones.">computeModel</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, std::vector<Expr>& vars);</div>
<div class="line"><a name="l00303"></a><span class="lineno"> 303</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#ad92218d82a1bf0005a223e6ed3b3726b" title="Check for satisfiability in the theory.">checkSat</a>(<span class="keywordtype">bool</span> fullEffort);</div>
<div class="line"><a name="l00304"></a><span class="lineno"> 304</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#a372ca4601f982473511cd0fc55c83374" title="Theory-specific rewrite rules.">rewrite</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00305"></a><span class="lineno"> 305</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#a9a07172dc5440407baddcc225166651e" title="Set up the term e for call-backs when e or its children change.">setup</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00306"></a><span class="lineno"> 306</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#a91d859d6893c57f28679590a23a32f15" title="Notify a theory of a new equality.">update</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& d);</div>
<div class="line"><a name="l00307"></a><span class="lineno"> 307</span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#a3faa3983fb7a7a37c24ccbf500528bbe" title="An optional solver.">solve</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e);</div>
<div class="line"><a name="l00308"></a><span class="lineno"> 308</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#ab609e73ab4f8ff747730845f864ef18a" title="A debug check used by the primary solver.">checkAssertEqInvariant</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e);</div>
<div class="line"><a name="l00309"></a><span class="lineno"> 309</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#a27cd5a977820921847abb91ffd728165" title="Check that e is a valid Type expr.">checkType</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00310"></a><span class="lineno"> 310</span>  <a class="code" href="namespaceCVC3.html#af969e724f8b7016909f5804e8cea3e54" title="Enum for cardinality of types.">Cardinality</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#a8b64f176481b2c25cf42e31efe2e64fd" title="Compute information related to finiteness of types.">finiteTypeInfo</a>(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a>& n,</div>
<div class="line"><a name="l00311"></a><span class="lineno"> 311</span>  <span class="keywordtype">bool</span> enumerate, <span class="keywordtype">bool</span> computeSize);</div>
<div class="line"><a name="l00312"></a><span class="lineno"> 312</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#a71487fca123272ebec2f37b6fecfbf3e" title="Compute and store the type of e.">computeType</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00313"></a><span class="lineno"> 313</span>  <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#a6d158689e4805c7d62a7a06b919e3d53" title="Compute the base type of the top-level operator of an arbitrary type.">computeBaseType</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& t);</div>
<div class="line"><a name="l00314"></a><span class="lineno"> 314</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#a00b11e39bb30b25373399c0cd20f6dd0" title="Add variables from 'e' to 'v' for constructing a concrete model.">computeModelTerm</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, std::vector<Expr>& v);</div>
<div class="line"><a name="l00315"></a><span class="lineno"> 315</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#a0aecfd1729c28dfb1229372a65edb3ad" title="Theory specific computation of the subtyping predicate for type t applied to the expression e...">computeTypePred</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& t, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00316"></a><span class="lineno"> 316</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#af49bfb7657ee001bbb3caeeb04630847" title="Compute and cache the TCC of e.">computeTCC</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00317"></a><span class="lineno"> 317</span>  <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& <a class="code" href="classCVC3_1_1TheoryArith3.html#a016c76766dead2d406c96f51138f72a3" title="Theory-specific pretty-printing.">print</a>(<a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& os, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00318"></a><span class="lineno"> 318</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#a26016acc412642afc4712d68dd4af25d" title="Theory-specific parsing implemented by the DP.">parseExprOp</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00319"></a><span class="lineno"> 319</span> </div>
<div class="line"><a name="l00320"></a><span class="lineno"> 320</span> <span class="keyword">private</span>:</div>
<div class="line"><a name="l00321"></a><span class="lineno"> 321</span>  <span class="comment"></span></div>
<div class="line"><a name="l00322"></a><span class="lineno"> 322</span> <span class="comment"> /** Map from variables to the maximal (by absolute value) of one of it's coefficients */</span> </div>
<div class="line"><a name="l00323"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3.html#aaafeb6382856c921da73af220df2ab1b"> 323</a></span>  <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, Rational></a> <a class="code" href="classCVC3_1_1TheoryArith3.html#aaafeb6382856c921da73af220df2ab1b">maxCoefficientLeft</a>;</div>
<div class="line"><a name="l00324"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3.html#a53ede9d74a99ac939974d488b146d13f"> 324</a></span>  <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, Rational></a> <a class="code" href="classCVC3_1_1TheoryArith3.html#a53ede9d74a99ac939974d488b146d13f">maxCoefficientRight</a>;</div>
<div class="line"><a name="l00325"></a><span class="lineno"> 325</span>  <span class="comment"></span></div>
<div class="line"><a name="l00326"></a><span class="lineno"> 326</span> <span class="comment"> /** Map from variables to the fixed value of one of it's coefficients */</span></div>
<div class="line"><a name="l00327"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryArith3.html#acefeaa2f3e7b84414fb92b90ab6364cb"> 327</a></span>  <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, Rational></a> <a class="code" href="classCVC3_1_1TheoryArith3.html#acefeaa2f3e7b84414fb92b90ab6364cb">fixedMaxCoefficient</a>; </div>
<div class="line"><a name="l00328"></a><span class="lineno"> 328</span>  <span class="comment"></span></div>
<div class="line"><a name="l00329"></a><span class="lineno"> 329</span> <span class="comment"> /** </span></div>
<div class="line"><a name="l00330"></a><span class="lineno"> 330</span> <span class="comment"> * Returns the current maximal coefficient of the variable.</span></div>
<div class="line"><a name="l00331"></a><span class="lineno"> 331</span> <span class="comment"> * </span></div>
<div class="line"><a name="l00332"></a><span class="lineno"> 332</span> <span class="comment"> * @param var the variable.</span></div>
<div class="line"><a name="l00333"></a><span class="lineno"> 333</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00334"></a><span class="lineno"> 334</span>  <a class="code" href="classCVC3_1_1Rational.html">Rational</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#a84f83db057e52785fe6ee6c7036668d2">currentMaxCoefficient</a>(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> var);</div>
<div class="line"><a name="l00335"></a><span class="lineno"> 335</span>  <span class="comment"></span></div>
<div class="line"><a name="l00336"></a><span class="lineno"> 336</span> <span class="comment"> /**</span></div>
<div class="line"><a name="l00337"></a><span class="lineno"> 337</span> <span class="comment"> * Fixes the current max coefficient to be used in the ordering. If the maximal coefficient</span></div>
<div class="line"><a name="l00338"></a><span class="lineno"> 338</span> <span class="comment"> * changes in the future, it will not be used in the ordering.</span></div>
<div class="line"><a name="l00339"></a><span class="lineno"> 339</span> <span class="comment"> * </span></div>
<div class="line"><a name="l00340"></a><span class="lineno"> 340</span> <span class="comment"> * @param variable the variable</span></div>
<div class="line"><a name="l00341"></a><span class="lineno"> 341</span> <span class="comment"> * @param max the value to set it to</span></div>
<div class="line"><a name="l00342"></a><span class="lineno"> 342</span> <span class="comment"> */</span> </div>
<div class="line"><a name="l00343"></a><span class="lineno"> 343</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#a16d4eb1ecd6adb8fde86f2c3ce4d6ef1">fixCurrentMaxCoefficient</a>(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> variable, <a class="code" href="classCVC3_1_1Rational.html">Rational</a> <a class="code" href="namespaceCVC3.html#a308233b4ca114e33cfa278d45f8d09ea">max</a>);</div>
<div class="line"><a name="l00344"></a><span class="lineno"> 344</span>  <span class="comment"></span></div>
<div class="line"><a name="l00345"></a><span class="lineno"> 345</span> <span class="comment"> /**</span></div>
<div class="line"><a name="l00346"></a><span class="lineno"> 346</span> <span class="comment"> * Among given input variables, select the smallest ones with respect to the coefficients.</span></div>
<div class="line"><a name="l00347"></a><span class="lineno"> 347</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00348"></a><span class="lineno"> 348</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#a21438a9cc9b82b7c6cf3b269b663a8d0">selectSmallestByCoefficient</a>(std::vector<Expr> input, std::vector<Expr>& output);</div>
<div class="line"><a name="l00349"></a><span class="lineno"> 349</span> };</div>
<div class="line"><a name="l00350"></a><span class="lineno"> 350</span> </div>
<div class="line"><a name="l00351"></a><span class="lineno"> 351</span> }</div>
<div class="line"><a name="l00352"></a><span class="lineno"> 352</span> </div>
<div class="line"><a name="l00353"></a><span class="lineno"> 353</span> <span class="preprocessor">#endif</span></div>
</div><!-- fragment --></div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:15 for CVC3 by  <a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/>
</a> 1.8.2
</small></address>
</body>
</html>
