mCRL2
Loading...
Searching...
No Matches
mcrl2::data::detail Namespace Reference

Namespaces

namespace  prover
 

Classes

struct  add_capture_avoiding_replacement
 
struct  add_capture_avoiding_replacement_with_an_identifier_generator
 
struct  add_data_rewriter
 Applies a data rewriter to data expressions appearing in a term. It works both with and without a substitution. More...
 
struct  anonymize_builder
 
struct  anonymize_builder_instance
 
struct  apply_rewriter_builder
 
class  BDD2Dot
 The class BDD2Dot offers the ability to write binary decision diagrams to dot files. The method BDD2Dot::output_bdd receives a binary decision diagram as parameter a_bdd and writes it to a file in dot format with the name passed as parameter a_file_name. More...
 
class  BDD_Info
 The class BDD_Info provides information about the structure of binary decision diagrams. More...
 
class  BDD_Path_Eliminator
 Base class for eliminating inconsistent paths from BDDs. More...
 
class  BDD_Prover
 
class  BDD_Simplifier
 A base class for simplifying binary decision diagrams. More...
 
class  build_pars
 
struct  capture_avoiding_substitution_updater
 
struct  compare_sort
 Tests if a term is a sort, and if it is equal to s. More...
 
struct  compare_term
 
struct  compare_variable
 Function object that determines if a term is equal to a given data variable. More...
 
struct  data_expression_actions
 
class  data_property_map
 Base class for storing properties of mCRL2 types. Properties are (key, value) pairs stored as strings in KEY = VALUE format. The data_property_map has some predefined functions for types in the Data Library. The optional type argument is used by derived classes. The type represents the name of a derived class as per CRTP. More...
 
struct  data_rewriter_builder
 
struct  data_specification_actions
 
class  dependencies_rewrite_rule_pair
 
struct  double_variable_traverser
 
struct  enumerator_iteration_limit
 
struct  enumerator_replace_builder
 
struct  equality_set_with_top
 
struct  find_equalities_expression
 
struct  find_equalities_traverser
 
struct  find_equalities_traverser_inst
 
class  Formula_Checker
 The class formula checker takes a data specification in mCRL2 format and a list of expressions. More...
 
struct  function_symbol_has_name
 
struct  if_rewrite_builder
 
struct  if_rewrite_with_rewriter_builder
 
class  Induction
 The class Induction generates statements corresponding to. More...
 
class  inequality_consistency_cache
 
class  inequality_inconsistency_cache
 
class  inequality_inconsistency_cache_base
 
class  Info
 Base class for classes that provide information about the structure of. More...
 
struct  is_a_variable
 
struct  is_untyped_traverser
 
class  jitty_argument_rewriter
 
struct  jitty_assignments_for_a_rewrite_rule
 
struct  jitty_variable_assignment_for_a_rewrite_rule
 
class  lhs_t
 
class  Manipulator
 Base class for classes that provide functionality to modify or create terms. More...
 
class  match_tree
 
class  match_tree_A
 
class  match_tree_C
 
class  match_tree_CRe
 
class  match_tree_D
 
class  match_tree_F
 
class  match_tree_M
 
class  match_tree_Me
 
class  match_tree_N
 
class  match_tree_R
 
class  match_tree_Re
 
class  match_tree_S
 
class  match_tree_X
 
class  nfs_array
 
struct  normalize_and_or_builder
 
struct  normalize_equality_builder
 
struct  normalize_sorts_function
 
struct  normalizer
 
struct  one_point_rule_preprocessor
 
class  one_point_rule_rewrite_builder
 
struct  one_point_rule_substitution_algorithm
 
class  parser
 
class  prepend_iterator_tag_convertor
 
class  prepend_iterator_tag_convertor< std::input_iterator_tag >
 
struct  printer
 
struct  quantifiers_inside_builder
 
struct  quantifiers_inside_exists_builder
 
struct  quantifiers_inside_forall_builder
 
struct  recalculate_term_as_stack_is_too_small
 
struct  replace_capture_avoiding_variables_builder
 
struct  replace_capture_avoiding_variables_builder_with_an_identifier_generator
 
struct  replace_constants_by_variables_builder
 Replace each constant data application c by a fresh variable v, and add extend the substitution sigma with the assignment v := r(c). This can be used in rewriting, to avoid that c is rewritten by the rewriter multiple times. More...
 
struct  rewrite_data_expressions_builder
 
struct  rewrite_data_expressions_with_substitution_builder
 
class  rewrite_stack
 
struct  rewrite_statistics
 
class  Rewriter
 Rewriter interface class. More...
 
struct  rewriter_wrapper
 
class  RewriterJitty
 
class  RewriterProver
 
struct  rule
 A rule describes a partially pattern-matched rewrite rule. More...
 
class  simplify_rewrite_builder
 
class  skip_function_application_to_head
 
class  skip_function_application_to_head_assignment
 
class  SMT_LIB_Solver
 
class  SMT_Solver
 
struct  sort_expression_actions
 
struct  sort_has_name
 
struct  sort_of_expression
 Function object that returns the sort of a data expression. More...
 
class  strategy
 A strategy is a list of rules and the number of variables that occur in it. More...
 
class  strategy_rule
 Is either a rewrite rule to be matched or an index that should be rewritten. More...
 
class  substitution_updater_with_an_identifier_generator
 
class  term_appl_prepend_iterator
 
class  translate_user_notation_builder
 
struct  translate_user_notation_function
 
class  variable_context
 
struct  variable_name
 Function object that returns the name of a data variable. More...
 
class  variable_or_number
 This is a list where variables and aterm ints can be stored. More...
 
class  variable_with_a_rational_factor
 

Typedefs

typedef sort_of_expression< variablesort_of_variable
 Function object that returns the sort of a data variable.
 
typedef atermpp::term_list< variable_or_numbervariable_or_number_list
 
typedef atermpp::term_list< match_treematch_tree_list
 
typedef std::vector< match_treematch_tree_vector
 
typedef atermpp::term_list< match_tree_listmatch_tree_list_list
 
typedef atermpp::term_list< match_tree_list_listmatch_tree_list_list_list
 
typedef std::map< variable, data_expressionmap_based_lhs_t
 

Enumerations

enum  Answer { answer_yes , answer_no , answer_undefined }
 A prover that uses EQ-BDDs. More...
 
enum  Compare_Result { compare_result_smaller , compare_result_equal , compare_result_bigger }
 
enum  smt_solver_type { solver_type_cvc , solver_type_z3 }
 The enumeration type smt_solver_type enumerates all available SMT solvers. More...
 
enum  comparison_t { less , less_eq , equal }
 
enum  node_type { true_end_node , false_end_node , intermediate_node }
 

Functions

bool contains_untyped_sort (const sort_expression &s)
 
const data_expressionevaluate_lambda_data_expression (const data_expression &t)
 
template<class TERM >
data_expression evaluate_lambda_data_expression (const TERM &t, typename std::enable_if< std::is_invocable_r< void, TERM, data_expression & >::value >::type *=nullptr)
 
template<class TERM >
data_expression evaluate_lambda_data_expression (const TERM &t, typename std::enable_if< std::is_invocable_r< const data_expression, TERM, void >::value >::type *=nullptr)
 
template<class HEAD , class CONTAINER >
bool check_whether_sorts_match (const HEAD &head_lambda, const CONTAINER &l)
 
data_expression_list get_arguments ()
 
template<class HEAD , class... ARGUMENTS>
data_expression_list get_arguments (const HEAD &h, const ARGUMENTS &... args)
 
atermpp::aterm_appl data_specification_to_aterm (const data_specification &s)
 
data_expression create_finite_set (const data_expression &x)
 Create the finite set { x }, with x a data expression.
 
data_expression create_set_comprehension (const variable &x, const data_expression &phi)
 Create the set { x | phi }, with phi a predicate that may depend on the variable x.
 
data_expression create_set_in (const data_expression &x, const data_expression &X)
 Create the predicate 'x in X', with X a set.
 
sort_expression get_set_sort (const container_sort &x)
 Returns the sort s of Set(s).
 
template<typename PropertyMap >
bool compare_property_maps (const std::string &message, const PropertyMap &map1, const std::string &expected_result)
 
variable_list set_intersection (const variable_list &x, const variable_list &y)
 Returns the intersection of two unordered sets, that are stored in ATerm lists.
 
variable_list set_difference (const variable_list &x, const variable_list &y)
 Returns the difference of two unordered sets, that are stored in aterm lists.
 
template<typename Container >
data::sort_expression_list parameter_sorts (const Container &parameters)
 Returns the sorts of a sequence of parameters.
 
template<class VariableContainer >
bool unique_names (const VariableContainer &variables)
 Returns true if the names of the given variables are unique.
 
bool check_assignment_variables (assignment_list const &assignments, variable_list const &variables)
 Returns true if the left hand sides of assignments are contained in variables.
 
template<typename SortContainer >
bool check_sort (const sort_expression &s, const SortContainer &sorts)
 Returns true if the domain sorts and the codomain sort of the given sort s are contained in sorts.
 
template<typename Iterator , typename SortContainer >
bool check_sorts (Iterator first, Iterator last, const SortContainer &sorts)
 Returns true if the domain sorts and the range sort of the sorts in the sequence [first, last) are contained in sorts.
 
template<typename VariableContainer , typename SortContainer >
bool check_variable_sorts (const VariableContainer &variables, const SortContainer &sorts)
 Returns true if the domain sorts and the range sort of the given variables are contained in sorts.
 
bool check_variable_names (variable_list const &variables, const std::set< core::identifier_string > &names)
 Returns true if names of the given variables are not contained in names.
 
template<typename Container , typename SortContainer >
bool check_data_spec_sorts (const Container &container, const SortContainer &sorts)
 Returns true if the domain sorts and range sort of the given functions are contained in sorts.
 
void set_enumerator_iteration_limit (std::size_t size)
 
std::size_t get_enumerator_iteration_limit ()
 
bool equal_sorts (const data::variable_list &v, const data::data_expression_list &w, const data::data_specification &data_spec)
 Checks if the sorts of the variables/expressions in both lists are equal.
 
std::set< core::identifier_stringvariable_names (const std::set< data::variable > &variables)
 Returns the names of a set of data variables.
 
std::set< std::string > variable_name_strings (const std::set< data::variable > &variables)
 Returns the names of a set of data variables as a set of strings.
 
std::set< std::string > variable_name_strings (const std::set< data::variable > &variables1, const std::set< data::variable > &variables2)
 Returns the names of a set of data variables.
 
