Fast SAT Solver (C++, GAlib)
File detail
Source code
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html><head><meta http-equiv="Content-Type" content="text/html;charset=UTF-8">
<title>Fast SAT Solver: SatSolver.h Source File</title>
<link href="doxygen.css" rel="stylesheet" type="text/css">
<link href="tabs.css" rel="stylesheet" type="text/css">
</head><body>
<!-- Generated by Doxygen 1.5.4 -->
<div class="tabs">
<ul>
<li><a href="index.html"><span>Main Page</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>
<h1>SatSolver.h</h1><a href="SatSolver_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"> * Copyright (C) 2008 Kamil Dudka <xdudka00@stud.fit.vutbr.cz></span>
<a name="l00003"></a>00003 <span class="comment"> *</span>
<a name="l00004"></a>00004 <span class="comment"> * This file is part of fss (Fast SAT Solver).</span>
<a name="l00005"></a>00005 <span class="comment"> *</span>
<a name="l00006"></a>00006 <span class="comment"> * fss is free software: you can redistribute it and/or modify</span>
<a name="l00007"></a>00007 <span class="comment"> * it under the terms of the GNU General Public License as published by</span>
<a name="l00008"></a>00008 <span class="comment"> * the Free Software Foundation, either version 3 of the License, or</span>
<a name="l00009"></a>00009 <span class="comment"> * any later version.</span>
<a name="l00010"></a>00010 <span class="comment"> *</span>
<a name="l00011"></a>00011 <span class="comment"> * fss is distributed in the hope that it will be useful,</span>
<a name="l00012"></a>00012 <span class="comment"> * but WITHOUT ANY WARRANTY; without even the implied warranty of</span>
<a name="l00013"></a>00013 <span class="comment"> * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the</span>
<a name="l00014"></a>00014 <span class="comment"> * GNU General Public License for more details.</span>
<a name="l00015"></a>00015 <span class="comment"> *</span>
<a name="l00016"></a>00016 <span class="comment"> * You should have received a copy of the GNU General Public License</span>
<a name="l00017"></a>00017 <span class="comment"> * along with fss. If not, see <http://www.gnu.org/licenses/>.</span>
<a name="l00018"></a>00018 <span class="comment"> */</span>
<a name="l00019"></a>00019
<a name="l00020"></a>00020 <span class="preprocessor">#ifndef SATSOLVER_H</span>
<a name="l00021"></a>00021 <span class="preprocessor"></span><span class="preprocessor">#define SATSOLVER_H</span>
<a name="l00022"></a>00022 <span class="preprocessor"></span>
<a name="l00031"></a>00031 <span class="preprocessor">#include <iostream></span>
<a name="l00032"></a>00032
<a name="l00033"></a>00033 <span class="keyword">namespace </span>FastSatSolver {
<a name="l00034"></a>00034 <span class="keyword">class </span>SatProblem;
<a name="l00035"></a>00035
<a name="l00042"></a><a class="code" href="classFastSatSolver_1_1ISatItem.html">00042</a> <span class="keyword">class </span><a class="code" href="classFastSatSolver_1_1ISatItem.html" title="Abstraction of solution candidate.">ISatItem</a>
<a name="l00043"></a>00043 {
<a name="l00044"></a>00044 <span class="keyword">public</span>:
<a name="l00045"></a><a class="code" href="classFastSatSolver_1_1ISatItem.html#9f0605e5663967052715e5b9370f88a2">00045</a> <span class="keyword">virtual</span> <a class="code" href="classFastSatSolver_1_1ISatItem.html#9f0605e5663967052715e5b9370f88a2">~ISatItem</a>() { }
<a name="l00046"></a>00046
<a name="l00051"></a>00051 <span class="keyword">virtual</span> <a class="code" href="classFastSatSolver_1_1ISatItem.html" title="Abstraction of solution candidate.">ISatItem</a>* <a class="code" href="classFastSatSolver_1_1ISatItem.html#ce35793be43d099862210ca953c725df" title="Returns clone of object&#39;s instance.">clone</a>() <span class="keyword">const</span> = 0;
<a name="l00052"></a>00052
<a name="l00057"></a>00057 <span class="keyword">virtual</span> <span class="keywordtype">int</span> <a class="code" href="classFastSatSolver_1_1ISatItem.html#0e6dd5fad9ead809b933defcdb4cc872" title="Returns count of bits (resp. variables) managed by object.">getLength</a> ( ) <span class="keyword">const</span> = 0;
<a name="l00058"></a>00058
<a name="l00063"></a>00063 <span class="keyword">virtual</span> <span class="keywordtype">bool</span> <a class="code" href="classFastSatSolver_1_1ISatItem.html#ef9eadbc8fd10e01f1b37f85c6e08a67" title="Returns value of desired bit (resp. variable).">getBit</a> (<span class="keywordtype">int</span> index ) <span class="keyword">const</span> = 0;
<a name="l00064"></a>00064 };
<a name="l00065"></a>00065
<a name="l00072"></a><a class="code" href="classFastSatSolver_1_1IObserver.html">00072</a> <span class="keyword">class </span><a class="code" href="classFastSatSolver_1_1IObserver.html" title="Simple observer&#39;s base class.">IObserver</a> {
<a name="l00073"></a>00073 <span class="keyword">public</span>:
<a name="l00074"></a><a class="code" href="classFastSatSolver_1_1IObserver.html#46df16d3047dd26f7eeaf8eef5709ccc">00074</a> <span class="keyword">virtual</span> <a class="code" href="classFastSatSolver_1_1IObserver.html#46df16d3047dd26f7eeaf8eef5709ccc">~IObserver</a>() { }
<a name="l00075"></a>00075
<a name="l00081"></a>00081 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1IObserver.html#db968cb3b9d5c0f9c62efbc1ea91de8d" title="Event notification, usually called by object implementing ISubject interface.">notify</a>() = 0;
<a name="l00082"></a>00082 };
<a name="l00083"></a>00083
<a name="l00090"></a><a class="code" href="classFastSatSolver_1_1ISubject.html">00090</a> <span class="keyword">class </span><a class="code" href="classFastSatSolver_1_1ISubject.html" title="Simple observer&#39;s subject base class.">ISubject</a> {
<a name="l00091"></a>00091 <span class="keyword">public</span>:
<a name="l00092"></a><a class="code" href="classFastSatSolver_1_1ISubject.html#221403938ce121b07e1939a03345ee24">00092</a> <span class="keyword">virtual</span> <a class="code" href="classFastSatSolver_1_1ISubject.html#221403938ce121b07e1939a03345ee24">~ISubject</a>() { }
<a name="l00093"></a>00093
<a name="l00101"></a>00101 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1ISubject.html#667a901632cfa1cf55790fed03a615c6" title="Add observer to list of listeners.">addObserver</a>(<a class="code" href="classFastSatSolver_1_1IObserver.html" title="Simple observer&#39;s base class.">IObserver</a> *observer) = 0;
<a name="l00102"></a>00102 };
<a name="l00103"></a>00103
<a name="l00104"></a>00104
<a name="l00110"></a><a class="code" href="classFastSatSolver_1_1AbstractSubject.html">00110</a> <span class="keyword">class </span><a class="code" href="classFastSatSolver_1_1AbstractSubject.html" title="Simple subject&#39;s base class.">AbstractSubject</a>: <span class="keyword">public</span> <a class="code" href="classFastSatSolver_1_1ISubject.html" title="Simple observer&#39;s subject base class.">ISubject</a> {
<a name="l00111"></a>00111 <span class="keyword">public</span>:
<a name="l00112"></a>00112 <span class="keyword">virtual</span> <a class="code" href="classFastSatSolver_1_1AbstractSubject.html#2c587a73a35eb4ea598134d72c8838b6">~AbstractSubject</a>();
<a name="l00113"></a>00113
<a name="l00114"></a>00114 <span class="comment">// see ISubject dox</span>
<a name="l00115"></a>00115 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1AbstractSubject.html#05bf56954cced132e03ec548c0557c88" title="Add observer to list of listeners.">addObserver</a>(<a class="code" href="classFastSatSolver_1_1IObserver.html" title="Simple observer&#39;s base class.">IObserver</a> *);
<a name="l00116"></a>00116 <span class="keyword">protected</span>:
<a name="l00117"></a>00117 <a class="code" href="classFastSatSolver_1_1AbstractSubject.html#a865e4c695bceddbeb387cd07b68e8db">AbstractSubject</a>();
<a name="l00118"></a>00118
<a name="l00124"></a>00124 <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1AbstractSubject.html#7ff19734eb024bd6f3e2ad95647b1b27" title="Send notification to all observers (listeners).">notify</a>();
<a name="l00125"></a>00125 <span class="keyword">private</span>:
<a name="l00126"></a>00126 <span class="keyword">struct </span><a class="code" href="structFastSatSolver_1_1AbstractSubject_1_1Private.html">Private</a>;
<a name="l00127"></a>00127 <a class="code" href="structFastSatSolver_1_1AbstractSubject_1_1Private.html">Private</a> *d;
<a name="l00128"></a>00128 };
<a name="l00129"></a>00129
<a name="l00135"></a><a class="code" href="classFastSatSolver_1_1IProcess.html">00135</a> <span class="keyword">class </span><a class="code" href="classFastSatSolver_1_1IProcess.html" title="Continous process interface.">IProcess</a> {
<a name="l00136"></a>00136 <span class="keyword">public</span>:
<a name="l00137"></a><a class="code" href="classFastSatSolver_1_1IProcess.html#3d6c1ead1183c80f1c5d6a53c2cbd21d">00137</a> <span class="keyword">virtual</span> <a class="code" href="classFastSatSolver_1_1IProcess.html#3d6c1ead1183c80f1c5d6a53c2cbd21d">~IProcess</a>() { }
<a name="l00138"></a>00138
<a name="l00143"></a>00143 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1IProcess.html#c0ae5f26cd2001d772aed9d2ea97d41c" title="Start process execution. This method returns control after process ends (or after...">start</a>() = 0;
<a name="l00144"></a>00144
<a name="l00148"></a>00148 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1IProcess.html#0efff8623a2fb79dad94a96dcf16d966" title="Stop currently executed process as soon as possible.">stop</a>() = 0;
<a name="l00149"></a>00149
<a name="l00154"></a>00154 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1IProcess.html#20dcbdfbd0ec77afc802522bb7e379c1" title="Reset process to its initial state.">reset</a>() = 0;
<a name="l00155"></a>00155 };
<a name="l00156"></a>00156
<a name="l00162"></a><a class="code" href="classFastSatSolver_1_1AbstractProcess.html">00162</a> <span class="keyword">class </span><a class="code" href="classFastSatSolver_1_1AbstractProcess.html" title="Base class of simple multi-step process.">AbstractProcess</a>:
<a name="l00163"></a>00163 <span class="keyword">public</span> <a class="code" href="classFastSatSolver_1_1AbstractSubject.html" title="Simple subject&#39;s base class.">AbstractSubject</a>,
<a name="l00164"></a>00164 <span class="keyword">public</span> <a class="code" href="classFastSatSolver_1_1IProcess.html" title="Continous process interface.">IProcess</a>
<a name="l00165"></a>00165 {
<a name="l00166"></a>00166 <span class="keyword">public</span>:
<a name="l00167"></a>00167 <span class="keyword">virtual</span> <a class="code" href="classFastSatSolver_1_1AbstractProcess.html#afd04fedb2739aea43546da557be9f29">~AbstractProcess</a>();
<a name="l00168"></a>00168 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1AbstractProcess.html#60de64d75454385b23995437f1d72669" title="Start process execution. This method returns control after process ends (or after...">start</a>();
<a name="l00169"></a>00169 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1AbstractProcess.html#8c528baf37154d347366083f0f816846" title="Stop currently executed process as soon as possible.">stop</a>();
<a name="l00170"></a>00170 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1AbstractProcess.html#d20897c5c8bd47f5d4005989bead0e55" title="Reset process to its initial state.">reset</a>();
<a name="l00171"></a>00171
<a name="l00176"></a>00176 <span class="keyword">virtual</span> <span class="keywordtype">int</span> <a class="code" href="classFastSatSolver_1_1AbstractProcess.html#14fa4258dc9ab261c5d4026ae3dfc882" title="Returns current step number.">getStepsCount</a>();
<a name="l00177"></a>00177 <span class="keyword">protected</span>:
<a name="l00178"></a>00178 <a class="code" href="classFastSatSolver_1_1AbstractProcess.html#c652d47533d553b2e07ea7367eda6038">AbstractProcess</a>();
<a name="l00179"></a>00179
<a name="l00184"></a>00184 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1AbstractProcess.html#a5085af8ee5e5c39b4c20c60231e5c92" title="Initialize process.">initialize</a>() = 0;
<a name="l00185"></a>00185
<a name="l00190"></a>00190 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1AbstractProcess.html#f40573eed2567df340143a72ddb6cd69" title="Do one step of process.">doStep</a>() = 0;
<a name="l00191"></a>00191 <span class="keyword">private</span>:
<a name="l00192"></a>00192 <span class="keyword">struct </span><a class="code" href="structFastSatSolver_1_1AbstractSubject_1_1Private.html">Private</a>;
<a name="l00193"></a>00193 <a class="code" href="structFastSatSolver_1_1AbstractSubject_1_1Private.html">Private</a> *d;
<a name="l00194"></a>00194 };
<a name="l00195"></a>00195
<a name="l00201"></a><a class="code" href="classFastSatSolver_1_1IStopWatch.html">00201</a> <span class="keyword">class </span><a class="code" href="classFastSatSolver_1_1IStopWatch.html" title="Interface of time-watchable activity.">IStopWatch</a> {
<a name="l00202"></a>00202 <span class="keyword">public</span>:
<a name="l00203"></a><a class="code" href="classFastSatSolver_1_1IStopWatch.html#341e2c27d7708e952b38c5b3094244ec">00203</a> <span class="keyword">virtual</span> <a class="code" href="classFastSatSolver_1_1IStopWatch.html#341e2c27d7708e952b38c5b3094244ec">~IStopWatch</a>() { }
<a name="l00204"></a>00204
<a name="l00209"></a>00209 <span class="keyword">virtual</span> <span class="keywordtype">long</span> <a class="code" href="classFastSatSolver_1_1IStopWatch.html#f649f409444bc5f814164e072a4c38e7" title="Returns time elapsed by activity.">getTimeElapsed</a>() = 0;
<a name="l00210"></a>00210 };
<a name="l00211"></a>00211
<a name="l00217"></a><a class="code" href="classFastSatSolver_1_1AbstractProcessWatched.html">00217</a> <span class="keyword">class </span><a class="code" href="classFastSatSolver_1_1AbstractProcessWatched.html" title="Multi-step process with time-watch extension.">AbstractProcessWatched</a>:
<a name="l00218"></a>00218 <span class="keyword">public</span> <a class="code" href="classFastSatSolver_1_1AbstractProcess.html" title="Base class of simple multi-step process.">AbstractProcess</a>,
<a name="l00219"></a>00219 <span class="keyword">public</span> <a class="code" href="classFastSatSolver_1_1IStopWatch.html" title="Interface of time-watchable activity.">IStopWatch</a>
<a name="l00220"></a>00220 {
<a name="l00221"></a>00221 <span class="keyword">public</span>:
<a name="l00222"></a>00222 <span class="keyword">virtual</span> <a class="code" href="classFastSatSolver_1_1AbstractProcessWatched.html#05e8cb6c6d5c68d6d7b4b8b122bf529b">~AbstractProcessWatched</a>();
<a name="l00223"></a>00223 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1AbstractProcessWatched.html#60de64d75454385b23995437f1d72669" title="Start process execution. This method returns control after process ends (or after...">start</a>();
<a name="l00224"></a>00224 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1AbstractProcessWatched.html#8c528baf37154d347366083f0f816846" title="Stop currently executed process as soon as possible.">stop</a>();
<a name="l00225"></a>00225 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1AbstractProcessWatched.html#d20897c5c8bd47f5d4005989bead0e55" title="Reset process to its initial state.">reset</a>();
<a name="l00226"></a>00226 <span class="keyword">virtual</span> <span class="keywordtype">long</span> <a class="code" href="classFastSatSolver_1_1AbstractProcessWatched.html#57e2ab43bf94f9adc686e788f8771681" title="Returns time elapsed by activity.">getTimeElapsed</a>();
<a name="l00227"></a>00227 <span class="keyword">protected</span>:
<a name="l00228"></a>00228 <a class="code" href="classFastSatSolver_1_1AbstractProcessWatched.html#f6310c38aa477863afc576fac02f1110">AbstractProcessWatched</a>();
<a name="l00229"></a>00229 <span class="keyword">private</span>:
<a name="l00230"></a>00230 <span class="keyword">struct </span><a class="code" href="structFastSatSolver_1_1AbstractSubject_1_1Private.html">Private</a>;
<a name="l00231"></a>00231 <a class="code" href="structFastSatSolver_1_1AbstractSubject_1_1Private.html">Private</a> *d;
<a name="l00232"></a>00232 };
<a name="l00233"></a>00233
<a name="l00240"></a><a class="code" href="classFastSatSolver_1_1SatItemVector.html">00240</a> <span class="keyword">class </span><a class="code" href="classFastSatSolver_1_1SatItemVector.html" title="Linear storage container for ISatItem objects.">SatItemVector</a> {
<a name="l00241"></a>00241 <span class="keyword">public</span>:
<a name="l00242"></a>00242 <a class="code" href="classFastSatSolver_1_1SatItemVector.html#fab085d58e8b05bfcf4065c4d6af9c67">SatItemVector</a>();
<a name="l00243"></a>00243 <a class="code" href="classFastSatSolver_1_1SatItemVector.html#fab085d58e8b05bfcf4065c4d6af9c67">SatItemVector</a>(<span class="keyword">const</span> <a class="code" href="classFastSatSolver_1_1SatItemVector.html" title="Linear storage container for ISatItem objects.">SatItemVector</a> &);
<a name="l00244"></a>00244 <a class="code" href="classFastSatSolver_1_1SatItemVector.html#6f497951e23c4434580791ec5096a271">~SatItemVector</a>();
<a name="l00245"></a>00245
<a name="l00249"></a>00249 <span class="keywordtype">int</span> <a class="code" href="classFastSatSolver_1_1SatItemVector.html#f59b115e86eaeac1f15673766852e428" title="Returns count of item managed by container.">getLength</a>() <span class="keyword">const</span>;
<a name="l00250"></a>00250
<a name="l00256"></a>00256 <a class="code" href="classFastSatSolver_1_1ISatItem.html" title="Abstraction of solution candidate.">ISatItem</a>* <a class="code" href="classFastSatSolver_1_1SatItemVector.html#e9908ff1674579e6a5ed8729dace445d" title="Direct access container item.">getItem</a>(<span class="keywordtype">int</span> index) <span class="keyword">const</span>;
<a name="l00257"></a>00257
<a name="l00264"></a>00264 <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1SatItemVector.html#e50e61bb65bb3328f6afbd8e005cb96f" title="Add item to container.">addItem</a>(<a class="code" href="classFastSatSolver_1_1ISatItem.html" title="Abstraction of solution candidate.">ISatItem</a> *item);
<a name="l00265"></a>00265
<a name="l00269"></a>00269 <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1SatItemVector.html#c8bb3912a3ce86b15842e79d0b421204" title="Remove all item from container and free from memory.">clear</a>();
<a name="l00270"></a>00270
<a name="l00277"></a>00277 <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1SatItemVector.html#3c0c3fdc04f467c4dcb62eabb407acc2" title="Human readable container dump.">writeOut</a>(<a class="code" href="classFastSatSolver_1_1SatProblem.html" title="SAT Problem module&#39;s facade.">SatProblem</a> *, std::ostream &streamTo) <span class="keyword">const</span>;
<a name="l00278"></a>00278 <span class="keyword">private</span>:
<a name="l00279"></a>00279 <span class="keyword">struct </span><a class="code" href="structFastSatSolver_1_1SatItemVector_1_1Private.html">Private</a>;
<a name="l00280"></a>00280 <a class="code" href="structFastSatSolver_1_1SatItemVector_1_1Private.html">Private</a> *d;
<a name="l00281"></a>00281 };
<a name="l00282"></a>00282
<a name="l00289"></a><a class="code" href="classFastSatSolver_1_1SatItemSet.html">00289</a> <span class="keyword">class </span><a class="code" href="classFastSatSolver_1_1SatItemSet.html" title="Associative array for ISatItem objects.">SatItemSet</a> {
<a name="l00290"></a>00290 <span class="keyword">public</span>:
<a name="l00291"></a>00291 <a class="code" href="classFastSatSolver_1_1SatItemSet.html#833d48be9570b6fe7286c0649058d7c1">SatItemSet</a>();
<a name="l00292"></a>00292 <a class="code" href="classFastSatSolver_1_1SatItemSet.html#a374f535d376a6adb5744cac83f0c52a">~SatItemSet</a>();
<a name="l00293"></a>00293
<a name="l00297"></a>00297 <span class="keywordtype">int</span> <a class="code" href="classFastSatSolver_1_1SatItemSet.html#ab0d4bbd0884d04dbe281cc2b9d21206" title="Returns count of item managed by container.">getLength</a>();
<a name="l00298"></a>00298
<a name="l00305"></a>00305 <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1SatItemSet.html#e50e61bb65bb3328f6afbd8e005cb96f" title="Add item to container, if it hasn&#39;t been there before.">addItem</a>(<a class="code" href="classFastSatSolver_1_1ISatItem.html" title="Abstraction of solution candidate.">ISatItem</a> *item);
<a name="l00306"></a>00306
<a name="l00311"></a>00311 <a class="code" href="classFastSatSolver_1_1SatItemVector.html" title="Linear storage container for ISatItem objects.">SatItemVector</a>* <a class="code" href="classFastSatSolver_1_1SatItemSet.html#1ec6a07165be87a359b04ee833c0a283" title="Export container&#39;s content to SatItemVector.">createVector</a>();
<a name="l00312"></a>00312
<a name="l00316"></a>00316 <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1SatItemSet.html#c8bb3912a3ce86b15842e79d0b421204" title="Remove all item from container and free from memory.">clear</a>();
<a name="l00317"></a>00317 <span class="keyword">private</span>:
<a name="l00318"></a>00318 <span class="keyword">struct </span><a class="code" href="structFastSatSolver_1_1SatItemSet_1_1Private.html">Private</a>;
<a name="l00319"></a>00319 <a class="code" href="structFastSatSolver_1_1SatItemSet_1_1Private.html">Private</a> *d;
<a name="l00320"></a>00320 };
<a name="l00321"></a>00321
<a name="l00328"></a><a class="code" href="classFastSatSolver_1_1AbstractSatSolver.html">00328</a> <span class="keyword">class </span><a class="code" href="classFastSatSolver_1_1AbstractSatSolver.html" title="SAT Solver base class.">AbstractSatSolver</a>: <span class="keyword">public</span> <a class="code" href="classFastSatSolver_1_1AbstractProcessWatched.html" title="Multi-step process with time-watch extension.">AbstractProcessWatched</a>
<a name="l00329"></a>00329 {
<a name="l00330"></a>00330 <span class="keyword">public</span>:
<a name="l00331"></a>00331 <span class="keyword">virtual</span> <a class="code" href="classFastSatSolver_1_1AbstractSatSolver.html#fae336fb16e0c147d36ad94b8bff70a5">~AbstractSatSolver</a>();
<a name="l00332"></a>00332
<a name="l00337"></a>00337 <span class="keyword">virtual</span> <a class="code" href="classFastSatSolver_1_1SatProblem.html" title="SAT Problem module&#39;s facade.">SatProblem</a>* <a class="code" href="classFastSatSolver_1_1AbstractSatSolver.html#bf3d0f5a5273e99c718f39966456814b" title="Returns pointer to instance of SatProblem used by solver.">getProblem</a>() = 0;
<a name="l00338"></a>00338
<a name="l00343"></a>00343 <span class="keyword">virtual</span> <span class="keywordtype">int</span> <a class="code" href="classFastSatSolver_1_1AbstractSatSolver.html#f70c2c7822e8a563a1685c9b68d5cc4a" title="Returns current count solutions founded by solver.">getSolutionsCount</a>() = 0;
<a name="l00344"></a>00344
<a name="l00350"></a>00350 <span class="keyword">virtual</span> <a class="code" href="classFastSatSolver_1_1SatItemVector.html" title="Linear storage container for ISatItem objects.">SatItemVector</a>* <a class="code" href="classFastSatSolver_1_1AbstractSatSolver.html#958ccb4759e38d9941f37717cf860bce" title="Returns a set of solutions founded by solver.">getSolutionVector</a>() = 0;
<a name="l00351"></a>00351
<a name="l00355"></a>00355 <span class="keyword">virtual</span> <span class="keywordtype">float</span> <a class="code" href="classFastSatSolver_1_1AbstractSatSolver.html#d1d0057d2029d7bfbf25323ab7c3b6ec" title="Returns fitness of the Worst solution managed by solver.">minFitness</a>() = 0;
<a name="l00356"></a>00356
<a name="l00360"></a>00360 <span class="keyword">virtual</span> <span class="keywordtype">float</span> <a class="code" href="classFastSatSolver_1_1AbstractSatSolver.html#1d214769e7d45e9fd04601b31adb8c70" title="Returns average fitness computed by solver.">avgFitness</a>() = 0;
<a name="l00361"></a>00361
<a name="l00366"></a>00366 <span class="keyword">virtual</span> <span class="keywordtype">float</span> <a class="code" href="classFastSatSolver_1_1AbstractSatSolver.html#5f493f0ddbb31c2e3fa53153b67501e6" title="Returns the Best fitness founded by solver.">maxFitness</a>() = 0;
<a name="l00367"></a>00367
<a name="l00368"></a>00368 <span class="keyword">protected</span>:
<a name="l00369"></a>00369 <a class="code" href="classFastSatSolver_1_1AbstractSatSolver.html#6716df2cfc865894f1d26905c27bdc19">AbstractSatSolver</a>();
<a name="l00370"></a>00370
<a name="l00371"></a>00371 <span class="keyword">private</span>:
<a name="l00372"></a>00372 <span class="keyword">struct </span><a class="code" href="structFastSatSolver_1_1AbstractSubject_1_1Private.html">Private</a>;
<a name="l00373"></a>00373 <a class="code" href="structFastSatSolver_1_1AbstractSubject_1_1Private.html">Private</a> *d;
<a name="l00374"></a>00374 };
<a name="l00375"></a>00375
<a name="l00376"></a>00376 } <span class="comment">// namespace FastSatSolver</span>
<a name="l00377"></a>00377
<a name="l00378"></a>00378 <span class="preprocessor">#endif // SATSOLVER_H</span>
</pre></div><hr size="1"><address style="text-align: right;"><small>Generated on Wed Nov 5 22:30:22 2008 for Fast SAT Solver by
<a href="http://www.doxygen.org/index.html">
<img src="doxygen.png" alt="doxygen" align="middle" border="0"></a> 1.5.4 </small></address>
</body>
</html>
Back to main page
SatSolver_8h-source.html [Download]