mcrl2::smt::smt4_data_specification

Include file:

#include "mcrl2/smt/cvc4.h
class mcrl2::smt::smt4_data_specification

Public member functions

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
std::string generate_variable_declaration(const std::string &type_name, const std::string &variable_name) const
smt4_data_specification(const data::data_specification &data_specification)

Protected member functions

constructed_sort_definition *create_constructed_sort(const data::sort_expression &sort, const constructed_sort_definition::constructors_t &constructors)
function_definition *create_recursive_function_definition(const data::function_symbol &function, const data::data_equation_vector &rewrite_rules)
std::string generate_assertion(const std::map<data::variable, std::string> &declared_variables, const data::data_expression &assertion) const
std::string generate_distinct_assertion(const std::map<data::variable, std::string> &declared_variables, const data::data_expression_list &distinct_terms) const
std::string generate_smt_problem(const std::string &variable_declarations, const std::string &assertions) const