atermpp::aterm_appl remove_index_impl (const atermpp::aterm_appl &x)
 
atermpp::aterm_appl add_index_impl (const atermpp::aterm_appl &x)
 
atermpp::aterm add_index (const atermpp::aterm &x)
 
atermpp::aterm remove_index (const atermpp::aterm &x)
 
bool is_untyped (const data_expression &x)
 
data_expression negate_inequality (const data_expression &e)
 
bool is_inequality (const data_expression &e)
 Determine whether a data expression is an inequality.
 
const data_expressioncondition_part (const data_expression &e)
 
const data_expressionthen_part (const data_expression &e)
 
const data_expressionelse_part (const data_expression &e)
 
static bool split_condition_aux (const data_expression &e, std::vector< data_expression_list > &real_conditions, std::vector< data_expression_list > &non_real_conditions, const bool negate=false)
 Splits a condition in expressions ranging over reals and the others.
 
void split_condition (const data_expression &e, std::vector< data_expression_list > &real_conditions, std::vector< data_expression > &non_real_conditions)
 This function first splits the given condition e into real conditions and non real conditions. \detail This function first uses split_condition_aux to split the condition e. Then.
 
template<typename MutableSubstitution >
void parse_substitution (std::string text, MutableSubstitution &sigma, const data_specification &data_spec=data::data_specification())
 Parses a string of the form "b: Bool := true, n: Nat := 0", and adds the substitutions to the substition function sigma. If the string is surrounded by brackets (e.g. "[b: Bool := true, n: Nat := 0]"), these are ignored.
 
void print_parse_check (const sort_expression &x, const data_specification &dataspec=data_specification())
 
void print_parse_check (const data_expression &x, const data_specification &dataspec=data_specification())
 
data::data_expression bool_to_numeric (data::data_expression const &e, data::sort_expression const &s)
 
data_expression reconstruct_pos_mult (const data_expression &x, std::vector< char > &result)
 
smt_solver_type parse_solver_type (const std::string &s)
 standard conversion from string to solver type
 
std::istream & operator>> (std::istream &is, smt_solver_type &s)
 standard conversion from stream to solver type
 
std::string print_solver_type (const smt_solver_type s)
 standard conversion from solver type to string
 
std::ostream & operator<< (std::ostream &os, smt_solver_type s)
 standard conversion from solvert type to stream
 
std::string description (const smt_solver_type s)
 description of solver type
 
std::shared_ptr< detail::RewritercreateRewriter (const data_specification &DataSpec, const used_data_equation_selector &equations_selector, const rewrite_strategy Strategy=jitty)
 Create a rewriter.
 
void CheckRewriteRule (const data_equation &data_eqn)
 Check that an mCRL2 data equation is a valid rewrite rule. If not, an runtime_error is thrown indicating the problem.
 
bool isValidRewriteRule (const data_equation &data_eqn)
 Check whether or not an mCRL2 data equation is a valid rewrite rule.
 
std::size_t getArity (const data::function_symbol &op)
 
std::size_t get_direct_arity (const data::function_symbol &op)
 
data_expression remove_normal_form_function (const data_expression &t)
 removes auxiliary expressions this_term_is_in_normal_form from data_expressions that are being rewritten.
 
variable_list get_free_vars (const data_expression &a)
 
sort_expression residual_sort (const sort_expression &s, std::size_t no_of_initial_arguments)
 
const data_expressionget_argument_of_higher_order_term_helper (const application &t, std::size_t &i)
 
const data_expressionget_argument_of_higher_order_term (const application &t, std::size_t i)
 
std::size_t recursive_number_of_args (const data_expression &t)
 
const data_expressionget_nested_head_helper (const application &t)
 
const data_expressionget_nested_head (const data_expression &t)
 
const data_expression replace_nested_head (const data_expression &t, const data_expression &head)
 
template<class ARGUMENT_REWRITER >
void rewrite_all_arguments (data_expression &result, const application &t, const ARGUMENT_REWRITER rewriter)
 
std::ostream & operator<< (std::ostream &s, const match_tree &t)
 
strategy create_strategy (data_equation_list rules)
 Creates a strategy for given set of rewrite rules with head symbol f.
 
std::size_t rewrite_count ()
 
void display_rewrite_statistics ()
 
void increment_rewrite_count ()
 
static std::vector< data::rewrite_strategyinitialise_test_rewrite_strategies (const bool with_prover)
 Static initialisation of rewrite strategies used for testing.
 
const std::vector< data::rewrite_strategy > & get_test_rewrite_strategies (const bool with_prover)
 Rewrite strategies that should be tested.
 
template<typename Iterator >
bool sequence_contains_duplicates (Iterator first, Iterator last)
 Returns true if the sequence [first, last) contains duplicates.
 
template<typename Iterator1 , typename Iterator2 >
bool sequences_do_overlap (Iterator1 first1, Iterator1 last1, Iterator2 first2, Iterator2 last2)
 Returns true if the two sequences [first1, last1) and [first2, last2) have a non empty intersection.
 
template<typename Iterator , typename T >
bool sequence_is_subset_of_set (Iterator first, Iterator last, const std::set< T > &s)
 Returns true if all elements of the range [first, last) are element of the set s.
 
template<class Container >
std::set< typename Container::value_type > make_set (const Container &c)
 Makes a set of the given container.
 
template<typename Sequence >
bool sequence_empty_intersection (Sequence s1, Sequence s2)
 Determines if the unordered sequences s1 and s2 have an empty intersection.
 
template<typename FILTER >
void split_finite_variables (data::variable_list variables, const data::data_specification &data, data::variable_list &finite_variables, data::variable_list &infinite_variables, data::variable_list &unused, const FILTER filter)
 Splits the variables in a subset with finite sort, with infinite sort and those that are not used according to a filter.
 
template<typename Rewriter , typename FILTER >
void split_enumerable_variables (data::variable_list variables, const data::data_specification &data, const Rewriter &rewr, data::variable_list &enumerable_variables, data::variable_list &non_enumerable_variables, data::variable_list &unused, const FILTER filter)
 Splits a list of variables in those that are enumerable, non enumerable and not used, according to a filter.
 
