mCRL2
|
Algorithm class for the constelm algorithm. More...
#include <constelm.h>
Classes | |
class | 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 | vertex |
Represents a vertex of the dependency graph. More... | |
Public Member Functions | |
pres_constelm_algorithm (const DataRewriter &datar, const PresRewriter &presr) | |
Constructor. | |
std::map< propositional_variable, std::vector< data::variable > > | redundant_parameters () const |
Returns the parameters that have been removed by the constelm algorithm. | |
void | run (pres &p, bool compute_conditions=false, bool check_quantifiers=true) |
Runs the constelm algorithm. | |
Protected Types | |
typedef std::map< data::variable, data::data_expression > | constraint_map |
A map with constraints on the vertices of the graph. | |
typedef std::list< detail::quantified_variable > | qvar_list |
typedef std::map< core::identifier_string, vertex > | vertex_map |
The storage type for vertices. | |
typedef std::map< core::identifier_string, std::vector< edge > > | edge_map |
The storage type for edges. | |
Protected Member Functions | |
std::string | print_vertices () const |
Logs the vertices of the dependency graph. | |
std::string | print_edges () |
Logs the edges of the dependency graph. | |
std::string | print_todo_list (const std::deque< propositional_variable > &todo) |
std::string | print_edge_update (const edge &e, const vertex &u, const vertex &v) |
std::string | print_condition (const edge &e, const vertex &u, const pres_expression &value) |
std::string | print_evaluation_failure (const edge &e, const vertex &u) |
template<typename E > | |
std::list< E > | concat (const std::list< E > a, const std::list< E > b) |
Protected Attributes | |
const DataRewriter & | m_data_rewriter |
Compares data expressions for equality. | |
const PresRewriter & | m_pres_rewriter |
Compares data expressions for equality. | |
vertex_map | m_vertices |
The vertices of the dependency graph. They are stored in a map, to support searching for a vertex. | |
edge_map | m_edges |
The edges of the dependency graph. They are stored in a map, to easily access all out-edges corresponding to a particular vertex. | |
std::map< core::identifier_string, std::vector< std::size_t > > | m_redundant_parameters |
The redundant parameters. | |
Algorithm class for the constelm algorithm.
Definition at line 406 of file constelm.h.
|
protected |
A map with constraints on the vertices of the graph.
Definition at line 410 of file constelm.h.
|
protected |
The storage type for edges.
Definition at line 735 of file constelm.h.
|
protected |
Definition at line 411 of file constelm.h.
|
protected |
The storage type for vertices.
Definition at line 732 of file constelm.h.
|
inline |
Constructor.
datar | A data rewriter |
presr | A PRES rewriter |
Definition at line 829 of file constelm.h.
|
inlineprotected |
Definition at line 817 of file constelm.h.
|
inlineprotected |
Definition at line 798 of file constelm.h.
|
inlineprotected |
Definition at line 789 of file constelm.h.
|
inlineprotected |
Logs the edges of the dependency graph.
Definition at line 760 of file constelm.h.
|
inlineprotected |
Definition at line 807 of file constelm.h.
|
inlineprotected |
Definition at line 773 of file constelm.h.
|
inlineprotected |
Logs the vertices of the dependency graph.
Definition at line 749 of file constelm.h.
|
inline |
Returns the parameters that have been removed by the constelm algorithm.
Definition at line 835 of file constelm.h.
|
inline |
Runs the constelm algorithm.
p | A pres |
compute_conditions | If true, propagation conditions are computed. Note that the currently implementation has exponential behavior. |
Definition at line 856 of file constelm.h.
|
protected |
Compares data expressions for equality.
Definition at line 414 of file constelm.h.
|
protected |
The edges of the dependency graph. They are stored in a map, to easily access all out-edges corresponding to a particular vertex.
Definition at line 743 of file constelm.h.
|
protected |
Compares data expressions for equality.
Definition at line 417 of file constelm.h.
|
protected |
The redundant parameters.
Definition at line 746 of file constelm.h.
|
protected |
The vertices of the dependency graph. They are stored in a map, to support searching for a vertex.
Definition at line 739 of file constelm.h.