mcrl2::smt::basic_data_specification

Include file:

#include "mcrl2/smt/basic_data_specification.h
class mcrl2::smt::basic_data_specification

Protected attributes

std::map<data::function_symbol, std::map<std::size_t, data::function_symbol_vector>> m_all_projections
std::map<data::function_symbol, data::function_symbol_vector> m_all_recognisers
std::map<data::sort_expression, std::set<data::function_symbol>> m_constructed_sort_constructors
data::data_specification m_data_specification
std::map<data::function_symbol, std::shared_ptr<function_definition>> m_functions
std::shared_ptr<data::set_identifier_generator> m_identifier_generator
std::map<data::function_symbol, std::map<std::size_t, data::function_symbol>> m_projections
std::map<data::function_symbol, data::function_symbol> m_recognisers
data::representative_generator m_representative_generator
std::map<data::function_symbol, data::data_equation_vector> m_rewrite_rules
std::map<data::sort_expression, std::shared_ptr<sort_definition>> m_sorts

Public member functions

basic_data_specification(const data::data_specification &data_specification, std::shared_ptr<data::set_identifier_generator> identifier_generator)
const std::set<data::function_symbol> &constructors(const data::sort_expression &constructed_sort) const
std::string generate_data_expression(const std::map<data::variable, std::string> &declared_variables, const data::data_expression &expression) const
virtual std::string generate_data_expression(const std::map<data::variable, std::string> &declared_variables, const std::string &function_name, const data::data_expression_vector &arguments) const = 0
std::string generate_data_specification() const
std::string generate_smt_problem(const smt_problem &problem)
std::string generate_sort_name(const data::sort_expression &sort) const
virtual std::string generate_variable_declaration(const std::string &type_name, const std::string &variable_name) const = 0
data::set_identifier_generator &identifier_generator()
bool is_constructed_sort(const data::sort_expression &sort) const
bool is_constructor(const data::function_symbol &function) const
const data::function_symbol &projection_function(const data::function_symbol &constructor, const std::size_t &field_index) const
const data::function_symbol &recogniser_function(const data::function_symbol &constructor) const
virtual data::data_expression representative(const data::sort_expression &sort)
virtual ~basic_data_specification()

Protected member functions

void add_boolean_operators(const data::data_specification &data_specification, const std::shared_ptr<function_definition> &not_, const std::shared_ptr<function_definition> &and_, const std::shared_ptr<function_definition> &or_, const std::shared_ptr<function_definition> &implies)
void add_constructed_sort(const data::data_specification &data_specification, const data::sort_expression &sort)
void add_constructed_sorts(const data::data_specification &data_specification)
void add_function_definition(const data::function_symbol &function, const std::shared_ptr<function_definition> &definition)
void add_function_definition(const data::function_symbol &function, const data::variable_vector &parameters, const data::data_expression &rhs)
void add_function_definition(const data::function_symbol &function, const std::shared_ptr<function_definition> &definition, const data::variable_vector &parameters, const data::data_expression &rhs)
void add_numerical_operators(const data::data_specification &data_specification, const std::shared_ptr<function_definition> &less, const std::shared_ptr<function_definition> &less_equal, const std::shared_ptr<function_definition> &greater, const std::shared_ptr<function_definition> &greater_equal, const std::shared_ptr<function_definition> &plus, const std::shared_ptr<function_definition> &minus, const std::shared_ptr<function_definition> &times, const std::shared_ptr<function_definition> &divides, const std::shared_ptr<function_definition> &div, const std::shared_ptr<function_definition> &mod, const std::shared_ptr<function_definition> &floor, const std::shared_ptr<function_definition> &ceil = nullptr, const std::shared_ptr<function_definition> &round = nullptr, const std::shared_ptr<function_definition> &unary_minus = nullptr, const std::shared_ptr<function_definition> &maximum = nullptr, const std::shared_ptr<function_definition> &minimum = nullptr, const std::shared_ptr<function_definition> &abs = nullptr)
void add_recursive_function(const data::function_symbol &function)
void add_recursive_functions(const data::data_specification &data_specification)
void add_sort_bool(const std::shared_ptr<sort_definition> &bool_definition, const std::string &true_string, const std::string &false_string)
void add_sort_definition(const data::sort_expression &sort, const std::shared_ptr<sort_definition> &definition)
void add_sort_int(const std::shared_ptr<sort_definition> &int_definition, Printer printer)
void add_sort_nat(const std::shared_ptr<sort_definition> &nat_definition, Printer printer)
void add_sort_pos(const std::shared_ptr<sort_definition> &pos_definition, Printer printer)
void add_sort_real(const std::shared_ptr<sort_definition> &real_definition, Printer printer)
void add_standard_operators(const data::data_specification &data_specification, const std::shared_ptr<function_definition> &equal_to, const std::shared_ptr<function_definition> &not_equal_to, const std::shared_ptr<function_definition> &if_)
virtual constructed_sort_definition *create_constructed_sort(const data::sort_expression &sort, const constructed_sort_definition::constructors_t &constructors) = 0
virtual function_definition *create_recursive_function_definition(const data::function_symbol &function, const data::data_equation_vector &rewrite_rules) = 0
void find_rewrite_rules(const data::data_specification &data_specification)
virtual std::string generate_assertion(const std::map<data::variable, std::string> &declared_variables, const data::data_expression &assertion) const = 0
std::string generate_distinct_assertion(const std::map<data::variable, std::string> &declared_variables, const data::data_expression_list &distinct_terms) const
virtual std::string generate_smt_problem(const std::string &variable_declarations, const std::string &assertions) const = 0