<!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_arith3.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_arith3.h</div> </div>
</div>
<div class="contents">
<a href="theory__arith3_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_arith3.h</span>
<a name="l00004"></a>00004 <span class="comment"> * </span>
<a name="l00005"></a>00005 <span class="comment"> * Author: Clark Barrett</span>
<a name="l00006"></a>00006 <span class="comment"> * </span>
<a name="l00007"></a>00007 <span class="comment"> * Created: Thu Jun 14 13:22:11 2007</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_arith3_h_</span>
<a name="l00022"></a>00022 <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__include__theory_arith3_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__arith_8h.html">theory_arith.h</a>"</span>
<a name="l00025"></a>00025
<a name="l00026"></a>00026 <span class="keyword">namespace </span>CVC3 {
<a name="l00027"></a>00027
<a name="l00028"></a><a class="code" href="classCVC3_1_1TheoryArith3.html">00028</a> <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> {
<a name="l00029"></a><a class="code" href="classCVC3_1_1TheoryArith3.html#a27d63b744292174502cd871610cd3d1f">00029</a> <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>
<a name="l00030"></a><a class="code" href="classCVC3_1_1TheoryArith3.html#a8f6255ef2bae62211980a687a178a923">00030</a> <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>
<a name="l00031"></a><a class="code" href="classCVC3_1_1TheoryArith3.html#ad36b56d2d11b3c5398c4d9f554bae18e">00031</a> <a class="code" href="classCVC3_1_1ArithProofRules.html">ArithProofRules</a>* <a class="code" href="classCVC3_1_1TheoryArith3.html#ad36b56d2d11b3c5398c4d9f554bae18e">d_rules</a>;
<a name="l00032"></a><a class="code" href="classCVC3_1_1TheoryArith3.html#ab6ea7bdf248ad9f15dbbb2a25c70d53d">00032</a> <a class="code" href="classCVC3_1_1CDO.html">CDO<bool></a> <a class="code" href="classCVC3_1_1TheoryArith3.html#ab6ea7bdf248ad9f15dbbb2a25c70d53d">d_inModelCreation</a>;
<a name="l00033"></a>00033 <span class="comment"></span>
<a name="l00034"></a>00034 <span class="comment"> //! Data class for the strongest free constant in separation inqualities</span>
<a name="l00035"></a><a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html">00035</a> <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> {
<a name="l00036"></a>00036 <span class="keyword">private</span>:
<a name="l00037"></a><a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html#a21b19900b574aa5811f8ff509f462adc">00037</a> <a class="code" href="classCVC3_1_1Rational.html">Rational</a> <a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html#a21b19900b574aa5811f8ff509f462adc">d_r</a>;
<a name="l00038"></a><a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html#abb9b46f53c831589cbd1a43fa8a454ed">00038</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html#abb9b46f53c831589cbd1a43fa8a454ed">d_strict</a>;
<a name="l00039"></a>00039 <span class="keyword">public</span>:
<a name="l00040"></a><a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html#ac351ae05917b9c1cf518def6ebc60931">00040</a> <a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html#ac351ae05917b9c1cf518def6ebc60931">FreeConst</a>() { }
<a name="l00041"></a><a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html#ab6f3c524cdb2b2cb8e690299f347510e">00041</a> <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) { }
<a name="l00042"></a><a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html#a0c5f7aef8c5d3c3e2dbca9a80711a523">00042</a> <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>; }
<a name="l00043"></a><a class="code" href="classCVC3_1_1TheoryArith3_1_1FreeConst.html#a81887e267dfe84df58a876474011601a">00043</a> <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>; }
<a name="l00044"></a>00044 };<span class="comment"></span>
<a name="l00045"></a>00045 <span class="comment"> //! Printing</span>
<a name="l00046"></a>00046 <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);
<a name="l00047"></a>00047 <span class="comment"></span>
<a name="l00048"></a>00048 <span class="comment"> //! Private class for an inequality in the Fourier-Motzkin database</span>
<a name="l00049"></a><a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html">00049</a> <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> {
<a name="l00050"></a>00050 <span class="keyword">private</span>:
<a name="l00051"></a><a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a1f60f98a9ea7af2ab7d88938a75adc9a">00051</a> <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>
<a name="l00052"></a><a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a7771529070ba56e5372268cd6bbf933b">00052</a> <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>
<a name="l00053"></a><a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a74cc096f9bd6c60e0eb03dfd6111eb72">00053</a> <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>
<a name="l00054"></a>00054 <span class="comment"></span><span class="comment"> //! Default constructor is disabled</span>
<a name="l00055"></a><a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a8abbe09b51cd4577f581259521fcd648">00055</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a8abbe09b51cd4577f581259521fcd648" title="Default constructor is disabled.">Ineq</a>() { }
<a name="l00056"></a>00056 <span class="keyword">public</span>:<span class="comment"></span>
<a name="l00057"></a>00057 <span class="comment"> //! Initial constructor. 'r' is taken from the subsumption database.</span>
<a name="l00058"></a><a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a805b109e6c6e114c224bd948a452fa90">00058</a> <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):
<a name="l00059"></a>00059 <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>
<a name="l00060"></a>00060 <span class="comment"> //! Get the inequality</span>
<a name="l00061"></a><a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#ae56ae01b38b372401bd3a8f407093558">00061</a> <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>
<a name="l00062"></a>00062 <span class="comment"> //! Get the max/min constant</span>
<a name="l00063"></a><a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a9207644df8d21b4db1c5e3a88fb2cdfb">00063</a> <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>
<a name="l00064"></a>00064 <span class="comment"> //! Flag whether var is isolated on the RHS</span>
<a name="l00065"></a><a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a7f588540905cfdd00b515ea59c8c0482">00065</a> <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>
<a name="l00066"></a>00066 <span class="comment"> //! Flag whether var is isolated on the LHS</span>
<a name="l00067"></a><a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a3f5d837020af57b45fbaa704727a7e11">00067</a> <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>
<a name="l00068"></a>00068 <span class="comment"> //! Auto-cast to Theorem</span>
<a name="l00069"></a><a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#ae9fce2eb529ed3a936ae93ef87273b0b">00069</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#ae9fce2eb529ed3a936ae93ef87273b0b" title="Auto-cast to Theorem.">operator 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>; }
<a name="l00070"></a>00070 };<span class="comment"></span>
<a name="l00071"></a>00071 <span class="comment"> //! Printing</span>
<a name="l00072"></a>00072 <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);
<a name="l00073"></a>00073 <span class="comment"></span>
<a name="l00074"></a>00074 <span class="comment"> //! Database of inequalities with a variable isolated on the right</span>
<a name="l00075"></a><a class="code" href="classCVC3_1_1TheoryArith3.html#ae907bba6bfb622671693d64fd4f7651b">00075</a> <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>;
<a name="l00076"></a>00076 <span class="comment"></span>
<a name="l00077"></a>00077 <span class="comment"> //! Database of inequalities with a variable isolated on the left</span>
<a name="l00078"></a><a class="code" href="classCVC3_1_1TheoryArith3.html#adef4166f884bc9d39c9649de29ba6223">00078</a> <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>;
<a name="l00079"></a>00079 <span class="comment"></span>
<a name="l00080"></a>00080 <span class="comment"> //! Mapping of inequalities to the largest/smallest free constant</span>
<a name="l00081"></a>00081 <span class="comment"></span><span class="comment"> /*! The Expr is the original inequality with the free constant</span>
<a name="l00082"></a>00082 <span class="comment"> * removed and inequality converted to non-strict (for indexing</span>
<a name="l00083"></a>00083 <span class="comment"> * purposes). I.e. ax<c+t becomes ax<=t. This inequality is mapped</span>
<a name="l00084"></a>00084 <span class="comment"> * to a pair<c,strict>, the smallest (largest for c+t<ax) constant</span>
<a name="l00085"></a>00085 <span class="comment"> * among inequalities with the same 'a', 'x', and 't', and a boolean</span>
<a name="l00086"></a>00086 <span class="comment"> * flag indicating whether the strongest inequality is strict.</span>
<a name="l00087"></a>00087 <span class="comment"> */</span>
<a name="l00088"></a><a class="code" href="classCVC3_1_1TheoryArith3.html#abe31caa3bc2ac4ee941a83870b802ab4">00088</a> <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>;
<a name="l00089"></a>00089
<a name="l00090"></a>00090 <span class="comment">// Input buffer to store the incoming inequalities</span>
<a name="l00091"></a><a class="code" href="classCVC3_1_1TheoryArith3.html#a3875f5f084ebf03733c8f94a4774c536">00091</a> <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>
<a name="l00092"></a>00092 <span class="comment"></span>
<a name="l00093"></a><a class="code" href="classCVC3_1_1TheoryArith3.html#a1e095f1d7e371b227dc08f3b8635c004">00093</a> <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>
<a name="l00094"></a>00094 <span class="comment"></span>
<a name="l00095"></a><a class="code" href="classCVC3_1_1TheoryArith3.html#aa1aa058a244693fbfadaa8326d9573a2">00095</a> <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>
<a name="l00096"></a>00096 <span class="comment"></span>
<a name="l00097"></a>00097 <span class="comment">// Statistics for the variables</span>
<a name="l00098"></a>00098 <span class="comment"></span>
<a name="l00099"></a>00099 <span class="comment"> /*! @brief Mapping of a variable to the number of inequalities where</span>
<a name="l00100"></a>00100 <span class="comment"> the variable would be isolated on the right */</span>
<a name="l00101"></a><a class="code" href="classCVC3_1_1TheoryArith3.html#a6d0840e19aef8d9e2e3eefad3cb5a279">00101</a> <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>;
<a name="l00102"></a>00102 <span class="comment"></span>
<a name="l00103"></a>00103 <span class="comment"> /*! @brief Mapping of a variable to the number of inequalities where</span>
<a name="l00104"></a>00104 <span class="comment"> the variable would be isolated on the left */</span>
<a name="l00105"></a><a class="code" href="classCVC3_1_1TheoryArith3.html#a45bee8f005bbd76195fd207f6e14b530">00105</a> <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>;
<a name="l00106"></a>00106 <span class="comment"></span>
<a name="l00107"></a>00107 <span class="comment"> //! Set of shared terms (for counterexample generation)</span>
<a name="l00108"></a><a class="code" href="classCVC3_1_1TheoryArith3.html#a4e74ec27493ce714497a40de4743a706">00108</a> <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>;
<a name="l00109"></a>00109 <span class="comment"></span>
<a name="l00110"></a>00110 <span class="comment"> //! Set of shared integer variables (i-leaves)</span>
<a name="l00111"></a><a class="code" href="classCVC3_1_1TheoryArith3.html#a333b1082c80655c02182b44a0c4a8dda">00111</a> <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>;
<a name="l00112"></a>00112
<a name="l00113"></a>00113 <span class="comment">//Directed Acyclic Graph representing partial variable ordering for</span>
<a name="l00114"></a>00114 <span class="comment">//variable projection over inequalities.</span>
<a name="l00115"></a><a class="code" href="classCVC3_1_1TheoryArith3_1_1VarOrderGraph.html">00115</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1TheoryArith3_1_1VarOrderGraph.html">VarOrderGraph</a> {
<a name="l00116"></a><a class="code" href="classCVC3_1_1TheoryArith3_1_1VarOrderGraph.html#addddfffbec3000a4203e471639b6bfab">00116</a> <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>;
<a name="l00117"></a><a class="code" href="classCVC3_1_1TheoryArith3_1_1VarOrderGraph.html#a16d50d02f53c31cfa278e25f3f6db518">00117</a> <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>;
<a name="l00118"></a>00118 <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);
<a name="l00119"></a>00119 <span class="keyword">public</span>:
<a name="l00120"></a>00120 <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);
<a name="l00121"></a>00121 <span class="comment">//returns true if e1 < e2, false otherwise.</span>
<a name="l00122"></a>00122 <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);
<a name="l00123"></a>00123 <span class="comment">//selects those variables which are largest and incomparable among</span>
<a name="l00124"></a>00124 <span class="comment">//v1 and puts it into v2</span>
<a name="l00125"></a>00125 <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);
<a name="l00126"></a>00126 <span class="comment">//selects those variables which are smallest and incomparable among</span>
<a name="l00127"></a>00127 <span class="comment">//v1, removes them from v1 and puts them into v2. </span>
<a name="l00128"></a>00128 <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);
<a name="l00129"></a>00129 };
<a name="l00130"></a>00130
<a name="l00131"></a><a class="code" href="classCVC3_1_1TheoryArith3.html#a7b9b0448e5f0149ea33709b1ba392c1e">00131</a> <a class="code" href="classCVC3_1_1TheoryArith3_1_1VarOrderGraph.html">VarOrderGraph</a> <a class="code" href="classCVC3_1_1TheoryArith3.html#a7b9b0448e5f0149ea33709b1ba392c1e">d_graph</a>;
<a name="l00132"></a>00132
<a name="l00133"></a>00133 <span class="comment">// Private methods</span>
<a name="l00134"></a>00134 <span class="comment"></span>
<a name="l00135"></a>00135 <span class="comment"> //! Check the term t for integrality. </span>
<a name="l00136"></a>00136 <span class="comment"></span><span class="comment"> /*! \return a theorem of IS_INTEGER(t) or Null. */</span>
<a name="l00137"></a>00137 <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);
<a name="l00138"></a>00138 <span class="comment"></span>
<a name="l00139"></a>00139 <span class="comment"> //! A helper method for isIntegerThm()</span>
<a name="l00140"></a>00140 <span class="comment"></span><span class="comment"> /*! Check if IS_INTEGER(e) is easily derivable from the given 'thm' */</span>
<a name="l00141"></a>00141 <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);
<a name="l00142"></a>00142 <span class="comment"></span>
<a name="l00143"></a>00143 <span class="comment"> //! Extract the free constant from an inequality</span>
<a name="l00144"></a>00144 <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);
<a name="l00145"></a>00145 <span class="comment"></span>
<a name="l00146"></a>00146 <span class="comment"> //! Update the free constant subsumption database with new inequality</span>
<a name="l00147"></a>00147 <span class="comment"></span><span class="comment"> /*! \return a reference to the max/min constant.</span>
<a name="l00148"></a>00148 <span class="comment"> *</span>
<a name="l00149"></a>00149 <span class="comment"> * Also, sets 'subsumed' argument to true if the inequality is</span>
<a name="l00150"></a>00150 <span class="comment"> * subsumed by an existing inequality.</span>
<a name="l00151"></a>00151 <span class="comment"> */</span>
<a name="l00152"></a>00152 <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,
<a name="l00153"></a>00153 <span class="keywordtype">bool</span>& subsumed);<span class="comment"></span>
<a name="l00154"></a>00154 <span class="comment"> //! Check if the kids of e are fully simplified and canonized (for debugging)</span>
<a name="l00155"></a>00155 <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);
<a name="l00156"></a>00156 <span class="comment"></span>
<a name="l00157"></a>00157 <span class="comment"> //! Canonize the expression e, assuming all children are canonical</span>
<a name="l00158"></a>00158 <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);
<a name="l00159"></a>00159 <span class="comment"></span>
<a name="l00160"></a>00160 <span class="comment"> /*! @brief Canonize and reduce e w.r.t. union-find database; assume</span>
<a name="l00161"></a>00161 <span class="comment"> * all children are canonical */</span>
<a name="l00162"></a>00162 <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);
<a name="l00163"></a>00163 <span class="comment"></span>
<a name="l00164"></a>00164 <span class="comment"> /*! @brief Composition of canonSimplify(const Expr&) by</span>
<a name="l00165"></a>00165 <span class="comment"> * transitivity: take e0 = e1, canonize and simplify e1 to e2,</span>
<a name="l00166"></a>00166 <span class="comment"> * return e0 = e2. */</span>
<a name="l00167"></a><a class="code" href="classCVC3_1_1TheoryArith3.html#aaef92a86079cf95107c7c4552fe77a34">00167</a> <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) {
<a name="l00168"></a>00168 <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>()));
<a name="l00169"></a>00169 }
<a name="l00170"></a>00170 <span class="comment"></span>
<a name="l00171"></a>00171 <span class="comment"> //! Canonize predicate (x = y, x < y, etc.)</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_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);
<a name="l00173"></a>00173 <span class="comment"></span>
<a name="l00174"></a>00174 <span class="comment"> //! Canonize predicate like canonPred except that the input theorem</span>
<a name="l00175"></a>00175 <span class="comment"> //! is an equivalent transformation.</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_1TheoryArith3.html#ac0c4f725256399640c17b0783fec9f13">canonPredEquiv</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);
<a name="l00177"></a>00177 <span class="comment"></span>
<a name="l00178"></a>00178 <span class="comment"> //! Solve an equation and return an equivalent Theorem in the solved form</span>
<a name="l00179"></a>00179 <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);
<a name="l00180"></a>00180 <span class="comment"></span>
<a name="l00181"></a>00181 <span class="comment"> //! takes in a conjunction equivalence Thm and canonizes it.</span>
<a name="l00182"></a>00182 <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);
<a name="l00183"></a>00183 <span class="comment"></span>
<a name="l00184"></a>00184 <span class="comment"> //! picks the monomial with the smallest abs(coeff) from the input</span>
<a name="l00185"></a>00185 <span class="comment"></span> <span class="comment">//integer equation.</span>
<a name="l00186"></a>00186 <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);
<a name="l00187"></a>00187 <span class="comment"></span>
<a name="l00188"></a>00188 <span class="comment"> //! processes equalities with 1 or more vars of type REAL</span>
<a name="l00189"></a>00189 <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);
<a name="l00190"></a>00190 <span class="comment"></span>
<a name="l00191"></a>00191 <span class="comment"> //! processes equalities whose vars are all of type INT</span>
<a name="l00192"></a>00192 <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);
<a name="l00193"></a>00193 <span class="comment"></span>
<a name="l00194"></a>00194 <span class="comment"> //! One step of INT equality processing (aux. method for processIntEq())</span>
<a name="l00195"></a>00195 <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);
<a name="l00196"></a>00196 <span class="comment"></span>
<a name="l00197"></a>00197 <span class="comment"> //! Process inequalities in the buffer</span>
<a name="l00198"></a>00198 <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>();
<a name="l00199"></a>00199 <span class="comment"></span>
<a name="l00200"></a>00200 <span class="comment"> //! Take an inequality and isolate a variable</span>
<a name="l00201"></a>00201 <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);
<a name="l00202"></a>00202 <span class="comment"></span>
<a name="l00203"></a>00203 <span class="comment"> //! Update the statistics counters for the variable with a coeff. c</span>
<a name="l00204"></a>00204 <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);
<a name="l00205"></a>00205 <span class="comment"></span>
<a name="l00206"></a>00206 <span class="comment"> //! Update the statistics counters for the monomial</span>
<a name="l00207"></a>00207 <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);
<a name="l00208"></a>00208 <span class="comment"></span>
<a name="l00209"></a>00209 <span class="comment"> //! Add an inequality to the input buffer. See also d_buffer</span>
<a name="l00210"></a>00210 <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);
<a name="l00211"></a>00211 <span class="comment"></span>
<a name="l00212"></a>00212 <span class="comment"> /*! @brief Given a canonized term, compute a factor to make all</span>
<a name="l00213"></a>00213 <span class="comment"> coefficients integer and relatively prime */</span>
<a name="l00214"></a>00214 <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);
<a name="l00215"></a>00215 <span class="comment"></span>
<a name="l00216"></a>00216 <span class="comment"> //! Normalize an equation (make all coefficients rel. prime integers)</span>
<a name="l00217"></a>00217 <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);
<a name="l00218"></a>00218 <span class="comment"></span>
<a name="l00219"></a>00219 <span class="comment"> //! Normalize an equation (make all coefficients rel. prime integers)</span>
<a name="l00220"></a>00220 <span class="comment"></span><span class="comment"> /*! accepts a rewrite theorem over eqn|ineqn and normalizes it</span>
<a name="l00221"></a>00221 <span class="comment"> * and returns a theorem to that effect.</span>
<a name="l00222"></a>00222 <span class="comment"> */</span>
<a name="l00223"></a>00223 <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);
<a name="l00224"></a>00224
<a name="l00225"></a>00225 <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>);
<a name="l00226"></a>00226
<a name="l00227"></a>00227 <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);
<a name="l00228"></a>00228
<a name="l00229"></a>00229 <span class="keyword">public</span>: <span class="comment">// ArithTheoremProducer needs this function, so make it public</span><span class="comment"></span>
<a name="l00230"></a>00230 <span class="comment"> //! Separate monomial e = c*p1*...*pn into c and 1*p1*...*pn</span>
<a name="l00231"></a>00231 <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>
<a name="l00232"></a>00232 <span class="comment"> //! Check the term t for integrality (return bool)</span>
<a name="l00233"></a><a class="code" href="classCVC3_1_1TheoryArith3.html#addd34c5d0ee1bdab0ecbbc92ebd0f175">00233</a> <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>()); }
<a name="l00234"></a>00234
<a name="l00235"></a>00235
<a name="l00236"></a>00236 <span class="keyword">private</span>:
<a name="l00237"></a>00237
<a name="l00238"></a>00238 <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);
<a name="l00239"></a>00239 <span class="comment"></span>
<a name="l00240"></a>00240 <span class="comment"> //! Check if the term expression is "stale"</span>
<a name="l00241"></a>00241 <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);
<a name="l00242"></a>00242 <span class="comment"></span>
<a name="l00243"></a>00243 <span class="comment"> //! Check if the inequality is "stale" or subsumed</span>
<a name="l00244"></a>00244 <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);
<a name="l00245"></a>00245
<a name="l00246"></a>00246 <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);
<a name="l00247"></a>00247
<a name="l00248"></a>00248 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#ab88556951a1e36e72efb357ed5ff8231">assignVariables</a>(std::vector<Expr>&v);
<a name="l00249"></a>00249
<a name="l00250"></a>00250 <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,
<a name="l00251"></a>00251 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& var,
<a name="l00252"></a>00252 <a class="code" href="classCVC3_1_1Rational.html">Rational</a> &r);
<a name="l00253"></a>00253
<a name="l00254"></a>00254 <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);
<a name="l00255"></a>00255
<a name="l00256"></a>00256 <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,
<a name="l00257"></a>00257 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& ineqThm2);
<a name="l00258"></a>00258 <span class="comment"></span>
<a name="l00259"></a>00259 <span class="comment"> //! Take a system of equations and turn it into a solved form</span>
<a name="l00260"></a>00260 <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);
<a name="l00261"></a>00261 <span class="comment"></span>
<a name="l00262"></a>00262 <span class="comment"> /*! @brief Substitute all vars in term 't' according to the</span>
<a name="l00263"></a>00263 <span class="comment"> * substitution 'subst' and canonize the result.</span>
<a name="l00264"></a>00264 <span class="comment"> */</span>
<a name="l00265"></a>00265 <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);
<a name="l00266"></a>00266 <span class="comment"></span>
<a name="l00267"></a>00267 <span class="comment"> /*! @brief Substitute all vars in the RHS of the equation 'eq' of</span>
<a name="l00268"></a>00268 <span class="comment"> * the form (x = t) according to the substitution 'subst', and</span>
<a name="l00269"></a>00269 <span class="comment"> * canonize the result.</span>
<a name="l00270"></a>00270 <span class="comment"> */</span>
<a name="l00271"></a>00271 <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);
<a name="l00272"></a>00272 <span class="comment"></span>
<a name="l00273"></a>00273 <span class="comment"> //! Traverse 'e' and push all the i-leaves into 'vars' vector</span>
<a name="l00274"></a>00274 <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,
<a name="l00275"></a>00275 std::set<Expr>& cache);
<a name="l00276"></a>00276 <span class="comment"></span>
<a name="l00277"></a>00277 <span class="comment"> /*! @brief Check if alpha <= ax & bx <= beta is a finite interval</span>
<a name="l00278"></a>00278 <span class="comment"> * for integer var 'x', and assert the corresponding constraint</span>
<a name="l00279"></a>00279 <span class="comment"> */</span>
<a name="l00280"></a>00280 <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,
<a name="l00281"></a>00281 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& bxLEbeta);
<a name="l00282"></a>00282 <span class="comment"></span>
<a name="l00283"></a>00283 <span class="comment"> //! For an integer var 'x', find and process all constraints A <= ax <= A+c </span>
<a name="l00284"></a>00284 <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);
<a name="l00285"></a>00285 <span class="comment"></span>
<a name="l00286"></a>00286 <span class="comment"> //! Recursive setup for isolated inequalities (and other new expressions)</span>
<a name="l00287"></a>00287 <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);
<a name="l00288"></a>00288
<a name="l00289"></a>00289 <span class="keyword">public</span>:
<a name="l00290"></a>00290 <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);
<a name="l00291"></a>00291 <a class="code" href="classCVC3_1_1TheoryArith3.html#a6ce33109bdf13407e2c36a6e608132cd">~TheoryArith3</a>();
<a name="l00292"></a>00292
<a name="l00293"></a>00293 <span class="comment">// Trusted method that creates the proof rules class (used in constructor).</span>
<a name="l00294"></a>00294 <span class="comment">// Implemented in arith_theorem_producer.cpp</span>
<a name="l00295"></a>00295 <a class="code" href="classCVC3_1_1ArithProofRules.html">ArithProofRules</a>* <a class="code" href="classCVC3_1_1TheoryArith3.html#af8a9ccde61831efd7b0e9093ed1d9770">createProofRules3</a>();
<a name="l00296"></a>00296
<a name="l00297"></a>00297 <span class="comment">// Theory interface</span>
<a name="l00298"></a>00298 <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);
<a name="l00299"></a>00299 <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);
<a name="l00300"></a>00300 <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>();
<a name="l00301"></a>00301 <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);
<a name="l00302"></a>00302 <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);
<a name="l00303"></a>00303 <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);
<a name="l00304"></a>00304 <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);
<a name="l00305"></a>00305 <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);
<a name="l00306"></a>00306 <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);
<a name="l00307"></a>00307 <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);
<a name="l00308"></a>00308 <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);
<a name="l00309"></a>00309 <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);
<a name="l00310"></a>00310 <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,
<a name="l00311"></a>00311 <span class="keywordtype">bool</span> enumerate, <span class="keywordtype">bool</span> computeSize);
<a name="l00312"></a>00312 <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);
<a name="l00313"></a>00313 <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);
<a name="l00314"></a>00314 <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);
<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_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);
<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_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);
<a name="l00317"></a>00317 <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);
<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_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);
<a name="l00319"></a>00319
<a name="l00320"></a>00320 <span class="keyword">private</span>:
<a name="l00321"></a>00321 <span class="comment"></span>
<a name="l00322"></a>00322 <span class="comment"> /** Map from variables to the maximal (by absolute value) of one of it's coefficients */</span>
<a name="l00323"></a><a class="code" href="classCVC3_1_1TheoryArith3.html#aaafeb6382856c921da73af220df2ab1b">00323</a> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, Rational></a> <a class="code" href="classCVC3_1_1TheoryArith3.html#aaafeb6382856c921da73af220df2ab1b">maxCoefficientLeft</a>;
<a name="l00324"></a><a class="code" href="classCVC3_1_1TheoryArith3.html#a53ede9d74a99ac939974d488b146d13f">00324</a> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, Rational></a> <a class="code" href="classCVC3_1_1TheoryArith3.html#a53ede9d74a99ac939974d488b146d13f">maxCoefficientRight</a>;
<a name="l00325"></a>00325 <span class="comment"></span>
<a name="l00326"></a>00326 <span class="comment"> /** Map from variables to the fixed value of one of it's coefficients */</span>
<a name="l00327"></a><a class="code" href="classCVC3_1_1TheoryArith3.html#acefeaa2f3e7b84414fb92b90ab6364cb">00327</a> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, Rational></a> <a class="code" href="classCVC3_1_1TheoryArith3.html#acefeaa2f3e7b84414fb92b90ab6364cb">fixedMaxCoefficient</a>;
<a name="l00328"></a>00328 <span class="comment"></span>
<a name="l00329"></a>00329 <span class="comment"> /** </span>
<a name="l00330"></a>00330 <span class="comment"> * Returns the current maximal coefficient of the variable.</span>
<a name="l00331"></a>00331 <span class="comment"> * </span>
<a name="l00332"></a>00332 <span class="comment"> * @param var the variable.</span>
<a name="l00333"></a>00333 <span class="comment"> */</span>
<a name="l00334"></a>00334 <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);
<a name="l00335"></a>00335 <span class="comment"></span>
<a name="l00336"></a>00336 <span class="comment"> /**</span>
<a name="l00337"></a>00337 <span class="comment"> * Fixes the current max coefficient to be used in the ordering. If the maximal coefficient</span>
<a name="l00338"></a>00338 <span class="comment"> * changes in the future, it will not be used in the ordering.</span>
<a name="l00339"></a>00339 <span class="comment"> * </span>
<a name="l00340"></a>00340 <span class="comment"> * @param variable the variable</span>
<a name="l00341"></a>00341 <span class="comment"> * @param max the value to set it to</span>
<a name="l00342"></a>00342 <span class="comment"> */</span>
<a name="l00343"></a>00343 <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#a03dcd07dcbd01da970af13f1dfc5e2dd">max</a>);
<a name="l00344"></a>00344 <span class="comment"></span>
<a name="l00345"></a>00345 <span class="comment"> /**</span>
<a name="l00346"></a>00346 <span class="comment"> * Among given input variables, select the smallest ones with respect to the coefficients.</span>
<a name="l00347"></a>00347 <span class="comment"> */</span>
<a name="l00348"></a>00348 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArith3.html#a21438a9cc9b82b7c6cf3b269b663a8d0">selectSmallestByCoefficient</a>(std::vector<Expr> input, std::vector<Expr>& output);
<a name="l00349"></a>00349 };
<a name="l00350"></a>00350
<a name="l00351"></a>00351 }
<a name="l00352"></a>00352
<a name="l00353"></a>00353 <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>
