boolVar.ml 14.5 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 8 9 10 11 12 13 14 15 16 17 18
  type elem
  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
Pietro Abate's avatar
Pietro Abate committed
22 23 24 25 26 27 28

  module T : sig
    include E
    val is_empty : s -> bool
    val is_full : s -> bool
  end

29
  type elem = s Var.pairvar
30 31 32 33 34
  type 'a bdd =
    [ `True
    | `False
    | `Split of int * 'a * ('a bdd) * ('a bdd) * ('a bdd) ]

35
  include Custom.T with type t = elem bdd
36

37
  (* returns the union of all leaves in the BDD *)
38
  val leafconj: t -> s
39

40
  val get: t -> (elem list * elem list) list
41 42 43

  val empty : t
  val full  : t
Pietro Abate's avatar
Pietro Abate committed
44 45 46
  (* same as full, but we keep it for the moment to avoid chaging 
   * the code everywhere *)
  val any  : t
47 48 49 50
  val cup   : t -> t -> t
  val cap   : t -> t -> t
  val diff  : t -> t -> t
  val atom  : elem -> t
Pietro Abate's avatar
Pietro Abate committed
51
  (* val neg_atom  : elem -> t *)
52

53 54
  val trivially_disjoint: t -> t -> bool

55
  (* vars a : return a bdd that is ( Any ^ Var a ) *)
56
  val vars  : Var.var -> t
57 58 59 60 61 62 63 64 65

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

  val compute: empty:'b -> full:'b -> cup:('b -> 'b -> 'b) 
    -> cap:('b -> 'b -> 'b) -> diff:('b -> 'b -> 'b) ->
    atom:(elem -> 'b) -> t -> 'b

  val is_empty : t -> bool

66
  val pp_print : Format.formatter -> t -> unit
67

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

70
(*
71
  val extractvars : t -> [> `Var of Var.t ] bdd * t 
72
*)
73 74
end

75 76 77 78
(*
module type MAKE = functor (T : E) -> S with type elem = T.t Custom.pairvar 
*)

79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96
(* ternary BDD
 * where the nodes are Atm of X.t | Var of String.t
 * Variables are always before Values
 * All the leaves are then base types 
 *
 * 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
 *
 * extract_var : copy the orginal tree and on one copy put to zero all 
 * leaves that have an Atm on the other all leaves that have a Var
 *
 * *)

97
module Make(T : E) : S with type s = T.t =
98 99 100
struct
  (* ternary decision trees . cf section 11.3.3 Frish PhD *)
  (* plus variables *)
101 102
  (* `Atm are containers (Atoms, Chars, Intervals, Pairs ... )
   * `Var are String
103
   *)
Pietro Abate's avatar
Pietro Abate committed
104 105 106 107 108 109
  module T = struct
    include T
    let is_empty t = (empty == t)
    let is_full t = (full == t)
  end

110
  type s = T.t
111 112
  module X = Var.Make(T)
  type elem = s Var.pairvar
113 114 115 116 117 118 119
  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 =
120 121
    (a == b) ||
    match (a,b) with
122
      | `Split (h1,x1,p1,i1,n1), `Split (h2,x2,p2,i2,n2) ->
123
	  (h1 == h2) &&
124 125
	  (equal_aux eq p1 p2) && (equal_aux eq i1 i2) &&
	  (equal_aux eq n1 n2) && (eq x1 x2)
126 127
      | _ -> false

128 129
  let equal = equal_aux X.equal

130 131 132 133 134 135
(* Idea: add a mutable "unique" identifier and set it to
   the minimum of the two when egality ... *)

  let rec compare a b =
    if (a == b) then 0 
    else match (a,b) with
136
      | `Split (h1,x1, p1,i1,n1), `Split (h2,x2, p2,i2,n2) ->
137 138 139 140 141
	  if h1 < h2 then -1 else if h1 > h2 then 1 
	  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
	  else let c = compare i1 i2 in if c <> 0 then c 
	  else compare n1 n2
