constelm.h File Reference

The constelm algorithm. More...

Go to the source code of this file.

Classes
class	mcrl2::pbes_system::detail::quantified_variable
struct	mcrl2::pbes_system::detail::QPVI
	A quantified predicate variable instantiation. More...
struct	mcrl2::pbes_system::detail::edge_details
struct	mcrl2::pbes_system::detail::edge_traverser_stack_elem
struct	mcrl2::pbes_system::detail::edge_condition_traverser
class	mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >
	Algorithm class for the constelm algorithm. More...
class	mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::edge
	Represents an edge of the dependency graph. The assignments are stored implicitly using the 'right' parameter. The condition determines under what circumstances the influence of the edge is propagated to its target vertex. More...
class	mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::vertex
	Represents a vertex of the dependency graph. More...

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

Functions
void	mcrl2::pbes_system::detail::make_constelm_substitution (const std::map< data::variable, data::data_expression > &m, data::rewriter::substitution_type &result)
void	mcrl2::pbes_system::constelm (pbes &p, data::rewrite_strategy rewrite_strategy, pbes_rewriter_type rewriter_type, bool compute_conditions=false, bool remove_redundant_equations=true, bool check_quantifiers=true)
	Apply the constelm algorithm.

Detailed Description

The constelm algorithm.

Definition in file constelm.h.