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: Scanner.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>Scanner.cpp</h1><a href="Scanner_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 <iostream></span>
<a name="l00021"></a>00021 <span class="preprocessor">#include <string></span>
<a name="l00022"></a>00022 <span class="preprocessor">#include <map></span>
<a name="l00023"></a>00023 <span class="preprocessor">#include "<a class="code" href="SatProblem_8h.html" title="SAT Problem representation.">SatProblem.h</a>"</span>
<a name="l00024"></a>00024 <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="l00025"></a>00025 <span class="preprocessor">#include "<a class="code" href="Formula_8h.html" title="Propositional formula representation.">Formula.h</a>"</span>
<a name="l00026"></a>00026
<a name="l00027"></a>00027 <span class="keyword">using</span> std::string;
<a name="l00028"></a>00028
<a name="l00029"></a>00029 <span class="keyword">namespace </span>FastSatSolver {
<a name="l00030"></a>00030
<a name="l00031"></a>00031 <span class="comment">// ////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////</span>
<a name="l00032"></a>00032 <span class="comment">// RawScanner implementation</span>
<a name="l00033"></a><a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html">00033</a> <span class="keyword">struct </span><a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html">RawScanner::Private</a> {
<a name="l00034"></a><a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html#f5cd382b45a5ef41d63b95e55fbeca95">00034</a> <span class="keyword">enum</span> <a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html#f5cd382b45a5ef41d63b95e55fbeca95">EState</a> {
<a name="l00035"></a><a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html#f5cd382b45a5ef41d63b95e55fbeca9598d2a2153b4ae0445fa0b114d65b94d9">00035</a> <a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html#f5cd382b45a5ef41d63b95e55fbeca9598d2a2153b4ae0445fa0b114d65b94d9">STATE_INIT</a>,
<a name="l00036"></a><a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html#f5cd382b45a5ef41d63b95e55fbeca95c8eb2b2e98642a979bcfeb3ee3f608c2">00036</a> <a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html#f5cd382b45a5ef41d63b95e55fbeca95c8eb2b2e98642a979bcfeb3ee3f608c2">STATE_BUILDING_STRING</a>
<a name="l00037"></a>00037 };
<a name="l00038"></a><a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html#600b792d6d2ff2e71096dfa60d97a3b0">00038</a> FILE *<a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html#600b792d6d2ff2e71096dfa60d97a3b0">fd</a>;
<a name="l00039"></a><a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html#d846f3735f5b516ab4bb38da639e661b">00039</a> <a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html#f5cd382b45a5ef41d63b95e55fbeca95">EState</a> <a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html#d846f3735f5b516ab4bb38da639e661b">state</a>;
<a name="l00040"></a><a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html#41ebd28ef1d7c6ade45642cb6acc1039">00040</a> <span class="keywordtype">int</span> <a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html#41ebd28ef1d7c6ade45642cb6acc1039">line</a>;
<a name="l00041"></a>00041 };
<a name="l00042"></a><a class="code" href="classFastSatSolver_1_1RawScanner.html#eda82a9d77be864913fef3a8249807e6">00042</a> <a class="code" href="classFastSatSolver_1_1RawScanner.html#eda82a9d77be864913fef3a8249807e6">RawScanner::RawScanner</a> (FILE* fd ):
<a name="l00043"></a>00043 d(new <a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html">Private</a>)
<a name="l00044"></a>00044 {
<a name="l00045"></a>00045 d-><a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html#600b792d6d2ff2e71096dfa60d97a3b0">fd</a> = fd;
<a name="l00046"></a>00046 d-><a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html#d846f3735f5b516ab4bb38da639e661b">state</a> = <a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html#f5cd382b45a5ef41d63b95e55fbeca9598d2a2153b4ae0445fa0b114d65b94d9">Private::STATE_INIT</a>;
<a name="l00047"></a>00047 d-><a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html#41ebd28ef1d7c6ade45642cb6acc1039">line</a> = 1;
<a name="l00048"></a>00048 }
<a name="l00049"></a><a class="code" href="classFastSatSolver_1_1RawScanner.html#6df59392d6637dca348239b3551f4171">00049</a> RawScanner::~RawScanner() {
<a name="l00050"></a>00050 <span class="keyword">delete</span> d;
<a name="l00051"></a>00051 }
<a name="l00052"></a><a class="code" href="classFastSatSolver_1_1RawScanner.html#9e4bab101d39572fe88b9d7c946b6dd6">00052</a> <span class="keywordtype">int</span> <a class="code" href="classFastSatSolver_1_1RawScanner.html#9e4bab101d39572fe88b9d7c946b6dd6" title="Abstract scanner&#39;s parsing method.">RawScanner::readNext</a> (<a class="code" href="structFastSatSolver_1_1Token.html" title="Syntax unit representation - also called token.">Token</a> *token) {
<a name="l00053"></a>00053 <span class="keywordflow">while</span> (1) {
<a name="l00054"></a>00054 token-><a class="code" href="structFastSatSolver_1_1Token.html#434474dfe11c603cd3512231cdaa8baa" title="Line number in input file (starting with number 1).">m_line</a> = d-><a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html#41ebd28ef1d7c6ade45642cb6acc1039">line</a>;
<a name="l00055"></a>00055 <span class="keywordtype">int</span> c = fgetc(d-><a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html#600b792d6d2ff2e71096dfa60d97a3b0">fd</a>);
<a name="l00056"></a>00056 <span class="keywordflow">switch</span>(d-><a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html#d846f3735f5b516ab4bb38da639e661b">state</a>) {
<a name="l00057"></a>00057 <span class="keywordflow">case</span> <a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html#f5cd382b45a5ef41d63b95e55fbeca9598d2a2153b4ae0445fa0b114d65b94d9">Private::STATE_INIT</a>:
<a name="l00058"></a>00058 token-><a class="code" href="structFastSatSolver_1_1Token.html#c394754bd9fa9188334758f4c3fb12d4" title="Extra text carried with token.">m_ext_text</a>.clear();
<a name="l00059"></a>00059 <span class="keywordflow">switch</span> (c) {
<a name="l00060"></a>00060 <span class="keywordflow">case</span> <span class="charliteral">'0'</span>: token-><a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a> = <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08d04c6fedfc6e82b9cd961d926579f541" title="0 = FALSE ">T_FALSE</a>; <span class="keywordflow">return</span> 0;
<a name="l00061"></a>00061 <span class="keywordflow">case</span> <span class="charliteral">'1'</span>: token-><a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a> = <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0866901c4f0f0cf6cd9002834b1f8f2075" title="1 = TRUE ">T_TRUE</a>; <span class="keywordflow">return</span> 0;
<a name="l00062"></a>00062 <span class="keywordflow">case</span> <span class="charliteral">'~'</span>: token-><a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a> = <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0836d22df926b610573f0870bcb5c896f4" title="~ = NOT ">T_NOT</a>; <span class="keywordflow">return</span> 0;
<a name="l00063"></a>00063 <span class="keywordflow">case</span> <span class="charliteral">'&'</span>: token-><a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a> = <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0809d3f67b151bc1e002a78de682fc1c8b" title="&amp; = AND ">T_AND</a>; <span class="keywordflow">return</span> 0;
<a name="l00064"></a>00064 <span class="keywordflow">case</span> <span class="charliteral">'|'</span>: token-><a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a> = <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ee13d53546c9358e6b15a455f1c81fb6" title="| = OR ">T_OR</a>; <span class="keywordflow">return</span> 0;
<a name="l00065"></a>00065 <span class="keywordflow">case</span> <span class="charliteral">'^'</span>: token-><a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a> = <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0839cfc5f9514bb57aa46ffa6ea56a1cc7" title="^ = XOR ">T_XOR</a>; <span class="keywordflow">return</span> 0;
<a name="l00066"></a>00066 <span class="keywordflow">case</span> <span class="charliteral">'('</span>: token-><a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a> = <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f084f1a38203f5130575e81ba913c563c6d" title="(">T_LPAR</a>; <span class="keywordflow">return</span> 0;
<a name="l00067"></a>00067 <span class="keywordflow">case</span> <span class="charliteral">')'</span>: token-><a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a> = <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0873ae5e7e19b86c649347b3fc95e448f9" title=")">T_RPAR</a>; <span class="keywordflow">return</span> 0;
<a name="l00068"></a>00068 <span class="keywordflow">case</span> <span class="charliteral">';'</span>: token-><a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a> = <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f085aa662332b125f31d3083778f48fc5c6" title=";">T_DELIM</a>; <span class="keywordflow">return</span> 0;
<a name="l00069"></a>00069 <span class="keywordflow">case</span> EOF: token-><a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a> = <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f089882ff017eb83e311ec8ad12ab646455" title="end of input">T_EOF</a>; <span class="keywordflow">return</span> 0;
<a name="l00070"></a>00070 <span class="keywordflow">case</span> <span class="charliteral">'\n'</span>:
<a name="l00071"></a>00071 d-><a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html#41ebd28ef1d7c6ade45642cb6acc1039">line</a> ++;
<a name="l00072"></a>00072 <span class="keywordflow">default</span>:
<a name="l00073"></a>00073 <span class="keywordflow">if</span> (isspace(c))
<a name="l00074"></a>00074 <span class="comment">// Ignore white characters</span>
<a name="l00075"></a>00075 <span class="keywordflow">break</span>;
<a name="l00076"></a>00076
<a name="l00077"></a>00077 <span class="keywordflow">if</span> (isalpha(c) || <span class="charliteral">'_'</span>==c) {
<a name="l00078"></a>00078 <span class="comment">// Initiate string building</span>
<a name="l00079"></a>00079 token-><a class="code" href="structFastSatSolver_1_1Token.html#c394754bd9fa9188334758f4c3fb12d4" title="Extra text carried with token.">m_ext_text</a> = c;
<a name="l00080"></a>00080 d-><a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html#d846f3735f5b516ab4bb38da639e661b">state</a> = <a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html#f5cd382b45a5ef41d63b95e55fbeca95c8eb2b2e98642a979bcfeb3ee3f608c2">Private::STATE_BUILDING_STRING</a>;
<a name="l00081"></a>00081 <span class="keywordflow">break</span>;
<a name="l00082"></a>00082 }
<a name="l00083"></a>00083 <span class="comment">// Lexical error</span>
<a name="l00084"></a>00084 token-><a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a> = <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08080dc4844adc27f572dfd7d4c72038f4" title="lexical error">T_ERR_LEX</a>;
<a name="l00085"></a>00085 <span class="keywordflow">return</span> 0;
<a name="l00086"></a>00086 }
<a name="l00087"></a>00087 <span class="keywordflow">break</span>;
<a name="l00088"></a>00088
<a name="l00089"></a>00089 <span class="keywordflow">case</span> <a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html#f5cd382b45a5ef41d63b95e55fbeca95c8eb2b2e98642a979bcfeb3ee3f608c2">Private::STATE_BUILDING_STRING</a>:
<a name="l00090"></a>00090 <span class="keywordflow">if</span> (isalpha(c) || isdigit(c) || <span class="charliteral">'_'</span>==c) {
<a name="l00091"></a>00091 <span class="comment">// Building string</span>
<a name="l00092"></a>00092 token-><a class="code" href="structFastSatSolver_1_1Token.html#c394754bd9fa9188334758f4c3fb12d4" title="Extra text carried with token.">m_ext_text</a> += c;
<a name="l00093"></a>00093 <span class="keywordflow">break</span>;
<a name="l00094"></a>00094 }
<a name="l00095"></a>00095 <span class="comment">// End of string</span>
<a name="l00096"></a>00096 ungetc(c, d-><a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html#600b792d6d2ff2e71096dfa60d97a3b0">fd</a>);
<a name="l00097"></a>00097 d-><a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html#d846f3735f5b516ab4bb38da639e661b">state</a> = <a class="code" href="structFastSatSolver_1_1RawScanner_1_1Private.html#f5cd382b45a5ef41d63b95e55fbeca9598d2a2153b4ae0445fa0b114d65b94d9">Private::STATE_INIT</a>;
<a name="l00098"></a>00098 token-><a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a> = <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f082b93aac4bda1ecc9cd242c671411c323" title="string red from input (shoud be catched by ScannerStringHandler)">T_STRING</a>;
<a name="l00099"></a>00099 <span class="keywordflow">return</span> 0;
<a name="l00100"></a>00100
<a name="l00101"></a>00101 <span class="keywordflow">default</span>:
<a name="l00102"></a>00102 <span class="comment">// Unknown state</span>
<a name="l00103"></a>00103 <span class="keywordflow">return</span> 1;
<a name="l00104"></a>00104 }
<a name="l00105"></a>00105 }
<a name="l00106"></a>00106 }
<a name="l00107"></a>00107
<a name="l00108"></a>00108
<a name="l00109"></a>00109 <span class="comment">// ////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////</span>
<a name="l00110"></a>00110 <span class="comment">// ScannerStringHandler implementation</span>
<a name="l00111"></a><a class="code" href="structFastSatSolver_1_1ScannerStringHandler_1_1Private.html">00111</a> <span class="keyword">struct </span><a class="code" href="structFastSatSolver_1_1ScannerStringHandler_1_1Private.html">ScannerStringHandler::Private</a> {
<a name="l00112"></a><a class="code" href="structFastSatSolver_1_1ScannerStringHandler_1_1Private.html#4995cd359fa71b1b94ceea2e36b68fb0">00112</a> <span class="keyword">typedef</span> std::map<std::string,EToken> TKeyWordMap;
<a name="l00113"></a><a class="code" href="structFastSatSolver_1_1ScannerStringHandler_1_1Private.html#c3875e76a13d85c9aa1c90690680f35d">00113</a> <a class="code" href="classFastSatSolver_1_1IScanner.html" title="Extensible lexical scanner&#39;s interface.">IScanner</a> *scanner;
<a name="l00114"></a><a class="code" href="structFastSatSolver_1_1ScannerStringHandler_1_1Private.html#26012f07dae504ec73e8da210a92b63f">00114</a> <a class="code" href="classFastSatSolver_1_1VariableContainer.html" title="Container for variables names.">VariableContainer</a> *vc;
<a name="l00115"></a><a class="code" href="structFastSatSolver_1_1ScannerStringHandler_1_1Private.html#7d31f86d43719b1e43b1625fb938bf53">00115</a> TKeyWordMap keyWordMap;
<a name="l00116"></a>00116 };
<a name="l00117"></a><a class="code" href="classFastSatSolver_1_1ScannerStringHandler.html#13dccdfc24291d61181a17e494b6c551">00117</a> <a class="code" href="classFastSatSolver_1_1ScannerStringHandler.html#13dccdfc24291d61181a17e494b6c551">ScannerStringHandler::ScannerStringHandler</a> (<a class="code" href="classFastSatSolver_1_1IScanner.html" title="Extensible lexical scanner&#39;s interface.">IScanner</a> *scanner, <a class="code" href="classFastSatSolver_1_1VariableContainer.html" title="Container for variables names.">VariableContainer</a> *vc ):
<a name="l00118"></a>00118 d(new <a class="code" href="structFastSatSolver_1_1ScannerStringHandler_1_1Private.html">Private</a>)
<a name="l00119"></a>00119 {
<a name="l00120"></a>00120 d-><a class="code" href="structFastSatSolver_1_1ScannerStringHandler_1_1Private.html#c3875e76a13d85c9aa1c90690680f35d">scanner</a> = scanner;
<a name="l00121"></a>00121 d-><a class="code" href="structFastSatSolver_1_1ScannerStringHandler_1_1Private.html#26012f07dae504ec73e8da210a92b63f">vc</a> = vc;
<a name="l00122"></a>00122
<a name="l00123"></a>00123 <span class="comment">// Keywords definition</span>
<a name="l00124"></a>00124 d-><a class="code" href="structFastSatSolver_1_1ScannerStringHandler_1_1Private.html#7d31f86d43719b1e43b1625fb938bf53">keyWordMap</a>[<span class="stringliteral">"NOT"</span>] = <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0836d22df926b610573f0870bcb5c896f4" title="~ = NOT ">T_NOT</a>;
<a name="l00125"></a>00125 d-><a class="code" href="structFastSatSolver_1_1ScannerStringHandler_1_1Private.html#7d31f86d43719b1e43b1625fb938bf53">keyWordMap</a>[<span class="stringliteral">"AND"</span>] = <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0809d3f67b151bc1e002a78de682fc1c8b" title="&amp; = AND ">T_AND</a>;
<a name="l00126"></a>00126 d-><a class="code" href="structFastSatSolver_1_1ScannerStringHandler_1_1Private.html#7d31f86d43719b1e43b1625fb938bf53">keyWordMap</a>[<span class="stringliteral">"OR"</span>] = <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ee13d53546c9358e6b15a455f1c81fb6" title="| = OR ">T_OR</a>;
<a name="l00127"></a>00127 d-><a class="code" href="structFastSatSolver_1_1ScannerStringHandler_1_1Private.html#7d31f86d43719b1e43b1625fb938bf53">keyWordMap</a>[<span class="stringliteral">"XOR"</span>] = <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0839cfc5f9514bb57aa46ffa6ea56a1cc7" title="^ = XOR ">T_XOR</a>;
<a name="l00128"></a>00128 d-><a class="code" href="structFastSatSolver_1_1ScannerStringHandler_1_1Private.html#7d31f86d43719b1e43b1625fb938bf53">keyWordMap</a>[<span class="stringliteral">"FALSE"</span>] = <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08d04c6fedfc6e82b9cd961d926579f541" title="0 = FALSE ">T_FALSE</a>;
<a name="l00129"></a>00129 d-><a class="code" href="structFastSatSolver_1_1ScannerStringHandler_1_1Private.html#7d31f86d43719b1e43b1625fb938bf53">keyWordMap</a>[<span class="stringliteral">"TRUE"</span>] = <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0866901c4f0f0cf6cd9002834b1f8f2075" title="1 = TRUE ">T_TRUE</a>;
<a name="l00130"></a>00130 }
<a name="l00131"></a><a class="code" href="classFastSatSolver_1_1ScannerStringHandler.html#fe5ebc1cc8499af6eba4856241e696ab">00131</a> <a class="code" href="classFastSatSolver_1_1ScannerStringHandler.html#fe5ebc1cc8499af6eba4856241e696ab">ScannerStringHandler::~ScannerStringHandler</a>() {
<a name="l00132"></a>00132 <span class="keyword">delete</span> d;
<a name="l00133"></a>00133 }
<a name="l00134"></a><a class="code" href="classFastSatSolver_1_1ScannerStringHandler.html#9e4bab101d39572fe88b9d7c946b6dd6">00134</a> <span class="keywordtype">int</span> <a class="code" href="classFastSatSolver_1_1ScannerStringHandler.html#9e4bab101d39572fe88b9d7c946b6dd6" title="Abstract scanner&#39;s parsing method.">ScannerStringHandler::readNext</a> (<a class="code" href="structFastSatSolver_1_1Token.html" title="Syntax unit representation - also called token.">Token</a>* token ) {
<a name="l00135"></a>00135 <span class="comment">// Use RawScanner to read token</span>
<a name="l00136"></a>00136 d-><a class="code" href="structFastSatSolver_1_1ScannerStringHandler_1_1Private.html#c3875e76a13d85c9aa1c90690680f35d">scanner</a>-><a class="code" href="classFastSatSolver_1_1IScanner.html#53b145cc4de33e6be8076171e8c6a799" title="Abstract scanner&#39;s parsing method.">readNext</a>(token);
<a name="l00137"></a>00137
<a name="l00138"></a>00138 <span class="comment">// Transformations</span>
<a name="l00139"></a>00139 <span class="keywordflow">switch</span> (token-><a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a>) {
<a name="l00140"></a>00140 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f082b93aac4bda1ecc9cd242c671411c323" title="string red from input (shoud be catched by ScannerStringHandler)">T_STRING</a>:
<a name="l00141"></a>00141 <span class="comment">// Handle only T_STRING</span>
<a name="l00142"></a>00142 {
<a name="l00143"></a>00143 <span class="keywordtype">string</span> &text = token-><a class="code" href="structFastSatSolver_1_1Token.html#c394754bd9fa9188334758f4c3fb12d4" title="Extra text carried with token.">m_ext_text</a>;
<a name="l00144"></a>00144 <span class="keywordflow">if</span> (d-><a class="code" href="structFastSatSolver_1_1ScannerStringHandler_1_1Private.html#7d31f86d43719b1e43b1625fb938bf53">keyWordMap</a>.end() != d-><a class="code" href="structFastSatSolver_1_1ScannerStringHandler_1_1Private.html#7d31f86d43719b1e43b1625fb938bf53">keyWordMap</a>.find(text)) {
<a name="l00145"></a>00145 <span class="comment">// Map T_STRING to keywords</span>
<a name="l00146"></a>00146 token-><a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a> = d-><a class="code" href="structFastSatSolver_1_1ScannerStringHandler_1_1Private.html#7d31f86d43719b1e43b1625fb938bf53">keyWordMap</a>[text];
<a name="l00147"></a>00147 <span class="keywordflow">return</span> 0;
<a name="l00148"></a>00148 }
<a name="l00149"></a>00149
<a name="l00150"></a>00150 <span class="comment">// Use string as variable name</span>
<a name="l00151"></a>00151 token-><a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a> = <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ed5262e7be4aa45d3018726fdba828e6" title="managed variable">T_VARIABLE</a>;
<a name="l00152"></a>00152 token-><a class="code" href="structFastSatSolver_1_1Token.html#c3f3512920573101c3e5f47ee86fc713" title="Extra number carried with token.">m_ext_number</a> = d-><a class="code" href="structFastSatSolver_1_1ScannerStringHandler_1_1Private.html#26012f07dae504ec73e8da210a92b63f">vc</a>-><a class="code" href="classFastSatSolver_1_1VariableContainer.html#5cfe545a4a8940c871fb05f3e6d55adc" title="Add variable to container, if it wasn&#39;t there before.">addVariable</a>(text);
<a name="l00153"></a>00153 }
<a name="l00154"></a>00154 <span class="keywordflow">default</span>:
<a name="l00155"></a>00155 <span class="comment">// Default behavior</span>
<a name="l00156"></a>00156 <span class="keywordflow">return</span> 0;
<a name="l00157"></a>00157 }
<a name="l00158"></a>00158 }
<a name="l00159"></a>00159
<a name="l00160"></a>00160
<a name="l00161"></a>00161 <span class="comment">// ////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////</span>
<a name="l00162"></a>00162 <span class="comment">// ScannerFormulaHandler implementation</span>
<a name="l00163"></a><a class="code" href="structFastSatSolver_1_1ScannerFormulaHandler_1_1Private.html">00163</a> <span class="keyword">struct </span><a class="code" href="structFastSatSolver_1_1ScannerFormulaHandler_1_1Private.html">ScannerFormulaHandler::Private</a> {
<a name="l00164"></a><a class="code" href="structFastSatSolver_1_1ScannerFormulaHandler_1_1Private.html#c3875e76a13d85c9aa1c90690680f35d">00164</a> <a class="code" href="classFastSatSolver_1_1IScanner.html" title="Extensible lexical scanner&#39;s interface.">IScanner</a> *scanner;
<a name="l00165"></a><a class="code" href="structFastSatSolver_1_1ScannerFormulaHandler_1_1Private.html#5e2a6b7b8ce6c09d45f67892c8e75719">00165</a> <a class="code" href="classFastSatSolver_1_1FormulaContainer.html" title="Container for evaluable formulas.">FormulaContainer</a> *fc;
<a name="l00166"></a><a class="code" href="structFastSatSolver_1_1ScannerFormulaHandler_1_1Private.html#dbca45c5169936d08319acf20a7dc1bc">00166</a> <a class="code" href="classFastSatSolver_1_1InterpretedFormula.html" title="Interpreted formula implementation.">InterpretedFormula</a> *current;
<a name="l00167"></a><a class="code" href="structFastSatSolver_1_1ScannerFormulaHandler_1_1Private.html#14f945c177f39f41c2efecb95cb69f0a">00167</a> <span class="keywordtype">bool</span> ignoreToDelim;
<a name="l00168"></a>00168 };
<a name="l00169"></a><a class="code" href="classFastSatSolver_1_1ScannerFormulaHandler.html#4be2332d18769e04acf05bac15b1d3ff">00169</a> <a class="code" href="classFastSatSolver_1_1ScannerFormulaHandler.html#4be2332d18769e04acf05bac15b1d3ff">ScannerFormulaHandler::ScannerFormulaHandler</a> (<a class="code" href="classFastSatSolver_1_1IScanner.html" title="Extensible lexical scanner&#39;s interface.">IScanner</a> *scanner, <a class="code" href="classFastSatSolver_1_1FormulaContainer.html" title="Container for evaluable formulas.">FormulaContainer</a> *fc ):
<a name="l00170"></a>00170 d(new <a class="code" href="structFastSatSolver_1_1ScannerFormulaHandler_1_1Private.html">Private</a>)
<a name="l00171"></a>00171 {
<a name="l00172"></a>00172 d-><a class="code" href="structFastSatSolver_1_1ScannerFormulaHandler_1_1Private.html#c3875e76a13d85c9aa1c90690680f35d">scanner</a> = scanner;
<a name="l00173"></a>00173 d-><a class="code" href="structFastSatSolver_1_1ScannerFormulaHandler_1_1Private.html#5e2a6b7b8ce6c09d45f67892c8e75719">fc</a> = fc;
<a name="l00174"></a>00174 d-><a class="code" href="structFastSatSolver_1_1ScannerFormulaHandler_1_1Private.html#14f945c177f39f41c2efecb95cb69f0a">ignoreToDelim</a> = <span class="keyword">false</span>;
<a name="l00175"></a>00175 d-><a class="code" href="structFastSatSolver_1_1ScannerFormulaHandler_1_1Private.html#dbca45c5169936d08319acf20a7dc1bc">current</a> = <span class="keyword">new</span> <a class="code" href="classFastSatSolver_1_1InterpretedFormula.html" title="Interpreted formula implementation.">InterpretedFormula</a>;
<a name="l00176"></a>00176 }
<a name="l00177"></a><a class="code" href="classFastSatSolver_1_1ScannerFormulaHandler.html#49bb111d05115e8cf3bdeeef7d7fad6e">00177</a> <a class="code" href="classFastSatSolver_1_1ScannerFormulaHandler.html#49bb111d05115e8cf3bdeeef7d7fad6e">ScannerFormulaHandler::~ScannerFormulaHandler</a>() {
<a name="l00178"></a>00178 <span class="keyword">delete</span> d-><a class="code" href="structFastSatSolver_1_1ScannerFormulaHandler_1_1Private.html#dbca45c5169936d08319acf20a7dc1bc">current</a>;
<a name="l00179"></a>00179 <span class="keyword">delete</span> d;
<a name="l00180"></a>00180 }
<a name="l00181"></a><a class="code" href="classFastSatSolver_1_1ScannerFormulaHandler.html#9e4bab101d39572fe88b9d7c946b6dd6">00181</a> <span class="keywordtype">int</span> <a class="code" href="classFastSatSolver_1_1ScannerFormulaHandler.html#9e4bab101d39572fe88b9d7c946b6dd6" title="Abstract scanner&#39;s parsing method.">ScannerFormulaHandler::readNext</a> (<a class="code" href="structFastSatSolver_1_1Token.html" title="Syntax unit representation - also called token.">Token</a>* token ) {
<a name="l00182"></a>00182 <span class="comment">// Use ScannerStringHandler to read token</span>
<a name="l00183"></a>00183 <span class="keywordflow">while</span> (0== d-><a class="code" href="structFastSatSolver_1_1ScannerFormulaHandler_1_1Private.html#c3875e76a13d85c9aa1c90690680f35d">scanner</a>-><a class="code" href="classFastSatSolver_1_1IScanner.html#53b145cc4de33e6be8076171e8c6a799" title="Abstract scanner&#39;s parsing method.">readNext</a>(token)) {
<a name="l00184"></a>00184 <span class="keywordflow">switch</span> (token-><a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a>) {
<a name="l00185"></a>00185 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08d04c6fedfc6e82b9cd961d926579f541" title="0 = FALSE ">T_FALSE</a>:
<a name="l00186"></a>00186 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0866901c4f0f0cf6cd9002834b1f8f2075" title="1 = TRUE ">T_TRUE</a>:
<a name="l00187"></a>00187 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0836d22df926b610573f0870bcb5c896f4" title="~ = NOT ">T_NOT</a>:
<a name="l00188"></a>00188 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0809d3f67b151bc1e002a78de682fc1c8b" title="&amp; = AND ">T_AND</a>:
<a name="l00189"></a>00189 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ee13d53546c9358e6b15a455f1c81fb6" title="| = OR ">T_OR</a>:
<a name="l00190"></a>00190 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0839cfc5f9514bb57aa46ffa6ea56a1cc7" title="^ = XOR ">T_XOR</a>:
<a name="l00191"></a>00191 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f084f1a38203f5130575e81ba913c563c6d" title="(">T_LPAR</a>:
<a name="l00192"></a>00192 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0873ae5e7e19b86c649347b3fc95e448f9" title=")">T_RPAR</a>:
<a name="l00193"></a>00193 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ed5262e7be4aa45d3018726fdba828e6" title="managed variable">T_VARIABLE</a>:
<a name="l00194"></a>00194 <span class="keywordflow">if</span> (d-><a class="code" href="structFastSatSolver_1_1ScannerFormulaHandler_1_1Private.html#14f945c177f39f41c2efecb95cb69f0a">ignoreToDelim</a>)
<a name="l00195"></a>00195 <span class="comment">// Ignore token</span>
<a name="l00196"></a>00196 <span class="keywordflow">break</span>;
<a name="l00197"></a>00197
<a name="l00198"></a>00198 <span class="comment">// Parse token by IFormulaBuilder</span>
<a name="l00199"></a>00199 <span class="keywordflow">if</span> (0!= d-><a class="code" href="structFastSatSolver_1_1ScannerFormulaHandler_1_1Private.html#dbca45c5169936d08319acf20a7dc1bc">current</a>-><a class="code" href="classFastSatSolver_1_1InterpretedFormula.html#3f098aa4027d962d5b9c58d6ea8b2a9b" title="Parse given token. Token to parse Returns zero, if no fatal error occurs. Parase...">parse</a>(*token)) {
<a name="l00200"></a>00200 <span class="comment">// Expression error</span>
<a name="l00201"></a>00201 d-><a class="code" href="structFastSatSolver_1_1ScannerFormulaHandler_1_1Private.html#14f945c177f39f41c2efecb95cb69f0a">ignoreToDelim</a> = <span class="keyword">true</span>;
<a name="l00202"></a>00202 token-><a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a> = <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ae35a8e0b44afb4174d0357d55484ff1">T_ERR_EXPR</a>;
<a name="l00203"></a>00203 <span class="keywordflow">return</span> 0;
<a name="l00204"></a>00204 }
<a name="l00205"></a>00205 <span class="keywordflow">break</span>;
<a name="l00206"></a>00206
<a name="l00207"></a>00207 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08080dc4844adc27f572dfd7d4c72038f4" title="lexical error">T_ERR_LEX</a>:
<a name="l00208"></a>00208 <span class="comment">// Lexical error</span>
<a name="l00209"></a>00209 <span class="keywordflow">if</span> (d-><a class="code" href="structFastSatSolver_1_1ScannerFormulaHandler_1_1Private.html#14f945c177f39f41c2efecb95cb69f0a">ignoreToDelim</a>)
<a name="l00210"></a>00210 <span class="comment">// Ignore error</span>
<a name="l00211"></a>00211 <span class="keywordflow">break</span>;
<a name="l00212"></a>00212 d-><a class="code" href="structFastSatSolver_1_1ScannerFormulaHandler_1_1Private.html#14f945c177f39f41c2efecb95cb69f0a">ignoreToDelim</a> = <span class="keyword">true</span>;
<a name="l00213"></a>00213 <span class="keywordflow">return</span> 0;
<a name="l00214"></a>00214
<a name="l00215"></a>00215 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f089882ff017eb83e311ec8ad12ab646455" title="end of input">T_EOF</a>:
<a name="l00216"></a>00216 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f085aa662332b125f31d3083778f48fc5c6" title=";">T_DELIM</a>:
<a name="l00217"></a>00217 d-><a class="code" href="structFastSatSolver_1_1ScannerFormulaHandler_1_1Private.html#dbca45c5169936d08319acf20a7dc1bc">current</a> -> parse(<a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f089882ff017eb83e311ec8ad12ab646455" title="end of input">T_EOF</a>);
<a name="l00218"></a>00218 <span class="keywordflow">if</span> (!d-><a class="code" href="structFastSatSolver_1_1ScannerFormulaHandler_1_1Private.html#14f945c177f39f41c2efecb95cb69f0a">ignoreToDelim</a> && d-><a class="code" href="structFastSatSolver_1_1ScannerFormulaHandler_1_1Private.html#dbca45c5169936d08319acf20a7dc1bc">current</a>-><a class="code" href="classFastSatSolver_1_1InterpretedFormula.html#fe93e17ac89cd97917811068ba2af214" title="Return true if formula is valid. Invalid formulas should be never evaluated. ">isValid</a>()) {
<a name="l00219"></a>00219 <span class="comment">// Formula successfully readed</span>
<a name="l00220"></a>00220 d-><a class="code" href="structFastSatSolver_1_1ScannerFormulaHandler_1_1Private.html#5e2a6b7b8ce6c09d45f67892c8e75719">fc</a>-><a class="code" href="classFastSatSolver_1_1FormulaContainer.html#845ab97b571220fabd160567843909a9" title="Add formula to container.">addFormula</a>(d-><a class="code" href="structFastSatSolver_1_1ScannerFormulaHandler_1_1Private.html#dbca45c5169936d08319acf20a7dc1bc">current</a>);
<a name="l00221"></a>00221 d-><a class="code" href="structFastSatSolver_1_1ScannerFormulaHandler_1_1Private.html#dbca45c5169936d08319acf20a7dc1bc">current</a> = <span class="keyword">new</span> <a class="code" href="classFastSatSolver_1_1InterpretedFormula.html" title="Interpreted formula implementation.">InterpretedFormula</a>;
<a name="l00222"></a>00222 <span class="preprocessor">#if 0//ndef NDEBUG</span>
<a name="l00223"></a>00223 <span class="preprocessor"></span> std::cerr << <span class="stringliteral">">>> Formula red successfully"</span> << std::endl;
<a name="l00224"></a>00224 <span class="preprocessor">#endif // NDEBUG</span>
<a name="l00225"></a>00225 <span class="preprocessor"></span> <span class="keywordflow">if</span> (<a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f085aa662332b125f31d3083778f48fc5c6" title=";">T_DELIM</a>==token-><a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a>)
<a name="l00226"></a>00226 <span class="keywordflow">break</span>;
<a name="l00227"></a>00227 <span class="keywordflow">else</span>
<a name="l00228"></a>00228 <span class="keywordflow">return</span> 0;
<a name="l00229"></a>00229 }
<a name="l00230"></a>00230 <span class="keywordflow">if</span> (<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="l00231"></a>00231 <span class="keywordflow">return</span> 0;
<a name="l00232"></a>00232
<a name="l00233"></a>00233 <span class="comment">// Error recover</span>
<a name="l00234"></a>00234 <span class="preprocessor">#ifndef NDEBUG</span>
<a name="l00235"></a>00235 <span class="preprocessor"></span> std::cerr << <span class="stringliteral">"--- Error recover"</span> << std::endl;
<a name="l00236"></a>00236 <span class="preprocessor">#endif // NDEBUG</span>
<a name="l00237"></a>00237 <span class="preprocessor"></span> <span class="keyword">delete</span> d-><a class="code" href="structFastSatSolver_1_1ScannerFormulaHandler_1_1Private.html#dbca45c5169936d08319acf20a7dc1bc">current</a>;
<a name="l00238"></a>00238 d-><a class="code" href="structFastSatSolver_1_1ScannerFormulaHandler_1_1Private.html#dbca45c5169936d08319acf20a7dc1bc">current</a> = <span class="keyword">new</span> <a class="code" href="classFastSatSolver_1_1InterpretedFormula.html" title="Interpreted formula implementation.">InterpretedFormula</a>;
<a name="l00239"></a>00239 <span class="keywordflow">if</span> (!d-><a class="code" href="structFastSatSolver_1_1ScannerFormulaHandler_1_1Private.html#14f945c177f39f41c2efecb95cb69f0a">ignoreToDelim</a>) {
<a name="l00240"></a>00240 <span class="comment">// Parse error</span>
<a name="l00241"></a>00241 token-><a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a> = <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08c76e1e4acf16e5ca401b5d82cbfe1f0f">T_ERR_PARSE</a>;
<a name="l00242"></a>00242 <span class="keywordflow">return</span> 0;
<a name="l00243"></a>00243 }
<a name="l00244"></a>00244 d-><a class="code" href="structFastSatSolver_1_1ScannerFormulaHandler_1_1Private.html#14f945c177f39f41c2efecb95cb69f0a">ignoreToDelim</a> = <span class="keyword">false</span>;
<a name="l00245"></a>00245 <span class="keywordflow">break</span>;
<a name="l00246"></a>00246
<a name="l00247"></a>00247 <span class="keywordflow">default</span>:
<a name="l00248"></a>00248 <span class="keywordflow">return</span> 0;
<a name="l00249"></a>00249 }
<a name="l00250"></a>00250 }
<a name="l00251"></a>00251 <span class="comment">// This sohould never happen</span>
<a name="l00252"></a>00252 <span class="keywordflow">return</span> -1;
<a name="l00253"></a>00253 }
<a name="l00254"></a>00254
<a name="l00255"></a>00255 } <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
Scanner_8cpp-source.html [Download]