module Diagram:`sig`

..`end`

Ordered diagrams representing propositional formulas.

`val smallSIZE : ``int`

Suitable small size for hash modules.

`val bigSIZE : ``int`

Suitable big size for hash modules.

`val hashSIZE : ``int Pervasives.ref`

Hash size used when making the module. Set to smallSIZE by default.

`type ``'a`

diag_raw =

`|` |
`Empty` |

`|` |
`Unit` |

`|` |
`And of ` |

Diagrams represent propositional formulas as printed by diag_str.
Each path in the tree ending in Unit represents a clause,
the disjunction over directions taken to get there. (The first one
in And is "not var", the second "var" and the third is just "nothing",
so And (v, n, p, o) represents exactly "(v or n) and (-v or p) and o").
Assertions.
(0) variables on all paths appear in order given by

`cmp`

, lesser first
(1) no And(_,Empty,Empty,_) appears in the tree (clean unneeded t variables)
(2) no And(_,Unit,Unit,_) appears in the tree (clean unneeded f variables)
(3) no And(_,_,_,Unit) appears (unit, i.e. false, moves up)
(4) no And(_,Unit,x,_) or And(_,x,Unit,_) for x <> Empty (literals push)type`'a`

diag =`'a diag_raw HashCons.hc`

module type Variables =`sig`

..`end`

Variables of the diagrams must be ordered.

module type S =`sig`

..`end`

The module for ordered diagrams.

module Make:

Implementation of diagrams.

Easy creation of integer diagrams (a bit unsafe).

`val weights_array : ``int array Pervasives.ref`

Simply set this array to the weights of integers in your diagrams.

`val cmp_weight : ``int -> int -> int`

Compare by weight if present in array, else simply the natural order.
As it is used also for literals, it makes equal variables equal,
i.e. cmp_weight (-v) v = 0 for all v.

module WeightIntOrd:`Variables`

`with type t = int`

Variables module for integers using the weights.

module WeightDiags:`S`

`with type var = int`

Diagrams based on WeightIntOrd.

`val diag_of_qbf : ``?reverse:bool ->`

?elim_quant:bool -> ?weights:int array -> QBF.qbf -> WeightDiags.t

Make a diagram of a QBF. Works only for CNF for now. Sets the weight
of each variable v to the number of clauses it occurs in.

module BigIntOrd:`Variables`

`with type t = int`

Variables module for integers using the bigger integer always.

module BigIntDiags:`S`

`with type var = int`

Diagrams based on BigIntOrd.

`val shape : ``WeightDiags.t -> BigIntDiags.t`

Shape of a weight-based diagram as a canonical int diagram.