module Bes:`sig`

..`end`

Operations for minimization of Boolean expressions.

type`ext_bool =`

`[ `Dontcare | `False | `True ]`

A boolean type with 3 values : true, false and don't care

type`dnf_minterm =`

`ext_bool list`

A minterm with true, false and dont't care values.

type`dnf_expression =`

`dnf_minterm list`

A sum of minterms.

`type `

optimization_algorithm =

`|` |
`Qmc` |
`(*` | Only Quine-McCluskey. | `*)` |

`|` |
`Qmc_CyclicCore` |
`(*` | Quine-McCluskey, then cyclic core. | `*)` |

`|` |
`Qmc_SimpleHeuristic_SortOnce` |
`(*` | Quine-McCluskey, then cyclic core, then heuristic cover search. The impicants are sorted by the number of covered minterms once before the optimization. The length of the implications is used as the heuristic value. | `*)` |

`|` |
`Qmc_SimpleHeuristic_SortEachTime` |
`(*` | Quine-McCluskey, then cyclic core, then heuristic cover search. The impicants are sorted by the number of covered minterms after each step. The length of the implications is used as the heuristic value. | `*)` |

`|` |
`Qmc_SimpleHeuristic_AdvancedHeuristic` |
`(*` | Quine-McCluskey, then cyclic core, then heuristic cover search. The impicants are sorted after each step. Advanced heuristic formula (see thesis) is used to calculate the heuristic value | `*)` |

`|` |
`Qmc_SimpleHeuristic_Best` |
`(*` | Quine-McCluskey, then cyclic core, then heuristic cover search. The impicants are sorted by after each step. Advanced heurisitc or the length of the implications is used as heuristic value, depending on the better results. | `*)` |

`|` |
`Qmc_PetricksMethod` |
`(*` | Quine-McCluskey and then Petrick's method. | `*)` |

`|` |
`In_Place_Heuristic` |
`(*` | EXPREREMNTAL, NOT TESTED: A heuristic optimization method that uses the Expand and Irrendundant (Here simple heuristic with advanced heuristic formaula) steps instead of the QMC algorithm | `*)` |

The algorithm for the optimization.

`val set_verbose_mode : ``bool -> unit`

Turns on or off the output of debug messages.
This is turned off by default.

`val set_result_verification : ``bool -> unit`

Sets whether the optimization results should be verfied.
This is done by testing of the equivalence of the original
expression and the minimized one. This is turned off by default.

`val optimize : ``optimization_algorithm -> dnf_expression -> dnf_expression`

Optimizes the given expression with the specified algorithm.

`val auto_optimize : ``dnf_expression -> dnf_expression * bool`

Optimizes the given expression with the suitable algoirthm.
When there is more then 12 non essential prime implicants
Qmc_SimpleHeuristic_Best is used, otherwise Qmc_PetricksMethod.
The result is a tuple of the minimized expression and a boolean
which indicates whether the optimization was exact (true) or not.

`val dnf_minterm_of_string : ``string -> dnf_minterm`

Converts the given string to a minterm. '1' is true,
'0' is false and 'x' is don't matter.

`val dnf_expression_of_string : ``char -> string -> dnf_expression`

Converts the given string, separated by the given separator to
a dnf expression. '1' is true, '0' is false and 'x'
is don't matter.

`val dnf_expression_of_string_list : ``string list -> dnf_expression`

Converts the given string list to a dnf expression.
'1' is true, '0' is false and 'x' is don't matter.

`val load_from_file : ``string -> dnf_expression`

Loads a dnf expression from file with the given name. The file should
contain one minterm per line. The format of the minterm
representations is as following: '1' means true, '0' means false and
'x' means don't matter. Lines starting with any other
characters then '0', '1' or 'x' are ignored.

`val string_of_dnf_expression : ``dnf_expression -> string`

Converts a dnf expression to a string.

`val string_of_dnf_minterm : ``dnf_minterm -> string`

Converts a minterm of a dnf expression to a string.

`val print_dnf_expression : ``dnf_expression -> unit`

Prints a dnf expression to the standard output.

`val print_dnf_minterm : ``dnf_minterm -> unit`

Prints a minterm of a dnf expression to the standard
output.