<!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"/>
<meta http-equiv="X-UA-Compatible" content="IE=9"/>
<title>CVC3: TReturn.h Source File</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="jquery.js"></script>
<script type="text/javascript" src="dynsections.js"></script>
<link href="doxygen.css" rel="stylesheet" type="text/css" />
</head>
<body>
<div id="top"><!-- do not remove this div, it is closed by doxygen! -->
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3
</div>
</td>
</tr>
</tbody>
</table>
</div>
<!-- end header part -->
<!-- Generated by Doxygen 1.8.2 -->
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li><a href="annotated.html"><span>Classes</span></a></li>
<li class="current"><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="files.html"><span>File List</span></a></li>
<li><a href="globals.html"><span>File Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="dir_68267d1309a1af8e8297ef4c3efbcdba.html">src</a></li><li class="navelem"><a class="el" href="dir_5e53e25df8c865d23c4f0f620d3a69fb.html">search</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="headertitle">
<div class="title">TReturn.h</div> </div>
</div><!--header-->
<div class="contents">
<a href="TReturn_8h.html">Go to the documentation of this file.</a><div class="fragment"><div class="line"><a name="l00001"></a><span class="lineno"> 1</span> <span class="preprocessor">#ifndef TRETURN_H_</span></div>
<div class="line"><a name="l00002"></a><span class="lineno"> 2</span> <span class="preprocessor"></span><span class="preprocessor">#define TRETURN_H_</span></div>
<div class="line"><a name="l00003"></a><span class="lineno"> 3</span> <span class="preprocessor"></span></div>
<div class="line"><a name="l00004"></a><span class="lineno"> 4</span> <span class="preprocessor">#include "<a class="code" href="LFSCProof_8h.html">LFSCProof.h</a>"</span></div>
<div class="line"><a name="l00005"></a><span class="lineno"> 5</span> <span class="comment"></span></div>
<div class="line"><a name="l00006"></a><span class="lineno"> 6</span> <span class="comment">//////////////////////////////////////////</span></div>
<div class="line"><a name="l00007"></a><span class="lineno"> 7</span> <span class="comment"></span><span class="comment">// TReturn = (p_lfsc, L, c)</span></div>
<div class="line"><a name="l00008"></a><span class="lineno"> 8</span> <span class="comment">// implements transformation</span><span class="comment"></span></div>
<div class="line"><a name="l00009"></a><span class="lineno"> 9</span> <span class="comment">/////////////////////////////////////////</span></div>
<div class="line"><a name="l00010"></a><span class="lineno"> 10</span> <span class="comment"></span></div>
<div class="line"><a name="l00011"></a><span class="lineno"><a class="code" href="classTReturn.html"> 11</a></span> <span class="keyword">class </span><a class="code" href="classTReturn.html">TReturn</a> : <span class="keyword">public</span> <a class="code" href="classLFSCObj.html">LFSCObj</a></div>
<div class="line"><a name="l00012"></a><span class="lineno"> 12</span> {</div>
<div class="line"><a name="l00013"></a><span class="lineno"> 13</span> <span class="keyword">private</span>:</div>
<div class="line"><a name="l00014"></a><span class="lineno"><a class="code" href="classTReturn.html#a934ee85a303379f5c699b88be35224ad"> 14</a></span>  <a class="code" href="classRefPtr.html">RefPtr< LFSCProof ></a> <a class="code" href="classTReturn.html#a934ee85a303379f5c699b88be35224ad">d_lfsc_pf</a>;</div>
<div class="line"><a name="l00015"></a><span class="lineno"> 15</span>  <span class="comment">// literals (we only store the indices) i corresponds to v_i and -i to not v_i</span></div>
<div class="line"><a name="l00016"></a><span class="lineno"><a class="code" href="classTReturn.html#a7b8e49b2d097ca45103e11e0dd2019aa"> 16</a></span>  std::vector <int> <a class="code" href="classTReturn.html#a7b8e49b2d097ca45103e11e0dd2019aa">d_L</a>;</div>
<div class="line"><a name="l00017"></a><span class="lineno"> 17</span>  <span class="comment">// literals we use</span></div>
<div class="line"><a name="l00018"></a><span class="lineno"><a class="code" href="classTReturn.html#ab2e40626799f04887f80159b0d74521a"> 18</a></span>  std::vector <int> <a class="code" href="classTReturn.html#ab2e40626799f04887f80159b0d74521a">d_L_used</a>;</div>
<div class="line"><a name="l00019"></a><span class="lineno"> 19</span>  <span class="comment">// constant</span></div>
<div class="line"><a name="l00020"></a><span class="lineno"><a class="code" href="classTReturn.html#a2306f247630ba7d133db2e63651a584a"> 20</a></span>  <a class="code" href="classCVC3_1_1Rational.html">Rational</a> <a class="code" href="classTReturn.html#a2306f247630ba7d133db2e63651a584a">d_c</a>;</div>
<div class="line"><a name="l00021"></a><span class="lineno"><a class="code" href="classTReturn.html#a3aeca59a077b015fe579ad447ac94e29"> 21</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classTReturn.html#a3aeca59a077b015fe579ad447ac94e29">d_hasRt</a>;</div>
<div class="line"><a name="l00022"></a><span class="lineno"> 22</span>  <span class="comment">// constructor</span></div>
<div class="line"><a name="l00023"></a><span class="lineno"> 23</span>  <span class="comment">//flag for whether d_lfsc_pf is proving</span></div>
<div class="line"><a name="l00024"></a><span class="lineno"> 24</span>  <span class="comment">//0: psi,</span></div>
<div class="line"><a name="l00025"></a><span class="lineno"> 25</span>  <span class="comment">//1: Y(psi) (arithmetic collapse)</span></div>
<div class="line"><a name="l00026"></a><span class="lineno"> 26</span>  <span class="comment">//2: Y2( psi ) (double implications are single implications)</span></div>
<div class="line"><a name="l00027"></a><span class="lineno"> 27</span>  <span class="comment">//3: clause( Y2( psi ) )</span></div>
<div class="line"><a name="l00028"></a><span class="lineno"><a class="code" href="classTReturn.html#a698d236c454a4d9ebe3c461d38d9dab0"> 28</a></span>  <span class="keywordtype">int</span> <a class="code" href="classTReturn.html#a698d236c454a4d9ebe3c461d38d9dab0">d_provesY</a>;</div>
<div class="line"><a name="l00029"></a><span class="lineno"><a class="code" href="classTReturn.html#aa05c68c3ad6926cb6bd48335092c9c4e"> 29</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classTReturn.html#aa05c68c3ad6926cb6bd48335092c9c4e">lcalced</a>;</div>
<div class="line"><a name="l00030"></a><span class="lineno"> 30</span> <span class="keyword">public</span>:</div>
<div class="line"><a name="l00031"></a><span class="lineno"> 31</span>  <a class="code" href="classTReturn.html#a9554576fa26fd8e19942ff4a2f566bbf">TReturn</a>(<a class="code" href="classLFSCProof.html">LFSCProof</a>* lfsc_pf, std::vector<int>& L, std::vector<int>& Lused, <a class="code" href="classCVC3_1_1Rational.html">Rational</a> r, <span class="keywordtype">bool</span> hasR, <span class="keywordtype">int</span> pvY);</div>
<div class="line"><a name="l00032"></a><span class="lineno"> 32</span> </div>
<div class="line"><a name="l00033"></a><span class="lineno"> 33</span>  <a class="code" href="classCVC3_1_1Rational.html">Rational</a> <a class="code" href="classTReturn.html#ac7a0e50d750845a8cfd72bc9faf4949d">mult_rational</a>( <a class="code" href="classTReturn.html">TReturn</a>* lhs );</div>
<div class="line"><a name="l00034"></a><span class="lineno"> 34</span>  <span class="keywordtype">void</span> <a class="code" href="classTReturn.html#ab5fe603ed277f47bdc014df335f33a44">getL</a>( std::vector< int >& lget, std::vector< int >& lgetu );</div>
<div class="line"><a name="l00035"></a><span class="lineno"><a class="code" href="classTReturn.html#abae84e878863b3a6978d7dde0d52522a"> 35</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classTReturn.html#abae84e878863b3a6978d7dde0d52522a">hasRational</a>() { <span class="keywordflow">return</span> <a class="code" href="classTReturn.html#a3aeca59a077b015fe579ad447ac94e29">d_hasRt</a>; }</div>
<div class="line"><a name="l00036"></a><span class="lineno"><a class="code" href="classTReturn.html#afc199e16f310243abfdf0f08f248401b"> 36</a></span>  <a class="code" href="classCVC3_1_1Rational.html">Rational</a> <a class="code" href="classTReturn.html#afc199e16f310243abfdf0f08f248401b">getRational</a>() { <span class="keywordflow">return</span> <a class="code" href="classTReturn.html#a2306f247630ba7d133db2e63651a584a">d_c</a>; }</div>
<div class="line"><a name="l00037"></a><span class="lineno"><a class="code" href="classTReturn.html#a75ec103851040bcd454dde054227a3c2"> 37</a></span>  <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classTReturn.html#a75ec103851040bcd454dde054227a3c2">getLFSCProof</a>(){ <span class="keywordflow">return</span> <a class="code" href="classTReturn.html#a934ee85a303379f5c699b88be35224ad">d_lfsc_pf</a>.<a class="code" href="classRefPtr.html#a2b987fbb75b20a1da1bd959325635e7e">get</a>(); }</div>
<div class="line"><a name="l00038"></a><span class="lineno"><a class="code" href="classTReturn.html#adfcacf33921f81fe720ef5b30b184153"> 38</a></span>  <span class="keywordtype">int</span> <a class="code" href="classTReturn.html#adfcacf33921f81fe720ef5b30b184153">getProvesY</a>() { <span class="keywordflow">return</span> <a class="code" href="classTReturn.html#a698d236c454a4d9ebe3c461d38d9dab0">d_provesY</a>; }</div>
<div class="line"><a name="l00039"></a><span class="lineno"><a class="code" href="classTReturn.html#a072febb7e4c799752ddc9c0c04eef157"> 39</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classTReturn.html#a072febb7e4c799752ddc9c0c04eef157">hasFv</a>() { <span class="keywordflow">return</span> !<a class="code" href="classTReturn.html#ab2e40626799f04887f80159b0d74521a">d_L_used</a>.empty(); }</div>
<div class="line"><a name="l00040"></a><span class="lineno"> 40</span> <span class="preprocessor">#ifdef OPTIMIZE</span></div>
<div class="line"><a name="l00041"></a><span class="lineno"> 41</span> <span class="preprocessor"></span> <span class="keywordtype">void</span> calcL( std::vector< int >& lget, std::vector< int >& lgetu );</div>
<div class="line"><a name="l00042"></a><span class="lineno"> 42</span> <span class="preprocessor">#endif</span></div>
<div class="line"><a name="l00043"></a><span class="lineno"> 43</span> <span class="preprocessor"></span></div>
<div class="line"><a name="l00044"></a><span class="lineno"> 44</span>  <span class="comment">// make it so that the two TReturns agree on what they are proving</span></div>
<div class="line"><a name="l00045"></a><span class="lineno"> 45</span>  <span class="comment">// t1 corresponds to the conversion of pf1, proving psi, Y( ps1 ), or Y2( ps1 )</span></div>
<div class="line"><a name="l00046"></a><span class="lineno"> 46</span>  <span class="comment">// t2 corresponds to the conversion of pf2, proving psi, Y( ps1 ), or Y2( ps1 )</span></div>
<div class="line"><a name="l00047"></a><span class="lineno"> 47</span>  <span class="comment">// on return, t1->d_proveY should equal t2->d_proveY</span></div>
<div class="line"><a name="l00048"></a><span class="lineno"> 48</span>  <span class="comment">// this will return the mode they normalized on, -1 means fail</span></div>
<div class="line"><a name="l00049"></a><span class="lineno"> 49</span>  <span class="keyword">static</span> <span class="keywordtype">int</span> <a class="code" href="classTReturn.html#adf5d458ca36004015a91b8be7dbd341b">normalize_tret</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& pf1, <a class="code" href="classTReturn.html">TReturn</a>*& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& pf2, <a class="code" href="classTReturn.html">TReturn</a>*& t2, <span class="keywordtype">bool</span> rev_pol = <span class="keyword">false</span> );</div>
<div class="line"><a name="l00050"></a><span class="lineno"> 50</span>  <span class="comment">//normalize TReturn to prove a certain type</span></div>
<div class="line"><a name="l00051"></a><span class="lineno"> 51</span>  <span class="comment">// this will return the mode it normalized on, -1 means fail</span></div>
<div class="line"><a name="l00052"></a><span class="lineno"> 52</span>  <span class="keyword">static</span> <span class="keywordtype">int</span> <a class="code" href="classTReturn.html#a76fa4cdab1d66c56bc96d3630150f030">normalize_tr</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& pf1, <a class="code" href="classTReturn.html">TReturn</a>*& t1, <span class="keywordtype">int</span> y, <span class="keywordtype">bool</span> rev_pol = <span class="keyword">false</span>, <span class="keywordtype">bool</span> printErr = <span class="keyword">true</span> );</div>
<div class="line"><a name="l00053"></a><span class="lineno"> 53</span>  <span class="comment">//normalize from polynomial formula to term formula atom</span></div>
<div class="line"><a name="l00054"></a><span class="lineno"> 54</span>  <span class="keyword">static</span> <span class="keywordtype">void</span> <a class="code" href="classTReturn.html#a4cb0fc0f38683bd372e4111771c273ef">normalize_to_tf</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& pf, <a class="code" href="classTReturn.html">TReturn</a>*& t1, <span class="keywordtype">int</span> y );</div>
<div class="line"><a name="l00055"></a><span class="lineno"> 55</span> };</div>
<div class="line"><a name="l00056"></a><span class="lineno"> 56</span> </div>
<div class="line"><a name="l00057"></a><span class="lineno"> 57</span> <span class="preprocessor">#endif</span></div>
</div><!-- fragment --></div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:16 for CVC3 by  <a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/>
</a> 1.8.2
</small></address>
</body>
</html>
