SAT Problem

---

Detailed Description

Internal SAT Problem representation with necessary tools for reading and working with SAT Problems.

Remarks:

• Interface IFormulaEvaluator - evaulable proposition formula's interface
• Class InterpretedFormula - interpreted proposition formula implementation
• Class SatProblem - facade to this module

Files
file	Formula.h
	Propositional formula representation.
file	SatProblem.h
	SAT Problem representation.
file	Scanner.h
	Extensible lexical scanner used for reading SAT Problem specification.
Classes
class	InterpretedFormula
	Interpreted formula implementation. More...
class	VariableContainer
	Container for variables names. More...
class	FormulaContainer
	Container for evaluable formulas. More...
class	SatProblem
	SAT Problem module's facade. More...
struct	Token
	Syntax unit representation - also called token. 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...
interface	IFormulaBuilder
	Interpreted formula's interface for parser which can read it. More...
interface	IFormulaEvaluator
	Evaluable formula's interface. More...
interface	IScanner
	Extensible lexical scanner's interface. More...
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...

---

Enumeration Type Documentation

enum EToken

Scanner tokens enumeration.

Attention:

Do not change enumeration order - it would break parser functionality

Note:

Parser error notifications can be dramatically extended in future.

Enumerator:

T_VARIABLE	managed variable
T_FALSE	0 = FALSE
T_TRUE	1 = TRUE
T_NOT	~ = NOT
T_AND	& = AND
T_OR	| = OR
T_XOR	^ = XOR
T_LPAR	(
T_RPAR	)
T_DELIM	;
T_EOF	end of input
T_STRING	string red from input (shoud be catched by ScannerStringHandler)
T_STACK_BOTTOM	bottom of parser stack (behaves as terminal)
T_PARSER_EXPR	expression (recursively)
T_PARSER_EQ	control =
T_PARSER_LT	control <
T_PARSER_GT	control >
T_PARSER_INV	invalid sequence
T_ERR_LEX	lexical error
T_ERR_EXPR
T_ERR_PARSE

Definition at line 44 of file Scanner.h.

---