<!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: LFSCBoolProof.h Source File</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li><a href="annotated.html"><span>Classes</span></a></li>
<li class="current"><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="files.html"><span>File List</span></a></li>
<li><a href="globals.html"><span>File Members</span></a></li>
</ul>
</div>
<div class="header">
<div class="headertitle">
<div class="title">LFSCBoolProof.h</div> </div>
</div>
<div class="contents">
<a href="LFSCBoolProof_8h.html">Go to the documentation of this file.</a><div class="fragment"><pre class="fragment"><a name="l00001"></a>00001 <span class="preprocessor">#ifndef LFSC_BOOL_PROOF_H_</span>
<a name="l00002"></a>00002 <span class="preprocessor"></span><span class="preprocessor">#define LFSC_BOOL_PROOF_H_</span>
<a name="l00003"></a>00003 <span class="preprocessor"></span>
<a name="l00004"></a>00004 <span class="preprocessor">#include "<a class="code" href="LFSCProof_8h.html">LFSCProof.h</a>"</span>
<a name="l00005"></a>00005
<a name="l00006"></a><a class="code" href="classLFSCBoolRes.html">00006</a> <span class="keyword">class </span><a class="code" href="classLFSCBoolRes.html">LFSCBoolRes</a> : <span class="keyword">public</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>
<a name="l00007"></a>00007 {
<a name="l00008"></a>00008 <span class="keyword">private</span>:
<a name="l00009"></a><a class="code" href="classLFSCBoolRes.html#ae045081b1f204a71e589fb246985f786">00009</a> <a class="code" href="classRefPtr.html">RefPtr< LFSCProof ></a> <a class="code" href="classLFSCBoolRes.html#ae045081b1f204a71e589fb246985f786">d_children</a>[2];
<a name="l00010"></a><a class="code" href="classLFSCBoolRes.html#aa2fc185fb1a1658b1933b91ae9f10b9c">00010</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCBoolRes.html#aa2fc185fb1a1658b1933b91ae9f10b9c">d_var</a>;
<a name="l00011"></a><a class="code" href="classLFSCBoolRes.html#a3dd333196cf99c1a5771ca50b5d45942">00011</a> <span class="keywordtype">bool</span> <a class="code" href="classLFSCBoolRes.html#a3dd333196cf99c1a5771ca50b5d45942">d_col</a>;
<a name="l00012"></a><a class="code" href="classLFSCBoolRes.html#ad015663423be640b082ed9d787b011e0">00012</a> <a class="code" href="classLFSCBoolRes.html#ad015663423be640b082ed9d787b011e0">LFSCBoolRes</a>(<a class="code" href="classLFSCProof.html">LFSCProof</a>* pf1, <a class="code" href="classLFSCProof.html">LFSCProof</a>* pf2, <span class="keywordtype">int</span> v, <span class="keywordtype">bool</span> col): <a class="code" href="classLFSCProof.html">LFSCProof</a>(),
<a name="l00013"></a>00013 <a class="code" href="classLFSCBoolRes.html#aa2fc185fb1a1658b1933b91ae9f10b9c">d_var</a>(v), <a class="code" href="classLFSCBoolRes.html#a3dd333196cf99c1a5771ca50b5d45942">d_col</a>(col){
<a name="l00014"></a>00014 <a class="code" href="classLFSCBoolRes.html#ae045081b1f204a71e589fb246985f786">d_children</a>[0] = pf1;
<a name="l00015"></a>00015 <a class="code" href="classLFSCBoolRes.html#ae045081b1f204a71e589fb246985f786">d_children</a>[1] = pf2;
<a name="l00016"></a>00016 }
<a name="l00017"></a><a class="code" href="classLFSCBoolRes.html#a706d6e18169832981459d9d53bf97b1d">00017</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCBoolRes.html#a706d6e18169832981459d9d53bf97b1d">~LFSCBoolRes</a>(){}
<a name="l00018"></a><a class="code" href="classLFSCBoolRes.html#a735517bb51cdfa5057945c87992ad14a">00018</a> <span class="keywordtype">long</span> <span class="keywordtype">int</span> <a class="code" href="classLFSCBoolRes.html#a735517bb51cdfa5057945c87992ad14a">get_length</a>(){
<a name="l00019"></a>00019 <span class="keywordflow">return</span> 10 + <a class="code" href="classLFSCBoolRes.html#ae045081b1f204a71e589fb246985f786">d_children</a>[0]->get_string_length() + <a class="code" href="classLFSCBoolRes.html#ae045081b1f204a71e589fb246985f786">d_children</a>[1]->get_string_length();
<a name="l00020"></a>00020 }
<a name="l00021"></a>00021 <span class="keyword">public</span>:
<a name="l00022"></a><a class="code" href="classLFSCBoolRes.html#a55ed62198bc8c13254cb8f7f38afbd05">00022</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCBoolRes.html">LFSCBoolRes</a>* <a class="code" href="classLFSCBoolRes.html#a55ed62198bc8c13254cb8f7f38afbd05">AsLFSCBoolRes</a>(){ <span class="keywordflow">return</span> <span class="keyword">this</span>; }
<a name="l00023"></a>00023 <span class="keywordtype">void</span> <a class="code" href="classLFSCBoolRes.html#a6d09024324b4d619bd9f34e178ac57d5">print_pf</a>( std::ostream& s, <span class="keywordtype">int</span> ind = 0 );
<a name="l00024"></a>00024 <span class="keywordtype">void</span> <a class="code" href="classLFSCBoolRes.html#a9b6c2508cb389bd861357b832bde2502">print_struct</a>( std::ostream& s, <span class="keywordtype">int</span> ind = 0 );
<a name="l00025"></a>00025 <span class="comment">//standard Make</span>
<a name="l00026"></a>00026 <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCBoolRes.html#a721ac95de042a1be9fcfe6d7b6e5df71">Make</a>(<a class="code" href="classLFSCProof.html">LFSCProof</a>* pf1, <a class="code" href="classLFSCProof.html">LFSCProof</a>* pf2, <span class="keywordtype">int</span> v, <span class="keywordtype">bool</span> col);
<a name="l00027"></a>00027 <span class="comment">// make the boolean resolution proof, where p1 corresponds to pf1, p2 corresponds to pf2</span>
<a name="l00028"></a>00028 <span class="comment">//res is the expression to resolve upon</span>
<a name="l00029"></a>00029 <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCBoolRes.html#a721ac95de042a1be9fcfe6d7b6e5df71">Make</a>( <a class="code" href="classLFSCProof.html">LFSCProof</a>* p1, <a class="code" href="classLFSCProof.html">LFSCProof</a>* p2, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& res, <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> cascadeOr = <span class="keyword">false</span> );
<a name="l00030"></a>00030 <span class="comment">//make the boolean resolution collection proof, where e is what to resolve</span>
<a name="l00031"></a>00031 <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCBoolRes.html#a6313b796f9dbbf3352cdb113eb83d42d">MakeC</a>( <a class="code" href="classLFSCProof.html">LFSCProof</a>* p, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& res );
<a name="l00032"></a><a class="code" href="classLFSCBoolRes.html#a8fa3bfd1f1e57790d7bfd697cee9c4c2">00032</a> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCBoolRes.html#a8fa3bfd1f1e57790d7bfd697cee9c4c2">clone</a>() { <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classLFSCBoolRes.html#ad015663423be640b082ed9d787b011e0">LFSCBoolRes</a>( <a class="code" href="classLFSCBoolRes.html#ae045081b1f204a71e589fb246985f786">d_children</a>[0].<span class="keyword">get</span>(), <a class="code" href="classLFSCBoolRes.html#ae045081b1f204a71e589fb246985f786">d_children</a>[1].<span class="keyword">get</span>(), <a class="code" href="classLFSCBoolRes.html#aa2fc185fb1a1658b1933b91ae9f10b9c">d_var</a>, <a class="code" href="classLFSCBoolRes.html#a3dd333196cf99c1a5771ca50b5d45942">d_col</a> ); }
<a name="l00033"></a><a class="code" href="classLFSCBoolRes.html#a44545b6339ce2e4f0dc483cf60f9e8e7">00033</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCBoolRes.html#a44545b6339ce2e4f0dc483cf60f9e8e7">getNumChildren</a>() { <span class="keywordflow">return</span> 2; }
<a name="l00034"></a><a class="code" href="classLFSCBoolRes.html#a7d68231f4e37f4acf4ce4e8460ebeb92">00034</a> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCBoolRes.html#a7d68231f4e37f4acf4ce4e8460ebeb92">getChild</a>( <span class="keywordtype">int</span> n ) { <span class="keywordflow">return</span> <a class="code" href="classLFSCBoolRes.html#ae045081b1f204a71e589fb246985f786">d_children</a>[n].<a class="code" href="classRefPtr.html#a2b987fbb75b20a1da1bd959325635e7e">get</a>(); }
<a name="l00035"></a>00035 <span class="keywordtype">int</span> <a class="code" href="classLFSCBoolRes.html#af17c4cbbc04604af6bdd4a893d07b1b0">checkBoolRes</a>( std::vector< int >& clause );
<a name="l00036"></a>00036 };
<a name="l00037"></a>00037
<a name="l00038"></a><a class="code" href="classLFSCLem.html">00038</a> <span class="keyword">class </span><a class="code" href="classLFSCLem.html">LFSCLem</a> : <span class="keyword">public</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>
<a name="l00039"></a>00039 {
<a name="l00040"></a>00040 <span class="keyword">private</span>:
<a name="l00041"></a><a class="code" href="classLFSCLem.html#a7c50798fae9bc2dd292af69aea46f0ca">00041</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCLem.html#a7c50798fae9bc2dd292af69aea46f0ca">d_var</a>;
<a name="l00042"></a><a class="code" href="classLFSCLem.html#a409936d5baa434b32b6c5a0bedfe3044">00042</a> <a class="code" href="classLFSCLem.html#a409936d5baa434b32b6c5a0bedfe3044">LFSCLem</a>( <span class="keywordtype">int</span> v ) : <a class="code" href="classLFSCProof.html">LFSCProof</a>(),
<a name="l00043"></a>00043 <a class="code" href="classLFSCLem.html#a7c50798fae9bc2dd292af69aea46f0ca">d_var</a>( v ) {}
<a name="l00044"></a><a class="code" href="classLFSCLem.html#ac384d7fdb899b676e7b44ab9db21427e">00044</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCLem.html#ac384d7fdb899b676e7b44ab9db21427e">~LFSCLem</a>(){}
<a name="l00045"></a><a class="code" href="classLFSCLem.html#ad1fa27fc76b749c9fad43121931936de">00045</a> <span class="keywordtype">long</span> <span class="keywordtype">int</span> <a class="code" href="classLFSCLem.html#ad1fa27fc76b749c9fad43121931936de">get_length</a>() { <span class="keywordflow">return</span> 10; }
<a name="l00046"></a>00046 <span class="keyword">public</span>:
<a name="l00047"></a><a class="code" href="classLFSCLem.html#a8889765b9388d270f84678585476ec06">00047</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCLem.html">LFSCLem</a>* <a class="code" href="classLFSCLem.html#a8889765b9388d270f84678585476ec06">AsLFSCLem</a>(){ <span class="keywordflow">return</span> <span class="keyword">this</span>; }
<a name="l00048"></a><a class="code" href="classLFSCLem.html#a38c060085273f0dd8c425a14683b4067">00048</a> <span class="keywordtype">void</span> <a class="code" href="classLFSCLem.html#a38c060085273f0dd8c425a14683b4067">print_pf</a>( std::ostream& s, <span class="keywordtype">int</span> ind = 0 ){ s << <span class="stringliteral">"(lem _ _ @a"</span> << <a class="code" href="namespaceCVC3.html#a39fc111339d6dffdc98d6a25b68dff0e">abs</a>( <a class="code" href="classLFSCLem.html#a7c50798fae9bc2dd292af69aea46f0ca">d_var</a> ) << <span class="stringliteral">")"</span>; }
<a name="l00049"></a><a class="code" href="classLFSCLem.html#a65692ca4d960a021ad165fb89c411021">00049</a> <span class="keywordtype">void</span> <a class="code" href="classLFSCLem.html#a65692ca4d960a021ad165fb89c411021">print_struct</a>( std::ostream& s, <span class="keywordtype">int</span> ind = 0 ){ s << <span class="stringliteral">"(lem "</span> << <a class="code" href="classLFSCLem.html#a7c50798fae9bc2dd292af69aea46f0ca">d_var</a> << <span class="stringliteral">")"</span>; }
<a name="l00050"></a><a class="code" href="classLFSCLem.html#abb9541ac21517f3bd70abb11a97a7715">00050</a> <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCLem.html#abb9541ac21517f3bd70abb11a97a7715">Make</a>(<span class="keywordtype">int</span> v){ <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classLFSCLem.html#a409936d5baa434b32b6c5a0bedfe3044">LFSCLem</a>( v ); }
<a name="l00051"></a><a class="code" href="classLFSCLem.html#aefd7d0d4c09421c5cf4c4832c828f642">00051</a> <span class="keywordtype">bool</span> <a class="code" href="classLFSCLem.html#aefd7d0d4c09421c5cf4c4832c828f642">IsTrivial</a>() { <span class="keywordflow">return</span> <span class="keyword">true</span>; }
<a name="l00052"></a><a class="code" href="classLFSCLem.html#a10cff9d19d35ca803eb2d86379fbfea9">00052</a> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCLem.html#a10cff9d19d35ca803eb2d86379fbfea9">clone</a>() { <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classLFSCLem.html#a409936d5baa434b32b6c5a0bedfe3044">LFSCLem</a>( <a class="code" href="classLFSCLem.html#a7c50798fae9bc2dd292af69aea46f0ca">d_var</a> ); }
<a name="l00053"></a><a class="code" href="classLFSCLem.html#a5ee6477298840bdaf7fb5103ac293180">00053</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCLem.html#a5ee6477298840bdaf7fb5103ac293180">checkBoolRes</a>( std::vector< int >& clause ){
<a name="l00054"></a>00054 clause.push_back( -<a class="code" href="classLFSCLem.html#a7c50798fae9bc2dd292af69aea46f0ca">d_var</a> );
<a name="l00055"></a>00055 clause.push_back( <a class="code" href="classLFSCLem.html#a7c50798fae9bc2dd292af69aea46f0ca">d_var</a> );
<a name="l00056"></a>00056 <span class="keywordflow">return</span> 0;
<a name="l00057"></a>00057 }
<a name="l00058"></a>00058 };
<a name="l00059"></a>00059
<a name="l00060"></a><a class="code" href="classLFSCClausify.html">00060</a> <span class="keyword">class </span><a class="code" href="classLFSCClausify.html">LFSCClausify</a> : <span class="keyword">public</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>
<a name="l00061"></a>00061 {
<a name="l00062"></a>00062 <span class="keyword">private</span>:
<a name="l00063"></a><a class="code" href="classLFSCClausify.html#a2d3cb4e50f5ffb662dc18e83ee206c2c">00063</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classLFSCPrinter.html">LFSCPrinter</a>;
<a name="l00064"></a><a class="code" href="classLFSCClausify.html#a84a1963e40def721dc6844f24c6a20f9">00064</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCClausify.html#a84a1963e40def721dc6844f24c6a20f9">d_var</a>;
<a name="l00065"></a><a class="code" href="classLFSCClausify.html#a4860ffb7bc3a8a3273e3a8d474e33d71">00065</a> <a class="code" href="classRefPtr.html">RefPtr< LFSCProof ></a> <a class="code" href="classLFSCClausify.html#a4860ffb7bc3a8a3273e3a8d474e33d71">d_pf</a>;
<a name="l00066"></a><a class="code" href="classLFSCClausify.html#a81445a757de59d083bd8d0073961ed8f">00066</a> <a class="code" href="classLFSCClausify.html#a81445a757de59d083bd8d0073961ed8f">LFSCClausify</a>( <span class="keywordtype">int</span> v, <a class="code" href="classLFSCProof.html">LFSCProof</a>* pf ) : <a class="code" href="classLFSCProof.html">LFSCProof</a>(), <a class="code" href="classLFSCClausify.html#a84a1963e40def721dc6844f24c6a20f9">d_var</a>( v ), <a class="code" href="classLFSCClausify.html#a4860ffb7bc3a8a3273e3a8d474e33d71">d_pf</a>( pf ){}
<a name="l00067"></a><a class="code" href="classLFSCClausify.html#aa14aa3c8b72b26c3669f9d4c8afcf0f0">00067</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCClausify.html#aa14aa3c8b72b26c3669f9d4c8afcf0f0">~LFSCClausify</a>(){}
<a name="l00068"></a><a class="code" href="classLFSCClausify.html#a36d74d26af6ecf508ff51445e3e4f7cd">00068</a> <span class="keywordtype">long</span> <span class="keywordtype">int</span> <a class="code" href="classLFSCClausify.html#a36d74d26af6ecf508ff51445e3e4f7cd">get_length</a>() { <span class="keywordflow">return</span> 10 + <a class="code" href="classLFSCClausify.html#a4860ffb7bc3a8a3273e3a8d474e33d71">d_pf</a>->get_string_length(); }
<a name="l00069"></a>00069 <span class="comment">//this should be called by Make</span>
<a name="l00070"></a>00070 <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCClausify.html#af22d08150cb2f47d017ed68e3c31093a">Make_i</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <a class="code" href="classLFSCProof.html">LFSCProof</a>* p, std::vector< Expr >& exprs, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& end );
<a name="l00071"></a>00071 <span class="keyword">public</span>:
<a name="l00072"></a><a class="code" href="classLFSCClausify.html#a891e43a4ad778be5cd450a414eca4214">00072</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCClausify.html">LFSCClausify</a>* <a class="code" href="classLFSCClausify.html#a891e43a4ad778be5cd450a414eca4214">AsLFSCClausify</a>(){ <span class="keywordflow">return</span> <span class="keyword">this</span>; }
<a name="l00073"></a>00073 <span class="keywordtype">void</span> <a class="code" href="classLFSCClausify.html#a571d958b1b69082a99ee3e8c2e1e5a82">print_pf</a>( std::ostream& s, <span class="keywordtype">int</span> ind = 0 );
<a name="l00074"></a><a class="code" href="classLFSCClausify.html#ab65fca27b5949176646d5b7c3c703604">00074</a> <span class="keywordtype">void</span> <a class="code" href="classLFSCClausify.html#ab65fca27b5949176646d5b7c3c703604">print_struct</a>( std::ostream& s, <span class="keywordtype">int</span> ind = 0 ){ s << <span class="stringliteral">"(clausify "</span> << <a class="code" href="classLFSCClausify.html#a84a1963e40def721dc6844f24c6a20f9">d_var</a> << <span class="stringliteral">")"</span>; }
<a name="l00075"></a>00075 <span class="comment">//standard Make</span>
<a name="l00076"></a><a class="code" href="classLFSCClausify.html#a976ffe7504641550090b29a9b5cf5732">00076</a> <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCClausify.html#a976ffe7504641550090b29a9b5cf5732">Make</a>( <span class="keywordtype">int</span> v, <a class="code" href="classLFSCProof.html">LFSCProof</a>* pf ){ <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classLFSCClausify.html#a81445a757de59d083bd8d0073961ed8f">LFSCClausify</a>( v, pf ); }
<a name="l00077"></a>00077 <span class="comment">// input : a formula e, and a proof of that formula p.</span>
<a name="l00078"></a>00078 <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCClausify.html#a976ffe7504641550090b29a9b5cf5732">Make</a>( <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <a class="code" href="classLFSCProof.html">LFSCProof</a>* p, <span class="keywordtype">bool</span> cascadeOr = <span class="keyword">false</span> );
<a name="l00079"></a>00079 <span class="comment">//clone</span>
<a name="l00080"></a><a class="code" href="classLFSCClausify.html#abfb721ca8127c842987d38302d4dee93">00080</a> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCClausify.html#abfb721ca8127c842987d38302d4dee93">clone</a>() { <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classLFSCClausify.html#a81445a757de59d083bd8d0073961ed8f">LFSCClausify</a>( <a class="code" href="classLFSCClausify.html#a84a1963e40def721dc6844f24c6a20f9">d_var</a>, <a class="code" href="classLFSCClausify.html#a4860ffb7bc3a8a3273e3a8d474e33d71">d_pf</a>.<a class="code" href="classRefPtr.html#a2b987fbb75b20a1da1bd959325635e7e">get</a>() ); }
<a name="l00081"></a><a class="code" href="classLFSCClausify.html#a3942b93955d5161fbcc7a48d49ffc351">00081</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCClausify.html#a3942b93955d5161fbcc7a48d49ffc351">getNumChildren</a>() { <span class="keywordflow">return</span> 1; }
<a name="l00082"></a><a class="code" href="classLFSCClausify.html#a7eb20929cbad20089813d56d92b4336e">00082</a> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCClausify.html#a7eb20929cbad20089813d56d92b4336e">getChild</a>( <span class="keywordtype">int</span> n ) { <span class="keywordflow">return</span> <a class="code" href="classLFSCClausify.html#a4860ffb7bc3a8a3273e3a8d474e33d71">d_pf</a>.<a class="code" href="classRefPtr.html#a2b987fbb75b20a1da1bd959325635e7e">get</a>(); }
<a name="l00083"></a><a class="code" href="classLFSCClausify.html#a60f52fa75358e5259eaf640bd2919d3f">00083</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCClausify.html#a60f52fa75358e5259eaf640bd2919d3f">checkBoolRes</a>( std::vector< int >& clause ){
<a name="l00084"></a>00084 <a class="code" href="classLFSCClausify.html#a4860ffb7bc3a8a3273e3a8d474e33d71">d_pf</a>->checkBoolRes( clause );
<a name="l00085"></a>00085 clause.push_back( <a class="code" href="classLFSCClausify.html#a84a1963e40def721dc6844f24c6a20f9">d_var</a> );
<a name="l00086"></a>00086 <span class="keywordflow">return</span> 0;
<a name="l00087"></a>00087 }
<a name="l00088"></a>00088 };
<a name="l00089"></a>00089
<a name="l00090"></a><a class="code" href="classLFSCAssume.html">00090</a> <span class="keyword">class </span><a class="code" href="classLFSCAssume.html">LFSCAssume</a> : <span class="keyword">public</span> <a class="code" href="classLFSCProof.html">LFSCProof</a> {
<a name="l00091"></a>00091 <span class="keyword">private</span>:
<a name="l00092"></a><a class="code" href="classLFSCAssume.html#af94fac0616eadaef230e68e417d12f32">00092</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCAssume.html#af94fac0616eadaef230e68e417d12f32">d_var</a>;
<a name="l00093"></a><a class="code" href="classLFSCAssume.html#aa3b39dbcb72090c1e629b79c9f247220">00093</a> <a class="code" href="classRefPtr.html">RefPtr< LFSCProof ></a> <a class="code" href="classLFSCAssume.html#aa3b39dbcb72090c1e629b79c9f247220">d_pf</a>;
<a name="l00094"></a><a class="code" href="classLFSCAssume.html#ad12dc19473bae44f36547594096ec3b2">00094</a> <span class="keywordtype">bool</span> <a class="code" href="classLFSCAssume.html#ad12dc19473bae44f36547594096ec3b2">d_assm</a>;
<a name="l00095"></a><a class="code" href="classLFSCAssume.html#a9ed812125981b8f0379eaa0b9b3f9ad7">00095</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCAssume.html#a9ed812125981b8f0379eaa0b9b3f9ad7">d_type</a>;
<a name="l00096"></a><a class="code" href="classLFSCAssume.html#a6599b800baaae695dea15a31a1f2384f">00096</a> <a class="code" href="classLFSCAssume.html#a6599b800baaae695dea15a31a1f2384f">LFSCAssume</a>( <span class="keywordtype">int</span> v, <a class="code" href="classLFSCProof.html">LFSCProof</a>* pf, <span class="keywordtype">bool</span> assm, <span class="keywordtype">int</span> type ) : <a class="code" href="classLFSCProof.html">LFSCProof</a>(), <a class="code" href="classLFSCAssume.html#af94fac0616eadaef230e68e417d12f32">d_var</a>( v ), <a class="code" href="classLFSCAssume.html#aa3b39dbcb72090c1e629b79c9f247220">d_pf</a>( pf ), <a class="code" href="classLFSCAssume.html#ad12dc19473bae44f36547594096ec3b2">d_assm</a>( assm ), <a class="code" href="classLFSCAssume.html#a9ed812125981b8f0379eaa0b9b3f9ad7">d_type</a>( type ){}
<a name="l00097"></a><a class="code" href="classLFSCAssume.html#a0b3112464ac68fe8cd3093fa0b0bb575">00097</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCAssume.html#a0b3112464ac68fe8cd3093fa0b0bb575">~LFSCAssume</a>(){}
<a name="l00098"></a><a class="code" href="classLFSCAssume.html#a2109fe5fdc3237a8b881564616b6bfbb">00098</a> <span class="keywordtype">long</span> <span class="keywordtype">int</span> <a class="code" href="classLFSCAssume.html#a2109fe5fdc3237a8b881564616b6bfbb">get_length</a>() { <span class="keywordflow">return</span> 10 + <a class="code" href="classLFSCAssume.html#aa3b39dbcb72090c1e629b79c9f247220">d_pf</a>->get_string_length(); }
<a name="l00099"></a>00099 <span class="keyword">public</span>:
<a name="l00100"></a><a class="code" href="classLFSCAssume.html#a62a38c16c3d0175a2a0e9ca1504716c7">00100</a> <span class="keyword">virtual</span> <a class="code" href="classLFSCAssume.html">LFSCAssume</a>* <a class="code" href="classLFSCAssume.html#a62a38c16c3d0175a2a0e9ca1504716c7">AsLFSCAssume</a>(){ <span class="keywordflow">return</span> <span class="keyword">this</span>; }
<a name="l00101"></a>00101 <span class="keywordtype">void</span> <a class="code" href="classLFSCAssume.html#ab8bc3cbf1aef169b856d704eceef4be6">print_pf</a>( std::ostream& s, <span class="keywordtype">int</span> ind = 0 );
<a name="l00102"></a>00102 <span class="keywordtype">void</span> <a class="code" href="classLFSCAssume.html#a61b64cc4b4ded52c63db33fa821ec20d">print_struct</a>( std::ostream& s, <span class="keywordtype">int</span> ind = 0 );
<a name="l00103"></a><a class="code" href="classLFSCAssume.html#a1936e5119fa84aec4acc5d8ba83bc30b">00103</a> <span class="keyword">static</span> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCAssume.html#a1936e5119fa84aec4acc5d8ba83bc30b">Make</a>( <span class="keywordtype">int</span> v, <a class="code" href="classLFSCProof.html">LFSCProof</a>* pf, <span class="keywordtype">bool</span> assm = <span class="keyword">true</span>, <span class="keywordtype">int</span> type=3 ){
<a name="l00104"></a>00104 <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classLFSCAssume.html#a6599b800baaae695dea15a31a1f2384f">LFSCAssume</a>( v, pf, assm, type );
<a name="l00105"></a>00105 }
<a name="l00106"></a><a class="code" href="classLFSCAssume.html#a09b11c30192e746c3d4f61786811a0c3">00106</a> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCAssume.html#a09b11c30192e746c3d4f61786811a0c3">clone</a>() { <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classLFSCAssume.html#a6599b800baaae695dea15a31a1f2384f">LFSCAssume</a>( <a class="code" href="classLFSCAssume.html#af94fac0616eadaef230e68e417d12f32">d_var</a>, <a class="code" href="classLFSCAssume.html#aa3b39dbcb72090c1e629b79c9f247220">d_pf</a>.<a class="code" href="classRefPtr.html#a2b987fbb75b20a1da1bd959325635e7e">get</a>(), <a class="code" href="classLFSCAssume.html#ad12dc19473bae44f36547594096ec3b2">d_assm</a>, <a class="code" href="classLFSCAssume.html#a9ed812125981b8f0379eaa0b9b3f9ad7">d_type</a> ); }
<a name="l00107"></a><a class="code" href="classLFSCAssume.html#a92ae711a4382449ee1923cb07742c5c4">00107</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCAssume.html#a92ae711a4382449ee1923cb07742c5c4">getNumChildren</a>() { <span class="keywordflow">return</span> 1; }
<a name="l00108"></a><a class="code" href="classLFSCAssume.html#ab2d0929158466c1c13a416cafe5f1b33">00108</a> <a class="code" href="classLFSCProof.html">LFSCProof</a>* <a class="code" href="classLFSCAssume.html#ab2d0929158466c1c13a416cafe5f1b33">getChild</a>( <span class="keywordtype">int</span> n ) { <span class="keywordflow">return</span> <a class="code" href="classLFSCAssume.html#aa3b39dbcb72090c1e629b79c9f247220">d_pf</a>.<a class="code" href="classRefPtr.html#a2b987fbb75b20a1da1bd959325635e7e">get</a>(); }
<a name="l00109"></a>00109
<a name="l00110"></a><a class="code" href="classLFSCAssume.html#a126a9b3917a465e3684d907195f10824">00110</a> <span class="keywordtype">int</span> <a class="code" href="classLFSCAssume.html#a126a9b3917a465e3684d907195f10824">checkBoolRes</a>( std::vector< int >& clause ){
<a name="l00111"></a>00111 <span class="keywordflow">if</span>( <a class="code" href="classLFSCAssume.html#a9ed812125981b8f0379eaa0b9b3f9ad7">d_type</a>==3 ){
<a name="l00112"></a>00112 <a class="code" href="classLFSCAssume.html#aa3b39dbcb72090c1e629b79c9f247220">d_pf</a>->checkBoolRes( clause );
<a name="l00113"></a>00113 clause.push_back( -<a class="code" href="classLFSCAssume.html#af94fac0616eadaef230e68e417d12f32">d_var</a> );
<a name="l00114"></a>00114 }
<a name="l00115"></a>00115 <span class="keywordflow">return</span> 0;
<a name="l00116"></a>00116 }
<a name="l00117"></a>00117 };
<a name="l00118"></a>00118
<a name="l00119"></a>00119 <span class="preprocessor">#endif</span>
</pre></div></div>
</div>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
