| 1 |
(* Implementation of boolean combination in disjunctive normal form (dnf).
|
| 2 |
A dnf is a disjunction of lines, each line consisting of a
|
| 3 |
conjunction of atoms and negations of atoms.
|
| 4 |
|
| 5 |
A line is coded as a pair (p,n) where p collects atoms and n
|
| 6 |
the negated atoms. p and n are disjoint and sorted lists without duplicates
|
| 7 |
(w.r.t Pervasives.compare).
|
| 8 |
|
| 9 |
A dnf is coded as a sorted list of lines without duplicated
|
| 10 |
(w.r.t Pervasives.compare).
|
| 11 |
*)
|
| 12 |
|
| 13 |
module type S =
|
| 14 |
sig
|
| 15 |
type 'a elem
|
| 16 |
type 'a t
|
| 17 |
|
| 18 |
val equal : 'a t -> 'a t -> bool
|
| 19 |
val compare: 'a t -> 'a t -> int
|
| 20 |
val hash: 'a t -> int
|
| 21 |
|
| 22 |
external get: 'a t -> ('a elem list * 'a elem list) list = "%identity"
|
| 23 |
|
| 24 |
val empty : 'a t
|
| 25 |
val full : 'a t
|
| 26 |
val cup : 'a t -> 'a t -> 'a t
|
| 27 |
val cap : 'a t -> 'a t -> 'a t
|
| 28 |
val diff : 'a t -> 'a t -> 'a t
|
| 29 |
val atom : 'a elem -> 'a t
|
| 30 |
|
| 31 |
val map : ('a elem-> 'b elem) -> 'a t -> 'b t
|
| 32 |
val iter: ('a elem-> unit) -> 'a t -> unit
|
| 33 |
val compute: empty:'d -> full:'c -> cup:('d -> 'c -> 'd)
|
| 34 |
-> cap:('c -> 'b -> 'c) -> diff:('c -> 'b -> 'c) ->
|
| 35 |
atom:('a elem -> 'b) -> 'a t -> 'd
|
| 36 |
val compute_bool: ('a elem -> 'b t) -> 'a t -> 'b t
|
| 37 |
|
| 38 |
val print: string -> (Format.formatter -> 'a elem -> unit) -> 'a t ->
|
| 39 |
(Format.formatter -> unit) list
|
| 40 |
|
| 41 |
|
| 42 |
val trivially_disjoint : 'a t -> 'a t -> bool
|
| 43 |
val check: 'a t -> unit
|
| 44 |
end
|
| 45 |
|
| 46 |
module Make(X : SortedList.ARG) : S with type 'a elem = 'a X.t
|
| 47 |
|
| 48 |
include S with type 'a elem = 'a and type 'a t = ('a list * 'a list) list
|
Parent Directory
| 
Revision Log