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	elements_per_domain

struct	enumerate_quantifiers_builder

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	influence_graph

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_MachineNumber

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

struct	parameter

class	parser

class	parvalues_algorithm
	Algorithm class that can be used to apply the lps_explore_domains algorithm. More...

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
using	variable_or_number_list = atermpp::term_list< variable_or_number >

using	match_tree_list = atermpp::term_list< match_tree >

using	match_tree_vector = std::vector< match_tree >

using	match_tree_list_list = atermpp::term_list< match_tree_list >

using	match_tree_list_list_list = atermpp::term_list< match_tree_list_list >

using	sort_of_variable = sort_of_expression< variable >
	Function object that returns the sort of a data variable.

using	map_based_lhs_t = std::map< variable, data_expression >

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
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)

bool	is_one (const data_expression &x)

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	head_matches_undefined_symbol (const data_expression &x, const core::identifier_string &s)

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)

data_equation	translate_user_notation_data_equation (const data_equation &x)

atermpp::aterm	data_specification_to_aterm (const data_specification &s)

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.

atermpp::aterm	remove_index_impl (const atermpp::aterm &x)

atermpp::aterm	add_index_impl (const atermpp::aterm &x)

atermpp::aterm	add_index (const atermpp::aterm &x)

atermpp::aterm	remove_index (const atermpp::aterm &x)

std::set< variable >	bound_variables_in_substitution (const jitty_assignments_for_a_rewrite_rule &assignments)

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)

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_expression *	get_argument_of_higher_order_term_helper (const application &t, std::size_t &i)

const data_expression &	get_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_expression &	get_nested_head_helper (const application &t)

const data_expression &	get_nested_head (const data_expression &t)

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, const bool skip_rewriting_head=false)

std::shared_ptr< detail::Rewriter >	createRewriter (const data_specification &DataSpec, const used_data_equation_selector &equations_selector, 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)

std::ostream &	operator<< (std::ostream &s, const match_tree &t)

static bool	occur_check (const variable &v, const atermpp::aterm &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)

void	set_enumerator_iteration_limit (std::size_t size)

std::size_t	get_enumerator_iteration_limit ()

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 , IsSubstitution 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)

strategy	create_strategy (data_equation_list rules)
	Creates a strategy for given set of rewrite rules with head symbol f.

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)

bool	contains_untyped_sort (const sort_expression &s)

const data_expression &	evaluate_lambda_data_expression (const data_expression &t)

template<class TERM > requires (std::is_invocable_r_v<void, TERM, data_expression&>)
data_expression	evaluate_lambda_data_expression (const TERM &t)

template<class TERM > requires (std::is_invocable_r_v<const data_expression, TERM, void>)
data_expression	evaluate_lambda_data_expression (const TERM &t)

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)

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.

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_string >	variable_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.

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_expression &	condition_part (const data_expression &e)

const data_expression &	then_part (const data_expression &e)

const data_expression &	else_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<IsSubstitution 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.

template<class VariableContainer >
std::string	ppsort (const VariableContainer &s)

std::ostream &	operator<< (std::ostream &out, const parameter &x)

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 (const data::data_expression &e, const data::sort_expression &s)

data_expression	reconstruct_pos_mult (const data_expression &x, const 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::size_t	rewrite_count ()

void	display_rewrite_statistics ()

void	increment_rewrite_count ()

static std::vector< data::rewrite_strategy >	initialise_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 > requires (std::is_base_of_v<atermpp::aterm, T>)
T	normalize_and_or (const T &x)

template<typename T > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	normalize_and_or (T &x)

template<typename T > requires (std::is_base_of_v<atermpp::aterm, T>)
T	normalize_equality (const T &x)

template<typename T > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	normalize_equality (T &x)

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)

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)

std::set< data_expression >	split_aggressive (const data_expression &expr, bool outermost_symbol_is_or)
	Splits a boolean term by rewriting it to the shape p1 \|\| p2 \|\| ... \|\| pn or p1 &&...&& pn and then yield a set of the form { p1, p2, ..., pn } where pi does not have \|\| or && anymore as main function symbol. The second parameter indicates what the outermost symbol is.

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)

