<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<title>CVC3: sat_api.h Source File</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><a href="annotated.html"><span>Classes</span></a></li>
<li class="current"><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="files.html"><span>File List</span></a></li>
<li><a href="globals.html"><span>File Members</span></a></li>
</ul>
</div>
<div class="header">
<div class="headertitle">
<div class="title">sat_api.h</div> </div>
</div>
<div class="contents">
<a href="sat__api_8h.html">Go to the documentation of this file.</a><div class="fragment"><pre class="fragment"><a name="l00001"></a>00001 <span class="comment">///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00002"></a>00002 <span class="comment"></span><span class="comment">// //</span>
<a name="l00003"></a>00003 <span class="comment">// File: sat_api.h //</span>
<a name="l00004"></a>00004 <span class="comment">// Author: Clark Barrett //</span>
<a name="l00005"></a>00005 <span class="comment">// Created: Tue Oct 22 11:30:54 2002 //</span>
<a name="l00006"></a>00006 <span class="comment">// Description: Generic enhanced SAT API //</span>
<a name="l00007"></a>00007 <span class="comment">// //</span><span class="comment"></span>
<a name="l00008"></a>00008 <span class="comment">///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00009"></a>00009 <span class="comment"></span>
<a name="l00010"></a>00010 <span class="preprocessor">#ifndef _SAT_API_H_</span>
<a name="l00011"></a>00011 <span class="preprocessor"></span><span class="preprocessor">#define _SAT_API_H_</span>
<a name="l00012"></a>00012 <span class="preprocessor"></span>
<a name="l00013"></a>00013 <span class="preprocessor">#include <vector></span>
<a name="l00014"></a>00014 <span class="preprocessor">#include <iostream></span>
<a name="l00015"></a>00015 <span class="comment"></span>
<a name="l00016"></a>00016 <span class="comment">///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00017"></a>00017 <span class="comment"></span><span class="comment">// //</span>
<a name="l00018"></a>00018 <span class="comment">// Class: SAT //</span>
<a name="l00019"></a>00019 <span class="comment">// Author: Clark Barrett //</span>
<a name="l00020"></a>00020 <span class="comment">// Created: Tue Oct 22 12:02:53 2002 //</span>
<a name="l00021"></a>00021 <span class="comment">// Description: API for generic SAT solver with enhanced interface features. //</span>
<a name="l00022"></a>00022 <span class="comment">// //</span><span class="comment"></span>
<a name="l00023"></a>00023 <span class="comment">///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00024"></a><a class="code" href="classSatSolver.html">00024</a> <span class="comment"></span><span class="keyword">class </span><a class="code" href="classSatSolver.html">SatSolver</a> {
<a name="l00025"></a>00025 <span class="keyword">public</span>:
<a name="l00026"></a><a class="code" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53">00026</a> <span class="keyword">typedef</span> <span class="keyword">enum</span> <a class="code" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53">SATStatus</a> {
<a name="l00027"></a><a class="code" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53a77f70e9dedb02009ba4ab7e6fbea1de3">00027</a> <a class="code" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53a77f70e9dedb02009ba4ab7e6fbea1de3">UNKNOWN</a>,
<a name="l00028"></a><a class="code" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53ad154fc26948177f01812d287e6340734">00028</a> <a class="code" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53ad154fc26948177f01812d287e6340734">UNSATISFIABLE</a>,
<a name="l00029"></a><a class="code" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53a8bc290b76f93dd68bdc44d083a7c4e25">00029</a> <a class="code" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53a8bc290b76f93dd68bdc44d083a7c4e25">SATISFIABLE</a>,
<a name="l00030"></a><a class="code" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53a1a1ccd6ae244cce5f08fcdf2d4621fe0">00030</a> <a class="code" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53a1a1ccd6ae244cce5f08fcdf2d4621fe0">BUDGET_EXCEEDED</a>,
<a name="l00031"></a><a class="code" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53a987b167d27ed988755362d6decb025d8">00031</a> <a class="code" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53a987b167d27ed988755362d6decb025d8">OUT_OF_MEMORY</a>
<a name="l00032"></a>00032 } <a class="code" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53">SATStatus</a>;
<a name="l00033"></a>00033
<a name="l00034"></a>00034 <span class="comment">// Constructor and Destructor</span>
<a name="l00035"></a><a class="code" href="classSatSolver.html#a362ed37d0180c370c2060628dc75dd32">00035</a> <a class="code" href="classSatSolver.html#a362ed37d0180c370c2060628dc75dd32">SatSolver</a>() {}
<a name="l00036"></a><a class="code" href="classSatSolver.html#a087f2258b1c1ccce271e826dc07d27e6">00036</a> <span class="keyword">virtual</span> <a class="code" href="classSatSolver.html#a087f2258b1c1ccce271e826dc07d27e6">~SatSolver</a>() {}
<a name="l00037"></a>00037
<a name="l00038"></a>00038 <span class="comment">// Implementation must provide this function</span>
<a name="l00039"></a>00039 <span class="keyword">static</span> <a class="code" href="classSatSolver.html">SatSolver</a> *<a class="code" href="classSatSolver.html#aad67f64508f2560518d09449cd4e39ee">Create</a>();
<a name="l00040"></a>00040 <span class="comment"></span>
<a name="l00041"></a>00041 <span class="comment"> /////////////////////////////////////////////////////////////////////////////</span>
<a name="l00042"></a>00042 <span class="comment"></span> <span class="comment">// Variables, Literals, and Clauses //</span><span class="comment"></span>
<a name="l00043"></a>00043 <span class="comment"> /////////////////////////////////////////////////////////////////////////////</span>
<a name="l00044"></a>00044 <span class="comment"></span>
<a name="l00045"></a>00045 <span class="comment">// Variables, literals and clauses are all simple union classes. This makes</span>
<a name="l00046"></a>00046 <span class="comment">// it easy to use integers or pointers to some more complex data structure</span>
<a name="l00047"></a>00047 <span class="comment">// for the implementation while at the same time increasing safety by</span>
<a name="l00048"></a>00048 <span class="comment">// imposing strict type requirements on users of the API.</span>
<a name="l00049"></a>00049 <span class="comment">// The value -1 is reserved to represent an empty or NULL value</span>
<a name="l00050"></a>00050
<a name="l00051"></a><a class="code" href="unionSatSolver_1_1Var.html">00051</a> <span class="keyword">union </span><a class="code" href="unionSatSolver_1_1Var.html">Var</a> {
<a name="l00052"></a><a class="code" href="unionSatSolver_1_1Var.html#a0dab20c0e01831dd8c30dd46fbeef533">00052</a> <span class="keywordtype">long</span> <a class="code" href="unionSatSolver_1_1Var.html#a0dab20c0e01831dd8c30dd46fbeef533">id</a>;
<a name="l00053"></a><a class="code" href="unionSatSolver_1_1Var.html#adeec53fa82541d260d5ed2a3452e6aad">00053</a> <span class="keywordtype">void</span> *<a class="code" href="unionSatSolver_1_1Var.html#adeec53fa82541d260d5ed2a3452e6aad">vptr</a>;
<a name="l00054"></a><a class="code" href="unionSatSolver_1_1Var.html#af6c9795e8f5f2e87e7d7a24660c7ccb4">00054</a> <a class="code" href="unionSatSolver_1_1Var.html#af6c9795e8f5f2e87e7d7a24660c7ccb4">Var</a>() : <a class="code" href="unionSatSolver_1_1Var.html#a0dab20c0e01831dd8c30dd46fbeef533">id</a>(-1) {}
<a name="l00055"></a><a class="code" href="unionSatSolver_1_1Var.html#a3e727743e01b381279b121462c5f2110">00055</a> <span class="keywordtype">bool</span> <a class="code" href="unionSatSolver_1_1Var.html#a3e727743e01b381279b121462c5f2110">IsNull</a>() { <span class="keywordflow">return</span> <span class="keywordtype">id</span> == -1; }
<a name="l00056"></a><a class="code" href="unionSatSolver_1_1Var.html#a0749bf538158732dcaaaa37a53130246">00056</a> <span class="keywordtype">void</span> <a class="code" href="unionSatSolver_1_1Var.html#a0749bf538158732dcaaaa37a53130246">Reset</a>() { <span class="keywordtype">id</span> = -1; }
<a name="l00057"></a>00057 };
<a name="l00058"></a>00058
<a name="l00059"></a><a class="code" href="unionSatSolver_1_1Lit.html">00059</a> <span class="keyword">union </span><a class="code" href="unionSatSolver_1_1Lit.html">Lit</a> {
<a name="l00060"></a><a class="code" href="unionSatSolver_1_1Lit.html#a96b4ad90adf8a2d6eee7af2c5b351481">00060</a> <span class="keywordtype">long</span> <a class="code" href="unionSatSolver_1_1Lit.html#a96b4ad90adf8a2d6eee7af2c5b351481">id</a>;
<a name="l00061"></a><a class="code" href="unionSatSolver_1_1Lit.html#afb3631b07ab665be6670adcacf75af8f">00061</a> <span class="keywordtype">void</span> *<a class="code" href="unionSatSolver_1_1Lit.html#afb3631b07ab665be6670adcacf75af8f">vptr</a>;
<a name="l00062"></a><a class="code" href="unionSatSolver_1_1Lit.html#a7f8920c25e25bb3e8448c6b4f6b7694d">00062</a> <a class="code" href="unionSatSolver_1_1Lit.html#a7f8920c25e25bb3e8448c6b4f6b7694d">Lit</a>() : <a class="code" href="unionSatSolver_1_1Lit.html#a96b4ad90adf8a2d6eee7af2c5b351481">id</a>(-1) {}
<a name="l00063"></a><a class="code" href="unionSatSolver_1_1Lit.html#a1445776bb4af130811f46b3ad41b564c">00063</a> <span class="keywordtype">bool</span> <a class="code" href="unionSatSolver_1_1Lit.html#a1445776bb4af130811f46b3ad41b564c">IsNull</a>() { <span class="keywordflow">return</span> <span class="keywordtype">id</span> == -1; }
<a name="l00064"></a><a class="code" href="unionSatSolver_1_1Lit.html#a920ad716dbc5a6695f234c80fa686c3f">00064</a> <span class="keywordtype">void</span> <a class="code" href="unionSatSolver_1_1Lit.html#a920ad716dbc5a6695f234c80fa686c3f">Reset</a>() { <span class="keywordtype">id</span> = -1; }
<a name="l00065"></a>00065 };
<a name="l00066"></a>00066
<a name="l00067"></a><a class="code" href="unionSatSolver_1_1Clause.html">00067</a> <span class="keyword">union </span><a class="code" href="unionSatSolver_1_1Clause.html">Clause</a> {
<a name="l00068"></a><a class="code" href="unionSatSolver_1_1Clause.html#a525bdedc03ca4e24251a3b715fc35da8">00068</a> <span class="keywordtype">long</span> <a class="code" href="unionSatSolver_1_1Clause.html#a525bdedc03ca4e24251a3b715fc35da8">id</a>;
<a name="l00069"></a><a class="code" href="unionSatSolver_1_1Clause.html#acd6572dae41469801089b872f63a2cdf">00069</a> <span class="keywordtype">void</span> *<a class="code" href="unionSatSolver_1_1Clause.html#acd6572dae41469801089b872f63a2cdf">vptr</a>;
<a name="l00070"></a><a class="code" href="unionSatSolver_1_1Clause.html#a7e85ff4cdc5c883d858472712ae3d485">00070</a> <a class="code" href="unionSatSolver_1_1Clause.html#a7e85ff4cdc5c883d858472712ae3d485">Clause</a>() : <a class="code" href="unionSatSolver_1_1Clause.html#a525bdedc03ca4e24251a3b715fc35da8">id</a>(-1) {}
<a name="l00071"></a><a class="code" href="unionSatSolver_1_1Clause.html#a0909ff4fdf3c02d96c2017d868129cc3">00071</a> <span class="keywordtype">bool</span> <a class="code" href="unionSatSolver_1_1Clause.html#a0909ff4fdf3c02d96c2017d868129cc3">IsNull</a>() { <span class="keywordflow">return</span> <span class="keywordtype">id</span> == -1; }
<a name="l00072"></a><a class="code" href="unionSatSolver_1_1Clause.html#a0301c94286fe257cbaa640aa77049dc1">00072</a> <span class="keywordtype">void</span> <a class="code" href="unionSatSolver_1_1Clause.html#a0301c94286fe257cbaa640aa77049dc1">Reset</a>() { <span class="keywordtype">id</span> = -1; }
<a name="l00073"></a>00073 };
<a name="l00074"></a>00074
<a name="l00075"></a>00075 <span class="comment">// Return total number of variables</span>
<a name="l00076"></a>00076 <span class="keyword">virtual</span> <span class="keywordtype">int</span> <a class="code" href="classSatSolver.html#a75ac3919b9d2794bd2443e32bb1f29fd">NumVariables</a>()=0;
<a name="l00077"></a>00077
<a name="l00078"></a>00078 <span class="comment">// Returns the first of nvar new variables.</span>
<a name="l00079"></a>00079 <span class="keyword">virtual</span> <a class="code" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> <a class="code" href="classSatSolver.html#acf0e4f44556b7cfcea37100f92962fee">AddVariables</a>(<span class="keywordtype">int</span> nvars)=0;
<a name="l00080"></a>00080
<a name="l00081"></a>00081 <span class="comment">// Return a new variable</span>
<a name="l00082"></a><a class="code" href="classSatSolver.html#a771730713d9da6f1161de299c6acc308">00082</a> <a class="code" href="unionSatSolver_1_1Var.html">Var</a> <a class="code" href="classSatSolver.html#a771730713d9da6f1161de299c6acc308">AddVariable</a>() { <span class="keywordflow">return</span> <a class="code" href="classSatSolver.html#acf0e4f44556b7cfcea37100f92962fee">AddVariables</a>(1); }
<a name="l00083"></a>00083
<a name="l00084"></a>00084 <span class="comment">// Get the varIndexth variable. varIndex must be between 1 and</span>
<a name="l00085"></a>00085 <span class="comment">// NumVariables() inclusive.</span>
<a name="l00086"></a>00086 <span class="keyword">virtual</span> <a class="code" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> <a class="code" href="classSatSolver.html#aebeecffca634f23d8c9b941b44b4cfe7">GetVar</a>(<span class="keywordtype">int</span> varIndex)=0;
<a name="l00087"></a>00087
<a name="l00088"></a>00088 <span class="comment">// Return the index (between 1 and NumVariables()) of v.</span>
<a name="l00089"></a>00089 <span class="keyword">virtual</span> <span class="keywordtype">int</span> <a class="code" href="classSatSolver.html#a78a8661d31ba8f3aca7e4c73a84f0bcf">GetVarIndex</a>(<a class="code" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> v)=0;
<a name="l00090"></a>00090
<a name="l00091"></a>00091 <span class="comment">// Get the first variable. Returns a NULL Var if there are no variables.</span>
<a name="l00092"></a>00092 <span class="keyword">virtual</span> <a class="code" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> <a class="code" href="classSatSolver.html#a6c62129375a3b6dda25ad2ba6c0a5696">GetFirstVar</a>()=0;
<a name="l00093"></a>00093
<a name="l00094"></a>00094 <span class="comment">// Get the next variable after var. Returns a NULL Var if var is the last</span>
<a name="l00095"></a>00095 <span class="comment">// variable.</span>
<a name="l00096"></a>00096 <span class="keyword">virtual</span> <a class="code" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> <a class="code" href="classSatSolver.html#a2a175341a5ca6b28add0a1cac3e9bc8a">GetNextVar</a>(<a class="code" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> var)=0;
<a name="l00097"></a>00097
<a name="l00098"></a>00098 <span class="comment">// Return a literal made from the given var and phase (0 is positive phase, 1</span>
<a name="l00099"></a>00099 <span class="comment">// is negative phase).</span>
<a name="l00100"></a>00100 <span class="keyword">virtual</span> Lit <a class="code" href="classSatSolver.html#a66bbef74a05f145e477adf37a1e1d116">MakeLit</a>(<a class="code" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> var, <span class="keywordtype">int</span> phase)=0;
<a name="l00101"></a>00101
<a name="l00102"></a>00102 <span class="comment">// Get var from literal.</span>
<a name="l00103"></a>00103 <span class="keyword">virtual</span> <a class="code" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> <a class="code" href="classSatSolver.html#a505146a1fb5715620935ec31f909932f">GetVarFromLit</a>(Lit lit)=0;
<a name="l00104"></a>00104
<a name="l00105"></a>00105 <span class="comment">// Get phase from literal ID.</span>
<a name="l00106"></a>00106 <span class="keyword">virtual</span> <span class="keywordtype">int</span> <a class="code" href="classSatSolver.html#a7187c85c8fc08c253b97de67509af3f2">GetPhaseFromLit</a>(Lit lit)=0;
<a name="l00107"></a>00107
<a name="l00108"></a>00108 <span class="comment">// Return total number of clauses</span>
<a name="l00109"></a>00109 <span class="keyword">virtual</span> <span class="keywordtype">int</span> <a class="code" href="classSatSolver.html#ad883af9527935afd6c8ad542ba119f4a">NumClauses</a>()=0;
<a name="l00110"></a>00110
<a name="l00111"></a>00111 <span class="comment">// Add a new clause. Lits is a vector of literal ID's. Note that this</span>
<a name="l00112"></a>00112 <span class="comment">// function can be called at any time, even after the search for solution has</span>
<a name="l00113"></a>00113 <span class="comment">// started. A clause ID is returned which can be used to refer to this</span>
<a name="l00114"></a>00114 <span class="comment">// clause in the future.</span>
<a name="l00115"></a>00115 <span class="keyword">virtual</span> Clause <a class="code" href="classSatSolver.html#a1fb269f00fd9da8242e2bad01967f097">AddClause</a>(std::vector<Lit>& lits)=0;
<a name="l00116"></a>00116
<a name="l00117"></a>00117 <span class="comment">// Delete a clause. This can only be done if the clause has unassigned</span>
<a name="l00118"></a>00118 <span class="comment">// literals and it must delete not only the clause in question, but</span>
<a name="l00119"></a>00119 <span class="comment">// any learned clauses which depend on it. Since this may be difficult to</span>
<a name="l00120"></a>00120 <span class="comment">// implement, implementing this function is not currently required.</span>
<a name="l00121"></a>00121 <span class="comment">// DeleteClause returns true if the clause was successfully deleted, and</span>
<a name="l00122"></a>00122 <span class="comment">// false otherwise.</span>
<a name="l00123"></a><a class="code" href="classSatSolver.html#a833d889d53fa2dbd609dac14625a5325">00123</a> <span class="keyword">virtual</span> <span class="keywordtype">bool</span> <a class="code" href="classSatSolver.html#a833d889d53fa2dbd609dac14625a5325">DeleteClause</a>(<a class="code" href="unionSatSolver_1_1Clause.html">Clause</a> clause) { <span class="keywordflow">return</span> <span class="keyword">false</span>; }
<a name="l00124"></a>00124
<a name="l00125"></a>00125 <span class="comment">// Get the clauseIndexth clause. clauseIndex must be between 0 and</span>
<a name="l00126"></a>00126 <span class="comment">// NumClauses()-1 inclusive.</span>
<a name="l00127"></a>00127 <span class="keyword">virtual</span> Clause <a class="code" href="classSatSolver.html#a3f5dcfdd713812059fdcba94bc6be3c1">GetClause</a>(<span class="keywordtype">int</span> clauseIndex)=0;
<a name="l00128"></a>00128
<a name="l00129"></a>00129 <span class="comment">// Get the first clause. Returns a NULL Clause if there are no clauses.</span>
<a name="l00130"></a>00130 <span class="keyword">virtual</span> Clause <a class="code" href="classSatSolver.html#a580f042cdf32047e73056dfd810226ad">GetFirstClause</a>()=0;
<a name="l00131"></a>00131
<a name="l00132"></a>00132 <span class="comment">// Get the next clause after clause. Returns a NULL Clause if clause is</span>
<a name="l00133"></a>00133 <span class="comment">// the last clause.</span>
<a name="l00134"></a>00134 <span class="keyword">virtual</span> Clause <a class="code" href="classSatSolver.html#a61ca72083b23704e2007f0c4b7414ff1">GetNextClause</a>(Clause clause)=0;
<a name="l00135"></a>00135
<a name="l00136"></a>00136 <span class="comment">// Returns in lits the literals that make up clause. lits is assumed to be</span>
<a name="l00137"></a>00137 <span class="comment">// empty when the function is called.</span>
<a name="l00138"></a>00138 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classSatSolver.html#af0c71f214e5980cf6848abaeaa3dbf16">GetClauseLits</a>(Clause clause, std::vector<Lit>* lits)=0;
<a name="l00139"></a>00139
<a name="l00140"></a>00140 <span class="comment"></span>
<a name="l00141"></a>00141 <span class="comment"> /////////////////////////////////////////////////////////////////////////////</span>
<a name="l00142"></a>00142 <span class="comment"></span> <span class="comment">// Checking Satisfiability and Retrieving Solutions //</span><span class="comment"></span>
<a name="l00143"></a>00143 <span class="comment"> /////////////////////////////////////////////////////////////////////////////</span>
<a name="l00144"></a>00144 <span class="comment"></span>
<a name="l00145"></a>00145
<a name="l00146"></a>00146 <span class="comment">// Main check for satisfiability. The parameter allowNewClauses tells the</span>
<a name="l00147"></a>00147 <span class="comment">// solver whether to expect additional clauses to be added by the API during</span>
<a name="l00148"></a>00148 <span class="comment">// the search for a solution. The default is that no new clauses will be</span>
<a name="l00149"></a>00149 <span class="comment">// added. If new clauses can be added, then certain optimizations such as</span>
<a name="l00150"></a>00150 <span class="comment">// the pure literal rule must be disabled.</span>
<a name="l00151"></a>00151 <span class="keyword">virtual</span> <a class="code" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53">SATStatus</a> <a class="code" href="classSatSolver.html#a0dfc1321f3446be70349f35881144433">Satisfiable</a>(<span class="keywordtype">bool</span> allowNewClauses=<span class="keyword">false</span>)=0;
<a name="l00152"></a>00152
<a name="l00153"></a>00153 <span class="comment">// Get current value of variable. -1=unassigned, 0=false, 1=true</span>
<a name="l00154"></a>00154 <span class="keyword">virtual</span> <span class="keywordtype">int</span> <a class="code" href="classSatSolver.html#a111b3a56be2feaae62bc57483f0aa9bf">GetVarAssignment</a>(<a class="code" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> var)=0;
<a name="l00155"></a>00155
<a name="l00156"></a>00156 <span class="comment">// After Satisfiable has returned with a SATISFIABLE result, this function</span>
<a name="l00157"></a>00157 <span class="comment">// may be called to search for the next satisfying assignment. If one is</span>
<a name="l00158"></a>00158 <span class="comment">// found then SATISFIABLE is returned. If there are no more satisfying</span>
<a name="l00159"></a>00159 <span class="comment">// assignments then UNSATISFIABLE is returned.</span>
<a name="l00160"></a>00160 <span class="keyword">virtual</span> <a class="code" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53">SATStatus</a> <a class="code" href="classSatSolver.html#ab4e73333fbc4b4372a18c66a40d4757f">Continue</a>()=0;
<a name="l00161"></a>00161
<a name="l00162"></a>00162 <span class="comment">// Pop all decision levels and remove all assignments, but do not delete any</span>
<a name="l00163"></a>00163 <span class="comment">// clauses</span>
<a name="l00164"></a>00164 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classSatSolver.html#aa05fce07f5c3363e2362a3b1de7795db">Restart</a>()=0;
<a name="l00165"></a>00165
<a name="l00166"></a>00166 <span class="comment">// Pop all decision levels, remove all assignments, and delete all clauses.</span>
<a name="l00167"></a>00167 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classSatSolver.html#ac64e81107b4b94fd1f6fb76b219a0517">Reset</a>()=0;
<a name="l00168"></a>00168
<a name="l00169"></a>00169 <span class="comment"></span>
<a name="l00170"></a>00170 <span class="comment"> /////////////////////////////////////////////////////////////////////////////</span>
<a name="l00171"></a>00171 <span class="comment"></span> <span class="comment">// Advanced Features //</span><span class="comment"></span>
<a name="l00172"></a>00172 <span class="comment"> /////////////////////////////////////////////////////////////////////////////</span>
<a name="l00173"></a>00173 <span class="comment"></span>
<a name="l00174"></a>00174
<a name="l00175"></a>00175 <span class="comment">// The following four methods allow callback functions to be registered.</span>
<a name="l00176"></a>00176 <span class="comment">// Each function that is registered may optionally provide a cookie (void *)</span>
<a name="l00177"></a>00177 <span class="comment">// which will be passed back to that function whenever it is called.</span>
<a name="l00178"></a>00178
<a name="l00179"></a>00179 <span class="comment">// Register a function f which is called every time the decision level</span>
<a name="l00180"></a>00180 <span class="comment">// increases or decreases (i.e. every time the stack is pushed or popped).</span>
<a name="l00181"></a>00181 <span class="comment">// The argument to f is the change in decision level. For example, +1 is a</span>
<a name="l00182"></a>00182 <span class="comment">// Push, -1 is a Pop.</span>
<a name="l00183"></a>00183 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classSatSolver.html#a2f5308d9fdff97f882186073f05d8874">RegisterDLevelHook</a>(<span class="keywordtype">void</span> (*f)(<span class="keywordtype">void</span> *, <span class="keywordtype">int</span>), <span class="keywordtype">void</span> *cookie)=0;
<a name="l00184"></a>00184
<a name="l00185"></a>00185 <span class="comment">// Register a function to replace the built-in decision heuristics. Every</span>
<a name="l00186"></a>00186 <span class="comment">// time a new decision needs to be made, the solver will call this function.</span>
<a name="l00187"></a>00187 <span class="comment">// The function should return a literal which should be set to true. If the</span>
<a name="l00188"></a>00188 <span class="comment">// bool pointer is returned with the value false, then a literal was</span>
<a name="l00189"></a>00189 <span class="comment">// successfully chosen. If the value is true, this signals the solver to</span>
<a name="l00190"></a>00190 <span class="comment">// exit with a satisfiable result. If the bool value is false and the</span>
<a name="l00191"></a>00191 <span class="comment">// literal is NULL, then this signals the solver to use its own internal</span>
<a name="l00192"></a>00192 <span class="comment">// method for making the next decision.</span>
<a name="l00193"></a>00193 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classSatSolver.html#a76cc15252a711e8a9a21e49a30d7e920">RegisterDecisionHook</a>(Lit (*f)(<span class="keywordtype">void</span> *, <span class="keywordtype">bool</span> *), <span class="keywordtype">void</span> *cookie)=0;
<a name="l00194"></a>00194
<a name="l00195"></a>00195 <span class="comment">// Register a function which is called every time the value of a variable is</span>
<a name="l00196"></a>00196 <span class="comment">// changed (i.e. assigned or unassigned). The first parameter is the</span>
<a name="l00197"></a>00197 <span class="comment">// variable ID which has changed. The second is the new value: -1=unassigned,</span>
<a name="l00198"></a>00198 <span class="comment">// 0=false, 1=true</span>
<a name="l00199"></a>00199 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classSatSolver.html#a658bb40c580f149024c59509e9e3acd0">RegisterAssignmentHook</a>(<span class="keywordtype">void</span> (*f)(<span class="keywordtype">void</span> *, <a class="code" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a>, <span class="keywordtype">int</span>),
<a name="l00200"></a>00200 <span class="keywordtype">void</span> *cookie)=0;
<a name="l00201"></a>00201
<a name="l00202"></a>00202 <span class="comment">// Register a function which will be called after Boolean propagation and</span>
<a name="l00203"></a>00203 <span class="comment">// before making a new decision. Note that the hook function may add new</span>
<a name="l00204"></a>00204 <span class="comment">// clauses and this should be handled correctly.</span>
<a name="l00205"></a>00205 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classSatSolver.html#a856cf7839d83dcc04ee421d2595fc671">RegisterDeductionHook</a>(<span class="keywordtype">void</span> (*f)(<span class="keywordtype">void</span> *), <span class="keywordtype">void</span> *cookie)=0;
<a name="l00206"></a>00206
<a name="l00207"></a>00207 <span class="comment"></span>
<a name="l00208"></a>00208 <span class="comment"> /////////////////////////////////////////////////////////////////////////////</span>
<a name="l00209"></a>00209 <span class="comment"></span> <span class="comment">// Setting Parameters //</span><span class="comment"></span>
<a name="l00210"></a>00210 <span class="comment"> /////////////////////////////////////////////////////////////////////////////</span>
<a name="l00211"></a>00211 <span class="comment"></span>
<a name="l00212"></a>00212
<a name="l00213"></a>00213 <span class="comment">// Implementations are not required to implement any of these</span>
<a name="l00214"></a>00214 <span class="comment">// parameter-adjusting routines. Each function will return true if the request</span>
<a name="l00215"></a>00215 <span class="comment">// is successful and false otherwise.</span>
<a name="l00216"></a>00216
<a name="l00217"></a>00217 <span class="comment">// Implementation will define budget. An example budget would be time.</span>
<a name="l00218"></a><a class="code" href="classSatSolver.html#ab6c0375792fa61834acc0e059b0f0215">00218</a> <span class="keyword">virtual</span> <span class="keywordtype">bool</span> <a class="code" href="classSatSolver.html#ab6c0375792fa61834acc0e059b0f0215">SetBudget</a>(<span class="keywordtype">int</span> budget) { <span class="keywordflow">return</span> <span class="keyword">false</span>; }
<a name="l00219"></a>00219
<a name="l00220"></a>00220 <span class="comment">// Set memory limit in bytes.</span>
<a name="l00221"></a><a class="code" href="classSatSolver.html#ae71ce584f847dd8f8cd79c15a1e18ac4">00221</a> <span class="keyword">virtual</span> <span class="keywordtype">bool</span> <a class="code" href="classSatSolver.html#ae71ce584f847dd8f8cd79c15a1e18ac4">SetMemLimit</a>(<span class="keywordtype">int</span> mem_limit) { <span class="keywordflow">return</span> <span class="keyword">false</span>; }
<a name="l00222"></a>00222
<a name="l00223"></a>00223 <span class="comment">// Set parameters controlling randomness. Implementation defines what this</span>
<a name="l00224"></a>00224 <span class="comment">// means.</span>
<a name="l00225"></a><a class="code" href="classSatSolver.html#a2d799de14b8f73985474b6e6bb391799">00225</a> <span class="keyword">virtual</span> <span class="keywordtype">bool</span> <a class="code" href="classSatSolver.html#a2d799de14b8f73985474b6e6bb391799">SetRandomness</a>(<span class="keywordtype">int</span> n) { <span class="keywordflow">return</span> <span class="keyword">false</span>; }
<a name="l00226"></a><a class="code" href="classSatSolver.html#a49baebbc72ee8480ce9b15931fd6a087">00226</a> <span class="keyword">virtual</span> <span class="keywordtype">bool</span> <a class="code" href="classSatSolver.html#a49baebbc72ee8480ce9b15931fd6a087">SetRandSeed</a>(<span class="keywordtype">int</span> seed) { <span class="keywordflow">return</span> <span class="keyword">false</span>; }
<a name="l00227"></a>00227
<a name="l00228"></a>00228 <span class="comment">// Enable or disable deletion of conflict clauses to help control memory.</span>
<a name="l00229"></a><a class="code" href="classSatSolver.html#aab2f83c7e7a2e0294904ff5c0fa3409d">00229</a> <span class="keyword">virtual</span> <span class="keywordtype">bool</span> <a class="code" href="classSatSolver.html#aab2f83c7e7a2e0294904ff5c0fa3409d">EnableClauseDeletion</a>() { <span class="keywordflow">return</span> <span class="keyword">false</span>; }
<a name="l00230"></a><a class="code" href="classSatSolver.html#ae4127dad23cea8d60a6eb2f5d0072554">00230</a> <span class="keyword">virtual</span> <span class="keywordtype">bool</span> <a class="code" href="classSatSolver.html#ae4127dad23cea8d60a6eb2f5d0072554">DisableClauseDeletion</a>() { <span class="keywordflow">return</span> <span class="keyword">false</span>; }
<a name="l00231"></a>00231
<a name="l00232"></a>00232 <span class="comment"></span>
<a name="l00233"></a>00233 <span class="comment"> ///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00234"></a>00234 <span class="comment"></span> <span class="comment">// Statistics //</span><span class="comment"></span>
<a name="l00235"></a>00235 <span class="comment"> ///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00236"></a>00236 <span class="comment"></span>
<a name="l00237"></a>00237
<a name="l00238"></a>00238 <span class="comment">// As with the parameter functions, the statistics-gathering functions may or</span>
<a name="l00239"></a>00239 <span class="comment">// may not be implemented. They return -1 if not implemented, and the</span>
<a name="l00240"></a>00240 <span class="comment">// correct value otherwise.</span>
<a name="l00241"></a>00241
<a name="l00242"></a>00242 <span class="comment">// Return the amount of the budget (set by SetBudget) which has been used</span>
<a name="l00243"></a><a class="code" href="classSatSolver.html#a9ab0d5988fd6b737626eddfdfb3086ca">00243</a> <span class="keyword">virtual</span> <span class="keywordtype">int</span> <a class="code" href="classSatSolver.html#a9ab0d5988fd6b737626eddfdfb3086ca">GetBudgetUsed</a>() { <span class="keywordflow">return</span> -1; }
<a name="l00244"></a>00244
<a name="l00245"></a>00245 <span class="comment">// Return the amount of memory in use</span>
<a name="l00246"></a><a class="code" href="classSatSolver.html#a409a256b9b590f8881690422ac34f566">00246</a> <span class="keyword">virtual</span> <span class="keywordtype">int</span> <a class="code" href="classSatSolver.html#a409a256b9b590f8881690422ac34f566">GetMemUsed</a>() { <span class="keywordflow">return</span> -1; }
<a name="l00247"></a>00247
<a name="l00248"></a>00248 <span class="comment">// Return the number of decisions made so far</span>
<a name="l00249"></a><a class="code" href="classSatSolver.html#a2a416ee5b49d9cf91a57c5b9e71388b8">00249</a> <span class="keyword">virtual</span> <span class="keywordtype">int</span> <a class="code" href="classSatSolver.html#a2a416ee5b49d9cf91a57c5b9e71388b8">GetNumDecisions</a>() { <span class="keywordflow">return</span> -1; }
<a name="l00250"></a>00250
<a name="l00251"></a>00251 <span class="comment">// Return the number of conflicts (equal to the number of backtracks)</span>
<a name="l00252"></a><a class="code" href="classSatSolver.html#ab81836241806bc37ca6c5cfcd1a77df4">00252</a> <span class="keyword">virtual</span> <span class="keywordtype">int</span> <a class="code" href="classSatSolver.html#ab81836241806bc37ca6c5cfcd1a77df4">GetNumConflicts</a>() { <span class="keywordflow">return</span> -1; }
<a name="l00253"></a>00253
<a name="l00254"></a>00254 <span class="comment">// Return the number of conflicts generated by the registered external</span>
<a name="l00255"></a>00255 <span class="comment">// conflict generator</span>
<a name="l00256"></a><a class="code" href="classSatSolver.html#af11d56356aa9a578f0baaa4cbcdc0b97">00256</a> <span class="keyword">virtual</span> <span class="keywordtype">int</span> <a class="code" href="classSatSolver.html#af11d56356aa9a578f0baaa4cbcdc0b97">GetNumExtConflicts</a>() { <span class="keywordflow">return</span> -1; }
<a name="l00257"></a>00257
<a name="l00258"></a>00258 <span class="comment">// Return the elapsed CPU time (in seconds) since the call to Satisfiable()</span>
<a name="l00259"></a><a class="code" href="classSatSolver.html#ab1d30058d42aecba7708cb9e29cbda67">00259</a> <span class="keyword">virtual</span> <span class="keywordtype">float</span> <a class="code" href="classSatSolver.html#ab1d30058d42aecba7708cb9e29cbda67">GetTotalTime</a>() { <span class="keywordflow">return</span> -1; }
<a name="l00260"></a>00260
<a name="l00261"></a>00261 <span class="comment">// Return the CPU time spent (in seconds) inside the SAT solver</span>
<a name="l00262"></a>00262 <span class="comment">// (as opposed to in the registered hook functions)</span>
<a name="l00263"></a><a class="code" href="classSatSolver.html#a4af09fc1738959db1c0d197a4fbf8a6a">00263</a> <span class="keyword">virtual</span> <span class="keywordtype">float</span> <a class="code" href="classSatSolver.html#a4af09fc1738959db1c0d197a4fbf8a6a">GetSATTime</a>() { <span class="keywordflow">return</span> -1; }
<a name="l00264"></a>00264
<a name="l00265"></a>00265 <span class="comment">// Return the total number of literals in all clauses</span>
<a name="l00266"></a><a class="code" href="classSatSolver.html#a6f617ce6eae22b959f135d347776cb27">00266</a> <span class="keyword">virtual</span> <span class="keywordtype">int</span> <a class="code" href="classSatSolver.html#a6f617ce6eae22b959f135d347776cb27">GetNumLiterals</a>() { <span class="keywordflow">return</span> -1; }
<a name="l00267"></a>00267
<a name="l00268"></a>00268 <span class="comment">// Return the number of clauses that were deleted</span>
<a name="l00269"></a><a class="code" href="classSatSolver.html#a6499994eb391919ce6542412e3e43d01">00269</a> <span class="keyword">virtual</span> <span class="keywordtype">int</span> <a class="code" href="classSatSolver.html#a6499994eb391919ce6542412e3e43d01">GetNumDeletedClauses</a>() { <span class="keywordflow">return</span> -1; }
<a name="l00270"></a>00270
<a name="l00271"></a>00271 <span class="comment">// Return the total number of literals in all deleted clauses</span>
<a name="l00272"></a><a class="code" href="classSatSolver.html#ab81eb4127972de38906425ba4babfadc">00272</a> <span class="keyword">virtual</span> <span class="keywordtype">int</span> <a class="code" href="classSatSolver.html#ab81eb4127972de38906425ba4babfadc">GetNumDeletedLiterals</a>() { <span class="keywordflow">return</span> -1; }
<a name="l00273"></a>00273
<a name="l00274"></a>00274 <span class="comment">// Return the number of unit propagations</span>
<a name="l00275"></a><a class="code" href="classSatSolver.html#a45923d3ff1c6145198098d7e689c23f0">00275</a> <span class="keyword">virtual</span> <span class="keywordtype">int</span> <a class="code" href="classSatSolver.html#a45923d3ff1c6145198098d7e689c23f0">GetNumImplications</a>() { <span class="keywordflow">return</span> -1; }
<a name="l00276"></a>00276
<a name="l00277"></a>00277 <span class="comment">// Return the maximum decision level reached</span>
<a name="l00278"></a><a class="code" href="classSatSolver.html#a74190d9fc4abdb54fc65c4efffdf75fc">00278</a> <span class="keyword">virtual</span> <span class="keywordtype">int</span> <a class="code" href="classSatSolver.html#a74190d9fc4abdb54fc65c4efffdf75fc">GetMaxDLevel</a>() { <span class="keywordflow">return</span> -1; }
<a name="l00279"></a>00279
<a name="l00280"></a>00280 <span class="comment">// Print all implemented statistics</span>
<a name="l00281"></a>00281 <span class="keywordtype">void</span> <a class="code" href="classSatSolver.html#a1e57a5f44892f0ef08a487a1516030df">PrintStatistics</a>(std::ostream & os = std::cout);
<a name="l00282"></a>00282
<a name="l00283"></a>00283 };
<a name="l00284"></a>00284
<a name="l00285"></a>00285 <span class="preprocessor">#endif</span>
</pre></div></div>
</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>
