SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Member Functions
smtrat::parser::BitvectorRelationInstantiator< type > Struct Template Reference
Inheritance diagram for smtrat::parser::BitvectorRelationInstantiator< type >:
Inheritance graph
[legend]
Collaboration diagram for smtrat::parser::BitvectorRelationInstantiator< type >:
Collaboration graph
[legend]

Public Member Functions

bool apply (const std::vector< types::BVTerm > &arguments, types::TermType &result, TheoryError &errors) const
 
bool operator() (const std::vector< types::TermType > &arguments, types::TermType &result, TheoryError &errors) const
 
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
 

Detailed Description

template<carl::BVCompareRelation type>
struct smtrat::parser::BitvectorRelationInstantiator< type >

Definition at line 57 of file Bitvector.cpp.

Member Function Documentation

◆ apply()

template<carl::BVCompareRelation type>
bool smtrat::parser::BitvectorRelationInstantiator< type >::apply ( const std::vector< types::BVTerm > &  arguments,
types::TermType &  result,
TheoryError &  errors 
) const
inlinevirtual

Implements smtrat::parser::BitvectorInstantiator.

Definition at line 58 of file Bitvector.cpp.

Here is the call graph for this function:

◆ 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()()

bool smtrat::parser::BitvectorInstantiator::operator() ( const std::vector< types::TermType > &  arguments,
types::TermType &  result,
TheoryError &  errors 
) const
inlinevirtualinherited

Reimplemented from smtrat::parser::FunctionInstantiator.

Definition at line 13 of file Bitvector.cpp.

Here is the call graph for this function:
The documentation for this struct was generated from the following file: