<!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_arith_new.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_arith_new.h</div> </div>
</div>
<div class="contents">
<a href="theory__arith__new_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_arith_new.h</span>
<a name="l00004"></a>00004 <span class="comment"> * </span>
<a name="l00005"></a>00005 <span class="comment"> * Author: Dejan Jovanovic</span>
<a name="l00006"></a>00006 <span class="comment"> *</span>
<a name="l00007"></a>00007 <span class="comment"> * Created: Thu Jun 14 13:38:16 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_arith_new_h_</span>
<a name="l00022"></a>00022 <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__include__theory_arith_new_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="preprocessor">#include <<a class="code" href="hash__fun_8h.html" title="hash functions">hash_fun.h</a>></span>
<a name="l00027"></a>00027 <span class="preprocessor">#include <<a class="code" href="hash__map_8h.html" title="hash map implementation">hash_map.h</a>></span>
<a name="l00028"></a>00028 <span class="preprocessor">#include <<a class="code" href="queryresult_8h.html" title="enumerated type for result of queries">queryresult.h</a>></span>
<a name="l00029"></a>00029 <span class="preprocessor">#include <map></span>
<a name="l00030"></a>00030
<a name="l00031"></a>00031 <span class="keyword">namespace </span>CVC3 {
<a name="l00032"></a>00032
<a name="l00033"></a>00033 <span class="comment"></span>
<a name="l00034"></a>00034 <span class="comment">/**</span>
<a name="l00035"></a>00035 <span class="comment"> * This theory handles basic linear arithmetic.</span>
<a name="l00036"></a>00036 <span class="comment"> *</span>
<a name="l00037"></a>00037 <span class="comment"> * @author Clark Barrett</span>
<a name="l00038"></a>00038 <span class="comment"> * </span>
<a name="l00039"></a>00039 <span class="comment"> * @since Sat Feb 8 14:44:32 2003</span>
<a name="l00040"></a>00040 <span class="comment"> */</span>
<a name="l00041"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html">00041</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1TheoryArithNew.html">TheoryArithNew</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="l00042"></a>00042 <span class="comment"></span>
<a name="l00043"></a>00043 <span class="comment"> /** For concrete model generation */</span>
<a name="l00044"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#a7f402d265d6f783bbc4139ba3dddd9db">00044</a> <a class="code" href="classCVC3_1_1CDList.html">CDList<Theorem></a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a7f402d265d6f783bbc4139ba3dddd9db">d_diseq</a>;<span class="comment"></span>
<a name="l00045"></a>00045 <span class="comment"> /** Index to the next unprocessed disequality */</span>
<a name="l00046"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#a40a1d8f8e7d2faf4ddffe3ca14a90e88">00046</a> <a class="code" href="classCVC3_1_1CDO.html">CDO<size_t></a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a40a1d8f8e7d2faf4ddffe3ca14a90e88">d_diseqIdx</a>;
<a name="l00047"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#a1fb30358f2875620fef664227f0d3d5e">00047</a> <a class="code" href="classCVC3_1_1ArithProofRules.html">ArithProofRules</a>* <a class="code" href="classCVC3_1_1TheoryArithNew.html#a1fb30358f2875620fef664227f0d3d5e">d_rules</a>;
<a name="l00048"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#ae29425ad828a82acb991db1ab50e8dd7">00048</a> <a class="code" href="classCVC3_1_1CDO.html">CDO<bool></a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#ae29425ad828a82acb991db1ab50e8dd7">d_inModelCreation</a>;
<a name="l00049"></a>00049 <span class="comment"></span>
<a name="l00050"></a>00050 <span class="comment"> /** Data class for the strongest free constant in separation inqualities **/</span>
<a name="l00051"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1FreeConst.html">00051</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1TheoryArithNew_1_1FreeConst.html">FreeConst</a> {
<a name="l00052"></a>00052 <span class="keyword">private</span>:
<a name="l00053"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1FreeConst.html#aa43789984c5e26235d744841b33a88bd">00053</a> <a class="code" href="classCVC3_1_1Rational.html">Rational</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1FreeConst.html#aa43789984c5e26235d744841b33a88bd">d_r</a>;
<a name="l00054"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1FreeConst.html#a5dc7303936808750bad632a25617653b">00054</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1FreeConst.html#a5dc7303936808750bad632a25617653b">d_strict</a>;
<a name="l00055"></a>00055 <span class="keyword">public</span>:
<a name="l00056"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1FreeConst.html#a992af10cf6690a5d73e0e9fcfc4b73e9">00056</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1FreeConst.html#a992af10cf6690a5d73e0e9fcfc4b73e9">FreeConst</a>() { }
<a name="l00057"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1FreeConst.html#a311d658e3f5aeade49ec35069774f1a9">00057</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1FreeConst.html#a311d658e3f5aeade49ec35069774f1a9">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_1TheoryArithNew_1_1FreeConst.html#a65e61d15258614bc371cf45954388092">strict</a>): <a class="code" href="classCVC3_1_1TheoryArithNew_1_1FreeConst.html#aa43789984c5e26235d744841b33a88bd">d_r</a>(r), <a class="code" href="classCVC3_1_1TheoryArithNew_1_1FreeConst.html#a5dc7303936808750bad632a25617653b">d_strict</a>(strict) { }
<a name="l00058"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1FreeConst.html#a15979fe7b9d6e2d90cece50ba47286b1">00058</a> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Rational.html">Rational</a>& <a class="code" href="classCVC3_1_1TheoryArithNew_1_1FreeConst.html#a15979fe7b9d6e2d90cece50ba47286b1">getConst</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1FreeConst.html#aa43789984c5e26235d744841b33a88bd">d_r</a>; }
<a name="l00059"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1FreeConst.html#a65e61d15258614bc371cf45954388092">00059</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1FreeConst.html#a65e61d15258614bc371cf45954388092">strict</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1FreeConst.html#a5dc7303936808750bad632a25617653b">d_strict</a>; }
<a name="l00060"></a>00060 };<span class="comment"></span>
<a name="l00061"></a>00061 <span class="comment"> //! Printing</span>
<a name="l00062"></a>00062 <span class="comment"></span> <span class="keyword">friend</span> std::ostream& <a class="code" href="classCVC3_1_1TheoryArithNew.html#a24b0687e8f0fa36a6d5bacc8155517e2" title="Printing.">operator<<</a>(std::ostream& os, <span class="keyword">const</span> FreeConst& fc);<span class="comment"></span>
<a name="l00063"></a>00063 <span class="comment"> //! Private class for an inequality in the Fourier-Motzkin database</span>
<a name="l00064"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html">00064</a> <span class="comment"></span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html" title="Private class for an inequality in the Fourier-Motzkin database.">Ineq</a> {
<a name="l00065"></a>00065 <span class="keyword">private</span>:
<a name="l00066"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html#ae2595281fd986de92d1f6838652e0e78">00066</a> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html#ae2595281fd986de92d1f6838652e0e78" title="The inequality.">d_ineq</a>; <span class="comment">//!< The inequality</span>
<a name="l00067"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html#afc355c2951050daef4cc1d7d43b58a64">00067</a> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html#afc355c2951050daef4cc1d7d43b58a64" title="Var is isolated on the RHS.">d_rhs</a>; <span class="comment">//!< Var is isolated on the RHS</span>
<a name="l00068"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html#a31ffd5476bfd8a5251a16ca80e93df6f">00068</a> <span class="comment"></span> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1FreeConst.html">FreeConst</a>* <a class="code" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html#a31ffd5476bfd8a5251a16ca80e93df6f">d_const</a>; <span class="comment">//!< The max/min const for subsumption check</span>
<a name="l00069"></a>00069 <span class="comment"></span><span class="comment"> //! Default constructor is disabled</span>
<a name="l00070"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html#a53222bef2f8bca064395eb61e51af45e">00070</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html#a53222bef2f8bca064395eb61e51af45e" title="Default constructor is disabled.">Ineq</a>() { }
<a name="l00071"></a>00071 <span class="keyword">public</span>:<span class="comment"></span>
<a name="l00072"></a>00072 <span class="comment"> //! Initial constructor. 'r' is taken from the subsumption database.</span>
<a name="l00073"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html#a230c7a36753e0acc09633d56dbeafe3b">00073</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html#a53222bef2f8bca064395eb61e51af45e" 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_1TheoryArithNew_1_1Ineq.html#acb2e06a2e5eccac4b72d8b4d88f13bdd" title="Get the inequality.">ineq</a>, <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html#abfbee8f90a20d877971571b814bccfc1" title="Flag whether var is isolated on the RHS.">varOnRHS</a>, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1FreeConst.html">FreeConst</a>& c):
<a name="l00074"></a>00074 <a class="code" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html#ae2595281fd986de92d1f6838652e0e78" title="The inequality.">d_ineq</a>(ineq), <a class="code" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html#afc355c2951050daef4cc1d7d43b58a64" title="Var is isolated on the RHS.">d_rhs</a>(varOnRHS), <a class="code" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html#a31ffd5476bfd8a5251a16ca80e93df6f">d_const</a>(&c) { }<span class="comment"></span>
<a name="l00075"></a>00075 <span class="comment"> //! Get the inequality</span>
<a name="l00076"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html#acb2e06a2e5eccac4b72d8b4d88f13bdd">00076</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_1TheoryArithNew_1_1Ineq.html#acb2e06a2e5eccac4b72d8b4d88f13bdd" title="Get the inequality.">ineq</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html#ae2595281fd986de92d1f6838652e0e78" title="The inequality.">d_ineq</a>; }<span class="comment"></span>
<a name="l00077"></a>00077 <span class="comment"> //! Get the max/min constant</span>
<a name="l00078"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html#a20f1455cf46f6e86f0175508f92e8aff">00078</a> <span class="comment"></span> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1FreeConst.html">FreeConst</a>& <a class="code" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html#a20f1455cf46f6e86f0175508f92e8aff" title="Get the max/min constant.">getConst</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> *<a class="code" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html#a31ffd5476bfd8a5251a16ca80e93df6f">d_const</a>; }<span class="comment"></span>
<a name="l00079"></a>00079 <span class="comment"> //! Flag whether var is isolated on the RHS</span>
<a name="l00080"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html#abfbee8f90a20d877971571b814bccfc1">00080</a> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html#abfbee8f90a20d877971571b814bccfc1" 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_1TheoryArithNew_1_1Ineq.html#afc355c2951050daef4cc1d7d43b58a64" title="Var is isolated on the RHS.">d_rhs</a>; }<span class="comment"></span>
<a name="l00081"></a>00081 <span class="comment"> //! Flag whether var is isolated on the LHS</span>
<a name="l00082"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html#a987945938565d6d6f00d1ca3ebbd125a">00082</a> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html#a987945938565d6d6f00d1ca3ebbd125a" 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_1TheoryArithNew_1_1Ineq.html#afc355c2951050daef4cc1d7d43b58a64" title="Var is isolated on the RHS.">d_rhs</a>; }<span class="comment"></span>
<a name="l00083"></a>00083 <span class="comment"> //! Auto-cast to Theorem</span>
<a name="l00084"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html#ae4c7795f466e160656ebc928608a7fd2">00084</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html#ae4c7795f466e160656ebc928608a7fd2" title="Auto-cast to Theorem.">operator Theorem</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html#ae2595281fd986de92d1f6838652e0e78" title="The inequality.">d_ineq</a>; }
<a name="l00085"></a>00085 };<span class="comment"></span>
<a name="l00086"></a>00086 <span class="comment"> //! Printing</span>
<a name="l00087"></a>00087 <span class="comment"></span> <span class="keyword">friend</span> std::ostream& <a class="code" href="classCVC3_1_1TheoryArithNew.html#a24b0687e8f0fa36a6d5bacc8155517e2" title="Printing.">operator<<</a>(std::ostream& os, <span class="keyword">const</span> Ineq& ineq);<span class="comment"></span>
<a name="l00088"></a>00088 <span class="comment"> //! Database of inequalities with a variable isolated on the right</span>
<a name="l00089"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#acb102f87cd4bcdba4d404a6951eac0aa">00089</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<CDList<Ineq></a> *> <a class="code" href="classCVC3_1_1TheoryArithNew.html#acb102f87cd4bcdba4d404a6951eac0aa" title="Database of inequalities with a variable isolated on the right.">d_inequalitiesRightDB</a>;<span class="comment"></span>
<a name="l00090"></a>00090 <span class="comment"> //! Database of inequalities with a variable isolated on the left</span>
<a name="l00091"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#a74167d750ba8d8cc8b0ec520e8a41894">00091</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<CDList<Ineq></a> *> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a74167d750ba8d8cc8b0ec520e8a41894" title="Database of inequalities with a variable isolated on the left.">d_inequalitiesLeftDB</a>;<span class="comment"></span>
<a name="l00092"></a>00092 <span class="comment"> //! Mapping of inequalities to the largest/smallest free constant</span>
<a name="l00093"></a>00093 <span class="comment"></span><span class="comment"> /*! The Expr is the original inequality with the free constant</span>
<a name="l00094"></a>00094 <span class="comment"> * removed and inequality converted to non-strict (for indexing</span>
<a name="l00095"></a>00095 <span class="comment"> * purposes). I.e. ax<c+t becomes ax<=t. This inequality is mapped</span>
<a name="l00096"></a>00096 <span class="comment"> * to a pair<c,strict>, the smallest (largest for c+t<ax) constant</span>
<a name="l00097"></a>00097 <span class="comment"> * among inequalities with the same 'a', 'x', and 't', and a boolean</span>
<a name="l00098"></a>00098 <span class="comment"> * flag indicating whether the strongest inequality is strict.</span>
<a name="l00099"></a>00099 <span class="comment"> */</span>
<a name="l00100"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#ab5a2165c11bc6867c349627682291fcf">00100</a> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, FreeConst></a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#ab5a2165c11bc6867c349627682291fcf" title="Mapping of inequalities to the largest/smallest free constant.">d_freeConstDB</a>;
<a name="l00101"></a>00101 <span class="comment">// Input buffer to store the incoming inequalities</span>
<a name="l00102"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#a2f0dca2d2952728c2556f8d255cfb008">00102</a> <a class="code" href="classCVC3_1_1CDList.html">CDList<Theorem></a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a2f0dca2d2952728c2556f8d255cfb008" title="Buffer of input inequalities.">d_buffer</a>; <span class="comment">//!< Buffer of input inequalities</span>
<a name="l00103"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#a9a394c94c0607e645c355489631ed690">00103</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<size_t></a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a9a394c94c0607e645c355489631ed690" title="Buffer index of the next unprocessed inequality.">d_bufferIdx</a>; <span class="comment">//!< Buffer index of the next unprocessed inequality</span>
<a name="l00104"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#a2f0bafe4d3eddd28d9d9484318c17e45">00104</a> <span class="comment"></span> <span class="keyword">const</span> <span class="keywordtype">int</span>* <a class="code" href="classCVC3_1_1TheoryArithNew.html#a2f0bafe4d3eddd28d9d9484318c17e45" title="Threshold when the buffer must be processed.">d_bufferThres</a>; <span class="comment">//!< Threshold when the buffer must be processed</span>
<a name="l00105"></a>00105 <span class="comment"></span> <span class="comment">// Statistics for the variables</span><span class="comment"></span>
<a name="l00106"></a>00106 <span class="comment"> /*! @brief Mapping of a variable to the number of inequalities where</span>
<a name="l00107"></a>00107 <span class="comment"> the variable would be isolated on the right */</span>
<a name="l00108"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#ad568a72b85a6bc0c70dfe14d279c9360">00108</a> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, int></a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#ad568a72b85a6bc0c70dfe14d279c9360" title="Mapping of a variable to the number of inequalities where the variable would be isolated on the right...">d_countRight</a>;<span class="comment"></span>
<a name="l00109"></a>00109 <span class="comment"> /*! @brief Mapping of a variable to the number of inequalities where</span>
<a name="l00110"></a>00110 <span class="comment"> the variable would be isolated on the left */</span>
<a name="l00111"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#add35a93fae75084ae5b77f1995477c77">00111</a> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, int></a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#add35a93fae75084ae5b77f1995477c77" title="Mapping of a variable to the number of inequalities where the variable would be isolated on the left...">d_countLeft</a>;<span class="comment"></span>
<a name="l00112"></a>00112 <span class="comment"> //! Set of shared terms (for counterexample generation)</span>
<a name="l00113"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#a6d0b6ef62c9feb4df9c71f2c11912b54">00113</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, bool></a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a6d0b6ef62c9feb4df9c71f2c11912b54" title="Set of shared terms (for counterexample generation)">d_sharedTerms</a>;<span class="comment"></span>
<a name="l00114"></a>00114 <span class="comment"> //! Set of shared integer variables (i-leaves)</span>
<a name="l00115"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#a7ae009f0e7ba96e071f45d9e1094c522">00115</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, bool></a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a7ae009f0e7ba96e071f45d9e1094c522" title="Set of shared integer variables (i-leaves)">d_sharedVars</a>;
<a name="l00116"></a>00116 <span class="comment">//Directed Acyclic Graph representing partial variable ordering for</span>
<a name="l00117"></a>00117 <span class="comment">//variable projection over inequalities.</span>
<a name="l00118"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1VarOrderGraph.html">00118</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1TheoryArithNew_1_1VarOrderGraph.html">VarOrderGraph</a> {
<a name="l00119"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1VarOrderGraph.html#ae941ea5380a21489aec365491e1b01ad">00119</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<std::vector<Expr></a> > <a class="code" href="classCVC3_1_1TheoryArithNew_1_1VarOrderGraph.html#ae941ea5380a21489aec365491e1b01ad">d_edges</a>;
<a name="l00120"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1VarOrderGraph.html#a34782de844ce31846dc6e3a72ff5760d">00120</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<bool></a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1VarOrderGraph.html#a34782de844ce31846dc6e3a72ff5760d">d_cache</a>;
<a name="l00121"></a>00121 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1VarOrderGraph.html#a2c7ec95ab41126a24fdd6370bcc20ee9">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="l00122"></a>00122 <span class="keyword">public</span>:
<a name="l00123"></a>00123 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1VarOrderGraph.html#a047107a1c6275d2eda161726a769a1f3">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="l00124"></a>00124 <span class="comment">//returns true if e1 < e2, false otherwise.</span>
<a name="l00125"></a>00125 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1VarOrderGraph.html#adbe5f447bda4db9d24dea612494c96f6">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="l00126"></a>00126 <span class="comment">//selects those variables which are largest and incomparable among</span>
<a name="l00127"></a>00127 <span class="comment">//v1 and puts it into v2</span>
<a name="l00128"></a>00128 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1VarOrderGraph.html#adabb8b1c5400e95cd7787f4965b33c82">selectLargest</a>(<span class="keyword">const</span> std::vector<Expr>& v1, std::vector<Expr>& v2);
<a name="l00129"></a>00129 <span class="comment">//selects those variables which are smallest and incomparable among</span>
<a name="l00130"></a>00130 <span class="comment">//v1, removes them from v1 and puts them into v2. </span>
<a name="l00131"></a>00131 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1VarOrderGraph.html#a18495afcef8aa0a2556214f5743dbc53">selectSmallest</a>( std::vector<Expr>& v1, std::vector<Expr>& v2);
<a name="l00132"></a>00132
<a name="l00133"></a>00133 };
<a name="l00134"></a>00134
<a name="l00135"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#aed79ec63593f899733e76790d28d4a62">00135</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1VarOrderGraph.html">VarOrderGraph</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#aed79ec63593f899733e76790d28d4a62">d_graph</a>;
<a name="l00136"></a>00136
<a name="l00137"></a>00137 <span class="comment">// Private methods</span><span class="comment"></span>
<a name="l00138"></a>00138 <span class="comment"> //! Check the term t for integrality. </span>
<a name="l00139"></a>00139 <span class="comment"></span><span class="comment"> /*! \return a theorem of IS_INTEGER(t) or Null. */</span>
<a name="l00140"></a>00140 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a1f78d51287d2a25282a94b7bb09d7932" 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);<span class="comment"></span>
<a name="l00141"></a>00141 <span class="comment"> //! A helper method for isIntegerThm()</span>
<a name="l00142"></a>00142 <span class="comment"></span><span class="comment"> /*! Check if IS_INTEGER(e) is easily derivable from the given 'thm' */</span>
<a name="l00143"></a>00143 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#aedd0b63568ada4ac3ddbc515e882a617" 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);<span class="comment"></span>
<a name="l00144"></a>00144 <span class="comment"> //! Check if the kids of e are fully simplified and canonized (for debugging)</span>
<a name="l00145"></a>00145 <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a89696e5cdd27e0e15711a7b9a027c205" 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="l00146"></a>00146 <span class="comment"></span>
<a name="l00147"></a>00147 <span class="comment"> //! Canonize the expression e, assuming all children are canonical</span>
<a name="l00148"></a>00148 <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a453194ac83f105514a4d95fca44bd08e" 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);<span class="comment"></span>
<a name="l00149"></a>00149 <span class="comment"> /*! @brief Canonize and reduce e w.r.t. union-find database; assume</span>
<a name="l00150"></a>00150 <span class="comment"> * all children are canonical */</span>
<a name="l00151"></a>00151 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#aeb8051f2049c78b1b007e274288fcc3b" 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);<span class="comment"></span>
<a name="l00152"></a>00152 <span class="comment"> /*! @brief Composition of canonSimplify(const Expr&) by</span>
<a name="l00153"></a>00153 <span class="comment"> * transitivity: take e0 = e1, canonize and simplify e1 to e2,</span>
<a name="l00154"></a>00154 <span class="comment"> * return e0 = e2. */</span>
<a name="l00155"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#a2a7779383e5e73671e5b29978f106c0d">00155</a> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a2a7779383e5e73671e5b29978f106c0d" 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="l00156"></a>00156 <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_1TheoryArithNew.html#aeb8051f2049c78b1b007e274288fcc3b" 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="l00157"></a>00157 }<span class="comment"></span>
<a name="l00158"></a>00158 <span class="comment"> //! Canonize predicate (x = y, x < y, etc.)</span>
<a name="l00159"></a>00159 <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a48756ab6f45691b827fc4e5545651778" 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);<span class="comment"></span>
<a name="l00160"></a>00160 <span class="comment"> //! Canonize predicate like canonPred except that the input theorem</span>
<a name="l00161"></a>00161 <span class="comment"> //! is an equivalent transformation.</span>
<a name="l00162"></a>00162 <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a18e20adf514c858e9cfeb535e545fb06">canonPredEquiv</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);<span class="comment"></span>
<a name="l00163"></a>00163 <span class="comment"> //! Solve an equation and return an equivalent Theorem in the solved form</span>
<a name="l00164"></a>00164 <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#ab43a4690bbc1cbe62a368efa7816de4a" 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);<span class="comment"></span>
<a name="l00165"></a>00165 <span class="comment"> //! takes in a conjunction equivalence Thm and canonizes it.</span>
<a name="l00166"></a>00166 <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a1e1a47d2be625ad62ac79da63678dc26" 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);<span class="comment"></span>
<a name="l00167"></a>00167 <span class="comment"> //! picks the monomial with the smallest abs(coeff) from the input</span>
<a name="l00168"></a>00168 <span class="comment"></span> <span class="comment">//integer equation.</span>
<a name="l00169"></a>00169 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a7e1ffe57de5017f1a3bc83aa3a6163a7" 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>);<span class="comment"></span>
<a name="l00170"></a>00170 <span class="comment"> //! processes equalities with 1 or more vars of type REAL</span>
<a name="l00171"></a>00171 <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a5cc134d71df3e702dc3785072f4d5bb3" 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);<span class="comment"></span>
<a name="l00172"></a>00172 <span class="comment"> //! processes equalities whose vars are all of type INT</span>
<a name="l00173"></a>00173 <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#afdcb8dc50f957161f878c563f09a48b3" 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);<span class="comment"></span>
<a name="l00174"></a>00174 <span class="comment"> //! One step of INT equality processing (aux. method for processIntEq())</span>
<a name="l00175"></a>00175 <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a25d8be2e57c83d2e810ee815fae992d7" 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);<span class="comment"></span>
<a name="l00176"></a>00176 <span class="comment"> //! Take an inequality and isolate a variable</span>
<a name="l00177"></a>00177 <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a210dc18f7e0df0a95ff00292e9dacdbc" 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);<span class="comment"></span>
<a name="l00178"></a>00178 <span class="comment"> //! Update the statistics counters for the variable with a coeff. c</span>
<a name="l00179"></a>00179 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#af80703576d25418c16a5a187e8bcd0ef" 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);<span class="comment"></span>
<a name="l00180"></a>00180 <span class="comment"> //! Update the statistics counters for the monomial</span>
<a name="l00181"></a>00181 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#af80703576d25418c16a5a187e8bcd0ef" 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);<span class="comment"></span>
<a name="l00182"></a>00182 <span class="comment"> //! Add an inequality to the input buffer. See also d_buffer</span>
<a name="l00183"></a>00183 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a4aa91ab5d33db7fbcaf1eb5e327f64f9" 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="l00184"></a>00184 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a5d94da8150af4d31977b695bfeac4801">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="l00185"></a>00185 <span class="keyword">public</span>: <span class="comment">// ArithTheoremProducer needs this function, so make it public</span><span class="comment"></span>
<a name="l00186"></a>00186 <span class="comment"> //! Separate monomial e = c*p1*...*pn into c and 1*p1*...*pn</span>
<a name="l00187"></a>00187 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a420591a664c53906e735b528f7dc2c94" 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="l00188"></a>00188 <span class="comment"> //! Check the term t for integrality (return bool)</span>
<a name="l00189"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#a8e6e4c763da5203506a4ccc89d884655">00189</a> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a8e6e4c763da5203506a4ccc89d884655" 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_1TheoryArithNew.html#a1f78d51287d2a25282a94b7bb09d7932" title="Check the term t for integrality.">isIntegerThm</a>(e).<a class="code" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</a>()); }
<a name="l00190"></a>00190 <span class="keyword">private</span>:
<a name="l00191"></a>00191 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#ad34845d9afc0b2091a4e07d6ee805066">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);<span class="comment"></span>
<a name="l00192"></a>00192 <span class="comment"> //! Check if the term expression is "stale"</span>
<a name="l00193"></a>00193 <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a2597ed8fe8f3cae03240a2064d516c88" 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);<span class="comment"></span>
<a name="l00194"></a>00194 <span class="comment"> //! Check if the inequality is "stale" or subsumed</span>
<a name="l00195"></a>00195 <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a2597ed8fe8f3cae03240a2064d516c88" title="Check if the term expression is "stale".">isStale</a>(<span class="keyword">const</span> Ineq& ineq);
<a name="l00196"></a>00196 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#ab4e8d03929cc1b660d29d94c3adf3fcc">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="l00197"></a>00197 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#ac327959d7f9b67467862643c33ff89c1">assignVariables</a>(std::vector<Expr>&v);
<a name="l00198"></a>00198 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#abb05a7ed953b9b3ac71497c44826c743">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="l00199"></a>00199 <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="l00200"></a>00200 <a class="code" href="classCVC3_1_1Rational.html">Rational</a> &r);
<a name="l00201"></a>00201 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#ad2690ef89c8acd959a9238c4f0bc0a57">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="l00202"></a>00202
<a name="l00203"></a>00203 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a9c096e8707864d1a0ecde75bd58cf424">normalizeProjectIneqs</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& ineqThm1,
<a name="l00204"></a>00204 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& ineqThm2);<span class="comment"></span>
<a name="l00205"></a>00205 <span class="comment"> //! Take a system of equations and turn it into a solved form</span>
<a name="l00206"></a>00206 <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a6a01623e613f46e0d8f2de1a05262ec2" title="Take a system of equations and turn it into a solved form.">solvedForm</a>(<span class="keyword">const</span> std::vector<Theorem>& solvedEqs);<span class="comment"></span>
<a name="l00207"></a>00207 <span class="comment"> /*! @brief Substitute all vars in term 't' according to the</span>
<a name="l00208"></a>00208 <span class="comment"> * substitution 'subst' and canonize the result.</span>
<a name="l00209"></a>00209 <span class="comment"> */</span>
<a name="l00210"></a>00210 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#aeeb80a89d9eb5c4fc2515d2108e197d8" 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);<span class="comment"></span>
<a name="l00211"></a>00211 <span class="comment"> /*! @brief Substitute all vars in the RHS of the equation 'eq' of</span>
<a name="l00212"></a>00212 <span class="comment"> * the form (x = t) according to the substitution 'subst', and</span>
<a name="l00213"></a>00213 <span class="comment"> * canonize the result.</span>
<a name="l00214"></a>00214 <span class="comment"> */</span>
<a name="l00215"></a>00215 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#aeeb80a89d9eb5c4fc2515d2108e197d8" 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);<span class="comment"></span>
<a name="l00216"></a>00216 <span class="comment"> //! Traverse 'e' and push all the i-leaves into 'vars' vector</span>
<a name="l00217"></a>00217 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a437f70ccbf4e58ba40b4b9a067b224f1" 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="l00218"></a>00218 std::set<Expr>& cache);<span class="comment"></span>
<a name="l00219"></a>00219 <span class="comment"> /*! @brief Check if alpha <= ax & bx <= beta is a finite interval</span>
<a name="l00220"></a>00220 <span class="comment"> * for integer var 'x', and assert the corresponding constraint</span>
<a name="l00221"></a>00221 <span class="comment"> */</span>
<a name="l00222"></a>00222 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a2f6e83fb2d863d7625c94d90bf5db856" 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="l00223"></a>00223 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& bxLEbeta);<span class="comment"></span>
<a name="l00224"></a>00224 <span class="comment"> //! For an integer var 'x', find and process all constraints A <= ax <= A+c </span>
<a name="l00225"></a>00225 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#aa2a249c2877aa16d3517a6cca9992216" 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);<span class="comment"></span>
<a name="l00226"></a>00226 <span class="comment"> //! Recursive setup for isolated inequalities (and other new expressions)</span>
<a name="l00227"></a>00227 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a251086c30f2a7939e6d624d4a4cd8db4" 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="l00228"></a>00228
<a name="l00229"></a>00229 <span class="keyword">public</span>:
<a name="l00230"></a>00230 <a class="code" href="classCVC3_1_1TheoryArithNew.html#ab4411e3c522623b9041aa52ce7d857f7">TheoryArithNew</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="l00231"></a>00231 <a class="code" href="classCVC3_1_1TheoryArithNew.html#ad1803172bb5078cdfc962febe9b080dc">~TheoryArithNew</a>();
<a name="l00232"></a>00232
<a name="l00233"></a>00233 <span class="comment">// Trusted method that creates the proof rules class (used in constructor).</span>
<a name="l00234"></a>00234 <span class="comment">// Implemented in arith_theorem_producer.cpp</span>
<a name="l00235"></a>00235 <a class="code" href="classCVC3_1_1ArithProofRules.html">ArithProofRules</a>* <a class="code" href="classCVC3_1_1TheoryArithNew.html#ac92f7d2a8db02ccf23fe15302dee278d">createProofRules</a>();
<a name="l00236"></a>00236
<a name="l00237"></a>00237 <span class="comment">// Theory interface</span>
<a name="l00238"></a>00238 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a73bfa7842e5dfb1bbcf540b6a0ce49c8">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="l00239"></a>00239 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#ad083c5101196d8ea5aecf48dc00a9341" 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="l00240"></a>00240 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a3dafcfa8f6451023a83ce69c53fac641" title="Process disequalities from the arrangement for model generation.">refineCounterExample</a>();
<a name="l00241"></a>00241 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a7d73feef91b15cb086f6d1b7a7bd19c2" title="Assign concrete values to basic-type variables in v.">computeModelBasic</a>(<span class="keyword">const</span> std::vector<Expr>& v);
<a name="l00242"></a>00242 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a5c9f6212127845ff56f5c88aff72d49a" 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="l00243"></a>00243 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#af7b2bbb0c854bab9488a19b1d3072cb5" title="Check for satisfiability in the theory.">checkSat</a>(<span class="keywordtype">bool</span> fullEffort);
<a name="l00244"></a>00244 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#adf76a677d3133da1fb3e8cf33ba26cc9" 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="l00245"></a>00245 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a36a8c831cfe356a9e779988cae3e101c" 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="l00246"></a>00246 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a3790410296752fded1074ce1b808598b" 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="l00247"></a>00247 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a35ee82710c965d845aecbe6320f2ae38" title="An optional solver.">solve</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e);
<a name="l00248"></a>00248 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#ae4ed8b9b3074828d356a35192288b397" 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="l00249"></a>00249 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a272700cefa9c3f96bde0b61cc1d0b69e" 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="l00250"></a>00250 <a class="code" href="namespaceCVC3.html#af969e724f8b7016909f5804e8cea3e54" title="Enum for cardinality of types.">Cardinality</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a1070c24b2f7c993390dc1e3f00282f94" 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="l00251"></a>00251 <span class="keywordtype">bool</span> enumerate, <span class="keywordtype">bool</span> computeSize);
<a name="l00252"></a>00252 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a86fdcfbc819885dac3640dcf68472554" 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="l00253"></a>00253 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a84a67c02055bd8d4e4eb3d7c60ddf495" 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="l00254"></a>00254 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#adb72936111e69a1ab0e032cc017ee2db" 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="l00255"></a>00255 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a46272039047747962cdfbb34d6e54476" 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="l00256"></a>00256 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#aa618dbba5196953efee6954efe321ef8" 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="l00257"></a>00257 <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_1TheoryArithNew.html#a01afc8056a17c0412af99b3c33bace20" 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="l00258"></a>00258 <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#ae909a0b86693e59e95c69de37e6adf08" 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="l00259"></a>00259
<a name="l00260"></a>00260 <span class="comment">// DDDDDDDDDDDDDDDDDDDDDDDDEEEEEEEEEEEEEEEEEEEEEEEJJJJJJJJJJJJJJJJJJJJJAAAAAAAAAAAAAAAAAAAAAAANNNNNNNNNNNNNNNNNNNNNNN</span>
<a name="l00261"></a>00261
<a name="l00262"></a>00262 <span class="keyword">public</span>:
<a name="l00263"></a>00263 <span class="comment"></span>
<a name="l00264"></a>00264 <span class="comment"> /**</span>
<a name="l00265"></a>00265 <span class="comment"> * EpsRational class ecapsulates the rationals with a symbolic small \f$\epsilon\f$ added. Each rational</span>
<a name="l00266"></a>00266 <span class="comment"> * number is presented as a pair \f$(q, k) = q + k\epsilon\f$, where \f$\epsilon\f$ is treated symbolically.</span>
<a name="l00267"></a>00267 <span class="comment"> * The operations on the new rationals are defined as</span>
<a name="l00268"></a>00268 <span class="comment"> * <ul></span>
<a name="l00269"></a>00269 <span class="comment"> * <li>\f$(q_1, k_1) + (q_2, k_2) \equiv (q_1 + q_2, k_1 + k_2)\f$</span>
<a name="l00270"></a>00270 <span class="comment"> * <li>\f$a \times (q, k) \equiv (a \times q, a \times k)\f$</span>
<a name="l00271"></a>00271 <span class="comment"> * <li>\f$(q_1, k_1) \leq (q_2, k_2) \equiv (q_1 < q_2) \vee (q_1 = q_2 \wedge k_1 \leq k_2)\f$</span>
<a name="l00272"></a>00272 <span class="comment"> * </ul></span>
<a name="l00273"></a>00273 <span class="comment"> * </span>
<a name="l00274"></a>00274 <span class="comment"> * Note that the operations on the infinite values are not defined, as they are never used currently. Infinities can</span>
<a name="l00275"></a>00275 <span class="comment"> * only be asigned or compared. </span>
<a name="l00276"></a>00276 <span class="comment"> */</span>
<a name="l00277"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">00277</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a> {
<a name="l00278"></a>00278
<a name="l00279"></a>00279 <span class="keyword">protected</span>:
<a name="l00280"></a>00280 <span class="comment"></span>
<a name="l00281"></a>00281 <span class="comment"> /** Type of rationals, normal and the two infinities */</span>
<a name="l00282"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3e6dee0c23408663cd2255ae8f126b17">00282</a> <span class="keyword">typedef</span> <span class="keyword">enum</span> { <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3e6dee0c23408663cd2255ae8f126b17a578decd93f386b9d6f92bc7979109b19">FINITE</a>, <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3e6dee0c23408663cd2255ae8f126b17ab5aa9438714402b01efb70160988ba73">PLUS_INFINITY</a>, <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3e6dee0c23408663cd2255ae8f126b17a3c3af8aff3249749ee05a6c76f5c0cab">MINUS_INFINITY</a> } <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3e6dee0c23408663cd2255ae8f126b17">RationalType</a>;
<a name="l00283"></a>00283 <span class="comment"></span>
<a name="l00284"></a>00284 <span class="comment"> /** The type of this rational */</span>
<a name="l00285"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a2f9dc6730d352be05039d15fe4465cec">00285</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3e6dee0c23408663cd2255ae8f126b17">RationalType</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a2f9dc6730d352be05039d15fe4465cec">type</a>;
<a name="l00286"></a>00286 <span class="comment"></span>
<a name="l00287"></a>00287 <span class="comment"> /** The rational part */</span>
<a name="l00288"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">00288</a> <a class="code" href="classCVC3_1_1Rational.html">Rational</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">q</a>;
<a name="l00289"></a>00289 <span class="comment"></span>
<a name="l00290"></a>00290 <span class="comment"> /** The epsilon multiplier */</span>
<a name="l00291"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a5f3ebb43a7806ac855f6676f23521f34">00291</a> <a class="code" href="classCVC3_1_1Rational.html">Rational</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a5f3ebb43a7806ac855f6676f23521f34">k</a>;
<a name="l00292"></a>00292 <span class="comment"></span>
<a name="l00293"></a>00293 <span class="comment"> /**</span>
<a name="l00294"></a>00294 <span class="comment"> * Private constructor to construt infinities.</span>
<a name="l00295"></a>00295 <span class="comment"> */</span>
<a name="l00296"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#aa403054428c31e895bfe2b3994434cba">00296</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#aa403054428c31e895bfe2b3994434cba">EpsRational</a>(<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3e6dee0c23408663cd2255ae8f126b17">RationalType</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a2f9dc6730d352be05039d15fe4465cec">type</a>) : type(type) {}
<a name="l00297"></a>00297
<a name="l00298"></a>00298 <span class="keyword">public</span>:
<a name="l00299"></a>00299 <span class="comment"></span>
<a name="l00300"></a>00300 <span class="comment"> /**</span>
<a name="l00301"></a>00301 <span class="comment"> * Returns if the number is a plain rational.</span>
<a name="l00302"></a>00302 <span class="comment"> * </span>
<a name="l00303"></a>00303 <span class="comment"> * @return true if rational, false otherwise</span>
<a name="l00304"></a>00304 <span class="comment"> */</span>
<a name="l00305"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#ae2cb5d8961f532736e96dc5e79528d3d">00305</a> <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#ae2cb5d8961f532736e96dc5e79528d3d">isRational</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a5f3ebb43a7806ac855f6676f23521f34">k</a> == 0; }
<a name="l00306"></a>00306 <span class="comment"></span>
<a name="l00307"></a>00307 <span class="comment"> /**</span>
<a name="l00308"></a>00308 <span class="comment"> * Returns if the number is a plain integer.</span>
<a name="l00309"></a>00309 <span class="comment"> * </span>
<a name="l00310"></a>00310 <span class="comment"> * @return true if rational, false otherwise</span>
<a name="l00311"></a>00311 <span class="comment"> */</span>
<a name="l00312"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#aaf6f23e935bf1fbdd8de33e2bc5d0ce0">00312</a> <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#aaf6f23e935bf1fbdd8de33e2bc5d0ce0">isInteger</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a5f3ebb43a7806ac855f6676f23521f34">k</a> == 0 && <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">q</a>.<a class="code" href="classCVC3_1_1Rational.html#a1366320f4de558bb964c67f8aecedb36">isInteger</a>(); }
<a name="l00313"></a>00313 <span class="comment"></span>
<a name="l00314"></a>00314 <span class="comment"> /** </span>
<a name="l00315"></a>00315 <span class="comment"> * Returns the floor of the number \f$x = q + k \epsilon\f$ using the following formula</span>
<a name="l00316"></a>00316 <span class="comment"> * \f[</span>
<a name="l00317"></a>00317 <span class="comment"> * \lfloor \beta(x) \rfloor = \left\{</span>
<a name="l00318"></a>00318 <span class="comment"> * \begin{tabular}{ll}</span>
<a name="l00319"></a>00319 <span class="comment"> * $\lfloor q \rfloor$ & $\mathrm{if\ } q \notin Z$\\</span>
<a name="l00320"></a>00320 <span class="comment"> * $q$ & $\mathrm{if\ } q \in Z \mathrm{\ and\ } k \geq 0$\\</span>
<a name="l00321"></a>00321 <span class="comment"> * $q - 1$ & $\mathrm{if\ } q \in Z \mathrm{\ and\ } k < 0$</span>
<a name="l00322"></a>00322 <span class="comment"> * \end{tabular}\right.</span>
<a name="l00323"></a>00323 <span class="comment"> * \f]</span>
<a name="l00324"></a>00324 <span class="comment"> */</span>
<a name="l00325"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3c1a3c57ad5a40cd979c5f1ae131d108">00325</a> <span class="keyword">inline</span> <a class="code" href="classCVC3_1_1Rational.html">Rational</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3c1a3c57ad5a40cd979c5f1ae131d108">getFloor</a>()<span class="keyword"> const </span>{
<a name="l00326"></a>00326 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">q</a>.<a class="code" href="classCVC3_1_1Rational.html#a1366320f4de558bb964c67f8aecedb36">isInteger</a>()) {
<a name="l00327"></a>00327 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a5f3ebb43a7806ac855f6676f23521f34">k</a> >= 0) <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">q</a>;
<a name="l00328"></a>00328 <span class="keywordflow">else</span> <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">q</a> - 1;
<a name="l00329"></a>00329 } <span class="keywordflow">else</span>
<a name="l00330"></a>00330 <span class="comment">// If not an integer, just floor it</span>
<a name="l00331"></a>00331 <span class="keywordflow">return</span> floor(<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">q</a>);
<a name="l00332"></a>00332 }
<a name="l00333"></a>00333
<a name="l00334"></a>00334 <span class="comment"></span>
<a name="l00335"></a>00335 <span class="comment"> /** </span>
<a name="l00336"></a>00336 <span class="comment"> * Returns the rational part of the number</span>
<a name="l00337"></a>00337 <span class="comment"> * </span>
<a name="l00338"></a>00338 <span class="comment"> * @return the rational </span>
<a name="l00339"></a>00339 <span class="comment"> */</span>
<a name="l00340"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a163b1f3f3e3fa7fb04ad621063c753df">00340</a> <span class="keyword">inline</span> <a class="code" href="classCVC3_1_1Rational.html">Rational</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a163b1f3f3e3fa7fb04ad621063c753df">getRational</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">q</a>; }
<a name="l00341"></a>00341 <span class="comment"></span>
<a name="l00342"></a>00342 <span class="comment"> /** The infinity constant */</span>
<a name="l00343"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#ad99ca04b28c17f2d294173861ee89a26">00343</a> <span class="keyword">static</span> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#ad99ca04b28c17f2d294173861ee89a26">PlusInfinity</a>;<span class="comment"></span>
<a name="l00344"></a>00344 <span class="comment"> /** The negative infinity constant */</span>
<a name="l00345"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#aa1fcdb8f16c42398b6c7364c3f69d295">00345</a> <span class="keyword">static</span> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#aa1fcdb8f16c42398b6c7364c3f69d295">MinusInfinity</a>;<span class="comment"></span>
<a name="l00346"></a>00346 <span class="comment"> /** The zero constant */</span>
<a name="l00347"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a0a2d8a9aa8a24a0bdd2fc5d100d76da5">00347</a> <span class="keyword">static</span> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a0a2d8a9aa8a24a0bdd2fc5d100d76da5">Zero</a>;
<a name="l00348"></a>00348
<a name="l00349"></a>00349 <span class="comment"></span>
<a name="l00350"></a>00350 <span class="comment"> /** The blank constructor */</span>
<a name="l00351"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a51870fa96815f68dc8e75ad031566b58">00351</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a51870fa96815f68dc8e75ad031566b58">EpsRational</a>() : <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a2f9dc6730d352be05039d15fe4465cec">type</a>(<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3e6dee0c23408663cd2255ae8f126b17a578decd93f386b9d6f92bc7979109b19">FINITE</a>), <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">q</a>(0), <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a5f3ebb43a7806ac855f6676f23521f34">k</a>(0) {}
<a name="l00352"></a>00352 <span class="comment"></span>
<a name="l00353"></a>00353 <span class="comment"> /** Copy constructor */</span>
<a name="l00354"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a40886ef4e4202cb03cb5f219e290ab83">00354</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a40886ef4e4202cb03cb5f219e290ab83">EpsRational</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a>& r) : <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a2f9dc6730d352be05039d15fe4465cec">type</a>(r.<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a2f9dc6730d352be05039d15fe4465cec">type</a>), <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">q</a>(r.<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">q</a>), <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a5f3ebb43a7806ac855f6676f23521f34">k</a>(r.<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a5f3ebb43a7806ac855f6676f23521f34">k</a>) {}
<a name="l00355"></a>00355 <span class="comment"></span>
<a name="l00356"></a>00356 <span class="comment"> /**</span>
<a name="l00357"></a>00357 <span class="comment"> * Constructor from a rational, constructs a new pair (q, 0).</span>
<a name="l00358"></a>00358 <span class="comment"> * </span>
<a name="l00359"></a>00359 <span class="comment"> * @param q the rational</span>
<a name="l00360"></a>00360 <span class="comment"> */</span>
<a name="l00361"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a00588c52341fd0c492492e429f1c351e">00361</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a00588c52341fd0c492492e429f1c351e">EpsRational</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Rational.html">Rational</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">q</a>) : <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a2f9dc6730d352be05039d15fe4465cec">type</a>(<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3e6dee0c23408663cd2255ae8f126b17a578decd93f386b9d6f92bc7979109b19">FINITE</a>), q(q), <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a5f3ebb43a7806ac855f6676f23521f34">k</a>(0) {}
<a name="l00362"></a>00362 <span class="comment"></span>
<a name="l00363"></a>00363 <span class="comment"> /**</span>
<a name="l00364"></a>00364 <span class="comment"> * Constructor from a rational and a given epsilon multiplier, constructs a </span>
<a name="l00365"></a>00365 <span class="comment"> * new pair (q, k).</span>
<a name="l00366"></a>00366 <span class="comment"> * </span>
<a name="l00367"></a>00367 <span class="comment"> * @param q the rational</span>
<a name="l00368"></a>00368 <span class="comment"> * @param k the epsilon multiplier</span>
<a name="l00369"></a>00369 <span class="comment"> */</span>
<a name="l00370"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a9885b5fde8018d1fb8dc8ea708bc02d5">00370</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a9885b5fde8018d1fb8dc8ea708bc02d5">EpsRational</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Rational.html">Rational</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">q</a>, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Rational.html">Rational</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a5f3ebb43a7806ac855f6676f23521f34">k</a>) : <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a2f9dc6730d352be05039d15fe4465cec">type</a>(<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3e6dee0c23408663cd2255ae8f126b17a578decd93f386b9d6f92bc7979109b19">FINITE</a>), q(q), k(k) {}
<a name="l00371"></a>00371 <span class="comment"></span>
<a name="l00372"></a>00372 <span class="comment"> /**</span>
<a name="l00373"></a>00373 <span class="comment"> * Addition operator for two EpsRational numbers.</span>
<a name="l00374"></a>00374 <span class="comment"> * </span>
<a name="l00375"></a>00375 <span class="comment"> * @param r the number to be added</span>
<a name="l00376"></a>00376 <span class="comment"> * @return the sum as defined in the class </span>
<a name="l00377"></a>00377 <span class="comment"> */</span>
<a name="l00378"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a926ca2ef08d2a367dc29df415768228b">00378</a> <span class="keyword">inline</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a926ca2ef08d2a367dc29df415768228b">operator + </a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a>& r)<span class="keyword"> const </span>{
<a name="l00379"></a>00379 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a2f9dc6730d352be05039d15fe4465cec">type</a> == <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3e6dee0c23408663cd2255ae8f126b17a578decd93f386b9d6f92bc7979109b19">FINITE</a>, <span class="stringliteral">"EpsRational::operator +, adding to infinite number"</span>);
<a name="l00380"></a>00380 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(r.<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a2f9dc6730d352be05039d15fe4465cec">type</a> == <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3e6dee0c23408663cd2255ae8f126b17a578decd93f386b9d6f92bc7979109b19">FINITE</a>, <span class="stringliteral">"EpsRational::operator +, adding an infinite number"</span>);
<a name="l00381"></a>00381 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a51870fa96815f68dc8e75ad031566b58">EpsRational</a>(<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">q</a> + r.<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">q</a>, <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a5f3ebb43a7806ac855f6676f23521f34">k</a> + r.<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a5f3ebb43a7806ac855f6676f23521f34">k</a>);
<a name="l00382"></a>00382 }
<a name="l00383"></a>00383 <span class="comment"></span>
<a name="l00384"></a>00384 <span class="comment"> /**</span>
<a name="l00385"></a>00385 <span class="comment"> * Addition operator for two EpsRational numbers.</span>
<a name="l00386"></a>00386 <span class="comment"> * </span>
<a name="l00387"></a>00387 <span class="comment"> * @param r the number to be added</span>
<a name="l00388"></a>00388 <span class="comment"> * @return the sum as defined in the class </span>
<a name="l00389"></a>00389 <span class="comment"> */</span>
<a name="l00390"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a45d50abcce56e98844b1971d57364cda">00390</a> <span class="keyword">inline</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a>& <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a45d50abcce56e98844b1971d57364cda">operator += </a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a>& r) {
<a name="l00391"></a>00391 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a2f9dc6730d352be05039d15fe4465cec">type</a> == <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3e6dee0c23408663cd2255ae8f126b17a578decd93f386b9d6f92bc7979109b19">FINITE</a>, <span class="stringliteral">"EpsRational::operator +, adding to infinite number"</span>);
<a name="l00392"></a>00392 <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">q</a> = <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">q</a> + r.<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">q</a>;
<a name="l00393"></a>00393 <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a5f3ebb43a7806ac855f6676f23521f34">k</a> = <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a5f3ebb43a7806ac855f6676f23521f34">k</a> + r.<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a5f3ebb43a7806ac855f6676f23521f34">k</a>;
<a name="l00394"></a>00394 <span class="keywordflow">return</span> *<span class="keyword">this</span>;
<a name="l00395"></a>00395 }
<a name="l00396"></a>00396 <span class="comment"></span>
<a name="l00397"></a>00397 <span class="comment"> /**</span>
<a name="l00398"></a>00398 <span class="comment"> * Subtraction operator for two EpsRational numbers.</span>
<a name="l00399"></a>00399 <span class="comment"> * </span>
<a name="l00400"></a>00400 <span class="comment"> * @param r the number to be added</span>
<a name="l00401"></a>00401 <span class="comment"> * @return the sum as defined in the class </span>
<a name="l00402"></a>00402 <span class="comment"> */</span>
<a name="l00403"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#acd0fb95e60277525829fe536769a7da7">00403</a> <span class="keyword">inline</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#acd0fb95e60277525829fe536769a7da7">operator - </a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a>& r)<span class="keyword"> const </span>{
<a name="l00404"></a>00404 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a2f9dc6730d352be05039d15fe4465cec">type</a> == <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3e6dee0c23408663cd2255ae8f126b17a578decd93f386b9d6f92bc7979109b19">FINITE</a>, <span class="stringliteral">"EpsRational::operator -, subtracting from infinite number"</span>);
<a name="l00405"></a>00405 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(r.<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a2f9dc6730d352be05039d15fe4465cec">type</a> == <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3e6dee0c23408663cd2255ae8f126b17a578decd93f386b9d6f92bc7979109b19">FINITE</a>, <span class="stringliteral">"EpsRational::operator -, subtracting an infinite number"</span>);
<a name="l00406"></a>00406 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a51870fa96815f68dc8e75ad031566b58">EpsRational</a>(<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">q</a> - r.<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">q</a>, <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a5f3ebb43a7806ac855f6676f23521f34">k</a> - r.<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a5f3ebb43a7806ac855f6676f23521f34">k</a>);
<a name="l00407"></a>00407 }
<a name="l00408"></a>00408 <span class="comment"></span>
<a name="l00409"></a>00409 <span class="comment"> /**</span>
<a name="l00410"></a>00410 <span class="comment"> * Multiplication operator EpsRational number and a rational number.</span>
<a name="l00411"></a>00411 <span class="comment"> * </span>
<a name="l00412"></a>00412 <span class="comment"> * @param a the number to be multiplied</span>
<a name="l00413"></a>00413 <span class="comment"> * @return the product as defined in the class </span>
<a name="l00414"></a>00414 <span class="comment"> */</span>
<a name="l00415"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a5a142bf7c929c8fab3d7588cd2ba3bf4">00415</a> <span class="keyword">inline</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a5a142bf7c929c8fab3d7588cd2ba3bf4">operator * </a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Rational.html">Rational</a>& a)<span class="keyword"> const </span>{
<a name="l00416"></a>00416 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a2f9dc6730d352be05039d15fe4465cec">type</a> == <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3e6dee0c23408663cd2255ae8f126b17a578decd93f386b9d6f92bc7979109b19">FINITE</a>, <span class="stringliteral">"EpsRational::operator *, multiplying an infinite number"</span>);
<a name="l00417"></a>00417 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a51870fa96815f68dc8e75ad031566b58">EpsRational</a>(a * <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">q</a>, a * <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a5f3ebb43a7806ac855f6676f23521f34">k</a>);
<a name="l00418"></a>00418 }
<a name="l00419"></a>00419 <span class="comment"></span>
<a name="l00420"></a>00420 <span class="comment"> /**</span>
<a name="l00421"></a>00421 <span class="comment"> * Division operator EpsRational number and a rational number.</span>
<a name="l00422"></a>00422 <span class="comment"> * </span>
<a name="l00423"></a>00423 <span class="comment"> * @param a the number to be multiplied</span>
<a name="l00424"></a>00424 <span class="comment"> * @return the product as defined in the class </span>
<a name="l00425"></a>00425 <span class="comment"> */</span>
<a name="l00426"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#af95d5297b670765dea3e3f236a6c264b">00426</a> <span class="keyword">inline</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#af95d5297b670765dea3e3f236a6c264b">operator / </a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Rational.html">Rational</a>& a)<span class="keyword"> const </span>{
<a name="l00427"></a>00427 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a2f9dc6730d352be05039d15fe4465cec">type</a> == <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3e6dee0c23408663cd2255ae8f126b17a578decd93f386b9d6f92bc7979109b19">FINITE</a>, <span class="stringliteral">"EpsRational::operator *, dividing an infinite number"</span>);
<a name="l00428"></a>00428 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a51870fa96815f68dc8e75ad031566b58">EpsRational</a>(<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">q</a> / a, <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a5f3ebb43a7806ac855f6676f23521f34">k</a> / a);
<a name="l00429"></a>00429 }
<a name="l00430"></a>00430 <span class="comment"></span>
<a name="l00431"></a>00431 <span class="comment"> /**</span>
<a name="l00432"></a>00432 <span class="comment"> * Equality comparison operator.</span>
<a name="l00433"></a>00433 <span class="comment"> */</span>
<a name="l00434"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a2bf83f3564619a05548f912b2b664a6b">00434</a> <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a2bf83f3564619a05548f912b2b664a6b">operator == </a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a>& r)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> (<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">q</a> == r.<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">q</a> && <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a5f3ebb43a7806ac855f6676f23521f34">k</a> == r.<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a5f3ebb43a7806ac855f6676f23521f34">k</a>); }
<a name="l00435"></a>00435 <span class="comment"></span>
<a name="l00436"></a>00436 <span class="comment"> /**</span>
<a name="l00437"></a>00437 <span class="comment"> * Less than or equal comparison operator.</span>
<a name="l00438"></a>00438 <span class="comment"> */</span>
<a name="l00439"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#ac7cf325c58d481b6e95e209ce889fde8">00439</a> <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#ac7cf325c58d481b6e95e209ce889fde8">operator <= </a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a>& r)<span class="keyword"> const </span>{
<a name="l00440"></a>00440 <span class="keywordflow">switch</span> (r.<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a2f9dc6730d352be05039d15fe4465cec">type</a>) {
<a name="l00441"></a>00441 <span class="keywordflow">case</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3e6dee0c23408663cd2255ae8f126b17a578decd93f386b9d6f92bc7979109b19">FINITE</a>:
<a name="l00442"></a>00442 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a2f9dc6730d352be05039d15fe4465cec">type</a> == <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3e6dee0c23408663cd2255ae8f126b17a578decd93f386b9d6f92bc7979109b19">FINITE</a>)
<a name="l00443"></a>00443 <span class="comment">// Normal comparison</span>
<a name="l00444"></a>00444 <span class="keywordflow">return</span> (<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">q</a> < r.<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">q</a> || (<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">q</a> == r.<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">q</a> && <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a5f3ebb43a7806ac855f6676f23521f34">k</a> <= r.<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a5f3ebb43a7806ac855f6676f23521f34">k</a>));
<a name="l00445"></a>00445 <span class="keywordflow">else</span>
<a name="l00446"></a>00446 <span class="comment">// Finite number is bigger only of the negative infinity </span>
<a name="l00447"></a>00447 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a2f9dc6730d352be05039d15fe4465cec">type</a> == <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3e6dee0c23408663cd2255ae8f126b17a3c3af8aff3249749ee05a6c76f5c0cab">MINUS_INFINITY</a>;
<a name="l00448"></a>00448 <span class="keywordflow">case</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3e6dee0c23408663cd2255ae8f126b17ab5aa9438714402b01efb70160988ba73">PLUS_INFINITY</a>:
<a name="l00449"></a>00449 <span class="comment">// Everything is less then or equal than +inf</span>
<a name="l00450"></a>00450 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00451"></a>00451 <span class="keywordflow">case</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3e6dee0c23408663cd2255ae8f126b17a3c3af8aff3249749ee05a6c76f5c0cab">MINUS_INFINITY</a>:
<a name="l00452"></a>00452 <span class="comment">// Only -inf is less then or equal than -inf</span>
<a name="l00453"></a>00453 <span class="keywordflow">return</span> (<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a2f9dc6730d352be05039d15fe4465cec">type</a> == <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3e6dee0c23408663cd2255ae8f126b17a3c3af8aff3249749ee05a6c76f5c0cab">MINUS_INFINITY</a>);
<a name="l00454"></a>00454 <span class="keywordflow">default</span>:
<a name="l00455"></a>00455 <span class="comment">// Ohohohohohoooooo, whats up</span>
<a name="l00456"></a>00456 <a class="code" href="debug_8h.html#a2637b2fffa22e3c9fad40cda8fcc3bce" title="If something goes horribly wrong, print a message and abort immediately with exit(1).">FatalAssert</a>(<span class="keyword">false</span>, <span class="stringliteral">"EpsRational::operator <=, what kind of number is this????"</span>);
<a name="l00457"></a>00457 }
<a name="l00458"></a>00458 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00459"></a>00459 }
<a name="l00460"></a>00460 <span class="comment"></span>
<a name="l00461"></a>00461 <span class="comment"> /**</span>
<a name="l00462"></a>00462 <span class="comment"> * Less than comparison operator.</span>
<a name="l00463"></a>00463 <span class="comment"> */</span>
<a name="l00464"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#abbd3c79ae53f49ea1afaf1df469e99f8">00464</a> <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#abbd3c79ae53f49ea1afaf1df469e99f8">operator < </a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a>& r)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> !(r <= *<span class="keyword">this</span>); }
<a name="l00465"></a>00465 <span class="comment"></span>
<a name="l00466"></a>00466 <span class="comment"> /**</span>
<a name="l00467"></a>00467 <span class="comment"> * Greater than comparison operator.</span>
<a name="l00468"></a>00468 <span class="comment"> */</span>
<a name="l00469"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#abaf5bacb79a2488211619952ae64e5fc">00469</a> <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#abaf5bacb79a2488211619952ae64e5fc">operator > </a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a>& r)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> !(*<span class="keyword">this</span> <= r); }
<a name="l00470"></a>00470 <span class="comment"></span>
<a name="l00471"></a>00471 <span class="comment"> /**</span>
<a name="l00472"></a>00472 <span class="comment"> * Returns the string representation of the number.</span>
<a name="l00473"></a>00473 <span class="comment"> * </span>
<a name="l00474"></a>00474 <span class="comment"> * @return the string representation of the number</span>
<a name="l00475"></a>00475 <span class="comment"> */</span>
<a name="l00476"></a><a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#ab0d611d32ebcc656770b85da811e02cd">00476</a> std::string <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#ab0d611d32ebcc656770b85da811e02cd">toString</a>()<span class="keyword"> const </span>{
<a name="l00477"></a>00477 <span class="keywordflow">switch</span> (<a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a2f9dc6730d352be05039d15fe4465cec">type</a>) {
<a name="l00478"></a>00478 <span class="keywordflow">case</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3e6dee0c23408663cd2255ae8f126b17a578decd93f386b9d6f92bc7979109b19">FINITE</a>:
<a name="l00479"></a>00479 <span class="keywordflow">return</span> <span class="stringliteral">"("</span> + <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3b7a3f391fc48b20d130cd995920774f">q</a>.<a class="code" href="classCVC3_1_1Rational.html#a195c125a76cb9a6c5731369e244a2de3">toString</a>() + <span class="stringliteral">", "</span> + <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a5f3ebb43a7806ac855f6676f23521f34">k</a>.<a class="code" href="classCVC3_1_1Rational.html#a195c125a76cb9a6c5731369e244a2de3">toString</a>() + <span class="stringliteral">")"</span>;
<a name="l00480"></a>00480 <span class="keywordflow">case</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3e6dee0c23408663cd2255ae8f126b17ab5aa9438714402b01efb70160988ba73">PLUS_INFINITY</a>:
<a name="l00481"></a>00481 <span class="keywordflow">return</span> <span class="stringliteral">"+inf"</span>;
<a name="l00482"></a>00482 <span class="keywordflow">case</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html#a3e6dee0c23408663cd2255ae8f126b17a3c3af8aff3249749ee05a6c76f5c0cab">MINUS_INFINITY</a>:
<a name="l00483"></a>00483 <span class="keywordflow">return</span> <span class="stringliteral">"-inf"</span>;
<a name="l00484"></a>00484 <span class="keywordflow">default</span>:
<a name="l00485"></a>00485 <a class="code" href="debug_8h.html#a2637b2fffa22e3c9fad40cda8fcc3bce" title="If something goes horribly wrong, print a message and abort immediately with exit(1).">FatalAssert</a>(<span class="keyword">false</span>, <span class="stringliteral">"EpsRational::toString, what kind of number is this????"</span>);
<a name="l00486"></a>00486 }
<a name="l00487"></a>00487 <span class="keywordflow">return</span> <span class="stringliteral">"hm, what am I?"</span>;
<a name="l00488"></a>00488 }
<a name="l00489"></a>00489 };
<a name="l00490"></a>00490 <span class="comment"></span>
<a name="l00491"></a>00491 <span class="comment"> /**</span>
<a name="l00492"></a>00492 <span class="comment"> * Registers the atom given from the core. This atoms are stored so that they can be used</span>
<a name="l00493"></a>00493 <span class="comment"> * for theory propagation.</span>
<a name="l00494"></a>00494 <span class="comment"> * </span>
<a name="l00495"></a>00495 <span class="comment"> * @param e the expression (atom) that is part of the input formula</span>
<a name="l00496"></a>00496 <span class="comment"> */</span>
<a name="l00497"></a>00497 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#acf71ca1da6261f1fb8f14522613de497">registerAtom</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="l00498"></a>00498
<a name="l00499"></a>00499 <span class="keyword">private</span>:
<a name="l00500"></a>00500 <span class="comment"></span>
<a name="l00501"></a>00501 <span class="comment"> /** A set of all integer variables */</span>
<a name="l00502"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#ae79693c72c0c7236d6d76cab2a4dcc0b">00502</a> std::set<Expr> <a class="code" href="classCVC3_1_1TheoryArithNew.html#ae79693c72c0c7236d6d76cab2a4dcc0b">intVariables</a>;
<a name="l00503"></a>00503 <span class="comment"></span>
<a name="l00504"></a>00504 <span class="comment"> /**</span>
<a name="l00505"></a>00505 <span class="comment"> * Return a Gomory cut plane derivation of the variable $x_i$. Mixed integer</span>
<a name="l00506"></a>00506 <span class="comment"> * Gomory cut can be constructed if </span>
<a name="l00507"></a>00507 <span class="comment"> * <ul></span>
<a name="l00508"></a>00508 <span class="comment"> * <li>\f$x_i\f$ is a integer basic variable with a non-integer value</span>
<a name="l00509"></a>00509 <span class="comment"> * <li>all non-basic variables in the row of \f$x_i\f$ are assigned to their</span>
<a name="l00510"></a>00510 <span class="comment"> * upper or lower bounds</span>
<a name="l00511"></a>00511 <span class="comment"> * <li>all the values on the right side of the row have rational values (non</span>
<a name="l00512"></a>00512 <span class="comment"> * eps-rational values)</span>
<a name="l00513"></a>00513 <span class="comment"> * </ul></span>
<a name="l00514"></a>00514 <span class="comment"> */</span>
<a name="l00515"></a>00515 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#aeee481c90c90340e900a847fc0c8b82e">deriveGomoryCut</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& x_i);
<a name="l00516"></a>00516 <span class="comment"></span>
<a name="l00517"></a>00517 <span class="comment"> /**</span>
<a name="l00518"></a>00518 <span class="comment"> * Tries to rafine the integer constraint of the theorem. For example,</span>
<a name="l00519"></a>00519 <span class="comment"> * x < 1 is rewritten as x <= 0, and x <(=) 1.5 is rewritten as x <= 1.</span>
<a name="l00520"></a>00520 <span class="comment"> * The constraint should be in the normal form.</span>
<a name="l00521"></a>00521 <span class="comment"> * </span>
<a name="l00522"></a>00522 <span class="comment"> * @param thm the derivation of the constraint </span>
<a name="l00523"></a>00523 <span class="comment"> */</span>
<a name="l00524"></a>00524 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a68884e312bf69a858ed5a45979571d1a">rafineIntegerConstraints</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);
<a name="l00525"></a>00525 <span class="comment"></span>
<a name="l00526"></a>00526 <span class="comment"> /** Are we consistent or not */</span>
<a name="l00527"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#a5d837dd76fd8ae099ace4c1e6492301d">00527</a> <a class="code" href="classCVC3_1_1CDO.html">CDO<QueryResult></a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a5d837dd76fd8ae099ace4c1e6492301d">consistent</a>;
<a name="l00528"></a>00528 <span class="comment"></span>
<a name="l00529"></a>00529 <span class="comment"> /** The theorem explaining the inconsistency */</span>
<a name="l00530"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#a26d56a1b473c8e770caba9f3eb85f79a">00530</a> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a26d56a1b473c8e770caba9f3eb85f79a">explanation</a>;
<a name="l00531"></a>00531 <span class="comment"></span>
<a name="l00532"></a>00532 <span class="comment"> /** </span>
<a name="l00533"></a>00533 <span class="comment"> * The structure necessaty to hold the bounds.</span>
<a name="l00534"></a>00534 <span class="comment"> */</span>
<a name="l00535"></a><a class="code" href="structCVC3_1_1TheoryArithNew_1_1BoundInfo.html">00535</a> <span class="keyword">struct </span><a class="code" href="structCVC3_1_1TheoryArithNew_1_1BoundInfo.html">BoundInfo</a> {<span class="comment"></span>
<a name="l00536"></a>00536 <span class="comment"> /** The bound itself */</span>
<a name="l00537"></a><a class="code" href="structCVC3_1_1TheoryArithNew_1_1BoundInfo.html#abf0c43ef88e518be04f4f95c45edf634">00537</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a> <a class="code" href="structCVC3_1_1TheoryArithNew_1_1BoundInfo.html#abf0c43ef88e518be04f4f95c45edf634">bound</a>;<span class="comment"></span>
<a name="l00538"></a>00538 <span class="comment"> /** The assertion theoreem of the bound */</span>
<a name="l00539"></a><a class="code" href="structCVC3_1_1TheoryArithNew_1_1BoundInfo.html#a9977b9019fb5543aa4d286bcd7e5f885">00539</a> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="structCVC3_1_1TheoryArithNew_1_1BoundInfo.html#a9977b9019fb5543aa4d286bcd7e5f885">theorem</a>;
<a name="l00540"></a>00540 <span class="comment"></span>
<a name="l00541"></a>00541 <span class="comment"> /** Constructor */</span>
<a name="l00542"></a><a class="code" href="structCVC3_1_1TheoryArithNew_1_1BoundInfo.html#ae9a6928b7c9bbb9aee95bff30209af42">00542</a> <a class="code" href="structCVC3_1_1TheoryArithNew_1_1BoundInfo.html#ae9a6928b7c9bbb9aee95bff30209af42">BoundInfo</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a>& <a class="code" href="structCVC3_1_1TheoryArithNew_1_1BoundInfo.html#abf0c43ef88e518be04f4f95c45edf634">bound</a>, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm): bound(bound), <a class="code" href="structCVC3_1_1TheoryArithNew_1_1BoundInfo.html#a9977b9019fb5543aa4d286bcd7e5f885">theorem</a>(thm) {}
<a name="l00543"></a>00543 <span class="comment"></span>
<a name="l00544"></a>00544 <span class="comment"> /** The empty constructor for the map */</span>
<a name="l00545"></a><a class="code" href="structCVC3_1_1TheoryArithNew_1_1BoundInfo.html#a2bb5cd4ccae5d40b50dda2fab66f8e37">00545</a> <a class="code" href="structCVC3_1_1TheoryArithNew_1_1BoundInfo.html#a2bb5cd4ccae5d40b50dda2fab66f8e37">BoundInfo</a>(): <a class="code" href="structCVC3_1_1TheoryArithNew_1_1BoundInfo.html#abf0c43ef88e518be04f4f95c45edf634">bound</a>(0), <a class="code" href="structCVC3_1_1TheoryArithNew_1_1BoundInfo.html#a9977b9019fb5543aa4d286bcd7e5f885">theorem</a>() {}
<a name="l00546"></a>00546 <span class="comment"></span>
<a name="l00547"></a>00547 <span class="comment"> /** </span>
<a name="l00548"></a>00548 <span class="comment"> * The comparator, just if we need it. Compares first by expressions then by bounds </span>
<a name="l00549"></a>00549 <span class="comment"> */</span>
<a name="l00550"></a><a class="code" href="structCVC3_1_1TheoryArithNew_1_1BoundInfo.html#a478acb92ee6370bec2087bd9978fef42">00550</a> <span class="keywordtype">bool</span> <a class="code" href="structCVC3_1_1TheoryArithNew_1_1BoundInfo.html#a478acb92ee6370bec2087bd9978fef42">operator < </a>(<span class="keyword">const</span> <a class="code" href="structCVC3_1_1TheoryArithNew_1_1BoundInfo.html">BoundInfo</a>& bI)<span class="keyword"> const </span>{
<a name="l00551"></a>00551 <span class="comment">// Get tje expressoins</span>
<a name="l00552"></a>00552 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& expr1 = (<a class="code" href="structCVC3_1_1TheoryArithNew_1_1BoundInfo.html#a9977b9019fb5543aa4d286bcd7e5f885">theorem</a>.<a class="code" href="classCVC3_1_1Theorem.html#a362c1d70e03803d804bbe300e5f6dc87">isRewrite</a>() ? <a class="code" href="structCVC3_1_1TheoryArithNew_1_1BoundInfo.html#a9977b9019fb5543aa4d286bcd7e5f885">theorem</a>.<a class="code" href="classCVC3_1_1Theorem.html#a97d957fcbf9094480851b1d2e5d3729f">getRHS</a>() : <a class="code" href="structCVC3_1_1TheoryArithNew_1_1BoundInfo.html#a9977b9019fb5543aa4d286bcd7e5f885">theorem</a>.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00553"></a>00553 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& expr2 = (bI.<a class="code" href="structCVC3_1_1TheoryArithNew_1_1BoundInfo.html#a9977b9019fb5543aa4d286bcd7e5f885">theorem</a>.<a class="code" href="classCVC3_1_1Theorem.html#a362c1d70e03803d804bbe300e5f6dc87">isRewrite</a>() ? bI.<a class="code" href="structCVC3_1_1TheoryArithNew_1_1BoundInfo.html#a9977b9019fb5543aa4d286bcd7e5f885">theorem</a>.<a class="code" href="classCVC3_1_1Theorem.html#a97d957fcbf9094480851b1d2e5d3729f">getRHS</a>() : bI.<a class="code" href="structCVC3_1_1TheoryArithNew_1_1BoundInfo.html#a9977b9019fb5543aa4d286bcd7e5f885">theorem</a>.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00554"></a>00554
<a name="l00555"></a>00555 std::cout << expr1 << <span class="stringliteral">" @ "</span> << expr2 << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">std::endl</a>;
<a name="l00556"></a>00556
<a name="l00557"></a>00557 <span class="comment">// Compare first by the expressions (right sides of expressions)</span>
<a name="l00558"></a>00558 <span class="keywordflow">if</span> (expr1[1] == expr2[1])
<a name="l00559"></a>00559 <span class="comment">// If the same, just return the bound comparison (plus a trick to order equal bounds, different relations) </span>
<a name="l00560"></a>00560 <span class="keywordflow">if</span> (<a class="code" href="structCVC3_1_1TheoryArithNew_1_1BoundInfo.html#abf0c43ef88e518be04f4f95c45edf634">bound</a> == bI.<a class="code" href="structCVC3_1_1TheoryArithNew_1_1BoundInfo.html#abf0c43ef88e518be04f4f95c45edf634">bound</a> && expr1.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() != expr2.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>())
<a name="l00561"></a>00561 <span class="keywordflow">return</span> expr1.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() == <a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024a1b768cf71a18713c90cd71f82488ffb1">LE</a>; <span class="comment">// LE before GE -- only case that can happen </span>
<a name="l00562"></a>00562 <span class="keywordflow">else</span>
<a name="l00563"></a>00563 <span class="keywordflow">return</span> <a class="code" href="structCVC3_1_1TheoryArithNew_1_1BoundInfo.html#abf0c43ef88e518be04f4f95c45edf634">bound</a> < bI.<a class="code" href="structCVC3_1_1TheoryArithNew_1_1BoundInfo.html#abf0c43ef88e518be04f4f95c45edf634">bound</a>;
<a name="l00564"></a>00564 <span class="keywordflow">else</span>
<a name="l00565"></a>00565 <span class="comment">// Return the expression comparison</span>
<a name="l00566"></a>00566 <span class="keywordflow">return</span> expr1[1] < expr2[1];
<a name="l00567"></a>00567 }
<a name="l00568"></a>00568 };
<a name="l00569"></a>00569
<a name="l00570"></a>00570 <span class="comment"></span>
<a name="l00571"></a>00571 <span class="comment"> /** </span>
<a name="l00572"></a>00572 <span class="comment"> * The structure necessaty to hold the bounds on expressions (for theory propagation).</span>
<a name="l00573"></a>00573 <span class="comment"> */</span>
<a name="l00574"></a><a class="code" href="structCVC3_1_1TheoryArithNew_1_1ExprBoundInfo.html">00574</a> <span class="keyword">struct </span><a class="code" href="structCVC3_1_1TheoryArithNew_1_1ExprBoundInfo.html">ExprBoundInfo</a> {<span class="comment"></span>
<a name="l00575"></a>00575 <span class="comment"> /** The bound itself */</span>
<a name="l00576"></a><a class="code" href="structCVC3_1_1TheoryArithNew_1_1ExprBoundInfo.html#ac0eb8a8a0923883d67a6d479c01187a6">00576</a> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a> <a class="code" href="structCVC3_1_1TheoryArithNew_1_1ExprBoundInfo.html#ac0eb8a8a0923883d67a6d479c01187a6">bound</a>;<span class="comment"></span>
<a name="l00577"></a>00577 <span class="comment"> /** The assertion theoreem of the bound */</span>
<a name="l00578"></a><a class="code" href="structCVC3_1_1TheoryArithNew_1_1ExprBoundInfo.html#acb01e96ff38206cb9e9b58cce91ad64a">00578</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="structCVC3_1_1TheoryArithNew_1_1ExprBoundInfo.html#acb01e96ff38206cb9e9b58cce91ad64a">e</a>;
<a name="l00579"></a>00579 <span class="comment"></span>
<a name="l00580"></a>00580 <span class="comment"> /** Constructor */</span>
<a name="l00581"></a><a class="code" href="structCVC3_1_1TheoryArithNew_1_1ExprBoundInfo.html#ac89e3bda24f4a540e68bdd5623ecbd2e">00581</a> <a class="code" href="structCVC3_1_1TheoryArithNew_1_1ExprBoundInfo.html#ac89e3bda24f4a540e68bdd5623ecbd2e">ExprBoundInfo</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a>& <a class="code" href="structCVC3_1_1TheoryArithNew_1_1ExprBoundInfo.html#ac0eb8a8a0923883d67a6d479c01187a6">bound</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="structCVC3_1_1TheoryArithNew_1_1ExprBoundInfo.html#acb01e96ff38206cb9e9b58cce91ad64a">e</a>): bound(bound), e(e) {}
<a name="l00582"></a>00582 <span class="comment"></span>
<a name="l00583"></a>00583 <span class="comment"> /** The empty constructor for the map */</span>
<a name="l00584"></a><a class="code" href="structCVC3_1_1TheoryArithNew_1_1ExprBoundInfo.html#a3683d09cf9dd78ec7c6aff19d8fc1cab">00584</a> <a class="code" href="structCVC3_1_1TheoryArithNew_1_1ExprBoundInfo.html#a3683d09cf9dd78ec7c6aff19d8fc1cab">ExprBoundInfo</a>(): <a class="code" href="structCVC3_1_1TheoryArithNew_1_1ExprBoundInfo.html#ac0eb8a8a0923883d67a6d479c01187a6">bound</a>(0) {}
<a name="l00585"></a>00585 <span class="comment"></span>
<a name="l00586"></a>00586 <span class="comment"> /** </span>
<a name="l00587"></a>00587 <span class="comment"> * The comparator, just if we need it. Compares first by expressions then by bounds </span>
<a name="l00588"></a>00588 <span class="comment"> */</span>
<a name="l00589"></a><a class="code" href="structCVC3_1_1TheoryArithNew_1_1ExprBoundInfo.html#a1947a7894c4c78a096aa6755885cf0dd">00589</a> <span class="keywordtype">bool</span> <a class="code" href="structCVC3_1_1TheoryArithNew_1_1ExprBoundInfo.html#a1947a7894c4c78a096aa6755885cf0dd">operator < </a>(<span class="keyword">const</span> <a class="code" href="structCVC3_1_1TheoryArithNew_1_1ExprBoundInfo.html">ExprBoundInfo</a>& bI)<span class="keyword"> const </span>{
<a name="l00590"></a>00590
<a name="l00591"></a>00591 <span class="comment">// Compare first by the expressions (right sides of expressions)</span>
<a name="l00592"></a>00592 <span class="keywordflow">if</span> (<a class="code" href="structCVC3_1_1TheoryArithNew_1_1ExprBoundInfo.html#acb01e96ff38206cb9e9b58cce91ad64a">e</a>[1] == bI.<a class="code" href="structCVC3_1_1TheoryArithNew_1_1ExprBoundInfo.html#acb01e96ff38206cb9e9b58cce91ad64a">e</a>[1])
<a name="l00593"></a>00593 <span class="comment">// If the same, just return the bound comparison (plus a trick to order equal bounds, different relations) </span>
<a name="l00594"></a>00594 <span class="keywordflow">if</span> (<a class="code" href="structCVC3_1_1TheoryArithNew_1_1ExprBoundInfo.html#ac0eb8a8a0923883d67a6d479c01187a6">bound</a> == bI.<a class="code" href="structCVC3_1_1TheoryArithNew_1_1ExprBoundInfo.html#ac0eb8a8a0923883d67a6d479c01187a6">bound</a> && <a class="code" href="structCVC3_1_1TheoryArithNew_1_1ExprBoundInfo.html#acb01e96ff38206cb9e9b58cce91ad64a">e</a>.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() != bI.<a class="code" href="structCVC3_1_1TheoryArithNew_1_1ExprBoundInfo.html#acb01e96ff38206cb9e9b58cce91ad64a">e</a>.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>())
<a name="l00595"></a>00595 <span class="keywordflow">return</span> <a class="code" href="structCVC3_1_1TheoryArithNew_1_1ExprBoundInfo.html#acb01e96ff38206cb9e9b58cce91ad64a">e</a>.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() == <a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024a1b768cf71a18713c90cd71f82488ffb1">LE</a>; <span class="comment">// LE before GE -- only case that can happen </span>
<a name="l00596"></a>00596 <span class="keywordflow">else</span>
<a name="l00597"></a>00597 <span class="keywordflow">return</span> <a class="code" href="structCVC3_1_1TheoryArithNew_1_1ExprBoundInfo.html#ac0eb8a8a0923883d67a6d479c01187a6">bound</a> < bI.<a class="code" href="structCVC3_1_1TheoryArithNew_1_1ExprBoundInfo.html#ac0eb8a8a0923883d67a6d479c01187a6">bound</a>;
<a name="l00598"></a>00598 <span class="keywordflow">else</span>
<a name="l00599"></a>00599 <span class="comment">// Return the expression comparison</span>
<a name="l00600"></a>00600 <span class="keywordflow">return</span> <a class="code" href="structCVC3_1_1TheoryArithNew_1_1ExprBoundInfo.html#acb01e96ff38206cb9e9b58cce91ad64a">e</a>[1] < bI.<a class="code" href="structCVC3_1_1TheoryArithNew_1_1ExprBoundInfo.html#acb01e96ff38206cb9e9b58cce91ad64a">e</a>[1];
<a name="l00601"></a>00601 }
<a name="l00602"></a>00602 };
<a name="l00603"></a>00603 <span class="comment"></span>
<a name="l00604"></a>00604 <span class="comment"> /** The map from variables to lower bounds (these must be backtrackable) */</span>
<a name="l00605"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#a9fd0d5eca20607172cb8260a02296e74">00605</a> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, BoundInfo></a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a9fd0d5eca20607172cb8260a02296e74">lowerBound</a>;<span class="comment"></span>
<a name="l00606"></a>00606 <span class="comment"> /** The map from variables to upper bounds (these must be backtrackable) */</span>
<a name="l00607"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#a485637b86fce6c4a8d53d54e286d2eb8">00607</a> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, BoundInfo></a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a485637b86fce6c4a8d53d54e286d2eb8">upperBound</a>;<span class="comment"></span>
<a name="l00608"></a>00608 <span class="comment"> /** The current real valuation of the variables (these must be backtrackable for the last succesefull checkSAT!!!) */</span>
<a name="l00609"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#ab75b8a7b5960850c91a39c7713fb2477">00609</a> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, EpsRational></a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#ab75b8a7b5960850c91a39c7713fb2477">beta</a>;
<a name="l00610"></a>00610
<a name="l00611"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#a159af481e211c2e18dd9280a17ae17a3">00611</a> <span class="keyword">typedef</span> <a class="code" href="classHash_1_1hash__map.html">Hash::hash_map<Expr, Theorem></a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a159af481e211c2e18dd9280a17ae17a3">TebleauxMap</a>;
<a name="l00612"></a>00612 <span class="comment">//typedef google::sparse_hash_map<Expr, Theorem, Hash::hash<Expr> > TebleauxMap;</span>
<a name="l00613"></a>00613 <span class="comment">//typedef std::map<Expr, Theorem> TebleauxMap;</span>
<a name="l00614"></a>00614
<a name="l00615"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#a57d34162d4006753f6202c531e2a9d9a">00615</a> <span class="keyword">typedef</span> std::set<Expr> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a57d34162d4006753f6202c531e2a9d9a">SetOfVariables</a>;
<a name="l00616"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#a3353b432dcd79f2168bfcefc072edb67">00616</a> <span class="keyword">typedef</span> <a class="code" href="classHash_1_1hash__map.html">Hash::hash_map<Expr, SetOfVariables></a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a3353b432dcd79f2168bfcefc072edb67">DependenciesMap</a>;
<a name="l00617"></a>00617 <span class="comment"></span>
<a name="l00618"></a>00618 <span class="comment"> /** Maps variables to sets of variables that depend on it in the tableaux */</span>
<a name="l00619"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#a5fd6d2cc2d018a67da124ef194f178ab">00619</a> <a class="code" href="classHash_1_1hash__map.html">DependenciesMap</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a5fd6d2cc2d018a67da124ef194f178ab">dependenciesMap</a>;
<a name="l00620"></a>00620 <span class="comment"></span>
<a name="l00621"></a>00621 <span class="comment"> /** The tableaux, a map from basic variables to the expressions over the non-basic ones (theorems that explain them how we got there) */</span>
<a name="l00622"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#ad96e0ca1cad09988822b88f82ebdc016">00622</a> <a class="code" href="classHash_1_1hash__map.html">TebleauxMap</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#ad96e0ca1cad09988822b88f82ebdc016">tableaux</a>;
<a name="l00623"></a>00623 <span class="comment"></span>
<a name="l00624"></a>00624 <span class="comment"> /** Additional tableaux map from expressions asserted to the corresponding theorems explaining the introduction of the new variables */</span>
<a name="l00625"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#ac7d4a8110239f9c2d6f17c7a46a69d6e">00625</a> <a class="code" href="classHash_1_1hash__map.html">TebleauxMap</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#ac7d4a8110239f9c2d6f17c7a46a69d6e">freshVariables</a>;
<a name="l00626"></a>00626 <span class="comment"></span>
<a name="l00627"></a>00627 <span class="comment"> /** A set containing all the unsatisfied basic variables */</span>
<a name="l00628"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#a3accb9cf21e2168036e7b365649820fa">00628</a> std::set<Expr> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a3accb9cf21e2168036e7b365649820fa">unsatBasicVariables</a>;
<a name="l00629"></a>00629 <span class="comment"></span>
<a name="l00630"></a>00630 <span class="comment"> /** The vector to keep the assignments from fresh variables to expressions they represent */</span>
<a name="l00631"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#a7ff415cf3c90ddb60ff436d4b0b4c04b">00631</a> std::vector<Expr> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a7ff415cf3c90ddb60ff436d4b0b4c04b">assertedExpr</a>;<span class="comment"></span>
<a name="l00632"></a>00632 <span class="comment"> /** The backtrackable number of fresh variables asserted so far */</span>
<a name="l00633"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#a74dc050dee06beacca0e7e32b4585ec0">00633</a> <a class="code" href="classCVC3_1_1CDO.html">CDO<unsigned int></a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a74dc050dee06beacca0e7e32b4585ec0">assertedExprCount</a>;
<a name="l00634"></a>00634 <span class="comment"></span>
<a name="l00635"></a>00635 <span class="comment"> /** A set of BoundInfo objects */</span>
<a name="l00636"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#a2a34551a41e235972300cd849314c472">00636</a> <span class="keyword">typedef</span> std::set<ExprBoundInfo> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a2a34551a41e235972300cd849314c472">BoundInfoSet</a>;
<a name="l00637"></a>00637 <span class="comment"></span>
<a name="l00638"></a>00638 <span class="comment"> /** Internal variable to see wheather to propagate or not */</span>
<a name="l00639"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#ace61ed893b9e6d4b5e8ff19f40e9152a">00639</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#ace61ed893b9e6d4b5e8ff19f40e9152a">propagate</a>;
<a name="l00640"></a>00640 <span class="comment"></span>
<a name="l00641"></a>00641 <span class="comment"> /** </span>
<a name="l00642"></a>00642 <span class="comment"> * Propagate all that is possible from given assertion and its bound</span>
<a name="l00643"></a>00643 <span class="comment"> */</span>
<a name="l00644"></a>00644 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#ac6fc7d06f3933010435be7f77b0022bc">propagateTheory</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& assertExpr, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a>& bound, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a>& oldBound);
<a name="l00645"></a>00645 <span class="comment"></span>
<a name="l00646"></a>00646 <span class="comment"> /**</span>
<a name="l00647"></a>00647 <span class="comment"> * Store all the atoms from the formula in this set. It is searchable by an expression</span>
<a name="l00648"></a>00648 <span class="comment"> * and the bound. To get all the implied atoms, one just has to go up (down) and check if the </span>
<a name="l00649"></a>00649 <span class="comment"> * atom or it's negation are implied.</span>
<a name="l00650"></a>00650 <span class="comment"> */</span>
<a name="l00651"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#ae72d6b44b420d4acb2935c00d0b01fec">00651</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a2a34551a41e235972300cd849314c472">BoundInfoSet</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#ae72d6b44b420d4acb2935c00d0b01fec">allBounds</a>;
<a name="l00652"></a>00652 <span class="comment"></span>
<a name="l00653"></a>00653 <span class="comment"> /**</span>
<a name="l00654"></a>00654 <span class="comment"> * Adds var to the dependencies sets of all the variables in the sum.</span>
<a name="l00655"></a>00655 <span class="comment"> * </span>
<a name="l00656"></a>00656 <span class="comment"> * @param var the variable on the left side </span>
<a name="l00657"></a>00657 <span class="comment"> * @param sum the sum that defines the variable</span>
<a name="l00658"></a>00658 <span class="comment"> */</span>
<a name="l00659"></a>00659 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a59752d5aa73e48dd1a6c133a41a3c5d4">updateDependenciesAdd</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& var, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& sum);
<a name="l00660"></a>00660 <span class="comment"></span>
<a name="l00661"></a>00661 <span class="comment"> /**</span>
<a name="l00662"></a>00662 <span class="comment"> * Remove var from the dependencies sets of all the variables in the sum.</span>
<a name="l00663"></a>00663 <span class="comment"> * </span>
<a name="l00664"></a>00664 <span class="comment"> * @param var the variable on the left side </span>
<a name="l00665"></a>00665 <span class="comment"> * @param sum the sum that defines the variable</span>
<a name="l00666"></a>00666 <span class="comment"> */</span>
<a name="l00667"></a>00667 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#aa21dc626bcc3110d6f90cddfa66e7729">updateDependenciesRemove</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& var, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& sum);
<a name="l00668"></a>00668 <span class="comment"></span>
<a name="l00669"></a>00669 <span class="comment"> /**</span>
<a name="l00670"></a>00670 <span class="comment"> * Updates the dependencies if a right side of an expression in the tableaux is changed. For example,</span>
<a name="l00671"></a>00671 <span class="comment"> * if oldExpr is x + y and newExpr is y + z, var will be added to the dependency list of z, and removed</span>
<a name="l00672"></a>00672 <span class="comment"> * from the dependency list of x.</span>
<a name="l00673"></a>00673 <span class="comment"> * </span>
<a name="l00674"></a>00674 <span class="comment"> * @param oldExpr the old right side of the tableaux </span>
<a name="l00675"></a>00675 <span class="comment"> * @param newExpr the new right side of the tableaux</span>
<a name="l00676"></a>00676 <span class="comment"> * @param var the variable that is defined by these two expressions</span>
<a name="l00677"></a>00677 <span class="comment"> * @param skipVar a variable to skip when going through the expressions</span>
<a name="l00678"></a>00678 <span class="comment"> */</span>
<a name="l00679"></a>00679 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a85da313a2d543ca7343191a4cc20fa0d">updateDependencies</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& oldExpr, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& newExpr, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& var, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& skipVar);
<a name="l00680"></a>00680 <span class="comment"></span>
<a name="l00681"></a>00681 <span class="comment"> /**</span>
<a name="l00682"></a>00682 <span class="comment"> * Update the values of variables that have appeared in the tableaux due to backtracking.</span>
<a name="l00683"></a>00683 <span class="comment"> */</span>
<a name="l00684"></a>00684 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a16a43c368ec23e06c847ae9684a98381">updateFreshVariables</a>();
<a name="l00685"></a>00685 <span class="comment"></span>
<a name="l00686"></a>00686 <span class="comment"> /** </span>
<a name="l00687"></a>00687 <span class="comment"> * Updates the value of variable var by computing the value of expression e.</span>
<a name="l00688"></a>00688 <span class="comment"> * </span>
<a name="l00689"></a>00689 <span class="comment"> * @param var the variable to update</span>
<a name="l00690"></a>00690 <span class="comment"> * @param e the expression to compute</span>
<a name="l00691"></a>00691 <span class="comment"> */</span>
<a name="l00692"></a>00692 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#ad22fa5522add29991c72dab60da2e922">updateValue</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& var, <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="l00693"></a>00693 <span class="comment"></span>
<a name="l00694"></a>00694 <span class="comment"> /**</span>
<a name="l00695"></a>00695 <span class="comment"> * Returns a string representation of the tableaux.</span>
<a name="l00696"></a>00696 <span class="comment"> * </span>
<a name="l00697"></a>00697 <span class="comment"> * @return tableaux as string</span>
<a name="l00698"></a>00698 <span class="comment"> */</span>
<a name="l00699"></a>00699 std::string <a class="code" href="classCVC3_1_1TheoryArithNew.html#af2a4bc0a133edf66fe040d72c4e7ea01">tableauxAsString</a>() <span class="keyword">const</span>;
<a name="l00700"></a>00700 <span class="comment"></span>
<a name="l00701"></a>00701 <span class="comment"> /**</span>
<a name="l00702"></a>00702 <span class="comment"> * Returns a string representation of the unsat variables.</span>
<a name="l00703"></a>00703 <span class="comment"> * </span>
<a name="l00704"></a>00704 <span class="comment"> * @return unsat as string</span>
<a name="l00705"></a>00705 <span class="comment"> */</span>
<a name="l00706"></a>00706 std::string <a class="code" href="classCVC3_1_1TheoryArithNew.html#afbbf8a22ba662eaea65afbbcb135ff83">unsatAsString</a>() <span class="keyword">const</span>;
<a name="l00707"></a>00707 <span class="comment"></span>
<a name="l00708"></a>00708 <span class="comment"> /**</span>
<a name="l00709"></a>00709 <span class="comment"> * Returns a string representation of the current bounds.</span>
<a name="l00710"></a>00710 <span class="comment"> * </span>
<a name="l00711"></a>00711 <span class="comment"> * @return tableaux as string</span>
<a name="l00712"></a>00712 <span class="comment"> */</span>
<a name="l00713"></a>00713 std::string <a class="code" href="classCVC3_1_1TheoryArithNew.html#acbfcb4d92182bdf9e185661ec0fc61e0">boundsAsString</a>();
<a name="l00714"></a>00714 <span class="comment"></span>
<a name="l00715"></a>00715 <span class="comment"> /**</span>
<a name="l00716"></a>00716 <span class="comment"> * Gets the equality of the fresh variable tableaux variable corresponding to this expression. If the expression has already been</span>
<a name="l00717"></a>00717 <span class="comment"> * asserted, the coresponding variable is returned, othervise a fresh variable is created and the theorem is returned.</span>
<a name="l00718"></a>00718 <span class="comment"> * </span>
<a name="l00719"></a>00719 <span class="comment"> * @param leftSide the left side of the asserted constraint</span>
<a name="l00720"></a>00720 <span class="comment"> * @return the equality theorem s = leftSide</span>
<a name="l00721"></a>00721 <span class="comment"> */</span>
<a name="l00722"></a>00722 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#ad6fc5bdbe7ed6bcd4df8543e96b2b079">getVariableIntroThm</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& leftSide);
<a name="l00723"></a>00723 <span class="comment"></span>
<a name="l00724"></a>00724 <span class="comment"> /**</span>
<a name="l00725"></a>00725 <span class="comment"> * Find the coefficient standing by the variable var in the expression expr. Expresion is expected to be</span>
<a name="l00726"></a>00726 <span class="comment"> * in canonical form, i.e either a rational constant, an arithmetic leaf (i.e. variable or term from some </span>
<a name="l00727"></a>00727 <span class="comment"> * other theory), (MULT rat leaf) where rat is a non-zero rational constant, leaf is an arithmetic leaf or</span>
<a name="l00728"></a>00728 <span class="comment"> * (PLUS \f$const term_0 term_1 ... term_n\f$) where each \f$term_i\f$ is either a leaf or (MULT \f$rat leaf\f$) </span>
<a name="l00729"></a>00729 <span class="comment"> * and each leaf in \f$term_i\f$ must be strictly greater than the leaf in \f$term_{i+1}\f$. </span>
<a name="l00730"></a>00730 <span class="comment"> * </span>
<a name="l00731"></a>00731 <span class="comment"> * @param var the variable</span>
<a name="l00732"></a>00732 <span class="comment"> * @param expr the expression to search in</span>
<a name="l00733"></a>00733 <span class="comment"> */</span>
<a name="l00734"></a>00734 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Rational.html">Rational</a>& <a class="code" href="classCVC3_1_1TheoryArithNew.html#a5fcebedad96665573ab5eafb7d70b2e0">findCoefficient</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& var, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& expr);
<a name="l00735"></a>00735 <span class="comment"></span>
<a name="l00736"></a>00736 <span class="comment"> /**</span>
<a name="l00737"></a>00737 <span class="comment"> * Return true iof the given variable is basic in the tableaux, i.e. it is on the left side, expressed</span>
<a name="l00738"></a>00738 <span class="comment"> * in terms of the non-basic variables.</span>
<a name="l00739"></a>00739 <span class="comment"> * </span>
<a name="l00740"></a>00740 <span class="comment"> * @param x the variable to be checked</span>
<a name="l00741"></a>00741 <span class="comment"> * @return true if the variable is basic, false if the variable is non-basic</span>
<a name="l00742"></a>00742 <span class="comment"> */</span>
<a name="l00743"></a>00743 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#af4eaf347e86ee4616a52676801213711">isBasic</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& x) <span class="keyword">const</span>;
<a name="l00744"></a>00744 <span class="comment"></span>
<a name="l00745"></a>00745 <span class="comment"> /**</span>
<a name="l00746"></a>00746 <span class="comment"> * Returns the coefficient at a_ij in the current tableaux, i.e. the coefficient </span>
<a name="l00747"></a>00747 <span class="comment"> * at x_j in the row of x_i.</span>
<a name="l00748"></a>00748 <span class="comment"> * </span>
<a name="l00749"></a>00749 <span class="comment"> * @param x_i a basic variable</span>
<a name="l00750"></a>00750 <span class="comment"> * @param x_j a non-basic variable</span>
<a name="l00751"></a>00751 <span class="comment"> * @return the reational coefficient </span>
<a name="l00752"></a>00752 <span class="comment"> */</span>
<a name="l00753"></a>00753 <a class="code" href="classCVC3_1_1Rational.html">Rational</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a4ed9c0c6e1bfa32ead951cb6c1221f0e">getTableauxEntry</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& x_i, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& x_j);
<a name="l00754"></a>00754 <span class="comment"></span>
<a name="l00755"></a>00755 <span class="comment"> /**</span>
<a name="l00756"></a>00756 <span class="comment"> * Swaps a basic variable \f$x_r\f$ and a non-basic variable \f$x_s\f$ such</span>
<a name="l00757"></a>00757 <span class="comment"> * that ars \f$a_{rs} \neq 0\f$. After pivoting, \f$x_s\f$ becomes basic and \f$x_r\f$ becomes non-basic. </span>
<a name="l00758"></a>00758 <span class="comment"> * The tableau is updated by replacing equation \f[x_r = \sum_{x_j \in N}{a_{rj}xj}\f] with</span>
<a name="l00759"></a>00759 <span class="comment"> * \f[x_s = \frac{x_r}{a_{rs}} - \sum_{x_j \in N }{\frac{a_{rj}}{a_rs}x_j}\f] and this equation </span>
<a name="l00760"></a>00760 <span class="comment"> * is used to eliminate \f$x_s\f$ from the rest of the tableau by substitution.</span>
<a name="l00761"></a>00761 <span class="comment"> * </span>
<a name="l00762"></a>00762 <span class="comment"> * @param x_r a basic variable</span>
<a name="l00763"></a>00763 <span class="comment"> * @param x_s a non-basic variable</span>
<a name="l00764"></a>00764 <span class="comment"> */</span>
<a name="l00765"></a>00765 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#ab19840152f3116c50edb0b6c0cc673f7">pivot</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& x_r, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& x_s);
<a name="l00766"></a>00766 <span class="comment"></span>
<a name="l00767"></a>00767 <span class="comment"> /**</span>
<a name="l00768"></a>00768 <span class="comment"> * Sets the value of a non-basic variable \f$x_i\f$ to \f$v\f$ and adjusts the value of all </span>
<a name="l00769"></a>00769 <span class="comment"> * the basic variables so that all equations remain satisfied.</span>
<a name="l00770"></a>00770 <span class="comment"> * </span>
<a name="l00771"></a>00771 <span class="comment"> * @param x_i a non-basic variable</span>
<a name="l00772"></a>00772 <span class="comment"> * @param v the value to set the variable \f$x_i\f$ to </span>
<a name="l00773"></a>00773 <span class="comment"> */</span>
<a name="l00774"></a>00774 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a3790410296752fded1074ce1b808598b" title="Notify a theory of a new equality.">update</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& x_i, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a>& v);
<a name="l00775"></a>00775 <span class="comment"></span>
<a name="l00776"></a>00776 <span class="comment"> /**</span>
<a name="l00777"></a>00777 <span class="comment"> * Pivots the basic variable \f$x_i\f$ and the non-basic variable \f$x_j\f$. It also sets \f$x_i\f$ to \f$v\f$ and adjusts all basic </span>
<a name="l00778"></a>00778 <span class="comment"> * variables to keep the equations satisfied.</span>
<a name="l00779"></a>00779 <span class="comment"> * </span>
<a name="l00780"></a>00780 <span class="comment"> * @param x_i a basic variable</span>
<a name="l00781"></a>00781 <span class="comment"> * @param x_j a non-basic variable</span>
<a name="l00782"></a>00782 <span class="comment"> * @param v the valie to assign to x_i</span>
<a name="l00783"></a>00783 <span class="comment"> */</span>
<a name="l00784"></a>00784 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#ae9e0aad1b930137d011dbab8bf4b0874">pivotAndUpdate</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& x_i, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& x_j, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a>& v);
<a name="l00785"></a>00785 <span class="comment"></span>
<a name="l00786"></a>00786 <span class="comment"> /**</span>
<a name="l00787"></a>00787 <span class="comment"> * Asserts a new upper bound constraint on a variable and performs a simple check for consistency (not complete).</span>
<a name="l00788"></a>00788 <span class="comment"> * </span>
<a name="l00789"></a>00789 <span class="comment"> * @param x_i the variable to assert the bound on</span>
<a name="l00790"></a>00790 <span class="comment"> * @param c the bound to assert</span>
<a name="l00791"></a>00791 <span class="comment"> */</span>
<a name="l00792"></a>00792 <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a344feb254ed4f336fc0dc41a66cf232c">assertUpper</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& x_i, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a>& c, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);
<a name="l00793"></a>00793 <span class="comment"></span>
<a name="l00794"></a>00794 <span class="comment"> /**</span>
<a name="l00795"></a>00795 <span class="comment"> * Asserts a new lower bound constraint on a variable and performs a simple check for consistency (not complete).</span>
<a name="l00796"></a>00796 <span class="comment"> * </span>
<a name="l00797"></a>00797 <span class="comment"> * @param x_i the variable to assert the bound on</span>
<a name="l00798"></a>00798 <span class="comment"> * @param c the bound to assert</span>
<a name="l00799"></a>00799 <span class="comment"> */</span>
<a name="l00800"></a>00800 <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#aa17423f3ce290e28544a356f0977f6f8">assertLower</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& x_i, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a>& c, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);
<a name="l00801"></a>00801 <span class="comment"></span>
<a name="l00802"></a>00802 <span class="comment"> /**</span>
<a name="l00803"></a>00803 <span class="comment"> * Asserts a new equality constraint on a variable by asserting both upper and lower bounds.</span>
<a name="l00804"></a>00804 <span class="comment"> * </span>
<a name="l00805"></a>00805 <span class="comment"> * @param x_i the variable to assert the bound on</span>
<a name="l00806"></a>00806 <span class="comment"> * @param c the bound to assert</span>
<a name="l00807"></a>00807 <span class="comment"> */</span>
<a name="l00808"></a>00808 <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#ace140a37ea260f769f4aa2756e5f22f0">assertEqual</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& x_i, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a>& c, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);
<a name="l00809"></a>00809 <span class="comment"></span>
<a name="l00810"></a>00810 <span class="comment"> /**</span>
<a name="l00811"></a>00811 <span class="comment"> * Type of noramlization GCD = 1 or just first coefficient 1</span>
<a name="l00812"></a>00812 <span class="comment"> */</span>
<a name="l00813"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#a9707c04f2d2af4812b8c18029f0368f4a382fccac5af0c0091adfac3b4048c2ba">00813</a> <span class="keyword">typedef</span> <span class="keyword">enum</span> { <a class="code" href="classCVC3_1_1TheoryArithNew.html#a9707c04f2d2af4812b8c18029f0368f4a5df10a1338d39c91f6886d5b09a2751d">NORMALIZE_GCD</a>, <a class="code" href="classCVC3_1_1TheoryArithNew.html#a9707c04f2d2af4812b8c18029f0368f4a382fccac5af0c0091adfac3b4048c2ba">NORMALIZE_UNIT</a> } <a class="code" href="classCVC3_1_1TheoryArithNew.html#a9707c04f2d2af4812b8c18029f0368f4">NormalizationType</a>;
<a name="l00814"></a>00814 <span class="comment"></span>
<a name="l00815"></a>00815 <span class="comment"> /**</span>
<a name="l00816"></a>00816 <span class="comment"> * Given a canonized term, compute a factor to make all coefficients integer and relatively prime </span>
<a name="l00817"></a>00817 <span class="comment"> */</span>
<a name="l00818"></a>00818 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a48d4a6a488973f4fc79fc8d0c4d1470c">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 class="code" href="classCVC3_1_1TheoryArithNew.html#a9707c04f2d2af4812b8c18029f0368f4">NormalizationType</a> type = <a class="code" href="classCVC3_1_1TheoryArithNew.html#a9707c04f2d2af4812b8c18029f0368f4a5df10a1338d39c91f6886d5b09a2751d">NORMALIZE_GCD</a>);
<a name="l00819"></a>00819 <span class="comment"></span>
<a name="l00820"></a>00820 <span class="comment"> /**</span>
<a name="l00821"></a>00821 <span class="comment"> * Normalize an equation (make all coefficients rel. prime integers)</span>
<a name="l00822"></a>00822 <span class="comment"> */</span>
<a name="l00823"></a>00823 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a243f5665943792345df52be2a94eb648">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 class="code" href="classCVC3_1_1TheoryArithNew.html#a9707c04f2d2af4812b8c18029f0368f4">NormalizationType</a> type = <a class="code" href="classCVC3_1_1TheoryArithNew.html#a9707c04f2d2af4812b8c18029f0368f4a5df10a1338d39c91f6886d5b09a2751d">NORMALIZE_GCD</a>);
<a name="l00824"></a>00824 <span class="comment"></span>
<a name="l00825"></a>00825 <span class="comment"> /**</span>
<a name="l00826"></a>00826 <span class="comment"> * Normalize an equation (make all coefficients rel. prime integers) accepts a rewrite theorem over </span>
<a name="l00827"></a>00827 <span class="comment"> * eqn|ineqn and normalizes it and returns a theorem to that effect.</span>
<a name="l00828"></a>00828 <span class="comment"> */</span>
<a name="l00829"></a>00829 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a243f5665943792345df52be2a94eb648">normalize</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm, <a class="code" href="classCVC3_1_1TheoryArithNew.html#a9707c04f2d2af4812b8c18029f0368f4">NormalizationType</a> type = <a class="code" href="classCVC3_1_1TheoryArithNew.html#a9707c04f2d2af4812b8c18029f0368f4a5df10a1338d39c91f6886d5b09a2751d">NORMALIZE_GCD</a>);
<a name="l00830"></a>00830 <span class="comment"></span>
<a name="l00831"></a>00831 <span class="comment"> /**</span>
<a name="l00832"></a>00832 <span class="comment"> * Canonise the equation using the tebleaux equations, i.e. replace all the tableaux right sides</span>
<a name="l00833"></a>00833 <span class="comment"> * with the corresponding left sides and canonise the result. </span>
<a name="l00834"></a>00834 <span class="comment"> * </span>
<a name="l00835"></a>00835 <span class="comment"> * @param eq the equation to canonise</span>
<a name="l00836"></a>00836 <span class="comment"> * @return the explaining theorem</span>
<a name="l00837"></a>00837 <span class="comment"> */</span>
<a name="l00838"></a>00838 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a349c59e5b2eb5c2a9154f5bdeff43fde">substAndCanonizeModTableaux</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& eq);
<a name="l00839"></a>00839 <span class="comment"></span>
<a name="l00840"></a>00840 <span class="comment"> /**</span>
<a name="l00841"></a>00841 <span class="comment"> * Canonise the sum using the tebleaux equations, i.e. replace all the tableaux right sides</span>
<a name="l00842"></a>00842 <span class="comment"> * with the corresponding left sides and canonise the result. </span>
<a name="l00843"></a>00843 <span class="comment"> * </span>
<a name="l00844"></a>00844 <span class="comment"> * @param sum the canonised sum to canonise</span>
<a name="l00845"></a>00845 <span class="comment"> * @return the explaining theorem</span>
<a name="l00846"></a>00846 <span class="comment"> */</span>
<a name="l00847"></a>00847 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a349c59e5b2eb5c2a9154f5bdeff43fde">substAndCanonizeModTableaux</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& sum);
<a name="l00848"></a>00848 <span class="comment"></span>
<a name="l00849"></a>00849 <span class="comment"> /**</span>
<a name="l00850"></a>00850 <span class="comment"> * Sustitute the given equation everywhere in the tableaux.</span>
<a name="l00851"></a>00851 <span class="comment"> * </span>
<a name="l00852"></a>00852 <span class="comment"> * @param eq the equation to use for substitution</span>
<a name="l00853"></a>00853 <span class="comment"> */</span>
<a name="l00854"></a>00854 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryArithNew.html#ad7d64d8e7110a9992654154b3e3613b0">substAndCanonizeTableaux</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& eq);
<a name="l00855"></a>00855 <span class="comment"></span>
<a name="l00856"></a>00856 <span class="comment"> /**</span>
<a name="l00857"></a>00857 <span class="comment"> * Given an equality eq: \f$\sum a_i x_i = y\f$ and a variable $var$ that appears in</span>
<a name="l00858"></a>00858 <span class="comment"> * on the left hand side, pivots $y$ and $var$ so that $y$ comes to the right-hand </span>
<a name="l00859"></a>00859 <span class="comment"> * side.</span>
<a name="l00860"></a>00860 <span class="comment"> * </span>
<a name="l00861"></a>00861 <span class="comment"> * @param eq the proof of the equality</span>
<a name="l00862"></a>00862 <span class="comment"> * @param var the variable to move to the right-hand side</span>
<a name="l00863"></a>00863 <span class="comment"> */</span>
<a name="l00864"></a>00864 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#abebb5cee14c85657ea68c873372b14d9">pivotRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& eq, <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="l00865"></a>00865 <span class="comment"></span>
<a name="l00866"></a>00866 <span class="comment"> /**</span>
<a name="l00867"></a>00867 <span class="comment"> * Knowing that the tableaux row for \f$x_i\f$ is the problematic one, generate the</span>
<a name="l00868"></a>00868 <span class="comment"> * explanation clause. The variables in the row of \f$x_i = \sum_{x_j \in \mathcal{N}}{a_ij x_j}\f$ are separated to</span>
<a name="l00869"></a>00869 <span class="comment"> * <ul></span>
<a name="l00870"></a>00870 <span class="comment"> * <li>\f$\mathcal{N}^+ = \left\lbrace x_j \in \mathcal{N} \; | \; a_{ij} > 0 \right\rbrace\f$</span>
<a name="l00871"></a>00871 <span class="comment"> * <li>\f$\mathcal{N}^- = \left\lbrace x_j \in \mathcal{N} \; | \; a_{ij} < 0\right\rbrace\f$ </span>
<a name="l00872"></a>00872 <span class="comment"> * </ul></span>
<a name="l00873"></a>00873 <span class="comment"> * Then, the explanation clause to be returned is </span>
<a name="l00874"></a>00874 <span class="comment"> * \f[\Gamma = \left\lbrace x_j \leq u_j \; | \; x_j \in \mathcal{N}^+\right\rbrace \cup \left\lbrace l_j \leq x_j \; | \; </span>
<a name="l00875"></a>00875 <span class="comment"> * x_j \in \mathcal{N}^-\right\rbrace \cup \left\lbrace l_i \leq x_i \right\rbrace\f]</span>
<a name="l00876"></a>00876 <span class="comment"> * </span>
<a name="l00877"></a>00877 <span class="comment"> * @param var_it the variable that caused the clash</span>
<a name="l00878"></a>00878 <span class="comment"> * @return the theorem explainang the clash</span>
<a name="l00879"></a>00879 <span class="comment"> */</span>
<a name="l00880"></a>00880 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a843498f8c1a569a296822e8f1f92d675">getLowerBoundExplanation</a>(<span class="keyword">const</span> <a class="code" href="classHash_1_1hash__map.html#a0fae180472ddfd8822c881caf23c11a9">TebleauxMap::iterator</a>& var_it);
<a name="l00881"></a>00881 <span class="comment"></span>
<a name="l00882"></a>00882 <span class="comment"> /**</span>
<a name="l00883"></a>00883 <span class="comment"> * Knowing that the tableaux row for \f$x_i\f$ is the problematic one, generate the</span>
<a name="l00884"></a>00884 <span class="comment"> * explanation clause. The variables in the row of \f$x_i = \sum_{x_j \in \mathcal{N}}{a_ij x_j}\f$ are separated to</span>
<a name="l00885"></a>00885 <span class="comment"> * <ul></span>
<a name="l00886"></a>00886 <span class="comment"> * <li>\f$\mathcal{N}^+ = \left\lbrace x_j \in \mathcal{N} \; | \; a_{ij} > 0 \right\rbrace\f$</span>
<a name="l00887"></a>00887 <span class="comment"> * <li>\f$\mathcal{N}^- = \left\lbrace x_j \in \mathcal{N} \; | \; a_{ij} < 0\right\rbrace\f$ </span>
<a name="l00888"></a>00888 <span class="comment"> * </ul></span>
<a name="l00889"></a>00889 <span class="comment"> * Then, the explanation clause to be returned is </span>
<a name="l00890"></a>00890 <span class="comment"> * \f[\Gamma = \left\lbrace x_j \leq u_j \; | \; x_j \in \mathcal{N}^-\right\rbrace \cup \left\lbrace l_j \leq x_j \; | \; </span>
<a name="l00891"></a>00891 <span class="comment"> * x_j \in \mathcal{N}^+\right\rbrace \cup \left\lbrace x_i \leq u_i \right\rbrace\f]</span>
<a name="l00892"></a>00892 <span class="comment"> * </span>
<a name="l00893"></a>00893 <span class="comment"> * @param var_it the variable that caused the clash</span>
<a name="l00894"></a>00894 <span class="comment"> * @return the theorem explainang the clash</span>
<a name="l00895"></a>00895 <span class="comment"> */</span>
<a name="l00896"></a>00896 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a6bbd3291d090682e1c8a2cadb0d8380d">getUpperBoundExplanation</a>(<span class="keyword">const</span> <a class="code" href="classHash_1_1hash__map.html#a0fae180472ddfd8822c881caf23c11a9">TebleauxMap::iterator</a>& var_it);
<a name="l00897"></a>00897
<a name="l00898"></a>00898 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a5402887425b9a029f2ae0718c5012cb2">addInequalities</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& le_1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& le_2);
<a name="l00899"></a>00899 <span class="comment"></span>
<a name="l00900"></a>00900 <span class="comment"> /**</span>
<a name="l00901"></a>00901 <span class="comment"> * Check the satisfiability </span>
<a name="l00902"></a>00902 <span class="comment"> */</span>
<a name="l00903"></a>00903 <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#ab67b64c7fd085bd9881aa7cef33217de">checkSatSimplex</a>();
<a name="l00904"></a>00904 <span class="comment"></span>
<a name="l00905"></a>00905 <span class="comment"> /**</span>
<a name="l00906"></a>00906 <span class="comment"> * Check the satisfiability of integer constraints</span>
<a name="l00907"></a>00907 <span class="comment"> */</span>
<a name="l00908"></a>00908 <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a7b516a72d54789b1403b8854b83aeb29">checkSatInteger</a>();
<a name="l00909"></a>00909 <span class="comment"></span>
<a name="l00910"></a>00910 <span class="comment"> /** </span>
<a name="l00911"></a>00911 <span class="comment"> * The last lemma that we asserted to check the integer satisfiability. We don't do checksat until</span>
<a name="l00912"></a>00912 <span class="comment"> * the lemma split has been asserted.</span>
<a name="l00913"></a>00913 <span class="comment"> */</span>
<a name="l00914"></a><a class="code" href="classCVC3_1_1TheoryArithNew.html#a17aa12461bb0531b62670e37499b38a0">00914</a> <a class="code" href="classCVC3_1_1CDO.html">CDO<Theorem></a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a17aa12461bb0531b62670e37499b38a0">integer_lemma</a>;
<a name="l00915"></a>00915
<a name="l00916"></a>00916 <span class="keyword">public</span>:
<a name="l00917"></a>00917 <span class="comment"></span>
<a name="l00918"></a>00918 <span class="comment"> /**</span>
<a name="l00919"></a>00919 <span class="comment"> * Gets the current lower bound on variable x.</span>
<a name="l00920"></a>00920 <span class="comment"> * </span>
<a name="l00921"></a>00921 <span class="comment"> * @param x the variable</span>
<a name="l00922"></a>00922 <span class="comment"> * @return the current lower bound on x</span>
<a name="l00923"></a>00923 <span class="comment"> */</span>
<a name="l00924"></a>00924 <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#ad4e8b908bccb2d534552f968bd27979c">getLowerBound</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& x) <span class="keyword">const</span>;
<a name="l00925"></a>00925 <span class="comment"></span>
<a name="l00926"></a>00926 <span class="comment"> /**</span>
<a name="l00927"></a>00927 <span class="comment"> * Get the current upper bound on variable x.</span>
<a name="l00928"></a>00928 <span class="comment"> * </span>
<a name="l00929"></a>00929 <span class="comment"> * @param x the variable</span>
<a name="l00930"></a>00930 <span class="comment"> * @return the current upper bound on x</span>
<a name="l00931"></a>00931 <span class="comment"> */</span>
<a name="l00932"></a>00932 <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a7fcc9a229fd6125188d69f4bc282cdfb">getUpperBound</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& x) <span class="keyword">const</span>;
<a name="l00933"></a>00933 <span class="comment"></span>
<a name="l00934"></a>00934 <span class="comment"> /**</span>
<a name="l00935"></a>00935 <span class="comment"> * Gets the theorem of the current lower bound on variable x.</span>
<a name="l00936"></a>00936 <span class="comment"> * </span>
<a name="l00937"></a>00937 <span class="comment"> * @param x the variable</span>
<a name="l00938"></a>00938 <span class="comment"> * @return the current lower bound on x</span>
<a name="l00939"></a>00939 <span class="comment"> */</span>
<a name="l00940"></a>00940 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#ab27c747e527f4e6a9f0bc39692a706af">getLowerBoundThm</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& x) <span class="keyword">const</span>;
<a name="l00941"></a>00941 <span class="comment"></span>
<a name="l00942"></a>00942 <span class="comment"> /**</span>
<a name="l00943"></a>00943 <span class="comment"> * Get the theorem of the current upper bound on variable x.</span>
<a name="l00944"></a>00944 <span class="comment"> * </span>
<a name="l00945"></a>00945 <span class="comment"> * @param x the variable</span>
<a name="l00946"></a>00946 <span class="comment"> * @return the current upper bound on x</span>
<a name="l00947"></a>00947 <span class="comment"> */</span>
<a name="l00948"></a>00948 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#ab41d31e40d053398a37f77a7a797c7a7">getUpperBoundThm</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& x) <span class="keyword">const</span>;
<a name="l00949"></a>00949 <span class="comment"></span>
<a name="l00950"></a>00950 <span class="comment"> /**</span>
<a name="l00951"></a>00951 <span class="comment"> * Gets the current valuation of variable x (beta).</span>
<a name="l00952"></a>00952 <span class="comment"> * </span>
<a name="l00953"></a>00953 <span class="comment"> * @param x the variable</span>
<a name="l00954"></a>00954 <span class="comment"> * @return the current value of variable x</span>
<a name="l00955"></a>00955 <span class="comment"> */</span>
<a name="l00956"></a>00956 <a class="code" href="classCVC3_1_1TheoryArithNew_1_1EpsRational.html">EpsRational</a> <a class="code" href="classCVC3_1_1TheoryArithNew.html#a41dbe160161458e73fa669fe891ec529">getBeta</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="l00957"></a>00957
<a name="l00958"></a>00958 <span class="comment">// DDDDDDDDDDDDDDDDDDDDDDDDEEEEEEEEEEEEEEEEEEEEEEEJJJJJJJJJJJJJJJJJJJJJAAAAAAAAAAAAAAAAAAAAAAANNNNNNNNNNNNNNNNNNNNNNN</span>
<a name="l00959"></a>00959
<a name="l00960"></a>00960 };
<a name="l00961"></a>00961
<a name="l00962"></a>00962 }
<a name="l00963"></a>00963
<a name="l00964"></a>00964 <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>