lhs_t	map_to_lhs_type (const map_based_lhs_t &lhs)

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)

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>
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)

lhs_t	add (const data_expression &v, const lhs_t &argument, const rewriter &r)

lhs_t	subtract (const lhs_t &argument, const data_expression &v, const rewriter &r)

lhs_t	multiply (const lhs_t &argument, const data_expression &v, const rewriter &r)

lhs_t	divide (const lhs_t &argument, const data_expression &v, const rewriter &r)

lhs_t	add (const lhs_t &argument, const lhs_t &e, const rewriter &r)

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.

static data_specification const &	default_specification ()

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, Rewriter >	make_rewrite_data_expressions_builder (Rewriter R)

template<template< class > class Builder, class Rewriter , IsSubstitution Substitution>
rewrite_data_expressions_with_substitution_builder< Builder, Rewriter, Substitution >	make_rewrite_data_expressions_with_substitution_builder (Rewriter R, Substitution sigma)

template<typename DataRewriter , IsSubstitution SubstitutionFunction>
void	data_rewrite (data_expression &result, const data_expression &x, const DataRewriter &R, SubstitutionFunction &sigma)

template<typename DataRewriter >
void	data_rewrite (data_expression &result, const data_expression &x, const DataRewriter &R, no_substitution &)

template<template< class, class, class > class Builder, class DataRewriter , IsSubstitution 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< variable >	make_variable_set (const variable_list &x)

variable_list	make_variable_list (const std::set< variable > &x)

template<typename BinaryOperation >
std::tuple< data_expression, data_expression >	compute_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, variable_list::const_iterator variables_begin, variable_list::const_iterator variables_end, 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)

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.

Typedef Documentation

◆ map_based_lhs_t

using mcrl2::data::detail::map_based_lhs_t = typedef std::map<variable, data_expression>

Definition at line 171 of file linear_inequalities.h.

◆ match_tree_list

using mcrl2::data::detail::match_tree_list = typedef atermpp::term_list<match_tree>

Definition at line 574 of file match_tree.h.

◆ match_tree_list_list

using mcrl2::data::detail::match_tree_list_list = typedef atermpp::term_list<match_tree_list>

Definition at line 576 of file match_tree.h.

◆ match_tree_list_list_list

using mcrl2::data::detail::match_tree_list_list_list = typedef atermpp::term_list<match_tree_list_list>

Definition at line 577 of file match_tree.h.

◆ match_tree_vector

using mcrl2::data::detail::match_tree_vector = typedef std::vector<match_tree>

Definition at line 575 of file match_tree.h.

◆ sort_of_variable

using mcrl2::data::detail::sort_of_variable = typedef sort_of_expression<variable>

Function object that returns the sort of a data variable.

Definition at line 93 of file data_functional.h.

◆ variable_or_number_list

using mcrl2::data::detail::variable_or_number_list = typedef atermpp::term_list<variable_or_number>

Definition at line 36 of file match_tree.h.

Enumeration Type Documentation

◆ Answer

enum mcrl2::data::detail::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 76 of file bdd_prover.h.

◆ Compare_Result

enum mcrl2::data::detail::Compare_Result

Enumerator
compare_result_smaller
compare_result_equal
compare_result_bigger

Definition at line 22 of file info.h.

◆ comparison_t

enum mcrl2::data::detail::comparison_t

Enumerator
less
less_eq
equal

Definition at line 102 of file linear_inequalities.h.

◆ node_type

enum mcrl2::data::detail::node_type

Enumerator
true_end_node
false_end_node
intermediate_node

Definition at line 1296 of file linear_inequalities.h.

◆ smt_solver_type

enum mcrl2::data::detail::smt_solver_type

The enumeration type smt_solver_type enumerates all available SMT solvers.

Enumerator
solver_type_cvc
solver_type_z3

Definition at line 22 of file solver_type.h.

Function Documentation

◆ add() [1/2]

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

inline

