spot::minato_isop Class Reference

Generate an irredundant sum-of-products (ISOP) form of a BDD function. More...

#include <spot/misc/minato.hh>

Collaboration diagram for spot::minato_isop:

Public Member Functions
	minato_isop (bdd input)
	Constructor.
	minato_isop (bdd input, bdd vars)
	Constructor.
	minato_isop (bdd input_min, bdd input_max, bool)
	Constructor.
bdd	next ()
	Compute the next sum term of the ISOP form. Return bddfalse when all terms have been output.

Detailed Description

Generate an irredundant sum-of-products (ISOP) form of a BDD function.

This algorithm implements a derecursived version the Minato-Morreale algorithm. [34]

Constructor & Destructor Documentation

minato_isop() [1/3]

spot::minato_isop::minato_isop

(

bdd

input

)

Constructor.

• input The BDD function to translate in ISOP.

minato_isop() [2/3]

spot::minato_isop::minato_isop	(	bdd	input,
		bdd	vars
	)

Constructor.

• input The BDD function to translate in ISOP.
• vars The set of BDD variables to factorize in input.

minato_isop() [3/3]

spot::minato_isop::minato_isop	(	bdd	input_min,
		bdd	input_max,
		bool
	)

Constructor.

This version allow some flexibility in computing the ISOP. the result must be within input_min and input_max.

• input_min The minimum BDD function to translate in ISOP.
• input_max The maximum BDD function to translate in ISOP.

Member Function Documentation

next()

bdd spot::minato_isop::next

(

)

Compute the next sum term of the ISOP form. Return bddfalse when all terms have been output.

---

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

• spot/misc/minato.hh