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

5
(* this is the the of the Constructor container *)
6
module type E = sig
7
  type elem
8 9 10 11 12 13 14 15 16 17 18
  include Custom.T

  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

end

19
module type S = sig
Pietro Abate's avatar
Pietro Abate committed
20

21
  type s
22
  type elem = s Var.var_or_atom
23
  include Custom.T
24

25
  (* returns the union of all leaves in the BDD *)
26
  val leafconj: t -> s
27

28
  val get: t -> (elem list * elem list) list
29
(*  val build : (elem list * elem list) list -> t*)
30 31
  val empty : t
  val full  : t
32
  (* same as full, but we keep it for the moment to avoid chaging
Pietro Abate's avatar
Pietro Abate committed
33 34
   * the code everywhere *)
  val any  : t
35 36 37 38
  val cup   : t -> t -> t
  val cap   : t -> t -> t
  val diff  : t -> t -> t
  val atom  : elem -> t
39

40 41
  val trivially_disjoint: t -> t -> bool

42
  (* vars a : return a bdd that is ( Any ^ Var a ) *)
43
  val vars  : Var.var -> t
44

45
  val iter: (elem -> unit) -> t -> unit
46

47
  val compute: empty:'b -> full:'b -> cup:('b -> 'b -> 'b)
48 49 50 51 52
    -> cap:('b -> 'b -> 'b) -> diff:('b -> 'b -> 'b) ->
    atom:(elem -> 'b) -> t -> 'b

  val is_empty : t -> bool

53
  val pp_print : Format.formatter -> t -> unit
54

55
  val print : ?f:(Format.formatter -> elem -> unit) -> t -> (Format.formatter -> unit) list
56

57
(*
58
  val extractvars : t -> [> `Var of Var.t ] bdd * t
59
*)
60 61
end

62
module type MAKE = functor (T : E) -> S with type s = T.t
63

64 65 66
(* ternary BDD
 * where the nodes are Atm of X.t | Var of String.t
 * Variables are always before Values
67
 * All the leaves are then base types
68 69 70 71 72 73 74 75 76
 *
 * 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
 *
77
 * extract_var : copy the orginal tree and on one copy put to zero all
78 79 80 81
 * leaves that have an Atm on the other all leaves that have a Var
 *
 * *)

82
module Make (T : E) : S with type s = T.t = struct
83 84
  (* ternary decision trees . cf section 11.3.3 Frish PhD *)
  (* plus variables *)
85 86
  (* `Atm are containers (Atoms, Chars, Intervals, Pairs ... )
   * `Var are String
87
   *)
Pietro Abate's avatar
Pietro Abate committed
88

89
  type s = T.t
90
  type elem = s Var.var_or_atom
91
  module X : Custom.T with type t = elem = Var.Make(T)
92 93 94 95 96 97 98
  type 'a bdd =
    [ `True
    | `False
    | `Split of int * 'a * ('a bdd) * ('a bdd) * ('a bdd) ]
  type t = elem bdd

  let rec equal_aux eq a b =
99 100
    (a == b) ||
    match (a,b) with
101
      | `Split (h1,x1,p1,i1,n1), `Split (h2,x2,p2,i2,n2) ->
102
	  (h1 == h2) &&
103 104
	  (equal_aux eq p1 p2) && (equal_aux eq i1 i2) &&
	  (equal_aux eq n1 n2) && (eq x1 x2)
105 106
      | _ -> false

107 108
  let equal = equal_aux X.equal

109 110 111 112
(* Idea: add a mutable "unique" identifier and set it to
   the minimum of the two when egality ... *)

  let rec compare a b =
113
    if (a == b) then 0
114
    else match (a,b) with
115
      | `Split (h1,x1, p1,i1,n1), `Split (h2,x2, p2,i2,n2) ->
116
	  if h1 < h2 then -1 else if h1 > h2 then 1
117 118
	  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
119
	  else let c = compare i1 i2 in if c <> 0 then c
120
	  else compare n1 n2
121 122 123 124
      | `True,_  -> -1
      | _, `True -> 1
      | `False,_ -> -1
      | _,`False -> 1
125 126

  let rec hash = function
127 128
    | `True -> 1
    | `False -> 0
Pietro Abate's avatar
Pietro Abate committed
129
    | `Split(h,_,_,_,_) -> h
130

131
  let compute_hash x p i n =
132
	(X.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)
133 134

  let rec check = function
135
    | `True -> ()
136 137
    | `False -> ()
    | `Split (h,x,p,i,n) ->
138
	assert (h = compute_hash x p i n);
139 140 141
	(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) | _ -> ());
142 143 144 145
	X.check x; check p; check i; check n

  let atom x =
    let h = X.hash x + 17 in (* partial evaluation of compute_hash... *)
146
    `Split (h, x,`True,`False,`False)
