TheoryTypes.h File Reference

#include "Common.h"
#include <carl-common/util/mpl_utils.h>
#include <boost/mpl/vector.hpp>
#include <boost/spirit/include/support_unused.hpp>

Include dependency graph for TheoryTypes.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Data Structures
struct	smtrat::parser::FixedWidthConstant< T >
	Represents a constant of a fixed width. More...
struct	smtrat::parser::types::CoreTheory
	Types of the core theory. More...
struct	smtrat::parser::types::ArithmeticTheory
	Types of the arithmetic theory. More...
struct	smtrat::parser::types::BitvectorTheory
	Types of the theory of bitvectors. More...
struct	smtrat::parser::types::UninterpretedTheory
	Types of the theory of equalities and uninterpreted functions. More...

Namespaces
	smtrat
	Class to create the formulas for axioms.
	smtrat::parser
	smtrat::parser::types

Macros
#define	PARSER_ENABLE_ARITHMETIC
#define	PARSER_ENABLE_BITVECTOR
#define	PARSER_ENABLE_UNINTERPRETED
#define	ARITHMETIC(...)   __VA_ARGS__
#define	BITVECTOR(...)   __VA_ARGS__
#define	UNINTERPRETED(...)   __VA_ARGS__

Typedefs
typedef carl::BVTerm	smtrat::parser::types::BVTerm
	Typedef for bitvector term. More...
typedef carl::BVVariable	smtrat::parser::types::BVVariable
typedef carl::BVConstraint	smtrat::parser::types::BVConstraint
	Typedef for bitvector constraint. More...
using	smtrat::parser::types::UTerm = carl::UTerm
typedef carl::mpl_concatenate< CoreTheory::ConstTypes, >::type	smtrat::parser::types::ConstTypes
	List of all types of constants. More...
typedef carl::mpl_variant_of< ConstTypes >::type	smtrat::parser::types::ConstType
	Variant type for all constants. More...
typedef carl::mpl_concatenate< CoreTheory::VariableTypes, >::type	smtrat::parser::types::VariableTypes
	List of all types of variables. More...
typedef carl::mpl_variant_of< VariableTypes >::type	smtrat::parser::types::VariableType
	Variant type for all variables. More...
typedef carl::mpl_concatenate< CoreTheory::ExpressionTypes, >::type	smtrat::parser::types::ExpressionTypes
	List of all types of expressions. More...
typedef carl::mpl_variant_of< ExpressionTypes >::type	smtrat::parser::types::ExpressionType
	Variant type for all expressions. More...
typedef carl::mpl_concatenate< CoreTheory::TermTypes, >::type	smtrat::parser::types::TermTypes
	List of all types of terms. More...
typedef carl::mpl_variant_of< TermTypes >::type	smtrat::parser::types::TermType
	Variant type for all terms. More...
typedef carl::mpl_concatenate< TermTypes, boost::mpl::vector< SExpressionSequence< types::ConstType >, std::string, bool, boost::spirit::unused_type > >::type	smtrat::parser::types::AttributeTypes
	List of all types of attributes. More...
typedef carl::mpl_variant_of< AttributeTypes >::type	smtrat::parser::types::AttributeValue
	Variant type for all attributes. More...

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

Macro Definition Documentation

ARITHMETIC

#define ARITHMETIC

(

...

)

__VA_ARGS__

Definition at line 19 of file TheoryTypes.h.

BITVECTOR

#define BITVECTOR

(

...

)

__VA_ARGS__

Definition at line 24 of file TheoryTypes.h.

PARSER_ENABLE_ARITHMETIC

#define PARSER_ENABLE_ARITHMETIC

Definition at line 10 of file TheoryTypes.h.

PARSER_ENABLE_BITVECTOR

#define PARSER_ENABLE_BITVECTOR

Definition at line 11 of file TheoryTypes.h.

PARSER_ENABLE_UNINTERPRETED

#define PARSER_ENABLE_UNINTERPRETED

Definition at line 12 of file TheoryTypes.h.

UNINTERPRETED

#define UNINTERPRETED

(

...

)

__VA_ARGS__

Definition at line 29 of file TheoryTypes.h.