smtrat::parser Namespace Reference

Namespaces
	arithmetic
	conversion
	core
	types
	uninterpreted

Data Structures
struct	AttributeValueParser
struct	AttributeParser
struct	Skipper
struct	IdentifierParser
class	OutputWrapper
class	InstructionHandler
struct	RationalPolicies
	Specialization of qi::real_policies for a Rational. More...
struct	NumeralParser
	Parses numerals: (0 | [1-9][0-9]*) More...
struct	DecimalParser
	Parses decimals: numeral.0*numeral More...
struct	HexadecimalParser
	Parses hexadecimals: #x[0-9a-fA-F]+ More...
struct	BinaryParser
	Parses binaries: #b[01]+ More...
struct	StringParser
	Parses strings: ".+" with escape sequences \\" and \\\\ More...
struct	SimpleSymbolParser
	Parses symbols: simple_symbol | quoted_symbol where. More...
struct	SymbolParser
struct	KeywordParser
	Parses keywords: :simple_symbol More...
class	SMTLIBParser
struct	ParserSettings
struct	LogicParser
struct	ErrorHandler
struct	ScriptParser
struct	SpecConstantParser
struct	SExpressionParser
struct	SortParser
struct	QualifiedIdentifierParser
struct	SortedVariableParser
struct	TermParser
struct	AbstractTheory
	Base class for all theories. More...
struct	ToRealInstantiator
struct	ArithmeticTheory
	Implements the theory of arithmetic, including LRA, LIA, NRA and NIA. More...
class	Attribute
	Represents an Attribute. More...
struct	BitvectorInstantiator
struct	IndexedBitvectorInstantiator
struct	UnaryBitvectorInstantiator
struct	BinaryBitvectorInstantiator
struct	BitvectorRelationInstantiator
struct	SingleIndexBitvectorInstantiator
struct	ExtractBitvectorInstantiator
struct	BitvectorConstantParser
struct	BitvectorTheory
	Implements the theory of bitvectors. More...
struct	EncodingInstantiator
struct	AtMostInstantiator
struct	BooleanEncodingTheory
	Implements the theory of bitvectors. More...
struct	TheoryError
struct	Identifier
struct	SExpressionSequence
struct	CoreInstantiator
struct	NaryCoreInstantiator
struct	NotCoreInstantiator
struct	ImpliesCoreInstantiator
struct	CoreTheory
	Implements the core theory of the booleans. More...
struct	FunctionInstantiator
struct	IndexedFunctionInstantiator
struct	Instantiator
struct	UserFunctionInstantiator
struct	ParserState
struct	Theories
	The Theories class combines all implemented theories and provides a single interface to interact with all theories at once. More...
struct	FixedWidthConstant
	Represents a constant of a fixed width. More...
struct	UninterpretedTheory
	Implements the theory of equalities and uninterpreted functions. More...

Typedefs
typedef boost::spirit::istream_iterator	BaseIteratorType
typedef boost::spirit::line_pos_iterator< BaseIteratorType >	PositionIteratorType
typedef PositionIteratorType	Iterator
template<typename T >
using	SExpression = boost::variant< T, boost::recursive_wrapper< SExpressionSequence< T > >>

Enumerations
enum class	OptimizationType { Maximize , Minimize }

Functions
std::ostream &	operator<< (std::ostream &os, OptimizationType ot)
template<typename T >
void	registerParserSettings (T &parser)
std::ostream &	operator<< (std::ostream &os, const Attribute &attr)
void	at_most_k_helper (size_t k, const std::vector< FormulaT > &set, FormulasT &working, long long int prev_idx, FormulasT &results)
FormulaT	at_most_k (size_t k, const std::vector< FormulaT > &set)
std::ostream &	operator<< (std::ostream &os, const Identifier &identifier)
template<typename T >
std::ostream &	operator<< (std::ostream &os, const SExpressionSequence< T > &ses)
template<typename T >
std::ostream &	operator<< (std::ostream &os, const FixedWidthConstant< T > &fwc)

Typedef Documentation

BaseIteratorType

typedef boost::spirit::istream_iterator smtrat::parser::BaseIteratorType

Definition at line 47 of file Common.h.

Iterator

typedef PositionIteratorType smtrat::parser::Iterator

Definition at line 49 of file Common.h.

PositionIteratorType

typedef boost::spirit::line_pos_iterator<BaseIteratorType> smtrat::parser::PositionIteratorType

Definition at line 48 of file Common.h.

SExpression

template<typename T >

using smtrat::parser::SExpression = typedef boost::variant<T, boost::recursive_wrapper<SExpressionSequence<T> >>

Definition at line 79 of file Common.h.

Enumeration Type Documentation

OptimizationType

enum smtrat::parser::OptimizationType

strong

Enumerator
Maximize
Minimize

Definition at line 17 of file InstructionHandler.h.

Function Documentation

at_most_k()

FormulaT smtrat::parser::at_most_k	(	size_t	k,
		const std::vector< FormulaT > &	set
	)

Definition at line 32 of file BooleanEncoding.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

at_most_k_helper()

void smtrat::parser::at_most_k_helper	(	size_t	k,
		const std::vector< FormulaT > &	set,
		FormulasT &	working,
		long long int	prev_idx,
		FormulasT &	results
	)

Definition at line 21 of file BooleanEncoding.cpp.

Here is the caller graph for this function:

operator<<() [1/5]

std::ostream& smtrat::parser::operator<< ( std::ostream &  os, const Attribute &  attr  )

inline

Definition at line 41 of file Attribute.h.

Here is the call graph for this function:

operator<<() [2/5]

template<typename T >

std::ostream& smtrat::parser::operator<< ( std::ostream &  os, const FixedWidthConstant< T > &  fwc  )

inline

Definition at line 48 of file TheoryTypes.h.

operator<<() [3/5]

std::ostream& smtrat::parser::operator<< ( std::ostream &  os, const Identifier &  identifier  )

inline

Definition at line 72 of file Common.h.

operator<<() [4/5]

template<typename T >

std::ostream& smtrat::parser::operator<< ( std::ostream &  os, const SExpressionSequence< T > &  ses  )

inline

Definition at line 86 of file Common.h.

operator<<() [5/5]

std::ostream& smtrat::parser::operator<< ( std::ostream &  os, OptimizationType  ot  )

inline

Definition at line 18 of file InstructionHandler.h.

registerParserSettings()

template<typename T >

void smtrat::parser::registerParserSettings

(

T &

parser

)

Definition at line 18 of file ParserSettings.h.

Here is the caller graph for this function: