Fast SAT Solver (C++, GAlib)
Detail souboru
Zdrojový kód
<!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.cpp 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.cpp</h1><a href="SatSolver_8cpp.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">#include <time.h></span>
<a name="l00021"></a>00021 <span class="preprocessor">#include <iostream></span>
<a name="l00022"></a>00022 <span class="preprocessor">#include <iomanip></span>
<a name="l00023"></a>00023 <span class="preprocessor">#include <list></span>
<a name="l00024"></a>00024 <span class="preprocessor">#include <vector></span>
<a name="l00025"></a>00025 <span class="preprocessor">#include <set></span>
<a name="l00026"></a>00026 <span class="preprocessor">#include "<a class="code" href="fssIO_8h.html" title="I/O module.">fssIO.h</a>"</span>
<a name="l00027"></a>00027 <span class="preprocessor">#include "<a class="code" href="SatProblem_8h.html" title="SAT Problem representation.">SatProblem.h</a>"</span>
<a name="l00028"></a>00028 <span class="preprocessor">#include "<a class="code" href="SatSolver_8h.html" title="ISatItem, IObserver and AbstractSatSolver with its base classes.">SatSolver.h</a>"</span>
<a name="l00029"></a>00029
<a name="l00030"></a>00030 <span class="keyword">namespace </span>FastSatSolver {
<a name="l00031"></a>00031
<a name="l00032"></a>00032 <span class="comment">// ////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////</span>
<a name="l00033"></a>00033 <span class="comment">// AbstractSubject implementation</span>
<a name="l00034"></a><a class="code" href="structFastSatSolver_1_1AbstractSubject_1_1Private.html">00034</a> <span class="keyword">struct </span><a class="code" href="structFastSatSolver_1_1AbstractSubject_1_1Private.html">AbstractSubject::Private</a> {
<a name="l00035"></a><a class="code" href="structFastSatSolver_1_1AbstractSubject_1_1Private.html#dd13d61a18fbaade63f48711a701df47">00035</a> <span class="keyword">typedef</span> std::list<IObserver *> <a class="code" href="structFastSatSolver_1_1AbstractSubject_1_1Private.html#dd13d61a18fbaade63f48711a701df47">TContainer</a>;
<a name="l00036"></a><a class="code" href="structFastSatSolver_1_1AbstractSubject_1_1Private.html#0d7d83f2b27e4d691661ac8bc466f4c6">00036</a> <a class="code" href="structFastSatSolver_1_1AbstractSubject_1_1Private.html#dd13d61a18fbaade63f48711a701df47">TContainer</a> <a class="code" href="structFastSatSolver_1_1AbstractSubject_1_1Private.html#0d7d83f2b27e4d691661ac8bc466f4c6">container</a>;
<a name="l00037"></a>00037 };
<a name="l00038"></a><a class="code" href="classFastSatSolver_1_1AbstractSubject.html#a865e4c695bceddbeb387cd07b68e8db">00038</a> <a class="code" href="classFastSatSolver_1_1AbstractSubject.html#a865e4c695bceddbeb387cd07b68e8db">AbstractSubject::AbstractSubject</a>():
<a name="l00039"></a>00039 d(new <a class="code" href="structFastSatSolver_1_1AbstractSubject_1_1Private.html">Private</a>)
<a name="l00040"></a>00040 {
<a name="l00041"></a>00041 }
<a name="l00042"></a><a class="code" href="classFastSatSolver_1_1AbstractSubject.html#2c587a73a35eb4ea598134d72c8838b6">00042</a> AbstractSubject::~AbstractSubject() {
<a name="l00043"></a>00043 <span class="comment">// ATTENTION: Observers are not deleted on object destruction</span>
<a name="l00044"></a>00044 <span class="keyword">delete</span> d;
<a name="l00045"></a>00045 }
<a name="l00046"></a><a class="code" href="classFastSatSolver_1_1AbstractSubject.html#05bf56954cced132e03ec548c0557c88">00046</a> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1AbstractSubject.html#05bf56954cced132e03ec548c0557c88" title="Add observer to list of listeners.">AbstractSubject::addObserver</a>(<a class="code" href="classFastSatSolver_1_1IObserver.html" title="Simple observer&#39;s base class.">IObserver</a> *observer) {
<a name="l00047"></a>00047 d-><a class="code" href="structFastSatSolver_1_1AbstractSubject_1_1Private.html#0d7d83f2b27e4d691661ac8bc466f4c6">container</a>.push_back(observer);
<a name="l00048"></a>00048 }
<a name="l00049"></a><a class="code" href="classFastSatSolver_1_1AbstractSubject.html#7ff19734eb024bd6f3e2ad95647b1b27">00049</a> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1AbstractSubject.html#7ff19734eb024bd6f3e2ad95647b1b27" title="Send notification to all observers (listeners).">AbstractSubject::notify</a>() {
<a name="l00050"></a>00050 Private::TContainer::iterator iter;
<a name="l00051"></a>00051 <span class="keywordflow">for</span>(iter=d-><a class="code" href="structFastSatSolver_1_1AbstractSubject_1_1Private.html#0d7d83f2b27e4d691661ac8bc466f4c6">container</a>.begin(); iter!=d-><a class="code" href="structFastSatSolver_1_1AbstractSubject_1_1Private.html#0d7d83f2b27e4d691661ac8bc466f4c6">container</a>.end(); iter++) {
<a name="l00052"></a>00052 <a class="code" href="classFastSatSolver_1_1IObserver.html" title="Simple observer&#39;s base class.">IObserver</a> *observer = *iter;
<a name="l00053"></a>00053 observer-><a class="code" href="classFastSatSolver_1_1IObserver.html#db968cb3b9d5c0f9c62efbc1ea91de8d" title="Event notification, usually called by object implementing ISubject interface.">notify</a>();
<a name="l00054"></a>00054 }
<a name="l00055"></a>00055 }
<a name="l00056"></a>00056
<a name="l00057"></a>00057 <span class="comment">// ////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////</span>
<a name="l00058"></a>00058 <span class="comment">// AbstractProcess implementation</span>
<a name="l00059"></a><a class="code" href="structFastSatSolver_1_1AbstractProcess_1_1Private.html">00059</a> <span class="keyword">struct </span><a class="code" href="structFastSatSolver_1_1AbstractProcess_1_1Private.html">AbstractProcess::Private</a> {
<a name="l00060"></a><a class="code" href="structFastSatSolver_1_1AbstractProcess_1_1Private.html#36f7b6be7108281af77939ceaec42fd6">00060</a> <span class="keywordtype">bool</span> running;
<a name="l00061"></a><a class="code" href="structFastSatSolver_1_1AbstractProcess_1_1Private.html#b4ae7205573977222eadd0795db193e2">00061</a> <span class="keywordtype">int</span> steps;
<a name="l00062"></a>00062 };
<a name="l00063"></a><a class="code" href="classFastSatSolver_1_1AbstractProcess.html#c652d47533d553b2e07ea7367eda6038">00063</a> <a class="code" href="classFastSatSolver_1_1AbstractProcess.html#c652d47533d553b2e07ea7367eda6038">AbstractProcess::AbstractProcess</a>():
<a name="l00064"></a>00064 d(new <a class="code" href="structFastSatSolver_1_1AbstractSubject_1_1Private.html">Private</a>)
<a name="l00065"></a>00065 {
<a name="l00066"></a>00066 d-><a class="code" href="structFastSatSolver_1_1AbstractProcess_1_1Private.html#36f7b6be7108281af77939ceaec42fd6">running</a> = <span class="keyword">false</span>;
<a name="l00067"></a>00067 d-><a class="code" href="structFastSatSolver_1_1AbstractProcess_1_1Private.html#b4ae7205573977222eadd0795db193e2">steps</a> = 0;
<a name="l00068"></a>00068 }
<a name="l00069"></a><a class="code" href="classFastSatSolver_1_1AbstractProcess.html#afd04fedb2739aea43546da557be9f29">00069</a> <a class="code" href="classFastSatSolver_1_1AbstractProcess.html#afd04fedb2739aea43546da557be9f29">AbstractProcess::~AbstractProcess</a>() {
<a name="l00070"></a>00070 <span class="keyword">delete</span> d;
<a name="l00071"></a>00071 }
<a name="l00072"></a><a class="code" href="classFastSatSolver_1_1AbstractProcess.html#60de64d75454385b23995437f1d72669">00072</a> <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...">AbstractProcess::start</a>() {
<a name="l00073"></a>00073 <span class="keywordflow">for</span>(d-><a class="code" href="structFastSatSolver_1_1AbstractProcess_1_1Private.html#36f7b6be7108281af77939ceaec42fd6">running</a>=<span class="keyword">true</span>; d-><a class="code" href="structFastSatSolver_1_1AbstractProcess_1_1Private.html#36f7b6be7108281af77939ceaec42fd6">running</a>; d-><a class="code" href="structFastSatSolver_1_1AbstractProcess_1_1Private.html#b4ae7205573977222eadd0795db193e2">steps</a>++) {
<a name="l00074"></a>00074 this-><a class="code" href="classFastSatSolver_1_1AbstractProcess.html#f40573eed2567df340143a72ddb6cd69" title="Do one step of process.">doStep</a>();
<a name="l00075"></a>00075 this-><a class="code" href="classFastSatSolver_1_1AbstractSubject.html#7ff19734eb024bd6f3e2ad95647b1b27" title="Send notification to all observers (listeners).">notify</a>();
<a name="l00076"></a>00076 }
<a name="l00077"></a>00077 }
<a name="l00078"></a><a class="code" href="classFastSatSolver_1_1AbstractProcess.html#8c528baf37154d347366083f0f816846">00078</a> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1AbstractProcess.html#8c528baf37154d347366083f0f816846" title="Stop currently executed process as soon as possible.">AbstractProcess::stop</a>() {
<a name="l00079"></a>00079 d-><a class="code" href="structFastSatSolver_1_1AbstractProcess_1_1Private.html#36f7b6be7108281af77939ceaec42fd6">running</a> = <span class="keyword">false</span>;
<a name="l00080"></a>00080 }
<a name="l00081"></a><a class="code" href="classFastSatSolver_1_1AbstractProcess.html#d20897c5c8bd47f5d4005989bead0e55">00081</a> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1AbstractProcess.html#d20897c5c8bd47f5d4005989bead0e55" title="Reset process to its initial state.">AbstractProcess::reset</a>() {
<a name="l00082"></a>00082 d-><a class="code" href="structFastSatSolver_1_1AbstractProcess_1_1Private.html#36f7b6be7108281af77939ceaec42fd6">running</a> = <span class="keyword">false</span>;
<a name="l00083"></a>00083 d-><a class="code" href="structFastSatSolver_1_1AbstractProcess_1_1Private.html#b4ae7205573977222eadd0795db193e2">steps</a> = 0;
<a name="l00084"></a>00084 this-><a class="code" href="classFastSatSolver_1_1AbstractProcess.html#a5085af8ee5e5c39b4c20c60231e5c92" title="Initialize process.">initialize</a>();
<a name="l00085"></a>00085 }
<a name="l00086"></a><a class="code" href="classFastSatSolver_1_1AbstractProcess.html#14fa4258dc9ab261c5d4026ae3dfc882">00086</a> <span class="keywordtype">int</span> <a class="code" href="classFastSatSolver_1_1AbstractProcess.html#14fa4258dc9ab261c5d4026ae3dfc882" title="Returns current step number.">AbstractProcess::getStepsCount</a>() {
<a name="l00087"></a>00087 <span class="keywordflow">return</span> d-><a class="code" href="structFastSatSolver_1_1AbstractProcess_1_1Private.html#b4ae7205573977222eadd0795db193e2">steps</a>;
<a name="l00088"></a>00088 }
<a name="l00089"></a>00089
<a name="l00090"></a>00090 <span class="comment">// ////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////</span>
<a name="l00091"></a>00091 <span class="comment">// AbstractProcessWatched implementation</span>
<a name="l00092"></a><a class="code" href="structFastSatSolver_1_1AbstractProcessWatched_1_1Private.html">00092</a> <span class="keyword">struct </span><a class="code" href="structFastSatSolver_1_1AbstractProcessWatched_1_1Private.html">AbstractProcessWatched::Private</a> {
<a name="l00093"></a><a class="code" href="structFastSatSolver_1_1AbstractProcessWatched_1_1Private.html#aa73388acaddd60fe9f118d4e2afefb6">00093</a> <span class="keyword">static</span> <span class="keyword">const</span> <span class="keywordtype">long</span> RATIO = CLOCKS_PER_SEC/1000L;
<a name="l00094"></a><a class="code" href="structFastSatSolver_1_1AbstractProcessWatched_1_1Private.html#42d6a906ce66d6fb751de59ce631abb3">00094</a> clock_t <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="l00095"></a><a class="code" href="structFastSatSolver_1_1AbstractProcessWatched_1_1Private.html#245b65fbced50370bf8a01069e5ee177">00095</a> <span class="keywordtype">long</span> total;
<a name="l00096"></a><a class="code" href="structFastSatSolver_1_1AbstractProcessWatched_1_1Private.html#36f7b6be7108281af77939ceaec42fd6">00096</a> <span class="keywordtype">bool</span> running;
<a name="l00097"></a><a class="code" href="structFastSatSolver_1_1AbstractProcessWatched_1_1Private.html#269516622814e5111575ef7eebd492a7">00097</a> <span class="keywordtype">long</span> currentElapsed() {
<a name="l00098"></a>00098 clock_t diff = clock() - <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="l00099"></a>00099 <span class="keywordflow">return</span> diff/RATIO;
<a name="l00100"></a>00100 }
<a name="l00101"></a>00101 };
<a name="l00102"></a><a class="code" href="classFastSatSolver_1_1AbstractProcessWatched.html#f6310c38aa477863afc576fac02f1110">00102</a> <a class="code" href="classFastSatSolver_1_1AbstractProcessWatched.html#f6310c38aa477863afc576fac02f1110">AbstractProcessWatched::AbstractProcessWatched</a>():
<a name="l00103"></a>00103 d(new <a class="code" href="structFastSatSolver_1_1AbstractSubject_1_1Private.html">Private</a>)
<a name="l00104"></a>00104 {
<a name="l00105"></a>00105 d-><a class="code" href="structFastSatSolver_1_1AbstractProcessWatched_1_1Private.html#245b65fbced50370bf8a01069e5ee177">total</a> = 0;
<a name="l00106"></a>00106 d-><a class="code" href="structFastSatSolver_1_1AbstractProcessWatched_1_1Private.html#36f7b6be7108281af77939ceaec42fd6">running</a> = <span class="keyword">false</span>;
<a name="l00107"></a>00107 }
<a name="l00108"></a><a class="code" href="classFastSatSolver_1_1AbstractProcessWatched.html#05e8cb6c6d5c68d6d7b4b8b122bf529b">00108</a> <a class="code" href="classFastSatSolver_1_1AbstractProcessWatched.html#05e8cb6c6d5c68d6d7b4b8b122bf529b">AbstractProcessWatched::~AbstractProcessWatched</a>() {
<a name="l00109"></a>00109 <span class="keyword">delete</span> d;
<a name="l00110"></a>00110 }
<a name="l00111"></a><a class="code" href="classFastSatSolver_1_1AbstractProcessWatched.html#60de64d75454385b23995437f1d72669">00111</a> <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...">AbstractProcessWatched::start</a>() {
<a name="l00112"></a>00112 d-><a class="code" href="structFastSatSolver_1_1AbstractProcessWatched_1_1Private.html#42d6a906ce66d6fb751de59ce631abb3">start</a> = clock();
<a name="l00113"></a>00113 d-><a class="code" href="structFastSatSolver_1_1AbstractProcessWatched_1_1Private.html#36f7b6be7108281af77939ceaec42fd6">running</a> = <span class="keyword">true</span>;
<a name="l00114"></a>00114 <span class="comment">// Delegate to base</span>
<a name="l00115"></a>00115 <a class="code" href="classFastSatSolver_1_1AbstractProcess.html#60de64d75454385b23995437f1d72669" title="Start process execution. This method returns control after process ends (or after...">AbstractProcess::start</a>();
<a name="l00116"></a>00116 }
<a name="l00117"></a><a class="code" href="classFastSatSolver_1_1AbstractProcessWatched.html#8c528baf37154d347366083f0f816846">00117</a> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1AbstractProcessWatched.html#8c528baf37154d347366083f0f816846" title="Stop currently executed process as soon as possible.">AbstractProcessWatched::stop</a>() {
<a name="l00118"></a>00118 <span class="keywordflow">if</span> (d-><a class="code" href="structFastSatSolver_1_1AbstractProcessWatched_1_1Private.html#36f7b6be7108281af77939ceaec42fd6">running</a>) {
<a name="l00119"></a>00119 d-><a class="code" href="structFastSatSolver_1_1AbstractProcessWatched_1_1Private.html#36f7b6be7108281af77939ceaec42fd6">running</a> = <span class="keyword">false</span>;
<a name="l00120"></a>00120 d-><a class="code" href="structFastSatSolver_1_1AbstractProcessWatched_1_1Private.html#245b65fbced50370bf8a01069e5ee177">total</a> += d-><a class="code" href="structFastSatSolver_1_1AbstractProcessWatched_1_1Private.html#269516622814e5111575ef7eebd492a7">currentElapsed</a>();
<a name="l00121"></a>00121 }
<a name="l00122"></a>00122 <span class="comment">// Delegate to base</span>
<a name="l00123"></a>00123 <a class="code" href="classFastSatSolver_1_1AbstractProcess.html#8c528baf37154d347366083f0f816846" title="Stop currently executed process as soon as possible.">AbstractProcess::stop</a>();
<a name="l00124"></a>00124 }
<a name="l00125"></a><a class="code" href="classFastSatSolver_1_1AbstractProcessWatched.html#d20897c5c8bd47f5d4005989bead0e55">00125</a> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1AbstractProcessWatched.html#d20897c5c8bd47f5d4005989bead0e55" title="Reset process to its initial state.">AbstractProcessWatched::reset</a>() {
<a name="l00126"></a>00126 d-><a class="code" href="structFastSatSolver_1_1AbstractProcessWatched_1_1Private.html#36f7b6be7108281af77939ceaec42fd6">running</a> = <span class="keyword">false</span>;
<a name="l00127"></a>00127 d-><a class="code" href="structFastSatSolver_1_1AbstractProcessWatched_1_1Private.html#245b65fbced50370bf8a01069e5ee177">total</a> = 0;
<a name="l00128"></a>00128 <span class="comment">// Delegate to base</span>
<a name="l00129"></a>00129 <a class="code" href="classFastSatSolver_1_1AbstractProcess.html#d20897c5c8bd47f5d4005989bead0e55" title="Reset process to its initial state.">AbstractProcess::reset</a>();
<a name="l00130"></a>00130 }
<a name="l00131"></a><a class="code" href="classFastSatSolver_1_1AbstractProcessWatched.html#57e2ab43bf94f9adc686e788f8771681">00131</a> <span class="keywordtype">long</span> <a class="code" href="classFastSatSolver_1_1AbstractProcessWatched.html#57e2ab43bf94f9adc686e788f8771681" title="Returns time elapsed by activity.">AbstractProcessWatched::getTimeElapsed</a>() {
<a name="l00132"></a>00132 <span class="comment">/*if (!d->running) {</span>
<a name="l00133"></a>00133 <span class="comment"> std::cerr << "AbstractProcessWatched::getTimeElapsed()" << std::endl;</span>
<a name="l00134"></a>00134 <span class="comment"> std::cerr << " running: false" << std::endl;</span>
<a name="l00135"></a>00135 <span class="comment"> std::cerr << " total: " << d->total << std::endl;</span>
<a name="l00136"></a>00136 <span class="comment"> std::cerr << " current: " << d->currentElapsed() << std::endl;</span>
<a name="l00137"></a>00137 <span class="comment"> }*/</span>
<a name="l00138"></a>00138 <span class="keywordtype">long</span> total = d-><a class="code" href="structFastSatSolver_1_1AbstractProcessWatched_1_1Private.html#245b65fbced50370bf8a01069e5ee177">total</a>;
<a name="l00139"></a>00139 <span class="keywordflow">if</span> (d-><a class="code" href="structFastSatSolver_1_1AbstractProcessWatched_1_1Private.html#36f7b6be7108281af77939ceaec42fd6">running</a>)
<a name="l00140"></a>00140 total+= d-><a class="code" href="structFastSatSolver_1_1AbstractProcessWatched_1_1Private.html#269516622814e5111575ef7eebd492a7">currentElapsed</a>();
<a name="l00141"></a>00141 <span class="keywordflow">return</span> total;
<a name="l00142"></a>00142 }
<a name="l00143"></a>00143
<a name="l00144"></a>00144 <span class="comment">// ////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////</span>
<a name="l00145"></a>00145 <span class="comment">// AbstractSatSolver implementation</span>
<a name="l00146"></a><a class="code" href="classFastSatSolver_1_1AbstractSatSolver.html#6716df2cfc865894f1d26905c27bdc19">00146</a> <a class="code" href="classFastSatSolver_1_1AbstractSatSolver.html#6716df2cfc865894f1d26905c27bdc19">AbstractSatSolver::AbstractSatSolver</a>() { }
<a name="l00147"></a><a class="code" href="classFastSatSolver_1_1AbstractSatSolver.html#fae336fb16e0c147d36ad94b8bff70a5">00147</a> <a class="code" href="classFastSatSolver_1_1AbstractSatSolver.html#fae336fb16e0c147d36ad94b8bff70a5">AbstractSatSolver::~AbstractSatSolver</a>() { }
<a name="l00148"></a>00148
<a name="l00149"></a>00149
<a name="l00150"></a>00150 <span class="comment">// ////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////</span>
<a name="l00151"></a>00151 <span class="comment">// SatItemVector implementation</span>
<a name="l00152"></a><a class="code" href="structFastSatSolver_1_1SatItemVector_1_1Private.html">00152</a> <span class="keyword">struct </span><a class="code" href="structFastSatSolver_1_1SatItemVector_1_1Private.html">SatItemVector::Private</a> {
<a name="l00153"></a><a class="code" href="structFastSatSolver_1_1SatItemVector_1_1Private.html#f6975adb7395e1f3a053625848be8631">00153</a> <span class="keyword">typedef</span> std::vector<ISatItem *> TVector;
<a name="l00154"></a><a class="code" href="structFastSatSolver_1_1SatItemVector_1_1Private.html#81df3021c00f1458769ab673cc47fefa">00154</a> TVector vect;
<a name="l00155"></a>00155
<a name="l00156"></a><a class="code" href="structFastSatSolver_1_1SatItemVector_1_1Private.html#717e3fa3a090a3e269d25b4ea443b036">00156</a> <a class="code" href="structFastSatSolver_1_1SatItemVector_1_1Private.html">Private</a>(<span class="keywordtype">unsigned</span> size=0): vect(size) { }
<a name="l00157"></a>00157 };
<a name="l00158"></a><a class="code" href="classFastSatSolver_1_1SatItemVector.html#fab085d58e8b05bfcf4065c4d6af9c67">00158</a> <a class="code" href="classFastSatSolver_1_1SatItemVector.html#fab085d58e8b05bfcf4065c4d6af9c67">SatItemVector::SatItemVector</a>():
<a name="l00159"></a>00159 d(new <a class="code" href="structFastSatSolver_1_1SatItemVector_1_1Private.html">Private</a>)
<a name="l00160"></a>00160 {
<a name="l00161"></a>00161 }
<a name="l00162"></a><a class="code" href="classFastSatSolver_1_1SatItemVector.html#f93ae0bf30899a0e011bc2f373938de7">00162</a> <a class="code" href="classFastSatSolver_1_1SatItemVector.html#fab085d58e8b05bfcf4065c4d6af9c67">SatItemVector::SatItemVector</a>(<span class="keyword">const</span> <a class="code" href="classFastSatSolver_1_1SatItemVector.html" title="Linear storage container for ISatItem objects.">SatItemVector</a> &other):
<a name="l00163"></a>00163 d(new <a class="code" href="structFastSatSolver_1_1SatItemVector_1_1Private.html">Private</a>(other.<a class="code" href="classFastSatSolver_1_1SatItemVector.html#f59b115e86eaeac1f15673766852e428" title="Returns count of item managed by container.">getLength</a>()))
<a name="l00164"></a>00164 {
<a name="l00165"></a>00165 <span class="keyword">const</span> <span class="keywordtype">int</span> length= other.<a class="code" href="classFastSatSolver_1_1SatItemVector.html#f59b115e86eaeac1f15673766852e428" title="Returns count of item managed by container.">getLength</a>();
<a name="l00166"></a>00166 <span class="keywordflow">for</span>(<span class="keywordtype">int</span> i=0; i<length; i++)
<a name="l00167"></a>00167 d-><a class="code" href="structFastSatSolver_1_1SatItemVector_1_1Private.html#81df3021c00f1458769ab673cc47fefa">vect</a>[i] = other.<a class="code" href="classFastSatSolver_1_1SatItemVector.html#e9908ff1674579e6a5ed8729dace445d" title="Direct access container item.">getItem</a>(i)-><a class="code" href="classFastSatSolver_1_1ISatItem.html#ce35793be43d099862210ca953c725df" title="Returns clone of object&#39;s instance.">clone</a>();
<a name="l00168"></a>00168 }
<a name="l00169"></a><a class="code" href="classFastSatSolver_1_1SatItemVector.html#6f497951e23c4434580791ec5096a271">00169</a> <a class="code" href="classFastSatSolver_1_1SatItemVector.html#6f497951e23c4434580791ec5096a271">SatItemVector::~SatItemVector</a>() {
<a name="l00170"></a>00170 this-><a class="code" href="classFastSatSolver_1_1SatItemVector.html#c8bb3912a3ce86b15842e79d0b421204" title="Remove all item from container and free from memory.">clear</a>();
<a name="l00171"></a>00171 <span class="keyword">delete</span> d;
<a name="l00172"></a>00172 }
<a name="l00173"></a><a class="code" href="classFastSatSolver_1_1SatItemVector.html#f59b115e86eaeac1f15673766852e428">00173</a> <span class="keywordtype">int</span> <a class="code" href="classFastSatSolver_1_1SatItemVector.html#f59b115e86eaeac1f15673766852e428" title="Returns count of item managed by container.">SatItemVector::getLength</a>()<span class="keyword"> const </span>{
<a name="l00174"></a>00174 <span class="keywordflow">return</span> d-><a class="code" href="structFastSatSolver_1_1SatItemVector_1_1Private.html#81df3021c00f1458769ab673cc47fefa">vect</a>.size();
<a name="l00175"></a>00175 }
<a name="l00176"></a><a class="code" href="classFastSatSolver_1_1SatItemVector.html#e9908ff1674579e6a5ed8729dace445d">00176</a> <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.">SatItemVector::getItem</a>(<span class="keywordtype">int</span> index)<span class="keyword"> const </span>{
<a name="l00177"></a>00177 <span class="keywordflow">return</span> d-><a class="code" href="structFastSatSolver_1_1SatItemVector_1_1Private.html#81df3021c00f1458769ab673cc47fefa">vect</a>[index];
<a name="l00178"></a>00178 }
<a name="l00179"></a><a class="code" href="classFastSatSolver_1_1SatItemVector.html#e50e61bb65bb3328f6afbd8e005cb96f">00179</a> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1SatItemVector.html#e50e61bb65bb3328f6afbd8e005cb96f" title="Add item to container.">SatItemVector::addItem</a>(<a class="code" href="classFastSatSolver_1_1ISatItem.html" title="Abstraction of solution candidate.">ISatItem</a> *item) {
<a name="l00180"></a>00180 d-><a class="code" href="structFastSatSolver_1_1SatItemVector_1_1Private.html#81df3021c00f1458769ab673cc47fefa">vect</a>.push_back(item);
<a name="l00181"></a>00181 }
<a name="l00182"></a><a class="code" href="classFastSatSolver_1_1SatItemVector.html#3c0c3fdc04f467c4dcb62eabb407acc2">00182</a> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1SatItemVector.html#3c0c3fdc04f467c4dcb62eabb407acc2" title="Human readable container dump.">SatItemVector::writeOut</a>(<a class="code" href="classFastSatSolver_1_1SatProblem.html" title="SAT Problem module&#39;s facade.">SatProblem</a> *problem, std::ostream &stream)<span class="keyword"> const </span>{
<a name="l00183"></a>00183 <span class="keyword">const</span> <span class="keywordtype">int</span> nForms= this-><a class="code" href="classFastSatSolver_1_1SatItemVector.html#f59b115e86eaeac1f15673766852e428" title="Returns count of item managed by container.">getLength</a>();
<a name="l00184"></a>00184 <span class="keyword">const</span> <span class="keywordtype">int</span> nVars= problem-><a class="code" href="classFastSatSolver_1_1SatProblem.html#92e7e3731c3c44467cadeb9038dd4cb9" title="Returns total count of variables managed by SatProblem.">getVarsCount</a>();
<a name="l00185"></a>00185 <span class="keywordflow">for</span>(<span class="keywordtype">int</span> f=0; f<nForms; f++) {
<a name="l00186"></a>00186 stream << std::setw(5) << f+1 << <span class="stringliteral">". "</span>;
<a name="l00187"></a>00187 <a class="code" href="classFastSatSolver_1_1ISatItem.html" title="Abstraction of solution candidate.">ISatItem</a> *item= <a class="code" href="classFastSatSolver_1_1SatItemVector.html#e9908ff1674579e6a5ed8729dace445d" title="Direct access container item.">getItem</a>(f);
<a name="l00188"></a>00188 <span class="keywordflow">for</span>(<span class="keywordtype">int</span> v=0; v<nVars; v++) {
<a name="l00189"></a>00189 stream << problem-><a class="code" href="classFastSatSolver_1_1SatProblem.html#139a3f2e63c60e612c649a57ba1ce9dd" title="Returns name of variable with desired index.">getVarName</a>(v) << <span class="stringliteral">"="</span> << item-><a class="code" href="classFastSatSolver_1_1ISatItem.html#ef9eadbc8fd10e01f1b37f85c6e08a67" title="Returns value of desired bit (resp. variable).">getBit</a>(v);
<a name="l00190"></a>00190 <span class="keywordflow">if</span> (v==nVars-1)
<a name="l00191"></a>00191 stream << std::endl;
<a name="l00192"></a>00192 <span class="keywordflow">else</span>
<a name="l00193"></a>00193 stream << <span class="stringliteral">", "</span>;
<a name="l00194"></a>00194 }
<a name="l00195"></a>00195 }
<a name="l00196"></a>00196 }
<a name="l00197"></a><a class="code" href="classFastSatSolver_1_1SatItemVector.html#c8bb3912a3ce86b15842e79d0b421204">00197</a> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1SatItemVector.html#c8bb3912a3ce86b15842e79d0b421204" title="Remove all item from container and free from memory.">SatItemVector::clear</a>() {
<a name="l00198"></a>00198 Private::TVector::iterator iter;
<a name="l00199"></a>00199 <span class="keywordflow">for</span>(iter=d-><a class="code" href="structFastSatSolver_1_1SatItemVector_1_1Private.html#81df3021c00f1458769ab673cc47fefa">vect</a>.begin(); iter!=d-><a class="code" href="structFastSatSolver_1_1SatItemVector_1_1Private.html#81df3021c00f1458769ab673cc47fefa">vect</a>.end(); iter++)
<a name="l00200"></a>00200 <span class="keyword">delete</span> *iter;
<a name="l00201"></a>00201 d-><a class="code" href="structFastSatSolver_1_1SatItemVector_1_1Private.html#81df3021c00f1458769ab673cc47fefa">vect</a>.clear();
<a name="l00202"></a>00202 }
<a name="l00203"></a>00203
<a name="l00204"></a>00204
<a name="l00205"></a>00205 <span class="comment">// ////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////</span>
<a name="l00206"></a>00206 <span class="comment">// SatItemSet implementation</span>
<a name="l00207"></a><a class="code" href="structFastSatSolver_1_1SatItemSet_1_1Private.html">00207</a> <span class="keyword">struct </span><a class="code" href="structFastSatSolver_1_1SatItemSet_1_1Private.html">SatItemSet::Private</a> {
<a name="l00208"></a><a class="code" href="classFastSatSolver_1_1SatItemSet_1_1Private_1_1SatItemHashDecorator.html">00208</a> <span class="keyword">class </span><a class="code" href="classFastSatSolver_1_1SatItemSet_1_1Private_1_1SatItemHashDecorator.html">SatItemHashDecorator</a>: <span class="keyword">public</span> <a class="code" href="classFastSatSolver_1_1ISatItem.html" title="Abstraction of solution candidate.">ISatItem</a> {
<a name="l00209"></a>00209 <span class="keyword">public</span>:
<a name="l00210"></a><a class="code" href="classFastSatSolver_1_1SatItemSet_1_1Private_1_1SatItemHashDecorator.html#b44e1c27925e2869bb30f7df0d385b20">00210</a> <a class="code" href="classFastSatSolver_1_1SatItemSet_1_1Private_1_1SatItemHashDecorator.html">SatItemHashDecorator</a>(<a class="code" href="classFastSatSolver_1_1ISatItem.html" title="Abstraction of solution candidate.">ISatItem</a> *item):
<a name="l00211"></a>00211 item_(item)
<a name="l00212"></a>00212 {
<a name="l00213"></a>00213 }
<a name="l00214"></a><a class="code" href="classFastSatSolver_1_1SatItemSet_1_1Private_1_1SatItemHashDecorator.html#b953e90edb69534eb052f9064f6b40e9">00214</a> <span class="keywordtype">void</span> dispose() {
<a name="l00215"></a>00215 <span class="keyword">delete</span> item_;
<a name="l00216"></a>00216 }
<a name="l00217"></a><a class="code" href="classFastSatSolver_1_1SatItemSet_1_1Private_1_1SatItemHashDecorator.html#cbf7308de3263e4a074a39504da4d582">00217</a> <span class="keyword">virtual</span> <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="l00218"></a>00218 <span class="keywordflow">return</span> item_->getLength();
<a name="l00219"></a>00219 }
<a name="l00220"></a><a class="code" href="classFastSatSolver_1_1SatItemSet_1_1Private_1_1SatItemHashDecorator.html#216d73f4179640329f596aead43c66ea">00220</a> <span class="keyword">virtual</span> <span class="keywordtype">bool</span> getBit(<span class="keywordtype">int</span> index)<span class="keyword"> const </span>{
<a name="l00221"></a>00221 <span class="keywordflow">return</span> item_->getBit(index);
<a name="l00222"></a>00222 }
<a name="l00223"></a><a class="code" href="classFastSatSolver_1_1SatItemSet_1_1Private_1_1SatItemHashDecorator.html#55978bf1ff3b31528829bb1f512dbf87">00223</a> <span class="keyword">virtual</span> <a class="code" href="classFastSatSolver_1_1ISatItem.html" title="Abstraction of solution candidate.">ISatItem</a>* clone()<span class="keyword"> const </span>{
<a name="l00224"></a>00224 <span class="keywordflow">return</span> item_->clone();
<a name="l00225"></a>00225 }
<a name="l00226"></a><a class="code" href="classFastSatSolver_1_1SatItemSet_1_1Private_1_1SatItemHashDecorator.html#d9490b2f3ebbe06c341ec56004e29751">00226</a> <span class="keywordtype">bool</span> operator< (<span class="keyword">const</span> <a class="code" href="classFastSatSolver_1_1SatItemSet_1_1Private_1_1SatItemHashDecorator.html">SatItemHashDecorator</a> &other)<span class="keyword"> const </span>{
<a name="l00227"></a>00227 <span class="keywordflow">for</span>(<span class="keywordtype">int</span> i=0; i<<a class="code" href="classFastSatSolver_1_1SatItemVector.html#f59b115e86eaeac1f15673766852e428" title="Returns count of item managed by container.">getLength</a>(); i++) {
<a name="l00228"></a>00228 <span class="keywordflow">if</span> (!getBit(i) && other.<a class="code" href="classFastSatSolver_1_1SatItemSet_1_1Private_1_1SatItemHashDecorator.html#216d73f4179640329f596aead43c66ea" title="Returns value of desired bit (resp. variable).">getBit</a>(i))
<a name="l00229"></a>00229 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00230"></a>00230 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (getBit(i) && !other.<a class="code" href="classFastSatSolver_1_1SatItemSet_1_1Private_1_1SatItemHashDecorator.html#216d73f4179640329f596aead43c66ea" title="Returns value of desired bit (resp. variable).">getBit</a>(i))
<a name="l00231"></a>00231 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00232"></a>00232 }
<a name="l00233"></a>00233 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00234"></a>00234 }
<a name="l00235"></a>00235 <span class="keyword">private</span>:
<a name="l00236"></a>00236 <a class="code" href="classFastSatSolver_1_1ISatItem.html" title="Abstraction of solution candidate.">ISatItem</a> *item_;
<a name="l00237"></a>00237 };
<a name="l00238"></a><a class="code" href="structFastSatSolver_1_1SatItemSet_1_1Private.html#7fab1a75ed2698002704ae5e7ba16310">00238</a> <span class="keyword">typedef</span> std::set<SatItemHashDecorator> TSet;
<a name="l00239"></a><a class="code" href="structFastSatSolver_1_1SatItemSet_1_1Private.html#28859a3f21ecd1d11c95e2d22898d5b0">00239</a> TSet <span class="keyword">set</span>;
<a name="l00240"></a>00240
<a name="l00241"></a><a class="code" href="structFastSatSolver_1_1SatItemSet_1_1Private.html#e50e61bb65bb3328f6afbd8e005cb96f">00241</a> <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="l00242"></a>00242 <a class="code" href="classFastSatSolver_1_1SatItemSet_1_1Private_1_1SatItemHashDecorator.html">SatItemHashDecorator</a> hashableItem(item);
<a name="l00243"></a>00243 <span class="keywordflow">if</span> (<span class="keyword">set</span>.end()==<span class="keyword">set</span>.find(hashableItem))
<a name="l00244"></a>00244 <span class="keyword">set</span>.insert(hashableItem);
<a name="l00245"></a>00245 <span class="keywordflow">else</span>
<a name="l00246"></a>00246 hashableItem.<a class="code" href="classFastSatSolver_1_1SatItemSet_1_1Private_1_1SatItemHashDecorator.html#b953e90edb69534eb052f9064f6b40e9">dispose</a>();
<a name="l00247"></a>00247 }
<a name="l00248"></a>00248 };
<a name="l00249"></a><a class="code" href="classFastSatSolver_1_1SatItemSet.html#833d48be9570b6fe7286c0649058d7c1">00249</a> <a class="code" href="classFastSatSolver_1_1SatItemSet.html#833d48be9570b6fe7286c0649058d7c1">SatItemSet::SatItemSet</a>():
<a name="l00250"></a>00250 d(new <a class="code" href="structFastSatSolver_1_1SatItemSet_1_1Private.html">Private</a>)
<a name="l00251"></a>00251 {
<a name="l00252"></a>00252 }
<a name="l00253"></a><a class="code" href="classFastSatSolver_1_1SatItemSet.html#a374f535d376a6adb5744cac83f0c52a">00253</a> <a class="code" href="classFastSatSolver_1_1SatItemSet.html#a374f535d376a6adb5744cac83f0c52a">SatItemSet::~SatItemSet</a>() {
<a name="l00254"></a>00254 this-><a class="code" href="classFastSatSolver_1_1SatItemSet.html#c8bb3912a3ce86b15842e79d0b421204" title="Remove all item from container and free from memory.">clear</a>();
<a name="l00255"></a>00255 <span class="keyword">delete</span> d;
<a name="l00256"></a>00256 }
<a name="l00257"></a><a class="code" href="classFastSatSolver_1_1SatItemSet.html#ab0d4bbd0884d04dbe281cc2b9d21206">00257</a> <span class="keywordtype">int</span> <a class="code" href="classFastSatSolver_1_1SatItemSet.html#ab0d4bbd0884d04dbe281cc2b9d21206" title="Returns count of item managed by container.">SatItemSet::getLength</a>() {
<a name="l00258"></a>00258 <span class="keywordflow">return</span> d-><a class="code" href="structFastSatSolver_1_1SatItemSet_1_1Private.html#28859a3f21ecd1d11c95e2d22898d5b0">set</a>.size();
<a name="l00259"></a>00259 }
<a name="l00260"></a><a class="code" href="classFastSatSolver_1_1SatItemSet.html#e50e61bb65bb3328f6afbd8e005cb96f">00260</a> <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.">SatItemSet::addItem</a>(<a class="code" href="classFastSatSolver_1_1ISatItem.html" title="Abstraction of solution candidate.">ISatItem</a> *item) {
<a name="l00261"></a>00261 d-><a class="code" href="structFastSatSolver_1_1SatItemSet_1_1Private.html#e50e61bb65bb3328f6afbd8e005cb96f">addItem</a>(item);
<a name="l00262"></a>00262 }
<a name="l00263"></a><a class="code" href="classFastSatSolver_1_1SatItemSet.html#1ec6a07165be87a359b04ee833c0a283">00263</a> <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.">SatItemSet::createVector</a>() {
<a name="l00264"></a>00264 <a class="code" href="classFastSatSolver_1_1SatItemVector.html" title="Linear storage container for ISatItem objects.">SatItemVector</a> *vect= <span class="keyword">new</span> <a class="code" href="classFastSatSolver_1_1SatItemVector.html" title="Linear storage container for ISatItem objects.">SatItemVector</a>;
<a name="l00265"></a>00265 Private::TSet::iterator iter;
<a name="l00266"></a>00266 <span class="keywordflow">for</span>(iter=d-><a class="code" href="structFastSatSolver_1_1SatItemSet_1_1Private.html#28859a3f21ecd1d11c95e2d22898d5b0">set</a>.begin(); iter!=d-><a class="code" href="structFastSatSolver_1_1SatItemSet_1_1Private.html#28859a3f21ecd1d11c95e2d22898d5b0">set</a>.end(); iter++) {
<a name="l00267"></a>00267 <span class="keyword">const</span> <a class="code" href="classFastSatSolver_1_1SatItemSet_1_1Private_1_1SatItemHashDecorator.html">Private::SatItemHashDecorator</a> &satItemHasable= *iter;
<a name="l00268"></a>00268 <a class="code" href="classFastSatSolver_1_1ISatItem.html" title="Abstraction of solution candidate.">ISatItem</a> *itemClone= satItemHasable.<a class="code" href="classFastSatSolver_1_1SatItemSet_1_1Private_1_1SatItemHashDecorator.html#55978bf1ff3b31528829bb1f512dbf87" title="Returns clone of object&#39;s instance.">clone</a>();
<a name="l00269"></a>00269 vect-><a class="code" href="classFastSatSolver_1_1SatItemVector.html#e50e61bb65bb3328f6afbd8e005cb96f" title="Add item to container.">addItem</a>(itemClone);
<a name="l00270"></a>00270 }
<a name="l00271"></a>00271 <span class="keywordflow">return</span> vect;
<a name="l00272"></a>00272 }
<a name="l00273"></a><a class="code" href="classFastSatSolver_1_1SatItemSet.html#c8bb3912a3ce86b15842e79d0b421204">00273</a> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1SatItemSet.html#c8bb3912a3ce86b15842e79d0b421204" title="Remove all item from container and free from memory.">SatItemSet::clear</a>() {
<a name="l00274"></a>00274 Private::TSet::iterator iter;
<a name="l00275"></a>00275 <span class="keywordflow">for</span>(iter=d-><a class="code" href="structFastSatSolver_1_1SatItemSet_1_1Private.html#28859a3f21ecd1d11c95e2d22898d5b0">set</a>.begin(); iter!=d-><a class="code" href="structFastSatSolver_1_1SatItemSet_1_1Private.html#28859a3f21ecd1d11c95e2d22898d5b0">set</a>.end(); iter++) {
<a name="l00276"></a>00276 <a class="code" href="classFastSatSolver_1_1SatItemSet_1_1Private_1_1SatItemHashDecorator.html">Private::SatItemHashDecorator</a> &i=
<a name="l00277"></a>00277 <span class="keyword">const_cast<</span><a class="code" href="classFastSatSolver_1_1SatItemSet_1_1Private_1_1SatItemHashDecorator.html">Private::SatItemHashDecorator</a> &<span class="keyword">></span>(*iter);
<a name="l00278"></a>00278 i.<a class="code" href="classFastSatSolver_1_1SatItemSet_1_1Private_1_1SatItemHashDecorator.html#b953e90edb69534eb052f9064f6b40e9">dispose</a>();
<a name="l00279"></a>00279 }
<a name="l00280"></a>00280 d-><a class="code" href="structFastSatSolver_1_1SatItemSet_1_1Private.html#28859a3f21ecd1d11c95e2d22898d5b0">set</a>.clear();
<a name="l00281"></a>00281 }
<a name="l00282"></a>00282
<a name="l00283"></a>00283 } <span class="comment">// namespace FastSatSolver</span>
<a name="l00284"></a>00284
</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>
Zpět na hlavní stránku
SatSolver_8cpp-source.html [Stáhnout]