<!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: MiniSat Namespace Reference</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li class="current"><a href="namespaces.html"><span>Namespaces</span></a></li>
<li><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="namespaces.html"><span>Namespace List</span></a></li>
<li><a href="namespacemembers.html"><span>Namespace Members</span></a></li>
</ul>
</div>
</div>
<div class="header">
<div class="summary">
<a href="#nested-classes">Classes</a> |
<a href="#typedef-members">Typedefs</a> |
<a href="#func-members">Functions</a> |
<a href="#var-members">Variables</a> </div>
<div class="headertitle">
<div class="title">MiniSat Namespace Reference</div> </div>
</div>
<div class="contents">
<h2><a name="nested-classes"></a>
Classes</h2>
<ul>
<li>class <a class="el" href="classMiniSat_1_1Inference.html">Inference</a>
<li>class <a class="el" href="classMiniSat_1_1Derivation.html">Derivation</a>
<li>struct <a class="el" href="structMiniSat_1_1STATIC__ASSERTION__FAILURE_3_01true_01_4.html">STATIC_ASSERTION_FAILURE< true ></a>
<li>class <a class="el" href="classMiniSat_1_1vec.html">vec</a>
<li>class <a class="el" href="classMiniSat_1_1lbool.html">lbool</a>
<li>class <a class="el" href="classMiniSat_1_1Heap.html">Heap</a>
<li>struct <a class="el" href="structMiniSat_1_1SolverStats.html">SolverStats</a>
<li>struct <a class="el" href="structMiniSat_1_1PushEntry.html">PushEntry</a>
<li>struct <a class="el" href="structMiniSat_1_1SearchParams.html">SearchParams</a>
<li>class <a class="el" href="classMiniSat_1_1Solver.html">Solver</a>
<li>class <a class="el" href="classMiniSat_1_1Lit.html">Lit</a>
<li>class <a class="el" href="classMiniSat_1_1Clause.html">Clause</a>
<li>struct <a class="el" href="structMiniSat_1_1VarOrder__lt.html">VarOrder_lt</a>
<li>class <a class="el" href="classMiniSat_1_1VarOrder.html">VarOrder</a>
</ul>
<h2><a name="typedef-members"></a>
Typedefs</h2>
<ul>
<li>typedef std::vector< int ><br class="typebreak"/>
::<a class="el" href="namespaceMiniSat.html#ad579041894c169fecdeb319f9aa5948d">size_type</a> <a class="el" href="namespaceMiniSat.html#ad579041894c169fecdeb319f9aa5948d">size_type</a>
<li>typedef int <a class="el" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a>
</ul>
<h2><a name="func-members"></a>
Functions</h2>
<ul>
<li>template<class T > static T <a class="el" href="namespaceMiniSat.html#a74c8343998008d4d992e491ec26d4d6a">min</a> (T x, T y)
<li>template<class T > static T <a class="el" href="namespaceMiniSat.html#aa07ebe3ac704ce3a2a931d5dc9d69b7a">max</a> (T x, T y)
<li>template<class T > static T * <a class="el" href="namespaceMiniSat.html#a7fffcd2c39ed50869273b98b2b19ca62">xmalloc</a> (size_t size)
<li>template<class T > static T * <a class="el" href="namespaceMiniSat.html#a82898b8da41c4146ecc083d3282450ba">xrealloc</a> (T *ptr, size_t size)
<li>template<class T > static void <a class="el" href="namespaceMiniSat.html#acbe7b3fac8ab3909327207b0fea1f4d8">xfree</a> (T *ptr)
<li>static double <a class="el" href="namespaceMiniSat.html#a24abdfa24bc8d99b5f25d3cd38adaa78">drand</a> (double &seed)
<li>static int <a class="el" href="namespaceMiniSat.html#a8ecdd514fb182dd7adadecd941f1be3b">irand</a> (double &seed, int size)
<li>int <a class="el" href="namespaceMiniSat.html#a4c585f2e8db13de83607a0d22761e91d">toInt</a> (<a class="el" href="classMiniSat_1_1lbool.html">lbool</a> l)
<li><a class="el" href="classMiniSat_1_1lbool.html">lbool</a> <a class="el" href="namespaceMiniSat.html#a1c28cb1733880d6dbc7aff894cb5527d">toLbool</a> (int v)
<li>template<class T > static bool <a class="el" href="namespaceMiniSat.html#adb0b165c3f6a6450e7fdcf8464b3c705">operator!=</a> (const T &x, const T &y)
<li>template<class T > static bool <a class="el" href="namespaceMiniSat.html#a8fdfa7da7da034221d598afabb5fbdab">operator></a> (const T &x, const T &y)
<li>template<class T > static bool <a class="el" href="namespaceMiniSat.html#a001a9e91f802a7d6f2bc0cce0585d52e">operator<=</a> (const T &x, const T &y)
<li>template<class T > static bool <a class="el" href="namespaceMiniSat.html#a875d1ff175c5ffbfafd097b7c550dd0d">operator>=</a> (const T &x, const T &y)
<li>static int <a class="el" href="namespaceMiniSat.html#ad93cb56673487974071ed3b75bf4ea83">left</a> (int i)
<li>static int <a class="el" href="namespaceMiniSat.html#a82558b7a36c52f5d3211d5d14bed99d4">right</a> (int i)
<li>static int <a class="el" href="namespaceMiniSat.html#a1e31c3827dae4bdfeeb6430c5c0f48b4">parent</a> (int i)
<li><a class="el" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> <a class="el" href="namespaceMiniSat.html#a6d37e2f7d3903e1a85baf8f1e83eff78">cvcToMiniSat</a> (const <a class="el" href="classSAT_1_1Var.html">SAT::Var</a> &var)
<li><a class="el" href="classSAT_1_1Var.html">SAT::Var</a> <a class="el" href="namespaceMiniSat.html#a72756c106b9bd53cf77c2aab214e7cf5">miniSatToCVC</a> (<a class="el" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> var)
<li><a class="el" href="classMiniSat_1_1Lit.html">Lit</a> <a class="el" href="namespaceMiniSat.html#a0eb766a18a8ba93182ee46d85a40c282">cvcToMiniSat</a> (const <a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> &literal)
<li><a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> <a class="el" href="namespaceMiniSat.html#a30ac392b840d0ee1aa3877dadebff3fd">miniSatToCVC</a> (<a class="el" href="classMiniSat_1_1Lit.html">Lit</a> literal)
<li>bool <a class="el" href="namespaceMiniSat.html#ace6b835dfa37172fd8e8177fa6373c4b">cvcToMiniSat</a> (const <a class="el" href="classSAT_1_1Clause.html">SAT::Clause</a> &clause, std::vector< <a class="el" href="classMiniSat_1_1Lit.html">Lit</a> > &literals)
<li>void * <a class="el" href="namespaceMiniSat.html#ab76c348e2f4f918b5117b8850462b0e0">malloc_clause</a> (const vector< <a class="el" href="classMiniSat_1_1Lit.html">Lit</a> > &ps)
<li><a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * <a class="el" href="namespaceMiniSat.html#a9a3ff2cc55978ca3a973861cad2814e2">Clause_new</a> (const vector< <a class="el" href="classMiniSat_1_1Lit.html">Lit</a> > &ps, <a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> theorem, int id)
<li><a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * <a class="el" href="namespaceMiniSat.html#a2659fd436dc00aebee015ce18ae2c89a">Lemma_new</a> (const vector< <a class="el" href="classMiniSat_1_1Lit.html">Lit</a> > &ps, int id, int pushID)
<li>const <a class="el" href="classMiniSat_1_1Lit.html">Lit</a> <a class="el" href="namespaceMiniSat.html#a120ea2f17b58215d657cd7b005edcd85">lit_Undef</a> (<a class="el" href="namespaceMiniSat.html#af0b81724f9c7f24ed9a52a4627b5db86">var_Undef</a>, false)
<li>const <a class="el" href="classMiniSat_1_1Lit.html">Lit</a> <a class="el" href="namespaceMiniSat.html#ad1ccf328f5909693679e1c703981b434">lit_Error</a> (<a class="el" href="namespaceMiniSat.html#af0b81724f9c7f24ed9a52a4627b5db86">var_Undef</a>, true)
</ul>
<h2><a name="var-members"></a>
Variables</h2>
<ul>
<li>const <a class="el" href="classMiniSat_1_1lbool.html">lbool</a> <a class="el" href="namespaceMiniSat.html#ad0b6e52186f3374f569c4de9db621be1">l_True</a> = toLbool( 1)
<li>const <a class="el" href="classMiniSat_1_1lbool.html">lbool</a> <a class="el" href="namespaceMiniSat.html#a810166165364a8a8262d24b13d7b1da9">l_False</a> = toLbool(-1)
<li>const <a class="el" href="classMiniSat_1_1lbool.html">lbool</a> <a class="el" href="namespaceMiniSat.html#aa6f5310857da28f01311aebd650a531f">l_Undef</a> = toLbool( 0)
<li>const int <a class="el" href="namespaceMiniSat.html#a633ea02a1812110095e4f982ff342b92">clause_mem_base</a>
<li>const int <a class="el" href="namespaceMiniSat.html#af0b81724f9c7f24ed9a52a4627b5db86">var_Undef</a> = -1
</ul>
<hr/><h2>Typedef Documentation</h2>
<a class="anchor" id="ad579041894c169fecdeb319f9aa5948d"></a><!-- doxytag: member="MiniSat::size_type" ref="ad579041894c169fecdeb319f9aa5948d" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">typedef std::vector<int>::<a class="el" href="namespaceMiniSat.html#ad579041894c169fecdeb319f9aa5948d">size_type</a> <a class="el" href="namespaceMiniSat.html#ad579041894c169fecdeb319f9aa5948d">MiniSat::size_type</a></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00110">110</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
</div>
</div>
<a class="anchor" id="a0d9722420b2afd308dceda22c1b05a5e"></a><!-- doxytag: member="MiniSat::Var" ref="a0d9722420b2afd308dceda22c1b05a5e" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">typedef int <a class="el" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">MiniSat::Var</a></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__types_8h_source.html#l00055">55</a> of file <a class="el" href="minisat__types_8h_source.html">minisat_types.h</a>.</p>
</div>
</div>
<hr/><h2>Function Documentation</h2>
<a class="anchor" id="a74c8343998008d4d992e491ec26d4d6a"></a><!-- doxytag: member="MiniSat::min" ref="a74c8343998008d4d992e491ec26d4d6a" args="(T x, T y)" -->
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class T > </div>
<table class="memname">
<tr>
<td class="memname">static T MiniSat::min </td>
<td>(</td>
<td class="paramtype">T </td>
<td class="paramname"><em>x</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">T </td>
<td class="paramname"><em>y</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [inline, static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__global_8h_source.html#l00058">58</a> of file <a class="el" href="minisat__global_8h_source.html">minisat_global.h</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l00563">CVC3::TheoryArithOld::pickIntEqMonomial()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00388">CVC3::TheoryArithNew::pickIntEqMonomial()</a>, and <a class="el" href="theory__arith3_8cpp_source.html#l00590">CVC3::TheoryArith3::pickIntEqMonomial()</a>.</p>
</div>
</div>
<a class="anchor" id="aa07ebe3ac704ce3a2a931d5dc9d69b7a"></a><!-- doxytag: member="MiniSat::max" ref="aa07ebe3ac704ce3a2a931d5dc9d69b7a" args="(T x, T y)" -->
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class T > </div>
<table class="memname">
<tr>
<td class="memname">static T MiniSat::max </td>
<td>(</td>
<td class="paramtype">T </td>
<td class="paramname"><em>x</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">T </td>
<td class="paramname"><em>y</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [inline, static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__global_8h_source.html#l00059">59</a> of file <a class="el" href="minisat__global_8h_source.html">minisat_global.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01091">MiniSat::Solver::analyze()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01278">MiniSat::Solver::analyze_minimize()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01473">MiniSat::Solver::assume()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00750">MiniSat::Solver::insertClause()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02496">MiniSat::Solver::setPushID()</a>.</p>
</div>
</div>
<a class="anchor" id="a7fffcd2c39ed50869273b98b2b19ca62"></a><!-- doxytag: member="MiniSat::xmalloc" ref="a7fffcd2c39ed50869273b98b2b19ca62" args="(size_t size)" -->
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class T > </div>
<table class="memname">
<tr>
<td class="memname">static T* MiniSat::xmalloc </td>
<td>(</td>
<td class="paramtype">size_t </td>
<td class="paramname"><em>size</em></td><td>)</td>
<td><code> [inline, static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__global_8h_source.html#l00070">70</a> of file <a class="el" href="minisat__global_8h_source.html">minisat_global.h</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>.</p>
</div>
</div>
<a class="anchor" id="a82898b8da41c4146ecc083d3282450ba"></a><!-- doxytag: member="MiniSat::xrealloc" ref="a82898b8da41c4146ecc083d3282450ba" args="(T *ptr, size_t size)" -->
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class T > </div>
<table class="memname">
<tr>
<td class="memname">static T* MiniSat::xrealloc </td>
<td>(</td>
<td class="paramtype">T * </td>
<td class="paramname"><em>ptr</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">size_t </td>
<td class="paramname"><em>size</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [inline, static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__global_8h_source.html#l00075">75</a> of file <a class="el" href="minisat__global_8h_source.html">minisat_global.h</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>.</p>
<p>Referenced by <a class="el" href="minisat__global_8h_source.html#l00163">MiniSat::vec< T >::grow()</a>.</p>
</div>
</div>
<a class="anchor" id="acbe7b3fac8ab3909327207b0fea1f4d8"></a><!-- doxytag: member="MiniSat::xfree" ref="acbe7b3fac8ab3909327207b0fea1f4d8" args="(T *ptr)" -->
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class T > </div>
<table class="memname">
<tr>
<td class="memname">static void MiniSat::xfree </td>
<td>(</td>
<td class="paramtype">T * </td>
<td class="paramname"><em>ptr</em></td><td>)</td>
<td><code> [inline, static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__global_8h_source.html#l00080">80</a> of file <a class="el" href="minisat__global_8h_source.html">minisat_global.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01481">MiniSat::Solver::backtrack()</a>, <a class="el" href="minisat__global_8h_source.html#l00184">MiniSat::vec< T >::clear()</a>, <a class="el" href="minisat__derivation_8cpp_source.html#l00406">MiniSat::Derivation::pop()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00869">MiniSat::Solver::remove()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00999">MiniSat::Solver::resolveTheoryImplication()</a>, <a class="el" href="minisat__derivation_8cpp_source.html#l00044">MiniSat::Derivation::~Derivation()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00292">MiniSat::Solver::~Solver()</a>.</p>
</div>
</div>
<a class="anchor" id="a24abdfa24bc8d99b5f25d3cd38adaa78"></a><!-- doxytag: member="MiniSat::drand" ref="a24abdfa24bc8d99b5f25d3cd38adaa78" args="(double &seed)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">static double MiniSat::drand </td>
<td>(</td>
<td class="paramtype">double & </td>
<td class="paramname"><em>seed</em></td><td>)</td>
<td><code> [inline, static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__global_8h_source.html#l00089">89</a> of file <a class="el" href="minisat__global_8h_source.html">minisat_global.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__global_8h_source.html#l00096">irand()</a>.</p>
</div>
</div>
<a class="anchor" id="a8ecdd514fb182dd7adadecd941f1be3b"></a><!-- doxytag: member="MiniSat::irand" ref="a8ecdd514fb182dd7adadecd941f1be3b" args="(double &seed, int size)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">static int MiniSat::irand </td>
<td>(</td>
<td class="paramtype">double & </td>
<td class="paramname"><em>seed</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>size</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [inline, static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__global_8h_source.html#l00096">96</a> of file <a class="el" href="minisat__global_8h_source.html">minisat_global.h</a>.</p>
<p>References <a class="el" href="minisat__global_8h_source.html#l00089">drand()</a>.</p>
</div>
</div>
<a class="anchor" id="a4c585f2e8db13de83607a0d22761e91d"></a><!-- doxytag: member="MiniSat::toInt" ref="a4c585f2e8db13de83607a0d22761e91d" args="(lbool l)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int MiniSat::toInt </td>
<td>(</td>
<td class="paramtype">lbool </td>
<td class="paramname"><em>l</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__global_8h_source.html#l00211">211</a> of file <a class="el" href="minisat__global_8h_source.html">minisat_global.h</a>.</p>
<p>References <a class="el" href="minisat__global_8h_source.html#l00202">MiniSat::lbool::toInt()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01481">MiniSat::Solver::backtrack()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02446">MiniSat::Solver::checkTrail()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01575">MiniSat::Solver::enqueue()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02668">MiniSat::Solver::pop()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01950">MiniSat::Solver::propLookahead()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00457">MiniSat::Solver::registerVar()</a>.</p>
</div>
</div>
<a class="anchor" id="a1c28cb1733880d6dbc7aff894cb5527d"></a><!-- doxytag: member="MiniSat::toLbool" ref="a1c28cb1733880d6dbc7aff894cb5527d" args="(int v)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classMiniSat_1_1lbool.html">lbool</a> MiniSat::toLbool </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>v</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__global_8h_source.html#l00212">212</a> of file <a class="el" href="minisat__global_8h_source.html">minisat_global.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8h_source.html#l00699">MiniSat::Solver::getValue()</a>, and <a class="el" href="minisat__varorder_8h_source.html#l00104">MiniSat::VarOrder::select()</a>.</p>
</div>
</div>
<a class="anchor" id="adb0b165c3f6a6450e7fdcf8464b3c705"></a><!-- doxytag: member="MiniSat::operator!=" ref="adb0b165c3f6a6450e7fdcf8464b3c705" args="(const T &x, const T &y)" -->
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class T > </div>
<table class="memname">
<tr>
<td class="memname">static bool MiniSat::operator!= </td>
<td>(</td>
<td class="paramtype">const T & </td>
<td class="paramname"><em>x</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const T & </td>
<td class="paramname"><em>y</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [inline, static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__global_8h_source.html#l00225">225</a> of file <a class="el" href="minisat__global_8h_source.html">minisat_global.h</a>.</p>
</div>
</div>
<a class="anchor" id="a8fdfa7da7da034221d598afabb5fbdab"></a><!-- doxytag: member="MiniSat::operator>" ref="a8fdfa7da7da034221d598afabb5fbdab" args="(const T &x, const T &y)" -->
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class T > </div>
<table class="memname">
<tr>
<td class="memname">static bool MiniSat::operator> </td>
<td>(</td>
<td class="paramtype">const T & </td>
<td class="paramname"><em>x</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const T & </td>
<td class="paramname"><em>y</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [inline, static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__global_8h_source.html#l00226">226</a> of file <a class="el" href="minisat__global_8h_source.html">minisat_global.h</a>.</p>
</div>
</div>
<a class="anchor" id="a001a9e91f802a7d6f2bc0cce0585d52e"></a><!-- doxytag: member="MiniSat::operator<=" ref="a001a9e91f802a7d6f2bc0cce0585d52e" args="(const T &x, const T &y)" -->
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class T > </div>
<table class="memname">
<tr>
<td class="memname">static bool MiniSat::operator<= </td>
<td>(</td>
<td class="paramtype">const T & </td>
<td class="paramname"><em>x</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const T & </td>
<td class="paramname"><em>y</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [inline, static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__global_8h_source.html#l00227">227</a> of file <a class="el" href="minisat__global_8h_source.html">minisat_global.h</a>.</p>
</div>
</div>
<a class="anchor" id="a875d1ff175c5ffbfafd097b7c550dd0d"></a><!-- doxytag: member="MiniSat::operator>=" ref="a875d1ff175c5ffbfafd097b7c550dd0d" args="(const T &x, const T &y)" -->
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class T > </div>
<table class="memname">
<tr>
<td class="memname">static bool MiniSat::operator>= </td>
<td>(</td>
<td class="paramtype">const T & </td>
<td class="paramname"><em>x</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const T & </td>
<td class="paramname"><em>y</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [inline, static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__global_8h_source.html#l00228">228</a> of file <a class="el" href="minisat__global_8h_source.html">minisat_global.h</a>.</p>
</div>
</div>
<a class="anchor" id="ad93cb56673487974071ed3b75bf4ea83"></a><!-- doxytag: member="MiniSat::left" ref="ad93cb56673487974071ed3b75bf4ea83" args="(int i)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">static int MiniSat::left </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em></td><td>)</td>
<td><code> [inline, static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__heap_8h_source.html#l00053">53</a> of file <a class="el" href="minisat__heap_8h_source.html">minisat_heap.h</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l01861">CVC3::CompleteInstPreProcessor::collect_forall_index()</a>, <a class="el" href="minisat__derivation_8cpp_source.html#l00260">MiniSat::Derivation::createProof()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00432">CVC3::TheoryArith3::doSolve()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l02780">CVC3::TheoryArithOld::findBounds()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l01348">CVC3::TheoryArithNew::findBounds()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02197">CVC3::TheoryArith3::findBounds()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l03043">CVC3::TheoryArithNew::findCoefficient()</a>, <a class="el" href="minisat__heap_8h_source.html#l00130">MiniSat::Heap< VarOrder_lt >::heapProperty()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02297">CVC3::ArithTheoremProducerOld::intVarEqnConst()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02095">CVC3::ArithTheoremProducer3::intVarEqnConst()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02138">CVC3::ArithTheoremProducer::intVarEqnConst()</a>, <a class="el" href="theory__quant_8cpp_source.html#l02103">CVC3::CompleteInstPreProcessor::isGoodQuant()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01373">CVC3::CompleteInstPreProcessor::isMacro()</a>, <a class="el" href="minisat__heap_8h_source.html#l00076">MiniSat::Heap< VarOrder_lt >::percolateDown()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l01430">CVC3::ArithTheoremProducerOld::plusPredicate()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01362">CVC3::ArithTheoremProducer3::plusPredicate()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01376">CVC3::ArithTheoremProducer::plusPredicate()</a>, <a class="el" href="main_8cpp_source.html#l00217">printUsage()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00615">CVC3::TheoryArithOld::processRealEq()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00420">CVC3::TheoryArithNew::processRealEq()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00642">CVC3::TheoryArith3::processRealEq()</a>, <a class="el" href="theory__array_8cpp_source.html#l00368">CVC3::TheoryArray::rewrite()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03076">CVC3::TheoryArithOld::rewrite()</a>, <a class="el" href="array__theorem__producer_8cpp_source.html#l00122">CVC3::ArrayTheoremProducer::rewriteWriteWrite()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l03524">CVC3::TheoryArithNew::substAndCanonizeTableaux()</a>, and <a class="el" href="cnf__manager_8cpp_source.html#l00147">SAT::CNF_Manager::translateExprRec()</a>.</p>
</div>
</div>
<a class="anchor" id="a82558b7a36c52f5d3211d5d14bed99d4"></a><!-- doxytag: member="MiniSat::right" ref="a82558b7a36c52f5d3211d5d14bed99d4" args="(int i)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">static int MiniSat::right </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em></td><td>)</td>
<td><code> [inline, static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__heap_8h_source.html#l00054">54</a> of file <a class="el" href="minisat__heap_8h_source.html">minisat_heap.h</a>.</p>
<p>Referenced by <a class="el" href="vcl_8cpp_source.html#l01113">CVC3::VCL::andExpr()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01861">CVC3::CompleteInstPreProcessor::collect_forall_index()</a>, <a class="el" href="minisat__derivation_8cpp_source.html#l00260">MiniSat::Derivation::createProof()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00447">CVC3::TheoryArithOld::doSolve()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00331">CVC3::TheoryArithNew::doSolve()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00432">CVC3::TheoryArith3::doSolve()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l02780">CVC3::TheoryArithOld::findBounds()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l01348">CVC3::TheoryArithNew::findBounds()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02197">CVC3::TheoryArith3::findBounds()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l03043">CVC3::TheoryArithNew::findCoefficient()</a>, <a class="el" href="minisat__heap_8h_source.html#l00130">MiniSat::Heap< VarOrder_lt >::heapProperty()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02297">CVC3::ArithTheoremProducerOld::intVarEqnConst()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02095">CVC3::ArithTheoremProducer3::intVarEqnConst()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02138">CVC3::ArithTheoremProducer::intVarEqnConst()</a>, <a class="el" href="theory__quant_8cpp_source.html#l02103">CVC3::CompleteInstPreProcessor::isGoodQuant()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01373">CVC3::CompleteInstPreProcessor::isMacro()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l01499">CVC3::TheoryArithOld::isolateVariable()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l01150">CVC3::TheoryArith3::isolateVariable()</a>, <a class="el" href="vcl_8cpp_source.html#l01333">CVC3::VCL::minusExpr()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l00911">CVC3::ArithTheoremProducerOld::moveSumConstantRight()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l00861">CVC3::ArithTheoremProducer3::moveSumConstantRight()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02773">CVC3::ArithTheoremProducer::moveSumConstantRight()</a>, <a class="el" href="vcl_8cpp_source.html#l01339">CVC3::VCL::multExpr()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l01822">CVC3::TheoryArithOld::normalizeProjectIneqs()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l01449">CVC3::TheoryArith3::normalizeProjectIneqs()</a>, <a class="el" href="vcl_8cpp_source.html#l01127">CVC3::VCL::orExpr()</a>, <a class="el" href="minisat__heap_8h_source.html#l00076">MiniSat::Heap< VarOrder_lt >::percolateDown()</a>, <a class="el" href="vcl_8cpp_source.html#l01322">CVC3::VCL::plusExpr()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l01430">CVC3::ArithTheoremProducerOld::plusPredicate()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01362">CVC3::ArithTheoremProducer3::plusPredicate()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01376">CVC3::ArithTheoremProducer::plusPredicate()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00615">CVC3::TheoryArithOld::processRealEq()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00420">CVC3::TheoryArithNew::processRealEq()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00642">CVC3::TheoryArith3::processRealEq()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00739">CVC3::TheoryArithOld::processSimpleIntEq()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00507">CVC3::TheoryArithNew::processSimpleIntEq()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00759">CVC3::TheoryArith3::processSimpleIntEq()</a>, <a class="el" href="theory__array_8cpp_source.html#l00368">CVC3::TheoryArray::rewrite()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03076">CVC3::TheoryArithOld::rewrite()</a>, <a class="el" href="array__theorem__producer_8cpp_source.html#l00122">CVC3::ArrayTheoremProducer::rewriteWriteWrite()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l03524">CVC3::TheoryArithNew::substAndCanonizeTableaux()</a>, and <a class="el" href="cnf__manager_8cpp_source.html#l00147">SAT::CNF_Manager::translateExprRec()</a>.</p>
</div>
</div>
<a class="anchor" id="a1e31c3827dae4bdfeeb6430c5c0f48b4"></a><!-- doxytag: member="MiniSat::parent" ref="a1e31c3827dae4bdfeeb6430c5c0f48b4" args="(int i)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">static int MiniSat::parent </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em></td><td>)</td>
<td><code> [inline, static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__heap_8h_source.html#l00055">55</a> of file <a class="el" href="minisat__heap_8h_source.html">minisat_heap.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__heap_8h_source.html#l00130">MiniSat::Heap< VarOrder_lt >::heapProperty()</a>, and <a class="el" href="minisat__heap_8h_source.html#l00064">MiniSat::Heap< VarOrder_lt >::percolateUp()</a>.</p>
</div>
</div>
<a class="anchor" id="a6d37e2f7d3903e1a85baf8f1e83eff78"></a><!-- doxytag: member="MiniSat::cvcToMiniSat" ref="a6d37e2f7d3903e1a85baf8f1e83eff78" args="(const SAT::Var &var)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> MiniSat::cvcToMiniSat </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classSAT_1_1Var.html">SAT::Var</a> & </td>
<td class="paramname"><em>var</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>conversions between <a class="el" href="namespaceMiniSat.html">MiniSat</a> and CVC data types: </p>
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00128">128</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="cnf_8h_source.html#l00044">SAT::Var::getIndex()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l00488">MiniSat::Solver::addClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00139">MiniSat::Solver::cvcToMiniSat()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00121">cvcToMiniSat()</a>, and <a class="el" href="dpllt__minisat_8cpp_source.html#l00244">SAT::DPLLTMiniSat::getValue()</a>.</p>
</div>
</div>
<a class="anchor" id="a72756c106b9bd53cf77c2aab214e7cf5"></a><!-- doxytag: member="MiniSat::miniSatToCVC" ref="a72756c106b9bd53cf77c2aab214e7cf5" args="(Var var)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classSAT_1_1Var.html">SAT::Var</a> MiniSat::miniSatToCVC </td>
<td>(</td>
<td class="paramtype">Var </td>
<td class="paramname"><em>var</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00132">132</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__derivation_8cpp_source.html#l00260">MiniSat::Derivation::createProof()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00351">MiniSat::Solver::curAssigns()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00360">MiniSat::Solver::curClauses()</a>, <a class="el" href="minisat__solver_8h_source.html#l00141">miniSatToCVC()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01689">MiniSat::Solver::propagate()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02510">MiniSat::Solver::push()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02005">MiniSat::Solver::search()</a>.</p>
</div>
</div>
<a class="anchor" id="a0eb766a18a8ba93182ee46d85a40c282"></a><!-- doxytag: member="MiniSat::cvcToMiniSat" ref="a0eb766a18a8ba93182ee46d85a40c282" args="(const SAT::Lit &literal)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classMiniSat_1_1Lit.html">Lit</a> MiniSat::cvcToMiniSat </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> & </td>
<td class="paramname"><em>literal</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00137">137</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00128">cvcToMiniSat()</a>, <a class="el" href="cnf_8h_source.html#l00070">SAT::Lit::getVar()</a>, and <a class="el" href="cnf_8h_source.html#l00064">SAT::Lit::isPositive()</a>.</p>
</div>
</div>
<a class="anchor" id="a30ac392b840d0ee1aa3877dadebff3fd"></a><!-- doxytag: member="MiniSat::miniSatToCVC" ref="a30ac392b840d0ee1aa3877dadebff3fd" args="(Lit literal)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> MiniSat::miniSatToCVC </td>
<td>(</td>
<td class="paramtype">Lit </td>
<td class="paramname"><em>literal</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00141">141</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00132">miniSatToCVC()</a>, <a class="el" href="minisat__types_8h_source.html#l00068">MiniSat::Lit::sign()</a>, and <a class="el" href="minisat__types_8h_source.html#l00069">MiniSat::Lit::var()</a>.</p>
</div>
</div>
<a class="anchor" id="ace6b835dfa37172fd8e8177fa6373c4b"></a><!-- doxytag: member="MiniSat::cvcToMiniSat" ref="ace6b835dfa37172fd8e8177fa6373c4b" args="(const SAT::Clause &clause, std::vector< Lit > &literals)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool MiniSat::cvcToMiniSat </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classSAT_1_1Clause.html">SAT::Clause</a> & </td>
<td class="paramname"><em>clause</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="classMiniSat_1_1Lit.html">Lit</a> > & </td>
<td class="paramname"><em>literals</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>conversions between <a class="el" href="namespaceMiniSat.html">MiniSat</a> and CVC data types: </p>
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00121">121</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="cnf_8h_source.html#l00093">SAT::Clause::begin()</a>, <a class="el" href="minisat__solver_8h_source.html#l00128">cvcToMiniSat()</a>, <a class="el" href="cnf_8h_source.html#l00094">SAT::Clause::end()</a>, <a class="el" href="cnf_8h_source.html#l00066">SAT::Lit::isFalse()</a>, and <a class="el" href="cnf_8h_source.html#l00067">SAT::Lit::isTrue()</a>.</p>
</div>
</div>
<a class="anchor" id="ab76c348e2f4f918b5117b8850462b0e0"></a><!-- doxytag: member="MiniSat::malloc_clause" ref="ab76c348e2f4f918b5117b8850462b0e0" args="(const vector< Lit > &ps)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void* MiniSat::malloc_clause </td>
<td>(</td>
<td class="paramtype">const vector< Lit > & </td>
<td class="paramname"><em>ps</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__types_8cpp_source.html#l00039">39</a> of file <a class="el" href="minisat__types_8cpp_source.html">minisat_types.cpp</a>.</p>
<p>References <a class="el" href="minisat__types_8cpp_source.html#l00033">clause_mem_base</a>, and <a class="el" href="cvc__util_8h_source.html#l00056">CVC3::max()</a>.</p>
<p>Referenced by <a class="el" href="minisat__types_8cpp_source.html#l00044">Clause_new()</a>, and <a class="el" href="minisat__types_8cpp_source.html#l00049">Lemma_new()</a>.</p>
</div>
</div>
<a class="anchor" id="a9a3ff2cc55978ca3a973861cad2814e2"></a><!-- doxytag: member="MiniSat::Clause_new" ref="a9a3ff2cc55978ca3a973861cad2814e2" args="(const vector< Lit > &ps, CVC3::Theorem theorem, int id)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * MiniSat::Clause_new </td>
<td>(</td>
<td class="paramtype">const vector< Lit > & </td>
<td class="paramname"><em>ps</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> </td>
<td class="paramname"><em>theorem</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>id</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__types_8cpp_source.html#l00044">44</a> of file <a class="el" href="minisat__types_8cpp_source.html">minisat_types.cpp</a>.</p>
<p>References <a class="el" href="minisat__types_8cpp_source.html#l00039">malloc_clause()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l00671">MiniSat::Solver::addClause()</a>, <a class="el" href="minisat__derivation_8cpp_source.html#l00062">MiniSat::Derivation::computeRootReason()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00139">MiniSat::Solver::cvcToMiniSat()</a>, <a class="el" href="minisat__types_8cpp_source.html#l00054">MiniSat::Clause::Decision()</a>, <a class="el" href="minisat__derivation_8cpp_source.html#l00115">MiniSat::Derivation::finish()</a>, and <a class="el" href="minisat__types_8cpp_source.html#l00063">MiniSat::Clause::TheoryImplication()</a>.</p>
</div>
</div>
<a class="anchor" id="a2659fd436dc00aebee015ce18ae2c89a"></a><!-- doxytag: member="MiniSat::Lemma_new" ref="a2659fd436dc00aebee015ce18ae2c89a" args="(const vector< Lit > &ps, int id, int pushID)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * MiniSat::Lemma_new </td>
<td>(</td>
<td class="paramtype">const vector< Lit > & </td>
<td class="paramname"><em>ps</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>id</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>pushID</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__types_8cpp_source.html#l00049">49</a> of file <a class="el" href="minisat__types_8cpp_source.html">minisat_types.cpp</a>.</p>
<p>References <a class="el" href="minisat__types_8cpp_source.html#l00039">malloc_clause()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01091">MiniSat::Solver::analyze()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00190">MiniSat::Solver::insertLemma()</a>.</p>
</div>
</div>
<a class="anchor" id="a120ea2f17b58215d657cd7b005edcd85"></a><!-- doxytag: member="MiniSat::lit_Undef" ref="a120ea2f17b58215d657cd7b005edcd85" args="(var_Undef, false)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classMiniSat_1_1Lit.html">Lit</a> MiniSat::lit_Undef </td>
<td>(</td>
<td class="paramtype">var_Undef </td>
<td class="paramname">, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">false </td>
<td class="paramname"> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01091">MiniSat::Solver::analyze()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02005">MiniSat::Solver::search()</a>.</p>
</div>
</div>
<a class="anchor" id="ad1ccf328f5909693679e1c703981b434"></a><!-- doxytag: member="MiniSat::lit_Error" ref="ad1ccf328f5909693679e1c703981b434" args="(var_Undef, true)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classMiniSat_1_1Lit.html">Lit</a> MiniSat::lit_Error </td>
<td>(</td>
<td class="paramtype">var_Undef </td>
<td class="paramname">, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">true </td>
<td class="paramname"> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
</div>
</div>
<hr/><h2>Variable Documentation</h2>
<a class="anchor" id="ad0b6e52186f3374f569c4de9db621be1"></a><!-- doxytag: member="MiniSat::l_True" ref="ad0b6e52186f3374f569c4de9db621be1" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classMiniSat_1_1lbool.html">lbool</a> <a class="el" href="namespaceMiniSat.html#ad0b6e52186f3374f569c4de9db621be1">MiniSat::l_True</a> = toLbool( 1)</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__global_8h_source.html#l00214">214</a> of file <a class="el" href="minisat__global_8h_source.html">minisat_global.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02313">MiniSat::Solver::allClausesSatisfied()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02398">MiniSat::Solver::checkClause()</a>, <a class="el" href="minisat__derivation_8cpp_source.html#l00062">MiniSat::Derivation::computeRootReason()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00950">MiniSat::Solver::getReason()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00244">SAT::DPLLTMiniSat::getValue()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00750">MiniSat::Solver::insertClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01458">MiniSat::Solver::isPermSatisfied()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00588">MiniSat::Solver::orderClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01689">MiniSat::Solver::propagate()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00999">MiniSat::Solver::resolveTheoryImplication()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00545">MiniSat::Solver::simplifyClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01816">MiniSat::Solver::simplifyDB()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00319">MiniSat::Solver::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="a810166165364a8a8262d24b13d7b1da9"></a><!-- doxytag: member="MiniSat::l_False" ref="a810166165364a8a8262d24b13d7b1da9" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classMiniSat_1_1lbool.html">lbool</a> <a class="el" href="namespaceMiniSat.html#a810166165364a8a8262d24b13d7b1da9">MiniSat::l_False</a> = toLbool(-1)</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__global_8h_source.html#l00215">215</a> of file <a class="el" href="minisat__global_8h_source.html">minisat_global.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01091">MiniSat::Solver::analyze()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02398">MiniSat::Solver::checkClause()</a>, <a class="el" href="minisat__derivation_8cpp_source.html#l00062">MiniSat::Derivation::computeRootReason()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01575">MiniSat::Solver::enqueue()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00935">MiniSat::Solver::getConflictLevel()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00910">MiniSat::Solver::getImplicationLevel()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00244">SAT::DPLLTMiniSat::getValue()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00750">MiniSat::Solver::insertClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00190">MiniSat::Solver::insertLemma()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00588">MiniSat::Solver::orderClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01689">MiniSat::Solver::propagate()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00999">MiniSat::Solver::resolveTheoryImplication()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00545">MiniSat::Solver::simplifyClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01816">MiniSat::Solver::simplifyDB()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00319">MiniSat::Solver::toString()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00977">MiniSat::Solver::updateConflict()</a>.</p>
</div>
</div>
<a class="anchor" id="aa6f5310857da28f01311aebd650a531f"></a><!-- doxytag: member="MiniSat::l_Undef" ref="aa6f5310857da28f01311aebd650a531f" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classMiniSat_1_1lbool.html">lbool</a> <a class="el" href="namespaceMiniSat.html#aa6f5310857da28f01311aebd650a531f">MiniSat::l_Undef</a> = toLbool( 0)</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__global_8h_source.html#l00216">216</a> of file <a class="el" href="minisat__global_8h_source.html">minisat_global.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01481">MiniSat::Solver::backtrack()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02398">MiniSat::Solver::checkClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01575">MiniSat::Solver::enqueue()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00750">MiniSat::Solver::insertClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02668">MiniSat::Solver::pop()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01950">MiniSat::Solver::propLookahead()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00457">MiniSat::Solver::registerVar()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02005">MiniSat::Solver::search()</a>, and <a class="el" href="minisat__varorder_8h_source.html#l00104">MiniSat::VarOrder::select()</a>.</p>
</div>
</div>
<a class="anchor" id="a633ea02a1812110095e4f982ff342b92"></a><!-- doxytag: member="MiniSat::clause_mem_base" ref="a633ea02a1812110095e4f982ff342b92" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const int <a class="el" href="namespaceMiniSat.html#a633ea02a1812110095e4f982ff342b92">MiniSat::clause_mem_base</a></td>
</tr>
</table>
</div>
<div class="memdoc">
<b>Initial value:</b><div class="fragment"><pre class="fragment">
<span class="keyword">sizeof</span>(<span class="keywordtype">unsigned</span> int)
+ 2 * <span class="keyword">sizeof</span>(<span class="keywordtype">int</span>)
+ <span class="keyword">sizeof</span>(float)
+ <span class="keyword">sizeof</span> (<a class="code" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a>)
</pre></div>
<p>Definition at line <a class="el" href="minisat__types_8cpp_source.html#l00033">33</a> of file <a class="el" href="minisat__types_8cpp_source.html">minisat_types.cpp</a>.</p>
<p>Referenced by <a class="el" href="minisat__types_8cpp_source.html#l00039">malloc_clause()</a>.</p>
</div>
</div>
<a class="anchor" id="af0b81724f9c7f24ed9a52a4627b5db86"></a><!-- doxytag: member="MiniSat::var_Undef" ref="af0b81724f9c7f24ed9a52a4627b5db86" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const int <a class="el" href="namespaceMiniSat.html#af0b81724f9c7f24ed9a52a4627b5db86">MiniSat::var_Undef</a> = -1</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__types_8h_source.html#l00056">56</a> of file <a class="el" href="minisat__types_8h_source.html">minisat_types.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01950">MiniSat::Solver::propLookahead()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02005">MiniSat::Solver::search()</a>, and <a class="el" href="minisat__varorder_8h_source.html#l00104">MiniSat::VarOrder::select()</a>.</p>
</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>
