Header menu logo F# Header menu logo Averest

LogicMin Module

This module implements algorithms for logic minimization

Functions and values

Function or value Description

DualRails inputSet posName negName phi

Full Usage: DualRails inputSet posName negName phi

Parameters:
    inputSet : Set<BoolExpr>
    posName : string -> string
    negName : string -> string
    phi : BoolExpr

Returns: BoolExpr * BoolExpr

Dual-rail encoding of a formula: If a variable x belongs to inputSet, it will be encoded as (x,!x) instead of (x+,x-).

inputSet : Set<BoolExpr>
posName : string -> string
negName : string -> string
phi : BoolExpr
Returns: BoolExpr * BoolExpr

KarnaughVeitch atomL

Full Usage: KarnaughVeitch atomL

Parameters:
Returns: Map<BoolExpr, bool>[] * Map<BoolExpr, bool>[]

Computes a KV diagram for a given list of atoms. The KV diagram is given as two arrays (col,row) where col and row denote the column and row vectors, respectively, i.e., col[i] and row[j] denote the assignments to the variables in entry (i,j) of the KV diagram, and their union is therefore the assignment to be evaluated there.

atomL : BoolExpr list
Returns: Map<BoolExpr, bool>[] * Map<BoolExpr, bool>[]

MkPrimImplicantBDD phi

Full Usage: MkPrimImplicantBDD phi

Parameters:
Returns: BoolExpr list list * BddAdr * BddAdr
phi : BoolExpr
Returns: BoolExpr list list * BddAdr * BddAdr

PrintKarnaughVeitch atomL (col, row) care phi

Full Usage: PrintKarnaughVeitch atomL (col, row) care phi

Parameters:

Print a KV diagram as constructed by KarnaughVeitch as a html table.

atomL : BoolExpr list
col : Map<BoolExpr, bool> seq
row : Map<BoolExpr, bool> seq
care : BoolExpr
phi : BoolExpr

QuineCube2BitvecStr atomL (idx, arg3)

Full Usage: QuineCube2BitvecStr atomL (idx, arg3)

Parameters:
Returns: string

Convert a cube (idx,(pos,neg)) as used in the Quine table to a string. The index set idx is written as a set of integers {i1,...,iN} and the cube (pos,neg) itself is written as a bitvector with * whenever there is a don't care.

atomL : BoolExpr list
idx : Set<'a>
arg2 : Set<BoolExpr> * Set<BoolExpr>
Returns: string

QuineCube2Minterm atomL (idx, arg3)

Full Usage: QuineCube2Minterm atomL (idx, arg3)

Parameters:
Returns: BoolExpr

Convert a cube (idx,(pos,neg)) as used in the Quine table to a boolean expression where the literals occur as specified by the variable order atomL.

atomL : BoolExpr list
idx : 'a
arg2 : Set<BoolExpr> * Set<BoolExpr>
Returns: BoolExpr

QuineMcCluskeyMinimalDNF atomL care phi

Full Usage: QuineMcCluskeyMinimalDNF atomL care phi

Parameters:
Returns: (Set<int> * (Set<BoolExpr> * Set<BoolExpr>)) list list list * (BoolExpr * (Set<int> * (Set<BoolExpr> * Set<BoolExpr>))) list * BoolExpr * Set<Set<BoolExpr>> * Set<BoolExpr>

The following function computes minimal DNFs for a given formula phi with a care set care, where the ordering of atoms atomL is respected. The function applies first the Quine method QuineTable to compute all cubes (implicants) of care->phi, and extracts then the prime cubes with function QuineTablePrimeImplicants where each prime cube is associated with a new boolean variable PI[i]. After this, it generates a formula coverPhi in CNF over the variables PI[i] such that coverPhi has a disjunct for each model of care&phi and that contains all PI[i] that cover that model. The formula coverPhi is then converted to DNF (in sets of sets representation) so that minimal DNFs for phi wrt. care can be derived. The function finally returns a tuple (qt,primeCubes,coverPhi,dnfCover,minDNFs) with:

  • qt is the Quine table as generated by function QuineTable.
  • primeCubes is a list of pairs (PI[i],pc[i]) where pi is a variable associated with prime cube pc[i].
  • coverPhi is the cover formula using variables PI[i] in CNF.
  • dnfCover is the set of set representation of coverPhi.
  • minDNFs is the list of minimal DNFs of phi wrt. care set care.

atomL : BoolExpr list
care : BoolExpr
phi : BoolExpr
Returns: (Set<int> * (Set<BoolExpr> * Set<BoolExpr>)) list list list * (BoolExpr * (Set<int> * (Set<BoolExpr> * Set<BoolExpr>))) list * BoolExpr * Set<Set<BoolExpr>> * Set<BoolExpr>

QuineTable atomL phi

Full Usage: QuineTable atomL phi

Parameters:
Returns: (Set<int> * (Set<BoolExpr> * Set<BoolExpr>)) list list list

Compute the Quine table: The function expects a formula phi and its variable order order atomL. It computes the Quine table that contains all implicants of phi as a list of list of lists [I0;...;In] where each Ik is the list of list of implicants of order k, i.e., where k variables are don't cares, hence, I0 are all full models of phi. Each Ik=[Lk0;...;Lkj] is partitioned into levels Lki according to the number of atoms made true (zero in Lk0 up to j in Lkj]. Each Lki is finally a list of cubes, where a cube (idx,(pos,neg)) is given by the sets of atoms (pos,neg) made true and false by the cube, respectively. The index idx is a set of integers that uniquely represents the cube; it is the union of binary numbers that an be derived when all don't cares are replaced by either true and false (following the order atomL).

atomL : BoolExpr list
phi : BoolExpr
Returns: (Set<int> * (Set<BoolExpr> * Set<BoolExpr>)) list list list

QuineTable2Html atomL qt

Full Usage: QuineTable2Html atomL qt

Parameters:

Print a Quine table as a html table

atomL : BoolExpr list
qt : (Set<int> * (Set<BoolExpr> * Set<BoolExpr>)) list list list

QuineTablePrimeImplicants qt

Full Usage: QuineTablePrimeImplicants qt

Parameters:
Returns: (BoolExpr * (Set<int> * (Set<BoolExpr> * Set<BoolExpr>))) list

Get the prime implicants of a formula phi from its Quine table: We check whether the index set of a cube is contained in one of the other cube's index set of the next level. If so, it is not a prime implicant, since it has been used to construct that higher cube. The function returns a list of tuples (piv,(idx,(pos,neg))) where piv is a boolean variable generated for the prime implicant (idx,(pos,neg)).

qt : (Set<int> * (Set<BoolExpr> * Set<BoolExpr>)) list list list
Returns: (BoolExpr * (Set<int> * (Set<BoolExpr> * Set<BoolExpr>))) list

Type something to start searching.