<!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::TheoryArithOld::DifferenceLogicGraph 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_1TheoryArithOld.html">TheoryArithOld</a> </li>
<li class="navelem"><a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html">DifferenceLogicGraph</a> </li>
</ul>
</div>
</div>
<div class="header">
<div class="summary">
<a href="#nested-classes">Classes</a> |
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pro-types">Protected Types</a> |
<a href="#pro-methods">Protected Member Functions</a> |
<a href="#pro-attribs">Protected Attributes</a> </div>
<div class="headertitle">
<div class="title">CVC3::TheoryArithOld::DifferenceLogicGraph Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="CVC3::TheoryArithOld::DifferenceLogicGraph" -->
<p><a href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph-members.html">List of all members.</a></p>
<h2><a name="nested-classes"></a>
Classes</h2>
<ul>
<li>struct <a class="el" href="structCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph_1_1EdgeInfo.html">EdgeInfo</a>
<li>class <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph_1_1EpsRational.html">EpsRational</a>
</ul>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li>void <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a58d23191bab044554e42ba0dd7f110de">getEdgeTheorems</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="structCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph_1_1EdgeInfo.html">EdgeInfo</a> &edgeInfo, std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &outputTheorems)
<li><a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph_1_1EpsRational.html">EpsRational</a> <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a70441880fa7ecde30265c3ec83f7e11d">getEdgeWeight</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)
<li>bool <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a33e10dce7990aaeedd588663c308c416">hasIncoming</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &x)
<li>bool <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a63b4374516dfa8f7c87de61b460dcf12">hasOutgoing</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &x)
<li>void <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#ae9325d9bce63e5a62cce23d4aac2db32">writeGraph</a> (std::ostream &out)
<li>void <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a4266a410f71d5536394188cd74034b18">getVariables</a> (std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &variables)
<li>void <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#ac13ef29f1852dd0d157b52bdfc050737">setRules</a> (<a class="el" href="classCVC3_1_1ArithProofRules.html">ArithProofRules</a> *<a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#acbbd4a2fbba125d1069f124e5c271826">rules</a>)
<li>void <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a5b2e50e6e3c75743ace5bb2fae432449">setArith</a> (<a class="el" href="classCVC3_1_1TheoryArithOld.html">TheoryArithOld</a> *<a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#ae172261f15e4d9903b4147b6ee1f4523">arith</a>)
<li><a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a0014118b800ec0cce12b84a3b8c921d1">DifferenceLogicGraph</a> (<a class="el" href="classCVC3_1_1TheoryArithOld.html">TheoryArithOld</a> *<a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#ae172261f15e4d9903b4147b6ee1f4523">arith</a>, <a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> *<a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a6bf38051f1bc2b0703e6ba8ca3b765ae">core</a>, <a class="el" href="classCVC3_1_1ArithProofRules.html">ArithProofRules</a> *<a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#acbbd4a2fbba125d1069f124e5c271826">rules</a>, <a class="el" href="classCVC3_1_1Context.html">Context</a> *context)
<li><a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a9ff61777e5df7bc75f9879a6a9f75419">~DifferenceLogicGraph</a> ()
<li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a216bfac9dcbcc62b7097d51fd91e8ac8">getUnsatTheorem</a> ()
<li>bool <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a828bb2ad8fc3c36506f6a8f3ca38579c">isUnsat</a> ()
<li>void <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#ae7f9ea562c26f55a0536a5cd85cf07b0">computeModel</a> ()
<li><a class="el" href="classCVC3_1_1Rational.html">Rational</a> <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a22cd1525ea447a3bc839fc737240eb4f">getValuation</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &x)
<li>void <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#acdd072f244d1d30d5b954bf7b0debe04">addEdge</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_1Rational.html">Rational</a> &c, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &edge_thm)
<li>bool <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a2213f2040667750f9878aa0ce3ba3f17">existsEdge</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)
<li>bool <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a75eceef3b27aa29d23d26ac2a624d095">inCycle</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &x)
<li>void <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a247245c8102db8596b73c76cf015fc5d">expandSharedTerm</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &x)
</ul>
<h2><a name="pro-types"></a>
Protected Types</h2>
<ul>
<li>typedef <a class="el" href="classCVC3_1_1CDMap.html">CDMap</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, <a class="el" href="structCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph_1_1EdgeInfo.html">EdgeInfo</a> > <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#abed3971d17b5d311101715558f879558">Graph</a>
<li>typedef <a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< <a class="el" href="classCVC3_1_1CDList.html">CDList</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > * > <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a0ceb7ab88e1c7ec4b29ddd7c8214e1c9">EdgesList</a>
</ul>
<h2><a name="pro-methods"></a>
Protected Member Functions</h2>
<ul>
<li><a class="el" href="classCVC3_1_1CDOmap.html">Graph::ElementReference</a> <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a16b2a3042303dce733abadbec2a86ee1">getEdge</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)
<li>bool <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a62c681d767c2100a822db1f86ebabaf2">tryUpdate</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)
<li>void <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#ad101bbc763a37fb902e4df4a654351de">analyseConflict</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &x, int kind)
</ul>
<h2><a name="pro-attribs"></a>
Protected Attributes</h2>
<ul>
<li>const int * <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#ae4ed3f0c509c959d36e6637371bf6e05">d_pathLenghtThres</a>
<li><a class="el" href="classCVC3_1_1TheoryArithOld.html">TheoryArithOld</a> * <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#ae172261f15e4d9903b4147b6ee1f4523">arith</a>
<li><a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> * <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a6bf38051f1bc2b0703e6ba8ca3b765ae">core</a>
<li><a class="el" href="classCVC3_1_1ArithProofRules.html">ArithProofRules</a> * <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#acbbd4a2fbba125d1069f124e5c271826">rules</a>
<li><a class="el" href="classCVC3_1_1CDO.html">CDO</a>< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a627796132ea73d35fbcf828d68425a3b">unsat_theorem</a>
<li><a class="el" href="classCVC3_1_1CDO.html">CDO</a>< <a class="el" href="classCVC3_1_1Rational.html">Rational</a> > <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#ae4d498b950e7b37b5b48c936139cfc70">biggestEpsilon</a>
<li><a class="el" href="classCVC3_1_1CDO.html">CDO</a>< <a class="el" href="classCVC3_1_1Rational.html">Rational</a> > <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a2519a13732d48786f8fe83351a7150c8">smallestPathDifference</a>
<li><a class="el" href="classCVC3_1_1CDMap.html">Graph</a> <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a47342aafbf5caa7aca2fbd5e9511cef1">leGraph</a>
<li><a class="el" href="classCVC3_1_1ExprMap.html">EdgesList</a> <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a6a605397e227cc5b9c287984ead0902b">incomingEdges</a>
<li><a class="el" href="classCVC3_1_1ExprMap.html">EdgesList</a> <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#ac0fa1b22e8ed0d8d0580599998b36bf2">outgoingEdges</a>
<li><a class="el" href="classCVC3_1_1CDMap.html">CDMap</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, bool > <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a478a837c6562772e151cbfef55e607ee">varInCycle</a>
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a7b0dd9d1e47d917391c0ed987608bb57">sourceVertex</a>
</ul>
<hr/><a name="details" id="details"></a><h2>Detailed Description</h2>
<div class="textblock">
<p>Definition at line <a class="el" href="theory__arith__old_8h_source.html#l00456">456</a> of file <a class="el" href="theory__arith__old_8h_source.html">theory_arith_old.h</a>.</p>
</div><hr/><h2>Member Typedef Documentation</h2>
<a class="anchor" id="abed3971d17b5d311101715558f879558"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::Graph" ref="abed3971d17b5d311101715558f879558" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">typedef <a class="el" href="classCVC3_1_1CDMap.html">CDMap</a><<a class="el" href="classCVC3_1_1Expr.html">Expr</a>, <a class="el" href="structCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph_1_1EdgeInfo.html">EdgeInfo</a>> <a class="el" href="classCVC3_1_1CDMap.html">CVC3::TheoryArithOld::DifferenceLogicGraph::Graph</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>The graph itself, maps expressions (x-y) to the edge information </p>
<p>Definition at line <a class="el" href="theory__arith__old_8h_source.html#l00771">771</a> of file <a class="el" href="theory__arith__old_8h_source.html">theory_arith_old.h</a>.</p>
</div>
</div>
<a class="anchor" id="a0ceb7ab88e1c7ec4b29ddd7c8214e1c9"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::EdgesList" ref="a0ceb7ab88e1c7ec4b29ddd7c8214e1c9" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">typedef <a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a><<a class="el" href="classCVC3_1_1CDList.html">CDList</a><<a class="el" href="classCVC3_1_1Expr.html">Expr</a>>*> <a class="el" href="classCVC3_1_1ExprMap.html">CVC3::TheoryArithOld::DifferenceLogicGraph::EdgesList</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__arith__old_8h_source.html#l00776">776</a> of file <a class="el" href="theory__arith__old_8h_source.html">theory_arith_old.h</a>.</p>
</div>
</div>
<hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="a0014118b800ec0cce12b84a3b8c921d1"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::DifferenceLogicGraph" ref="a0014118b800ec0cce12b84a3b8c921d1" args="(TheoryArithOld *arith, TheoryCore *core, ArithProofRules *rules, Context *context)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">TheoryArithOld::DifferenceLogicGraph::DifferenceLogicGraph </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoryArithOld.html">TheoryArithOld</a> * </td>
<td class="paramname"><em>arith</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> * </td>
<td class="paramname"><em>core</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ArithProofRules.html">ArithProofRules</a> * </td>
<td class="paramname"><em>rules</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Context.html">Context</a> * </td>
<td class="paramname"><em>context</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Class constructor. </p>
<p>Definition at line <a class="el" href="theory__arith__old_8cpp_source.html#l04711">4711</a> of file <a class="el" href="theory__arith__old_8cpp_source.html">theory_arith_old.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="a9ff61777e5df7bc75f9879a6a9f75419"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::~DifferenceLogicGraph" ref="a9ff61777e5df7bc75f9879a6a9f75419" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">TheoryArithOld::DifferenceLogicGraph::~DifferenceLogicGraph </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Destructor </p>
<p>Definition at line <a class="el" href="theory__arith__old_8cpp_source.html#l05024">5024</a> of file <a class="el" href="theory__arith__old_8cpp_source.html">theory_arith_old.cpp</a>.</p>
<p>References <a class="el" href="expr__map_8h_source.html#l00190">CVC3::ExprMap< Data >::begin()</a>.</p>
</div>
</div>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="a58d23191bab044554e42ba0dd7f110de"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems" ref="a58d23191bab044554e42ba0dd7f110de" args="(const Expr &x, const Expr &y, const EdgeInfo &edgeInfo, std::vector< Theorem > &outputTheorems)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems </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="structCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph_1_1EdgeInfo.html">EdgeInfo</a> & </td>
<td class="paramname"><em>edgeInfo</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>outputTheorems</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Given two vertices in the graph and an path edge, reconstruct all the theorems and put them in the output vector </p>
<p>Definition at line <a class="el" href="theory__arith__old_8cpp_source.html#l04888">4888</a> of file <a class="el" href="theory__arith__old_8cpp_source.html">theory_arith_old.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theory__arith__old_8h_source.html#l00718">CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::explanation</a>, <a class="el" href="theory__arith__old_8h_source.html#l00716">CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::in_path_vertex</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="theory__arith__old_8h_source.html#l00721">CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::isDefined()</a>, <a class="el" href="theorem_8h_source.html#l00164">CVC3::Theorem::isNull()</a>, <a class="el" href="theory__arith__old_8h_source.html#l00712">CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::length</a>, <a class="el" href="theory__arith__old_8h_source.html#l00714">CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::path_length_in_edges</a>, <a class="el" href="theory__arith__old_8h_source.html#l00695">CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::toString()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="kinds_8h_source.html#l00099">TRACE</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="a70441880fa7ecde30265c3ec83f7e11d"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::getEdgeWeight" ref="a70441880fa7ecde30265c3ec83f7e11d" args="(const Expr &x, const Expr &y)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph_1_1EpsRational.html">TheoryArithOld::DifferenceLogicGraph::EpsRational</a> TheoryArithOld::DifferenceLogicGraph::getEdgeWeight </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></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Returns the current weight of the edge. </p>
<p>Definition at line <a class="el" href="theory__arith__old_8cpp_source.html#l04778">4778</a> of file <a class="el" href="theory__arith__old_8cpp_source.html">theory_arith_old.cpp</a>.</p>
<p>References <a class="el" href="theory__arith__old_8h_source.html#l00712">CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::length</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l05535">CVC3::TheoryArithOld::computeTermBounds()</a>.</p>
</div>
</div>
<a class="anchor" id="a33e10dce7990aaeedd588663c308c416"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::hasIncoming" ref="a33e10dce7990aaeedd588663c308c416" args="(const Expr &x)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool TheoryArithOld::DifferenceLogicGraph::hasIncoming </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></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Returns whether a vertex has incoming edges. </p>
<p>Definition at line <a class="el" href="theory__arith__old_8cpp_source.html#l05809">5809</a> of file <a class="el" href="theory__arith__old_8cpp_source.html">theory_arith_old.cpp</a>.</p>
<p>References <a class="el" href="cdlist_8h_source.html#l00064">CVC3::CDList< T >::size()</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l05535">CVC3::TheoryArithOld::computeTermBounds()</a>, and <a class="el" href="theory__arith__old_8cpp_source.html#l05895">CVC3::TheoryArithOld::isUnconstrained()</a>.</p>
</div>
</div>
<a class="anchor" id="a63b4374516dfa8f7c87de61b460dcf12"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::hasOutgoing" ref="a63b4374516dfa8f7c87de61b460dcf12" args="(const Expr &x)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool TheoryArithOld::DifferenceLogicGraph::hasOutgoing </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></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Returns whether a vertex has outgoing edges. </p>
<p>Definition at line <a class="el" href="theory__arith__old_8cpp_source.html#l05827">5827</a> of file <a class="el" href="theory__arith__old_8cpp_source.html">theory_arith_old.cpp</a>.</p>
<p>References <a class="el" href="cdlist_8h_source.html#l00064">CVC3::CDList< T >::size()</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l05535">CVC3::TheoryArithOld::computeTermBounds()</a>, and <a class="el" href="theory__arith__old_8cpp_source.html#l05895">CVC3::TheoryArithOld::isUnconstrained()</a>.</p>
</div>
</div>
<a class="anchor" id="a16b2a3042303dce733abadbec2a86ee1"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::getEdge" ref="a16b2a3042303dce733abadbec2a86ee1" args="(const Expr &x, const Expr &y)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDOmap.html">TheoryArithOld::DifferenceLogicGraph::Graph::ElementReference</a> TheoryArithOld::DifferenceLogicGraph::getEdge </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> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Returns the edge (path) info for the given kind</p>
<dl><dt><b>Parameters:</b></dt><dd>
<table class="params">
<tr><td class="paramname">x</td><td>the starting vertex </td></tr>
<tr><td class="paramname">y</td><td>the ending vertex </td></tr>
</table>
</dd>
</dl>
<dl class="return"><dt><b>Returns:</b></dt><dd>the edge information </dd></dl>
<p>Definition at line <a class="el" href="theory__arith__old_8cpp_source.html#l04748">4748</a> of file <a class="el" href="theory__arith__old_8cpp_source.html">theory_arith_old.cpp</a>.</p>
<p>References <a class="el" href="cdmap_8h_source.html#l00106">CVC3::CDOmap< Key, Data, HashFcn >::get()</a>, <a class="el" href="theory__arith__old_8h_source.html#l00721">CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::isDefined()</a>, and <a class="el" href="cdlist_8h_source.html#l00066">CVC3::CDList< T >::push_back()</a>.</p>
</div>
</div>
<a class="anchor" id="a62c681d767c2100a822db1f86ebabaf2"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::tryUpdate" ref="a62c681d767c2100a822db1f86ebabaf2" args="(const Expr &x, const Expr &y, const Expr &z)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool TheoryArithOld::DifferenceLogicGraph::tryUpdate </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> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Try to update the shortest path from x to z using y. </p>
<p>Definition at line <a class="el" href="theory__arith__old_8cpp_source.html#l04927">4927</a> of file <a class="el" href="theory__arith__old_8cpp_source.html">theory_arith_old.cpp</a>.</p>
<p>References <a class="el" href="theory__arith__old_8h_source.html#l00548">CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getEpsilon()</a>, <a class="el" href="theory__arith__old_8h_source.html#l00541">CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getRational()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="theory__arith__old_8h_source.html#l00716">CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::in_path_vertex</a>, <a class="el" href="theory__arith__old_8h_source.html#l00721">CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::isDefined()</a>, <a class="el" href="theory__arith__old_8h_source.html#l00513">CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::isInteger()</a>, <a class="el" href="theory__arith_8h_source.html#l00050">CVC3::LE</a>, <a class="el" href="theory__arith__old_8h_source.html#l00712">CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::length</a>, <a class="el" href="theory__arith__old_8h_source.html#l00714">CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::path_length_in_edges</a>, <a class="el" href="theory__arith__old_8h_source.html#l00695">CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::toString()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>.</p>
</div>
</div>
<a class="anchor" id="ae9325d9bce63e5a62cce23d4aac2db32"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::writeGraph" ref="ae9325d9bce63e5a62cce23d4aac2db32" args="(std::ostream &out)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TheoryArithOld::DifferenceLogicGraph::writeGraph </td>
<td>(</td>
<td class="paramtype">std::ostream & </td>
<td class="paramname"><em>out</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__arith__old_8cpp_source.html#l05872">5872</a> of file <a class="el" href="theory__arith__old_8cpp_source.html">theory_arith_old.cpp</a>.</p>
<p>References <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="cdlist_8h_source.html#l00064">CVC3::CDList< T >::size()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l05535">CVC3::TheoryArithOld::computeTermBounds()</a>.</p>
</div>
</div>
<a class="anchor" id="a4266a410f71d5536394188cd74034b18"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::getVariables" ref="a4266a410f71d5536394188cd74034b18" args="(std::vector< Expr > &variables)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TheoryArithOld::DifferenceLogicGraph::getVariables </td>
<td>(</td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>variables</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Fills the vector with all the variables (vertices) in the graph </p>
<p>Definition at line <a class="el" href="theory__arith__old_8cpp_source.html#l05842">5842</a> of file <a class="el" href="theory__arith__old_8cpp_source.html">theory_arith_old.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l05535">CVC3::TheoryArithOld::computeTermBounds()</a>.</p>
</div>
</div>
<a class="anchor" id="ac13ef29f1852dd0d157b52bdfc050737"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::setRules" ref="ac13ef29f1852dd0d157b52bdfc050737" args="(ArithProofRules *rules)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::TheoryArithOld::DifferenceLogicGraph::setRules </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ArithProofRules.html">ArithProofRules</a> * </td>
<td class="paramname"><em>rules</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__arith__old_8h_source.html#l00806">806</a> of file <a class="el" href="theory__arith__old_8h_source.html">theory_arith_old.h</a>.</p>
<p>References <a class="el" href="theory__arith__old_8h_source.html#l00759">rules</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l02227">CVC3::TheoryArithOld::TheoryArithOld()</a>.</p>
</div>
</div>
<a class="anchor" id="a5b2e50e6e3c75743ace5bb2fae432449"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::setArith" ref="a5b2e50e6e3c75743ace5bb2fae432449" args="(TheoryArithOld *arith)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::TheoryArithOld::DifferenceLogicGraph::setArith </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoryArithOld.html">TheoryArithOld</a> * </td>
<td class="paramname"><em>arith</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__arith__old_8h_source.html#l00810">810</a> of file <a class="el" href="theory__arith__old_8h_source.html">theory_arith_old.h</a>.</p>
<p>References <a class="el" href="theory__arith__old_8h_source.html#l00753">arith</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l02227">CVC3::TheoryArithOld::TheoryArithOld()</a>.</p>
</div>
</div>
<a class="anchor" id="a216bfac9dcbcc62b7097d51fd91e8ac8"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::getUnsatTheorem" ref="a216bfac9dcbcc62b7097d51fd91e8ac8" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> TheoryArithOld::DifferenceLogicGraph::getUnsatTheorem </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Returns the reference to the unsat theorem if there is a negative cycle in the graph.</p>
<dl class="return"><dt><b>Returns:</b></dt><dd>the unsat theorem </dd></dl>
<p>Definition at line <a class="el" href="theory__arith__old_8cpp_source.html#l04724">4724</a> of file <a class="el" href="theory__arith__old_8cpp_source.html">theory_arith_old.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="a828bb2ad8fc3c36506f6a8f3ca38579c"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::isUnsat" ref="a828bb2ad8fc3c36506f6a8f3ca38579c" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool TheoryArithOld::DifferenceLogicGraph::isUnsat </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Returns true if there is a negative cycle in the graph. </p>
<p>Definition at line <a class="el" href="theory__arith__old_8cpp_source.html#l04728">4728</a> of file <a class="el" href="theory__arith__old_8cpp_source.html">theory_arith_old.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="ae7f9ea562c26f55a0536a5cd85cf07b0"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::computeModel" ref="ae7f9ea562c26f55a0536a5cd85cf07b0" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TheoryArithOld::DifferenceLogicGraph::computeModel </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__arith__old_8cpp_source.html#l05111">5111</a> of file <a class="el" href="theory__arith__old_8cpp_source.html">theory_arith_old.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, and <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l02831">CVC3::TheoryArithOld::assignVariables()</a>.</p>
</div>
</div>
<a class="anchor" id="a22cd1525ea447a3bc839fc737240eb4f"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::getValuation" ref="a22cd1525ea447a3bc839fc737240eb4f" args="(const Expr &x)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Rational.html">Rational</a> TheoryArithOld::DifferenceLogicGraph::getValuation </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></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__arith__old_8cpp_source.html#l05150">5150</a> of file <a class="el" href="theory__arith__old_8cpp_source.html">theory_arith_old.cpp</a>.</p>
<p>References <a class="el" href="theory__arith__old_8h_source.html#l00548">CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getEpsilon()</a>, <a class="el" href="theory__arith__old_8h_source.html#l00541">CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getRational()</a>, <a class="el" href="expr_8h_source.html#l01135">CVC3::Expr::getRational()</a>, <a class="el" href="expr_8h_source.html#l00431">CVC3::Expr::isRational()</a>, <a class="el" href="theory__arith__old_8h_source.html#l00712">CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::length</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l02831">CVC3::TheoryArithOld::assignVariables()</a>.</p>
</div>
</div>
<a class="anchor" id="acdd072f244d1d30d5b954bf7b0debe04"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::addEdge" ref="acdd072f244d1d30d5b954bf7b0debe04" args="(const Expr &x, const Expr &y, const Rational &c, const Theorem &edge_thm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TheoryArithOld::DifferenceLogicGraph::addEdge </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_1Rational.html">Rational</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_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>edge_thm</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Adds an edge corresponding to the constraint x - y <= c.</p>
<dl><dt><b>Parameters:</b></dt><dd>
<table class="params">
<tr><td class="paramname">x</td><td>variable x::Difference </td></tr>
<tr><td class="paramname">y</td><td>variable y </td></tr>
<tr><td class="paramname">c</td><td>rational c </td></tr>
<tr><td class="paramname">edge_thm</td><td>the theorem for this edge </td></tr>
</table>
</dd>
</dl>
<p>Definition at line <a class="el" href="theory__arith__old_8cpp_source.html#l04788">4788</a> of file <a class="el" href="theory__arith__old_8cpp_source.html">theory_arith_old.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theory__arith__old_8h_source.html#l00718">CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::explanation</a>, <a class="el" href="cdmap_8h_source.html#l00106">CVC3::CDOmap< Key, Data, HashFcn >::get()</a>, <a class="el" href="theory__arith__old_8h_source.html#l00548">CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getEpsilon()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="theory__arith__old_8h_source.html#l00541">CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getRational()</a>, <a class="el" href="expr_8h_source.html#l01232">CVC3::Expr::hasFind()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="theorem_8cpp_source.html#l00395">CVC3::Theorem::isAssump()</a>, <a class="el" href="theory__arith__old_8h_source.html#l00721">CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::isDefined()</a>, <a class="el" href="theorem_8h_source.html#l00164">CVC3::Theorem::isNull()</a>, <a class="el" href="theory__arith_8h_source.html#l00050">CVC3::LE</a>, <a class="el" href="theory__arith__old_8h_source.html#l00712">CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::length</a>, <a class="el" href="theory__arith_8h_source.html#l00049">CVC3::LT</a>, <a class="el" href="theory__arith__old_8h_source.html#l00714">CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::path_length_in_edges</a>, <a class="el" href="cdlist_8h_source.html#l00066">CVC3::CDList< T >::push_back()</a>, <a class="el" href="cdlist_8h_source.html#l00064">CVC3::CDList< T >::size()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>.</p>
</div>
</div>
<a class="anchor" id="a2213f2040667750f9878aa0ce3ba3f17"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::existsEdge" ref="a2213f2040667750f9878aa0ce3ba3f17" args="(const Expr &x, const Expr &y)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool TheoryArithOld::DifferenceLogicGraph::existsEdge </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></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Check if there is an edge from x to y </p>
<p>Definition at line <a class="el" href="theory__arith__old_8cpp_source.html#l04732">4732</a> of file <a class="el" href="theory__arith__old_8cpp_source.html">theory_arith_old.cpp</a>.</p>
<p>References <a class="el" href="theory__arith__old_8h_source.html#l00721">CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::isDefined()</a>.</p>
</div>
</div>
<a class="anchor" id="a75eceef3b27aa29d23d26ac2a624d095"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::inCycle" ref="a75eceef3b27aa29d23d26ac2a624d095" args="(const Expr &x)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool TheoryArithOld::DifferenceLogicGraph::inCycle </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></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Check if x is in a cycle </p>
<p>Definition at line <a class="el" href="theory__arith__old_8cpp_source.html#l04744">4744</a> of file <a class="el" href="theory__arith__old_8cpp_source.html">theory_arith_old.cpp</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l05535">CVC3::TheoryArithOld::computeTermBounds()</a>.</p>
</div>
</div>
<a class="anchor" id="a247245c8102db8596b73c76cf015fc5d"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::expandSharedTerm" ref="a247245c8102db8596b73c76cf015fc5d" args="(const Expr &x)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TheoryArithOld::DifferenceLogicGraph::expandSharedTerm </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></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Given a shared integer term expand it into the gray shadow on the bounds (if bounded from both sides). </p>
<p>Definition at line <a class="el" href="theory__arith__old_8cpp_source.html#l05020">5020</a> of file <a class="el" href="theory__arith__old_8cpp_source.html">theory_arith_old.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="ad101bbc763a37fb902e4df4a654351de"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::analyseConflict" ref="ad101bbc763a37fb902e4df4a654351de" args="(const Expr &x, int kind)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TheoryArithOld::DifferenceLogicGraph::analyseConflict </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">int </td>
<td class="paramname"><em>kind</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Produced the unsat theorem from a cycle x --> x of negative length</p>
<dl><dt><b>Parameters:</b></dt><dd>
<table class="params">
<tr><td class="paramname">x</td><td>the variable to use for the conflict </td></tr>
<tr><td class="paramname">kind</td><td>the kind of edges to consider </td></tr>
</table>
</dd>
</dl>
<p>Definition at line <a class="el" href="theory__arith__old_8cpp_source.html#l04907">4907</a> of file <a class="el" href="theory__arith__old_8cpp_source.html">theory_arith_old.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="cdmap_8h_source.html#l00106">CVC3::CDOmap< Key, Data, HashFcn >::get()</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="theory__arith__old_8h_source.html#l00721">CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::isDefined()</a>, and <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>.</p>
</div>
</div>
<hr/><h2>Member Data Documentation</h2>
<a class="anchor" id="ae4ed3f0c509c959d36e6637371bf6e05"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::d_pathLenghtThres" ref="ae4ed3f0c509c959d36e6637371bf6e05" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const int* <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#ae4ed3f0c509c959d36e6637371bf6e05">CVC3::TheoryArithOld::DifferenceLogicGraph::d_pathLenghtThres</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Threshold on path length to process (ignore bigger than and set incomplete) </p>
<p>Definition at line <a class="el" href="theory__arith__old_8h_source.html#l00750">750</a> of file <a class="el" href="theory__arith__old_8h_source.html">theory_arith_old.h</a>.</p>
</div>
</div>
<a class="anchor" id="ae172261f15e4d9903b4147b6ee1f4523"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::arith" ref="ae172261f15e4d9903b4147b6ee1f4523" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1TheoryArithOld.html">TheoryArithOld</a>* <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#ae172261f15e4d9903b4147b6ee1f4523">CVC3::TheoryArithOld::DifferenceLogicGraph::arith</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>The arithmetic that's using this graph </p>
<p>Definition at line <a class="el" href="theory__arith__old_8h_source.html#l00753">753</a> of file <a class="el" href="theory__arith__old_8h_source.html">theory_arith_old.h</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8h_source.html#l00810">setArith()</a>.</p>
</div>
</div>
<a class="anchor" id="a6bf38051f1bc2b0703e6ba8ca3b765ae"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::core" ref="a6bf38051f1bc2b0703e6ba8ca3b765ae" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a>* <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a6bf38051f1bc2b0703e6ba8ca3b765ae">CVC3::TheoryArithOld::DifferenceLogicGraph::core</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>The core theory </p>
<p>Definition at line <a class="el" href="theory__arith__old_8h_source.html#l00756">756</a> of file <a class="el" href="theory__arith__old_8h_source.html">theory_arith_old.h</a>.</p>
</div>
</div>
<a class="anchor" id="acbbd4a2fbba125d1069f124e5c271826"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::rules" ref="acbbd4a2fbba125d1069f124e5c271826" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ArithProofRules.html">ArithProofRules</a>* <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#acbbd4a2fbba125d1069f124e5c271826">CVC3::TheoryArithOld::DifferenceLogicGraph::rules</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>The arithmetic that is using u us </p>
<p>Definition at line <a class="el" href="theory__arith__old_8h_source.html#l00759">759</a> of file <a class="el" href="theory__arith__old_8h_source.html">theory_arith_old.h</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8h_source.html#l00806">setRules()</a>.</p>
</div>
</div>
<a class="anchor" id="a627796132ea73d35fbcf828d68425a3b"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::unsat_theorem" ref="a627796132ea73d35fbcf828d68425a3b" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDO.html">CDO</a><<a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>> <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a627796132ea73d35fbcf828d68425a3b">CVC3::TheoryArithOld::DifferenceLogicGraph::unsat_theorem</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>The unsat theorem if available </p>
<p>Definition at line <a class="el" href="theory__arith__old_8h_source.html#l00762">762</a> of file <a class="el" href="theory__arith__old_8h_source.html">theory_arith_old.h</a>.</p>
</div>
</div>
<a class="anchor" id="ae4d498b950e7b37b5b48c936139cfc70"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::biggestEpsilon" ref="ae4d498b950e7b37b5b48c936139cfc70" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDO.html">CDO</a><<a class="el" href="classCVC3_1_1Rational.html">Rational</a>> <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#ae4d498b950e7b37b5b48c936139cfc70">CVC3::TheoryArithOld::DifferenceLogicGraph::biggestEpsilon</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>The biggest epsilon from <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph_1_1EpsRational.html">EpsRational</a> we used in paths </p>
<p>Definition at line <a class="el" href="theory__arith__old_8h_source.html#l00765">765</a> of file <a class="el" href="theory__arith__old_8h_source.html">theory_arith_old.h</a>.</p>
</div>
</div>
<a class="anchor" id="a2519a13732d48786f8fe83351a7150c8"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::smallestPathDifference" ref="a2519a13732d48786f8fe83351a7150c8" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDO.html">CDO</a><<a class="el" href="classCVC3_1_1Rational.html">Rational</a>> <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a2519a13732d48786f8fe83351a7150c8">CVC3::TheoryArithOld::DifferenceLogicGraph::smallestPathDifference</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>The smallest rational difference we used in path relaxation </p>
<p>Definition at line <a class="el" href="theory__arith__old_8h_source.html#l00768">768</a> of file <a class="el" href="theory__arith__old_8h_source.html">theory_arith_old.h</a>.</p>
</div>
</div>
<a class="anchor" id="a47342aafbf5caa7aca2fbd5e9511cef1"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::leGraph" ref="a47342aafbf5caa7aca2fbd5e9511cef1" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDMap.html">Graph</a> <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a47342aafbf5caa7aca2fbd5e9511cef1">CVC3::TheoryArithOld::DifferenceLogicGraph::leGraph</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Graph of <= paths </p>
<p>Definition at line <a class="el" href="theory__arith__old_8h_source.html#l00774">774</a> of file <a class="el" href="theory__arith__old_8h_source.html">theory_arith_old.h</a>.</p>
</div>
</div>
<a class="anchor" id="a6a605397e227cc5b9c287984ead0902b"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::incomingEdges" ref="a6a605397e227cc5b9c287984ead0902b" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprMap.html">EdgesList</a> <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a6a605397e227cc5b9c287984ead0902b">CVC3::TheoryArithOld::DifferenceLogicGraph::incomingEdges</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>List of vertices adjacent backwards to a vertex </p>
<p>Definition at line <a class="el" href="theory__arith__old_8h_source.html#l00779">779</a> of file <a class="el" href="theory__arith__old_8h_source.html">theory_arith_old.h</a>.</p>
</div>
</div>
<a class="anchor" id="ac0fa1b22e8ed0d8d0580599998b36bf2"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::outgoingEdges" ref="ac0fa1b22e8ed0d8d0580599998b36bf2" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprMap.html">EdgesList</a> <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#ac0fa1b22e8ed0d8d0580599998b36bf2">CVC3::TheoryArithOld::DifferenceLogicGraph::outgoingEdges</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>List of vertices adjacent forward to a vertex </p>
<p>Definition at line <a class="el" href="theory__arith__old_8h_source.html#l00781">781</a> of file <a class="el" href="theory__arith__old_8h_source.html">theory_arith_old.h</a>.</p>
</div>
</div>
<a class="anchor" id="a478a837c6562772e151cbfef55e607ee"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::varInCycle" ref="a478a837c6562772e151cbfef55e607ee" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDMap.html">CDMap</a><<a class="el" href="classCVC3_1_1Expr.html">Expr</a>, bool> <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a478a837c6562772e151cbfef55e607ee">CVC3::TheoryArithOld::DifferenceLogicGraph::varInCycle</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Whether the variable is in a cycle </p>
<p>Definition at line <a class="el" href="theory__arith__old_8h_source.html#l00871">871</a> of file <a class="el" href="theory__arith__old_8h_source.html">theory_arith_old.h</a>.</p>
</div>
</div>
<a class="anchor" id="a7b0dd9d1e47d917391c0ed987608bb57"></a><!-- doxytag: member="CVC3::TheoryArithOld::DifferenceLogicGraph::sourceVertex" ref="a7b0dd9d1e47d917391c0ed987608bb57" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a7b0dd9d1e47d917391c0ed987608bb57">CVC3::TheoryArithOld::DifferenceLogicGraph::sourceVertex</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__arith__old_8h_source.html#l00873">873</a> of file <a class="el" href="theory__arith__old_8h_source.html">theory_arith_old.h</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="theory__arith__old_8h_source.html">theory_arith_old.h</a></li>
<li><a class="el" href="theory__arith__old_8cpp_source.html">theory_arith_old.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>
