boolVar.ml 12.4 KB
Newer Older
1 2 3 4 5
let (<) : int -> int -> bool = (<)
let (>) : int -> int -> bool = (>)
let (=) : int -> int -> bool = (=)


6
module type S = sig
7

8
  module Atom : Bool.S
9

10
  include Bool.S with type elem = Atom.t Var.var_or_atom
11

12
  val var : Var.t -> t
13

14 15
  (** returns the union of all leaves in the BDD *)
  val leafconj: t -> Atom.t
16 17 18

  val is_empty : t -> bool

19
  val pp_print : Format.formatter -> t -> unit
20

21
  val print : ?f:(Format.formatter -> elem -> unit) -> t -> (Format.formatter -> unit) list
22
  val extract : t -> [ `Empty | `Full | `Split of (elem * t * t * t) ]
23

24 25 26 27 28
end

(* ternary BDD
 * where the nodes are Atm of X.t | Var of String.t
 * Variables are always before Values
29
 * All the leaves are then base types
30 31 32 33 34 35 36 37 38
 *
 * we add a third case when two leaves of the bdd are of the same
 * kind, that's it Val of t1 , Val of t2
 *
 * This representation can be used for all kinds.
 * Intervals, Atoms and Chars can be always merged (for union and intersection)
 * Products can be merged for intersections
 * Arrows can be never merged
 *
39
 * extract_var : copy the orginal tree and on one copy put to zero all
40 41 42 43
 * leaves that have an Atm on the other all leaves that have a Var
 *
 * *)

44
module Make (T : Bool.S) : S with module Atom = T and type elem = T.t Var.var_or_atom = struct
45 46
  (* ternary decision trees . cf section 11.3.3 Frish PhD *)
  (* plus variables *)
47 48
  (* `Atm are containers (Atoms, Chars, Intervals, Pairs ... )
   * `Var are String
49
   *)
50

51 52
  module Atom = T
  type elem = T.t Var.var_or_atom
53
  module X : Custom.T with type t = elem = Var.Make(T)
54 55 56 57
  type 'a bdd = False
               | True
               | Split of int * 'a * ('a bdd) * ('a bdd) * ('a bdd)

58 59 60
  type t = elem bdd

  let rec equal_aux eq a b =
61 62
    (a == b) ||
    match (a,b) with
63
      | Split (h1,x1,p1,i1,n1), Split (h2,x2,p2,i2,n2) ->
64
	  (h1 == h2) &&
65 66
	  (equal_aux eq p1 p2) && (equal_aux eq i1 i2) &&
	  (equal_aux eq n1 n2) && (eq x1 x2)
67 68
      | _ -> false

69 70
  let equal = equal_aux X.equal

71 72 73 74
(* Idea: add a mutable "unique" identifier and set it to
   the minimum of the two when egality ... *)

  let rec compare a b =
75
    if (a == b) then 0
76
    else match (a,b) with
77
      | Split (h1,x1, p1,i1,n1), Split (h2,x2, p2,i2,n2) ->
78
	  if h1 < h2 then -1 else if h1 > h2 then 1
79 80
	  else let c = X.compare x1 x2 in if c <> 0 then c
	  else let c = compare p1 p2 in if c <> 0 then c
81
	  else let c = compare i1 i2 in if c <> 0 then c
82
	  else compare n1 n2
83 84 85 86
      | True,_  -> -1
      | _, True -> 1
      | False,_ -> -1
      | _,False -> 1
87 88

  let rec hash = function
89 90 91
    | True -> 1
    | False -> 0
    | Split(h,_,_,_,_) -> h
92

93
  let compute_hash x p i n =
94
	(X.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)
95 96

  let rec check = function
97 98 99
    | True -> ()
    | False -> ()
    | Split (h,x,p,i,n) ->
100
	assert (h = compute_hash x p i n);
101 102 103
	(match p with Split (_,y,_,_,_) -> assert (X.compare x y < 0) | _ -> ());
	(match i with Split (_,y,_,_,_) -> assert (X.compare x y < 0) | _ -> ());
	(match n with Split (_,y,_,_,_) -> assert (X.compare x y < 0) | _ -> ());
104 105 106 107
	X.check x; check p; check i; check n

  let atom x =
    let h = X.hash x + 17 in (* partial evaluation of compute_hash... *)
108
    Split (h, x,True,False,False)
109

110
  let var v =
111
    let compute_hash x p i n =
112 113
        (Var.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)
    in
114
    let a = atom (`Atm T.full) in
