smtrat::parser::IndexedBitvectorInstantiator Struct Reference

Inheritance diagram for smtrat::parser::IndexedBitvectorInstantiator:

Collaboration diagram for smtrat::parser::IndexedBitvectorInstantiator:

Public Member Functions
bool	operator() (const std::vector< std::size_t > &indices, const std::vector< types::TermType > &arguments, types::TermType &result, TheoryError &errors) const
virtual bool	apply (const std::vector< std::size_t > &indices, const std::vector< types::BVTerm > &arguments, types::TermType &result, TheoryError &errors) const =0
template<typename T >
bool	convert (const std::vector< types::TermType > &from, std::vector< T > &to) const

Detailed Description

Definition at line 23 of file Bitvector.cpp.

Member Function Documentation

apply()

virtual bool smtrat::parser::IndexedBitvectorInstantiator::apply ( const std::vector< std::size_t > &  indices, const std::vector< types::BVTerm > &  arguments, types::TermType &  result, TheoryError &  errors  ) const

pure virtual

Implemented in smtrat::parser::ExtractBitvectorInstantiator, and smtrat::parser::SingleIndexBitvectorInstantiator< type >.

Here is the caller graph for this function:

convert()

template<typename T >

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

inlineinherited

Definition at line 31 of file FunctionInstantiator.h.

Here is the caller graph for this function:

operator()()

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

inlinevirtual

Reimplemented from smtrat::parser::IndexedFunctionInstantiator.

Definition at line 24 of file Bitvector.cpp.

Here is the call graph for this function:

---

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

• cli/parser/theories/Bitvector.cpp