Definition at line 471 of file linear_inequalities.h.

◆ add() [2/2]

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

inline

Definition at line 491 of file linear_inequalities.h.

◆ add_index()

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

inline

Definition at line 44 of file io.h.

◆ add_index_impl()

atermpp::aterm mcrl2::data::detail::add_index_impl ( const atermpp::aterm & x )

inline

Definition at line 33 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 127 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
	)

Definition at line 166 of file replace_capture_avoiding_with_an_identifier_generator.h.

◆ bool_to_numeric()

data::data_expression mcrl2::data::detail::bool_to_numeric	(	const data::data_expression &	e,
		const data::sort_expression &	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 30 of file print_utility.h.

◆ bound_variables_in_substitution()

std::set< variable > mcrl2::data::detail::bound_variables_in_substitution ( const jitty_assignments_for_a_rewrite_rule & assignments )

Definition at line 212 of file jitty.cpp.

◆ 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

assignments	A sequence of assignments to data variables
variables	A sequence of data variables

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

Definition at line 56 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

range	A sequence of data operations
sorts	A set of sort expressions

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

Definition at line 184 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 26 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

s	A sort expression
sorts	A set of sort expressions

Returns: True if the sort is contained in sorts

Definition at line 76 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

first	Start of a sequence of sorts
last	End of a sequence of sorts
sorts	A set of sort expressions

Returns: True if the sequence of sorts is contained in sorts

Definition at line 130 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

variables	A sequence of data variables
names	A set of strings

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

Definition at line 164 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

variables	A container with data variables
sorts	A 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 147 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 524 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 535 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 286 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 558 of file rewrite.cpp.

◆ checkPattern() [2/2]

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

static

Definition at line 567 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

DataEqn The mCRL2 data equation to be checked.

Exceptions

std::runtime_error containing a reason why DataEqn is not a valid rewrite rule.

Definition at line 582 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 296 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 107 of file enumerator.h.

◆ compute_finite_set_elements()

template<class Rewriter , IsSubstitution 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 80 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 42 of file quantifiers_inside_rewriter.h.

◆ condition_part()

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

inline

Definition at line 68 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 109 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 148 of file unfold_pattern_matching.h.

◆ contains_untyped_sort()

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

inline

Definition at line 232 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 23 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 33 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 42 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,
		rewrite_strategy	Strategy = `jitty`
	)

Create a rewriter.

Parameters

DataSpec	A data specification.
Strategy	The 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 498 of file rewrite.cpp.

◆ data_rewrite() [1/2]

template<typename DataRewriter >

void mcrl2::data::detail::data_rewrite	(	data_expression &	result,
		const data_expression &	x,
		const DataRewriter &	R,
		no_substitution &
	)

Definition at line 30 of file data_rewriter.h.

◆ data_rewrite() [2/2]

template<typename DataRewriter , IsSubstitution SubstitutionFunction>

void mcrl2::data::detail::data_rewrite	(	data_expression &	result,
		const data_expression &	x,
		const DataRewriter &	R,
		SubstitutionFunction &	sigma
	)

Definition at line 24 of file data_rewriter.h.

◆ data_specification_to_aterm()

atermpp::aterm mcrl2::data::detail::data_specification_to_aterm ( const data_specification & s )

Returns: A term that represetns this data_specification.

Definition at line 39 of file data_io.cpp.

◆ default_specification()

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

inlinestatic

Definition at line 28 of file parse.h.

◆ description()

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

inline

description of solver type

Definition at line 84 of file solver_type.h.

◆ display_rewrite_statistics()

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

inline

Definition at line 36 of file rewrite_statistics.h.

◆ divide()

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

inline

Definition at line 486 of file linear_inequalities.h.

◆ else_part()

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

inline

Definition at line 84 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 396 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 88 of file enumerator_substitution.h.

◆ enumerator_replace() [2/2]

template<typename T >

data_expression mcrl2::data::detail::enumerator_replace	(	const T &	x,
		variable_list::const_iterator	variables_begin,
		variable_list::const_iterator	variables_end,
		data_expression_list::const_iterator	expressions_begin
	)

