<!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: CVC3::ArithProofRules Class Reference</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 class="current"><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="annotated.html"><span>Class List</span></a></li>
<li><a href="classes.html"><span>Class Index</span></a></li>
<li><a href="hierarchy.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="namespaceCVC3.html">CVC3</a> </li>
<li class="navelem"><a class="el" href="classCVC3_1_1ArithProofRules.html">ArithProofRules</a> </li>
</ul>
</div>
</div>
<div class="header">
<div class="summary">
<a href="#pub-methods">Public Member Functions</a> </div>
<div class="headertitle">
<div class="title">CVC3::ArithProofRules Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="CVC3::ArithProofRules" -->
<p><code>#include <<a class="el" href="arith__proof__rules_8h_source.html">arith_proof_rules.h</a>></code></p>
<div class="dynheader">
Inheritance diagram for CVC3::ArithProofRules:</div>
<div class="dyncontent">
<div class="center">
<img src="classCVC3_1_1ArithProofRules.png" usemap="#CVC3::ArithProofRules_map" alt=""/>
<map id="CVC3::ArithProofRules_map" name="CVC3::ArithProofRules_map">
<area href="classCVC3_1_1ArithTheoremProducer.html" alt="CVC3::ArithTheoremProducer" shape="rect" coords="0,56,201,80"/>
<area href="classCVC3_1_1ArithTheoremProducer3.html" alt="CVC3::ArithTheoremProducer3" shape="rect" coords="211,56,412,80"/>
<area href="classCVC3_1_1ArithTheoremProducerOld.html" alt="CVC3::ArithTheoremProducerOld" shape="rect" coords="422,56,623,80"/>
</map>
</div></div>
<p><a href="classCVC3_1_1ArithProofRules-members.html">List of all members.</a></p>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li>virtual <a class="el" href="classCVC3_1_1ArithProofRules.html#a410c697fc050feca9680a388397b0968">~ArithProofRules</a> ()
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a8b8db5ad0a8d4968f429e98964db93c1">varToMult</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">==> e = 1 * e <a href="#a8b8db5ad0a8d4968f429e98964db93c1"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#aa95faca93e7b4a1cf21667ff88d390e4">uMinusToMult</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">==> -(e) = (-1) * e <a href="#aa95faca93e7b4a1cf21667ff88d390e4"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a4319c532082c0f43794b34a2fb9df73f">minusToPlus</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &x, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &y)=0
<dl class="el"><dd class="mdescRight">==> x - y = x + (-1) * y <a href="#a4319c532082c0f43794b34a2fb9df73f"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a0053398d4a8fc49d9a2f8ede6949fc70">canonUMinusToDivide</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a18e5970bc4f670a63ca5775750f099ab">moveSumConstantRight</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a79c759f2bb7dc41ed98c5962febef804">canonDivideConst</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &c, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &d)=0
<dl class="el"><dd class="mdescRight">(c) / d ==> (c/d), takes c and d <a href="#a79c759f2bb7dc41ed98c5962febef804"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#aee487a2a1e8ce4c34075568eb70ea874">canonDivideMult</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &cx, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &d)=0
<dl class="el"><dd class="mdescRight">(c * x) / d ==> (c/d) * x, takes (c*x) and d <a href="#aee487a2a1e8ce4c34075568eb70ea874"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a92846ee0cdab98d1759a13ff7e8d710d">canonDividePlus</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &d)=0
<dl class="el"><dd class="mdescRight">(+ c ...)/d ==> push division to all the coefficients. <a href="#a92846ee0cdab98d1759a13ff7e8d710d"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a4ab0351b340ecb82d6ced530e4f30510">canonDivideVar</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &d)=0
<dl class="el"><dd class="mdescRight">x / d ==> (1/d) * x, takes x and d <a href="#a4ab0351b340ecb82d6ced530e4f30510"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#aa38d5c06ebe0b672570641fe933cfedb">canonMultMtermMterm</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a225fe511e6f654f313048e86c1550510">canonPlus</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">Canonize (PLUS t1 ... tn) <a href="#a225fe511e6f654f313048e86c1550510"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#aca910e6ff44389aac100b14b486c1942">canonMult</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">Canonize (MULT t1 ... tn) <a href="#aca910e6ff44389aac100b14b486c1942"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a9a806d487932bbfa9a019d4d1eed1cea">canonInvert</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">==> 1/e = e' where e' is canonical; takes e. <a href="#a9a806d487932bbfa9a019d4d1eed1cea"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a198b0b44145b8e33555ffd212f43b7b3">canonDivide</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">Canonize t1/t2. <a href="#a198b0b44145b8e33555ffd212f43b7b3"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a11870b90dbfcc61d2b9a2820df7f6057">canonMultTermConst</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &c, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &t)=0
<dl class="el"><dd class="mdescRight">t*c ==> c*t, takes constant c and term t <a href="#a11870b90dbfcc61d2b9a2820df7f6057"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a8b9abf99f0b013714eaaa49e81a618b9">canonMultTerm1Term2</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &t1, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &t2)=0
<dl class="el"><dd class="mdescRight">t1*t2 ==> Error, takes t1 and t2 where both are non-constants <a href="#a8b9abf99f0b013714eaaa49e81a618b9"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#aae559b4d1558fecba5621c9ba27daa88">canonMultZero</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">0*t ==> 0, takes 0*t <a href="#aae559b4d1558fecba5621c9ba27daa88"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a87f9a39ecb1bec46adff5187bc899726">canonMultOne</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">1*t ==> t, takes 1*t <a href="#a87f9a39ecb1bec46adff5187bc899726"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a71be38a9fa2d89e147ac4fde35c49e21">canonMultConstConst</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &c1, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &c2)=0
<dl class="el"><dd class="mdescRight">c1*c2 ==> c', takes constant c1*c2 <a href="#a71be38a9fa2d89e147ac4fde35c49e21"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a96b1cb83272cf80c2de663de429e6a15">canonMultConstTerm</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &c1, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &c2, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &t)=0
<dl class="el"><dd class="mdescRight">c1*(c2*t) ==> c'*t, takes c1 and c2 and t <a href="#a96b1cb83272cf80c2de663de429e6a15"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a978068749de266dbbba2000d9e0c3d39">canonMultConstSum</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &c1, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &sum)=0
<dl class="el"><dd class="mdescRight">c1*(+ c2 v1 ...) ==> (+ c' c1v1 ...), takes c1 and the sum <a href="#a978068749de266dbbba2000d9e0c3d39"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a999f13a6fa4a6d8cbe97f02f93fc9ed3">canonPowConst</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &pow)=0
<dl class="el"><dd class="mdescRight">c^n = c' (compute the constant power expression) <a href="#a999f13a6fa4a6d8cbe97f02f93fc9ed3"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#af0f4877d7326a53faec76bef54a3d400">canonFlattenSum</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">flattens the input. accepts a PLUS expr <a href="#af0f4877d7326a53faec76bef54a3d400"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a1da0c47c02ff2392ca3e0b6493ac4823">canonComboLikeTerms</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">combine like terms. accepts a flattened PLUS expr <a href="#a1da0c47c02ff2392ca3e0b6493ac4823"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#af8f4f59bd12fdd8f93d1fd49ae41279e">multEqZero</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &expr)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#af17a5dbf4ebbe9d7e46d63ad1284ddaf">powEqZero</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &expr)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a0e6f19ba5333f667efa3a0e3d8787775">elimPower</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &expr)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a0e240fba4eac33522b24be6581d98346">elimPowerConst</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &expr, const <a class="el" href="classCVC3_1_1Rational.html">Rational</a> &root)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a80f948f405f0b1a88283c97b70aab43e">evenPowerEqNegConst</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &expr)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#aff57d78a7d743fffd21de7d4415df3e4">intEqIrrational</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &expr, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &isInt)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a8dd6bb6fed9a4745469b0cad5ed4a139">constPredicate</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">e0 @ e1 <==> true | false, where @ is {=,<,<=,>,>=} <a href="#a8dd6bb6fed9a4745469b0cad5ed4a139"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#acde77bf4aa73ff6b9a079b372ed7cc51">rightMinusLeft</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">e[0] @ e[1] <==> 0 @ e[1] - e[0], where @ is {=,<,<=,>,>=} <a href="#acde77bf4aa73ff6b9a079b372ed7cc51"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a0201544f06baaba23df9946f5da47978">leftMinusRight</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">e[0] @ e[1] <==> e[0] - e[1] @ 0, where @ is {=,<,<=,>,>=} <a href="#a0201544f06baaba23df9946f5da47978"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a0fa920a2a5cfa4419dbde10b1d913687">plusPredicate</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &x, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &y, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &z, int kind)=0
<dl class="el"><dd class="mdescRight">x @ y <==> x + z @ y + z, where @ is {=,<,<=,>,>=} (given as 'kind') <a href="#a0fa920a2a5cfa4419dbde10b1d913687"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#ad62d795eb10e67c655c608774881bde3">multEqn</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &x, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &y, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &z)=0
<dl class="el"><dd class="mdescRight">x = y <==> x * z = y * z, where z is a non-zero constant <a href="#ad62d795eb10e67c655c608774881bde3"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a419dd84177b5ca1fda7a23f3052b6132">divideEqnNonConst</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &x, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &y, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &z)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a70e83cfbc207a5d15fedd4adde7e9e76">multIneqn</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &z)=0
<dl class="el"><dd class="mdescRight">Multiplying inequation by a non-zero constant. <a href="#a70e83cfbc207a5d15fedd4adde7e9e76"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a646e312e12d5d23dca0c4db39d2c9fb9">eqToIneq</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">x = y ==> x <= y and x >= y <a href="#a646e312e12d5d23dca0c4db39d2c9fb9"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#aff4a01da77770b0b60089444c83c9cef">flipInequality</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">"op1 GE|GT op2" <==> op2 LE|LT op1 <a href="#aff4a01da77770b0b60089444c83c9cef"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#aee47bda46999143ea29d7d4ff0be89d4">negatedInequality</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">Propagating negation over <,<=,>,>=. <a href="#aee47bda46999143ea29d7d4ff0be89d4"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a203c7079289189cd4bf4f604c10645e5">realShadow</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &alphaLTt, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &tLTbeta)=0
<dl class="el"><dd class="mdescRight">Real shadow: a <(=) t, t <(=) b ==> a <(=) b. <a href="#a203c7079289189cd4bf4f604c10645e5"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a08dfccc28787af2a4141ed0f5a66bc9d">realShadowEq</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &alphaLEt, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &tLEalpha)=0
<dl class="el"><dd class="mdescRight">Projecting a tight inequality: alpha <= t <= alpha ==> t = alpha. <a href="#a08dfccc28787af2a4141ed0f5a66bc9d"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a5d419e48b93820624e356ba33efef27c">finiteInterval</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &aLEt, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &tLEac, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &isInta, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &isIntt)=0
<dl class="el"><dd class="mdescRight">Finite interval for integers: a <= t <= a + c ==> G(t, a, 0, c) <a href="#a5d419e48b93820624e356ba33efef27c"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a37835b10dd0f73b5c4cf36c1eebf0d1f">darkGrayShadow2ab</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &betaLEbx, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &axLEalpha, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &isIntAlpha, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &isIntBeta, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &isIntx)=0
<dl class="el"><dd class="mdescRight">Dark & Gray shadows when a <= b. <a href="#a37835b10dd0f73b5c4cf36c1eebf0d1f"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#ab17282c2e4de9965586f4821f17bf60d">darkGrayShadow2ba</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &betaLEbx, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &axLEalpha, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &isIntAlpha, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &isIntBeta, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &isIntx)=0
<dl class="el"><dd class="mdescRight">Dark & Gray shadows when b <= a. <a href="#ab17282c2e4de9965586f4821f17bf60d"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a94ffe313b29aa63c32d5c3facb3bc917">expandDarkShadow</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &darkShadow)=0
<dl class="el"><dd class="mdescRight">DARK_SHADOW(t1, t2) ==> t1 <= t2. <a href="#a94ffe313b29aa63c32d5c3facb3bc917"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a32df170ed2ec7fb3d1c7541e6f3dda77">expandGrayShadow0</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &g)=0
<dl class="el"><dd class="mdescRight">GRAY_SHADOW(v, e, c, c) ==> v=e+c. <a href="#a32df170ed2ec7fb3d1c7541e6f3dda77"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a4b6ef5b29b05bada6ea2df72873abea6">splitGrayShadow</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &g)=0
<dl class="el"><dd class="mdescRight">G(x, e, c1, c2) ==> (G1 or G2) and (!G1 or !G2) <a href="#a4b6ef5b29b05bada6ea2df72873abea6"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#aa33975feef2a9cdd513e5d641f14dc7a">splitGrayShadowSmall</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &g)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#af936b764ef75b0a6f63043d01a819044">expandGrayShadow</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &g)=0
<dl class="el"><dd class="mdescRight">G(x, e, c1, c2) ==> e+c1 <= x AND x <= e+c2. <a href="#af936b764ef75b0a6f63043d01a819044"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a3083a3c5893123f2a3ec54ce31718e09">expandGrayShadowConst</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &g)=0
<dl class="el"><dd class="mdescRight">Optimized rules: GRAY_SHADOW(a*x, c, c1, c2) ==> [expansion]. <a href="#a3083a3c5893123f2a3ec54ce31718e09"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a597adbe8879c33bffefae537a5bca7c0">grayShadowConst</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &g)=0
<dl class="el"><dd class="mdescRight">|- G(ax, c, c1, c2) ==> |- G(x, 0, ceil((c1+c)/a), floor((c2+c)/a)) <a href="#a597adbe8879c33bffefae537a5bca7c0"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a7a0dad5cb9c2815421457dabc25bc537">lessThanToLE</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &less, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &isIntLHS, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &isIntRHS, bool changeRight)=0
<dl class="el"><dd class="mdescRight">a,b: INT; a < b ==> a <= b-1 [or a+1 <= b] <a href="#a7a0dad5cb9c2815421457dabc25bc537"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#af5cfb693ee5ee6f3463e83f01196b31e">lessThanToLERewrite</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &ineq, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &isIntLHS, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &isIntRHS, bool changeRight)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a62d76b2ccca8af5e1f28c5104ea2e313">intVarEqnConst</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &eqn, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &isIntx)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a8c3d5fdc2b0c9c11291d41c3c20067e4">IsIntegerElim</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &isIntx)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a08b14a730bbc6b4ca28bb808e6f6dc85">eqElimIntRule</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &eqn, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &isIntx, const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &isIntVars)=0
<dl class="el"><dd class="mdescRight">Equality elimination rule for integers: </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\mathsf{int}(a\cdot x)\quad \mathsf{int}(C+\sum_{i=1}^{n}a_{i}\cdot x_{i})} {a\cdot x=C+\sum_{i=1}^{n}a_{i}\cdot x_{i} \quad\equiv\quad x=t_{2}\wedge 0=t_{3}} \]" src="form_311.png"/>
</p>
<p> See the detailed description for explanations. <a href="#a08b14a730bbc6b4ca28bb808e6f6dc85"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a5e9bccd77000156ab34b0b42d3e3bb18">isIntConst</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<dl class="el"><dd class="mdescRight">return e <=> TRUE/FALSE for e == IS_INTEGER(c), where c is a constant <a href="#a5e9bccd77000156ab34b0b42d3e3bb18"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#ac05fd3606540a5222ebaa68f9091345b">equalLeaves1</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a5052c783af25243987424ef66e2bf5fc">equalLeaves2</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a893c86f0404789d229540f7a0a00df89">equalLeaves3</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#aa9018c4d16d3d0a2d8f1614f8e7cae23">equalLeaves4</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#af180898d9f1d255ef3a2f528ecd8ac65">diseqToIneq</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &diseq)=0
<dl class="el"><dd class="mdescRight">x /= y ==> (x < y) OR (x > y) <a href="#af180898d9f1d255ef3a2f528ecd8ac65"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a24ea340651805e648d7180debad17225">dummyTheorem</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a1ebae10d65430ab1a3a14c866af93de6">oneElimination</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &x)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#ad0b23fb01a7adea349c8958059b9f7fd">clashingBounds</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &lowerBound, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &upperBound)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#ac06dd83948d0f3e474f073ecac592343">addInequalities</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm1, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm2)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#ab87b1e3a09aa830063d51c24a2147095">addInequalities</a> (const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &thms)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a9abe85f95b61d94fa308a0b15f2b2ef8">implyWeakerInequality</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &expr1, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &expr2)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a5eaf4d106f7ce86227ab1d96ffc66b55">implyNegatedInequality</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &expr1, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &expr2)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a0090e0d4065efbf936ec92f0e99935e9">integerSplit</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &intVar, const <a class="el" href="classCVC3_1_1Rational.html">Rational</a> &intPoint)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a11976de555ee2e88236575893f2ed766">trustedRewrite</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &expr1, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &expr2)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a4b61e3ea9d5ac911806de95241cf35de">rafineStrictInteger</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &isIntConstrThm, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &constr)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a95bc88d9e126e6b9c938691ce92985aa">simpleIneqInt</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &ineq, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &isIntRHS)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a93489420e882a93eb308c7d99c27dc1e">intEqualityRationalConstant</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &isIntConstrThm, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &constr)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a5a544980652c3f6793057b16cbc43cf9">cycleConflict</a> (const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &inequalitites)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a5b475214a53d70298e55f4ac5f3db71f">implyEqualities</a> (const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &inequalities)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#aafc12b4bdf180f3475ecf4eaa40648d9">implyWeakerInequalityDiffLogic</a> (const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &antecedentThms, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &implied)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a61ecf1cfc7219c010519cd90cb31d465">implyNegatedInequalityDiffLogic</a> (const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &antecedentThms, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &implied)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#ac48d6f8b2ad8e8f8fefac775d33825b5">expandGrayShadowRewrite</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &theShadow)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a98020e790bcb60c9c2cc5a7e406f500f">compactNonLinearTerm</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &nonLinear)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#aa6874fa9f5b02db0adb8149af9664b05">nonLinearIneqSignSplit</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &ineqThm)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#af80ad28bb01d8a37e32f29c746d22dbc">implyDiffLogicBothBounds</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &x, std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &c1_le_x, <a class="el" href="classCVC3_1_1Rational.html">Rational</a> c1, std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &x_le_c2, <a class="el" href="classCVC3_1_1Rational.html">Rational</a> c2)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#ad3dee93f4078a4fc79ccacef33f05119">powerOfOne</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)=0
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ArithProofRules.html#a81d9ea1e5c2d42c2b60a893c879145bd">rewriteLeavesConst</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
</ul>
<hr/><a name="details" id="details"></a><h2>Detailed Description</h2>
<div class="textblock">
<p>Definition at line <a class="el" href="arith__proof__rules_8h_source.html#l00033">33</a> of file <a class="el" href="arith__proof__rules_8h_source.html">arith_proof_rules.h</a>.</p>
</div><hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="a410c697fc050feca9680a388397b0968"></a><!-- doxytag: member="CVC3::ArithProofRules::~ArithProofRules" ref="a410c697fc050feca9680a388397b0968" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual CVC3::ArithProofRules::~ArithProofRules </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="arith__proof__rules_8h_source.html#l00036">36</a> of file <a class="el" href="arith__proof__rules_8h_source.html">arith_proof_rules.h</a>.</p>
</div>
</div>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="a8b8db5ad0a8d4968f429e98964db93c1"></a><!-- doxytag: member="CVC3::ArithProofRules::varToMult" ref="a8b8db5ad0a8d4968f429e98964db93c1" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::varToMult </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> e = 1 * e </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a7568925b6c26f1c7ba882893f596d214">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a23340f90880cb869fdcfe6e69a7a2631">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#aebcc9153d9e9bfff3678c271674a6053">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="aa95faca93e7b4a1cf21667ff88d390e4"></a><!-- doxytag: member="CVC3::ArithProofRules::uMinusToMult" ref="aa95faca93e7b4a1cf21667ff88d390e4" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::uMinusToMult </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> -(e) = (-1) * e </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#aaafdbe9dcc49728cc2bf16b43045c193">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a878e091ad5cfd2877ddce73d6f664e16">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a8165eb2a8fea70e0d1d2c8ebb1358855">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a4319c532082c0f43794b34a2fb9df73f"></a><!-- doxytag: member="CVC3::ArithProofRules::minusToPlus" ref="a4319c532082c0f43794b34a2fb9df73f" args="(const Expr &x, const Expr &y)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::minusToPlus </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>x</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>y</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> x - y = x + (-1) * y </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ab369e518fc2ee411503253fa0b1515d6">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ab0d610d377cc20e3ce16823713d25403">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#ae3458f7b381a95e124e3204ed66904ef">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a0053398d4a8fc49d9a2f8ede6949fc70"></a><!-- doxytag: member="CVC3::ArithProofRules::canonUMinusToDivide" ref="a0053398d4a8fc49d9a2f8ede6949fc70" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::canonUMinusToDivide </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>-(e) ==> e / (-1); takes 'e'</p>
<p>Canon Rule for unary minus: it just converts it to division by -1, the result is not yet canonical: </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a4671174ae8ff61c52f16ddd53a3cdd27">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a9bf439248afb24bb63ea435193b68524">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a693a5043cf100f13390b358290940dd5">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a18e5970bc4f670a63ca5775750f099ab"></a><!-- doxytag: member="CVC3::ArithProofRules::moveSumConstantRight" ref="a18e5970bc4f670a63ca5775750f099ab" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::moveSumConstantRight </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Transform e = (SUM r t1 ... tn) @ 0 into (SUM t1 ... tn) @ -r. The first sum term (r) must be a rational and t1 ... tn terms must be canonised.</p>
<dl><dt><b>Parameters:</b></dt><dd>
<table class="params">
<tr><td class="paramname">e</td><td>the expression to transform </td></tr>
</table>
</dd>
</dl>
<dl class="return"><dt><b>Returns:</b></dt><dd>rewrite theorem representing the transformation </dd></dl>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a77b99e94956d407e5cd20701e6771120">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aad289f36b55fe8be7f7af0f62aedaae8">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a2b44fabb65bb6748259aee8959be465e">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a79c759f2bb7dc41ed98c5962febef804"></a><!-- doxytag: member="CVC3::ArithProofRules::canonDivideConst" ref="a79c759f2bb7dc41ed98c5962febef804" args="(const Expr &c, const Expr &d)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::canonDivideConst </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>c</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>d</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>(c) / d ==> (c/d), takes c and d </p>
<p>Canon Rules for division by constant 'd' </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a515e5d076ed135a6d943c2f5d5e34188">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a3a2bf5e3b8c71543b1512f1606825a02">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a237d508b95295db21e9ce21172d4366a">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="aee487a2a1e8ce4c34075568eb70ea874"></a><!-- doxytag: member="CVC3::ArithProofRules::canonDivideMult" ref="aee487a2a1e8ce4c34075568eb70ea874" args="(const Expr &cx, const Expr &d)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::canonDivideMult </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>cx</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>d</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>(c * x) / d ==> (c/d) * x, takes (c*x) and d </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a4d2d8da9de6d6faaa07758c01e3a9fe8">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a39a2efadcc13383fd860340c6d76db54">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#aea8367eb1c88d26b83aea3e5e63f66db">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a92846ee0cdab98d1759a13ff7e8d710d"></a><!-- doxytag: member="CVC3::ArithProofRules::canonDividePlus" ref="a92846ee0cdab98d1759a13ff7e8d710d" args="(const Expr &e, const Expr &d)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::canonDividePlus </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>d</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>(+ c ...)/d ==> push division to all the coefficients. </p>
<p>The result is not canonical, but canonizing the summands will make it canonical. Takes (+ c ...) and d </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a4338b85f1dd0fca0cc58e6b7259a20b4">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a897c950b6bb741189f1c33752159b587">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a844e1fe500be8d1c083ddf6c06fcc85c">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a4ab0351b340ecb82d6ced530e4f30510"></a><!-- doxytag: member="CVC3::ArithProofRules::canonDivideVar" ref="a4ab0351b340ecb82d6ced530e4f30510" args="(const Expr &e, const Expr &d)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::canonDivideVar </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>d</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>x / d ==> (1/d) * x, takes x and d </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#aa651eb7a4d20a77135efa2d3e984c355">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a9fddb49ed54796e6a5487be554eb14f4">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#af79a13a84e24d58135d13d7520726134">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="aa38d5c06ebe0b672570641fe933cfedb"></a><!-- doxytag: member="CVC3::ArithProofRules::canonMultMtermMterm" ref="aa38d5c06ebe0b672570641fe933cfedb" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::canonMultMtermMterm </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ab5166b206f49897a6a49ba0014c0b808">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aa1ab000ca8a6a2605b2cb57f8b881d91">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#ad7982dec66d9ebd08596c5b7d352604b">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a225fe511e6f654f313048e86c1550510"></a><!-- doxytag: member="CVC3::ArithProofRules::canonPlus" ref="a225fe511e6f654f313048e86c1550510" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::canonPlus </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Canonize (PLUS t1 ... tn) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a41f7000c783a82e9a86cad823b06bff4">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#acbd2c2b8d5a0728aa00dcf55c7c646f2">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a4a213b741317120ee84b6e61f50e484f">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__new_8cpp_source.html#l03662">CVC3::TheoryArithNew::getLowerBoundExplanation()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l03749">CVC3::TheoryArithNew::getUpperBoundExplanation()</a>, and <a class="el" href="theory__arith__new_8cpp_source.html#l01570">CVC3::TheoryArithNew::rewrite()</a>.</p>
</div>
</div>
<a class="anchor" id="aca910e6ff44389aac100b14b486c1942"></a><!-- doxytag: member="CVC3::ArithProofRules::canonMult" ref="aca910e6ff44389aac100b14b486c1942" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::canonMult </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Canonize (MULT t1 ... tn) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a9bd77385dd0cbaac271aaab4b6c6ec09">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a627a219305f83b200e36b28b1865729a">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a50819c4cc053538490a2cbb535edf39d">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a9a806d487932bbfa9a019d4d1eed1cea"></a><!-- doxytag: member="CVC3::ArithProofRules::canonInvert" ref="a9a806d487932bbfa9a019d4d1eed1cea" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::canonInvert </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>==> 1/e = e' where e' is canonical; takes e. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a7c7c860b193ec63a776dd13613aeca25">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a1a4b78b01763b1ca5a80c0211bc3ba4b">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a67391e426738cbd4a15f6fbc5b2d19e1">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a198b0b44145b8e33555ffd212f43b7b3"></a><!-- doxytag: member="CVC3::ArithProofRules::canonDivide" ref="a198b0b44145b8e33555ffd212f43b7b3" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::canonDivide </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Canonize t1/t2. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a92540cc58f6203c2904fc2bd197190da">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#acfe4060947cb28e9fc9c4ea859df565c">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#aec48ed7710110960c6f87e6946500494">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a11870b90dbfcc61d2b9a2820df7f6057"></a><!-- doxytag: member="CVC3::ArithProofRules::canonMultTermConst" ref="a11870b90dbfcc61d2b9a2820df7f6057" args="(const Expr &c, const Expr &t)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::canonMultTermConst </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>c</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>t</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>t*c ==> c*t, takes constant c and term t </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#af6ba91fa47c4c9139c4d93fe3de0112f">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a401fca0c453a94c8c0053eb77e014af0">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a70d0d0fa8c08582a17399c0570812afa">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__new_8cpp_source.html#l03662">CVC3::TheoryArithNew::getLowerBoundExplanation()</a>, and <a class="el" href="theory__arith__new_8cpp_source.html#l03749">CVC3::TheoryArithNew::getUpperBoundExplanation()</a>.</p>
</div>
</div>
<a class="anchor" id="a8b9abf99f0b013714eaaa49e81a618b9"></a><!-- doxytag: member="CVC3::ArithProofRules::canonMultTerm1Term2" ref="a8b9abf99f0b013714eaaa49e81a618b9" args="(const Expr &t1, const Expr &t2)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::canonMultTerm1Term2 </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>t1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>t2</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>t1*t2 ==> Error, takes t1 and t2 where both are non-constants </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a529fe89fea243d932879a1a74e9d36a7">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a294916be1e9ac30e3c824b0b8e4ff093">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a10ed8952ec021d78cf1bc8b60e6634c6">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="aae559b4d1558fecba5621c9ba27daa88"></a><!-- doxytag: member="CVC3::ArithProofRules::canonMultZero" ref="aae559b4d1558fecba5621c9ba27daa88" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::canonMultZero </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>0*t ==> 0, takes 0*t </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a55ec89d6cf310694e9f4b1013a795ce2">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a55fb07d5df2b4068bf5df327ae0d89d4">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#af62a070ed7a3a326db5b121b282bd47c">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a87f9a39ecb1bec46adff5187bc899726"></a><!-- doxytag: member="CVC3::ArithProofRules::canonMultOne" ref="a87f9a39ecb1bec46adff5187bc899726" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::canonMultOne </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>1*t ==> t, takes 1*t </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ae5a6e1b2c7b9239b7e53027c51a2dc7e">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aed0a2d1337910f3027ac867e0f18b8de">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#abc03e832be081de0ca6f7f4e905e0f4f">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a71be38a9fa2d89e147ac4fde35c49e21"></a><!-- doxytag: member="CVC3::ArithProofRules::canonMultConstConst" ref="a71be38a9fa2d89e147ac4fde35c49e21" args="(const Expr &c1, const Expr &c2)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::canonMultConstConst </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>c1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>c2</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>c1*c2 ==> c', takes constant c1*c2 </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#affbdf02016310d8cd6a9037fdd9eddc6">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a4ea3884dff8c1606fd05e61eb78e379d">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a3c1740f98f0ac4952c8d7a721767535e">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__new_8cpp_source.html#l03662">CVC3::TheoryArithNew::getLowerBoundExplanation()</a>, and <a class="el" href="theory__arith__new_8cpp_source.html#l03749">CVC3::TheoryArithNew::getUpperBoundExplanation()</a>.</p>
</div>
</div>
<a class="anchor" id="a96b1cb83272cf80c2de663de429e6a15"></a><!-- doxytag: member="CVC3::ArithProofRules::canonMultConstTerm" ref="a96b1cb83272cf80c2de663de429e6a15" args="(const Expr &c1, const Expr &c2, const Expr &t)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::canonMultConstTerm </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>c1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>c2</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>t</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>c1*(c2*t) ==> c'*t, takes c1 and c2 and t </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ad51f0d5c3232b6c247939a10e253f53d">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a9e5b7c75f1f662071942150df1a4d69e">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a8e0a636c4ee9bb70b8f36ee3f6acab49">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a978068749de266dbbba2000d9e0c3d39"></a><!-- doxytag: member="CVC3::ArithProofRules::canonMultConstSum" ref="a978068749de266dbbba2000d9e0c3d39" args="(const Expr &c1, const Expr &sum)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::canonMultConstSum </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>c1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>sum</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>c1*(+ c2 v1 ...) ==> (+ c' c1v1 ...), takes c1 and the sum </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ab0e0e14c71501a9f8208963c54010fe4">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a2765c1485aac81cc42ed3186f7a1f244">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a5892d8574e2787b95005211cf0517952">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a999f13a6fa4a6d8cbe97f02f93fc9ed3"></a><!-- doxytag: member="CVC3::ArithProofRules::canonPowConst" ref="a999f13a6fa4a6d8cbe97f02f93fc9ed3" args="(const Expr &pow)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::canonPowConst </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>pow</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>c^n = c' (compute the constant power expression) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#af673275ae1c3dc606b29979b60df35c5">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a5347a8208d4d7aa05fad463bd6da8c41">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a7b083f1e452bd42475d9f0b313651fac">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="af0f4877d7326a53faec76bef54a3d400"></a><!-- doxytag: member="CVC3::ArithProofRules::canonFlattenSum" ref="af0f4877d7326a53faec76bef54a3d400" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::canonFlattenSum </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>flattens the input. accepts a PLUS expr </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a19964269c705bafbe69cb1052fe7bec8">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a5ec4889e730c0b1d4fb584d16af08a9d">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#aba0cab7c4879b336dfac9cd1673be1c8">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a1da0c47c02ff2392ca3e0b6493ac4823"></a><!-- doxytag: member="CVC3::ArithProofRules::canonComboLikeTerms" ref="a1da0c47c02ff2392ca3e0b6493ac4823" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::canonComboLikeTerms </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>combine like terms. accepts a flattened PLUS expr </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ac9ee451992ab00f200ee8aee26e99e0c">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a245f64776d0b1fbd14d18bb145f717e4">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a7f2a1a065eac005fa6b47c32040d9401">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="af8f4f59bd12fdd8f93d1fd49ae41279e"></a><!-- doxytag: member="CVC3::ArithProofRules::multEqZero" ref="af8f4f59bd12fdd8f93d1fd49ae41279e" args="(const Expr &expr)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::multEqZero </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>expr</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a0040d5d848f7040df940b92d95a75930">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a57eafe7c2a127ca4b4706437b777d610">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#ad73622cdec4a472af97d68de6716fe0a">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l03076">CVC3::TheoryArithOld::rewrite()</a>.</p>
</div>
</div>
<a class="anchor" id="af17a5dbf4ebbe9d7e46d63ad1284ddaf"></a><!-- doxytag: member="CVC3::ArithProofRules::powEqZero" ref="af17a5dbf4ebbe9d7e46d63ad1284ddaf" args="(const Expr &expr)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::powEqZero </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>expr</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a9cd618abf322c0389f1fc40f274059c2">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#acbea7826fe54b91e8d4bc2c21f7137ae">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a9cc96dbb9ae7fa063146b9924f51fe68">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a0e6f19ba5333f667efa3a0e3d8787775"></a><!-- doxytag: member="CVC3::ArithProofRules::elimPower" ref="a0e6f19ba5333f667efa3a0e3d8787775" args="(const Expr &expr)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::elimPower </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>expr</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a3c454b863142345e1093663fbb89d306">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ab29b63e40b7f2c624e6e4f11c4eff27e">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#aeed414c650deb9b1e619ffb8f3266ea4">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l03076">CVC3::TheoryArithOld::rewrite()</a>.</p>
</div>
</div>
<a class="anchor" id="a0e240fba4eac33522b24be6581d98346"></a><!-- doxytag: member="CVC3::ArithProofRules::elimPowerConst" ref="a0e240fba4eac33522b24be6581d98346" args="(const Expr &expr, const Rational &root)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::elimPowerConst </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>expr</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Rational.html">Rational</a> & </td>
<td class="paramname"><em>root</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a21456f49d3a6711f21e3c13fb3c0d34a">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a942f9f0fc0ceff798b607e9fe032175a">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a2483c968c6a4d7f8ae63595c839b70f2">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l03076">CVC3::TheoryArithOld::rewrite()</a>.</p>
</div>
</div>
<a class="anchor" id="a80f948f405f0b1a88283c97b70aab43e"></a><!-- doxytag: member="CVC3::ArithProofRules::evenPowerEqNegConst" ref="a80f948f405f0b1a88283c97b70aab43e" args="(const Expr &expr)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::evenPowerEqNegConst </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>expr</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#afbf059903de8b1e87aef9a4a75340d6c">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#abe913a6cc9430faf8f0ac50ec51aa36c">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#afe5f71b9fdeb8be95e0e71e94df0b598">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l03076">CVC3::TheoryArithOld::rewrite()</a>.</p>
</div>
</div>
<a class="anchor" id="aff57d78a7d743fffd21de7d4415df3e4"></a><!-- doxytag: member="CVC3::ArithProofRules::intEqIrrational" ref="aff57d78a7d743fffd21de7d4415df3e4" args="(const Expr &expr, const Theorem &isInt)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::intEqIrrational </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>expr</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>isInt</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#aa3838fe1c003a9f47f3ec8344d192dea">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a946832931094bb746277d8b95c471690">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a75a67906db6381d408ea1a9830c36cf7">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l03076">CVC3::TheoryArithOld::rewrite()</a>.</p>
</div>
</div>
<a class="anchor" id="a8dd6bb6fed9a4745469b0cad5ed4a139"></a><!-- doxytag: member="CVC3::ArithProofRules::constPredicate" ref="a8dd6bb6fed9a4745469b0cad5ed4a139" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::constPredicate </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>e0 @ e1 <==> true | false, where @ is {=,<,<=,>,>=} </p>
<dl><dt><b>Parameters:</b></dt><dd>
<table class="params">
<tr><td class="paramname">e</td><td>takes e is (e0@e1) where e0 and e1 are constants </td></tr>
</table>
</dd>
</dl>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a621015d4894231ecd9ab465494e9c9c8">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a7a2a8059fa49da5a8877b28b1cfa445a">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#aefea69c7f808394db447b9ed658c59fa">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l03076">CVC3::TheoryArithOld::rewrite()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l01570">CVC3::TheoryArithNew::rewrite()</a>, and <a class="el" href="theory__arith3_8cpp_source.html#l02387">CVC3::TheoryArith3::rewrite()</a>.</p>
</div>
</div>
<a class="anchor" id="acde77bf4aa73ff6b9a079b372ed7cc51"></a><!-- doxytag: member="CVC3::ArithProofRules::rightMinusLeft" ref="acde77bf4aa73ff6b9a079b372ed7cc51" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::rightMinusLeft </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>e[0] @ e[1] <==> 0 @ e[1] - e[0], where @ is {=,<,<=,>,>=} </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a3eb1309c184247837239c098d9c9100a">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aca76a2dbee73d7ad9e2529ac8ce142a4">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a088b20af694e737e1c7ff12d2ff74d7c">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l03076">CVC3::TheoryArithOld::rewrite()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l01570">CVC3::TheoryArithNew::rewrite()</a>, and <a class="el" href="theory__arith3_8cpp_source.html#l02387">CVC3::TheoryArith3::rewrite()</a>.</p>
</div>
</div>
<a class="anchor" id="a0201544f06baaba23df9946f5da47978"></a><!-- doxytag: member="CVC3::ArithProofRules::leftMinusRight" ref="a0201544f06baaba23df9946f5da47978" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::leftMinusRight </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>e[0] @ e[1] <==> e[0] - e[1] @ 0, where @ is {=,<,<=,>,>=} </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a8196042ba713a7c782ee4b5eb4c69ccc">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aedad2be1c60515921f8c3761581afca5">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a36301e14b9eb42fc9842a3a7f60f8b17">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a0fa920a2a5cfa4419dbde10b1d913687"></a><!-- doxytag: member="CVC3::ArithProofRules::plusPredicate" ref="a0fa920a2a5cfa4419dbde10b1d913687" args="(const Expr &x, const Expr &y, const Expr &z, int kind)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::plusPredicate </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>x</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>y</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>z</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>kind</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>x @ y <==> x + z @ y + z, where @ is {=,<,<=,>,>=} (given as 'kind') </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a3c3041eb3b0144e21d72ffe6999953e2">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ab190e4d8fefb74f2a8117ca17ae49b48">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a35577ad70c513422af5cbfca00cde1e2">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__new_8cpp_source.html#l03600">CVC3::TheoryArithNew::pivotRule()</a>, and <a class="el" href="theory__arith__new_8cpp_source.html#l01570">CVC3::TheoryArithNew::rewrite()</a>.</p>
</div>
</div>
<a class="anchor" id="ad62d795eb10e67c655c608774881bde3"></a><!-- doxytag: member="CVC3::ArithProofRules::multEqn" ref="ad62d795eb10e67c655c608774881bde3" args="(const Expr &x, const Expr &y, const Expr &z)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::multEqn </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>x</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>y</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>z</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>x = y <==> x * z = y * z, where z is a non-zero constant </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ae66ddbc1457e3c032ea9059625059992">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#afd7a6da45999fb3237cdbbbf9c5f19e8">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#aeb54d03f4672718b7de6160a88bf33cb">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l02994">CVC3::TheoryArithOld::normalize()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02319">CVC3::TheoryArith3::normalize()</a>, and <a class="el" href="theory__arith__new_8cpp_source.html#l03600">CVC3::TheoryArithNew::pivotRule()</a>.</p>
</div>
</div>
<a class="anchor" id="a419dd84177b5ca1fda7a23f3052b6132"></a><!-- doxytag: member="CVC3::ArithProofRules::divideEqnNonConst" ref="a419dd84177b5ca1fda7a23f3052b6132" args="(const Expr &x, const Expr &y, const Expr &z)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::divideEqnNonConst </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>x</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>y</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>z</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#aa371616db9ac1a4a9c7a4b1ce0f2a05c">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a7bf31f4d4bd6e3f7ff7e37dd5236a792">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a16c7325daba5b9e8cea7284fafaa5382">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l03076">CVC3::TheoryArithOld::rewrite()</a>.</p>
</div>
</div>
<a class="anchor" id="a70e83cfbc207a5d15fedd4adde7e9e76"></a><!-- doxytag: member="CVC3::ArithProofRules::multIneqn" ref="a70e83cfbc207a5d15fedd4adde7e9e76" args="(const Expr &e, const Expr &z)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::multIneqn </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>z</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Multiplying inequation by a non-zero constant. </p>
<p>z>0 ==> e[0] @ e[1] <==> e[0]*z @ e[1]*z</p>
<p>z<0 ==> e[0] @ e[1] <==> e[1]*z @ e[0]*z</p>
<p>for @ in {<,<=,>,>=}: </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a3d245f36a2e42684ec2fd9356d89111f">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a8af6455fe4a8889cfb7b0b8c865b847c">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#aa425318a5846e14a94b2a3a34bb99b6d">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__new_8cpp_source.html#l03662">CVC3::TheoryArithNew::getLowerBoundExplanation()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l03749">CVC3::TheoryArithNew::getUpperBoundExplanation()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l02994">CVC3::TheoryArithOld::normalize()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l01468">CVC3::TheoryArithNew::normalize()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02319">CVC3::TheoryArith3::normalize()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l01168">CVC3::TheoryArithNew::processFiniteInterval()</a>, and <a class="el" href="theory__arith3_8cpp_source.html#l01917">CVC3::TheoryArith3::processFiniteInterval()</a>.</p>
</div>
</div>
<a class="anchor" id="a646e312e12d5d23dca0c4db39d2c9fb9"></a><!-- doxytag: member="CVC3::ArithProofRules::eqToIneq" ref="a646e312e12d5d23dca0c4db39d2c9fb9" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::eqToIneq </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>x = y ==> x <= y and x >= y </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a517d45514aefcab0dc6aabb400f149fd">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ad2f144d3a2ffe108e0d8e7df8e263832">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a8edb275846dc5d938d3a8716436f0e1e">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l03076">CVC3::TheoryArithOld::rewrite()</a>, and <a class="el" href="theory__arith__new_8cpp_source.html#l01570">CVC3::TheoryArithNew::rewrite()</a>.</p>
</div>
</div>
<a class="anchor" id="aff4a01da77770b0b60089444c83c9cef"></a><!-- doxytag: member="CVC3::ArithProofRules::flipInequality" ref="aff4a01da77770b0b60089444c83c9cef" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::flipInequality </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>"op1 GE|GT op2" <==> op2 LE|LT op1 </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#af069fc1b320c0455ec7cde192668884b">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a216a950228aad3cdef0c5dd5213be4fb">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a86c578d9592d6782d2224118b755e0fa">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l03076">CVC3::TheoryArithOld::rewrite()</a>, and <a class="el" href="theory__arith3_8cpp_source.html#l02387">CVC3::TheoryArith3::rewrite()</a>.</p>
</div>
</div>
<a class="anchor" id="aee47bda46999143ea29d7d4ff0be89d4"></a><!-- doxytag: member="CVC3::ArithProofRules::negatedInequality" ref="aee47bda46999143ea29d7d4ff0be89d4" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::negatedInequality </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Propagating negation over <,<=,>,>=. </p>
<p>NOT (op1 < op2) <==> (op1 >= op2)</p>
<p>NOT (op1 <= op2) <==> (op1 > op2)</p>
<p>NOT (op1 > op2) <==> (op1 <= op2)</p>
<p>NOT (op1 >= op2) <==> (op1 < op2) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a07368f8a2e12b5c189645a99bc934102">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a27bb939c33616b21a83aabdb5d47a660">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a0b1fba36612db00956767d73bb1b6623">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith3_8cpp_source.html#l02020">CVC3::TheoryArith3::assertFact()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03076">CVC3::TheoryArithOld::rewrite()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l01570">CVC3::TheoryArithNew::rewrite()</a>, and <a class="el" href="theory__arith3_8cpp_source.html#l02387">CVC3::TheoryArith3::rewrite()</a>.</p>
</div>
</div>
<a class="anchor" id="a203c7079289189cd4bf4f604c10645e5"></a><!-- doxytag: member="CVC3::ArithProofRules::realShadow" ref="a203c7079289189cd4bf4f604c10645e5" args="(const Theorem &alphaLTt, const Theorem &tLTbeta)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::realShadow </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>alphaLTt</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>tLTbeta</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Real shadow: a <(=) t, t <(=) b ==> a <(=) b. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a8092c96a87d952fc1e572bb9237ff994">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a6f08ce700f85f9ba2967ecee42e7a550">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a8f7858787d55442d57e5924dd232f842">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a08dfccc28787af2a4141ed0f5a66bc9d"></a><!-- doxytag: member="CVC3::ArithProofRules::realShadowEq" ref="a08dfccc28787af2a4141ed0f5a66bc9d" args="(const Theorem &alphaLEt, const Theorem &tLEalpha)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::realShadowEq </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>alphaLEt</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>tLEalpha</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Projecting a tight inequality: alpha <= t <= alpha ==> t = alpha. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a6e14251c516153e14539a34598daca04">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a955e74558aee9ebc9de4c084819e93ac">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a5033cb7a4be3d2e9bc1cd60582482c5f">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a5d419e48b93820624e356ba33efef27c"></a><!-- doxytag: member="CVC3::ArithProofRules::finiteInterval" ref="a5d419e48b93820624e356ba33efef27c" args="(const Theorem &aLEt, const Theorem &tLEac, const Theorem &isInta, const Theorem &isIntt)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::finiteInterval </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>aLEt</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>tLEac</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>isInta</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>isIntt</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Finite interval for integers: a <= t <= a + c ==> G(t, a, 0, c) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a7f4c82e18e7a3ed3b5b22a6ce7d7cf27">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aaba7798eb77a93ac0de8978507dca731">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#ae2869b5a206710a6c890d81ded080838">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__new_8cpp_source.html#l01168">CVC3::TheoryArithNew::processFiniteInterval()</a>, and <a class="el" href="theory__arith3_8cpp_source.html#l01917">CVC3::TheoryArith3::processFiniteInterval()</a>.</p>
</div>
</div>
<a class="anchor" id="a37835b10dd0f73b5c4cf36c1eebf0d1f"></a><!-- doxytag: member="CVC3::ArithProofRules::darkGrayShadow2ab" ref="a37835b10dd0f73b5c4cf36c1eebf0d1f" args="(const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::darkGrayShadow2ab </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>betaLEbx</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>axLEalpha</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>isIntAlpha</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>isIntBeta</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>isIntx</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Dark & Gray shadows when a <= b. </p>
<p>takes two integer ineqs (i.e. all vars are ints) "|- beta <= b.x" and "|- a.x <= alpha" and checks if "1 <= a <= b" and returns (D or G) and (!D or !G), where D = Dark_Shadow(ab-1, b.alpha - a.beta), G = Gray_Shadow(a.x, alpha, -(a-1), 0). </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#aef6fd1261bea182d4554d0423803b05e">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a2ad479414c401fb8a4ea9631cbdd95c0">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a07e973f55e9daf1def982c84c3a078b1">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="ab17282c2e4de9965586f4821f17bf60d"></a><!-- doxytag: member="CVC3::ArithProofRules::darkGrayShadow2ba" ref="ab17282c2e4de9965586f4821f17bf60d" args="(const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::darkGrayShadow2ba </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>betaLEbx</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>axLEalpha</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>isIntAlpha</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>isIntBeta</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>isIntx</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Dark & Gray shadows when b <= a. </p>
<p>takes two integer ineqs (i.e. all vars are ints) "|- beta <= b.x" and "|- a.x <= alpha" and checks if "1 <= b < a" and returns (D or G) and (!D or !G), where D = Dark_Shadow(ab-1, b.alpha - a.beta), G = Gray_Shadow(b.x, beta, 0, b-1). </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#aaf64935bb620ab79fd7383f1913bd8b8">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a8b2e8589d24fc69616ba431588c50b3e">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#ae27df6e46accf919b67dda1cb914c160">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a94ffe313b29aa63c32d5c3facb3bc917"></a><!-- doxytag: member="CVC3::ArithProofRules::expandDarkShadow" ref="a94ffe313b29aa63c32d5c3facb3bc917" args="(const Theorem &darkShadow)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::expandDarkShadow </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>darkShadow</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>DARK_SHADOW(t1, t2) ==> t1 <= t2. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#aafadfc6ae6013ab18a7b4ee570cce16a">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a372efa694fb08c901deff55f5f108ffb">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a0b28ed8d0e2ef812bcfc8bba931e46cd">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l02481">CVC3::TheoryArithOld::assertFact()</a>, and <a class="el" href="theory__arith3_8cpp_source.html#l02020">CVC3::TheoryArith3::assertFact()</a>.</p>
</div>
</div>
<a class="anchor" id="a32df170ed2ec7fb3d1c7541e6f3dda77"></a><!-- doxytag: member="CVC3::ArithProofRules::expandGrayShadow0" ref="a32df170ed2ec7fb3d1c7541e6f3dda77" args="(const Theorem &g)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::expandGrayShadow0 </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>g</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>GRAY_SHADOW(v, e, c, c) ==> v=e+c. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ac8a2c0a97ace8f17153ad784c87ba5a2">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aacc831490c52da277133fe625522216f">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a273501b582758aca3ebabe6bd3ce83e4">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l02481">CVC3::TheoryArithOld::assertFact()</a>, and <a class="el" href="theory__arith3_8cpp_source.html#l02020">CVC3::TheoryArith3::assertFact()</a>.</p>
</div>
</div>
<a class="anchor" id="a4b6ef5b29b05bada6ea2df72873abea6"></a><!-- doxytag: member="CVC3::ArithProofRules::splitGrayShadow" ref="a4b6ef5b29b05bada6ea2df72873abea6" args="(const Theorem &g)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::splitGrayShadow </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>g</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>G(x, e, c1, c2) ==> (G1 or G2) and (!G1 or !G2) </p>
<p>Here G1 = G(x,e,c1,c), G2 = G(x,e,c+1,c2), and c = floor((c1+c2)/2). </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a14af8b5ecbfaaee4600453bd9d681838">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ae609e58a7bee454d0f18dc1465cd2167">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a7fa5dbc59e8ce9a4315373092329a029">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l02481">CVC3::TheoryArithOld::assertFact()</a>, and <a class="el" href="theory__arith3_8cpp_source.html#l02020">CVC3::TheoryArith3::assertFact()</a>.</p>
</div>
</div>
<a class="anchor" id="aa33975feef2a9cdd513e5d641f14dc7a"></a><!-- doxytag: member="CVC3::ArithProofRules::splitGrayShadowSmall" ref="aa33975feef2a9cdd513e5d641f14dc7a" args="(const Theorem &g)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::splitGrayShadowSmall </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>g</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#acaa835c8569f6667fa26bfedb0502cf1">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aab0ccd490624628fa990b1dd473e7e8a">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a0d76b8569909514e1f6a392a3778c04b">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l02481">CVC3::TheoryArithOld::assertFact()</a>.</p>
</div>
</div>
<a class="anchor" id="af936b764ef75b0a6f63043d01a819044"></a><!-- doxytag: member="CVC3::ArithProofRules::expandGrayShadow" ref="af936b764ef75b0a6f63043d01a819044" args="(const Theorem &g)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::expandGrayShadow </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>g</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>G(x, e, c1, c2) ==> e+c1 <= x AND x <= e+c2. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ac6714d4922aea3413f9aeed742bc645e">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ab9dd38464b6e02af6d7c570119c6aec3">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a0e43921a028cfe58d5b50acd0c4a70ed">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l02481">CVC3::TheoryArithOld::assertFact()</a>, and <a class="el" href="theory__arith3_8cpp_source.html#l02020">CVC3::TheoryArith3::assertFact()</a>.</p>
</div>
</div>
<a class="anchor" id="a3083a3c5893123f2a3ec54ce31718e09"></a><!-- doxytag: member="CVC3::ArithProofRules::expandGrayShadowConst" ref="a3083a3c5893123f2a3ec54ce31718e09" args="(const Theorem &g)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::expandGrayShadowConst </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>g</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Optimized rules: GRAY_SHADOW(a*x, c, c1, c2) ==> [expansion]. </p>
<p>Implements three versions of the rule:</p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\mathrm{GRAY\_SHADOW}(ax,c,c1,c2)} {ax = c + i - \mathrm{sign}(i)\cdot j(c,i,a) \lor GRAY\_SHADOW(ax, c, i-\mathrm{sign}(i)\cdot (a+j(c,i,a)))}\]" src="form_310.png"/>
</p>
<p>where the conclusion may become FALSE or without the GRAY_SHADOW part, depending on the values of a, c and i. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#af091e13254c983370c46707a03b1ad30">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a43d1cf15faefe439c344508bf60e5e96">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#ae8c25031e88732d3259cd8e33d75e094">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a597adbe8879c33bffefae537a5bca7c0"></a><!-- doxytag: member="CVC3::ArithProofRules::grayShadowConst" ref="a597adbe8879c33bffefae537a5bca7c0" args="(const Theorem &g)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::grayShadowConst </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>g</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>|- G(ax, c, c1, c2) ==> |- G(x, 0, ceil((c1+c)/a), floor((c2+c)/a)) </p>
<p>In the case the new c1 > c2, return |- FALSE </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#af0070c5da95d33029e54b1d669d5b1f0">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a0a5eb9028805dd1ee141713b7c70be77">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a04d45720968a5ff4ccd6411413bd826e">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l02481">CVC3::TheoryArithOld::assertFact()</a>, and <a class="el" href="theory__arith3_8cpp_source.html#l02020">CVC3::TheoryArith3::assertFact()</a>.</p>
</div>
</div>
<a class="anchor" id="a7a0dad5cb9c2815421457dabc25bc537"></a><!-- doxytag: member="CVC3::ArithProofRules::lessThanToLE" ref="a7a0dad5cb9c2815421457dabc25bc537" args="(const Theorem &less, const Theorem &isIntLHS, const Theorem &isIntRHS, bool changeRight)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::lessThanToLE </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>less</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>isIntLHS</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>isIntRHS</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>changeRight</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>a,b: INT; a < b ==> a <= b-1 [or a+1 <= b] </p>
<p>Takes a <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>(\alpha < \beta) and returns <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>(\alpha < \beta <==> \alpha <= \beta -1) or <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>(\alpha < \beta <==> \alpha + 1 <= \beta), depending on which side must be changed (changeRight flag) </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ac5d4056f00cee80d73b5b46f63bd5b3d">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a91447c7423622c037a2956114fd549f4">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a0ce54f8c725be25a6f6b11c7fbdc5321">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="af5cfb693ee5ee6f3463e83f01196b31e"></a><!-- doxytag: member="CVC3::ArithProofRules::lessThanToLERewrite" ref="af5cfb693ee5ee6f3463e83f01196b31e" args="(const Expr &ineq, const Theorem &isIntLHS, const Theorem &isIntRHS, bool changeRight)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::lessThanToLERewrite </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>ineq</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>isIntLHS</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>isIntRHS</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>changeRight</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#af55c5d0a2626f955b0843381ca8b50f3">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a55c056040dc960b598706a94650acccb">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#ab872ead63494b4afa6571e61a5cdd977">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l03076">CVC3::TheoryArithOld::rewrite()</a>.</p>
</div>
</div>
<a class="anchor" id="a62d76b2ccca8af5e1f28c5104ea2e313"></a><!-- doxytag: member="CVC3::ArithProofRules::intVarEqnConst" ref="a62d76b2ccca8af5e1f28c5104ea2e313" args="(const Expr &eqn, const Theorem &isIntx)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::intVarEqnConst </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>eqn</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>isIntx</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<dl><dt><b>Parameters:</b></dt><dd>
<table class="params">
<tr><td class="paramname">eqn</td><td>is an equation 0 = a.x or 0 = c + a.x, where x is integer </td></tr>
<tr><td class="paramname">isIntx</td><td>is a proof of IS_INTEGER(x)</td></tr>
</table>
</dd>
</dl>
<dl class="return"><dt><b>Returns:</b></dt><dd>the theorem 0 = c + a.x <==> x=-c/a if -c/a is int else return the theorem 0 = c + a.x <==> false.</dd></dl>
<p>It also handles the special case of 0 = a.x <==> x = 0 </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a92936e3de514c430659486b00e84b0a9">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a608b3a7da8f2824d3cc8188d7606396e">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a99692dc40111d3082e7c583590c32188">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a8c3d5fdc2b0c9c11291d41c3c20067e4"></a><!-- doxytag: member="CVC3::ArithProofRules::IsIntegerElim" ref="a8c3d5fdc2b0c9c11291d41c3c20067e4" args="(const Theorem &isIntx)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::IsIntegerElim </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>isIntx</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>IS_INTEGER(x) <=> EXISTS (y : INT) y = x where x is not already known to be an integer. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a85e9c7d93d6d1433fea606b0c3878e25">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ad2438a34ff1edb7268495d4105cb6c9c">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#adc3a59f76832fd2671407c85b4b721a5">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l02481">CVC3::TheoryArithOld::assertFact()</a>.</p>
</div>
</div>
<a class="anchor" id="a08b14a730bbc6b4ca28bb808e6f6dc85"></a><!-- doxytag: member="CVC3::ArithProofRules::eqElimIntRule" ref="a08b14a730bbc6b4ca28bb808e6f6dc85" args="(const Theorem &eqn, const Theorem &isIntx, const std::vector< Theorem > &isIntVars)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::eqElimIntRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>eqn</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>isIntx</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>isIntVars</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Equality elimination rule for integers: </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\mathsf{int}(a\cdot x)\quad \mathsf{int}(C+\sum_{i=1}^{n}a_{i}\cdot x_{i})} {a\cdot x=C+\sum_{i=1}^{n}a_{i}\cdot x_{i} \quad\equiv\quad x=t_{2}\wedge 0=t_{3}} \]" src="form_311.png"/>
</p>
<p> See the detailed description for explanations. </p>
<p>This rule implements a step in the iterative algorithm for eliminating integer equality. The terms in the rule are defined as follows:</p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\begin{array}{rcl} t_{2} & = & -(C\ \mathbf{mod}\ m+\sum_{i=1}^{n}(a_{i}\ \mathbf{mod}\ m) \cdot x_{i}-m\cdot\sigma(t))\\ & & \\ t_{3} & = & \mathbf{f}(C,m)+\sum_{i=1}^{n}\mathbf{f}(a_{i},m)\cdot x_{i} -a\cdot\sigma(t)\\ & & \\ t & = & (C\ \mathbf{mod}\ m+\sum_{i=1}^{n}(a_{i}\ \mathbf{mod}\ m) \cdot x_{i}+x)/m\\ & & \\ m & = & a+1\\ & & \\ \mathbf{f}(i,m) & = & \left\lfloor \frac{i}{m} +\frac{1}{2}\right\rfloor +i\ \mathbf{mod}\ m\\ & & \\ i\ \mathbf{mod}\ m & = & i-m\left\lfloor\frac{i}{m} +\frac{1}{2}\right\rfloor \end{array} \]" src="form_312.png"/>
</p>
<p>All the variables and coefficients are integer, and a >= 2.</p>
<dl><dt><b>Parameters:</b></dt><dd>
<table class="params">
<tr><td class="paramname">eqn</td><td>is the equation <p class="formulaDsp">
<img class="formulaDsp" alt="\[a\cdot x = C + \sum_{i=1}^n a_i\cdot x_i.\]" src="form_313.png"/>
</p>
</td></tr>
</table>
</dd>
</dl>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma\models ax=t\quad \Gamma'\models\mathsf{int}(x)\quad \{\Gamma_i\models\mathsf{int}(x_i) | x_i\mbox{ is var in }t\}} {\Gamma,\Gamma',\bigcup_i\Gamma_i\models \exists (y:\mathrm{int}).\ x=t_2(y)\wedge 0=t_3(y)} \]" src="form_314.png"/>
</p>
<p> See detailed docs for more information.</p>
<p>This rule implements a step in the iterative algorithm for eliminating integer equality. The terms in the rule are defined as follows:</p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\begin{array}{rcl} t & = & C+\sum_{i=1}^na_{i}\cdot x_{i}\\ t_{2}(y) & = & -(C\ \mathbf{mod}\ m+\sum_{i=1}^{n}(a_{i}\ \mathbf{mod}\ m) \cdot x_{i}-m\cdot y)\\ & & \\ t_{3}(y) & = & \mathbf{f}(C,m)+\sum_{i=1}^{n}\mathbf{f}(a_{i},m)\cdot x_{i} -a\cdot y\\ & & \\ m & = & a+1\\ & & \\ \mathbf{f}(i,m) & = & \left\lfloor \frac{i}{m} +\frac{1}{2}\right\rfloor +i\ \mathbf{mod}\ m\\ & & \\ i\ \mathbf{mod}\ m & = & i-m\left\lfloor\frac{i}{m} +\frac{1}{2}\right\rfloor \end{array} \]" src="form_315.png"/>
</p>
<p>All the variables and coefficients are integer, and a >= 2.</p>
<dl><dt><b>Parameters:</b></dt><dd>
<table class="params">
<tr><td class="paramname">eqn</td><td>is the equation ax=t: <p class="formulaDsp">
<img class="formulaDsp" alt="\[a\cdot x = C + \sum_{i=1}^n a_i\cdot x_i.\]" src="form_313.png"/>
</p>
</td></tr>
<tr><td class="paramname">isIntx</td><td>is a <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> deriving the integrality of the LHS variable: IS_INTEGER(x)</td></tr>
<tr><td class="paramname">isIntVars</td><td>is a vector of Theorems deriving the integrality of all variables on the RHS </td></tr>
</table>
</dd>
</dl>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a49d6559f50d51cde3c2e723c2a254cff">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a1f5430f425efc533ca5881aaaeb42554">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a85fd2ee0f7126d421fb53f4823ec8e77">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a5e9bccd77000156ab34b0b42d3e3bb18"></a><!-- doxytag: member="CVC3::ArithProofRules::isIntConst" ref="a5e9bccd77000156ab34b0b42d3e3bb18" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::isIntConst </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>return e <=> TRUE/FALSE for e == IS_INTEGER(c), where c is a constant </p>
<dl><dt><b>Parameters:</b></dt><dd>
<table class="params">
<tr><td class="paramname">e</td><td>is a predicate IS_INTEGER(c) where c is a rational constant </td></tr>
</table>
</dd>
</dl>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#af1baf70d6108dc52cbb9704e2a8889ec">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a24216d1be10b57272b918ba416783b76">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a5ef5359db9aa12e8d196f7a39fc0fb55">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="ac05fd3606540a5222ebaa68f9091345b"></a><!-- doxytag: member="CVC3::ArithProofRules::equalLeaves1" ref="ac05fd3606540a5222ebaa68f9091345b" args="(const Theorem &thm)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::equalLeaves1 </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a512f22a4a025477ced8c27f3d62809d7">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#acb64cdcb59f042dd38a9bf9b70f043ad">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a0a3f404013d038207a13103500e09c99">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a5052c783af25243987424ef66e2bf5fc"></a><!-- doxytag: member="CVC3::ArithProofRules::equalLeaves2" ref="a5052c783af25243987424ef66e2bf5fc" args="(const Theorem &thm)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::equalLeaves2 </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a77ae567431bf98e20cc08903deb2ec99">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ae97e571a8d541a31aef5c1c703190437">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#ae1820f8d68e98363139d77deae464f4f">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a893c86f0404789d229540f7a0a00df89"></a><!-- doxytag: member="CVC3::ArithProofRules::equalLeaves3" ref="a893c86f0404789d229540f7a0a00df89" args="(const Theorem &thm)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::equalLeaves3 </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a8de6b6b44c60cf495b455b980a7c681b">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aba1a7d51f8b8291c30cc32c0f3ff5a4d">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a8e8ce7a2f17e5a855985bd0abfac6f12">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="aa9018c4d16d3d0a2d8f1614f8e7cae23"></a><!-- doxytag: member="CVC3::ArithProofRules::equalLeaves4" ref="aa9018c4d16d3d0a2d8f1614f8e7cae23" args="(const Theorem &thm)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::equalLeaves4 </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a97768870957319cdc68eb94694a37dc5">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a5876760c9171eca18490c779cc2bbc73">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a24c874d01ca341845373cd41851a5a1b">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="af180898d9f1d255ef3a2f528ecd8ac65"></a><!-- doxytag: member="CVC3::ArithProofRules::diseqToIneq" ref="af180898d9f1d255ef3a2f528ecd8ac65" args="(const Theorem &diseq)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::diseqToIneq </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>diseq</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>x /= y ==> (x < y) OR (x > y) </p>
<p>Used in concrete model generation </p>
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a3d6e1d8668360c20b5a6a47e3fcc4612">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a20fdbcbe80fa06a175aae548af7d2519">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#ae723d1459d8c6f797ec08451f80f0798">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l02606">CVC3::TheoryArithOld::checkSat()</a>, and <a class="el" href="theory__arith3_8cpp_source.html#l02124">CVC3::TheoryArith3::checkSat()</a>.</p>
</div>
</div>
<a class="anchor" id="a24ea340651805e648d7180debad17225"></a><!-- doxytag: member="CVC3::ArithProofRules::dummyTheorem" ref="a24ea340651805e648d7180debad17225" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::dummyTheorem </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a753c339b31e38915ae6f06e0fe6e48da">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ae1e994559a2318ec45a758042371a71d">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a3a3dd2d9c47ec607c816a9004c3659a5">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__new_8cpp_source.html#l01570">CVC3::TheoryArithNew::rewrite()</a>.</p>
</div>
</div>
<a class="anchor" id="a1ebae10d65430ab1a3a14c866af93de6"></a><!-- doxytag: member="CVC3::ArithProofRules::oneElimination" ref="a1ebae10d65430ab1a3a14c866af93de6" args="(const Expr &x)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::oneElimination </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>x</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a23051d23d509f9cda35c64d4a5ff1dbf">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a2caebbed8d00af9c80195413ed2cc568">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#aeb6d93e58c5c069ecbea38d013cbcf3e">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__new_8cpp_source.html#l03138">CVC3::TheoryArithNew::assertFact()</a>, and <a class="el" href="theory__arith__new_8cpp_source.html#l03600">CVC3::TheoryArithNew::pivotRule()</a>.</p>
</div>
</div>
<a class="anchor" id="ad0b23fb01a7adea349c8958059b9f7fd"></a><!-- doxytag: member="CVC3::ArithProofRules::clashingBounds" ref="ad0b23fb01a7adea349c8958059b9f7fd" args="(const Theorem &lowerBound, const Theorem &upperBound)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::clashingBounds </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>lowerBound</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>upperBound</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ad4513630a9eec6c841b527222a79ea1d">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#af05299dbe2defe9679365201cd60c516">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#aa71bcce02e1c1ce0d6ae588b4f341e4a">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__new_8cpp_source.html#l02777">CVC3::TheoryArithNew::assertLower()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l02740">CVC3::TheoryArithNew::assertUpper()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l03662">CVC3::TheoryArithNew::getLowerBoundExplanation()</a>, and <a class="el" href="theory__arith__new_8cpp_source.html#l03749">CVC3::TheoryArithNew::getUpperBoundExplanation()</a>.</p>
</div>
</div>
<a class="anchor" id="ac06dd83948d0f3e474f073ecac592343"></a><!-- doxytag: member="CVC3::ArithProofRules::addInequalities" ref="ac06dd83948d0f3e474f073ecac592343" args="(const Theorem &thm1, const Theorem &thm2)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::addInequalities </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm2</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a3b2bea72cd9163daa7c41388037bca29">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a301d62f207b9cfd50096417d1f5852df">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a582df53749ebc6fd4011c614ff767181">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__new_8cpp_source.html#l03662">CVC3::TheoryArithNew::getLowerBoundExplanation()</a>, and <a class="el" href="theory__arith__new_8cpp_source.html#l03749">CVC3::TheoryArithNew::getUpperBoundExplanation()</a>.</p>
</div>
</div>
<a class="anchor" id="ab87b1e3a09aa830063d51c24a2147095"></a><!-- doxytag: member="CVC3::ArithProofRules::addInequalities" ref="ab87b1e3a09aa830063d51c24a2147095" args="(const std::vector< Theorem > &thms)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::addInequalities </td>
<td>(</td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>thms</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a0eb949bb19e618a8318f236b249fadd5">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aa2d099917106ead1062c72dde26a17a5">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a0d40393a73ca5ac2e0078a6e955d7988">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a9abe85f95b61d94fa308a0b15f2b2ef8"></a><!-- doxytag: member="CVC3::ArithProofRules::implyWeakerInequality" ref="a9abe85f95b61d94fa308a0b15f2b2ef8" args="(const Expr &expr1, const Expr &expr2)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::implyWeakerInequality </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>expr1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>expr2</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a364ef37224bae3afb4f62a5c0f75d02c">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ae856ca9fab9699b655d7fd76cdf778d4">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a08879e8160aca1424c12e098f78df383">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__new_8cpp_source.html#l04000">CVC3::TheoryArithNew::propagateTheory()</a>, and <a class="el" href="theory__arith__old_8cpp_source.html#l04662">CVC3::TheoryArithOld::registerAtom()</a>.</p>
</div>
</div>
<a class="anchor" id="a5eaf4d106f7ce86227ab1d96ffc66b55"></a><!-- doxytag: member="CVC3::ArithProofRules::implyNegatedInequality" ref="a5eaf4d106f7ce86227ab1d96ffc66b55" args="(const Expr &expr1, const Expr &expr2)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::implyNegatedInequality </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>expr1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>expr2</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a1bf4d45330b587882e726daa9117cdfb">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a1797b422d1100edc2464666121d7017b">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a3597b8abdecd9f22c11f3ed1b570b6e8">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__new_8cpp_source.html#l04000">CVC3::TheoryArithNew::propagateTheory()</a>, and <a class="el" href="theory__arith__old_8cpp_source.html#l04662">CVC3::TheoryArithOld::registerAtom()</a>.</p>
</div>
</div>
<a class="anchor" id="a0090e0d4065efbf936ec92f0e99935e9"></a><!-- doxytag: member="CVC3::ArithProofRules::integerSplit" ref="a0090e0d4065efbf936ec92f0e99935e9" args="(const Expr &intVar, const Rational &intPoint)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::integerSplit </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>intVar</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Rational.html">Rational</a> & </td>
<td class="paramname"><em>intPoint</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ab9395a2ee958d70c780df2514e517320">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ae25218af53e642382f30948adc991313">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#ad6dec83ab198a011e429c0f4b3aa218f">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__new_8cpp_source.html#l02868">CVC3::TheoryArithNew::checkSatInteger()</a>.</p>
</div>
</div>
<a class="anchor" id="a11976de555ee2e88236575893f2ed766"></a><!-- doxytag: member="CVC3::ArithProofRules::trustedRewrite" ref="a11976de555ee2e88236575893f2ed766" args="(const Expr &expr1, const Expr &expr2)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::trustedRewrite </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>expr1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>expr2</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a43fa5f7c8c3ad3915de7f068ac8cefbd">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ad58ee7b299de278620860c9d67a2662b">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a929689864e6c95280fcf1caa08ae28e1">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a4b61e3ea9d5ac911806de95241cf35de"></a><!-- doxytag: member="CVC3::ArithProofRules::rafineStrictInteger" ref="a4b61e3ea9d5ac911806de95241cf35de" args="(const Theorem &isIntConstrThm, const Expr &constr)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::rafineStrictInteger </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>isIntConstrThm</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>constr</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a4b28aa17702ca3f9703e61ca012ca236">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a7638b18d73c05e7bedad7c4cdfeca809">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#af6182f9b295bde40a9047b1651d979a5">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l02953">CVC3::TheoryArithOld::rafineInequalityToInteger()</a>, and <a class="el" href="theory__arith__new_8cpp_source.html#l01541">CVC3::TheoryArithNew::rafineIntegerConstraints()</a>.</p>
</div>
</div>
<a class="anchor" id="a95bc88d9e126e6b9c938691ce92985aa"></a><!-- doxytag: member="CVC3::ArithProofRules::simpleIneqInt" ref="a95bc88d9e126e6b9c938691ce92985aa" args="(const Expr &ineq, const Theorem &isIntRHS)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::simpleIneqInt </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>ineq</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>isIntRHS</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#afd5bca9b136254b904b931680180ac83">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a6fe0e5ebaf81278f55759fff05c275c1">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a21b67f29c32a44f6194d127feb316d99">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a93489420e882a93eb308c7d99c27dc1e"></a><!-- doxytag: member="CVC3::ArithProofRules::intEqualityRationalConstant" ref="a93489420e882a93eb308c7d99c27dc1e" args="(const Theorem &isIntConstrThm, const Expr &constr)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::intEqualityRationalConstant </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>isIntConstrThm</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>constr</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ad5f121b6b7d6b8ae951dfb4cce064575">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a84ec7197bec26c33753e98b6adf55dce">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a33232797bdaaa27ecd2f077478605bf6">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l02913">CVC3::TheoryArithOld::checkIntegerEquality()</a>.</p>
</div>
</div>
<a class="anchor" id="a5a544980652c3f6793057b16cbc43cf9"></a><!-- doxytag: member="CVC3::ArithProofRules::cycleConflict" ref="a5a544980652c3f6793057b16cbc43cf9" args="(const std::vector< Theorem > &inequalitites)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::cycleConflict </td>
<td>(</td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>inequalitites</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a0111aa5645658dbd6a4bc030178edb94">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a5411413ef39cb6029a8e85fc03908de3">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#aacf793e26f8917dbd96d235b9399a18e">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a5b475214a53d70298e55f4ac5f3db71f"></a><!-- doxytag: member="CVC3::ArithProofRules::implyEqualities" ref="a5b475214a53d70298e55f4ac5f3db71f" args="(const std::vector< Theorem > &inequalities)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::implyEqualities </td>
<td>(</td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>inequalities</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#abb8aff055ea56ad8de2b66fd9a7aeba9">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a1efa679a45d71f60bf2be6f4f7a4430d">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a6a98470138f38710024a7cc8f37706fb">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="aafc12b4bdf180f3475ecf4eaa40648d9"></a><!-- doxytag: member="CVC3::ArithProofRules::implyWeakerInequalityDiffLogic" ref="aafc12b4bdf180f3475ecf4eaa40648d9" args="(const std::vector< Theorem > &antecedentThms, const Expr &implied)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::implyWeakerInequalityDiffLogic </td>
<td>(</td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>antecedentThms</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>implied</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ae3a7aa0ebe8e84b806efaa59278ea75e">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a8e90a0d0e2050a7f0eb1dde6df7f6842">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#af6d982874e310ba4bdbc796fcbc720fc">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l05039">CVC3::TheoryArithOld::tryPropagate()</a>.</p>
</div>
</div>
<a class="anchor" id="a61ecf1cfc7219c010519cd90cb31d465"></a><!-- doxytag: member="CVC3::ArithProofRules::implyNegatedInequalityDiffLogic" ref="a61ecf1cfc7219c010519cd90cb31d465" args="(const std::vector< Theorem > &antecedentThms, const Expr &implied)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::implyNegatedInequalityDiffLogic </td>
<td>(</td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>antecedentThms</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>implied</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ab794c1f9d6e971ac56e0063f409b4774">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a6ef98983cca8d3723f50fbea60c37cef">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#aee41f9c7c0f2a6b82383076327e316a0">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l05039">CVC3::TheoryArithOld::tryPropagate()</a>.</p>
</div>
</div>
<a class="anchor" id="ac48d6f8b2ad8e8f8fefac775d33825b5"></a><!-- doxytag: member="CVC3::ArithProofRules::expandGrayShadowRewrite" ref="ac48d6f8b2ad8e8f8fefac775d33825b5" args="(const Expr &theShadow)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::expandGrayShadowRewrite </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>theShadow</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a84a9652acc5908e5d1ead5c54c1f2d90">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aa9b6fa1339b7e68cb730bdf2f63c0914">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#abb0ca6212da8280b0026369e449f900e">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a98020e790bcb60c9c2cc5a7e406f500f"></a><!-- doxytag: member="CVC3::ArithProofRules::compactNonLinearTerm" ref="a98020e790bcb60c9c2cc5a7e406f500f" args="(const Expr &nonLinear)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::compactNonLinearTerm </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>nonLinear</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ae43400e7e4c9e3695a75da3bd5718eda">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aac90a712f81d969d8aa0322b4d31de0b">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#ad54e479f1a44912397237a557590c597">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="aa6874fa9f5b02db0adb8149af9664b05"></a><!-- doxytag: member="CVC3::ArithProofRules::nonLinearIneqSignSplit" ref="aa6874fa9f5b02db0adb8149af9664b05" args="(const Theorem &ineqThm)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::nonLinearIneqSignSplit </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>ineqThm</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a9edd8b9ee6a8b4d14e9a2f967b78d52f">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aaa91789edbf7fb936789379dd15a3a4f">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#afe7a4ea7cbce967d7f160c21995c8b39">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="af80ad28bb01d8a37e32f29c746d22dbc"></a><!-- doxytag: member="CVC3::ArithProofRules::implyDiffLogicBothBounds" ref="af80ad28bb01d8a37e32f29c746d22dbc" args="(const Expr &x, std::vector< Theorem > &c1_le_x, Rational c1, std::vector< Theorem > &x_le_c2, Rational c2)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::implyDiffLogicBothBounds </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>x</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>c1_le_x</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Rational.html">Rational</a> </td>
<td class="paramname"><em>c1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>x_le_c2</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Rational.html">Rational</a> </td>
<td class="paramname"><em>c2</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a45d8f89bdb0e57ddbaec273a24bf34b4">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a9edd45196fbd8e61a4927134fde15e97">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a8581e89bb73352a8e368e7b87acd78f4">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="ad3dee93f4078a4fc79ccacef33f05119"></a><!-- doxytag: member="CVC3::ArithProofRules::powerOfOne" ref="ad3dee93f4078a4fc79ccacef33f05119" args="(const Expr &e)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ArithProofRules::powerOfOne </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a0433b1ba53a33275015c26450acb09d0">CVC3::ArithTheoremProducer</a>, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#abf49b0eeb6087702dd1a8e9c03f7379a">CVC3::ArithTheoremProducer3</a>, and <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#aadb554e4e8877b135fb01d6e2471ccba">CVC3::ArithTheoremProducerOld</a>.</p>
</div>
</div>
<a class="anchor" id="a81d9ea1e5c2d42c2b60a893c879145bd"></a><!-- doxytag: member="CVC3::ArithProofRules::rewriteLeavesConst" ref="a81d9ea1e5c2d42c2b60a893c879145bd" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> ArithProofRules::rewriteLeavesConst </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a120563be6dbb828da3e9b6a9d4d35e32">CVC3::ArithTheoremProducerOld</a>.</p>
<p>Definition at line <a class="el" href="arith__theorem__producer_8cpp_source.html#l03243">3243</a> of file <a class="el" href="arith__theorem__producer_8cpp_source.html">arith_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l03076">CVC3::TheoryArithOld::rewrite()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="arith__proof__rules_8h_source.html">arith_proof_rules.h</a></li>
<li><a class="el" href="arith__theorem__producer_8cpp_source.html">arith_theorem_producer.cpp</a></li>
</ul>
</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>
