<!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: LFSCUtilProof.h Source File</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><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 class="header">
<div class="headertitle">
<div class="title">LFSCUtilProof.h</div> </div>
</div>
<div class="contents">
<a href="LFSCUtilProof_8h.html">Go to the documentation of this file.</a><div class="fragment"><pre class="fragment"><a name="l00001"></a>00001 <span class="preprocessor">#ifndef LFSC_UTIL_PROOF_H_</span>
<a name="l00002"></a>00002 <span class="preprocessor"></span><span class="preprocessor">#define LFSC_UTIL_PROOF_H_</span>
<a name="l00003"></a>00003 <span class="preprocessor"></span>
<a name="l00004"></a>00004 <span class="preprocessor">#include "<a class="code" href="LFSCProof_8h.html">LFSCProof.h</a>"</span>
<a name="l00005"></a>00005
<a name="l00006"></a><a class="code" href="classLFSCProofExpr.html">00006</a> <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>
<a name="l00007"></a>00007 {
<a name="l00008"></a><a class="code" href="classLFSCProofExpr.html#a106f3177a0ffd00ba0020e29386ce7a1">00008</a> <span class="keywordtype">bool</span> <a class="code" href="classLFSCProofExpr.html#a106f3177a0ffd00ba0020e29386ce7a1">isHole</a>;
<a name="l00009"></a><a class="code" href="classLFSCProofExpr.html#a4e869144eebfc398c8cc1fd0a9c16e87">00009</a> <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>;
<a name="l00010"></a>00010 <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> );
<a name="l00011"></a>00011 <span class="keywordtype">void</span> <a class="code" href="classLFSCProofExpr.html#a0193ac878cd5eaafdedc1d4ee669d73c">initialize</a>();
<a name="l00012"></a><a class="code" href="classLFSCProofExpr.html#a6a432651f947000fef20ee0f955301c8">00012</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCProofExpr.html#a6a432651f947000fef20ee0f955301c8">~LFSCProofExpr</a>(){}
<a name="l00013"></a><a class="code" href="classLFSCProofExpr.html#a6c3db39b65904445c0dfc727cbba3996">00013</a> <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; }
<a name="l00014"></a>00014 <span class="keyword">public</span>:
<a name="l00015"></a><a class="code" href="classLFSCProofExpr.html#a0e718fc15fa1ab162fb38489a2c2c579">00015</a> <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>; }
<a name="l00016"></a>00016 <span class="keywordtype">void</span> <a class="code" href="classLFSCProofExpr.html#af732b18f23d3bb237583048f52dc60c1">print_pf</a>( std::ostream& s, <span class="keywordtype">int</span> ind );
<a name="l00017"></a><a class="code" href="classLFSCProofExpr.html#a5889c9d07ff4346fe7cd9533a236839a">00017</a> <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 ); }
<a name="l00018"></a><a class="code" href="classLFSCProofExpr.html#a6cc953e364c97a359d09c63fe08be7be">00018</a> <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> ); }
<a name="l00019"></a>00019
<a name="l00020"></a><a class="code" href="classLFSCProofExpr.html#aac86e160f1dc7ac8b8c6cf90e22ebfee">00020</a> <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>; }
<a name="l00021"></a>00021 };
<a name="l00022"></a>00022
<a name="l00023"></a><a class="code" href="classLFSCPfVar.html">00023</a> <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> {
<a name="l00024"></a>00024 <span class="keyword">private</span>:
<a name="l00025"></a><a class="code" href="classLFSCPfVar.html#af190aa354850d11f2f183a46401fe685">00025</a> <span class="keyword">static</span> std::map< int, RefPtr< LFSCProof > > <a class="code" href="classLFSCPfVar.html#af190aa354850d11f2f183a46401fe685">vMap</a>;
<a name="l00026"></a><a class="code" href="classLFSCPfVar.html#a04fb4e87bdae6825800546d84b5368dd">00026</a> <span class="keywordtype">string</span> <a class="code" href="classLFSCPfVar.html#a04fb4e87bdae6825800546d84b5368dd">name</a>;
<a name="l00027"></a><a class="code" href="classLFSCPfVar.html#a91a2fc1851dd341464eca5811e0b9775">00027</a> <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 ){}
<a name="l00028"></a><a class="code" href="classLFSCPfVar.html#aaea0a9b256a1c9080968c2306e8c35b9">00028</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCPfVar.html#aaea0a9b256a1c9080968c2306e8c35b9">~LFSCPfVar</a>(){}
<a name="l00029"></a><a class="code" href="classLFSCPfVar.html#afbdfac3e19586ccbf29321b2a08feddc">00029</a> <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(); }
<a name="l00030"></a>00030 <span class="keyword">public</span>:
<a name="l00031"></a><a class="code" href="classLFSCPfVar.html#a5b6e5edc54a507a7c695ffa2999671b0">00031</a> <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>; }
<a name="l00032"></a><a class="code" href="classLFSCPfVar.html#a0b69489a9e1546ba6741de5b5400c8e9">00032</a> <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>; }
<a name="l00033"></a><a class="code" href="classLFSCPfVar.html#aca4bf1d3cd471df00f7354797553be35">00033</a> <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>; }
<a name="l00034"></a>00034 <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 );
<a name="l00035"></a>00035 <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 );
<a name="l00036"></a><a class="code" href="classLFSCPfVar.html#a6156af7863569dca0abed952fa938978">00036</a> <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> ); }
<a name="l00037"></a>00037 };
<a name="l00038"></a>00038
<a name="l00039"></a><a class="code" href="classLFSCPfLambda.html">00039</a> <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> {
<a name="l00040"></a>00040 <span class="keyword">private</span>:
<a name="l00041"></a><a class="code" href="classLFSCPfLambda.html#a96501c8c824e1fac2840f20deb1d7863">00041</a> <a class="code" href="classRefPtr.html">RefPtr< LFSCPfVar ></a> <a class="code" href="classLFSCPfLambda.html#a96501c8c824e1fac2840f20deb1d7863">pfV</a>;
<a name="l00042"></a><a class="code" href="classLFSCPfLambda.html#adf3639aa319befe98b862f5456732606">00042</a> <a class="code" href="classRefPtr.html">RefPtr< LFSCProof ></a> <a class="code" href="classLFSCPfLambda.html#adf3639aa319befe98b862f5456732606">body</a>;
<a name="l00043"></a>00043 <span class="comment">//just a placeholder. This is what the lambda abstracts.</span>
<a name="l00044"></a><a class="code" href="classLFSCPfLambda.html#a0c5823bc758214d9fbb3cfb942cc8ac6">00044</a> <a class="code" href="classRefPtr.html">RefPtr< LFSCProof ></a> <a class="code" href="classLFSCPfLambda.html#a0c5823bc758214d9fbb3cfb942cc8ac6">abstVal</a>;
<a name="l00045"></a>00045 <span class="comment">//constructor</span>
<a name="l00046"></a><a class="code" href="classLFSCPfLambda.html#a0020ea0939d16f4bf36ce64627996976">00046</a> <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>(),
<a name="l00047"></a>00047 <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 ){}
<a name="l00048"></a><a class="code" href="classLFSCPfLambda.html#a70761805bf4943d2de917ca7d0ff2466">00048</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCPfLambda.html#a70761805bf4943d2de917ca7d0ff2466">~LFSCPfLambda</a>(){}
<a name="l00049"></a><a class="code" href="classLFSCPfLambda.html#aacda4aaa9a0c51ee7bcf59559d77db1d">00049</a> <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>->get_string_length() + <a class="code" href="classLFSCPfLambda.html#adf3639aa319befe98b862f5456732606">body</a>->get_string_length(); }
<a name="l00050"></a>00050 <span class="keyword">public</span>:
<a name="l00051"></a><a class="code" href="classLFSCPfLambda.html#a2dac1e9539015c086c3a6e9df2fa948e">00051</a> <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>; }
<a name="l00052"></a>00052 <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 );
<a name="l00053"></a><a class="code" href="classLFSCPfLambda.html#abcb32823122bdb0558104cceeed81490">00053</a> <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 ){
<a name="l00054"></a>00054 <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classLFSCPfLambda.html#a0020ea0939d16f4bf36ce64627996976">LFSCPfLambda</a>( v, bd, aVal );
<a name="l00055"></a>00055 }
<a name="l00056"></a><a class="code" href="classLFSCPfLambda.html#ace06bdec9d26641fe98c7b32b582d67e">00056</a> <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>() ); }
<a name="l00057"></a><a class="code" href="classLFSCPfLambda.html#a96fd9ae0a48dd8bb55e9e0fcde2fbe16">00057</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCPfLambda.html#a96fd9ae0a48dd8bb55e9e0fcde2fbe16">getNumChildren</a>() { <span class="keywordflow">return</span> 2; }
<a name="l00058"></a><a class="code" href="classLFSCPfLambda.html#a697280bf0655b2861c5073daa847a33e">00058</a> <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>(); }
<a name="l00059"></a>00059 };
<a name="l00060"></a>00060 <span class="comment">//</span>
<a name="l00061"></a><a class="code" href="classLFSCProofGeneric.html">00061</a> <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>{
<a name="l00062"></a>00062 <span class="keyword">private</span>:
<a name="l00063"></a><a class="code" href="classLFSCProofGeneric.html#af785d15d167f9f5f3985caa179ca9f85">00063</a> vector< RefPtr< LFSCProof > > <a class="code" href="classLFSCProofGeneric.html#af785d15d167f9f5f3985caa179ca9f85">d_pf</a>;
<a name="l00064"></a><a class="code" href="classLFSCProofGeneric.html#ae985971cfcdba65ec9e39472b023effe">00064</a> vector< string > <a class="code" href="classLFSCProofGeneric.html#ae985971cfcdba65ec9e39472b023effe">d_str</a>;
<a name="l00065"></a><a class="code" href="classLFSCProofGeneric.html#ab1c9b0ca7c6984d0bf6de79761510131">00065</a> <span class="keywordtype">bool</span> <a class="code" href="classLFSCProofGeneric.html#ab1c9b0ca7c6984d0bf6de79761510131">debug_str</a>;
<a name="l00066"></a>00066 <span class="comment">//Proof in the form "S1.print(P1).S2.print(P2).....print(Pn).S{n+1}"</span>
<a name="l00067"></a><a class="code" href="classLFSCProofGeneric.html#a45f64e0c33400e0a27191914e9e7054e">00067</a> <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>(){
<a name="l00068"></a>00068 <span class="keywordflow">for</span>( <span class="keywordtype">int</span> a=0; a<(int)d_pfs.size(); a++ )
<a name="l00069"></a>00069 <a class="code" href="classLFSCProofGeneric.html#af785d15d167f9f5f3985caa179ca9f85">d_pf</a>.push_back( d_pfs[a].get() );
<a name="l00070"></a>00070 <span class="keywordflow">for</span>( <span class="keywordtype">int</span> a=0; a<(int)d_strs.size(); a++ )
<a name="l00071"></a>00071 <a class="code" href="classLFSCProofGeneric.html#ae985971cfcdba65ec9e39472b023effe">d_str</a>.push_back( d_strs[a] );
<a name="l00072"></a>00072 <a class="code" href="classLFSCProofGeneric.html#ab1c9b0ca7c6984d0bf6de79761510131">debug_str</a> = db_str;
<a name="l00073"></a>00073 }
<a name="l00074"></a><a class="code" href="classLFSCProofGeneric.html#a356d195515529108c3c143abcf1850d8">00074</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCProofGeneric.html#a356d195515529108c3c143abcf1850d8">~LFSCProofGeneric</a>(){}
<a name="l00075"></a>00075 <span class="keywordtype">long</span> <span class="keywordtype">int</span> <a class="code" href="classLFSCProofGeneric.html#a7acae5a8c672b63f1aab26c3feb9ab67">get_length</a>();
<a name="l00076"></a>00076 <span class="keyword">public</span>:
<a name="l00077"></a><a class="code" href="classLFSCProofGeneric.html#a89efd3123a97c54a31a477e75185dd63">00077</a> <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>; }
<a name="l00078"></a>00078 <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 );
<a name="l00079"></a>00079 <span class="comment">//Proof in the form "S1.print(P1).S2.print(P2).....print(Pn).S{n+1}"</span>
<a name="l00080"></a><a class="code" href="classLFSCProofGeneric.html#a1bf5343c88454d1ffb552a3e2f59ddc8">00080</a> <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> ){
<a name="l00081"></a>00081 <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 );
<a name="l00082"></a>00082 }
<a name="l00083"></a>00083 <span class="comment">//proof printed in the form "S1.print(P1).S2"</span>
<a name="l00084"></a>00084 <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> );
<a name="l00085"></a>00085 <span class="comment">//proof printed in the form "S1.print(P1).print(P2).S2"</span>
<a name="l00086"></a>00086 <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> );
<a name="l00087"></a>00087 <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> );
<a name="l00088"></a><a class="code" href="classLFSCProofGeneric.html#a49ff2fcc1122bbecf8fff0559ddeccad">00088</a> <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> ); }
<a name="l00089"></a><a class="code" href="classLFSCProofGeneric.html#aec701cd210f5e2aa1734c644c0ab4c6a">00089</a> <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> ); }
<a name="l00090"></a><a class="code" href="classLFSCProofGeneric.html#a588df357bf41ff575e52cb7dd0d34040">00090</a> <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(); }
<a name="l00091"></a><a class="code" href="classLFSCProofGeneric.html#a10ab8502f739ebccfa77b8a8436223fe">00091</a> <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(); }
<a name="l00092"></a>00092 };
<a name="l00093"></a>00093
<a name="l00094"></a>00094
<a name="l00095"></a><a class="code" href="classLFSCPfLet.html">00095</a> <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>{
<a name="l00096"></a>00096 <span class="keyword">private</span>:
<a name="l00097"></a><a class="code" href="classLFSCPfLet.html#a01244b4de08d6beaf09a0fc7c5263a65">00097</a> <a class="code" href="classRefPtr.html">RefPtr< LFSCProof ></a> <a class="code" href="classLFSCPfLet.html#a01244b4de08d6beaf09a0fc7c5263a65">d_letPf</a>;
<a name="l00098"></a><a class="code" href="classLFSCPfLet.html#a256986dda0a58de4e8aed2a5e582ed67">00098</a> <a class="code" href="classRefPtr.html">RefPtr< LFSCPfVar ></a> <a class="code" href="classLFSCPfLet.html#a256986dda0a58de4e8aed2a5e582ed67">d_pv</a>;
<a name="l00099"></a><a class="code" href="classLFSCPfLet.html#acc201153269f577e4f90827e0804f5f3">00099</a> <a class="code" href="classRefPtr.html">RefPtr< LFSCProof ></a> <a class="code" href="classLFSCPfLet.html#acc201153269f577e4f90827e0804f5f3">d_body</a>;
<a name="l00100"></a>00100 <span class="comment">//this should be equal to d_letPf, although it could be something else based on fv</span>
<a name="l00101"></a><a class="code" href="classLFSCPfLet.html#abb7a9123dbd3efff87166fcf3642815f">00101</a> <a class="code" href="classRefPtr.html">RefPtr< LFSCProof ></a> <a class="code" href="classLFSCPfLet.html#abb7a9123dbd3efff87166fcf3642815f">d_letPfRpl</a>;
<a name="l00102"></a>00102 <span class="comment">//this by default is d_pv, although it could be something else based on fv</span>
<a name="l00103"></a><a class="code" href="classLFSCPfLet.html#af289f9e13c553b1115a4f6fcd56b4423">00103</a> <a class="code" href="classRefPtr.html">RefPtr< LFSCProof ></a> <a class="code" href="classLFSCPfLet.html#af289f9e13c553b1115a4f6fcd56b4423">d_pvRpl</a>;
<a name="l00104"></a><a class="code" href="classLFSCPfLet.html#ad52e42e731d1a53a5acbf84f852879ac">00104</a> <span class="keywordtype">bool</span> <a class="code" href="classLFSCPfLet.html#ad52e42e731d1a53a5acbf84f852879ac">d_isTh</a>;
<a name="l00105"></a><a class="code" href="classLFSCPfLet.html#acfc17527ee09a3f10203af05cd972a4a">00105</a> <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,
<a name="l00106"></a>00106 <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>(),
<a name="l00107"></a>00107 <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 ){}
<a name="l00108"></a>00108 <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,
<a name="l00109"></a>00109 <span class="keywordtype">bool</span> isTh, std::vector< int >& fv );
<a name="l00110"></a><a class="code" href="classLFSCPfLet.html#ad31eff106a2d0c78172390d755d625e2">00110</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCPfLet.html#ad31eff106a2d0c78172390d755d625e2">~LFSCPfLet</a>(){}
<a name="l00111"></a><a class="code" href="classLFSCPfLet.html#a49cb76df6e4fbb2f13a21e9c626efc45">00111</a> <span class="keywordtype">long</span> <span class="keywordtype">int</span> <a class="code" href="classLFSCPfLet.html#a49cb76df6e4fbb2f13a21e9c626efc45">get_length</a>() {
<a name="l00112"></a>00112 <span class="keywordflow">return</span> 10 + <a class="code" href="classLFSCPfLet.html#a01244b4de08d6beaf09a0fc7c5263a65">d_letPf</a>->get_string_length() + <a class="code" href="classLFSCPfLet.html#a256986dda0a58de4e8aed2a5e582ed67">d_pv</a>->get_string_length() + <a class="code" href="classLFSCPfLet.html#acc201153269f577e4f90827e0804f5f3">d_body</a>->get_string_length();
<a name="l00113"></a>00113 }
<a name="l00114"></a>00114 <span class="keyword">public</span>:
<a name="l00115"></a><a class="code" href="classLFSCPfLet.html#a554bd849b6be3e87301664a78af548c2">00115</a> <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>; }
<a name="l00116"></a>00116 <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 );
<a name="l00117"></a>00117 <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 );
<a name="l00118"></a><a class="code" href="classLFSCPfLet.html#a8a9295947ba6381d158f39b570fcebaf">00118</a> <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,
<a name="l00119"></a>00119 <span class="keywordtype">bool</span> isTh, std::vector< int >& fv ){
<a name="l00120"></a>00120 <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classLFSCPfLet.html#acfc17527ee09a3f10203af05cd972a4a">LFSCPfLet</a>( letPf, pv, body, isTh, fv );
<a name="l00121"></a>00121 }
<a name="l00122"></a><a class="code" href="classLFSCPfLet.html#ab436db06a158bf463c0614f34608cfaf">00122</a> <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>(),
<a name="l00123"></a>00123 <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>() ); }
<a name="l00124"></a>00124 <span class="comment">//should not be part of the children structure.</span>
<a name="l00125"></a>00125 };
<a name="l00126"></a>00126
<a name="l00127"></a>00127
<a name="l00128"></a>00128 <span class="preprocessor">#endif</span>
</pre></div></div>
</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>
