<!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: LFSCConvert 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="#pri-methods">Private Member Functions</a> |
<a href="#pri-attribs">Private Attributes</a> </div>
<div class="headertitle">
<div class="title">LFSCConvert Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="LFSCConvert" --><!-- doxytag: inherits="LFSCObj" -->
<p><code>#include <<a class="el" href="LFSCConvert_8h_source.html">LFSCConvert.h</a>></code></p>
<div class="dynheader">
Inheritance diagram for LFSCConvert:</div>
<div class="dyncontent">
<div class="center">
<img src="classLFSCConvert.png" usemap="#LFSCConvert_map" alt=""/>
<map id="LFSCConvert_map" name="LFSCConvert_map">
<area href="classLFSCObj.html" alt="LFSCObj" shape="rect" coords="0,56,89,80"/>
<area href="classObj.html" alt="Obj" shape="rect" coords="0,0,89,24"/>
</map>
</div></div>
<p><a href="classLFSCConvert-members.html">List of all members.</a></p>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li><a class="el" href="classLFSCConvert.html#a7e5801505c585084591a7ed38eb33deb">LFSCConvert</a> (int lfscm)
<li>void <a class="el" href="classLFSCConvert.html#acedb89ecccd0488bb5e8425aa8ca5a14">convert</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &pf)
<li><a class="el" href="classLFSCProof.html">LFSCProof</a> * <a class="el" href="classLFSCConvert.html#ad27ba1f700e2b8950d11e4fa8edd325b">getLFSCProof</a> ()
</ul>
<h2><a name="pri-methods"></a>
Private Member Functions</h2>
<ul>
<li>bool <a class="el" href="classLFSCConvert.html#a07f851b2f599d57a9eb6406939486a49">isTrivialTheoryAxiom</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &expr, bool checkBody=false)
<li>bool <a class="el" href="classLFSCConvert.html#a0a154ba73b0cb1d375e4149dcd2178f5">isTrivialBooleanAxiom</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &expr)
<li>bool <a class="el" href="classLFSCConvert.html#a979ce0b6389586f13820f9e02ba5cd85">isIgnoredRule</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &expr)
<li><a class="el" href="classTReturn.html">TReturn</a> * <a class="el" href="classLFSCConvert.html#a70747a7c0f9de54f8d29784fa99c3987">cvc3_to_lfsc</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &pf, bool beneath_lc=false, bool rev_pol=false)
<li><a class="el" href="classTReturn.html">TReturn</a> * <a class="el" href="classLFSCConvert.html#afb93601f9c8e8ca8c09f796af341cf76">cvc3_to_lfsc_h</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &pf, bool beneath_lc=false, bool rev_pol=false)
<li><a class="el" href="classTReturn.html">TReturn</a> * <a class="el" href="classLFSCConvert.html#a751648ad72a06ae67e86a2cbbf798641">do_bso</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &pf, bool beneath_lc, bool rev_pol, <a class="el" href="classTReturn.html">TReturn</a> *t1, <a class="el" href="classTReturn.html">TReturn</a> *t2, ostringstream &ose)
<li>int <a class="el" href="classLFSCConvert.html#ac0a8b733a7e2dcaf23b7489a22c9e171">get_proof_pattern</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &pf, <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &modE)
<li><a class="el" href="classLFSCProof.html">LFSCProof</a> * <a class="el" href="classLFSCConvert.html#a4632b62661448d6fde086cbe7d260398">make_let_proof</a> (<a class="el" href="classLFSCProof.html">LFSCProof</a> *p)
<li><a class="el" href="classTReturn.html">TReturn</a> * <a class="el" href="classLFSCConvert.html#a973be3db649311c32e126e0c15c8e51e">make_trusted</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &pf)
<li>virtual <a class="el" href="classLFSCConvert.html#af9bfb12729fecdac8e9ce8b301b58209">~LFSCConvert</a> ()
</ul>
<h2><a name="pri-attribs"></a>
Private Attributes</h2>
<ul>
<li><a class="el" href="classRefPtr.html">RefPtr</a>< <a class="el" href="classLFSCProof.html">LFSCProof</a> > <a class="el" href="classLFSCConvert.html#ac93000eef387bdfa14a2b3994a241c00">pfinal</a>
<li><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< bool > <a class="el" href="classLFSCConvert.html#a10db6bada50083de6660a11f68e4431d">d_th_trans</a>
<li><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< <a class="el" href="classTReturn.html">TReturn</a> * > <a class="el" href="classLFSCConvert.html#a21833bc8f1a0982794266a2f24abf3d8">d_th_trans_map</a> [2]
<li>std::map< <a class="el" href="classTReturn.html">TReturn</a> *, bool > <a class="el" href="classLFSCConvert.html#ab6740d10097cad6ab22f2d5976163c30">d_th_trans_lam</a> [2]
<li>int <a class="el" href="classLFSCConvert.html#a56e0bda1943b3a0dbe37fedb9ec95bb7">nodeCount</a>
<li>int <a class="el" href="classLFSCConvert.html#ad79a7dc7af33a6a7f0168d7c5ed9a60e">nodeCountTh</a>
<li>int <a class="el" href="classLFSCConvert.html#a30a3b3353b977cc9b3e359f3aa8e2876">unodeCount</a>
<li>int <a class="el" href="classLFSCConvert.html#afc452237398520ff33c13c05d95d3083">unodeCountTh</a>
<li>bool <a class="el" href="classLFSCConvert.html#a49a4bb15eeceb470be396b6742f0c974">ignore_theory_lemmas</a>
</ul>
<hr/><a name="details" id="details"></a><h2>Detailed Description</h2>
<div class="textblock">
<p>Definition at line <a class="el" href="LFSCConvert_8h_source.html#l00006">6</a> of file <a class="el" href="LFSCConvert_8h_source.html">LFSCConvert.h</a>.</p>
</div><hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="af9bfb12729fecdac8e9ce8b301b58209"></a><!-- doxytag: member="LFSCConvert::~LFSCConvert" ref="af9bfb12729fecdac8e9ce8b301b58209" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual LFSCConvert::~LFSCConvert </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, private, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCConvert_8h_source.html#l00045">45</a> of file <a class="el" href="LFSCConvert_8h_source.html">LFSCConvert.h</a>.</p>
</div>
</div>
<a class="anchor" id="a7e5801505c585084591a7ed38eb33deb"></a><!-- doxytag: member="LFSCConvert::LFSCConvert" ref="a7e5801505c585084591a7ed38eb33deb" args="(int lfscm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">LFSCConvert::LFSCConvert </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>lfscm</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCConvert_8cpp_source.html#l00009">9</a> of file <a class="el" href="LFSCConvert_8cpp_source.html">LFSCConvert.cpp</a>.</p>
<p>References <a class="el" href="LFSCConvert_8h_source.html#l00023">ignore_theory_lemmas</a>, <a class="el" href="LFSCObject_8h_source.html#l00023">LFSCObj::lfsc_mode</a>, <a class="el" href="LFSCConvert_8h_source.html#l00018">nodeCount</a>, <a class="el" href="LFSCConvert_8h_source.html#l00019">nodeCountTh</a>, <a class="el" href="LFSCConvert_8h_source.html#l00020">unodeCount</a>, and <a class="el" href="LFSCConvert_8h_source.html#l00021">unodeCountTh</a>.</p>
</div>
</div>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="a07f851b2f599d57a9eb6406939486a49"></a><!-- doxytag: member="LFSCConvert::isTrivialTheoryAxiom" ref="a07f851b2f599d57a9eb6406939486a49" args="(const Expr &expr, bool checkBody=false)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool LFSCConvert::isTrivialTheoryAxiom </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>expr</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>checkBody</em> = <code>false</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCConvert_8cpp_source.html#l00057">57</a> of file <a class="el" href="LFSCConvert_8cpp_source.html">LFSCConvert.cpp</a>.</p>
<p>References <a class="el" href="LFSCObject_8h_source.html#l00119">LFSCObj::d_canon_invert_divide_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00118">LFSCObj::d_canon_mult_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00106">LFSCObj::d_canon_plus_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00113">LFSCObj::d_flip_inequality_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00142">LFSCObj::d_int_const_eq_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00110">LFSCObj::d_minus_to_plus_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00121">LFSCObj::d_mult_eqn_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00102">LFSCObj::d_mult_ineqn_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00112">LFSCObj::d_negated_inequality_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00111">LFSCObj::d_plus_predicate_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00107">LFSCObj::d_refl_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00143">LFSCObj::d_rewrite_eq_refl_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00122">LFSCObj::d_rewrite_eq_symm_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00138">LFSCObj::d_rewrite_not_false_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00137">LFSCObj::d_rewrite_not_true_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00103">LFSCObj::d_right_minus_left_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00147">LFSCObj::d_uminus_to_mult_str</a>, <a class="el" href="LFSCObject_8cpp_source.html#l00448">LFSCObj::getY()</a>, and <a class="el" href="LFSCObject_8cpp_source.html#l00539">LFSCObj::what_is_proven()</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00093">cvc3_to_lfsc()</a>.</p>
</div>
</div>
<a class="anchor" id="a0a154ba73b0cb1d375e4149dcd2178f5"></a><!-- doxytag: member="LFSCConvert::isTrivialBooleanAxiom" ref="a0a154ba73b0cb1d375e4149dcd2178f5" args="(const Expr &expr)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool LFSCConvert::isTrivialBooleanAxiom </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>expr</em></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCConvert_8cpp_source.html#l00079">79</a> of file <a class="el" href="LFSCConvert_8cpp_source.html">LFSCConvert.cpp</a>.</p>
<p>References <a class="el" href="LFSCObject_8h_source.html#l00136">LFSCObj::d_rewrite_not_not_str</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00093">cvc3_to_lfsc()</a>.</p>
</div>
</div>
<a class="anchor" id="a979ce0b6389586f13820f9e02ba5cd85"></a><!-- doxytag: member="LFSCConvert::isIgnoredRule" ref="a979ce0b6389586f13820f9e02ba5cd85" args="(const Expr &expr)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool LFSCConvert::isIgnoredRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>expr</em></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCConvert_8cpp_source.html#l00086">86</a> of file <a class="el" href="LFSCConvert_8cpp_source.html">LFSCConvert.cpp</a>.</p>
<p>References <a class="el" href="LFSCObject_8h_source.html#l00132">LFSCObj::d_iff_false_elim_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00130">LFSCObj::d_iff_not_false_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00115">LFSCObj::d_iff_true_elim_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00120">LFSCObj::d_iff_true_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00134">LFSCObj::d_not_not_elim_str</a>, and <a class="el" href="LFSCObject_8h_source.html#l00133">LFSCObj::d_not_to_iff_str</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00093">cvc3_to_lfsc()</a>.</p>
</div>
</div>
<a class="anchor" id="a70747a7c0f9de54f8d29784fa99c3987"></a><!-- doxytag: member="LFSCConvert::cvc3_to_lfsc" ref="a70747a7c0f9de54f8d29784fa99c3987" args="(const Expr &pf, bool beneath_lc=false, bool rev_pol=false)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classTReturn.html">TReturn</a> * LFSCConvert::cvc3_to_lfsc </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">bool </td>
<td class="paramname"><em>beneath_lc</em> = <code>false</code>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>rev_pol</em> = <code>false</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCConvert_8cpp_source.html#l00093">93</a> of file <a class="el" href="LFSCConvert_8cpp_source.html">LFSCConvert.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#l00026">LFSCObj::cvc3_mimic</a>, <a class="el" href="LFSCObject_8h_source.html#l00027">LFSCObj::cvc3_mimic_input</a>, <a class="el" href="LFSCObject_8h_source.html#l00152">LFSCObj::d_addInequalities_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00164">LFSCObj::d_and_mid_s</a>, <a class="el" href="LFSCObject_8h_source.html#l00150">LFSCObj::d_andE_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00066">LFSCObj::d_assump_map</a>, <a class="el" href="LFSCObject_8h_source.html#l00093">LFSCObj::d_assump_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00117">LFSCObj::d_basic_subst_op0_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00116">LFSCObj::d_basic_subst_op1_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00101">LFSCObj::d_basic_subst_op_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00092">LFSCObj::d_bool_res_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00119">LFSCObj::d_canon_invert_divide_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00118">LFSCObj::d_canon_mult_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00106">LFSCObj::d_canon_plus_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00155">LFSCObj::d_cnf_add_unit_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00108">LFSCObj::d_cnf_convert_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00154">LFSCObj::d_CNF_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00140">LFSCObj::d_CNFITE_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00135">LFSCObj::d_const_predicate_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00099">LFSCObj::d_cycle_conflict_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00105">LFSCObj::d_eq_symm_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00104">LFSCObj::d_eq_trans_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00113">LFSCObj::d_flip_inequality_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00062">LFSCObj::d_formulas_printed</a>, <a class="el" href="LFSCObject_8h_source.html#l00095">LFSCObj::d_iff_mp_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00144">LFSCObj::d_iff_symm_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00097">LFSCObj::d_iff_trans_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00162">LFSCObj::d_imp_s</a>, <a class="el" href="LFSCObject_8h_source.html#l00096">LFSCObj::d_impl_mp_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00151">LFSCObj::d_implyEqualities_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00146">LFSCObj::d_implyNegatedInequality_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00123">LFSCObj::d_implyWeakerInequality_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00142">LFSCObj::d_int_const_eq_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00160">LFSCObj::d_ite_s</a>, <a class="el" href="LFSCObject_8h_source.html#l00109">LFSCObj::d_learned_clause_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00148">LFSCObj::d_lessThan_To_LE_rhs_rwr_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00156">LFSCObj::d_minisat_proof_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00110">LFSCObj::d_minus_to_plus_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00121">LFSCObj::d_mult_eqn_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00102">LFSCObj::d_mult_ineqn_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00112">LFSCObj::d_negated_inequality_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00114">LFSCObj::d_optimized_subst_op_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00064">LFSCObj::d_pf_expr</a>, <a class="el" href="LFSCObject_8h_source.html#l00111">LFSCObj::d_plus_predicate_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00100">LFSCObj::d_real_shadow_eq_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00098">LFSCObj::d_real_shadow_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00107">LFSCObj::d_refl_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00128">LFSCObj::d_rewrite_and_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00143">LFSCObj::d_rewrite_eq_refl_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00122">LFSCObj::d_rewrite_eq_symm_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00145">LFSCObj::d_rewrite_iff_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00129">LFSCObj::d_rewrite_iff_symm_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00126">LFSCObj::d_rewrite_implies_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00149">LFSCObj::d_rewrite_ite_same_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00138">LFSCObj::d_rewrite_not_false_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00136">LFSCObj::d_rewrite_not_not_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00137">LFSCObj::d_rewrite_not_true_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00127">LFSCObj::d_rewrite_or_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00103">LFSCObj::d_right_minus_left_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00090">LFSCObj::d_rules</a>, <a class="el" href="LFSCConvert_8h_source.html#l00013">d_th_trans</a>, <a class="el" href="LFSCConvert_8h_source.html#l00016">d_th_trans_lam</a>, <a class="el" href="LFSCConvert_8h_source.html#l00014">d_th_trans_map</a>, <a class="el" href="LFSCObject_8h_source.html#l00147">LFSCObj::d_uminus_to_mult_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00024">LFSCObj::debug_conv</a>, <a class="el" href="LFSCObject_8h_source.html#l00025">LFSCObj::debug_var</a>, <a class="el" href="kinds_8h_source.html#l00063">DISTINCT</a>, <a class="el" href="LFSCConvert_8cpp_source.html#l01718">do_bso()</a>, <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="kinds_8h_source.html#l00061">EQ</a>, <a class="el" href="kinds_8h_source.html#l00036">FALSE_EXPR</a>, <a class="el" href="expr__manager_8h_source.html#l00278">CVC3::ExprManager::falseExpr()</a>, <a class="el" href="expr__map_8h_source.html#l00194">CVC3::ExprMap< Data >::find()</a>, <a class="el" href="theory__arith_8h_source.html#l00052">CVC3::GE</a>, <a class="el" href="Object_8h_source.html#l00056">RefPtr< T >::get()</a>, <a class="el" href="Util_8cpp_source.html#l00100">get_normalized()</a>, <a class="el" href="Util_8cpp_source.html#l00075">get_not()</a>, <a class="el" href="LFSCConvert_8cpp_source.html#l01641">get_proof_pattern()</a>, <a class="el" href="LFSCProof_8h_source.html#l00073">LFSCProof::get_string_length()</a>, <a class="el" href="expr_8h_source.html#l01156">CVC3::Expr::getEM()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="TReturn_8cpp_source.html#l00037">TReturn::getL()</a>, <a class="el" href="LFSCConvert_8h_source.html#l00051">getLFSCProof()</a>, <a class="el" href="TReturn_8h_source.html#l00037">TReturn::getLFSCProof()</a>, <a class="el" href="LFSCObject_8cpp_source.html#l00263">LFSCObj::getNumNodes()</a>, <a class="el" href="TReturn_8h_source.html#l00038">TReturn::getProvesY()</a>, <a class="el" href="Util_8cpp_source.html#l00158">getRat()</a>, <a class="el" href="TReturn_8h_source.html#l00036">TReturn::getRational()</a>, <a class="el" href="LFSCObject_8cpp_source.html#l00448">LFSCObj::getY()</a>, <a class="el" href="theory__arith_8h_source.html#l00051">CVC3::GT</a>, <a class="el" href="TReturn_8h_source.html#l00035">TReturn::hasRational()</a>, <a class="el" href="kinds_8h_source.html#l00070">IFF</a>, <a class="el" href="LFSCConvert_8h_source.html#l00023">ignore_theory_lemmas</a>, <a class="el" href="kinds_8h_source.html#l00071">IMPLIES</a>, <a class="el" href="Util_8cpp_source.html#l00070">is_comparison()</a>, <a class="el" href="Util_8cpp_source.html#l00047">is_eq_kind()</a>, <a class="el" href="expr_8h_source.html#l00355">CVC3::Expr::isFalse()</a>, <a class="el" href="Util_8cpp_source.html#l00173">isFlat()</a>, <a class="el" href="LFSCObject_8cpp_source.html#l00514">LFSCObj::isFormula()</a>, <a class="el" href="LFSCConvert_8cpp_source.html#l00086">isIgnoredRule()</a>, <a class="el" href="theory__arith_8h_source.html#l00177">CVC3::isRational()</a>, <a class="el" href="LFSCProof_8h_source.html#l00072">LFSCProof::isTrivial()</a>, <a class="el" href="LFSCConvert_8cpp_source.html#l00079">isTrivialBooleanAxiom()</a>, <a class="el" href="LFSCConvert_8cpp_source.html#l00057">isTrivialTheoryAxiom()</a>, <a class="el" href="kinds_8h_source.html#l00081">ITE</a>, <a class="el" href="Util_8cpp_source.html#l00017">kind_to_str()</a>, <a class="el" href="LFSCObject_8h_source.html#l00023">LFSCObj::lfsc_mode</a>, <a class="el" href="LFSCBoolProof_8h_source.html#l00050">LFSCLem::Make()</a>, <a class="el" href="LFSCBoolProof_8h_source.html#l00103">LFSCAssume::Make()</a>, <a class="el" href="LFSCUtilProof_8h_source.html#l00017">LFSCProofExpr::Make()</a>, <a class="el" href="LFSCLraProof_8h_source.html#l00159">LFSCLraContra::Make()</a>, <a class="el" href="LFSCUtilProof_8h_source.html#l00080">LFSCProofGeneric::Make()</a>, <a class="el" href="LFSCLraProof_8cpp_source.html#l00089">LFSCLraSub::Make()</a>, <a class="el" href="LFSCLraProof_8cpp_source.html#l00017">LFSCLraAdd::Make()</a>, <a class="el" href="LFSCLraProof_8cpp_source.html#l00065">LFSCLraMulC::Make()</a>, <a class="el" href="LFSCLraProof_8h_source.html#l00127">LFSCLraPoly::Make()</a>, <a class="el" href="LFSCUtilProof_8cpp_source.html#l00033">LFSCPfVar::Make()</a>, <a class="el" href="LFSCBoolProof_8cpp_source.html#l00032">LFSCBoolRes::Make()</a>, <a class="el" href="LFSCBoolProof_8h_source.html#l00076">LFSCClausify::Make()</a>, <a class="el" href="LFSCProof_8cpp_source.html#l00397">LFSCProof::Make_and_elim()</a>, <a class="el" href="LFSCProof_8cpp_source.html#l00104">LFSCProof::Make_CNF()</a>, <a class="el" href="Util_8cpp_source.html#l00203">make_flatten_expr()</a>, <a class="el" href="LFSCProof_8cpp_source.html#l00384">LFSCProof::Make_mimic()</a>, <a class="el" href="LFSCProof_8cpp_source.html#l00372">LFSCProof::Make_not_not_elim()</a>, <a class="el" href="LFSCConvert_8cpp_source.html#l01705">make_trusted()</a>, <a class="el" href="LFSCLraProof_8cpp_source.html#l00037">LFSCLraAxiom::MakeEq()</a>, <a class="el" href="LFSCUtilProof_8cpp_source.html#l00113">LFSCProofGeneric::MakeStr()</a>, <a class="el" href="LFSCUtilProof_8h_source.html#l00088">LFSCProofGeneric::MakeUnk()</a>, <a class="el" href="LFSCUtilProof_8cpp_source.html#l00040">LFSCPfVar::MakeV()</a>, <a class="el" href="theory__arith_8h_source.html#l00043">CVC3::MINUS</a>, <a class="el" href="theory__arith_8h_source.html#l00044">CVC3::MULT</a>, <a class="el" href="TReturn_8cpp_source.html#l00024">TReturn::mult_rational()</a>, <a class="el" href="expr__manager_8h_source.html#l00471">CVC3::ExprManager::newRatExpr()</a>, <a class="el" href="LFSCConvert_8h_source.html#l00018">nodeCount</a>, <a class="el" href="LFSCConvert_8h_source.html#l00019">nodeCountTh</a>, <a class="el" href="TReturn_8cpp_source.html#l00125">TReturn::normalize_tr()</a>, <a class="el" href="TReturn_8cpp_source.html#l00084">TReturn::normalize_tret()</a>, <a class="el" href="LFSCObject_8h_source.html#l00029">LFSCObj::nullRat</a>, <a class="el" href="kinds_8h_source.html#l00068">OR</a>, <a class="el" href="kinds_8h_source.html#l00275">PF_APPLY</a>, <a class="el" href="theory__arith_8h_source.html#l00042">CVC3::PLUS</a>, <a class="el" href="LFSCObject_8h_source.html#l00060">LFSCObj::pntNeeded</a>, <a class="el" href="Object_8h_source.html#l00095">Obj::print_error()</a>, <a class="el" href="Util_8cpp_source.html#l00136">print_rational()</a>, <a class="el" href="LFSCObject_8cpp_source.html#l00365">LFSCObj::queryAtomic()</a>, <a class="el" href="LFSCObject_8cpp_source.html#l00386">LFSCObj::queryM()</a>, <a class="el" href="LFSCObject_8cpp_source.html#l00418">LFSCObj::queryMt()</a>, <a class="el" href="kinds_8h_source.html#l00035">TRUE_EXPR</a>, <a class="el" href="expr__manager_8h_source.html#l00280">CVC3::ExprManager::trueExpr()</a>, <a class="el" href="theory__arith_8h_source.html#l00041">CVC3::UMINUS</a>, <a class="el" href="LFSCConvert_8h_source.html#l00020">unodeCount</a>, <a class="el" href="LFSCConvert_8h_source.html#l00021">unodeCountTh</a>, <a class="el" href="LFSCConvert_8cpp_source.html#l00007">vMap</a>, and <a class="el" href="LFSCObject_8cpp_source.html#l00539">LFSCObj::what_is_proven()</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00018">convert()</a>.</p>
</div>
</div>
<a class="anchor" id="afb93601f9c8e8ca8c09f796af341cf76"></a><!-- doxytag: member="LFSCConvert::cvc3_to_lfsc_h" ref="afb93601f9c8e8ca8c09f796af341cf76" args="(const Expr &pf, bool beneath_lc=false, bool rev_pol=false)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classTReturn.html">TReturn</a>* LFSCConvert::cvc3_to_lfsc_h </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">bool </td>
<td class="paramname"><em>beneath_lc</em> = <code>false</code>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>rev_pol</em> = <code>false</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
</div>
</div>
<a class="anchor" id="a751648ad72a06ae67e86a2cbbf798641"></a><!-- doxytag: member="LFSCConvert::do_bso" ref="a751648ad72a06ae67e86a2cbbf798641" args="(const Expr &pf, bool beneath_lc, bool rev_pol, TReturn *t1, TReturn *t2, ostringstream &ose)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classTReturn.html">TReturn</a> * LFSCConvert::do_bso </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">bool </td>
<td class="paramname"><em>beneath_lc</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>rev_pol</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classTReturn.html">TReturn</a> * </td>
<td class="paramname"><em>t1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classTReturn.html">TReturn</a> * </td>
<td class="paramname"><em>t2</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">ostringstream & </td>
<td class="paramname"><em>ose</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCConvert_8cpp_source.html#l01718">1718</a> of file <a class="el" href="LFSCConvert_8cpp_source.html">LFSCConvert.cpp</a>.</p>
<p>References <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#l00024">LFSCObj::debug_conv</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="kinds_8h_source.html#l00061">EQ</a>, <a class="el" href="Object_8h_source.html#l00056">RefPtr< T >::get()</a>, <a class="el" href="TReturn_8cpp_source.html#l00037">TReturn::getL()</a>, <a class="el" href="TReturn_8h_source.html#l00037">TReturn::getLFSCProof()</a>, <a class="el" href="TReturn_8h_source.html#l00038">TReturn::getProvesY()</a>, <a class="el" href="Util_8cpp_source.html#l00158">getRat()</a>, <a class="el" href="kinds_8h_source.html#l00070">IFF</a>, <a class="el" href="Util_8cpp_source.html#l00047">is_eq_kind()</a>, <a class="el" href="Util_8cpp_source.html#l00066">is_opposite()</a>, <a class="el" href="Util_8cpp_source.html#l00017">kind_to_str()</a>, <a class="el" href="LFSCUtilProof_8h_source.html#l00080">LFSCProofGeneric::Make()</a>, <a class="el" href="LFSCUtilProof_8h_source.html#l00017">LFSCProofExpr::Make()</a>, <a class="el" href="LFSCLraProof_8cpp_source.html#l00065">LFSCLraMulC::Make()</a>, <a class="el" href="LFSCLraProof_8cpp_source.html#l00089">LFSCLraSub::Make()</a>, <a class="el" href="LFSCLraProof_8cpp_source.html#l00017">LFSCLraAdd::Make()</a>, <a class="el" href="theory__arith_8h_source.html#l00043">CVC3::MINUS</a>, <a class="el" href="theory__arith_8h_source.html#l00044">CVC3::MULT</a>, <a class="el" href="TReturn_8cpp_source.html#l00125">TReturn::normalize_tr()</a>, <a class="el" href="TReturn_8cpp_source.html#l00084">TReturn::normalize_tret()</a>, <a class="el" href="LFSCObject_8h_source.html#l00029">LFSCObj::nullRat</a>, <a class="el" href="kinds_8h_source.html#l00068">OR</a>, <a class="el" href="theory__arith_8h_source.html#l00042">CVC3::PLUS</a>, <a class="el" href="Object_8h_source.html#l00095">Obj::print_error()</a>, and <a class="el" href="LFSCObject_8cpp_source.html#l00539">LFSCObj::what_is_proven()</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00093">cvc3_to_lfsc()</a>.</p>
</div>
</div>
<a class="anchor" id="ac0a8b733a7e2dcaf23b7489a22c9e171"></a><!-- doxytag: member="LFSCConvert::get_proof_pattern" ref="ac0a8b733a7e2dcaf23b7489a22c9e171" args="(const Expr &pf, Expr &modE)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int LFSCConvert::get_proof_pattern </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="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>modE</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCConvert_8cpp_source.html#l01641">1641</a> of file <a class="el" href="LFSCConvert_8cpp_source.html">LFSCConvert.cpp</a>.</p>
<p>References <a class="el" href="LFSCObject_8h_source.html#l00093">LFSCObj::d_assump_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00155">LFSCObj::d_cnf_add_unit_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00105">LFSCObj::d_eq_symm_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00139">LFSCObj::d_if_lift_rule_str</a>, <a class="el" href="LFSCObject_8h_source.html#l00095">LFSCObj::d_iff_mp_str</a>, and <a class="el" href="LFSCObject_8h_source.html#l00141">LFSCObj::d_var_intro_str</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00093">cvc3_to_lfsc()</a>.</p>
</div>
</div>
<a class="anchor" id="a4632b62661448d6fde086cbe7d260398"></a><!-- doxytag: member="LFSCConvert::make_let_proof" ref="a4632b62661448d6fde086cbe7d260398" args="(LFSCProof *p)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classLFSCProof.html">LFSCProof</a> * LFSCConvert::make_let_proof </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> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCConvert_8cpp_source.html#l01663">1663</a> of file <a class="el" href="LFSCConvert_8cpp_source.html">LFSCConvert.cpp</a>.</p>
<p>References <a class="el" href="expr__map_8h_source.html#l00190">CVC3::ExprMap< Data >::begin()</a>, <a class="el" href="LFSCConvert_8h_source.html#l00013">d_th_trans</a>, <a class="el" href="LFSCConvert_8h_source.html#l00016">d_th_trans_lam</a>, <a class="el" href="LFSCConvert_8h_source.html#l00014">d_th_trans_map</a>, <a class="el" href="LFSCObject_8h_source.html#l00024">LFSCObj::debug_conv</a>, <a class="el" href="expr__map_8h_source.html#l00170">CVC3::ExprMap< Data >::empty()</a>, <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="TReturn_8cpp_source.html#l00037">TReturn::getL()</a>, <a class="el" href="LFSCUtilProof_8h_source.html#l00118">LFSCPfLet::Make()</a>, <a class="el" href="LFSCUtilProof_8cpp_source.html#l00033">LFSCPfVar::Make()</a>, and <a class="el" href="LFSCProof_8h_source.html#l00063">LFSCProof::make_lambda()</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00018">convert()</a>.</p>
</div>
</div>
<a class="anchor" id="a973be3db649311c32e126e0c15c8e51e"></a><!-- doxytag: member="LFSCConvert::make_trusted" ref="a973be3db649311c32e126e0c15c8e51e" args="(const Expr &pf)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classTReturn.html">TReturn</a> * LFSCConvert::make_trusted </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><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCConvert_8cpp_source.html#l01705">1705</a> of file <a class="el" href="LFSCConvert_8cpp_source.html">LFSCConvert.cpp</a>.</p>
<p>References <a class="el" href="LFSCUtilProof_8cpp_source.html#l00033">LFSCPfVar::Make()</a>, <a class="el" href="LFSCUtilProof_8cpp_source.html#l00113">LFSCProofGeneric::MakeStr()</a>, <a class="el" href="LFSCObject_8h_source.html#l00029">LFSCObj::nullRat</a>, <a class="el" href="LFSCObject_8cpp_source.html#l00386">LFSCObj::queryM()</a>, and <a class="el" href="LFSCObject_8cpp_source.html#l00539">LFSCObj::what_is_proven()</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00093">cvc3_to_lfsc()</a>.</p>
</div>
</div>
<a class="anchor" id="acedb89ecccd0488bb5e8425aa8ca5a14"></a><!-- doxytag: member="LFSCConvert::convert" ref="acedb89ecccd0488bb5e8425aa8ca5a14" args="(const Expr &pf)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void LFSCConvert::convert </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><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCConvert_8cpp_source.html#l00018">18</a> of file <a class="el" href="LFSCConvert_8cpp_source.html">LFSCConvert.cpp</a>.</p>
<p>References <a class="el" href="LFSCConvert_8cpp_source.html#l00093">cvc3_to_lfsc()</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="TReturn_8h_source.html#l00037">TReturn::getLFSCProof()</a>, <a class="el" href="TReturn_8h_source.html#l00038">TReturn::getProvesY()</a>, <a class="el" href="LFSCUtilProof_8h_source.html#l00080">LFSCProofGeneric::Make()</a>, <a class="el" href="LFSCConvert_8cpp_source.html#l01663">make_let_proof()</a>, and <a class="el" href="LFSCConvert_8h_source.html#l00010">pfinal</a>.</p>
</div>
</div>
<a class="anchor" id="ad27ba1f700e2b8950d11e4fa8edd325b"></a><!-- doxytag: member="LFSCConvert::getLFSCProof" ref="ad27ba1f700e2b8950d11e4fa8edd325b" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classLFSCProof.html">LFSCProof</a>* LFSCConvert::getLFSCProof </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="LFSCConvert_8h_source.html#l00051">51</a> of file <a class="el" href="LFSCConvert_8h_source.html">LFSCConvert.h</a>.</p>
<p>References <a class="el" href="Object_8h_source.html#l00056">RefPtr< T >::get()</a>, and <a class="el" href="LFSCConvert_8h_source.html#l00010">pfinal</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00093">cvc3_to_lfsc()</a>.</p>
</div>
</div>
<hr/><h2>Member Data Documentation</h2>
<a class="anchor" id="ac93000eef387bdfa14a2b3994a241c00"></a><!-- doxytag: member="LFSCConvert::pfinal" ref="ac93000eef387bdfa14a2b3994a241c00" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classRefPtr.html">RefPtr</a>< <a class="el" href="classLFSCProof.html">LFSCProof</a> > <a class="el" href="classLFSCConvert.html#ac93000eef387bdfa14a2b3994a241c00">LFSCConvert::pfinal</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCConvert_8h_source.html#l00010">10</a> of file <a class="el" href="LFSCConvert_8h_source.html">LFSCConvert.h</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00018">convert()</a>, and <a class="el" href="LFSCConvert_8h_source.html#l00051">getLFSCProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a10db6bada50083de6660a11f68e4431d"></a><!-- doxytag: member="LFSCConvert::d_th_trans" ref="a10db6bada50083de6660a11f68e4431d" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a><bool> <a class="el" href="classLFSCConvert.html#a10db6bada50083de6660a11f68e4431d">LFSCConvert::d_th_trans</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCConvert_8h_source.html#l00013">13</a> of file <a class="el" href="LFSCConvert_8h_source.html">LFSCConvert.h</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00093">cvc3_to_lfsc()</a>, and <a class="el" href="LFSCConvert_8cpp_source.html#l01663">make_let_proof()</a>.</p>
</div>
</div>
<a class="anchor" id="a21833bc8f1a0982794266a2f24abf3d8"></a><!-- doxytag: member="LFSCConvert::d_th_trans_map" ref="a21833bc8f1a0982794266a2f24abf3d8" args="[2]" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a><<a class="el" href="classTReturn.html">TReturn</a>*> <a class="el" href="classLFSCConvert.html#a21833bc8f1a0982794266a2f24abf3d8">LFSCConvert::d_th_trans_map</a>[2]<code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCConvert_8h_source.html#l00014">14</a> of file <a class="el" href="LFSCConvert_8h_source.html">LFSCConvert.h</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00093">cvc3_to_lfsc()</a>, and <a class="el" href="LFSCConvert_8cpp_source.html#l01663">make_let_proof()</a>.</p>
</div>
</div>
<a class="anchor" id="ab6740d10097cad6ab22f2d5976163c30"></a><!-- doxytag: member="LFSCConvert::d_th_trans_lam" ref="ab6740d10097cad6ab22f2d5976163c30" args="[2]" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::map<<a class="el" href="classTReturn.html">TReturn</a>*, bool> <a class="el" href="classLFSCConvert.html#ab6740d10097cad6ab22f2d5976163c30">LFSCConvert::d_th_trans_lam</a>[2]<code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCConvert_8h_source.html#l00016">16</a> of file <a class="el" href="LFSCConvert_8h_source.html">LFSCConvert.h</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00093">cvc3_to_lfsc()</a>, and <a class="el" href="LFSCConvert_8cpp_source.html#l01663">make_let_proof()</a>.</p>
</div>
</div>
<a class="anchor" id="a56e0bda1943b3a0dbe37fedb9ec95bb7"></a><!-- doxytag: member="LFSCConvert::nodeCount" ref="a56e0bda1943b3a0dbe37fedb9ec95bb7" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classLFSCConvert.html#a56e0bda1943b3a0dbe37fedb9ec95bb7">LFSCConvert::nodeCount</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCConvert_8h_source.html#l00018">18</a> of file <a class="el" href="LFSCConvert_8h_source.html">LFSCConvert.h</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00093">cvc3_to_lfsc()</a>, and <a class="el" href="LFSCConvert_8cpp_source.html#l00009">LFSCConvert()</a>.</p>
</div>
</div>
<a class="anchor" id="ad79a7dc7af33a6a7f0168d7c5ed9a60e"></a><!-- doxytag: member="LFSCConvert::nodeCountTh" ref="ad79a7dc7af33a6a7f0168d7c5ed9a60e" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classLFSCConvert.html#ad79a7dc7af33a6a7f0168d7c5ed9a60e">LFSCConvert::nodeCountTh</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCConvert_8h_source.html#l00019">19</a> of file <a class="el" href="LFSCConvert_8h_source.html">LFSCConvert.h</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00093">cvc3_to_lfsc()</a>, and <a class="el" href="LFSCConvert_8cpp_source.html#l00009">LFSCConvert()</a>.</p>
</div>
</div>
<a class="anchor" id="a30a3b3353b977cc9b3e359f3aa8e2876"></a><!-- doxytag: member="LFSCConvert::unodeCount" ref="a30a3b3353b977cc9b3e359f3aa8e2876" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classLFSCConvert.html#a30a3b3353b977cc9b3e359f3aa8e2876">LFSCConvert::unodeCount</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCConvert_8h_source.html#l00020">20</a> of file <a class="el" href="LFSCConvert_8h_source.html">LFSCConvert.h</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00093">cvc3_to_lfsc()</a>, and <a class="el" href="LFSCConvert_8cpp_source.html#l00009">LFSCConvert()</a>.</p>
</div>
</div>
<a class="anchor" id="afc452237398520ff33c13c05d95d3083"></a><!-- doxytag: member="LFSCConvert::unodeCountTh" ref="afc452237398520ff33c13c05d95d3083" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classLFSCConvert.html#afc452237398520ff33c13c05d95d3083">LFSCConvert::unodeCountTh</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCConvert_8h_source.html#l00021">21</a> of file <a class="el" href="LFSCConvert_8h_source.html">LFSCConvert.h</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00093">cvc3_to_lfsc()</a>, and <a class="el" href="LFSCConvert_8cpp_source.html#l00009">LFSCConvert()</a>.</p>
</div>
</div>
<a class="anchor" id="a49a4bb15eeceb470be396b6742f0c974"></a><!-- doxytag: member="LFSCConvert::ignore_theory_lemmas" ref="a49a4bb15eeceb470be396b6742f0c974" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classLFSCConvert.html#a49a4bb15eeceb470be396b6742f0c974">LFSCConvert::ignore_theory_lemmas</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="LFSCConvert_8h_source.html#l00023">23</a> of file <a class="el" href="LFSCConvert_8h_source.html">LFSCConvert.h</a>.</p>
<p>Referenced by <a class="el" href="LFSCConvert_8cpp_source.html#l00093">cvc3_to_lfsc()</a>, and <a class="el" href="LFSCConvert_8cpp_source.html#l00009">LFSCConvert()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="LFSCConvert_8h_source.html">LFSCConvert.h</a></li>
<li><a class="el" href="LFSCConvert_8cpp_source.html">LFSCConvert.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>
