Classes
struct	fixed_string_translation

struct	translate_data_expression_traverser

struct	translate_sort_expression_traverser

Functions
template<typename OutputStream >
void	translate_sort_definition (const std::string &sort_name, const data::sort_expression &s, const data::data_specification &dataspec, OutputStream &out, const native_translations &nt, std::map< data::structured_sort, std::string > &struct_name_map)

template<typename OutputStream >
void	translate_sort_definition (const data::basic_sort &s, const data::data_specification &dataspec, OutputStream &out, const native_translations &nt, std::map< data::structured_sort, std::string > &struct_name_map)

static std::set< data::sort_expression >	find_dependencies (const data::data_specification &dataspec, const data::sort_expression &sort)

std::map< data::sort_expression, std::set< data::sort_expression > >	find_sorts_and_dependencies (const data::data_specification &dataspec, std::map< data::structured_sort, std::string > &struct_name_map)

template<typename OutputStream >
void	translate_sort_definitions (const data::data_specification &dataspec, OutputStream &out, const native_translations &nt, data::set_identifier_generator &id_gen, std::map< data::structured_sort, std::string > &struct_name_map)

template<typename OutputStream >
void	translate_alias (const data::alias &s, OutputStream &out, const native_translations &nt, const std::map< data::structured_sort, std::string > &struct_name_map)

bool	is_higher_order (const data::function_symbol &f)

bool	is_higher_order (const data::application &a)

bool	is_higher_order (const data::data_equation &eq)

template<typename OutputStream >
void	translate_mapping (const data::function_symbol &f, OutputStream &out, const native_translations &nt, const std::map< data::structured_sort, std::string > &snm, bool check_native=true)

template<typename OutputStream >
void	translate_native_mappings (OutputStream &out, std::unordered_map< data::data_expression, std::string > &c, const native_translations &nt, const std::map< data::structured_sort, std::string > &snm)

template<typename OutputStream >
void	translate_equation (const data::data_equation &eq, OutputStream &out, std::unordered_map< data::data_expression, std::string > &c, const native_translations &nt)

std::string	translate_symbol_disambiguate (const data::function_symbol &f, const native_translations &nt)

template<typename OutputStream >
data::data_expression	declare_variables_binder (const data::variable_list &vars, OutputStream &out, const native_translations &nt)
	Declare variables to be used in binder such as exists or forall and print the declaration to out.

static const std::map< data::structured_sort, std::string > &	empty_name_map ()

template<template< class > class Traverser, class OutputStream >
translate_sort_expression_traverser< Traverser, OutputStream >	make_translate_sort_expression_traverser (OutputStream &out, const native_translations &nt, const std::map< data::structured_sort, std::string > &snm)

Variables
static const native_translation_t	pp_translation

static const native_translation_t	pp_real_translation

static const native_translation_t	reconstruct_divmod

Function Documentation

◆ declare_variables_binder()

template<typename OutputStream >

data::data_expression mcrl2::smt::detail::declare_variables_binder	(	const data::variable_list &	vars,
		OutputStream &	out,
		const native_translations &	nt
	)

Declare variables to be used in binder such as exists or forall and print the declaration to out.

Returns: An expression that constrains the domains of Pos and Nat variables

Definition at line 49 of file translate_expression.h.

◆ empty_name_map()

static const std::map< data::structured_sort, std::string > & mcrl2::smt::detail::empty_name_map ( )

inlinestatic

Definition at line 23 of file translate_sort.h.

◆ find_dependencies()

static std::set< data::sort_expression > mcrl2::smt::detail::find_dependencies	(	const data::data_specification &	dataspec,
		const data::sort_expression &	sort
	)

inlinestatic

Definition at line 74 of file translate_specification.h.

◆ find_sorts_and_dependencies()

std::map< data::sort_expression, std::set< data::sort_expression > > mcrl2::smt::detail::find_sorts_and_dependencies	(	const data::data_specification &	dataspec,
		std::map< data::structured_sort, std::string > &	struct_name_map
	)

inline

Definition at line 95 of file translate_specification.h.

◆ is_higher_order() [1/3]

bool mcrl2::smt::detail::is_higher_order ( const data::application & a )

inline

Definition at line 183 of file translate_specification.h.

◆ is_higher_order() [2/3]

bool mcrl2::smt::detail::is_higher_order ( const data::data_equation & eq )

inline

Definition at line 194 of file translate_specification.h.

◆ is_higher_order() [3/3]

bool mcrl2::smt::detail::is_higher_order ( const data::function_symbol & f )

inline

Definition at line 165 of file translate_specification.h.

◆ make_translate_sort_expression_traverser()

template<template< class > class Traverser, class OutputStream >

translate_sort_expression_traverser< Traverser, OutputStream > mcrl2::smt::detail::make_translate_sort_expression_traverser	(	OutputStream &	out,
		const native_translations &	nt,
		const std::map< data::structured_sort, std::string > &	snm
	)

Definition at line 87 of file translate_sort.h.

◆ translate_alias()

template<typename OutputStream >

void mcrl2::smt::detail::translate_alias	(	const data::alias &	s,
		OutputStream &	out,
		const native_translations &	nt,
		const std::map< data::structured_sort, std::string > &	struct_name_map
	)

