smtrat::expression Namespace Reference

Namespaces
	simplifier

Data Structures
class	Expression
struct	ITEExpression
struct	QuantifierExpression
struct	UnaryExpression
struct	BinaryExpression
struct	NaryExpression
struct	ExpressionContent
struct	ExpressionTypeChecker
struct	ExpressionConverter
class	ExpressionPool
class	ExpressionVisitor
class	ExpressionModifier

Typedefs
typedef std::vector< Expression >	Expressions

Enumerations
enum	ITEType { ITE }
enum	QuantifierType { EXISTS , FORALL }
enum	UnaryType { NOT }
enum	BinaryType
enum	NaryType { AND , OR , XOR , IFF }

Functions
std::ostream &	operator<< (std::ostream &os, const Expression &expr)
std::ostream &	operator<< (std::ostream &os, const ITEExpression &expr)
std::ostream &	operator<< (std::ostream &os, const QuantifierExpression &expr)
std::ostream &	operator<< (std::ostream &os, const UnaryExpression &expr)
std::ostream &	operator<< (std::ostream &os, const BinaryExpression &expr)
std::ostream &	operator<< (std::ostream &os, const NaryExpression &expr)
std::ostream &	operator<< (std::ostream &os, const ExpressionContent &expr)
std::ostream &	operator<< (std::ostream &os, const ExpressionContent *expr)
std::ostream &	operator<< (std::ostream &os, ITEType)
std::ostream &	operator<< (std::ostream &os, QuantifierType type)
std::ostream &	operator<< (std::ostream &os, UnaryType type)
std::ostream &	operator<< (std::ostream &os, BinaryType type)
std::ostream &	operator<< (std::ostream &os, NaryType type)

Typedef Documentation

Expressions

typedef std::vector<Expression> smtrat::expression::Expressions

Definition at line 21 of file ExpressionTypes.h.

Enumeration Type Documentation

BinaryType

enum smtrat::expression::BinaryType

Definition at line 27 of file ExpressionTypes.h.

ITEType

enum smtrat::expression::ITEType

Enumerator
ITE

Definition at line 24 of file ExpressionTypes.h.

NaryType

enum smtrat::expression::NaryType

Enumerator
AND
OR
XOR
IFF

Definition at line 28 of file ExpressionTypes.h.

QuantifierType

enum smtrat::expression::QuantifierType

Enumerator
EXISTS
FORALL

Definition at line 25 of file ExpressionTypes.h.

UnaryType

enum smtrat::expression::UnaryType

Enumerator
NOT

Definition at line 26 of file ExpressionTypes.h.

Function Documentation

operator<<() [1/13]

std::ostream& smtrat::expression::operator<< ( std::ostream &  os, BinaryType  type  )

inline

Definition at line 45 of file ExpressionTypes.h.

Here is the call graph for this function:

operator<<() [2/13]

std::ostream& smtrat::expression::operator<< ( std::ostream &  os, const BinaryExpression &  expr  )

inline

Definition at line 66 of file ExpressionContent.h.

operator<<() [3/13]

std::ostream & smtrat::expression::operator<<	(	std::ostream &	os,
		const Expression &	expr
	)

operator<<() [4/13]

std::ostream& smtrat::expression::operator<< ( std::ostream &  os, const ExpressionContent &  expr  )

inline

Definition at line 119 of file ExpressionContent.h.

operator<<() [5/13]

std::ostream& smtrat::expression::operator<< ( std::ostream &  os, const ExpressionContent *  expr  )

inline

Definition at line 122 of file ExpressionContent.h.

operator<<() [6/13]

std::ostream& smtrat::expression::operator<< ( std::ostream &  os, const ITEExpression &  expr  )

inline

Definition at line 26 of file ExpressionContent.h.

operator<<() [7/13]

std::ostream& smtrat::expression::operator<< ( std::ostream &  os, const NaryExpression &  expr  )

inline

Definition at line 90 of file ExpressionContent.h.

operator<<() [8/13]

std::ostream& smtrat::expression::operator<< ( std::ostream &  os, const QuantifierExpression &  expr  )

inline

Definition at line 39 of file ExpressionContent.h.

operator<<() [9/13]

std::ostream& smtrat::expression::operator<< ( std::ostream &  os, const UnaryExpression &  expr  )

inline

Definition at line 51 of file ExpressionContent.h.

operator<<() [10/13]

std::ostream& smtrat::expression::operator<< ( std::ostream &  os, ITEType    )

inline

Definition at line 31 of file ExpressionTypes.h.

operator<<() [11/13]

std::ostream& smtrat::expression::operator<< ( std::ostream &  os, NaryType  type  )

inline

Definition at line 49 of file ExpressionTypes.h.

Here is the call graph for this function:

operator<<() [12/13]

std::ostream& smtrat::expression::operator<< ( std::ostream &  os, QuantifierType  type  )

inline

Definition at line 34 of file ExpressionTypes.h.

Here is the call graph for this function:

operator<<() [13/13]

std::ostream& smtrat::expression::operator<< ( std::ostream &  os, UnaryType  type  )

inline

Definition at line 40 of file ExpressionTypes.h.

Here is the call graph for this function: