pbeschain.h File Reference

This file provides a tool that can simplify PBESs by substituting PBES equations for variables in the rhs, simplifying the result, and keeping it when it can eliminate PBES variables. More...

Go to the source code of this file.

Classes
struct	mcrl2::pbes_system::pbeschain_options
struct	mcrl2::pbes_system::substitute_propositional_variables_for_true_false_builder< Builder >
struct	mcrl2::pbes_system::rewrite_if_builder< Builder >
struct	mcrl2::pbes_system::substitute_propositional_variables_builder< Builder >
struct	mcrl2::pbes_system::substitute_propositional_variables_i_builder< Builder >
struct	mcrl2::pbes_system::timing_tracker
	Helper class to track multiple time measurements and call counts. More...
struct	mcrl2::pbes_system::timing_tracker::measurement
struct	mcrl2::pbes_system::pbeschain_pbes_backward_substituter

Namespaces
namespace	mcrl2
namespace	mcrl2::pbes_system
	The main namespace for the PBES library.

Functions
template<typename Container >
std::vector< propositional_variable_instantiation >	mcrl2::pbes_system::get_propositional_variable_instantiations (Container const &container)
	Returns all data variables that occur in a range of expressions.
template<typename Func >
auto	mcrl2::pbes_system::measure_time (timing_tracker &timer, const std::string &name, Func &&func)
	Generic decorator to wrap any function call with timing measurements.
pbes_expression	mcrl2::pbes_system::simplify_expr (pbes_expression &phi, rewrite_if_builder< pbes_system::pbes_expression_builder > &if_substituter, simplify_data_rewriter< data::rewriter > &pbes_rewriter)
bool	mcrl2::pbes_system::is_quantifier_free (pbes_expression &phi, pbeschain_options options)
bool	mcrl2::pbes_system::is_not_too_big (pbeschain_options &options, propositional_variable_instantiation &cur_x, pbes_expression &phi)
bool	mcrl2::pbes_system::is_avoiding_alternation (const pbeschain_options &options, const propositional_variable_instantiation &new_x, const pbes_equation &eq)
void	mcrl2::pbes_system::log_number_pvi (std::size_t &initial_size, std::size_t &current_size)
void	mcrl2::pbes_system::self_substitute (pbes_equation &equation, std::size_t initial_size, substitute_propositional_variables_for_true_false_builder< pbes_system::pbes_expression_builder > &pvi_substituter, rewrite_if_builder< pbes_system::pbes_expression_builder > &if_substituter, simplify_data_rewriter< data::rewriter > &pbes_rewriter, simplify_data_rewriter< data::rewriter > &pbes_default_rewriter, pbeschain_options options)
void	mcrl2::pbes_system::substitute (pbes_equation &into, const pbes_equation &by, substitute_propositional_variables_builder< pbes_system::pbes_expression_builder > &substituter)
pbes	mcrl2::pbes_system::fill_pvi (pbes &p, data::rewriter data_rewriter)
pbes	mcrl2::pbes_system::tosrf (pbes_system::pbes pbesspec, bool split_srf_conditions=false)
void	mcrl2::pbes_system::pbeschain (const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format, pbeschain_options options)

Detailed Description

This file provides a tool that can simplify PBESs by substituting PBES equations for variables in the rhs, simplifying the result, and keeping it when it can eliminate PBES variables.

Definition in file pbeschain.h.