<!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::DPLLT 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_1DPLLT.html">DPLLT</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="summary">
<a href="#nested-classes">Classes</a> |
<a href="#pub-types">Public Types</a> |
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pro-attribs">Protected Attributes</a> |
<a href="classSAT_1_1DPLLT-members.html">List of all members</a> </div>
<div class="headertitle">
<div class="title">SAT::DPLLT Class Reference<span class="mlabels"><span class="mlabel">abstract</span></span></div> </div>
</div><!--header-->
<div class="contents">
<p><code>#include <<a class="el" href="dpllt_8h_source.html">dpllt.h</a>></code></p>
<p>Inherited by <a class="el" href="classSAT_1_1DPLLTBasic.html">SAT::DPLLTBasic</a>, and <a class="el" href="classSAT_1_1DPLLTMiniSat.html">SAT::DPLLTMiniSat</a>.</p>
<div class="dynheader">
Collaboration diagram for SAT::DPLLT:</div>
<div class="dyncontent">
<div class="center"><img src="classSAT_1_1DPLLT__coll__graph.gif" border="0" usemap="#SAT_1_1DPLLT_coll__map" alt="Collaboration graph"/></div>
<map name="SAT_1_1DPLLT_coll__map" id="SAT_1_1DPLLT_coll__map">
</map>
</div>
<table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="nested-classes"></a>
Classes</h2></td></tr>
<tr class="memitem:"><td class="memItemLeft" align="right" valign="top">class  </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLT_1_1Decider.html">Decider</a></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:"><td class="memItemLeft" align="right" valign="top">class  </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html">TheoryAPI</a></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pub-types"></a>
Public Types</h2></td></tr>
<tr class="memitem:ac612908684032ffe76ad97f04afd0ca8"><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"><td class="memSeparator" colspan="2"> </td></tr>
</table><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:abb3fd219fe5a66e70a70fe33b34b45f5"><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"><td class="mdescLeft"> </td><td class="mdescRight">Constructor. <a href="#abb3fd219fe5a66e70a70fe33b34b45f5"></a><br/></td></tr>
<tr class="separator:abb3fd219fe5a66e70a70fe33b34b45f5"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a59bc482fa7ea2517b7dcccbfd5690420"><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"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:adec2886c41b3443c264b852bc5f5a84c"><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"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:add78f8065e68c538dd0914949fb87aef"><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"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:adbf7530318ac373ba6c82983dc4dd595"><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"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa074d69f0937b579b5f6cfefabadd083"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLT.html#aa074d69f0937b579b5f6cfefabadd083">push</a> ()=0</td></tr>
<tr class="memdesc:aa074d69f0937b579b5f6cfefabadd083"><td class="mdescLeft"> </td><td class="mdescRight">Set a checkpoint for backtracking. <a href="#aa074d69f0937b579b5f6cfefabadd083"></a><br/></td></tr>
<tr class="separator:aa074d69f0937b579b5f6cfefabadd083"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a59925cdeed3751c4fe4b5d759ebd755c"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLT.html#a59925cdeed3751c4fe4b5d759ebd755c">pop</a> ()=0</td></tr>
<tr class="memdesc:a59925cdeed3751c4fe4b5d759ebd755c"><td class="mdescLeft"> </td><td class="mdescRight">Restore checkpoint. <a href="#a59925cdeed3751c4fe4b5d759ebd755c"></a><br/></td></tr>
<tr class="separator:a59925cdeed3751c4fe4b5d759ebd755c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aaaa6884de9ebd8b9596e85167e8f9273"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLT.html#aaaa6884de9ebd8b9596e85167e8f9273">addAssertion</a> (const <a class="el" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a> &cnf)=0</td></tr>
<tr class="memdesc:aaaa6884de9ebd8b9596e85167e8f9273"><td class="mdescLeft"> </td><td class="mdescRight">Add new clauses to the <a class="el" href="namespaceSAT.html">SAT</a> solver. <a href="#aaaa6884de9ebd8b9596e85167e8f9273"></a><br/></td></tr>
<tr class="separator:aaaa6884de9ebd8b9596e85167e8f9273"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a46312fb7854ac482f28c28564f83494d"><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_1DPLLT.html#a46312fb7854ac482f28c28564f83494d">getCurAssignments</a> ()=0</td></tr>
<tr class="separator:a46312fb7854ac482f28c28564f83494d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac73560398ae2ae153d318b53d37c7c71"><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_1DPLLT.html#ac73560398ae2ae153d318b53d37c7c71">getCurClauses</a> ()=0</td></tr>
<tr class="separator:ac73560398ae2ae153d318b53d37c7c71"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a245df0d49bda0e9bdf69a1153e0d76be"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">CVC3::QueryResult</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLT.html#a245df0d49bda0e9bdf69a1153e0d76be">checkSat</a> (const <a class="el" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a> &cnf)=0</td></tr>
<tr class="memdesc:a245df0d49bda0e9bdf69a1153e0d76be"><td class="mdescLeft"> </td><td class="mdescRight">Check the satisfiability of a set of clauses in the current context. <a href="#a245df0d49bda0e9bdf69a1153e0d76be"></a><br/></td></tr>
<tr class="separator:a245df0d49bda0e9bdf69a1153e0d76be"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a713db9fe798e2a9be337b8726540a24e"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">CVC3::QueryResult</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLT.html#a713db9fe798e2a9be337b8726540a24e">continueCheck</a> (const <a class="el" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a> &cnf)=0</td></tr>
<tr class="memdesc:a713db9fe798e2a9be337b8726540a24e"><td class="mdescLeft"> </td><td class="mdescRight">Continue checking the last check with additional constraints. <a href="#a713db9fe798e2a9be337b8726540a24e"></a><br/></td></tr>
<tr class="separator:a713db9fe798e2a9be337b8726540a24e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a961364ed0ea77af61dbabd7a3a07670c"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">Var::Val</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLT.html#a961364ed0ea77af61dbabd7a3a07670c">getValue</a> (<a class="el" href="classSAT_1_1Var.html">Var</a> v)=0</td></tr>
<tr class="memdesc:a961364ed0ea77af61dbabd7a3a07670c"><td class="mdescLeft"> </td><td class="mdescRight">Get value of variable: unassigned, false, or true. <a href="#a961364ed0ea77af61dbabd7a3a07670c"></a><br/></td></tr>
<tr class="separator:a961364ed0ea77af61dbabd7a3a07670c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ada559a7b19d3dfe82acfa084b8b634ad"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Proof.html">CVC3::Proof</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSAT_1_1DPLLT.html#ada559a7b19d3dfe82acfa084b8b634ad">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> *)=0</td></tr>
<tr class="memdesc:ada559a7b19d3dfe82acfa084b8b634ad"><td class="mdescLeft"> </td><td class="mdescRight">Get the proof from <a class="el" href="namespaceSAT.html">SAT</a> engine. <a href="#ada559a7b19d3dfe82acfa084b8b634ad"></a><br/></td></tr>
<tr class="separator:ada559a7b19d3dfe82acfa084b8b634ad"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pro-attribs"></a>
Protected Attributes</h2></td></tr>
<tr class="memitem:aafa21967afbd30f8c18ebc9f6c37bfa9"><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"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aebea99801d1e6b690feb9610403f1162"><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"><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_8h_source.html#l00023">23</a> of file <a class="el" href="dpllt_8h_source.html">dpllt.h</a>.</p>
</div><h2 class="groupheader">Member Enumeration Documentation</h2>
<a class="anchor" id="ac612908684032ffe76ad97f04afd0ca8"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">enum <a class="el" href="classSAT_1_1DPLLT.html#ac612908684032ffe76ad97f04afd0ca8">SAT::DPLLT::ConsistentResult</a></td>
</tr>
</table>
</div><div class="memdoc">
<dl><dt><b>Enumerator: </b></dt><dd><table border="0" cellspacing="2" cellpadding="0">
<tr><td valign="top"><em><a class="anchor" id="ac612908684032ffe76ad97f04afd0ca8a1dbdf8ba98f0b618f9f4dffcbc947f95"></a>INCONSISTENT</em> </td><td>
</td></tr>
<tr><td valign="top"><em><a class="anchor" id="ac612908684032ffe76ad97f04afd0ca8ab418da559e5bf8e1e7bb7f21dbd1b8ac"></a>MAYBE_CONSISTENT</em> </td><td>
</td></tr>
<tr><td valign="top"><em><a class="anchor" id="ac612908684032ffe76ad97f04afd0ca8ae8ec5d9933decee81ba80f5bd5cfbed2"></a>CONSISTENT</em> </td><td>
</td></tr>
</table>
</dd>
</dl>
<p>Definition at line <a class="el" href="dpllt_8h_source.html#l00026">26</a> of file <a class="el" href="dpllt_8h_source.html">dpllt.h</a>.</p>
</div>
</div>
<h2 class="groupheader">Constructor & Destructor Documentation</h2>
<a class="anchor" id="abb3fd219fe5a66e70a70fe33b34b45f5"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">SAT::DPLLT::DPLLT </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></td>
<td>)</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>Constructor. </p>
<p>The client constructing <a class="el" href="classSAT_1_1DPLLT.html">DPLLT</a> must provide an implementation of <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html">TheoryAPI</a>. It may also optionally provide an implementation of <a class="el" href="classSAT_1_1DPLLT_1_1Decider.html">Decider</a>. If decider is NULL, then the <a class="el" href="classSAT_1_1DPLLT.html">DPLLT</a> class must make its own decisions. </p>
<p>Definition at line <a class="el" href="dpllt_8h_source.html#l00113">113</a> of file <a class="el" href="dpllt_8h_source.html">dpllt.h</a>.</p>
</div>
</div>
<a class="anchor" id="a59bc482fa7ea2517b7dcccbfd5690420"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual SAT::DPLLT::~DPLLT </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 class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="dpllt_8h_source.html#l00115">115</a> of file <a class="el" href="dpllt_8h_source.html">dpllt.h</a>.</p>
</div>
</div>
<h2 class="groupheader">Member Function Documentation</h2>
<a class="anchor" id="adec2886c41b3443c264b852bc5f5a84c"></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_1DPLLT_1_1TheoryAPI.html">TheoryAPI</a>* SAT::DPLLT::theoryAPI </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_8h_source.html#l00117">117</a> of file <a class="el" href="dpllt_8h_source.html">dpllt.h</a>.</p>
<p>References <a class="el" href="dpllt_8h_source.html#l00104">d_theoryAPI</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00396">SAT::DPLLTBasic::checkSat()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00472">SAT::DPLLTBasic::continueCheck()</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>
</div>
</div>
<a class="anchor" id="add78f8065e68c538dd0914949fb87aef"></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_1DPLLT_1_1Decider.html">Decider</a>* SAT::DPLLT::decider </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_8h_source.html#l00118">118</a> of file <a class="el" href="dpllt_8h_source.html">dpllt.h</a>.</p>
<p>References <a class="el" href="dpllt_8h_source.html#l00105">d_decider</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00050">SATDecisionHook()</a>, and <a class="el" href="dpllt_8h_source.html#l00120">setDecider()</a>.</p>
</div>
</div>
<a class="anchor" id="adbf7530318ac373ba6c82983dc4dd595"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void SAT::DPLLT::setDecider </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><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_8h_source.html#l00120">120</a> of file <a class="el" href="dpllt_8h_source.html">dpllt.h</a>.</p>
<p>References <a class="el" href="dpllt_8h_source.html#l00105">d_decider</a>, and <a class="el" href="dpllt_8h_source.html#l00118">decider()</a>.</p>
</div>
</div>
<a class="anchor" id="aa074d69f0937b579b5f6cfefabadd083"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual void SAT::DPLLT::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">pure 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>Implemented in <a class="el" href="classSAT_1_1DPLLTMiniSat.html#a169decc11aac46183d6213a2c6f12633">SAT::DPLLTMiniSat</a>, and <a class="el" href="classSAT_1_1DPLLTBasic.html#a8c8f7e178849aead6754e44e3e63dc0c">SAT::DPLLTBasic</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8h_source.html#l00271">CVC3::SearchSat::push()</a>.</p>
</div>
</div>
<a class="anchor" id="a59925cdeed3751c4fe4b5d759ebd755c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual void SAT::DPLLT::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">pure 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>Implemented in <a class="el" href="classSAT_1_1DPLLTMiniSat.html#a6cf0c23d330fc8609323cb3dd8282377">SAT::DPLLTMiniSat</a>, and <a class="el" href="classSAT_1_1DPLLTBasic.html#aff5dbd3c2a47f003d7b388a8b673cc85">SAT::DPLLTBasic</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8h_source.html#l00272">CVC3::SearchSat::pop()</a>.</p>
</div>
</div>
<a class="anchor" id="aaaa6884de9ebd8b9596e85167e8f9273"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual void SAT::DPLLT::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">pure 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>Implemented in <a class="el" href="classSAT_1_1DPLLTMiniSat.html#afdf7f3a5aa5eccf6c04ba4326567f0b9">SAT::DPLLTMiniSat</a>, and <a class="el" href="classSAT_1_1DPLLTBasic.html#afaffe075e05bcd2e56aeede2154e0d5a">SAT::DPLLTBasic</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l01102">CVC3::SearchSat::newUserAssumption()</a>.</p>
</div>
</div>
<a class="anchor" id="a46312fb7854ac482f28c28564f83494d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual std::vector<<a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a>> SAT::DPLLT::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">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classSAT_1_1DPLLTMiniSat.html#aae30c40897ec35d1a0485899865b723e">SAT::DPLLTMiniSat</a>, and <a class="el" href="classSAT_1_1DPLLTBasic.html#a4047558a5e4a9e84b81e388b220d4e79">SAT::DPLLTBasic</a>.</p>
</div>
</div>
<a class="anchor" id="ac73560398ae2ae153d318b53d37c7c71"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual std::vector<std::vector<<a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a>> > SAT::DPLLT::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">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classSAT_1_1DPLLTMiniSat.html#a1a19b6494dbc9bdd404e5917ee9eea24">SAT::DPLLTMiniSat</a>, and <a class="el" href="classSAT_1_1DPLLTBasic.html#abaf2763764a68c9e4fbc190953b4e6c8">SAT::DPLLTBasic</a>.</p>
</div>
</div>
<a class="anchor" id="a245df0d49bda0e9bdf69a1153e0d76be"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">CVC3::QueryResult</a> SAT::DPLLT::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">pure 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_1DPLLT.html#a59925cdeed3751c4fe4b5d759ebd755c" 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>Implemented in <a class="el" href="classSAT_1_1DPLLTMiniSat.html#a51a36acb7b2ed49d97fa8d5524604604">SAT::DPLLTMiniSat</a>, and <a class="el" href="classSAT_1_1DPLLTBasic.html#a195fdfa1972c882fd3d87eae0742c7ac">SAT::DPLLTBasic</a>.</p>
</div>
</div>
<a class="anchor" id="a713db9fe798e2a9be337b8726540a24e"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">CVC3::QueryResult</a> SAT::DPLLT::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">pure 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_1DPLLT.html#a59925cdeed3751c4fe4b5d759ebd755c" 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>Implemented in <a class="el" href="classSAT_1_1DPLLTMiniSat.html#aae7502914c5ca0708d0bd11ebc766d0a">SAT::DPLLTMiniSat</a>, and <a class="el" href="classSAT_1_1DPLLTBasic.html#a1271494f0f1f6e9c249d8fce8418ecd7">SAT::DPLLTBasic</a>.</p>
</div>
</div>
<a class="anchor" id="a961364ed0ea77af61dbabd7a3a07670c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">Var::Val</a> SAT::DPLLT::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">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Get value of variable: unassigned, false, or true. </p>
<p>Implemented in <a class="el" href="classSAT_1_1DPLLTMiniSat.html#a06fd86d63383adc68d1ace6deb466175">SAT::DPLLTMiniSat</a>, and <a class="el" href="classSAT_1_1DPLLTBasic.html#ab0eac02c714ede751cf48fb188e375f6">SAT::DPLLTBasic</a>.</p>
</div>
</div>
<a class="anchor" id="ada559a7b19d3dfe82acfa084b8b634ad"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1Proof.html">CVC3::Proof</a> SAT::DPLLT::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">pure 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>Implemented in <a class="el" href="classSAT_1_1DPLLTMiniSat.html#ae465fc059c93948333a16b2c21a8828b">SAT::DPLLTMiniSat</a>, and <a class="el" href="classSAT_1_1DPLLTBasic.html#a0c4e0f09aacb6791929ac0eb6e6662c0">SAT::DPLLTBasic</a>.</p>
</div>
</div>
<h2 class="groupheader">Member Data Documentation</h2>
<a class="anchor" id="aafa21967afbd30f8c18ebc9f6c37bfa9"></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_1DPLLT_1_1TheoryAPI.html">TheoryAPI</a>* SAT::DPLLT::d_theoryAPI</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="dpllt_8h_source.html#l00104">104</a> of file <a class="el" href="dpllt_8h_source.html">dpllt.h</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00379">SAT::DPLLTBasic::addAssertion()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00223">SAT::DPLLTMiniSat::addAssertion()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00396">SAT::DPLLTBasic::checkSat()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00131">SAT::DPLLTMiniSat::checkSat()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00472">SAT::DPLLTBasic::continueCheck()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00324">SAT::DPLLTBasic::pop()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00192">SAT::DPLLTMiniSat::pop()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00314">SAT::DPLLTBasic::push()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00179">SAT::DPLLTMiniSat::push()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00056">SAT::DPLLTMiniSat::pushSolver()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00065">SAT::DPLLTMiniSat::search()</a>, and <a class="el" href="dpllt_8h_source.html#l00117">theoryAPI()</a>.</p>
</div>
</div>
<a class="anchor" id="aebea99801d1e6b690feb9610403f1162"></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_1DPLLT_1_1Decider.html">Decider</a>* SAT::DPLLT::d_decider</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="dpllt_8h_source.html#l00105">105</a> of file <a class="el" href="dpllt_8h_source.html">dpllt.h</a>.</p>
<p>Referenced by <a class="el" href="dpllt_8h_source.html#l00118">decider()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00056">SAT::DPLLTMiniSat::pushSolver()</a>, and <a class="el" href="dpllt_8h_source.html#l00120">setDecider()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following file:<ul>
<li><a class="el" href="dpllt_8h_source.html">dpllt.h</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>
