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.