SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
smtrat::parser::IndexedFunctionInstantiator Struct Reference

#include <FunctionInstantiator.h>

Inheritance diagram for smtrat::parser::IndexedFunctionInstantiator:

Public Member Functions

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

Detailed Description

Definition at line 28 of file FunctionInstantiator.h.

Constructor & Destructor Documentation

◆ ~IndexedFunctionInstantiator()

virtual smtrat::parser::IndexedFunctionInstantiator::~IndexedFunctionInstantiator ( )
inlinevirtual

Definition at line 29 of file FunctionInstantiator.h.

Member Function Documentation

◆ convert()

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

Definition at line 31 of file FunctionInstantiator.h.

Here is the caller graph for this function:

◆ operator()()

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

Reimplemented in smtrat::parser::EncodingInstantiator, and smtrat::parser::IndexedBitvectorInstantiator.

Definition at line 35 of file FunctionInstantiator.h.

Here is the call graph for this function:

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