<!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: LFSCProof.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">LFSCProof.h</div> </div>
</div>
<div class="contents">
<a href="LFSCProof_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_PROOF_H_</span>
<a name="l00002"></a>00002 <span class="preprocessor"></span><span class="preprocessor">#define LFSC_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="LFSCObject_8h.html">LFSCObject.h</a>"</span>
<a name="l00005"></a>00005 <span class="comment"></span>
<a name="l00006"></a>00006 <span class="comment">//////////////////////////////////</span>
<a name="l00007"></a>00007 <span class="comment">/// LFSC Proof Class & subclasses</span>
<a name="l00008"></a>00008 <span class="comment">//////////////////////////////////</span>
<a name="l00009"></a>00009 <span class="comment"></span>
<a name="l00010"></a>00010 <span class="keyword">class </span><a class="code" href="classLFSCProofExpr.html">LFSCProofExpr</a>;
<a name="l00011"></a>00011 <span class="keyword">class </span><a class="code" href="classLFSCLraAdd.html">LFSCLraAdd</a>;
<a name="l00012"></a>00012 <span class="keyword">class </span><a class="code" href="classLFSCLraSub.html">LFSCLraSub</a>;
<a name="l00013"></a>00013 <span class="keyword">class </span><a class="code" href="classLFSCLraMulC.html">LFSCLraMulC</a>;
<a name="l00014"></a>00014 <span class="keyword">class </span><a class="code" href="classLFSCLraAxiom.html">LFSCLraAxiom</a>;
<a name="l00015"></a>00015 <span class="keyword">class </span><a class="code" href="classLFSCLraContra.html">LFSCLraContra</a>;
<a name="l00016"></a>00016 <span class="keyword">class </span><a class="code" href="classLFSCLraPoly.html">LFSCLraPoly</a>;
<a name="l00017"></a>00017 <span class="keyword">class </span><a class="code" href="classLFSCBoolRes.html">LFSCBoolRes</a>;
<a name="l00018"></a>00018 <span class="keyword">class </span><a class="code" href="classLFSCLem.html">LFSCLem</a>;
<a name="l00019"></a>00019 <span class="keyword">class </span><a class="code" href="classLFSCClausify.html">LFSCClausify</a>;
<a name="l00020"></a>00020 <span class="keyword">class </span><a class="code" href="classLFSCAssume.html">LFSCAssume</a>;
<a name="l00021"></a>00021 <span class="keyword">class </span><a class="code" href="classLFSCProofGeneric.html">LFSCProofGeneric</a>;
<a name="l00022"></a>00022 <span class="keyword">class </span><a class="code" href="classLFSCPfVar.html">LFSCPfVar</a>;
<a name="l00023"></a>00023 <span class="keyword">class </span><a class="code" href="classLFSCPfLambda.html">LFSCPfLambda</a>;
<a name="l00024"></a>00024 <span class="keyword">class </span><a class="code" href="classLFSCPfLet.html">LFSCPfLet</a>;
<a name="l00025"></a>00025
<a name="l00026"></a><a class="code" href="classLFSCProof.html">00026</a> <span class="keyword">class </span><a class="code" href="classLFSCProof.html">LFSCProof</a> : <span class="keyword">public</span> <a class="code" href="classLFSCObj.html">LFSCObj</a>{
<a name="l00027"></a>00027 <span class="keyword">protected</span>:
<a name="l00028"></a><a class="code" href="classLFSCProof.html#a3614c6ce131c1d8a0fd2c18610659117">00028</a> <span class="keyword">static</span> <span class="keywordtype">int</span> <a class="code" href="classLFSCProof.html#a3614c6ce131c1d8a0fd2c18610659117">pf_counter</a>;
<a name="l00029"></a><a class="code" href="classLFSCProof.html#a5f40eaf9f09aa0607f5063e460de1552">00029</a> <span class="keyword">static</span> std::map< LFSCProof*, int > <a class="code" href="classLFSCProof.html#a5f40eaf9f09aa0607f5063e460de1552">lambdaMap</a>;
<a name="l00030"></a><a class="code" href="classLFSCProof.html#ac8fd8287bbc4d4f0a8f8f456b6dca0a4">00030</a> <span class="keyword">static</span> std::map< LFSCProof*, LFSCProof* > <a class="code" href="classLFSCProof.html#ac8fd8287bbc4d4f0a8f8f456b6dca0a4">lambdaPrintMap</a>;
<a name="l00031"></a><a class="code" href="classLFSCProof.html#ae133e339354b3013e30d2c3c1fb5e26e">00031</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCProof.html#ae133e339354b3013e30d2c3c1fb5e26e">printCounter</a>;
<a name="l00032"></a><a class="code" href="classLFSCProof.html#a23e3f4b905b79583835415f70576fc76">00032</a> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCProof.html#a23e3f4b905b79583835415f70576fc76">rplProof</a>;
<a name="l00033"></a><a class="code" href="classLFSCProof.html#a6ce5b89de4d7cb2731e503272d746199">00033</a> <span class="keyword">static</span> <span class="keywordtype">int</span> <a class="code" href="classLFSCProof.html#a6ce5b89de4d7cb2731e503272d746199">lambdaCounter</a>;
<a name="l00034"></a><a class="code" href="classLFSCProof.html#a4e612043c9a9fbf3410d56cd2ff78b5e">00034</a> <span class="keywordtype">long</span> <span class="keywordtype">int</span> <a class="code" href="classLFSCProof.html#a4e612043c9a9fbf3410d56cd2ff78b5e">strLen</a>;
<a name="l00035"></a><a class="code" href="classLFSCProof.html#addc61701b4bbfb7119df3b00667e808a">00035</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCProof.html#addc61701b4bbfb7119df3b00667e808a">chOp</a>;
<a name="l00036"></a><a class="code" href="classLFSCProof.html#a425fcc2ea8b8801dbd7780ddcc20d624">00036</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCProof.html#a425fcc2ea8b8801dbd7780ddcc20d624">assumeVar</a>;
<a name="l00037"></a><a class="code" href="classLFSCProof.html#a3080390335b3e2338814bbfed11356f6">00037</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCProof.html#a3080390335b3e2338814bbfed11356f6">assumeVarUsed</a>;
<a name="l00038"></a>00038
<a name="l00039"></a><a class="code" href="classLFSCProof.html#a80c629f061bf236f2cfe1c4ad3449b75">00039</a> std::vector< int > <a class="code" href="classLFSCProof.html#a80c629f061bf236f2cfe1c4ad3449b75">br</a>;
<a name="l00040"></a><a class="code" href="classLFSCProof.html#acc878f584c9d1c1c59737870fd006e0b">00040</a> <span class="keywordtype">bool</span> <a class="code" href="classLFSCProof.html#acc878f584c9d1c1c59737870fd006e0b">brComputed</a>;
<a name="l00041"></a>00041
<a name="l00042"></a>00042 <a class="code" href="classLFSCProof.html#a08258b1a59261c0dd0edcd775a883cfc">LFSCProof</a>();
<a name="l00043"></a><a class="code" href="classLFSCProof.html#a4f6cb66f81baeb838874bfc2ee51595e">00043</a> <span class="keyword">virtual</span> <span class="keywordtype">long</span> <span class="keywordtype">int</span> <a class="code" href="classLFSCProof.html#a4f6cb66f81baeb838874bfc2ee51595e">get_length</a>() { <span class="keywordflow">return</span> 0; }
<a name="l00044"></a><a class="code" href="classLFSCProof.html#a734881b4ad199d3251973cc844a18929">00044</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCProof.html#a734881b4ad199d3251973cc844a18929">~LFSCProof</a>(){}
<a name="l00045"></a>00045 <span class="keyword">public</span>:
<a name="l00046"></a><a class="code" href="classLFSCProof.html#ae1a19870033df1a9656e54ca2e4c21a6">00046</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCProofExpr.html">LFSCProofExpr</a>* <a class="code" href="classLFSCProof.html#ae1a19870033df1a9656e54ca2e4c21a6">AsLFSCProofExpr</a>(){ <span class="keywordflow">return</span> NULL; }
<a name="l00047"></a><a class="code" href="classLFSCProof.html#a7cc0f70e22642f958d58bdcebcd06530">00047</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCLraAdd.html">LFSCLraAdd</a>* <a class="code" href="classLFSCProof.html#a7cc0f70e22642f958d58bdcebcd06530">AsLFSCLraAdd</a>(){ <span class="keywordflow">return</span> NULL; }
<a name="l00048"></a><a class="code" href="classLFSCProof.html#a60be4bca8e5d7487bd19f391b675d49b">00048</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCLraSub.html">LFSCLraSub</a>* <a class="code" href="classLFSCProof.html#a60be4bca8e5d7487bd19f391b675d49b">AsLFSCLraSub</a>(){ <span class="keywordflow">return</span> NULL; }
<a name="l00049"></a><a class="code" href="classLFSCProof.html#a87f99538036f96fd800bc97049478af2">00049</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCLraMulC.html">LFSCLraMulC</a>* <a class="code" href="classLFSCProof.html#a87f99538036f96fd800bc97049478af2">AsLFSCLraMulC</a>(){ <span class="keywordflow">return</span> NULL; }
<a name="l00050"></a><a class="code" href="classLFSCProof.html#a9b6a71f2857c0bbdd2689aa3665657da">00050</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCLraAxiom.html">LFSCLraAxiom</a>* <a class="code" href="classLFSCProof.html#a9b6a71f2857c0bbdd2689aa3665657da">AsLFSCLraAxiom</a>(){ <span class="keywordflow">return</span> NULL; }
<a name="l00051"></a><a class="code" href="classLFSCProof.html#a52f0d889a8439f484b1995ae2536a671">00051</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCLraContra.html">LFSCLraContra</a>* <a class="code" href="classLFSCProof.html#a52f0d889a8439f484b1995ae2536a671">AsLFSCLraContra</a>(){ <span class="keywordflow">return</span> NULL; }
<a name="l00052"></a><a class="code" href="classLFSCProof.html#a13a5d84e3c02842c331c0093689edd58">00052</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCLraPoly.html">LFSCLraPoly</a>* <a class="code" href="classLFSCProof.html#a13a5d84e3c02842c331c0093689edd58">AsLFSCLraPoly</a>(){ <span class="keywordflow">return</span> NULL; }
<a name="l00053"></a><a class="code" href="classLFSCProof.html#a6b5678c20b54da5345d66b595a33a719">00053</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCBoolRes.html">LFSCBoolRes</a>* <a class="code" href="classLFSCProof.html#a6b5678c20b54da5345d66b595a33a719">AsLFSCBoolRes</a>(){ <span class="keywordflow">return</span> NULL; }
<a name="l00054"></a><a class="code" href="classLFSCProof.html#a35b9ae21403a09523359d96d182c7431">00054</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCLem.html">LFSCLem</a>* <a class="code" href="classLFSCProof.html#a35b9ae21403a09523359d96d182c7431">AsLFSCLem</a>(){ <span class="keywordflow">return</span> NULL; }
<a name="l00055"></a><a class="code" href="classLFSCProof.html#a1ae53259bdc504ba263e86b0d85ccede">00055</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCClausify.html">LFSCClausify</a>* <a class="code" href="classLFSCProof.html#a1ae53259bdc504ba263e86b0d85ccede">AsLFSCClausify</a>(){ <span class="keywordflow">return</span> NULL; }
<a name="l00056"></a><a class="code" href="classLFSCProof.html#a090256e5ceadaccaa46826689f95f238">00056</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCAssume.html">LFSCAssume</a>* <a class="code" href="classLFSCProof.html#a090256e5ceadaccaa46826689f95f238">AsLFSCAssume</a>(){ <span class="keywordflow">return</span> NULL; }
<a name="l00057"></a><a class="code" href="classLFSCProof.html#a11df493e82f924825e42d2bcef64c1f6">00057</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCProofGeneric.html">LFSCProofGeneric</a>* <a class="code" href="classLFSCProof.html#a11df493e82f924825e42d2bcef64c1f6">AsLFSCProofGeneric</a>(){ <span class="keywordflow">return</span> NULL; }
<a name="l00058"></a><a class="code" href="classLFSCProof.html#a3204930c32bc4a67ec0ddb23b3be51be">00058</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCPfVar.html">LFSCPfVar</a>* <a class="code" href="classLFSCProof.html#a3204930c32bc4a67ec0ddb23b3be51be">AsLFSCPfVar</a>(){ <span class="keywordflow">return</span> NULL; }
<a name="l00059"></a><a class="code" href="classLFSCProof.html#ad56845dc18ff11a9a054c7137ce5a680">00059</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCPfLambda.html">LFSCPfLambda</a>* <a class="code" href="classLFSCProof.html#ad56845dc18ff11a9a054c7137ce5a680">AsLFSCPfLambda</a>(){ <span class="keywordflow">return</span> NULL; }
<a name="l00060"></a><a class="code" href="classLFSCProof.html#aefd45e8a659276c68dd2797a995ffc87">00060</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCPfLet.html">LFSCPfLet</a>* <a class="code" href="classLFSCProof.html#aefd45e8a659276c68dd2797a995ffc87">AsLFSCPfLet</a>(){ <span class="keywordflow">return</span> NULL; }
<a name="l00061"></a>00061
<a name="l00062"></a><a class="code" href="classLFSCProof.html#aa1dbda64d42f7bf7c81a1b6e68da2766">00062</a> <span class="keyword">virtual</span> <span class="keywordtype">bool</span> <a class="code" href="classLFSCProof.html#aa1dbda64d42f7bf7c81a1b6e68da2766">isLraMulC</a>() { <span class="keywordflow">return</span> <span class="keyword">false</span>; }
<a name="l00063"></a><a class="code" href="classLFSCProof.html#a396c41fc6012caf4dde358af52d25905">00063</a> <span class="keyword">static</span> <span class="keywordtype">int</span> <a class="code" href="classLFSCProof.html#a396c41fc6012caf4dde358af52d25905">make_lambda</a>( <a class="code" href="classLFSCProof.html">LFSCProof</a>* p ){
<a name="l00064"></a>00064 <span class="keywordflow">if</span>( <a class="code" href="classLFSCProof.html#a5f40eaf9f09aa0607f5063e460de1552">lambdaMap</a>[p]==0 ){
<a name="l00065"></a>00065 <a class="code" href="classLFSCProof.html#a5f40eaf9f09aa0607f5063e460de1552">lambdaMap</a>[p] = <a class="code" href="classLFSCProof.html#a6ce5b89de4d7cb2731e503272d746199">lambdaCounter</a>;
<a name="l00066"></a>00066 <a class="code" href="classLFSCProof.html#a6ce5b89de4d7cb2731e503272d746199">lambdaCounter</a>++;
<a name="l00067"></a>00067 }
<a name="l00068"></a>00068 <span class="keywordflow">return</span> <a class="code" href="classLFSCProof.html#a5f40eaf9f09aa0607f5063e460de1552">lambdaMap</a>[p];
<a name="l00069"></a>00069 }
<a name="l00070"></a>00070 <span class="keywordtype">void</span> <a class="code" href="classLFSCProof.html#aed472da83c57ed8a1ac6d2a6bc34eeba">print</a>( std::ostream& s, <span class="keywordtype">int</span> ind = 0 );
<a name="l00071"></a>00071 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classLFSCProof.html#a9ad1d738b10d731108f63b9d86796c00">print_pf</a>( std::ostream& s, <span class="keywordtype">int</span> ind = 0 )=0;
<a name="l00072"></a><a class="code" href="classLFSCProof.html#a094c8c12bcb8ee3b1ec7a51b5568c355">00072</a> <span class="keyword">virtual</span> <span class="keywordtype">bool</span> <a class="code" href="classLFSCProof.html#a094c8c12bcb8ee3b1ec7a51b5568c355">isTrivial</a>() { <span class="keywordflow">return</span> <span class="keyword">false</span>; }
<a name="l00073"></a><a class="code" href="classLFSCProof.html#a784c4a1295785719bce419d3e9ee9be1">00073</a> <span class="keywordtype">long</span> <span class="keywordtype">int</span> <a class="code" href="classLFSCProof.html#a784c4a1295785719bce419d3e9ee9be1">get_string_length</a>() {
<a name="l00074"></a>00074 <span class="keywordflow">if</span>( <a class="code" href="classLFSCProof.html#a4e612043c9a9fbf3410d56cd2ff78b5e">strLen</a><0 ){
<a name="l00075"></a>00075 <a class="code" href="classLFSCProof.html#a4e612043c9a9fbf3410d56cd2ff78b5e">strLen</a> = <a class="code" href="classLFSCProof.html#a4f6cb66f81baeb838874bfc2ee51595e">get_length</a>();
<a name="l00076"></a>00076 <span class="comment">//to prevent overflow</span>
<a name="l00077"></a>00077 <span class="keywordflow">for</span>( <span class="keywordtype">int</span> a=0; a<<a class="code" href="classLFSCProof.html#aedc30ad27db2049d1e6782918bdc2608">getNumChildren</a>(); a++ ){
<a name="l00078"></a>00078 <span class="keywordflow">if</span>( <a class="code" href="classLFSCProof.html#a4e612043c9a9fbf3410d56cd2ff78b5e">strLen</a><<a class="code" href="classLFSCProof.html#ac60cfef82cf6aaa935668cbfab2ecd10">getChild</a>( a )-><a class="code" href="classLFSCProof.html#a784c4a1295785719bce419d3e9ee9be1">get_string_length</a>() ){
<a name="l00079"></a>00079 <a class="code" href="classLFSCProof.html#a4e612043c9a9fbf3410d56cd2ff78b5e">strLen</a> = <a class="code" href="classLFSCProof.html#ac60cfef82cf6aaa935668cbfab2ecd10">getChild</a>( a )-><a class="code" href="classLFSCProof.html#a784c4a1295785719bce419d3e9ee9be1">get_string_length</a>();
<a name="l00080"></a>00080 }
<a name="l00081"></a>00081 }
<a name="l00082"></a>00082 }
<a name="l00083"></a>00083 <span class="keywordflow">return</span> <a class="code" href="classLFSCProof.html#a4e612043c9a9fbf3410d56cd2ff78b5e">strLen</a>;
<a name="l00084"></a>00084 }
<a name="l00085"></a>00085 <span class="keywordtype">void</span> <a class="code" href="classLFSCProof.html#ae135f7109d7cc2a9185a48487840b683">print_structure</a>( std::ostream& s, <span class="keywordtype">int</span> ind = 0 );
<a name="l00086"></a><a class="code" href="classLFSCProof.html#a989d58a3910834809ddbfc89c04f6d87">00086</a> <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classLFSCProof.html#a989d58a3910834809ddbfc89c04f6d87">print_struct</a>( std::ostream& s, <span class="keywordtype">int</span> ind = 0 ){
<a name="l00087"></a>00087 <span class="keyword">static</span> <span class="keywordtype">int</span> psCounter = 0;
<a name="l00088"></a>00088 s << <span class="stringliteral">"P"</span> << psCounter;
<a name="l00089"></a>00089 psCounter++;
<a name="l00090"></a>00090 }
<a name="l00091"></a><a class="code" href="classLFSCProof.html#ae8e4007daade52b31f52182192d46abc">00091</a> <span class="keywordtype">void</span> <a class="code" href="classLFSCProof.html#ae8e4007daade52b31f52182192d46abc">setRplProof</a>( <a class="code" href="classLFSCProof.html">LFSCProof</a>* p ) { <a class="code" href="classLFSCProof.html#a23e3f4b905b79583835415f70576fc76">rplProof</a> = p; }
<a name="l00092"></a>00092 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classLFSCProof.html#ada9a53bcd04fe712b1fc22f9a0a23ccc">fillHoles</a>();
<a name="l00093"></a>00093 <span class="preprocessor">#ifdef OPTIMIZE</span>
<a name="l00094"></a>00094 <span class="preprocessor"></span> <span class="keywordtype">void</span> calcL( std::vector< int >& lget, std::vector< int >& lgetu );
<a name="l00095"></a>00095 <span class="preprocessor">#endif</span>
<a name="l00096"></a>00096 <span class="preprocessor"></span>
<a name="l00097"></a><a class="code" href="classLFSCProof.html#a2d3cb4e50f5ffb662dc18e83ee206c2c">00097</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classLFSCPrinter.html">LFSCPrinter</a>;
<a name="l00098"></a>00098
<a name="l00099"></a>00099 <span class="keyword">virtual</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCProof.html#a0fff5e24b97c44080514e3ec6f15d751">clone</a>() = 0;
<a name="l00100"></a><a class="code" href="classLFSCProof.html#aedc30ad27db2049d1e6782918bdc2608">00100</a> <span class="keyword">virtual</span> <span class="keywordtype">int</span> <a class="code" href="classLFSCProof.html#aedc30ad27db2049d1e6782918bdc2608">getNumChildren</a>() { <span class="keywordflow">return</span> 0; }
<a name="l00101"></a><a class="code" href="classLFSCProof.html#ac60cfef82cf6aaa935668cbfab2ecd10">00101</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCProof.html#ac60cfef82cf6aaa935668cbfab2ecd10">getChild</a>( <span class="keywordtype">int</span> n ) { <span class="keywordflow">return</span> NULL; }
<a name="l00102"></a>00102 <span class="keyword">virtual</span> <span class="keywordtype">int</span> <a class="code" href="classLFSCProof.html#a8bb7d43de0773db524227b1c2af54bb0">checkOp</a>();
<a name="l00103"></a><a class="code" href="classLFSCProof.html#a6b95ef9fff90f5410755fdb628c6897c">00103</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCProof.html#a6b95ef9fff90f5410755fdb628c6897c">getChOp</a>(){ <span class="keywordflow">return</span> <a class="code" href="classLFSCProof.html#addc61701b4bbfb7119df3b00667e808a">chOp</a>; }
<a name="l00104"></a><a class="code" href="classLFSCProof.html#a5152d42d473b2305cae68012da611208">00104</a> <span class="keywordtype">void</span> <a class="code" href="classLFSCProof.html#a5152d42d473b2305cae68012da611208">setChOp</a>( <span class="keywordtype">int</span> c ) { <a class="code" href="classLFSCProof.html#addc61701b4bbfb7119df3b00667e808a">chOp</a> = c; }
<a name="l00105"></a><a class="code" href="classLFSCProof.html#a46af0498dd659ccba0549191102cf75d">00105</a> <span class="keyword">virtual</span> <span class="keywordtype">int</span> <a class="code" href="classLFSCProof.html#a46af0498dd659ccba0549191102cf75d">checkBoolRes</a>( std::vector< int >& clause ){ <span class="keywordflow">return</span> 0; }
<a name="l00106"></a>00106
<a name="l00107"></a>00107 <span class="comment">//proof making methods</span>
<a name="l00108"></a>00108 <span class="keyword">public</span>:
<a name="l00109"></a>00109 <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCProof.html#ab1b22c672f110e3f9abe22b2bf377fb3">Make_CNF</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& form, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& reason, <span class="keywordtype">int</span> pos );
<a name="l00110"></a>00110 <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCProof.html#a95e3c7629c196ed189ad0525304e48cb">Make_not_not_elim</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="classLFSCProof.html">LFSCProof</a>* p );
<a name="l00111"></a>00111 <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCProof.html#a979135fb775da82a9bf06befd9def730">Make_mimic</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="classLFSCProof.html">LFSCProof</a>* p, <span class="keywordtype">int</span> numHoles );
<a name="l00112"></a>00112 <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCProof.html#a547ec01104eb074ab2eb4f25ea9435e0">Make_and_elim</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& form, <a class="code" href="classLFSCProof.html">LFSCProof</a>* p, <span class="keywordtype">int</span> n, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& expected );
<a name="l00113"></a>00113
<a name="l00114"></a><a class="code" href="classLFSCProof.html#a43144544220e21b8519c959973a35c49">00114</a> <span class="keyword">static</span> <span class="keywordtype">int</span> <a class="code" href="classLFSCProof.html#a43144544220e21b8519c959973a35c49">get_proof_counter</a>() { <span class="keywordflow">return</span> <a class="code" href="classLFSCProof.html#a3614c6ce131c1d8a0fd2c18610659117">pf_counter</a>; }
<a name="l00115"></a>00115 };
<a name="l00116"></a>00116
<a name="l00117"></a>00117
<a name="l00118"></a>00118 <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>
