<!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: LFSCObject.cpp Source File</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li><a href="annotated.html"><span>Classes</span></a></li>
<li class="current"><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="files.html"><span>File List</span></a></li>
<li><a href="globals.html"><span>File Members</span></a></li>
</ul>
</div>
<div class="header">
<div class="headertitle">
<div class="title">LFSCObject.cpp</div> </div>
</div>
<div class="contents">
<a href="LFSCObject_8cpp.html">Go to the documentation of this file.</a><div class="fragment"><pre class="fragment"><a name="l00001"></a>00001 <span class="preprocessor">#include "<a class="code" href="LFSCObject_8h.html">LFSCObject.h</a>"</span>
<a name="l00002"></a>00002
<a name="l00003"></a>00003 <a class="code" href="classLFSCPrinter.html">LFSCPrinter</a>* <a class="code" href="classLFSCObj.html#a2c02fa7d095d8fd333578ca552c5ef04">LFSCObj::printer</a>;
<a name="l00004"></a>00004 <span class="keywordtype">int</span> <a class="code" href="classLFSCObj.html#a66bb07d4b7e20596d9f324c5f3ce689a">LFSCObj::formula_i</a> = 1;
<a name="l00005"></a>00005 <span class="keywordtype">int</span> <a class="code" href="classLFSCObj.html#aa53d3da9dab58f7e4670db1619d8947e">LFSCObj::term_i</a> = 1;
<a name="l00006"></a>00006 <span class="keywordtype">int</span> <a class="code" href="classLFSCObj.html#acd1b788ca21cbc01682501f940f1a4f5">LFSCObj::trusted_i</a> = 1;
<a name="l00007"></a>00007 <span class="keywordtype">int</span> <a class="code" href="classLFSCObj.html#a1c1342a9b79a1a2406a9a2c3c958addb">LFSCObj::tnorm_i</a> = 1;
<a name="l00008"></a>00008 <span class="keywordtype">bool</span> <a class="code" href="classLFSCObj.html#ac43ede316cf83e0eb037d3f5291f4074">LFSCObj::debug_conv</a>;
<a name="l00009"></a>00009 <span class="keywordtype">bool</span> <a class="code" href="classLFSCObj.html#ab1fc8cb8c7ac32a1d117877c629cc178">LFSCObj::debug_var</a>;
<a name="l00010"></a>00010 <span class="keywordtype">bool</span> <a class="code" href="classLFSCObj.html#a81a07dd023d7a37bff9fa514fff9a787">LFSCObj::cvc3_mimic</a>;
<a name="l00011"></a>00011 <span class="keywordtype">bool</span> <a class="code" href="classLFSCObj.html#a5aa64bcaf0af2b4b52e75c9354c7409f">LFSCObj::cvc3_mimic_input</a>;
<a name="l00012"></a>00012 <span class="keywordtype">int</span> <a class="code" href="classLFSCObj.html#ae9fad86fecb58ee3be0b330a37acecae">LFSCObj::lfsc_mode</a>;
<a name="l00013"></a>00013 <a class="code" href="classCVC3_1_1Rational.html">Rational</a> <a class="code" href="classLFSCObj.html#a379c9c653101afe6c2db9c58cd4c81e1">LFSCObj::nullRat</a>;
<a name="l00014"></a>00014 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap< int ></a> <a class="code" href="classLFSCObj.html#afe177d3bd72f6abd93377e6661218c1b">LFSCObj::nnode_map</a>;
<a name="l00015"></a>00015 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap< Expr ></a> <a class="code" href="classLFSCObj.html#a6a3e7f3fc21a2291ad793eba84f76a4c">LFSCObj::cas_map</a>;
<a name="l00016"></a>00016 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap< Expr ></a> <a class="code" href="classLFSCObj.html#a43226f1b59b50c73af82f2f1f7a8b2d2">LFSCObj::skolem_vars</a>;
<a name="l00017"></a>00017 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap< bool ></a> <a class="code" href="classLFSCObj.html#a36e0f50de989f0c82ada5d7f968268de">LFSCObj::temp_visited</a>;
<a name="l00018"></a>00018 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<int></a> <a class="code" href="classLFSCObj.html#a9741b35e18a1dc2dd135fb85face8288">LFSCObj::d_formulas</a>;
<a name="l00019"></a>00019 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<int></a> <a class="code" href="classLFSCObj.html#aa62d284471e6be2f733711bc01037ded">LFSCObj::d_trusted</a>;
<a name="l00020"></a>00020 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<int></a> <a class="code" href="classLFSCObj.html#a53e3990d17d606c9dd5b28b7950d5cd5">LFSCObj::d_pn</a>;
<a name="l00021"></a>00021 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<int></a> <a class="code" href="classLFSCObj.html#aa4fa55b8acd57b674418c69dee792fd7">LFSCObj::d_pn_form</a>;
<a name="l00022"></a>00022 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap< int ></a> <a class="code" href="classLFSCObj.html#aa8ad0677d224a27c6b7376619a9a037d">LFSCObj::d_terms</a>;
<a name="l00023"></a>00023 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<bool></a> <a class="code" href="classLFSCObj.html#ae7a9bf905373af442a0ef70db558440c">LFSCObj::input_vars</a>;
<a name="l00024"></a>00024 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<bool></a> <a class="code" href="classLFSCObj.html#a0b89bc2bbc7e2bb9474026ff4b111302">LFSCObj::input_preds</a>;
<a name="l00025"></a>00025 std::map< int, bool > <a class="code" href="classLFSCObj.html#a03e6dd5795f3ad53cb25667fecd692a7">LFSCObj::pntNeeded</a>;
<a name="l00026"></a>00026 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<bool></a> <a class="code" href="classLFSCObj.html#af9962ba4dfb9b457c96365924e018ff3">LFSCObj::d_formulas_printed</a>;
<a name="l00027"></a>00027 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#ad4d5ea192b766a7020fdfc7a462e99fe">LFSCObj::d_pf_expr</a>;
<a name="l00028"></a>00028 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<bool></a> <a class="code" href="classLFSCObj.html#ad8e86790f4adb2570714da3d4f7eb8c5">LFSCObj::d_assump_map</a>;
<a name="l00029"></a>00029 <span class="comment">//differentiate between variables and rules</span>
<a name="l00030"></a>00030 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<bool></a> <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">LFSCObj::d_rules</a>;
<a name="l00031"></a>00031 <span class="comment">//boolean resultion rules</span>
<a name="l00032"></a>00032 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a515cbe72a3391aebb245ca77c70b7f76">LFSCObj::d_bool_res_str</a>;
<a name="l00033"></a>00033 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a49af9dbc7a770f4372be4642e32f39c8">LFSCObj::d_assump_str</a>;
<a name="l00034"></a>00034 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a482a3a5c4c6ca22f8bc08f7e8942b7be">LFSCObj::d_iff_mp_str</a>;
<a name="l00035"></a>00035 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a71dc551ca9a26bfa90d971e5627293fb">LFSCObj::d_impl_mp_str</a>;
<a name="l00036"></a>00036 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#af1c7635ff7d9d7a6d4ca6d5f524e838e">LFSCObj::d_iff_trans_str</a>;
<a name="l00037"></a>00037 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#ae75e0ca40a864dac2009ac40da5c83d6">LFSCObj::d_real_shadow_str</a>;
<a name="l00038"></a>00038 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#acebf70a838fce6dbdb1ad46c2ce277b9">LFSCObj::d_cycle_conflict_str</a>;
<a name="l00039"></a>00039 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a32683494b48bed158c9373f18af0b524">LFSCObj::d_real_shadow_eq_str</a>;
<a name="l00040"></a>00040 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a3806475a625a97dc4eeaecd3ecc82eee">LFSCObj::d_basic_subst_op_str</a>;
<a name="l00041"></a>00041 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a40c4f5943b21296bb1ba3b250a39be5b">LFSCObj::d_mult_ineqn_str</a>;
<a name="l00042"></a>00042 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#ae68fd62549e5191b31a2a9ff6e919033">LFSCObj::d_right_minus_left_str</a>;
<a name="l00043"></a>00043 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a988780a33a8cd1c4a79ada79535e3133">LFSCObj::d_eq_trans_str</a>;
<a name="l00044"></a>00044 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a008e6fb099a79edcff2f47ffd8c1bf84">LFSCObj::d_eq_symm_str</a>;
<a name="l00045"></a>00045 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a088e49cbb378c0ac9e6c4515cc6b99b8">LFSCObj::d_canon_plus_str</a>;
<a name="l00046"></a>00046 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a18907b513101487ecbdc956b8d9884ce">LFSCObj::d_refl_str</a>;
<a name="l00047"></a>00047 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#afe9d28e7d8efbeb59913023779116cdb">LFSCObj::d_cnf_convert_str</a>;
<a name="l00048"></a>00048 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a4419339e214cefcb4de40cfa1e318c88">LFSCObj::d_learned_clause_str</a>;
<a name="l00049"></a>00049 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#ae1b08b3ef34d91064a5d990c573916e8">LFSCObj::d_minus_to_plus_str</a>;
<a name="l00050"></a>00050 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a59fc7e6797f9f710385d96dd63fe3c7a">LFSCObj::d_plus_predicate_str</a>;
<a name="l00051"></a>00051 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#ad1ebf052401eba516c3328f6a99ab389">LFSCObj::d_negated_inequality_str</a>;
<a name="l00052"></a>00052 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a11a0ed93bc57d8787486d8c663dd1369">LFSCObj::d_flip_inequality_str</a>;
<a name="l00053"></a>00053 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#ab1cfbe69faad1806adce5f1d83b6ad06">LFSCObj::d_optimized_subst_op_str</a>;
<a name="l00054"></a>00054 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a9037ec508663dc84ab2d72631171c9e8">LFSCObj::d_iff_true_elim_str</a>;
<a name="l00055"></a>00055 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a033351a8f7c305990b272c70f210cf6c">LFSCObj::d_basic_subst_op1_str</a>;
<a name="l00056"></a>00056 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#ac1e17603638979d251aa6bce9fbf6443">LFSCObj::d_basic_subst_op0_str</a>;
<a name="l00057"></a>00057 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a59423ce52bac130c25372804f1a3b2fa">LFSCObj::d_canon_mult_str</a>;
<a name="l00058"></a>00058 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a8f8d5a3b46f96de7a286c109ba89002b">LFSCObj::d_canon_invert_divide_str</a>;
<a name="l00059"></a>00059 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a5e8f7307cd69eaa8381b94a55cb6b5f7">LFSCObj::d_iff_true_str</a>;
<a name="l00060"></a>00060 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#ab77f0a4102ceaaba81aae959b38fff1b">LFSCObj::d_mult_eqn_str</a>;
<a name="l00061"></a>00061 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a97b66c2bb2a7cf5475969f4929802cb2">LFSCObj::d_rewrite_eq_symm_str</a>;
<a name="l00062"></a>00062 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a5eb9b49376b9c44fdd1c879a56cb4927">LFSCObj::d_implyWeakerInequality_str</a>;
<a name="l00063"></a>00063 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#ab93f73a7292e8f8c93c7579ed4b10258">LFSCObj::d_implyWeakerInequalityDiffLogic_str</a>;
<a name="l00064"></a>00064 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a6183ebe28c2d6284ad2924348f27c0a0">LFSCObj::d_imp_mp_str</a>;
<a name="l00065"></a>00065 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a8ee48c649017b77e06deda136fde968d">LFSCObj::d_rewrite_implies_str</a>;
<a name="l00066"></a>00066 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a2c2af826a423bd5059c20462d664bd9c">LFSCObj::d_rewrite_or_str</a>;
<a name="l00067"></a>00067 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#ad5e78e0799f54a4aa89dcce1b5ef1591">LFSCObj::d_rewrite_and_str</a>;
<a name="l00068"></a>00068 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a881021008ed360cbc5e7573e52fc7ec4">LFSCObj::d_rewrite_iff_symm_str</a>;
<a name="l00069"></a>00069 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a11a736d065275de2558ac8ba4ab624e5">LFSCObj::d_iff_not_false_str</a>;
<a name="l00070"></a>00070 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#ac6f3e4aff2a0e7cd2890b089ee5520df">LFSCObj::d_iff_false_str</a>;
<a name="l00071"></a>00071 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#aa69b286d7f0dcc65e178cb7f189ce4e7">LFSCObj::d_iff_false_elim_str</a>;
<a name="l00072"></a>00072 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#ab7930db598045de2b9b715d810f4821a">LFSCObj::d_not_to_iff_str</a>;
<a name="l00073"></a>00073 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a58583da73255b5ad31d3415e6eecb200">LFSCObj::d_not_not_elim_str</a>;
<a name="l00074"></a>00074 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a8a9baf936097ef0146666cf6a0019d86">LFSCObj::d_const_predicate_str</a>;
<a name="l00075"></a>00075 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#abe33b1cf4b7a701afd26466b8bbb3b3c">LFSCObj::d_rewrite_not_not_str</a>;
<a name="l00076"></a>00076 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a182c63a54b3d0435c67fd5dd212a43b1">LFSCObj::d_rewrite_not_true_str</a>;
<a name="l00077"></a>00077 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a07f5cf7de5d7bd2f51a7dab8e8ced3ba">LFSCObj::d_rewrite_not_false_str</a>;
<a name="l00078"></a>00078 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#aa0d31e1ccc537ed4ec541e109b8533ee">LFSCObj::d_if_lift_rule_str</a>;
<a name="l00079"></a>00079 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#ae62723cd3b241eb95c7d637fbbf25414">LFSCObj::d_CNFITE_str</a>;
<a name="l00080"></a>00080 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#aa8be0f6329de8878837686420aee5092">LFSCObj::d_var_intro_str</a>;
<a name="l00081"></a>00081 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#ac62c8dc4c83d5a3e19cfdce0ef60cd0e">LFSCObj::d_int_const_eq_str</a>;
<a name="l00082"></a>00082 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a1eb48aeb323149091a40c35962d087b0">LFSCObj::d_rewrite_eq_refl_str</a>;
<a name="l00083"></a>00083 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a06306648e20078ba6436aee671dfdf5e">LFSCObj::d_iff_symm_str</a>;
<a name="l00084"></a>00084 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#ae22d245587e43b53436e8bdf99914c5c">LFSCObj::d_rewrite_iff_str</a>;
<a name="l00085"></a>00085 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a4d5aacd643a90b9082037521c561eebc">LFSCObj::d_implyNegatedInequality_str</a>;
<a name="l00086"></a>00086 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#ad239f7556c548642b93bbad7808e4d08">LFSCObj::d_uminus_to_mult_str</a>;
<a name="l00087"></a>00087 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#aecc91fcc3b651c68ba124c3d205d6c3d">LFSCObj::d_lessThan_To_LE_rhs_rwr_str</a>;
<a name="l00088"></a>00088 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#aa8367786a66947c4c6e390918e995eb9">LFSCObj::d_rewrite_ite_same_str</a>;
<a name="l00089"></a>00089 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a1c4d27683bd50cfb2a3598aed1eaa52b">LFSCObj::d_andE_str</a>;
<a name="l00090"></a>00090 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#ad5b7a93ffe8bb6c33527008d0584c5ac">LFSCObj::d_implyEqualities_str</a>;
<a name="l00091"></a>00091 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#ad016421378038e3ceaee715f0ed67cb3">LFSCObj::d_CNF_str</a>;
<a name="l00092"></a>00092 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#aae6e50323f43de730d052249b3540603">LFSCObj::d_cnf_add_unit_str</a>;
<a name="l00093"></a>00093 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a06ba8bfd2f179eaec49222d62ff3b914">LFSCObj::d_minisat_proof_str</a>;
<a name="l00094"></a>00094 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a3ce45729a0273ed5c43dba4b9d439cc1">LFSCObj::d_or_final_s</a>;
<a name="l00095"></a>00095 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a8052510576f68336a8a9937f8f8584c1">LFSCObj::d_and_final_s</a>;
<a name="l00096"></a>00096 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a5b534911a5916e4d03589364030b0881">LFSCObj::d_ite_s</a>;
<a name="l00097"></a>00097 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#af19867df31a4aa59d558a1e7bb3cf3d4">LFSCObj::d_iff_s</a>;
<a name="l00098"></a>00098 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#ac682735316d59354edaae5db3025ff3e">LFSCObj::d_imp_s</a>;
<a name="l00099"></a>00099 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a2508c14b5f7432f7ee0241603d5deb88">LFSCObj::d_or_mid_s</a>;
<a name="l00100"></a>00100 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a155d135b8fbc4eef20388f07ce30453d">LFSCObj::d_and_mid_s</a>;
<a name="l00101"></a>00101 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a5d4ef3ef402573511319acf31a482587">LFSCObj::d_addInequalities_str</a>;
<a name="l00102"></a>00102
<a name="l00103"></a>00103
<a name="l00104"></a><a class="code" href="classLFSCObj.html#aa085ed1c617cfdf6536863782cf88a26">00104</a> <span class="keywordtype">void</span> <a class="code" href="classObj.html#a6bbb1d0fa8c4fc2d8a574ff9c4adf918">LFSCObj::initialize</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& pf_expr, <span class="keywordtype">int</span> lfscm )
<a name="l00105"></a>00105 {
<a name="l00106"></a>00106 <a class="code" href="classLFSCObj.html#ae9fad86fecb58ee3be0b330a37acecae">lfsc_mode</a> = lfscm;
<a name="l00107"></a>00107 <a class="code" href="classLFSCObj.html#a81a07dd023d7a37bff9fa514fff9a787">cvc3_mimic</a> = <a class="code" href="classLFSCObj.html#ae9fad86fecb58ee3be0b330a37acecae">lfsc_mode</a>==2 || <a class="code" href="classLFSCObj.html#ae9fad86fecb58ee3be0b330a37acecae">lfsc_mode</a>==7 || (<a class="code" href="classLFSCObj.html#ae9fad86fecb58ee3be0b330a37acecae">lfsc_mode</a>>=20 && <a class="code" href="classLFSCObj.html#ae9fad86fecb58ee3be0b330a37acecae">lfsc_mode</a> <= 29 );
<a name="l00108"></a>00108 <a class="code" href="classLFSCObj.html#a5aa64bcaf0af2b4b52e75c9354c7409f">cvc3_mimic_input</a> = <a class="code" href="classLFSCObj.html#a81a07dd023d7a37bff9fa514fff9a787">cvc3_mimic</a>;
<a name="l00109"></a>00109 <a class="code" href="classLFSCObj.html#ac43ede316cf83e0eb037d3f5291f4074">debug_conv</a> = <a class="code" href="classLFSCObj.html#ae9fad86fecb58ee3be0b330a37acecae">lfsc_mode</a>%10 == 0;
<a name="l00110"></a>00110 <a class="code" href="classLFSCObj.html#ab1fc8cb8c7ac32a1d117877c629cc178">debug_var</a> = <a class="code" href="classLFSCObj.html#ae9fad86fecb58ee3be0b330a37acecae">lfsc_mode</a>>10 && ( <a class="code" href="classLFSCObj.html#ae9fad86fecb58ee3be0b330a37acecae">lfsc_mode</a>%10 == 1 );
<a name="l00111"></a>00111
<a name="l00112"></a>00112 <a class="code" href="classLFSCObj.html#ad4d5ea192b766a7020fdfc7a462e99fe">d_pf_expr</a> = pf_expr;
<a name="l00113"></a>00113 <span class="comment">// initialize rules</span>
<a name="l00114"></a>00114 <a class="code" href="classLFSCObj.html#a515cbe72a3391aebb245ca77c70b7f76">d_bool_res_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"bool_resolution"</span>);
<a name="l00115"></a>00115 <a class="code" href="classLFSCObj.html#a49af9dbc7a770f4372be4642e32f39c8">d_assump_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"assumptions"</span>);
<a name="l00116"></a>00116 <a class="code" href="classLFSCObj.html#a482a3a5c4c6ca22f8bc08f7e8942b7be">d_iff_mp_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"iff_mp"</span>);
<a name="l00117"></a>00117 <a class="code" href="classLFSCObj.html#a71dc551ca9a26bfa90d971e5627293fb">d_impl_mp_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"impl_mp"</span>);
<a name="l00118"></a>00118 <a class="code" href="classLFSCObj.html#af1c7635ff7d9d7a6d4ca6d5f524e838e">d_iff_trans_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"iff_trans"</span>);
<a name="l00119"></a>00119 <a class="code" href="classLFSCObj.html#ae75e0ca40a864dac2009ac40da5c83d6">d_real_shadow_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"real_shadow"</span>);
<a name="l00120"></a>00120 <a class="code" href="classLFSCObj.html#acebf70a838fce6dbdb1ad46c2ce277b9">d_cycle_conflict_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"cycleConflict"</span>);
<a name="l00121"></a>00121 <a class="code" href="classLFSCObj.html#a32683494b48bed158c9373f18af0b524">d_real_shadow_eq_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"real_shadow_eq"</span>);
<a name="l00122"></a>00122 <a class="code" href="classLFSCObj.html#a3806475a625a97dc4eeaecd3ecc82eee">d_basic_subst_op_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"basic_subst_op"</span>);
<a name="l00123"></a>00123 <a class="code" href="classLFSCObj.html#a40c4f5943b21296bb1ba3b250a39be5b">d_mult_ineqn_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"mult_ineqn"</span>);
<a name="l00124"></a>00124 <a class="code" href="classLFSCObj.html#a11a0ed93bc57d8787486d8c663dd1369">d_flip_inequality_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"flip_inequality"</span>);
<a name="l00125"></a>00125 <a class="code" href="classLFSCObj.html#ae68fd62549e5191b31a2a9ff6e919033">d_right_minus_left_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"right_minus_left"</span>);
<a name="l00126"></a>00126 <a class="code" href="classLFSCObj.html#a988780a33a8cd1c4a79ada79535e3133">d_eq_trans_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"eq_trans"</span>);
<a name="l00127"></a>00127 <a class="code" href="classLFSCObj.html#a008e6fb099a79edcff2f47ffd8c1bf84">d_eq_symm_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"eq_symm"</span>);
<a name="l00128"></a>00128 <a class="code" href="classLFSCObj.html#a088e49cbb378c0ac9e6c4515cc6b99b8">d_canon_plus_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"canon_plus"</span>);
<a name="l00129"></a>00129 <a class="code" href="classLFSCObj.html#a18907b513101487ecbdc956b8d9884ce">d_refl_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"refl"</span>);
<a name="l00130"></a>00130 <a class="code" href="classLFSCObj.html#afe9d28e7d8efbeb59913023779116cdb">d_cnf_convert_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"cnf_convert"</span>);
<a name="l00131"></a>00131 <a class="code" href="classLFSCObj.html#a4419339e214cefcb4de40cfa1e318c88">d_learned_clause_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"learned_clause"</span>);
<a name="l00132"></a>00132 <a class="code" href="classLFSCObj.html#ae1b08b3ef34d91064a5d990c573916e8">d_minus_to_plus_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"minus_to_plus"</span>);
<a name="l00133"></a>00133 <a class="code" href="classLFSCObj.html#a59fc7e6797f9f710385d96dd63fe3c7a">d_plus_predicate_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"plus_predicate"</span>);
<a name="l00134"></a>00134 <a class="code" href="classLFSCObj.html#a11a0ed93bc57d8787486d8c663dd1369">d_flip_inequality_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"flip_inequality"</span>);
<a name="l00135"></a>00135 <a class="code" href="classLFSCObj.html#ad1ebf052401eba516c3328f6a99ab389">d_negated_inequality_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"negated_inequality"</span>);
<a name="l00136"></a>00136
<a name="l00137"></a>00137 <a class="code" href="classLFSCObj.html#a9037ec508663dc84ab2d72631171c9e8">d_iff_true_elim_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"iff_true_elim"</span>);
<a name="l00138"></a>00138 <a class="code" href="classLFSCObj.html#a033351a8f7c305990b272c70f210cf6c">d_basic_subst_op1_str</a>= pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"basic_subst_op1"</span>);
<a name="l00139"></a>00139 <a class="code" href="classLFSCObj.html#ac1e17603638979d251aa6bce9fbf6443">d_basic_subst_op0_str</a>= pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"basic_subst_op0"</span>);
<a name="l00140"></a>00140 <a class="code" href="classLFSCObj.html#a59423ce52bac130c25372804f1a3b2fa">d_canon_mult_str</a>= pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"canon_mult"</span>);
<a name="l00141"></a>00141 <a class="code" href="classLFSCObj.html#a8f8d5a3b46f96de7a286c109ba89002b">d_canon_invert_divide_str</a>= pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"canon_invert_divide"</span>);
<a name="l00142"></a>00142 <a class="code" href="classLFSCObj.html#a5e8f7307cd69eaa8381b94a55cb6b5f7">d_iff_true_str</a>= pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"iff_true"</span>);
<a name="l00143"></a>00143 <a class="code" href="classLFSCObj.html#ab77f0a4102ceaaba81aae959b38fff1b">d_mult_eqn_str</a>= pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"mult_eqn"</span>);
<a name="l00144"></a>00144 <a class="code" href="classLFSCObj.html#a97b66c2bb2a7cf5475969f4929802cb2">d_rewrite_eq_symm_str</a>= pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"rewrite_eq_symm"</span>);
<a name="l00145"></a>00145 <a class="code" href="classLFSCObj.html#ab1cfbe69faad1806adce5f1d83b6ad06">d_optimized_subst_op_str</a>= pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"optimized_subst_op"</span>);
<a name="l00146"></a>00146 <a class="code" href="classLFSCObj.html#a5eb9b49376b9c44fdd1c879a56cb4927">d_implyWeakerInequality_str</a>= pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"implyWeakerInequality"</span>);
<a name="l00147"></a>00147 <a class="code" href="classLFSCObj.html#ab93f73a7292e8f8c93c7579ed4b10258">d_implyWeakerInequalityDiffLogic_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"implyWeakerInequalityDiffLogic"</span>);
<a name="l00148"></a>00148 <a class="code" href="classLFSCObj.html#a6183ebe28c2d6284ad2924348f27c0a0">d_imp_mp_str</a>= pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"impl_mp"</span>);
<a name="l00149"></a>00149 <a class="code" href="classLFSCObj.html#a8ee48c649017b77e06deda136fde968d">d_rewrite_implies_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"rewrite_implies"</span>);
<a name="l00150"></a>00150 <a class="code" href="classLFSCObj.html#a2c2af826a423bd5059c20462d664bd9c">d_rewrite_or_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"rewrite_or"</span>);
<a name="l00151"></a>00151 <a class="code" href="classLFSCObj.html#ad5e78e0799f54a4aa89dcce1b5ef1591">d_rewrite_and_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"rewrite_and"</span>);
<a name="l00152"></a>00152 <a class="code" href="classLFSCObj.html#a881021008ed360cbc5e7573e52fc7ec4">d_rewrite_iff_symm_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"rewrite_iff_symm"</span>);
<a name="l00153"></a>00153 <a class="code" href="classLFSCObj.html#a11a736d065275de2558ac8ba4ab624e5">d_iff_not_false_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"iff_not_false"</span>);
<a name="l00154"></a>00154 <a class="code" href="classLFSCObj.html#ac6f3e4aff2a0e7cd2890b089ee5520df">d_iff_false_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"iff_false"</span>);
<a name="l00155"></a>00155 <a class="code" href="classLFSCObj.html#aa69b286d7f0dcc65e178cb7f189ce4e7">d_iff_false_elim_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"iff_false_elim"</span>);
<a name="l00156"></a>00156 <a class="code" href="classLFSCObj.html#ab7930db598045de2b9b715d810f4821a">d_not_to_iff_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"not_to_iff"</span>);
<a name="l00157"></a>00157 <a class="code" href="classLFSCObj.html#a58583da73255b5ad31d3415e6eecb200">d_not_not_elim_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"not_not_elim"</span>);
<a name="l00158"></a>00158 <a class="code" href="classLFSCObj.html#a8a9baf936097ef0146666cf6a0019d86">d_const_predicate_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"const_predicate"</span>);
<a name="l00159"></a>00159 <a class="code" href="classLFSCObj.html#abe33b1cf4b7a701afd26466b8bbb3b3c">d_rewrite_not_not_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"rewrite_not_not"</span>);
<a name="l00160"></a>00160 <a class="code" href="classLFSCObj.html#a182c63a54b3d0435c67fd5dd212a43b1">d_rewrite_not_true_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"rewrite_not_true"</span>);
<a name="l00161"></a>00161 <a class="code" href="classLFSCObj.html#a07f5cf7de5d7bd2f51a7dab8e8ced3ba">d_rewrite_not_false_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"rewrite_not_false"</span>);
<a name="l00162"></a>00162
<a name="l00163"></a>00163 <a class="code" href="classLFSCObj.html#aa0d31e1ccc537ed4ec541e109b8533ee">d_if_lift_rule_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"if_lift_rule"</span>);
<a name="l00164"></a>00164 <a class="code" href="classLFSCObj.html#ae62723cd3b241eb95c7d637fbbf25414">d_CNFITE_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"CNFITE"</span>);
<a name="l00165"></a>00165 <a class="code" href="classLFSCObj.html#aa8be0f6329de8878837686420aee5092">d_var_intro_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"var_intro"</span>);
<a name="l00166"></a>00166 <a class="code" href="classLFSCObj.html#ac62c8dc4c83d5a3e19cfdce0ef60cd0e">d_int_const_eq_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"int_const_eq"</span>);
<a name="l00167"></a>00167 <a class="code" href="classLFSCObj.html#a1eb48aeb323149091a40c35962d087b0">d_rewrite_eq_refl_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"rewrite_eq_refl"</span>);
<a name="l00168"></a>00168 <a class="code" href="classLFSCObj.html#a06306648e20078ba6436aee671dfdf5e">d_iff_symm_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"iff_symm"</span>);
<a name="l00169"></a>00169 <a class="code" href="classLFSCObj.html#ae22d245587e43b53436e8bdf99914c5c">d_rewrite_iff_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"rewrite_iff"</span>);
<a name="l00170"></a>00170 <a class="code" href="classLFSCObj.html#a4d5aacd643a90b9082037521c561eebc">d_implyNegatedInequality_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"implyNegatedInequality"</span>);
<a name="l00171"></a>00171 <a class="code" href="classLFSCObj.html#ad239f7556c548642b93bbad7808e4d08">d_uminus_to_mult_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"uminus_to_mult"</span>);
<a name="l00172"></a>00172 <a class="code" href="classLFSCObj.html#aecc91fcc3b651c68ba124c3d205d6c3d">d_lessThan_To_LE_rhs_rwr_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"lessThan_To_LE_rhs_rwr"</span>);
<a name="l00173"></a>00173
<a name="l00174"></a>00174 <a class="code" href="classLFSCObj.html#ad016421378038e3ceaee715f0ed67cb3">d_CNF_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"CNF"</span>);
<a name="l00175"></a>00175 <a class="code" href="classLFSCObj.html#aae6e50323f43de730d052249b3540603">d_cnf_add_unit_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"cnf_add_unit"</span>);
<a name="l00176"></a>00176 <a class="code" href="classLFSCObj.html#a06ba8bfd2f179eaec49222d62ff3b914">d_minisat_proof_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"minisat_proof"</span>);
<a name="l00177"></a>00177 <a class="code" href="classLFSCObj.html#aa8367786a66947c4c6e390918e995eb9">d_rewrite_ite_same_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"rewrite_ite_same"</span>);
<a name="l00178"></a>00178 <a class="code" href="classLFSCObj.html#a1c4d27683bd50cfb2a3598aed1eaa52b">d_andE_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"andE"</span>);
<a name="l00179"></a>00179 <a class="code" href="classLFSCObj.html#ad5b7a93ffe8bb6c33527008d0584c5ac">d_implyEqualities_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"implyEqualities"</span>);
<a name="l00180"></a>00180 <a class="code" href="classLFSCObj.html#a5d4ef3ef402573511319acf31a482587">d_addInequalities_str</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a>(<span class="stringliteral">"addInequalities"</span>);
<a name="l00181"></a>00181
<a name="l00182"></a>00182 <span class="comment">//reasons for CNF</span>
<a name="l00183"></a>00183 <a class="code" href="classLFSCObj.html#a3ce45729a0273ed5c43dba4b9d439cc1">d_or_final_s</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga3c1f298d2fdd7aaba48d000ca27df636">newStringExpr</a>(<span class="stringliteral">"or_final"</span>);
<a name="l00184"></a>00184 <a class="code" href="classLFSCObj.html#a8052510576f68336a8a9937f8f8584c1">d_and_final_s</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga3c1f298d2fdd7aaba48d000ca27df636">newStringExpr</a>(<span class="stringliteral">"and_final"</span>);
<a name="l00185"></a>00185 <a class="code" href="classLFSCObj.html#a5b534911a5916e4d03589364030b0881">d_ite_s</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga3c1f298d2fdd7aaba48d000ca27df636">newStringExpr</a>(<span class="stringliteral">"ite"</span>);
<a name="l00186"></a>00186 <a class="code" href="classLFSCObj.html#af19867df31a4aa59d558a1e7bb3cf3d4">d_iff_s</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga3c1f298d2fdd7aaba48d000ca27df636">newStringExpr</a>(<span class="stringliteral">"iff"</span>);
<a name="l00187"></a>00187 <a class="code" href="classLFSCObj.html#ac682735316d59354edaae5db3025ff3e">d_imp_s</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga3c1f298d2fdd7aaba48d000ca27df636">newStringExpr</a>(<span class="stringliteral">"imp"</span>);
<a name="l00188"></a>00188 <a class="code" href="classLFSCObj.html#a2508c14b5f7432f7ee0241603d5deb88">d_or_mid_s</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga3c1f298d2fdd7aaba48d000ca27df636">newStringExpr</a>(<span class="stringliteral">"or_mid"</span>);
<a name="l00189"></a>00189 <a class="code" href="classLFSCObj.html#a155d135b8fbc4eef20388f07ce30453d">d_and_mid_s</a> = pf_expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga3c1f298d2fdd7aaba48d000ca27df636">newStringExpr</a>(<span class="stringliteral">"and_mid"</span>);
<a name="l00190"></a>00190
<a name="l00191"></a>00191 <span class="comment">// add them to d_rules</span>
<a name="l00192"></a>00192 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a482a3a5c4c6ca22f8bc08f7e8942b7be">d_iff_mp_str</a>]=<span class="keyword">true</span>;
<a name="l00193"></a>00193 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a71dc551ca9a26bfa90d971e5627293fb">d_impl_mp_str</a>]=<span class="keyword">true</span>;
<a name="l00194"></a>00194 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#af1c7635ff7d9d7a6d4ca6d5f524e838e">d_iff_trans_str</a>]=<span class="keyword">true</span>;
<a name="l00195"></a>00195 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#ae75e0ca40a864dac2009ac40da5c83d6">d_real_shadow_str</a>]=<span class="keyword">true</span>;
<a name="l00196"></a>00196 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#acebf70a838fce6dbdb1ad46c2ce277b9">d_cycle_conflict_str</a>]=<span class="keyword">true</span>;
<a name="l00197"></a>00197 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a32683494b48bed158c9373f18af0b524">d_real_shadow_eq_str</a>]=<span class="keyword">true</span>;
<a name="l00198"></a>00198 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a3806475a625a97dc4eeaecd3ecc82eee">d_basic_subst_op_str</a>]=<span class="keyword">true</span>;
<a name="l00199"></a>00199 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a40c4f5943b21296bb1ba3b250a39be5b">d_mult_ineqn_str</a>]=<span class="keyword">true</span>;
<a name="l00200"></a>00200 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a11a0ed93bc57d8787486d8c663dd1369">d_flip_inequality_str</a>]=<span class="keyword">true</span>;
<a name="l00201"></a>00201 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#ae68fd62549e5191b31a2a9ff6e919033">d_right_minus_left_str</a>]=<span class="keyword">true</span>;
<a name="l00202"></a>00202 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a988780a33a8cd1c4a79ada79535e3133">d_eq_trans_str</a>]=<span class="keyword">true</span>;
<a name="l00203"></a>00203 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a008e6fb099a79edcff2f47ffd8c1bf84">d_eq_symm_str</a>]=<span class="keyword">true</span>;
<a name="l00204"></a>00204 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a088e49cbb378c0ac9e6c4515cc6b99b8">d_canon_plus_str</a>]=<span class="keyword">true</span>;
<a name="l00205"></a>00205 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a18907b513101487ecbdc956b8d9884ce">d_refl_str</a>]=<span class="keyword">true</span>;
<a name="l00206"></a>00206 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#afe9d28e7d8efbeb59913023779116cdb">d_cnf_convert_str</a>]=<span class="keyword">true</span>;
<a name="l00207"></a>00207 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a4419339e214cefcb4de40cfa1e318c88">d_learned_clause_str</a>]=<span class="keyword">true</span>;
<a name="l00208"></a>00208 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a515cbe72a3391aebb245ca77c70b7f76">d_bool_res_str</a>] = <span class="keyword">true</span>;
<a name="l00209"></a>00209 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a49af9dbc7a770f4372be4642e32f39c8">d_assump_str</a>] = <span class="keyword">true</span>;
<a name="l00210"></a>00210 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#ae1b08b3ef34d91064a5d990c573916e8">d_minus_to_plus_str</a>] = <span class="keyword">true</span>;
<a name="l00211"></a>00211 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#ae1b08b3ef34d91064a5d990c573916e8">d_minus_to_plus_str</a>] = <span class="keyword">true</span>;
<a name="l00212"></a>00212 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a59fc7e6797f9f710385d96dd63fe3c7a">d_plus_predicate_str</a>] = <span class="keyword">true</span>;
<a name="l00213"></a>00213 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a11a0ed93bc57d8787486d8c663dd1369">d_flip_inequality_str</a>] = <span class="keyword">true</span>;
<a name="l00214"></a>00214 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#ad1ebf052401eba516c3328f6a99ab389">d_negated_inequality_str</a>] = <span class="keyword">true</span>;
<a name="l00215"></a>00215 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a9037ec508663dc84ab2d72631171c9e8">d_iff_true_elim_str</a>] = <span class="keyword">true</span>;
<a name="l00216"></a>00216 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a033351a8f7c305990b272c70f210cf6c">d_basic_subst_op1_str</a>] = <span class="keyword">true</span>;
<a name="l00217"></a>00217 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#ac1e17603638979d251aa6bce9fbf6443">d_basic_subst_op0_str</a>] = <span class="keyword">true</span>;
<a name="l00218"></a>00218 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a59423ce52bac130c25372804f1a3b2fa">d_canon_mult_str</a>] = <span class="keyword">true</span>;
<a name="l00219"></a>00219 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a8f8d5a3b46f96de7a286c109ba89002b">d_canon_invert_divide_str</a>] = <span class="keyword">true</span>;
<a name="l00220"></a>00220 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a5e8f7307cd69eaa8381b94a55cb6b5f7">d_iff_true_str</a>] = <span class="keyword">true</span>;
<a name="l00221"></a>00221 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#ab77f0a4102ceaaba81aae959b38fff1b">d_mult_eqn_str</a>] = <span class="keyword">true</span>;
<a name="l00222"></a>00222 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a97b66c2bb2a7cf5475969f4929802cb2">d_rewrite_eq_symm_str</a>] = <span class="keyword">true</span>;
<a name="l00223"></a>00223 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#ab1cfbe69faad1806adce5f1d83b6ad06">d_optimized_subst_op_str</a>] = <span class="keyword">true</span>;
<a name="l00224"></a>00224 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a5eb9b49376b9c44fdd1c879a56cb4927">d_implyWeakerInequality_str</a>] = <span class="keyword">true</span>;
<a name="l00225"></a>00225 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#ab93f73a7292e8f8c93c7579ed4b10258">d_implyWeakerInequalityDiffLogic_str</a>] = <span class="keyword">true</span>;
<a name="l00226"></a>00226 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a6183ebe28c2d6284ad2924348f27c0a0">d_imp_mp_str</a>] = <span class="keyword">true</span>;
<a name="l00227"></a>00227 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a5d4ef3ef402573511319acf31a482587">d_addInequalities_str</a>] = <span class="keyword">true</span>;
<a name="l00228"></a>00228 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a8ee48c649017b77e06deda136fde968d">d_rewrite_implies_str</a>] = <span class="keyword">true</span>;
<a name="l00229"></a>00229 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a2c2af826a423bd5059c20462d664bd9c">d_rewrite_or_str</a>] = <span class="keyword">true</span>;
<a name="l00230"></a>00230 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#ad5e78e0799f54a4aa89dcce1b5ef1591">d_rewrite_and_str</a>] = <span class="keyword">true</span>;
<a name="l00231"></a>00231 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a881021008ed360cbc5e7573e52fc7ec4">d_rewrite_iff_symm_str</a>] = <span class="keyword">true</span>;
<a name="l00232"></a>00232 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a11a736d065275de2558ac8ba4ab624e5">d_iff_not_false_str</a>] = <span class="keyword">true</span>;
<a name="l00233"></a>00233 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#ac6f3e4aff2a0e7cd2890b089ee5520df">d_iff_false_str</a>] = <span class="keyword">true</span>;
<a name="l00234"></a>00234 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#aa69b286d7f0dcc65e178cb7f189ce4e7">d_iff_false_elim_str</a>] = <span class="keyword">true</span>;
<a name="l00235"></a>00235 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#ab7930db598045de2b9b715d810f4821a">d_not_to_iff_str</a>] = <span class="keyword">true</span>;
<a name="l00236"></a>00236 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a58583da73255b5ad31d3415e6eecb200">d_not_not_elim_str</a>] = <span class="keyword">true</span>;
<a name="l00237"></a>00237 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a8a9baf936097ef0146666cf6a0019d86">d_const_predicate_str</a>] = <span class="keyword">true</span>;
<a name="l00238"></a>00238 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#abe33b1cf4b7a701afd26466b8bbb3b3c">d_rewrite_not_not_str</a>] = <span class="keyword">true</span>;
<a name="l00239"></a>00239 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a182c63a54b3d0435c67fd5dd212a43b1">d_rewrite_not_true_str</a>] = <span class="keyword">true</span>;
<a name="l00240"></a>00240 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a07f5cf7de5d7bd2f51a7dab8e8ced3ba">d_rewrite_not_false_str</a>] = <span class="keyword">true</span>;
<a name="l00241"></a>00241
<a name="l00242"></a>00242 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#aa0d31e1ccc537ed4ec541e109b8533ee">d_if_lift_rule_str</a>] = <span class="keyword">true</span>;
<a name="l00243"></a>00243 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#ae62723cd3b241eb95c7d637fbbf25414">d_CNFITE_str</a>] = <span class="keyword">true</span>;
<a name="l00244"></a>00244 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#aa8be0f6329de8878837686420aee5092">d_var_intro_str</a>] = <span class="keyword">true</span>;
<a name="l00245"></a>00245 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#ac62c8dc4c83d5a3e19cfdce0ef60cd0e">d_int_const_eq_str</a>] = <span class="keyword">true</span>;
<a name="l00246"></a>00246 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a1eb48aeb323149091a40c35962d087b0">d_rewrite_eq_refl_str</a>] = <span class="keyword">true</span>;
<a name="l00247"></a>00247 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a06306648e20078ba6436aee671dfdf5e">d_iff_symm_str</a>] = <span class="keyword">true</span>;
<a name="l00248"></a>00248 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#ae22d245587e43b53436e8bdf99914c5c">d_rewrite_iff_str</a>] = <span class="keyword">true</span>;
<a name="l00249"></a>00249 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a4d5aacd643a90b9082037521c561eebc">d_implyNegatedInequality_str</a>] = <span class="keyword">true</span>;
<a name="l00250"></a>00250 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#ad239f7556c548642b93bbad7808e4d08">d_uminus_to_mult_str</a>] = <span class="keyword">true</span>;
<a name="l00251"></a>00251 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#aecc91fcc3b651c68ba124c3d205d6c3d">d_lessThan_To_LE_rhs_rwr_str</a>] = <span class="keyword">true</span>;
<a name="l00252"></a>00252
<a name="l00253"></a>00253 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#ad016421378038e3ceaee715f0ed67cb3">d_CNF_str</a>] = <span class="keyword">true</span>;
<a name="l00254"></a>00254 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#aae6e50323f43de730d052249b3540603">d_cnf_add_unit_str</a>] = <span class="keyword">true</span>;
<a name="l00255"></a>00255 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a06ba8bfd2f179eaec49222d62ff3b914">d_minisat_proof_str</a>] = <span class="keyword">true</span>;
<a name="l00256"></a>00256
<a name="l00257"></a>00257 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#a1c4d27683bd50cfb2a3598aed1eaa52b">d_andE_str</a>] = <span class="keyword">true</span>;
<a name="l00258"></a>00258 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#ad5b7a93ffe8bb6c33527008d0584c5ac">d_implyEqualities_str</a>] = <span class="keyword">true</span>;
<a name="l00259"></a>00259 <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[<a class="code" href="classLFSCObj.html#aa8367786a66947c4c6e390918e995eb9">d_rewrite_ite_same_str</a>] = <span class="keyword">true</span>;
<a name="l00260"></a>00260 }
<a name="l00261"></a>00261
<a name="l00262"></a>00262
<a name="l00263"></a><a class="code" href="classLFSCObj.html#a7cc463260b3fd747b9ab510b5623b401">00263</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCObj.html#a7cc463260b3fd747b9ab510b5623b401">LFSCObj::getNumNodes</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& pf, <span class="keywordtype">bool</span> recount ){
<a name="l00264"></a>00264 <span class="keywordflow">if</span>( pf.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()>0 && <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[pf[0]] ){
<a name="l00265"></a>00265 <span class="keywordflow">if</span>( <a class="code" href="classLFSCObj.html#afe177d3bd72f6abd93377e6661218c1b">nnode_map</a>.<a class="code" href="classCVC3_1_1ExprMap.html#ae50ab1874dd63b575553e7db769abe28">find</a>( pf )==<a class="code" href="classLFSCObj.html#afe177d3bd72f6abd93377e6661218c1b">nnode_map</a>.<a class="code" href="classCVC3_1_1ExprMap.html#a283ae6c44308cbdda0d82da5a16e52c8">end</a>() ){
<a name="l00266"></a>00266 <span class="keywordtype">int</span> sum=0;
<a name="l00267"></a>00267 <span class="keywordflow">for</span>( <span class="keywordtype">int</span> a=1; a<pf.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>(); a++ ){
<a name="l00268"></a>00268 sum += <a class="code" href="classLFSCObj.html#a7cc463260b3fd747b9ab510b5623b401">getNumNodes</a>( pf[a], recount );
<a name="l00269"></a>00269 }
<a name="l00270"></a>00270 <a class="code" href="classLFSCObj.html#afe177d3bd72f6abd93377e6661218c1b">nnode_map</a>[pf] = sum + 1;
<a name="l00271"></a>00271 <span class="keywordflow">return</span> sum + 1;
<a name="l00272"></a>00272 }<span class="keywordflow">else</span> <span class="keywordflow">if</span>( recount ){
<a name="l00273"></a>00273 <span class="keywordflow">return</span> <a class="code" href="classLFSCObj.html#afe177d3bd72f6abd93377e6661218c1b">nnode_map</a>[pf];
<a name="l00274"></a>00274 }<span class="keywordflow">else</span>{
<a name="l00275"></a>00275 <span class="keywordflow">return</span> 1;
<a name="l00276"></a>00276 }
<a name="l00277"></a>00277 }
<a name="l00278"></a>00278 <span class="keywordflow">return</span> 0;
<a name="l00279"></a>00279 }
<a name="l00280"></a>00280
<a name="l00281"></a><a class="code" href="classLFSCObj.html#a9d972614227f1b88721d36b33f04750f">00281</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a9d972614227f1b88721d36b33f04750f">LFSCObj::cascade_expr</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e )
<a name="l00282"></a>00282 {
<a name="l00283"></a>00283 <span class="keywordflow">if</span>( <a class="code" href="classLFSCObj.html#a6a3e7f3fc21a2291ad793eba84f76a4c">cas_map</a>.<a class="code" href="classCVC3_1_1ExprMap.html#ae50ab1874dd63b575553e7db769abe28">find</a>( e ) != <a class="code" href="classLFSCObj.html#a6a3e7f3fc21a2291ad793eba84f76a4c">cas_map</a>.<a class="code" href="classCVC3_1_1ExprMap.html#a283ae6c44308cbdda0d82da5a16e52c8">end</a>() ){
<a name="l00284"></a>00284 <span class="keywordflow">return</span> <a class="code" href="classLFSCObj.html#a6a3e7f3fc21a2291ad793eba84f76a4c">cas_map</a>[e];
<a name="l00285"></a>00285 }<span class="keywordflow">else</span>{
<a name="l00286"></a>00286 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> ce;
<a name="l00287"></a>00287 <span class="keywordflow">if</span>( e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()==<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba73072b2c6fef896d006d6691e932cf37">SKOLEM_VAR</a> ){
<a name="l00288"></a>00288 ce = <a class="code" href="classLFSCObj.html#a43226f1b59b50c73af82f2f1f7a8b2d2">skolem_vars</a>[e];
<a name="l00289"></a>00289 }<span class="keywordflow">else</span> <span class="keywordflow">if</span>( e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()==<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3a4cfaf3eae8eac1dc2fd27d9f0994dc">ITE</a> ){
<a name="l00290"></a>00290 ce = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3a4cfaf3eae8eac1dc2fd27d9f0994dc">ITE</a>, <a class="code" href="classLFSCObj.html#a9d972614227f1b88721d36b33f04750f">cascade_expr</a>( e[0] ),
<a name="l00291"></a>00291 <a class="code" href="classLFSCObj.html#a9d972614227f1b88721d36b33f04750f">cascade_expr</a>( e[1] ),
<a name="l00292"></a>00292 <a class="code" href="classLFSCObj.html#a9d972614227f1b88721d36b33f04750f">cascade_expr</a>( e[2] ) );
<a name="l00293"></a>00293 }<span class="keywordflow">else</span> <span class="keywordflow">if</span>( e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()==1 ){
<a name="l00294"></a>00294 ce = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>(), <a class="code" href="classLFSCObj.html#a9d972614227f1b88721d36b33f04750f">cascade_expr</a>( e[0] ) );
<a name="l00295"></a>00295 }<span class="keywordflow">else</span> <span class="keywordflow">if</span>( e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()>0 ){
<a name="l00296"></a>00296 ce = <a class="code" href="classLFSCObj.html#a9d972614227f1b88721d36b33f04750f">cascade_expr</a>( e[e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()-1] );
<a name="l00297"></a>00297 <span class="keywordflow">for</span>( <span class="keywordtype">int</span> a=e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()-2; a>=0; a-- ){
<a name="l00298"></a>00298 ce = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>(), <a class="code" href="classLFSCObj.html#a9d972614227f1b88721d36b33f04750f">cascade_expr</a>( e[a] ), ce );
<a name="l00299"></a>00299 }
<a name="l00300"></a>00300 }<span class="keywordflow">else</span>{
<a name="l00301"></a>00301 <span class="keywordflow">return</span> e;
<a name="l00302"></a>00302 }
<a name="l00303"></a>00303 <a class="code" href="classLFSCObj.html#a6a3e7f3fc21a2291ad793eba84f76a4c">cas_map</a>[e] = ce;
<a name="l00304"></a>00304 <span class="keywordflow">return</span> ce;
<a name="l00305"></a>00305 }
<a name="l00306"></a>00306 }
<a name="l00307"></a>00307
<a name="l00308"></a><a class="code" href="classLFSCObj.html#a2a8667f109db440dc7d05933fdf2c857">00308</a> <span class="keywordtype">void</span> <a class="code" href="classLFSCObj.html#a2a8667f109db440dc7d05933fdf2c857">LFSCObj::define_skolem_vars</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e )
<a name="l00309"></a>00309 {
<a name="l00310"></a>00310 <span class="keywordflow">if</span>( e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()>0 && <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[ e[0] ] && !<a class="code" href="classLFSCObj.html#a36e0f50de989f0c82ada5d7f968268de">temp_visited</a>[e] )
<a name="l00311"></a>00311 {
<a name="l00312"></a>00312 <a class="code" href="classLFSCObj.html#a36e0f50de989f0c82ada5d7f968268de">temp_visited</a>[e] = <span class="keyword">true</span>;
<a name="l00313"></a>00313 <span class="keywordflow">if</span>( e[0] == <a class="code" href="classLFSCObj.html#a49af9dbc7a770f4372be4642e32f39c8">d_assump_str</a> )
<a name="l00314"></a>00314 {
<a name="l00315"></a>00315 <span class="keywordflow">if</span>( e[1].isIff() && e[1][1].<a class="code" href="group__ExprPkg.html#gac4af2026c180da0f18d66ac616f61f3a">isEq</a>() && e[1][1][1].<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()==<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba73072b2c6fef896d006d6691e932cf37">SKOLEM_VAR</a> ){
<a name="l00316"></a>00316 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> ce = <a class="code" href="classLFSCObj.html#a9d972614227f1b88721d36b33f04750f">cascade_expr</a>( e[1][1][0] );
<a name="l00317"></a>00317 <a class="code" href="classLFSCObj.html#a43226f1b59b50c73af82f2f1f7a8b2d2">skolem_vars</a>[ e[1][1][1] ] = ce;
<a name="l00318"></a>00318 <span class="comment">//store it in the tmap</span>
<a name="l00319"></a>00319 <a class="code" href="classLFSCObj.html#a3dfb8a205672108cc821801faa9f37d3">queryT</a>( ce );
<a name="l00320"></a>00320 }<span class="keywordflow">else</span>{
<a name="l00321"></a>00321 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> ce = <a class="code" href="classLFSCObj.html#a9d972614227f1b88721d36b33f04750f">cascade_expr</a>( e[1] );
<a name="l00322"></a>00322 <span class="keywordflow">if</span>( !<a class="code" href="classLFSCObj.html#ad8e86790f4adb2570714da3d4f7eb8c5">d_assump_map</a>[ ce ] ){
<a name="l00323"></a>00323 ostringstream ose;
<a name="l00324"></a>00324 ose << <span class="stringliteral">"Unexpected non-discharged assumption "</span> << ce;
<a name="l00325"></a>00325 <a class="code" href="classObj.html#a7a13d6281d09d895f9db31157fe62f0d">print_error</a>( ose.str().c_str(), cout );
<a name="l00326"></a>00326 }
<a name="l00327"></a>00327 }
<a name="l00328"></a>00328 }
<a name="l00329"></a>00329 <span class="keywordflow">if</span>( e[0]!=<a class="code" href="classLFSCObj.html#a4419339e214cefcb4de40cfa1e318c88">d_learned_clause_str</a> ){
<a name="l00330"></a>00330 <span class="keywordflow">for</span>( <span class="keywordtype">int</span> a=1; a<e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>(); a++ ){
<a name="l00331"></a>00331 <a class="code" href="classLFSCObj.html#a2a8667f109db440dc7d05933fdf2c857">define_skolem_vars</a>( e[a] );
<a name="l00332"></a>00332 }
<a name="l00333"></a>00333 }
<a name="l00334"></a>00334 }
<a name="l00335"></a>00335 }
<a name="l00336"></a>00336
<a name="l00337"></a><a class="code" href="classLFSCObj.html#a00db5afdd2da1a7bc146e8a609b3445c">00337</a> <span class="keywordtype">bool</span> <a class="code" href="classLFSCObj.html#a00db5afdd2da1a7bc146e8a609b3445c">LFSCObj::isVar</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e )
<a name="l00338"></a>00338 {
<a name="l00339"></a>00339 <span class="keywordflow">return</span> (e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()==<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2efaeb22f8803588598706b73cec8bda">UCONST</a> && <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[e]==<span class="keyword">false</span>);
<a name="l00340"></a>00340 }
<a name="l00341"></a>00341
<a name="l00342"></a><a class="code" href="classLFSCObj.html#af95a913ddd8f4f9282386096e14de00c">00342</a> <span class="keywordtype">void</span> <a class="code" href="classLFSCObj.html#af95a913ddd8f4f9282386096e14de00c">LFSCObj::collect_vars</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e,<span class="keywordtype">bool</span> readPred){
<a name="l00343"></a>00343 <span class="keywordflow">if</span>(<a class="code" href="classLFSCObj.html#a00db5afdd2da1a7bc146e8a609b3445c">isVar</a>(e)){
<a name="l00344"></a>00344 <span class="keywordflow">if</span>( readPred )
<a name="l00345"></a>00345 <a class="code" href="classLFSCObj.html#a0b89bc2bbc7e2bb9474026ff4b111302">input_preds</a>[e] = <span class="keyword">true</span>;
<a name="l00346"></a>00346 <span class="keywordflow">else</span>
<a name="l00347"></a>00347 <a class="code" href="classLFSCObj.html#ae7a9bf905373af442a0ef70db558440c">input_vars</a>[e]=<span class="keyword">true</span>;
<a name="l00348"></a>00348 }<span class="keywordflow">else</span>{
<a name="l00349"></a>00349 readPred = !<a class="code" href="Util_8cpp.html#a5462f02c7d83367f4d9e1b99f1975cb7">is_eq_kind</a>( e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() ) && readPred;
<a name="l00350"></a>00350 <span class="keywordflow">for</span>(<span class="keywordtype">int</span> a=0; a<e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>(); a++ ){
<a name="l00351"></a>00351 <a class="code" href="classLFSCObj.html#af95a913ddd8f4f9282386096e14de00c">collect_vars</a>( e[a], ( readPred || (e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()==<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3a4cfaf3eae8eac1dc2fd27d9f0994dc">ITE</a> && a==0 ) ) );
<a name="l00352"></a>00352 }
<a name="l00353"></a>00353 }
<a name="l00354"></a>00354 }
<a name="l00355"></a>00355
<a name="l00356"></a><a class="code" href="classLFSCObj.html#af30e3e73af0d18b0775f0ccc6ddb9441">00356</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#af30e3e73af0d18b0775f0ccc6ddb9441">LFSCObj::queryElimNotNot</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& expr)
<a name="l00357"></a>00357 {
<a name="l00358"></a>00358 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e = expr;
<a name="l00359"></a>00359 <span class="keywordflow">while</span>( e.<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>() && e[0].<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>() )
<a name="l00360"></a>00360 e = e[0][0];
<a name="l00361"></a>00361 <span class="keywordflow">return</span> e;
<a name="l00362"></a>00362 }
<a name="l00363"></a>00363
<a name="l00364"></a>00364
<a name="l00365"></a><a class="code" href="classLFSCObj.html#a024a42781132867e23a7f6e65e6d0f98">00365</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classLFSCObj.html#a024a42781132867e23a7f6e65e6d0f98">LFSCObj::queryAtomic</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& expr, <span class="keywordtype">bool</span> getBase)
<a name="l00366"></a>00366 {
<a name="l00367"></a>00367 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e = <a class="code" href="classLFSCObj.html#a9d972614227f1b88721d36b33f04750f">cascade_expr</a>( <a class="code" href="classLFSCObj.html#af30e3e73af0d18b0775f0ccc6ddb9441">queryElimNotNot</a>( expr ) );
<a name="l00368"></a>00368 <span class="keywordflow">if</span>( e.<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>() ){
<a name="l00369"></a>00369 <span class="keywordflow">if</span>( getBase ){
<a name="l00370"></a>00370 <span class="keywordflow">return</span> e[0];
<a name="l00371"></a>00371 }<span class="keywordflow">else</span>{
<a name="l00372"></a>00372 <span class="keywordflow">if</span>( e[0].isTrue() ){
<a name="l00373"></a>00373 e = <a class="code" href="classLFSCObj.html#ad4d5ea192b766a7020fdfc7a462e99fe">d_pf_expr</a>.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#gaae9db4c93c67cbf8bbf5d1e60e94f1ae" title="FALSE Expr.">falseExpr</a>();
<a name="l00374"></a>00374 <span class="keywordflow">return</span> e;
<a name="l00375"></a>00375 }<span class="keywordflow">else</span> <span class="keywordflow">if</span>( e[0].isFalse() ){
<a name="l00376"></a>00376 e = <a class="code" href="classLFSCObj.html#ad4d5ea192b766a7020fdfc7a462e99fe">d_pf_expr</a>.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4471fca49c2acbb7b4cf71e72bc55d6a" title="TRUE Expr.">trueExpr</a>();
<a name="l00377"></a>00377 <span class="keywordflow">return</span> e;
<a name="l00378"></a>00378 }<span class="keywordflow">else</span> <span class="keywordflow">if</span>( <a class="code" href="Util_8cpp.html#a5462f02c7d83367f4d9e1b99f1975cb7">is_eq_kind</a>( e[0].getKind() ) ){
<a name="l00379"></a>00379 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="Util_8cpp.html#a796942d5524726336add29080f902785">get_not</a>( e[0].getKind() ), e[0][1], e[0][0] );
<a name="l00380"></a>00380 }
<a name="l00381"></a>00381 }
<a name="l00382"></a>00382 }
<a name="l00383"></a>00383 <span class="keywordflow">return</span> e;
<a name="l00384"></a>00384 }
<a name="l00385"></a>00385
<a name="l00386"></a><a class="code" href="classLFSCObj.html#ab0f17f592443a6a15fe2cb7446308e65">00386</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCObj.html#ab0f17f592443a6a15fe2cb7446308e65">LFSCObj::queryM</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& expr, <span class="keywordtype">bool</span> add, <span class="keywordtype">bool</span> trusted)
<a name="l00387"></a>00387 {
<a name="l00388"></a>00388 <span class="comment">//cout << "query : " << expr << endl;</span>
<a name="l00389"></a>00389 <span class="keywordtype">bool</span> neg = <span class="keyword">false</span>;
<a name="l00390"></a>00390 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e = <a class="code" href="classLFSCObj.html#a9d972614227f1b88721d36b33f04750f">cascade_expr</a>( <a class="code" href="classLFSCObj.html#af30e3e73af0d18b0775f0ccc6ddb9441">queryElimNotNot</a>( expr ) );
<a name="l00391"></a>00391 <span class="keywordflow">if</span>( !trusted ){
<a name="l00392"></a>00392 <span class="keywordflow">if</span>( e.<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>() ){
<a name="l00393"></a>00393 neg = <span class="keyword">true</span>;
<a name="l00394"></a>00394 e = e[0];
<a name="l00395"></a>00395 }
<a name="l00396"></a>00396 <span class="keywordtype">int</span> val = <a class="code" href="classLFSCObj.html#a9741b35e18a1dc2dd135fb85face8288">d_formulas</a>[e];
<a name="l00397"></a>00397 <span class="keywordflow">if</span>( val==0 && add )
<a name="l00398"></a>00398 {
<a name="l00399"></a>00399 <span class="keywordflow">if</span>( !e.<a class="code" href="group__ExprPkg.html#gaa3359d5f6638eba5479c4c4036a551a8">isInitialized</a>() ){
<a name="l00400"></a>00400 <a class="code" href="classObj.html#a7a13d6281d09d895f9db31157fe62f0d">print_error</a>( <span class="stringliteral">"WARNING: uninitialized e in query"</span>, cout );
<a name="l00401"></a>00401 }
<a name="l00402"></a>00402 <a class="code" href="classLFSCObj.html#a9741b35e18a1dc2dd135fb85face8288">d_formulas</a>[e] = <a class="code" href="classLFSCObj.html#a66bb07d4b7e20596d9f324c5f3ce689a">formula_i</a>;
<a name="l00403"></a>00403 val = <a class="code" href="classLFSCObj.html#a66bb07d4b7e20596d9f324c5f3ce689a">formula_i</a>;
<a name="l00404"></a>00404 <a class="code" href="classLFSCObj.html#a66bb07d4b7e20596d9f324c5f3ce689a">formula_i</a>++;
<a name="l00405"></a>00405 }
<a name="l00406"></a>00406 <span class="keywordflow">return</span> val*(neg ? -1 : 1 );
<a name="l00407"></a>00407 }<span class="keywordflow">else</span>{
<a name="l00408"></a>00408 <span class="keywordtype">int</span> val = <a class="code" href="classLFSCObj.html#aa62d284471e6be2f733711bc01037ded">d_trusted</a>[e];
<a name="l00409"></a>00409 <span class="keywordflow">if</span>( val==0 && add ){
<a name="l00410"></a>00410 <a class="code" href="classLFSCObj.html#aa62d284471e6be2f733711bc01037ded">d_trusted</a>[e] = <a class="code" href="classLFSCObj.html#acd1b788ca21cbc01682501f940f1a4f5">trusted_i</a>;
<a name="l00411"></a>00411 val = <a class="code" href="classLFSCObj.html#acd1b788ca21cbc01682501f940f1a4f5">trusted_i</a>;
<a name="l00412"></a>00412 <a class="code" href="classLFSCObj.html#acd1b788ca21cbc01682501f940f1a4f5">trusted_i</a>++;
<a name="l00413"></a>00413 }
<a name="l00414"></a>00414 <span class="keywordflow">return</span> val;
<a name="l00415"></a>00415 }
<a name="l00416"></a>00416 }
<a name="l00417"></a>00417
<a name="l00418"></a><a class="code" href="classLFSCObj.html#a4ce15858a0bfeca1b9fdd86b0315005d">00418</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCObj.html#a4ce15858a0bfeca1b9fdd86b0315005d">LFSCObj::queryMt</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& expr)
<a name="l00419"></a>00419 {
<a name="l00420"></a>00420 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> ce = <a class="code" href="classLFSCObj.html#a9d972614227f1b88721d36b33f04750f">cascade_expr</a>( expr );
<a name="l00421"></a>00421 <span class="keywordflow">if</span>( !<a class="code" href="classLFSCObj.html#a38fba3c1b92848531100ff1a0f2c0e6a">can_pnorm</a>( ce ) ){
<a name="l00422"></a>00422 ostringstream os;
<a name="l00423"></a>00423 os << <span class="stringliteral">"ERROR: cannot make polynomial normalization for "</span> << ce << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">std::endl</a>;
<a name="l00424"></a>00424 <a class="code" href="classObj.html#a7a13d6281d09d895f9db31157fe62f0d">print_error</a>( os.str().c_str(), cout );
<a name="l00425"></a>00425 }
<a name="l00426"></a>00426 <span class="keywordtype">int</span> val = <a class="code" href="classLFSCObj.html#a53e3990d17d606c9dd5b28b7950d5cd5">d_pn</a>[ce];
<a name="l00427"></a>00427 <span class="keywordflow">if</span>( val==0 )
<a name="l00428"></a>00428 {
<a name="l00429"></a>00429 <a class="code" href="classLFSCObj.html#a53e3990d17d606c9dd5b28b7950d5cd5">d_pn</a>[ce] = <a class="code" href="classLFSCObj.html#a1c1342a9b79a1a2406a9a2c3c958addb">tnorm_i</a>;
<a name="l00430"></a>00430 val = <a class="code" href="classLFSCObj.html#a1c1342a9b79a1a2406a9a2c3c958addb">tnorm_i</a>;
<a name="l00431"></a>00431 <a class="code" href="classLFSCObj.html#a1c1342a9b79a1a2406a9a2c3c958addb">tnorm_i</a>++;
<a name="l00432"></a>00432 }
<a name="l00433"></a>00433 <span class="keywordflow">return</span> val;
<a name="l00434"></a>00434 }
<a name="l00435"></a>00435
<a name="l00436"></a><a class="code" href="classLFSCObj.html#a3dfb8a205672108cc821801faa9f37d3">00436</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCObj.html#a3dfb8a205672108cc821801faa9f37d3">LFSCObj::queryT</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e )
<a name="l00437"></a>00437 {
<a name="l00438"></a>00438 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> ce = <a class="code" href="classLFSCObj.html#a9d972614227f1b88721d36b33f04750f">cascade_expr</a>( e );
<a name="l00439"></a>00439 <span class="keywordtype">int</span> val = <a class="code" href="classLFSCObj.html#aa8ad0677d224a27c6b7376619a9a037d">d_terms</a>[ce];
<a name="l00440"></a>00440 <span class="keywordflow">if</span>( val==0 ){
<a name="l00441"></a>00441 <a class="code" href="classLFSCObj.html#aa8ad0677d224a27c6b7376619a9a037d">d_terms</a>[ce] = <a class="code" href="classLFSCObj.html#aa53d3da9dab58f7e4670db1619d8947e">term_i</a>;
<a name="l00442"></a>00442 val = <a class="code" href="classLFSCObj.html#aa53d3da9dab58f7e4670db1619d8947e">term_i</a>;
<a name="l00443"></a>00443 <a class="code" href="classLFSCObj.html#aa53d3da9dab58f7e4670db1619d8947e">term_i</a>++;
<a name="l00444"></a>00444 }
<a name="l00445"></a>00445 <span class="keywordflow">return</span> val;
<a name="l00446"></a>00446 }
<a name="l00447"></a>00447
<a name="l00448"></a><a class="code" href="classLFSCObj.html#a47da52a2dbb7eb81f830586692e9f9a1">00448</a> <span class="keywordtype">bool</span> <a class="code" href="classLFSCObj.html#a47da52a2dbb7eb81f830586692e9f9a1">LFSCObj::getY</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& pe, <span class="keywordtype">bool</span> doIff, <span class="keywordtype">bool</span> doLogic )
<a name="l00449"></a>00449 {
<a name="l00450"></a>00450 <span class="comment">//cout << "getY = " << e << std::endl;</span>
<a name="l00451"></a>00451 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> ea = <a class="code" href="classLFSCObj.html#a024a42781132867e23a7f6e65e6d0f98">queryAtomic</a>( e );
<a name="l00452"></a>00452 <span class="keywordflow">if</span>( <a class="code" href="Util_8cpp.html#a5462f02c7d83367f4d9e1b99f1975cb7">is_eq_kind</a>( ea.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() ) ){
<a name="l00453"></a>00453 <span class="comment">//must be able to pnorm it</span>
<a name="l00454"></a>00454 <span class="keywordflow">if</span>( <a class="code" href="classLFSCObj.html#a38fba3c1b92848531100ff1a0f2c0e6a">can_pnorm</a>( ea[0] ) && <a class="code" href="classLFSCObj.html#a38fba3c1b92848531100ff1a0f2c0e6a">can_pnorm</a>( ea[1] ) ){
<a name="l00455"></a>00455 <span class="keywordflow">if</span>( <a class="code" href="Util_8cpp.html#a1b08319c48e19ef89eb32d27801c9bfb">is_opposite</a>( ea.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() ) ){
<a name="l00456"></a>00456 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="Util_8cpp.html#a667a5939ed7f0fba1d9a06f52a674832">get_normalized</a>( ea.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() ), ea[1], ea[0] );
<a name="l00457"></a>00457 }<span class="keywordflow">else</span>{
<a name="l00458"></a>00458 pe = ea;
<a name="l00459"></a>00459 }
<a name="l00460"></a>00460 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00461"></a>00461 }<span class="keywordflow">else</span>{
<a name="l00462"></a>00462 ostringstream ose;
<a name="l00463"></a>00463 ose << <span class="stringliteral">"Can't pnorm "</span> << ea[0] << <span class="stringliteral">" "</span> << ea[1] << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">std::endl</a>;
<a name="l00464"></a>00464 <a class="code" href="classObj.html#a7a13d6281d09d895f9db31157fe62f0d">print_error</a>( ose.str().c_str(), cout );
<a name="l00465"></a>00465 }
<a name="l00466"></a>00466 }
<a name="l00467"></a>00467 <span class="keywordflow">if</span>( doIff ){
<a name="l00468"></a>00468 <span class="keywordflow">if</span>( e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()==2 )
<a name="l00469"></a>00469 {
<a name="l00470"></a>00470 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> pe1;
<a name="l00471"></a>00471 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> pe2;
<a name="l00472"></a>00472 <span class="keywordflow">if</span> ( e.<a class="code" href="group__ExprPkg.html#gabe385fb97505cccb75702378511c5375">isIff</a>() ){
<a name="l00473"></a>00473 <span class="keywordflow">if</span>( <a class="code" href="classLFSCObj.html#a47da52a2dbb7eb81f830586692e9f9a1">getY</a>( e[1], pe2, <span class="keyword">false</span> ) ){
<a name="l00474"></a>00474 <span class="keywordflow">if</span>( <a class="code" href="classLFSCObj.html#a47da52a2dbb7eb81f830586692e9f9a1">getY</a>( e[0], pe1, <span class="keyword">false</span>, pe2.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()==<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba1fad76919fba496de21807e2beec533d">TRUE_EXPR</a> || pe2.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()==<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5f71bd33a6528411ae681f5291de1d82">FALSE_EXPR</a> ) ){
<a name="l00475"></a>00475 <span class="keywordflow">if</span>( pe2.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()==<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba1fad76919fba496de21807e2beec533d">TRUE_EXPR</a> ){
<a name="l00476"></a>00476 pe = pe1;
<a name="l00477"></a>00477 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00478"></a>00478 }<span class="keywordflow">else</span> <span class="keywordflow">if</span>( pe1.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()==<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5f71bd33a6528411ae681f5291de1d82">FALSE_EXPR</a> ){
<a name="l00479"></a>00479 pe = <a class="code" href="classLFSCObj.html#ad4d5ea192b766a7020fdfc7a462e99fe">d_pf_expr</a>.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4471fca49c2acbb7b4cf71e72bc55d6a" title="TRUE Expr.">trueExpr</a>();
<a name="l00480"></a>00480 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00481"></a>00481 }
<a name="l00482"></a>00482 <span class="keywordflow">if</span>( pe1.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()==pe2.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() ){
<a name="l00483"></a>00483 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9efdc855f3c1477957fb50affec07f8f">EQ</a>, <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024aba18e0accfb91ddb34f4dcc79c626ec5">MINUS</a>, pe1[0], pe2[0] ), <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024aba18e0accfb91ddb34f4dcc79c626ec5">MINUS</a>, pe1[1], pe2[1] ) );
<a name="l00484"></a>00484 }
<a name="l00485"></a>00485 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00486"></a>00486 }
<a name="l00487"></a>00487 }
<a name="l00488"></a>00488 }
<a name="l00489"></a>00489 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( e.<a class="code" href="group__ExprPkg.html#ga9067c706c6454ea1761ace7d7837af46">isImpl</a>() ){
<a name="l00490"></a>00490 <span class="keywordflow">if</span>( <a class="code" href="classLFSCObj.html#a47da52a2dbb7eb81f830586692e9f9a1">getY</a>( e[1], pe2, <span class="keyword">false</span>, <span class="keyword">false</span> ) ){
<a name="l00491"></a>00491 <span class="keywordflow">if</span>( <a class="code" href="classLFSCObj.html#a47da52a2dbb7eb81f830586692e9f9a1">getY</a>( e[0], pe1, <span class="keyword">false</span>, <span class="keyword">false</span> ) ){
<a name="l00492"></a>00492 <span class="keywordflow">if</span>( <a class="code" href="Util_8cpp.html#a30860522c71b3bd189f3c5789c42a9d7">is_comparison</a>( pe1.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() ) && <a class="code" href="Util_8cpp.html#a30860522c71b3bd189f3c5789c42a9d7">is_comparison</a>( pe2.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() ) ){
<a name="l00493"></a>00493 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( pe1.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()==<a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024a589b68b2d271254aa9fd3d89b4bf33b9">GT</a> && pe2.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()==<a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024a589b68b2d271254aa9fd3d89b4bf33b9">GT</a> ? <a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024a589b68b2d271254aa9fd3d89b4bf33b9">GT</a> : <a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024aad2afa561f31a801e12ab3fdd50a6229">GE</a>,
<a name="l00494"></a>00494 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024aba18e0accfb91ddb34f4dcc79c626ec5">MINUS</a>, pe1[0], pe2[0] ), <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024aba18e0accfb91ddb34f4dcc79c626ec5">MINUS</a>, pe1[1], pe2[1] ) );
<a name="l00495"></a>00495 }
<a name="l00496"></a>00496 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00497"></a>00497 }
<a name="l00498"></a>00498 }
<a name="l00499"></a>00499 }
<a name="l00500"></a>00500 }
<a name="l00501"></a>00501 }
<a name="l00502"></a>00502 <span class="keywordflow">if</span>( doLogic ){
<a name="l00503"></a>00503 <span class="keywordflow">if</span>( ea.<a class="code" href="group__ExprPkg.html#ga6173f64b22cba76472cd0c814bbf6dae">isFalse</a>() ){
<a name="l00504"></a>00504 pe = <a class="code" href="classLFSCObj.html#ad4d5ea192b766a7020fdfc7a462e99fe">d_pf_expr</a>.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4471fca49c2acbb7b4cf71e72bc55d6a" title="TRUE Expr.">trueExpr</a>();
<a name="l00505"></a>00505 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00506"></a>00506 }<span class="keywordflow">else</span> <span class="keywordflow">if</span>( ea.<a class="code" href="group__ExprPkg.html#gadf8596df73fa69ff8e6a22b9321f5c34">isTrue</a>() ){
<a name="l00507"></a>00507 pe = ea;
<a name="l00508"></a>00508 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00509"></a>00509 }
<a name="l00510"></a>00510 }
<a name="l00511"></a>00511 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00512"></a>00512 }
<a name="l00513"></a>00513
<a name="l00514"></a><a class="code" href="classLFSCObj.html#ace5ae3c05a540f101645ecfbacdd2928">00514</a> <span class="keywordtype">bool</span> <a class="code" href="classLFSCObj.html#ace5ae3c05a540f101645ecfbacdd2928">LFSCObj::isFormula</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e )
<a name="l00515"></a>00515 {
<a name="l00516"></a>00516 <span class="keywordflow">return</span> ( <a class="code" href="Util_8cpp.html#a5462f02c7d83367f4d9e1b99f1975cb7">is_eq_kind</a>( e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() ) || e.<a class="code" href="group__ExprPkg.html#ga383260cf4f8919728e2712e6e11f21fa">isAnd</a>() || e.<a class="code" href="group__ExprPkg.html#ga36f1eff876808586db368dc1b6da5f56">isOr</a>() || e.<a class="code" href="group__ExprPkg.html#ga9067c706c6454ea1761ace7d7837af46">isImpl</a>() || e.<a class="code" href="group__ExprPkg.html#gabe385fb97505cccb75702378511c5375">isIff</a>() || e.<a class="code" href="group__ExprPkg.html#ga6173f64b22cba76472cd0c814bbf6dae">isFalse</a>() || e.<a class="code" href="group__ExprPkg.html#gadf8596df73fa69ff8e6a22b9321f5c34">isTrue</a>() || e.<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>() ||
<a name="l00517"></a>00517 ( e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()==<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3a4cfaf3eae8eac1dc2fd27d9f0994dc">ITE</a> && <a class="code" href="classLFSCObj.html#ace5ae3c05a540f101645ecfbacdd2928">isFormula</a>( e[1] ) ) || ( <a class="code" href="classLFSCObj.html#a0b89bc2bbc7e2bb9474026ff4b111302">input_preds</a>.<a class="code" href="classCVC3_1_1ExprMap.html#ae50ab1874dd63b575553e7db769abe28">find</a>( e )!=<a class="code" href="classLFSCObj.html#a0b89bc2bbc7e2bb9474026ff4b111302">input_preds</a>.<a class="code" href="classCVC3_1_1ExprMap.html#a283ae6c44308cbdda0d82da5a16e52c8">end</a>() ) );
<a name="l00518"></a>00518 }
<a name="l00519"></a>00519
<a name="l00520"></a><a class="code" href="classLFSCObj.html#a38fba3c1b92848531100ff1a0f2c0e6a">00520</a> <span class="keywordtype">bool</span> <a class="code" href="classLFSCObj.html#a38fba3c1b92848531100ff1a0f2c0e6a">LFSCObj::can_pnorm</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e )
<a name="l00521"></a>00521 {
<a name="l00522"></a>00522 <span class="keywordflow">if</span>( <a class="code" href="Util_8cpp.html#a5462f02c7d83367f4d9e1b99f1975cb7">is_eq_kind</a>( e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() ) ){
<a name="l00523"></a>00523 <span class="keywordflow">return</span> <a class="code" href="classLFSCObj.html#a38fba3c1b92848531100ff1a0f2c0e6a">can_pnorm</a>( e[0] ) && <a class="code" href="classLFSCObj.html#a38fba3c1b92848531100ff1a0f2c0e6a">can_pnorm</a>( e[1] );
<a name="l00524"></a>00524 }<span class="keywordflow">else</span> <span class="keywordflow">if</span>( e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()==<a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024a9a12fbdcaa45ef17eaa1802161f9ca98">PLUS</a> || e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()==<a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024aba18e0accfb91ddb34f4dcc79c626ec5">MINUS</a> || e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()==<a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024ad77e825b0133e40de2760344377ee1fa">MULT</a> || e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()==<a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024ac3c38ad296d5671b7fde3373fdd87ea1">DIVIDE</a> ){
<a name="l00525"></a>00525 <span class="keywordflow">return</span> <a class="code" href="classLFSCObj.html#a38fba3c1b92848531100ff1a0f2c0e6a">can_pnorm</a>( e[0] ) && <a class="code" href="classLFSCObj.html#a38fba3c1b92848531100ff1a0f2c0e6a">can_pnorm</a>( e[1] );
<a name="l00526"></a>00526 }<span class="keywordflow">else</span> <span class="keywordflow">if</span>( e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()==<a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024a0b79738a0067780987896f3b91e8b0f1">UMINUS</a> ){
<a name="l00527"></a>00527 <span class="keywordflow">return</span> <a class="code" href="classLFSCObj.html#a38fba3c1b92848531100ff1a0f2c0e6a">can_pnorm</a>( e[0] );
<a name="l00528"></a>00528 }<span class="keywordflow">else</span> <span class="keywordflow">if</span>( e.<a class="code" href="group__ExprPkg.html#gac5ced6adc7a60945ea6707ef494aa28f">isRational</a>() ){
<a name="l00529"></a>00529 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00530"></a>00530 }<span class="keywordflow">else</span> <span class="keywordflow">if</span>( e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()==<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3a4cfaf3eae8eac1dc2fd27d9f0994dc">ITE</a> ){
<a name="l00531"></a>00531 <a class="code" href="classLFSCObj.html#a3dfb8a205672108cc821801faa9f37d3">queryT</a>( e );
<a name="l00532"></a>00532 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00533"></a>00533 }<span class="keywordflow">else</span> <span class="keywordflow">if</span>( e.<a class="code" href="group__ExprPkg.html#ga55b6a203b4375e64598306596851d9ae">isVar</a>() && <a class="code" href="classLFSCObj.html#a0b89bc2bbc7e2bb9474026ff4b111302">input_preds</a>.<a class="code" href="classCVC3_1_1ExprMap.html#ae50ab1874dd63b575553e7db769abe28">find</a>( e )==<a class="code" href="classLFSCObj.html#a0b89bc2bbc7e2bb9474026ff4b111302">input_preds</a>.<a class="code" href="classCVC3_1_1ExprMap.html#a283ae6c44308cbdda0d82da5a16e52c8">end</a>() ){
<a name="l00534"></a>00534 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00535"></a>00535 }
<a name="l00536"></a>00536 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00537"></a>00537 }
<a name="l00538"></a>00538
<a name="l00539"></a><a class="code" href="classLFSCObj.html#a99916378da692faa903591fd5e460c69">00539</a> <span class="keywordtype">bool</span> <a class="code" href="classLFSCObj.html#a99916378da692faa903591fd5e460c69">LFSCObj::what_is_proven</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& pf, <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& pe )
<a name="l00540"></a>00540 {
<a name="l00541"></a>00541 <span class="keywordflow">if</span>(pf.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()>0 ){
<a name="l00542"></a>00542 <span class="keywordflow">if</span>(<a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[pf[0]]&&pf[0].getKind()==<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2efaeb22f8803588598706b73cec8bda">UCONST</a>){
<a name="l00543"></a>00543 <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#a49af9dbc7a770f4372be4642e32f39c8">d_assump_str</a> || pf[0] == <a class="code" href="classLFSCObj.html#aae6e50323f43de730d052249b3540603">d_cnf_add_unit_str</a> ||
<a name="l00544"></a>00544 pf[0]== <a class="code" href="classLFSCObj.html#afe9d28e7d8efbeb59913023779116cdb">d_cnf_convert_str</a> || pf[0] == <a class="code" href="classLFSCObj.html#a9037ec508663dc84ab2d72631171c9e8">d_iff_true_elim_str</a> ){
<a name="l00545"></a>00545 pe = pf[1];
<a name="l00546"></a>00546 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00547"></a>00547 }
<a name="l00548"></a>00548 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#a088e49cbb378c0ac9e6c4515cc6b99b8">d_canon_plus_str</a> || pf[0]==<a class="code" href="classLFSCObj.html#a59423ce52bac130c25372804f1a3b2fa">d_canon_mult_str</a> ){
<a name="l00549"></a>00549 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9efdc855f3c1477957fb50affec07f8f">EQ</a>, pf[1], pf[2] );
<a name="l00550"></a>00550 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00551"></a>00551 }
<a name="l00552"></a>00552 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#a8f8d5a3b46f96de7a286c109ba89002b">d_canon_invert_divide_str</a> )
<a name="l00553"></a>00553 {
<a name="l00554"></a>00554 <a class="code" href="classCVC3_1_1Rational.html">Rational</a> r1 = <a class="code" href="classCVC3_1_1Rational.html">Rational</a>( 1 );
<a name="l00555"></a>00555 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> er1 = <a class="code" href="classLFSCObj.html#ad4d5ea192b766a7020fdfc7a462e99fe">d_pf_expr</a>.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga18423a42ce6557dc33287d3979ccc3c6">newRatExpr</a>( pf[1][0].getRational() );
<a name="l00556"></a>00556 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> er2 = <a class="code" href="classLFSCObj.html#ad4d5ea192b766a7020fdfc7a462e99fe">d_pf_expr</a>.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga18423a42ce6557dc33287d3979ccc3c6">newRatExpr</a>( r1/pf[1][1].getRational() );
<a name="l00557"></a>00557 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9efdc855f3c1477957fb50affec07f8f">EQ</a>, pf[1], <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024ad77e825b0133e40de2760344377ee1fa">MULT</a>, er1, er2 ) );
<a name="l00558"></a>00558 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00559"></a>00559 }
<a name="l00560"></a>00560 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#af1c7635ff7d9d7a6d4ca6d5f524e838e">d_iff_trans_str</a> )
<a name="l00561"></a>00561 {
<a name="l00562"></a>00562 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>, pf[1], pf[3] );
<a name="l00563"></a>00563 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00564"></a>00564 }
<a name="l00565"></a>00565 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#a482a3a5c4c6ca22f8bc08f7e8942b7be">d_iff_mp_str</a> || pf[0] == <a class="code" href="classLFSCObj.html#a71dc551ca9a26bfa90d971e5627293fb">d_impl_mp_str</a>)
<a name="l00566"></a>00566 {
<a name="l00567"></a>00567 pe = pf[2];
<a name="l00568"></a>00568 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00569"></a>00569 }
<a name="l00570"></a>00570 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#a988780a33a8cd1c4a79ada79535e3133">d_eq_trans_str</a> )
<a name="l00571"></a>00571 {
<a name="l00572"></a>00572 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9efdc855f3c1477957fb50affec07f8f">EQ</a>, pf[2], pf[4] );
<a name="l00573"></a>00573 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00574"></a>00574 }
<a name="l00575"></a>00575 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#a008e6fb099a79edcff2f47ffd8c1bf84">d_eq_symm_str</a> )
<a name="l00576"></a>00576 {
<a name="l00577"></a>00577 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9efdc855f3c1477957fb50affec07f8f">EQ</a>, pf[3], pf[2] );
<a name="l00578"></a>00578 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00579"></a>00579 }
<a name="l00580"></a>00580 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#a3806475a625a97dc4eeaecd3ecc82eee">d_basic_subst_op_str</a> || pf[0] == <a class="code" href="classLFSCObj.html#ad5e78e0799f54a4aa89dcce1b5ef1591">d_rewrite_and_str</a> ||
<a name="l00581"></a>00581 pf[0] == <a class="code" href="classLFSCObj.html#a2c2af826a423bd5059c20462d664bd9c">d_rewrite_or_str</a> || pf[0] == <a class="code" href="classLFSCObj.html#aecc91fcc3b651c68ba124c3d205d6c3d">d_lessThan_To_LE_rhs_rwr_str</a> ||
<a name="l00582"></a>00582 pf[0] == <a class="code" href="classLFSCObj.html#a40c4f5943b21296bb1ba3b250a39be5b">d_mult_ineqn_str</a> || pf[0] == <a class="code" href="classLFSCObj.html#a59fc7e6797f9f710385d96dd63fe3c7a">d_plus_predicate_str</a> ||
<a name="l00583"></a>00583 pf[0] == <a class="code" href="classLFSCObj.html#a11a0ed93bc57d8787486d8c663dd1369">d_flip_inequality_str</a> || pf[0] == <a class="code" href="classLFSCObj.html#ac62c8dc4c83d5a3e19cfdce0ef60cd0e">d_int_const_eq_str</a> ||
<a name="l00584"></a>00584 pf[0] == <a class="code" href="classLFSCObj.html#a8a9baf936097ef0146666cf6a0019d86">d_const_predicate_str</a> )
<a name="l00585"></a>00585 {
<a name="l00586"></a>00586 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>, pf[1], pf[2] );
<a name="l00587"></a>00587 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00588"></a>00588 }
<a name="l00589"></a>00589 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (pf[0] == <a class="code" href="classLFSCObj.html#a06306648e20078ba6436aee671dfdf5e">d_iff_symm_str</a>){
<a name="l00590"></a>00590 pe = pf[2].<a class="code" href="group__ExprPkg.html#gaae017ca8e68af655ba285c985dd9fba5">iffExpr</a>(pf[1]);
<a name="l00591"></a>00591 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00592"></a>00592 }
<a name="l00593"></a>00593 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#ac1e17603638979d251aa6bce9fbf6443">d_basic_subst_op0_str</a> )
<a name="l00594"></a>00594 {
<a name="l00595"></a>00595 <span class="keywordflow">if</span>( pf[1].getKind()==<a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024a0b79738a0067780987896f3b91e8b0f1">UMINUS</a> ){
<a name="l00596"></a>00596 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9efdc855f3c1477957fb50affec07f8f">EQ</a>, pf[1], pf[2] );
<a name="l00597"></a>00597 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00598"></a>00598 }<span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[1].getKind()==<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0378ebc895849163b249d0b330257dd6">NOT</a> ){
<a name="l00599"></a>00599 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>, pf[1], pf[2] );
<a name="l00600"></a>00600 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00601"></a>00601 }
<a name="l00602"></a>00602 }
<a name="l00603"></a>00603 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#ab77f0a4102ceaaba81aae959b38fff1b">d_mult_eqn_str</a> )
<a name="l00604"></a>00604 {
<a name="l00605"></a>00605 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>, <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9efdc855f3c1477957fb50affec07f8f">EQ</a>, pf[1], pf[2] ),
<a name="l00606"></a>00606 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9efdc855f3c1477957fb50affec07f8f">EQ</a>, <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024ad77e825b0133e40de2760344377ee1fa">MULT</a>, pf[1], pf[3] ), <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024ad77e825b0133e40de2760344377ee1fa">MULT</a>, pf[2], pf[3] ) ) );
<a name="l00607"></a>00607 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00608"></a>00608 }
<a name="l00609"></a>00609 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#ae75e0ca40a864dac2009ac40da5c83d6">d_real_shadow_str</a> )
<a name="l00610"></a>00610 {
<a name="l00611"></a>00611 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( ( pf[1].getKind()==<a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024a1b768cf71a18713c90cd71f82488ffb1">LE</a> && pf[2].getKind()==<a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024a1b768cf71a18713c90cd71f82488ffb1">LE</a> ) ? <a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024a1b768cf71a18713c90cd71f82488ffb1">LE</a> : <a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024a9e29ecc77281f945fb50c183cfae6749">LT</a>, pf[1][0], pf[2][1] );
<a name="l00612"></a>00612 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00613"></a>00613 }
<a name="l00614"></a>00614 <span class="keywordflow">else</span> <span class="keywordflow">if</span>(pf[0] == <a class="code" href="classLFSCObj.html#a32683494b48bed158c9373f18af0b524">d_real_shadow_eq_str</a>){
<a name="l00615"></a>00615 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9efdc855f3c1477957fb50affec07f8f">EQ</a>, pf[2][0], pf[2][1]);
<a name="l00616"></a>00616 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00617"></a>00617 }
<a name="l00618"></a>00618 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#ab1cfbe69faad1806adce5f1d83b6ad06">d_optimized_subst_op_str</a> || pf[0] == <a class="code" href="classLFSCObj.html#a033351a8f7c305990b272c70f210cf6c">d_basic_subst_op1_str</a> )
<a name="l00619"></a>00619 {
<a name="l00620"></a>00620 <span class="keywordflow">if</span>( pf[1].getKind()==<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba865555c9f2e0458a7078486aa1b3254f">AND</a> || pf[1].getKind()==<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba96727447c0ad447987df1c6415aef074">OR</a> || pf[1].getKind()==<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a> || <a class="code" href="Util_8cpp.html#a5462f02c7d83367f4d9e1b99f1975cb7">is_eq_kind</a>( pf[1].getKind() ) ||
<a name="l00621"></a>00621 ( pf[1].getKind()==<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3a4cfaf3eae8eac1dc2fd27d9f0994dc">ITE</a> && <a class="code" href="classLFSCObj.html#ace5ae3c05a540f101645ecfbacdd2928">isFormula</a>( pf[1] ) ) ){
<a name="l00622"></a>00622 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>, pf[1], pf[2] );
<a name="l00623"></a>00623 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00624"></a>00624 }<span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[1].getKind()==<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3a4cfaf3eae8eac1dc2fd27d9f0994dc">ITE</a> || pf[1].getKind()==<a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024a9a12fbdcaa45ef17eaa1802161f9ca98">PLUS</a> || pf[1].getKind()==<a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024aba18e0accfb91ddb34f4dcc79c626ec5">MINUS</a> || pf[1].getKind()==<a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024ad77e825b0133e40de2760344377ee1fa">MULT</a> ){
<a name="l00625"></a>00625 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9efdc855f3c1477957fb50affec07f8f">EQ</a>, pf[1], pf[2] );
<a name="l00626"></a>00626 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00627"></a>00627 }
<a name="l00628"></a>00628 }
<a name="l00629"></a>00629 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#a1c4d27683bd50cfb2a3598aed1eaa52b">d_andE_str</a> )
<a name="l00630"></a>00630 {
<a name="l00631"></a>00631 pe = pf[2][ pf[1].<a class="code" href="group__ExprPkg.html#gab0eee70e4a7f97c09954dc61b71b65e5" title="Get the Rational value out of RATIONAL_EXPR.">getRational</a>().<a class="code" href="classCVC3_1_1Rational.html#a953f2eb850fc3612097b5320dcda6047">getNumerator</a>().<a class="code" href="classCVC3_1_1Rational.html#a094636dfa3a740640ca1b0c7406f7e8f">getInt</a>() ];
<a name="l00632"></a>00632 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00633"></a>00633 }
<a name="l00634"></a>00634 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#a8ee48c649017b77e06deda136fde968d">d_rewrite_implies_str</a> )
<a name="l00635"></a>00635 {
<a name="l00636"></a>00636 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e1 = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7338bb59b9aa936104a6d2f631d4d8db">IMPLIES</a>, pf[1], pf[2] );
<a name="l00637"></a>00637 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e2 = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0378ebc895849163b249d0b330257dd6">NOT</a>, pf[1] );
<a name="l00638"></a>00638 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e3 = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba96727447c0ad447987df1c6415aef074">OR</a>, e2, pf[2] );
<a name="l00639"></a>00639 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>, e1, e3 );
<a name="l00640"></a>00640 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00641"></a>00641 }
<a name="l00642"></a>00642 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#a97b66c2bb2a7cf5475969f4929802cb2">d_rewrite_eq_symm_str</a> )
<a name="l00643"></a>00643 {
<a name="l00644"></a>00644 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e1 = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9efdc855f3c1477957fb50affec07f8f">EQ</a>, pf[2], pf[3] );
<a name="l00645"></a>00645 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e2 = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9efdc855f3c1477957fb50affec07f8f">EQ</a>, pf[3], pf[2] );
<a name="l00646"></a>00646 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>, e1, e2 );
<a name="l00647"></a>00647 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00648"></a>00648 }
<a name="l00649"></a>00649 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#a881021008ed360cbc5e7573e52fc7ec4">d_rewrite_iff_symm_str</a> )
<a name="l00650"></a>00650 {
<a name="l00651"></a>00651 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e1 = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>, pf[1], pf[2] );
<a name="l00652"></a>00652 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e2 = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>, pf[2], pf[1] );
<a name="l00653"></a>00653 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>, e1, e2 );
<a name="l00654"></a>00654 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00655"></a>00655 }
<a name="l00656"></a>00656 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#aa8367786a66947c4c6e390918e995eb9">d_rewrite_ite_same_str</a> )
<a name="l00657"></a>00657 {
<a name="l00658"></a>00658 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9efdc855f3c1477957fb50affec07f8f">EQ</a>, <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3a4cfaf3eae8eac1dc2fd27d9f0994dc">ITE</a>, pf[2], pf[3], pf[3] ), pf[3] );
<a name="l00659"></a>00659 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00660"></a>00660 }
<a name="l00661"></a>00661 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#a1eb48aeb323149091a40c35962d087b0">d_rewrite_eq_refl_str</a> )
<a name="l00662"></a>00662 {
<a name="l00663"></a>00663 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>, <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9efdc855f3c1477957fb50affec07f8f">EQ</a>, pf[2], pf[2] ), <a class="code" href="classLFSCObj.html#ad4d5ea192b766a7020fdfc7a462e99fe">d_pf_expr</a>.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4471fca49c2acbb7b4cf71e72bc55d6a" title="TRUE Expr.">trueExpr</a>() );
<a name="l00664"></a>00664 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00665"></a>00665 }
<a name="l00666"></a>00666 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#a18907b513101487ecbdc956b8d9884ce">d_refl_str</a> )
<a name="l00667"></a>00667 {
<a name="l00668"></a>00668 <span class="keywordflow">if</span>( <a class="code" href="classLFSCObj.html#ace5ae3c05a540f101645ecfbacdd2928">isFormula</a>( pf[1] ) )
<a name="l00669"></a>00669 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>, pf[1], pf[1] );
<a name="l00670"></a>00670 <span class="keywordflow">else</span>
<a name="l00671"></a>00671 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9efdc855f3c1477957fb50affec07f8f">EQ</a>, pf[1], pf[1] );
<a name="l00672"></a>00672 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00673"></a>00673 }
<a name="l00674"></a>00674 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#abe33b1cf4b7a701afd26466b8bbb3b3c">d_rewrite_not_not_str</a> )
<a name="l00675"></a>00675 {
<a name="l00676"></a>00676 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e1 = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0378ebc895849163b249d0b330257dd6">NOT</a>, pf[1] );
<a name="l00677"></a>00677 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0378ebc895849163b249d0b330257dd6">NOT</a>, e1 );
<a name="l00678"></a>00678 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00679"></a>00679 }
<a name="l00680"></a>00680 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#ab7930db598045de2b9b715d810f4821a">d_not_to_iff_str</a> )
<a name="l00681"></a>00681 {
<a name="l00682"></a>00682 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>, <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0378ebc895849163b249d0b330257dd6">NOT</a>, pf[1] ), <a class="code" href="classLFSCObj.html#ad4d5ea192b766a7020fdfc7a462e99fe">d_pf_expr</a>.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#gaae9db4c93c67cbf8bbf5d1e60e94f1ae" title="FALSE Expr.">falseExpr</a>() );
<a name="l00683"></a>00683 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00684"></a>00684 }
<a name="l00685"></a>00685 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#ae1b08b3ef34d91064a5d990c573916e8">d_minus_to_plus_str</a> )
<a name="l00686"></a>00686 {
<a name="l00687"></a>00687 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> er1 = <a class="code" href="classLFSCObj.html#ad4d5ea192b766a7020fdfc7a462e99fe">d_pf_expr</a>.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga18423a42ce6557dc33287d3979ccc3c6">newRatExpr</a>( <a class="code" href="classCVC3_1_1Rational.html">Rational</a>( -1 ) );
<a name="l00688"></a>00688 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9efdc855f3c1477957fb50affec07f8f">EQ</a>, <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024aba18e0accfb91ddb34f4dcc79c626ec5">MINUS</a>, pf[1], pf[2] ), <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024a9a12fbdcaa45ef17eaa1802161f9ca98">PLUS</a>, pf[1], <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024ad77e825b0133e40de2760344377ee1fa">MULT</a>, er1, pf[2] ) ) );
<a name="l00689"></a>00689 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00690"></a>00690 }
<a name="l00691"></a>00691 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#ae68fd62549e5191b31a2a9ff6e919033">d_right_minus_left_str</a> )
<a name="l00692"></a>00692 {
<a name="l00693"></a>00693 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> er1 = <a class="code" href="classLFSCObj.html#ad4d5ea192b766a7020fdfc7a462e99fe">d_pf_expr</a>.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga18423a42ce6557dc33287d3979ccc3c6">newRatExpr</a>( <a class="code" href="classCVC3_1_1Rational.html">Rational</a>( 0 ) );
<a name="l00694"></a>00694 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e1 = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( pf[1].getKind(), er1, <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024aba18e0accfb91ddb34f4dcc79c626ec5">MINUS</a>, pf[1][1], pf[1][0] ) );
<a name="l00695"></a>00695 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>, pf[1], e1);
<a name="l00696"></a>00696 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00697"></a>00697 }
<a name="l00698"></a>00698 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#ad1ebf052401eba516c3328f6a99ab389">d_negated_inequality_str</a> )
<a name="l00699"></a>00699 {
<a name="l00700"></a>00700 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>, pf[1], <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="Util_8cpp.html#a796942d5524726336add29080f902785">get_not</a>( pf[1][0].getKind() ), pf[1][0][0], pf[1][0][1] ) );
<a name="l00701"></a>00701 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00702"></a>00702 }
<a name="l00703"></a>00703 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#aa69b286d7f0dcc65e178cb7f189ce4e7">d_iff_false_elim_str</a> )
<a name="l00704"></a>00704 {
<a name="l00705"></a>00705 pe = <a class="code" href="classLFSCObj.html#af30e3e73af0d18b0775f0ccc6ddb9441">queryElimNotNot</a>( <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0378ebc895849163b249d0b330257dd6">NOT</a>, pf[1] ) );
<a name="l00706"></a>00706 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00707"></a>00707 }
<a name="l00708"></a>00708 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#a5e8f7307cd69eaa8381b94a55cb6b5f7">d_iff_true_str</a> )
<a name="l00709"></a>00709 {
<a name="l00710"></a>00710 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>, pf[1], <a class="code" href="classLFSCObj.html#ad4d5ea192b766a7020fdfc7a462e99fe">d_pf_expr</a>.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4471fca49c2acbb7b4cf71e72bc55d6a" title="TRUE Expr.">trueExpr</a>() );
<a name="l00711"></a>00711 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00712"></a>00712 }
<a name="l00713"></a>00713 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#a11a736d065275de2558ac8ba4ab624e5">d_iff_not_false_str</a> )
<a name="l00714"></a>00714 {
<a name="l00715"></a>00715 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>, <a class="code" href="classLFSCObj.html#af30e3e73af0d18b0775f0ccc6ddb9441">queryElimNotNot</a>( <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0378ebc895849163b249d0b330257dd6">NOT</a>, pf[1] ) ), <a class="code" href="classLFSCObj.html#ad4d5ea192b766a7020fdfc7a462e99fe">d_pf_expr</a>.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#gaae9db4c93c67cbf8bbf5d1e60e94f1ae" title="FALSE Expr.">falseExpr</a>() );
<a name="l00716"></a>00716 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00717"></a>00717 }
<a name="l00718"></a>00718 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#ad239f7556c548642b93bbad7808e4d08">d_uminus_to_mult_str</a> )
<a name="l00719"></a>00719 {
<a name="l00720"></a>00720 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> er1 = <a class="code" href="classLFSCObj.html#ad4d5ea192b766a7020fdfc7a462e99fe">d_pf_expr</a>.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga18423a42ce6557dc33287d3979ccc3c6">newRatExpr</a>( <a class="code" href="classCVC3_1_1Rational.html">Rational</a>( -1 ) );
<a name="l00721"></a>00721 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9efdc855f3c1477957fb50affec07f8f">EQ</a>, <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024a0b79738a0067780987896f3b91e8b0f1">UMINUS</a>, pf[1] ), <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="namespaceCVC3.html#a32d50a30de0e9e5bc4c2451de0107024ad77e825b0133e40de2760344377ee1fa">MULT</a>, er1, pf[1] ) );
<a name="l00722"></a>00722 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00723"></a>00723 }
<a name="l00724"></a>00724 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#a182c63a54b3d0435c67fd5dd212a43b1">d_rewrite_not_true_str</a> )
<a name="l00725"></a>00725 {
<a name="l00726"></a>00726 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>, <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0378ebc895849163b249d0b330257dd6">NOT</a>, <a class="code" href="classLFSCObj.html#ad4d5ea192b766a7020fdfc7a462e99fe">d_pf_expr</a>.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4471fca49c2acbb7b4cf71e72bc55d6a" title="TRUE Expr.">trueExpr</a>() ),
<a name="l00727"></a>00727 <a class="code" href="classLFSCObj.html#ad4d5ea192b766a7020fdfc7a462e99fe">d_pf_expr</a>.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#gaae9db4c93c67cbf8bbf5d1e60e94f1ae" title="FALSE Expr.">falseExpr</a>() );
<a name="l00728"></a>00728 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00729"></a>00729 }
<a name="l00730"></a>00730 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#a07f5cf7de5d7bd2f51a7dab8e8ced3ba">d_rewrite_not_false_str</a> )
<a name="l00731"></a>00731 {
<a name="l00732"></a>00732 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>, <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0378ebc895849163b249d0b330257dd6">NOT</a>, <a class="code" href="classLFSCObj.html#ad4d5ea192b766a7020fdfc7a462e99fe">d_pf_expr</a>.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#gaae9db4c93c67cbf8bbf5d1e60e94f1ae" title="FALSE Expr.">falseExpr</a>() ),
<a name="l00733"></a>00733 <a class="code" href="classLFSCObj.html#ad4d5ea192b766a7020fdfc7a462e99fe">d_pf_expr</a>.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4471fca49c2acbb7b4cf71e72bc55d6a" title="TRUE Expr.">trueExpr</a>() );
<a name="l00734"></a>00734 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00735"></a>00735 }
<a name="l00736"></a>00736 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#acebf70a838fce6dbdb1ad46c2ce277b9">d_cycle_conflict_str</a> )
<a name="l00737"></a>00737 {
<a name="l00738"></a>00738 pe = <a class="code" href="classLFSCObj.html#ad4d5ea192b766a7020fdfc7a462e99fe">d_pf_expr</a>.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#gaae9db4c93c67cbf8bbf5d1e60e94f1ae" title="FALSE Expr.">falseExpr</a>();
<a name="l00739"></a>00739 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00740"></a>00740 }
<a name="l00741"></a>00741 <span class="keywordflow">else</span> <span class="keywordflow">if</span>(pf[0] == <a class="code" href="classLFSCObj.html#a4d5aacd643a90b9082037521c561eebc">d_implyNegatedInequality_str</a>)
<a name="l00742"></a>00742 {
<a name="l00743"></a>00743 pe = pf[1].<a class="code" href="group__ExprPkg.html#ga8dd97bcdeb9d8870238f94a263fd083b">impExpr</a>(pf[3]);
<a name="l00744"></a>00744 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00745"></a>00745 }
<a name="l00746"></a>00746 <span class="keywordflow">else</span> <span class="keywordflow">if</span>(pf[0] == <a class="code" href="classLFSCObj.html#a5eb9b49376b9c44fdd1c879a56cb4927">d_implyWeakerInequality_str</a>){
<a name="l00747"></a>00747 pe = pf[1].<a class="code" href="group__ExprPkg.html#ga8dd97bcdeb9d8870238f94a263fd083b">impExpr</a>(pf[2]);
<a name="l00748"></a>00748 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00749"></a>00749 }
<a name="l00750"></a>00750 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#a881021008ed360cbc5e7573e52fc7ec4">d_rewrite_iff_symm_str</a> )
<a name="l00751"></a>00751 {
<a name="l00752"></a>00752 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e1 = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>, pf[1], pf[2] );
<a name="l00753"></a>00753 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e2 = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>, pf[2], pf[1] );
<a name="l00754"></a>00754 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>, e1, e2 );
<a name="l00755"></a>00755 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00756"></a>00756 }
<a name="l00757"></a>00757 <span class="keywordflow">else</span> <span class="keywordflow">if</span>( pf[0] == <a class="code" href="classLFSCObj.html#ae22d245587e43b53436e8bdf99914c5c">d_rewrite_iff_str</a>){
<a name="l00758"></a>00758 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>( <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>, pf[1], pf[2]);
<a name="l00759"></a>00759 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e_true = <a class="code" href="classLFSCObj.html#ad4d5ea192b766a7020fdfc7a462e99fe">d_pf_expr</a>.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4471fca49c2acbb7b4cf71e72bc55d6a" title="TRUE Expr.">trueExpr</a>();
<a name="l00760"></a>00760 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e_false = <a class="code" href="classLFSCObj.html#ad4d5ea192b766a7020fdfc7a462e99fe">d_pf_expr</a>.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#gaae9db4c93c67cbf8bbf5d1e60e94f1ae" title="FALSE Expr.">falseExpr</a>();
<a name="l00761"></a>00761
<a name="l00762"></a>00762 <span class="keywordflow">if</span>(pf[1] == pf[2]){
<a name="l00763"></a>00763 pe = e.<a class="code" href="group__ExprPkg.html#gaae017ca8e68af655ba285c985dd9fba5">iffExpr</a>(<a class="code" href="classLFSCObj.html#ad4d5ea192b766a7020fdfc7a462e99fe">d_pf_expr</a>.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4471fca49c2acbb7b4cf71e72bc55d6a" title="TRUE Expr.">trueExpr</a>());
<a name="l00764"></a>00764 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00765"></a>00765 }
<a name="l00766"></a>00766
<a name="l00767"></a>00767 <span class="keywordflow">if</span>(pf[1] == e_true){
<a name="l00768"></a>00768 pe = e.<a class="code" href="group__ExprPkg.html#gaae017ca8e68af655ba285c985dd9fba5">iffExpr</a>(e_true);
<a name="l00769"></a>00769 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00770"></a>00770 }
<a name="l00771"></a>00771 <span class="keywordflow">if</span>(pf[1] == e_false){
<a name="l00772"></a>00772 pe = e.<a class="code" href="group__ExprPkg.html#gaae017ca8e68af655ba285c985dd9fba5">iffExpr</a>(e_false);
<a name="l00773"></a>00773 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00774"></a>00774 }
<a name="l00775"></a>00775
<a name="l00776"></a>00776 <span class="keywordflow">if</span>(pf[1].isNot() && pf[1][0] == pf[2]){
<a name="l00777"></a>00777 pe = e.<a class="code" href="group__ExprPkg.html#gaae017ca8e68af655ba285c985dd9fba5">iffExpr</a>(pf[2].negate());
<a name="l00778"></a>00778 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00779"></a>00779 }
<a name="l00780"></a>00780
<a name="l00781"></a>00781 <span class="keywordflow">if</span>(pf[2] == e_true){
<a name="l00782"></a>00782 pe = e.<a class="code" href="group__ExprPkg.html#gaae017ca8e68af655ba285c985dd9fba5">iffExpr</a>(e_true);
<a name="l00783"></a>00783 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00784"></a>00784 }
<a name="l00785"></a>00785
<a name="l00786"></a>00786 <span class="keywordflow">if</span>(pf[2] == e_false){
<a name="l00787"></a>00787 pe = e.<a class="code" href="group__ExprPkg.html#gaae017ca8e68af655ba285c985dd9fba5">iffExpr</a>(e_false);
<a name="l00788"></a>00788 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00789"></a>00789 }
<a name="l00790"></a>00790
<a name="l00791"></a>00791 <span class="keywordflow">if</span>(pf[2].isNot() && pf[2][0] == pf[1]){
<a name="l00792"></a>00792 pe = e.<a class="code" href="group__ExprPkg.html#gaae017ca8e68af655ba285c985dd9fba5">iffExpr</a>(pf[1].negate());
<a name="l00793"></a>00793 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00794"></a>00794 }
<a name="l00795"></a>00795
<a name="l00796"></a>00796 <span class="keywordflow">if</span>(pf[1] < pf[2]){
<a name="l00797"></a>00797 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e_sym = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>, pf[2], pf[1]);
<a name="l00798"></a>00798 pe = e.<a class="code" href="group__ExprPkg.html#gaae017ca8e68af655ba285c985dd9fba5">iffExpr</a>(e_sym);
<a name="l00799"></a>00799 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00800"></a>00800 }
<a name="l00801"></a>00801 pe = e.<a class="code" href="group__ExprPkg.html#gaae017ca8e68af655ba285c985dd9fba5">iffExpr</a>(e);
<a name="l00802"></a>00802 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00803"></a>00803 }
<a name="l00804"></a>00804 <span class="keywordflow">else</span> <span class="keywordflow">if</span>(pf[0] == <a class="code" href="classLFSCObj.html#ad5b7a93ffe8bb6c33527008d0584c5ac">d_implyEqualities_str</a>){
<a name="l00805"></a>00805 pe = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba865555c9f2e0458a7078486aa1b3254f">AND</a>, pf[1][0]);
<a name="l00806"></a>00806 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00807"></a>00807 }
<a name="l00808"></a>00808 }
<a name="l00809"></a>00809 }
<a name="l00810"></a>00810 ostringstream ose;
<a name="l00811"></a>00811 ose << <span class="stringliteral">"What_is_proven, unknown: ("</span> << <a class="code" href="classLFSCObj.html#af10438dca895f5232bc436e0d95acdd3">d_rules</a>[pf[0]] << <span class="stringliteral">"): "</span> << pf[0];
<a name="l00812"></a>00812 <a class="code" href="classObj.html#a7a13d6281d09d895f9db31157fe62f0d">print_error</a>( ose.str().c_str(), cout );
<a name="l00813"></a>00813 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00814"></a>00814 }
</pre></div></div>
</div>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
