The Theories class combines all implemented theories and provides a single interface to interact with all theories at once. More...

#include <Theories.h>

Collaboration diagram for smtrat::parser::Theories:

[legend]

Data Structures
struct	ConstantAdder
	Helper functor for addConstants() method. More...

struct	SimpleSortAdder
	Helper functor for addSimpleSorts() method. More...

Public Types
typedef boost::mpl::vector< CoreTheory , ArithmeticTheory , BitvectorTheory , UninterpretedTheory , BooleanEncodingTheory * >::type	Modules

Public Member Functions
	Theories (ParserState *state)

	~Theories ()

void	addGlobalFormulas (FormulasT &formulas)

void	declareVariable (const std::string &name, const carl::Sort &sort)

void	declareFunction (const std::string &name, const std::vector< carl::Sort > &args, const carl::Sort &sort)

types::VariableType	declareFunctionArgument (const std::pair< std::string, carl::Sort > &arg)

void	defineFunction (const std::string &name, const std::vector< types::VariableType > &arguments, const carl::Sort &sort, const types::TermType &definition)

types::TermType	resolveSymbol (const Identifier &identifier) const

types::VariableType	resolveVariable (const Identifier &identifier) const

void	pushExpressionScope (std::size_t n)

void	popExpressionScope (std::size_t n)

void	pushScriptScope (std::size_t n)

void	popScriptScope (std::size_t n)

const auto &	annotateTerm (const types::TermType &term, const std::vector< Attribute > &attributes)

void	handleLet (const std::string &symbol, const types::TermType &term)

types::TermType	handleITE (const std::vector< types::TermType > &arguments)

types::TermType	handleDistinct (const std::vector< types::TermType > &arguments)

bool	instantiate (const UserFunctionInstantiator &function, const types::VariableType &var, const types::TermType &repl, types::TermType &subject)

bool	instantiateUserFunction (const UserFunctionInstantiator &function, const std::vector< types::TermType > &arguments, types::TermType &result, TheoryError &errors)

types::TermType	functionCall (const Identifier &identifier, const std::vector< types::TermType > &arguments)

types::TermType	quantifiedTerm (const std::vector< std::pair< std::string, carl::Sort >> &vars, const types::TermType &term, bool universal)

bool	isVariableDeclared (const std::string &name) const

Static Public Member Functions
static void	addConstants (qi::symbols< char, types::ConstType > &constants)
	Collects constants from all theory modules. More...

static void	addSimpleSorts (qi::symbols< char, carl::Sort > &sorts)
	Collects simple sorts from all theory modules. More...

Private Attributes
ParserState *	state

std::map< std::string, AbstractTheory * >	theories

Detailed Description

The Theories class combines all implemented theories and provides a single interface to interact with all theories at once.

Definition at line 28 of file Theories.h.

Member Typedef Documentation

◆ Modules

typedef boost::mpl::vector< CoreTheory* , ArithmeticTheory* , BitvectorTheory* , UninterpretedTheory* , BooleanEncodingTheory* >::type smtrat::parser::Theories::Modules

Definition at line 42 of file Theories.h.

Constructor & Destructor Documentation

◆ Theories()

smtrat::parser::Theories::Theories ( ParserState * state )

inline

Definition at line 45 of file Theories.h.

◆ ~Theories()

smtrat::parser::Theories::~Theories ( )

inline

Definition at line 61 of file Theories.h.

Member Function Documentation

◆ addConstants()

static void smtrat::parser::Theories::addConstants ( qi::symbols< char, types::ConstType > & constants )

inlinestatic

Collects constants from all theory modules.

Definition at line 82 of file Theories.h.

Here is the caller graph for this function:

◆ addGlobalFormulas()

void smtrat::parser::Theories::addGlobalFormulas ( FormulasT & formulas )

inline

Definition at line 103 of file Theories.h.

Here is the caller graph for this function:

◆ addSimpleSorts()

static void smtrat::parser::Theories::addSimpleSorts ( qi::symbols< char, carl::Sort > & sorts )

inlinestatic

Collects simple sorts from all theory modules.

Definition at line 99 of file Theories.h.

Here is the caller graph for this function:

◆ annotateTerm()

const auto& smtrat::parser::Theories::annotateTerm	(	const types::TermType &	term,
		const std::vector< Attribute > &	attributes
	)

inline

Definition at line 213 of file Theories.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ declareFunction()

void smtrat::parser::Theories::declareFunction	(	const std::string &	name,
		const std::vector< carl::Sort > &	args,
		const carl::Sort &	sort
	)

inline

Definition at line 122 of file Theories.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ declareFunctionArgument()

