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: SatProblem.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>SatProblem.cpp</h1><a href="SatProblem_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 <stdio.h></span>
<a name="l00021"></a>00021 <span class="preprocessor">#include <assert.h></span>
<a name="l00022"></a>00022 <span class="preprocessor">#include <iostream></span>
<a name="l00023"></a>00023 <span class="preprocessor">#include <string></span>
<a name="l00024"></a>00024 <span class="preprocessor">#include <vector></span>
<a name="l00025"></a>00025 <span class="preprocessor">#include <list></span>
<a name="l00026"></a>00026 <span class="preprocessor">#include <map></span>
<a name="l00027"></a>00027 <span class="preprocessor">#include "<a class="code" href="fssIO_8h.html" title="I/O module.">fssIO.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 <span class="preprocessor">#include "<a class="code" href="Scanner_8h.html" title="Extensible lexical scanner used for reading SAT Problem specification.">Scanner.h</a>"</span>
<a name="l00030"></a>00030 <span class="preprocessor">#include "<a class="code" href="Formula_8h.html" title="Propositional formula representation.">Formula.h</a>"</span>
<a name="l00031"></a>00031 <span class="preprocessor">#include "<a class="code" href="SatProblem_8h.html" title="SAT Problem representation.">SatProblem.h</a>"</span>
<a name="l00032"></a>00032
<a name="l00033"></a>00033 <span class="keyword">using</span> std::string;
<a name="l00034"></a>00034
<a name="l00035"></a>00035 <span class="keyword">namespace </span>FastSatSolver {
<a name="l00036"></a>00036
<a name="l00037"></a>00037 <span class="comment">// ////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////</span>
<a name="l00038"></a>00038 <span class="comment">// SatProblem implementation</span>
<a name="l00039"></a><a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html">00039</a> <span class="keyword">struct </span><a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html">SatProblem::Private</a> {
<a name="l00040"></a><a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#5e7656006c54c5a38ba22f9fd0bcb2f1">00040</a> <span class="keywordtype">bool</span> <a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#5e7656006c54c5a38ba22f9fd0bcb2f1">hasError</a>;
<a name="l00041"></a><a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#aa540a1fb84ff7b45694df3ef8b00486">00041</a> <a class="code" href="classFastSatSolver_1_1VariableContainer.html" title="Container for variables names.">VariableContainer</a> <a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#aa540a1fb84ff7b45694df3ef8b00486">vc</a>;
<a name="l00042"></a><a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#7e4ae4fbcc08a74a001974dda465b041">00042</a> <a class="code" href="classFastSatSolver_1_1FormulaContainer.html" title="Container for evaluable formulas.">FormulaContainer</a> <a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#7e4ae4fbcc08a74a001974dda465b041">fc</a>;
<a name="l00043"></a><a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#c81f9269c8d57eed4d5b56f054fc84de">00043</a> std::string <a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#c81f9269c8d57eed4d5b56f054fc84de">fileName</a>;
<a name="l00044"></a>00044
<a name="l00045"></a>00045 <span class="keywordtype">void</span> <a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#df436c08b00c0f824d199d75730f9989">parseFile</a>(FILE *);
<a name="l00046"></a>00046 <span class="keywordtype">void</span> <a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#1f253aaff031757c99ad290a139d4572">parserLoop</a>(<a class="code" href="classFastSatSolver_1_1IScanner.html" title="Extensible lexical scanner&#39;s interface.">IScanner</a> *);
<a name="l00047"></a>00047 <span class="keywordtype">void</span> <a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#4a9777d181b01d3df14636fee61ae5b9">printError</a>(<a class="code" href="structFastSatSolver_1_1Token.html" title="Syntax unit representation - also called token.">Token</a>);
<a name="l00048"></a>00048 };
<a name="l00049"></a><a class="code" href="classFastSatSolver_1_1SatProblem.html#5d3fd105680101a0b884e521e48c3706">00049</a> <a class="code" href="classFastSatSolver_1_1SatProblem.html#5d3fd105680101a0b884e521e48c3706">SatProblem::SatProblem</a>():
<a name="l00050"></a>00050 d(new <a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html">Private</a>)
<a name="l00051"></a>00051 {
<a name="l00052"></a>00052 d-><a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#5e7656006c54c5a38ba22f9fd0bcb2f1">hasError</a> = <span class="keyword">false</span>;
<a name="l00053"></a>00053 }
<a name="l00054"></a><a class="code" href="classFastSatSolver_1_1SatProblem.html#2a8df988c3c0c2cf1391d7de1497020d">00054</a> SatProblem::~SatProblem() {
<a name="l00055"></a>00055 <span class="keyword">delete</span> d;
<a name="l00056"></a>00056 }
<a name="l00057"></a><a class="code" href="classFastSatSolver_1_1SatProblem.html#e4a205ad3acbe7e655676a4f31377456">00057</a> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1SatProblem.html#e4a205ad3acbe7e655676a4f31377456" title="Load SAT Problem specification from file.">SatProblem::loadFromFile</a> (std::string fileName ) {
<a name="l00058"></a>00058 d-><a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#c81f9269c8d57eed4d5b56f054fc84de">fileName</a> = fileName;
<a name="l00059"></a>00059
<a name="l00060"></a>00060 <span class="comment">// OpenedFile RAII</span>
<a name="l00061"></a>00061 <span class="keyword">class </span>OpenedFileRAII {
<a name="l00062"></a>00062 <span class="keyword">public</span>:
<a name="l00063"></a>00063 OpenedFileRAII(<span class="keywordtype">string</span> fileName) {
<a name="l00064"></a>00064 fd_ = fopen(fileName.c_str(), <span class="stringliteral">"r"</span>);
<a name="l00065"></a>00065 <span class="keywordflow">if</span> (0== fd_) {
<a name="l00066"></a>00066 <span class="keywordtype">string</span> error(<span class="stringliteral">"Could not open file: "</span>);
<a name="l00067"></a>00067 <span class="keywordflow">throw</span> <a class="code" href="classFastSatSolver_1_1GenericException.html" title="Common-usage exception containing error message inside.">GenericException</a>(error + fileName);
<a name="l00068"></a>00068 }
<a name="l00069"></a>00069 }
<a name="l00070"></a>00070 ~OpenedFileRAII() { fclose(fd_); }
<a name="l00071"></a>00071 FILE* getFd() { <span class="keywordflow">return</span> fd_; }
<a name="l00072"></a>00072 <span class="keyword">private</span>:
<a name="l00073"></a>00073 FILE* fd_;
<a name="l00074"></a>00074 } openedFile(fileName);
<a name="l00075"></a>00075 d-><a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#df436c08b00c0f824d199d75730f9989">parseFile</a>(openedFile.getFd());
<a name="l00076"></a>00076 }
<a name="l00077"></a>00077
<a name="l00078"></a>00078
<a name="l00081"></a><a class="code" href="classFastSatSolver_1_1SatProblem.html#60bbd7b131b3eb0838488828f574fe40">00081</a> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1SatProblem.html#60bbd7b131b3eb0838488828f574fe40" title="Load SAT Problem specification from standard input.">SatProblem::loadFromInput</a> ( ) {
<a name="l00082"></a>00082 d-><a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#c81f9269c8d57eed4d5b56f054fc84de">fileName</a> = <span class="stringliteral">"-"</span>;
<a name="l00083"></a>00083 d-><a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#df436c08b00c0f824d199d75730f9989">parseFile</a>(stdin);
<a name="l00084"></a>00084 }
<a name="l00085"></a>00085
<a name="l00086"></a>00086
<a name="l00087"></a>00087 <span class="comment">// @private</span>
<a name="l00088"></a><a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#df436c08b00c0f824d199d75730f9989">00088</a> <span class="keywordtype">void</span> <a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#df436c08b00c0f824d199d75730f9989">SatProblem::Private::parseFile</a>(FILE *fd) {
<a name="l00089"></a>00089 <span class="comment">// RawScanner RAII</span>
<a name="l00090"></a>00090 <span class="keyword">class </span>RawScanRAII {
<a name="l00091"></a>00091 <span class="keyword">public</span>:
<a name="l00092"></a>00092 RawScanRAII(FILE *fd) { ptr_ = <span class="keyword">new</span> <a class="code" href="classFastSatSolver_1_1RawScanner.html" title="Low-level scanner parses lexical units from opened file.">RawScanner</a>(fd); }
<a name="l00093"></a>00093 ~RawScanRAII() { <span class="keyword">delete</span> ptr_; }
<a name="l00094"></a>00094 <a class="code" href="classFastSatSolver_1_1RawScanner.html" title="Low-level scanner parses lexical units from opened file.">RawScanner</a>* instance() { <span class="keywordflow">return</span> ptr_; }
<a name="l00095"></a>00095 <span class="keyword">private</span>:
<a name="l00096"></a>00096 <a class="code" href="classFastSatSolver_1_1RawScanner.html" title="Low-level scanner parses lexical units from opened file.">RawScanner</a> *ptr_;
<a name="l00097"></a>00097 } rawScan(fd);
<a name="l00098"></a>00098
<a name="l00099"></a>00099 <span class="comment">// ScannerStringHandler RAII</span>
<a name="l00100"></a>00100 <span class="keyword">class </span>StringScanRAII {
<a name="l00101"></a>00101 <span class="keyword">public</span>:
<a name="l00102"></a>00102 StringScanRAII(<a class="code" href="classFastSatSolver_1_1IScanner.html" title="Extensible lexical scanner&#39;s interface.">IScanner</a> *scan, <a class="code" href="classFastSatSolver_1_1VariableContainer.html" title="Container for variables names.">VariableContainer</a> *<a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#aa540a1fb84ff7b45694df3ef8b00486">vc</a>) {
<a name="l00103"></a>00103 ptr_ = <span class="keyword">new</span> <a class="code" href="classFastSatSolver_1_1ScannerStringHandler.html" title="Part of parser handling keywords and variable names.">ScannerStringHandler</a>(scan, vc);
<a name="l00104"></a>00104 }
<a name="l00105"></a>00105 ~StringScanRAII() { <span class="keyword">delete</span> ptr_; }
<a name="l00106"></a>00106 <a class="code" href="classFastSatSolver_1_1ScannerStringHandler.html" title="Part of parser handling keywords and variable names.">ScannerStringHandler</a>* instance() { <span class="keywordflow">return</span> ptr_; }
<a name="l00107"></a>00107 <span class="keyword">private</span>:
<a name="l00108"></a>00108 <a class="code" href="classFastSatSolver_1_1ScannerStringHandler.html" title="Part of parser handling keywords and variable names.">ScannerStringHandler</a> *ptr_;
<a name="l00109"></a>00109 } stringScan(rawScan.instance(), &<a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#aa540a1fb84ff7b45694df3ef8b00486">vc</a>);
<a name="l00110"></a>00110
<a name="l00111"></a>00111 <span class="comment">// ScannerFormulaHandler RAII</span>
<a name="l00112"></a>00112 <span class="keyword">class </span>FormulaScanRAII {
<a name="l00113"></a>00113 <span class="keyword">public</span>:
<a name="l00114"></a>00114 FormulaScanRAII(<a class="code" href="classFastSatSolver_1_1IScanner.html" title="Extensible lexical scanner&#39;s interface.">IScanner</a> *scan, <a class="code" href="classFastSatSolver_1_1FormulaContainer.html" title="Container for evaluable formulas.">FormulaContainer</a> *<a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#7e4ae4fbcc08a74a001974dda465b041">fc</a>) {
<a name="l00115"></a>00115 ptr_ = <span class="keyword">new</span> <a class="code" href="classFastSatSolver_1_1ScannerFormulaHandler.html" title="High-level part of parser handling almost all tokens and building InterpretedFormula...">ScannerFormulaHandler</a>(scan, fc);
<a name="l00116"></a>00116 }
<a name="l00117"></a>00117 ~FormulaScanRAII() { <span class="keyword">delete</span> ptr_; }
<a name="l00118"></a>00118 <a class="code" href="classFastSatSolver_1_1ScannerFormulaHandler.html" title="High-level part of parser handling almost all tokens and building InterpretedFormula...">ScannerFormulaHandler</a>* instance() { <span class="keywordflow">return</span> ptr_; }
<a name="l00119"></a>00119 <span class="keyword">private</span>:
<a name="l00120"></a>00120 <a class="code" href="classFastSatSolver_1_1ScannerFormulaHandler.html" title="High-level part of parser handling almost all tokens and building InterpretedFormula...">ScannerFormulaHandler</a> *ptr_;
<a name="l00121"></a>00121 } formulaScan(stringScan.instance(), &<a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#7e4ae4fbcc08a74a001974dda465b041">fc</a>);
<a name="l00122"></a>00122
<a name="l00123"></a>00123 this-><a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#1f253aaff031757c99ad290a139d4572">parserLoop</a>(formulaScan.instance());
<a name="l00124"></a>00124 <span class="keywordflow">if</span> (0==<a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#7e4ae4fbcc08a74a001974dda465b041">fc</a>.<a class="code" href="classFastSatSolver_1_1FormulaContainer.html#ab0d4bbd0884d04dbe281cc2b9d21206" title="Returns count of formulas managed by container.">getLength</a>() || 0==<a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#aa540a1fb84ff7b45694df3ef8b00486">vc</a>.<a class="code" href="classFastSatSolver_1_1VariableContainer.html#ab0d4bbd0884d04dbe281cc2b9d21206" title="Returns count of variables managed by container.">getLength</a>())
<a name="l00125"></a>00125 <a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#5e7656006c54c5a38ba22f9fd0bcb2f1">hasError</a> = <span class="keyword">true</span>;
<a name="l00126"></a>00126 }
<a name="l00127"></a>00127
<a name="l00128"></a>00128
<a name="l00129"></a>00129 <span class="comment">// @private</span>
<a name="l00130"></a><a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#1f253aaff031757c99ad290a139d4572">00130</a> <span class="keywordtype">void</span> <a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#1f253aaff031757c99ad290a139d4572">SatProblem::Private::parserLoop</a>(<a class="code" href="classFastSatSolver_1_1IScanner.html" title="Extensible lexical scanner&#39;s interface.">IScanner</a> *scanner) {
<a name="l00131"></a>00131 <a class="code" href="structFastSatSolver_1_1Token.html" title="Syntax unit representation - also called token.">Token</a> token;
<a name="l00132"></a>00132 <span class="keywordflow">while</span> (0== scanner-><a class="code" href="classFastSatSolver_1_1IScanner.html#53b145cc4de33e6be8076171e8c6a799" title="Abstract scanner&#39;s parsing method.">readNext</a>(&token) && <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f089882ff017eb83e311ec8ad12ab646455" title="end of input">T_EOF</a>!=token.<a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a>) {
<a name="l00133"></a>00133 <span class="keywordflow">switch</span> (token.<a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a>) {
<a name="l00134"></a>00134 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08080dc4844adc27f572dfd7d4c72038f4" title="lexical error">T_ERR_LEX</a>:
<a name="l00135"></a>00135 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ae35a8e0b44afb4174d0357d55484ff1">T_ERR_EXPR</a>:
<a name="l00136"></a>00136 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08c76e1e4acf16e5ca401b5d82cbfe1f0f">T_ERR_PARSE</a>:
<a name="l00137"></a>00137 this-><a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#4a9777d181b01d3df14636fee61ae5b9">printError</a>(token);
<a name="l00138"></a>00138 <span class="keywordflow">break</span>;
<a name="l00139"></a>00139
<a name="l00140"></a>00140 <span class="keywordflow">default</span>:
<a name="l00141"></a>00141 <span class="keywordflow">throw</span> <a class="code" href="classFastSatSolver_1_1GenericException.html" title="Common-usage exception containing error message inside.">GenericException</a>(<span class="stringliteral">"Unhandled token in SatProblemImp::parserLoop"</span>);
<a name="l00142"></a>00142 }
<a name="l00143"></a>00143 }
<a name="l00144"></a>00144 }
<a name="l00145"></a>00145
<a name="l00146"></a>00146
<a name="l00147"></a>00147 <span class="comment">// @private</span>
<a name="l00148"></a><a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#4a9777d181b01d3df14636fee61ae5b9">00148</a> <span class="keywordtype">void</span> <a class="code" href="group__fssIO.html#g7532fbb551a0335ad6c5964a0b9a0364" title="Common routine for printing errors.">SatProblem::Private::printError</a>(<a class="code" href="structFastSatSolver_1_1Token.html" title="Syntax unit representation - also called token.">Token</a> token) {
<a name="l00149"></a>00149 this-><a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#5e7656006c54c5a38ba22f9fd0bcb2f1">hasError</a> = <span class="keyword">true</span>;
<a name="l00150"></a>00150 std::cerr << <a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#c81f9269c8d57eed4d5b56f054fc84de">fileName</a> << <span class="stringliteral">":"</span> << token.<a class="code" href="structFastSatSolver_1_1Token.html#434474dfe11c603cd3512231cdaa8baa" title="Line number in input file (starting with number 1).">m_line</a> << <span class="stringliteral">": error: "</span>;
<a name="l00151"></a>00151 <span class="keywordflow">switch</span> (token.<a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a>) {
<a name="l00152"></a>00152 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08080dc4844adc27f572dfd7d4c72038f4" title="lexical error">T_ERR_LEX</a>: std::cerr << <span class="stringliteral">"lexical error"</span>; <span class="keywordflow">break</span>;
<a name="l00153"></a>00153 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ae35a8e0b44afb4174d0357d55484ff1">T_ERR_EXPR</a>: std::cerr << <span class="stringliteral">"expression error"</span>; <span class="keywordflow">break</span>;
<a name="l00154"></a>00154 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08c76e1e4acf16e5ca401b5d82cbfe1f0f">T_ERR_PARSE</a>: std::cerr << <span class="stringliteral">"syntax error"</span>; <span class="keywordflow">break</span>;
<a name="l00155"></a>00155 <span class="keywordflow">default</span>:
<a name="l00156"></a>00156 <span class="keywordflow">throw</span> <a class="code" href="classFastSatSolver_1_1GenericException.html" title="Common-usage exception containing error message inside.">GenericException</a>(<span class="stringliteral">"Unhandled error in SatProblemImp::printError"</span>);
<a name="l00157"></a>00157 }
<a name="l00158"></a>00158 std::cerr << std::endl;
<a name="l00159"></a>00159 }
<a name="l00160"></a>00160
<a name="l00161"></a>00161
<a name="l00165"></a><a class="code" href="classFastSatSolver_1_1SatProblem.html#92e7e3731c3c44467cadeb9038dd4cb9">00165</a> <span class="keywordtype">int</span> <a class="code" href="classFastSatSolver_1_1SatProblem.html#92e7e3731c3c44467cadeb9038dd4cb9" title="Returns total count of variables managed by SatProblem.">SatProblem::getVarsCount</a> ( ) {
<a name="l00166"></a>00166 <span class="keywordflow">return</span> d-><a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#aa540a1fb84ff7b45694df3ef8b00486">vc</a>.<a class="code" href="classFastSatSolver_1_1VariableContainer.html#ab0d4bbd0884d04dbe281cc2b9d21206" title="Returns count of variables managed by container.">getLength</a>();
<a name="l00167"></a>00167 }
<a name="l00168"></a>00168
<a name="l00169"></a>00169
<a name="l00174"></a><a class="code" href="classFastSatSolver_1_1SatProblem.html#139a3f2e63c60e612c649a57ba1ce9dd">00174</a> <span class="keywordtype">string</span> <a class="code" href="classFastSatSolver_1_1SatProblem.html#139a3f2e63c60e612c649a57ba1ce9dd" title="Returns name of variable with desired index.">SatProblem::getVarName</a> (<span class="keywordtype">int</span> index ) {
<a name="l00175"></a>00175 <span class="keywordflow">return</span> d-><a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#aa540a1fb84ff7b45694df3ef8b00486">vc</a>.<a class="code" href="classFastSatSolver_1_1VariableContainer.html#139a3f2e63c60e612c649a57ba1ce9dd" title="Read name of variable on desired index.">getVarName</a>(index);
<a name="l00176"></a>00176 }
<a name="l00177"></a>00177
<a name="l00178"></a>00178
<a name="l00182"></a><a class="code" href="classFastSatSolver_1_1SatProblem.html#fa9215848a08453610b67d1eb882c641">00182</a> <span class="keywordtype">int</span> <a class="code" href="classFastSatSolver_1_1SatProblem.html#fa9215848a08453610b67d1eb882c641" title="Returns total count of formulas managed by SatProblem.">SatProblem::getFormulasCount</a>() {
<a name="l00183"></a>00183 <span class="keywordflow">return</span> d-><a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#7e4ae4fbcc08a74a001974dda465b041">fc</a>.<a class="code" href="classFastSatSolver_1_1FormulaContainer.html#ab0d4bbd0884d04dbe281cc2b9d21206" title="Returns count of formulas managed by container.">getLength</a>();
<a name="l00184"></a>00184 }
<a name="l00185"></a>00185
<a name="l00186"></a>00186
<a name="l00191"></a><a class="code" href="classFastSatSolver_1_1SatProblem.html#3c6475887daf5925eadbc98109b8a3dc">00191</a> <span class="keywordtype">int</span> <a class="code" href="classFastSatSolver_1_1SatProblem.html#3c6475887daf5925eadbc98109b8a3dc" title="Evaluate all formulas in container using given data and return satisfaction ratio...">SatProblem::getSatsCount</a> (<a class="code" href="classFastSatSolver_1_1ISatItem.html" title="Abstraction of solution candidate.">ISatItem</a> *data ) {
<a name="l00192"></a>00192 <span class="keywordflow">return</span> d-><a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#7e4ae4fbcc08a74a001974dda465b041">fc</a>.<a class="code" href="classFastSatSolver_1_1FormulaContainer.html#b7e70416f171d0356ab2437d92577906" title="Evaluate all formulas in container using given data and return satisfaction ratio...">evalAll</a>(data);
<a name="l00193"></a>00193 }
<a name="l00194"></a>00194
<a name="l00195"></a>00195
<a name="l00199"></a><a class="code" href="classFastSatSolver_1_1SatProblem.html#e9649a3c36b3d2060e9b8bf174f9048e">00199</a> <span class="keywordtype">bool</span> <a class="code" href="classFastSatSolver_1_1SatProblem.html#e9649a3c36b3d2060e9b8bf174f9048e" title="Returns true if SAT Problem is not valid.">SatProblem::hasError</a> ( ) {
<a name="l00200"></a>00200 <span class="keywordflow">return</span> d-><a class="code" href="structFastSatSolver_1_1SatProblem_1_1Private.html#5e7656006c54c5a38ba22f9fd0bcb2f1">hasError</a>;
<a name="l00201"></a>00201 }
<a name="l00202"></a>00202
<a name="l00203"></a>00203 <span class="comment">// ////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////</span>
<a name="l00204"></a>00204 <span class="comment">// VariableContainer implementation</span>
<a name="l00205"></a><a class="code" href="structFastSatSolver_1_1VariableContainer_1_1Private.html">00205</a> <span class="keyword">struct </span><a class="code" href="structFastSatSolver_1_1VariableContainer_1_1Private.html">VariableContainer::Private</a> {
<a name="l00206"></a><a class="code" href="structFastSatSolver_1_1VariableContainer_1_1Private.html#8d18307fda103ddc0a104fff82b251e9">00206</a> <span class="keyword">typedef</span> std::string TVarName;
<a name="l00207"></a><a class="code" href="structFastSatSolver_1_1VariableContainer_1_1Private.html#5776fb6afffc2dda922855d638935161">00207</a> <span class="keyword">typedef</span> std::vector<TVarName> TIndexToName;
<a name="l00208"></a><a class="code" href="structFastSatSolver_1_1VariableContainer_1_1Private.html#a564eb557932c6903a28487ccd5cef5f">00208</a> <span class="keyword">typedef</span> std::map<TVarName, int> TNameToIndex;
<a name="l00209"></a><a class="code" href="structFastSatSolver_1_1VariableContainer_1_1Private.html#db46a4f7f158b11356d781f6f0b3b9f6">00209</a> TIndexToName indexToName;
<a name="l00210"></a><a class="code" href="structFastSatSolver_1_1VariableContainer_1_1Private.html#c592b0427f8cf91d13851480db10de06">00210</a> TNameToIndex nameToIndex;
<a name="l00211"></a><a class="code" href="structFastSatSolver_1_1VariableContainer_1_1Private.html#8b41910066b877c9effd739880b6b15e">00211</a> <span class="keywordtype">int</span> currentIndex;
<a name="l00212"></a>00212 };
<a name="l00213"></a><a class="code" href="classFastSatSolver_1_1VariableContainer.html#00f1722e56ddf903f93f0cde9c47ab04">00213</a> <a class="code" href="classFastSatSolver_1_1VariableContainer.html#00f1722e56ddf903f93f0cde9c47ab04">VariableContainer::VariableContainer</a>():
<a name="l00214"></a>00214 d(new <a class="code" href="structFastSatSolver_1_1VariableContainer_1_1Private.html">Private</a>)
<a name="l00215"></a>00215 {
<a name="l00216"></a>00216 d-><a class="code" href="structFastSatSolver_1_1VariableContainer_1_1Private.html#8b41910066b877c9effd739880b6b15e">currentIndex</a> = 0;
<a name="l00217"></a>00217 }
<a name="l00218"></a><a class="code" href="classFastSatSolver_1_1VariableContainer.html#f7643e55f019aea93deabcb798965a46">00218</a> <a class="code" href="classFastSatSolver_1_1VariableContainer.html#f7643e55f019aea93deabcb798965a46">VariableContainer::~VariableContainer</a>() {
<a name="l00219"></a>00219 <span class="keyword">delete</span> d;
<a name="l00220"></a>00220 }
<a name="l00221"></a><a class="code" href="classFastSatSolver_1_1VariableContainer.html#ab0d4bbd0884d04dbe281cc2b9d21206">00221</a> <span class="keywordtype">int</span> <a class="code" href="classFastSatSolver_1_1VariableContainer.html#ab0d4bbd0884d04dbe281cc2b9d21206" title="Returns count of variables managed by container.">VariableContainer::getLength</a> ( ) {
<a name="l00222"></a>00222 <span class="keywordflow">return</span> d-><a class="code" href="structFastSatSolver_1_1VariableContainer_1_1Private.html#8b41910066b877c9effd739880b6b15e">currentIndex</a>;
<a name="l00223"></a>00223 }
<a name="l00224"></a><a class="code" href="classFastSatSolver_1_1VariableContainer.html#139a3f2e63c60e612c649a57ba1ce9dd">00224</a> <span class="keywordtype">string</span> <a class="code" href="classFastSatSolver_1_1VariableContainer.html#139a3f2e63c60e612c649a57ba1ce9dd" title="Read name of variable on desired index.">VariableContainer::getVarName</a> (<span class="keywordtype">int</span> index ) {
<a name="l00225"></a>00225 assert(index < d->currentIndex);
<a name="l00226"></a>00226 <span class="keywordflow">return</span> d-><a class="code" href="structFastSatSolver_1_1VariableContainer_1_1Private.html#db46a4f7f158b11356d781f6f0b3b9f6">indexToName</a>[index];
<a name="l00227"></a>00227 }
<a name="l00228"></a><a class="code" href="classFastSatSolver_1_1VariableContainer.html#5cfe545a4a8940c871fb05f3e6d55adc">00228</a> <span class="keywordtype">int</span> <a class="code" href="classFastSatSolver_1_1VariableContainer.html#5cfe545a4a8940c871fb05f3e6d55adc" title="Add variable to container, if it wasn&#39;t there before.">VariableContainer::addVariable</a> (std::string name ) {
<a name="l00229"></a>00229 <span class="keywordflow">if</span> (d-><a class="code" href="structFastSatSolver_1_1VariableContainer_1_1Private.html#c592b0427f8cf91d13851480db10de06">nameToIndex</a>.end() != d-><a class="code" href="structFastSatSolver_1_1VariableContainer_1_1Private.html#c592b0427f8cf91d13851480db10de06">nameToIndex</a>.find(name))
<a name="l00230"></a>00230 <span class="comment">// Variable already exists</span>
<a name="l00231"></a>00231 <span class="keywordflow">return</span> d-><a class="code" href="structFastSatSolver_1_1VariableContainer_1_1Private.html#c592b0427f8cf91d13851480db10de06">nameToIndex</a>[name];
<a name="l00232"></a>00232
<a name="l00233"></a>00233 <span class="comment">// Add new variable</span>
<a name="l00234"></a>00234 d-><a class="code" href="structFastSatSolver_1_1VariableContainer_1_1Private.html#c592b0427f8cf91d13851480db10de06">nameToIndex</a>[name] = d-><a class="code" href="structFastSatSolver_1_1VariableContainer_1_1Private.html#8b41910066b877c9effd739880b6b15e">currentIndex</a>;
<a name="l00235"></a>00235 d-><a class="code" href="structFastSatSolver_1_1VariableContainer_1_1Private.html#db46a4f7f158b11356d781f6f0b3b9f6">indexToName</a>.push_back(name);
<a name="l00236"></a>00236 <span class="keywordflow">return</span> (d-><a class="code" href="structFastSatSolver_1_1VariableContainer_1_1Private.html#8b41910066b877c9effd739880b6b15e">currentIndex</a>)++;
<a name="l00237"></a>00237 }
<a name="l00238"></a>00238
<a name="l00239"></a>00239 <span class="comment">// ////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////</span>
<a name="l00240"></a>00240 <span class="comment">// FormulaContainer implementation</span>
<a name="l00241"></a><a class="code" href="structFastSatSolver_1_1FormulaContainer_1_1Private.html">00241</a> <span class="keyword">struct </span><a class="code" href="structFastSatSolver_1_1FormulaContainer_1_1Private.html">FormulaContainer::Private</a> {
<a name="l00242"></a><a class="code" href="structFastSatSolver_1_1FormulaContainer_1_1Private.html#10124ecfa838f96974f7a809ae015cac">00242</a> <span class="keyword">typedef</span> std::list<IFormulaEvaluator *> TContainer;
<a name="l00243"></a><a class="code" href="structFastSatSolver_1_1FormulaContainer_1_1Private.html#0d7d83f2b27e4d691661ac8bc466f4c6">00243</a> TContainer container;
<a name="l00244"></a>00244 };
<a name="l00245"></a><a class="code" href="classFastSatSolver_1_1FormulaContainer.html#68821237779770a79d4e2010928b7897">00245</a> <a class="code" href="classFastSatSolver_1_1FormulaContainer.html#68821237779770a79d4e2010928b7897">FormulaContainer::FormulaContainer</a>():
<a name="l00246"></a>00246 d(new <a class="code" href="structFastSatSolver_1_1FormulaContainer_1_1Private.html">Private</a>)
<a name="l00247"></a>00247 {
<a name="l00248"></a>00248 }
<a name="l00249"></a><a class="code" href="classFastSatSolver_1_1FormulaContainer.html#0fa72f6267c27fdd75c5251fd51757ec">00249</a> <a class="code" href="classFastSatSolver_1_1FormulaContainer.html#0fa72f6267c27fdd75c5251fd51757ec">FormulaContainer::~FormulaContainer</a>() {
<a name="l00250"></a>00250 Private::TContainer::iterator iter;
<a name="l00251"></a>00251 <span class="keywordflow">for</span>(iter=d-><a class="code" href="structFastSatSolver_1_1FormulaContainer_1_1Private.html#0d7d83f2b27e4d691661ac8bc466f4c6">container</a>.begin(); iter!=d-><a class="code" href="structFastSatSolver_1_1FormulaContainer_1_1Private.html#0d7d83f2b27e4d691661ac8bc466f4c6">container</a>.end(); iter++)
<a name="l00252"></a>00252 <span class="keyword">delete</span> *iter;
<a name="l00253"></a>00253 <span class="keyword">delete</span> d;
<a name="l00254"></a>00254 }
<a name="l00255"></a>00255
<a name="l00256"></a>00256
<a name="l00260"></a><a class="code" href="classFastSatSolver_1_1FormulaContainer.html#ab0d4bbd0884d04dbe281cc2b9d21206">00260</a> <span class="keywordtype">int</span> <a class="code" href="classFastSatSolver_1_1FormulaContainer.html#ab0d4bbd0884d04dbe281cc2b9d21206" title="Returns count of formulas managed by container.">FormulaContainer::getLength</a> ( ) {
<a name="l00261"></a>00261 <span class="keywordflow">return</span> d-><a class="code" href="structFastSatSolver_1_1FormulaContainer_1_1Private.html#0d7d83f2b27e4d691661ac8bc466f4c6">container</a>.size();
<a name="l00262"></a>00262 }
<a name="l00263"></a>00263
<a name="l00264"></a>00264
<a name="l00269"></a><a class="code" href="classFastSatSolver_1_1FormulaContainer.html#b7e70416f171d0356ab2437d92577906">00269</a> <span class="keywordtype">int</span> <a class="code" href="classFastSatSolver_1_1FormulaContainer.html#b7e70416f171d0356ab2437d92577906" title="Evaluate all formulas in container using given data and return satisfaction ratio...">FormulaContainer::evalAll</a> (<a class="code" href="classFastSatSolver_1_1ISatItem.html" title="Abstraction of solution candidate.">ISatItem</a> *data ) {
<a name="l00270"></a>00270 <span class="keywordtype">int</span> counter = 0;
<a name="l00271"></a>00271
<a name="l00272"></a>00272 Private::TContainer::iterator iter;
<a name="l00273"></a>00273 <span class="keywordflow">for</span>(iter=d-><a class="code" href="structFastSatSolver_1_1FormulaContainer_1_1Private.html#0d7d83f2b27e4d691661ac8bc466f4c6">container</a>.begin(); iter!=d-><a class="code" href="structFastSatSolver_1_1FormulaContainer_1_1Private.html#0d7d83f2b27e4d691661ac8bc466f4c6">container</a>.end(); iter++) {
<a name="l00274"></a>00274 <a class="code" href="classFastSatSolver_1_1IFormulaEvaluator.html" title="Evaluable formula&#39;s interface.">IFormulaEvaluator</a> *fe = *iter;
<a name="l00275"></a>00275 counter += fe-><a class="code" href="classFastSatSolver_1_1IFormulaEvaluator.html#fb7ef8f1f92d2c0f51e326e05b7b70f4" title="Return true if formula is satisfied for given data.">eval</a>(data);
<a name="l00276"></a>00276 }
<a name="l00277"></a>00277
<a name="l00278"></a>00278 <span class="keywordflow">return</span> counter;
<a name="l00279"></a>00279 }
<a name="l00280"></a>00280
<a name="l00284"></a><a class="code" href="classFastSatSolver_1_1FormulaContainer.html#845ab97b571220fabd160567843909a9">00284</a> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1FormulaContainer.html#845ab97b571220fabd160567843909a9" title="Add formula to container.">FormulaContainer::addFormula</a> (<a class="code" href="classFastSatSolver_1_1IFormulaEvaluator.html" title="Evaluable formula&#39;s interface.">IFormulaEvaluator</a> *formula ) {
<a name="l00285"></a>00285 d-><a class="code" href="structFastSatSolver_1_1FormulaContainer_1_1Private.html#0d7d83f2b27e4d691661ac8bc466f4c6">container</a>.push_back(formula);
<a name="l00286"></a>00286 }
<a name="l00287"></a>00287
<a name="l00288"></a>00288 } <span class="comment">// namespace FastSatSolver</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
SatProblem_8cpp-source.html [Download]