142 143 144 145
      | `True,_  -> -1
      | _, `True -> 1
      | `False,_ -> -1
      | _,`False -> 1
146 147

  let rec hash = function
148 149
    | `True -> 1
    | `False -> 0
Pietro Abate's avatar
Pietro Abate committed
150
    | `Split(h,_,_,_,_) -> h
151 152

  let compute_hash x p i n = 
153
	(X.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)
154 155

  let rec check = function
156
    | `True -> ()
157 158
    | `False -> ()
    | `Split (h,x,p,i,n) ->
159
	assert (h = compute_hash x p i n);
160 161 162
	(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) | _ -> ());
163 164 165 166
	X.check x; check p; check i; check n

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

   (* 
170 171
  let neg_atom x =
    let h = X.hash x + 16637 in (* partial evaluation of compute_hash... *)
172
    `Split (h, x,`False,`False,`True)
Pietro Abate's avatar
Pietro Abate committed
173
   *)
174 175 176 177 178

  let vars v =
    let a = atom (`Atm T.full) in 
    let h = compute_hash v a `False `False in 
    ( `Split (h,v,a,`False,`False) :> t )
179 180

  let rec iter f = function
181
    | `Split (_, x, p,i,n) -> f x; iter f p; iter f i; iter f n
182 183 184
    | _ -> ()

  let rec dump ppf = function
185 186 187 188 189
    | `True -> Format.fprintf ppf "+"
    | `False -> Format.fprintf ppf "-"
    | `Split (_,x, p,i,n) -> 
	Format.fprintf ppf "%a(@[%a,%a,%a@])" 
	X.dump x (*X.hash x*) dump p dump i dump n
190 191

  let rec print f ppf = function
192 193 194
    | `True -> Format.fprintf ppf "Any"
    | `False -> Format.fprintf ppf "Empty"
    | `Split (_, x, p,i, n) ->
195 196 197
	let flag = ref false in
	let b () = if !flag then Format.fprintf ppf " | " else flag := true in
	(match p with 
198 199
	   | `True -> b(); Format.fprintf ppf "%a" f x
	   | `False -> ()
200 201
	   | _ -> b (); Format.fprintf ppf "%a & @[(%a)@]" f x (print f) p );
	(match i with 
202 203
	   | `True -> assert false;
	   | `False -> ()
204 205
	   | _ -> b(); print f ppf i);
	(match n with 
206 207
	   | `True -> b (); Format.fprintf ppf "@[~%a@]" f x
	   | `False -> ()
208
	   | _ -> b (); Format.fprintf ppf "@[~%a@] & @[(%a)@]" f x (print f) n)
209 210 211

  let pp_print = print X.dump 

212 213 214 215
  let print ?(f=X.dump) = function
    | `True -> [] (* [] a bdd cannot be of this type *)
    | `False -> [ fun ppf -> Format.fprintf ppf "Empty" ]
    | c -> [ fun ppf -> print f ppf c ]
216

217 218 219 220
  (* 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
221
      | `True -> (List.rev pos, List.rev neg) :: accu
