<!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: LFSCLraProof.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">LFSCLraProof.h</div> </div>
</div>
<div class="contents">
<a href="LFSCLraProof_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_LRA_PROOF_H_</span>
<a name="l00002"></a>00002 <span class="preprocessor"></span><span class="preprocessor">#define LFSC_LRA_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>00006 <span class="comment">// lra_add_~_~</span>
<a name="l00007"></a><a class="code" href="classLFSCLraAdd.html">00007</a> <span class="keyword">class </span><a class="code" href="classLFSCLraAdd.html">LFSCLraAdd</a>: <span class="keyword">public</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>{
<a name="l00008"></a>00008 <span class="keyword">private</span>:
<a name="l00009"></a><a class="code" href="classLFSCLraAdd.html#ac6719308cb218ceb7298c05c26bc9eca">00009</a> <a class="code" href="classRefPtr.html">RefPtr< LFSCProof ></a> <a class="code" href="classLFSCLraAdd.html#ac6719308cb218ceb7298c05c26bc9eca">d_children</a>[2];
<a name="l00010"></a><a class="code" href="classLFSCLraAdd.html#a08bbcfafa29abbc7aafbfca31bafc878">00010</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCLraAdd.html#afb25f59c4b8a73e1b4bea1f43d4b42c8">d_op1</a>, <a class="code" href="classLFSCLraAdd.html#a08bbcfafa29abbc7aafbfca31bafc878">d_op2</a>;
<a name="l00011"></a>00011
<a name="l00012"></a><a class="code" href="classLFSCLraAdd.html#a9724d04ec280ff9130b332f76a6051d1">00012</a> <a class="code" href="classLFSCLraAdd.html#a9724d04ec280ff9130b332f76a6051d1">LFSCLraAdd</a>(<a class="code" href="classLFSCProof.html">LFSCProof</a>* pf1, <a class="code" href="classLFSCProof.html">LFSCProof</a>* pf2, <span class="keywordtype">int</span> op1, <span class="keywordtype">int</span> op2): <a class="code" href="classLFSCProof.html">LFSCProof</a>(),
<a name="l00013"></a>00013 <a class="code" href="classLFSCLraAdd.html#afb25f59c4b8a73e1b4bea1f43d4b42c8">d_op1</a>(op1),
<a name="l00014"></a>00014 <a class="code" href="classLFSCLraAdd.html#a08bbcfafa29abbc7aafbfca31bafc878">d_op2</a>(op2){
<a name="l00015"></a>00015 <a class="code" href="classLFSCLraAdd.html#ac6719308cb218ceb7298c05c26bc9eca">d_children</a>[0] = pf1;
<a name="l00016"></a>00016 <a class="code" href="classLFSCLraAdd.html#ac6719308cb218ceb7298c05c26bc9eca">d_children</a>[1] = pf2;
<a name="l00017"></a>00017 }
<a name="l00018"></a><a class="code" href="classLFSCLraAdd.html#ae89d372ad8f9980c064ebc1ca5437e70">00018</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCLraAdd.html#ae89d372ad8f9980c064ebc1ca5437e70">~LFSCLraAdd</a>(){}
<a name="l00019"></a><a class="code" href="classLFSCLraAdd.html#a61994da8716e9432d11d2f6666237425">00019</a> <span class="keywordtype">long</span> <span class="keywordtype">int</span> <a class="code" href="classLFSCLraAdd.html#a61994da8716e9432d11d2f6666237425">get_length</a>(){
<a name="l00020"></a>00020 <span class="keywordflow">return</span> 20 + <a class="code" href="classLFSCLraAdd.html#ac6719308cb218ceb7298c05c26bc9eca">d_children</a>[0]->get_string_length() + <a class="code" href="classLFSCLraAdd.html#ac6719308cb218ceb7298c05c26bc9eca">d_children</a>[1]->get_string_length();
<a name="l00021"></a>00021 }
<a name="l00022"></a>00022 <span class="keyword">public</span>:
<a name="l00023"></a><a class="code" href="classLFSCLraAdd.html#a13e0f9aff803816bc0d1b8908a03a488">00023</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCLraAdd.html">LFSCLraAdd</a>* <a class="code" href="classLFSCLraAdd.html#a13e0f9aff803816bc0d1b8908a03a488">AsLFSCLraAdd</a>(){ <span class="keywordflow">return</span> <span class="keyword">this</span>; }
<a name="l00024"></a>00024 <span class="keywordtype">void</span> <a class="code" href="classLFSCLraAdd.html#a606f0a1297b4cce586f3111c1598808b">print_pf</a>( std::ostream& s, <span class="keywordtype">int</span> ind = 0 );
<a name="l00025"></a>00025 <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCLraAdd.html#aa1d14054914f4333c90cf53a0d23de76">Make</a>(<a class="code" href="classLFSCProof.html">LFSCProof</a>* pf1, <a class="code" href="classLFSCProof.html">LFSCProof</a>* pf2, <span class="keywordtype">int</span> op1, <span class="keywordtype">int</span> op2);
<a name="l00026"></a><a class="code" href="classLFSCLraAdd.html#aff3aea69c6c937ddf277ae9c4a545a1a">00026</a> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCLraAdd.html#aff3aea69c6c937ddf277ae9c4a545a1a">clone</a>() { <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classLFSCLraAdd.html#a9724d04ec280ff9130b332f76a6051d1">LFSCLraAdd</a>( <a class="code" href="classLFSCLraAdd.html#ac6719308cb218ceb7298c05c26bc9eca">d_children</a>[0].<span class="keyword">get</span>(), <a class="code" href="classLFSCLraAdd.html#ac6719308cb218ceb7298c05c26bc9eca">d_children</a>[1].<span class="keyword">get</span>(), <a class="code" href="classLFSCLraAdd.html#afb25f59c4b8a73e1b4bea1f43d4b42c8">d_op1</a>, <a class="code" href="classLFSCLraAdd.html#a08bbcfafa29abbc7aafbfca31bafc878">d_op2</a> ); }
<a name="l00027"></a><a class="code" href="classLFSCLraAdd.html#a92ad459567cc680a6b0873ce39c893e0">00027</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCLraAdd.html#a92ad459567cc680a6b0873ce39c893e0">getNumChildren</a>() { <span class="keywordflow">return</span> 2; }
<a name="l00028"></a><a class="code" href="classLFSCLraAdd.html#a725352c47c99ff47e32957de18177df9">00028</a> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCLraAdd.html#a725352c47c99ff47e32957de18177df9">getChild</a>( <span class="keywordtype">int</span> n ) { <span class="keywordflow">return</span> <a class="code" href="classLFSCLraAdd.html#ac6719308cb218ceb7298c05c26bc9eca">d_children</a>[n].<a class="code" href="classRefPtr.html#a2b987fbb75b20a1da1bd959325635e7e">get</a>(); }
<a name="l00029"></a><a class="code" href="classLFSCLraAdd.html#ac8da622f5eb219b6258fe574a3992784">00029</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCLraAdd.html#ac8da622f5eb219b6258fe574a3992784">checkOp</a>() { <span class="keywordflow">return</span> <a class="code" href="Util_8cpp.html#a801074ec6fbda15a3cf5535e664ebff1">get_knd_result</a>( <a class="code" href="classLFSCLraAdd.html#afb25f59c4b8a73e1b4bea1f43d4b42c8">d_op1</a>, <a class="code" href="classLFSCLraAdd.html#a08bbcfafa29abbc7aafbfca31bafc878">d_op2</a> ); }
<a name="l00030"></a>00030 };
<a name="l00031"></a>00031
<a name="l00032"></a>00032
<a name="l00033"></a>00033 <span class="comment">// lra_~_axiom</span>
<a name="l00034"></a>00034
<a name="l00035"></a><a class="code" href="classLFSCLraAxiom.html">00035</a> <span class="keyword">class </span><a class="code" href="classLFSCLraAxiom.html">LFSCLraAxiom</a>: <span class="keyword">public</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>{
<a name="l00036"></a>00036 <span class="keyword">private</span>:
<a name="l00037"></a><a class="code" href="classLFSCLraAxiom.html#a0ca69fa241c154902481aca414233c63">00037</a> <span class="keyword">static</span> <a class="code" href="classRefPtr.html">RefPtr< LFSCProof ></a> <a class="code" href="classLFSCLraAxiom.html#a0ca69fa241c154902481aca414233c63">eq</a>;
<a name="l00038"></a><a class="code" href="classLFSCLraAxiom.html#aac2856c31f86b81c01c047a0767ec915">00038</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCLraAxiom.html#aac2856c31f86b81c01c047a0767ec915">d_op</a>;
<a name="l00039"></a><a class="code" href="classLFSCLraAxiom.html#a47d22d436209e94a4f609a22ef3e9169">00039</a> <a class="code" href="classCVC3_1_1Rational.html">Rational</a> <a class="code" href="classLFSCLraAxiom.html#a47d22d436209e94a4f609a22ef3e9169">d_r</a>;
<a name="l00040"></a><a class="code" href="classLFSCLraAxiom.html#a6fab77061a7a774bac25d9c85bd0c051">00040</a> <a class="code" href="classLFSCLraAxiom.html#a6fab77061a7a774bac25d9c85bd0c051">LFSCLraAxiom</a>(<span class="keywordtype">int</span> op ) : <a class="code" href="classLFSCProof.html">LFSCProof</a>(), <a class="code" href="classLFSCLraAxiom.html#aac2856c31f86b81c01c047a0767ec915">d_op</a>(op){}
<a name="l00041"></a><a class="code" href="classLFSCLraAxiom.html#a93b740ae623337198c5ca448bfdde844">00041</a> <a class="code" href="classLFSCLraAxiom.html#a6fab77061a7a774bac25d9c85bd0c051">LFSCLraAxiom</a>(<span class="keywordtype">int</span> op, <a class="code" href="classCVC3_1_1Rational.html">Rational</a> r): <a class="code" href="classLFSCProof.html">LFSCProof</a>(),
<a name="l00042"></a>00042 <a class="code" href="classLFSCLraAxiom.html#aac2856c31f86b81c01c047a0767ec915">d_op</a>(op),
<a name="l00043"></a>00043 <a class="code" href="classLFSCLraAxiom.html#a47d22d436209e94a4f609a22ef3e9169">d_r</a>(r){}
<a name="l00044"></a><a class="code" href="classLFSCLraAxiom.html#a07741ac6ae75b7f167b1040454bf1adb">00044</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCLraAxiom.html#a07741ac6ae75b7f167b1040454bf1adb">~LFSCLraAxiom</a>(){}
<a name="l00045"></a><a class="code" href="classLFSCLraAxiom.html#ad33974a576d8c078bbe6a1a65590f6eb">00045</a> <span class="keywordtype">long</span> <span class="keywordtype">int</span> <a class="code" href="classLFSCLraAxiom.html#ad33974a576d8c078bbe6a1a65590f6eb">get_length</a>(){ <span class="keywordflow">return</span> 15; }
<a name="l00046"></a>00046 <span class="keyword">public</span>:
<a name="l00047"></a><a class="code" href="classLFSCLraAxiom.html#ac4fb660f4e21d9e6b73699687ad88eb8">00047</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCLraAxiom.html">LFSCLraAxiom</a>* <a class="code" href="classLFSCLraAxiom.html#ac4fb660f4e21d9e6b73699687ad88eb8">AsLFSCLraAxiom</a>(){ <span class="keywordflow">return</span> <span class="keyword">this</span>; }
<a name="l00048"></a>00048 <span class="keywordtype">void</span> <a class="code" href="classLFSCLraAxiom.html#a48603e9301acbd8b355ac92a6c4db0cd">print_pf</a>( std::ostream& s, <span class="keywordtype">int</span> ind = 0 );
<a name="l00049"></a><a class="code" href="classLFSCLraAxiom.html#a46689ab969bc06af37c9e139d5f98f2e">00049</a> <span class="keywordtype">bool</span> <a class="code" href="classLFSCLraAxiom.html#a46689ab969bc06af37c9e139d5f98f2e">isTrivial</a>() { <span class="keywordflow">return</span> <a class="code" href="classLFSCLraAxiom.html#aac2856c31f86b81c01c047a0767ec915">d_op</a>==<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9efdc855f3c1477957fb50affec07f8f">EQ</a>; }
<a name="l00050"></a>00050 <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCLraAxiom.html#aa66e0ed64485094885554d14f6129112">MakeEq</a>();
<a name="l00051"></a><a class="code" href="classLFSCLraAxiom.html#ae8250c8db4183085e62a5b0c5966127a">00051</a> <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCLraAxiom.html#ae8250c8db4183085e62a5b0c5966127a">Make</a>( <a class="code" href="classCVC3_1_1Rational.html">Rational</a> r, <span class="keywordtype">int</span> op ){ <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classLFSCLraAxiom.html#a6fab77061a7a774bac25d9c85bd0c051">LFSCLraAxiom</a>( op,r ); }
<a name="l00052"></a><a class="code" href="classLFSCLraAxiom.html#a335fef727fe4f6c89b94c4f6f199297f">00052</a> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCLraAxiom.html#a335fef727fe4f6c89b94c4f6f199297f">clone</a>() { <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classLFSCLraAxiom.html#a6fab77061a7a774bac25d9c85bd0c051">LFSCLraAxiom</a>( <a class="code" href="classLFSCLraAxiom.html#aac2856c31f86b81c01c047a0767ec915">d_op</a>, <a class="code" href="classLFSCLraAxiom.html#a47d22d436209e94a4f609a22ef3e9169">d_r</a> ); }
<a name="l00053"></a><a class="code" href="classLFSCLraAxiom.html#aa371ea95da1f4044a286f23f52cfead6">00053</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCLraAxiom.html#aa371ea95da1f4044a286f23f52cfead6">checkOp</a>() { <span class="keywordflow">return</span> <a class="code" href="classLFSCLraAxiom.html#aac2856c31f86b81c01c047a0767ec915">d_op</a>; }
<a name="l00054"></a>00054 };
<a name="l00055"></a>00055
<a name="l00056"></a>00056
<a name="l00057"></a>00057 <span class="comment">// lra_mult_c</span>
<a name="l00058"></a><a class="code" href="classLFSCLraMulC.html">00058</a> <span class="keyword">class </span><a class="code" href="classLFSCLraMulC.html">LFSCLraMulC</a>: <span class="keyword">public</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>{
<a name="l00059"></a>00059 <span class="keyword">private</span>:
<a name="l00060"></a><a class="code" href="classLFSCLraMulC.html#aed28c2bba2487f155b4f536526603047">00060</a> <a class="code" href="classRefPtr.html">RefPtr< LFSCProof ></a> <a class="code" href="classLFSCLraMulC.html#aed28c2bba2487f155b4f536526603047">d_pf</a>;
<a name="l00061"></a><a class="code" href="classLFSCLraMulC.html#a490a2ef1271a491509ab625033fd9713">00061</a> <a class="code" href="classCVC3_1_1Rational.html">Rational</a> <a class="code" href="classLFSCLraMulC.html#a490a2ef1271a491509ab625033fd9713">d_r</a>;
<a name="l00062"></a><a class="code" href="classLFSCLraMulC.html#a23906851fdc8d8093a1e01fa6d2ba2cc">00062</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCLraMulC.html#a23906851fdc8d8093a1e01fa6d2ba2cc">d_op</a>; <span class="comment">// = | > | >= | distinct</span>
<a name="l00063"></a><a class="code" href="classLFSCLraMulC.html#ac6b96c5fd8fbc5099b751b373edc7141">00063</a> <a class="code" href="classLFSCLraMulC.html#ac6b96c5fd8fbc5099b751b373edc7141">LFSCLraMulC</a>(<a class="code" href="classLFSCProof.html">LFSCProof</a>* pf, <a class="code" href="classCVC3_1_1Rational.html">Rational</a> r, <span class="keywordtype">int</span> op): <a class="code" href="classLFSCProof.html">LFSCProof</a>(),
<a name="l00064"></a>00064 <a class="code" href="classLFSCLraMulC.html#aed28c2bba2487f155b4f536526603047">d_pf</a>(pf),
<a name="l00065"></a>00065 <a class="code" href="classLFSCLraMulC.html#a490a2ef1271a491509ab625033fd9713">d_r</a>(r),
<a name="l00066"></a>00066 <a class="code" href="classLFSCLraMulC.html#a23906851fdc8d8093a1e01fa6d2ba2cc">d_op</a>(op){
<a name="l00067"></a>00067 <a class="code" href="classLFSCLraMulC.html#a23906851fdc8d8093a1e01fa6d2ba2cc">d_op</a> = pf-><a class="code" href="classLFSCProof.html#a8bb7d43de0773db524227b1c2af54bb0">checkOp</a>() != -1 ? pf-><a class="code" href="classLFSCProof.html#a8bb7d43de0773db524227b1c2af54bb0">checkOp</a>() : <a class="code" href="classLFSCLraMulC.html#a23906851fdc8d8093a1e01fa6d2ba2cc">d_op</a>;
<a name="l00068"></a>00068 }
<a name="l00069"></a><a class="code" href="classLFSCLraMulC.html#adcd34de56620e8c3c6c40af545a34290">00069</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCLraMulC.html#adcd34de56620e8c3c6c40af545a34290">~LFSCLraMulC</a>(){}
<a name="l00070"></a><a class="code" href="classLFSCLraMulC.html#ab1de62b88ec2355fed8f496c2b23cc2d">00070</a> <span class="keywordtype">long</span> <span class="keywordtype">int</span> <a class="code" href="classLFSCLraMulC.html#ab1de62b88ec2355fed8f496c2b23cc2d">get_length</a>(){ <span class="keywordflow">return</span> 20 + <a class="code" href="classLFSCLraMulC.html#aed28c2bba2487f155b4f536526603047">d_pf</a>->get_string_length(); }
<a name="l00071"></a>00071 <span class="keyword">public</span>:
<a name="l00072"></a><a class="code" href="classLFSCLraMulC.html#abcf992e31f8c3d27d007a58e0b979a31">00072</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCLraMulC.html">LFSCLraMulC</a>* <a class="code" href="classLFSCLraMulC.html#abcf992e31f8c3d27d007a58e0b979a31">AsLFSCLraMulC</a>(){ <span class="keywordflow">return</span> <span class="keyword">this</span>; }
<a name="l00073"></a><a class="code" href="classLFSCLraMulC.html#a748192deaf801da5721da450dce18e13">00073</a> <span class="keywordtype">bool</span> <a class="code" href="classLFSCLraMulC.html#a748192deaf801da5721da450dce18e13">isLraMulC</a>() { <span class="keywordflow">return</span> <span class="keyword">true</span>; }
<a name="l00074"></a>00074 <span class="keywordtype">void</span> <a class="code" href="classLFSCLraMulC.html#a2bf14817557003c1c3f07b7e6bc61796">print_pf</a>( std::ostream& s, <span class="keywordtype">int</span> ind = 0 );
<a name="l00075"></a>00075 <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCLraMulC.html#ab2262ccc40a6212bbc9182700a2b0e73">Make</a>(<a class="code" href="classLFSCProof.html">LFSCProof</a>* pf, <a class="code" href="classCVC3_1_1Rational.html">Rational</a> r, <span class="keywordtype">int</span> op);
<a name="l00076"></a><a class="code" href="classLFSCLraMulC.html#ab781508a39b0d77c42b0b1899fa8d52e">00076</a> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCLraMulC.html#ab781508a39b0d77c42b0b1899fa8d52e">clone</a>() { <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classLFSCLraMulC.html#ac6b96c5fd8fbc5099b751b373edc7141">LFSCLraMulC</a>( <a class="code" href="classLFSCLraMulC.html#aed28c2bba2487f155b4f536526603047">d_pf</a>.<a class="code" href="classRefPtr.html#a2b987fbb75b20a1da1bd959325635e7e">get</a>(), <a class="code" href="classLFSCLraMulC.html#a490a2ef1271a491509ab625033fd9713">d_r</a>, <a class="code" href="classLFSCLraMulC.html#a23906851fdc8d8093a1e01fa6d2ba2cc">d_op</a> ); }
<a name="l00077"></a><a class="code" href="classLFSCLraMulC.html#a21a98611a0b197c990a28200d46774c1">00077</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCLraMulC.html#a21a98611a0b197c990a28200d46774c1">getNumChildren</a>() { <span class="keywordflow">return</span> 1; }
<a name="l00078"></a><a class="code" href="classLFSCLraMulC.html#a8947cecdeaa2f3501f1fe07203f3f15e">00078</a> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCLraMulC.html#a8947cecdeaa2f3501f1fe07203f3f15e">getChild</a>( <span class="keywordtype">int</span> n ) { <span class="keywordflow">return</span> <a class="code" href="classLFSCLraMulC.html#aed28c2bba2487f155b4f536526603047">d_pf</a>.<a class="code" href="classRefPtr.html#a2b987fbb75b20a1da1bd959325635e7e">get</a>(); }
<a name="l00079"></a><a class="code" href="classLFSCLraMulC.html#ade7db00f45b31f5f4cf8df1d3c5b255c">00079</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCLraMulC.html#ade7db00f45b31f5f4cf8df1d3c5b255c">checkOp</a>() { <span class="keywordflow">return</span> <a class="code" href="classLFSCLraMulC.html#a23906851fdc8d8093a1e01fa6d2ba2cc">d_op</a>; }
<a name="l00080"></a>00080 };
<a name="l00081"></a>00081
<a name="l00082"></a>00082
<a name="l00083"></a>00083 <span class="comment">// lra_sub_~_~</span>
<a name="l00084"></a><a class="code" href="classLFSCLraSub.html">00084</a> <span class="keyword">class </span><a class="code" href="classLFSCLraSub.html">LFSCLraSub</a>: <span class="keyword">public</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>{
<a name="l00085"></a>00085 <span class="keyword">private</span>:
<a name="l00086"></a><a class="code" href="classLFSCLraSub.html#ad94dea36a4e215e4f6d6ffc8c773ff69">00086</a> <a class="code" href="classRefPtr.html">RefPtr< LFSCProof ></a> <a class="code" href="classLFSCLraSub.html#ad94dea36a4e215e4f6d6ffc8c773ff69">d_children</a>[2];
<a name="l00087"></a><a class="code" href="classLFSCLraSub.html#a59044704622ff8cf4a328f2561e5739f">00087</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCLraSub.html#acfa4dc578e51efaa96bdae49830879a1">d_op1</a>, <a class="code" href="classLFSCLraSub.html#a59044704622ff8cf4a328f2561e5739f">d_op2</a>;
<a name="l00088"></a><a class="code" href="classLFSCLraSub.html#afd42d8df24158087e418c8b948caa0b1">00088</a> <a class="code" href="classLFSCLraSub.html#afd42d8df24158087e418c8b948caa0b1">LFSCLraSub</a>(<a class="code" href="classLFSCProof.html">LFSCProof</a>* pf1, <a class="code" href="classLFSCProof.html">LFSCProof</a>* pf2, <span class="keywordtype">int</span> op1, <span class="keywordtype">int</span> op2): <a class="code" href="classLFSCProof.html">LFSCProof</a>(),
<a name="l00089"></a>00089 <a class="code" href="classLFSCLraSub.html#acfa4dc578e51efaa96bdae49830879a1">d_op1</a>(op1),
<a name="l00090"></a>00090 <a class="code" href="classLFSCLraSub.html#a59044704622ff8cf4a328f2561e5739f">d_op2</a>(op2){
<a name="l00091"></a>00091 <a class="code" href="classLFSCLraSub.html#ad94dea36a4e215e4f6d6ffc8c773ff69">d_children</a>[0] = pf1;
<a name="l00092"></a>00092 <a class="code" href="classLFSCLraSub.html#ad94dea36a4e215e4f6d6ffc8c773ff69">d_children</a>[1] = pf2;
<a name="l00093"></a>00093 <a class="code" href="classLFSCLraSub.html#acfa4dc578e51efaa96bdae49830879a1">d_op1</a> = pf1-><a class="code" href="classLFSCProof.html#a8bb7d43de0773db524227b1c2af54bb0">checkOp</a>()!=-1 ? pf1-><a class="code" href="classLFSCProof.html#a8bb7d43de0773db524227b1c2af54bb0">checkOp</a>() : <a class="code" href="classLFSCLraSub.html#acfa4dc578e51efaa96bdae49830879a1">d_op1</a>;
<a name="l00094"></a>00094 <a class="code" href="classLFSCLraSub.html#a59044704622ff8cf4a328f2561e5739f">d_op2</a> = pf2-><a class="code" href="classLFSCProof.html#a8bb7d43de0773db524227b1c2af54bb0">checkOp</a>()!=-1 ? pf2-><a class="code" href="classLFSCProof.html#a8bb7d43de0773db524227b1c2af54bb0">checkOp</a>() : <a class="code" href="classLFSCLraSub.html#a59044704622ff8cf4a328f2561e5739f">d_op2</a>;
<a name="l00095"></a>00095 }
<a name="l00096"></a><a class="code" href="classLFSCLraSub.html#a8ea4642b00395358b117855d9c191ff4">00096</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCLraSub.html#a8ea4642b00395358b117855d9c191ff4">~LFSCLraSub</a>(){}
<a name="l00097"></a><a class="code" href="classLFSCLraSub.html#a20fbc15d7eb7c372678b281d4caabd0a">00097</a> <span class="keywordtype">long</span> <span class="keywordtype">int</span> <a class="code" href="classLFSCLraSub.html#a20fbc15d7eb7c372678b281d4caabd0a">get_length</a>(){
<a name="l00098"></a>00098 <span class="keywordflow">return</span> 20 + <a class="code" href="classLFSCLraSub.html#ad94dea36a4e215e4f6d6ffc8c773ff69">d_children</a>[0]->get_string_length() + <a class="code" href="classLFSCLraSub.html#ad94dea36a4e215e4f6d6ffc8c773ff69">d_children</a>[1]->get_string_length();
<a name="l00099"></a>00099 }
<a name="l00100"></a>00100 <span class="keyword">public</span>:
<a name="l00101"></a><a class="code" href="classLFSCLraSub.html#a967e3068a4e96821799f447812bcc932">00101</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCLraSub.html">LFSCLraSub</a>* <a class="code" href="classLFSCLraSub.html#a967e3068a4e96821799f447812bcc932">AsLFSCLraSub</a>(){ <span class="keywordflow">return</span> <span class="keyword">this</span>; }
<a name="l00102"></a>00102 <span class="keywordtype">void</span> <a class="code" href="classLFSCLraSub.html#a636294ce853f360b1813b6547cb8d37c">print_pf</a>( std::ostream& s, <span class="keywordtype">int</span> ind = 0 );
<a name="l00103"></a>00103 <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCLraSub.html#a66b3327a7dadc49a0e072b6d1f6f6289">Make</a>(<a class="code" href="classLFSCProof.html">LFSCProof</a>* pf1, <a class="code" href="classLFSCProof.html">LFSCProof</a>* pf2, <span class="keywordtype">int</span> op1, <span class="keywordtype">int</span> op2);
<a name="l00104"></a><a class="code" href="classLFSCLraSub.html#aca5efb16b2920eea3c4e7a1ebd31ad30">00104</a> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCLraSub.html#aca5efb16b2920eea3c4e7a1ebd31ad30">clone</a>() { <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classLFSCLraSub.html#afd42d8df24158087e418c8b948caa0b1">LFSCLraSub</a>( <a class="code" href="classLFSCLraSub.html#ad94dea36a4e215e4f6d6ffc8c773ff69">d_children</a>[0].<span class="keyword">get</span>(), <a class="code" href="classLFSCLraSub.html#ad94dea36a4e215e4f6d6ffc8c773ff69">d_children</a>[1].<span class="keyword">get</span>(), <a class="code" href="classLFSCLraSub.html#acfa4dc578e51efaa96bdae49830879a1">d_op1</a>, <a class="code" href="classLFSCLraSub.html#a59044704622ff8cf4a328f2561e5739f">d_op2</a> ); }
<a name="l00105"></a><a class="code" href="classLFSCLraSub.html#a4dc6c463232726a4e5d9c0fd9bc512b0">00105</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCLraSub.html#a4dc6c463232726a4e5d9c0fd9bc512b0">getNumChildren</a>() { <span class="keywordflow">return</span> 2; }
<a name="l00106"></a><a class="code" href="classLFSCLraSub.html#abb598f94655a242f379e036f4a343f0c">00106</a> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCLraSub.html#abb598f94655a242f379e036f4a343f0c">getChild</a>( <span class="keywordtype">int</span> n ) { <span class="keywordflow">return</span> <a class="code" href="classLFSCLraSub.html#ad94dea36a4e215e4f6d6ffc8c773ff69">d_children</a>[n].<a class="code" href="classRefPtr.html#a2b987fbb75b20a1da1bd959325635e7e">get</a>(); }
<a name="l00107"></a><a class="code" href="classLFSCLraSub.html#a5c5b56cfc4a9f44971325de01ac28669">00107</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCLraSub.html#a5c5b56cfc4a9f44971325de01ac28669">checkOp</a>() { <span class="keywordflow">return</span> <a class="code" href="Util_8cpp.html#a801074ec6fbda15a3cf5535e664ebff1">get_knd_result</a>( <a class="code" href="classLFSCLraSub.html#acfa4dc578e51efaa96bdae49830879a1">d_op1</a>, <a class="code" href="classLFSCLraSub.html#a59044704622ff8cf4a328f2561e5739f">d_op2</a> ); }
<a name="l00108"></a>00108 };
<a name="l00109"></a>00109
<a name="l00110"></a><a class="code" href="classLFSCLraPoly.html">00110</a> <span class="keyword">class </span><a class="code" href="classLFSCLraPoly.html">LFSCLraPoly</a> : <span class="keyword">public</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>
<a name="l00111"></a>00111 {
<a name="l00112"></a>00112 <span class="keyword">private</span>:
<a name="l00113"></a><a class="code" href="classLFSCLraPoly.html#a088b97fe13460e7ab5240f6484606033">00113</a> <a class="code" href="classRefPtr.html">RefPtr< LFSCProof ></a> <a class="code" href="classLFSCLraPoly.html#a088b97fe13460e7ab5240f6484606033">d_pf</a>;
<a name="l00114"></a><a class="code" href="classLFSCLraPoly.html#a29115b181eddb84f4958b9b729a13990">00114</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCLraPoly.html#a29115b181eddb84f4958b9b729a13990">d_var</a>;
<a name="l00115"></a><a class="code" href="classLFSCLraPoly.html#a5ce29cb2c6cb3955220e54be0a5d91af">00115</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCLraPoly.html#a5ce29cb2c6cb3955220e54be0a5d91af">d_op</a>;
<a name="l00116"></a><a class="code" href="classLFSCLraPoly.html#a50105ea931049364352ebe97dbd03705">00116</a> <a class="code" href="classLFSCLraPoly.html#a50105ea931049364352ebe97dbd03705">LFSCLraPoly</a>( <a class="code" href="classLFSCProof.html">LFSCProof</a>* pf, <span class="keywordtype">int</span> var, <span class="keywordtype">int</span> op ) : <a class="code" href="classLFSCProof.html">LFSCProof</a>(),
<a name="l00117"></a>00117 <a class="code" href="classLFSCLraPoly.html#a088b97fe13460e7ab5240f6484606033">d_pf</a>( pf ),
<a name="l00118"></a>00118 <a class="code" href="classLFSCLraPoly.html#a29115b181eddb84f4958b9b729a13990">d_var</a>( var ),
<a name="l00119"></a>00119 <a class="code" href="classLFSCLraPoly.html#a5ce29cb2c6cb3955220e54be0a5d91af">d_op</a>( op ){
<a name="l00120"></a>00120 <a class="code" href="classLFSCLraPoly.html#a5ce29cb2c6cb3955220e54be0a5d91af">d_op</a> = pf-><a class="code" href="classLFSCProof.html#a8bb7d43de0773db524227b1c2af54bb0">checkOp</a>() != -1 ? pf-><a class="code" href="classLFSCProof.html#a8bb7d43de0773db524227b1c2af54bb0">checkOp</a>() : <a class="code" href="classLFSCLraPoly.html#a5ce29cb2c6cb3955220e54be0a5d91af">d_op</a>;
<a name="l00121"></a>00121 }
<a name="l00122"></a><a class="code" href="classLFSCLraPoly.html#a578b4b2a22a07b3666af56a8ac1cff79">00122</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCLraPoly.html#a578b4b2a22a07b3666af56a8ac1cff79">~LFSCLraPoly</a>(){}
<a name="l00123"></a><a class="code" href="classLFSCLraPoly.html#a204461047f2b488c01841ce1dc4408cc">00123</a> <span class="keywordtype">long</span> <span class="keywordtype">int</span> <a class="code" href="classLFSCLraPoly.html#a204461047f2b488c01841ce1dc4408cc">get_length</a>(){ <span class="keywordflow">return</span> 15 + <a class="code" href="classLFSCLraPoly.html#a088b97fe13460e7ab5240f6484606033">d_pf</a>->get_string_length(); }
<a name="l00124"></a>00124 <span class="keyword">public</span>:
<a name="l00125"></a><a class="code" href="classLFSCLraPoly.html#ac608cb36f274f970de7ce3a395621203">00125</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCLraPoly.html">LFSCLraPoly</a>* <a class="code" href="classLFSCLraPoly.html#ac608cb36f274f970de7ce3a395621203">AsLFSCLraPoly</a>(){ <span class="keywordflow">return</span> <span class="keyword">this</span>; }
<a name="l00126"></a>00126 <span class="keywordtype">void</span> <a class="code" href="classLFSCLraPoly.html#a94af3dd8672407e26643aaec09e7bc49">print_pf</a>( std::ostream& s, <span class="keywordtype">int</span> ind = 0 );
<a name="l00127"></a><a class="code" href="classLFSCLraPoly.html#ac525239ecb136141bfa7e2b2f2b0391d">00127</a> <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCLraPoly.html#ac525239ecb136141bfa7e2b2f2b0391d">Make</a>( <a class="code" href="classLFSCProof.html">LFSCProof</a>* pf, <span class="keywordtype">int</span> var, <span class="keywordtype">int</span> op ){
<a name="l00128"></a>00128 <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classLFSCLraPoly.html#a50105ea931049364352ebe97dbd03705">LFSCLraPoly</a>( pf, var, op );
<a name="l00129"></a>00129 }
<a name="l00130"></a>00130 <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCLraPoly.html#ac525239ecb136141bfa7e2b2f2b0391d">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, <a class="code" href="classLFSCProof.html">LFSCProof</a>* p );
<a name="l00131"></a><a class="code" href="classLFSCLraPoly.html#a66f249a42dce384be16a1d58c243ea4a">00131</a> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCLraPoly.html#a66f249a42dce384be16a1d58c243ea4a">clone</a>() { <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classLFSCLraPoly.html#a50105ea931049364352ebe97dbd03705">LFSCLraPoly</a>( <a class="code" href="classLFSCLraPoly.html#a088b97fe13460e7ab5240f6484606033">d_pf</a>.<a class="code" href="classRefPtr.html#a2b987fbb75b20a1da1bd959325635e7e">get</a>(), <a class="code" href="classLFSCLraPoly.html#a29115b181eddb84f4958b9b729a13990">d_var</a>, <a class="code" href="classLFSCLraPoly.html#a5ce29cb2c6cb3955220e54be0a5d91af">d_op</a> ); }
<a name="l00132"></a><a class="code" href="classLFSCLraPoly.html#ad9bee6a3ddb3a58059b22dd7112e2496">00132</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCLraPoly.html#ad9bee6a3ddb3a58059b22dd7112e2496">getNumChildren</a>() { <span class="keywordflow">return</span> 1; }
<a name="l00133"></a><a class="code" href="classLFSCLraPoly.html#a5c7256d609c9be9b1dbccc1d0b401c30">00133</a> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCLraPoly.html#a5c7256d609c9be9b1dbccc1d0b401c30">getChild</a>( <span class="keywordtype">int</span> n ) { <span class="keywordflow">return</span> <a class="code" href="classLFSCLraPoly.html#a088b97fe13460e7ab5240f6484606033">d_pf</a>.<a class="code" href="classRefPtr.html#a2b987fbb75b20a1da1bd959325635e7e">get</a>(); }
<a name="l00134"></a><a class="code" href="classLFSCLraPoly.html#a38c685a24cc6d5cf395632a9077fa734">00134</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCLraPoly.html#a38c685a24cc6d5cf395632a9077fa734">checkOp</a>() {
<a name="l00135"></a>00135 <span class="keywordflow">return</span> <a class="code" href="Util_8cpp.html#a667a5939ed7f0fba1d9a06f52a674832">get_normalized</a>( <a class="code" href="classLFSCLraPoly.html#a5ce29cb2c6cb3955220e54be0a5d91af">d_op</a>, <a class="code" href="classLFSCLraPoly.html#a29115b181eddb84f4958b9b729a13990">d_var</a><0 );
<a name="l00136"></a>00136 }
<a name="l00137"></a>00137
<a name="l00138"></a>00138 };
<a name="l00139"></a>00139
<a name="l00140"></a><a class="code" href="classLFSCLraContra.html">00140</a> <span class="keyword">class </span><a class="code" href="classLFSCLraContra.html">LFSCLraContra</a> : <span class="keyword">public</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>
<a name="l00141"></a>00141 {
<a name="l00142"></a>00142 <span class="keyword">private</span>:
<a name="l00143"></a><a class="code" href="classLFSCLraContra.html#af43193d45dd28ef37661f1703bb7fbe0">00143</a> <a class="code" href="classRefPtr.html">RefPtr< LFSCProof ></a> <a class="code" href="classLFSCLraContra.html#af43193d45dd28ef37661f1703bb7fbe0">d_pf</a>;
<a name="l00144"></a><a class="code" href="classLFSCLraContra.html#aa7cda55c2cdd9d84a84d12a45238397b">00144</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCLraContra.html#aa7cda55c2cdd9d84a84d12a45238397b">d_op</a>;
<a name="l00145"></a><a class="code" href="classLFSCLraContra.html#a1fa648f3260212bef270de3f3a648419">00145</a> <a class="code" href="classLFSCLraContra.html#a1fa648f3260212bef270de3f3a648419">LFSCLraContra</a>( <a class="code" href="classLFSCProof.html">LFSCProof</a>* pf, <span class="keywordtype">int</span> op ) : <a class="code" href="classLFSCProof.html">LFSCProof</a>(),
<a name="l00146"></a>00146 <a class="code" href="classLFSCLraContra.html#af43193d45dd28ef37661f1703bb7fbe0">d_pf</a>( pf ),
<a name="l00147"></a>00147 <a class="code" href="classLFSCLraContra.html#aa7cda55c2cdd9d84a84d12a45238397b">d_op</a>( op ){
<a name="l00148"></a>00148 <a class="code" href="classLFSCLraContra.html#aa7cda55c2cdd9d84a84d12a45238397b">d_op</a> = pf-><a class="code" href="classLFSCProof.html#a8bb7d43de0773db524227b1c2af54bb0">checkOp</a>() != -1 ? pf-><a class="code" href="classLFSCProof.html#a8bb7d43de0773db524227b1c2af54bb0">checkOp</a>() : <a class="code" href="classLFSCLraContra.html#aa7cda55c2cdd9d84a84d12a45238397b">d_op</a>;
<a name="l00149"></a>00149 }
<a name="l00150"></a><a class="code" href="classLFSCLraContra.html#af1b23ec534978e98677a0eb8d140eff6">00150</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCLraContra.html#af1b23ec534978e98677a0eb8d140eff6">~LFSCLraContra</a>(){}
<a name="l00151"></a><a class="code" href="classLFSCLraContra.html#a0787be4effc2ca8551fb5d6ee0e9b88c">00151</a> <span class="keywordtype">long</span> <span class="keywordtype">int</span> <a class="code" href="classLFSCLraContra.html#a0787be4effc2ca8551fb5d6ee0e9b88c">get_length</a>(){ <span class="keywordflow">return</span> 15 + <a class="code" href="classLFSCLraContra.html#af43193d45dd28ef37661f1703bb7fbe0">d_pf</a>->get_string_length(); }
<a name="l00152"></a>00152 <span class="keyword">public</span>:
<a name="l00153"></a><a class="code" href="classLFSCLraContra.html#afe3e4873b5cf92408193cd0fc64858de">00153</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCLraContra.html">LFSCLraContra</a>* <a class="code" href="classLFSCLraContra.html#afe3e4873b5cf92408193cd0fc64858de">AsLFSCLraContra</a>(){ <span class="keywordflow">return</span> <span class="keyword">this</span>; }
<a name="l00154"></a><a class="code" href="classLFSCLraContra.html#a41be91fb05ac0a256e34461080eca14b">00154</a> <span class="keywordtype">void</span> <a class="code" href="classLFSCLraContra.html#a41be91fb05ac0a256e34461080eca14b">print_pf</a>( std::ostream& s, <span class="keywordtype">int</span> ind = 0 ){
<a name="l00155"></a>00155 s <<<span class="stringliteral">"(lra_contra_"</span> << <a class="code" href="Util_8cpp.html#af0ed1bf9d4012011aa2b42be9c26a0b5">kind_to_str</a>(<a class="code" href="classLFSCLraContra.html#aa7cda55c2cdd9d84a84d12a45238397b">d_op</a>) << <span class="stringliteral">" _ "</span>;
<a name="l00156"></a>00156 <a class="code" href="classLFSCLraContra.html#af43193d45dd28ef37661f1703bb7fbe0">d_pf</a>->print( s, ind+1 );
<a name="l00157"></a>00157 s << <span class="stringliteral">")"</span>;
<a name="l00158"></a>00158 }
<a name="l00159"></a><a class="code" href="classLFSCLraContra.html#aa561c53b9672b46c4490329b65b1f5fd">00159</a> <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCLraContra.html#aa561c53b9672b46c4490329b65b1f5fd">Make</a>( <a class="code" href="classLFSCProof.html">LFSCProof</a>* pf, <span class="keywordtype">int</span> op ){
<a name="l00160"></a>00160 <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classLFSCLraContra.html#a1fa648f3260212bef270de3f3a648419">LFSCLraContra</a>( pf, op );
<a name="l00161"></a>00161 }
<a name="l00162"></a><a class="code" href="classLFSCLraContra.html#ae33a5e48d100094da883af525acc7d66">00162</a> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCLraContra.html#ae33a5e48d100094da883af525acc7d66">clone</a>() { <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classLFSCLraContra.html#a1fa648f3260212bef270de3f3a648419">LFSCLraContra</a>( <a class="code" href="classLFSCLraContra.html#af43193d45dd28ef37661f1703bb7fbe0">d_pf</a>.<a class="code" href="classRefPtr.html#a2b987fbb75b20a1da1bd959325635e7e">get</a>(), <a class="code" href="classLFSCLraContra.html#aa7cda55c2cdd9d84a84d12a45238397b">d_op</a> ); }
<a name="l00163"></a><a class="code" href="classLFSCLraContra.html#a6220f85da35d769ae06b46cfce82e636">00163</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCLraContra.html#a6220f85da35d769ae06b46cfce82e636">getNumChildren</a>() { <span class="keywordflow">return</span> 1; }
<a name="l00164"></a><a class="code" href="classLFSCLraContra.html#a11dfd0ee07e2707db165a87697c8c8f3">00164</a> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCLraContra.html#a11dfd0ee07e2707db165a87697c8c8f3">getChild</a>( <span class="keywordtype">int</span> n ) { <span class="keywordflow">return</span> <a class="code" href="classLFSCLraContra.html#af43193d45dd28ef37661f1703bb7fbe0">d_pf</a>.<a class="code" href="classRefPtr.html#a2b987fbb75b20a1da1bd959325635e7e">get</a>(); }
<a name="l00165"></a><a class="code" href="classLFSCLraContra.html#a9fcfcdf0bb6470616c36d8e9b61c3fa6">00165</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCLraContra.html#a9fcfcdf0bb6470616c36d8e9b61c3fa6">checkOp</a>() { <span class="keywordflow">return</span> <a class="code" href="classLFSCLraContra.html#aa7cda55c2cdd9d84a84d12a45238397b">d_op</a>; }
<a name="l00166"></a>00166 };
<a name="l00167"></a>00167
<a name="l00168"></a>00168
<a name="l00169"></a>00169 <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>
