FastSatSolver Namespace Reference

---

Detailed Description

Namespace encapsulating whole project.

All public and/or non-public classes and types belongs to this namespace. There can be also some nested namespaces.

Classes
class	LongSatItem
	ISatItem implementation used by BlindSatSolver. More...
class	BlindSatSolver
	Solver using brute force method to solve SAT problem. More...
class	ParserStack
class	Cmd
class	CmdConstant
class	CmdVariable
class	CmdUnaryNot
class	CmdBinary
class	CmdList
interface	IFormulaBuilder
	Interpreted formula's interface for parser which can read it. More...
interface	IFormulaEvaluator
	Evaluable formula's interface. More...
class	InterpretedFormula
	Interpreted formula implementation. More...
class	GenericException
	Common-usage exception containing error message inside. More...
class	GaSatItem
	ISatItem implementation used by GaSatSolver. More...
class	SatItemGalibAdatper
	Leightweight, optimized ISatItem implementation used by GaSatSolver time-critical parts of code. More...
class	GaSatSolver
	Solver using GAlib library to solve SAT problem. More...
class	VariableContainer
	Container for variables names. More...
class	FormulaContainer
	Container for evaluable formulas. More...
class	SatProblem
	SAT Problem module's facade. More...
interface	ISatItem
	Abstraction of solution candidate. More...
interface	IObserver
	Simple observer's base class. More...
interface	ISubject
	Simple observer's subject base class. More...
class	AbstractSubject
	Simple subject's base class. More...
interface	IProcess
	Continous process interface. More...
class	AbstractProcess
	Base class of simple multi-step process. More...
interface	IStopWatch
	Interface of time-watchable activity. More...
class	AbstractProcessWatched
	Multi-step process with time-watch extension. More...
class	SatItemVector
	Linear storage container for ISatItem objects. More...
class	SatItemSet
	Associative array for ISatItem objects. More...
class	AbstractSatSolver
	SAT Solver base class. More...
class	TimedStop
	Observer which stops process after specified time. More...
class	ProgressWatch
	Observer which write out progress percentage when it is changed. More...
class	SolutionsCountStop
	Observer which stop solver after specified count of solutions is found. More...
class	FitnessWatch
	Observer which write out message when maxFitness value is increased. More...
class	ResultsWatch
	Observer which write out message when solution is found. More...
struct	Token
	Syntax unit representation - also called token. More...
interface	IScanner
	Extensible lexical scanner's interface. More...
class	RawScanner
	Low-level scanner parses lexical units from opened file. More...
class	ScannerStringHandler
	Part of parser handling keywords and variable names. More...
class	ScannerFormulaHandler
	High-level part of parser handling almost all tokens and building InterpretedFormula objects. More...
Namespaces
namespace	StreamDecorator
	Sett of common stuff to work with streams. (colored console output, etc.).
Typedefs
typedef std::stack< bool >	TRuntimeStack
Enumerations
enum	EToken {   T_VARIABLE, T_FALSE, T_TRUE, T_NOT,   T_AND, T_OR, T_XOR, T_LPAR,   T_RPAR, T_DELIM, T_EOF, T_STRING,   T_STACK_BOTTOM, T_PARSER_EXPR, T_PARSER_EQ, T_PARSER_LT,   T_PARSER_GT, T_PARSER_INV, T_ERR_LEX = -1, T_ERR_EXPR = -2,   T_ERR_PARSE = -3 }
	Scanner tokens enumeration. More...
Functions
int	tableGetIndex (EToken e)
EToken	tableLookup (EToken topTerm, EToken input)
bool	isTokenTerminal (Token token)
void	printError (std::string szMsg)
	Common routine for printing errors.
std::ostream &	operator<< (std::ostream &stream, EToken e)
std::ostream &	operator<< (std::ostream &stream, Token token)
Variables
static const int	TABLE_SIZE = 8
	Precedence table size (2 dimensional table).
static const EToken	table [TABLE_SIZE][TABLE_SIZE]
	Precedence table.

---

Typedef Documentation

typedef std::stack<bool> TRuntimeStack