template<typename T >
normalize_and_or (const T &x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T >
void normalize_and_or (T &x, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=0)
 
template<typename T >
normalize_equality (const T &x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T >
void normalize_equality (T &x, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=0)
 
template<typename Function >
normalizer< Function > N (const Function &f)
 
std::string VARIABLE_SPECIFICATION ()
 
template<typename Rewriter1 , typename Rewriter2 >
void test_rewriters (Rewriter1 R1, Rewriter2 R2, std::string expr1, std::string expr2, const std::string &var_decl=VARIABLE_SPECIFICATION(), const std::string &data_spec="")
 
data_expression I (const data_expression &x)
 
void check_duplicate_variable_names (const data::variable_list &x, const std::string &msg)
 
data_expression make_set_ (std::size_t function_index, const sort_expression &element_sort, const data_expression_vector &set_elements)
 
data_expression make_if_expression_ (std::size_t &function_index, const std::size_t argument_index, const std::vector< data_expression_vector > &data_domain_expressions, const data_expression_vector &codomain_expressions, const variable_vector &parameters)
 
template<class Rewriter , class MutableSubstitution >
bool compute_finite_set_elements (const container_sort &sort, const data_specification &dataspec, Rewriter datar, MutableSubstitution &sigma, data_expression_vector &result, enumerator_identifier_generator &id_generator)
 Computes the elements of a finite set sort, and puts them in result. If there are too many elements, false is returned.
 
template<class Rewriter >
bool compute_finite_function_sorts (const function_sort &sort, enumerator_identifier_generator &id_generator, const data::data_specification &dataspec, Rewriter datar, data_expression_vector &result, variable_list &function_parameter_list)
 Computes the elements of a finite function sort, and puts them in result. If there are too many elements, false is returned.
 
template<typename Rewriter >
bool is_enumerable (const data_specification &dataspec, const Rewriter &rewr, const sort_expression &sort, std::list< sort_expression > &parents)
 
bool is_pos (const core::identifier_string &Number)
 
bool is_nat (const core::identifier_string &Number)
 
function_sort make_function_sort_ (const sort_expression &domain, const sort_expression &codomain)
 
template<typename Function , typename T >
atermpp::term_list< T > transform_aterm_list (const Function &f, const atermpp::term_list< T > &x)
 
sort_expression unwind_sort_expression (const sort_expression &x, const alias_vector &aliases)
 
bool is_numeric_type (const sort_expression &x)
 
std::ostream & operator<< (std::ostream &out, const find_equalities_expression &x)
 
bool is_numeric_sort (const sort_expression &x)
 
std::size_t numeric_sort_value (const sort_expression &x)
 
std::string pp (const detail::lhs_t &lhs)
 
detail::comparison_t negate (const detail::comparison_t t)
 
std::string pp (const detail::comparison_t t)
 
atermpp::function_symbol f_variable_with_a_rational_factor ()
 
void set_factor_for_a_variable (detail::map_based_lhs_t &new_lhs, const variable &x, const data_expression &e)
 
lhs_t set_factor_for_a_variable (const lhs_t &lhs, const variable &x, const data_expression &e)
 
const lhs_t map_to_lhs_type (const map_based_lhs_t &lhs)
 
const lhs_t map_to_lhs_type (const map_based_lhs_t &lhs, const data_expression &factor, const rewriter &r)
 
bool is_well_formed (const lhs_t &lhs)
 
const lhs_t remove_variable_and_divide (const lhs_t &lhs, const variable &v, const data_expression &f, const rewriter &r)
 
void emplace_back_if_not_zero (std::vector< detail::variable_with_a_rational_factor > &r, const variable &v, const data_expression &f)
 
template<application Operation>
const lhs_t meta_operation_constant (const lhs_t &argument, const data_expression &v, const rewriter &r)
 
template<class OPERATION >
lhs_t meta_operation_lhs (const lhs_t &argument1, const lhs_t &argument2, OPERATION operation, const rewriter &r)
 
const lhs_t add (const data_expression &v, const lhs_t &argument, const rewriter &r)
 
const lhs_t subtract (const lhs_t &argument, const data_expression &v, const rewriter &r)
 
const lhs_t multiply (const lhs_t &argument, const data_expression &v, const rewriter &r)
 
const lhs_t divide (const lhs_t &argument, const data_expression &v, const rewriter &r)
 
const lhs_t add (const lhs_t &argument, const lhs_t &e, const rewriter &r)
 
const lhs_t subtract (const lhs_t &argument, const lhs_t &e, const rewriter &r)
 
atermpp::function_symbol linear_inequality_less ()
 
atermpp::function_symbol linear_inequality_less_equal ()
 
atermpp::function_symbol linear_inequality_equal ()
 
template<typename TermTraits >
void optimized_not (typename TermTraits::term_type &result, const typename TermTraits::term_type &arg, TermTraits)
 
template<typename TermTraits >
void optimized_and (typename TermTraits::term_type &result, const typename TermTraits::term_type &left, const typename TermTraits::term_type &right, TermTraits)
 Make a conjunction and optimize it if possible.
 
template<typename TermTraits >
void optimized_or (typename TermTraits::term_type &result, const typename TermTraits::term_type &left, const typename TermTraits::term_type &right, TermTraits)
 Make a disjunction.
 
template<typename TermTraits >
void optimized_imp (typename TermTraits::term_type &result, const typename TermTraits::term_type &left, const typename TermTraits::term_type &right, TermTraits t)
 Make an implication.
 
template<typename TermTraits >
void optimized_forall (typename TermTraits::term_type &result, const typename TermTraits::variable_sequence_type &v, const typename TermTraits::term_type &arg, bool remove_variables, bool empty_domain_allowed, TermTraits)
 Make a universal quantification.
 
template<typename TermTraits >
void optimized_exists (typename TermTraits::term_type &result, const typename TermTraits::variable_sequence_type &v, const typename TermTraits::term_type &arg, bool remove_variables, bool empty_domain_allowed, TermTraits)
 Make an existential quantification.
 
sort_expression parse_sort_expression (const std::string &text)
 
variable_list parse_variables (const std::string &text)
 
data_expression parse_data_expression (const std::string &text)
 
data_specification parse_data_specification_new (const std::string &text)
 
variable_list parse_variable_declaration_list (const std::string &text)
 
static data_specification const & default_specification ()
 
bool is_numeric_cast (const data_expression &x)
 
bool look_through_numeric_casts (const data_expression &x, std::function< bool(const data_expression &)> f)
 
bool is_plus (const application &x)
 
bool is_minus (const application &x)
 
bool is_mod (const application &x)
 
bool is_div (const application &x)
 
bool is_divmod (const application &x)
 
bool is_divides (const application &x)
 
bool is_implies (const application &x)
 
bool is_set_union (const application &x)
 
bool is_set_difference (const application &x)
 
bool is_bag_join (const application &x)
 
bool is_bag_difference (const application &x)
 
bool is_and (const application &x)
 
bool is_or (const application &x)
 
bool is_equal_to (const application &x)
 
bool is_not_equal_to (const application &x)
 
bool is_less (const application &x)
 
bool is_less_equal (const application &x)
 
bool is_greater (const application &x)
 
bool is_greater_equal (const application &x)
 
bool is_in (const application &x)
 
bool is_times (const application &x)
 
bool is_element_at (const application &x)
 
bool is_set_intersection (const application &x)
 
bool is_bag_intersection (const application &x)
 
bool is_concat (const application &x)
 
bool is_cons_list (data_expression x)
 
bool is_snoc_list (data_expression x)
 
bool is_cons (const application &x)
 
bool is_snoc (const application &x)
 
template<typename Substitution >
std::ostream & operator<< (std::ostream &out, const capture_avoiding_substitution_updater< Substitution > &sigma)
 
template<template< class > class Builder, template< template< class > class, class, class > class Binder, class Substitution >
replace_capture_avoiding_variables_builder< Builder, Binder, Substitution > apply_replace_capture_avoiding_variables_builder (capture_avoiding_substitution_updater< Substitution > &sigma)
 
template<typename Substitution , typename IdentifierGenerator >
data::variable update_substitution (Substitution &sigma, const data::variable &v, const std::multiset< data::variable > &V, IdentifierGenerator &id_generator)
 
template<typename Substitution , typename IdentifierGenerator , typename VariableContainer >
VariableContainer update_substitution (Substitution &sigma, const VariableContainer &v, const std::multiset< data::variable > &V, IdentifierGenerator &id_generator)
 
template<template< class > class Builder, template< template< class > class, class, class, class > class Binder, class Substitution , class IdentifierGenerator >
replace_capture_avoiding_variables_builder_with_an_identifier_generator< Builder, Binder, Substitution, IdentifierGenerator > apply_replace_capture_avoiding_variables_builder_with_an_identifier_generator (Substitution &sigma, IdentifierGenerator &id_generator)
 
template<template< class > class Builder, class Rewriter >
rewrite_data_expressions_builder< Builder, Rewritermake_rewrite_data_expressions_builder (Rewriter R)
 
template<template< class > class Builder, class Rewriter , class Substitution >
rewrite_data_expressions_with_substitution_builder< Builder, Rewriter, Substitution > make_rewrite_data_expressions_with_substitution_builder (Rewriter R, Substitution sigma)
 
template<typename DataRewriter , typename SubstitutionFunction >
data::data_expression data_rewrite (const data::data_expression &x, const DataRewriter &R, SubstitutionFunction &sigma)
 
template<typename DataRewriter >
data::data_expression data_rewrite (const data::data_expression &x, const DataRewriter &R, data::no_substitution &)
 
template<template< class, class, class > class Builder, class DataRewriter , class SubstitutionFunction >
apply_rewriter_builder< Builder, DataRewriter, SubstitutionFunction > make_apply_rewriter_builder (const DataRewriter &datar, SubstitutionFunction &sigma)
 
application replace_argument (const application &x, std::size_t i, const data_expression &y)
 
data_expression push_if_outside (const application &x)
 
data_expression quantifiers_inside (const data_expression &x)
 
data_expression quantifiers_inside_forall (const std::set< variable > &variables, const data_expression &x)
 
data_expression quantifiers_inside_exists (const std::set< variable > &variables, const data_expression &x)
 
std::set< variablemake_variable_set (const variable_list &x)
 
variable_list make_variable_list (const std::set< variable > &x)
 
template<typename BinaryOperation >
std::tuple< data_expression, data_expressioncompute_Phi_Psi (const std::vector< data_expression > &X, const std::set< variable > &V, BinaryOperation op, data_expression empty_sequence_result)
 
template<typename T >
data_expression enumerator_replace (const T &x, const variable_list::const_iterator variables_begin, const variable_list::const_iterator variables_end, const data_expression_list::const_iterator expressions_begin)
 
template<typename T >
data_expression enumerator_replace (const T &x, const variable_list &variables, const data_expression_list &expressions)
 
data_equation translate_user_notation_data_equation (const data_equation &x)
 
std::ostream & operator<< (std::ostream &out, const rule &r)
 
function_symbol get_top_fs (const data_expression &expr)
 Get the top level function symbol f if expr is of the shape f or f(t1,...,tn)
 
data_expression construct_condition_rhs (const std::vector< rule > &rules, const data_expression &representative)
 For a list of rules with equal left hand sides of match_criteria and only variables in the right hand sides of match_criteria, construct a right hand side based on the conditions and right hand sides of the rules.
 
template<typename StructInfo >
data_expression construct_rhs (StructInfo &ssf, representative_generator &gen, const std::vector< rule > &rules, const sort_expression &sort)
 For a list of rules with equal left hand sides of match_criteria, construct a right hand side.
 
static bool match_jitty (const data_expression &t, const data_expression &p, jitty_assignments_for_a_rewrite_rule &assignments, const bool term_context_guarantees_normal_form)
 
static bool occur_check (const variable &v, const atermpp::aterm_appl &e)
 
static void check_vars (const data_expression &expr, const std::set< variable > &vars, std::set< variable > &used_vars)
 
static void check_vars (application::const_iterator begin, const application::const_iterator &end, const std::set< variable > &vars, std::set< variable > &used_vars)
 
static void checkPattern (const data_expression &p)
 
static void checkPattern (application::const_iterator begin, const application::const_iterator &end)
 
static bool includes (const std::set< variable > &s1, const std::set< variable > &s2, variable &culprit)
 
static bool IsPos (const core::identifier_string &Number)
 
static bool IsNat (const core::identifier_string &Number)
 
static sort_expression_list GetVarTypes (variable_list VarDecls)
 
static bool HasUnknown (const sort_expression &Type)
 
static bool IsNumericType (const sort_expression &Type)
 
static sort_expression MinType (const sort_expression_list &TypeList)
 
static sort_expression replace_possible_sorts (const sort_expression &Type)
 
template<class S >
atermpp::term_list< S > insert_sort_unique (const atermpp::term_list< S > &list, const S &el)
 

Typedef Documentation

◆ map_based_lhs_t

◆ match_tree_list

◆ match_tree_list_list

◆ match_tree_list_list_list

◆ match_tree_vector

Definition at line 546 of file match_tree.h.

◆ sort_of_variable

Function object that returns the sort of a data variable.

Definition at line 95 of file data_functional.h.

◆ variable_or_number_list

Enumeration Type Documentation

◆ Answer

A prover that uses EQ-BDDs.

\detail A class based on the Prover class that takes an expression of sort Bool in internal mCRL2 format and creates the corresponding EQ-BDD. Using this EQ-BDD, the class can determine if the original formula is a tautology or a contradiction. The term "formula" in the following text denotes arbitrary expressions of sort Bool in the mCRL2 format.

A prover uses a rewriter to rewrite parts of the formulas it manipulates. The constructor BDD_Prover::BDD_Prover initializes the prover's rewriter with the data equations in internal mCRL2 format contained in the LPS passed as parameter a_lps and the rewrite strategy passed as parameter a_rewrite_strategy. The parameter a_rewrite_strategy can be set to either GS_REWR_data::jitty or GS_REWR_data::jittyC. To limit the number of seconds spent on proving a single formula, a time limit can be set. If the time limit is set to 0, no time limit will be enforced. The parameter a_apply_induction indicates whether or induction on lists is applied. The constructor BDD_Prover::BDD_Prover has two additional parameters, a_path_eliminator and a_solver_type. The parameter a_path_eliminator can be used to enable the use of an instance of the class BDD_Path_Eliminator. Instances of this class use an SMT solver to eliminate inconsistent paths from BDDs. The parameter a_solver_type can be used to indicate which SMT solver should be used for this task. Either the SMT solver ario (http://www.eecs.umich.edu/~ario/) or cvc-lite (http://www.cs.nyu.edu/acsys/cvcl/) can be used. To use one of these solvers, the directory containing the corresponding executable must be in the path. If the parameter a_path_eliminator is set to false, the parameter a_solver_type is ignored and no instance of the class BDD_Path_Eliminator is initialized.

The formula to be handled is set using the method Prover::set_formula inherited from the class Prover. An entity of the class BDD_Prover uses binary decision diagrams to determine if a given formula is a tautology or a contradiction. The resulting BDD can be retreived using the method BDD_Prover::get_bdd.

The methods BDD_Prover::is_tautology and BDD_Prover::is_contradiction indicate whether or not a formula is a tautology or a contradiction. These methods will return answer_yes, answer_no or answer_undefined. If a formula is neither a tautology nor a contradiction according to the prover, a so called witness or counter example can be returned by the methods BDD_Prover::get_witness and BDD_Prover::get_counter_example. A witness is a valuation for which the formula holds, a counter example is a valuation for which it does not hold.

Enumerator
answer_yes 
answer_no 
answer_undefined 

Definition at line 77 of file bdd_prover.h.

◆ Compare_Result

Enumerator
compare_result_smaller 
compare_result_equal 
compare_result_bigger 

Definition at line 25 of file info.h.

◆ comparison_t

Enumerator
less 
less_eq 
equal 

Definition at line 102 of file linear_inequalities.h.

◆ node_type

Enumerator
true_end_node 
false_end_node 
intermediate_node 

Definition at line 1303 of file linear_inequalities.h.

◆ smt_solver_type

The enumeration type smt_solver_type enumerates all available SMT solvers.

Enumerator
solver_type_cvc 
solver_type_z3 

Definition at line 26 of file solver_type.h.

Function Documentation

◆ add() [1/2]

const lhs_t mcrl2::data::detail::add ( const data_expression v,
const lhs_t argument,
const rewriter r 
)
inline

Definition at line 469 of file linear_inequalities.h.

◆ add() [2/2]

const lhs_t mcrl2::data::detail::add ( const lhs_t argument,
const lhs_t e,
const rewriter r 
)
inline

Definition at line 489 of file linear_inequalities.h.

◆ add_index()

atermpp::aterm mcrl2::data::detail::add_index ( const atermpp::aterm x)
inline

Definition at line 55 of file io.h.

◆ add_index_impl()

atermpp::aterm_appl mcrl2::data::detail::add_index_impl ( const atermpp::aterm_appl x)
inline

Definition at line 39 of file io.h.

◆ apply_replace_capture_avoiding_variables_builder()

template<template< class > class Builder, template< template< class > class, class, class > class Binder, class Substitution >
replace_capture_avoiding_variables_builder< Builder, Binder, Substitution > mcrl2::data::detail::apply_replace_capture_avoiding_variables_builder ( capture_avoiding_substitution_updater< Substitution > &  sigma)

Definition at line 122 of file replace_capture_avoiding.h.

◆ apply_replace_capture_avoiding_variables_builder_with_an_identifier_generator()

template<template< class > class Builder, template< template< class > class, class, class, class > class Binder, class Substitution , class IdentifierGenerator >
replace_capture_avoiding_variables_builder_with_an_identifier_generator< Builder, Binder, Substitution, IdentifierGenerator > mcrl2::data::detail::apply_replace_capture_avoiding_variables_builder_with_an_identifier_generator ( Substitution &  sigma,
IdentifierGenerator &  id_generator 
)

◆ bool_to_numeric()

data::data_expression mcrl2::data::detail::bool_to_numeric ( data::data_expression const &  e,
data::sort_expression const &  s 
)
inline
Precondition
BoolExpr is a boolean expression, SortExpr is of type Pos, Nat, Int or
Returns
if(BoolExpr, 1, 0) of sort SortExpr

Definition at line 32 of file print_utility.h.

◆ check_assignment_variables()

bool mcrl2::data::detail::check_assignment_variables ( assignment_list const &  assignments,
variable_list const &  variables 
)
inline

Returns true if the left hand sides of assignments are contained in variables.

Parameters
assignmentsA sequence of assignments to data variables
variablesA sequence of data variables
Returns
True if the left hand sides of assignments are contained in variables.

Definition at line 62 of file data_utility.h.

◆ check_data_spec_sorts()

template<typename Container , typename SortContainer >
bool mcrl2::data::detail::check_data_spec_sorts ( const Container &  container,
const SortContainer &  sorts 
)
inline

Returns true if the domain sorts and range sort of the given functions are contained in sorts.

Parameters
rangeA sequence of data operations
sortsA set of sort expressions
Returns
True if the domain sorts and range sort of the given functions are contained in sorts.

Definition at line 190 of file data_utility.h.

◆ check_duplicate_variable_names()

void mcrl2::data::detail::check_duplicate_variable_names ( const data::variable_list x,
const std::string &  msg 
)
inline

Definition at line 27 of file variable_context.h.

◆ check_sort()

template<typename SortContainer >
bool mcrl2::data::detail::check_sort ( const sort_expression s,
const SortContainer &  sorts 
)
inline

Returns true if the domain sorts and the codomain sort of the given sort s are contained in sorts.

Parameters
sA sort expression
sortsA set of sort expressions
Returns
True if the sort is contained in sorts

Definition at line 82 of file data_utility.h.

◆ check_sorts()

template<typename Iterator , typename SortContainer >
bool mcrl2::data::detail::check_sorts ( Iterator  first,
Iterator  last,
const SortContainer &  sorts 
)

Returns true if the domain sorts and the range sort of the sorts in the sequence [first, last) are contained in sorts.

Parameters
firstStart of a sequence of sorts
lastEnd of a sequence of sorts
sortsA set of sort expressions
Returns
True if the sequence of sorts is contained in sorts

Definition at line 136 of file data_utility.h.

◆ check_variable_names()

bool mcrl2::data::detail::check_variable_names ( variable_list const &  variables,
const std::set< core::identifier_string > &  names 
)
inline

Returns true if names of the given variables are not contained in names.

Parameters
variablesA sequence of data variables
namesA set of strings
Returns
True if names of the given variables are not contained in names.

Definition at line 170 of file data_utility.h.

◆ check_variable_sorts()

template<typename VariableContainer , typename SortContainer >
bool mcrl2::data::detail::check_variable_sorts ( const VariableContainer &  variables,
const SortContainer &  sorts 
)

Returns true if the domain sorts and the range sort of the given variables are contained in sorts.

Parameters
variablesA container with data variables
sortsA set of sort expressions
Returns
True if the domain sorts and the range sort of the given variables are contained in sorts.

Definition at line 153 of file data_utility.h.

◆ check_vars() [1/2]

static void mcrl2::data::detail::check_vars ( application::const_iterator  begin,
const application::const_iterator end,
const std::set< variable > &  vars,
std::set< variable > &  used_vars 
)
static

Definition at line 546 of file rewrite.cpp.

◆ check_vars() [2/2]

static void mcrl2::data::detail::check_vars ( const data_expression expr,
const std::set< variable > &  vars,
std::set< variable > &  used_vars 
)
static

Definition at line 557 of file rewrite.cpp.

◆ check_whether_sorts_match()

template<class HEAD , class CONTAINER >
bool mcrl2::data::detail::check_whether_sorts_match ( const HEAD &  head_lambda,
const CONTAINER &  l 
)
inline

Definition at line 295 of file application.h.

◆ checkPattern() [1/2]

static void mcrl2::data::detail::checkPattern ( application::const_iterator  begin,
const application::const_iterator end 
)
static

Definition at line 580 of file rewrite.cpp.

◆ checkPattern() [2/2]

static void mcrl2::data::detail::checkPattern ( const data_expression p)
static

Definition at line 589 of file rewrite.cpp.

◆ CheckRewriteRule()

void mcrl2::data::detail::CheckRewriteRule ( const data_equation data_eqn)

Check that an mCRL2 data equation is a valid rewrite rule. If not, an runtime_error is thrown indicating the problem.

Parameters
DataEqnThe mCRL2 data equation to be checked.
Exceptions
std::runtime_errorcontaining a reason why DataEqn is not a valid rewrite rule.

Definition at line 604 of file rewrite.cpp.

◆ compare_property_maps()

template<typename PropertyMap >
bool mcrl2::data::detail::compare_property_maps ( const std::string &  message,
const PropertyMap &  map1,
const std::string &  expected_result 
)

Definition at line 302 of file data_property_map.h.

◆ compute_finite_function_sorts()

template<class Rewriter >
bool mcrl2::data::detail::compute_finite_function_sorts ( const function_sort sort,
enumerator_identifier_generator id_generator,
const data::data_specification dataspec,
Rewriter  datar,
data_expression_vector result,
variable_list function_parameter_list 
)

Computes the elements of a finite function sort, and puts them in result. If there are too many elements, false is returned.

Definition at line 109 of file enumerator.h.

◆ compute_finite_set_elements()

template<class Rewriter , class MutableSubstitution >
bool mcrl2::data::detail::compute_finite_set_elements ( const container_sort sort,
const data_specification dataspec,
Rewriter  datar,
MutableSubstitution &  sigma,
data_expression_vector result,
enumerator_identifier_generator id_generator 
)

Computes the elements of a finite set sort, and puts them in result. If there are too many elements, false is returned.

Definition at line 82 of file enumerator.h.

◆ compute_Phi_Psi()

template<typename BinaryOperation >
std::tuple< data_expression, data_expression > mcrl2::data::detail::compute_Phi_Psi ( const std::vector< data_expression > &  X,
const std::set< variable > &  V,
BinaryOperation  op,
data_expression  empty_sequence_result 
)

Definition at line 43 of file quantifiers_inside_rewriter.h.

◆ condition_part()

const data_expression & mcrl2::data::detail::condition_part ( const data_expression e)
inline

Definition at line 74 of file linear_inequalities_utilities.h.

◆ construct_condition_rhs()

data_expression mcrl2::data::detail::construct_condition_rhs ( const std::vector< rule > &  rules,
const data_expression representative 
)
inline

For a list of rules with equal left hand sides of match_criteria and only variables in the right hand sides of match_criteria, construct a right hand side based on the conditions and right hand sides of the rules.

Definition at line 108 of file unfold_pattern_matching.h.

◆ construct_rhs()

template<typename StructInfo >
data_expression mcrl2::data::detail::construct_rhs ( StructInfo &  ssf,
representative_generator gen,
const std::vector< rule > &  rules,
const sort_expression sort 
)

For a list of rules with equal left hand sides of match_criteria, construct a right hand side.

Definition at line 154 of file unfold_pattern_matching.h.

◆ contains_untyped_sort()

bool mcrl2::data::detail::contains_untyped_sort ( const sort_expression s)
inline

Definition at line 239 of file application.h.

◆ create_finite_set()

data_expression mcrl2::data::detail::create_finite_set ( const data_expression x)
inline

Create the finite set { x }, with x a data expression.

Definition at line 26 of file data_construction.h.

◆ create_set_comprehension()

data_expression mcrl2::data::detail::create_set_comprehension ( const variable x,
const data_expression phi 
)
inline

Create the set { x | phi }, with phi a predicate that may depend on the variable x.

Definition at line 36 of file data_construction.h.

◆ create_set_in()

data_expression mcrl2::data::detail::create_set_in ( const data_expression x,
const data_expression X 
)
inline

Create the predicate 'x in X', with X a set.

Definition at line 45 of file data_construction.h.

◆ create_strategy()

strategy mcrl2::data::detail::create_strategy ( data_equation_list  rules)

Creates a strategy for given set of rewrite rules with head symbol f.

◆ createRewriter()

std::shared_ptr< Rewriter > mcrl2::data::detail::createRewriter ( const data_specification DataSpec,
const used_data_equation_selector equations_selector,
const rewrite_strategy  Strategy = jitty 
)

Create a rewriter.

Parameters
DataSpecA data specification.
StrategyThe rewrite strategy to be used by the rewriter.
Returns
A (pointer to a) rewriter that uses the data specification DataSpec and strategy Strategy to rewrite.

Definition at line 520 of file rewrite.cpp.

◆ data_rewrite() [1/2]

template<typename DataRewriter >
data::data_expression mcrl2::data::detail::data_rewrite ( const data::data_expression x,
const DataRewriter &  R,
data::no_substitution  
)

Definition at line 32 of file data_rewriter.h.

◆ data_rewrite() [2/2]

template<typename DataRewriter , typename SubstitutionFunction >
data::data_expression mcrl2::data::detail::data_rewrite ( const data::data_expression x,
const DataRewriter &  R,
SubstitutionFunction &  sigma 
)

Definition at line 25 of file data_rewriter.h.

◆ data_specification_to_aterm()

atermpp::aterm_appl mcrl2::data::detail::data_specification_to_aterm ( const data_specification s)
Returns
A term that represetns this data_specification.

Definition at line 44 of file data_io.cpp.

◆ default_specification()

static data_specification const & mcrl2::data::detail::default_specification ( )
inlinestatic

Definition at line 31 of file parse.h.

◆ description()

std::string mcrl2::data::detail::description ( const smt_solver_type  s)
inline

description of solver type

Definition at line 79 of file solver_type.h.

◆ display_rewrite_statistics()

void mcrl2::data::detail::display_rewrite_statistics ( )
inline

Definition at line 42 of file rewrite_statistics.h.

◆ divide()

const lhs_t mcrl2::data::detail::divide ( const lhs_t argument,
const data_expression v,
const rewriter r 
)
inline

Definition at line 484 of file linear_inequalities.h.

◆ else_part()

const data_expression & mcrl2::data::detail::else_part ( const data_expression e)
inline

Definition at line 90 of file linear_inequalities_utilities.h.

◆ emplace_back_if_not_zero()

void mcrl2::data::detail::emplace_back_if_not_zero ( std::vector< detail::variable_with_a_rational_factor > &  r,
const variable v,
const data_expression f 
)
inline

Definition at line 394 of file linear_inequalities.h.

◆ enumerator_replace() [1/2]

template<typename T >
data_expression mcrl2::data::detail::enumerator_replace ( const T &  x,
const variable_list variables,
const data_expression_list expressions 
)
inline

Definition at line 89 of file enumerator_substitution.h.

◆ enumerator_replace() [2/2]

template<typename T >
data_expression mcrl2::data::detail::enumerator_replace ( const T &  x,
const variable_list::const_iterator  variables_begin,
const variable_list::const_iterator  variables_end,
const data_expression_list::const_iterator  expressions_begin 
)
inline

Definition at line 76 of file enumerator_substitution.h.

◆ equal_sorts()

bool mcrl2::data::detail::equal_sorts ( const data::variable_list v,
const data::data_expression_list w,
const data::data_specification data_spec 
)
inline

Checks if the sorts of the variables/expressions in both lists are equal.

Parameters
vA sequence of data variables
wA sequence of data expressions
Returns
True if the sorts match pairwise

Definition at line 28 of file equal_sorts.h.

◆ evaluate_lambda_data_expression() [1/3]

const data_expression & mcrl2::data::detail::evaluate_lambda_data_expression ( const data_expression t)
inline

Definition at line 271 of file application.h.

◆ evaluate_lambda_data_expression() [2/3]

template<class TERM >
data_expression mcrl2::data::detail::evaluate_lambda_data_expression ( const TERM &  t,
typename std::enable_if< std::is_invocable_r< const data_expression, TERM, void >::value >::type *  = nullptr 
)
inline

Definition at line 287 of file application.h.

◆ evaluate_lambda_data_expression() [3/3]

template<class TERM >
data_expression mcrl2::data::detail::evaluate_lambda_data_expression ( const TERM &  t,
typename std::enable_if< std::is_invocable_r< void, TERM, data_expression & >::value >::type *  = nullptr 
)
inline

Definition at line 277 of file application.h.

◆ f_variable_with_a_rational_factor()

atermpp::function_symbol mcrl2::data::detail::f_variable_with_a_rational_factor ( )
inline

Definition at line 128 of file linear_inequalities.h.

◆ get_argument_of_higher_order_term()

const data_expression & mcrl2::data::detail::get_argument_of_higher_order_term ( const application t,
std::size_t  i 
)
inline

Definition at line 108 of file jitty_jittyc.h.

◆ get_argument_of_higher_order_term_helper()

const data_expression * mcrl2::data::detail::get_argument_of_higher_order_term_helper ( const application t,
std::size_t &  i 
)
inline

Definition at line 76 of file jitty_jittyc.h.

◆ get_arguments() [1/2]

data_expression_list mcrl2::data::detail::get_arguments ( )
inline

Definition at line 328 of file application.h.

◆ get_arguments() [2/2]

template<class HEAD , class... ARGUMENTS>
data_expression_list mcrl2::data::detail::get_arguments ( const HEAD &  h,
const ARGUMENTS &...  args 
)
inline

Definition at line 335 of file application.h.

◆ get_direct_arity()

std::size_t mcrl2::data::detail::get_direct_arity ( const data::function_symbol op)
inline

Definition at line 290 of file rewrite.h.

◆ get_enumerator_iteration_limit()

std::size_t mcrl2::data::detail::get_enumerator_iteration_limit ( )
inline

Definition at line 42 of file enumerator_iteration_limit.h.

◆ get_free_vars()

variable_list mcrl2::data::detail::get_free_vars ( const data_expression a)
inline

Definition at line 49 of file jitty_jittyc.h.

◆ get_nested_head()

const data_expression & mcrl2::data::detail::get_nested_head ( const data_expression t)
inline

Definition at line 160 of file jitty_jittyc.h.

◆ get_nested_head_helper()

const data_expression & mcrl2::data::detail::get_nested_head_helper ( const application t)
inline

Definition at line 149 of file jitty_jittyc.h.

◆ get_set_sort()

sort_expression mcrl2::data::detail::get_set_sort ( const container_sort x)
inline

Returns the sort s of Set(s).

Parameters
xA set expression

Definition at line 54 of file data_construction.h.

◆ get_test_rewrite_strategies()

const std::vector< data::rewrite_strategy > & mcrl2::data::detail::get_test_rewrite_strategies ( const bool  with_prover)
inline

Rewrite strategies that should be tested.

Definition at line 55 of file rewrite_strategies.h.

◆ get_top_fs()

function_symbol mcrl2::data::detail::get_top_fs ( const data_expression expr)
inline

Get the top level function symbol f if expr is of the shape f or f(t1,...,tn)

Parameters
exprThe expression from which to extract the top function symbol
Returns
The top function symbol, or function_symbol() if it has none

Definition at line 85 of file unfold_pattern_matching.h.

◆ getArity()

std::size_t mcrl2::data::detail::getArity ( const data::function_symbol op)
inline

Definition at line 274 of file rewrite.h.

◆ GetVarTypes()

static sort_expression_list mcrl2::data::detail::GetVarTypes ( variable_list  VarDecls)
static

Definition at line 4509 of file typecheck.cpp.

◆ HasUnknown()

static bool mcrl2::data::detail::HasUnknown ( const sort_expression Type)
static

Definition at line 4562 of file typecheck.cpp.

◆ I()

data_expression mcrl2::data::detail::I ( const data_expression x)
inline

Definition at line 248 of file test_rewriters.h.

◆ includes()

static bool mcrl2::data::detail::includes ( const std::set< variable > &  s1,
const std::set< variable > &  s2,
variable culprit 
)
static

Definition at line 32 of file typecheck.cpp.

◆ increment_rewrite_count()

void mcrl2::data::detail::increment_rewrite_count ( )
inline

Definition at line 48 of file rewrite_statistics.h.

◆ initialise_test_rewrite_strategies()

static std::vector< data::rewrite_strategy > mcrl2::data::detail::initialise_test_rewrite_strategies ( const bool  with_prover)
inlinestatic

Static initialisation of rewrite strategies used for testing.

Definition at line 32 of file rewrite_strategies.h.

◆ insert_sort_unique()

template<class S >
atermpp::term_list< S > mcrl2::data::detail::insert_sort_unique ( const atermpp::term_list< S > &  list,
const S &  el 
)
inline

Definition at line 63 of file typecheck.cpp.

◆ is_and()

bool mcrl2::data::detail::is_and ( const application x)
inline

Definition at line 153 of file print.h.

◆ is_bag_difference()

bool mcrl2::data::detail::is_bag_difference ( const application x)
inline

Definition at line 147 of file print.h.

◆ is_bag_intersection()

bool mcrl2::data::detail::is_bag_intersection ( const application x)
inline

Definition at line 228 of file print.h.

◆ is_bag_join()

bool mcrl2::data::detail::is_bag_join ( const application x)
inline

Definition at line 141 of file print.h.

◆ is_concat()

bool mcrl2::data::detail::is_concat ( const application x)
inline

Definition at line 234 of file print.h.

◆ is_cons()

bool mcrl2::data::detail::is_cons ( const application x)
inline

Definition at line 260 of file print.h.

◆ is_cons_list()

bool mcrl2::data::detail::is_cons_list ( data_expression  x)
inline

Definition at line 240 of file print.h.

◆ is_div()

bool mcrl2::data::detail::is_div ( const application x)
inline

Definition at line 95 of file print.h.

◆ is_divides()

bool mcrl2::data::detail::is_divides ( const application x)
inline

Definition at line 114 of file print.h.

◆ is_divmod()

bool mcrl2::data::detail::is_divmod ( const application x)
inline

Definition at line 105 of file print.h.

◆ is_element_at()

bool mcrl2::data::detail::is_element_at ( const application x)
inline

Definition at line 216 of file print.h.

◆ is_enumerable()

template<typename Rewriter >
bool mcrl2::data::detail::is_enumerable ( const data_specification dataspec,
const Rewriter rewr,
const sort_expression sort,
std::list< sort_expression > &  parents 
)

Definition at line 159 of file enumerator.h.

◆ is_equal_to()

bool mcrl2::data::detail::is_equal_to ( const application x)
inline

Definition at line 165 of file print.h.

◆ is_greater()

bool mcrl2::data::detail::is_greater ( const application x)
inline

Definition at line 189 of file print.h.

◆ is_greater_equal()

bool mcrl2::data::detail::is_greater_equal ( const application x)
inline

Definition at line 195 of file print.h.

◆ is_implies()

bool mcrl2::data::detail::is_implies ( const application x)
inline

Definition at line 123 of file print.h.

◆ is_in()

bool mcrl2::data::detail::is_in ( const application x)
inline

Definition at line 201 of file print.h.

◆ is_inequality()

bool mcrl2::data::detail::is_inequality ( const data_expression e)
inline

Determine whether a data expression is an inequality.

Parameters
eA data expression
Returns
true iff e is a data application of ==, <, <=, > or >= to two arguments.

Definition at line 66 of file linear_inequalities_utilities.h.

◆ is_less()

bool mcrl2::data::detail::is_less ( const application x)
inline

Definition at line 177 of file print.h.

◆ is_less_equal()

bool mcrl2::data::detail::is_less_equal ( const application x)
inline

Definition at line 183 of file print.h.

◆ is_minus()

bool mcrl2::data::detail::is_minus ( const application x)
inline

Definition at line 75 of file print.h.

◆ is_mod()

bool mcrl2::data::detail::is_mod ( const application x)
inline

Definition at line 85 of file print.h.

◆ is_nat()

bool mcrl2::data::detail::is_nat ( const core::identifier_string Number)
inline

Definition at line 31 of file type_checker.h.

◆ is_not_equal_to()

bool mcrl2::data::detail::is_not_equal_to ( const application x)
inline

Definition at line 171 of file print.h.

◆ is_numeric_cast()

bool mcrl2::data::detail::is_numeric_cast ( const data_expression x)
inline

Definition at line 29 of file print.h.

◆ is_numeric_sort()

bool mcrl2::data::detail::is_numeric_sort ( const sort_expression x)
inline

Definition at line 27 of file is_sub_sort.h.

◆ is_numeric_type()

bool mcrl2::data::detail::is_numeric_type ( const sort_expression x)
inline

Definition at line 83 of file type_checker.h.

◆ is_or()

bool mcrl2::data::detail::is_or ( const application x)
inline

Definition at line 159 of file print.h.

◆ is_plus()

bool mcrl2::data::detail::is_plus ( const application x)
inline

Definition at line 63 of file print.h.

◆ is_pos()

bool mcrl2::data::detail::is_pos ( const core::identifier_string Number)
inline

Definition at line 24 of file type_checker.h.

◆ is_set_difference()

bool mcrl2::data::detail::is_set_difference ( const application x)
inline

Definition at line 135 of file print.h.

◆ is_set_intersection()

bool mcrl2::data::detail::is_set_intersection ( const application x)
inline

Definition at line 222 of file print.h.

◆ is_set_union()

bool mcrl2::data::detail::is_set_union ( const application x)
inline

Definition at line 129 of file print.h.

◆ is_snoc()

bool mcrl2::data::detail::is_snoc ( const application x)
inline

Definition at line 266 of file print.h.

◆ is_snoc_list()

bool mcrl2::data::detail::is_snoc_list ( data_expression  x)
inline

Definition at line 250 of file print.h.

◆ is_times()

bool mcrl2::data::detail::is_times ( const application x)
inline

Definition at line 207 of file print.h.

◆ is_untyped()

bool mcrl2::data::detail::is_untyped ( const data_expression x)
inline

Definition at line 73 of file is_untyped.h.

◆ is_well_formed()

bool mcrl2::data::detail::is_well_formed ( const lhs_t lhs)
inline

Definition at line 354 of file linear_inequalities.h.

◆ IsNat()

static bool mcrl2::data::detail::IsNat ( const core::identifier_string Number)
inlinestatic

Definition at line 50 of file typecheck.cpp.

◆ IsNumericType()

static bool mcrl2::data::detail::IsNumericType ( const sort_expression Type)
static

Definition at line 4595 of file typecheck.cpp.

◆ IsPos()

static bool mcrl2::data::detail::IsPos ( const core::identifier_string Number)
inlinestatic

Definition at line 45 of file typecheck.cpp.

◆ isValidRewriteRule()

bool mcrl2::data::detail::isValidRewriteRule ( const data_equation data_eqn)

Check whether or not an mCRL2 data equation is a valid rewrite rule.

Parameters
DataEqnThe mCRL2 data equation to be checked.
Returns
Whether or not DataEqn is a valid rewrite rule.

Definition at line 662 of file rewrite.cpp.

◆ linear_inequality_equal()

atermpp::function_symbol mcrl2::data::detail::linear_inequality_equal ( )
inline

Definition at line 548 of file linear_inequalities.h.

◆ linear_inequality_less()

atermpp::function_symbol mcrl2::data::detail::linear_inequality_less ( )
inline

Definition at line 534 of file linear_inequalities.h.

◆ linear_inequality_less_equal()

atermpp::function_symbol mcrl2::data::detail::linear_inequality_less_equal ( )
inline

Definition at line 541 of file linear_inequalities.h.

◆ look_through_numeric_casts()

bool mcrl2::data::detail::look_through_numeric_casts ( const data_expression x,
std::function< bool(const data_expression &)>  f 
)
inline

Definition at line 43 of file print.h.

◆ make_apply_rewriter_builder()

template<template< class, class, class > class Builder, class DataRewriter , class SubstitutionFunction >
apply_rewriter_builder< Builder, DataRewriter, SubstitutionFunction > mcrl2::data::detail::make_apply_rewriter_builder ( const DataRewriter &  datar,
SubstitutionFunction &  sigma 
)

Definition at line 99 of file data_rewriter.h.

◆ make_function_sort_()

function_sort mcrl2::data::detail::make_function_sort_ ( const sort_expression domain,
const sort_expression codomain 
)
inline

Definition at line 37 of file type_checker.h.

◆ make_if_expression_()

data_expression mcrl2::data::detail::make_if_expression_ ( std::size_t &  function_index,
const std::size_t  argument_index,
const std::vector< data_expression_vector > &  data_domain_expressions,
const data_expression_vector codomain_expressions,
const variable_vector parameters 
)
inline

Definition at line 47 of file enumerator.h.

◆ make_rewrite_data_expressions_builder()

template<template< class > class Builder, class Rewriter >
rewrite_data_expressions_builder< Builder, Rewriter > mcrl2::data::detail::make_rewrite_data_expressions_builder ( Rewriter  R)

Definition at line 48 of file rewrite.h.

◆ make_rewrite_data_expressions_with_substitution_builder()

template<template< class > class Builder, class Rewriter , class Substitution >
rewrite_data_expressions_with_substitution_builder< Builder, Rewriter, Substitution > mcrl2::data::detail::make_rewrite_data_expressions_with_substitution_builder ( Rewriter  R,
Substitution  sigma 
)

Definition at line 79 of file rewrite.h.

◆ make_set()

template<class Container >
std::set< typename Container::value_type > mcrl2::data::detail::make_set ( const Container &  c)

Makes a set of the given container.

Parameters
cA container
Returns
A set containing the elements of the container

Definition at line 80 of file sequence_algorithm.h.

◆ make_set_()

data_expression mcrl2::data::detail::make_set_ ( std::size_t  function_index,
const sort_expression element_sort,
const data_expression_vector set_elements 
)
inline

Definition at line 32 of file enumerator.h.

◆ make_variable_list()

variable_list mcrl2::data::detail::make_variable_list ( const std::set< variable > &  x)
inline

Definition at line 37 of file quantifiers_inside_rewriter.h.

◆ make_variable_set()

std::set< variable > mcrl2::data::detail::make_variable_set ( const variable_list x)
inline

Definition at line 31 of file quantifiers_inside_rewriter.h.

◆ map_to_lhs_type() [1/2]

const lhs_t mcrl2::data::detail::map_to_lhs_type ( const map_based_lhs_t lhs)
inline

Definition at line 333 of file linear_inequalities.h.

◆ map_to_lhs_type() [2/2]

const lhs_t mcrl2::data::detail::map_to_lhs_type ( const map_based_lhs_t lhs,
const data_expression factor,
const rewriter r 
)
inline

Definition at line 343 of file linear_inequalities.h.

◆ match_jitty()

static bool mcrl2::data::detail::match_jitty ( const data_expression t,
const data_expression p,
jitty_assignments_for_a_rewrite_rule assignments,
const bool  term_context_guarantees_normal_form 
)
static

Definition at line 322 of file jitty.cpp.

◆ meta_operation_constant()

template<application Operation>
const lhs_t mcrl2::data::detail::meta_operation_constant ( const lhs_t argument,
const data_expression v,
const rewriter r 
)
inline

Definition at line 404 of file linear_inequalities.h.

◆ meta_operation_lhs()

template<class OPERATION >
lhs_t mcrl2::data::detail::meta_operation_lhs ( const lhs_t argument1,
const lhs_t argument2,
OPERATION  operation,
const rewriter r 
)
inline

Definition at line 418 of file linear_inequalities.h.

◆ MinType()

static sort_expression mcrl2::data::detail::MinType ( const sort_expression_list TypeList)
static

Definition at line 4611 of file typecheck.cpp.

◆ multiply()

const lhs_t mcrl2::data::detail::multiply ( const lhs_t argument,
const data_expression v,
const rewriter r 
)
inline

Definition at line 479 of file linear_inequalities.h.

◆ N()

template<typename Function >
normalizer< Function > mcrl2::data::detail::N ( const Function &  f)

Definition at line 187 of file test_rewriters.h.

◆ negate()

detail::comparison_t mcrl2::data::detail::negate ( const detail::comparison_t  t)
inline

Definition at line 106 of file linear_inequalities.h.

◆ negate_inequality()

data_expression mcrl2::data::detail::negate_inequality ( const data_expression e)
inline

Definition at line 28 of file linear_inequalities_utilities.h.

◆ normalize_and_or() [1/2]

template<typename T >
T mcrl2::data::detail::normalize_and_or ( const T &  x,
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

Definition at line 86 of file test_rewriters.h.

◆ normalize_and_or() [2/2]

template<typename T >
void mcrl2::data::detail::normalize_and_or ( T &  x,
typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *  = 0 
)

Definition at line 96 of file test_rewriters.h.

◆ normalize_equality() [1/2]

template<typename T >
T mcrl2::data::detail::normalize_equality ( const T &  x,
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

Definition at line 152 of file test_rewriters.h.

◆ normalize_equality() [2/2]

template<typename T >
void mcrl2::data::detail::normalize_equality ( T &  x,
typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *  = 0 
)

Definition at line 162 of file test_rewriters.h.

◆ numeric_sort_value()

std::size_t mcrl2::data::detail::numeric_sort_value ( const sort_expression x)
inline

Definition at line 33 of file is_sub_sort.h.

◆ occur_check()

static bool mcrl2::data::detail::occur_check ( const variable v,
const atermpp::aterm_appl e 
)
static

Definition at line 44 of file rewrite.cpp.

◆ operator<<() [1/5]

std::ostream & mcrl2::data::detail::operator<< ( std::ostream &  os,
smt_solver_type  s 
)
inline

standard conversion from solvert type to stream

Definition at line 71 of file solver_type.h.

◆ operator<<() [2/5]

template<typename Substitution >
std::ostream & mcrl2::data::detail::operator<< ( std::ostream &  out,
const capture_avoiding_substitution_updater< Substitution > &  sigma 
)

Definition at line 96 of file replace_capture_avoiding.h.

◆ operator<<() [3/5]

std::ostream & mcrl2::data::detail::operator<< ( std::ostream &  out,
const find_equalities_expression x 
)
inline

Definition at line 216 of file find_equalities.h.

◆ operator<<() [4/5]

std::ostream & mcrl2::data::detail::operator<< ( std::ostream &  out,
const rule r 
)
inline

Definition at line 75 of file unfold_pattern_matching.h.

◆ operator<<() [5/5]

std::ostream & mcrl2::data::detail::operator<< ( std::ostream &  s,
const match_tree t 
)
inline

Definition at line 576 of file match_tree.h.

◆ operator>>()

std::istream & mcrl2::data::detail::operator>> ( std::istream &  is,
smt_solver_type s 
)
inline

standard conversion from stream to solver type

Definition at line 43 of file solver_type.h.

◆ optimized_and()

template<typename TermTraits >
void mcrl2::data::detail::optimized_and ( typename TermTraits::term_type &  result,
const typename TermTraits::term_type &  left,
const typename TermTraits::term_type &  right,
TermTraits   
)
inline

Make a conjunction and optimize it if possible.

Parameters
leftA term
rightA term
Returns
The value left && right

Definition at line 59 of file optimized_boolean_operators.h.

◆ optimized_exists()

template<typename TermTraits >
void mcrl2::data::detail::optimized_exists ( typename TermTraits::term_type &  result,
const typename TermTraits::variable_sequence_type &  v,
const typename TermTraits::term_type &  arg,
bool  remove_variables,
bool  empty_domain_allowed,
TermTraits   
)
inline

Make an existential quantification.

Parameters
vA sequence of variables
argA term
remove_variablesIf true, remove bound variables that do not occur in arg.
empty_domain_allowedIf true, and there are no variables in v, treat as empty domain, hence yielding false, otherwise arg arg is returned in this case.
Returns
The existential quantification exists v.arg

Definition at line 270 of file optimized_boolean_operators.h.

◆ optimized_forall()

template<typename TermTraits >
void mcrl2::data::detail::optimized_forall ( typename TermTraits::term_type &  result,
const typename TermTraits::variable_sequence_type &  v,
const typename TermTraits::term_type &  arg,
bool  remove_variables,
bool  empty_domain_allowed,
TermTraits   
)
inline

Make a universal quantification.

Parameters
vA sequence of variables
argA term
remove_variablesIf true, remove bound variables that do not occur in arg.
empty_domain_allowedIf true, and there are no variables in v, treat as empty domain, hence yielding true, otherwise arg arg is returned in this case.
Returns
The universal quantification forall v.arg

Definition at line 212 of file optimized_boolean_operators.h.

◆ optimized_imp()

template<typename TermTraits >
void mcrl2::data::detail::optimized_imp ( typename TermTraits::term_type &  result,
const typename TermTraits::term_type &  left,
const typename TermTraits::term_type &  right,
TermTraits  t 
)
inline

Make an implication.

Parameters
leftA term
rightA term
Returns
The value left => right

Definition at line 170 of file optimized_boolean_operators.h.

◆ optimized_not()

template<typename TermTraits >
void mcrl2::data::detail::optimized_not ( typename TermTraits::term_type &  result,
const typename TermTraits::term_type &  arg,
TermTraits   
)
inline
Returns
The value !arg

Definition at line 29 of file optimized_boolean_operators.h.

◆ optimized_or()

template<typename TermTraits >
void mcrl2::data::detail::optimized_or ( typename TermTraits::term_type &  result,
const typename TermTraits::term_type &  left,
const typename TermTraits::term_type &  right,
TermTraits   
)
inline

Make a disjunction.

Parameters
leftA term
rightA term
Returns
The value left || right

Definition at line 132 of file optimized_boolean_operators.h.

◆ parameter_sorts()

template<typename Container >
data::sort_expression_list mcrl2::data::detail::parameter_sorts ( const Container &  parameters)

Returns the sorts of a sequence of parameters.

Definition at line 32 of file data_utility.h.

◆ parse_data_expression()

data_expression mcrl2::data::detail::parse_data_expression ( const std::string &  text)

Definition at line 217 of file data.cpp.

◆ parse_data_specification_new()

data_specification mcrl2::data::detail::parse_data_specification_new ( const std::string &  text)

Definition at line 228 of file data.cpp.

◆ parse_solver_type()

smt_solver_type mcrl2::data::detail::parse_solver_type ( const std::string &  s)
inline

standard conversion from string to solver type

Definition at line 34 of file solver_type.h.

◆ parse_sort_expression()

sort_expression mcrl2::data::detail::parse_sort_expression ( const std::string &  text)

Definition at line 196 of file data.cpp.

◆ parse_substitution()

template<typename MutableSubstitution >
void mcrl2::data::detail::parse_substitution ( std::string  text,
MutableSubstitution &  sigma,
const data_specification data_spec = data::data_specification() 
)

Parses a string of the form "b: Bool := true, n: Nat := 0", and adds the substitutions to the substition function sigma. If the string is surrounded by brackets (e.g. "[b: Bool := true, n: Nat := 0]"), these are ignored.

Definition at line 30 of file parse_substitution.h.

◆ parse_variable_declaration_list()

variable_list mcrl2::data::detail::parse_variable_declaration_list ( const std::string &  text)

Definition at line 239 of file data.cpp.

◆ parse_variables()

variable_list mcrl2::data::detail::parse_variables ( const std::string &  text)

Definition at line 206 of file data.cpp.

◆ pp() [1/2]

std::string mcrl2::data::detail::pp ( const detail::comparison_t  t)
inline

Definition at line 117 of file linear_inequalities.h.

◆ pp() [2/2]

std::string mcrl2::data::detail::pp ( const detail::lhs_t lhs)
inline

Definition at line 507 of file linear_inequalities.h.

◆ print_parse_check() [1/2]

void mcrl2::data::detail::print_parse_check ( const data_expression x,
const data_specification dataspec = data_specification() 
)
inline

Definition at line 39 of file print_parse_check.h.

◆ print_parse_check() [2/2]

void mcrl2::data::detail::print_parse_check ( const sort_expression x,
const data_specification dataspec = data_specification() 
)
inline

Definition at line 25 of file print_parse_check.h.

◆ print_solver_type()

std::string mcrl2::data::detail::print_solver_type ( const smt_solver_type  s)
inline

standard conversion from solver type to string

Definition at line 60 of file solver_type.h.

◆ push_if_outside()

data_expression mcrl2::data::detail::push_if_outside ( const application x)
inline

Definition at line 35 of file if_rewriter.h.

◆ quantifiers_inside()

data_expression mcrl2::data::detail::quantifiers_inside ( const data_expression x)
inline

Definition at line 283 of file quantifiers_inside_rewriter.h.

◆ quantifiers_inside_exists()

data_expression mcrl2::data::detail::quantifiers_inside_exists ( const std::set< variable > &  variables,
const data_expression x 
)
inline

Definition at line 301 of file quantifiers_inside_rewriter.h.

◆ quantifiers_inside_forall()

data_expression mcrl2::data::detail::quantifiers_inside_forall ( const std::set< variable > &  variables,
const data_expression x 
)
inline

Definition at line 292 of file quantifiers_inside_rewriter.h.

◆ reconstruct_pos_mult()

data_expression mcrl2::data::detail::reconstruct_pos_mult ( const data_expression x,
std::vector< char > &  result 
)
inline

Definition at line 39 of file print_utility.h.

◆ recursive_number_of_args()

std::size_t mcrl2::data::detail::recursive_number_of_args ( const data_expression t)
inline

Definition at line 128 of file jitty_jittyc.h.

◆ remove_index()

atermpp::aterm mcrl2::data::detail::remove_index ( const atermpp::aterm x)
inline

Definition at line 61 of file io.h.

◆ remove_index_impl()

atermpp::aterm_appl mcrl2::data::detail::remove_index_impl ( const atermpp::aterm_appl x)
inline

Definition at line 28 of file io.h.

◆ remove_normal_form_function()

data_expression mcrl2::data::detail::remove_normal_form_function ( const data_expression t)

removes auxiliary expressions this_term_is_in_normal_form from data_expressions that are being rewritten.

The function below is intended to remove the auxiliary function this_term_is_in_normal_form from a term such that it can for instance be pretty printed. This auxiliary function is used internally in terms when rewriting to avoid to rewrite too often.

◆ remove_variable_and_divide()

const lhs_t mcrl2::data::detail::remove_variable_and_divide ( const lhs_t lhs,
const variable v,
const data_expression f,
const rewriter r 
)
inline

Definition at line 381 of file linear_inequalities.h.

◆ replace_argument()

application mcrl2::data::detail::replace_argument ( const application x,
std::size_t  i,
const data_expression y 
)
inline

Definition at line 28 of file if_rewriter.h.

◆ replace_nested_head()

const data_expression mcrl2::data::detail::replace_nested_head ( const data_expression t,
const data_expression head 
)
inline

Definition at line 184 of file jitty_jittyc.h.

◆ replace_possible_sorts()

static sort_expression mcrl2::data::detail::replace_possible_sorts ( const sort_expression Type)
static

Definition at line 4521 of file typecheck.cpp.

◆ residual_sort()

sort_expression mcrl2::data::detail::residual_sort ( const sort_expression s,
std::size_t  no_of_initial_arguments 
)
inline

Definition at line 55 of file jitty_jittyc.h.

◆ rewrite_all_arguments()

template<class ARGUMENT_REWRITER >
void mcrl2::data::detail::rewrite_all_arguments ( data_expression result,
const application t,
const ARGUMENT_REWRITER  rewriter 
)
inline

Definition at line 196 of file jitty_jittyc.h.

◆ rewrite_count()

std::size_t mcrl2::data::detail::rewrite_count ( )
inline

Definition at line 36 of file rewrite_statistics.h.

◆ sequence_contains_duplicates()

template<typename Iterator >
bool mcrl2::data::detail::sequence_contains_duplicates ( Iterator  first,
Iterator  last 
)

Returns true if the sequence [first, last) contains duplicates.

Parameters
firstStart of a sequence
lastEnd of a sequence
Returns
True if the sequence [first, last) contains duplicates.

Definition at line 34 of file sequence_algorithm.h.

◆ sequence_empty_intersection()

template<typename Sequence >
bool mcrl2::data::detail::sequence_empty_intersection ( Sequence  s1,
Sequence  s2 
)

Determines if the unordered sequences s1 and s2 have an empty intersection.

Parameters
s1A sequence
s2A sequence
Returns
True if the intersection of s1 and s2 is empty

Definition at line 92 of file sequence_algorithm.h.

◆ sequence_is_subset_of_set()

template<typename Iterator , typename T >
bool mcrl2::data::detail::sequence_is_subset_of_set ( Iterator  first,
Iterator  last,
const std::set< T > &  s 
)

Returns true if all elements of the range [first, last) are element of the set s.

Parameters
firstStart of a sequence
lastEnd of a sequence
sA set
Returns
True if all elements of the range [first, last) are element of the set s.

Definition at line 64 of file sequence_algorithm.h.

◆ sequences_do_overlap()

template<typename Iterator1 , typename Iterator2 >
bool mcrl2::data::detail::sequences_do_overlap ( Iterator1  first1,
Iterator1  last1,
Iterator2  first2,
Iterator2  last2 
)

Returns true if the two sequences [first1, last1) and [first2, last2) have a non empty intersection.

Parameters
first1Start of a sequence
last1End of a sequence
first2Start of a sequence
last2End of a sequence
Returns
True if the two sequences [first1, last1) and [first2, last2) have a non empty intersection.

Definition at line 48 of file sequence_algorithm.h.

◆ set_difference()

variable_list mcrl2::data::detail::set_difference ( const variable_list x,
const variable_list y 
)
inline

Returns the difference of two unordered sets, that are stored in aterm lists.

Parameters
xA sequence of data variables
yA sequence of data variables
Returns
The difference of two sets.

Definition at line 54 of file data_sequence_algorithm.h.

◆ set_enumerator_iteration_limit()

void mcrl2::data::detail::set_enumerator_iteration_limit ( std::size_t  size)
inline

Definition at line 36 of file enumerator_iteration_limit.h.

◆ set_factor_for_a_variable() [1/2]

lhs_t mcrl2::data::detail::set_factor_for_a_variable ( const lhs_t lhs,
const variable x,
const data_expression e 
)
inline

Definition at line 307 of file linear_inequalities.h.

◆ set_factor_for_a_variable() [2/2]

void mcrl2::data::detail::set_factor_for_a_variable ( detail::map_based_lhs_t new_lhs,
const variable x,
const data_expression e 
)
inline

Definition at line 290 of file linear_inequalities.h.

◆ set_intersection()

variable_list mcrl2::data::detail::set_intersection ( const variable_list x,
const variable_list y 
)
inline

Returns the intersection of two unordered sets, that are stored in ATerm lists.

Parameters
xA sequence of data variables
yA sequence of data variables
Returns
The intersection of two sets.

Definition at line 31 of file data_sequence_algorithm.h.

◆ split_condition()

void mcrl2::data::detail::split_condition ( const data_expression e,
std::vector< data_expression_list > &  real_conditions,
std::vector< data_expression > &  non_real_conditions 
)
inline

This function first splits the given condition e into real conditions and non real conditions. \detail This function first uses split_condition_aux to split the condition e. Then.

Definition at line 230 of file linear_inequalities_utilities.h.

◆ split_condition_aux()

static bool mcrl2::data::detail::split_condition_aux ( const data_expression e,
std::vector< data_expression_list > &  real_conditions,
std::vector< data_expression_list > &  non_real_conditions,
const bool  negate = false 
)
static

Splits a condition in expressions ranging over reals and the others.

Conceptually, the condition is first transformed to disjunctive normal form. For each disjunct, there will be an entry in both resulting std::vectors, where the real conditions are in "real_conditions", and the others in non_real_conditions. If there are conjuncts with both real and non-real variables an exception is thrown. If negate is true the result will be negated.

Parameters
eA data expression of sort bool.
real_conditionThose parts of e with only variables over sort Real.
non_real_conditionThose parts of e with only variables not of sort Real.
negateA boolean variable that indicates whether the result must be negated.
Returns
True when e contains real variables
Precondition
The parameter e must be of sort Bool.

Definition at line 114 of file linear_inequalities_utilities.h.

◆ split_enumerable_variables()

template<typename Rewriter , typename FILTER >
void mcrl2::data::detail::split_enumerable_variables ( data::variable_list  variables,
const data::data_specification data,
const Rewriter rewr,
data::variable_list enumerable_variables,
data::variable_list non_enumerable_variables,
data::variable_list unused,
const FILTER  filter 
)
inline

Splits a list of variables in those that are enumerable, non enumerable and not used, according to a filter.

Parameters
variablesA sequence of data variables.
dataA data specification.
rewrA data rewriter to determine which elements are enumerable.
finite_variablesA sequence of data variables.
infinite_variablesA sequence of data variables.
unusedA sequence of data variables that do not pass the filter.
FILTERA predicate that indicates whether a variable is used.

Definition at line 66 of file split_finite_variables.h.

◆ split_finite_variables()

template<typename FILTER >
void mcrl2::data::detail::split_finite_variables ( data::variable_list  variables,
const data::data_specification data,
data::variable_list finite_variables,
data::variable_list infinite_variables,
data::variable_list unused,
const FILTER  filter 
)
inline

Splits the variables in a subset with finite sort, with infinite sort and those that are not used according to a filter.

Parameters
variablesA sequence of data variables.
dataA data specification.
finite_variablesA sequence of data variables.
infinite_variablesA sequence of data variables.
unusedA sequence of data variables that do not pass the filter.
FILTERA predicate that indicates whether a variable is used.

Definition at line 32 of file split_finite_variables.h.

◆ subtract() [1/2]

const lhs_t mcrl2::data::detail::subtract ( const lhs_t argument,
const data_expression v,
const rewriter r 
)
inline

Definition at line 474 of file linear_inequalities.h.

◆ subtract() [2/2]

const lhs_t mcrl2::data::detail::subtract ( const lhs_t argument,
const lhs_t e,
const rewriter r 
)
inline

Definition at line 498 of file linear_inequalities.h.

◆ test_rewriters()

template<typename Rewriter1 , typename Rewriter2 >
void mcrl2::data::detail::test_rewriters ( Rewriter1  R1,
Rewriter2  R2,
std::string  expr1,
std::string  expr2,
const std::string &  var_decl = VARIABLE_SPECIFICATION(),
const std::string &  data_spec = "" 
)

Definition at line 233 of file test_rewriters.h.

◆ then_part()

const data_expression & mcrl2::data::detail::then_part ( const data_expression e)
inline

Definition at line 82 of file linear_inequalities_utilities.h.

◆ transform_aterm_list()

template<typename Function , typename T >
atermpp::term_list< T > mcrl2::data::detail::transform_aterm_list ( const Function &  f,
const atermpp::term_list< T > &  x 
)

Definition at line 43 of file type_checker.h.

◆ translate_user_notation_data_equation()

data_equation mcrl2::data::detail::translate_user_notation_data_equation ( const data_equation x)
inline

Definition at line 177 of file translate_user_notation.h.

◆ unique_names()

template<class VariableContainer >
bool mcrl2::data::detail::unique_names ( const VariableContainer &  variables)
inline

Returns true if the names of the given variables are unique.

Parameters
variablesA sequence of data variables
Returns
True if the names of the given variables are unique.

Definition at line 47 of file data_utility.h.

◆ unwind_sort_expression()

sort_expression mcrl2::data::detail::unwind_sort_expression ( const sort_expression x,
const alias_vector aliases 
)
inline

Definition at line 54 of file type_checker.h.

◆ update_substitution() [1/2]

template<typename Substitution , typename IdentifierGenerator >
data::variable mcrl2::data::detail::update_substitution ( Substitution &  sigma,
const data::variable v,
const std::multiset< data::variable > &  V,
IdentifierGenerator &  id_generator 
)

◆ update_substitution() [2/2]

template<typename Substitution , typename IdentifierGenerator , typename VariableContainer >
VariableContainer mcrl2::data::detail::update_substitution ( Substitution &  sigma,
const VariableContainer &  v,
const std::multiset< data::variable > &  V,
IdentifierGenerator &  id_generator 
)

◆ variable_name_strings() [1/2]

std::set< std::string > mcrl2::data::detail::variable_name_strings ( const std::set< data::variable > &  variables)
inline

Returns the names of a set of data variables as a set of strings.

Parameters
variablesA set of data variables

Definition at line 39 of file find.h.

◆ variable_name_strings() [2/2]

std::set< std::string > mcrl2::data::detail::variable_name_strings ( const std::set< data::variable > &  variables1,
const std::set< data::variable > &  variables2 
)
inline

Returns the names of a set of data variables.

Parameters
variablesA set of data variables

Definition at line 52 of file find.h.

◆ variable_names()

std::set< core::identifier_string > mcrl2::data::detail::variable_names ( const std::set< data::variable > &  variables)
inline

Returns the names of a set of data variables.

Parameters
variablesA set of data variables

Definition at line 26 of file find.h.

◆ VARIABLE_SPECIFICATION()

std::string mcrl2::data::detail::VARIABLE_SPECIFICATION ( )
inline

Definition at line 193 of file test_rewriters.h.