inline

Definition at line 75 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

v	A sequence of data variables
w	A sequence of data expressions

Returns: True if the sorts match pairwise

Definition at line 25 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 264 of file application.h.

◆ evaluate_lambda_data_expression() [2/3]

template<class TERM >
requires (std::is_invocable_r_v<void, TERM, data_expression&>)

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

inline

Definition at line 271 of file application.h.

◆ evaluate_lambda_data_expression() [3/3]

template<class TERM >
requires (std::is_invocable_r_v<const data_expression, TERM, void>)

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

inline

Definition at line 280 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 106 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 74 of file jitty_jittyc.h.

◆ get_arguments() [1/2]

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

inline

Definition at line 319 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 326 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 226 of file rewrite.h.

◆ get_enumerator_iteration_limit()

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

inline

Definition at line 39 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 47 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 159 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 148 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

x	A set expression

Definition at line 51 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 49 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

expr	The expression from which to extract the top function symbol

Returns: The top function symbol, or function_symbol() if it has none

Definition at line 86 of file unfold_pattern_matching.h.

◆ getArity()

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

inline

Definition at line 210 of file rewrite.h.

◆ GetVarTypes()

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

static

Definition at line 4624 of file typecheck.cpp.

◆ HasUnknown()

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

static

Definition at line 4677 of file typecheck.cpp.

◆ head_matches_undefined_symbol()

bool mcrl2::data::detail::head_matches_undefined_symbol	(	const data_expression &	x,
		const core::identifier_string &	s
	)

inline

Definition at line 70 of file print.h.

◆ I()

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

inline

Definition at line 241 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 35 of file typecheck.cpp.

◆ increment_rewrite_count()

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

inline

Definition at line 42 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 26 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 66 of file typecheck.cpp.

◆ is_and()

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

inline

Definition at line 181 of file print.h.

◆ is_bag_difference()

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

inline

Definition at line 175 of file print.h.

◆ is_bag_intersection()

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

inline

Definition at line 257 of file print.h.

◆ is_bag_join()

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

inline

Definition at line 169 of file print.h.

◆ is_concat()

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

inline

Definition at line 263 of file print.h.

◆ is_cons()

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

inline

Definition at line 289 of file print.h.

◆ is_cons_list()

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

inline

Definition at line 269 of file print.h.

◆ is_div()

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

inline

Definition at line 120 of file print.h.

◆ is_divides()

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

inline

Definition at line 141 of file print.h.

◆ is_divmod()

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

inline

Definition at line 131 of file print.h.

◆ is_element_at()

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

inline

Definition at line 245 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 157 of file enumerator.h.

◆ is_equal_to()

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

inline

Definition at line 193 of file print.h.

◆ is_greater()

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

inline

Definition at line 217 of file print.h.

◆ is_greater_equal()

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

inline

Definition at line 223 of file print.h.

◆ is_implies()

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

inline

Definition at line 151 of file print.h.

◆ is_in()

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

inline

Definition at line 229 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

e	A data expression

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

Definition at line 60 of file linear_inequalities_utilities.h.

◆ is_less()

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

inline

Definition at line 205 of file print.h.

◆ is_less_equal()

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

inline

Definition at line 211 of file print.h.

◆ is_minus()

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

inline

Definition at line 99 of file print.h.

◆ is_mod()

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

inline

Definition at line 110 of file print.h.

◆ is_nat()

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

inline

Definition at line 29 of file type_checker.h.

◆ is_not_equal_to()

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

inline

Definition at line 199 of file print.h.

◆ is_numeric_cast()

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

inline

Definition at line 43 of file print.h.

◆ is_numeric_type()

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

inline

Definition at line 81 of file type_checker.h.

◆ is_one()

bool mcrl2::data::detail::is_one ( const data_expression & x )

inline

Definition at line 28 of file print.h.

◆ is_or()

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

inline

Definition at line 187 of file print.h.

◆ is_plus()

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

inline

Definition at line 85 of file print.h.

