<!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 Class Reference</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 class="current"><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="annotated.html"><span>Class List</span></a></li>
<li><a href="classes.html"><span>Class Index</span></a></li>
<li><a href="hierarchy.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
</div>
<div class="header">
<div class="summary">
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pub-static-methods">Static Public Member Functions</a> |
<a href="#pro-methods">Protected Member Functions</a> |
<a href="#pro-attribs">Protected Attributes</a> |
<a href="#pro-static-attribs">Static Protected Attributes</a> |
<a href="#friends">Friends</a> </div>
<div class="headertitle">
<div class="title">LFSCProof Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="LFSCProof" --><!-- doxytag: inherits="LFSCObj" -->
<p><code>#include <<a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>></code></p>
<div class="dynheader">
Inheritance diagram for LFSCProof:</div>
<div class="dyncontent">
<div class="center">
<img src="classLFSCProof.png" usemap="#LFSCProof_map" alt=""/>
<map id="LFSCProof_map" name="LFSCProof_map">
<area href="classLFSCObj.html" alt="LFSCObj" shape="rect" coords="0,56,120,80"/>
<area href="classObj.html" alt="Obj" shape="rect" coords="0,0,120,24"/>
<area href="classLFSCAssume.html" alt="LFSCAssume" shape="rect" coords="130,168,250,192"/>
<area href="classLFSCBoolRes.html" alt="LFSCBoolRes" shape="rect" coords="130,224,250,248"/>
<area href="classLFSCClausify.html" alt="LFSCClausify" shape="rect" coords="130,280,250,304"/>
<area href="classLFSCLem.html" alt="LFSCLem" shape="rect" coords="130,336,250,360"/>
<area href="classLFSCLraAdd.html" alt="LFSCLraAdd" shape="rect" coords="130,392,250,416"/>
<area href="classLFSCLraAxiom.html" alt="LFSCLraAxiom" shape="rect" coords="130,448,250,472"/>
<area href="classLFSCLraContra.html" alt="LFSCLraContra" shape="rect" coords="130,504,250,528"/>
<area href="classLFSCLraMulC.html" alt="LFSCLraMulC" shape="rect" coords="130,560,250,584"/>
<area href="classLFSCLraPoly.html" alt="LFSCLraPoly" shape="rect" coords="130,616,250,640"/>
<area href="classLFSCLraSub.html" alt="LFSCLraSub" shape="rect" coords="130,672,250,696"/>
<area href="classLFSCPfLambda.html" alt="LFSCPfLambda" shape="rect" coords="130,728,250,752"/>
<area href="classLFSCPfLet.html" alt="LFSCPfLet" shape="rect" coords="130,784,250,808"/>
<area href="classLFSCPfVar.html" alt="LFSCPfVar" shape="rect" coords="130,840,250,864"/>
<area href="classLFSCProofExpr.html" alt="LFSCProofExpr" shape="rect" coords="130,896,250,920"/>
<area href="classLFSCProofGeneric.html" alt="LFSCProofGeneric" shape="rect" coords="130,952,250,976"/>
</map>
</div></div>
<p><a href="classLFSCProof-members.html">List of all members.</a></p>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li>virtual <a class="el" href="classLFSCProofExpr.html">LFSCProofExpr</a> * <a class="el" href="classLFSCProof.html#ae1a19870033df1a9656e54ca2e4c21a6">AsLFSCProofExpr</a> ()
<li>virtual <a class="el" href="classLFSCLraAdd.html">LFSCLraAdd</a> * <a class="el" href="classLFSCProof.html#a7cc0f70e22642f958d58bdcebcd06530">AsLFSCLraAdd</a> ()
<li>virtual <a class="el" href="classLFSCLraSub.html">LFSCLraSub</a> * <a class="el" href="classLFSCProof.html#a60be4bca8e5d7487bd19f391b675d49b">AsLFSCLraSub</a> ()
<li>virtual <a class="el" href="classLFSCLraMulC.html">LFSCLraMulC</a> * <a class="el" href="classLFSCProof.html#a87f99538036f96fd800bc97049478af2">AsLFSCLraMulC</a> ()
<li>virtual <a class="el" href="classLFSCLraAxiom.html">LFSCLraAxiom</a> * <a class="el" href="classLFSCProof.html#a9b6a71f2857c0bbdd2689aa3665657da">AsLFSCLraAxiom</a> ()
<li>virtual <a class="el" href="classLFSCLraContra.html">LFSCLraContra</a> * <a class="el" href="classLFSCProof.html#a52f0d889a8439f484b1995ae2536a671">AsLFSCLraContra</a> ()
<li>virtual <a class="el" href="classLFSCLraPoly.html">LFSCLraPoly</a> * <a class="el" href="classLFSCProof.html#a13a5d84e3c02842c331c0093689edd58">AsLFSCLraPoly</a> ()
<li>virtual <a class="el" href="classLFSCBoolRes.html">LFSCBoolRes</a> * <a class="el" href="classLFSCProof.html#a6b5678c20b54da5345d66b595a33a719">AsLFSCBoolRes</a> ()
<li>virtual <a class="el" href="classLFSCLem.html">LFSCLem</a> * <a class="el" href="classLFSCProof.html#a35b9ae21403a09523359d96d182c7431">AsLFSCLem</a> ()
<li>virtual <a class="el" href="classLFSCClausify.html">LFSCClausify</a> * <a class="el" href="classLFSCProof.html#a1ae53259bdc504ba263e86b0d85ccede">AsLFSCClausify</a> ()
<li>virtual <a class="el" href="classLFSCAssume.html">LFSCAssume</a> * <a class="el" href="classLFSCProof.html#a090256e5ceadaccaa46826689f95f238">AsLFSCAssume</a> ()
<li>virtual <a class="el" href="classLFSCProofGeneric.html">LFSCProofGeneric</a> * <a class="el" href="classLFSCProof.html#a11df493e82f924825e42d2bcef64c1f6">AsLFSCProofGeneric</a> ()
<li>virtual <a class="el" href="classLFSCPfVar.html">LFSCPfVar</a> * <a class="el" href="classLFSCProof.html#a3204930c32bc4a67ec0ddb23b3be51be">AsLFSCPfVar</a> ()
<li>virtual <a class="el" href="classLFSCPfLambda.html">LFSCPfLambda</a> * <a class="el" href="classLFSCProof.html#ad56845dc18ff11a9a054c7137ce5a680">AsLFSCPfLambda</a> ()
<li>virtual <a class="el" href="classLFSCPfLet.html">LFSCPfLet</a> * <a class="el" href="classLFSCProof.html#aefd45e8a659276c68dd2797a995ffc87">AsLFSCPfLet</a> ()
<li>virtual bool <a class="el" href="classLFSCProof.html#aa1dbda64d42f7bf7c81a1b6e68da2766">isLraMulC</a> ()
<li>void <a class="el" href="classLFSCProof.html#aed472da83c57ed8a1ac6d2a6bc34eeba">print</a> (std::ostream &s, int ind=0)
<li>virtual void <a class="el" href="classLFSCProof.html#a9ad1d738b10d731108f63b9d86796c00">print_pf</a> (std::ostream &s, int ind=0)=0
<li>virtual bool <a class="el" href="classLFSCProof.html#a094c8c12bcb8ee3b1ec7a51b5568c355">isTrivial</a> ()
<li>long int <a class="el" href="classLFSCProof.html#a784c4a1295785719bce419d3e9ee9be1">get_string_length</a> ()
<li>void <a class="el" href="classLFSCProof.html#ae135f7109d7cc2a9185a48487840b683">print_structure</a> (std::ostream &s, int ind=0)
<li>virtual void <a class="el" href="classLFSCProof.html#a989d58a3910834809ddbfc89c04f6d87">print_struct</a> (std::ostream &s, int ind=0)
<li>void <a class="el" href="classLFSCProof.html#ae8e4007daade52b31f52182192d46abc">setRplProof</a> (<a class="el" href="classLFSCProof.html">LFSCProof</a> *p)
<li>virtual void <a class="el" href="classLFSCProof.html#ada9a53bcd04fe712b1fc22f9a0a23ccc">fillHoles</a> ()
<li>virtual <a class="el" href="classLFSCProof.html">LFSCProof</a> * <a class="el" href="classLFSCProof.html#a0fff5e24b97c44080514e3ec6f15d751">clone</a> ()=0
<li>virtual int <a class="el" href="classLFSCProof.html#aedc30ad27db2049d1e6782918bdc2608">getNumChildren</a> ()
<li>virtual <a class="el" href="classLFSCProof.html">LFSCProof</a> * <a class="el" href="classLFSCProof.html#ac60cfef82cf6aaa935668cbfab2ecd10">getChild</a> (int n)
<li>virtual int <a class="el" href="classLFSCProof.html#a8bb7d43de0773db524227b1c2af54bb0">checkOp</a> ()
<li>int <a class="el" href="classLFSCProof.html#a6b95ef9fff90f5410755fdb628c6897c">getChOp</a> ()
<li>void <a class="el" href="classLFSCProof.html#a5152d42d473b2305cae68012da611208">setChOp</a> (int c)
<li>virtual int <a class="el" href="classLFSCProof.html#a46af0498dd659ccba0549191102cf75d">checkBoolRes</a> (std::vector< int > &clause)
</ul>
<h2><a name="pub-static-methods"></a>
Static Public Member Functions</h2>
<ul>
<li>static int <a class="el" href="classLFSCProof.html#a396c41fc6012caf4dde358af52d25905">make_lambda</a> (<a class="el" href="classLFSCProof.html">LFSCProof</a> *p)
<li>static <a class="el" href="classLFSCProof.html">LFSCProof</a> * <a class="el" href="classLFSCProof.html#ab1b22c672f110e3f9abe22b2bf377fb3">Make_CNF</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &form, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &reason, int pos)
<li>static <a class="el" href="classLFSCProof.html">LFSCProof</a> * <a class="el" href="classLFSCProof.html#a95e3c7629c196ed189ad0525304e48cb">Make_not_not_elim</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &pf, <a class="el" href="classLFSCProof.html">LFSCProof</a> *p)
<li>static <a class="el" href="classLFSCProof.html">LFSCProof</a> * <a class="el" href="classLFSCProof.html#a979135fb775da82a9bf06befd9def730">Make_mimic</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &pf, <a class="el" href="classLFSCProof.html">LFSCProof</a> *p, int numHoles)
<li>static <a class="el" href="classLFSCProof.html">LFSCProof</a> * <a class="el" href="classLFSCProof.html#a547ec01104eb074ab2eb4f25ea9435e0">Make_and_elim</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &form, <a class="el" href="classLFSCProof.html">LFSCProof</a> *p, int n, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &expected)
<li>static int <a class="el" href="classLFSCProof.html#a43144544220e21b8519c959973a35c49">get_proof_counter</a> ()
</ul>
<h2><a name="pro-methods"></a>
Protected Member Functions</h2>
<ul>
<li><a class="el" href="classLFSCProof.html#a08258b1a59261c0dd0edcd775a883cfc">LFSCProof</a> ()
<li>virtual long int <a class="el" href="classLFSCProof.html#a4f6cb66f81baeb838874bfc2ee51595e">get_length</a> ()
<li>virtual <a class="el" href="classLFSCProof.html#a734881b4ad199d3251973cc844a18929">~LFSCProof</a> ()
</ul>
<h2><a name="pro-attribs"></a>
Protected Attributes</h2>
<ul>
<li>int <a class="el" href="classLFSCProof.html#ae133e339354b3013e30d2c3c1fb5e26e">printCounter</a>
<li><a class="el" href="classLFSCProof.html">LFSCProof</a> * <a class="el" href="classLFSCProof.html#a23e3f4b905b79583835415f70576fc76">rplProof</a>
<li>long int <a class="el" href="classLFSCProof.html#a4e612043c9a9fbf3410d56cd2ff78b5e">strLen</a>
<li>int <a class="el" href="classLFSCProof.html#addc61701b4bbfb7119df3b00667e808a">chOp</a>
<li>int <a class="el" href="classLFSCProof.html#a425fcc2ea8b8801dbd7780ddcc20d624">assumeVar</a>
<li>int <a class="el" href="classLFSCProof.html#a3080390335b3e2338814bbfed11356f6">assumeVarUsed</a>
<li>std::vector< int > <a class="el" href="classLFSCProof.html#a80c629f061bf236f2cfe1c4ad3449b75">br</a>
<li>bool <a class="el" href="classLFSCProof.html#acc878f584c9d1c1c59737870fd006e0b">brComputed</a>
</ul>
<h2><a name="pro-static-attribs"></a>
Static Protected Attributes</h2>
<ul>
<li>static int <a class="el" href="classLFSCProof.html#a3614c6ce131c1d8a0fd2c18610659117">pf_counter</a> = 0
<li>static std::map< <a class="el" href="classLFSCProof.html">LFSCProof</a> *, int > <a class="el" href="classLFSCProof.html#a5f40eaf9f09aa0607f5063e460de1552">lambdaMap</a>
<li>static std::map< <a class="el" href="classLFSCProof.html">LFSCProof</a> <br class="typebreak"/>
*, <a class="el" href="classLFSCProof.html">LFSCProof</a> * > <a class="el" href="classLFSCProof.html#ac8fd8287bbc4d4f0a8f8f456b6dca0a4">lambdaPrintMap</a>
<li>static int <a class="el" href="classLFSCProof.html#a6ce5b89de4d7cb2731e503272d746199">lambdaCounter</a> = 1
</ul>
<h2><a name="friends"></a>
Friends</h2>
<ul>
<li>class <a class="el" href="classLFSCProof.html#a2d3cb4e50f5ffb662dc18e83ee206c2c">LFSCPrinter</a>
</ul>
<hr/><a name="details" id="details"></a><h2>Detailed Description</h2>
<div class="textblock">
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00026">26</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
</div><hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="a08258b1a59261c0dd0edcd775a883cfc"></a><!-- doxytag: member="LFSCProof::LFSCProof" ref="a08258b1a59261c0dd0edcd775a883cfc" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">LFSCProof::LFSCProof </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCProof_8cpp_source.html#l00011">11</a> of file <a class="el" href="LFSCProof_8cpp_source.html">LFSCProof.cpp</a>.</p>
<p>References <a class="el" href="LFSCProof_8h_source.html#l00036">assumeVar</a>, <a class="el" href="LFSCProof_8h_source.html#l00037">assumeVarUsed</a>, <a class="el" href="LFSCProof_8h_source.html#l00040">brComputed</a>, <a class="el" href="LFSCProof_8h_source.html#l00035">chOp</a>, <a class="el" href="LFSCProof_8h_source.html#l00028">pf_counter</a>, <a class="el" href="LFSCProof_8h_source.html#l00031">printCounter</a>, <a class="el" href="LFSCProof_8h_source.html#l00032">rplProof</a>, and <a class="el" href="LFSCProof_8h_source.html#l00034">strLen</a>.</p>
</div>
</div>
<a class="anchor" id="a734881b4ad199d3251973cc844a18929"></a><!-- doxytag: member="LFSCProof::~LFSCProof" ref="a734881b4ad199d3251973cc844a18929" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual LFSCProof::~LFSCProof </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, protected, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00044">44</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
</div>
</div>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="a4f6cb66f81baeb838874bfc2ee51595e"></a><!-- doxytag: member="LFSCProof::get_length" ref="a4f6cb66f81baeb838874bfc2ee51595e" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual long int LFSCProof::get_length </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, protected, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classLFSCBoolRes.html#a735517bb51cdfa5057945c87992ad14a">LFSCBoolRes</a>, <a class="el" href="classLFSCLem.html#ad1fa27fc76b749c9fad43121931936de">LFSCLem</a>, <a class="el" href="classLFSCClausify.html#a36d74d26af6ecf508ff51445e3e4f7cd">LFSCClausify</a>, <a class="el" href="classLFSCAssume.html#a2109fe5fdc3237a8b881564616b6bfbb">LFSCAssume</a>, <a class="el" href="classLFSCLraAdd.html#a61994da8716e9432d11d2f6666237425">LFSCLraAdd</a>, <a class="el" href="classLFSCLraAxiom.html#ad33974a576d8c078bbe6a1a65590f6eb">LFSCLraAxiom</a>, <a class="el" href="classLFSCLraMulC.html#ab1de62b88ec2355fed8f496c2b23cc2d">LFSCLraMulC</a>, <a class="el" href="classLFSCLraSub.html#a20fbc15d7eb7c372678b281d4caabd0a">LFSCLraSub</a>, <a class="el" href="classLFSCLraPoly.html#a204461047f2b488c01841ce1dc4408cc">LFSCLraPoly</a>, <a class="el" href="classLFSCLraContra.html#a0787be4effc2ca8551fb5d6ee0e9b88c">LFSCLraContra</a>, <a class="el" href="classLFSCProofExpr.html#a6c3db39b65904445c0dfc727cbba3996">LFSCProofExpr</a>, <a class="el" href="classLFSCPfVar.html#afbdfac3e19586ccbf29321b2a08feddc">LFSCPfVar</a>, <a class="el" href="classLFSCPfLambda.html#aacda4aaa9a0c51ee7bcf59559d77db1d">LFSCPfLambda</a>, <a class="el" href="classLFSCProofGeneric.html#a7acae5a8c672b63f1aab26c3feb9ab67">LFSCProofGeneric</a>, and <a class="el" href="classLFSCPfLet.html#a49cb76df6e4fbb2f13a21e9c626efc45">LFSCPfLet</a>.</p>
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00043">43</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
<p>Referenced by <a class="el" href="LFSCProof_8h_source.html#l00073">get_string_length()</a>.</p>
</div>
</div>
<a class="anchor" id="ae1a19870033df1a9656e54ca2e4c21a6"></a><!-- doxytag: member="LFSCProof::AsLFSCProofExpr" ref="ae1a19870033df1a9656e54ca2e4c21a6" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classLFSCProofExpr.html">LFSCProofExpr</a>* LFSCProof::AsLFSCProofExpr </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classLFSCProofExpr.html#a0e718fc15fa1ab162fb38489a2c2c579">LFSCProofExpr</a>.</p>
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00046">46</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
</div>
</div>
<a class="anchor" id="a7cc0f70e22642f958d58bdcebcd06530"></a><!-- doxytag: member="LFSCProof::AsLFSCLraAdd" ref="a7cc0f70e22642f958d58bdcebcd06530" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classLFSCLraAdd.html">LFSCLraAdd</a>* LFSCProof::AsLFSCLraAdd </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classLFSCLraAdd.html#a13e0f9aff803816bc0d1b8908a03a488">LFSCLraAdd</a>.</p>
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00047">47</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
</div>
</div>
<a class="anchor" id="a60be4bca8e5d7487bd19f391b675d49b"></a><!-- doxytag: member="LFSCProof::AsLFSCLraSub" ref="a60be4bca8e5d7487bd19f391b675d49b" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classLFSCLraSub.html">LFSCLraSub</a>* LFSCProof::AsLFSCLraSub </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classLFSCLraSub.html#a967e3068a4e96821799f447812bcc932">LFSCLraSub</a>.</p>
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00048">48</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
</div>
</div>
<a class="anchor" id="a87f99538036f96fd800bc97049478af2"></a><!-- doxytag: member="LFSCProof::AsLFSCLraMulC" ref="a87f99538036f96fd800bc97049478af2" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classLFSCLraMulC.html">LFSCLraMulC</a>* LFSCProof::AsLFSCLraMulC </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classLFSCLraMulC.html#abcf992e31f8c3d27d007a58e0b979a31">LFSCLraMulC</a>.</p>
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00049">49</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
<p>Referenced by <a class="el" href="LFSCLraProof_8cpp_source.html#l00065">LFSCLraMulC::Make()</a>.</p>
</div>
</div>
<a class="anchor" id="a9b6a71f2857c0bbdd2689aa3665657da"></a><!-- doxytag: member="LFSCProof::AsLFSCLraAxiom" ref="a9b6a71f2857c0bbdd2689aa3665657da" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classLFSCLraAxiom.html">LFSCLraAxiom</a>* LFSCProof::AsLFSCLraAxiom </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classLFSCLraAxiom.html#ac4fb660f4e21d9e6b73699687ad88eb8">LFSCLraAxiom</a>.</p>
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00050">50</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
</div>
</div>
<a class="anchor" id="a52f0d889a8439f484b1995ae2536a671"></a><!-- doxytag: member="LFSCProof::AsLFSCLraContra" ref="a52f0d889a8439f484b1995ae2536a671" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classLFSCLraContra.html">LFSCLraContra</a>* LFSCProof::AsLFSCLraContra </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classLFSCLraContra.html#afe3e4873b5cf92408193cd0fc64858de">LFSCLraContra</a>.</p>
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00051">51</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
</div>
</div>
<a class="anchor" id="a13a5d84e3c02842c331c0093689edd58"></a><!-- doxytag: member="LFSCProof::AsLFSCLraPoly" ref="a13a5d84e3c02842c331c0093689edd58" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classLFSCLraPoly.html">LFSCLraPoly</a>* LFSCProof::AsLFSCLraPoly </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classLFSCLraPoly.html#ac608cb36f274f970de7ce3a395621203">LFSCLraPoly</a>.</p>
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00052">52</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
<p>Referenced by <a class="el" href="TReturn_8cpp_source.html#l00423">TReturn::normalize_to_tf()</a>.</p>
</div>
</div>
<a class="anchor" id="a6b5678c20b54da5345d66b595a33a719"></a><!-- doxytag: member="LFSCProof::AsLFSCBoolRes" ref="a6b5678c20b54da5345d66b595a33a719" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classLFSCBoolRes.html">LFSCBoolRes</a>* LFSCProof::AsLFSCBoolRes </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classLFSCBoolRes.html#a55ed62198bc8c13254cb8f7f38afbd05">LFSCBoolRes</a>.</p>
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00053">53</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
</div>
</div>
<a class="anchor" id="a35b9ae21403a09523359d96d182c7431"></a><!-- doxytag: member="LFSCProof::AsLFSCLem" ref="a35b9ae21403a09523359d96d182c7431" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classLFSCLem.html">LFSCLem</a>* LFSCProof::AsLFSCLem </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classLFSCLem.html#a8889765b9388d270f84678585476ec06">LFSCLem</a>.</p>
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00054">54</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
</div>
</div>
<a class="anchor" id="a1ae53259bdc504ba263e86b0d85ccede"></a><!-- doxytag: member="LFSCProof::AsLFSCClausify" ref="a1ae53259bdc504ba263e86b0d85ccede" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classLFSCClausify.html">LFSCClausify</a>* LFSCProof::AsLFSCClausify </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classLFSCClausify.html#a891e43a4ad778be5cd450a414eca4214">LFSCClausify</a>.</p>
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00055">55</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
</div>
</div>
<a class="anchor" id="a090256e5ceadaccaa46826689f95f238"></a><!-- doxytag: member="LFSCProof::AsLFSCAssume" ref="a090256e5ceadaccaa46826689f95f238" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classLFSCAssume.html">LFSCAssume</a>* LFSCProof::AsLFSCAssume </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classLFSCAssume.html#a62a38c16c3d0175a2a0e9ca1504716c7">LFSCAssume</a>.</p>
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00056">56</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
</div>
</div>
<a class="anchor" id="a11df493e82f924825e42d2bcef64c1f6"></a><!-- doxytag: member="LFSCProof::AsLFSCProofGeneric" ref="a11df493e82f924825e42d2bcef64c1f6" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classLFSCProofGeneric.html">LFSCProofGeneric</a>* LFSCProof::AsLFSCProofGeneric </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classLFSCProofGeneric.html#a89efd3123a97c54a31a477e75185dd63">LFSCProofGeneric</a>.</p>
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00057">57</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
</div>
</div>
<a class="anchor" id="a3204930c32bc4a67ec0ddb23b3be51be"></a><!-- doxytag: member="LFSCProof::AsLFSCPfVar" ref="a3204930c32bc4a67ec0ddb23b3be51be" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classLFSCPfVar.html">LFSCPfVar</a>* LFSCProof::AsLFSCPfVar </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classLFSCPfVar.html#a5b6e5edc54a507a7c695ffa2999671b0">LFSCPfVar</a>.</p>
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00058">58</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
</div>
</div>
<a class="anchor" id="ad56845dc18ff11a9a054c7137ce5a680"></a><!-- doxytag: member="LFSCProof::AsLFSCPfLambda" ref="ad56845dc18ff11a9a054c7137ce5a680" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classLFSCPfLambda.html">LFSCPfLambda</a>* LFSCProof::AsLFSCPfLambda </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classLFSCPfLambda.html#a2dac1e9539015c086c3a6e9df2fa948e">LFSCPfLambda</a>.</p>
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00059">59</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
</div>
</div>
<a class="anchor" id="aefd45e8a659276c68dd2797a995ffc87"></a><!-- doxytag: member="LFSCProof::AsLFSCPfLet" ref="aefd45e8a659276c68dd2797a995ffc87" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classLFSCPfLet.html">LFSCPfLet</a>* LFSCProof::AsLFSCPfLet </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classLFSCPfLet.html#a554bd849b6be3e87301664a78af548c2">LFSCPfLet</a>.</p>
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00060">60</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
</div>
</div>
<a class="anchor" id="aa1dbda64d42f7bf7c81a1b6e68da2766"></a><!-- doxytag: member="LFSCProof::isLraMulC" ref="aa1dbda64d42f7bf7c81a1b6e68da2766" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual bool LFSCProof::isLraMulC </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classLFSCLraMulC.html#a748192deaf801da5721da450dce18e13">LFSCLraMulC</a>.</p>
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00062">62</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
</div>
</div>
<a class="anchor" id="a396c41fc6012caf4dde358af52d25905"></a><!-- doxytag: member="LFSCProof::make_lambda" ref="a396c41fc6012caf4dde358af52d25905" args="(LFSCProof *p)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">static int LFSCProof::make_lambda </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classLFSCProof.html">LFSCProof</a> * </td>
<td class="paramname"><em>p</em></td><td>)</td>
<td><code> [inline, static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00063">63</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
<p>References <a class="el" href="LFSCProof_8h_source.html#l00033">lambdaCounter</a>, and <a class="el" href="LFSCProof_8h_source.html#l00029">lambdaMap</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l01663">LFSCConvert::make_let_proof()</a>.</p>
</div>
</div>
<a class="anchor" id="aed472da83c57ed8a1ac6d2a6bc34eeba"></a><!-- doxytag: member="LFSCProof::print" ref="aed472da83c57ed8a1ac6d2a6bc34eeba" args="(std::ostream &s, int ind=0)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void LFSCProof::print </td>
<td>(</td>
<td class="paramtype">std::ostream & </td>
<td class="paramname"><em>s</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>ind</em> = <code>0</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCProof_8cpp_source.html#l00023">23</a> of file <a class="el" href="LFSCProof_8cpp_source.html">LFSCProof.cpp</a>.</p>
<p>References <a class="el" href="Object_8h_source.html#l00073">Obj::indent()</a>, <a class="el" href="LFSCProof_8h_source.html#l00029">lambdaMap</a>, <a class="el" href="LFSCProof_8h_source.html#l00030">lambdaPrintMap</a>, <a class="el" href="LFSCProof_8cpp_source.html#l00023">print()</a>, <a class="el" href="classLFSCProof.html#a9ad1d738b10d731108f63b9d86796c00">print_pf()</a>, <a class="el" href="Object_8h_source.html#l00104">Obj::print_warning()</a>, <a class="el" href="LFSCProof_8h_source.html#l00031">printCounter</a>, and <a class="el" href="LFSCProof_8h_source.html#l00032">rplProof</a>.</p>
<p>Referenced by <a class="el" href="LFSCProof_8cpp_source.html#l00023">print()</a>, and <a class="el" href="LFSCProof_8cpp_source.html#l00043">print_structure()</a>.</p>
</div>
</div>
<a class="anchor" id="a9ad1d738b10d731108f63b9d86796c00"></a><!-- doxytag: member="LFSCProof::print_pf" ref="a9ad1d738b10d731108f63b9d86796c00" args="(std::ostream &s, int ind=0)=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual void LFSCProof::print_pf </td>
<td>(</td>
<td class="paramtype">std::ostream & </td>
<td class="paramname"><em>s</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>ind</em> = <code>0</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classLFSCBoolRes.html#a6d09024324b4d619bd9f34e178ac57d5">LFSCBoolRes</a>, <a class="el" href="classLFSCLem.html#a38c060085273f0dd8c425a14683b4067">LFSCLem</a>, <a class="el" href="classLFSCClausify.html#a571d958b1b69082a99ee3e8c2e1e5a82">LFSCClausify</a>, <a class="el" href="classLFSCAssume.html#ab8bc3cbf1aef169b856d704eceef4be6">LFSCAssume</a>, <a class="el" href="classLFSCLraAdd.html#a606f0a1297b4cce586f3111c1598808b">LFSCLraAdd</a>, <a class="el" href="classLFSCLraAxiom.html#a48603e9301acbd8b355ac92a6c4db0cd">LFSCLraAxiom</a>, <a class="el" href="classLFSCLraMulC.html#a2bf14817557003c1c3f07b7e6bc61796">LFSCLraMulC</a>, <a class="el" href="classLFSCLraSub.html#a636294ce853f360b1813b6547cb8d37c">LFSCLraSub</a>, <a class="el" href="classLFSCLraPoly.html#a94af3dd8672407e26643aaec09e7bc49">LFSCLraPoly</a>, <a class="el" href="classLFSCLraContra.html#a41be91fb05ac0a256e34461080eca14b">LFSCLraContra</a>, <a class="el" href="classLFSCProofExpr.html#af732b18f23d3bb237583048f52dc60c1">LFSCProofExpr</a>, <a class="el" href="classLFSCPfVar.html#a0b69489a9e1546ba6741de5b5400c8e9">LFSCPfVar</a>, <a class="el" href="classLFSCPfLambda.html#af3b36357fab483afc642f4c77bd4a497">LFSCPfLambda</a>, <a class="el" href="classLFSCProofGeneric.html#aa1bc4b22316c2bff7f852d2a4799f533">LFSCProofGeneric</a>, and <a class="el" href="classLFSCPfLet.html#aaadb919e3b6b04b3acd02d984011b088">LFSCPfLet</a>.</p>
<p>Referenced by <a class="el" href="LFSCProof_8cpp_source.html#l00023">print()</a>.</p>
</div>
</div>
<a class="anchor" id="a094c8c12bcb8ee3b1ec7a51b5568c355"></a><!-- doxytag: member="LFSCProof::isTrivial" ref="a094c8c12bcb8ee3b1ec7a51b5568c355" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual bool LFSCProof::isTrivial </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classLFSCLraAxiom.html#a46689ab969bc06af37c9e139d5f98f2e">LFSCLraAxiom</a>.</p>
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00072">72</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00093">LFSCConvert::cvc3_to_lfsc()</a>, <a class="el" href="LFSCLraProof_8cpp_source.html#l00089">LFSCLraSub::Make()</a>, <a class="el" href="LFSCLraProof_8cpp_source.html#l00065">LFSCLraMulC::Make()</a>, <a class="el" href="LFSCLraProof_8cpp_source.html#l00017">LFSCLraAdd::Make()</a>, and <a class="el" href="LFSCBoolProof_8cpp_source.html#l00032">LFSCBoolRes::Make()</a>.</p>
</div>
</div>
<a class="anchor" id="a784c4a1295785719bce419d3e9ee9be1"></a><!-- doxytag: member="LFSCProof::get_string_length" ref="a784c4a1295785719bce419d3e9ee9be1" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">long int LFSCProof::get_string_length </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00073">73</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
<p>References <a class="el" href="LFSCProof_8h_source.html#l00043">get_length()</a>, <a class="el" href="LFSCProof_8h_source.html#l00073">get_string_length()</a>, <a class="el" href="LFSCProof_8h_source.html#l00101">getChild()</a>, <a class="el" href="LFSCProof_8h_source.html#l00100">getNumChildren()</a>, and <a class="el" href="LFSCProof_8h_source.html#l00034">strLen</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00093">LFSCConvert::cvc3_to_lfsc()</a>, <a class="el" href="LFSCUtilProof_8cpp_source.html#l00070">LFSCProofGeneric::get_length()</a>, and <a class="el" href="LFSCProof_8h_source.html#l00073">get_string_length()</a>.</p>
</div>
</div>
<a class="anchor" id="ae135f7109d7cc2a9185a48487840b683"></a><!-- doxytag: member="LFSCProof::print_structure" ref="ae135f7109d7cc2a9185a48487840b683" args="(std::ostream &s, int ind=0)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void LFSCProof::print_structure </td>
<td>(</td>
<td class="paramtype">std::ostream & </td>
<td class="paramname"><em>s</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>ind</em> = <code>0</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCProof_8cpp_source.html#l00043">43</a> of file <a class="el" href="LFSCProof_8cpp_source.html">LFSCProof.cpp</a>.</p>
<p>References <a class="el" href="Object_8h_source.html#l00073">Obj::indent()</a>, <a class="el" href="LFSCProof_8h_source.html#l00029">lambdaMap</a>, <a class="el" href="LFSCProof_8h_source.html#l00030">lambdaPrintMap</a>, <a class="el" href="LFSCProof_8cpp_source.html#l00023">print()</a>, <a class="el" href="LFSCProof_8h_source.html#l00086">print_struct()</a>, <a class="el" href="Object_8h_source.html#l00104">Obj::print_warning()</a>, <a class="el" href="LFSCProof_8h_source.html#l00031">printCounter</a>, and <a class="el" href="LFSCProof_8h_source.html#l00032">rplProof</a>.</p>
</div>
</div>
<a class="anchor" id="a989d58a3910834809ddbfc89c04f6d87"></a><!-- doxytag: member="LFSCProof::print_struct" ref="a989d58a3910834809ddbfc89c04f6d87" args="(std::ostream &s, int ind=0)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual void LFSCProof::print_struct </td>
<td>(</td>
<td class="paramtype">std::ostream & </td>
<td class="paramname"><em>s</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>ind</em> = <code>0</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classLFSCBoolRes.html#a9b6c2508cb389bd861357b832bde2502">LFSCBoolRes</a>, <a class="el" href="classLFSCLem.html#a65692ca4d960a021ad165fb89c411021">LFSCLem</a>, <a class="el" href="classLFSCClausify.html#ab65fca27b5949176646d5b7c3c703604">LFSCClausify</a>, <a class="el" href="classLFSCAssume.html#a61b64cc4b4ded52c63db33fa821ec20d">LFSCAssume</a>, <a class="el" href="classLFSCPfVar.html#aca4bf1d3cd471df00f7354797553be35">LFSCPfVar</a>, and <a class="el" href="classLFSCPfLet.html#a71496a1b0012750fec8ab33ea1998f7a">LFSCPfLet</a>.</p>
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00086">86</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
<p>Referenced by <a class="el" href="LFSCProof_8cpp_source.html#l00043">print_structure()</a>.</p>
</div>
</div>
<a class="anchor" id="ae8e4007daade52b31f52182192d46abc"></a><!-- doxytag: member="LFSCProof::setRplProof" ref="ae8e4007daade52b31f52182192d46abc" args="(LFSCProof *p)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void LFSCProof::setRplProof </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classLFSCProof.html">LFSCProof</a> * </td>
<td class="paramname"><em>p</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00091">91</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
<p>References <a class="el" href="LFSCProof_8h_source.html#l00032">rplProof</a>.</p>
</div>
</div>
<a class="anchor" id="ada9a53bcd04fe712b1fc22f9a0a23ccc"></a><!-- doxytag: member="LFSCProof::fillHoles" ref="ada9a53bcd04fe712b1fc22f9a0a23ccc" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void LFSCProof::fillHoles </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classLFSCProofExpr.html#aac86e160f1dc7ac8b8c6cf90e22ebfee">LFSCProofExpr</a>.</p>
<p>Definition at line <a class="el" href="LFSCProof_8cpp_source.html#l00061">61</a> of file <a class="el" href="LFSCProof_8cpp_source.html">LFSCProof.cpp</a>.</p>
<p>References <a class="el" href="LFSCProof_8cpp_source.html#l00061">fillHoles()</a>, <a class="el" href="LFSCProof_8h_source.html#l00101">getChild()</a>, and <a class="el" href="LFSCProof_8h_source.html#l00100">getNumChildren()</a>.</p>
<p>Referenced by <a class="el" href="LFSCProof_8cpp_source.html#l00061">fillHoles()</a>.</p>
</div>
</div>
<a class="anchor" id="a0fff5e24b97c44080514e3ec6f15d751"></a><!-- doxytag: member="LFSCProof::clone" ref="a0fff5e24b97c44080514e3ec6f15d751" args="()=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classLFSCProof.html">LFSCProof</a>* LFSCProof::clone </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classLFSCBoolRes.html#a8fa3bfd1f1e57790d7bfd697cee9c4c2">LFSCBoolRes</a>, <a class="el" href="classLFSCLem.html#a10cff9d19d35ca803eb2d86379fbfea9">LFSCLem</a>, <a class="el" href="classLFSCClausify.html#abfb721ca8127c842987d38302d4dee93">LFSCClausify</a>, <a class="el" href="classLFSCAssume.html#a09b11c30192e746c3d4f61786811a0c3">LFSCAssume</a>, <a class="el" href="classLFSCLraAdd.html#aff3aea69c6c937ddf277ae9c4a545a1a">LFSCLraAdd</a>, <a class="el" href="classLFSCLraAxiom.html#a335fef727fe4f6c89b94c4f6f199297f">LFSCLraAxiom</a>, <a class="el" href="classLFSCLraMulC.html#ab781508a39b0d77c42b0b1899fa8d52e">LFSCLraMulC</a>, <a class="el" href="classLFSCLraSub.html#aca5efb16b2920eea3c4e7a1ebd31ad30">LFSCLraSub</a>, <a class="el" href="classLFSCLraPoly.html#a66f249a42dce384be16a1d58c243ea4a">LFSCLraPoly</a>, <a class="el" href="classLFSCLraContra.html#ae33a5e48d100094da883af525acc7d66">LFSCLraContra</a>, <a class="el" href="classLFSCProofExpr.html#a6cc953e364c97a359d09c63fe08be7be">LFSCProofExpr</a>, <a class="el" href="classLFSCPfVar.html#a6156af7863569dca0abed952fa938978">LFSCPfVar</a>, <a class="el" href="classLFSCPfLambda.html#ace06bdec9d26641fe98c7b32b582d67e">LFSCPfLambda</a>, <a class="el" href="classLFSCProofGeneric.html#aec701cd210f5e2aa1734c644c0ab4c6a">LFSCProofGeneric</a>, and <a class="el" href="classLFSCPfLet.html#ab436db06a158bf463c0614f34608cfaf">LFSCPfLet</a>.</p>
</div>
</div>
<a class="anchor" id="aedc30ad27db2049d1e6782918bdc2608"></a><!-- doxytag: member="LFSCProof::getNumChildren" ref="aedc30ad27db2049d1e6782918bdc2608" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual int LFSCProof::getNumChildren </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classLFSCBoolRes.html#a44545b6339ce2e4f0dc483cf60f9e8e7">LFSCBoolRes</a>, <a class="el" href="classLFSCClausify.html#a3942b93955d5161fbcc7a48d49ffc351">LFSCClausify</a>, <a class="el" href="classLFSCAssume.html#a92ae711a4382449ee1923cb07742c5c4">LFSCAssume</a>, <a class="el" href="classLFSCLraAdd.html#a92ad459567cc680a6b0873ce39c893e0">LFSCLraAdd</a>, <a class="el" href="classLFSCLraMulC.html#a21a98611a0b197c990a28200d46774c1">LFSCLraMulC</a>, <a class="el" href="classLFSCLraSub.html#a4dc6c463232726a4e5d9c0fd9bc512b0">LFSCLraSub</a>, <a class="el" href="classLFSCLraPoly.html#ad9bee6a3ddb3a58059b22dd7112e2496">LFSCLraPoly</a>, <a class="el" href="classLFSCLraContra.html#a6220f85da35d769ae06b46cfce82e636">LFSCLraContra</a>, <a class="el" href="classLFSCPfLambda.html#a96fd9ae0a48dd8bb55e9e0fcde2fbe16">LFSCPfLambda</a>, and <a class="el" href="classLFSCProofGeneric.html#a588df357bf41ff575e52cb7dd0d34040">LFSCProofGeneric</a>.</p>
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00100">100</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
<p>Referenced by <a class="el" href="LFSCProof_8cpp_source.html#l00083">checkOp()</a>, <a class="el" href="LFSCProof_8cpp_source.html#l00061">fillHoles()</a>, and <a class="el" href="LFSCProof_8h_source.html#l00073">get_string_length()</a>.</p>
</div>
</div>
<a class="anchor" id="ac60cfef82cf6aaa935668cbfab2ecd10"></a><!-- doxytag: member="LFSCProof::getChild" ref="ac60cfef82cf6aaa935668cbfab2ecd10" args="(int n)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classLFSCProof.html">LFSCProof</a>* LFSCProof::getChild </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>n</em></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classLFSCBoolRes.html#a7d68231f4e37f4acf4ce4e8460ebeb92">LFSCBoolRes</a>, <a class="el" href="classLFSCClausify.html#a7eb20929cbad20089813d56d92b4336e">LFSCClausify</a>, <a class="el" href="classLFSCAssume.html#ab2d0929158466c1c13a416cafe5f1b33">LFSCAssume</a>, <a class="el" href="classLFSCLraAdd.html#a725352c47c99ff47e32957de18177df9">LFSCLraAdd</a>, <a class="el" href="classLFSCLraMulC.html#a8947cecdeaa2f3501f1fe07203f3f15e">LFSCLraMulC</a>, <a class="el" href="classLFSCLraSub.html#abb598f94655a242f379e036f4a343f0c">LFSCLraSub</a>, <a class="el" href="classLFSCLraPoly.html#a5c7256d609c9be9b1dbccc1d0b401c30">LFSCLraPoly</a>, <a class="el" href="classLFSCLraContra.html#a11dfd0ee07e2707db165a87697c8c8f3">LFSCLraContra</a>, <a class="el" href="classLFSCPfLambda.html#a697280bf0655b2861c5073daa847a33e">LFSCPfLambda</a>, and <a class="el" href="classLFSCProofGeneric.html#a10ab8502f739ebccfa77b8a8436223fe">LFSCProofGeneric</a>.</p>
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00101">101</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
<p>Referenced by <a class="el" href="LFSCProof_8cpp_source.html#l00083">checkOp()</a>, <a class="el" href="LFSCProof_8cpp_source.html#l00061">fillHoles()</a>, <a class="el" href="LFSCProof_8h_source.html#l00073">get_string_length()</a>, and <a class="el" href="TReturn_8cpp_source.html#l00423">TReturn::normalize_to_tf()</a>.</p>
</div>
</div>
<a class="anchor" id="a8bb7d43de0773db524227b1c2af54bb0"></a><!-- doxytag: member="LFSCProof::checkOp" ref="a8bb7d43de0773db524227b1c2af54bb0" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int LFSCProof::checkOp </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classLFSCLraAdd.html#ac8da622f5eb219b6258fe574a3992784">LFSCLraAdd</a>, <a class="el" href="classLFSCLraAxiom.html#aa371ea95da1f4044a286f23f52cfead6">LFSCLraAxiom</a>, <a class="el" href="classLFSCLraMulC.html#ade7db00f45b31f5f4cf8df1d3c5b255c">LFSCLraMulC</a>, <a class="el" href="classLFSCLraSub.html#a5c5b56cfc4a9f44971325de01ac28669">LFSCLraSub</a>, <a class="el" href="classLFSCLraPoly.html#a38c685a24cc6d5cf395632a9077fa734">LFSCLraPoly</a>, and <a class="el" href="classLFSCLraContra.html#a9fcfcdf0bb6470616c36d8e9b61c3fa6">LFSCLraContra</a>.</p>
<p>Definition at line <a class="el" href="LFSCProof_8cpp_source.html#l00083">83</a> of file <a class="el" href="LFSCProof_8cpp_source.html">LFSCProof.cpp</a>.</p>
<p>References <a class="el" href="LFSCProof_8cpp_source.html#l00083">checkOp()</a>, <a class="el" href="LFSCProof_8h_source.html#l00035">chOp</a>, <a class="el" href="LFSCProof_8h_source.html#l00101">getChild()</a>, and <a class="el" href="LFSCProof_8h_source.html#l00100">getNumChildren()</a>.</p>
<p>Referenced by <a class="el" href="LFSCProof_8cpp_source.html#l00083">checkOp()</a>, <a class="el" href="LFSCLraProof_8h_source.html#l00145">LFSCLraContra::LFSCLraContra()</a>, <a class="el" href="LFSCLraProof_8h_source.html#l00063">LFSCLraMulC::LFSCLraMulC()</a>, <a class="el" href="LFSCLraProof_8h_source.html#l00116">LFSCLraPoly::LFSCLraPoly()</a>, <a class="el" href="LFSCLraProof_8h_source.html#l00088">LFSCLraSub::LFSCLraSub()</a>, and <a class="el" href="LFSCLraProof_8cpp_source.html#l00017">LFSCLraAdd::Make()</a>.</p>
</div>
</div>
<a class="anchor" id="a6b95ef9fff90f5410755fdb628c6897c"></a><!-- doxytag: member="LFSCProof::getChOp" ref="a6b95ef9fff90f5410755fdb628c6897c" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int LFSCProof::getChOp </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00103">103</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
<p>References <a class="el" href="LFSCProof_8h_source.html#l00035">chOp</a>.</p>
<p>Referenced by <a class="el" href="TReturn_8cpp_source.html#l00423">TReturn::normalize_to_tf()</a>, and <a class="el" href="TReturn_8cpp_source.html#l00125">TReturn::normalize_tr()</a>.</p>
</div>
</div>
<a class="anchor" id="a5152d42d473b2305cae68012da611208"></a><!-- doxytag: member="LFSCProof::setChOp" ref="a5152d42d473b2305cae68012da611208" args="(int c)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void LFSCProof::setChOp </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>c</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00104">104</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
<p>References <a class="el" href="LFSCProof_8h_source.html#l00035">chOp</a>.</p>
<p>Referenced by <a class="el" href="LFSCLraProof_8cpp_source.html#l00117">LFSCLraPoly::Make()</a>, <a class="el" href="TReturn_8cpp_source.html#l00423">TReturn::normalize_to_tf()</a>, and <a class="el" href="TReturn_8cpp_source.html#l00125">TReturn::normalize_tr()</a>.</p>
</div>
</div>
<a class="anchor" id="a46af0498dd659ccba0549191102cf75d"></a><!-- doxytag: member="LFSCProof::checkBoolRes" ref="a46af0498dd659ccba0549191102cf75d" args="(std::vector< int > &clause)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual int LFSCProof::checkBoolRes </td>
<td>(</td>
<td class="paramtype">std::vector< int > & </td>
<td class="paramname"><em>clause</em></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classLFSCBoolRes.html#af17c4cbbc04604af6bdd4a893d07b1b0">LFSCBoolRes</a>, <a class="el" href="classLFSCLem.html#a5ee6477298840bdaf7fb5103ac293180">LFSCLem</a>, <a class="el" href="classLFSCClausify.html#a60f52fa75358e5259eaf640bd2919d3f">LFSCClausify</a>, and <a class="el" href="classLFSCAssume.html#a126a9b3917a465e3684d907195f10824">LFSCAssume</a>.</p>
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00105">105</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
</div>
</div>
<a class="anchor" id="ab1b22c672f110e3f9abe22b2bf377fb3"></a><!-- doxytag: member="LFSCProof::Make_CNF" ref="ab1b22c672f110e3f9abe22b2bf377fb3" args="(const Expr &form, const Expr &reason, int pos)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classLFSCProof.html">LFSCProof</a> * LFSCProof::Make_CNF </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>form</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>reason</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>pos</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCProof_8cpp_source.html#l00104">104</a> of file <a class="el" href="LFSCProof_8cpp_source.html">LFSCProof.cpp</a>.</p>
<p>References <a class="el" href="cvc__util_8h_source.html#l00053">CVC3::abs()</a>, <a class="el" href="kinds_8h_source.html#l00067">AND</a>, <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="LFSCObject_8cpp_source.html#l00281">LFSCObj::cascade_expr()</a>, <a class="el" href="LFSCObject_8h_source.html#l00159">LFSCObj::d_and_final_s</a>, <a class="el" href="LFSCObject_8h_source.html#l00164">LFSCObj::d_and_mid_s</a>, <a class="el" href="LFSCObject_8h_source.html#l00161">LFSCObj::d_iff_s</a>, <a class="el" href="LFSCObject_8h_source.html#l00162">LFSCObj::d_imp_s</a>, <a class="el" href="LFSCObject_8h_source.html#l00160">LFSCObj::d_ite_s</a>, <a class="el" href="LFSCObject_8h_source.html#l00158">LFSCObj::d_or_final_s</a>, <a class="el" href="LFSCObject_8h_source.html#l00163">LFSCObj::d_or_mid_s</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="Object_8h_source.html#l00056">RefPtr< T >::get()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="LFSCUtilProof_8h_source.html#l00080">LFSCProofGeneric::Make()</a>, <a class="el" href="LFSCBoolProof_8h_source.html#l00103">LFSCAssume::Make()</a>, <a class="el" href="LFSCBoolProof_8h_source.html#l00076">LFSCClausify::Make()</a>, <a class="el" href="LFSCUtilProof_8cpp_source.html#l00033">LFSCPfVar::Make()</a>, <a class="el" href="LFSCProof_8cpp_source.html#l00397">Make_and_elim()</a>, <a class="el" href="LFSCUtilProof_8cpp_source.html#l00113">LFSCProofGeneric::MakeStr()</a>, <a class="el" href="kinds_8h_source.html#l00066">NOT</a>, <a class="el" href="Object_8h_source.html#l00095">Obj::print_error()</a>, and <a class="el" href="LFSCObject_8cpp_source.html#l00386">LFSCObj::queryM()</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00093">LFSCConvert::cvc3_to_lfsc()</a>.</p>
</div>
</div>
<a class="anchor" id="a95e3c7629c196ed189ad0525304e48cb"></a><!-- doxytag: member="LFSCProof::Make_not_not_elim" ref="a95e3c7629c196ed189ad0525304e48cb" args="(const Expr &pf, LFSCProof *p)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classLFSCProof.html">LFSCProof</a> * LFSCProof::Make_not_not_elim </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>pf</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classLFSCProof.html">LFSCProof</a> * </td>
<td class="paramname"><em>p</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCProof_8cpp_source.html#l00372">372</a> of file <a class="el" href="LFSCProof_8cpp_source.html">LFSCProof.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, and <a class="el" href="LFSCUtilProof_8h_source.html#l00080">LFSCProofGeneric::Make()</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00093">LFSCConvert::cvc3_to_lfsc()</a>.</p>
</div>
</div>
<a class="anchor" id="a979135fb775da82a9bf06befd9def730"></a><!-- doxytag: member="LFSCProof::Make_mimic" ref="a979135fb775da82a9bf06befd9def730" args="(const Expr &pf, LFSCProof *p, int numHoles)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classLFSCProof.html">LFSCProof</a> * LFSCProof::Make_mimic </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>pf</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classLFSCProof.html">LFSCProof</a> * </td>
<td class="paramname"><em>p</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>numHoles</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCProof_8cpp_source.html#l00384">384</a> of file <a class="el" href="LFSCProof_8cpp_source.html">LFSCProof.cpp</a>.</p>
<p>References <a class="el" href="LFSCUtilProof_8h_source.html#l00080">LFSCProofGeneric::Make()</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00093">LFSCConvert::cvc3_to_lfsc()</a>.</p>
</div>
</div>
<a class="anchor" id="a547ec01104eb074ab2eb4f25ea9435e0"></a><!-- doxytag: member="LFSCProof::Make_and_elim" ref="a547ec01104eb074ab2eb4f25ea9435e0" args="(const Expr &form, LFSCProof *p, int n, const Expr &expected)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classLFSCProof.html">LFSCProof</a> * LFSCProof::Make_and_elim </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>form</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classLFSCProof.html">LFSCProof</a> * </td>
<td class="paramname"><em>p</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>n</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>expected</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCProof_8cpp_source.html#l00397">397</a> of file <a class="el" href="LFSCProof_8cpp_source.html">LFSCProof.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="LFSCObject_8cpp_source.html#l00281">LFSCObj::cascade_expr()</a>, <a class="el" href="LFSCUtilProof_8h_source.html#l00080">LFSCProofGeneric::Make()</a>, and <a class="el" href="Object_8h_source.html#l00095">Obj::print_error()</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00093">LFSCConvert::cvc3_to_lfsc()</a>, and <a class="el" href="LFSCProof_8cpp_source.html#l00104">Make_CNF()</a>.</p>
</div>
</div>
<a class="anchor" id="a43144544220e21b8519c959973a35c49"></a><!-- doxytag: member="LFSCProof::get_proof_counter" ref="a43144544220e21b8519c959973a35c49" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">static int LFSCProof::get_proof_counter </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00114">114</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
<p>References <a class="el" href="LFSCProof_8h_source.html#l00028">pf_counter</a>.</p>
</div>
</div>
<hr/><h2>Friends And Related Function Documentation</h2>
<a class="anchor" id="a2d3cb4e50f5ffb662dc18e83ee206c2c"></a><!-- doxytag: member="LFSCProof::LFSCPrinter" ref="a2d3cb4e50f5ffb662dc18e83ee206c2c" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classLFSCPrinter.html">LFSCPrinter</a><code> [friend]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classLFSCClausify.html#a2d3cb4e50f5ffb662dc18e83ee206c2c">LFSCClausify</a>.</p>
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00097">97</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
</div>
</div>
<hr/><h2>Member Data Documentation</h2>
<a class="anchor" id="a3614c6ce131c1d8a0fd2c18610659117"></a><!-- doxytag: member="LFSCProof::pf_counter" ref="a3614c6ce131c1d8a0fd2c18610659117" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classLFSCProof.html#a3614c6ce131c1d8a0fd2c18610659117">LFSCProof::pf_counter</a> = 0<code> [static, protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00028">28</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
<p>Referenced by <a class="el" href="LFSCProof_8h_source.html#l00114">get_proof_counter()</a>, and <a class="el" href="LFSCProof_8cpp_source.html#l00011">LFSCProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a5f40eaf9f09aa0607f5063e460de1552"></a><!-- doxytag: member="LFSCProof::lambdaMap" ref="a5f40eaf9f09aa0607f5063e460de1552" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::map< <a class="el" href="classLFSCProof.html">LFSCProof</a> *, int > <a class="el" href="classLFSCProof.html#a5f40eaf9f09aa0607f5063e460de1552">LFSCProof::lambdaMap</a><code> [static, protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00029">29</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
<p>Referenced by <a class="el" href="LFSCProof_8h_source.html#l00063">make_lambda()</a>, <a class="el" href="LFSCProof_8cpp_source.html#l00023">print()</a>, and <a class="el" href="LFSCProof_8cpp_source.html#l00043">print_structure()</a>.</p>
</div>
</div>
<a class="anchor" id="ac8fd8287bbc4d4f0a8f8f456b6dca0a4"></a><!-- doxytag: member="LFSCProof::lambdaPrintMap" ref="ac8fd8287bbc4d4f0a8f8f456b6dca0a4" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::map< <a class="el" href="classLFSCProof.html">LFSCProof</a> *, <a class="el" href="classLFSCProof.html">LFSCProof</a> * > <a class="el" href="classLFSCProof.html#ac8fd8287bbc4d4f0a8f8f456b6dca0a4">LFSCProof::lambdaPrintMap</a><code> [static, protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00030">30</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
<p>Referenced by <a class="el" href="LFSCProof_8cpp_source.html#l00023">print()</a>, <a class="el" href="LFSCUtilProof_8cpp_source.html#l00153">LFSCPfLet::print_pf()</a>, <a class="el" href="LFSCUtilProof_8cpp_source.html#l00052">LFSCPfLambda::print_pf()</a>, <a class="el" href="LFSCUtilProof_8cpp_source.html#l00169">LFSCPfLet::print_struct()</a>, and <a class="el" href="LFSCProof_8cpp_source.html#l00043">print_structure()</a>.</p>
</div>
</div>
<a class="anchor" id="ae133e339354b3013e30d2c3c1fb5e26e"></a><!-- doxytag: member="LFSCProof::printCounter" ref="ae133e339354b3013e30d2c3c1fb5e26e" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classLFSCProof.html#ae133e339354b3013e30d2c3c1fb5e26e">LFSCProof::printCounter</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00031">31</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
<p>Referenced by <a class="el" href="LFSCProof_8cpp_source.html#l00011">LFSCProof()</a>, <a class="el" href="LFSCProof_8cpp_source.html#l00023">print()</a>, and <a class="el" href="LFSCProof_8cpp_source.html#l00043">print_structure()</a>.</p>
</div>
</div>
<a class="anchor" id="a23e3f4b905b79583835415f70576fc76"></a><!-- doxytag: member="LFSCProof::rplProof" ref="a23e3f4b905b79583835415f70576fc76" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classLFSCProof.html">LFSCProof</a>* <a class="el" href="classLFSCProof.html#a23e3f4b905b79583835415f70576fc76">LFSCProof::rplProof</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00032">32</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
<p>Referenced by <a class="el" href="LFSCProof_8cpp_source.html#l00011">LFSCProof()</a>, <a class="el" href="LFSCProof_8cpp_source.html#l00023">print()</a>, <a class="el" href="LFSCProof_8cpp_source.html#l00043">print_structure()</a>, and <a class="el" href="LFSCProof_8h_source.html#l00091">setRplProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a6ce5b89de4d7cb2731e503272d746199"></a><!-- doxytag: member="LFSCProof::lambdaCounter" ref="a6ce5b89de4d7cb2731e503272d746199" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classLFSCProof.html#a6ce5b89de4d7cb2731e503272d746199">LFSCProof::lambdaCounter</a> = 1<code> [static, protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00033">33</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
<p>Referenced by <a class="el" href="LFSCProof_8h_source.html#l00063">make_lambda()</a>.</p>
</div>
</div>
<a class="anchor" id="a4e612043c9a9fbf3410d56cd2ff78b5e"></a><!-- doxytag: member="LFSCProof::strLen" ref="a4e612043c9a9fbf3410d56cd2ff78b5e" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">long int <a class="el" href="classLFSCProof.html#a4e612043c9a9fbf3410d56cd2ff78b5e">LFSCProof::strLen</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00034">34</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
<p>Referenced by <a class="el" href="LFSCProof_8h_source.html#l00073">get_string_length()</a>, and <a class="el" href="LFSCProof_8cpp_source.html#l00011">LFSCProof()</a>.</p>
</div>
</div>
<a class="anchor" id="addc61701b4bbfb7119df3b00667e808a"></a><!-- doxytag: member="LFSCProof::chOp" ref="addc61701b4bbfb7119df3b00667e808a" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classLFSCProof.html#addc61701b4bbfb7119df3b00667e808a">LFSCProof::chOp</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00035">35</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
<p>Referenced by <a class="el" href="LFSCProof_8cpp_source.html#l00083">checkOp()</a>, <a class="el" href="LFSCProof_8h_source.html#l00103">getChOp()</a>, <a class="el" href="LFSCProof_8cpp_source.html#l00011">LFSCProof()</a>, and <a class="el" href="LFSCProof_8h_source.html#l00104">setChOp()</a>.</p>
</div>
</div>
<a class="anchor" id="a425fcc2ea8b8801dbd7780ddcc20d624"></a><!-- doxytag: member="LFSCProof::assumeVar" ref="a425fcc2ea8b8801dbd7780ddcc20d624" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classLFSCProof.html#a425fcc2ea8b8801dbd7780ddcc20d624">LFSCProof::assumeVar</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00036">36</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
<p>Referenced by <a class="el" href="LFSCProof_8cpp_source.html#l00011">LFSCProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a3080390335b3e2338814bbfed11356f6"></a><!-- doxytag: member="LFSCProof::assumeVarUsed" ref="a3080390335b3e2338814bbfed11356f6" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classLFSCProof.html#a3080390335b3e2338814bbfed11356f6">LFSCProof::assumeVarUsed</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00037">37</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
<p>Referenced by <a class="el" href="LFSCProof_8cpp_source.html#l00011">LFSCProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a80c629f061bf236f2cfe1c4ad3449b75"></a><!-- doxytag: member="LFSCProof::br" ref="a80c629f061bf236f2cfe1c4ad3449b75" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector< int > <a class="el" href="classLFSCProof.html#a80c629f061bf236f2cfe1c4ad3449b75">LFSCProof::br</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00039">39</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
</div>
</div>
<a class="anchor" id="acc878f584c9d1c1c59737870fd006e0b"></a><!-- doxytag: member="LFSCProof::brComputed" ref="acc878f584c9d1c1c59737870fd006e0b" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classLFSCProof.html#acc878f584c9d1c1c59737870fd006e0b">LFSCProof::brComputed</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCProof_8h_source.html#l00040">40</a> of file <a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a>.</p>
<p>Referenced by <a class="el" href="LFSCProof_8cpp_source.html#l00011">LFSCProof()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="LFSCProof_8h_source.html">LFSCProof.h</a></li>
<li><a class="el" href="LFSCProof_8cpp_source.html">LFSCProof.cpp</a></li>
</ul>
</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>
