Sophie

Sophie

distrib > Fedora > 15 > i386 > by-pkgid > 583ffa4ba069126c3ba0bc565dc0485a > files > 791

cvc3-doc-2.4.1-1.fc15.noarch.rpm

<!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: cnf.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&#160;<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&#160;Page</span></a></li>
      <li><a href="pages.html"><span>Related&#160;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&#160;List</span></a></li>
      <li><a href="globals.html"><span>File&#160;Members</span></a></li>
    </ul>
  </div>
<div class="header">
  <div class="headertitle">
<div class="title">cnf.h</div>  </div>
</div>
<div class="contents">
<a href="cnf_8h.html">Go to the documentation of this file.</a><div class="fragment"><pre class="fragment"><a name="l00001"></a>00001 <span class="comment">/*****************************************************************************/</span><span class="comment"></span>
<a name="l00002"></a>00002 <span class="comment">/*!</span>
<a name="l00003"></a>00003 <span class="comment"> *\file cnf.h</span>
<a name="l00004"></a>00004 <span class="comment"> *\brief Basic classes for reasoning about formulas in CNF</span>
<a name="l00005"></a>00005 <span class="comment"> *</span>
<a name="l00006"></a>00006 <span class="comment"> * Author: Clark Barrett</span>
<a name="l00007"></a>00007 <span class="comment"> *</span>
<a name="l00008"></a>00008 <span class="comment"> * Created: Mon Dec 12 20:32:33 2005</span>
<a name="l00009"></a>00009 <span class="comment"> *</span>
<a name="l00010"></a>00010 <span class="comment"> * &lt;hr&gt;</span>
<a name="l00011"></a>00011 <span class="comment"> *</span>
<a name="l00012"></a>00012 <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span>
<a name="l00013"></a>00013 <span class="comment"> * and its documentation for any purpose is hereby granted without</span>
<a name="l00014"></a>00014 <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span>
<a name="l00015"></a>00015 <span class="comment"> * LICENSE file provided with this distribution.</span>
<a name="l00016"></a>00016 <span class="comment"> * </span>
<a name="l00017"></a>00017 <span class="comment"> * &lt;hr&gt;</span>
<a name="l00018"></a>00018 <span class="comment"> */</span>
<a name="l00019"></a>00019 <span class="comment">/*****************************************************************************/</span>
<a name="l00020"></a>00020 
<a name="l00021"></a>00021 <span class="preprocessor">#ifndef _cvc3__include__cnf_h_</span>
<a name="l00022"></a>00022 <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__include__cnf_h_</span>
<a name="l00023"></a>00023 <span class="preprocessor"></span>
<a name="l00024"></a>00024 <span class="preprocessor">#include &lt;deque&gt;</span>
<a name="l00025"></a>00025 <span class="preprocessor">#include &quot;<a class="code" href="compat__hash__map_8h.html">compat_hash_map.h</a>&quot;</span>
<a name="l00026"></a>00026 <span class="preprocessor">#include &quot;<a class="code" href="cvc__util_8h.html" title="basic helper utilities">cvc_util.h</a>&quot;</span>
<a name="l00027"></a>00027 <span class="preprocessor">#include &quot;<a class="code" href="cdo_8h.html">cdo.h</a>&quot;</span>
<a name="l00028"></a>00028 <span class="preprocessor">#include &quot;<a class="code" href="cdlist_8h.html">cdlist.h</a>&quot;</span>
<a name="l00029"></a>00029 <span class="preprocessor">#include &quot;<a class="code" href="theorem_8h.html">theorem.h</a>&quot;</span>
<a name="l00030"></a>00030 
<a name="l00031"></a>00031 
<a name="l00032"></a><a class="code" href="namespaceSAT.html">00032</a> <span class="keyword">namespace </span>SAT {
<a name="l00033"></a>00033 
<a name="l00034"></a><a class="code" href="classSAT_1_1Var.html">00034</a> <span class="keyword">class </span><a class="code" href="classSAT_1_1Var.html">Var</a> {
<a name="l00035"></a><a class="code" href="classSAT_1_1Var.html#a01ef74403ce6078716f39185f5f4c0b0">00035</a>   <span class="keywordtype">int</span> <a class="code" href="classSAT_1_1Var.html#a01ef74403ce6078716f39185f5f4c0b0">d_index</a>;
<a name="l00036"></a>00036 <span class="keyword">public</span>:
<a name="l00037"></a><a class="code" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">00037</a>   <span class="keyword">enum</span> <a class="code" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">Val</a> { <a class="code" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5aea98bec3ab0d44524d1ea379c9209b9b1a">UNKNOWN</a> = -1, <a class="code" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5aea008d21718d47e187cbc98a0fcd8fbc03">FALSE_VAL</a>, <a class="code" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5aea9e61954c8499a11875554e5583da88b7">TRUE_VAL</a>};
<a name="l00038"></a>00038   <span class="keyword">static</span> <a class="code" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">Val</a> <a class="code" href="classSAT_1_1Var.html#a6925789c47aff6619853a1f47592fee5">invertValue</a>(<a class="code" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">Val</a>);
<a name="l00039"></a><a class="code" href="classSAT_1_1Var.html#a9f8ea526dd81b86484d019619070b2d3">00039</a>   <a class="code" href="classSAT_1_1Var.html#a9f8ea526dd81b86484d019619070b2d3">Var</a>() : <a class="code" href="classSAT_1_1Var.html#a01ef74403ce6078716f39185f5f4c0b0">d_index</a>(-1) {}
<a name="l00040"></a><a class="code" href="classSAT_1_1Var.html#a3db749176e3431f8c80b7b2ecf97f93b">00040</a>   <a class="code" href="classSAT_1_1Var.html#a3db749176e3431f8c80b7b2ecf97f93b">Var</a>(<span class="keywordtype">int</span> index) :<a class="code" href="classSAT_1_1Var.html#a01ef74403ce6078716f39185f5f4c0b0">d_index</a>(index) {}
<a name="l00041"></a><a class="code" href="classSAT_1_1Var.html#a19796fef4a1ceef4a29540a9c378cdad">00041</a>   <a class="code" href="classSAT_1_1Var.html#a19796fef4a1ceef4a29540a9c378cdad">operator int</a>() { <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1Var.html#a01ef74403ce6078716f39185f5f4c0b0">d_index</a>; }
<a name="l00042"></a><a class="code" href="classSAT_1_1Var.html#a95b8a85adb5fa5eba0fc090c240558b9">00042</a>   <span class="keywordtype">bool</span> <a class="code" href="classSAT_1_1Var.html#a95b8a85adb5fa5eba0fc090c240558b9">isNull</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1Var.html#a01ef74403ce6078716f39185f5f4c0b0">d_index</a> == -1; }
<a name="l00043"></a><a class="code" href="classSAT_1_1Var.html#a625819a54d89e98b26ae423b7a9fe1c8">00043</a>   <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1Var.html#a625819a54d89e98b26ae423b7a9fe1c8">reset</a>() { <a class="code" href="classSAT_1_1Var.html#a01ef74403ce6078716f39185f5f4c0b0">d_index</a> = -1; }
<a name="l00044"></a><a class="code" href="classSAT_1_1Var.html#a736443cd1ae4e1135d83c13bda3cbd80">00044</a>   <span class="keywordtype">int</span> <a class="code" href="classSAT_1_1Var.html#a736443cd1ae4e1135d83c13bda3cbd80">getIndex</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1Var.html#a01ef74403ce6078716f39185f5f4c0b0">d_index</a>; }
<a name="l00045"></a><a class="code" href="classSAT_1_1Var.html#a685cd5d7b11f6ce00074de3e1241c708">00045</a>   <span class="keywordtype">bool</span> <a class="code" href="classSAT_1_1Var.html#a685cd5d7b11f6ce00074de3e1241c708">isVar</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1Var.html#a01ef74403ce6078716f39185f5f4c0b0">d_index</a> &gt; 0; }
<a name="l00046"></a><a class="code" href="classSAT_1_1Var.html#ac66aa57028fd1b9f5271bd6710dac2b4">00046</a>   <span class="keywordtype">bool</span> <a class="code" href="classSAT_1_1Var.html#ac66aa57028fd1b9f5271bd6710dac2b4">operator==</a>(<span class="keyword">const</span> <a class="code" href="classSAT_1_1Var.html">Var</a>&amp; var)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> (<a class="code" href="classSAT_1_1Var.html#a01ef74403ce6078716f39185f5f4c0b0">d_index</a> == var.<a class="code" href="classSAT_1_1Var.html#a01ef74403ce6078716f39185f5f4c0b0">d_index</a>); }
<a name="l00047"></a>00047 };
<a name="l00048"></a><a class="code" href="classSAT_1_1Var.html#a6925789c47aff6619853a1f47592fee5">00048</a> <span class="keyword">inline</span> <a class="code" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">Var::Val</a> <a class="code" href="classSAT_1_1Var.html#a6925789c47aff6619853a1f47592fee5">Var::invertValue</a>(<a class="code" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">Var::Val</a> v)
<a name="l00049"></a>00049 { <span class="keywordflow">return</span> v == <a class="code" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5aea98bec3ab0d44524d1ea379c9209b9b1a">Var::UNKNOWN</a> ? <a class="code" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5aea98bec3ab0d44524d1ea379c9209b9b1a">Var::UNKNOWN</a> : <a class="code" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">Var::Val</a>(1-v); }
<a name="l00050"></a>00050 
<a name="l00051"></a><a class="code" href="classSAT_1_1Lit.html">00051</a> <span class="keyword">class </span><a class="code" href="classSAT_1_1Lit.html">Lit</a> {
<a name="l00052"></a><a class="code" href="classSAT_1_1Lit.html#a91211e315ebefaa64af5111f6dce2ac3">00052</a>   <span class="keywordtype">int</span> <a class="code" href="classSAT_1_1Lit.html#a91211e315ebefaa64af5111f6dce2ac3">d_index</a>;
<a name="l00053"></a><a class="code" href="classSAT_1_1Lit.html#a4ce14efe342a740556003ec1c0d2e006">00053</a>   <span class="keyword">static</span> <a class="code" href="classSAT_1_1Lit.html">Lit</a> <a class="code" href="classSAT_1_1Lit.html#a4ce14efe342a740556003ec1c0d2e006">mkLit</a>(<span class="keywordtype">int</span> index) { <a class="code" href="classSAT_1_1Lit.html">Lit</a> l; l.<a class="code" href="classSAT_1_1Lit.html#a91211e315ebefaa64af5111f6dce2ac3">d_index</a> = index; <span class="keywordflow">return</span> l; }
<a name="l00054"></a>00054 <span class="keyword">public</span>:
<a name="l00055"></a><a class="code" href="classSAT_1_1Lit.html#ad350b64d5c89f8544d0a2f814e93755e">00055</a>   <a class="code" href="classSAT_1_1Lit.html#ad350b64d5c89f8544d0a2f814e93755e">Lit</a>() : <a class="code" href="classSAT_1_1Lit.html#a91211e315ebefaa64af5111f6dce2ac3">d_index</a>(0) {}
<a name="l00056"></a><a class="code" href="classSAT_1_1Lit.html#a5c955a0b510f25a1ec1493f9b559c6e5">00056</a>   <span class="keyword">explicit</span> <a class="code" href="classSAT_1_1Lit.html#a5c955a0b510f25a1ec1493f9b559c6e5">Lit</a>(<a class="code" href="classSAT_1_1Var.html">Var</a> v, <span class="keywordtype">bool</span> positive=<span class="keyword">true</span>) {
<a name="l00057"></a>00057     <span class="keywordflow">if</span> (v.<a class="code" href="classSAT_1_1Var.html#a95b8a85adb5fa5eba0fc090c240558b9">isNull</a>()) <a class="code" href="classSAT_1_1Lit.html#a91211e315ebefaa64af5111f6dce2ac3">d_index</a> = 0;
<a name="l00058"></a>00058     <span class="keywordflow">else</span> <a class="code" href="classSAT_1_1Lit.html#a91211e315ebefaa64af5111f6dce2ac3">d_index</a> = positive ? v+1 : -v-1;
<a name="l00059"></a>00059   }
<a name="l00060"></a><a class="code" href="classSAT_1_1Lit.html#ae639d83f877c976508d280a25c54e12b">00060</a>   <span class="keyword">static</span> <a class="code" href="classSAT_1_1Lit.html">Lit</a> <a class="code" href="classSAT_1_1Lit.html#ae639d83f877c976508d280a25c54e12b">getTrue</a>() { <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1Lit.html#a4ce14efe342a740556003ec1c0d2e006">mkLit</a>(1); }
<a name="l00061"></a><a class="code" href="classSAT_1_1Lit.html#af31c280c018065d2c1232a2cb8503fa7">00061</a>   <span class="keyword">static</span> <a class="code" href="classSAT_1_1Lit.html">Lit</a> <a class="code" href="classSAT_1_1Lit.html#af31c280c018065d2c1232a2cb8503fa7">getFalse</a>() { <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1Lit.html#a4ce14efe342a740556003ec1c0d2e006">mkLit</a>(-1); }
<a name="l00062"></a>00062 
<a name="l00063"></a><a class="code" href="classSAT_1_1Lit.html#ad5f6236c582c95356d720a7401623f36">00063</a>   <span class="keywordtype">bool</span> <a class="code" href="classSAT_1_1Lit.html#ad5f6236c582c95356d720a7401623f36">isNull</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1Lit.html#a91211e315ebefaa64af5111f6dce2ac3">d_index</a> == 0; }
<a name="l00064"></a><a class="code" href="classSAT_1_1Lit.html#ada14f3ca2b88500b5c2500d60e7f554b">00064</a>   <span class="keywordtype">bool</span> <a class="code" href="classSAT_1_1Lit.html#ada14f3ca2b88500b5c2500d60e7f554b">isPositive</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1Lit.html#a91211e315ebefaa64af5111f6dce2ac3">d_index</a> &gt; 1; }
<a name="l00065"></a><a class="code" href="classSAT_1_1Lit.html#ae6fbaf94176fd32347ff14ba3cbc3363">00065</a>   <span class="keywordtype">bool</span> <a class="code" href="classSAT_1_1Lit.html#ae6fbaf94176fd32347ff14ba3cbc3363">isInverted</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1Lit.html#a91211e315ebefaa64af5111f6dce2ac3">d_index</a> &lt; -1; }
<a name="l00066"></a><a class="code" href="classSAT_1_1Lit.html#ab866c8154de88e5285f166f53cdf2d33">00066</a>   <span class="keywordtype">bool</span> <a class="code" href="classSAT_1_1Lit.html#ab866c8154de88e5285f166f53cdf2d33">isFalse</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1Lit.html#a91211e315ebefaa64af5111f6dce2ac3">d_index</a> == -1; }
<a name="l00067"></a><a class="code" href="classSAT_1_1Lit.html#a770e1901858f699490f50e9d2ff1d070">00067</a>   <span class="keywordtype">bool</span> <a class="code" href="classSAT_1_1Lit.html#a770e1901858f699490f50e9d2ff1d070">isTrue</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1Lit.html#a91211e315ebefaa64af5111f6dce2ac3">d_index</a> == 1; }
<a name="l00068"></a><a class="code" href="classSAT_1_1Lit.html#aeb84cef22c7dbf459f95dff9b7cbb4a7">00068</a>   <span class="keywordtype">bool</span> <a class="code" href="classSAT_1_1Lit.html#aeb84cef22c7dbf459f95dff9b7cbb4a7">isVar</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="namespaceCVC3.html#a39fc111339d6dffdc98d6a25b68dff0e">abs</a>(<a class="code" href="classSAT_1_1Lit.html#a91211e315ebefaa64af5111f6dce2ac3">d_index</a>) &gt; 1; }
<a name="l00069"></a><a class="code" href="classSAT_1_1Lit.html#a744e350c39286a2ea093c3c5f1d083a4">00069</a>   <span class="keywordtype">int</span> <a class="code" href="classSAT_1_1Lit.html#a744e350c39286a2ea093c3c5f1d083a4">getID</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1Lit.html#a91211e315ebefaa64af5111f6dce2ac3">d_index</a>; }
<a name="l00070"></a><a class="code" href="classSAT_1_1Lit.html#a57e2e6e37cad9595c3edbea88a41262f">00070</a>   <a class="code" href="classSAT_1_1Var.html">Var</a> <a class="code" href="classSAT_1_1Lit.html#a57e2e6e37cad9595c3edbea88a41262f">getVar</a>()<span class="keyword"> const </span>{
<a name="l00071"></a>00071     <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classSAT_1_1Lit.html#aeb84cef22c7dbf459f95dff9b7cbb4a7">isVar</a>(),<span class="stringliteral">&quot;Bad call to Lit::getVar&quot;</span>);
<a name="l00072"></a>00072     <span class="keywordflow">return</span> <a class="code" href="namespaceCVC3.html#a39fc111339d6dffdc98d6a25b68dff0e">abs</a>(<a class="code" href="classSAT_1_1Lit.html#a91211e315ebefaa64af5111f6dce2ac3">d_index</a>)-1;
<a name="l00073"></a>00073   }
<a name="l00074"></a><a class="code" href="classSAT_1_1Lit.html#a3bb64db99db01facd58c54e48b3f7800">00074</a>   <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1Lit.html#a3bb64db99db01facd58c54e48b3f7800">reset</a>() { <a class="code" href="classSAT_1_1Lit.html#a91211e315ebefaa64af5111f6dce2ac3">d_index</a> = 0; }
<a name="l00075"></a><a class="code" href="classSAT_1_1Lit.html#ae5bf44d7d8e353cd1968ed105ef842cd">00075</a>   <span class="keyword">friend</span> <a class="code" href="classSAT_1_1Lit.html">Lit</a> <a class="code" href="classSAT_1_1Lit.html#ae5bf44d7d8e353cd1968ed105ef842cd">operator!</a>(<span class="keyword">const</span> <a class="code" href="classSAT_1_1Lit.html">Lit</a>&amp; lit) { <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1Lit.html#a4ce14efe342a740556003ec1c0d2e006">mkLit</a>(-lit.<a class="code" href="classSAT_1_1Lit.html#a91211e315ebefaa64af5111f6dce2ac3">d_index</a>); }
<a name="l00076"></a>00076 };
<a name="l00077"></a>00077 
<a name="l00078"></a><a class="code" href="classSAT_1_1Clause.html">00078</a> <span class="keyword">class </span><a class="code" href="classSAT_1_1Clause.html">Clause</a> {
<a name="l00079"></a><a class="code" href="classSAT_1_1Clause.html#a82a2e007da132feab7b6a2322a669b22">00079</a>   <span class="keywordtype">int</span> <a class="code" href="classSAT_1_1Clause.html#a82a2e007da132feab7b6a2322a669b22">d_satisfied</a>:1;
<a name="l00080"></a><a class="code" href="classSAT_1_1Clause.html#a0f0c7bf5e7ed13659de7833887921c98">00080</a>   <span class="keywordtype">int</span> <a class="code" href="classSAT_1_1Clause.html#a0f0c7bf5e7ed13659de7833887921c98">d_unit</a>:1;
<a name="l00081"></a><a class="code" href="classSAT_1_1Clause.html#ae5504b9674dbfbb7c579027805d7bb16">00081</a>   std::vector&lt;Lit&gt; <a class="code" href="classSAT_1_1Clause.html#ae5504b9674dbfbb7c579027805d7bb16">d_lits</a>; 
<a name="l00082"></a><a class="code" href="classSAT_1_1Clause.html#a1f48e48e24f17ae7131c2fe3a1879cd6">00082</a>   <a class="code" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> <a class="code" href="classSAT_1_1Clause.html#a1f48e48e24f17ae7131c2fe3a1879cd6">d_reason</a>; <span class="comment">//the theorem for the clause, used in proofs. by yeting</span>
<a name="l00083"></a>00083 
<a name="l00084"></a>00084  <span class="keyword">public</span>:
<a name="l00085"></a>00085 
<a name="l00086"></a><a class="code" href="classSAT_1_1Clause.html#a50d7f57e0458520fbd90ec157e14b1ab">00086</a>   <a class="code" href="classSAT_1_1Clause.html#a50d7f57e0458520fbd90ec157e14b1ab">Clause</a>(): <a class="code" href="classSAT_1_1Clause.html#a82a2e007da132feab7b6a2322a669b22">d_satisfied</a>(0), <a class="code" href="classSAT_1_1Clause.html#a0f0c7bf5e7ed13659de7833887921c98">d_unit</a>(0) { };
<a name="l00087"></a>00087     
<a name="l00088"></a><a class="code" href="classSAT_1_1Clause.html#abce68afd36de5c1b77d2957671342efc">00088</a>   <a class="code" href="classSAT_1_1Clause.html#a50d7f57e0458520fbd90ec157e14b1ab">Clause</a>(<span class="keyword">const</span> <a class="code" href="classSAT_1_1Clause.html">Clause</a>&amp; clause)
<a name="l00089"></a>00089     : <a class="code" href="classSAT_1_1Clause.html#a82a2e007da132feab7b6a2322a669b22">d_satisfied</a>(clause.<a class="code" href="classSAT_1_1Clause.html#a82a2e007da132feab7b6a2322a669b22">d_satisfied</a>), <a class="code" href="classSAT_1_1Clause.html#a0f0c7bf5e7ed13659de7833887921c98">d_unit</a>(clause.<a class="code" href="classSAT_1_1Clause.html#a0f0c7bf5e7ed13659de7833887921c98">d_unit</a>),
<a name="l00090"></a><a class="code" href="classSAT_1_1Clause.html#af739bca890fe8219a7ebda3beefb0474">00090</a>       <a class="code" href="classSAT_1_1Clause.html#ae5504b9674dbfbb7c579027805d7bb16">d_lits</a>(clause.<a class="code" href="classSAT_1_1Clause.html#ae5504b9674dbfbb7c579027805d7bb16">d_lits</a>), <a class="code" href="classSAT_1_1Clause.html#a1f48e48e24f17ae7131c2fe3a1879cd6">d_reason</a>(clause.<a class="code" href="classSAT_1_1Clause.html#a1f48e48e24f17ae7131c2fe3a1879cd6">d_reason</a>) { };
<a name="l00091"></a>00091 
<a name="l00092"></a>00092   <span class="keyword">typedef</span> std::vector&lt;Lit&gt;::const_iterator <a class="code" href="classSAT_1_1Clause.html#af739bca890fe8219a7ebda3beefb0474">const_iterator</a>;
<a name="l00093"></a><a class="code" href="classSAT_1_1Clause.html#a6d0f568c60e06a1c59c2bf37788ff778">00093</a>   <a class="code" href="classSAT_1_1Clause.html#af739bca890fe8219a7ebda3beefb0474">const_iterator</a> <a class="code" href="classSAT_1_1Clause.html#a6d0f568c60e06a1c59c2bf37788ff778">begin</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1Clause.html#ae5504b9674dbfbb7c579027805d7bb16">d_lits</a>.begin(); }
<a name="l00094"></a><a class="code" href="classSAT_1_1Clause.html#a38094b009b923d08ca9b1a8f517b591e">00094</a>   <a class="code" href="classSAT_1_1Clause.html#af739bca890fe8219a7ebda3beefb0474">const_iterator</a> <a class="code" href="classSAT_1_1Clause.html#a38094b009b923d08ca9b1a8f517b591e">end</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1Clause.html#ae5504b9674dbfbb7c579027805d7bb16">d_lits</a>.end(); }
<a name="l00095"></a>00095 
<a name="l00096"></a><a class="code" href="classSAT_1_1Clause.html#a7c3a264e08e022cd1b7526b62a55302d">00096</a>   <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1Clause.html#a7c3a264e08e022cd1b7526b62a55302d">clear</a>() { <a class="code" href="classSAT_1_1Clause.html#a82a2e007da132feab7b6a2322a669b22">d_satisfied</a> = <a class="code" href="classSAT_1_1Clause.html#a0f0c7bf5e7ed13659de7833887921c98">d_unit</a> = 0; <a class="code" href="classSAT_1_1Clause.html#ae5504b9674dbfbb7c579027805d7bb16">d_lits</a>.clear(); }
<a name="l00097"></a><a class="code" href="classSAT_1_1Clause.html#a3c64729606d93f16b66f58d62ef253d5">00097</a>   <span class="keywordtype">unsigned</span> <a class="code" href="classSAT_1_1Clause.html#a3c64729606d93f16b66f58d62ef253d5">size</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1Clause.html#ae5504b9674dbfbb7c579027805d7bb16">d_lits</a>.size(); }
<a name="l00098"></a><a class="code" href="classSAT_1_1Clause.html#a70345bd3ad10d629dde238b8868dcfd3">00098</a>   <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1Clause.html#a70345bd3ad10d629dde238b8868dcfd3">addLiteral</a>(<a class="code" href="classSAT_1_1Lit.html">Lit</a> l) { <span class="keywordflow">if</span> (!<a class="code" href="classSAT_1_1Clause.html#a82a2e007da132feab7b6a2322a669b22">d_satisfied</a>) <a class="code" href="classSAT_1_1Clause.html#ae5504b9674dbfbb7c579027805d7bb16">d_lits</a>.push_back(l); }
<a name="l00099"></a>00099   <span class="keywordtype">unsigned</span> <a class="code" href="classSAT_1_1Clause.html#a88bfd90868e75a24feffc7f428e30369">getMaxVar</a>() <span class="keyword">const</span>;
<a name="l00100"></a><a class="code" href="classSAT_1_1Clause.html#aa3369b90f9db9e4653be5544117b4ba1">00100</a>   <span class="keywordtype">bool</span> <a class="code" href="classSAT_1_1Clause.html#aa3369b90f9db9e4653be5544117b4ba1">isSatisfied</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1Clause.html#a82a2e007da132feab7b6a2322a669b22">d_satisfied</a> != 0; }
<a name="l00101"></a><a class="code" href="classSAT_1_1Clause.html#abcf5873b0dcc37651c1af59c610a13a9">00101</a>   <span class="keywordtype">bool</span> <a class="code" href="classSAT_1_1Clause.html#abcf5873b0dcc37651c1af59c610a13a9">isUnit</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1Clause.html#a0f0c7bf5e7ed13659de7833887921c98">d_unit</a> != 0; }
<a name="l00102"></a><a class="code" href="classSAT_1_1Clause.html#a2b0467a4d28bbb34316aefd11113c273">00102</a>   <span class="keywordtype">bool</span> <a class="code" href="classSAT_1_1Clause.html#a2b0467a4d28bbb34316aefd11113c273">isNull</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1Clause.html#ae5504b9674dbfbb7c579027805d7bb16">d_lits</a>.size() == 0; }
<a name="l00103"></a><a class="code" href="classSAT_1_1Clause.html#aab7aa74c7b44a33a190fb8f04bc6c6fe">00103</a>   <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1Clause.html#aab7aa74c7b44a33a190fb8f04bc6c6fe">setSatisfied</a>() { <a class="code" href="classSAT_1_1Clause.html#a82a2e007da132feab7b6a2322a669b22">d_satisfied</a> = 1; }
<a name="l00104"></a><a class="code" href="classSAT_1_1Clause.html#a0f3cbc4ee36da4af89d7be70252222d9">00104</a>   <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1Clause.html#a0f3cbc4ee36da4af89d7be70252222d9">setUnit</a>() { <a class="code" href="classSAT_1_1Clause.html#a0f0c7bf5e7ed13659de7833887921c98">d_unit</a> = 1; }
<a name="l00105"></a>00105   <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1Clause.html#ad906b9b541550cffbf95b6ed3c68e6d4">print</a>() <span class="keyword">const</span>;
<a name="l00106"></a><a class="code" href="classSAT_1_1Clause.html#a69be447d7ada144c2a905cf42f4a7a82">00106</a>   <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1Clause.html#a69be447d7ada144c2a905cf42f4a7a82">setClauseTheorem</a>(<a class="code" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> thm){ <a class="code" href="classSAT_1_1Clause.html#a1f48e48e24f17ae7131c2fe3a1879cd6">d_reason</a> = thm;}
<a name="l00107"></a>00107 
<a name="l00108"></a><a class="code" href="classSAT_1_1Clause.html#aa4d692df8aaef4ea4c1c45af006c1301">00108</a>   <a class="code" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> <a class="code" href="classSAT_1_1Clause.html#aa4d692df8aaef4ea4c1c45af006c1301">getClauseTheorem</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1Clause.html#a1f48e48e24f17ae7131c2fe3a1879cd6">d_reason</a>;}
<a name="l00109"></a>00109 };
<a name="l00110"></a>00110 
<a name="l00111"></a>00111 
<a name="l00112"></a><a class="code" href="classSAT_1_1CNF__Formula.html">00112</a> <span class="keyword">class </span><a class="code" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a> {
<a name="l00113"></a>00113 <span class="keyword">protected</span>:
<a name="l00114"></a><a class="code" href="classSAT_1_1CNF__Formula.html#ac638646a5ac87ff246e3d1d7278463f0">00114</a>   <a class="code" href="classSAT_1_1Clause.html">Clause</a>* <a class="code" href="classSAT_1_1CNF__Formula.html#ac638646a5ac87ff246e3d1d7278463f0">d_current</a>;
<a name="l00115"></a>00115 
<a name="l00116"></a>00116   <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1CNF__Formula.html#a2a648614c90bccd3fe0a884749349ef1">setNumVars</a>(<span class="keywordtype">unsigned</span> <a class="code" href="classSAT_1_1CNF__Formula.html#acbdfb5348367dd76a65661dd1ea3599f">numVars</a>) = 0;
<a name="l00117"></a>00117   <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1CNF__Formula.html#a9f9af9ad14a66890d4dbb001aa070dc3">copy</a>(<span class="keyword">const</span> <a class="code" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a>&amp; cnf);
<a name="l00118"></a>00118 
<a name="l00119"></a>00119 <span class="keyword">public</span>:
<a name="l00120"></a><a class="code" href="classSAT_1_1CNF__Formula.html#af57c405a51d608f57626df49ffe825f9">00120</a>   <a class="code" href="classSAT_1_1CNF__Formula.html#af57c405a51d608f57626df49ffe825f9">CNF_Formula</a>() : <a class="code" href="classSAT_1_1CNF__Formula.html#ac638646a5ac87ff246e3d1d7278463f0">d_current</a>(NULL) {}
<a name="l00121"></a><a class="code" href="classSAT_1_1CNF__Formula.html#a3d0f37f512f07883394805a90df9d641">00121</a>   <span class="keyword">virtual</span> <a class="code" href="classSAT_1_1CNF__Formula.html#a3d0f37f512f07883394805a90df9d641">~CNF_Formula</a>() {}
<a name="l00122"></a>00122 
<a name="l00123"></a><a class="code" href="classSAT_1_1CNF__Formula.html#ac247d01a4cc1e5aab84294cb4c00ddbf">00123</a>   <span class="keyword">typedef</span> std::deque&lt;Clause&gt;::const_iterator <a class="code" href="classSAT_1_1CNF__Formula.html#ac247d01a4cc1e5aab84294cb4c00ddbf">const_iterator</a>;
<a name="l00124"></a>00124 
<a name="l00125"></a>00125   <span class="keyword">virtual</span> <span class="keywordtype">bool</span> <a class="code" href="classSAT_1_1CNF__Formula.html#a15e2d3d65a38c23558a0ae8cf35f1938">empty</a>() <span class="keyword">const</span> = 0;
<a name="l00126"></a>00126   <span class="keyword">virtual</span> <span class="keyword">const</span> <a class="code" href="classSAT_1_1Clause.html">Clause</a>&amp; <a class="code" href="classSAT_1_1CNF__Formula.html#a46737d000053162c46af92bf15766642">operator[]</a>(<span class="keywordtype">int</span> i) <span class="keyword">const</span> = 0;
<a name="l00127"></a>00127   <span class="keyword">virtual</span> <a class="code" href="classSAT_1_1CNF__Formula.html#ac247d01a4cc1e5aab84294cb4c00ddbf">const_iterator</a> <a class="code" href="classSAT_1_1CNF__Formula.html#a69dfc94796b23b6913c44a4d6d60f0d8">begin</a>() <span class="keyword">const</span> = 0;
<a name="l00128"></a>00128   <span class="keyword">virtual</span> <a class="code" href="classSAT_1_1CNF__Formula.html#ac247d01a4cc1e5aab84294cb4c00ddbf">const_iterator</a> <a class="code" href="classSAT_1_1CNF__Formula.html#a6631cf3c5a6938f655360f7f63522b79">end</a>() <span class="keyword">const</span> = 0;
<a name="l00129"></a>00129   <span class="keyword">virtual</span> <span class="keywordtype">unsigned</span> <a class="code" href="classSAT_1_1CNF__Formula.html#acbdfb5348367dd76a65661dd1ea3599f">numVars</a>() <span class="keyword">const</span> = 0;
<a name="l00130"></a>00130   <span class="keyword">virtual</span> <span class="keywordtype">unsigned</span> <a class="code" href="classSAT_1_1CNF__Formula.html#a78d99de58d45109256158d55e65bb96f">numClauses</a>() <span class="keyword">const</span> = 0;
<a name="l00131"></a>00131   <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1CNF__Formula.html#ab9f3ffd03469b827138a14392960ba30">newClause</a>() = 0;
<a name="l00132"></a>00132   <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1CNF__Formula.html#a3b0eb426b9713bbc92041f046dd83ab5">registerUnit</a>() = 0;
<a name="l00133"></a>00133 
<a name="l00134"></a><a class="code" href="classSAT_1_1CNF__Formula.html#a4c59929d06b987ed68639f1b85a62606">00134</a>   <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1CNF__Formula.html#a4c59929d06b987ed68639f1b85a62606">addLiteral</a>(<a class="code" href="classSAT_1_1Lit.html">Lit</a> l, <span class="keywordtype">bool</span> invert=<span class="keyword">false</span>)
<a name="l00135"></a>00135     { <span class="keywordflow">if</span> (l.<a class="code" href="classSAT_1_1Lit.html#aeb84cef22c7dbf459f95dff9b7cbb4a7">isVar</a>() &amp;&amp; unsigned(l.<a class="code" href="classSAT_1_1Lit.html#a57e2e6e37cad9595c3edbea88a41262f">getVar</a>()) &gt; <a class="code" href="classSAT_1_1CNF__Formula.html#acbdfb5348367dd76a65661dd1ea3599f">numVars</a>())
<a name="l00136"></a>00136         <a class="code" href="classSAT_1_1CNF__Formula.html#a2a648614c90bccd3fe0a884749349ef1">setNumVars</a>(l.<a class="code" href="classSAT_1_1Lit.html#a57e2e6e37cad9595c3edbea88a41262f">getVar</a>());
<a name="l00137"></a>00137       <a class="code" href="classSAT_1_1CNF__Formula.html#ac638646a5ac87ff246e3d1d7278463f0">d_current</a>-&gt;<a class="code" href="classSAT_1_1Clause.html#a70345bd3ad10d629dde238b8868dcfd3">addLiteral</a>(invert ? !l : l); }
<a name="l00138"></a><a class="code" href="classSAT_1_1CNF__Formula.html#ac7c33df20bc0ac09a831de55bc4773a9">00138</a>   <a class="code" href="classSAT_1_1Clause.html">Clause</a>&amp; <a class="code" href="classSAT_1_1CNF__Formula.html#ac7c33df20bc0ac09a831de55bc4773a9">getCurrentClause</a>() { <span class="keywordflow">return</span> *<a class="code" href="classSAT_1_1CNF__Formula.html#ac638646a5ac87ff246e3d1d7278463f0">d_current</a>; }
<a name="l00139"></a>00139   <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1CNF__Formula.html#a7d85ca3c21713ab64142ecda50bf8476">print</a>() <span class="keyword">const</span>;
<a name="l00140"></a>00140   <span class="keyword">const</span> <a class="code" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a>&amp; <a class="code" href="classSAT_1_1CNF__Formula.html#a77b5e97b49bc46d0eb7928c29a341a98">operator+=</a>(<span class="keyword">const</span> <a class="code" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a>&amp; cnf);
<a name="l00141"></a>00141   <span class="keyword">const</span> <a class="code" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a>&amp; <a class="code" href="classSAT_1_1CNF__Formula.html#a77b5e97b49bc46d0eb7928c29a341a98">operator+=</a>(<span class="keyword">const</span> <a class="code" href="classSAT_1_1Clause.html">Clause</a>&amp; c);
<a name="l00142"></a>00142 };
<a name="l00143"></a>00143 
<a name="l00144"></a>00144 
<a name="l00145"></a><a class="code" href="classSAT_1_1CNF__Formula__Impl.html">00145</a> <span class="keyword">class </span><a class="code" href="classSAT_1_1CNF__Formula__Impl.html">CNF_Formula_Impl</a> :<span class="keyword">public</span> <a class="code" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a> {
<a name="l00146"></a><a class="code" href="classSAT_1_1CNF__Formula__Impl.html#a572e3d2d4333290f5632902ce701d1a5">00146</a>   <a class="code" href="classHash_1_1hash__map.html">std::hash_map&lt;int, bool&gt;</a> <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#a572e3d2d4333290f5632902ce701d1a5">d_lits</a>;
<a name="l00147"></a><a class="code" href="classSAT_1_1CNF__Formula__Impl.html#ac96490e959862063b370e79085e4ab67">00147</a>   std::deque&lt;Clause&gt; <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#ac96490e959862063b370e79085e4ab67">d_formula</a>;
<a name="l00148"></a><a class="code" href="classSAT_1_1CNF__Formula__Impl.html#a64d083ac6c0bbd52edaca213dcf84b0a">00148</a>   <span class="keywordtype">unsigned</span> <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#a64d083ac6c0bbd52edaca213dcf84b0a">d_numVars</a>;
<a name="l00149"></a>00149 <span class="keyword">private</span>:
<a name="l00150"></a><a class="code" href="classSAT_1_1CNF__Formula__Impl.html#a096fb99ab48eb623116c288bc43d7877">00150</a>   <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#a096fb99ab48eb623116c288bc43d7877">setNumVars</a>(<span class="keywordtype">unsigned</span> <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#acf6148ff29fbfa341e58c134dc77fda0">numVars</a>) { <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#a64d083ac6c0bbd52edaca213dcf84b0a">d_numVars</a> = <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#acf6148ff29fbfa341e58c134dc77fda0">numVars</a>; }
<a name="l00151"></a>00151 <span class="keyword">public</span>:
<a name="l00152"></a><a class="code" href="classSAT_1_1CNF__Formula__Impl.html#a4d1ed697fe1e2c50a6442304480b496b">00152</a>   <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#a4d1ed697fe1e2c50a6442304480b496b">CNF_Formula_Impl</a>() : <a class="code" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a>(), <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#a64d083ac6c0bbd52edaca213dcf84b0a">d_numVars</a>(0) {}
<a name="l00153"></a><a class="code" href="classSAT_1_1CNF__Formula__Impl.html#a39b98ba60bf53df6247643de77706ac2">00153</a>   <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#a39b98ba60bf53df6247643de77706ac2">CNF_Formula_Impl</a>(<span class="keyword">const</span> <a class="code" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a>&amp; cnf) : <a class="code" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a>() { <a class="code" href="classSAT_1_1CNF__Formula.html#a9f9af9ad14a66890d4dbb001aa070dc3">copy</a>(cnf); }
<a name="l00154"></a><a class="code" href="classSAT_1_1CNF__Formula__Impl.html#a41f7fb3a1ae1922889e0745f91f56a93">00154</a>   <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#a41f7fb3a1ae1922889e0745f91f56a93">~CNF_Formula_Impl</a>() {};
<a name="l00155"></a>00155 
<a name="l00156"></a><a class="code" href="classSAT_1_1CNF__Formula__Impl.html#a22f2d325345957ac96478fd4aa87fd9c">00156</a>   <span class="keywordtype">bool</span> <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#a22f2d325345957ac96478fd4aa87fd9c">empty</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#ac96490e959862063b370e79085e4ab67">d_formula</a>.empty(); }
<a name="l00157"></a><a class="code" href="classSAT_1_1CNF__Formula__Impl.html#ade695e467e158eb2550683c14f19be34">00157</a>   <span class="keyword">const</span> <a class="code" href="classSAT_1_1Clause.html">Clause</a>&amp; <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#ade695e467e158eb2550683c14f19be34">operator[]</a>(<span class="keywordtype">int</span> i)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#ac96490e959862063b370e79085e4ab67">d_formula</a>[i]; }
<a name="l00158"></a><a class="code" href="classSAT_1_1CNF__Formula__Impl.html#a688bb703f9faac959eed7e9587c13658">00158</a>   <a class="code" href="classSAT_1_1CNF__Formula.html#ac247d01a4cc1e5aab84294cb4c00ddbf">const_iterator</a> <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#a688bb703f9faac959eed7e9587c13658">begin</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#ac96490e959862063b370e79085e4ab67">d_formula</a>.begin(); }
<a name="l00159"></a><a class="code" href="classSAT_1_1CNF__Formula__Impl.html#a91087be2e218a74f381ed2b77e4c79dd">00159</a>   <a class="code" href="classSAT_1_1CNF__Formula.html#ac247d01a4cc1e5aab84294cb4c00ddbf">const_iterator</a> <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#a91087be2e218a74f381ed2b77e4c79dd">end</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#ac96490e959862063b370e79085e4ab67">d_formula</a>.end(); }
<a name="l00160"></a><a class="code" href="classSAT_1_1CNF__Formula__Impl.html#acf6148ff29fbfa341e58c134dc77fda0">00160</a>   <span class="keywordtype">unsigned</span> <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#acf6148ff29fbfa341e58c134dc77fda0">numVars</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#a64d083ac6c0bbd52edaca213dcf84b0a">d_numVars</a>; }
<a name="l00161"></a><a class="code" href="classSAT_1_1CNF__Formula__Impl.html#a136ece8939e5be6f5218705694fa7f14">00161</a>   <span class="keywordtype">unsigned</span> <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#a136ece8939e5be6f5218705694fa7f14">numClauses</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#ac96490e959862063b370e79085e4ab67">d_formula</a>.size(); }
<a name="l00162"></a><a class="code" href="classSAT_1_1CNF__Formula__Impl.html#accfd5e8d24cbb46cef5c4025a92c40eb">00162</a>   <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#accfd5e8d24cbb46cef5c4025a92c40eb">deleteLast</a>() { <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classSAT_1_1CNF__Formula__Impl.html#ac96490e959862063b370e79085e4ab67">d_formula</a>.size() &gt; 0, <span class="stringliteral">&quot;size == 0&quot;</span>); <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#ac96490e959862063b370e79085e4ab67">d_formula</a>.pop_back(); }
<a name="l00163"></a>00163   <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#adffd09ad005d74fdad1be0fc80727767">newClause</a>();
<a name="l00164"></a>00164   <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#ab72a764586f913bc1aa45e0334a75140">registerUnit</a>();
<a name="l00165"></a>00165 
<a name="l00166"></a>00166   <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#ad4e85285d108ed917b748e09c356aa7d">simplify</a>();
<a name="l00167"></a>00167   <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1CNF__Formula__Impl.html#a6bc99606944e873ded2b37c954b18170">reset</a>();
<a name="l00168"></a>00168 };
<a name="l00169"></a>00169 
<a name="l00170"></a>00170 
<a name="l00171"></a><a class="code" href="classSAT_1_1CD__CNF__Formula.html">00171</a> <span class="keyword">class </span><a class="code" href="classSAT_1_1CD__CNF__Formula.html">CD_CNF_Formula</a> :<span class="keyword">public</span> <a class="code" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a> {
<a name="l00172"></a><a class="code" href="classSAT_1_1CD__CNF__Formula.html#ad8b8b293de3947b8dce36a60589a0beb">00172</a>   <a class="code" href="classCVC3_1_1CDList.html">CVC3::CDList&lt;Clause&gt;</a> <a class="code" href="classSAT_1_1CD__CNF__Formula.html#ad8b8b293de3947b8dce36a60589a0beb">d_formula</a>;
<a name="l00173"></a><a class="code" href="classSAT_1_1CD__CNF__Formula.html#ad4d9ce6f94857fe118ea7221912f54c2">00173</a>   <a class="code" href="classCVC3_1_1CDO.html">CVC3::CDO&lt;unsigned&gt;</a> <a class="code" href="classSAT_1_1CD__CNF__Formula.html#ad4d9ce6f94857fe118ea7221912f54c2">d_numVars</a>;
<a name="l00174"></a>00174 <span class="keyword">private</span>:
<a name="l00175"></a><a class="code" href="classSAT_1_1CD__CNF__Formula.html#ae4dbe394f6fd9ef53b6d2b7951c704e3">00175</a>   <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1CD__CNF__Formula.html#ae4dbe394f6fd9ef53b6d2b7951c704e3">setNumVars</a>(<span class="keywordtype">unsigned</span> <a class="code" href="classSAT_1_1CD__CNF__Formula.html#a32f2ac750f25a593d413dc5fa43d6dd2">numVars</a>) { <a class="code" href="classSAT_1_1CD__CNF__Formula.html#ad4d9ce6f94857fe118ea7221912f54c2">d_numVars</a> = <a class="code" href="classSAT_1_1CD__CNF__Formula.html#a32f2ac750f25a593d413dc5fa43d6dd2">numVars</a>; }
<a name="l00176"></a>00176 <span class="keyword">public</span>:
<a name="l00177"></a><a class="code" href="classSAT_1_1CD__CNF__Formula.html#a5ed0499393400456a1da983d79fee59d">00177</a>   <a class="code" href="classSAT_1_1CD__CNF__Formula.html#a5ed0499393400456a1da983d79fee59d">CD_CNF_Formula</a>(<a class="code" href="classCVC3_1_1Context.html">CVC3::Context</a>* context)
<a name="l00178"></a>00178     : <a class="code" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a>(), <a class="code" href="classSAT_1_1CD__CNF__Formula.html#ad8b8b293de3947b8dce36a60589a0beb">d_formula</a>(context), <a class="code" href="classSAT_1_1CD__CNF__Formula.html#ad4d9ce6f94857fe118ea7221912f54c2">d_numVars</a>(context, 0, 0) {}
<a name="l00179"></a><a class="code" href="classSAT_1_1CD__CNF__Formula.html#a481478397e9a56a75f9ab1db76dcee42">00179</a>   <a class="code" href="classSAT_1_1CD__CNF__Formula.html#a481478397e9a56a75f9ab1db76dcee42">~CD_CNF_Formula</a>() {}
<a name="l00180"></a>00180 
<a name="l00181"></a><a class="code" href="classSAT_1_1CD__CNF__Formula.html#a3773c2c9cbbe24234b6f4c85a48d9e01">00181</a>   <span class="keywordtype">bool</span> <a class="code" href="classSAT_1_1CD__CNF__Formula.html#a3773c2c9cbbe24234b6f4c85a48d9e01">empty</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1CD__CNF__Formula.html#ad8b8b293de3947b8dce36a60589a0beb">d_formula</a>.<a class="code" href="classCVC3_1_1CDList.html#afafb842f23a41289eb104404e5eb94bf">empty</a>(); }
<a name="l00182"></a><a class="code" href="classSAT_1_1CD__CNF__Formula.html#aab7165cf79dc81e322c6988e972d6bc1">00182</a>   <span class="keyword">const</span> <a class="code" href="classSAT_1_1Clause.html">Clause</a>&amp; <a class="code" href="classSAT_1_1CD__CNF__Formula.html#aab7165cf79dc81e322c6988e972d6bc1">operator[]</a>(<span class="keywordtype">int</span> i)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1CD__CNF__Formula.html#ad8b8b293de3947b8dce36a60589a0beb">d_formula</a>[i]; }
<a name="l00183"></a><a class="code" href="classSAT_1_1CD__CNF__Formula.html#a4022c7fcf4f27acd242be18f4a1f0c6a">00183</a>   <a class="code" href="classSAT_1_1CNF__Formula.html#ac247d01a4cc1e5aab84294cb4c00ddbf">const_iterator</a> <a class="code" href="classSAT_1_1CD__CNF__Formula.html#a4022c7fcf4f27acd242be18f4a1f0c6a">begin</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1CD__CNF__Formula.html#ad8b8b293de3947b8dce36a60589a0beb">d_formula</a>.<a class="code" href="classCVC3_1_1CDList.html#ae2cf006604b1ab88139332a5e2c08568">begin</a>(); }
<a name="l00184"></a><a class="code" href="classSAT_1_1CD__CNF__Formula.html#aa11182c6a4126ca808ea88e4255a7f80">00184</a>   <a class="code" href="classSAT_1_1CNF__Formula.html#ac247d01a4cc1e5aab84294cb4c00ddbf">const_iterator</a> <a class="code" href="classSAT_1_1CD__CNF__Formula.html#aa11182c6a4126ca808ea88e4255a7f80">end</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1CD__CNF__Formula.html#ad8b8b293de3947b8dce36a60589a0beb">d_formula</a>.<a class="code" href="classCVC3_1_1CDList.html#a96313ff2924c89a93d7fe6c618c837af">end</a>(); }
<a name="l00185"></a><a class="code" href="classSAT_1_1CD__CNF__Formula.html#a32f2ac750f25a593d413dc5fa43d6dd2">00185</a>   <span class="keywordtype">unsigned</span> <a class="code" href="classSAT_1_1CD__CNF__Formula.html#a32f2ac750f25a593d413dc5fa43d6dd2">numVars</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1CD__CNF__Formula.html#ad4d9ce6f94857fe118ea7221912f54c2">d_numVars</a>.<a class="code" href="classCVC3_1_1CDO.html#a818fcacc7b30b0f05347335ab125626c">get</a>(); }
<a name="l00186"></a><a class="code" href="classSAT_1_1CD__CNF__Formula.html#a40948c1f2c702dfe58e4b63776ec18fd">00186</a>   <span class="keywordtype">unsigned</span> <a class="code" href="classSAT_1_1CD__CNF__Formula.html#a40948c1f2c702dfe58e4b63776ec18fd">numClauses</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1CD__CNF__Formula.html#ad8b8b293de3947b8dce36a60589a0beb">d_formula</a>.<a class="code" href="classCVC3_1_1CDList.html#adf92d0f391d73e7ac70da57db135af27">size</a>(); }
<a name="l00187"></a><a class="code" href="classSAT_1_1CD__CNF__Formula.html#a4eb2135609863c3a5e28383e279ec5a8">00187</a>   <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1CD__CNF__Formula.html#a4eb2135609863c3a5e28383e279ec5a8">deleteLast</a>() { <a class="code" href="classSAT_1_1CD__CNF__Formula.html#ad8b8b293de3947b8dce36a60589a0beb">d_formula</a>.<a class="code" href="classCVC3_1_1CDList.html#a49d135664e22701bc537fd799f82c740">pop_back</a>(); }
<a name="l00188"></a>00188 
<a name="l00189"></a>00189   <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1CD__CNF__Formula.html#a9ef7d443b6dddb0f23fd07e81a60970c">newClause</a>();
<a name="l00190"></a>00190   <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1CD__CNF__Formula.html#a41c4e53bdf4c9d98afbdbea4a735fce9">registerUnit</a>();
<a name="l00191"></a>00191 };
<a name="l00192"></a>00192 
<a name="l00193"></a>00193 }
<a name="l00194"></a>00194 
<a name="l00195"></a>00195 <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&#160;
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>

Perl :: Catalyst :: PostgreSQL :: RPM Valid HTML 4.01 Transitional