<!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: LFSCUtilProof.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">LFSCUtilProof.h</div> </div>
</div><!--header-->
<div class="contents">
<a href="LFSCUtilProof_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 LFSC_UTIL_PROOF_H_</span></div>
<div class="line"><a name="l00002"></a><span class="lineno"> 2</span> <span class="preprocessor"></span><span class="preprocessor">#define LFSC_UTIL_PROOF_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> </div>
<div class="line"><a name="l00006"></a><span class="lineno"><a class="code" href="classLFSCProofExpr.html"> 6</a></span> <span class="keyword">class </span><a class="code" href="classLFSCProofExpr.html">LFSCProofExpr</a> : <span class="keyword">public</span> <a class="code" href="classLFSCProof.html">LFSCProof</a></div>
<div class="line"><a name="l00007"></a><span class="lineno"> 7</span> {</div>
<div class="line"><a name="l00008"></a><span class="lineno"><a class="code" href="classLFSCProofExpr.html#a106f3177a0ffd00ba0020e29386ce7a1"> 8</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classLFSCProofExpr.html#a106f3177a0ffd00ba0020e29386ce7a1">isHole</a>;</div>
<div class="line"><a name="l00009"></a><span class="lineno"><a class="code" href="classLFSCProofExpr.html#a4e869144eebfc398c8cc1fd0a9c16e87"> 9</a></span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCProofExpr.html#a4e869144eebfc398c8cc1fd0a9c16e87">d_e</a>;</div>
<div class="line"><a name="l00010"></a><span class="lineno"> 10</span>  <a class="code" href="classLFSCProofExpr.html#aaabf771a0fe49f267541505964a0e146">LFSCProofExpr</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <span class="keywordtype">bool</span> isH = <span class="keyword">false</span> );</div>
<div class="line"><a name="l00011"></a><span class="lineno"> 11</span>  <span class="keywordtype">void</span> <a class="code" href="classLFSCProofExpr.html#a0193ac878cd5eaafdedc1d4ee669d73c">initialize</a>();</div>
<div class="line"><a name="l00012"></a><span class="lineno"><a class="code" href="classLFSCProofExpr.html#a6a432651f947000fef20ee0f955301c8"> 12</a></span>  <span class="keyword">virtual</span> <a class="code" href="classLFSCProofExpr.html#a6a432651f947000fef20ee0f955301c8">~LFSCProofExpr</a>(){}</div>
<div class="line"><a name="l00013"></a><span class="lineno"><a class="code" href="classLFSCProofExpr.html#a6c3db39b65904445c0dfc727cbba3996"> 13</a></span>  <span class="keywordtype">long</span> <span class="keywordtype">int</span> <a class="code" href="classLFSCProofExpr.html#a6c3db39b65904445c0dfc727cbba3996">get_length</a>() { <span class="keywordflow">return</span> 10; }</div>
<div class="line"><a name="l00014"></a><span class="lineno"> 14</span> <span class="keyword">public</span>:</div>
<div class="line"><a name="l00015"></a><span class="lineno"><a class="code" href="classLFSCProofExpr.html#a0e718fc15fa1ab162fb38489a2c2c579"> 15</a></span>  <span class="keyword">virtual</span> <a class="code" href="classLFSCProofExpr.html">LFSCProofExpr</a>* <a class="code" href="classLFSCProofExpr.html#a0e718fc15fa1ab162fb38489a2c2c579">AsLFSCProofExpr</a>(){ <span class="keywordflow">return</span> <span class="keyword">this</span>; }</div>
<div class="line"><a name="l00016"></a><span class="lineno"> 16</span>  <span class="keywordtype">void</span> <a class="code" href="classLFSCProofExpr.html#af732b18f23d3bb237583048f52dc60c1">print_pf</a>( std::ostream& s, <span class="keywordtype">int</span> ind );</div>
<div class="line"><a name="l00017"></a><span class="lineno"><a class="code" href="classLFSCProofExpr.html#a5889c9d07ff4346fe7cd9533a236839a"> 17</a></span>  <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCProofExpr.html#a5889c9d07ff4346fe7cd9533a236839a">Make</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <span class="keywordtype">bool</span> isH = <span class="keyword">false</span> ) { <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classLFSCProofExpr.html#aaabf771a0fe49f267541505964a0e146">LFSCProofExpr</a>( e, isH ); }</div>
<div class="line"><a name="l00018"></a><span class="lineno"><a class="code" href="classLFSCProofExpr.html#a6cc953e364c97a359d09c63fe08be7be"> 18</a></span>  <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCProofExpr.html#a6cc953e364c97a359d09c63fe08be7be">clone</a>() { <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classLFSCProofExpr.html#aaabf771a0fe49f267541505964a0e146">LFSCProofExpr</a>( <a class="code" href="classLFSCProofExpr.html#a4e869144eebfc398c8cc1fd0a9c16e87">d_e</a>, <a class="code" href="classLFSCProofExpr.html#a106f3177a0ffd00ba0020e29386ce7a1">isHole</a> ); }</div>
<div class="line"><a name="l00019"></a><span class="lineno"> 19</span> </div>
<div class="line"><a name="l00020"></a><span class="lineno"><a class="code" href="classLFSCProofExpr.html#aac86e160f1dc7ac8b8c6cf90e22ebfee"> 20</a></span>  <span class="keywordtype">void</span> <a class="code" href="classLFSCProofExpr.html#aac86e160f1dc7ac8b8c6cf90e22ebfee">fillHoles</a>() { <a class="code" href="classLFSCProofExpr.html#a106f3177a0ffd00ba0020e29386ce7a1">isHole</a> = <span class="keyword">false</span>; }</div>
<div class="line"><a name="l00021"></a><span class="lineno"> 21</span> };</div>
<div class="line"><a name="l00022"></a><span class="lineno"> 22</span> </div>
<div class="line"><a name="l00023"></a><span class="lineno"><a class="code" href="classLFSCPfVar.html"> 23</a></span> <span class="keyword">class </span><a class="code" href="classLFSCPfVar.html">LFSCPfVar</a> : <span class="keyword">public</span> <a class="code" href="classLFSCProof.html">LFSCProof</a> {</div>
<div class="line"><a name="l00024"></a><span class="lineno"> 24</span> <span class="keyword">private</span>:</div>
<div class="line"><a name="l00025"></a><span class="lineno"><a class="code" href="classLFSCPfVar.html#af190aa354850d11f2f183a46401fe685"> 25</a></span>  <span class="keyword">static</span> std::map< int, RefPtr< LFSCProof > > <a class="code" href="classLFSCPfVar.html#af190aa354850d11f2f183a46401fe685">vMap</a>;</div>
<div class="line"><a name="l00026"></a><span class="lineno"><a class="code" href="classLFSCPfVar.html#a04fb4e87bdae6825800546d84b5368dd"> 26</a></span>  <span class="keywordtype">string</span> <a class="code" href="classLFSCPfVar.html#a04fb4e87bdae6825800546d84b5368dd">name</a>;</div>
<div class="line"><a name="l00027"></a><span class="lineno"><a class="code" href="classLFSCPfVar.html#a91a2fc1851dd341464eca5811e0b9775"> 27</a></span>  <a class="code" href="classLFSCPfVar.html#a91a2fc1851dd341464eca5811e0b9775">LFSCPfVar</a>( <span class="keywordtype">string</span> nm ) : <a class="code" href="classLFSCProof.html">LFSCProof</a>(), <a class="code" href="classLFSCPfVar.html#a04fb4e87bdae6825800546d84b5368dd">name</a>( nm ){}</div>
<div class="line"><a name="l00028"></a><span class="lineno"><a class="code" href="classLFSCPfVar.html#aaea0a9b256a1c9080968c2306e8c35b9"> 28</a></span>  <span class="keyword">virtual</span> <a class="code" href="classLFSCPfVar.html#aaea0a9b256a1c9080968c2306e8c35b9">~LFSCPfVar</a>(){}</div>
<div class="line"><a name="l00029"></a><span class="lineno"><a class="code" href="classLFSCPfVar.html#afbdfac3e19586ccbf29321b2a08feddc"> 29</a></span>  <span class="keywordtype">long</span> <span class="keywordtype">int</span> <a class="code" href="classLFSCPfVar.html#afbdfac3e19586ccbf29321b2a08feddc">get_length</a>() { <span class="keywordflow">return</span> <a class="code" href="classLFSCPfVar.html#a04fb4e87bdae6825800546d84b5368dd">name</a>.length(); }</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"><a class="code" href="classLFSCPfVar.html#a5b6e5edc54a507a7c695ffa2999671b0"> 31</a></span>  <span class="keyword">virtual</span> <a class="code" href="classLFSCPfVar.html">LFSCPfVar</a>* <a class="code" href="classLFSCPfVar.html#a5b6e5edc54a507a7c695ffa2999671b0">AsLFSCPfVar</a>(){ <span class="keywordflow">return</span> <span class="keyword">this</span>; }</div>
<div class="line"><a name="l00032"></a><span class="lineno"><a class="code" href="classLFSCPfVar.html#a0b69489a9e1546ba6741de5b5400c8e9"> 32</a></span>  <span class="keywordtype">void</span> <a class="code" href="classLFSCPfVar.html#a0b69489a9e1546ba6741de5b5400c8e9">print_pf</a>( std::ostream& s, <span class="keywordtype">int</span> ind = 0 ){ s << <a class="code" href="classLFSCPfVar.html#a04fb4e87bdae6825800546d84b5368dd">name</a>; }</div>
<div class="line"><a name="l00033"></a><span class="lineno"><a class="code" href="classLFSCPfVar.html#aca4bf1d3cd471df00f7354797553be35"> 33</a></span>  <span class="keywordtype">void</span> <a class="code" href="classLFSCPfVar.html#aca4bf1d3cd471df00f7354797553be35">print_struct</a>( std::ostream& s, <span class="keywordtype">int</span> ind = 0 ){ s << <a class="code" href="classLFSCPfVar.html#a04fb4e87bdae6825800546d84b5368dd">name</a>; }</div>
<div class="line"><a name="l00034"></a><span class="lineno"> 34</span>  <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCPfVar.html#ac7b68737c0763fbc46619c54bd1df148">Make</a>( <span class="keyword">const</span> <span class="keywordtype">char</span>* c, <span class="keywordtype">int</span> v );</div>
<div class="line"><a name="l00035"></a><span class="lineno"> 35</span>  <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCPfVar.html#a0d9785d85b1d55610f43d6f0ba3de955">MakeV</a>( <span class="keywordtype">int</span> v );</div>
<div class="line"><a name="l00036"></a><span class="lineno"><a class="code" href="classLFSCPfVar.html#a6156af7863569dca0abed952fa938978"> 36</a></span>  <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCPfVar.html#a6156af7863569dca0abed952fa938978">clone</a>() { <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classLFSCPfVar.html#a91a2fc1851dd341464eca5811e0b9775">LFSCPfVar</a>( <a class="code" href="classLFSCPfVar.html#a04fb4e87bdae6825800546d84b5368dd">name</a> ); }</div>
<div class="line"><a name="l00037"></a><span class="lineno"> 37</span> };</div>
<div class="line"><a name="l00038"></a><span class="lineno"> 38</span> </div>
<div class="line"><a name="l00039"></a><span class="lineno"><a class="code" href="classLFSCPfLambda.html"> 39</a></span> <span class="keyword">class </span><a class="code" href="classLFSCPfLambda.html">LFSCPfLambda</a> : <span class="keyword">public</span> <a class="code" href="classLFSCProof.html">LFSCProof</a> {</div>
<div class="line"><a name="l00040"></a><span class="lineno"> 40</span> <span class="keyword">private</span>:</div>
<div class="line"><a name="l00041"></a><span class="lineno"><a class="code" href="classLFSCPfLambda.html#a96501c8c824e1fac2840f20deb1d7863"> 41</a></span>  <a class="code" href="classRefPtr.html">RefPtr< LFSCPfVar ></a> <a class="code" href="classLFSCPfLambda.html#a96501c8c824e1fac2840f20deb1d7863">pfV</a>;</div>
<div class="line"><a name="l00042"></a><span class="lineno"><a class="code" href="classLFSCPfLambda.html#adf3639aa319befe98b862f5456732606"> 42</a></span>  <a class="code" href="classRefPtr.html">RefPtr< LFSCProof ></a> <a class="code" href="classLFSCPfLambda.html#adf3639aa319befe98b862f5456732606">body</a>;</div>
<div class="line"><a name="l00043"></a><span class="lineno"> 43</span>  <span class="comment">//just a placeholder. This is what the lambda abstracts.</span></div>
<div class="line"><a name="l00044"></a><span class="lineno"><a class="code" href="classLFSCPfLambda.html#a0c5823bc758214d9fbb3cfb942cc8ac6"> 44</a></span>  <a class="code" href="classRefPtr.html">RefPtr< LFSCProof ></a> <a class="code" href="classLFSCPfLambda.html#a0c5823bc758214d9fbb3cfb942cc8ac6">abstVal</a>;</div>
<div class="line"><a name="l00045"></a><span class="lineno"> 45</span>  <span class="comment">//constructor</span></div>
<div class="line"><a name="l00046"></a><span class="lineno"><a class="code" href="classLFSCPfLambda.html#a0020ea0939d16f4bf36ce64627996976"> 46</a></span>  <a class="code" href="classLFSCPfLambda.html#a0020ea0939d16f4bf36ce64627996976">LFSCPfLambda</a>( <a class="code" href="classLFSCPfVar.html">LFSCPfVar</a>* v, <a class="code" href="classLFSCProof.html">LFSCProof</a>* bd, <a class="code" href="classLFSCProof.html">LFSCProof</a>* aVal = NULL ) : <a class="code" href="classLFSCProof.html">LFSCProof</a>(),</div>
<div class="line"><a name="l00047"></a><span class="lineno"> 47</span>  <a class="code" href="classLFSCPfLambda.html#a96501c8c824e1fac2840f20deb1d7863">pfV</a>( v ), <a class="code" href="classLFSCPfLambda.html#adf3639aa319befe98b862f5456732606">body</a>( bd ), <a class="code" href="classLFSCPfLambda.html#a0c5823bc758214d9fbb3cfb942cc8ac6">abstVal</a>( aVal ){}</div>
<div class="line"><a name="l00048"></a><span class="lineno"><a class="code" href="classLFSCPfLambda.html#a70761805bf4943d2de917ca7d0ff2466"> 48</a></span>  <span class="keyword">virtual</span> <a class="code" href="classLFSCPfLambda.html#a70761805bf4943d2de917ca7d0ff2466">~LFSCPfLambda</a>(){}</div>
<div class="line"><a name="l00049"></a><span class="lineno"><a class="code" href="classLFSCPfLambda.html#aacda4aaa9a0c51ee7bcf59559d77db1d"> 49</a></span>  <span class="keywordtype">long</span> <span class="keywordtype">int</span> <a class="code" href="classLFSCPfLambda.html#aacda4aaa9a0c51ee7bcf59559d77db1d">get_length</a>() { <span class="keywordflow">return</span> 5 + <a class="code" href="classLFSCPfLambda.html#a96501c8c824e1fac2840f20deb1d7863">pfV</a>-><a class="code" href="classLFSCProof.html#a784c4a1295785719bce419d3e9ee9be1">get_string_length</a>() + <a class="code" href="classLFSCPfLambda.html#adf3639aa319befe98b862f5456732606">body</a>-><a class="code" href="classLFSCProof.html#a784c4a1295785719bce419d3e9ee9be1">get_string_length</a>(); }</div>
<div class="line"><a name="l00050"></a><span class="lineno"> 50</span> <span class="keyword">public</span>:</div>
<div class="line"><a name="l00051"></a><span class="lineno"><a class="code" href="classLFSCPfLambda.html#a2dac1e9539015c086c3a6e9df2fa948e"> 51</a></span>  <span class="keyword">virtual</span> <a class="code" href="classLFSCPfLambda.html">LFSCPfLambda</a>* <a class="code" href="classLFSCPfLambda.html#a2dac1e9539015c086c3a6e9df2fa948e">AsLFSCPfLambda</a>(){ <span class="keywordflow">return</span> <span class="keyword">this</span>; }</div>
<div class="line"><a name="l00052"></a><span class="lineno"> 52</span>  <span class="keywordtype">void</span> <a class="code" href="classLFSCPfLambda.html#af3b36357fab483afc642f4c77bd4a497">print_pf</a>( std::ostream& s, <span class="keywordtype">int</span> ind = 0 );</div>
<div class="line"><a name="l00053"></a><span class="lineno"><a class="code" href="classLFSCPfLambda.html#abcb32823122bdb0558104cceeed81490"> 53</a></span>  <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCPfLambda.html#abcb32823122bdb0558104cceeed81490">Make</a>( <a class="code" href="classLFSCPfVar.html">LFSCPfVar</a>* v, <a class="code" href="classLFSCProof.html">LFSCProof</a>* bd, <a class="code" href="classLFSCProof.html">LFSCProof</a>* aVal = NULL ){</div>
<div class="line"><a name="l00054"></a><span class="lineno"> 54</span>  <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classLFSCPfLambda.html#a0020ea0939d16f4bf36ce64627996976">LFSCPfLambda</a>( v, bd, aVal );</div>
<div class="line"><a name="l00055"></a><span class="lineno"> 55</span>  }</div>
<div class="line"><a name="l00056"></a><span class="lineno"><a class="code" href="classLFSCPfLambda.html#ace06bdec9d26641fe98c7b32b582d67e"> 56</a></span>  <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCPfLambda.html#ace06bdec9d26641fe98c7b32b582d67e">clone</a>() { <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classLFSCPfLambda.html#a0020ea0939d16f4bf36ce64627996976">LFSCPfLambda</a>( <a class="code" href="classLFSCPfLambda.html#a96501c8c824e1fac2840f20deb1d7863">pfV</a>.<a class="code" href="classRefPtr.html#a2b987fbb75b20a1da1bd959325635e7e">get</a>(), <a class="code" href="classLFSCPfLambda.html#adf3639aa319befe98b862f5456732606">body</a>.<a class="code" href="classRefPtr.html#a2b987fbb75b20a1da1bd959325635e7e">get</a>(), <a class="code" href="classLFSCPfLambda.html#a0c5823bc758214d9fbb3cfb942cc8ac6">abstVal</a>.<a class="code" href="classRefPtr.html#a2b987fbb75b20a1da1bd959325635e7e">get</a>() ); }</div>
<div class="line"><a name="l00057"></a><span class="lineno"><a class="code" href="classLFSCPfLambda.html#a96fd9ae0a48dd8bb55e9e0fcde2fbe16"> 57</a></span>  <span class="keywordtype">int</span> <a class="code" href="classLFSCPfLambda.html#a96fd9ae0a48dd8bb55e9e0fcde2fbe16">getNumChildren</a>() { <span class="keywordflow">return</span> 2; }</div>
<div class="line"><a name="l00058"></a><span class="lineno"><a class="code" href="classLFSCPfLambda.html#a697280bf0655b2861c5073daa847a33e"> 58</a></span>  <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCPfLambda.html#a697280bf0655b2861c5073daa847a33e">getChild</a>( <span class="keywordtype">int</span> n ) { <span class="keywordflow">return</span> (n==0) ? (<a class="code" href="classLFSCProof.html">LFSCProof</a>*)<a class="code" href="classLFSCPfLambda.html#a96501c8c824e1fac2840f20deb1d7863">pfV</a>.<a class="code" href="classRefPtr.html#a2b987fbb75b20a1da1bd959325635e7e">get</a>() : <a class="code" href="classLFSCPfLambda.html#adf3639aa319befe98b862f5456732606">body</a>.<a class="code" href="classRefPtr.html#a2b987fbb75b20a1da1bd959325635e7e">get</a>(); }</div>
<div class="line"><a name="l00059"></a><span class="lineno"> 59</span> };</div>
<div class="line"><a name="l00060"></a><span class="lineno"> 60</span> <span class="comment">//</span></div>
<div class="line"><a name="l00061"></a><span class="lineno"><a class="code" href="classLFSCProofGeneric.html"> 61</a></span> <span class="keyword">class </span><a class="code" href="classLFSCProofGeneric.html">LFSCProofGeneric</a> : <span class="keyword">public</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>{</div>
<div class="line"><a name="l00062"></a><span class="lineno"> 62</span> <span class="keyword">private</span>:</div>
<div class="line"><a name="l00063"></a><span class="lineno"><a class="code" href="classLFSCProofGeneric.html#af785d15d167f9f5f3985caa179ca9f85"> 63</a></span>  vector< RefPtr< LFSCProof > > <a class="code" href="classLFSCProofGeneric.html#af785d15d167f9f5f3985caa179ca9f85">d_pf</a>;</div>
<div class="line"><a name="l00064"></a><span class="lineno"><a class="code" href="classLFSCProofGeneric.html#ae985971cfcdba65ec9e39472b023effe"> 64</a></span>  vector< string > <a class="code" href="classLFSCProofGeneric.html#ae985971cfcdba65ec9e39472b023effe">d_str</a>;</div>
<div class="line"><a name="l00065"></a><span class="lineno"><a class="code" href="classLFSCProofGeneric.html#ab1c9b0ca7c6984d0bf6de79761510131"> 65</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classLFSCProofGeneric.html#ab1c9b0ca7c6984d0bf6de79761510131">debug_str</a>;</div>
<div class="line"><a name="l00066"></a><span class="lineno"> 66</span>  <span class="comment">//Proof in the form "S1.print(P1).S2.print(P2).....print(Pn).S{n+1}"</span></div>
<div class="line"><a name="l00067"></a><span class="lineno"><a class="code" href="classLFSCProofGeneric.html#a45f64e0c33400e0a27191914e9e7054e"> 67</a></span>  <a class="code" href="classLFSCProofGeneric.html#a45f64e0c33400e0a27191914e9e7054e">LFSCProofGeneric</a>( vector< <a class="code" href="classRefPtr.html">RefPtr< LFSCProof ></a> >& d_pfs, vector< string >& d_strs, <span class="keywordtype">bool</span> db_str = <span class="keyword">false</span> ) : <a class="code" href="classLFSCProof.html">LFSCProof</a>(){</div>
<div class="line"><a name="l00068"></a><span class="lineno"> 68</span>  <span class="keywordflow">for</span>( <span class="keywordtype">int</span> a=0; a<(int)d_pfs.size(); a++ )</div>
<div class="line"><a name="l00069"></a><span class="lineno"> 69</span>  <a class="code" href="classLFSCProofGeneric.html#af785d15d167f9f5f3985caa179ca9f85">d_pf</a>.push_back( d_pfs[a].get() );</div>
<div class="line"><a name="l00070"></a><span class="lineno"> 70</span>  <span class="keywordflow">for</span>( <span class="keywordtype">int</span> a=0; a<(int)d_strs.size(); a++ )</div>
<div class="line"><a name="l00071"></a><span class="lineno"> 71</span>  <a class="code" href="classLFSCProofGeneric.html#ae985971cfcdba65ec9e39472b023effe">d_str</a>.push_back( d_strs[a] );</div>
<div class="line"><a name="l00072"></a><span class="lineno"> 72</span>  <a class="code" href="classLFSCProofGeneric.html#ab1c9b0ca7c6984d0bf6de79761510131">debug_str</a> = db_str;</div>
<div class="line"><a name="l00073"></a><span class="lineno"> 73</span>  }</div>
<div class="line"><a name="l00074"></a><span class="lineno"><a class="code" href="classLFSCProofGeneric.html#a356d195515529108c3c143abcf1850d8"> 74</a></span>  <span class="keyword">virtual</span> <a class="code" href="classLFSCProofGeneric.html#a356d195515529108c3c143abcf1850d8">~LFSCProofGeneric</a>(){}</div>
<div class="line"><a name="l00075"></a><span class="lineno"> 75</span>  <span class="keywordtype">long</span> <span class="keywordtype">int</span> <a class="code" href="classLFSCProofGeneric.html#a7acae5a8c672b63f1aab26c3feb9ab67">get_length</a>();</div>
<div class="line"><a name="l00076"></a><span class="lineno"> 76</span> <span class="keyword">public</span>:</div>
<div class="line"><a name="l00077"></a><span class="lineno"><a class="code" href="classLFSCProofGeneric.html#a89efd3123a97c54a31a477e75185dd63"> 77</a></span>  <span class="keyword">virtual</span> <a class="code" href="classLFSCProofGeneric.html">LFSCProofGeneric</a>* <a class="code" href="classLFSCProofGeneric.html#a89efd3123a97c54a31a477e75185dd63">AsLFSCProofGeneric</a>(){ <span class="keywordflow">return</span> <span class="keyword">this</span>; }</div>
<div class="line"><a name="l00078"></a><span class="lineno"> 78</span>  <span class="keywordtype">void</span> <a class="code" href="classLFSCProofGeneric.html#aa1bc4b22316c2bff7f852d2a4799f533">print_pf</a>( std::ostream& s, <span class="keywordtype">int</span> ind = 0 );</div>
<div class="line"><a name="l00079"></a><span class="lineno"> 79</span>  <span class="comment">//Proof in the form "S1.print(P1).S2.print(P2).....print(Pn).S{n+1}"</span></div>
<div class="line"><a name="l00080"></a><span class="lineno"><a class="code" href="classLFSCProofGeneric.html#a1bf5343c88454d1ffb552a3e2f59ddc8"> 80</a></span>  <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCProofGeneric.html#a1bf5343c88454d1ffb552a3e2f59ddc8">Make</a>( vector< <a class="code" href="classRefPtr.html">RefPtr< LFSCProof ></a> >& d_pfs, std::vector< string >& d_strs, <span class="keywordtype">bool</span> db_str = <span class="keyword">false</span> ){</div>
<div class="line"><a name="l00081"></a><span class="lineno"> 81</span>  <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classLFSCProofGeneric.html#a45f64e0c33400e0a27191914e9e7054e">LFSCProofGeneric</a>( d_pfs, d_strs, db_str );</div>
<div class="line"><a name="l00082"></a><span class="lineno"> 82</span>  }</div>
<div class="line"><a name="l00083"></a><span class="lineno"> 83</span>  <span class="comment">//proof printed in the form "S1.print(P1).S2"</span></div>
<div class="line"><a name="l00084"></a><span class="lineno"> 84</span>  <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCProofGeneric.html#a1bf5343c88454d1ffb552a3e2f59ddc8">Make</a>( <span class="keywordtype">string</span> str_pre, <a class="code" href="classLFSCProof.html">LFSCProof</a>* sub_pf, <span class="keywordtype">string</span> str_post, <span class="keywordtype">bool</span> db_str = <span class="keyword">false</span> );</div>
<div class="line"><a name="l00085"></a><span class="lineno"> 85</span>  <span class="comment">//proof printed in the form "S1.print(P1).print(P2).S2"</span></div>
<div class="line"><a name="l00086"></a><span class="lineno"> 86</span>  <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCProofGeneric.html#a1bf5343c88454d1ffb552a3e2f59ddc8">Make</a>( <span class="keywordtype">string</span> str_pre, <a class="code" href="classLFSCProof.html">LFSCProof</a>* sub_pf1, <a class="code" href="classLFSCProof.html">LFSCProof</a>* sub_pf2, <span class="keywordtype">string</span> str_post, <span class="keywordtype">bool</span> db_str = <span class="keyword">false</span> );</div>
<div class="line"><a name="l00087"></a><span class="lineno"> 87</span>  <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCProofGeneric.html#abf29b3cdedf8439a6ee65ebc137340f5">MakeStr</a>( <span class="keyword">const</span> <span class="keywordtype">char</span>* c, <span class="keywordtype">bool</span> db_str = <span class="keyword">false</span> );</div>
<div class="line"><a name="l00088"></a><span class="lineno"><a class="code" href="classLFSCProofGeneric.html#a49ff2fcc1122bbecf8fff0559ddeccad"> 88</a></span>  <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCProofGeneric.html#a49ff2fcc1122bbecf8fff0559ddeccad">MakeUnk</a>(){ <span class="keywordflow">return</span> <a class="code" href="classLFSCProofGeneric.html#abf29b3cdedf8439a6ee65ebc137340f5">MakeStr</a>( <span class="stringliteral">"unk"</span> ); }</div>
<div class="line"><a name="l00089"></a><span class="lineno"><a class="code" href="classLFSCProofGeneric.html#aec701cd210f5e2aa1734c644c0ab4c6a"> 89</a></span>  <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCProofGeneric.html#aec701cd210f5e2aa1734c644c0ab4c6a">clone</a>(){ <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classLFSCProofGeneric.html#a45f64e0c33400e0a27191914e9e7054e">LFSCProofGeneric</a>( <a class="code" href="classLFSCProofGeneric.html#af785d15d167f9f5f3985caa179ca9f85">d_pf</a>, <a class="code" href="classLFSCProofGeneric.html#ae985971cfcdba65ec9e39472b023effe">d_str</a>, <a class="code" href="classLFSCProofGeneric.html#ab1c9b0ca7c6984d0bf6de79761510131">debug_str</a> ); }</div>
<div class="line"><a name="l00090"></a><span class="lineno"><a class="code" href="classLFSCProofGeneric.html#a588df357bf41ff575e52cb7dd0d34040"> 90</a></span>  <span class="keywordtype">int</span> <a class="code" href="classLFSCProofGeneric.html#a588df357bf41ff575e52cb7dd0d34040">getNumChildren</a>() { <span class="keywordflow">return</span> (<span class="keywordtype">int</span>)<a class="code" href="classLFSCProofGeneric.html#af785d15d167f9f5f3985caa179ca9f85">d_pf</a>.size(); }</div>
<div class="line"><a name="l00091"></a><span class="lineno"><a class="code" href="classLFSCProofGeneric.html#a10ab8502f739ebccfa77b8a8436223fe"> 91</a></span>  <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCProofGeneric.html#a10ab8502f739ebccfa77b8a8436223fe">getChild</a>( <span class="keywordtype">int</span> n ) { <span class="keywordflow">return</span> <a class="code" href="classLFSCProofGeneric.html#af785d15d167f9f5f3985caa179ca9f85">d_pf</a>[n].get(); }</div>
<div class="line"><a name="l00092"></a><span class="lineno"> 92</span> };</div>
<div class="line"><a name="l00093"></a><span class="lineno"> 93</span> </div>
<div class="line"><a name="l00094"></a><span class="lineno"> 94</span> </div>
<div class="line"><a name="l00095"></a><span class="lineno"><a class="code" href="classLFSCPfLet.html"> 95</a></span> <span class="keyword">class </span><a class="code" href="classLFSCPfLet.html">LFSCPfLet</a> : <span class="keyword">public</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>{</div>
<div class="line"><a name="l00096"></a><span class="lineno"> 96</span> <span class="keyword">private</span>:</div>
<div class="line"><a name="l00097"></a><span class="lineno"><a class="code" href="classLFSCPfLet.html#a01244b4de08d6beaf09a0fc7c5263a65"> 97</a></span>  <a class="code" href="classRefPtr.html">RefPtr< LFSCProof ></a> <a class="code" href="classLFSCPfLet.html#a01244b4de08d6beaf09a0fc7c5263a65">d_letPf</a>;</div>
<div class="line"><a name="l00098"></a><span class="lineno"><a class="code" href="classLFSCPfLet.html#a256986dda0a58de4e8aed2a5e582ed67"> 98</a></span>  <a class="code" href="classRefPtr.html">RefPtr< LFSCPfVar ></a> <a class="code" href="classLFSCPfLet.html#a256986dda0a58de4e8aed2a5e582ed67">d_pv</a>;</div>
<div class="line"><a name="l00099"></a><span class="lineno"><a class="code" href="classLFSCPfLet.html#acc201153269f577e4f90827e0804f5f3"> 99</a></span>  <a class="code" href="classRefPtr.html">RefPtr< LFSCProof ></a> <a class="code" href="classLFSCPfLet.html#acc201153269f577e4f90827e0804f5f3">d_body</a>;</div>
<div class="line"><a name="l00100"></a><span class="lineno"> 100</span>  <span class="comment">//this should be equal to d_letPf, although it could be something else based on fv</span></div>
<div class="line"><a name="l00101"></a><span class="lineno"><a class="code" href="classLFSCPfLet.html#abb7a9123dbd3efff87166fcf3642815f"> 101</a></span>  <a class="code" href="classRefPtr.html">RefPtr< LFSCProof ></a> <a class="code" href="classLFSCPfLet.html#abb7a9123dbd3efff87166fcf3642815f">d_letPfRpl</a>;</div>
<div class="line"><a name="l00102"></a><span class="lineno"> 102</span>  <span class="comment">//this by default is d_pv, although it could be something else based on fv</span></div>
<div class="line"><a name="l00103"></a><span class="lineno"><a class="code" href="classLFSCPfLet.html#af289f9e13c553b1115a4f6fcd56b4423"> 103</a></span>  <a class="code" href="classRefPtr.html">RefPtr< LFSCProof ></a> <a class="code" href="classLFSCPfLet.html#af289f9e13c553b1115a4f6fcd56b4423">d_pvRpl</a>;</div>
<div class="line"><a name="l00104"></a><span class="lineno"><a class="code" href="classLFSCPfLet.html#ad52e42e731d1a53a5acbf84f852879ac"> 104</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classLFSCPfLet.html#ad52e42e731d1a53a5acbf84f852879ac">d_isTh</a>;</div>
<div class="line"><a name="l00105"></a><span class="lineno"><a class="code" href="classLFSCPfLet.html#acfc17527ee09a3f10203af05cd972a4a"> 105</a></span>  <a class="code" href="classLFSCPfLet.html#acfc17527ee09a3f10203af05cd972a4a">LFSCPfLet</a>( <a class="code" href="classLFSCProof.html">LFSCProof</a>* letPf, <a class="code" href="classLFSCPfVar.html">LFSCPfVar</a>* pv, <a class="code" href="classLFSCProof.html">LFSCProof</a>* body,</div>
<div class="line"><a name="l00106"></a><span class="lineno"> 106</span>  <span class="keywordtype">bool</span> isTh, <a class="code" href="classLFSCProof.html">LFSCProof</a>* letPfRpl, <a class="code" href="classLFSCProof.html">LFSCProof</a>* pvRpl ) : <a class="code" href="classLFSCProof.html">LFSCProof</a>(),</div>
<div class="line"><a name="l00107"></a><span class="lineno"> 107</span>  <a class="code" href="classLFSCPfLet.html#a01244b4de08d6beaf09a0fc7c5263a65">d_letPf</a>( letPf ),<a class="code" href="classLFSCPfLet.html#a256986dda0a58de4e8aed2a5e582ed67">d_pv</a>( pv ),<a class="code" href="classLFSCPfLet.html#acc201153269f577e4f90827e0804f5f3">d_body</a>( body ),<a class="code" href="classLFSCPfLet.html#abb7a9123dbd3efff87166fcf3642815f">d_letPfRpl</a>( letPfRpl ),<a class="code" href="classLFSCPfLet.html#af289f9e13c553b1115a4f6fcd56b4423">d_pvRpl</a>( pvRpl ),<a class="code" href="classLFSCPfLet.html#ad52e42e731d1a53a5acbf84f852879ac">d_isTh</a>( isTh ){}</div>
<div class="line"><a name="l00108"></a><span class="lineno"> 108</span>  <a class="code" href="classLFSCPfLet.html#acfc17527ee09a3f10203af05cd972a4a">LFSCPfLet</a>( <a class="code" href="classLFSCProof.html">LFSCProof</a>* letPf, <a class="code" href="classLFSCPfVar.html">LFSCPfVar</a>* pv, <a class="code" href="classLFSCProof.html">LFSCProof</a>* body,</div>
<div class="line"><a name="l00109"></a><span class="lineno"> 109</span>  <span class="keywordtype">bool</span> isTh, std::vector< int >& fv );</div>
<div class="line"><a name="l00110"></a><span class="lineno"><a class="code" href="classLFSCPfLet.html#ad31eff106a2d0c78172390d755d625e2"> 110</a></span>  <span class="keyword">virtual</span> <a class="code" href="classLFSCPfLet.html#ad31eff106a2d0c78172390d755d625e2">~LFSCPfLet</a>(){}</div>
<div class="line"><a name="l00111"></a><span class="lineno"><a class="code" href="classLFSCPfLet.html#a49cb76df6e4fbb2f13a21e9c626efc45"> 111</a></span>  <span class="keywordtype">long</span> <span class="keywordtype">int</span> <a class="code" href="classLFSCPfLet.html#a49cb76df6e4fbb2f13a21e9c626efc45">get_length</a>() {</div>
<div class="line"><a name="l00112"></a><span class="lineno"> 112</span>  <span class="keywordflow">return</span> 10 + <a class="code" href="classLFSCPfLet.html#a01244b4de08d6beaf09a0fc7c5263a65">d_letPf</a>-><a class="code" href="classLFSCProof.html#a784c4a1295785719bce419d3e9ee9be1">get_string_length</a>() + <a class="code" href="classLFSCPfLet.html#a256986dda0a58de4e8aed2a5e582ed67">d_pv</a>-><a class="code" href="classLFSCProof.html#a784c4a1295785719bce419d3e9ee9be1">get_string_length</a>() + <a class="code" href="classLFSCPfLet.html#acc201153269f577e4f90827e0804f5f3">d_body</a>-><a class="code" href="classLFSCProof.html#a784c4a1295785719bce419d3e9ee9be1">get_string_length</a>();</div>
<div class="line"><a name="l00113"></a><span class="lineno"> 113</span>  }</div>
<div class="line"><a name="l00114"></a><span class="lineno"> 114</span> <span class="keyword">public</span>:</div>
<div class="line"><a name="l00115"></a><span class="lineno"><a class="code" href="classLFSCPfLet.html#a554bd849b6be3e87301664a78af548c2"> 115</a></span>  <span class="keyword">virtual</span> <a class="code" href="classLFSCPfLet.html">LFSCPfLet</a>* <a class="code" href="classLFSCPfLet.html#a554bd849b6be3e87301664a78af548c2">AsLFSCPfLet</a>(){ <span class="keywordflow">return</span> <span class="keyword">this</span>; }</div>
<div class="line"><a name="l00116"></a><span class="lineno"> 116</span>  <span class="keywordtype">void</span> <a class="code" href="classLFSCPfLet.html#aaadb919e3b6b04b3acd02d984011b088">print_pf</a>( std::ostream& s, <span class="keywordtype">int</span> ind = 0 );</div>
<div class="line"><a name="l00117"></a><span class="lineno"> 117</span>  <span class="keywordtype">void</span> <a class="code" href="classLFSCPfLet.html#a71496a1b0012750fec8ab33ea1998f7a">print_struct</a>( std::ostream& s, <span class="keywordtype">int</span> ind = 0 );</div>
<div class="line"><a name="l00118"></a><span class="lineno"><a class="code" href="classLFSCPfLet.html#a8a9295947ba6381d158f39b570fcebaf"> 118</a></span>  <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCPfLet.html#a8a9295947ba6381d158f39b570fcebaf">Make</a>( <a class="code" href="classLFSCProof.html">LFSCProof</a>* letPf, <a class="code" href="classLFSCPfVar.html">LFSCPfVar</a>* pv, <a class="code" href="classLFSCProof.html">LFSCProof</a>* body,</div>
<div class="line"><a name="l00119"></a><span class="lineno"> 119</span>  <span class="keywordtype">bool</span> isTh, std::vector< int >& fv ){</div>
<div class="line"><a name="l00120"></a><span class="lineno"> 120</span>  <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classLFSCPfLet.html#acfc17527ee09a3f10203af05cd972a4a">LFSCPfLet</a>( letPf, pv, body, isTh, fv );</div>
<div class="line"><a name="l00121"></a><span class="lineno"> 121</span>  }</div>
<div class="line"><a name="l00122"></a><span class="lineno"><a class="code" href="classLFSCPfLet.html#ab436db06a158bf463c0614f34608cfaf"> 122</a></span>  <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCPfLet.html#ab436db06a158bf463c0614f34608cfaf">clone</a>() { <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classLFSCPfLet.html#acfc17527ee09a3f10203af05cd972a4a">LFSCPfLet</a>( <a class="code" href="classLFSCPfLet.html#a01244b4de08d6beaf09a0fc7c5263a65">d_letPf</a>.<a class="code" href="classRefPtr.html#a2b987fbb75b20a1da1bd959325635e7e">get</a>(), <a class="code" href="classLFSCPfLet.html#a256986dda0a58de4e8aed2a5e582ed67">d_pv</a>.<a class="code" href="classRefPtr.html#a2b987fbb75b20a1da1bd959325635e7e">get</a>(), <a class="code" href="classLFSCPfLet.html#acc201153269f577e4f90827e0804f5f3">d_body</a>.<a class="code" href="classRefPtr.html#a2b987fbb75b20a1da1bd959325635e7e">get</a>(),</div>
<div class="line"><a name="l00123"></a><span class="lineno"> 123</span>  <a class="code" href="classLFSCPfLet.html#ad52e42e731d1a53a5acbf84f852879ac">d_isTh</a>, <a class="code" href="classLFSCPfLet.html#abb7a9123dbd3efff87166fcf3642815f">d_letPfRpl</a>.<a class="code" href="classRefPtr.html#a2b987fbb75b20a1da1bd959325635e7e">get</a>(), <a class="code" href="classLFSCPfLet.html#af289f9e13c553b1115a4f6fcd56b4423">d_pvRpl</a>.<a class="code" href="classRefPtr.html#a2b987fbb75b20a1da1bd959325635e7e">get</a>() ); }</div>
<div class="line"><a name="l00124"></a><span class="lineno"> 124</span>  <span class="comment">//should not be part of the children structure.</span></div>
<div class="line"><a name="l00125"></a><span class="lineno"> 125</span> };</div>
<div class="line"><a name="l00126"></a><span class="lineno"> 126</span> </div>
<div class="line"><a name="l00127"></a><span class="lineno"> 127</span> </div>
<div class="line"><a name="l00128"></a><span class="lineno"> 128</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:14 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>
