SMT-RAT
24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
|
#include <FunctionInstantiator.h>
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 |
Definition at line 28 of file FunctionInstantiator.h.
|
inlinevirtual |
Definition at line 29 of file FunctionInstantiator.h.
|
inline |
|
inlinevirtual |
Reimplemented in smtrat::parser::EncodingInstantiator, and smtrat::parser::IndexedBitvectorInstantiator.
Definition at line 35 of file FunctionInstantiator.h.