Module Diagram

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 'a * 'a diag * 'a diag * 'a diag`

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: functor (V : Variables) -> S  with type var = V.t

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.