◆ is_pos()

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

inline

Definition at line 22 of file type_checker.h.

◆ is_set_difference()

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

inline

Definition at line 163 of file print.h.

◆ is_set_intersection()

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

inline

Definition at line 251 of file print.h.

◆ is_set_union()

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

inline

Definition at line 157 of file print.h.

◆ is_snoc()

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

inline

Definition at line 295 of file print.h.

◆ is_snoc_list()

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

inline

Definition at line 279 of file print.h.

◆ is_times()

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

inline

Definition at line 235 of file print.h.

◆ is_untyped()

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

inline

Definition at line 66 of file is_untyped.h.

◆ is_well_formed()

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

inline

Definition at line 356 of file linear_inequalities.h.

◆ IsNat()

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

inlinestatic

Definition at line 53 of file typecheck.cpp.

◆ IsNumericType()

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

static

Definition at line 4712 of file typecheck.cpp.

◆ IsPos()

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

inlinestatic

Definition at line 48 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

DataEqn The mCRL2 data equation to be checked.

Returns: Whether or not DataEqn is a valid rewrite rule.

Definition at line 640 of file rewrite.cpp.

◆ linear_inequality_equal()

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

inline

Definition at line 550 of file linear_inequalities.h.

◆ linear_inequality_less()

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

inline

Definition at line 536 of file linear_inequalities.h.

◆ linear_inequality_less_equal()

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

inline

Definition at line 543 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 59 of file print.h.

◆ make_apply_rewriter_builder()

template<template< class, class, class > class Builder, class DataRewriter , IsSubstitution 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 35 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 45 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 47 of file rewrite.h.

◆ make_rewrite_data_expressions_with_substitution_builder()

template<template< class > class Builder, class Rewriter , IsSubstitution 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 78 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

c	A container

Returns: A set containing the elements of the container

Definition at line 74 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 30 of file enumerator.h.

◆ make_variable_list()

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

inline

Definition at line 36 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 30 of file quantifiers_inside_rewriter.h.

◆ map_to_lhs_type() [1/2]

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

inline

Definition at line 335 of file linear_inequalities.h.

◆ map_to_lhs_type() [2/2]

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 345 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 346 of file jitty.cpp.

◆ meta_operation_constant()

template<application Operation>

lhs_t mcrl2::data::detail::meta_operation_constant	(	const lhs_t &	argument,
		const data_expression &	v,
		const rewriter &	r
	)

inline

Definition at line 406 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 420 of file linear_inequalities.h.

◆ MinType()

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

static

Definition at line 4728 of file typecheck.cpp.

◆ multiply()

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

inline

Definition at line 481 of file linear_inequalities.h.

◆ N()

template<typename Function >

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

Definition at line 180 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 22 of file linear_inequalities_utilities.h.

◆ normalize_and_or() [1/2]

template<typename T >
requires (std::is_base_of_v<atermpp::aterm, T>)

T mcrl2::data::detail::normalize_and_or ( const T & x )

Definition at line 84 of file test_rewriters.h.

◆ normalize_and_or() [2/2]

template<typename T >
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::data::detail::normalize_and_or ( T & x )

Definition at line 93 of file test_rewriters.h.

◆ normalize_equality() [1/2]

template<typename T >
requires (std::is_base_of_v<atermpp::aterm, T>)

T mcrl2::data::detail::normalize_equality ( const T & x )

Definition at line 148 of file test_rewriters.h.

◆ normalize_equality() [2/2]

template<typename T >
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::data::detail::normalize_equality ( T & x )

Definition at line 157 of file test_rewriters.h.

◆ occur_check()

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

static

Definition at line 44 of file rewrite.cpp.

◆ operator<<() [1/6]

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

inline

standard conversion from solvert type to stream

Definition at line 76 of file solver_type.h.

◆ operator<<() [2/6]

template<typename Substitution >

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

Definition at line 100 of file replace_capture_avoiding.h.

◆ operator<<() [3/6]

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

inline

Definition at line 213 of file find_equalities.h.

◆ operator<<() [4/6]

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