222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243
      | `False -> accu
      | `Split (_,x, p,i,n) ->
        (*OPT: can avoid creating this list cell when pos or neg =`False *)
        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)
244 245 246

  let compute ~empty ~full ~cup ~cap ~diff ~atom b =
    let rec aux = function
247 248 249
      | `True -> full
      | `False -> empty
      | `Split(_,x, p,i,n) ->
250 251 252 253 254 255 256 257 258 259
	  let p = cap (atom x) (aux p)
	  and i = aux i
	  and n = diff (aux n) (atom x) in
	  cup (cup p i) n
    in
    aux b
      
(* Invariant: correct hash value *)

  let split0 x pos ign neg =
260
    `Split (compute_hash x pos ign neg, x, pos, ign, neg)
261

262 263 264
  let empty = `False
  let full = split0 (`Atm T.full) `True `False `False
  let any = full
265 266 267 268

  let is_empty t = (t == empty)

(* Invariants:
269
     `Split (x, pos,ign,neg) ==>  (ign <> `True), (pos <> neg)
270 271 272 273
*)

  let rec has_true = function
    | [] -> false
274
    | `True :: _ -> true
275 276
    | _ :: l -> has_true l

277 278 279 280
  let rec has_same a = function
    | [] -> false
    | b :: l -> (equal a b) || (has_same a l)

281 282
  (* split removes redundant subtrees from the positive and negative
   * branch if they are present in the lazy union branch *)
283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326
  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

  (* 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
327

328 329
    | `Split (_,`Atm x1, `True,`False,`False), `Split (_,`Atm x2, `True,`False,`False) ->
        split (`Atm (T.cup x1 x2)) `True `False `False
330

331 332 333 334 335
    | `Split (_,`Atm x1, `False,`False,`True), `Split (_,`Atm x2, `False,`False,`True) ->
        assert false
        (*
        split (`Atm (T.cup (T.diff T.full x1) (T.diff T.full x2))) `True `False `False
        *)
336

337 338 339 340 341
    | `Split (_,`Atm x1, `True,`False,`False), `Split (_,`Atm x2, `False,`False,`True) ->
        assert false
        (*
        split (`Atm (T.cup x1 (T.diff T.full x2))) `True `False `False
        *)
342

343 344 345 346 347 348 349 350 351 352 353
    | `Split (_,`Atm x1, `False,`False,`True), `Split (_,`Atm x2, `True,`False,`False) ->
        assert false
        (*
        split (`Atm (T.cup (T.diff T.full 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 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
354 355 356 357 358 359

(* 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
360 361
    | `True, a | a, `True -> a
    | `False, _ | _, `False -> `False
362

363 364
    | `Split (_,`Atm x1, `True,`False,`False), `Split (_,`Atm x2, `True,`False,`False) ->
        split (`Atm(T.cap x1 x2)) `True `False `False
365

366 367
    | `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
368

369 370
    | `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
371

372 373
    | `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
374

375
    | `Split (_,x1, p1,i1,n1), `Split (_,x2, p2,i2,n2) ->
376 377 378 379 380 381 382 383 384 385
	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)

  let rec trivially_disjoint a b =
386
    if a == b then a == `False
387
    else match (a,b) with
388 389 390
      | `True, a | a, `True -> a == `False
      | `False, _ | _, `False -> true
      | `Split (_,x1, p1,i1,n1), `Split (_,x2, p2,i2,n2) ->
391 392 393 394 395 396 397 398 399 400 401 402 403 404 405
	  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
406 407 408 409 410 411 412 413
    | `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))
414 415 416
	      
  let rec ( // ) a b =
    let negatm = T.diff T.full in
417
    if a == b then `False 
418
    else match (a,b) with
419 420 421
      | `False,_ | _, `True -> `False
      | a, `False -> a
      | `True, b -> neg b
422

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

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

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

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

435
      | `Split (_,x1, p1,i1,n1), `Split (_,x2, p2,i2,n2) ->
436 437
	  let c = X.compare x1 x2 in
	  if c = 0 then
438
	    if (i2 == `False) && (n2 == `False) 
439 440
	    then split x1 (p1 // p2) (i1 // p2) (n1 ++ i1)
	    else 
441
	      split x1 ((p1++i1) // (p2 ++ i2)) `False ((n1++i1) // (n2 ++ i2))
442 443 444
	  else if c < 0 then
	    split x1 (p1 // b) (i1 // b) (n1 // b) 
	  else
445
	    split x2 (a // (i2 ++ p2)) `False (a // (i2 ++ n2))
446 447 448 449 450
	      
  let cup = ( ++ )
  let cap = ( ** )
  let diff = ( // )

451
(*
452
  (* return a couple of trees (v,a)
453 454 455
   * v = only variables as leaves
   * a = only atoms as leaves
   *)
456 457 458 459 460 461 462 463 464 465 466 467 468 469 470
  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)
471
*)
Pietro Abate's avatar
Pietro Abate committed
472

473
end