Base class for eliminating inconsistent paths from BDDs. More...

#include <bdd_path_eliminator.h>

Inheritance diagram for mcrl2::data::detail::BDD_Path_Eliminator:

Public Member Functions
	BDD_Path_Eliminator (smt_solver_type a_solver_type)
	Constructor that initializes the field BDD_Path_Eliminator::f_smt_solver.

data_expression	simplify (const data_expression &a_bdd) override
	Returns a BDD without inconsistent paths, equivalent to a_bdd. precondition: The argument passed as parameter a_bdd is a data expression in internal mCRL2 format with the following restrictions: It either represents the constant true or the constant false, or it is an if-then-else expression with an expression of sort Bool as guard, and a then-branch and an else-branch that again follow these restrictions.

Public Member Functions inherited from mcrl2::data::detail::BDD_Simplifier
virtual	~BDD_Simplifier ()=default
	Destructor without any additional functionality.

void	set_time_limit (time_t a_time_limit)
	Sets the attribute BDD_Simplifier::f_deadline.

virtual data_expression	simplify (const data_expression &a_bdd)
	Returns a simplified BDD, equivalent to the bdd a_bdd. precondition: The argument passed as parameter a_bdd is a data expression in internal mCRL2 format with the following restrictions: It either represents the constant true or the constant false, or it is an if-then-else expression with an expression of sort Bool as guard, and a then-branch and an else-branch that again follow these restrictions.

Private Member Functions
data_expression_list	create_condition (data_expression_list a_path, const data_expression &a_guard, bool a_minimal)
	Returns a list representing the conjunction of all guards in a_path and the guard a_guard.

data_expression	aux_simplify (const data_expression &a_bdd, const data_expression_list &a_path)
	Simplifies the BDD a_bdd using path a_path. Paths whose guards in conjunction with the guards in.

bool	variables_overlap (const data_expression &a_expression_1, const data_expression &a_expression_2)
	Returns true if the expression a_expression_1 has variables in common with expression a_expression_2.

Private Attributes
SMT_Solver *	f_smt_solver
	Pointer to an SMT solver used to determine whether or not a path is inconsistent.

BDD_Info	f_bdd_info
	Class that provides information about the structure of BDDs.

Additional Inherited Members
Protected Attributes inherited from mcrl2::data::detail::BDD_Simplifier
time_t	f_deadline = 0L
	An integer representing the moment in time when the maximal amount of seconds has been spent on simplifying.

Detailed Description

Base class for eliminating inconsistent paths from BDDs.

\detail The class BDD_Path_Eliminator is a base class for classes that eliminate inconsistent paths from BDDs. The class BDD_Path_Eliminator inherits from the class BDD_Simplifier. It uses an SMT solver to eliminate inconsistent paths from BDDs. The parameter a_solver_type of the constructor BDD_Path_Eliminator::BDD_Path_Eliminator is used to indicate which SMT solver should be used for this task. A path in a BDD is constructed by selecting a set of guards as follows: starting at the root node, one of the two edges at each guard is followed until a leaf is reached. Each time the true-edge is chosen, the guard is added to the set. Each time the false-edge is chosen, the negation of the guard is added to the set. If the conjunction of all elements in this set is a contradiction, the path is inconsistent.

The method BDD_Path_Eliminator::simplify receives a BDD as parameter a_bdd and returns the equivalent BDD from which all inconsistent paths have been removed.

Definition at line 46 of file bdd_path_eliminator.h.

Constructor & Destructor Documentation

◆ BDD_Path_Eliminator()

mcrl2::data::detail::BDD_Path_Eliminator::BDD_Path_Eliminator ( smt_solver_type a_solver_type )

inline

Constructor that initializes the field BDD_Path_Eliminator::f_smt_solver.

Parameters

a_solver_type A value of an enumerated type, representing an SMT solver.

Definition at line 179 of file bdd_path_eliminator.h.

Member Function Documentation

◆ aux_simplify()

data_expression mcrl2::data::detail::BDD_Path_Eliminator::aux_simplify	(	const data_expression &	a_bdd,
		const data_expression_list &	a_path
	)

inlineprivate

Simplifies the BDD a_bdd using path a_path. Paths whose guards in conjunction with the guards in.

a_path are inconsistent are removed.

Parameters

a_bdd	A binary decision diagram.
a_path	A list of guards and negated guards, representing a path in a BDD.

Definition at line 109 of file bdd_path_eliminator.h.

◆ create_condition()

data_expression_list mcrl2::data::detail::BDD_Path_Eliminator::create_condition	(	data_expression_list	a_path,
		const data_expression &	a_guard,
		bool	a_minimal
	)

inlineprivate

Returns a list representing the conjunction of all guards in a_path and the guard a_guard.

Parameters

a_path	A list of guards and negated guards, representing a path in a BDD.
a_guard	A guard or a negated guard.
a_minimal	A boolean value indicating whether or not minimal sets of possibly inconsistent guards are constructed.

Definition at line 61 of file bdd_path_eliminator.h.

◆ simplify()

data_expression mcrl2::data::detail::BDD_Path_Eliminator::simplify ( const data_expression & a_bdd )

inlineoverridevirtual

Returns a BDD without inconsistent paths, equivalent to a_bdd. precondition: The argument passed as parameter a_bdd is a data expression in internal mCRL2 format with the following restrictions: It either represents the constant true or the constant false, or it is an if-then-else expression with an expression of sort Bool as guard, and a then-branch and an else-branch that again follow these restrictions.

Parameters

a_bdd A binary decision diagram.

Reimplemented from mcrl2::data::detail::BDD_Simplifier.

Definition at line 215 of file bdd_path_eliminator.h.

◆ variables_overlap()

bool mcrl2::data::detail::BDD_Path_Eliminator::variables_overlap	(	const data_expression &	a_expression_1,
		const data_expression &	a_expression_2
	)

inlineprivate

Returns true if the expression a_expression_1 has variables in common with expression a_expression_2.

Parameters

a_expression_1	An arbitrary expression.
a_expression_2	An arbitrary expression.

Definition at line 162 of file bdd_path_eliminator.h.

Member Data Documentation

◆ f_bdd_info

BDD_Info mcrl2::data::detail::BDD_Path_Eliminator::f_bdd_info

private

Class that provides information about the structure of BDDs.

Definition at line 55 of file bdd_path_eliminator.h.

◆ f_smt_solver

SMT_Solver* mcrl2::data::detail::BDD_Path_Eliminator::f_smt_solver

private

Pointer to an SMT solver used to determine whether or not a path is inconsistent.

Definition at line 52 of file bdd_path_eliminator.h.

The documentation for this class was generated from the following file:

data/include/mcrl2/data/detail/prover/bdd_path_eliminator.h

Public Member Functions

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ BDD_Path_Eliminator()

Member Function Documentation

◆ aux_simplify()

◆ create_condition()

◆ simplify()

◆ variables_overlap()

Member Data Documentation

◆ f_bdd_info

◆ f_smt_solver