<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<title>CVC3: SatSolver Class Reference</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li class="current"><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="annotated.html"><span>Class List</span></a></li>
<li><a href="classes.html"><span>Class Index</span></a></li>
<li><a href="hierarchy.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
</div>
<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> </div>
<div class="headertitle">
<div class="title">SatSolver Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="SatSolver" -->
<p><code>#include <<a class="el" href="sat__api_8h_source.html">sat_api.h</a>></code></p>
<div class="dynheader">
Inheritance diagram for SatSolver:</div>
<div class="dyncontent">
<div class="center">
<img src="classSatSolver.png" usemap="#SatSolver_map" alt=""/>
<map id="SatSolver_map" name="SatSolver_map">
<area href="classXchaff.html" alt="Xchaff" shape="rect" coords="0,56,67,80"/>
</map>
</div></div>
<p><a href="classSatSolver-members.html">List of all members.</a></p>
<h2><a name="nested-classes"></a>
Classes</h2>
<ul>
<li>union <a class="el" href="unionSatSolver_1_1Clause.html">Clause</a>
<li>union <a class="el" href="unionSatSolver_1_1Lit.html">Lit</a>
<li>union <a class="el" href="unionSatSolver_1_1Var.html">Var</a>
</ul>
<h2><a name="pub-types"></a>
Public Types</h2>
<ul>
<li>enum <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/>
}
<li>typedef enum <a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53">SatSolver::SATStatus</a> <a class="el" href="classSatSolver.html#a5310ac0594841d926d40d6ddb3d749b6">SATStatus</a>
</ul>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li><a class="el" href="classSatSolver.html#a362ed37d0180c370c2060628dc75dd32">SatSolver</a> ()
<li>virtual <a class="el" href="classSatSolver.html#a087f2258b1c1ccce271e826dc07d27e6">~SatSolver</a> ()
<li>virtual int <a class="el" href="classSatSolver.html#a75ac3919b9d2794bd2443e32bb1f29fd">NumVariables</a> ()=0
<li>virtual <a class="el" href="unionSatSolver_1_1Var.html">Var</a> <a class="el" href="classSatSolver.html#acf0e4f44556b7cfcea37100f92962fee">AddVariables</a> (int nvars)=0
<li><a class="el" href="unionSatSolver_1_1Var.html">Var</a> <a class="el" href="classSatSolver.html#a771730713d9da6f1161de299c6acc308">AddVariable</a> ()
<li>virtual <a class="el" href="unionSatSolver_1_1Var.html">Var</a> <a class="el" href="classSatSolver.html#aebeecffca634f23d8c9b941b44b4cfe7">GetVar</a> (int varIndex)=0
<li>virtual int <a class="el" href="classSatSolver.html#a78a8661d31ba8f3aca7e4c73a84f0bcf">GetVarIndex</a> (<a class="el" href="unionSatSolver_1_1Var.html">Var</a> v)=0
<li>virtual <a class="el" href="unionSatSolver_1_1Var.html">Var</a> <a class="el" href="classSatSolver.html#a6c62129375a3b6dda25ad2ba6c0a5696">GetFirstVar</a> ()=0
<li>virtual <a class="el" href="unionSatSolver_1_1Var.html">Var</a> <a class="el" href="classSatSolver.html#a2a175341a5ca6b28add0a1cac3e9bc8a">GetNextVar</a> (<a class="el" href="unionSatSolver_1_1Var.html">Var</a> var)=0
<li>virtual <a class="el" href="unionSatSolver_1_1Lit.html">Lit</a> <a class="el" href="classSatSolver.html#a66bbef74a05f145e477adf37a1e1d116">MakeLit</a> (<a class="el" href="unionSatSolver_1_1Var.html">Var</a> var, int phase)=0
<li>virtual <a class="el" href="unionSatSolver_1_1Var.html">Var</a> <a class="el" href="classSatSolver.html#a505146a1fb5715620935ec31f909932f">GetVarFromLit</a> (<a class="el" href="unionSatSolver_1_1Lit.html">Lit</a> lit)=0
<li>virtual int <a class="el" href="classSatSolver.html#a7187c85c8fc08c253b97de67509af3f2">GetPhaseFromLit</a> (<a class="el" href="unionSatSolver_1_1Lit.html">Lit</a> lit)=0
<li>virtual int <a class="el" href="classSatSolver.html#ad883af9527935afd6c8ad542ba119f4a">NumClauses</a> ()=0
<li>virtual <a class="el" href="unionSatSolver_1_1Clause.html">Clause</a> <a class="el" href="classSatSolver.html#a1fb269f00fd9da8242e2bad01967f097">AddClause</a> (std::vector< <a class="el" href="unionSatSolver_1_1Lit.html">Lit</a> > &lits)=0
<li>virtual bool <a class="el" href="classSatSolver.html#a833d889d53fa2dbd609dac14625a5325">DeleteClause</a> (<a class="el" href="unionSatSolver_1_1Clause.html">Clause</a> clause)
<li>virtual <a class="el" href="unionSatSolver_1_1Clause.html">Clause</a> <a class="el" href="classSatSolver.html#a3f5dcfdd713812059fdcba94bc6be3c1">GetClause</a> (int clauseIndex)=0
<li>virtual <a class="el" href="unionSatSolver_1_1Clause.html">Clause</a> <a class="el" href="classSatSolver.html#a580f042cdf32047e73056dfd810226ad">GetFirstClause</a> ()=0
<li>virtual <a class="el" href="unionSatSolver_1_1Clause.html">Clause</a> <a class="el" href="classSatSolver.html#a61ca72083b23704e2007f0c4b7414ff1">GetNextClause</a> (<a class="el" href="unionSatSolver_1_1Clause.html">Clause</a> clause)=0
<li>virtual void <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
<li>virtual <a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53">SATStatus</a> <a class="el" href="classSatSolver.html#a0dfc1321f3446be70349f35881144433">Satisfiable</a> (bool allowNewClauses=false)=0
<li>virtual int <a class="el" href="classSatSolver.html#a111b3a56be2feaae62bc57483f0aa9bf">GetVarAssignment</a> (<a class="el" href="unionSatSolver_1_1Var.html">Var</a> var)=0
<li>virtual <a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53">SATStatus</a> <a class="el" href="classSatSolver.html#ab4e73333fbc4b4372a18c66a40d4757f">Continue</a> ()=0
<li>virtual void <a class="el" href="classSatSolver.html#aa05fce07f5c3363e2362a3b1de7795db">Restart</a> ()=0
<li>virtual void <a class="el" href="classSatSolver.html#ac64e81107b4b94fd1f6fb76b219a0517">Reset</a> ()=0
<li>virtual void <a class="el" href="classSatSolver.html#a2f5308d9fdff97f882186073f05d8874">RegisterDLevelHook</a> (void(*f)(void *, int), void *cookie)=0
<li>virtual void <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
<li>virtual void <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
<li>virtual void <a class="el" href="classSatSolver.html#a856cf7839d83dcc04ee421d2595fc671">RegisterDeductionHook</a> (void(*f)(void *), void *cookie)=0
<li>virtual bool <a class="el" href="classSatSolver.html#ab6c0375792fa61834acc0e059b0f0215">SetBudget</a> (int budget)
<li>virtual bool <a class="el" href="classSatSolver.html#ae71ce584f847dd8f8cd79c15a1e18ac4">SetMemLimit</a> (int mem_limit)
<li>virtual bool <a class="el" href="classSatSolver.html#a2d799de14b8f73985474b6e6bb391799">SetRandomness</a> (int n)
<li>virtual bool <a class="el" href="classSatSolver.html#a49baebbc72ee8480ce9b15931fd6a087">SetRandSeed</a> (int seed)
<li>virtual bool <a class="el" href="classSatSolver.html#aab2f83c7e7a2e0294904ff5c0fa3409d">EnableClauseDeletion</a> ()
<li>virtual bool <a class="el" href="classSatSolver.html#ae4127dad23cea8d60a6eb2f5d0072554">DisableClauseDeletion</a> ()
<li>virtual int <a class="el" href="classSatSolver.html#a9ab0d5988fd6b737626eddfdfb3086ca">GetBudgetUsed</a> ()
<li>virtual int <a class="el" href="classSatSolver.html#a409a256b9b590f8881690422ac34f566">GetMemUsed</a> ()
<li>virtual int <a class="el" href="classSatSolver.html#a2a416ee5b49d9cf91a57c5b9e71388b8">GetNumDecisions</a> ()
<li>virtual int <a class="el" href="classSatSolver.html#ab81836241806bc37ca6c5cfcd1a77df4">GetNumConflicts</a> ()
<li>virtual int <a class="el" href="classSatSolver.html#af11d56356aa9a578f0baaa4cbcdc0b97">GetNumExtConflicts</a> ()
<li>virtual float <a class="el" href="classSatSolver.html#ab1d30058d42aecba7708cb9e29cbda67">GetTotalTime</a> ()
<li>virtual float <a class="el" href="classSatSolver.html#a4af09fc1738959db1c0d197a4fbf8a6a">GetSATTime</a> ()
<li>virtual int <a class="el" href="classSatSolver.html#a6f617ce6eae22b959f135d347776cb27">GetNumLiterals</a> ()
<li>virtual int <a class="el" href="classSatSolver.html#a6499994eb391919ce6542412e3e43d01">GetNumDeletedClauses</a> ()
<li>virtual int <a class="el" href="classSatSolver.html#ab81eb4127972de38906425ba4babfadc">GetNumDeletedLiterals</a> ()
<li>virtual int <a class="el" href="classSatSolver.html#a45923d3ff1c6145198098d7e689c23f0">GetNumImplications</a> ()
<li>virtual int <a class="el" href="classSatSolver.html#a74190d9fc4abdb54fc65c4efffdf75fc">GetMaxDLevel</a> ()
<li>void <a class="el" href="classSatSolver.html#a1e57a5f44892f0ef08a487a1516030df">PrintStatistics</a> (std::ostream &os=std::cout)
</ul>
<h2><a name="pub-static-methods"></a>
Static Public Member Functions</h2>
<ul>
<li>static <a class="el" href="classSatSolver.html">SatSolver</a> * <a class="el" href="classSatSolver.html#aad67f64508f2560518d09449cd4e39ee">Create</a> ()
</ul>
<hr/><a name="details" id="details"></a><h2>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><hr/><h2>Member Typedef Documentation</h2>
<a class="anchor" id="a5310ac0594841d926d40d6ddb3d749b6"></a><!-- doxytag: member="SatSolver::SATStatus" ref="a5310ac0594841d926d40d6ddb3d749b6" args="" -->
<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>
<hr/><h2>Member Enumeration Documentation</h2>
<a class="anchor" id="a09aef5b79042b31f37d0184667c34d53"></a><!-- doxytag: member="SatSolver::SATStatus" ref="a09aef5b79042b31f37d0184667c34d53" args="" -->
<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><!-- doxytag: member="UNKNOWN" ref="a09aef5b79042b31f37d0184667c34d53a77f70e9dedb02009ba4ab7e6fbea1de3" args="" -->UNKNOWN</em> </td><td>
</td></tr>
<tr><td valign="top"><em><a class="anchor" id="a09aef5b79042b31f37d0184667c34d53ad154fc26948177f01812d287e6340734"></a><!-- doxytag: member="UNSATISFIABLE" ref="a09aef5b79042b31f37d0184667c34d53ad154fc26948177f01812d287e6340734" args="" -->UNSATISFIABLE</em> </td><td>
</td></tr>
<tr><td valign="top"><em><a class="anchor" id="a09aef5b79042b31f37d0184667c34d53a8bc290b76f93dd68bdc44d083a7c4e25"></a><!-- doxytag: member="SATISFIABLE" ref="a09aef5b79042b31f37d0184667c34d53a8bc290b76f93dd68bdc44d083a7c4e25" args="" -->SATISFIABLE</em> </td><td>
</td></tr>
<tr><td valign="top"><em><a class="anchor" id="a09aef5b79042b31f37d0184667c34d53a1a1ccd6ae244cce5f08fcdf2d4621fe0"></a><!-- doxytag: member="BUDGET_EXCEEDED" ref="a09aef5b79042b31f37d0184667c34d53a1a1ccd6ae244cce5f08fcdf2d4621fe0" args="" -->BUDGET_EXCEEDED</em> </td><td>
</td></tr>
<tr><td valign="top"><em><a class="anchor" id="a09aef5b79042b31f37d0184667c34d53a987b167d27ed988755362d6decb025d8"></a><!-- doxytag: member="OUT_OF_MEMORY" ref="a09aef5b79042b31f37d0184667c34d53a987b167d27ed988755362d6decb025d8" args="" -->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>
<hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="a362ed37d0180c370c2060628dc75dd32"></a><!-- doxytag: member="SatSolver::SatSolver" ref="a362ed37d0180c370c2060628dc75dd32" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">SatSolver::SatSolver </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="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><!-- doxytag: member="SatSolver::~SatSolver" ref="a087f2258b1c1ccce271e826dc07d27e6" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual SatSolver::~SatSolver </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></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>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="aad67f64508f2560518d09449cd4e39ee"></a><!-- doxytag: member="SatSolver::Create" ref="aad67f64508f2560518d09449cd4e39ee" args="()" -->
<div class="memitem">
<div class="memproto">
<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><code> [static]</code></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><!-- doxytag: member="SatSolver::NumVariables" ref="a75ac3919b9d2794bd2443e32bb1f29fd" args="()=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual int SatSolver::NumVariables </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [pure virtual]</code></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><!-- doxytag: member="SatSolver::AddVariables" ref="acf0e4f44556b7cfcea37100f92962fee" args="(int nvars)=0" -->
<div class="memitem">
<div class="memproto">
<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><code> [pure virtual]</code></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><!-- doxytag: member="SatSolver::AddVariable" ref="a771730713d9da6f1161de299c6acc308" args="()" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="SatSolver::GetVar" ref="aebeecffca634f23d8c9b941b44b4cfe7" args="(int varIndex)=0" -->
<div class="memitem">
<div class="memproto">
<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><code> [pure virtual]</code></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><!-- doxytag: member="SatSolver::GetVarIndex" ref="a78a8661d31ba8f3aca7e4c73a84f0bcf" args="(Var v)=0" -->
<div class="memitem">
<div class="memproto">
<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><code> [pure virtual]</code></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><!-- doxytag: member="SatSolver::GetFirstVar" ref="a6c62129375a3b6dda25ad2ba6c0a5696" args="()=0" -->
<div class="memitem">
<div class="memproto">
<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><code> [pure virtual]</code></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><!-- doxytag: member="SatSolver::GetNextVar" ref="a2a175341a5ca6b28add0a1cac3e9bc8a" args="(Var var)=0" -->
<div class="memitem">
<div class="memproto">
<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><code> [pure virtual]</code></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><!-- doxytag: member="SatSolver::MakeLit" ref="a66bbef74a05f145e477adf37a1e1d116" args="(Var var, int phase)=0" -->
<div class="memitem">
<div class="memproto">
<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><code> [pure virtual]</code></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><!-- doxytag: member="SatSolver::GetVarFromLit" ref="a505146a1fb5715620935ec31f909932f" args="(Lit lit)=0" -->
<div class="memitem">
<div class="memproto">
<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><code> [pure virtual]</code></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><!-- doxytag: member="SatSolver::GetPhaseFromLit" ref="a7187c85c8fc08c253b97de67509af3f2" args="(Lit lit)=0" -->
<div class="memitem">
<div class="memproto">
<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><code> [pure virtual]</code></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><!-- doxytag: member="SatSolver::NumClauses" ref="ad883af9527935afd6c8ad542ba119f4a" args="()=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual int SatSolver::NumClauses </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [pure virtual]</code></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><!-- doxytag: member="SatSolver::AddClause" ref="a1fb269f00fd9da8242e2bad01967f097" args="(std::vector< Lit > &lits)=0" -->
<div class="memitem">
<div class="memproto">
<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><code> [pure virtual]</code></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><!-- doxytag: member="SatSolver::DeleteClause" ref="a833d889d53fa2dbd609dac14625a5325" args="(Clause clause)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline, virtual]</code></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><!-- doxytag: member="SatSolver::GetClause" ref="a3f5dcfdd713812059fdcba94bc6be3c1" args="(int clauseIndex)=0" -->
<div class="memitem">
<div class="memproto">
<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><code> [pure virtual]</code></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><!-- doxytag: member="SatSolver::GetFirstClause" ref="a580f042cdf32047e73056dfd810226ad" args="()=0" -->
<div class="memitem">
<div class="memproto">
<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><code> [pure virtual]</code></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><!-- doxytag: member="SatSolver::GetNextClause" ref="a61ca72083b23704e2007f0c4b7414ff1" args="(Clause clause)=0" -->
<div class="memitem">
<div class="memproto">
<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><code> [pure virtual]</code></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><!-- doxytag: member="SatSolver::GetClauseLits" ref="af0c71f214e5980cf6848abaeaa3dbf16" args="(Clause clause, std::vector< Lit > *lits)=0" -->
<div class="memitem">
<div class="memproto">
<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><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
</div>
</div>
<a class="anchor" id="a0dfc1321f3446be70349f35881144433"></a><!-- doxytag: member="SatSolver::Satisfiable" ref="a0dfc1321f3446be70349f35881144433" args="(bool allowNewClauses=false)=0" -->
<div class="memitem">
<div class="memproto">
<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><code> [pure virtual]</code></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><!-- doxytag: member="SatSolver::GetVarAssignment" ref="a111b3a56be2feaae62bc57483f0aa9bf" args="(Var var)=0" -->
<div class="memitem">
<div class="memproto">
<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><code> [pure virtual]</code></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><!-- doxytag: member="SatSolver::Continue" ref="ab4e73333fbc4b4372a18c66a40d4757f" args="()=0" -->
<div class="memitem">
<div class="memproto">
<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><code> [pure virtual]</code></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><!-- doxytag: member="SatSolver::Restart" ref="aa05fce07f5c3363e2362a3b1de7795db" args="()=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual void SatSolver::Restart </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [pure virtual]</code></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><!-- doxytag: member="SatSolver::Reset" ref="ac64e81107b4b94fd1f6fb76b219a0517" args="()=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual void SatSolver::Reset </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [pure virtual]</code></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><!-- doxytag: member="SatSolver::RegisterDLevelHook" ref="a2f5308d9fdff97f882186073f05d8874" args="(void(*f)(void *, int), void *cookie)=0" -->
<div class="memitem">
<div class="memproto">
<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><code> [pure virtual]</code></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><!-- doxytag: member="SatSolver::RegisterDecisionHook" ref="a76cc15252a711e8a9a21e49a30d7e920" args="(Lit(*f)(void *, bool *), void *cookie)=0" -->
<div class="memitem">
<div class="memproto">
<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><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
</div>
</div>
<a class="anchor" id="a658bb40c580f149024c59509e9e3acd0"></a><!-- doxytag: member="SatSolver::RegisterAssignmentHook" ref="a658bb40c580f149024c59509e9e3acd0" args="(void(*f)(void *, Var, int), void *cookie)=0" -->
<div class="memitem">
<div class="memproto">
<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><code> [pure virtual]</code></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><!-- doxytag: member="SatSolver::RegisterDeductionHook" ref="a856cf7839d83dcc04ee421d2595fc671" args="(void(*f)(void *), void *cookie)=0" -->
<div class="memitem">
<div class="memproto">
<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><code> [pure virtual]</code></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><!-- doxytag: member="SatSolver::SetBudget" ref="ab6c0375792fa61834acc0e059b0f0215" args="(int budget)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline, virtual]</code></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><!-- doxytag: member="SatSolver::SetMemLimit" ref="ae71ce584f847dd8f8cd79c15a1e18ac4" args="(int mem_limit)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline, virtual]</code></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><!-- doxytag: member="SatSolver::SetRandomness" ref="a2d799de14b8f73985474b6e6bb391799" args="(int n)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline, virtual]</code></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><!-- doxytag: member="SatSolver::SetRandSeed" ref="a49baebbc72ee8480ce9b15931fd6a087" args="(int seed)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline, virtual]</code></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><!-- doxytag: member="SatSolver::EnableClauseDeletion" ref="aab2f83c7e7a2e0294904ff5c0fa3409d" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual bool SatSolver::EnableClauseDeletion </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></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><!-- doxytag: member="SatSolver::DisableClauseDeletion" ref="ae4127dad23cea8d60a6eb2f5d0072554" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual bool SatSolver::DisableClauseDeletion </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></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><!-- doxytag: member="SatSolver::GetBudgetUsed" ref="a9ab0d5988fd6b737626eddfdfb3086ca" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual int SatSolver::GetBudgetUsed </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></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><!-- doxytag: member="SatSolver::GetMemUsed" ref="a409a256b9b590f8881690422ac34f566" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual int SatSolver::GetMemUsed </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></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><!-- doxytag: member="SatSolver::GetNumDecisions" ref="a2a416ee5b49d9cf91a57c5b9e71388b8" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual int SatSolver::GetNumDecisions </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></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><!-- doxytag: member="SatSolver::GetNumConflicts" ref="ab81836241806bc37ca6c5cfcd1a77df4" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual int SatSolver::GetNumConflicts </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></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><!-- doxytag: member="SatSolver::GetNumExtConflicts" ref="af11d56356aa9a578f0baaa4cbcdc0b97" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual int SatSolver::GetNumExtConflicts </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></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><!-- doxytag: member="SatSolver::GetTotalTime" ref="ab1d30058d42aecba7708cb9e29cbda67" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual float SatSolver::GetTotalTime </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></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><!-- doxytag: member="SatSolver::GetSATTime" ref="a4af09fc1738959db1c0d197a4fbf8a6a" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual float SatSolver::GetSATTime </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></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><!-- doxytag: member="SatSolver::GetNumLiterals" ref="a6f617ce6eae22b959f135d347776cb27" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual int SatSolver::GetNumLiterals </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></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><!-- doxytag: member="SatSolver::GetNumDeletedClauses" ref="a6499994eb391919ce6542412e3e43d01" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual int SatSolver::GetNumDeletedClauses </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></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><!-- doxytag: member="SatSolver::GetNumDeletedLiterals" ref="ab81eb4127972de38906425ba4babfadc" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual int SatSolver::GetNumDeletedLiterals </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></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><!-- doxytag: member="SatSolver::GetNumImplications" ref="a45923d3ff1c6145198098d7e689c23f0" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual int SatSolver::GetNumImplications </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></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><!-- doxytag: member="SatSolver::GetMaxDLevel" ref="a74190d9fc4abdb54fc65c4efffdf75fc" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual int SatSolver::GetMaxDLevel </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></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><!-- doxytag: member="SatSolver::PrintStatistics" ref="a1e57a5f44892f0ef08a487a1516030df" args="(std::ostream &os=std::cout)" -->
<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>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