Pietro Abate's avatar
Pietro Abate committed
147

148
  let vars v =
149
    let compute_hash x p i n =
150 151
        (Var.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)
    in
152 153
    let a = atom (`Atm T.full) in
    let h = compute_hash v a `False `False in
154
    ( `Split (h,`Var v,a,`False,`False) :> t )
155 156

  let rec iter f = function
157
    | `Split (_, x, p,i,n) -> f x; iter f p; iter f i; iter f n
158 159 160
    | _ -> ()

  let rec dump ppf = function
161 162
    | `True -> Format.fprintf ppf "⫧"
    | `False -> Format.fprintf ppf "⫨"
163
    | `Split (_,x, p,i,n) ->
164 165 166 167 168 169 170 171 172 173
      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
174 175

  let rec print f ppf = function
176 177 178
    | `True -> Format.fprintf ppf "Any"
    | `False -> Format.fprintf ppf "Empty"
    | `Split (_, x, p,i, n) ->
179 180
	let flag = ref false in
	let b () = if !flag then Format.fprintf ppf " | " else flag := true in
181
	(match p with
182 183
	   | `True -> b(); Format.fprintf ppf "%a" f x
	   | `False -> ()
184
	   | _ -> b (); Format.fprintf ppf "%a & @[(%a)@]" f x (print f) p );
185
	(match i with
186 187
	   | `True -> assert false;
	   | `False -> ()
188
	   | _ -> b(); print f ppf i);
189
	(match n with
190 191
	   | `True -> b (); Format.fprintf ppf "@[~%a@]" f x
	   | `False -> ()
192
	   | _ -> b (); Format.fprintf ppf "@[~%a@] & @[(%a)@]" f x (print f) n)
193

Pietro Abate's avatar
Pietro Abate committed
194
  let pp_print = print X.dump
195

196
  let print ?(f=X.dump) = function
197
    | `True -> assert false (* [] a bdd cannot be of this type *)
198 199
    | `False -> [ fun ppf -> Format.fprintf ppf "Empty" ]
    | c -> [ fun ppf -> print f ppf c ]
200

201 202 203 204
  (* 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
205
      | `True -> (List.rev pos, List.rev neg) :: accu
206 207 208 209 210 211 212 213
      | `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

214
  let leafconj x =
215 216 217 218 219 220 221 222 223 224 225 226
    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)
227 228 229

  let compute ~empty ~full ~cup ~cap ~diff ~atom b =
    let rec aux = function
230
      | `True  -> full
231
      | `False -> empty
232 233
      | `Split (_,`Atm x,`True,_,_) when T.equal x T.empty -> empty
      | `Split (_,`Atm x,`True,_,_) when T.equal x T.full -> full
234
      | `Split(_,x, p,i,n) ->
235 236 237 238 239
        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
240 241
    in
    aux b
242

243 244 245
(* Invariant: correct hash value *)

  let split0 x pos ign neg =
246
    `Split (compute_hash x pos ign neg, x, pos, ign, neg)
247

248 249 250
  let empty = `False
  let full = split0 (`Atm T.full) `True `False `False
  let any = full
251 252 253 254

  let is_empty t = (t == empty)

(* Invariants:
255
     `Split (x, pos,ign,neg) ==>  (ign <> `True), (pos <> neg)
256 257 258 259
*)

  let rec has_true = function
    | [] -> false
260
    | `True :: _ -> true
261 262
    | _ :: l -> has_true l

263 264 265 266
  let rec has_same a = function
    | [] -> false
    | b :: l -> (equal a b) || (has_same a l)

267 268
  (* split removes redundant subtrees from the positive and negative
   * branch if they are present in the lazy union branch *)
269 270 271
  let rec split x p i n =
    if X.equal (`Atm T.empty) x then `False
    (* 0?p:i:n -> 0 *)
272
    else if i == `True then `True
273 274 275 276
    (* 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) *)
277
    if equal p n then p ++ i
278 279 280 281 282 283 284 285 286 287 288 289 290
    else split0 x p i n

  (* 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
291 292
    | [] ->
      let p = simplify p ap
293 294 295
      and n = simplify n an
      and i = simplify i ai in
      if equal p n then p ++ i else split0 x p i n
296
    | b :: l -> s_aux3 a x p i n ap ai an l b
297 298 299 300
  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 ->
301
      if equal a b then `False
302 303 304 305 306 307 308 309 310 311 312
      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
313

314 315
    | `Split (_,`Atm x1, `True,`False,`False), `Split (_,`Atm x2, `True,`False,`False) ->
        split (`Atm (T.cup x1 x2)) `True `False `False
316

Pietro Abate's avatar
Pietro Abate committed
317 318
    | `Split (_,`Atm x1, `False,`False,`True), `Split (_,`Atm x2, `False,`False,`True)
    | `Split (_,`Atm x1, `True,`False,`False), `Split (_,`Atm x2, `False,`False,`True)
319 320
    | `Split (_,`Atm x1, `False,`False,`True), `Split (_,`Atm x2, `True,`False,`False) ->
        assert false
321

322 323 324 325 326
    | `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
327 328 329 330 331 332

(* 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
333 334
    | `True, a | a, `True -> a
    | `False, _ | _, `False -> `False
335

336 337
    | `Split (_,`Atm x1, `True,`False,`False), `Split (_,`Atm x2, `True,`False,`False) ->
        split (`Atm(T.cap x1 x2)) `True `False `False
338

339 340
    | `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
341

342 343
    | `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
344

345 346
    | `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
347

348
    | `Split (_,x1, p1,i1,n1), `Split (_,x2, p2,i2,n2) ->
349 350
	let c = X.compare x1 x2 in
	if c = 0 then
351
	  split x1
352 353
	    (p1 ** (p2 ++ i2) ++ (p2 ** i1))
	    (i1 ** i2)
354
	    (n1 ** (n2 ++ i2) ++ (n2 ** i1))
355 356 357 358
	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 =
359
    if a == b then a == `False
360
    else match (a,b) with
361 362 363
      | `True, a | a, `True -> a == `False
      | `False, _ | _, `False -> true
      | `Split (_,x1, p1,i1,n1), `Split (_,x2, p2,i2,n2) ->
364 365 366 367 368 369 370 371 372 373 374 375 376 377 378
	  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
379 380 381 382 383
    | `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)
384 385
    | `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)
386
    | `Split (_,x, p,i,n) -> split x (neg (i ++ p)) `False (neg (i ++ n))
387

388 389
  let rec ( // ) a b =
    let negatm = T.diff T.full in
390
    if a == b then `False
391
    else match (a,b) with
392 393 394
      | `False,_ | _, `True -> `False
      | a, `False -> a
      | `True, b -> neg b
395

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

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

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

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

408
      | `Split (_,x1, p1,i1,n1), `Split (_,x2, p2,i2,n2) ->
409 410
	  let c = X.compare x1 x2 in
	  if c = 0 then
411
	    if (i2 == `False) && (n2 == `False)
412
	    then split x1 (p1 // p2) (i1 // p2) (n1 ++ i1)
413
	    else
414
	      split x1 ((p1++i1) // (p2 ++ i2)) `False ((n1++i1) // (n2 ++ i2))
415
	  else if c < 0 then
416
	    split x1 (p1 // b) (i1 // b) (n1 // b)
417
	  else
418
	    split x2 (a // (i2 ++ p2)) `False (a // (i2 ++ n2))
419

420 421 422 423
  let cup = ( ++ )
  let cap = ( ** )
  let diff = ( // )

424
(*
425
  (* return a couple of trees (v,a)
426 427 428
   * v = only variables as leaves
   * a = only atoms as leaves
   *)
429 430 431 432 433 434 435 436 437 438 439 440 441 442 443
  let rec extractvars = function
    (* `True or `False can only be under a variable *)
    | `True -> `True,`False
    | `False -> `False,`False
    | `Split (_,`Atm _, `True,`False,`False) as x -> `False, x
    | `Split (_,`Atm _, _,_,_) -> assert false
    | `Split (_,((`Var y) as x),p,i,n) ->
        let p1,p2 = extractvars p in
        let i1,i2 = extractvars i in
        let n1,n2 = extractvars n in
        (* let v = `Split (compute_hash x p1 i1 n1,x,p1,i1,n1) in   *)
        let v = (fst(gensplit Pervasives.compare (fun x -> x) (fun x -> x) (fun _ -> false)) x p1 i1 n1) in
        let t = split x p2 i2 n2 in
        assert(v <> `True);
        (v,t)
444
*)
Pietro Abate's avatar
Pietro Abate committed
445

446 447 448 449 450 451 452
  let build l =
    let conj acc cons l =
      List.fold_left (fun acc e -> cons acc (atom e)) acc l
    in
    List.fold_left (fun acc (p, n) ->
      cup acc (diff (conj full cap p) (conj empty cup n)))
      empty l
453
end