Definition at line 34 of file Formula.cpp.

---

Function Documentation

bool FastSatSolver::isTokenTerminal

(

Token

token

)

[inline]

Definition at line 98 of file Formula.cpp.

References Token::m_token, and T_PARSER_EXPR.

Referenced by ParserStack::insertLt(), and ParserStack::topTerm().

std::ostream& FastSatSolver::operator<<	(	std::ostream &	stream,
		Token	token
	)			[inline]

Definition at line 124 of file Scanner.h.

References Token::m_ext_number, Token::m_ext_text, Token::m_line, Token::m_token, and T_VARIABLE.

Referenced by CmdList::operator<<().

std::ostream& FastSatSolver::operator<<	(	std::ostream &	stream,
		EToken	e
	)			[inline]

Definition at line 95 of file Scanner.h.

References T_AND, T_DELIM, T_EOF, T_ERR_EXPR, T_ERR_LEX, T_ERR_PARSE, T_FALSE, T_LPAR, T_NOT, T_OR, T_PARSER_EQ, T_PARSER_EXPR, T_PARSER_GT, T_PARSER_INV, T_PARSER_LT, T_RPAR, T_STACK_BOTTOM, T_STRING, T_TRUE, T_VARIABLE, and T_XOR.

int FastSatSolver::tableGetIndex

(

EToken

e

)

[inline]

Definition at line 57 of file Formula.cpp.

References T_AND, T_DELIM, T_EOF, T_FALSE, T_LPAR, T_NOT, T_OR, T_RPAR, T_STACK_BOTTOM, T_TRUE, T_VARIABLE, and T_XOR.

Referenced by tableLookup().

EToken FastSatSolver::tableLookup	(	EToken	topTerm,
		EToken	input
	)			[inline]

Definition at line 84 of file Formula.cpp.

References T_PARSER_INV, table, and tableGetIndex().

Referenced by InterpretedFormula::parse().

---

Variable Documentation

const EToken table[TABLE_SIZE][TABLE_SIZE] [static]

Initial value:

 {
    
    
     { T_PARSER_GT,  T_PARSER_GT,  T_PARSER_GT,  T_PARSER_LT,  T_PARSER_LT,  T_PARSER_GT,  T_PARSER_LT,  T_PARSER_GT,  },
     { T_PARSER_GT,  T_PARSER_GT,  T_PARSER_GT,  T_PARSER_LT,  T_PARSER_LT,  T_PARSER_GT,  T_PARSER_LT,  T_PARSER_GT,  },
     { T_PARSER_GT,  T_PARSER_GT,  T_PARSER_GT,  T_PARSER_LT,  T_PARSER_LT,  T_PARSER_GT,  T_PARSER_LT,  T_PARSER_GT,  },
     { T_PARSER_GT,  T_PARSER_GT,  T_PARSER_GT,  T_PARSER_LT,  T_PARSER_LT,  T_PARSER_GT,  T_PARSER_LT,  T_PARSER_GT,  },
     { T_PARSER_LT,  T_PARSER_LT,  T_PARSER_LT,  T_PARSER_LT,  T_PARSER_LT,  T_PARSER_EQ,  T_PARSER_LT,  T_PARSER_INV, },
     { T_PARSER_GT,  T_PARSER_GT,  T_PARSER_GT,  T_PARSER_GT,  T_PARSER_INV, T_PARSER_GT,  T_PARSER_INV, T_PARSER_GT,  },
     { T_PARSER_GT,  T_PARSER_GT,  T_PARSER_GT,  T_PARSER_GT,  T_PARSER_INV, T_PARSER_GT,  T_PARSER_INV, T_PARSER_GT,  },
     { T_PARSER_LT,  T_PARSER_LT,  T_PARSER_LT,  T_PARSER_LT,  T_PARSER_LT,  T_PARSER_INV, T_PARSER_LT,  T_EOF,        },
  }

Precedence table.

Definition at line 44 of file Formula.cpp.

Referenced by tableLookup().

const int TABLE_SIZE = 8 [static]

Precedence table size (2 dimensional table).

Definition at line 39 of file Formula.cpp.

---