<!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"/>
<meta http-equiv="X-UA-Compatible" content="IE=9"/>
<title>CVC3: MiniSat Namespace Reference</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="jquery.js"></script>
<script type="text/javascript" src="dynsections.js"></script>
<link href="doxygen.css" rel="stylesheet" type="text/css" />
</head>
<body>
<div id="top"><!-- do not remove this div, it is closed by doxygen! -->
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3
</div>
</td>
</tr>
</tbody>
</table>
</div>
<!-- end header part -->
<!-- Generated by Doxygen 1.8.2 -->
<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><!-- top -->
<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><!--header-->
<div class="contents">
<table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="nested-classes"></a>
Classes</h2></td></tr>
<tr class="memitem:"><td class="memItemLeft" align="right" valign="top">class  </td><td class="memItemRight" valign="bottom"><a class="el" href="classMiniSat_1_1Inference.html">Inference</a></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:"><td class="memItemLeft" align="right" valign="top">class  </td><td class="memItemRight" valign="bottom"><a class="el" href="classMiniSat_1_1Derivation.html">Derivation</a></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:"><td class="memItemLeft" align="right" valign="top">struct  </td><td class="memItemRight" valign="bottom"><a class="el" href="structMiniSat_1_1STATIC__ASSERTION__FAILURE_3_01true_01_4.html">STATIC_ASSERTION_FAILURE< true ></a></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:"><td class="memItemLeft" align="right" valign="top">class  </td><td class="memItemRight" valign="bottom"><a class="el" href="classMiniSat_1_1vec.html">vec</a></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:"><td class="memItemLeft" align="right" valign="top">class  </td><td class="memItemRight" valign="bottom"><a class="el" href="classMiniSat_1_1lbool.html">lbool</a></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:"><td class="memItemLeft" align="right" valign="top">class  </td><td class="memItemRight" valign="bottom"><a class="el" href="classMiniSat_1_1Heap.html">Heap</a></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:"><td class="memItemLeft" align="right" valign="top">struct  </td><td class="memItemRight" valign="bottom"><a class="el" href="structMiniSat_1_1SolverStats.html">SolverStats</a></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:"><td class="memItemLeft" align="right" valign="top">struct  </td><td class="memItemRight" valign="bottom"><a class="el" href="structMiniSat_1_1PushEntry.html">PushEntry</a></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:"><td class="memItemLeft" align="right" valign="top">struct  </td><td class="memItemRight" valign="bottom"><a class="el" href="structMiniSat_1_1SearchParams.html">SearchParams</a></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:"><td class="memItemLeft" align="right" valign="top">class  </td><td class="memItemRight" valign="bottom"><a class="el" href="classMiniSat_1_1Solver.html">Solver</a></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:"><td class="memItemLeft" align="right" valign="top">class  </td><td class="memItemRight" valign="bottom"><a class="el" href="classMiniSat_1_1Lit.html">Lit</a></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:"><td class="memItemLeft" align="right" valign="top">class  </td><td class="memItemRight" valign="bottom"><a class="el" href="classMiniSat_1_1Clause.html">Clause</a></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:"><td class="memItemLeft" align="right" valign="top">struct  </td><td class="memItemRight" valign="bottom"><a class="el" href="structMiniSat_1_1VarOrder__lt.html">VarOrder_lt</a></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:"><td class="memItemLeft" align="right" valign="top">class  </td><td class="memItemRight" valign="bottom"><a class="el" href="classMiniSat_1_1VarOrder.html">VarOrder</a></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="typedef-members"></a>
Typedefs</h2></td></tr>
<tr class="memitem:ad579041894c169fecdeb319f9aa5948d"><td class="memItemLeft" align="right" valign="top">typedef std::vector< int ><br class="typebreak"/>
::<a class="el" href="namespaceMiniSat.html#ad579041894c169fecdeb319f9aa5948d">size_type</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#ad579041894c169fecdeb319f9aa5948d">size_type</a></td></tr>
<tr class="separator:ad579041894c169fecdeb319f9aa5948d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0d9722420b2afd308dceda22c1b05a5e"><td class="memItemLeft" align="right" valign="top">typedef int </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a></td></tr>
<tr class="separator:a0d9722420b2afd308dceda22c1b05a5e"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="func-members"></a>
Functions</h2></td></tr>
<tr class="memitem:a342fc8b6bcd668b931a0bff2119e9aa8"><td class="memTemplParams" colspan="2">template<class T > </td></tr>
<tr class="memitem:a342fc8b6bcd668b931a0bff2119e9aa8"><td class="memTemplItemLeft" align="right" valign="top">static T </td><td class="memTemplItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#a342fc8b6bcd668b931a0bff2119e9aa8">min</a> (T x, T y)</td></tr>
<tr class="separator:a342fc8b6bcd668b931a0bff2119e9aa8"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a96d27264120083122347d87a2d82cd98"><td class="memTemplParams" colspan="2">template<class T > </td></tr>
<tr class="memitem:a96d27264120083122347d87a2d82cd98"><td class="memTemplItemLeft" align="right" valign="top">static T </td><td class="memTemplItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#a96d27264120083122347d87a2d82cd98">max</a> (T x, T y)</td></tr>
<tr class="separator:a96d27264120083122347d87a2d82cd98"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad9cef9b7ffc30b1480a990f00e96e74f"><td class="memTemplParams" colspan="2">template<class T > </td></tr>
<tr class="memitem:ad9cef9b7ffc30b1480a990f00e96e74f"><td class="memTemplItemLeft" align="right" valign="top">static T * </td><td class="memTemplItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#ad9cef9b7ffc30b1480a990f00e96e74f">xmalloc</a> (size_t size)</td></tr>
<tr class="separator:ad9cef9b7ffc30b1480a990f00e96e74f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6b9f3f6257910e2c48a3e8384bdd06a0"><td class="memTemplParams" colspan="2">template<class T > </td></tr>
<tr class="memitem:a6b9f3f6257910e2c48a3e8384bdd06a0"><td class="memTemplItemLeft" align="right" valign="top">static T * </td><td class="memTemplItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#a6b9f3f6257910e2c48a3e8384bdd06a0">xrealloc</a> (T *ptr, size_t size)</td></tr>
<tr class="separator:a6b9f3f6257910e2c48a3e8384bdd06a0"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a4e5f70e98cdfee0fd9b018a267f09e4a"><td class="memTemplParams" colspan="2">template<class T > </td></tr>
<tr class="memitem:a4e5f70e98cdfee0fd9b018a267f09e4a"><td class="memTemplItemLeft" align="right" valign="top">static void </td><td class="memTemplItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#a4e5f70e98cdfee0fd9b018a267f09e4a">xfree</a> (T *ptr)</td></tr>
<tr class="separator:a4e5f70e98cdfee0fd9b018a267f09e4a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a24abdfa24bc8d99b5f25d3cd38adaa78"><td class="memItemLeft" align="right" valign="top">static double </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#a24abdfa24bc8d99b5f25d3cd38adaa78">drand</a> (double &seed)</td></tr>
<tr class="separator:a24abdfa24bc8d99b5f25d3cd38adaa78"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a8ecdd514fb182dd7adadecd941f1be3b"><td class="memItemLeft" align="right" valign="top">static int </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#a8ecdd514fb182dd7adadecd941f1be3b">irand</a> (double &seed, int size)</td></tr>
<tr class="separator:a8ecdd514fb182dd7adadecd941f1be3b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a4c585f2e8db13de83607a0d22761e91d"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#a4c585f2e8db13de83607a0d22761e91d">toInt</a> (<a class="el" href="classMiniSat_1_1lbool.html">lbool</a> l)</td></tr>
<tr class="separator:a4c585f2e8db13de83607a0d22761e91d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a1c28cb1733880d6dbc7aff894cb5527d"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classMiniSat_1_1lbool.html">lbool</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#a1c28cb1733880d6dbc7aff894cb5527d">toLbool</a> (int v)</td></tr>
<tr class="separator:a1c28cb1733880d6dbc7aff894cb5527d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a9d1c1a3916831204073248d296b421cb"><td class="memTemplParams" colspan="2">template<class T > </td></tr>
<tr class="memitem:a9d1c1a3916831204073248d296b421cb"><td class="memTemplItemLeft" align="right" valign="top">static bool </td><td class="memTemplItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#a9d1c1a3916831204073248d296b421cb">operator!=</a> (const T &x, const T &y)</td></tr>
<tr class="separator:a9d1c1a3916831204073248d296b421cb"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a59c5830d74a29955f16068e5fce9af1d"><td class="memTemplParams" colspan="2">template<class T > </td></tr>
<tr class="memitem:a59c5830d74a29955f16068e5fce9af1d"><td class="memTemplItemLeft" align="right" valign="top">static bool </td><td class="memTemplItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#a59c5830d74a29955f16068e5fce9af1d">operator></a> (const T &x, const T &y)</td></tr>
<tr class="separator:a59c5830d74a29955f16068e5fce9af1d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a3d181ba7d131f3d5687df617dc2f07ed"><td class="memTemplParams" colspan="2">template<class T > </td></tr>
<tr class="memitem:a3d181ba7d131f3d5687df617dc2f07ed"><td class="memTemplItemLeft" align="right" valign="top">static bool </td><td class="memTemplItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#a3d181ba7d131f3d5687df617dc2f07ed">operator<=</a> (const T &x, const T &y)</td></tr>
<tr class="separator:a3d181ba7d131f3d5687df617dc2f07ed"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a515d121183f07238ec3361bde2b3c32f"><td class="memTemplParams" colspan="2">template<class T > </td></tr>
<tr class="memitem:a515d121183f07238ec3361bde2b3c32f"><td class="memTemplItemLeft" align="right" valign="top">static bool </td><td class="memTemplItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#a515d121183f07238ec3361bde2b3c32f">operator>=</a> (const T &x, const T &y)</td></tr>
<tr class="separator:a515d121183f07238ec3361bde2b3c32f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad93cb56673487974071ed3b75bf4ea83"><td class="memItemLeft" align="right" valign="top">static int </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#ad93cb56673487974071ed3b75bf4ea83">left</a> (int i)</td></tr>
<tr class="separator:ad93cb56673487974071ed3b75bf4ea83"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a82558b7a36c52f5d3211d5d14bed99d4"><td class="memItemLeft" align="right" valign="top">static int </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#a82558b7a36c52f5d3211d5d14bed99d4">right</a> (int i)</td></tr>
<tr class="separator:a82558b7a36c52f5d3211d5d14bed99d4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a1e31c3827dae4bdfeeb6430c5c0f48b4"><td class="memItemLeft" align="right" valign="top">static int </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#a1e31c3827dae4bdfeeb6430c5c0f48b4">parent</a> (int i)</td></tr>
<tr class="separator:a1e31c3827dae4bdfeeb6430c5c0f48b4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6d37e2f7d3903e1a85baf8f1e83eff78"><td class="memItemLeft" align="right" valign="top"><a class="el" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#a6d37e2f7d3903e1a85baf8f1e83eff78">cvcToMiniSat</a> (const <a class="el" href="classSAT_1_1Var.html">SAT::Var</a> &var)</td></tr>
<tr class="separator:a6d37e2f7d3903e1a85baf8f1e83eff78"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a72756c106b9bd53cf77c2aab214e7cf5"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classSAT_1_1Var.html">SAT::Var</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#a72756c106b9bd53cf77c2aab214e7cf5">miniSatToCVC</a> (<a class="el" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> var)</td></tr>
<tr class="separator:a72756c106b9bd53cf77c2aab214e7cf5"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0eb766a18a8ba93182ee46d85a40c282"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classMiniSat_1_1Lit.html">Lit</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#a0eb766a18a8ba93182ee46d85a40c282">cvcToMiniSat</a> (const <a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> &literal)</td></tr>
<tr class="separator:a0eb766a18a8ba93182ee46d85a40c282"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a30ac392b840d0ee1aa3877dadebff3fd"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#a30ac392b840d0ee1aa3877dadebff3fd">miniSatToCVC</a> (<a class="el" href="classMiniSat_1_1Lit.html">Lit</a> literal)</td></tr>
<tr class="separator:a30ac392b840d0ee1aa3877dadebff3fd"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ace6b835dfa37172fd8e8177fa6373c4b"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><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)</td></tr>
<tr class="separator:ace6b835dfa37172fd8e8177fa6373c4b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab76c348e2f4f918b5117b8850462b0e0"><td class="memItemLeft" align="right" valign="top">void * </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#ab76c348e2f4f918b5117b8850462b0e0">malloc_clause</a> (const vector< <a class="el" href="classMiniSat_1_1Lit.html">Lit</a> > &ps)</td></tr>
<tr class="separator:ab76c348e2f4f918b5117b8850462b0e0"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a9a3ff2cc55978ca3a973861cad2814e2"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * </td><td class="memItemRight" valign="bottom"><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)</td></tr>
<tr class="separator:a9a3ff2cc55978ca3a973861cad2814e2"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a2659fd436dc00aebee015ce18ae2c89a"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * </td><td class="memItemRight" valign="bottom"><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)</td></tr>
<tr class="separator:a2659fd436dc00aebee015ce18ae2c89a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a120ea2f17b58215d657cd7b005edcd85"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classMiniSat_1_1Lit.html">Lit</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#a120ea2f17b58215d657cd7b005edcd85">lit_Undef</a> (<a class="el" href="namespaceMiniSat.html#af0b81724f9c7f24ed9a52a4627b5db86">var_Undef</a>, false)</td></tr>
<tr class="separator:a120ea2f17b58215d657cd7b005edcd85"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad1ccf328f5909693679e1c703981b434"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classMiniSat_1_1Lit.html">Lit</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#ad1ccf328f5909693679e1c703981b434">lit_Error</a> (<a class="el" href="namespaceMiniSat.html#af0b81724f9c7f24ed9a52a4627b5db86">var_Undef</a>, true)</td></tr>
<tr class="separator:ad1ccf328f5909693679e1c703981b434"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="var-members"></a>
Variables</h2></td></tr>
<tr class="memitem:ad0b6e52186f3374f569c4de9db621be1"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classMiniSat_1_1lbool.html">lbool</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#ad0b6e52186f3374f569c4de9db621be1">l_True</a> = <a class="el" href="namespaceMiniSat.html#a1c28cb1733880d6dbc7aff894cb5527d">toLbool</a>( 1)</td></tr>
<tr class="separator:ad0b6e52186f3374f569c4de9db621be1"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a810166165364a8a8262d24b13d7b1da9"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classMiniSat_1_1lbool.html">lbool</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#a810166165364a8a8262d24b13d7b1da9">l_False</a> = <a class="el" href="namespaceMiniSat.html#a1c28cb1733880d6dbc7aff894cb5527d">toLbool</a>(-1)</td></tr>
<tr class="separator:a810166165364a8a8262d24b13d7b1da9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa6f5310857da28f01311aebd650a531f"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classMiniSat_1_1lbool.html">lbool</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#aa6f5310857da28f01311aebd650a531f">l_Undef</a> = <a class="el" href="namespaceMiniSat.html#a1c28cb1733880d6dbc7aff894cb5527d">toLbool</a>( 0)</td></tr>
<tr class="separator:aa6f5310857da28f01311aebd650a531f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a633ea02a1812110095e4f982ff342b92"><td class="memItemLeft" align="right" valign="top">const int </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#a633ea02a1812110095e4f982ff342b92">clause_mem_base</a></td></tr>
<tr class="separator:a633ea02a1812110095e4f982ff342b92"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:af0b81724f9c7f24ed9a52a4627b5db86"><td class="memItemLeft" align="right" valign="top">const int </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceMiniSat.html#af0b81724f9c7f24ed9a52a4627b5db86">var_Undef</a> = -1</td></tr>
<tr class="separator:af0b81724f9c7f24ed9a52a4627b5db86"><td class="memSeparator" colspan="2"> </td></tr>
</table>
<h2 class="groupheader">Typedef Documentation</h2>
<a class="anchor" id="ad579041894c169fecdeb319f9aa5948d"></a>
<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>
<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>
<h2 class="groupheader">Function Documentation</h2>
<a class="anchor" id="a342fc8b6bcd668b931a0bff2119e9aa8"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class T > </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">static</span></span> </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__new_8cpp_source.html#l00388">CVC3::TheoryArithNew::pickIntEqMonomial()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00590">CVC3::TheoryArith3::pickIntEqMonomial()</a>, and <a class="el" href="theory__arith__old_8cpp_source.html#l00563">CVC3::TheoryArithOld::pickIntEqMonomial()</a>.</p>
</div>
</div>
<a class="anchor" id="a96d27264120083122347d87a2d82cd98"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class T > </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">static</span></span> </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>, and <a class="el" href="minisat__solver_8cpp_source.html#l00750">MiniSat::Solver::insertClause()</a>.</p>
</div>
</div>
<a class="anchor" id="ad9cef9b7ffc30b1480a990f00e96e74f"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class T > </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">static</span></span> </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="a6b9f3f6257910e2c48a3e8384bdd06a0"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class T > </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">static</span></span> </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="a4e5f70e98cdfee0fd9b018a267f09e4a"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class T > </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">static</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">static</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">static</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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="a9d1c1a3916831204073248d296b421cb"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class T > </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">static</span></span> </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="a59c5830d74a29955f16068e5fce9af1d"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class T > </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">static</span></span> </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="a3d181ba7d131f3d5687df617dc2f07ed"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class T > </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">static</span></span> </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="a515d121183f07238ec3361bde2b3c32f"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class T > </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">static</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">static</span></span> </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__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__old_8cpp_source.html#l02780">CVC3::TheoryArithOld::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__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="arith__theorem__producer__old_8cpp_source.html#l02297">CVC3::ArithTheoremProducerOld::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__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#l00615">CVC3::TheoryArithOld::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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">static</span></span> </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__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#l00447">CVC3::TheoryArithOld::doSolve()</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__old_8cpp_source.html#l02780">CVC3::TheoryArithOld::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__producer3_8cpp_source.html#l02095">CVC3::ArithTheoremProducer3::intVarEqnConst()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02297">CVC3::ArithTheoremProducerOld::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__arith3_8cpp_source.html#l01150">CVC3::TheoryArith3::isolateVariable()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l01499">CVC3::TheoryArithOld::isolateVariable()</a>, <a class="el" href="vcl_8cpp_source.html#l01333">CVC3::VCL::minusExpr()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l00861">CVC3::ArithTheoremProducer3::moveSumConstantRight()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l00911">CVC3::ArithTheoremProducerOld::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__arith3_8cpp_source.html#l01449">CVC3::TheoryArith3::normalizeProjectIneqs()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l01822">CVC3::TheoryArithOld::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__producer3_8cpp_source.html#l01362">CVC3::ArithTheoremProducer3::plusPredicate()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l01430">CVC3::ArithTheoremProducerOld::plusPredicate()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01376">CVC3::ArithTheoremProducer::plusPredicate()</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#l00615">CVC3::TheoryArithOld::processRealEq()</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__arith__old_8cpp_source.html#l00739">CVC3::TheoryArithOld::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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">static</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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#l00121">cvcToMiniSat()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00139">MiniSat::Solver::cvcToMiniSat()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00244">SAT::DPLLTMiniSat::getValue()</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="a72756c106b9bd53cf77c2aab214e7cf5"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<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>
<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>
<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>
<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>
<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>
<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>
<h2 class="groupheader">Variable Documentation</h2>
<a class="anchor" id="ad0b6e52186f3374f569c4de9db621be1"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classMiniSat_1_1lbool.html">lbool</a> MiniSat::l_True = <a class="el" href="namespaceMiniSat.html#a1c28cb1733880d6dbc7aff894cb5527d">toLbool</a>( 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>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classMiniSat_1_1lbool.html">lbool</a> MiniSat::l_False = <a class="el" href="namespaceMiniSat.html#a1c28cb1733880d6dbc7aff894cb5527d">toLbool</a>(-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>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classMiniSat_1_1lbool.html">lbool</a> MiniSat::l_Undef = <a class="el" href="namespaceMiniSat.html#a1c28cb1733880d6dbc7aff894cb5527d">toLbool</a>( 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>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const int MiniSat::clause_mem_base</td>
</tr>
</table>
</div><div class="memdoc">
<b>Initial value:</b><div class="fragment"><div class="line">=</div>
<div class="line"> <span class="keyword">sizeof</span>(<span class="keywordtype">unsigned</span> int)</div>
<div class="line"> + 2 * <span class="keyword">sizeof</span>(<span class="keywordtype">int</span>)</div>
<div class="line"> + <span class="keyword">sizeof</span>(float)</div>
<div class="line"> + <span class="keyword">sizeof</span> (<a class="code" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a>)</div>
</div><!-- fragment -->
<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>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const int MiniSat::var_Undef = -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><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:20 for CVC3 by  <a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/>
</a> 1.8.2
</small></address>
</body>
</html>
