#include <FunctionInstantiator.h>

Inheritance diagram for smtrat::parser::UserFunctionInstantiator:

Collaboration diagram for smtrat::parser::UserFunctionInstantiator:

[legend]

Public Member Functions
	UserFunctionInstantiator (const std::vector< types::VariableType > &arguments, const carl::Sort &sort, const types::TermType &definition, const std::set< types::VariableType > &auxiliaries)

template<typename T >
bool	convert (const std::vector< types::TermType > &from, std::vector< T > &to) const

template<typename T >
bool	convert (const std::vector< types::TermType > &from, std::vector< T > &to, TheoryError &errors) const

virtual bool	operator() (const std::vector< types::TermType > &, types::TermType &, TheoryError &errors) const

Data Fields
std::vector< types::VariableType >	arguments

carl::Sort	sort

types::TermType	definition

std::set< types::VariableType >	auxiliaries

FormulasT	globalFormulas

Detailed Description

Definition at line 91 of file FunctionInstantiator.h.

Constructor & Destructor Documentation

◆ UserFunctionInstantiator()

smtrat::parser::UserFunctionInstantiator::UserFunctionInstantiator	(	const std::vector< types::VariableType > &	arguments,
		const carl::Sort &	sort,
		const types::TermType &	definition,
		const std::set< types::VariableType > &	auxiliaries
	)

inline

Definition at line 97 of file FunctionInstantiator.h.

Member Function Documentation

◆ convert() [1/2]

template<typename T >

bool smtrat::parser::FunctionInstantiator::convert	(	const std::vector< types::TermType > &	from,
		std::vector< T > &	to
	)		const

inlineinherited

Definition at line 14 of file FunctionInstantiator.h.

Here is the caller graph for this function:

◆ convert() [2/2]

template<typename T >

bool smtrat::parser::FunctionInstantiator::convert	(	const std::vector< types::TermType > &	from,
		std::vector< T > &	to,
		TheoryError &	errors
	)		const

inlineinherited

Definition at line 19 of file FunctionInstantiator.h.

◆ operator()()

virtual bool smtrat::parser::FunctionInstantiator::operator()	(	const std::vector< types::TermType > &	,
		types::TermType &	,
		TheoryError &	errors
	)		const

inlinevirtualinherited

Reimplemented in smtrat::parser::CoreInstantiator, smtrat::parser::BitvectorInstantiator, and smtrat::parser::ToRealInstantiator.

Definition at line 23 of file FunctionInstantiator.h.

Here is the call graph for this function:

Field Documentation

◆ arguments

std::vector<types::VariableType> smtrat::parser::UserFunctionInstantiator::arguments

Definition at line 92 of file FunctionInstantiator.h.

◆ auxiliaries

std::set<types::VariableType> smtrat::parser::UserFunctionInstantiator::auxiliaries

Definition at line 95 of file FunctionInstantiator.h.

◆ definition

types::TermType smtrat::parser::UserFunctionInstantiator::definition

Definition at line 94 of file FunctionInstantiator.h.

◆ globalFormulas

FormulasT smtrat::parser::UserFunctionInstantiator::globalFormulas

Definition at line 96 of file FunctionInstantiator.h.

◆ sort

carl::Sort smtrat::parser::UserFunctionInstantiator::sort

Definition at line 93 of file FunctionInstantiator.h.

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

cli/parser/theories/FunctionInstantiator.h

Public Member Functions

Data Fields