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

5 6
module type S =
sig
7 8
  type elem
  include Custom.T
9

10
  val get: t -> (elem list * elem list) list
11

12 13 14 15 16 17
  val empty : t
  val full  : t
  val cup   : t -> t -> t
  val cap   : t -> t -> t
  val diff  : t -> t -> t
  val atom  : elem -> t
18

19
  val iter: (elem-> unit) -> t -> unit
20

21 22 23 24 25
  val compute:
    empty:'b -> full:'b ->
    cup:('b -> 'b -> 'b) ->
    cap:('b -> 'b -> 'b) ->
    diff:('b -> 'b -> 'b) ->
26
    atom:(elem -> 'b) -> t -> 'b
27

28
  val trivially_disjoint: t -> t -> bool
29

30 31
end

32 33

module Make(X : Custom.T) =
34
struct
35 36
  type elem = X.t
  type t =
37 38
    | True
    | False
39
    | Split of int * elem * t * t * t
40

41 42 43 44 45
  let rec equal a b =
    (a == b) ||
    match (a,b) with
      | Split (h1,x1, p1,i1,n1), Split (h2,x2, p2,i2,n2) ->
	  (h1 == h2) &&
46 47
	  (equal p1 p2) && (equal i1 i2) &&
	  (equal n1 n2) && (X.equal x1 x2)
48 49
      | _ -> false

50 51 52
(* Idea: add a mutable "unique" identifier and set it to
   the minimum of the two when egality ... *)

53
  let rec compare a b =
54
    if (a == b) then 0
55 56
    else match (a,b) with
      | Split (h1,x1, p1,i1,n1), Split (h2,x2, p2,i2,n2) ->
57
	  if h1 < h2 then -1 else if h1 > h2 then 1
58 59
	  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
60
	  else let c = compare i1 i2 in if c <> 0 then c
61 62 63 64 65
	  else compare n1 n2
      | True,_  -> -1
      | _, True -> 1
      | False,_ -> -1
      | _,False -> 1
66 67


68 69 70 71 72
  let rec hash = function
    | True -> 1
    | False -> 0
    | Split(h, _,_,_,_) -> h

73
  let compute_hash x p i n =
74 75
	(X.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)

76 77 78 79 80 81 82
  let rec check = function
    | True | False -> ()
    | Split (h,x,p,i,n) ->
	assert (h = compute_hash x p i n);
	(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) | _ -> ());
83
	X.check x; check p; check i; check n
84

85 86 87
  let atom x =
    let h = X.hash x + 17 in (* partial evaluation of compute_hash... *)
    Split (h, x,True,False,False)
88

89 90 91
  let neg_atom x =
    let h = X.hash x + 16637 in (* partial evaluation of compute_hash... *)
    Split (h, x,False,False,True)
92 93 94 95 96 97

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

  let rec dump ppf = function
98
    | False -> Format.fprintf ppf "⊥"
99
    | True -> Format.fprintf ppf "⊤"
100 101 102
    | Split (_,x, p,i,n) ->
      Format.fprintf ppf "@[@[%a@][@[<hov>%a,@\n%a,@\n%a@]]@]"
	X.dump x dump p dump i dump n
103

104 105 106 107 108 109
  let rec print f ppf = function
    | True -> Format.fprintf ppf "Any"
    | False -> Format.fprintf ppf "Empty"
    | Split (_, x, p,i, n) ->
	let flag = ref false in
	let b () = if !flag then Format.fprintf ppf " | " else flag := true in
110
	(match p with
111 112 113
	   | True -> b(); Format.fprintf ppf "%a" f x
	   | False -> ()
	   | _ -> b (); Format.fprintf ppf "%a & @[(%a)@]" f x (print f) p );
114
	(match i with
115 116 117
	   | True -> assert false;
	   | False -> ()
	   | _ -> b(); print f ppf i);
118
	(match n with
119 120 121
	   | True -> b (); Format.fprintf ppf "@[~%a@]" f x
	   | False -> ()
	   | _ -> b (); Format.fprintf ppf "@[~%a@] & @[(%a)@]" f x (print f) n)
122

123 124 125 126
  let print a f = function
    | True -> [ fun ppf -> Format.fprintf ppf "%s" a ]
    | False -> []
    | c -> [ fun ppf -> print f ppf c ]
127 128


129 130 131 132
  let rec get accu pos neg = function
    | True -> (pos,neg) :: accu
    | False -> accu
    | Split (_,x, p,i,n) ->
133
	(*OPT: can avoid creating this list cell when pos or neg =False *)
134 135 136 137
	let accu = get accu (x::pos) neg p in
	let accu = get accu pos (x::neg) n in
	let accu = get accu pos neg i in
	accu
138

139
  let get x = get [] [] [] x
140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157

  let rec get' accu pos neg = function
    | True -> (pos,neg) :: accu
    | False -> accu
    | Split (_,x,p,i,n) ->
	let accu = get' accu (x::pos) neg p in
	let rec aux l = function
	  | Split (_,x,False,i,n') when equal n n' ->
	      aux (x :: l) i
	  | i ->
(*	      if (List.length l > 1) then (print_int (List.length l); flush stdout); *)
	      let accu = get' accu pos (l :: neg) n in
	      get' accu pos neg i
	in
	aux [x] i

  let get' x = get' [] [] [] x

158 159 160 161 162
  let compute ~empty ~full ~cup ~cap ~diff ~atom b =
    let rec aux = function
      | True -> full
      | False -> empty
      | Split(_,x, p,i,n) ->
163 164 165 166 167
          let x1 = atom x in
          let p = cap x1 (aux p)
          and i = aux i
          and n = diff (aux n) x1 in
          cup (cup p i) n
168 169
    in
    aux b
170

171 172
(* Invariant: correct hash value *)

173
  let split0 x pos ign neg =
174 175 176 177
    Split (compute_hash x pos ign neg, x, pos, ign, neg)

  let empty = False
  let full = True
178 179

(* Invariants:
180
     Split (x, pos,ign,neg) ==>  (ign <> True), (pos <> neg)
181 182
*)

183 184 185 186
  let rec has_true = function
    | [] -> false
    | True :: _ -> true
    | _ :: l -> has_true l
187

188 189 190
  let rec has_same a = function
    | [] -> false
    | b :: l -> (equal a b) || (has_same a l)
191

192
  let rec split x p i n =
193
    if i == True then True
194 195 196 197
    else if equal p n then p ++ i
    else let p = simplify p [i] and n = simplify n [i] in
    if equal p n then p ++ i
    else split0 x p i n
198

199 200 201 202 203 204 205 206
  and simplify a l =
    match a with
      | False -> False
      | True -> if has_true l then False else True
      | Split (_,x,p,i,n) ->
	  if (has_true l) || (has_same a l) then False
	  else s_aux2 a x p i n [] [] [] l
  and s_aux2 a x p i n ap ai an = function
207 208
    | [] ->
	let p = simplify p ap
209 210 211
	and n = simplify n an
	and i = simplify i ai in
	if equal p n then p ++ i else split0 x p i n
212
    | b :: l -> s_aux3 a x p i n ap ai an l b
213 214
  and s_aux3 a x p i n ap ai an l = function
    | False -> s_aux2 a x p i n ap ai an l
215 216
    | True -> assert false
    | Split (_,x2,p2,i2,n2) as b ->
217
	if equal a b then False
218 219 220 221 222 223 224 225 226 227 228 229 230 231
	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

  and ( ++ ) a b = if a == b then a
  else match (a,b) with
    | True, _ | _, True -> True
    | False, a | a, False -> a
    | Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
	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
232 233 234 235

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

236 237 238 239 240 241
  let rec ( ** ) a b = if a == b then a else match (a,b) with
    | True, a | a, True -> a
    | False, _ | _, False -> False
    | Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
	let c = X.compare x1 x2 in
	if c = 0 then
242
	  split x1
243 244
	    (p1 ** (p2 ++ i2) ++ (p2 ** i1))
	    (i1 ** i2)
245 246
	    (n1 ** (n2 ++ i2) ++ (n2 ** i1))
(*	  if (p2 == True) && (n2 == False)
247 248 249
	  then split x1 (p1 ++ i1) (i1 ** i2) (n1 ** i2)
	  else if (p2 == False) && (n2 == True)
	  then split x1 (p1 ** i2) (i1 ** i2) (n1 ++ i1)
250 251
	  else
	    split x1 ((p1++i1) ** (p2 ++ i2)) False ((n1 ++ i1) ** (n2 ++ i2))
252 253 254
*)
	else if c < 0 then split x1 (p1 ** b) (i1 ** b) (n1 ** b)
	else split x2 (p2 ** a) (i2 ** a) (n2 ** a)
255

256
  let rec trivially_disjoint a b =
257
    if a == b then a == False
258
    else match (a,b) with
259
      | True, a | a, True -> a == False
260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275
      | False, _ | _, False -> true
      | Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
	  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

276 277 278
  let rec neg = function
    | True -> False
    | False -> True
279
    | Split (_,x, p,i,False) -> split x False (neg (i ++ p)) (neg i)
280 281 282
    | 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, False, False) ->
283 284
	split x False (neg p) True
    | Split (_,x, False, False, n) -> split x True (neg n) False *)
285
    | Split (_,x, p,i,n) -> split x (neg (i ++ p)) False (neg (i ++ n))
286 287

  let rec ( // ) a b =
288
(*    if equal a b then False  *)
289
    if a == b then False
290 291 292 293 294 295 296
    else match (a,b) with
      | False,_ | _, True -> False
      | a, False -> a
      | True, b -> neg b
      | Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
	  let c = X.compare x1 x2 in
	  if c = 0 then
297
	    if (i2 == False) && (n2 == False)
298 299 300
	    then split x1 (p1 // p2) (i1 // p2) (n1 ++ i1)
(*	    else if (i2 == False) && (p2 == False)
	    then split x1 (p1 ++ i1) (i1 // n2) (n1 // n2) *)
301
	    else
302
	      split x1 ((p1++i1) // (p2 ++ i2)) False ((n1++i1) // (n2 ++ i2))
303
	  else if c < 0 then
304
	    split x1 (p1 // b) (i1 // b) (n1 // b)
305 306 307
(*	    split x1 ((p1 ++ i1)// b) False ((n1 ++i1) // b)  *)
	  else
	    split x2 (a // (i2 ++ p2)) False (a // (i2 ++ n2))
308

309 310 311 312 313

  let cup = ( ++ )
  let cap = ( ** )
  let diff = ( // )

314
end
315

316 317
module type V =
sig
318

319 320 321
  module Atom : S

  include S with type elem = Atom.t Var.var_or_atom
322

323 324 325 326 327 328 329 330 331
  val var : Var.t -> t

  (** returns the union of all leaves in the BDD *)

  val leafconj: t -> Atom.t

  val is_empty : t -> bool

  val extract : t -> [ `Empty | `Full | `Split of (elem * t * t * t) ]
332

333
end
334 335

module MakeVar (T : S) =
336
struct
337 338 339
  module Atom = T
  module X = Var.Make(Atom)
  include Make(X)
340

341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372
  let var v =
    let compute_hash x p i n =
        (Var.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)
    in
    let a = atom (`Atm T.full) in
    let h = compute_hash v a False False in
    (Split (h,`Var v, a, False, False) :> t )

  let get x =
    let rec aux accu pos neg = function
      | True -> (List.rev pos, List.rev neg) :: accu
      | False -> accu
      | Split (_,x, p,i,n) ->
        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

  let leafconj x =
    let rec aux accu = function
      | True -> accu
      | False -> accu
      | Split (_,`Atm x, True,False,False) -> x :: accu
      | Split (_,`Atm x, _,_,_) -> assert false
      | Split (_,`Var x, p,i,n) ->
        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)
373

374 375 376 377 378 379 380 381 382 383 384 385 386 387
  let compute ~empty ~full ~cup ~cap ~diff ~atom b =
    let rec aux = function
      | 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) ->
        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
    in
    aux b
388

389 390 391
  let empty = False
  let full = split0 (`Atm T.full) True False False
  let is_empty = function False -> true | _ -> false
392

393 394 395 396 397 398 399 400 401 402
  let rec split x p i n =
    if X.equal (`Atm T.empty) x then False
    (* 0?p:i:n -> 0 *)
    else if i == True then True
    (* 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) *)
    if equal p n then p ++ i
    else split0 x p i n
403

404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436
  (* simplify t l -> bdd of ( t // l ) *)
  and simplify a l =
    match a with
      | 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
        else s_aux2 a x p i n [] [] [] l
  and s_aux2 a x p i n ap ai an = function
    | [] ->
      let p = simplify p ap
      and n = simplify n an
      and i = simplify i ai in
      if equal p n then p ++ i else split0 x p i n
    | b :: l -> s_aux3 a x p i n ap ai an l b
  and s_aux3 a x p i n ap ai an l = function
    | 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
      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
    | True, _ | _, True -> True
    | False, a | a, False -> a
437

438 439
    | Split (_,`Atm x1, True,False,False), Split (_,`Atm x2, True,False,False) ->
        split (`Atm (T.cup x1 x2)) True False False
440

441 442 443 444
    | 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) ->
        assert false
445

446 447 448 449 450
    | Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
      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
451

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

455 456 457 458
  (* intersection *)
  let rec ( ** ) a b = if a == b then a else match (a,b) with
    | True, a | a, True -> a
    | False, _ | _, False -> False
459

460 461
    | Split (_,`Atm x1, True,False,False), Split (_,`Atm x2, True,False,False) ->
        split (`Atm(T.cap x1 x2)) True False False
462

463 464
    | 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
465

466 467
    | 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
468

469 470
    | 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
471

472 473 474 475 476 477 478 479 480
    | Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
	let c = X.compare x1 x2 in
	if c = 0 then
	  split x1
	    (p1 ** (p2 ++ i2) ++ (p2 ** i1))
	    (i1 ** i2)
	    (n1 ** (n2 ++ i2) ++ (n2 ** i1))
	else if c < 0 then split x1 (p1 ** b) (i1 ** b) (n1 ** b)
	else split x2 (p2 ** a) (i2 ** a) (n2 ** a)
481

482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552
  let rec trivially_disjoint a b =
    if a == b then a == False
    else match (a,b) with
      | True, a | a, True -> a == False
      | False, _ | _, False -> true
      | Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
	  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
    | 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))

  let rec ( // ) a b =
    let negatm = T.diff T.full in
    if a == b then False
    else match (a,b) with
      | False,_ | _, True -> False
      | a, False -> a
      | True, b -> neg b

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

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

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

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

      | Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
	  let c = X.compare x1 x2 in
	  if c = 0 then
	    if (i2 == False) && (n2 == False)
	    then split x1 (p1 // p2) (i1 // p2) (n1 ++ i1)
	    else
	      split x1 ((p1++i1) // (p2 ++ i2)) False ((n1++i1) // (n2 ++ i2))
	  else if c < 0 then
	    split x1 (p1 // b) (i1 // b) (n1 // b)
	  else
	    split x2 (a // (i2 ++ p2)) False (a // (i2 ++ n2))

  let cup = ( ++ )
  let cap = ( ** )
  let diff = ( // )

  let extract =
    function
    | False -> `Empty
    | True -> `Full
    | Split (_,x,p,i,n) -> `Split (x,p,i,n)
553

554
end