mCRL2
Loading...
Searching...
No Matches
Public Member Functions | Public Attributes | List of all members
mcrl2::smt::native_translations Struct Reference

#include <native_translation.h>

Public Member Functions

 native_translations ()=default
 
std::map< data::function_symbol, native_translation_t >::const_iterator find_native_translation (const data::application &a) const
 
bool has_native_definition (const data::function_symbol &f) const
 
bool has_native_definition (const data::application &a) const
 
bool has_native_definition (const data::data_equation &eq) const
 
bool is_ambiguous (const data::function_symbol &f) const
 
void set_native_definition (const data::function_symbol &f)
 Record that the mapping and equations for f should not be translated.
 
void set_native_definition (const data::function_symbol &f, const data::data_equation &eq)
 
void set_native_definition (const data::function_symbol &f, const std::string &s)
 
void set_alternative_name (const data::function_symbol &f, const std::string &s)
 
void set_ambiguous (const data::function_symbol &f)
 

Public Attributes

std::map< data::function_symbol, std::string > symbols
 
std::map< data::function_symbol, native_translation_t > expressions
 
std::set< data::function_symbol > do_not_define
 
std::map< data::function_symbol, data::data_equation > mappings
 
std::map< data::sort_expression, std::string > sorts
 
std::set< data::function_symbol > ambiguous_symbols
 
std::map< data::function_symbol, std::string > special_recogniser
 

Detailed Description

Definition at line 20 of file native_translation.h.

Constructor & Destructor Documentation

◆ native_translations()

mcrl2::smt::native_translations::native_translations ( )
default

Member Function Documentation

◆ find_native_translation()

std::map< data::function_symbol, native_translation_t >::const_iterator mcrl2::smt::native_translations::find_native_translation ( const data::application &  a) const
inline

Definition at line 50 of file native_translation.h.

◆ has_native_definition() [1/3]

bool mcrl2::smt::native_translations::has_native_definition ( const data::application &  a) const
inline

Definition at line 65 of file native_translation.h.

◆ has_native_definition() [2/3]

bool mcrl2::smt::native_translations::has_native_definition ( const data::data_equation &  eq) const
inline

Definition at line 75 of file native_translation.h.

◆ has_native_definition() [3/3]

bool mcrl2::smt::native_translations::has_native_definition ( const data::function_symbol &  f) const
inline

Definition at line 60 of file native_translation.h.

◆ is_ambiguous()

bool mcrl2::smt::native_translations::is_ambiguous ( const data::function_symbol &  f) const
inline

Definition at line 92 of file native_translation.h.

◆ set_alternative_name()

void mcrl2::smt::native_translations::set_alternative_name ( const data::function_symbol &  f,
const std::string &  s 
)
inline

Definition at line 119 of file native_translation.h.

◆ set_ambiguous()

void mcrl2::smt::native_translations::set_ambiguous ( const data::function_symbol &  f)
inline

Definition at line 124 of file native_translation.h.

◆ set_native_definition() [1/3]

void mcrl2::smt::native_translations::set_native_definition ( const data::function_symbol &  f)
inline

Record that the mapping and equations for f should not be translated.

This translation is either not desired because there is a native Z3 counterpart, or because the function symbol is only used internally.

Definition at line 102 of file native_translation.h.

◆ set_native_definition() [2/3]

void mcrl2::smt::native_translations::set_native_definition ( const data::function_symbol &  f,
const data::data_equation &  eq 
)
inline

Definition at line 107 of file native_translation.h.

◆ set_native_definition() [3/3]

void mcrl2::smt::native_translations::set_native_definition ( const data::function_symbol &  f,
const std::string &  s 
)
inline

Definition at line 113 of file native_translation.h.

Member Data Documentation

◆ ambiguous_symbols

std::set<data::function_symbol> mcrl2::smt::native_translations::ambiguous_symbols

Definition at line 33 of file native_translation.h.

◆ do_not_define

std::set<data::function_symbol> mcrl2::smt::native_translations::do_not_define

Definition at line 27 of file native_translation.h.

◆ expressions

std::map<data::function_symbol, native_translation_t> mcrl2::smt::native_translations::expressions

Definition at line 25 of file native_translation.h.

◆ mappings

std::map<data::function_symbol, data::data_equation> mcrl2::smt::native_translations::mappings

Definition at line 29 of file native_translation.h.

◆ sorts

std::map<data::sort_expression, std::string> mcrl2::smt::native_translations::sorts

Definition at line 31 of file native_translation.h.

◆ special_recogniser

std::map<data::function_symbol, std::string> mcrl2::smt::native_translations::special_recogniser

Definition at line 35 of file native_translation.h.

◆ symbols

std::map<data::function_symbol, std::string> mcrl2::smt::native_translations::symbols

Definition at line 23 of file native_translation.h.

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