<!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: Formula.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>Formula.cpp</h1><a href="Formula_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 <assert.h></span>
<a name="l00021"></a>00021 <span class="preprocessor">#include <iostream></span>
<a name="l00022"></a>00022 <span class="preprocessor">#include <sstream></span>
<a name="l00023"></a>00023 <span class="preprocessor">#include <vector></span>
<a name="l00024"></a>00024 <span class="preprocessor">#include <stack></span>
<a name="l00025"></a>00025 <span class="preprocessor">#include <list></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="SatSolver_8h.html" title="ISatItem, IObserver and AbstractSatSolver with its base classes.">SatSolver.h</a>"</span>
<a name="l00028"></a>00028 <span class="preprocessor">#include "<a class="code" href="Formula_8h.html" title="Propositional formula representation.">Formula.h</a>"</span>
<a name="l00029"></a>00029
<a name="l00030"></a>00030 <span class="keyword">using</span> std::string;
<a name="l00031"></a>00031
<a name="l00032"></a>00032 <span class="keyword">namespace </span>FastSatSolver {
<a name="l00033"></a>00033
<a name="l00034"></a><a class="code" href="namespaceFastSatSolver.html#3283c5d2be8501320d2e0b9bb810d24f">00034</a> <span class="keyword">typedef</span> std::stack<bool> <a class="code" href="namespaceFastSatSolver.html#3283c5d2be8501320d2e0b9bb810d24f">TRuntimeStack</a>;
<a name="l00035"></a>00035
<a name="l00039"></a><a class="code" href="namespaceFastSatSolver.html#da4ebb227211f96616c9e6681a944bc1">00039</a> <span class="keyword">static</span> <span class="keyword">const</span> <span class="keywordtype">int</span> <a class="code" href="namespaceFastSatSolver.html#da4ebb227211f96616c9e6681a944bc1" title="Precedence table size (2 dimensional table).">TABLE_SIZE</a> = 8;
<a name="l00040"></a>00040
<a name="l00044"></a><a class="code" href="namespaceFastSatSolver.html#bc8561e3a5409d789692b9a1dc78d653">00044</a> <span class="keyword">static</span> <span class="keyword">const</span> <a class="code" href="group__SatProblem.html#g9093554967c90043b2a4a74c028f3f08" title="Scanner tokens enumeration.">EToken</a> <a class="code" href="namespaceFastSatSolver.html#bc8561e3a5409d789692b9a1dc78d653" title="Precedence table.">table</a>[<a class="code" href="namespaceFastSatSolver.html#da4ebb227211f96616c9e6681a944bc1" title="Precedence table size (2 dimensional table).">TABLE_SIZE</a>][<a class="code" href="namespaceFastSatSolver.html#da4ebb227211f96616c9e6681a944bc1" title="Precedence table size (2 dimensional table).">TABLE_SIZE</a>] = {
<a name="l00045"></a>00045 <span class="comment">/* 0 1 2 3 4 5 6 7 */</span>
<a name="l00046"></a>00046 <span class="comment">/* XOR OR AND NOT ( ) i $ */</span>
<a name="l00047"></a>00047 <span class="comment">/* 0 XOR */</span> { <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08c53e9b3c78892af3eabea36deee730a8" title="control &gt; ">T_PARSER_GT</a>, <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08c53e9b3c78892af3eabea36deee730a8" title="control &gt; ">T_PARSER_GT</a>, T_PARSER_GT, <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0807b73798f72d658ca655a549447b47d6" title="control &lt; ">T_PARSER_LT</a>, T_PARSER_LT, T_PARSER_GT, T_PARSER_LT, T_PARSER_GT, },
<a name="l00048"></a>00048 <span class="comment">/* 1 OR */</span> { <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08c53e9b3c78892af3eabea36deee730a8" title="control &gt; ">T_PARSER_GT</a>, <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08c53e9b3c78892af3eabea36deee730a8" title="control &gt; ">T_PARSER_GT</a>, T_PARSER_GT, <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0807b73798f72d658ca655a549447b47d6" title="control &lt; ">T_PARSER_LT</a>, T_PARSER_LT, T_PARSER_GT, T_PARSER_LT, T_PARSER_GT, },
<a name="l00049"></a>00049 <span class="comment">/* 2 AND */</span> { <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08c53e9b3c78892af3eabea36deee730a8" title="control &gt; ">T_PARSER_GT</a>, <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08c53e9b3c78892af3eabea36deee730a8" title="control &gt; ">T_PARSER_GT</a>, T_PARSER_GT, <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0807b73798f72d658ca655a549447b47d6" title="control &lt; ">T_PARSER_LT</a>, T_PARSER_LT, T_PARSER_GT, T_PARSER_LT, T_PARSER_GT, },
<a name="l00050"></a>00050 <span class="comment">/* 3 NOT */</span> { <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08c53e9b3c78892af3eabea36deee730a8" title="control &gt; ">T_PARSER_GT</a>, <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08c53e9b3c78892af3eabea36deee730a8" title="control &gt; ">T_PARSER_GT</a>, T_PARSER_GT, <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0807b73798f72d658ca655a549447b47d6" title="control &lt; ">T_PARSER_LT</a>, T_PARSER_LT, T_PARSER_GT, T_PARSER_LT, T_PARSER_GT, },
<a name="l00051"></a>00051 <span class="comment">/* 4 ( */</span> { <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0807b73798f72d658ca655a549447b47d6" title="control &lt; ">T_PARSER_LT</a>, <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0807b73798f72d658ca655a549447b47d6" title="control &lt; ">T_PARSER_LT</a>, T_PARSER_LT, T_PARSER_LT, T_PARSER_LT, <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f086198c3be29647549fdb9e8a6da818acd" title="control = ">T_PARSER_EQ</a>, T_PARSER_LT, <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f084a234c50a27b7ab40334ab8d52b6b67f" title="invalid sequence">T_PARSER_INV</a>, },
<a name="l00052"></a>00052 <span class="comment">/* 5 ) */</span> { <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08c53e9b3c78892af3eabea36deee730a8" title="control &gt; ">T_PARSER_GT</a>, <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08c53e9b3c78892af3eabea36deee730a8" title="control &gt; ">T_PARSER_GT</a>, T_PARSER_GT, T_PARSER_GT, <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f084a234c50a27b7ab40334ab8d52b6b67f" title="invalid sequence">T_PARSER_INV</a>, T_PARSER_GT, T_PARSER_INV, T_PARSER_GT, },
<a name="l00053"></a>00053 <span class="comment">/* 6 i */</span> { <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08c53e9b3c78892af3eabea36deee730a8" title="control &gt; ">T_PARSER_GT</a>, <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08c53e9b3c78892af3eabea36deee730a8" title="control &gt; ">T_PARSER_GT</a>, T_PARSER_GT, T_PARSER_GT, <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f084a234c50a27b7ab40334ab8d52b6b67f" title="invalid sequence">T_PARSER_INV</a>, T_PARSER_GT, T_PARSER_INV, T_PARSER_GT, },
<a name="l00054"></a>00054 <span class="comment">/* 7 $ */</span> { <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0807b73798f72d658ca655a549447b47d6" title="control &lt; ">T_PARSER_LT</a>, <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0807b73798f72d658ca655a549447b47d6" title="control &lt; ">T_PARSER_LT</a>, T_PARSER_LT, T_PARSER_LT, T_PARSER_LT, <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f084a234c50a27b7ab40334ab8d52b6b67f" title="invalid sequence">T_PARSER_INV</a>, T_PARSER_LT, <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f089882ff017eb83e311ec8ad12ab646455" title="end of input">T_EOF</a>, },
<a name="l00055"></a>00055 };
<a name="l00056"></a>00056
<a name="l00057"></a><a class="code" href="namespaceFastSatSolver.html#c133e51b507357315bd8f3083d0566ce">00057</a> <span class="keyword">inline</span> <span class="keywordtype">int</span> <a class="code" href="namespaceFastSatSolver.html#c133e51b507357315bd8f3083d0566ce">tableGetIndex</a>(<a class="code" href="group__SatProblem.html#g9093554967c90043b2a4a74c028f3f08" title="Scanner tokens enumeration.">EToken</a> e) {
<a name="l00058"></a>00058 <span class="keywordflow">switch</span> (e) {
<a name="l00059"></a>00059 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0839cfc5f9514bb57aa46ffa6ea56a1cc7" title="^ = XOR ">T_XOR</a>: <span class="comment">/* 0 XOR */</span> <span class="keywordflow">return</span> 0;
<a name="l00060"></a>00060 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ee13d53546c9358e6b15a455f1c81fb6" title="| = OR ">T_OR</a>: <span class="comment">/* 1 OR */</span> <span class="keywordflow">return</span> 1;
<a name="l00061"></a>00061 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0809d3f67b151bc1e002a78de682fc1c8b" title="&amp; = AND ">T_AND</a>: <span class="comment">/* 2 AND */</span> <span class="keywordflow">return</span> 2;
<a name="l00062"></a>00062 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0836d22df926b610573f0870bcb5c896f4" title="~ = NOT ">T_NOT</a>: <span class="comment">/* 3 NOT */</span> <span class="keywordflow">return</span> 3;
<a name="l00063"></a>00063 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f084f1a38203f5130575e81ba913c563c6d" title="(">T_LPAR</a>: <span class="comment">/* 4 ( */</span> <span class="keywordflow">return</span> 4;
<a name="l00064"></a>00064 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0873ae5e7e19b86c649347b3fc95e448f9" title=")">T_RPAR</a>: <span class="comment">/* 5 ) */</span> <span class="keywordflow">return</span> 5;
<a name="l00065"></a>00065
<a name="l00066"></a>00066 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ed5262e7be4aa45d3018726fdba828e6" title="managed variable">T_VARIABLE</a>:
<a name="l00067"></a>00067 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08d04c6fedfc6e82b9cd961d926579f541" title="0 = FALSE ">T_FALSE</a>:
<a name="l00068"></a>00068 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0866901c4f0f0cf6cd9002834b1f8f2075" title="1 = TRUE ">T_TRUE</a>:
<a name="l00069"></a>00069 <span class="comment">/* 6 i */</span>
<a name="l00070"></a>00070 <span class="keywordflow">return</span> 6;
<a name="l00071"></a>00071
<a name="l00072"></a>00072 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f085aa662332b125f31d3083778f48fc5c6" title=";">T_DELIM</a>:
<a name="l00073"></a>00073 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f089882ff017eb83e311ec8ad12ab646455" title="end of input">T_EOF</a>:
<a name="l00074"></a>00074 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f085a46ce2527667b882c7cb58ba5062e2a" title="bottom of parser stack (behaves as terminal)">T_STACK_BOTTOM</a>:
<a name="l00075"></a>00075 <span class="comment">/* 7 $ */</span>
<a name="l00076"></a>00076 <span class="keywordflow">return</span> 7;
<a name="l00077"></a>00077
<a name="l00078"></a>00078 <span class="keywordflow">default</span>:
<a name="l00079"></a>00079 <span class="comment">// Out of range</span>
<a name="l00080"></a>00080 <span class="keywordflow">return</span> -1;
<a name="l00081"></a>00081 }
<a name="l00082"></a>00082 }
<a name="l00083"></a>00083
<a name="l00084"></a><a class="code" href="namespaceFastSatSolver.html#dbd4b0d41cba5d4e22426cf58ecbd05c">00084</a> <span class="keyword">inline</span> <a class="code" href="group__SatProblem.html#g9093554967c90043b2a4a74c028f3f08" title="Scanner tokens enumeration.">EToken</a> <a class="code" href="namespaceFastSatSolver.html#dbd4b0d41cba5d4e22426cf58ecbd05c">tableLookup</a>(<a class="code" href="group__SatProblem.html#g9093554967c90043b2a4a74c028f3f08" title="Scanner tokens enumeration.">EToken</a> topTerm, <a class="code" href="group__SatProblem.html#g9093554967c90043b2a4a74c028f3f08" title="Scanner tokens enumeration.">EToken</a> input) {
<a name="l00085"></a>00085 <span class="keyword">const</span> <span class="keywordtype">int</span> i = <a class="code" href="namespaceFastSatSolver.html#c133e51b507357315bd8f3083d0566ce">tableGetIndex</a>(topTerm);
<a name="l00086"></a>00086 <span class="keyword">const</span> <span class="keywordtype">int</span> j = <a class="code" href="namespaceFastSatSolver.html#c133e51b507357315bd8f3083d0566ce">tableGetIndex</a>(input);
<a name="l00087"></a>00087 <span class="keywordflow">if</span> (i<0 || j<0)
<a name="l00088"></a>00088 <span class="comment">// Out of range</span>
<a name="l00089"></a>00089 <span class="keywordflow">return</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f084a234c50a27b7ab40334ab8d52b6b67f" title="invalid sequence">T_PARSER_INV</a>;
<a name="l00090"></a>00090
<a name="l00091"></a>00091 <a class="code" href="group__SatProblem.html#g9093554967c90043b2a4a74c028f3f08" title="Scanner tokens enumeration.">EToken</a> result = <a class="code" href="namespaceFastSatSolver.html#bc8561e3a5409d789692b9a1dc78d653" title="Precedence table.">table</a>[i][j];
<a name="l00092"></a>00092 <span class="preprocessor">#if 0//ndef NDEBUG</span>
<a name="l00093"></a>00093 <span class="preprocessor"></span> std::cerr << <span class="stringliteral">"tableLookup("</span> << i << <span class="stringliteral">", "</span> << j << <span class="stringliteral">") = "</span> << result << std::endl;
<a name="l00094"></a>00094 <span class="preprocessor">#endif // NDEBUG</span>
<a name="l00095"></a>00095 <span class="preprocessor"></span> <span class="keywordflow">return</span> result;
<a name="l00096"></a>00096 }
<a name="l00097"></a>00097
<a name="l00098"></a><a class="code" href="namespaceFastSatSolver.html#b217e1ddb2f6d7563346b307ad40b9ff">00098</a> <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceFastSatSolver.html#b217e1ddb2f6d7563346b307ad40b9ff">isTokenTerminal</a> (<a class="code" href="structFastSatSolver_1_1Token.html" title="Syntax unit representation - also called token.">Token</a> token) {
<a name="l00099"></a>00099 <span class="comment">// FIXME: not sure while copy-pasting</span>
<a name="l00100"></a>00100 <span class="keywordflow">return</span> (token.<a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a> < <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ec24fb692561834cef7a9475281a778b" title="expression (recursively)">T_PARSER_EXPR</a>);
<a name="l00101"></a>00101 }
<a name="l00102"></a>00102
<a name="l00103"></a><a class="code" href="classFastSatSolver_1_1ParserStack.html">00103</a> <span class="keyword">class </span><a class="code" href="classFastSatSolver_1_1ParserStack.html">ParserStack</a> {
<a name="l00104"></a>00104 <span class="keyword">public</span>:
<a name="l00105"></a><a class="code" href="classFastSatSolver_1_1ParserStack.html#3f7874f293605da18e594ec788f2e04c">00105</a> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1ParserStack.html#3f7874f293605da18e594ec788f2e04c">push</a>(<a class="code" href="structFastSatSolver_1_1Token.html" title="Syntax unit representation - also called token.">Token</a> token) {
<a name="l00106"></a>00106 container_.push_back(token);
<a name="l00107"></a>00107 }
<a name="l00108"></a>00108
<a name="l00109"></a>00109 <span class="comment">// TODO: Copy warning from original code</span>
<a name="l00110"></a><a class="code" href="classFastSatSolver_1_1ParserStack.html#d255a481013734591759fed43b2d4dd5">00110</a> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1ParserStack.html#d255a481013734591759fed43b2d4dd5">insertLt</a>() {
<a name="l00111"></a>00111 <a class="code" href="structFastSatSolver_1_1Token.html" title="Syntax unit representation - also called token.">Token</a> last = container_.back();
<a name="l00112"></a>00112 <span class="keywordflow">if</span> (<a class="code" href="namespaceFastSatSolver.html#b217e1ddb2f6d7563346b307ad40b9ff">isTokenTerminal</a>(last))
<a name="l00113"></a>00113 container_.push_back(<a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0807b73798f72d658ca655a549447b47d6" title="control &lt; ">T_PARSER_LT</a>);
<a name="l00114"></a>00114 <span class="keywordflow">else</span> {
<a name="l00115"></a>00115 <a class="code" href="structFastSatSolver_1_1Token.html" title="Syntax unit representation - also called token.">Token</a> last = container_.back();
<a name="l00116"></a>00116 container_.pop_back();
<a name="l00117"></a>00117 container_.push_back(<a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0807b73798f72d658ca655a549447b47d6" title="control &lt; ">T_PARSER_LT</a>);
<a name="l00118"></a>00118 container_.push_back(last);
<a name="l00119"></a>00119 }
<a name="l00120"></a>00120 }
<a name="l00121"></a>00121
<a name="l00122"></a><a class="code" href="classFastSatSolver_1_1ParserStack.html#f2e6332cb53b0f9e5c0c70fd6b45fde1">00122</a> <a class="code" href="structFastSatSolver_1_1Token.html" title="Syntax unit representation - also called token.">Token</a> <a class="code" href="classFastSatSolver_1_1ParserStack.html#f2e6332cb53b0f9e5c0c70fd6b45fde1">top</a>() {
<a name="l00123"></a>00123 <span class="keywordflow">return</span> container_.back();
<a name="l00124"></a>00124 }
<a name="l00125"></a>00125
<a name="l00126"></a><a class="code" href="classFastSatSolver_1_1ParserStack.html#dabcc89ce1a26243aa760d2340caf2ce">00126</a> <a class="code" href="structFastSatSolver_1_1Token.html" title="Syntax unit representation - also called token.">Token</a> <a class="code" href="classFastSatSolver_1_1ParserStack.html#dabcc89ce1a26243aa760d2340caf2ce">pop</a>() {
<a name="l00127"></a>00127 <a class="code" href="structFastSatSolver_1_1Token.html" title="Syntax unit representation - also called token.">Token</a> last = container_.back();
<a name="l00128"></a>00128 container_.pop_back();
<a name="l00129"></a>00129 <span class="keywordflow">return</span> last;
<a name="l00130"></a>00130 }
<a name="l00131"></a>00131
<a name="l00132"></a><a class="code" href="classFastSatSolver_1_1ParserStack.html#a956625529b5f3ba0ae69f37730b2da9">00132</a> <span class="keywordtype">bool</span> <a class="code" href="classFastSatSolver_1_1ParserStack.html#a956625529b5f3ba0ae69f37730b2da9">popAndCompare</a>(<a class="code" href="group__SatProblem.html#g9093554967c90043b2a4a74c028f3f08" title="Scanner tokens enumeration.">EToken</a> e) {
<a name="l00133"></a>00133 <a class="code" href="structFastSatSolver_1_1Token.html" title="Syntax unit representation - also called token.">Token</a> t = this-><a class="code" href="classFastSatSolver_1_1ParserStack.html#dabcc89ce1a26243aa760d2340caf2ce">pop</a>();
<a name="l00134"></a>00134 <span class="keywordflow">return</span> t.<a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a> == e;
<a name="l00135"></a>00135 }
<a name="l00136"></a>00136
<a name="l00137"></a><a class="code" href="classFastSatSolver_1_1ParserStack.html#17b77b7c79888263bd2c2a98e5093c36">00137</a> <a class="code" href="structFastSatSolver_1_1Token.html" title="Syntax unit representation - also called token.">Token</a> <a class="code" href="classFastSatSolver_1_1ParserStack.html#17b77b7c79888263bd2c2a98e5093c36">topTerm</a>() {
<a name="l00138"></a>00138 <span class="keywordtype">size_t</span> size = container_.size();
<a name="l00139"></a>00139 <a class="code" href="structFastSatSolver_1_1Token.html" title="Syntax unit representation - also called token.">Token</a> last = container_.back();
<a name="l00140"></a>00140 <span class="keywordflow">if</span> (<a class="code" href="namespaceFastSatSolver.html#b217e1ddb2f6d7563346b307ad40b9ff">isTokenTerminal</a>(last))
<a name="l00141"></a>00141 <span class="keywordflow">return</span> last;
<a name="l00142"></a>00142 <span class="keywordflow">else</span>
<a name="l00143"></a>00143 <span class="comment">// return one before last</span>
<a name="l00144"></a>00144 <span class="keywordflow">return</span> container_[size-2];
<a name="l00145"></a>00145 }
<a name="l00146"></a>00146
<a name="l00147"></a>00147 <span class="keyword">private</span>:
<a name="l00148"></a>00148 <span class="keyword">typedef</span> std::vector<Token> TContainer;
<a name="l00149"></a>00149 TContainer container_;
<a name="l00150"></a>00150 };
<a name="l00151"></a>00151
<a name="l00152"></a><a class="code" href="classFastSatSolver_1_1Cmd.html">00152</a> <span class="keyword">class </span><a class="code" href="classFastSatSolver_1_1Cmd.html">Cmd</a> {
<a name="l00153"></a>00153 <span class="keyword">public</span>:
<a name="l00154"></a>00154 <span class="keyword">static</span> <a class="code" href="classFastSatSolver_1_1Cmd.html">Cmd</a>* <a class="code" href="classFastSatSolver_1_1Cmd.html#1588352becd13ca8d6fdf0e89f659187">fromToken</a>(<a class="code" href="structFastSatSolver_1_1Token.html" title="Syntax unit representation - also called token.">Token</a> token);
<a name="l00155"></a><a class="code" href="classFastSatSolver_1_1Cmd.html#b318b4e712b6af4cc150d5ca756e96c3">00155</a> <span class="keyword">virtual</span> <a class="code" href="classFastSatSolver_1_1Cmd.html#b318b4e712b6af4cc150d5ca756e96c3">~Cmd</a>() { }
<a name="l00156"></a>00156 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1Cmd.html#ba38bc9dd22a41193bcfe1670d539009">execute</a>(<a class="code" href="namespaceFastSatSolver.html#3283c5d2be8501320d2e0b9bb810d24f">TRuntimeStack</a> *, <a class="code" href="classFastSatSolver_1_1ISatItem.html" title="Abstraction of solution candidate.">ISatItem</a> *) = 0;
<a name="l00157"></a>00157 <span class="keyword">protected</span>:
<a name="l00158"></a><a class="code" href="classFastSatSolver_1_1Cmd.html#4576bda79facb39fdec949dd3d0c045b">00158</a> <a class="code" href="classFastSatSolver_1_1Cmd.html#4576bda79facb39fdec949dd3d0c045b">Cmd</a>() { }
<a name="l00159"></a>00159 };
<a name="l00160"></a><a class="code" href="classFastSatSolver_1_1CmdConstant.html">00160</a> <span class="keyword">class </span><a class="code" href="classFastSatSolver_1_1CmdConstant.html">CmdConstant</a>: <span class="keyword">public</span> <a class="code" href="classFastSatSolver_1_1Cmd.html">Cmd</a> {
<a name="l00161"></a>00161 <span class="keyword">public</span>:
<a name="l00162"></a><a class="code" href="classFastSatSolver_1_1CmdConstant.html#6ab2f543cbaef0c718148b521e358263">00162</a> <a class="code" href="classFastSatSolver_1_1CmdConstant.html#6ab2f543cbaef0c718148b521e358263">CmdConstant</a>(<span class="keywordtype">bool</span> value): b(value) { }
<a name="l00163"></a><a class="code" href="classFastSatSolver_1_1CmdConstant.html#6ea521b36577ea6a30407c28ab1e0189">00163</a> <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1CmdConstant.html#6ea521b36577ea6a30407c28ab1e0189">execute</a>(<a class="code" href="namespaceFastSatSolver.html#3283c5d2be8501320d2e0b9bb810d24f">TRuntimeStack</a> *stack, <a class="code" href="classFastSatSolver_1_1ISatItem.html" title="Abstraction of solution candidate.">ISatItem</a> *) {
<a name="l00164"></a>00164 stack->push(b);
<a name="l00165"></a>00165 }
<a name="l00166"></a>00166 <span class="keyword">private</span>:
<a name="l00167"></a>00167 <span class="keywordtype">bool</span> b;
<a name="l00168"></a>00168 };
<a name="l00169"></a><a class="code" href="classFastSatSolver_1_1CmdVariable.html">00169</a> <span class="keyword">class </span><a class="code" href="classFastSatSolver_1_1CmdVariable.html">CmdVariable</a>: <span class="keyword">public</span> <a class="code" href="classFastSatSolver_1_1Cmd.html">Cmd</a> {
<a name="l00170"></a>00170 <span class="keyword">public</span>:
<a name="l00171"></a><a class="code" href="classFastSatSolver_1_1CmdVariable.html#9feddef4f090adfb49b07b1f05b503c6">00171</a> <a class="code" href="classFastSatSolver_1_1CmdVariable.html#9feddef4f090adfb49b07b1f05b503c6">CmdVariable</a>(<span class="keywordtype">int</span> varId): id(varId) { }
<a name="l00172"></a><a class="code" href="classFastSatSolver_1_1CmdVariable.html#fdae54d91f3afa272d6260f16b99f0c6">00172</a> <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1CmdVariable.html#fdae54d91f3afa272d6260f16b99f0c6">execute</a>(<a class="code" href="namespaceFastSatSolver.html#3283c5d2be8501320d2e0b9bb810d24f">TRuntimeStack</a> *stack, <a class="code" href="classFastSatSolver_1_1ISatItem.html" title="Abstraction of solution candidate.">ISatItem</a> *data) {
<a name="l00173"></a>00173 assert(<span class="keywordtype">id</span> >= 0);
<a name="l00174"></a>00174 assert(id < data->getLength());
<a name="l00175"></a>00175 <span class="keywordtype">bool</span> b = data-><a class="code" href="classFastSatSolver_1_1ISatItem.html#ef9eadbc8fd10e01f1b37f85c6e08a67" title="Returns value of desired bit (resp. variable).">getBit</a>(<span class="keywordtype">id</span>);
<a name="l00176"></a>00176 stack->push(b);
<a name="l00177"></a>00177 }
<a name="l00178"></a>00178 <span class="keyword">private</span>:
<a name="l00179"></a>00179 <span class="keywordtype">int</span> id;
<a name="l00180"></a>00180 };
<a name="l00181"></a><a class="code" href="classFastSatSolver_1_1CmdUnaryNot.html">00181</a> <span class="keyword">class </span><a class="code" href="classFastSatSolver_1_1CmdUnaryNot.html">CmdUnaryNot</a>: <span class="keyword">public</span> <a class="code" href="classFastSatSolver_1_1Cmd.html">Cmd</a> {
<a name="l00182"></a>00182 <span class="keyword">public</span>:
<a name="l00183"></a><a class="code" href="classFastSatSolver_1_1CmdUnaryNot.html#6ea521b36577ea6a30407c28ab1e0189">00183</a> <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1CmdUnaryNot.html#6ea521b36577ea6a30407c28ab1e0189">execute</a>(<a class="code" href="namespaceFastSatSolver.html#3283c5d2be8501320d2e0b9bb810d24f">TRuntimeStack</a> *stack, <a class="code" href="classFastSatSolver_1_1ISatItem.html" title="Abstraction of solution candidate.">ISatItem</a> *) {
<a name="l00184"></a>00184 assert(!stack->empty());
<a name="l00185"></a>00185 <span class="keywordtype">bool</span> b = stack->top();
<a name="l00186"></a>00186 stack->pop();
<a name="l00187"></a>00187 stack->push(!b);
<a name="l00188"></a>00188 }
<a name="l00189"></a>00189 };
<a name="l00190"></a><a class="code" href="classFastSatSolver_1_1CmdBinary.html">00190</a> <span class="keyword">class </span><a class="code" href="classFastSatSolver_1_1CmdBinary.html">CmdBinary</a>: <span class="keyword">public</span> <a class="code" href="classFastSatSolver_1_1Cmd.html">Cmd</a> {
<a name="l00191"></a>00191 <span class="keyword">public</span>:
<a name="l00192"></a><a class="code" href="classFastSatSolver_1_1CmdBinary.html#f8dd8d81cecfc5fc598090df8d5171f6">00192</a> <a class="code" href="classFastSatSolver_1_1CmdBinary.html#f8dd8d81cecfc5fc598090df8d5171f6">CmdBinary</a>(<a class="code" href="group__SatProblem.html#g9093554967c90043b2a4a74c028f3f08" title="Scanner tokens enumeration.">EToken</a> e): et(e) { }
<a name="l00193"></a><a class="code" href="classFastSatSolver_1_1CmdBinary.html#6ea521b36577ea6a30407c28ab1e0189">00193</a> <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classFastSatSolver_1_1CmdBinary.html#6ea521b36577ea6a30407c28ab1e0189">execute</a>(<a class="code" href="namespaceFastSatSolver.html#3283c5d2be8501320d2e0b9bb810d24f">TRuntimeStack</a> *stack, <a class="code" href="classFastSatSolver_1_1ISatItem.html" title="Abstraction of solution candidate.">ISatItem</a> *) {
<a name="l00194"></a>00194 assert(!stack->empty());
<a name="l00195"></a>00195 <span class="keywordtype">bool</span> a = stack->top();
<a name="l00196"></a>00196 stack->pop();
<a name="l00197"></a>00197
<a name="l00198"></a>00198 assert(!stack->empty());
<a name="l00199"></a>00199 <span class="keywordtype">bool</span> b = stack->top();
<a name="l00200"></a>00200 stack->pop();
<a name="l00201"></a>00201
<a name="l00202"></a>00202 <span class="keywordtype">bool</span> c;
<a name="l00203"></a>00203 <span class="keywordflow">switch</span> (et) {
<a name="l00204"></a>00204 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0809d3f67b151bc1e002a78de682fc1c8b" title="&amp; = AND ">T_AND</a>: c = a & b; <span class="keywordflow">break</span>;
<a name="l00205"></a>00205 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ee13d53546c9358e6b15a455f1c81fb6" title="| = OR ">T_OR</a>: c = a | b; <span class="keywordflow">break</span>;
<a name="l00206"></a>00206 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0839cfc5f9514bb57aa46ffa6ea56a1cc7" title="^ = XOR ">T_XOR</a>: c = a ^ b; <span class="keywordflow">break</span>;
<a name="l00207"></a>00207 <span class="keywordflow">default</span>:
<a name="l00208"></a>00208 {
<a name="l00209"></a>00209 std::ostringstream stream;
<a name="l00210"></a>00210 stream << <span class="stringliteral">"CmdBinary::execute(): unknown token: "</span> << et;
<a name="l00211"></a>00211 <span class="keywordflow">throw</span> <a class="code" href="classFastSatSolver_1_1GenericException.html" title="Common-usage exception containing error message inside.">GenericException</a>(stream.str());
<a name="l00212"></a>00212 }
<a name="l00213"></a>00213 }
<a name="l00214"></a>00214 stack->push(c);
<a name="l00215"></a>00215 }
<a name="l00216"></a>00216 <span class="keyword">private</span>:
<a name="l00217"></a>00217 <a class="code" href="group__SatProblem.html#g9093554967c90043b2a4a74c028f3f08" title="Scanner tokens enumeration.">EToken</a> et;
<a name="l00218"></a>00218 };
<a name="l00219"></a><a class="code" href="classFastSatSolver_1_1Cmd.html#1588352becd13ca8d6fdf0e89f659187">00219</a> <a class="code" href="classFastSatSolver_1_1Cmd.html">Cmd</a>* <a class="code" href="classFastSatSolver_1_1Cmd.html#1588352becd13ca8d6fdf0e89f659187">Cmd::fromToken</a>(<a class="code" href="structFastSatSolver_1_1Token.html" title="Syntax unit representation - also called token.">Token</a> token) {
<a name="l00220"></a>00220 <span class="keywordflow">switch</span> (token.<a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a>) {
<a name="l00221"></a>00221 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08d04c6fedfc6e82b9cd961d926579f541" title="0 = FALSE ">T_FALSE</a>: <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classFastSatSolver_1_1CmdConstant.html">CmdConstant</a>(<span class="keyword">false</span>);
<a name="l00222"></a>00222 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0866901c4f0f0cf6cd9002834b1f8f2075" title="1 = TRUE ">T_TRUE</a>: <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classFastSatSolver_1_1CmdConstant.html">CmdConstant</a>(<span class="keyword">true</span>);
<a name="l00223"></a>00223 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ed5262e7be4aa45d3018726fdba828e6" title="managed variable">T_VARIABLE</a>: <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classFastSatSolver_1_1CmdVariable.html">CmdVariable</a>(token.<a class="code" href="structFastSatSolver_1_1Token.html#c3f3512920573101c3e5f47ee86fc713" title="Extra number carried with token.">m_ext_number</a>);
<a name="l00224"></a>00224 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0836d22df926b610573f0870bcb5c896f4" title="~ = NOT ">T_NOT</a>: <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classFastSatSolver_1_1CmdUnaryNot.html">CmdUnaryNot</a>;
<a name="l00225"></a>00225 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0809d3f67b151bc1e002a78de682fc1c8b" title="&amp; = AND ">T_AND</a>:
<a name="l00226"></a>00226 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ee13d53546c9358e6b15a455f1c81fb6" title="| = OR ">T_OR</a>:
<a name="l00227"></a>00227 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0839cfc5f9514bb57aa46ffa6ea56a1cc7" title="^ = XOR ">T_XOR</a>:
<a name="l00228"></a>00228 <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classFastSatSolver_1_1CmdBinary.html">CmdBinary</a>(token.<a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a>);
<a name="l00229"></a>00229 <span class="keywordflow">default</span>:
<a name="l00230"></a>00230 {
<a name="l00231"></a>00231 std::ostringstream stream;
<a name="l00232"></a>00232 stream << <span class="stringliteral">"Cmd::fromToken(): unknown token: "</span> << token;
<a name="l00233"></a>00233 <span class="keywordflow">throw</span> <a class="code" href="classFastSatSolver_1_1GenericException.html" title="Common-usage exception containing error message inside.">GenericException</a>(stream.str());
<a name="l00234"></a>00234 }
<a name="l00235"></a>00235 }
<a name="l00236"></a>00236 }
<a name="l00237"></a><a class="code" href="classFastSatSolver_1_1CmdList.html">00237</a> <span class="keyword">class </span><a class="code" href="classFastSatSolver_1_1CmdList.html">CmdList</a>: <span class="keyword">public</span> <a class="code" href="classFastSatSolver_1_1Cmd.html">Cmd</a> {
<a name="l00238"></a>00238 <span class="keyword">public</span>:
<a name="l00239"></a><a class="code" href="classFastSatSolver_1_1CmdList.html#a8e3ec6eb7c5514e45f0b32ab27ab670">00239</a> <span class="keyword">virtual</span> ~<a class="code" href="classFastSatSolver_1_1CmdList.html">CmdList</a>() {
<a name="l00240"></a>00240 TContainer::iterator iter;
<a name="l00241"></a>00241 <span class="keywordflow">for</span>(iter=container_.begin(); iter!=container_.end(); iter++)
<a name="l00242"></a>00242 <span class="keyword">delete</span> *iter;
<a name="l00243"></a>00243 }
<a name="l00244"></a><a class="code" href="classFastSatSolver_1_1CmdList.html#fdae54d91f3afa272d6260f16b99f0c6">00244</a> <span class="keyword">virtual</span> <span class="keywordtype">void</span> execute(<a class="code" href="namespaceFastSatSolver.html#3283c5d2be8501320d2e0b9bb810d24f">TRuntimeStack</a> *stack, <a class="code" href="classFastSatSolver_1_1ISatItem.html" title="Abstraction of solution candidate.">ISatItem</a> *data) {
<a name="l00245"></a>00245 TContainer::iterator iter;
<a name="l00246"></a>00246 <span class="keywordflow">for</span>(iter=container_.begin(); iter!=container_.end(); iter++) {
<a name="l00247"></a>00247 <a class="code" href="classFastSatSolver_1_1Cmd.html">Cmd</a> *cmd = *iter;
<a name="l00248"></a>00248 cmd-><a class="code" href="classFastSatSolver_1_1Cmd.html#ba38bc9dd22a41193bcfe1670d539009">execute</a>(stack, data);
<a name="l00249"></a>00249 }
<a name="l00250"></a>00250 }
<a name="l00251"></a><a class="code" href="classFastSatSolver_1_1CmdList.html#78056d4fa6e7eef828f7c12778a00684">00251</a> <span class="keywordtype">void</span> <a class="code" href="namespaceFastSatSolver.html#ced98a0a0b6f548d61444222aaecf7a2">operator<< </a>(<a class="code" href="classFastSatSolver_1_1Cmd.html">Cmd</a> *cmd) {
<a name="l00252"></a>00252 container_.push_back(cmd);
<a name="l00253"></a>00253 }
<a name="l00254"></a><a class="code" href="classFastSatSolver_1_1CmdList.html#cea7372d12ae6ea9b888d6bca358e74f">00254</a> <span class="keywordtype">void</span> <a class="code" href="namespaceFastSatSolver.html#ced98a0a0b6f548d61444222aaecf7a2">operator<< </a>(<span class="keyword">const</span> <a class="code" href="structFastSatSolver_1_1Token.html" title="Syntax unit representation - also called token.">Token</a> &token) {
<a name="l00255"></a>00255 <a class="code" href="namespaceFastSatSolver.html#ced98a0a0b6f548d61444222aaecf7a2">operator<< </a>(Cmd::fromToken(token));
<a name="l00256"></a>00256 }
<a name="l00257"></a>00257 <span class="keyword">private</span>:
<a name="l00258"></a>00258 <span class="keyword">typedef</span> std::list<Cmd *> TContainer;
<a name="l00259"></a>00259 TContainer container_;
<a name="l00260"></a>00260 };
<a name="l00261"></a>00261
<a name="l00262"></a><a class="code" href="structFastSatSolver_1_1InterpretedFormula_1_1Private.html">00262</a> <span class="keyword">struct </span><a class="code" href="structFastSatSolver_1_1InterpretedFormula_1_1Private.html">InterpretedFormula::Private</a> {
<a name="l00263"></a><a class="code" href="structFastSatSolver_1_1InterpretedFormula_1_1Private.html#6229a375c79845911c8f3b2528fe1b3b">00263</a> <a class="code" href="classFastSatSolver_1_1ParserStack.html">ParserStack</a> parserStack;
<a name="l00264"></a><a class="code" href="structFastSatSolver_1_1InterpretedFormula_1_1Private.html#6264162be4152935f6b927826dca6762">00264</a> <span class="keywordtype">bool</span> errorDetected;
<a name="l00265"></a><a class="code" href="structFastSatSolver_1_1InterpretedFormula_1_1Private.html#18652f23c412c1af6c65c15c40a26de6">00265</a> <a class="code" href="classFastSatSolver_1_1CmdList.html">CmdList</a> cmdList;
<a name="l00266"></a>00266 };
<a name="l00267"></a>00267
<a name="l00268"></a><a class="code" href="classFastSatSolver_1_1InterpretedFormula.html#70391c3b7bda85402f81df606bc00ca4">00268</a> InterpretedFormula::InterpretedFormula():
<a name="l00269"></a>00269 d(new <a class="code" href="structFastSatSolver_1_1InterpretedFormula_1_1Private.html">Private</a>)
<a name="l00270"></a>00270 {
<a name="l00271"></a>00271 d-><a class="code" href="structFastSatSolver_1_1InterpretedFormula_1_1Private.html#6229a375c79845911c8f3b2528fe1b3b">parserStack</a>.<a class="code" href="classFastSatSolver_1_1ParserStack.html#3f7874f293605da18e594ec788f2e04c">push</a>(<a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f085a46ce2527667b882c7cb58ba5062e2a" title="bottom of parser stack (behaves as terminal)">T_STACK_BOTTOM</a>);
<a name="l00272"></a>00272 d-><a class="code" href="structFastSatSolver_1_1InterpretedFormula_1_1Private.html#6264162be4152935f6b927826dca6762">errorDetected</a> = <span class="keyword">false</span>;
<a name="l00273"></a>00273 }
<a name="l00274"></a>00274
<a name="l00275"></a><a class="code" href="classFastSatSolver_1_1InterpretedFormula.html#51cbf88d9b86742b97ce8988039cd458">00275</a> <a class="code" href="classFastSatSolver_1_1InterpretedFormula.html#51cbf88d9b86742b97ce8988039cd458">InterpretedFormula::~InterpretedFormula</a>() {
<a name="l00276"></a>00276 <span class="keyword">delete</span> d;
<a name="l00277"></a>00277 }
<a name="l00278"></a>00278
<a name="l00282"></a><a class="code" href="classFastSatSolver_1_1InterpretedFormula.html#3f098aa4027d962d5b9c58d6ea8b2a9b">00282</a> <span class="keywordtype">int</span> <a class="code" href="classFastSatSolver_1_1InterpretedFormula.html#3f098aa4027d962d5b9c58d6ea8b2a9b" title="Parse given token. Token to parse Returns zero, if no fatal error occurs. Parase...">InterpretedFormula::parse</a> (<a class="code" href="structFastSatSolver_1_1Token.html" title="Syntax unit representation - also called token.">Token</a> token ) {
<a name="l00283"></a>00283 <a class="code" href="classFastSatSolver_1_1ParserStack.html">ParserStack</a> &stack = d-><a class="code" href="structFastSatSolver_1_1InterpretedFormula_1_1Private.html#6229a375c79845911c8f3b2528fe1b3b">parserStack</a>;
<a name="l00284"></a>00284 <a class="code" href="group__SatProblem.html#g9093554967c90043b2a4a74c028f3f08" title="Scanner tokens enumeration.">EToken</a> mode;
<a name="l00285"></a>00285 <span class="keywordflow">do</span> {
<a name="l00286"></a>00286 <a class="code" href="structFastSatSolver_1_1Token.html" title="Syntax unit representation - also called token.">Token</a> topTerm = stack.<a class="code" href="classFastSatSolver_1_1ParserStack.html#17b77b7c79888263bd2c2a98e5093c36">topTerm</a>();
<a name="l00287"></a>00287 mode = <a class="code" href="namespaceFastSatSolver.html#dbd4b0d41cba5d4e22426cf58ecbd05c">tableLookup</a>(topTerm.<a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a>, token.<a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a>);
<a name="l00288"></a>00288 <span class="keywordflow">switch</span> (mode) {
<a name="l00289"></a>00289 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0807b73798f72d658ca655a549447b47d6" title="control &lt; ">T_PARSER_LT</a>:
<a name="l00290"></a>00290 <span class="comment">// Insert '<' after last terminal</span>
<a name="l00291"></a>00291 stack.<a class="code" href="classFastSatSolver_1_1ParserStack.html#d255a481013734591759fed43b2d4dd5">insertLt</a>();
<a name="l00292"></a>00292 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f086198c3be29647549fdb9e8a6da818acd" title="control = ">T_PARSER_EQ</a>:
<a name="l00293"></a>00293 <span class="comment">// Insert token to stack</span>
<a name="l00294"></a>00294 stack.<a class="code" href="classFastSatSolver_1_1ParserStack.html#3f7874f293605da18e594ec788f2e04c">push</a>(token);
<a name="l00295"></a>00295 <span class="keywordflow">break</span>;
<a name="l00296"></a>00296
<a name="l00297"></a>00297 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08c53e9b3c78892af3eabea36deee730a8" title="control &gt; ">T_PARSER_GT</a>:
<a name="l00298"></a>00298 <span class="comment">// Reduction</span>
<a name="l00299"></a>00299
<a name="l00300"></a>00300 <span class="keywordflow">switch</span> (topTerm.<a class="code" href="structFastSatSolver_1_1Token.html#c9e3e1f005a3b8c9f5a7b0b1bef9b78a" title="token enumeration">m_token</a>) {
<a name="l00301"></a>00301 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08d04c6fedfc6e82b9cd961d926579f541" title="0 = FALSE ">T_FALSE</a>:
<a name="l00302"></a>00302 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0866901c4f0f0cf6cd9002834b1f8f2075" title="1 = TRUE ">T_TRUE</a>:
<a name="l00303"></a>00303 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ed5262e7be4aa45d3018726fdba828e6" title="managed variable">T_VARIABLE</a>:
<a name="l00304"></a>00304 {
<a name="l00305"></a>00305 <span class="comment">// Operand reduction</span>
<a name="l00306"></a>00306 <a class="code" href="structFastSatSolver_1_1Token.html" title="Syntax unit representation - also called token.">Token</a> opToken = stack.<a class="code" href="classFastSatSolver_1_1ParserStack.html#dabcc89ce1a26243aa760d2340caf2ce">pop</a>();
<a name="l00307"></a>00307 <span class="keywordflow">if</span> (!stack.<a class="code" href="classFastSatSolver_1_1ParserStack.html#a956625529b5f3ba0ae69f37730b2da9">popAndCompare</a>(<a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0807b73798f72d658ca655a549447b47d6" title="control &lt; ">T_PARSER_LT</a>)) {
<a name="l00308"></a>00308 <span class="comment">// Invalid expression</span>
<a name="l00309"></a>00309 d-><a class="code" href="structFastSatSolver_1_1InterpretedFormula_1_1Private.html#6264162be4152935f6b927826dca6762">errorDetected</a> = <span class="keyword">true</span>;
<a name="l00310"></a>00310 <span class="keywordflow">return</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ae35a8e0b44afb4174d0357d55484ff1">T_ERR_EXPR</a>;
<a name="l00311"></a>00311 }
<a name="l00312"></a>00312
<a name="l00313"></a>00313 <span class="comment">// Handle operand</span>
<a name="l00314"></a>00314 d-><a class="code" href="structFastSatSolver_1_1InterpretedFormula_1_1Private.html#18652f23c412c1af6c65c15c40a26de6">cmdList</a> << opToken;
<a name="l00315"></a>00315 <span class="comment">//std::cerr << "<<< Execute command: " << opToken << std::endl;</span>
<a name="l00316"></a>00316 }
<a name="l00317"></a>00317 <span class="keywordflow">break</span>;
<a name="l00318"></a>00318
<a name="l00319"></a>00319 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0873ae5e7e19b86c649347b3fc95e448f9" title=")">T_RPAR</a>:
<a name="l00320"></a>00320 <span class="comment">// Parthesis reduction</span>
<a name="l00321"></a>00321 stack.<a class="code" href="classFastSatSolver_1_1ParserStack.html#dabcc89ce1a26243aa760d2340caf2ce">pop</a>();
<a name="l00322"></a>00322 <span class="keywordflow">if</span> (
<a name="l00323"></a>00323 !stack.<a class="code" href="classFastSatSolver_1_1ParserStack.html#a956625529b5f3ba0ae69f37730b2da9">popAndCompare</a>(<a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ec24fb692561834cef7a9475281a778b" title="expression (recursively)">T_PARSER_EXPR</a>) ||
<a name="l00324"></a>00324 !stack.<a class="code" href="classFastSatSolver_1_1ParserStack.html#a956625529b5f3ba0ae69f37730b2da9">popAndCompare</a>(<a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f084f1a38203f5130575e81ba913c563c6d" title="(">T_LPAR</a>) ||
<a name="l00325"></a>00325 !stack.<a class="code" href="classFastSatSolver_1_1ParserStack.html#a956625529b5f3ba0ae69f37730b2da9">popAndCompare</a>(<a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0807b73798f72d658ca655a549447b47d6" title="control &lt; ">T_PARSER_LT</a>)
<a name="l00326"></a>00326 )
<a name="l00327"></a>00327 {
<a name="l00328"></a>00328 <span class="comment">// Error in parenthesis</span>
<a name="l00329"></a>00329 d-><a class="code" href="structFastSatSolver_1_1InterpretedFormula_1_1Private.html#6264162be4152935f6b927826dca6762">errorDetected</a> = <span class="keyword">true</span>;
<a name="l00330"></a>00330 <span class="keywordflow">return</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ae35a8e0b44afb4174d0357d55484ff1">T_ERR_EXPR</a>;
<a name="l00331"></a>00331 }
<a name="l00332"></a>00332 <span class="preprocessor">#if 0//ndef NDEBUG</span>
<a name="l00333"></a>00333 <span class="preprocessor"></span> std::cerr << <span class="stringliteral">"Droping brackets..."</span> << std::endl;
<a name="l00334"></a>00334 <span class="preprocessor">#endif // NDEBUG</span>
<a name="l00335"></a>00335 <span class="preprocessor"></span> <span class="keywordflow">break</span>;
<a name="l00336"></a>00336
<a name="l00337"></a>00337 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0836d22df926b610573f0870bcb5c896f4" title="~ = NOT ">T_NOT</a>:
<a name="l00338"></a>00338 {
<a name="l00339"></a>00339 <span class="comment">// Unary operator NOT</span>
<a name="l00340"></a>00340 <span class="keywordflow">if</span> (!stack.<a class="code" href="classFastSatSolver_1_1ParserStack.html#a956625529b5f3ba0ae69f37730b2da9">popAndCompare</a>(<a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ec24fb692561834cef7a9475281a778b" title="expression (recursively)">T_PARSER_EXPR</a>)) {
<a name="l00341"></a>00341 <span class="comment">// operand expected</span>
<a name="l00342"></a>00342 d-><a class="code" href="structFastSatSolver_1_1InterpretedFormula_1_1Private.html#6264162be4152935f6b927826dca6762">errorDetected</a> = <span class="keyword">true</span>;
<a name="l00343"></a>00343 <span class="keywordflow">return</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ae35a8e0b44afb4174d0357d55484ff1">T_ERR_EXPR</a>;
<a name="l00344"></a>00344 }
<a name="l00345"></a>00345
<a name="l00346"></a>00346 <a class="code" href="structFastSatSolver_1_1Token.html" title="Syntax unit representation - also called token.">Token</a> t = stack.<a class="code" href="classFastSatSolver_1_1ParserStack.html#dabcc89ce1a26243aa760d2340caf2ce">pop</a>();
<a name="l00347"></a>00347 <span class="comment">// Handle token</span>
<a name="l00348"></a>00348 d-><a class="code" href="structFastSatSolver_1_1InterpretedFormula_1_1Private.html#18652f23c412c1af6c65c15c40a26de6">cmdList</a> << t;
<a name="l00349"></a>00349 <span class="comment">//std::cerr << "<<< Execute command: " << t << std::endl;</span>
<a name="l00350"></a>00350
<a name="l00351"></a>00351 <span class="keywordflow">if</span> (!stack.<a class="code" href="classFastSatSolver_1_1ParserStack.html#a956625529b5f3ba0ae69f37730b2da9">popAndCompare</a>(<a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0807b73798f72d658ca655a549447b47d6" title="control &lt; ">T_PARSER_LT</a>)) {
<a name="l00352"></a>00352 <span class="comment">// invalid expression</span>
<a name="l00353"></a>00353 d-><a class="code" href="structFastSatSolver_1_1InterpretedFormula_1_1Private.html#6264162be4152935f6b927826dca6762">errorDetected</a> = <span class="keyword">true</span>;
<a name="l00354"></a>00354 <span class="keywordflow">return</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ae35a8e0b44afb4174d0357d55484ff1">T_ERR_EXPR</a>;
<a name="l00355"></a>00355 }
<a name="l00356"></a>00356 }
<a name="l00357"></a>00357 <span class="keywordflow">break</span>;
<a name="l00358"></a>00358
<a name="l00359"></a>00359 <span class="keywordflow">default</span>:
<a name="l00360"></a>00360 {
<a name="l00361"></a>00361 <span class="comment">// Binary operator</span>
<a name="l00362"></a>00362 <span class="keywordflow">if</span> (!stack.<a class="code" href="classFastSatSolver_1_1ParserStack.html#a956625529b5f3ba0ae69f37730b2da9">popAndCompare</a>(<a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ec24fb692561834cef7a9475281a778b" title="expression (recursively)">T_PARSER_EXPR</a>)) {
<a name="l00363"></a>00363 <span class="comment">// operand expected</span>
<a name="l00364"></a>00364 d-><a class="code" href="structFastSatSolver_1_1InterpretedFormula_1_1Private.html#6264162be4152935f6b927826dca6762">errorDetected</a> = <span class="keyword">true</span>;
<a name="l00365"></a>00365 <span class="keywordflow">return</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ae35a8e0b44afb4174d0357d55484ff1">T_ERR_EXPR</a>;
<a name="l00366"></a>00366 }
<a name="l00367"></a>00367
<a name="l00368"></a>00368 <a class="code" href="structFastSatSolver_1_1Token.html" title="Syntax unit representation - also called token.">Token</a> t = stack.<a class="code" href="classFastSatSolver_1_1ParserStack.html#dabcc89ce1a26243aa760d2340caf2ce">pop</a>();
<a name="l00369"></a>00369 <span class="comment">// Handle token</span>
<a name="l00370"></a>00370 d-><a class="code" href="structFastSatSolver_1_1InterpretedFormula_1_1Private.html#18652f23c412c1af6c65c15c40a26de6">cmdList</a> << t;
<a name="l00371"></a>00371 <span class="comment">//std::cerr << "<<< Execute command: " << t << std::endl;</span>
<a name="l00372"></a>00372
<a name="l00373"></a>00373 <span class="keywordflow">if</span> (!stack.<a class="code" href="classFastSatSolver_1_1ParserStack.html#a956625529b5f3ba0ae69f37730b2da9">popAndCompare</a>(<a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ec24fb692561834cef7a9475281a778b" title="expression (recursively)">T_PARSER_EXPR</a>)) {
<a name="l00374"></a>00374 <span class="comment">// operand expected</span>
<a name="l00375"></a>00375 d-><a class="code" href="structFastSatSolver_1_1InterpretedFormula_1_1Private.html#6264162be4152935f6b927826dca6762">errorDetected</a> = <span class="keyword">true</span>;
<a name="l00376"></a>00376 <span class="keywordflow">return</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ae35a8e0b44afb4174d0357d55484ff1">T_ERR_EXPR</a>;
<a name="l00377"></a>00377 }
<a name="l00378"></a>00378
<a name="l00379"></a>00379 <span class="keywordflow">if</span> (!stack.<a class="code" href="classFastSatSolver_1_1ParserStack.html#a956625529b5f3ba0ae69f37730b2da9">popAndCompare</a>(<a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0807b73798f72d658ca655a549447b47d6" title="control &lt; ">T_PARSER_LT</a>)) {
<a name="l00380"></a>00380 <span class="comment">// invalid expression</span>
<a name="l00381"></a>00381 d-><a class="code" href="structFastSatSolver_1_1InterpretedFormula_1_1Private.html#6264162be4152935f6b927826dca6762">errorDetected</a> = <span class="keyword">true</span>;
<a name="l00382"></a>00382 <span class="keywordflow">return</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ae35a8e0b44afb4174d0357d55484ff1">T_ERR_EXPR</a>;
<a name="l00383"></a>00383 }
<a name="l00384"></a>00384 }
<a name="l00385"></a>00385 }
<a name="l00386"></a>00386 stack.<a class="code" href="classFastSatSolver_1_1ParserStack.html#3f7874f293605da18e594ec788f2e04c">push</a>(<a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ec24fb692561834cef7a9475281a778b" title="expression (recursively)">T_PARSER_EXPR</a>);
<a name="l00387"></a>00387 <span class="keywordflow">break</span>;
<a name="l00388"></a>00388
<a name="l00389"></a>00389 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f089882ff017eb83e311ec8ad12ab646455" title="end of input">T_EOF</a>:
<a name="l00390"></a>00390 <span class="comment">// End of expression</span>
<a name="l00391"></a>00391 d-><a class="code" href="structFastSatSolver_1_1InterpretedFormula_1_1Private.html#6264162be4152935f6b927826dca6762">errorDetected</a> = !(this-><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="l00392"></a>00392 <span class="keywordflow">if</span> (d-><a class="code" href="structFastSatSolver_1_1InterpretedFormula_1_1Private.html#6264162be4152935f6b927826dca6762">errorDetected</a>)
<a name="l00393"></a>00393 <span class="keywordflow">return</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ae35a8e0b44afb4174d0357d55484ff1">T_ERR_EXPR</a>;
<a name="l00394"></a>00394 <span class="keywordflow">else</span>
<a name="l00395"></a>00395 <span class="keywordflow">return</span> 0;
<a name="l00396"></a>00396
<a name="l00397"></a>00397 <span class="keywordflow">case</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f084a234c50a27b7ab40334ab8d52b6b67f" title="invalid sequence">T_PARSER_INV</a>:
<a name="l00398"></a>00398 <span class="comment">// Invalid token sequence</span>
<a name="l00399"></a>00399 d-><a class="code" href="structFastSatSolver_1_1InterpretedFormula_1_1Private.html#6264162be4152935f6b927826dca6762">errorDetected</a> = <span class="keyword">true</span>;
<a name="l00400"></a>00400 <span class="keywordflow">return</span> <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ae35a8e0b44afb4174d0357d55484ff1">T_ERR_EXPR</a>;
<a name="l00401"></a>00401
<a name="l00402"></a>00402 <span class="keywordflow">default</span>:
<a name="l00403"></a>00403 {
<a name="l00404"></a>00404 d-><a class="code" href="structFastSatSolver_1_1InterpretedFormula_1_1Private.html#6264162be4152935f6b927826dca6762">errorDetected</a> = <span class="keyword">true</span>;
<a name="l00405"></a>00405 std::ostringstream stream;
<a name="l00406"></a>00406 stream << <span class="stringliteral">"Unexpected symbol in precedence table: "</span> << mode;
<a name="l00407"></a>00407 <span class="keywordflow">throw</span> <a class="code" href="classFastSatSolver_1_1GenericException.html" title="Common-usage exception containing error message inside.">GenericException</a>(stream.str());
<a name="l00408"></a>00408 }
<a name="l00409"></a>00409 } <span class="comment">// switch</span>
<a name="l00410"></a>00410 } <span class="keywordflow">while</span> (<a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08c53e9b3c78892af3eabea36deee730a8" title="control &gt; ">T_PARSER_GT</a> == mode);
<a name="l00411"></a>00411 <span class="comment">// TODO</span>
<a name="l00412"></a>00412 <span class="keywordflow">return</span> 0;
<a name="l00413"></a>00413 }
<a name="l00414"></a>00414
<a name="l00418"></a><a class="code" href="classFastSatSolver_1_1InterpretedFormula.html#fe93e17ac89cd97917811068ba2af214">00418</a> <span class="keywordtype">bool</span> <a class="code" href="classFastSatSolver_1_1InterpretedFormula.html#fe93e17ac89cd97917811068ba2af214" title="Return true if formula is valid. Invalid formulas should be never evaluated. ">InterpretedFormula::isValid</a> ( ) {
<a name="l00419"></a>00419 <a class="code" href="classFastSatSolver_1_1ParserStack.html">ParserStack</a> &stack = d-><a class="code" href="structFastSatSolver_1_1InterpretedFormula_1_1Private.html#6229a375c79845911c8f3b2528fe1b3b">parserStack</a>;
<a name="l00420"></a>00420 <a class="code" href="structFastSatSolver_1_1Token.html" title="Syntax unit representation - also called token.">Token</a> topTerm = stack.<a class="code" href="classFastSatSolver_1_1ParserStack.html#17b77b7c79888263bd2c2a98e5093c36">topTerm</a>();
<a name="l00421"></a>00421 <a class="code" href="structFastSatSolver_1_1Token.html" title="Syntax unit representation - also called token.">Token</a> top = stack.<a class="code" href="classFastSatSolver_1_1ParserStack.html#f2e6332cb53b0f9e5c0c70fd6b45fde1">top</a>();
<a name="l00422"></a>00422 <span class="preprocessor">#if 0//ndef NDEBUG</span>
<a name="l00423"></a>00423 <span class="preprocessor"></span> std::cerr << <span class="stringliteral">"InterpretedFormula::isValid(): topTerm = "</span> << topTerm;
<a name="l00424"></a>00424 std::cerr << <span class="stringliteral">"InterpretedFormula::isValid(): top = "</span> << top;
<a name="l00425"></a>00425 std::cerr << <span class="stringliteral">"InterpretedFormula::isValid(): errorDetected = "</span> << d-><a class="code" href="structFastSatSolver_1_1InterpretedFormula_1_1Private.html#6264162be4152935f6b927826dca6762">errorDetected</a> << std::endl;
<a name="l00426"></a>00426 std::cerr << std::endl;
<a name="l00427"></a>00427 <span class="preprocessor">#endif // NDEBUG</span>
<a name="l00428"></a>00428 <span class="preprocessor"></span> <span class="keywordflow">return</span>
<a name="l00429"></a>00429 topTerm.m_token == <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f085a46ce2527667b882c7cb58ba5062e2a" title="bottom of parser stack (behaves as terminal)">T_STACK_BOTTOM</a> &&
<a name="l00430"></a>00430 top.m_token == <a class="code" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ec24fb692561834cef7a9475281a778b" title="expression (recursively)">T_PARSER_EXPR</a> &&
<a name="l00431"></a>00431 !(d-><a class="code" href="structFastSatSolver_1_1InterpretedFormula_1_1Private.html#6264162be4152935f6b927826dca6762">errorDetected</a>);
<a name="l00432"></a>00432 }
<a name="l00433"></a>00433
<a name="l00437"></a><a class="code" href="classFastSatSolver_1_1InterpretedFormula.html#5a0dfaf3d1d0ec78d17c0796e9fe6e62">00437</a> <span class="keywordtype">bool</span> <a class="code" href="classFastSatSolver_1_1InterpretedFormula.html#5a0dfaf3d1d0ec78d17c0796e9fe6e62" title="Return true if formula is satisfied for given data. Evaluation data to use for evaluation...">InterpretedFormula::eval</a> (<a class="code" href="classFastSatSolver_1_1ISatItem.html" title="Abstraction of solution candidate.">ISatItem</a> *data) {
<a name="l00438"></a>00438 <span class="keywordflow">if</span> (!this->isValid())
<a name="l00439"></a>00439 <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">"InterpretedFormula::eval(): called for invalid formula"</span>);
<a name="l00440"></a>00440
<a name="l00441"></a>00441 <a class="code" href="namespaceFastSatSolver.html#3283c5d2be8501320d2e0b9bb810d24f">TRuntimeStack</a> stack;
<a name="l00442"></a>00442 d-><a class="code" href="structFastSatSolver_1_1InterpretedFormula_1_1Private.html#18652f23c412c1af6c65c15c40a26de6">cmdList</a>.<a class="code" href="classFastSatSolver_1_1CmdList.html#fdae54d91f3afa272d6260f16b99f0c6">execute</a>(&stack, data);
<a name="l00443"></a>00443
<a name="l00444"></a>00444 <span class="comment">// Check stack size (should be 1)</span>
<a name="l00445"></a>00445 <span class="keyword">const</span> <span class="keywordtype">int</span> stackSize = stack.size();
<a name="l00446"></a>00446 <span class="keywordflow">if</span> (1!=stackSize) {
<a name="l00447"></a>00447 std::ostringstream stream;
<a name="l00448"></a>00448 stream << <span class="stringliteral">"InterpretedFormula::eval(): incorrect stack size after cmdList.execute(): "</span> << stackSize;
<a name="l00449"></a>00449 <span class="keywordflow">throw</span> <a class="code" href="classFastSatSolver_1_1GenericException.html" title="Common-usage exception containing error message inside.">GenericException</a>(stream.str());
<a name="l00450"></a>00450 }
<a name="l00451"></a>00451
<a name="l00452"></a>00452 <span class="keywordflow">return</span> stack.top();
<a name="l00453"></a>00453 }
<a name="l00454"></a>00454
<a name="l00455"></a>00455
<a name="l00456"></a>00456 } <span class="comment">// namespace FastSatSolver</span>
<a name="l00457"></a>00457
</pre></div><hr size="1"><address style="text-align: right;"><small>Generated on Wed Nov 5 22:30:21 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
Formula_8cpp-source.html [Download]