<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<title>CVC3: SAT::DPLLTMiniSat Class Reference</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><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="hierarchy.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_1DPLLTMiniSat.html">DPLLTMiniSat</a> </li>
</ul>
</div>
</div>
<div class="header">
<div class="summary">
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pro-methods">Protected Member Functions</a> |
<a href="#pro-attribs">Protected Attributes</a> </div>
<div class="headertitle">
<div class="title">SAT::DPLLTMiniSat Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="SAT::DPLLTMiniSat" --><!-- doxytag: inherits="SAT::DPLLT" -->
<p><code>#include <<a class="el" href="dpllt__minisat_8h_source.html">dpllt_minisat.h</a>></code></p>
<div class="dynheader">
Inheritance diagram for SAT::DPLLTMiniSat:</div>
<div class="dyncontent">
<div class="center">
<img src="classSAT_1_1DPLLTMiniSat.png" usemap="#SAT::DPLLTMiniSat_map" alt=""/>
<map id="SAT::DPLLTMiniSat_map" name="SAT::DPLLTMiniSat_map">
<area href="classSAT_1_1DPLLT.html" alt="SAT::DPLLT" shape="rect" coords="0,0,122,24"/>
</map>
</div></div>
<p><a href="classSAT_1_1DPLLTMiniSat-members.html">List of all members.</a></p>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li><a class="el" href="classSAT_1_1DPLLTMiniSat.html#a8845ef99231d4f4096f0254423aca649">DPLLTMiniSat</a> (<a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html">TheoryAPI</a> *theoryAPI, <a class="el" href="classSAT_1_1DPLLT_1_1Decider.html">Decider</a> *decider, bool printStats=false, bool createProof=false)
<li>virtual <a class="el" href="classSAT_1_1DPLLTMiniSat.html#ad95c622192084c6fb35d4a944b02a41f">~DPLLTMiniSat</a> ()
<li>virtual <a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">CVC3::QueryResult</a> <a class="el" href="classSAT_1_1DPLLTMiniSat.html#a51a36acb7b2ed49d97fa8d5524604604">checkSat</a> (const <a class="el" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a> &cnf)
<dl class="el"><dd class="mdescRight">Check the satisfiability of a set of clauses in the current context. <a href="#a51a36acb7b2ed49d97fa8d5524604604"></a><br/></dl><li>virtual <a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">CVC3::QueryResult</a> <a class="el" href="classSAT_1_1DPLLTMiniSat.html#aae7502914c5ca0708d0bd11ebc766d0a">continueCheck</a> (const <a class="el" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a> &cnf)
<dl class="el"><dd class="mdescRight">Continue checking the last check with additional constraints. <a href="#aae7502914c5ca0708d0bd11ebc766d0a"></a><br/></dl><li>virtual void <a class="el" href="classSAT_1_1DPLLTMiniSat.html#a169decc11aac46183d6213a2c6f12633">push</a> ()
<dl class="el"><dd class="mdescRight">Set a checkpoint for backtracking. <a href="#a169decc11aac46183d6213a2c6f12633"></a><br/></dl><li>virtual void <a class="el" href="classSAT_1_1DPLLTMiniSat.html#a6cf0c23d330fc8609323cb3dd8282377">pop</a> ()
<dl class="el"><dd class="mdescRight">Restore checkpoint. <a href="#a6cf0c23d330fc8609323cb3dd8282377"></a><br/></dl><li>virtual void <a class="el" href="classSAT_1_1DPLLTMiniSat.html#afdf7f3a5aa5eccf6c04ba4326567f0b9">addAssertion</a> (const <a class="el" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a> &cnf)
<dl class="el"><dd class="mdescRight">Add new clauses to the <a class="el" href="namespaceSAT.html">SAT</a> solver. <a href="#afdf7f3a5aa5eccf6c04ba4326567f0b9"></a><br/></dl><li>virtual std::vector< <a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> > <a class="el" href="classSAT_1_1DPLLTMiniSat.html#aae30c40897ec35d1a0485899865b723e">getCurAssignments</a> ()
<li>virtual std::vector<br class="typebreak"/>
< std::vector< <a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> > > <a class="el" href="classSAT_1_1DPLLTMiniSat.html#a1a19b6494dbc9bdd404e5917ee9eea24">getCurClauses</a> ()
<li>virtual <a class="el" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">Var::Val</a> <a class="el" href="classSAT_1_1DPLLTMiniSat.html#a06fd86d63383adc68d1ace6deb466175">getValue</a> (<a class="el" href="classSAT_1_1Var.html">Var</a> v)
<dl class="el"><dd class="mdescRight">Get value of variable: unassigned, false, or true. <a href="#a06fd86d63383adc68d1ace6deb466175"></a><br/></dl><li><a class="el" href="classSAT_1_1SatProof.html">SatProof</a> * <a class="el" href="classSAT_1_1DPLLTMiniSat.html#a679c7d58efef6a952128669e7fb7e493">getProof</a> ()
<li><a class="el" href="classCVC3_1_1Proof.html">CVC3::Proof</a> <a class="el" href="classSAT_1_1DPLLTMiniSat.html#ae465fc059c93948333a16b2c21a8828b">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> *)
<dl class="el"><dd class="mdescRight">Get the proof from <a class="el" href="namespaceSAT.html">SAT</a> engine. <a href="#ae465fc059c93948333a16b2c21a8828b"></a><br/></dl></ul>
<h2><a name="pro-methods"></a>
Protected Member Functions</h2>
<ul>
<li><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a> * <a class="el" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a> ()
<li>void <a class="el" href="classSAT_1_1DPLLTMiniSat.html#a2ee2582067c44520f4554de44ebec16a">pushSolver</a> ()
<li><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">CVC3::QueryResult</a> <a class="el" href="classSAT_1_1DPLLTMiniSat.html#a30d61595534052f920440688f5cec73b">search</a> ()
</ul>
<h2><a name="pro-attribs"></a>
Protected Attributes</h2>
<ul>
<li>bool <a class="el" href="classSAT_1_1DPLLTMiniSat.html#afa6ba4582477c902c7eb4d498c42882e">d_printStats</a>
<li>bool <a class="el" href="classSAT_1_1DPLLTMiniSat.html#ac6230604f45056b39c0869f05fe0ae7e">d_createProof</a>
<li><a class="el" href="classSAT_1_1SatProof.html">SatProof</a> * <a class="el" href="classSAT_1_1DPLLTMiniSat.html#a9eb24ce4c4b1a9f1dae868b18017f905">d_proof</a>
<li>std::stack< <a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a> * > <a class="el" href="classSAT_1_1DPLLTMiniSat.html#a36d133e42dbd9557434a166d1e97d050">d_solvers</a>
</ul>
<hr/><a name="details" id="details"></a><h2>Detailed Description</h2>
<div class="textblock">
<p>Definition at line <a class="el" href="dpllt__minisat_8h_source.html#l00040">40</a> of file <a class="el" href="dpllt__minisat_8h_source.html">dpllt_minisat.h</a>.</p>
</div><hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="a8845ef99231d4f4096f0254423aca649"></a><!-- doxytag: member="SAT::DPLLTMiniSat::DPLLTMiniSat" ref="a8845ef99231d4f4096f0254423aca649" args="(TheoryAPI *theoryAPI, Decider *decider, bool printStats=false, bool createProof=false)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">DPLLTMiniSat::DPLLTMiniSat </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">bool </td>
<td class="paramname"><em>printStats</em> = <code>false</code>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>createProof</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__minisat_8cpp_source.html#l00034">34</a> of file <a class="el" href="dpllt__minisat_8cpp_source.html">dpllt_minisat.cpp</a>.</p>
<p>References <a class="el" href="dpllt__minisat_8cpp_source.html#l00056">pushSolver()</a>.</p>
</div>
</div>
<a class="anchor" id="ad95c622192084c6fb35d4a944b02a41f"></a><!-- doxytag: member="SAT::DPLLTMiniSat::~DPLLTMiniSat" ref="ad95c622192084c6fb35d4a944b02a41f" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">DPLLTMiniSat::~DPLLTMiniSat </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__minisat_8cpp_source.html#l00041">41</a> of file <a class="el" href="dpllt__minisat_8cpp_source.html">dpllt_minisat.cpp</a>.</p>
<p>References <a class="el" href="dpllt__minisat_8h_source.html#l00055">d_proof</a>, and <a class="el" href="dpllt__minisat_8h_source.html#l00061">d_solvers</a>.</p>
</div>
</div>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="a19b4d9e00382a6b386ac51461f156785"></a><!-- doxytag: member="SAT::DPLLTMiniSat::getActiveSolver" ref="a19b4d9e00382a6b386ac51461f156785" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a> * DPLLTMiniSat::getActiveSolver </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__minisat_8cpp_source.html#l00050">50</a> of file <a class="el" href="dpllt__minisat_8cpp_source.html">dpllt_minisat.cpp</a>.</p>
<p>References <a class="el" href="dpllt__minisat_8h_source.html#l00061">d_solvers</a>, and <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>.</p>
<p>Referenced by <a class="el" href="dpllt__minisat_8cpp_source.html#l00223">addAssertion()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00131">checkSat()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00154">continueCheck()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00215">getCurAssignments()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00219">getCurClauses()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00244">getValue()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00192">pop()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00179">push()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00056">pushSolver()</a>, and <a class="el" href="dpllt__minisat_8cpp_source.html#l00065">search()</a>.</p>
</div>
</div>
<a class="anchor" id="a2ee2582067c44520f4554de44ebec16a"></a><!-- doxytag: member="SAT::DPLLTMiniSat::pushSolver" ref="a2ee2582067c44520f4554de44ebec16a" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void DPLLTMiniSat::pushSolver </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__minisat_8cpp_source.html#l00056">56</a> of file <a class="el" href="dpllt__minisat_8cpp_source.html">dpllt_minisat.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8cpp_source.html#l00248">MiniSat::Solver::createFrom()</a>, <a class="el" href="dpllt__minisat_8h_source.html#l00052">d_createProof</a>, <a class="el" href="dpllt_8h_source.html#l00105">SAT::DPLLT::d_decider</a>, <a class="el" href="dpllt__minisat_8h_source.html#l00061">d_solvers</a>, <a class="el" href="dpllt_8h_source.html#l00104">SAT::DPLLT::d_theoryAPI</a>, and <a class="el" href="dpllt__minisat_8cpp_source.html#l00050">getActiveSolver()</a>.</p>
<p>Referenced by <a class="el" href="dpllt__minisat_8cpp_source.html#l00223">addAssertion()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00131">checkSat()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00034">DPLLTMiniSat()</a>, and <a class="el" href="dpllt__minisat_8cpp_source.html#l00179">push()</a>.</p>
</div>
</div>
<a class="anchor" id="a30d61595534052f920440688f5cec73b"></a><!-- doxytag: member="SAT::DPLLTMiniSat::search" ref="a30d61595534052f920440688f5cec73b" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> DPLLTMiniSat::search </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__minisat_8cpp_source.html#l00065">65</a> of file <a class="el" href="dpllt__minisat_8cpp_source.html">dpllt_minisat.cpp</a>.</p>
<p>References <a class="el" href="queryresult_8h_source.html#l00037">CVC3::ABORT</a>, <a class="el" href="dpllt__minisat_8h_source.html#l00052">d_createProof</a>, <a class="el" href="dpllt__minisat_8h_source.html#l00047">d_printStats</a>, <a class="el" href="dpllt__minisat_8h_source.html#l00055">d_proof</a>, <a class="el" href="dpllt__minisat_8h_source.html#l00061">d_solvers</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="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00050">getActiveSolver()</a>, <a class="el" href="minisat__solver_8h_source.html#l00722">MiniSat::Solver::getClauses()</a>, <a class="el" href="minisat__solver_8h_source.html#l00725">MiniSat::Solver::getLemmas()</a>, <a class="el" href="minisat__solver_8h_source.html#l00736">MiniSat::Solver::getStats()</a>, <a class="el" href="minisat__solver_8h_source.html#l00749">MiniSat::Solver::nVars()</a>, <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a51a08aab04c2185513676a316aee14b4">SAT::DPLLT::TheoryAPI::pop()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00055">SATISFIABLE</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02005">MiniSat::Solver::search()</a>, <a class="el" href="xchaff__base_8h_source.html#l00048">UNKNOWN</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00054">UNSATISFIABLE</a>.</p>
<p>Referenced by <a class="el" href="dpllt__minisat_8cpp_source.html#l00131">checkSat()</a>, and <a class="el" href="dpllt__minisat_8cpp_source.html#l00154">continueCheck()</a>.</p>
</div>
</div>
<a class="anchor" id="a51a36acb7b2ed49d97fa8d5524604604"></a><!-- doxytag: member="SAT::DPLLTMiniSat::checkSat" ref="a51a36acb7b2ed49d97fa8d5524604604" args="(const CNF_Formula &cnf)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> DPLLTMiniSat::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><code> [virtual]</code></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_1DPLLTMiniSat.html#a6cf0c23d330fc8609323cb3dd8282377" 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__minisat_8cpp_source.html#l00131">131</a> of file <a class="el" href="dpllt__minisat_8cpp_source.html">dpllt_minisat.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8cpp_source.html#l00529">MiniSat::Solver::addFormula()</a>, <a class="el" href="dpllt__minisat_8h_source.html#l00061">d_solvers</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="minisat__solver_8cpp_source.html#l02630">MiniSat::Solver::doPops()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00050">getActiveSolver()</a>, <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a771e84ea6308cb7d3f7d02e7858b37db">SAT::DPLLT::TheoryAPI::push()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00056">pushSolver()</a>, and <a class="el" href="dpllt__minisat_8cpp_source.html#l00065">search()</a>.</p>
</div>
</div>
<a class="anchor" id="aae7502914c5ca0708d0bd11ebc766d0a"></a><!-- doxytag: member="SAT::DPLLTMiniSat::continueCheck" ref="aae7502914c5ca0708d0bd11ebc766d0a" args="(const CNF_Formula &cnf)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> DPLLTMiniSat::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><code> [virtual]</code></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_1DPLLTMiniSat.html#a6cf0c23d330fc8609323cb3dd8282377" 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__minisat_8cpp_source.html#l00154">154</a> of file <a class="el" href="dpllt__minisat_8cpp_source.html">dpllt_minisat.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8cpp_source.html#l00529">MiniSat::Solver::addFormula()</a>, <a class="el" href="dpllt__minisat_8h_source.html#l00061">d_solvers</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02630">MiniSat::Solver::doPops()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00050">getActiveSolver()</a>, <a class="el" href="minisat__solver_8h_source.html#l00692">MiniSat::Solver::inPush()</a>, and <a class="el" href="dpllt__minisat_8cpp_source.html#l00065">search()</a>.</p>
</div>
</div>
<a class="anchor" id="a169decc11aac46183d6213a2c6f12633"></a><!-- doxytag: member="SAT::DPLLTMiniSat::push" ref="a169decc11aac46183d6213a2c6f12633" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void DPLLTMiniSat::push </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [virtual]</code></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__minisat_8cpp_source.html#l00179">179</a> of file <a class="el" href="dpllt__minisat_8cpp_source.html">dpllt_minisat.cpp</a>.</p>
<p>References <a class="el" href="dpllt_8h_source.html#l00104">SAT::DPLLT::d_theoryAPI</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02630">MiniSat::Solver::doPops()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00050">getActiveSolver()</a>, <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a771e84ea6308cb7d3f7d02e7858b37db">SAT::DPLLT::TheoryAPI::push()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02510">MiniSat::Solver::push()</a>, and <a class="el" href="dpllt__minisat_8cpp_source.html#l00056">pushSolver()</a>.</p>
</div>
</div>
<a class="anchor" id="a6cf0c23d330fc8609323cb3dd8282377"></a><!-- doxytag: member="SAT::DPLLTMiniSat::pop" ref="a6cf0c23d330fc8609323cb3dd8282377" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void DPLLTMiniSat::pop </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [virtual]</code></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__minisat_8cpp_source.html#l00192">192</a> of file <a class="el" href="dpllt__minisat_8cpp_source.html">dpllt_minisat.cpp</a>.</p>
<p>References <a class="el" href="dpllt__minisat_8h_source.html#l00061">d_solvers</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__minisat_8cpp_source.html#l00050">getActiveSolver()</a>, <a class="el" href="minisat__solver_8h_source.html#l00692">MiniSat::Solver::inPush()</a>, <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a51a08aab04c2185513676a316aee14b4">SAT::DPLLT::TheoryAPI::pop()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02621">MiniSat::Solver::requestPop()</a>.</p>
</div>
</div>
<a class="anchor" id="afdf7f3a5aa5eccf6c04ba4326567f0b9"></a><!-- doxytag: member="SAT::DPLLTMiniSat::addAssertion" ref="afdf7f3a5aa5eccf6c04ba4326567f0b9" args="(const CNF_Formula &cnf)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void DPLLTMiniSat::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><code> [virtual]</code></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__minisat_8cpp_source.html#l00223">223</a> of file <a class="el" href="dpllt__minisat_8cpp_source.html">dpllt_minisat.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8cpp_source.html#l00529">MiniSat::Solver::addFormula()</a>, <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>, <a class="el" href="minisat__solver_8cpp_source.html#l02630">MiniSat::Solver::doPops()</a>, <a class="el" href="classSAT_1_1CNF__Formula.html#a6631cf3c5a6938f655360f7f63522b79">SAT::CNF_Formula::end()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00050">getActiveSolver()</a>, <a class="el" href="minisat__solver_8h_source.html#l00671">MiniSat::Solver::isConsistent()</a>, and <a class="el" href="dpllt__minisat_8cpp_source.html#l00056">pushSolver()</a>.</p>
</div>
</div>
<a class="anchor" id="aae30c40897ec35d1a0485899865b723e"></a><!-- doxytag: member="SAT::DPLLTMiniSat::getCurAssignments" ref="aae30c40897ec35d1a0485899865b723e" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector< <a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> > DPLLTMiniSat::getCurAssignments </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [virtual]</code></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__minisat_8cpp_source.html#l00215">215</a> of file <a class="el" href="dpllt__minisat_8cpp_source.html">dpllt_minisat.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8cpp_source.html#l00351">MiniSat::Solver::curAssigns()</a>, and <a class="el" href="dpllt__minisat_8cpp_source.html#l00050">getActiveSolver()</a>.</p>
</div>
</div>
<a class="anchor" id="a1a19b6494dbc9bdd404e5917ee9eea24"></a><!-- doxytag: member="SAT::DPLLTMiniSat::getCurClauses" ref="a1a19b6494dbc9bdd404e5917ee9eea24" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector< std::vector< <a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> > > DPLLTMiniSat::getCurClauses </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [virtual]</code></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__minisat_8cpp_source.html#l00219">219</a> of file <a class="el" href="dpllt__minisat_8cpp_source.html">dpllt_minisat.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8cpp_source.html#l00360">MiniSat::Solver::curClauses()</a>, and <a class="el" href="dpllt__minisat_8cpp_source.html#l00050">getActiveSolver()</a>.</p>
</div>
</div>
<a class="anchor" id="a06fd86d63383adc68d1ace6deb466175"></a><!-- doxytag: member="SAT::DPLLTMiniSat::getValue" ref="a06fd86d63383adc68d1ace6deb466175" args="(Var v)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">Var::Val</a> DPLLTMiniSat::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><code> [virtual]</code></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__minisat_8cpp_source.html#l00244">244</a> of file <a class="el" href="dpllt__minisat_8cpp_source.html">dpllt_minisat.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00128">MiniSat::cvcToMiniSat()</a>, <a class="el" href="dpllt__minisat_8h_source.html#l00061">d_solvers</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="formula__value_8h_source.html#l00033">CVC3::FALSE_VAL</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00050">getActiveSolver()</a>, <a class="el" href="minisat__solver_8h_source.html#l00699">MiniSat::Solver::getValue()</a>, <a class="el" href="minisat__global_8h_source.html#l00215">MiniSat::l_False</a>, <a class="el" href="minisat__global_8h_source.html#l00214">MiniSat::l_True</a>, <a class="el" href="formula__value_8h_source.html#l00032">CVC3::TRUE_VAL</a>, and <a class="el" href="xchaff__base_8h_source.html#l00048">UNKNOWN</a>.</p>
</div>
</div>
<a class="anchor" id="a679c7d58efef6a952128669e7fb7e493"></a><!-- doxytag: member="SAT::DPLLTMiniSat::getProof" ref="a679c7d58efef6a952128669e7fb7e493" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classSAT_1_1SatProof.html">SatProof</a>* SAT::DPLLTMiniSat::getProof </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__minisat_8h_source.html#l00099">99</a> of file <a class="el" href="dpllt__minisat_8h_source.html">dpllt_minisat.h</a>.</p>
<p>References <a class="el" href="dpllt__minisat_8h_source.html#l00055">d_proof</a>, and <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>.</p>
<p>Referenced by <a class="el" href="dpllt__minisat_8cpp_source.html#l00378">getSatProof()</a>.</p>
</div>
</div>
<a class="anchor" id="ae465fc059c93948333a16b2c21a8828b"></a><!-- doxytag: member="SAT::DPLLTMiniSat::getSatProof" ref="ae465fc059c93948333a16b2c21a8828b" args="(CNF_Manager *, CVC3::TheoryCore *)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Proof.html">CVC3::Proof</a> DPLLTMiniSat::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><code> [virtual]</code></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__minisat_8cpp_source.html#l00378">378</a> of file <a class="el" href="dpllt__minisat_8cpp_source.html">dpllt_minisat.cpp</a>.</p>
<p>References <a class="el" href="dpllt__minisat_8cpp_source.html#l00258">generateSatProof()</a>, <a class="el" href="dpllt__minisat_8h_source.html#l00099">getProof()</a>, <a class="el" href="sat__proof_8h_source.html#l00108">SAT::SatProof::getRoot()</a>, and <a class="el" href="theory__core_8h_source.html#l00349">CVC3::TheoryCore::getTM()</a>.</p>
</div>
</div>
<hr/><h2>Member Data Documentation</h2>
<a class="anchor" id="afa6ba4582477c902c7eb4d498c42882e"></a><!-- doxytag: member="SAT::DPLLTMiniSat::d_printStats" ref="afa6ba4582477c902c7eb4d498c42882e" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classSAT_1_1DPLLTMiniSat.html#afa6ba4582477c902c7eb4d498c42882e">SAT::DPLLTMiniSat::d_printStats</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__minisat_8h_source.html#l00047">47</a> of file <a class="el" href="dpllt__minisat_8h_source.html">dpllt_minisat.h</a>.</p>
<p>Referenced by <a class="el" href="dpllt__minisat_8cpp_source.html#l00065">search()</a>.</p>
</div>
</div>
<a class="anchor" id="ac6230604f45056b39c0869f05fe0ae7e"></a><!-- doxytag: member="SAT::DPLLTMiniSat::d_createProof" ref="ac6230604f45056b39c0869f05fe0ae7e" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classSAT_1_1DPLLTMiniSat.html#ac6230604f45056b39c0869f05fe0ae7e">SAT::DPLLTMiniSat::d_createProof</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__minisat_8h_source.html#l00052">52</a> of file <a class="el" href="dpllt__minisat_8h_source.html">dpllt_minisat.h</a>.</p>
<p>Referenced by <a class="el" href="dpllt__minisat_8cpp_source.html#l00056">pushSolver()</a>, and <a class="el" href="dpllt__minisat_8cpp_source.html#l00065">search()</a>.</p>
</div>
</div>
<a class="anchor" id="a9eb24ce4c4b1a9f1dae868b18017f905"></a><!-- doxytag: member="SAT::DPLLTMiniSat::d_proof" ref="a9eb24ce4c4b1a9f1dae868b18017f905" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classSAT_1_1SatProof.html">SatProof</a>* <a class="el" href="classSAT_1_1DPLLTMiniSat.html#a9eb24ce4c4b1a9f1dae868b18017f905">SAT::DPLLTMiniSat::d_proof</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__minisat_8h_source.html#l00055">55</a> of file <a class="el" href="dpllt__minisat_8h_source.html">dpllt_minisat.h</a>.</p>
<p>Referenced by <a class="el" href="dpllt__minisat_8h_source.html#l00099">getProof()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00065">search()</a>, and <a class="el" href="dpllt__minisat_8cpp_source.html#l00041">~DPLLTMiniSat()</a>.</p>
</div>
</div>
<a class="anchor" id="a36d133e42dbd9557434a166d1e97d050"></a><!-- doxytag: member="SAT::DPLLTMiniSat::d_solvers" ref="a36d133e42dbd9557434a166d1e97d050" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::stack<<a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a>*> <a class="el" href="classSAT_1_1DPLLTMiniSat.html#a36d133e42dbd9557434a166d1e97d050">SAT::DPLLTMiniSat::d_solvers</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="dpllt__minisat_8h_source.html#l00061">61</a> of file <a class="el" href="dpllt__minisat_8h_source.html">dpllt_minisat.h</a>.</p>
<p>Referenced by <a class="el" href="dpllt__minisat_8cpp_source.html#l00131">checkSat()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00154">continueCheck()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00050">getActiveSolver()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00244">getValue()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00192">pop()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00056">pushSolver()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00065">search()</a>, and <a class="el" href="dpllt__minisat_8cpp_source.html#l00041">~DPLLTMiniSat()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="dpllt__minisat_8h_source.html">dpllt_minisat.h</a></li>
<li><a class="el" href="dpllt__minisat_8cpp_source.html">dpllt_minisat.cpp</a></li>
</ul>
</div>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