types::VariableType smtrat::parser::Theories::declareFunctionArgument ( const std::pair< std::string, carl::Sort > & arg )

inline

Definition at line 141 of file Theories.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ declareVariable()

void smtrat::parser::Theories::declareVariable	(	const std::string &	name,
		const carl::Sort &	sort
	)

inline

Definition at line 108 of file Theories.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ defineFunction()

void smtrat::parser::Theories::defineFunction	(	const std::string &	name,
		const std::vector< types::VariableType > &	arguments,
		const carl::Sort &	sort,
		const types::TermType &	definition
	)

inline

Todo:: check that definition matches the sort

Definition at line 157 of file Theories.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ functionCall()

types::TermType smtrat::parser::Theories::functionCall	(	const Identifier &	identifier,
		const std::vector< types::TermType > &	arguments
	)

inline

Definition at line 337 of file Theories.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ handleDistinct()

types::TermType smtrat::parser::Theories::handleDistinct ( const std::vector< types::TermType > & arguments )

inline

Definition at line 268 of file Theories.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ handleITE()

types::TermType smtrat::parser::Theories::handleITE ( const std::vector< types::TermType > & arguments )

inline

Definition at line 242 of file Theories.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ handleLet()

void smtrat::parser::Theories::handleLet	(	const std::string &	symbol,
		const types::TermType &	term
	)

inline

Definition at line 237 of file Theories.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ instantiate()

bool smtrat::parser::Theories::instantiate	(	const UserFunctionInstantiator &	function,
		const types::VariableType &	var,
		const types::TermType &	repl,
		types::TermType &	subject
	)

inline

Definition at line 280 of file Theories.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ instantiateUserFunction()

bool smtrat::parser::Theories::instantiateUserFunction	(	const UserFunctionInstantiator &	function,
		const std::vector< types::TermType > &	arguments,
		types::TermType &	result,
		TheoryError &	errors
	)

inline

Definition at line 304 of file Theories.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ isVariableDeclared()

bool smtrat::parser::Theories::isVariableDeclared ( const std::string & name ) const

inline

Definition at line 425 of file Theories.h.

Here is the caller graph for this function:

◆ popExpressionScope()

void smtrat::parser::Theories::popExpressionScope ( std::size_t n )

inline

Definition at line 203 of file Theories.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ popScriptScope()

void smtrat::parser::Theories::popScriptScope ( std::size_t n )

inline

Definition at line 209 of file Theories.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ pushExpressionScope()

void smtrat::parser::Theories::pushExpressionScope ( std::size_t n )

inline

Definition at line 200 of file Theories.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ pushScriptScope()

void smtrat::parser::Theories::pushScriptScope ( std::size_t n )

inline

Definition at line 206 of file Theories.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ quantifiedTerm()

types::TermType smtrat::parser::Theories::quantifiedTerm	(	const std::vector< std::pair< std::string, carl::Sort >> &	vars,
		const types::TermType &	term,
		bool	universal
	)

inline

Definition at line 412 of file Theories.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ resolveSymbol()

types::TermType smtrat::parser::Theories::resolveSymbol ( const Identifier & identifier ) const

inline

Definition at line 174 of file Theories.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ resolveVariable()

types::VariableType smtrat::parser::Theories::resolveVariable ( const Identifier & identifier ) const

inline

Definition at line 190 of file Theories.h.

Here is the call graph for this function:

Field Documentation

◆ state

ParserState* smtrat::parser::Theories::state

private

Definition at line 430 of file Theories.h.

◆ theories

std::map<std::string, AbstractTheory*> smtrat::parser::Theories::theories

private

Definition at line 431 of file Theories.h.

The documentation for this struct was generated from the following file:

cli/parser/theories/Theories.h

Data Structures

Public Types

Public Member Functions

Static Public Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ Modules

Constructor & Destructor Documentation

◆ Theories()

◆ ~Theories()

Member Function Documentation

◆ addConstants()

◆ addGlobalFormulas()

◆ addSimpleSorts()

◆ annotateTerm()

◆ declareFunction()

◆ declareFunctionArgument()

◆ declareVariable()

◆ defineFunction()

◆ functionCall()

◆ handleDistinct()

◆ handleITE()

◆ handleLet()

◆ instantiate()

◆ instantiateUserFunction()

◆ isVariableDeclared()

◆ popExpressionScope()

◆ popScriptScope()

◆ pushExpressionScope()

◆ pushScriptScope()

◆ quantifiedTerm()

◆ resolveSymbol()

◆ resolveVariable()

Field Documentation

◆ state

◆ theories