mcrl2/smt/translate_expression.h

Include file:

#include "mcrl2/smt/translate_expression.h"

Classes

• mcrl2::smt::detail::translate_data_expression_traverser

Functions

void mcrl2::smt::translate_assertion(const T &x, OutputStream &o, std::unordered_map<data::data_expression, std::string> &c, const native_translations &nt)

void translate_data_expression(const T &x, OutputStream &o, std::unordered_map<data::data_expression, std::string> &c, const native_translations &nt)

void mcrl2::smt::translate_variable_declaration(const Container &vars, OutputStream &o, std::unordered_map<data::data_expression, std::string> &c, const native_translations &nt)

Functions

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

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