inline

Definition at line 72 of file parvalues.h.

◆ operator<<() [5/6]

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

inline

Definition at line 76 of file unfold_pattern_matching.h.

◆ operator<<() [6/6]

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

inline

Definition at line 605 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 48 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

left	A term
right	A term

Returns: The value left && right

Definition at line 56 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

v	A sequence of variables
arg	A term
remove_variables	If true, remove bound variables that do not occur in arg.
empty_domain_allowed	If 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 233 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

v	A sequence of variables
arg	A term
remove_variables	If true, remove bound variables that do not occur in arg.
empty_domain_allowed	If 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 175 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

left	A term
right	A term

Returns: The value left => right

Definition at line 133 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 26 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

left	A term
right	A term

Returns: The value left || right

Definition at line 95 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 26 of file data_utility.h.

◆ parse_data_expression()

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

Definition at line 223 of file data.cpp.

◆ parse_data_specification_new()

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

Definition at line 234 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 30 of file solver_type.h.

◆ parse_sort_expression()

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

Definition at line 202 of file data.cpp.

◆ parse_substitution()

template<IsSubstitution 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 25 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 245 of file data.cpp.

◆ parse_variables()

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

Definition at line 212 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 509 of file linear_inequalities.h.

◆ ppsort()

template<class VariableContainer >

std::string mcrl2::data::detail::ppsort ( const VariableContainer & s )

Definition at line 28 of file parvalues.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 36 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 22 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 65 of file solver_type.h.

◆ push_if_outside()

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

inline

Definition at line 33 of file if_rewriter.h.

◆ quantifiers_inside()

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

inline

Definition at line 282 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 300 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 291 of file quantifiers_inside_rewriter.h.

◆ reconstruct_pos_mult()

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

inline

Definition at line 37 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 126 of file jitty_jittyc.h.

◆ remove_index()

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

inline

Definition at line 50 of file io.h.

◆ remove_index_impl()

atermpp::aterm mcrl2::data::detail::remove_index_impl ( const atermpp::aterm & x )

inline

Definition at line 23 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()

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 383 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 26 of file if_rewriter.h.

◆ replace_nested_head()

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

inline

Definition at line 185 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 4636 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 53 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,
		const bool	skip_rewriting_head = `false`
	)

inline

Definition at line 197 of file jitty_jittyc.h.

◆ rewrite_count()

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

inline

Definition at line 30 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

first	Start of a sequence
last	End of a sequence

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

Definition at line 28 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

s1	A sequence
s2	A sequence

Returns: True if the intersection of s1 and s2 is empty

Definition at line 86 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

first	Start of a sequence
last	End of a sequence
s	A set

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

Definition at line 58 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

first1	Start of a sequence
last1	End of a sequence
first2	Start of a sequence
last2	End of a sequence

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

Definition at line 42 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

x	A sequence of data variables
y	A sequence of data variables

Returns: The difference of two sets.

Definition at line 48 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 33 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 306 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 289 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

x	A sequence of data variables
y	A sequence of data variables

Returns: The intersection of two sets.

Definition at line 25 of file data_sequence_algorithm.h.

◆ split_aggressive()

std::set< data_expression > mcrl2::data::detail::split_aggressive	(	const data_expression &	expr,
		bool	outermost_symbol_is_or
	)

inline

Splits a boolean term by rewriting it to the shape p1 || p2 || ... || pn or p1 &&...&& pn and then yield a set of the form { p1, p2, ..., pn } where pi does not have || or && anymore as main function symbol. The second parameter indicates what the outermost symbol is.

Parameters

expr	A data expression.
outermost_symbol_is_or	Indicates whether the outermost symbol is \|\|. If false it is &&.

Returns: A set of data expressions of type bool.

Definition at line 67 of file join.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 226 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

e	A data expression of sort bool.
real_condition	Those parts of e with only variables over sort Real.
non_real_condition	Those parts of e with only variables not of sort Real.
negate	A 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 108 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

