<!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: SatSolver 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><!-- 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="#pub-static-methods">Static Public Member Functions</a> |
<a href="classSatSolver-members.html">List of all members</a> </div>
<div class="headertitle">
<div class="title">SatSolver 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="sat__api_8h_source.html">sat_api.h</a>></code></p>
<p>Inherited by <a class="el" href="classXchaff.html">Xchaff</a>.</p>
<div class="dynheader">
Collaboration diagram for SatSolver:</div>
<div class="dyncontent">
<div class="center"><img src="classSatSolver__coll__graph.gif" border="0" usemap="#SatSolver_coll__map" alt="Collaboration graph"/></div>
<map name="SatSolver_coll__map" id="SatSolver_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">union  </td><td class="memItemRight" valign="bottom"><a class="el" href="unionSatSolver_1_1Clause.html">Clause</a></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:"><td class="memItemLeft" align="right" valign="top">union  </td><td class="memItemRight" valign="bottom"><a class="el" href="unionSatSolver_1_1Lit.html">Lit</a></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:"><td class="memItemLeft" align="right" valign="top">union  </td><td class="memItemRight" valign="bottom"><a class="el" href="unionSatSolver_1_1Var.html">Var</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:a09aef5b79042b31f37d0184667c34d53"><td class="memItemLeft" align="right" valign="top">enum  </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53">SATStatus</a> { <br/>
  <a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53a77f70e9dedb02009ba4ab7e6fbea1de3">UNKNOWN</a>,
<a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53ad154fc26948177f01812d287e6340734">UNSATISFIABLE</a>,
<a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53a8bc290b76f93dd68bdc44d083a7c4e25">SATISFIABLE</a>,
<a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53a1a1ccd6ae244cce5f08fcdf2d4621fe0">BUDGET_EXCEEDED</a>,
<br/>
  <a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53a987b167d27ed988755362d6decb025d8">OUT_OF_MEMORY</a>
<br/>
}</td></tr>
<tr class="separator:a09aef5b79042b31f37d0184667c34d53"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5310ac0594841d926d40d6ddb3d749b6"><td class="memItemLeft" align="right" valign="top">typedef enum <a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53">SatSolver::SATStatus</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a5310ac0594841d926d40d6ddb3d749b6">SATStatus</a></td></tr>
<tr class="separator:a5310ac0594841d926d40d6ddb3d749b6"><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:a362ed37d0180c370c2060628dc75dd32"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a362ed37d0180c370c2060628dc75dd32">SatSolver</a> ()</td></tr>
<tr class="separator:a362ed37d0180c370c2060628dc75dd32"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a087f2258b1c1ccce271e826dc07d27e6"><td class="memItemLeft" align="right" valign="top">virtual </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a087f2258b1c1ccce271e826dc07d27e6">~SatSolver</a> ()</td></tr>
<tr class="separator:a087f2258b1c1ccce271e826dc07d27e6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a75ac3919b9d2794bd2443e32bb1f29fd"><td class="memItemLeft" align="right" valign="top">virtual int </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a75ac3919b9d2794bd2443e32bb1f29fd">NumVariables</a> ()=0</td></tr>
<tr class="separator:a75ac3919b9d2794bd2443e32bb1f29fd"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:acf0e4f44556b7cfcea37100f92962fee"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="unionSatSolver_1_1Var.html">Var</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#acf0e4f44556b7cfcea37100f92962fee">AddVariables</a> (int nvars)=0</td></tr>
<tr class="separator:acf0e4f44556b7cfcea37100f92962fee"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a771730713d9da6f1161de299c6acc308"><td class="memItemLeft" align="right" valign="top"><a class="el" href="unionSatSolver_1_1Var.html">Var</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a771730713d9da6f1161de299c6acc308">AddVariable</a> ()</td></tr>
<tr class="separator:a771730713d9da6f1161de299c6acc308"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aebeecffca634f23d8c9b941b44b4cfe7"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="unionSatSolver_1_1Var.html">Var</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#aebeecffca634f23d8c9b941b44b4cfe7">GetVar</a> (int varIndex)=0</td></tr>
<tr class="separator:aebeecffca634f23d8c9b941b44b4cfe7"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a78a8661d31ba8f3aca7e4c73a84f0bcf"><td class="memItemLeft" align="right" valign="top">virtual int </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a78a8661d31ba8f3aca7e4c73a84f0bcf">GetVarIndex</a> (<a class="el" href="unionSatSolver_1_1Var.html">Var</a> v)=0</td></tr>
<tr class="separator:a78a8661d31ba8f3aca7e4c73a84f0bcf"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6c62129375a3b6dda25ad2ba6c0a5696"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="unionSatSolver_1_1Var.html">Var</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a6c62129375a3b6dda25ad2ba6c0a5696">GetFirstVar</a> ()=0</td></tr>
<tr class="separator:a6c62129375a3b6dda25ad2ba6c0a5696"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a2a175341a5ca6b28add0a1cac3e9bc8a"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="unionSatSolver_1_1Var.html">Var</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a2a175341a5ca6b28add0a1cac3e9bc8a">GetNextVar</a> (<a class="el" href="unionSatSolver_1_1Var.html">Var</a> var)=0</td></tr>
<tr class="separator:a2a175341a5ca6b28add0a1cac3e9bc8a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a66bbef74a05f145e477adf37a1e1d116"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="unionSatSolver_1_1Lit.html">Lit</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a66bbef74a05f145e477adf37a1e1d116">MakeLit</a> (<a class="el" href="unionSatSolver_1_1Var.html">Var</a> var, int phase)=0</td></tr>
<tr class="separator:a66bbef74a05f145e477adf37a1e1d116"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a505146a1fb5715620935ec31f909932f"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="unionSatSolver_1_1Var.html">Var</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a505146a1fb5715620935ec31f909932f">GetVarFromLit</a> (<a class="el" href="unionSatSolver_1_1Lit.html">Lit</a> lit)=0</td></tr>
<tr class="separator:a505146a1fb5715620935ec31f909932f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a7187c85c8fc08c253b97de67509af3f2"><td class="memItemLeft" align="right" valign="top">virtual int </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a7187c85c8fc08c253b97de67509af3f2">GetPhaseFromLit</a> (<a class="el" href="unionSatSolver_1_1Lit.html">Lit</a> lit)=0</td></tr>
<tr class="separator:a7187c85c8fc08c253b97de67509af3f2"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad883af9527935afd6c8ad542ba119f4a"><td class="memItemLeft" align="right" valign="top">virtual int </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#ad883af9527935afd6c8ad542ba119f4a">NumClauses</a> ()=0</td></tr>
<tr class="separator:ad883af9527935afd6c8ad542ba119f4a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a1fb269f00fd9da8242e2bad01967f097"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="unionSatSolver_1_1Clause.html">Clause</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a1fb269f00fd9da8242e2bad01967f097">AddClause</a> (std::vector< <a class="el" href="unionSatSolver_1_1Lit.html">Lit</a> > &lits)=0</td></tr>
<tr class="separator:a1fb269f00fd9da8242e2bad01967f097"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a833d889d53fa2dbd609dac14625a5325"><td class="memItemLeft" align="right" valign="top">virtual bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a833d889d53fa2dbd609dac14625a5325">DeleteClause</a> (<a class="el" href="unionSatSolver_1_1Clause.html">Clause</a> clause)</td></tr>
<tr class="separator:a833d889d53fa2dbd609dac14625a5325"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a3f5dcfdd713812059fdcba94bc6be3c1"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="unionSatSolver_1_1Clause.html">Clause</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a3f5dcfdd713812059fdcba94bc6be3c1">GetClause</a> (int clauseIndex)=0</td></tr>
<tr class="separator:a3f5dcfdd713812059fdcba94bc6be3c1"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a580f042cdf32047e73056dfd810226ad"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="unionSatSolver_1_1Clause.html">Clause</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a580f042cdf32047e73056dfd810226ad">GetFirstClause</a> ()=0</td></tr>
<tr class="separator:a580f042cdf32047e73056dfd810226ad"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a61ca72083b23704e2007f0c4b7414ff1"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="unionSatSolver_1_1Clause.html">Clause</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a61ca72083b23704e2007f0c4b7414ff1">GetNextClause</a> (<a class="el" href="unionSatSolver_1_1Clause.html">Clause</a> clause)=0</td></tr>
<tr class="separator:a61ca72083b23704e2007f0c4b7414ff1"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:af0c71f214e5980cf6848abaeaa3dbf16"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#af0c71f214e5980cf6848abaeaa3dbf16">GetClauseLits</a> (<a class="el" href="unionSatSolver_1_1Clause.html">Clause</a> clause, std::vector< <a class="el" href="unionSatSolver_1_1Lit.html">Lit</a> > *lits)=0</td></tr>
<tr class="separator:af0c71f214e5980cf6848abaeaa3dbf16"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0dfc1321f3446be70349f35881144433"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53">SATStatus</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a0dfc1321f3446be70349f35881144433">Satisfiable</a> (bool allowNewClauses=false)=0</td></tr>
<tr class="separator:a0dfc1321f3446be70349f35881144433"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a111b3a56be2feaae62bc57483f0aa9bf"><td class="memItemLeft" align="right" valign="top">virtual int </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a111b3a56be2feaae62bc57483f0aa9bf">GetVarAssignment</a> (<a class="el" href="unionSatSolver_1_1Var.html">Var</a> var)=0</td></tr>
<tr class="separator:a111b3a56be2feaae62bc57483f0aa9bf"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab4e73333fbc4b4372a18c66a40d4757f"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53">SATStatus</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#ab4e73333fbc4b4372a18c66a40d4757f">Continue</a> ()=0</td></tr>
<tr class="separator:ab4e73333fbc4b4372a18c66a40d4757f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa05fce07f5c3363e2362a3b1de7795db"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#aa05fce07f5c3363e2362a3b1de7795db">Restart</a> ()=0</td></tr>
<tr class="separator:aa05fce07f5c3363e2362a3b1de7795db"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac64e81107b4b94fd1f6fb76b219a0517"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#ac64e81107b4b94fd1f6fb76b219a0517">Reset</a> ()=0</td></tr>
<tr class="separator:ac64e81107b4b94fd1f6fb76b219a0517"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a2f5308d9fdff97f882186073f05d8874"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a2f5308d9fdff97f882186073f05d8874">RegisterDLevelHook</a> (void(*f)(void *, int), void *cookie)=0</td></tr>
<tr class="separator:a2f5308d9fdff97f882186073f05d8874"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a76cc15252a711e8a9a21e49a30d7e920"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a76cc15252a711e8a9a21e49a30d7e920">RegisterDecisionHook</a> (<a class="el" href="unionSatSolver_1_1Lit.html">Lit</a>(*f)(void *, bool *), void *cookie)=0</td></tr>
<tr class="separator:a76cc15252a711e8a9a21e49a30d7e920"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a658bb40c580f149024c59509e9e3acd0"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a658bb40c580f149024c59509e9e3acd0">RegisterAssignmentHook</a> (void(*f)(void *, <a class="el" href="unionSatSolver_1_1Var.html">Var</a>, int), void *cookie)=0</td></tr>
<tr class="separator:a658bb40c580f149024c59509e9e3acd0"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a856cf7839d83dcc04ee421d2595fc671"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a856cf7839d83dcc04ee421d2595fc671">RegisterDeductionHook</a> (void(*f)(void *), void *cookie)=0</td></tr>
<tr class="separator:a856cf7839d83dcc04ee421d2595fc671"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab6c0375792fa61834acc0e059b0f0215"><td class="memItemLeft" align="right" valign="top">virtual bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#ab6c0375792fa61834acc0e059b0f0215">SetBudget</a> (int budget)</td></tr>
<tr class="separator:ab6c0375792fa61834acc0e059b0f0215"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae71ce584f847dd8f8cd79c15a1e18ac4"><td class="memItemLeft" align="right" valign="top">virtual bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#ae71ce584f847dd8f8cd79c15a1e18ac4">SetMemLimit</a> (int mem_limit)</td></tr>
<tr class="separator:ae71ce584f847dd8f8cd79c15a1e18ac4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a2d799de14b8f73985474b6e6bb391799"><td class="memItemLeft" align="right" valign="top">virtual bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a2d799de14b8f73985474b6e6bb391799">SetRandomness</a> (int n)</td></tr>
<tr class="separator:a2d799de14b8f73985474b6e6bb391799"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a49baebbc72ee8480ce9b15931fd6a087"><td class="memItemLeft" align="right" valign="top">virtual bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a49baebbc72ee8480ce9b15931fd6a087">SetRandSeed</a> (int seed)</td></tr>
<tr class="separator:a49baebbc72ee8480ce9b15931fd6a087"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aab2f83c7e7a2e0294904ff5c0fa3409d"><td class="memItemLeft" align="right" valign="top">virtual bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#aab2f83c7e7a2e0294904ff5c0fa3409d">EnableClauseDeletion</a> ()</td></tr>
<tr class="separator:aab2f83c7e7a2e0294904ff5c0fa3409d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae4127dad23cea8d60a6eb2f5d0072554"><td class="memItemLeft" align="right" valign="top">virtual bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#ae4127dad23cea8d60a6eb2f5d0072554">DisableClauseDeletion</a> ()</td></tr>
<tr class="separator:ae4127dad23cea8d60a6eb2f5d0072554"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a9ab0d5988fd6b737626eddfdfb3086ca"><td class="memItemLeft" align="right" valign="top">virtual int </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a9ab0d5988fd6b737626eddfdfb3086ca">GetBudgetUsed</a> ()</td></tr>
<tr class="separator:a9ab0d5988fd6b737626eddfdfb3086ca"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a409a256b9b590f8881690422ac34f566"><td class="memItemLeft" align="right" valign="top">virtual int </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a409a256b9b590f8881690422ac34f566">GetMemUsed</a> ()</td></tr>
<tr class="separator:a409a256b9b590f8881690422ac34f566"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a2a416ee5b49d9cf91a57c5b9e71388b8"><td class="memItemLeft" align="right" valign="top">virtual int </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a2a416ee5b49d9cf91a57c5b9e71388b8">GetNumDecisions</a> ()</td></tr>
<tr class="separator:a2a416ee5b49d9cf91a57c5b9e71388b8"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab81836241806bc37ca6c5cfcd1a77df4"><td class="memItemLeft" align="right" valign="top">virtual int </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#ab81836241806bc37ca6c5cfcd1a77df4">GetNumConflicts</a> ()</td></tr>
<tr class="separator:ab81836241806bc37ca6c5cfcd1a77df4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:af11d56356aa9a578f0baaa4cbcdc0b97"><td class="memItemLeft" align="right" valign="top">virtual int </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#af11d56356aa9a578f0baaa4cbcdc0b97">GetNumExtConflicts</a> ()</td></tr>
<tr class="separator:af11d56356aa9a578f0baaa4cbcdc0b97"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab1d30058d42aecba7708cb9e29cbda67"><td class="memItemLeft" align="right" valign="top">virtual float </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#ab1d30058d42aecba7708cb9e29cbda67">GetTotalTime</a> ()</td></tr>
<tr class="separator:ab1d30058d42aecba7708cb9e29cbda67"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a4af09fc1738959db1c0d197a4fbf8a6a"><td class="memItemLeft" align="right" valign="top">virtual float </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a4af09fc1738959db1c0d197a4fbf8a6a">GetSATTime</a> ()</td></tr>
<tr class="separator:a4af09fc1738959db1c0d197a4fbf8a6a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6f617ce6eae22b959f135d347776cb27"><td class="memItemLeft" align="right" valign="top">virtual int </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a6f617ce6eae22b959f135d347776cb27">GetNumLiterals</a> ()</td></tr>
<tr class="separator:a6f617ce6eae22b959f135d347776cb27"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6499994eb391919ce6542412e3e43d01"><td class="memItemLeft" align="right" valign="top">virtual int </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a6499994eb391919ce6542412e3e43d01">GetNumDeletedClauses</a> ()</td></tr>
<tr class="separator:a6499994eb391919ce6542412e3e43d01"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab81eb4127972de38906425ba4babfadc"><td class="memItemLeft" align="right" valign="top">virtual int </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#ab81eb4127972de38906425ba4babfadc">GetNumDeletedLiterals</a> ()</td></tr>
<tr class="separator:ab81eb4127972de38906425ba4babfadc"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a45923d3ff1c6145198098d7e689c23f0"><td class="memItemLeft" align="right" valign="top">virtual int </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a45923d3ff1c6145198098d7e689c23f0">GetNumImplications</a> ()</td></tr>
<tr class="separator:a45923d3ff1c6145198098d7e689c23f0"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a74190d9fc4abdb54fc65c4efffdf75fc"><td class="memItemLeft" align="right" valign="top">virtual int </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a74190d9fc4abdb54fc65c4efffdf75fc">GetMaxDLevel</a> ()</td></tr>
<tr class="separator:a74190d9fc4abdb54fc65c4efffdf75fc"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a1e57a5f44892f0ef08a487a1516030df"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#a1e57a5f44892f0ef08a487a1516030df">PrintStatistics</a> (std::ostream &os=std::cout)</td></tr>
<tr class="separator:a1e57a5f44892f0ef08a487a1516030df"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pub-static-methods"></a>
Static Public Member Functions</h2></td></tr>
<tr class="memitem:aad67f64508f2560518d09449cd4e39ee"><td class="memItemLeft" align="right" valign="top">static <a class="el" href="classSatSolver.html">SatSolver</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classSatSolver.html#aad67f64508f2560518d09449cd4e39ee">Create</a> ()</td></tr>
<tr class="separator:aad67f64508f2560518d09449cd4e39ee"><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="sat__api_8h_source.html#l00024">24</a> of file <a class="el" href="sat__api_8h_source.html">sat_api.h</a>.</p>
</div><h2 class="groupheader">Member Typedef Documentation</h2>
<a class="anchor" id="a5310ac0594841d926d40d6ddb3d749b6"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">typedef enum <a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53">SatSolver::SATStatus</a> <a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53">SatSolver::SATStatus</a></td>
</tr>
</table>
</div><div class="memdoc">
</div>
</div>
<h2 class="groupheader">Member Enumeration Documentation</h2>
<a class="anchor" id="a09aef5b79042b31f37d0184667c34d53"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">enum <a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53">SatSolver::SATStatus</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="a09aef5b79042b31f37d0184667c34d53a77f70e9dedb02009ba4ab7e6fbea1de3"></a>UNKNOWN</em> </td><td>
</td></tr>
<tr><td valign="top"><em><a class="anchor" id="a09aef5b79042b31f37d0184667c34d53ad154fc26948177f01812d287e6340734"></a>UNSATISFIABLE</em> </td><td>
</td></tr>
<tr><td valign="top"><em><a class="anchor" id="a09aef5b79042b31f37d0184667c34d53a8bc290b76f93dd68bdc44d083a7c4e25"></a>SATISFIABLE</em> </td><td>
</td></tr>
<tr><td valign="top"><em><a class="anchor" id="a09aef5b79042b31f37d0184667c34d53a1a1ccd6ae244cce5f08fcdf2d4621fe0"></a>BUDGET_EXCEEDED</em> </td><td>
</td></tr>
<tr><td valign="top"><em><a class="anchor" id="a09aef5b79042b31f37d0184667c34d53a987b167d27ed988755362d6decb025d8"></a>OUT_OF_MEMORY</em> </td><td>
</td></tr>
</table>
</dd>
</dl>
<p>Definition at line <a class="el" href="sat__api_8h_source.html#l00026">26</a> of file <a class="el" href="sat__api_8h_source.html">sat_api.h</a>.</p>
</div>
</div>
<h2 class="groupheader">Constructor & Destructor Documentation</h2>
<a class="anchor" id="a362ed37d0180c370c2060628dc75dd32"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">SatSolver::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="sat__api_8h_source.html#l00035">35</a> of file <a class="el" href="sat__api_8h_source.html">sat_api.h</a>.</p>
</div>
</div>
<a class="anchor" id="a087f2258b1c1ccce271e826dc07d27e6"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual SatSolver::~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 class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="sat__api_8h_source.html#l00036">36</a> of file <a class="el" href="sat__api_8h_source.html">sat_api.h</a>.</p>
</div>
</div>
<h2 class="groupheader">Member Function Documentation</h2>
<a class="anchor" id="aad67f64508f2560518d09449cd4e39ee"></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> * SatSolver::Create </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">static</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="sat__api_8cpp_source.html#l00015">15</a> of file <a class="el" href="sat__api_8cpp_source.html">sat_api.cpp</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00137">SAT::DPLLTBasic::createManager()</a>.</p>
</div>
</div>
<a class="anchor" id="a75ac3919b9d2794bd2443e32bb1f29fd"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual int SatSolver::NumVariables </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="classXchaff.html#a271a1d5d92cf07c60d70a9939d623391">Xchaff</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00275">SAT::DPLLTBasic::addNewClause()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00289">SAT::DPLLTBasic::addNewClauses()</a>, and <a class="el" href="dpllt__basic_8cpp_source.html#l00396">SAT::DPLLTBasic::checkSat()</a>.</p>
</div>
</div>
<a class="anchor" id="acf0e4f44556b7cfcea37100f92962fee"></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="unionSatSolver_1_1Var.html">Var</a> SatSolver::AddVariables </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>nvars</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>Implemented in <a class="el" href="classXchaff.html#a510ddbd9f083c5372bdaf5f449f4846b">Xchaff</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00289">SAT::DPLLTBasic::addNewClauses()</a>, and <a class="el" href="sat__api_8h_source.html#l00082">AddVariable()</a>.</p>
</div>
</div>
<a class="anchor" id="a771730713d9da6f1161de299c6acc308"></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_1Var.html">Var</a> SatSolver::AddVariable </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="sat__api_8h_source.html#l00082">82</a> of file <a class="el" href="sat__api_8h_source.html">sat_api.h</a>.</p>
<p>References <a class="el" href="classSatSolver.html#acf0e4f44556b7cfcea37100f92962fee">AddVariables()</a>.</p>
</div>
</div>
<a class="anchor" id="aebeecffca634f23d8c9b941b44b4cfe7"></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="unionSatSolver_1_1Var.html">Var</a> SatSolver::GetVar </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>varIndex</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>Implemented in <a class="el" href="classXchaff.html#a41296b8c022c75dd7e2233631a5ac704">Xchaff</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_8h_source.html#l00064">SAT::DPLLTBasic::cvc2SAT()</a>, and <a class="el" href="dpllt__basic_8h_source.html#l00085">SAT::DPLLTBasic::getValue()</a>.</p>
</div>
</div>
<a class="anchor" id="a78a8661d31ba8f3aca7e4c73a84f0bcf"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual int SatSolver::GetVarIndex </td>
<td>(</td>
<td class="paramtype"><a class="el" href="unionSatSolver_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>Implemented in <a class="el" href="classXchaff.html#a4f9ad9e1ff0a150b3f8fad414912cd9e">Xchaff</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8h_source.html#l00068">SAT::DPLLTBasic::SAT2cvc()</a>, and <a class="el" href="dpllt__basic_8cpp_source.html#l00098">SATAssignmentHook()</a>.</p>
</div>
</div>
<a class="anchor" id="a6c62129375a3b6dda25ad2ba6c0a5696"></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="unionSatSolver_1_1Var.html">Var</a> SatSolver::GetFirstVar </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="classXchaff.html#ac3891ccb7f41fb72e294da3899779c62">Xchaff</a>.</p>
</div>
</div>
<a class="anchor" id="a2a175341a5ca6b28add0a1cac3e9bc8a"></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="unionSatSolver_1_1Var.html">Var</a> SatSolver::GetNextVar </td>
<td>(</td>
<td class="paramtype"><a class="el" href="unionSatSolver_1_1Var.html">Var</a> </td>
<td class="paramname"><em>var</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classXchaff.html#aff81fd8f5d3c694e8f5112077142ea03">Xchaff</a>.</p>
</div>
</div>
<a class="anchor" id="a66bbef74a05f145e477adf37a1e1d116"></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="unionSatSolver_1_1Lit.html">Lit</a> SatSolver::MakeLit </td>
<td>(</td>
<td class="paramtype"><a class="el" href="unionSatSolver_1_1Var.html">Var</a> </td>
<td class="paramname"><em>var</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>phase</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">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classXchaff.html#a9e916fd4048dfdcfdec013481e970303">Xchaff</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8h_source.html#l00064">SAT::DPLLTBasic::cvc2SAT()</a>.</p>
</div>
</div>
<a class="anchor" id="a505146a1fb5715620935ec31f909932f"></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="unionSatSolver_1_1Var.html">Var</a> SatSolver::GetVarFromLit </td>
<td>(</td>
<td class="paramtype"><a class="el" href="unionSatSolver_1_1Lit.html">Lit</a> </td>
<td class="paramname"><em>lit</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>Referenced by <a class="el" href="dpllt__basic_8h_source.html#l00068">SAT::DPLLTBasic::SAT2cvc()</a>.</p>
</div>
</div>
<a class="anchor" id="a7187c85c8fc08c253b97de67509af3f2"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual int SatSolver::GetPhaseFromLit </td>
<td>(</td>
<td class="paramtype"><a class="el" href="unionSatSolver_1_1Lit.html">Lit</a> </td>
<td class="paramname"><em>lit</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>Referenced by <a class="el" href="dpllt__basic_8h_source.html#l00068">SAT::DPLLTBasic::SAT2cvc()</a>.</p>
</div>
</div>
<a class="anchor" id="ad883af9527935afd6c8ad542ba119f4a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual int SatSolver::NumClauses </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="classXchaff.html#a1a3fb172ed4b688d7938e160cc00716b">Xchaff</a>.</p>
</div>
</div>
<a class="anchor" id="a1fb269f00fd9da8242e2bad01967f097"></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="unionSatSolver_1_1Clause.html">Clause</a> SatSolver::AddClause </td>
<td>(</td>
<td class="paramtype">std::vector< <a class="el" href="unionSatSolver_1_1Lit.html">Lit</a> > & </td>
<td class="paramname"><em>lits</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>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00275">SAT::DPLLTBasic::addNewClause()</a>, and <a class="el" href="dpllt__basic_8cpp_source.html#l00289">SAT::DPLLTBasic::addNewClauses()</a>.</p>
</div>
</div>
<a class="anchor" id="a833d889d53fa2dbd609dac14625a5325"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual bool SatSolver::DeleteClause </td>
<td>(</td>
<td class="paramtype"><a class="el" href="unionSatSolver_1_1Clause.html">Clause</a> </td>
<td class="paramname"><em>clause</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>Definition at line <a class="el" href="sat__api_8h_source.html#l00123">123</a> of file <a class="el" href="sat__api_8h_source.html">sat_api.h</a>.</p>
</div>
</div>
<a class="anchor" id="a3f5dcfdd713812059fdcba94bc6be3c1"></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="unionSatSolver_1_1Clause.html">Clause</a> SatSolver::GetClause </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>clauseIndex</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>Implemented in <a class="el" href="classXchaff.html#aa7755a77a17224ef7540ff9cf475ebe0">Xchaff</a>.</p>
</div>
</div>
<a class="anchor" id="a580f042cdf32047e73056dfd810226ad"></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="unionSatSolver_1_1Clause.html">Clause</a> SatSolver::GetFirstClause </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="classXchaff.html#a4683a3d3e3c9ea39da714c76f0aa4471">Xchaff</a>.</p>
</div>
</div>
<a class="anchor" id="a61ca72083b23704e2007f0c4b7414ff1"></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="unionSatSolver_1_1Clause.html">Clause</a> SatSolver::GetNextClause </td>
<td>(</td>
<td class="paramtype"><a class="el" href="unionSatSolver_1_1Clause.html">Clause</a> </td>
<td class="paramname"><em>clause</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>Implemented in <a class="el" href="classXchaff.html#af02ffc8cb39e8740a7536323ee937d76">Xchaff</a>.</p>
</div>
</div>
<a class="anchor" id="af0c71f214e5980cf6848abaeaa3dbf16"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual void SatSolver::GetClauseLits </td>
<td>(</td>
<td class="paramtype"><a class="el" href="unionSatSolver_1_1Clause.html">Clause</a> </td>
<td class="paramname"><em>clause</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="unionSatSolver_1_1Lit.html">Lit</a> > * </td>
<td class="paramname"><em>lits</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">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
</div>
</div>
<a class="anchor" id="a0dfc1321f3446be70349f35881144433"></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="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53">SATStatus</a> SatSolver::Satisfiable </td>
<td>(</td>
<td class="paramtype">bool </td>
<td class="paramname"><em>allowNewClauses</em> = <code>false</code></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="classXchaff.html#af833605af7d820b9d7a350a77cd41ed1">Xchaff</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00396">SAT::DPLLTBasic::checkSat()</a>.</p>
</div>
</div>
<a class="anchor" id="a111b3a56be2feaae62bc57483f0aa9bf"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual int SatSolver::GetVarAssignment </td>
<td>(</td>
<td class="paramtype"><a class="el" href="unionSatSolver_1_1Var.html">Var</a> </td>
<td class="paramname"><em>var</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classXchaff.html#a00d874effad75d5544cdd9d257b2573d">Xchaff</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00396">SAT::DPLLTBasic::checkSat()</a>, and <a class="el" href="dpllt__basic_8h_source.html#l00085">SAT::DPLLTBasic::getValue()</a>.</p>
</div>
</div>
<a class="anchor" id="ab4e73333fbc4b4372a18c66a40d4757f"></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="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53">SATStatus</a> SatSolver::Continue </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="classXchaff.html#ab20bcd7cd57b138b62e63d0e1d9a425f">Xchaff</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00472">SAT::DPLLTBasic::continueCheck()</a>.</p>
</div>
</div>
<a class="anchor" id="aa05fce07f5c3363e2362a3b1de7795db"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual void SatSolver::Restart </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="classXchaff.html#a53ce24894150638b3285f7b12ebf23ba">Xchaff</a>.</p>
</div>
</div>
<a class="anchor" id="ac64e81107b4b94fd1f6fb76b219a0517"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual void SatSolver::Reset </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="classXchaff.html#ae8d8fe530dede206922f26f52f1cafcf">Xchaff</a>.</p>
</div>
</div>
<a class="anchor" id="a2f5308d9fdff97f882186073f05d8874"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual void SatSolver::RegisterDLevelHook </td>
<td>(</td>
<td class="paramtype">void(*)(void *, int) </td>
<td class="paramname"><em>f</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">void * </td>
<td class="paramname"><em>cookie</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">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classXchaff.html#a9826417dcd2303591eaeb3259ac154f9">Xchaff</a>.</p>
</div>
</div>
<a class="anchor" id="a76cc15252a711e8a9a21e49a30d7e920"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual void SatSolver::RegisterDecisionHook </td>
<td>(</td>
<td class="paramtype"><a class="el" href="unionSatSolver_1_1Lit.html">Lit</a>(*)(void *, bool *) </td>
<td class="paramname"><em>f</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">void * </td>
<td class="paramname"><em>cookie</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">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
</div>
</div>
<a class="anchor" id="a658bb40c580f149024c59509e9e3acd0"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual void SatSolver::RegisterAssignmentHook </td>
<td>(</td>
<td class="paramtype">void(*)(void *, <a class="el" href="unionSatSolver_1_1Var.html">Var</a>, int) </td>
<td class="paramname"><em>f</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">void * </td>
<td class="paramname"><em>cookie</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">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classXchaff.html#a0a98f9f270df69b9f86d15258b915afb">Xchaff</a>.</p>
</div>
</div>
<a class="anchor" id="a856cf7839d83dcc04ee421d2595fc671"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual void SatSolver::RegisterDeductionHook </td>
<td>(</td>
<td class="paramtype">void(*)(void *) </td>
<td class="paramname"><em>f</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">void * </td>
<td class="paramname"><em>cookie</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">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classXchaff.html#a2ffce1f21eb64712d4e26e1dbc4b0e36">Xchaff</a>.</p>
</div>
</div>
<a class="anchor" id="ab6c0375792fa61834acc0e059b0f0215"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual bool SatSolver::SetBudget </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>budget</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>Reimplemented in <a class="el" href="classXchaff.html#aae25937c3c0f355220a4533fb127edf7">Xchaff</a>.</p>
<p>Definition at line <a class="el" href="sat__api_8h_source.html#l00218">218</a> of file <a class="el" href="sat__api_8h_source.html">sat_api.h</a>.</p>
</div>
</div>
<a class="anchor" id="ae71ce584f847dd8f8cd79c15a1e18ac4"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual bool SatSolver::SetMemLimit </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>mem_limit</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>Reimplemented in <a class="el" href="classXchaff.html#a58905ab92772d4603d41b8155a59f0c2">Xchaff</a>.</p>
<p>Definition at line <a class="el" href="sat__api_8h_source.html#l00221">221</a> of file <a class="el" href="sat__api_8h_source.html">sat_api.h</a>.</p>
</div>
</div>
<a class="anchor" id="a2d799de14b8f73985474b6e6bb391799"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual bool SatSolver::SetRandomness </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>n</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>Reimplemented in <a class="el" href="classXchaff.html#aa334fc9dd8673ff86d7214e439986e57">Xchaff</a>.</p>
<p>Definition at line <a class="el" href="sat__api_8h_source.html#l00225">225</a> of file <a class="el" href="sat__api_8h_source.html">sat_api.h</a>.</p>
</div>
</div>
<a class="anchor" id="a49baebbc72ee8480ce9b15931fd6a087"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual bool SatSolver::SetRandSeed </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>seed</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Reimplemented in <a class="el" href="classXchaff.html#a390d585a7258c0237ea17893587d1ee0">Xchaff</a>.</p>
<p>Definition at line <a class="el" href="sat__api_8h_source.html#l00226">226</a> of file <a class="el" href="sat__api_8h_source.html">sat_api.h</a>.</p>
</div>
</div>
<a class="anchor" id="aab2f83c7e7a2e0294904ff5c0fa3409d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual bool SatSolver::EnableClauseDeletion </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>Reimplemented in <a class="el" href="classXchaff.html#a8a481eb175d81a80556e13ecff483da1">Xchaff</a>.</p>
<p>Definition at line <a class="el" href="sat__api_8h_source.html#l00229">229</a> of file <a class="el" href="sat__api_8h_source.html">sat_api.h</a>.</p>
</div>
</div>
<a class="anchor" id="ae4127dad23cea8d60a6eb2f5d0072554"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual bool SatSolver::DisableClauseDeletion </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>Reimplemented in <a class="el" href="classXchaff.html#ab763aebc2ca5e3b489aab695ed469213">Xchaff</a>.</p>
<p>Definition at line <a class="el" href="sat__api_8h_source.html#l00230">230</a> of file <a class="el" href="sat__api_8h_source.html">sat_api.h</a>.</p>
</div>
</div>
<a class="anchor" id="a9ab0d5988fd6b737626eddfdfb3086ca"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual int SatSolver::GetBudgetUsed </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>Reimplemented in <a class="el" href="classXchaff.html#a90a038ad50d710508f2f3c0a3f909528">Xchaff</a>.</p>
<p>Definition at line <a class="el" href="sat__api_8h_source.html#l00243">243</a> of file <a class="el" href="sat__api_8h_source.html">sat_api.h</a>.</p>
</div>
</div>
<a class="anchor" id="a409a256b9b590f8881690422ac34f566"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual int SatSolver::GetMemUsed </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>Reimplemented in <a class="el" href="classXchaff.html#ad483bd394ba347d90afb2354a3579d5b">Xchaff</a>.</p>
<p>Definition at line <a class="el" href="sat__api_8h_source.html#l00246">246</a> of file <a class="el" href="sat__api_8h_source.html">sat_api.h</a>.</p>
</div>
</div>
<a class="anchor" id="a2a416ee5b49d9cf91a57c5b9e71388b8"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual int SatSolver::GetNumDecisions </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>Reimplemented in <a class="el" href="classXchaff.html#a0ae00dfb15ac6f1f6947056c448cc4db">Xchaff</a>.</p>
<p>Definition at line <a class="el" href="sat__api_8h_source.html#l00249">249</a> of file <a class="el" href="sat__api_8h_source.html">sat_api.h</a>.</p>
</div>
</div>
<a class="anchor" id="ab81836241806bc37ca6c5cfcd1a77df4"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual int SatSolver::GetNumConflicts </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>Reimplemented in <a class="el" href="classXchaff.html#aafeebd0e319671ade2b15418a5491aa1">Xchaff</a>.</p>
<p>Definition at line <a class="el" href="sat__api_8h_source.html#l00252">252</a> of file <a class="el" href="sat__api_8h_source.html">sat_api.h</a>.</p>
</div>
</div>
<a class="anchor" id="af11d56356aa9a578f0baaa4cbcdc0b97"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual int SatSolver::GetNumExtConflicts </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>Reimplemented in <a class="el" href="classXchaff.html#aa0c48459562f98b52b01999bb7c394ec">Xchaff</a>.</p>
<p>Definition at line <a class="el" href="sat__api_8h_source.html#l00256">256</a> of file <a class="el" href="sat__api_8h_source.html">sat_api.h</a>.</p>
</div>
</div>
<a class="anchor" id="ab1d30058d42aecba7708cb9e29cbda67"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual float SatSolver::GetTotalTime </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>Reimplemented in <a class="el" href="classXchaff.html#a554b43a08c1aadad56bcb16d7a5ae8f5">Xchaff</a>.</p>
<p>Definition at line <a class="el" href="sat__api_8h_source.html#l00259">259</a> of file <a class="el" href="sat__api_8h_source.html">sat_api.h</a>.</p>
</div>
</div>
<a class="anchor" id="a4af09fc1738959db1c0d197a4fbf8a6a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual float SatSolver::GetSATTime </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>Reimplemented in <a class="el" href="classXchaff.html#a892c44f9b8bd6bb98a57c67f6e0261fa">Xchaff</a>.</p>
<p>Definition at line <a class="el" href="sat__api_8h_source.html#l00263">263</a> of file <a class="el" href="sat__api_8h_source.html">sat_api.h</a>.</p>
</div>
</div>
<a class="anchor" id="a6f617ce6eae22b959f135d347776cb27"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual int SatSolver::GetNumLiterals </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>Reimplemented in <a class="el" href="classXchaff.html#aefa4cd2058553d7946cbebdb667e8670">Xchaff</a>.</p>
<p>Definition at line <a class="el" href="sat__api_8h_source.html#l00266">266</a> of file <a class="el" href="sat__api_8h_source.html">sat_api.h</a>.</p>
</div>
</div>
<a class="anchor" id="a6499994eb391919ce6542412e3e43d01"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual int SatSolver::GetNumDeletedClauses </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>Reimplemented in <a class="el" href="classXchaff.html#a6f69523569c280d1486b7c6ddde2b112">Xchaff</a>.</p>
<p>Definition at line <a class="el" href="sat__api_8h_source.html#l00269">269</a> of file <a class="el" href="sat__api_8h_source.html">sat_api.h</a>.</p>
</div>
</div>
<a class="anchor" id="ab81eb4127972de38906425ba4babfadc"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual int SatSolver::GetNumDeletedLiterals </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>Reimplemented in <a class="el" href="classXchaff.html#a0939c01d21987c020eb5fa783af11164">Xchaff</a>.</p>
<p>Definition at line <a class="el" href="sat__api_8h_source.html#l00272">272</a> of file <a class="el" href="sat__api_8h_source.html">sat_api.h</a>.</p>
</div>
</div>
<a class="anchor" id="a45923d3ff1c6145198098d7e689c23f0"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual int SatSolver::GetNumImplications </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>Reimplemented in <a class="el" href="classXchaff.html#aec9cba92c3e56ed8aa68693c6083e54d">Xchaff</a>.</p>
<p>Definition at line <a class="el" href="sat__api_8h_source.html#l00275">275</a> of file <a class="el" href="sat__api_8h_source.html">sat_api.h</a>.</p>
</div>
</div>
<a class="anchor" id="a74190d9fc4abdb54fc65c4efffdf75fc"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual int SatSolver::GetMaxDLevel </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>Reimplemented in <a class="el" href="classXchaff.html#a4ff03b5c032c7344058759ef1165ad9e">Xchaff</a>.</p>
<p>Definition at line <a class="el" href="sat__api_8h_source.html#l00278">278</a> of file <a class="el" href="sat__api_8h_source.html">sat_api.h</a>.</p>
</div>
</div>
<a class="anchor" id="a1e57a5f44892f0ef08a487a1516030df"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SatSolver::PrintStatistics </td>
<td>(</td>
<td class="paramtype">std::ostream & </td>
<td class="paramname"><em>os</em> = <code>std::cout</code></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="sat__api_8cpp_source.html#l00021">21</a> of file <a class="el" href="sat__api_8cpp_source.html">sat_api.cpp</a>.</p>
<p>References <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="sat__api_8h_source.html">sat_api.h</a></li>
<li><a class="el" href="sat__api_8cpp_source.html">sat_api.cpp</a></li>
<li><a class="el" href="xchaff_8cpp_source.html">xchaff.cpp</a></li>
</ul>
</div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:17 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>
