<!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: FastSatSolver Namespace Reference</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 class="current"><a href="namespaces.html"><span>Namespaces</span></a></li>
<li><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div class="tabs">
<ul>
<li><a href="namespaces.html"><span>Namespace List</span></a></li>
<li><a href="namespacemembers.html"><span>Namespace Members</span></a></li>
</ul>
</div>
<h1>FastSatSolver Namespace Reference</h1><hr><a name="_details"></a><h2>Detailed Description</h2>
Namespace encapsulating whole project.
<p>
All public and/or non-public classes and types belongs to this namespace. There can be also some nested namespaces.
<p>
<p>
<table border="0" cellpadding="0" cellspacing="0">
<tr><td></td></tr>
<tr><td colspan="2"><br><h2>Classes</h2></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1LongSatItem.html">LongSatItem</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight"><a class="el" href="classFastSatSolver_1_1ISatItem.html" title="Abstraction of solution candidate.">ISatItem</a> implementation used by <a class="el" href="classFastSatSolver_1_1BlindSatSolver.html" title="Solver using brute force method to solve SAT problem.">BlindSatSolver</a>. <a href="classFastSatSolver_1_1LongSatItem.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1BlindSatSolver.html">BlindSatSolver</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Solver using brute force method to solve SAT problem. <a href="classFastSatSolver_1_1BlindSatSolver.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1ParserStack.html">ParserStack</a></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1Cmd.html">Cmd</a></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1CmdConstant.html">CmdConstant</a></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1CmdVariable.html">CmdVariable</a></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1CmdUnaryNot.html">CmdUnaryNot</a></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1CmdBinary.html">CmdBinary</a></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1CmdList.html">CmdList</a></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">interface </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1IFormulaBuilder.html">IFormulaBuilder</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Interpreted formula's interface for parser which can read it. <a href="classFastSatSolver_1_1IFormulaBuilder.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">interface </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1IFormulaEvaluator.html">IFormulaEvaluator</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Evaluable formula's interface. <a href="classFastSatSolver_1_1IFormulaEvaluator.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1InterpretedFormula.html">InterpretedFormula</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Interpreted formula implementation. <a href="classFastSatSolver_1_1InterpretedFormula.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1GenericException.html">GenericException</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Common-usage exception containing error message inside. <a href="classFastSatSolver_1_1GenericException.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1GaSatItem.html">GaSatItem</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight"><a class="el" href="classFastSatSolver_1_1ISatItem.html" title="Abstraction of solution candidate.">ISatItem</a> implementation used by <a class="el" href="classFastSatSolver_1_1GaSatSolver.html" title="Solver using GAlib library to solve SAT problem.">GaSatSolver</a>. <a href="classFastSatSolver_1_1GaSatItem.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1SatItemGalibAdatper.html">SatItemGalibAdatper</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Leightweight, optimized <a class="el" href="classFastSatSolver_1_1ISatItem.html" title="Abstraction of solution candidate.">ISatItem</a> implementation used by <a class="el" href="classFastSatSolver_1_1GaSatSolver.html" title="Solver using GAlib library to solve SAT problem.">GaSatSolver</a> time-critical parts of code. <a href="classFastSatSolver_1_1SatItemGalibAdatper.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1GaSatSolver.html">GaSatSolver</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Solver using GAlib library to solve SAT problem. <a href="classFastSatSolver_1_1GaSatSolver.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1VariableContainer.html">VariableContainer</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Container for variables names. <a href="classFastSatSolver_1_1VariableContainer.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1FormulaContainer.html">FormulaContainer</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Container for evaluable formulas. <a href="classFastSatSolver_1_1FormulaContainer.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1SatProblem.html">SatProblem</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">SAT Problem module's facade. <a href="classFastSatSolver_1_1SatProblem.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">interface </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1ISatItem.html">ISatItem</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Abstraction of solution candidate. <a href="classFastSatSolver_1_1ISatItem.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">interface </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1IObserver.html">IObserver</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Simple observer's base class. <a href="classFastSatSolver_1_1IObserver.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">interface </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1ISubject.html">ISubject</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Simple observer's subject base class. <a href="classFastSatSolver_1_1ISubject.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1AbstractSubject.html">AbstractSubject</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Simple subject's base class. <a href="classFastSatSolver_1_1AbstractSubject.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">interface </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1IProcess.html">IProcess</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Continous process interface. <a href="classFastSatSolver_1_1IProcess.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1AbstractProcess.html">AbstractProcess</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Base class of simple multi-step process. <a href="classFastSatSolver_1_1AbstractProcess.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">interface </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1IStopWatch.html">IStopWatch</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Interface of time-watchable activity. <a href="classFastSatSolver_1_1IStopWatch.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1AbstractProcessWatched.html">AbstractProcessWatched</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Multi-step process with time-watch extension. <a href="classFastSatSolver_1_1AbstractProcessWatched.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1SatItemVector.html">SatItemVector</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Linear storage container for <a class="el" href="classFastSatSolver_1_1ISatItem.html" title="Abstraction of solution candidate.">ISatItem</a> objects. <a href="classFastSatSolver_1_1SatItemVector.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1SatItemSet.html">SatItemSet</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Associative array for <a class="el" href="classFastSatSolver_1_1ISatItem.html" title="Abstraction of solution candidate.">ISatItem</a> objects. <a href="classFastSatSolver_1_1SatItemSet.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1AbstractSatSolver.html">AbstractSatSolver</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">SAT Solver base class. <a href="classFastSatSolver_1_1AbstractSatSolver.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1TimedStop.html">TimedStop</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Observer which stops process after specified time. <a href="classFastSatSolver_1_1TimedStop.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1ProgressWatch.html">ProgressWatch</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Observer which write out progress percentage when it is changed. <a href="classFastSatSolver_1_1ProgressWatch.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1SolutionsCountStop.html">SolutionsCountStop</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Observer which stop solver after specified count of solutions is found. <a href="classFastSatSolver_1_1SolutionsCountStop.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1FitnessWatch.html">FitnessWatch</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Observer which write out message when maxFitness value is increased. <a href="classFastSatSolver_1_1FitnessWatch.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1ResultsWatch.html">ResultsWatch</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Observer which write out message when solution is found. <a href="classFastSatSolver_1_1ResultsWatch.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">struct </td><td class="memItemRight" valign="bottom"><a class="el" href="structFastSatSolver_1_1Token.html">Token</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Syntax unit representation - also called <b>token</b>. <a href="structFastSatSolver_1_1Token.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">interface </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1IScanner.html">IScanner</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Extensible lexical scanner's interface. <a href="classFastSatSolver_1_1IScanner.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1RawScanner.html">RawScanner</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Low-level scanner parses lexical units from opened file. <a href="classFastSatSolver_1_1RawScanner.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1ScannerStringHandler.html">ScannerStringHandler</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Part of parser handling keywords and variable names. <a href="classFastSatSolver_1_1ScannerStringHandler.html#_details">More...</a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classFastSatSolver_1_1ScannerFormulaHandler.html">ScannerFormulaHandler</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">High-level part of parser handling almost all tokens and building <a class="el" href="classFastSatSolver_1_1InterpretedFormula.html" title="Interpreted formula implementation.">InterpretedFormula</a> objects. <a href="classFastSatSolver_1_1ScannerFormulaHandler.html#_details">More...</a><br></td></tr>
<tr><td colspan="2"><br><h2>Namespaces</h2></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">namespace </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceFastSatSolver_1_1StreamDecorator.html">StreamDecorator</a></td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Sett of common stuff to work with streams. (colored console output, etc.). <br></td></tr>
<p>
<tr><td colspan="2"><br><h2>Typedefs</h2></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">typedef std::stack< bool > </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceFastSatSolver.html#3283c5d2be8501320d2e0b9bb810d24f">TRuntimeStack</a></td></tr>
<tr><td colspan="2"><br><h2>Enumerations</h2></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">enum </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SatProblem.html#g9093554967c90043b2a4a74c028f3f08">EToken</a> { <br>
<a class="el" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ed5262e7be4aa45d3018726fdba828e6">T_VARIABLE</a>,
<a class="el" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08d04c6fedfc6e82b9cd961d926579f541">T_FALSE</a>,
<a class="el" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0866901c4f0f0cf6cd9002834b1f8f2075">T_TRUE</a>,
<a class="el" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0836d22df926b610573f0870bcb5c896f4">T_NOT</a>,
<br>
<a class="el" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0809d3f67b151bc1e002a78de682fc1c8b">T_AND</a>,
<a class="el" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ee13d53546c9358e6b15a455f1c81fb6">T_OR</a>,
<a class="el" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0839cfc5f9514bb57aa46ffa6ea56a1cc7">T_XOR</a>,
<a class="el" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f084f1a38203f5130575e81ba913c563c6d">T_LPAR</a>,
<br>
<a class="el" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0873ae5e7e19b86c649347b3fc95e448f9">T_RPAR</a>,
<a class="el" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f085aa662332b125f31d3083778f48fc5c6">T_DELIM</a>,
<a class="el" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f089882ff017eb83e311ec8ad12ab646455">T_EOF</a>,
<a class="el" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f082b93aac4bda1ecc9cd242c671411c323">T_STRING</a>,
<br>
<a class="el" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f085a46ce2527667b882c7cb58ba5062e2a">T_STACK_BOTTOM</a>,
<a class="el" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ec24fb692561834cef7a9475281a778b">T_PARSER_EXPR</a>,
<a class="el" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f086198c3be29647549fdb9e8a6da818acd">T_PARSER_EQ</a>,
<a class="el" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f0807b73798f72d658ca655a549447b47d6">T_PARSER_LT</a>,
<br>
<a class="el" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08c53e9b3c78892af3eabea36deee730a8">T_PARSER_GT</a>,
<a class="el" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f084a234c50a27b7ab40334ab8d52b6b67f">T_PARSER_INV</a>,
<a class="el" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08080dc4844adc27f572dfd7d4c72038f4">T_ERR_LEX</a> = -1,
<a class="el" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08ae35a8e0b44afb4174d0357d55484ff1">T_ERR_EXPR</a> = -2,
<br>
<a class="el" href="group__SatProblem.html#gg9093554967c90043b2a4a74c028f3f08c76e1e4acf16e5ca401b5d82cbfe1f0f">T_ERR_PARSE</a> = -3
<br>
}</td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Scanner tokens enumeration. <a href="group__SatProblem.html#g9093554967c90043b2a4a74c028f3f08">More...</a><br></td></tr>
<tr><td colspan="2"><br><h2>Functions</h2></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceFastSatSolver.html#c133e51b507357315bd8f3083d0566ce">tableGetIndex</a> (<a class="el" href="group__SatProblem.html#g9093554967c90043b2a4a74c028f3f08">EToken</a> e)</td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top"><a class="el" href="group__SatProblem.html#g9093554967c90043b2a4a74c028f3f08">EToken</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceFastSatSolver.html#dbd4b0d41cba5d4e22426cf58ecbd05c">tableLookup</a> (<a class="el" href="group__SatProblem.html#g9093554967c90043b2a4a74c028f3f08">EToken</a> topTerm, <a class="el" href="group__SatProblem.html#g9093554967c90043b2a4a74c028f3f08">EToken</a> input)</td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceFastSatSolver.html#b217e1ddb2f6d7563346b307ad40b9ff">isTokenTerminal</a> (<a class="el" href="structFastSatSolver_1_1Token.html">Token</a> token)</td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__fssIO.html#g7532fbb551a0335ad6c5964a0b9a0364">printError</a> (std::string szMsg)</td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Common routine for printing errors. <a href="group__fssIO.html#g7532fbb551a0335ad6c5964a0b9a0364"></a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">std::ostream & </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceFastSatSolver.html#ad6095c6b805623148e4d15a5c802486">operator<<</a> (std::ostream &stream, <a class="el" href="group__SatProblem.html#g9093554967c90043b2a4a74c028f3f08">EToken</a> e)</td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">std::ostream & </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceFastSatSolver.html#ced98a0a0b6f548d61444222aaecf7a2">operator<<</a> (std::ostream &stream, <a class="el" href="structFastSatSolver_1_1Token.html">Token</a> token)</td></tr>
<tr><td colspan="2"><br><h2>Variables</h2></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">static const int </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceFastSatSolver.html#da4ebb227211f96616c9e6681a944bc1">TABLE_SIZE</a> = 8</td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Precedence table size (2 dimensional table). <a href="#da4ebb227211f96616c9e6681a944bc1"></a><br></td></tr>
<tr><td class="memItemLeft" nowrap align="right" valign="top">static const <a class="el" href="group__SatProblem.html#g9093554967c90043b2a4a74c028f3f08">EToken</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="namespaceFastSatSolver.html#bc8561e3a5409d789692b9a1dc78d653">table</a> [<a class="el" href="namespaceFastSatSolver.html#da4ebb227211f96616c9e6681a944bc1">TABLE_SIZE</a>][<a class="el" href="namespaceFastSatSolver.html#da4ebb227211f96616c9e6681a944bc1">TABLE_SIZE</a>]</td></tr>
<tr><td class="mdescLeft"> </td><td class="mdescRight">Precedence table. <a href="#bc8561e3a5409d789692b9a1dc78d653"></a><br></td></tr>
</table>
<hr><h2>Typedef Documentation</h2>
<a class="anchor" name="3283c5d2be8501320d2e0b9bb810d24f"></a><!-- doxytag: member="FastSatSolver::TRuntimeStack" ref="3283c5d2be8501320d2e0b9bb810d24f" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">typedef std::stack<bool> <a class="el" href="namespaceFastSatSolver.html#3283c5d2be8501320d2e0b9bb810d24f">TRuntimeStack</a> </td>
</tr>
</table>
</div>
<div class="memdoc">
<p>
<p>Definition at line <a class="el" href="Formula_8cpp-source.html#l00034">34</a> of file <a class="el" href="Formula_8cpp-source.html">Formula.cpp</a>.</p>
</div>
</div><p>
<hr><h2>Function Documentation</h2>
<a class="anchor" name="b217e1ddb2f6d7563346b307ad40b9ff"></a><!-- doxytag: member="FastSatSolver::isTokenTerminal" ref="b217e1ddb2f6d7563346b307ad40b9ff" args="(Token token)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool FastSatSolver::isTokenTerminal </td>
<td>(</td>
<td class="paramtype">Token </td>
<td class="paramname"> <em>token</em> </td>
<td> ) </td>
<td width="100%"><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>
<p>Definition at line <a class="el" href="Formula_8cpp-source.html#l00098">98</a> of file <a class="el" href="Formula_8cpp-source.html">Formula.cpp</a>.</p>
<p>References <a class="el" href="Scanner_8h-source.html#l00077">Token::m_token</a>, and <a class="el" href="Scanner_8h-source.html#l00059">T_PARSER_EXPR</a>.</p>
<p>Referenced by <a class="el" href="Formula_8cpp-source.html#l00110">ParserStack::insertLt()</a>, and <a class="el" href="Formula_8cpp-source.html#l00137">ParserStack::topTerm()</a>.</p>
</div>
</div><p>
<a class="anchor" name="ced98a0a0b6f548d61444222aaecf7a2"></a><!-- doxytag: member="FastSatSolver::operator<<" ref="ced98a0a0b6f548d61444222aaecf7a2" args="(std::ostream &stream, Token token)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::ostream& FastSatSolver::operator<< </td>
<td>(</td>
<td class="paramtype">std::ostream & </td>
<td class="paramname"> <em>stream</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">Token </td>
<td class="paramname"> <em>token</em></td><td> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td><td width="100%"><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>
<p>Definition at line <a class="el" href="Scanner_8h-source.html#l00124">124</a> of file <a class="el" href="Scanner_8h-source.html">Scanner.h</a>.</p>
<p>References <a class="el" href="Scanner_8h-source.html#l00078">Token::m_ext_number</a>, <a class="el" href="Scanner_8h-source.html#l00079">Token::m_ext_text</a>, <a class="el" href="Scanner_8h-source.html#l00075">Token::m_line</a>, <a class="el" href="Scanner_8h-source.html#l00077">Token::m_token</a>, and <a class="el" href="Scanner_8h-source.html#l00045">T_VARIABLE</a>.</p>
<p>Referenced by <a class="el" href="Formula_8cpp-source.html#l00254">CmdList::operator<<()</a>.</p>
</div>
</div><p>
<a class="anchor" name="ad6095c6b805623148e4d15a5c802486"></a><!-- doxytag: member="FastSatSolver::operator<<" ref="ad6095c6b805623148e4d15a5c802486" args="(std::ostream &stream, EToken e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::ostream& FastSatSolver::operator<< </td>
<td>(</td>
<td class="paramtype">std::ostream & </td>
<td class="paramname"> <em>stream</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">EToken </td>
<td class="paramname"> <em>e</em></td><td> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td><td width="100%"><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>
<p>Definition at line <a class="el" href="Scanner_8h-source.html#l00095">95</a> of file <a class="el" href="Scanner_8h-source.html">Scanner.h</a>.</p>
<p>References <a class="el" href="Scanner_8h-source.html#l00049">T_AND</a>, <a class="el" href="Scanner_8h-source.html#l00054">T_DELIM</a>, <a class="el" href="Scanner_8h-source.html#l00055">T_EOF</a>, <a class="el" href="Scanner_8h-source.html#l00065">T_ERR_EXPR</a>, <a class="el" href="Scanner_8h-source.html#l00064">T_ERR_LEX</a>, <a class="el" href="Scanner_8h-source.html#l00066">T_ERR_PARSE</a>, <a class="el" href="Scanner_8h-source.html#l00046">T_FALSE</a>, <a class="el" href="Scanner_8h-source.html#l00052">T_LPAR</a>, <a class="el" href="Scanner_8h-source.html#l00048">T_NOT</a>, <a class="el" href="Scanner_8h-source.html#l00050">T_OR</a>, <a class="el" href="Scanner_8h-source.html#l00060">T_PARSER_EQ</a>, <a class="el" href="Scanner_8h-source.html#l00059">T_PARSER_EXPR</a>, <a class="el" href="Scanner_8h-source.html#l00062">T_PARSER_GT</a>, <a class="el" href="Scanner_8h-source.html#l00063">T_PARSER_INV</a>, <a class="el" href="Scanner_8h-source.html#l00061">T_PARSER_LT</a>, <a class="el" href="Scanner_8h-source.html#l00053">T_RPAR</a>, <a class="el" href="Scanner_8h-source.html#l00058">T_STACK_BOTTOM</a>, <a class="el" href="Scanner_8h-source.html#l00056">T_STRING</a>, <a class="el" href="Scanner_8h-source.html#l00047">T_TRUE</a>, <a class="el" href="Scanner_8h-source.html#l00045">T_VARIABLE</a>, and <a class="el" href="Scanner_8h-source.html#l00051">T_XOR</a>.</p>
</div>
</div><p>
<a class="anchor" name="c133e51b507357315bd8f3083d0566ce"></a><!-- doxytag: member="FastSatSolver::tableGetIndex" ref="c133e51b507357315bd8f3083d0566ce" args="(EToken e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int FastSatSolver::tableGetIndex </td>
<td>(</td>
<td class="paramtype">EToken </td>
<td class="paramname"> <em>e</em> </td>
<td> ) </td>
<td width="100%"><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>
<p>Definition at line <a class="el" href="Formula_8cpp-source.html#l00057">57</a> of file <a class="el" href="Formula_8cpp-source.html">Formula.cpp</a>.</p>
<p>References <a class="el" href="Scanner_8h-source.html#l00049">T_AND</a>, <a class="el" href="Scanner_8h-source.html#l00054">T_DELIM</a>, <a class="el" href="Scanner_8h-source.html#l00055">T_EOF</a>, <a class="el" href="Scanner_8h-source.html#l00046">T_FALSE</a>, <a class="el" href="Scanner_8h-source.html#l00052">T_LPAR</a>, <a class="el" href="Scanner_8h-source.html#l00048">T_NOT</a>, <a class="el" href="Scanner_8h-source.html#l00050">T_OR</a>, <a class="el" href="Scanner_8h-source.html#l00053">T_RPAR</a>, <a class="el" href="Scanner_8h-source.html#l00058">T_STACK_BOTTOM</a>, <a class="el" href="Scanner_8h-source.html#l00047">T_TRUE</a>, <a class="el" href="Scanner_8h-source.html#l00045">T_VARIABLE</a>, and <a class="el" href="Scanner_8h-source.html#l00051">T_XOR</a>.</p>
<p>Referenced by <a class="el" href="Formula_8cpp-source.html#l00084">tableLookup()</a>.</p>
</div>
</div><p>
<a class="anchor" name="dbd4b0d41cba5d4e22426cf58ecbd05c"></a><!-- doxytag: member="FastSatSolver::tableLookup" ref="dbd4b0d41cba5d4e22426cf58ecbd05c" args="(EToken topTerm, EToken input)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="group__SatProblem.html#g9093554967c90043b2a4a74c028f3f08">EToken</a> FastSatSolver::tableLookup </td>
<td>(</td>
<td class="paramtype">EToken </td>
<td class="paramname"> <em>topTerm</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">EToken </td>
<td class="paramname"> <em>input</em></td><td> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td><td width="100%"><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>
<p>Definition at line <a class="el" href="Formula_8cpp-source.html#l00084">84</a> of file <a class="el" href="Formula_8cpp-source.html">Formula.cpp</a>.</p>
<p>References <a class="el" href="Scanner_8h-source.html#l00063">T_PARSER_INV</a>, <a class="el" href="Formula_8cpp-source.html#l00044">table</a>, and <a class="el" href="Formula_8cpp-source.html#l00057">tableGetIndex()</a>.</p>
<p>Referenced by <a class="el" href="Formula_8cpp-source.html#l00282">InterpretedFormula::parse()</a>.</p>
</div>
</div><p>
<hr><h2>Variable Documentation</h2>
<a class="anchor" name="bc8561e3a5409d789692b9a1dc78d653"></a><!-- doxytag: member="FastSatSolver::table" ref="bc8561e3a5409d789692b9a1dc78d653" args="[TABLE_SIZE][TABLE_SIZE]" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="group__SatProblem.html#g9093554967c90043b2a4a74c028f3f08">EToken</a> <a class="el" href="namespaceFastSatSolver.html#bc8561e3a5409d789692b9a1dc78d653">table</a>[<a class="el" href="namespaceFastSatSolver.html#da4ebb227211f96616c9e6681a944bc1">TABLE_SIZE</a>][<a class="el" href="namespaceFastSatSolver.html#da4ebb227211f96616c9e6681a944bc1">TABLE_SIZE</a>]<code> [static]</code> </td>
</tr>
</table>
</div>
<div class="memdoc">
<p>
<b>Initial value:</b><div class="fragment"><pre class="fragment"> {
{ <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 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 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 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 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 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 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 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>, },
}
</pre></div>Precedence table.
<p>
<p>Definition at line <a class="el" href="Formula_8cpp-source.html#l00044">44</a> of file <a class="el" href="Formula_8cpp-source.html">Formula.cpp</a>.</p>
<p>Referenced by <a class="el" href="Formula_8cpp-source.html#l00084">tableLookup()</a>.</p>
</div>
</div><p>
<a class="anchor" name="da4ebb227211f96616c9e6681a944bc1"></a><!-- doxytag: member="FastSatSolver::TABLE_SIZE" ref="da4ebb227211f96616c9e6681a944bc1" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const int <a class="el" href="namespaceFastSatSolver.html#da4ebb227211f96616c9e6681a944bc1">TABLE_SIZE</a> = 8<code> [static]</code> </td>
</tr>
</table>
</div>
<div class="memdoc">
<p>
Precedence table size (2 dimensional table).
<p>
<p>Definition at line <a class="el" href="Formula_8cpp-source.html#l00039">39</a> of file <a class="el" href="Formula_8cpp-source.html">Formula.cpp</a>.</p>
</div>
</div><p>
<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
namespaceFastSatSolver.html [Download]