variables	A sequence of data variables.
data	A data specification.
rewr	A data rewriter to determine which elements are enumerable.
finite_variables	A sequence of data variables.
infinite_variables	A sequence of data variables.
unused	A sequence of data variables that do not pass the filter.
FILTER	A predicate that indicates whether a variable is used.

Definition at line 63 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

variables	A sequence of data variables.
data	A data specification.
finite_variables	A sequence of data variables.
infinite_variables	A sequence of data variables.
unused	A sequence of data variables that do not pass the filter.
FILTER	A predicate that indicates whether a variable is used.

Definition at line 29 of file split_finite_variables.h.

◆ subtract() [1/2]

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

inline

Definition at line 476 of file linear_inequalities.h.

◆ subtract() [2/2]

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

inline

Definition at line 500 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 226 of file test_rewriters.h.

◆ then_part()

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

inline

Definition at line 76 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 41 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 185 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

variables A sequence of data variables

Returns: True if the names of the given variables are unique.

Definition at line 41 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 52 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
	)

Definition at line 106 of file replace_capture_avoiding_with_an_identifier_generator.h.

◆ 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
	)

Definition at line 128 of file replace_capture_avoiding_with_an_identifier_generator.h.

◆ 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

variables A set of data variables

Definition at line 36 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

variables A set of data variables

Definition at line 49 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

variables A set of data variables

Definition at line 23 of file find.h.

◆ VARIABLE_SPECIFICATION()

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

inline

Definition at line 186 of file test_rewriters.h.

Namespaces

Classes

Typedefs

Enumerations

Functions

Typedef Documentation

◆ map_based_lhs_t

◆ match_tree_list

◆ match_tree_list_list

◆ match_tree_list_list_list

◆ match_tree_vector

◆ sort_of_variable

◆ variable_or_number_list

Enumeration Type Documentation

◆ Answer

◆ Compare_Result

◆ comparison_t

◆ node_type

◆ smt_solver_type

Function Documentation

◆ add() [1/2]

◆ add() [2/2]

◆ add_index()

◆ add_index_impl()

◆ apply_replace_capture_avoiding_variables_builder()

◆ apply_replace_capture_avoiding_variables_builder_with_an_identifier_generator()

◆ bool_to_numeric()

◆ bound_variables_in_substitution()

◆ check_assignment_variables()

◆ check_data_spec_sorts()

◆ check_duplicate_variable_names()

◆ check_sort()

◆ check_sorts()

◆ check_variable_names()

◆ check_variable_sorts()

◆ check_vars() [1/2]

◆ check_vars() [2/2]

◆ check_whether_sorts_match()

◆ checkPattern() [1/2]

◆ checkPattern() [2/2]

◆ CheckRewriteRule()

◆ compare_property_maps()

◆ compute_finite_function_sorts()

◆ compute_finite_set_elements()

◆ compute_Phi_Psi()

◆ condition_part()

◆ construct_condition_rhs()

◆ construct_rhs()

◆ contains_untyped_sort()

◆ create_finite_set()

◆ create_set_comprehension()

◆ create_set_in()

◆ create_strategy()

◆ createRewriter()

◆ data_rewrite() [1/2]

◆ data_rewrite() [2/2]

◆ data_specification_to_aterm()

◆ default_specification()

◆ description()

◆ display_rewrite_statistics()

◆ divide()

◆ else_part()

◆ emplace_back_if_not_zero()

◆ enumerator_replace() [1/2]

◆ enumerator_replace() [2/2]

◆ equal_sorts()

◆ evaluate_lambda_data_expression() [1/3]

◆ evaluate_lambda_data_expression() [2/3]

◆ evaluate_lambda_data_expression() [3/3]

◆ f_variable_with_a_rational_factor()

◆ get_argument_of_higher_order_term()

◆ get_argument_of_higher_order_term_helper()

◆ get_arguments() [1/2]

◆ get_arguments() [2/2]

◆ get_direct_arity()

◆ get_enumerator_iteration_limit()

◆ get_free_vars()

◆ get_nested_head()

◆ get_nested_head_helper()

◆ get_set_sort()