inline

Definition at line 155 of file translate_specification.h.

◆ translate_equation()

template<typename OutputStream >

void mcrl2::smt::detail::translate_equation	(	const data::data_equation &	eq,
		OutputStream &	out,
		std::unordered_map< data::data_expression, std::string > &	c,
		const native_translations &	nt
	)

inline

Definition at line 282 of file translate_specification.h.

◆ translate_mapping()

template<typename OutputStream >

void mcrl2::smt::detail::translate_mapping	(	const data::function_symbol &	f,
		OutputStream &	out,
		const native_translations &	nt,
		const std::map< data::structured_sort, std::string > &	snm,
		bool	check_native = `true`
	)

inline

Definition at line 213 of file translate_specification.h.

◆ translate_native_mappings()

template<typename OutputStream >

void mcrl2::smt::detail::translate_native_mappings	(	OutputStream &	out,
		std::unordered_map< data::data_expression, std::string > &	c,
		const native_translations &	nt,
		const std::map< data::structured_sort, std::string > &	snm
	)

inline

Definition at line 244 of file translate_specification.h.

◆ translate_sort_definition() [1/2]

template<typename OutputStream >

void mcrl2::smt::detail::translate_sort_definition	(	const data::basic_sort &	s,
		const data::data_specification &	dataspec,
		OutputStream &	out,
		const native_translations &	nt,
		std::map< data::structured_sort, std::string > &	struct_name_map
	)

inline

Definition at line 63 of file translate_specification.h.

◆ translate_sort_definition() [2/2]

template<typename OutputStream >

void mcrl2::smt::detail::translate_sort_definition	(	const std::string &	sort_name,
		const data::sort_expression &	s,
		const data::data_specification &	dataspec,
		OutputStream &	out,
		const native_translations &	nt,
		std::map< data::structured_sort, std::string > &	struct_name_map
	)

inline

Definition at line 26 of file translate_specification.h.

◆ translate_sort_definitions()

template<typename OutputStream >

void mcrl2::smt::detail::translate_sort_definitions	(	const data::data_specification &	dataspec,
		OutputStream &	out,
		const native_translations &	nt,
		data::set_identifier_generator &	id_gen,
		std::map< data::structured_sort, std::string > &	struct_name_map
	)

inline

Definition at line 125 of file translate_specification.h.

◆ translate_symbol_disambiguate()

std::string mcrl2::smt::detail::translate_symbol_disambiguate	(	const data::function_symbol &	f,
		const native_translations &	nt
	)

inline

Definition at line 28 of file translate_expression.h.

Variable Documentation

◆ pp_real_translation

static const native_translation_t mcrl2::smt::detail::pp_real_translation

static

Initial value:

= [](const data::data_expression& e,
                                                           const std::function<void(std::string)>& output_func,
                                                           const std::function<void(data::data_expression)>& )
{
  assert(data::sort_real::is_creal_application(e));
  const data::application& a = atermpp::down_cast<data::application>(e);
  output_func("(/ " +  data::pp(a[0]) + ".0  " + data::pp(a[1]) + ".0)");
}

Definition at line 91 of file solver.cpp.

◆ pp_translation

static const native_translation_t mcrl2::smt::detail::pp_translation

static

Initial value:

= [](const data::data_expression& e,
                                                      const std::function<void(std::string)>& output_func,
                                                      const std::function<void(data::data_expression)>& )
{
  output_func(data::pp(e));
}

Definition at line 85 of file solver.cpp.

◆ reconstruct_divmod

static const native_translation_t mcrl2::smt::detail::reconstruct_divmod

static

Initial value:

= [](const data::data_expression& e,
                                                          const std::function<void(std::string)>& output_func,
                                                          const std::function<void(data::data_expression)>& translate_func)
{
utilities::mcrl2_unused(output_func);
utilities::mcrl2_unused(translate_func);
 
  assert(data::sort_nat::is_first_application(e) || data::sort_nat::is_last_application(e));
  const data::application& a = atermpp::down_cast<data::application>(e);
  if(data::sort_nat::is_divmod_application(a[0]))
  {
    const data::application& a2 = atermpp::down_cast<data::application>(a[0]);
    output_func("(" + std::string(data::sort_nat::is_first_application(a2) ? "div" : "mod") + " ");
    translate_func(a2[0]);
    output_func(" ");
    translate_func(a2[1]);
    output_func(")");
  }
  else
 
  {
    throw translation_error("Cannot perform native translation of " + pp(e));
  }
}

Definition at line 99 of file solver.cpp.

Classes

Functions

Variables

Function Documentation

◆ declare_variables_binder()

◆ empty_name_map()

◆ find_dependencies()

◆ find_sorts_and_dependencies()

◆ is_higher_order() [1/3]

◆ is_higher_order() [2/3]

◆ is_higher_order() [3/3]

◆ make_translate_sort_expression_traverser()

◆ translate_alias()

◆ translate_equation()

◆ translate_mapping()

◆ translate_native_mappings()

◆ translate_sort_definition() [1/2]

◆ translate_sort_definition() [2/2]

◆ translate_sort_definitions()

◆ translate_symbol_disambiguate()

Variable Documentation

◆ pp_real_translation

◆ pp_translation

◆ reconstruct_divmod