smtrat::parser::Instantiator< V, T > Struct Template Reference

#include <FunctionInstantiator.h>

Inheritance diagram for smtrat::parser::Instantiator< V, T >:

Collaboration diagram for smtrat::parser::Instantiator< V, T >:

Public Member Functions
template<typename Res >
bool	operator() (const Res &)
bool	operator() (carl::Variable v)
template<typename TYPE = T>
std::enable_if< std::is_same< TYPE, Poly >::value, bool >::type	operator() (const Poly &p)
bool	operator() (const FormulaT &f)
template<typename VAR = V>
std::enable_if< std::is_same< VAR, types::BVVariable >::value, bool >::type	operator() (const types::BVVariable &v)
template<typename VAR = V>
std::enable_if< std::is_same< VAR, types::BVVariable >::value, bool >::type	operator() (const types::BVTerm &t)
bool	instantiate (V v, const T &repl, types::TermType &subject)

Protected Attributes
V	var
T	replacement
types::TermType	result

Detailed Description

template<typename V, typename T>
struct smtrat::parser::Instantiator< V, T >

Definition at line 42 of file FunctionInstantiator.h.

Member Function Documentation

instantiate()

template<typename V , typename T >

bool smtrat::parser::Instantiator< V, T >::instantiate ( V  v, const T &  repl, types::TermType &  subject  )

inline

Definition at line 80 of file FunctionInstantiator.h.

Here is the caller graph for this function:

operator()() [1/6]

template<typename V , typename T >

bool smtrat::parser::Instantiator< V, T >::operator() ( carl::Variable  v )

inline

Definition at line 52 of file FunctionInstantiator.h.

operator()() [2/6]

template<typename V , typename T >

bool smtrat::parser::Instantiator< V, T >::operator() ( const FormulaT &  f )

inline

Definition at line 62 of file FunctionInstantiator.h.

Here is the call graph for this function:

operator()() [3/6]

template<typename V , typename T >

template<typename TYPE = T>

std::enable_if<std::is_same<TYPE,Poly>::value, bool>::type smtrat::parser::Instantiator< V, T >::operator() ( const Poly &  p )

inline

Definition at line 58 of file FunctionInstantiator.h.

Here is the call graph for this function:

operator()() [4/6]

template<typename V , typename T >

template<typename Res >

bool smtrat::parser::Instantiator< V, T >::operator() ( const Res &  )

inline

Definition at line 49 of file FunctionInstantiator.h.

operator()() [5/6]

template<typename V , typename T >

template<typename VAR = V>

std::enable_if<std::is_same<VAR,types::BVVariable>::value, bool>::type smtrat::parser::Instantiator< V, T >::operator() ( const types::BVTerm &  t )

inline

Definition at line 74 of file FunctionInstantiator.h.

operator()() [6/6]

template<typename V , typename T >

template<typename VAR = V>

std::enable_if<std::is_same<VAR,types::BVVariable>::value, bool>::type smtrat::parser::Instantiator< V, T >::operator() ( const types::BVVariable &  v )

inline

Definition at line 68 of file FunctionInstantiator.h.

Field Documentation

replacement

template<typename V , typename T >

T smtrat::parser::Instantiator< V, T >::replacement

protected

Definition at line 45 of file FunctionInstantiator.h.

result

template<typename V , typename T >

types::TermType smtrat::parser::Instantiator< V, T >::result

protected

Definition at line 46 of file FunctionInstantiator.h.

var

template<typename V , typename T >

V smtrat::parser::Instantiator< V, T >::var

protected

Definition at line 44 of file FunctionInstantiator.h.

---

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

• cli/parser/theories/FunctionInstantiator.h