<!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: SAT::DPLLTBasic Class 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><a href="namespaces.html"><span>Namespaces</span></a></li>
<li class="current"><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="annotated.html"><span>Class List</span></a></li>
<li><a href="classes.html"><span>Class Index</span></a></li>
<li><a href="inherits.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="namespaceSAT.html">SAT</a></li><li class="navelem"><a class="el" href="classSAT_1_1DPLLTBasic.html">DPLLTBasic</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="summary">
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pri-methods">Private Member Functions</a> |
<a href="#pri-attribs">Private Attributes</a> |
<a href="classSAT_1_1DPLLTBasic-members.html">List of all members</a> </div>
<div class="headertitle">
<div class="title">SAT::DPLLTBasic Class Reference</div> </div>
</div><!--header-->
<div class="contents">
<p><code>#include <<a class="el" href="dpllt__basic_8h_source.html">dpllt_basic.h</a>></code></p>
<p>Inherits <a class="el" href="classSAT_1_1DPLLT.html">SAT::DPLLT</a>.</p>
<div class="dynheader">
Collaboration diagram for SAT::DPLLTBasic:</div>
<div class="dyncontent">
<div class="center"><img src="classSAT_1_1DPLLTBasic__coll__graph.gif" border="0" usemap="#SAT_1_1DPLLTBasic_coll__map" alt="Collaboration graph"/></div>
<map name="SAT_1_1DPLLTBasic_coll__map" id="SAT_1_1DPLLTBasic_coll__map">
</map>
</div>
<table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pub-methods"></a>
Public Member Functions</h2></td></tr>
<tr class="memitem:a11ff82c567a310525206ba0260fbde5e"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#a11ff82c567a310525206ba0260fbde5e">DPLLTBasic</a> (<a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html">TheoryAPI</a> *<a class="el" href="classSAT_1_1DPLLT.html#adec2886c41b3443c264b852bc5f5a84c">theoryAPI</a>, <a class="el" href="classSAT_1_1DPLLT_1_1Decider.html">Decider</a> *<a class="el" href="classSAT_1_1DPLLT.html#add78f8065e68c538dd0914949fb87aef">decider</a>, <a class="el" href="classCVC3_1_1ContextManager.html">CVC3::ContextManager</a> *cm, bool printStats=false)</td></tr>
<tr class="separator:a11ff82c567a310525206ba0260fbde5e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a080afc4433840fd154465360ec97ca2b"><td class="memItemLeft" align="right" valign="top">virtual </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#a080afc4433840fd154465360ec97ca2b">~DPLLTBasic</a> ()</td></tr>
<tr class="separator:a080afc4433840fd154465360ec97ca2b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:abfe1c680e074676f0f291125e7eb150e"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#abfe1c680e074676f0f291125e7eb150e">addNewClause</a> (const <a class="el" href="classSAT_1_1Clause.html">Clause</a> &c)</td></tr>
<tr class="separator:abfe1c680e074676f0f291125e7eb150e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:acc013b97f0368bc1ca43cf374f06521c"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#acc013b97f0368bc1ca43cf374f06521c">addNewClauses</a> (<a class="el" href="classSAT_1_1CNF__Formula__Impl.html">CNF_Formula_Impl</a> &cnf)</td></tr>
<tr class="separator:acc013b97f0368bc1ca43cf374f06521c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a96c27b95e07e062a16beb412f68608a1"><td class="memItemLeft" align="right" valign="top"><a class="el" href="unionSatSolver_1_1Lit.html">SatSolver::Lit</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#a96c27b95e07e062a16beb412f68608a1">cvc2SAT</a> (<a class="el" href="classSAT_1_1Lit.html">Lit</a> l)</td></tr>
<tr class="separator:a96c27b95e07e062a16beb412f68608a1"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad9ce5fbf4bb808f859d6aae48bfb07db"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classSAT_1_1Lit.html">Lit</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#ad9ce5fbf4bb808f859d6aae48bfb07db">SAT2cvc</a> (<a class="el" href="unionSatSolver_1_1Lit.html">SatSolver::Lit</a> l)</td></tr>
<tr class="separator:ad9ce5fbf4bb808f859d6aae48bfb07db"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0a36ed4b453c94678f0fbbc380a7d3fd"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classSatSolver.html">SatSolver</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#a0a36ed4b453c94678f0fbbc380a7d3fd">satSolver</a> ()</td></tr>
<tr class="separator:a0a36ed4b453c94678f0fbbc380a7d3fd"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a8c8f7e178849aead6754e44e3e63dc0c"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#a8c8f7e178849aead6754e44e3e63dc0c">push</a> ()</td></tr>
<tr class="memdesc:a8c8f7e178849aead6754e44e3e63dc0c"><td class="mdescLeft"> </td><td class="mdescRight">Set a checkpoint for backtracking. <a href="#a8c8f7e178849aead6754e44e3e63dc0c"></a><br/></td></tr>
<tr class="separator:a8c8f7e178849aead6754e44e3e63dc0c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aff5dbd3c2a47f003d7b388a8b673cc85"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#aff5dbd3c2a47f003d7b388a8b673cc85">pop</a> ()</td></tr>
<tr class="memdesc:aff5dbd3c2a47f003d7b388a8b673cc85"><td class="mdescLeft"> </td><td class="mdescRight">Restore checkpoint. <a href="#aff5dbd3c2a47f003d7b388a8b673cc85"></a><br/></td></tr>
<tr class="separator:aff5dbd3c2a47f003d7b388a8b673cc85"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:afaffe075e05bcd2e56aeede2154e0d5a"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#afaffe075e05bcd2e56aeede2154e0d5a">addAssertion</a> (const <a class="el" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a> &cnf)</td></tr>
<tr class="memdesc:afaffe075e05bcd2e56aeede2154e0d5a"><td class="mdescLeft"> </td><td class="mdescRight">Add new clauses to the <a class="el" href="namespaceSAT.html">SAT</a> solver. <a href="#afaffe075e05bcd2e56aeede2154e0d5a"></a><br/></td></tr>
<tr class="separator:afaffe075e05bcd2e56aeede2154e0d5a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a4047558a5e4a9e84b81e388b220d4e79"><td class="memItemLeft" align="right" valign="top">virtual std::vector< <a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> > </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#a4047558a5e4a9e84b81e388b220d4e79">getCurAssignments</a> ()</td></tr>
<tr class="separator:a4047558a5e4a9e84b81e388b220d4e79"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:abaf2763764a68c9e4fbc190953b4e6c8"><td class="memItemLeft" align="right" valign="top">virtual std::vector<br class="typebreak"/>
< std::vector< <a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> > > </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#abaf2763764a68c9e4fbc190953b4e6c8">getCurClauses</a> ()</td></tr>
<tr class="separator:abaf2763764a68c9e4fbc190953b4e6c8"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a195fdfa1972c882fd3d87eae0742c7ac"><td class="memItemLeft" align="right" valign="top"><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">CVC3::QueryResult</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#a195fdfa1972c882fd3d87eae0742c7ac">checkSat</a> (const <a class="el" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a> &cnf)</td></tr>
<tr class="memdesc:a195fdfa1972c882fd3d87eae0742c7ac"><td class="mdescLeft"> </td><td class="mdescRight">Check the satisfiability of a set of clauses in the current context. <a href="#a195fdfa1972c882fd3d87eae0742c7ac"></a><br/></td></tr>
<tr class="separator:a195fdfa1972c882fd3d87eae0742c7ac"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a1271494f0f1f6e9c249d8fce8418ecd7"><td class="memItemLeft" align="right" valign="top"><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">CVC3::QueryResult</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#a1271494f0f1f6e9c249d8fce8418ecd7">continueCheck</a> (const <a class="el" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a> &cnf)</td></tr>
<tr class="memdesc:a1271494f0f1f6e9c249d8fce8418ecd7"><td class="mdescLeft"> </td><td class="mdescRight">Continue checking the last check with additional constraints. <a href="#a1271494f0f1f6e9c249d8fce8418ecd7"></a><br/></td></tr>
<tr class="separator:a1271494f0f1f6e9c249d8fce8418ecd7"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab0eac02c714ede751cf48fb188e375f6"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">Var::Val</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#ab0eac02c714ede751cf48fb188e375f6">getValue</a> (<a class="el" href="classSAT_1_1Var.html">Var</a> v)</td></tr>
<tr class="memdesc:ab0eac02c714ede751cf48fb188e375f6"><td class="mdescLeft"> </td><td class="mdescRight">Get value of variable: unassigned, false, or true. <a href="#ab0eac02c714ede751cf48fb188e375f6"></a><br/></td></tr>
<tr class="separator:ab0eac02c714ede751cf48fb188e375f6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0c4e0f09aacb6791929ac0eb6e6662c0"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Proof.html">CVC3::Proof</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#a0c4e0f09aacb6791929ac0eb6e6662c0">getSatProof</a> (<a class="el" href="classSAT_1_1CNF__Manager.html">CNF_Manager</a> *, <a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a> *)</td></tr>
<tr class="memdesc:a0c4e0f09aacb6791929ac0eb6e6662c0"><td class="mdescLeft"> </td><td class="mdescRight">Get the proof from <a class="el" href="namespaceSAT.html">SAT</a> engine. <a href="#a0c4e0f09aacb6791929ac0eb6e6662c0"></a><br/></td></tr>
<tr class="separator:a0c4e0f09aacb6791929ac0eb6e6662c0"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="inherit_header pub_methods_classSAT_1_1DPLLT"><td colspan="2" onclick="javascript:toggleInherit('pub_methods_classSAT_1_1DPLLT')"><img src="closed.png" alt="-"/> Public Member Functions inherited from <a class="el" href="classSAT_1_1DPLLT.html">SAT::DPLLT</a></td></tr>
<tr class="memitem:abb3fd219fe5a66e70a70fe33b34b45f5 inherit pub_methods_classSAT_1_1DPLLT"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLT.html#abb3fd219fe5a66e70a70fe33b34b45f5">DPLLT</a> (<a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html">TheoryAPI</a> *<a class="el" href="classSAT_1_1DPLLT.html#adec2886c41b3443c264b852bc5f5a84c">theoryAPI</a>, <a class="el" href="classSAT_1_1DPLLT_1_1Decider.html">Decider</a> *<a class="el" href="classSAT_1_1DPLLT.html#add78f8065e68c538dd0914949fb87aef">decider</a>)</td></tr>
<tr class="memdesc:abb3fd219fe5a66e70a70fe33b34b45f5 inherit pub_methods_classSAT_1_1DPLLT"><td class="mdescLeft"> </td><td class="mdescRight">Constructor. <a href="#abb3fd219fe5a66e70a70fe33b34b45f5"></a><br/></td></tr>
<tr class="separator:abb3fd219fe5a66e70a70fe33b34b45f5 inherit pub_methods_classSAT_1_1DPLLT"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a59bc482fa7ea2517b7dcccbfd5690420 inherit pub_methods_classSAT_1_1DPLLT"><td class="memItemLeft" align="right" valign="top">virtual </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLT.html#a59bc482fa7ea2517b7dcccbfd5690420">~DPLLT</a> ()</td></tr>
<tr class="separator:a59bc482fa7ea2517b7dcccbfd5690420 inherit pub_methods_classSAT_1_1DPLLT"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:adec2886c41b3443c264b852bc5f5a84c inherit pub_methods_classSAT_1_1DPLLT"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html">TheoryAPI</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLT.html#adec2886c41b3443c264b852bc5f5a84c">theoryAPI</a> ()</td></tr>
<tr class="separator:adec2886c41b3443c264b852bc5f5a84c inherit pub_methods_classSAT_1_1DPLLT"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:add78f8065e68c538dd0914949fb87aef inherit pub_methods_classSAT_1_1DPLLT"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classSAT_1_1DPLLT_1_1Decider.html">Decider</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLT.html#add78f8065e68c538dd0914949fb87aef">decider</a> ()</td></tr>
<tr class="separator:add78f8065e68c538dd0914949fb87aef inherit pub_methods_classSAT_1_1DPLLT"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:adbf7530318ac373ba6c82983dc4dd595 inherit pub_methods_classSAT_1_1DPLLT"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLT.html#adbf7530318ac373ba6c82983dc4dd595">setDecider</a> (<a class="el" href="classSAT_1_1DPLLT_1_1Decider.html">Decider</a> *<a class="el" href="classSAT_1_1DPLLT.html#add78f8065e68c538dd0914949fb87aef">decider</a>)</td></tr>
<tr class="separator:adbf7530318ac373ba6c82983dc4dd595 inherit pub_methods_classSAT_1_1DPLLT"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pri-methods"></a>
Private Member Functions</h2></td></tr>
<tr class="memitem:a082ff0d184786dbd60a400320dbc826a"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#a082ff0d184786dbd60a400320dbc826a">createManager</a> ()</td></tr>
<tr class="separator:a082ff0d184786dbd60a400320dbc826a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a744ab3115b0c945843cc1310d06280b3"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#a744ab3115b0c945843cc1310d06280b3">generate_CDB</a> (<a class="el" href="classSAT_1_1CNF__Formula__Impl.html">CNF_Formula_Impl</a> &cnf)</td></tr>
<tr class="separator:a744ab3115b0c945843cc1310d06280b3"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa41a72c436f5faf03128d53bc4e3f9ef"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#aa41a72c436f5faf03128d53bc4e3f9ef">handle_result</a> (<a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53">SatSolver::SATStatus</a> outcome)</td></tr>
<tr class="separator:aa41a72c436f5faf03128d53bc4e3f9ef"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a1340aa7926370e1bc90d1da906eb8e79"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#a1340aa7926370e1bc90d1da906eb8e79">verify_solution</a> ()</td></tr>
<tr class="separator:a1340aa7926370e1bc90d1da906eb8e79"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pri-attribs"></a>
Private Attributes</h2></td></tr>
<tr class="memitem:a9e8593063e800cb17793629543493624"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ContextManager.html">CVC3::ContextManager</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#a9e8593063e800cb17793629543493624">d_cm</a></td></tr>
<tr class="separator:a9e8593063e800cb17793629543493624"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:af53a2ee63b573d7ddd70395cc58fab6a"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#af53a2ee63b573d7ddd70395cc58fab6a">d_ready</a></td></tr>
<tr class="separator:af53a2ee63b573d7ddd70395cc58fab6a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a21ec19cee9ab93b7cda66d209dd6e676"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classSatSolver.html">SatSolver</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#a21ec19cee9ab93b7cda66d209dd6e676">d_mng</a></td></tr>
<tr class="separator:a21ec19cee9ab93b7cda66d209dd6e676"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a191c0c9c76c2ab5a37038c32a7c6ab58"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classSAT_1_1CNF__Formula__Impl.html">CNF_Formula_Impl</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#a191c0c9c76c2ab5a37038c32a7c6ab58">d_cnf</a></td></tr>
<tr class="separator:a191c0c9c76c2ab5a37038c32a7c6ab58"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6032bad91260ee1c03ed4553425d6cf9"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classSAT_1_1CD__CNF__Formula.html">CD_CNF_Formula</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#a6032bad91260ee1c03ed4553425d6cf9">d_assertions</a></td></tr>
<tr class="separator:a6032bad91260ee1c03ed4553425d6cf9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aba339d2d7e2f5ed7bf1367e497e73087"><td class="memItemLeft" align="right" valign="top">std::vector< <a class="el" href="classSatSolver.html">SatSolver</a> * > </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#aba339d2d7e2f5ed7bf1367e497e73087">d_mngStack</a></td></tr>
<tr class="separator:aba339d2d7e2f5ed7bf1367e497e73087"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a423ff42fd5ccad2be5f8dd97654e9a81"><td class="memItemLeft" align="right" valign="top">std::vector< <a class="el" href="classSAT_1_1CNF__Formula__Impl.html">CNF_Formula_Impl</a> * > </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#a423ff42fd5ccad2be5f8dd97654e9a81">d_cnfStack</a></td></tr>
<tr class="separator:a423ff42fd5ccad2be5f8dd97654e9a81"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a4194dcc23968652060be41902ca5b376"><td class="memItemLeft" align="right" valign="top">std::vector< <a class="el" href="classSAT_1_1CD__CNF__Formula.html">CD_CNF_Formula</a> * > </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#a4194dcc23968652060be41902ca5b376">d_assertionsStack</a></td></tr>
<tr class="separator:a4194dcc23968652060be41902ca5b376"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a347d0b91280f484b5035505f148864e6"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#a347d0b91280f484b5035505f148864e6">d_printStats</a></td></tr>
<tr class="separator:a347d0b91280f484b5035505f148864e6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac1e928276774bc77063ee05aa2ceb078"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1CDO.html">CVC3::CDO</a>< unsigned > </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#ac1e928276774bc77063ee05aa2ceb078">d_pushLevel</a></td></tr>
<tr class="separator:ac1e928276774bc77063ee05aa2ceb078"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a04bf3fdf12271b364b22d40dc352f634"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1CDO.html">CVC3::CDO</a>< bool > </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#a04bf3fdf12271b364b22d40dc352f634">d_readyPrev</a></td></tr>
<tr class="separator:a04bf3fdf12271b364b22d40dc352f634"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ada4aa8a05927fc1ea334edea0b5f8fd3"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1CDO.html">CVC3::CDO</a>< unsigned > </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#ada4aa8a05927fc1ea334edea0b5f8fd3">d_prevStackSize</a></td></tr>
<tr class="separator:ada4aa8a05927fc1ea334edea0b5f8fd3"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0bd6e3a5262667eed68fd59cf6c39551"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1CDO.html">CVC3::CDO</a>< unsigned > </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLTBasic.html#a0bd6e3a5262667eed68fd59cf6c39551">d_prevAStackSize</a></td></tr>
<tr class="separator:a0bd6e3a5262667eed68fd59cf6c39551"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="inherited"></a>
Additional Inherited Members</h2></td></tr>
<tr class="inherit_header pub_types_classSAT_1_1DPLLT"><td colspan="2" onclick="javascript:toggleInherit('pub_types_classSAT_1_1DPLLT')"><img src="closed.png" alt="-"/> Public Types inherited from <a class="el" href="classSAT_1_1DPLLT.html">SAT::DPLLT</a></td></tr>
<tr class="memitem:ac612908684032ffe76ad97f04afd0ca8 inherit pub_types_classSAT_1_1DPLLT"><td class="memItemLeft" align="right" valign="top">enum  </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLT.html#ac612908684032ffe76ad97f04afd0ca8">ConsistentResult</a> { <a class="el" href="classSAT_1_1DPLLT.html#ac612908684032ffe76ad97f04afd0ca8a1dbdf8ba98f0b618f9f4dffcbc947f95">INCONSISTENT</a>,
<a class="el" href="classSAT_1_1DPLLT.html#ac612908684032ffe76ad97f04afd0ca8ab418da559e5bf8e1e7bb7f21dbd1b8ac">MAYBE_CONSISTENT</a>,
<a class="el" href="classSAT_1_1DPLLT.html#ac612908684032ffe76ad97f04afd0ca8ae8ec5d9933decee81ba80f5bd5cfbed2">CONSISTENT</a>
}</td></tr>
<tr class="separator:ac612908684032ffe76ad97f04afd0ca8 inherit pub_types_classSAT_1_1DPLLT"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="inherit_header pro_attribs_classSAT_1_1DPLLT"><td colspan="2" onclick="javascript:toggleInherit('pro_attribs_classSAT_1_1DPLLT')"><img src="closed.png" alt="-"/> Protected Attributes inherited from <a class="el" href="classSAT_1_1DPLLT.html">SAT::DPLLT</a></td></tr>
<tr class="memitem:aafa21967afbd30f8c18ebc9f6c37bfa9 inherit pro_attribs_classSAT_1_1DPLLT"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html">TheoryAPI</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLT.html#aafa21967afbd30f8c18ebc9f6c37bfa9">d_theoryAPI</a></td></tr>
<tr class="separator:aafa21967afbd30f8c18ebc9f6c37bfa9 inherit pro_attribs_classSAT_1_1DPLLT"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aebea99801d1e6b690feb9610403f1162 inherit pro_attribs_classSAT_1_1DPLLT"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classSAT_1_1DPLLT_1_1Decider.html">Decider</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLT.html#aebea99801d1e6b690feb9610403f1162">d_decider</a></td></tr>
<tr class="separator:aebea99801d1e6b690feb9610403f1162 inherit pro_attribs_classSAT_1_1DPLLT"><td class="memSeparator" colspan="2"> </td></tr>
</table>
<a name="details" id="details"></a><h2 class="groupheader">Detailed Description</h2>
<div class="textblock">
<p>Definition at line <a class="el" href="dpllt__basic_8h_source.html#l00032">32</a> of file <a class="el" href="dpllt__basic_8h_source.html">dpllt_basic.h</a>.</p>
</div><h2 class="groupheader">Constructor & Destructor Documentation</h2>
<a class="anchor" id="a11ff82c567a310525206ba0260fbde5e"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">DPLLTBasic::DPLLTBasic </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html">TheoryAPI</a> * </td>
<td class="paramname"><em>theoryAPI</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classSAT_1_1DPLLT_1_1Decider.html">Decider</a> * </td>
<td class="paramname"><em>decider</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ContextManager.html">CVC3::ContextManager</a> * </td>
<td class="paramname"><em>cm</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>printStats</em> = <code>false</code> </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="dpllt__basic_8cpp_source.html#l00239">239</a> of file <a class="el" href="dpllt__basic_8cpp_source.html">dpllt_basic.cpp</a>.</p>
<p>References <a class="el" href="dpllt__basic_8cpp_source.html#l00137">createManager()</a>, <a class="el" href="dpllt__basic_8h_source.html#l00039">d_assertions</a>, <a class="el" href="dpllt__basic_8h_source.html#l00034">d_cm</a>, <a class="el" href="dpllt__basic_8h_source.html#l00038">d_cnf</a>, and <a class="el" href="context_8h_source.html#l00406">CVC3::ContextManager::getCurrentContext()</a>.</p>
</div>
</div>
<a class="anchor" id="a080afc4433840fd154465360ec97ca2b"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">DPLLTBasic::~DPLLTBasic </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__basic_8cpp_source.html#l00254">254</a> of file <a class="el" href="dpllt__basic_8cpp_source.html">dpllt_basic.cpp</a>.</p>
<p>References <a class="el" href="dpllt__basic_8h_source.html#l00039">d_assertions</a>, <a class="el" href="dpllt__basic_8h_source.html#l00043">d_assertionsStack</a>, <a class="el" href="dpllt__basic_8h_source.html#l00038">d_cnf</a>, <a class="el" href="dpllt__basic_8h_source.html#l00042">d_cnfStack</a>, <a class="el" href="dpllt__basic_8h_source.html#l00037">d_mng</a>, and <a class="el" href="dpllt__basic_8h_source.html#l00041">d_mngStack</a>.</p>
</div>
</div>
<h2 class="groupheader">Member Function Documentation</h2>
<a class="anchor" id="a082ff0d184786dbd60a400320dbc826a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void DPLLTBasic::createManager </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__basic_8cpp_source.html#l00137">137</a> of file <a class="el" href="dpllt__basic_8cpp_source.html">dpllt_basic.cpp</a>.</p>
<p>References <a class="el" href="sat__api_8cpp_source.html#l00015">SatSolver::Create()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00098">SATAssignmentHook()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00050">SATDecisionHook()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00117">SATDeductionHook()</a>, and <a class="el" href="dpllt__basic_8cpp_source.html#l00035">SATDLevelHook()</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00396">checkSat()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00472">continueCheck()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00239">DPLLTBasic()</a>, and <a class="el" href="dpllt__basic_8cpp_source.html#l00324">pop()</a>.</p>
</div>
</div>
<a class="anchor" id="a744ab3115b0c945843cc1310d06280b3"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void DPLLTBasic::generate_CDB </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1CNF__Formula__Impl.html">CNF_Formula_Impl</a> & </td>
<td class="paramname"><em>cnf</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__basic_8cpp_source.html#l00147">147</a> of file <a class="el" href="dpllt__basic_8cpp_source.html">dpllt_basic.cpp</a>.</p>
<p>References <a class="el" href="cnf_8h_source.html#l00158">SAT::CNF_Formula_Impl::begin()</a>, <a class="el" href="cnf_8h_source.html#l00159">SAT::CNF_Formula_Impl::end()</a>, <a class="el" href="cnf_8h_source.html#l00160">SAT::CNF_Formula_Impl::numVars()</a>, and <a class="el" href="cnf_8cpp_source.html#l00153">SAT::CNF_Formula_Impl::simplify()</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00289">addNewClauses()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00396">checkSat()</a>, and <a class="el" href="dpllt__basic_8cpp_source.html#l00472">continueCheck()</a>.</p>
</div>
</div>
<a class="anchor" id="aa41a72c436f5faf03128d53bc4e3f9ef"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void DPLLTBasic::handle_result </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53">SatSolver::SATStatus</a> </td>
<td class="paramname"><em>outcome</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__basic_8cpp_source.html#l00170">170</a> of file <a class="el" href="dpllt__basic_8cpp_source.html">dpllt_basic.cpp</a>.</p>
<p>References <a class="el" href="sat__api_8h_source.html#l00030">SatSolver::BUDGET_EXCEEDED</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="sat__api_8h_source.html#l00031">SatSolver::OUT_OF_MEMORY</a>, <a class="el" href="sat__api_8h_source.html#l00029">SatSolver::SATISFIABLE</a>, and <a class="el" href="sat__api_8h_source.html#l00028">SatSolver::UNSATISFIABLE</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00396">checkSat()</a>, and <a class="el" href="dpllt__basic_8cpp_source.html#l00472">continueCheck()</a>.</p>
</div>
</div>
<a class="anchor" id="a1340aa7926370e1bc90d1da906eb8e79"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void DPLLTBasic::verify_solution </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__basic_8cpp_source.html#l00215">215</a> of file <a class="el" href="dpllt__basic_8cpp_source.html">dpllt_basic.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, and <a class="el" href="sat__api_8h_source.html#l00071">SatSolver::Clause::IsNull()</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00396">checkSat()</a>, and <a class="el" href="dpllt__basic_8cpp_source.html#l00472">continueCheck()</a>.</p>
</div>
</div>
<a class="anchor" id="abfe1c680e074676f0f291125e7eb150e"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void DPLLTBasic::addNewClause </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classSAT_1_1Clause.html">Clause</a> & </td>
<td class="paramname"><em>c</em></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__basic_8cpp_source.html#l00275">275</a> of file <a class="el" href="dpllt__basic_8cpp_source.html">dpllt_basic.cpp</a>.</p>
<p>References <a class="el" href="classSatSolver.html#a1fb269f00fd9da8242e2bad01967f097">SatSolver::AddClause()</a>, <a class="el" href="cnf_8h_source.html#l00093">SAT::Clause::begin()</a>, <a class="el" href="dpllt__basic_8h_source.html#l00064">cvc2SAT()</a>, <a class="el" href="dpllt__basic_8h_source.html#l00037">d_mng</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="cnf_8h_source.html#l00094">SAT::Clause::end()</a>, <a class="el" href="cnf_8cpp_source.html#l00030">SAT::Clause::getMaxVar()</a>, <a class="el" href="classSatSolver.html#a75ac3919b9d2794bd2443e32bb1f29fd">SatSolver::NumVariables()</a>, <a class="el" href="dpllt__basic_8h_source.html#l00073">satSolver()</a>, and <a class="el" href="cnf_8h_source.html#l00097">SAT::Clause::size()</a>.</p>
</div>
</div>
<a class="anchor" id="acc013b97f0368bc1ca43cf374f06521c"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void DPLLTBasic::addNewClauses </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1CNF__Formula__Impl.html">CNF_Formula_Impl</a> & </td>
<td class="paramname"><em>cnf</em></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__basic_8cpp_source.html#l00289">289</a> of file <a class="el" href="dpllt__basic_8cpp_source.html">dpllt_basic.cpp</a>.</p>
<p>References <a class="el" href="classSatSolver.html#a1fb269f00fd9da8242e2bad01967f097">SatSolver::AddClause()</a>, <a class="el" href="classSatSolver.html#acf0e4f44556b7cfcea37100f92962fee">SatSolver::AddVariables()</a>, <a class="el" href="cnf_8h_source.html#l00158">SAT::CNF_Formula_Impl::begin()</a>, <a class="el" href="dpllt__basic_8h_source.html#l00064">cvc2SAT()</a>, <a class="el" href="dpllt__basic_8h_source.html#l00037">d_mng</a>, <a class="el" href="cnf_8h_source.html#l00159">SAT::CNF_Formula_Impl::end()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00147">generate_CDB()</a>, <a class="el" href="classSatSolver.html#a75ac3919b9d2794bd2443e32bb1f29fd">SatSolver::NumVariables()</a>, <a class="el" href="cnf_8h_source.html#l00160">SAT::CNF_Formula_Impl::numVars()</a>, and <a class="el" href="cnf_8cpp_source.html#l00153">SAT::CNF_Formula_Impl::simplify()</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00098">SATAssignmentHook()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00050">SATDecisionHook()</a>, and <a class="el" href="dpllt__basic_8cpp_source.html#l00117">SATDeductionHook()</a>.</p>
</div>
</div>
<a class="anchor" id="a96c27b95e07e062a16beb412f68608a1"></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="unionSatSolver_1_1Lit.html">SatSolver::Lit</a> SAT::DPLLTBasic::cvc2SAT </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1Lit.html">Lit</a> </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="dpllt__basic_8h_source.html#l00064">64</a> of file <a class="el" href="dpllt__basic_8h_source.html">dpllt_basic.h</a>.</p>
<p>References <a class="el" href="dpllt__basic_8h_source.html#l00037">d_mng</a>, <a class="el" href="cnf_8h_source.html#l00070">SAT::Lit::getVar()</a>, <a class="el" href="classSatSolver.html#aebeecffca634f23d8c9b941b44b4cfe7">SatSolver::GetVar()</a>, <a class="el" href="cnf_8h_source.html#l00063">SAT::Lit::isNull()</a>, <a class="el" href="cnf_8h_source.html#l00064">SAT::Lit::isPositive()</a>, and <a class="el" href="classSatSolver.html#a66bbef74a05f145e477adf37a1e1d116">SatSolver::MakeLit()</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00275">addNewClause()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00289">addNewClauses()</a>, and <a class="el" href="dpllt__basic_8cpp_source.html#l00050">SATDecisionHook()</a>.</p>
</div>
</div>
<a class="anchor" id="ad9ce5fbf4bb808f859d6aae48bfb07db"></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">Lit</a> SAT::DPLLTBasic::SAT2cvc </td>
<td>(</td>
<td class="paramtype"><a class="el" href="unionSatSolver_1_1Lit.html">SatSolver::Lit</a> </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="dpllt__basic_8h_source.html#l00068">68</a> of file <a class="el" href="dpllt__basic_8h_source.html">dpllt_basic.h</a>.</p>
<p>References <a class="el" href="dpllt__basic_8h_source.html#l00037">d_mng</a>, <a class="el" href="classSatSolver.html#a7187c85c8fc08c253b97de67509af3f2">SatSolver::GetPhaseFromLit()</a>, <a class="el" href="classSatSolver.html#a505146a1fb5715620935ec31f909932f">SatSolver::GetVarFromLit()</a>, <a class="el" href="classSatSolver.html#a78a8661d31ba8f3aca7e4c73a84f0bcf">SatSolver::GetVarIndex()</a>, and <a class="el" href="sat__api_8h_source.html#l00063">SatSolver::Lit::IsNull()</a>.</p>
</div>
</div>
<a class="anchor" id="a0a36ed4b453c94678f0fbbc380a7d3fd"></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="classSatSolver.html">SatSolver</a>* SAT::DPLLTBasic::satSolver </td>
<td>(</td>
<td class="paramname"></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="dpllt__basic_8h_source.html#l00073">73</a> of file <a class="el" href="dpllt__basic_8h_source.html">dpllt_basic.h</a>.</p>
<p>References <a class="el" href="dpllt__basic_8h_source.html#l00037">d_mng</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00275">addNewClause()</a>, and <a class="el" href="dpllt__basic_8cpp_source.html#l00098">SATAssignmentHook()</a>.</p>
</div>
</div>
<a class="anchor" id="a8c8f7e178849aead6754e44e3e63dc0c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void DPLLTBasic::push </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Set a checkpoint for backtracking. </p>
<p>This should effectively save the current state of the solver. Note that it should also result in a call to <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a771e84ea6308cb7d3f7d02e7858b37db" title="Set a checkpoint for backtracking.">TheoryAPI::push</a>. </p>
<p>Implements <a class="el" href="classSAT_1_1DPLLT.html#aa074d69f0937b579b5f6cfefabadd083">SAT::DPLLT</a>.</p>
<p>Definition at line <a class="el" href="dpllt__basic_8cpp_source.html#l00314">314</a> of file <a class="el" href="dpllt__basic_8cpp_source.html">dpllt_basic.cpp</a>.</p>
<p>References <a class="el" href="dpllt__basic_8h_source.html#l00043">d_assertionsStack</a>, <a class="el" href="dpllt__basic_8h_source.html#l00041">d_mngStack</a>, <a class="el" href="dpllt__basic_8h_source.html#l00049">d_prevAStackSize</a>, <a class="el" href="dpllt__basic_8h_source.html#l00048">d_prevStackSize</a>, <a class="el" href="dpllt__basic_8h_source.html#l00046">d_pushLevel</a>, <a class="el" href="dpllt__basic_8h_source.html#l00036">d_ready</a>, <a class="el" href="dpllt__basic_8h_source.html#l00047">d_readyPrev</a>, <a class="el" href="dpllt_8h_source.html#l00104">SAT::DPLLT::d_theoryAPI</a>, and <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a771e84ea6308cb7d3f7d02e7858b37db">SAT::DPLLT::TheoryAPI::push()</a>.</p>
</div>
</div>
<a class="anchor" id="aff5dbd3c2a47f003d7b388a8b673cc85"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void DPLLTBasic::pop </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Restore checkpoint. </p>
<p>This should return the state to what it was immediately before the last call to push. In particular, if one or more calls to checkSat, continueCheck, or addAssertion have been made since the last push, these should be undone. Note also that in this case, a single call to <a class="el" href="classSAT_1_1DPLLT.html#a59925cdeed3751c4fe4b5d759ebd755c" title="Restore checkpoint.">DPLLT::pop</a> may result in multiple calls to <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a51a08aab04c2185513676a316aee14b4" title="Restore most recent checkpoint.">TheoryAPI::pop</a>. </p>
<p>Implements <a class="el" href="classSAT_1_1DPLLT.html#a59925cdeed3751c4fe4b5d759ebd755c">SAT::DPLLT</a>.</p>
<p>Definition at line <a class="el" href="dpllt__basic_8cpp_source.html#l00324">324</a> of file <a class="el" href="dpllt__basic_8cpp_source.html">dpllt_basic.cpp</a>.</p>
<p>References <a class="el" href="dpllt__basic_8cpp_source.html#l00137">createManager()</a>, <a class="el" href="dpllt__basic_8h_source.html#l00039">d_assertions</a>, <a class="el" href="dpllt__basic_8h_source.html#l00043">d_assertionsStack</a>, <a class="el" href="dpllt__basic_8h_source.html#l00038">d_cnf</a>, <a class="el" href="dpllt__basic_8h_source.html#l00042">d_cnfStack</a>, <a class="el" href="dpllt__basic_8h_source.html#l00037">d_mng</a>, <a class="el" href="dpllt__basic_8h_source.html#l00041">d_mngStack</a>, <a class="el" href="dpllt__basic_8h_source.html#l00049">d_prevAStackSize</a>, <a class="el" href="dpllt__basic_8h_source.html#l00048">d_prevStackSize</a>, <a class="el" href="dpllt__basic_8h_source.html#l00046">d_pushLevel</a>, <a class="el" href="dpllt__basic_8h_source.html#l00036">d_ready</a>, <a class="el" href="dpllt__basic_8h_source.html#l00047">d_readyPrev</a>, <a class="el" href="dpllt_8h_source.html#l00104">SAT::DPLLT::d_theoryAPI</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, and <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a51a08aab04c2185513676a316aee14b4">SAT::DPLLT::TheoryAPI::pop()</a>.</p>
</div>
</div>
<a class="anchor" id="afaffe075e05bcd2e56aeede2154e0d5a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void DPLLTBasic::addAssertion </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a> & </td>
<td class="paramname"><em>cnf</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Add new clauses to the <a class="el" href="namespaceSAT.html">SAT</a> solver. </p>
<p>This is used to add clauses that form a "context" for the next call to checkSat </p>
<p>Implements <a class="el" href="classSAT_1_1DPLLT.html#aaaa6884de9ebd8b9596e85167e8f9273">SAT::DPLLT</a>.</p>
<p>Definition at line <a class="el" href="dpllt__basic_8cpp_source.html#l00379">379</a> of file <a class="el" href="dpllt__basic_8cpp_source.html">dpllt_basic.cpp</a>.</p>
<p>References <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a3b3ef70567e0298cd3e971fd57d26fa6">SAT::DPLLT::TheoryAPI::assertLit()</a>, <a class="el" href="classSAT_1_1CNF__Formula.html#a69dfc94796b23b6913c44a4d6d60f0d8">SAT::CNF_Formula::begin()</a>, <a class="el" href="dpllt_8h_source.html#l00104">SAT::DPLLT::d_theoryAPI</a>, and <a class="el" href="classSAT_1_1CNF__Formula.html#a6631cf3c5a6938f655360f7f63522b79">SAT::CNF_Formula::end()</a>.</p>
</div>
</div>
<a class="anchor" id="a4047558a5e4a9e84b81e388b220d4e79"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">std::vector< <a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> > DPLLTBasic::getCurAssignments </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implements <a class="el" href="classSAT_1_1DPLLT.html#a46312fb7854ac482f28c28564f83494d">SAT::DPLLT</a>.</p>
<p>Definition at line <a class="el" href="dpllt__basic_8cpp_source.html#l00368">368</a> of file <a class="el" href="dpllt__basic_8cpp_source.html">dpllt_basic.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="abaf2763764a68c9e4fbc190953b4e6c8"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">std::vector< std::vector< <a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> > > DPLLTBasic::getCurClauses </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implements <a class="el" href="classSAT_1_1DPLLT.html#ac73560398ae2ae153d318b53d37c7c71">SAT::DPLLT</a>.</p>
<p>Definition at line <a class="el" href="dpllt__basic_8cpp_source.html#l00373">373</a> of file <a class="el" href="dpllt__basic_8cpp_source.html">dpllt_basic.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="a195fdfa1972c882fd3d87eae0742c7ac"></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="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> DPLLTBasic::checkSat </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a> & </td>
<td class="paramname"><em>cnf</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Check the satisfiability of a set of clauses in the current context. </p>
<p>If the result is SATISFIABLE, UNKNOWN, or ABORT, the <a class="el" href="classSAT_1_1DPLLT.html">DPLLT</a> engine should remain in the state it is in until <a class="el" href="classSAT_1_1DPLLTBasic.html#aff5dbd3c2a47f003d7b388a8b673cc85" title="Restore checkpoint.">pop()</a> is called. If the result is UNSATISFIABLE, the <a class="el" href="classSAT_1_1DPLLT.html">DPLLT</a> engine should return to the state it was in when called. Note that it should be possible to call checkSat multiple times, even if the result is true (each additional call should use the context left by the previous call). </p>
<p>Implements <a class="el" href="classSAT_1_1DPLLT.html#a245df0d49bda0e9bdf69a1153e0d76be">SAT::DPLLT</a>.</p>
<p>Definition at line <a class="el" href="dpllt__basic_8cpp_source.html#l00396">396</a> of file <a class="el" href="dpllt__basic_8cpp_source.html">dpllt_basic.cpp</a>.</p>
<p>References <a class="el" href="queryresult_8h_source.html#l00037">CVC3::ABORT</a>, <a class="el" href="cnf_8h_source.html#l00134">SAT::CNF_Formula::addLiteral()</a>, <a class="el" href="sat__api_8h_source.html#l00030">SatSolver::BUDGET_EXCEEDED</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00137">createManager()</a>, <a class="el" href="dpllt__basic_8h_source.html#l00039">d_assertions</a>, <a class="el" href="dpllt__basic_8h_source.html#l00043">d_assertionsStack</a>, <a class="el" href="dpllt__basic_8h_source.html#l00034">d_cm</a>, <a class="el" href="dpllt__basic_8h_source.html#l00038">d_cnf</a>, <a class="el" href="dpllt__basic_8h_source.html#l00042">d_cnfStack</a>, <a class="el" href="dpllt__basic_8h_source.html#l00037">d_mng</a>, <a class="el" href="dpllt__basic_8h_source.html#l00041">d_mngStack</a>, <a class="el" href="dpllt__basic_8h_source.html#l00036">d_ready</a>, <a class="el" href="dpllt_8h_source.html#l00104">SAT::DPLLT::d_theoryAPI</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00147">generate_CDB()</a>, <a class="el" href="context_8h_source.html#l00406">CVC3::ContextManager::getCurrentContext()</a>, <a class="el" href="classSatSolver.html#aebeecffca634f23d8c9b941b44b4cfe7">SatSolver::GetVar()</a>, <a class="el" href="classSatSolver.html#a111b3a56be2feaae62bc57483f0aa9bf">SatSolver::GetVarAssignment()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00170">handle_result()</a>, <a class="el" href="cnf_8cpp_source.html#l00137">SAT::CNF_Formula_Impl::newClause()</a>, <a class="el" href="cnf_8h_source.html#l00186">SAT::CD_CNF_Formula::numClauses()</a>, <a class="el" href="classSatSolver.html#a75ac3919b9d2794bd2443e32bb1f29fd">SatSolver::NumVariables()</a>, <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a51a08aab04c2185513676a316aee14b4">SAT::DPLLT::TheoryAPI::pop()</a>, <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a771e84ea6308cb7d3f7d02e7858b37db">SAT::DPLLT::TheoryAPI::push()</a>, <a class="el" href="sat__api_8h_source.html#l00029">SatSolver::SATISFIABLE</a>, <a class="el" href="xchaff__solver_8h_source.html#l00055">SATISFIABLE</a>, <a class="el" href="classSatSolver.html#a0dfc1321f3446be70349f35881144433">SatSolver::Satisfiable()</a>, <a class="el" href="dpllt_8h_source.html#l00117">SAT::DPLLT::theoryAPI()</a>, <a class="el" href="sat__api_8h_source.html#l00028">SatSolver::UNSATISFIABLE</a>, <a class="el" href="xchaff__solver_8h_source.html#l00054">UNSATISFIABLE</a>, and <a class="el" href="dpllt__basic_8cpp_source.html#l00215">verify_solution()</a>.</p>
</div>
</div>
<a class="anchor" id="a1271494f0f1f6e9c249d8fce8418ecd7"></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="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> DPLLTBasic::continueCheck </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a> & </td>
<td class="paramname"><em>cnf</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Continue checking the last check with additional constraints. </p>
<p>Should only be called after a previous call to checkSat (or continueCheck) that returned SATISFIABLE. It should add the clauses in cnf to the existing clause database and search for a satisfying assignment. As with checkSat, if the result is not UNSATISFIABLE, the <a class="el" href="classSAT_1_1DPLLT.html">DPLLT</a> engine should remain in the state containing the satisfiable assignment until <a class="el" href="classSAT_1_1DPLLTBasic.html#aff5dbd3c2a47f003d7b388a8b673cc85" title="Restore checkpoint.">pop()</a> is called. Similarly, if the result is UNSATISFIABLE, the <a class="el" href="classSAT_1_1DPLLT.html">DPLLT</a> engine should return to the state it was in when checkSat was last called. </p>
<p>Implements <a class="el" href="classSAT_1_1DPLLT.html#a713db9fe798e2a9be337b8726540a24e">SAT::DPLLT</a>.</p>
<p>Definition at line <a class="el" href="dpllt__basic_8cpp_source.html#l00472">472</a> of file <a class="el" href="dpllt__basic_8cpp_source.html">dpllt_basic.cpp</a>.</p>
<p>References <a class="el" href="queryresult_8h_source.html#l00037">CVC3::ABORT</a>, <a class="el" href="sat__api_8h_source.html#l00030">SatSolver::BUDGET_EXCEEDED</a>, <a class="el" href="classSatSolver.html#ab4e73333fbc4b4372a18c66a40d4757f">SatSolver::Continue()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00137">createManager()</a>, <a class="el" href="dpllt__basic_8h_source.html#l00039">d_assertions</a>, <a class="el" href="dpllt__basic_8h_source.html#l00038">d_cnf</a>, <a class="el" href="dpllt__basic_8h_source.html#l00042">d_cnfStack</a>, <a class="el" href="dpllt__basic_8h_source.html#l00037">d_mng</a>, <a class="el" href="dpllt__basic_8h_source.html#l00041">d_mngStack</a>, <a class="el" href="dpllt__basic_8h_source.html#l00036">d_ready</a>, <a class="el" href="dpllt_8h_source.html#l00104">SAT::DPLLT::d_theoryAPI</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00147">generate_CDB()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00170">handle_result()</a>, <a class="el" href="cnf_8h_source.html#l00186">SAT::CD_CNF_Formula::numClauses()</a>, <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a51a08aab04c2185513676a316aee14b4">SAT::DPLLT::TheoryAPI::pop()</a>, <a class="el" href="sat__api_8h_source.html#l00029">SatSolver::SATISFIABLE</a>, <a class="el" href="xchaff__solver_8h_source.html#l00055">SATISFIABLE</a>, <a class="el" href="dpllt_8h_source.html#l00117">SAT::DPLLT::theoryAPI()</a>, <a class="el" href="sat__api_8h_source.html#l00028">SatSolver::UNSATISFIABLE</a>, <a class="el" href="xchaff__solver_8h_source.html#l00054">UNSATISFIABLE</a>, and <a class="el" href="dpllt__basic_8cpp_source.html#l00215">verify_solution()</a>.</p>
</div>
</div>
<a class="anchor" id="ab0eac02c714ede751cf48fb188e375f6"></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#ac9cf10f19f5f4d86ad539777fd8ca5ae">Var::Val</a> SAT::DPLLTBasic::getValue </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1Var.html">Var</a> </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 class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Get value of variable: unassigned, false, or true. </p>
<p>Implements <a class="el" href="classSAT_1_1DPLLT.html#a961364ed0ea77af61dbabd7a3a07670c">SAT::DPLLT</a>.</p>
<p>Definition at line <a class="el" href="dpllt__basic_8h_source.html#l00085">85</a> of file <a class="el" href="dpllt__basic_8h_source.html">dpllt_basic.h</a>.</p>
<p>References <a class="el" href="dpllt__basic_8h_source.html#l00037">d_mng</a>, <a class="el" href="classSatSolver.html#aebeecffca634f23d8c9b941b44b4cfe7">SatSolver::GetVar()</a>, and <a class="el" href="classSatSolver.html#a111b3a56be2feaae62bc57483f0aa9bf">SatSolver::GetVarAssignment()</a>.</p>
</div>
</div>
<a class="anchor" id="a0c4e0f09aacb6791929ac0eb6e6662c0"></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="classCVC3_1_1Proof.html">CVC3::Proof</a> DPLLTBasic::getSatProof </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1CNF__Manager.html">CNF_Manager</a> * </td>
<td class="paramname">, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoryCore.html">CVC3::TheoryCore</a> * </td>
<td class="paramname"> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Get the proof from <a class="el" href="namespaceSAT.html">SAT</a> engine. </p>
<p>Implements <a class="el" href="classSAT_1_1DPLLT.html#ada559a7b19d3dfe82acfa084b8b634ad">SAT::DPLLT</a>.</p>
<p>Definition at line <a class="el" href="dpllt__basic_8cpp_source.html#l00522">522</a> of file <a class="el" href="dpllt__basic_8cpp_source.html">dpllt_basic.cpp</a>.</p>
</div>
</div>
<h2 class="groupheader">Member Data Documentation</h2>
<a class="anchor" id="a9e8593063e800cb17793629543493624"></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="classCVC3_1_1ContextManager.html">CVC3::ContextManager</a>* SAT::DPLLTBasic::d_cm</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__basic_8h_source.html#l00034">34</a> of file <a class="el" href="dpllt__basic_8h_source.html">dpllt_basic.h</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00396">checkSat()</a>, and <a class="el" href="dpllt__basic_8cpp_source.html#l00239">DPLLTBasic()</a>.</p>
</div>
</div>
<a class="anchor" id="af53a2ee63b573d7ddd70395cc58fab6a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool SAT::DPLLTBasic::d_ready</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__basic_8h_source.html#l00036">36</a> of file <a class="el" href="dpllt__basic_8h_source.html">dpllt_basic.h</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00396">checkSat()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00472">continueCheck()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00324">pop()</a>, and <a class="el" href="dpllt__basic_8cpp_source.html#l00314">push()</a>.</p>
</div>
</div>
<a class="anchor" id="a21ec19cee9ab93b7cda66d209dd6e676"></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="classSatSolver.html">SatSolver</a>* SAT::DPLLTBasic::d_mng</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__basic_8h_source.html#l00037">37</a> of file <a class="el" href="dpllt__basic_8h_source.html">dpllt_basic.h</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00275">addNewClause()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00289">addNewClauses()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00396">checkSat()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00472">continueCheck()</a>, <a class="el" href="dpllt__basic_8h_source.html#l00064">cvc2SAT()</a>, <a class="el" href="dpllt__basic_8h_source.html#l00085">getValue()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00324">pop()</a>, <a class="el" href="dpllt__basic_8h_source.html#l00068">SAT2cvc()</a>, <a class="el" href="dpllt__basic_8h_source.html#l00073">satSolver()</a>, and <a class="el" href="dpllt__basic_8cpp_source.html#l00254">~DPLLTBasic()</a>.</p>
</div>
</div>
<a class="anchor" id="a191c0c9c76c2ab5a37038c32a7c6ab58"></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_1CNF__Formula__Impl.html">CNF_Formula_Impl</a>* SAT::DPLLTBasic::d_cnf</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__basic_8h_source.html#l00038">38</a> of file <a class="el" href="dpllt__basic_8h_source.html">dpllt_basic.h</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00396">checkSat()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00472">continueCheck()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00239">DPLLTBasic()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00324">pop()</a>, and <a class="el" href="dpllt__basic_8cpp_source.html#l00254">~DPLLTBasic()</a>.</p>
</div>
</div>
<a class="anchor" id="a6032bad91260ee1c03ed4553425d6cf9"></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_1CD__CNF__Formula.html">CD_CNF_Formula</a>* SAT::DPLLTBasic::d_assertions</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__basic_8h_source.html#l00039">39</a> of file <a class="el" href="dpllt__basic_8h_source.html">dpllt_basic.h</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00396">checkSat()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00472">continueCheck()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00239">DPLLTBasic()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00324">pop()</a>, and <a class="el" href="dpllt__basic_8cpp_source.html#l00254">~DPLLTBasic()</a>.</p>
</div>
</div>
<a class="anchor" id="aba339d2d7e2f5ed7bf1367e497e73087"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">std::vector<<a class="el" href="classSatSolver.html">SatSolver</a>*> SAT::DPLLTBasic::d_mngStack</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__basic_8h_source.html#l00041">41</a> of file <a class="el" href="dpllt__basic_8h_source.html">dpllt_basic.h</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00396">checkSat()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00472">continueCheck()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00324">pop()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00314">push()</a>, and <a class="el" href="dpllt__basic_8cpp_source.html#l00254">~DPLLTBasic()</a>.</p>
</div>
</div>
<a class="anchor" id="a423ff42fd5ccad2be5f8dd97654e9a81"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">std::vector<<a class="el" href="classSAT_1_1CNF__Formula__Impl.html">CNF_Formula_Impl</a>*> SAT::DPLLTBasic::d_cnfStack</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__basic_8h_source.html#l00042">42</a> of file <a class="el" href="dpllt__basic_8h_source.html">dpllt_basic.h</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00396">checkSat()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00472">continueCheck()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00324">pop()</a>, and <a class="el" href="dpllt__basic_8cpp_source.html#l00254">~DPLLTBasic()</a>.</p>
</div>
</div>
<a class="anchor" id="a4194dcc23968652060be41902ca5b376"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">std::vector<<a class="el" href="classSAT_1_1CD__CNF__Formula.html">CD_CNF_Formula</a>*> SAT::DPLLTBasic::d_assertionsStack</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__basic_8h_source.html#l00043">43</a> of file <a class="el" href="dpllt__basic_8h_source.html">dpllt_basic.h</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00396">checkSat()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00324">pop()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00314">push()</a>, and <a class="el" href="dpllt__basic_8cpp_source.html#l00254">~DPLLTBasic()</a>.</p>
</div>
</div>
<a class="anchor" id="a347d0b91280f484b5035505f148864e6"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool SAT::DPLLTBasic::d_printStats</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__basic_8h_source.html#l00044">44</a> of file <a class="el" href="dpllt__basic_8h_source.html">dpllt_basic.h</a>.</p>
</div>
</div>
<a class="anchor" id="ac1e928276774bc77063ee05aa2ceb078"></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="classCVC3_1_1CDO.html">CVC3::CDO</a><unsigned> SAT::DPLLTBasic::d_pushLevel</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__basic_8h_source.html#l00046">46</a> of file <a class="el" href="dpllt__basic_8h_source.html">dpllt_basic.h</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00324">pop()</a>, and <a class="el" href="dpllt__basic_8cpp_source.html#l00314">push()</a>.</p>
</div>
</div>
<a class="anchor" id="a04bf3fdf12271b364b22d40dc352f634"></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="classCVC3_1_1CDO.html">CVC3::CDO</a><bool> SAT::DPLLTBasic::d_readyPrev</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__basic_8h_source.html#l00047">47</a> of file <a class="el" href="dpllt__basic_8h_source.html">dpllt_basic.h</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00324">pop()</a>, and <a class="el" href="dpllt__basic_8cpp_source.html#l00314">push()</a>.</p>
</div>
</div>
<a class="anchor" id="ada4aa8a05927fc1ea334edea0b5f8fd3"></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="classCVC3_1_1CDO.html">CVC3::CDO</a><unsigned> SAT::DPLLTBasic::d_prevStackSize</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__basic_8h_source.html#l00048">48</a> of file <a class="el" href="dpllt__basic_8h_source.html">dpllt_basic.h</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00324">pop()</a>, and <a class="el" href="dpllt__basic_8cpp_source.html#l00314">push()</a>.</p>
</div>
</div>
<a class="anchor" id="a0bd6e3a5262667eed68fd59cf6c39551"></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="classCVC3_1_1CDO.html">CVC3::CDO</a><unsigned> SAT::DPLLTBasic::d_prevAStackSize</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__basic_8h_source.html#l00049">49</a> of file <a class="el" href="dpllt__basic_8h_source.html">dpllt_basic.h</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00324">pop()</a>, and <a class="el" href="dpllt__basic_8cpp_source.html#l00314">push()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="dpllt__basic_8h_source.html">dpllt_basic.h</a></li>
<li><a class="el" href="dpllt__basic_8cpp_source.html">dpllt_basic.cpp</a></li>
</ul>
</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>
