<!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: TReturn 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>
<div class="header">
<div class="summary">
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pub-static-methods">Static Public Member Functions</a> |
<a href="#pri-attribs">Private Attributes</a> </div>
<div class="headertitle">
<div class="title">TReturn Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="TReturn" --><!-- doxytag: inherits="LFSCObj" -->
<p><code>#include <<a class="el" href="TReturn_8h_source.html">TReturn.h</a>></code></p>
<div class="dynheader">
Inheritance diagram for TReturn:</div>
<div class="dyncontent">
<div class="center">
<img src="classTReturn.png" usemap="#TReturn_map" alt=""/>
<map id="TReturn_map" name="TReturn_map">
<area href="classLFSCObj.html" alt="LFSCObj" shape="rect" coords="0,56,64,80"/>
<area href="classObj.html" alt="Obj" shape="rect" coords="0,0,64,24"/>
</map>
</div></div>
<p><a href="classTReturn-members.html">List of all members.</a></p>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li><a class="el" href="classTReturn.html#a9554576fa26fd8e19942ff4a2f566bbf">TReturn</a> (<a class="el" href="classLFSCProof.html">LFSCProof</a> *lfsc_pf, std::vector< int > &L, std::vector< int > &Lused, <a class="el" href="classCVC3_1_1Rational.html">Rational</a> r, bool hasR, int pvY)
<li><a class="el" href="classCVC3_1_1Rational.html">Rational</a> <a class="el" href="classTReturn.html#ac7a0e50d750845a8cfd72bc9faf4949d">mult_rational</a> (<a class="el" href="classTReturn.html">TReturn</a> *lhs)
<li>void <a class="el" href="classTReturn.html#ab5fe603ed277f47bdc014df335f33a44">getL</a> (std::vector< int > &lget, std::vector< int > &lgetu)
<li>bool <a class="el" href="classTReturn.html#abae84e878863b3a6978d7dde0d52522a">hasRational</a> ()
<li><a class="el" href="classCVC3_1_1Rational.html">Rational</a> <a class="el" href="classTReturn.html#afc199e16f310243abfdf0f08f248401b">getRational</a> ()
<li><a class="el" href="classLFSCProof.html">LFSCProof</a> * <a class="el" href="classTReturn.html#a75ec103851040bcd454dde054227a3c2">getLFSCProof</a> ()
<li>int <a class="el" href="classTReturn.html#adfcacf33921f81fe720ef5b30b184153">getProvesY</a> ()
<li>bool <a class="el" href="classTReturn.html#a072febb7e4c799752ddc9c0c04eef157">hasFv</a> ()
</ul>
<h2><a name="pub-static-methods"></a>
Static Public Member Functions</h2>
<ul>
<li>static int <a class="el" href="classTReturn.html#adf5d458ca36004015a91b8be7dbd341b">normalize_tret</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &pf1, <a class="el" href="classTReturn.html">TReturn</a> *&t1, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &pf2, <a class="el" href="classTReturn.html">TReturn</a> *&t2, bool rev_pol=false)
<li>static int <a class="el" href="classTReturn.html#a76fa4cdab1d66c56bc96d3630150f030">normalize_tr</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &pf1, <a class="el" href="classTReturn.html">TReturn</a> *&t1, int y, bool rev_pol=false, bool printErr=true)
<li>static void <a class="el" href="classTReturn.html#a4cb0fc0f38683bd372e4111771c273ef">normalize_to_tf</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &pf, <a class="el" href="classTReturn.html">TReturn</a> *&t1, int y)
</ul>
<h2><a name="pri-attribs"></a>
Private Attributes</h2>
<ul>
<li><a class="el" href="classRefPtr.html">RefPtr</a>< <a class="el" href="classLFSCProof.html">LFSCProof</a> > <a class="el" href="classTReturn.html#a934ee85a303379f5c699b88be35224ad">d_lfsc_pf</a>
<li>std::vector< int > <a class="el" href="classTReturn.html#a7b8e49b2d097ca45103e11e0dd2019aa">d_L</a>
<li>std::vector< int > <a class="el" href="classTReturn.html#ab2e40626799f04887f80159b0d74521a">d_L_used</a>
<li><a class="el" href="classCVC3_1_1Rational.html">Rational</a> <a class="el" href="classTReturn.html#a2306f247630ba7d133db2e63651a584a">d_c</a>
<li>bool <a class="el" href="classTReturn.html#a3aeca59a077b015fe579ad447ac94e29">d_hasRt</a>
<li>int <a class="el" href="classTReturn.html#a698d236c454a4d9ebe3c461d38d9dab0">d_provesY</a>
<li>bool <a class="el" href="classTReturn.html#aa05c68c3ad6926cb6bd48335092c9c4e">lcalced</a>
</ul>
<hr/><a name="details" id="details"></a><h2>Detailed Description</h2>
<div class="textblock">
<p>Definition at line <a class="el" href="TReturn_8h_source.html#l00011">11</a> of file <a class="el" href="TReturn_8h_source.html">TReturn.h</a>.</p>
</div><hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="a9554576fa26fd8e19942ff4a2f566bbf"></a><!-- doxytag: member="TReturn::TReturn" ref="a9554576fa26fd8e19942ff4a2f566bbf" args="(LFSCProof *lfsc_pf, std::vector< int > &L, std::vector< int > &Lused, Rational r, bool hasR, int pvY)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">TReturn::TReturn </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classLFSCProof.html">LFSCProof</a> * </td>
<td class="paramname"><em>lfsc_pf</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< int > & </td>
<td class="paramname"><em>L</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< int > & </td>
<td class="paramname"><em>Lused</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>r</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>hasR</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>pvY</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="TReturn_8cpp_source.html#l00008">8</a> of file <a class="el" href="TReturn_8cpp_source.html">TReturn.cpp</a>.</p>
<p>References <a class="el" href="TReturn_8h_source.html#l00021">d_hasRt</a>, <a class="el" href="TReturn_8h_source.html#l00016">d_L</a>, <a class="el" href="TReturn_8h_source.html#l00018">d_L_used</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, and <a class="el" href="TReturn_8h_source.html#l00029">lcalced</a>.</p>
<p>Referenced by <a class="el" href="TReturn_8cpp_source.html#l00423">normalize_to_tf()</a>, and <a class="el" href="TReturn_8cpp_source.html#l00125">normalize_tr()</a>.</p>
</div>
</div>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="ac7a0e50d750845a8cfd72bc9faf4949d"></a><!-- doxytag: member="TReturn::mult_rational" ref="ac7a0e50d750845a8cfd72bc9faf4949d" args="(TReturn *lhs)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Rational.html">Rational</a> TReturn::mult_rational </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classTReturn.html">TReturn</a> * </td>
<td class="paramname"><em>lhs</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="TReturn_8cpp_source.html#l00024">24</a> of file <a class="el" href="TReturn_8cpp_source.html">TReturn.cpp</a>.</p>
<p>References <a class="el" href="TReturn_8h_source.html#l00020">d_c</a>, <a class="el" href="TReturn_8h_source.html#l00035">hasRational()</a>, and <a class="el" href="TReturn_8cpp_source.html#l00024">mult_rational()</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00093">LFSCConvert::cvc3_to_lfsc()</a>, and <a class="el" href="TReturn_8cpp_source.html#l00024">mult_rational()</a>.</p>
</div>
</div>
<a class="anchor" id="ab5fe603ed277f47bdc014df335f33a44"></a><!-- doxytag: member="TReturn::getL" ref="ab5fe603ed277f47bdc014df335f33a44" args="(std::vector< int > &lget, std::vector< int > &lgetu)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TReturn::getL </td>
<td>(</td>
<td class="paramtype">std::vector< int > & </td>
<td class="paramname"><em>lget</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< int > & </td>
<td class="paramname"><em>lgetu</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="TReturn_8cpp_source.html#l00037">37</a> of file <a class="el" href="TReturn_8cpp_source.html">TReturn.cpp</a>.</p>
<p>References <a class="el" href="TReturn_8h_source.html#l00016">d_L</a>, and <a class="el" href="TReturn_8h_source.html#l00018">d_L_used</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00093">LFSCConvert::cvc3_to_lfsc()</a>, <a class="el" href="LFSCConvert_8cpp_source.html#l01718">LFSCConvert::do_bso()</a>, <a class="el" href="LFSCConvert_8cpp_source.html#l01663">LFSCConvert::make_let_proof()</a>, <a class="el" href="TReturn_8cpp_source.html#l00423">normalize_to_tf()</a>, and <a class="el" href="TReturn_8cpp_source.html#l00125">normalize_tr()</a>.</p>
</div>
</div>
<a class="anchor" id="abae84e878863b3a6978d7dde0d52522a"></a><!-- doxytag: member="TReturn::hasRational" ref="abae84e878863b3a6978d7dde0d52522a" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool TReturn::hasRational </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="TReturn_8h_source.html#l00035">35</a> of file <a class="el" href="TReturn_8h_source.html">TReturn.h</a>.</p>
<p>References <a class="el" href="TReturn_8h_source.html#l00021">d_hasRt</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00093">LFSCConvert::cvc3_to_lfsc()</a>, <a class="el" href="TReturn_8cpp_source.html#l00024">mult_rational()</a>, and <a class="el" href="TReturn_8cpp_source.html#l00125">normalize_tr()</a>.</p>
</div>
</div>
<a class="anchor" id="afc199e16f310243abfdf0f08f248401b"></a><!-- doxytag: member="TReturn::getRational" ref="afc199e16f310243abfdf0f08f248401b" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Rational.html">Rational</a> TReturn::getRational </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="TReturn_8h_source.html#l00036">36</a> of file <a class="el" href="TReturn_8h_source.html">TReturn.h</a>.</p>
<p>References <a class="el" href="TReturn_8h_source.html#l00020">d_c</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00093">LFSCConvert::cvc3_to_lfsc()</a>, and <a class="el" href="TReturn_8cpp_source.html#l00125">normalize_tr()</a>.</p>
</div>
</div>
<a class="anchor" id="a75ec103851040bcd454dde054227a3c2"></a><!-- doxytag: member="TReturn::getLFSCProof" ref="a75ec103851040bcd454dde054227a3c2" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classLFSCProof.html">LFSCProof</a>* TReturn::getLFSCProof </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="TReturn_8h_source.html#l00037">37</a> of file <a class="el" href="TReturn_8h_source.html">TReturn.h</a>.</p>
<p>References <a class="el" href="TReturn_8h_source.html#l00014">d_lfsc_pf</a>, and <a class="el" href="Object_8h_source.html#l00056">RefPtr< T >::get()</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00018">LFSCConvert::convert()</a>, <a class="el" href="LFSCConvert_8cpp_source.html#l00093">LFSCConvert::cvc3_to_lfsc()</a>, <a class="el" href="LFSCConvert_8cpp_source.html#l01718">LFSCConvert::do_bso()</a>, <a class="el" href="TReturn_8cpp_source.html#l00423">normalize_to_tf()</a>, and <a class="el" href="TReturn_8cpp_source.html#l00125">normalize_tr()</a>.</p>
</div>
</div>
<a class="anchor" id="adfcacf33921f81fe720ef5b30b184153"></a><!-- doxytag: member="TReturn::getProvesY" ref="adfcacf33921f81fe720ef5b30b184153" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int TReturn::getProvesY </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="TReturn_8h_source.html#l00038">38</a> of file <a class="el" href="TReturn_8h_source.html">TReturn.h</a>.</p>
<p>References <a class="el" href="TReturn_8h_source.html#l00028">d_provesY</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00018">LFSCConvert::convert()</a>, <a class="el" href="LFSCConvert_8cpp_source.html#l00093">LFSCConvert::cvc3_to_lfsc()</a>, <a class="el" href="LFSCConvert_8cpp_source.html#l01718">LFSCConvert::do_bso()</a>, <a class="el" href="TReturn_8cpp_source.html#l00423">normalize_to_tf()</a>, <a class="el" href="TReturn_8cpp_source.html#l00125">normalize_tr()</a>, and <a class="el" href="TReturn_8cpp_source.html#l00084">normalize_tret()</a>.</p>
</div>
</div>
<a class="anchor" id="a072febb7e4c799752ddc9c0c04eef157"></a><!-- doxytag: member="TReturn::hasFv" ref="a072febb7e4c799752ddc9c0c04eef157" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool TReturn::hasFv </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="TReturn_8h_source.html#l00039">39</a> of file <a class="el" href="TReturn_8h_source.html">TReturn.h</a>.</p>
<p>References <a class="el" href="TReturn_8h_source.html#l00018">d_L_used</a>.</p>
</div>
</div>
<a class="anchor" id="adf5d458ca36004015a91b8be7dbd341b"></a><!-- doxytag: member="TReturn::normalize_tret" ref="adf5d458ca36004015a91b8be7dbd341b" args="(const Expr &pf1, TReturn *&t1, const Expr &pf2, TReturn *&t2, bool rev_pol=false)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int TReturn::normalize_tret </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>pf1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classTReturn.html">TReturn</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>pf2</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classTReturn.html">TReturn</a> *& </td>
<td class="paramname"><em>t2</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>rev_pol</em> = <code>false</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="TReturn_8cpp_source.html#l00084">84</a> of file <a class="el" href="TReturn_8cpp_source.html">TReturn.cpp</a>.</p>
<p>References <a class="el" href="LFSCObject_8h_source.html#l00024">LFSCObj::debug_conv</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="TReturn_8h_source.html#l00038">getProvesY()</a>, <a class="el" href="TReturn_8cpp_source.html#l00125">normalize_tr()</a>, and <a class="el" href="Object_8h_source.html#l00095">Obj::print_error()</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00093">LFSCConvert::cvc3_to_lfsc()</a>, and <a class="el" href="LFSCConvert_8cpp_source.html#l01718">LFSCConvert::do_bso()</a>.</p>
</div>
</div>
<a class="anchor" id="a76fa4cdab1d66c56bc96d3630150f030"></a><!-- doxytag: member="TReturn::normalize_tr" ref="a76fa4cdab1d66c56bc96d3630150f030" args="(const Expr &pf1, TReturn *&t1, int y, bool rev_pol=false, bool printErr=true)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int TReturn::normalize_tr </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>pf1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classTReturn.html">TReturn</a> *& </td>
<td class="paramname"><em>t1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>y</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>rev_pol</em> = <code>false</code>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>printErr</em> = <code>true</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="TReturn_8cpp_source.html#l00125">125</a> of file <a class="el" href="TReturn_8cpp_source.html">TReturn.cpp</a>.</p>
<p>References <a class="el" href="cvc__util_8h_source.html#l00053">CVC3::abs()</a>, <a class="el" href="LFSCObject_8cpp_source.html#l00520">LFSCObj::can_pnorm()</a>, <a class="el" href="LFSCObject_8h_source.html#l00024">LFSCObj::debug_conv</a>, <a class="el" href="kinds_8h_source.html#l00063">DISTINCT</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="kinds_8h_source.html#l00061">EQ</a>, <a class="el" href="Object_8h_source.html#l00056">RefPtr< T >::get()</a>, <a class="el" href="Util_8cpp_source.html#l00100">get_normalized()</a>, <a class="el" href="LFSCProof_8h_source.html#l00103">LFSCProof::getChOp()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="TReturn_8cpp_source.html#l00037">getL()</a>, <a class="el" href="TReturn_8h_source.html#l00037">getLFSCProof()</a>, <a class="el" href="TReturn_8h_source.html#l00038">getProvesY()</a>, <a class="el" href="TReturn_8h_source.html#l00036">getRational()</a>, <a class="el" href="theory__arith_8h_source.html#l00051">CVC3::GT</a>, <a class="el" href="TReturn_8h_source.html#l00035">hasRational()</a>, <a class="el" href="kinds_8h_source.html#l00070">IFF</a>, <a class="el" href="kinds_8h_source.html#l00071">IMPLIES</a>, <a class="el" href="Util_8cpp_source.html#l00070">is_comparison()</a>, <a class="el" href="Util_8cpp_source.html#l00047">is_eq_kind()</a>, <a class="el" href="expr_8h_source.html#l00355">CVC3::Expr::isFalse()</a>, <a class="el" href="expr_8h_source.html#l00424">CVC3::Expr::isIff()</a>, <a class="el" href="expr_8h_source.html#l00425">CVC3::Expr::isImpl()</a>, <a class="el" href="expr_8h_source.html#l00356">CVC3::Expr::isTrue()</a>, <a class="el" href="LFSCBoolProof_8h_source.html#l00103">LFSCAssume::Make()</a>, <a class="el" href="LFSCLraProof_8cpp_source.html#l00089">LFSCLraSub::Make()</a>, <a class="el" href="LFSCLraProof_8cpp_source.html#l00065">LFSCLraMulC::Make()</a>, <a class="el" href="LFSCLraProof_8h_source.html#l00159">LFSCLraContra::Make()</a>, <a class="el" href="LFSCLraProof_8cpp_source.html#l00017">LFSCLraAdd::Make()</a>, <a class="el" href="LFSCUtilProof_8cpp_source.html#l00033">LFSCPfVar::Make()</a>, <a class="el" href="LFSCUtilProof_8h_source.html#l00080">LFSCProofGeneric::Make()</a>, <a class="el" href="LFSCUtilProof_8h_source.html#l00017">LFSCProofExpr::Make()</a>, <a class="el" href="LFSCLraProof_8h_source.html#l00127">LFSCLraPoly::Make()</a>, <a class="el" href="LFSCBoolProof_8h_source.html#l00076">LFSCClausify::Make()</a>, <a class="el" href="LFSCUtilProof_8cpp_source.html#l00113">LFSCProofGeneric::MakeStr()</a>, <a class="el" href="TReturn_8cpp_source.html#l00423">normalize_to_tf()</a>, <a class="el" href="kinds_8h_source.html#l00066">NOT</a>, <a class="el" href="LFSCObject_8h_source.html#l00029">LFSCObj::nullRat</a>, <a class="el" href="Object_8h_source.html#l00095">Obj::print_error()</a>, <a class="el" href="LFSCPrinter_8h_source.html#l00042">LFSCPrinter::print_formula()</a>, <a class="el" href="LFSCObject_8h_source.html#l00016">LFSCObj::printer</a>, <a class="el" href="LFSCObject_8cpp_source.html#l00365">LFSCObj::queryAtomic()</a>, <a class="el" href="LFSCObject_8cpp_source.html#l00356">LFSCObj::queryElimNotNot()</a>, <a class="el" href="LFSCObject_8cpp_source.html#l00386">LFSCObj::queryM()</a>, <a class="el" href="LFSCProof_8h_source.html#l00104">LFSCProof::setChOp()</a>, <a class="el" href="TReturn_8cpp_source.html#l00008">TReturn()</a>, and <a class="el" href="LFSCObject_8cpp_source.html#l00539">LFSCObj::what_is_proven()</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00093">LFSCConvert::cvc3_to_lfsc()</a>, <a class="el" href="LFSCConvert_8cpp_source.html#l01718">LFSCConvert::do_bso()</a>, and <a class="el" href="TReturn_8cpp_source.html#l00084">normalize_tret()</a>.</p>
</div>
</div>
<a class="anchor" id="a4cb0fc0f38683bd372e4111771c273ef"></a><!-- doxytag: member="TReturn::normalize_to_tf" ref="a4cb0fc0f38683bd372e4111771c273ef" args="(const Expr &pf, TReturn *&t1, int y)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TReturn::normalize_to_tf </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>pf</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classTReturn.html">TReturn</a> *& </td>
<td class="paramname"><em>t1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>y</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="TReturn_8cpp_source.html#l00423">423</a> of file <a class="el" href="TReturn_8cpp_source.html">TReturn.cpp</a>.</p>
<p>References <a class="el" href="cvc__util_8h_source.html#l00053">CVC3::abs()</a>, <a class="el" href="LFSCProof_8h_source.html#l00052">LFSCProof::AsLFSCLraPoly()</a>, <a class="el" href="kinds_8h_source.html#l00063">DISTINCT</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="Object_8h_source.html#l00056">RefPtr< T >::get()</a>, <a class="el" href="Util_8cpp_source.html#l00100">get_normalized()</a>, <a class="el" href="LFSCProof_8h_source.html#l00101">LFSCProof::getChild()</a>, <a class="el" href="LFSCProof_8h_source.html#l00103">LFSCProof::getChOp()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="TReturn_8cpp_source.html#l00037">getL()</a>, <a class="el" href="TReturn_8h_source.html#l00037">getLFSCProof()</a>, <a class="el" href="TReturn_8h_source.html#l00038">getProvesY()</a>, <a class="el" href="theory__arith_8h_source.html#l00051">CVC3::GT</a>, <a class="el" href="Util_8cpp_source.html#l00070">is_comparison()</a>, <a class="el" href="LFSCBoolProof_8h_source.html#l00103">LFSCAssume::Make()</a>, <a class="el" href="LFSCLraProof_8cpp_source.html#l00017">LFSCLraAdd::Make()</a>, <a class="el" href="LFSCLraProof_8h_source.html#l00159">LFSCLraContra::Make()</a>, <a class="el" href="LFSCLraProof_8h_source.html#l00127">LFSCLraPoly::Make()</a>, <a class="el" href="LFSCUtilProof_8cpp_source.html#l00033">LFSCPfVar::Make()</a>, <a class="el" href="kinds_8h_source.html#l00066">NOT</a>, <a class="el" href="LFSCObject_8h_source.html#l00029">LFSCObj::nullRat</a>, <a class="el" href="Object_8h_source.html#l00095">Obj::print_error()</a>, <a class="el" href="LFSCObject_8cpp_source.html#l00365">LFSCObj::queryAtomic()</a>, <a class="el" href="LFSCObject_8cpp_source.html#l00386">LFSCObj::queryM()</a>, <a class="el" href="LFSCProof_8h_source.html#l00104">LFSCProof::setChOp()</a>, and <a class="el" href="TReturn_8cpp_source.html#l00008">TReturn()</a>.</p>
<p>Referenced by <a class="el" href="TReturn_8cpp_source.html#l00125">normalize_tr()</a>.</p>
</div>
</div>
<hr/><h2>Member Data Documentation</h2>
<a class="anchor" id="a934ee85a303379f5c699b88be35224ad"></a><!-- doxytag: member="TReturn::d_lfsc_pf" ref="a934ee85a303379f5c699b88be35224ad" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classRefPtr.html">RefPtr</a>< <a class="el" href="classLFSCProof.html">LFSCProof</a> > <a class="el" href="classTReturn.html#a934ee85a303379f5c699b88be35224ad">TReturn::d_lfsc_pf</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="TReturn_8h_source.html#l00014">14</a> of file <a class="el" href="TReturn_8h_source.html">TReturn.h</a>.</p>
<p>Referenced by <a class="el" href="TReturn_8h_source.html#l00037">getLFSCProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a7b8e49b2d097ca45103e11e0dd2019aa"></a><!-- doxytag: member="TReturn::d_L" ref="a7b8e49b2d097ca45103e11e0dd2019aa" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<int> <a class="el" href="classTReturn.html#a7b8e49b2d097ca45103e11e0dd2019aa">TReturn::d_L</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="TReturn_8h_source.html#l00016">16</a> of file <a class="el" href="TReturn_8h_source.html">TReturn.h</a>.</p>
<p>Referenced by <a class="el" href="TReturn_8cpp_source.html#l00037">getL()</a>, and <a class="el" href="TReturn_8cpp_source.html#l00008">TReturn()</a>.</p>
</div>
</div>
<a class="anchor" id="ab2e40626799f04887f80159b0d74521a"></a><!-- doxytag: member="TReturn::d_L_used" ref="ab2e40626799f04887f80159b0d74521a" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<int> <a class="el" href="classTReturn.html#ab2e40626799f04887f80159b0d74521a">TReturn::d_L_used</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="TReturn_8h_source.html#l00018">18</a> of file <a class="el" href="TReturn_8h_source.html">TReturn.h</a>.</p>
<p>Referenced by <a class="el" href="TReturn_8cpp_source.html#l00037">getL()</a>, <a class="el" href="TReturn_8h_source.html#l00039">hasFv()</a>, and <a class="el" href="TReturn_8cpp_source.html#l00008">TReturn()</a>.</p>
</div>
</div>
<a class="anchor" id="a2306f247630ba7d133db2e63651a584a"></a><!-- doxytag: member="TReturn::d_c" ref="a2306f247630ba7d133db2e63651a584a" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Rational.html">Rational</a> <a class="el" href="classTReturn.html#a2306f247630ba7d133db2e63651a584a">TReturn::d_c</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="TReturn_8h_source.html#l00020">20</a> of file <a class="el" href="TReturn_8h_source.html">TReturn.h</a>.</p>
<p>Referenced by <a class="el" href="TReturn_8h_source.html#l00036">getRational()</a>, and <a class="el" href="TReturn_8cpp_source.html#l00024">mult_rational()</a>.</p>
</div>
</div>
<a class="anchor" id="a3aeca59a077b015fe579ad447ac94e29"></a><!-- doxytag: member="TReturn::d_hasRt" ref="a3aeca59a077b015fe579ad447ac94e29" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classTReturn.html#a3aeca59a077b015fe579ad447ac94e29">TReturn::d_hasRt</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="TReturn_8h_source.html#l00021">21</a> of file <a class="el" href="TReturn_8h_source.html">TReturn.h</a>.</p>
<p>Referenced by <a class="el" href="TReturn_8h_source.html#l00035">hasRational()</a>, and <a class="el" href="TReturn_8cpp_source.html#l00008">TReturn()</a>.</p>
</div>
</div>
<a class="anchor" id="a698d236c454a4d9ebe3c461d38d9dab0"></a><!-- doxytag: member="TReturn::d_provesY" ref="a698d236c454a4d9ebe3c461d38d9dab0" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classTReturn.html#a698d236c454a4d9ebe3c461d38d9dab0">TReturn::d_provesY</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="TReturn_8h_source.html#l00028">28</a> of file <a class="el" href="TReturn_8h_source.html">TReturn.h</a>.</p>
<p>Referenced by <a class="el" href="TReturn_8h_source.html#l00038">getProvesY()</a>.</p>
</div>
</div>
<a class="anchor" id="aa05c68c3ad6926cb6bd48335092c9c4e"></a><!-- doxytag: member="TReturn::lcalced" ref="aa05c68c3ad6926cb6bd48335092c9c4e" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classTReturn.html#aa05c68c3ad6926cb6bd48335092c9c4e">TReturn::lcalced</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="TReturn_8h_source.html#l00029">29</a> of file <a class="el" href="TReturn_8h_source.html">TReturn.h</a>.</p>
<p>Referenced by <a class="el" href="TReturn_8cpp_source.html#l00008">TReturn()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="TReturn_8h_source.html">TReturn.h</a></li>
<li><a class="el" href="TReturn_8cpp_source.html">TReturn.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>