115 116
    let h = compute_hash v a False False in
    ( Split (h,`Var v,a,False,False) :> t )
117 118

  let rec iter f = function
119
    | Split (_, x, p,i,n) -> f x; iter f p; iter f i; iter f n
120 121 122
    | _ -> ()

  let rec dump ppf = function
123 124
    | False -> Format.fprintf ppf "⊥"
    | True -> Format.fprintf ppf "⊤"
125
    | Split (_,x, p,i,n) ->
126 127 128 129 130 131 132 133 134 135
      let fmt = format_of_string (
        match x with
          `Var _ ->
            "@[{@[%a@]}{@[<hov>%a,@ %a,@ %a@]}@]"
        | `Atm _ ->
          "@[ {@[%a@]}@\n {@[<hov>%a,@ %a,@ %a@]}@]"
      )
      in
      Format.fprintf ppf fmt
        X.dump x dump p dump i dump n
136 137

  let rec print f ppf = function
138 139 140
    | True -> Format.fprintf ppf "Any"
    | False -> Format.fprintf ppf "Empty"
    | Split (_, x, p,i, n) ->
141 142
	let flag = ref false in
	let b () = if !flag then Format.fprintf ppf " | " else flag := true in
143
	(match p with
144 145
	   | True -> b(); Format.fprintf ppf "%a" f x
	   | False -> ()
146
	   | _ -> b (); Format.fprintf ppf "%a & @[(%a)@]" f x (print f) p );
147
	(match i with
148 149
	   | True -> assert false;
	   | False -> ()
150
	   | _ -> b(); print f ppf i);
151
	(match n with
152 153
	   | True -> b (); Format.fprintf ppf "@[~%a@]" f x
	   | False -> ()
154
	   | _ -> b (); Format.fprintf ppf "@[~%a@] & @[(%a)@]" f x (print f) n)
155

Pietro Abate's avatar
Pietro Abate committed
156
  let pp_print = print X.dump
157

158
  let print ?(f=X.dump) = function
159 160
    | True -> assert false (* [] a bdd cannot be of this type *)
    | False -> [ fun ppf -> Format.fprintf ppf "Empty" ]
161
    | c -> [ fun ppf -> print f ppf c ]
162

163 164 165 166
  (* return a list of pairs, where each pair holds the list
   * of positive and negative elements on a branch *)
  let get x =
    let rec aux accu pos neg = function
167 168 169
      | True -> (List.rev pos, List.rev neg) :: accu
      | False -> accu
      | Split (_,x, p,i,n) ->
170 171 172 173 174 175
        let accu = aux accu (x::pos) neg p in
        let accu = aux accu pos (x::neg) n in
        let accu = aux accu pos neg i in
        accu
    in aux [] [] [] x

176

177
  let leafconj x =
178
    let rec aux accu = function
179 180 181 182 183
      | True -> accu
      | False -> accu
      | Split (_,`Atm x, True,False,False) -> x :: accu
      | Split (_,`Atm x, _,_,_) -> assert false
      | Split (_,`Var x, p,i,n) ->
184 185 186 187 188 189
        let accu = aux accu p in
        let accu = aux accu n in
        let accu = aux accu i in
        accu
    in
    List.fold_left T.cup T.empty (aux [] x)
190 191 192

  let compute ~empty ~full ~cup ~cap ~diff ~atom b =
    let rec aux = function
193 194 195 196 197
      | True  -> full
      | False -> empty
      | Split (_,`Atm x,True,_,_) when T.equal x T.empty -> empty
      | Split (_,`Atm x,True,_,_) when T.equal x T.full -> full
      | Split(_,x, p,i,n) ->
198 199 200 201 202
        let x1 = atom x in
	let p = cap x1 (aux p) in
        let i = aux i in
        let n = diff (aux n) x1 in
	cup (cup p i) n
203 204
    in
    aux b
205

206 207 208
(* Invariant: correct hash value *)

  let split0 x pos ign neg =
209
    Split (compute_hash x pos ign neg, x, pos, ign, neg)
210

211 212
  let empty = False
  let full = split0 (`Atm T.full) True False False
213 214 215 216

  let is_empty t = (t == empty)

(* Invariants:
217
     Split (x, pos,ign,neg) ==>  (ign <> True), (pos <> neg)
218 219 220 221
*)

  let rec has_true = function
    | [] -> false
222
    | True :: _ -> true
223 224
    | _ :: l -> has_true l

225 226 227 228
  let rec has_same a = function
    | [] -> false
    | b :: l -> (equal a b) || (has_same a l)

229 230
  (* split removes redundant subtrees from the positive and negative
   * branch if they are present in the lazy union branch *)
231
  let rec split x p i n =
232
    if X.equal (`Atm T.empty) x then False
233
    (* 0?p:i:n -> 0 *)
234
    else if i == True then True
235 236 237 238
    (* x?p:1:n -> 1 *)
    else if equal p n then p ++ i
    else let p = simplify p [i] and n = simplify n [i] in
    (* x?p:i:n when p = n -> bdd of (p ++ i) *)
239
    if equal p n then p ++ i
240 241 242 243 244
    else split0 x p i n

  (* simplify t l -> bdd of ( t // l ) *)
  and simplify a l =
    match a with
245 246 247 248 249 250
      | False -> False
      | True -> if has_true l then False else True
      | Split (_,`Atm x, False,False,True) ->
          split (`Atm(T.diff T.full x)) True False False
      | Split (_,x,p,i,n) ->
        if (has_true l) || (has_same a l) then False
251 252
        else s_aux2 a x p i n [] [] [] l
  and s_aux2 a x p i n ap ai an = function
253 254
    | [] ->
      let p = simplify p ap
255 256 257
      and n = simplify n an
      and i = simplify i ai in
      if equal p n then p ++ i else split0 x p i n
258
    | b :: l -> s_aux3 a x p i n ap ai an l b
259
  and s_aux3 a x p i n ap ai an l = function
260 261 262 263
    | False -> s_aux2 a x p i n ap ai an l
    | True -> assert false
    | Split (_,x2,p2,i2,n2) as b ->
      if equal a b then False
264 265 266 267 268 269 270 271 272
      else let c = X.compare x2 x in
      if c < 0 then s_aux3 a x p i n ap ai an l i2
      else if c > 0 then s_aux2 a x p i n (b :: ap) (b :: ai) (b :: an) l
      else s_aux2 a x p i n (p2 :: i2 :: ap) (i2 :: ai) (n2 :: i2 :: an) l

  (* Inv : all leafs are of type Atm and they are always merged *)
  (* union *)
  and ( ++ ) a b = if a == b then a
  else match (a,b) with
273 274
    | True, _ | _, True -> True
    | False, a | a, False -> a
275

276 277
    | Split (_,`Atm x1, True,False,False), Split (_,`Atm x2, True,False,False) ->
        split (`Atm (T.cup x1 x2)) True False False
278

279 280 281
    | Split (_,`Atm x1, False,False,True), Split (_,`Atm x2, False,False,True)
    | Split (_,`Atm x1, True,False,False), Split (_,`Atm x2, False,False,True)
    | Split (_,`Atm x1, False,False,True), Split (_,`Atm x2, True,False,False) ->
282
        assert false
283

284
    | Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
285 286 287 288
      let c = X.compare x1 x2 in
      if c = 0 then split x1 (p1 ++ p2) (i1 ++ i2) (n1 ++ n2)
      else if c < 0 then split x1 p1 (i1 ++ b) n1
      else split x2 p2 (i2 ++ a) n2
289 290 291 292 293 294

(* seems better not to make ++ and this split mutually recursive;
   is the invariant still inforced ? *)

  (* intersection *)
  let rec ( ** ) a b = if a == b then a else match (a,b) with
295 296
    | True, a | a, True -> a
    | False, _ | _, False -> False
297

298 299
    | Split (_,`Atm x1, True,False,False), Split (_,`Atm x2, True,False,False) ->
        split (`Atm(T.cap x1 x2)) True False False
300

301 302
    | Split (_,`Atm x1, False,False,True), Split (_,`Atm x2, False,False,True) ->
        split (`Atm(T.cap (T.diff T.full x1) (T.diff T.full x2))) True False False
303

304 305
    | Split (_,`Atm x1, True,False,False), Split (_,`Atm x2, False,False,True) ->
        split (`Atm(T.cap x1 (T.diff T.full x2))) True False False
306

307 308
    | Split (_,`Atm x1, False,False,True), Split (_,`Atm x2, True,False,False) ->
        split (`Atm(T.cap (T.diff T.full x1) x2)) True False False
309

310
    | Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
311 312
	let c = X.compare x1 x2 in
	if c = 0 then
313
	  split x1
314 315
	    (p1 ** (p2 ++ i2) ++ (p2 ** i1))
	    (i1 ** i2)
316
	    (n1 ** (n2 ++ i2) ++ (n2 ** i1))
317 318 319 320
	else if c < 0 then split x1 (p1 ** b) (i1 ** b) (n1 ** b)
	else split x2 (p2 ** a) (i2 ** a) (n2 ** a)

  let rec trivially_disjoint a b =
321
    if a == b then a == False
322
    else match (a,b) with
323 324 325
      | True, a | a, True -> a == False
      | False, _ | _, False -> true
      | Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
326 327 328 329 330 331 332 333 334 335 336 337 338 339 340
	  let c = X.compare x1 x2 in
	  if c = 0 then
(* try expanding -> p1 p2; p1 i2; i1 p2; i1 i2 ... *)
	    trivially_disjoint (p1 ++ i1) (p2 ++ i2) &&
	    trivially_disjoint (n1 ++ i1) (n2 ++ i2)
	  else if c < 0 then
	    trivially_disjoint p1 b &&
	    trivially_disjoint i1 b &&
	    trivially_disjoint n1 b
	  else
	    trivially_disjoint p2 a &&
	    trivially_disjoint i2 a &&
	    trivially_disjoint n2 a

  let rec neg = function
341 342 343 344 345 346 347 348
    | True -> False
    | False -> True
    | Split (_,`Atm x, True,False,False) -> split0 (`Atm(T.diff T.full x)) True False False
    | Split (_,`Atm x, False,False,True) -> split0 (`Atm(T.diff T.full x)) True False False
    | Split (_,x, p,i,False) -> split x False (neg (i ++ p)) (neg i)
    | Split (_,x, False,i,n) -> split x (neg i) (neg (i ++ n)) False
    | Split (_,x, p,False,n) -> split x (neg p) (neg (p ++ n)) (neg n)
    | Split (_,x, p,i,n) -> split x (neg (i ++ p)) False (neg (i ++ n))
349

350 351
  let rec ( // ) a b =
    let negatm = T.diff T.full in
352
    if a == b then False
353
    else match (a,b) with
354 355 356
      | False,_ | _, True -> False
      | a, False -> a
      | True, b -> neg b
357

358 359
      | Split (_,`Atm x1, True,False,False), Split (_,`Atm x2, True,False,False) ->
          split (`Atm(T.diff x1 x2)) True False False
360

361 362
      | Split (_,`Atm x1, False,False,True), Split (_,`Atm x2, False,False,True) ->
          split (`Atm(T.diff (negatm x1) (negatm x2))) True False False
363

364 365
      | Split (_,`Atm x1, True,False,False), Split (_,`Atm x2, False,False,True) ->
          split (`Atm(T.diff x1 (negatm x2))) True False False
366

367 368
      | Split (_,`Atm x1, False,False,True), Split (_,`Atm x2, True,False,False) ->
          split (`Atm(T.diff (negatm x1) x2)) True False False
369

370
      | Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
371 372
	  let c = X.compare x1 x2 in
	  if c = 0 then
373
	    if (i2 == False) && (n2 == False)
374
	    then split x1 (p1 // p2) (i1 // p2) (n1 ++ i1)
375
	    else
376
	      split x1 ((p1++i1) // (p2 ++ i2)) False ((n1++i1) // (n2 ++ i2))
377
	  else if c < 0 then
378
	    split x1 (p1 // b) (i1 // b) (n1 // b)
379
	  else
380
	    split x2 (a // (i2 ++ p2)) False (a // (i2 ++ n2))
381

382 383 384 385
  let cup = ( ++ )
  let cap = ( ** )
  let diff = ( // )

386 387 388 389 390 391
  let extract =
    function
    | False -> `Empty
    | True -> `Full
    | Split (_,x,p,i,n) -> `Split (x,p,i,n)

392
end