Class mata::Mintermization

class Mintermization

Public Functions

std::unordered_set<BDD> compute_minterms(const std::unordered_set<BDD> &source_bdds)

Takes a set of BDDs and build a minterm tree over it.

The leaves of BDDs, which are minterms of input set, are returned

Parameters:

source_bdds – BDDs for which minterms are computed

Returns:

Computed minterms

BDD graph_to_bdd_nfa(const FormulaGraph &graph)

Transforms a graph representing formula at transition to bdd.

Parameters:

graph – Graph to be transformed

Returns:

Resulting BDD

OptionalBdd graph_to_bdd_afa(const FormulaGraph &graph)

Transforms a graph representing formula at transition to bdd.

This version of method is a more general one and accepts also formula including states.

Parameters:

graph – Graph to be transformed

Returns:

Resulting BDD

mata::IntermediateAut mintermize(const mata::IntermediateAut &aut)

Method mintermizes given automaton which has bitvector alphabet.

It transforms its transitions to BDDs, then build a minterm tree over the BDDs and finally transforms automaton to explicit one.

Parameters:

aut – Automaton to be mintermized.

Returns:

Mintermized automaton

std::vector<mata::IntermediateAut> mintermize(const std::vector<const mata::IntermediateAut*> &auts)

Methods mintermize given automata which have bitvector alphabet.

It transforms transitions of all automata to BDDs, then build a minterm tree over the BDDs and finally transforms automata to explicit one (sharing the same minterms).

Parameters:

auts – Automata to be mintermized.

Returns:

Mintermized automata corresponding to the input autamata

void minterms_to_aut_nfa(mata::IntermediateAut &res, const mata::IntermediateAut &aut, const std::unordered_set<BDD> &minterms)

The method performs the mintermization over @aut with given @minterms.

It is method specialized for NFA.

Parameters:

• res – The resulting mintermized automaton

• aut – Automaton to be mintermized

• minterms – Set of minterms for mintermization

void minterms_to_aut_afa(mata::IntermediateAut &res, const mata::IntermediateAut &aut, const std::unordered_set<BDD> &minterms)

The method for mintermization of alternating finite automaton using a given set of minterms.

Parameters:

• res – The resulting mintermized automaton

• aut – Automaton to be mintermized

• minterms – Set of minterms for mintermization