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
  let print ?(f=X.dump) = function
213
    | `True -> assert false (* [] a bdd cannot be of this type *)
214 215
    | `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
      | `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)
243 244 245

  let compute ~empty ~full ~cup ~cap ~diff ~atom b =
    let rec aux = function
246 247 248
      | `True -> full
      | `False -> empty
      | `Split(_,x, p,i,n) ->
249 250 251 252 253 254 255 256 257 258
	  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 =
259
    `Split (compute_hash x pos ign neg, x, pos, ign, neg)
260

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

  let is_empty t = (t == empty)

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

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

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

280 281
  (* split removes redundant subtrees from the positive and negative
   * branch if they are present in the lazy union branch *)
282 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
  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
326

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

330 331 332 333 334
    | `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
        *)
335

336 337 338 339 340
    | `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
        *)
341

342 343 344 345 346 347 348 349 350 351 352
    | `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
353 354 355 356 357 358

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

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

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

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

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

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

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

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

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

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

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

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

472
end