A base class for simplifying binary decision diagrams. More...

#include <bdd_simplifier.h>

Inheritance diagram for mcrl2::data::detail::BDD_Simplifier:

Public Member Functions
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.

Protected Attributes
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

A base class for simplifying binary decision diagrams.

\detail These classes take a BDD as input and try to simplify this BDD. The method BDD_Simplifier::simplify receives a BDD as parameter a_bdd and tries to find an equivalent BDD that is smaller. It returns the reduced BDD if such a BDD is found. If a reduced BDD is not found, the original BDD is returned.

Definition at line 30 of file bdd_simplifier.h.

Constructor & Destructor Documentation

◆ ~BDD_Simplifier()

virtual mcrl2::data::detail::BDD_Simplifier::~BDD_Simplifier ( )

virtualdefault

Destructor without any additional functionality.

Member Function Documentation

◆ set_time_limit()

void mcrl2::data::detail::BDD_Simplifier::set_time_limit ( time_t a_time_limit )

inline

Sets the attribute BDD_Simplifier::f_deadline.

Definition at line 41 of file bdd_simplifier.h.

◆ simplify()

virtual data_expression mcrl2::data::detail::BDD_Simplifier::simplify ( const data_expression & a_bdd )

inlinevirtual

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.

Reimplemented in mcrl2::data::detail::BDD_Path_Eliminator.

Definition at line 58 of file bdd_simplifier.h.

Member Data Documentation

◆ f_deadline

time_t mcrl2::data::detail::BDD_Simplifier::f_deadline = 0L

protected

An integer representing the moment in time when the maximal amount of seconds has been spent on simplifying.

the BDD.

Definition at line 35 of file bdd_simplifier.h.

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

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

Public Member Functions

Protected Attributes