boolVar.ml 14 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 172
  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 )
173 174

  let rec iter f = function
175
    | `Split (_, x, p,i,n) -> f x; iter f p; iter f i; iter f n
176 177 178
    | _ -> ()

  let rec dump ppf = function
179 180 181 182 183
    | `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
184 185

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

Pietro Abate's avatar
Pietro Abate committed
204
  let pp_print = print X.dump
205

206
  let print ?(f=X.dump) = function
207
    | `True -> assert false (* [] a bdd cannot be of this type *)
208 209
    | `False -> [ fun ppf -> Format.fprintf ppf "Empty" ]
    | c -> [ fun ppf -> print f ppf c ]
210

211 212 213 214
  (* 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
215
      | `True -> (List.rev pos, List.rev neg) :: accu
216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236
      | `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)
237 238 239

  let compute ~empty ~full ~cup ~cap ~diff ~atom b =
    let rec aux = function
240 241 242
      | `True -> full
      | `False -> empty
      | `Split(_,x, p,i,n) ->
243 244 245 246 247 248 249 250 251 252
	  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 =
253
    `Split (compute_hash x pos ign neg, x, pos, ign, neg)
254

255 256 257
  let empty = `False
  let full = split0 (`Atm T.full) `True `False `False
  let any = full
258 259 260 261

  let is_empty t = (t == empty)

(* Invariants:
262
     `Split (x, pos,ign,neg) ==>  (ign <> `True), (pos <> neg)
263 264 265 266
*)

  let rec has_true = function
    | [] -> false
267
    | `True :: _ -> true
268 269
    | _ :: l -> has_true l

270 271 272 273
  let rec has_same a = function
    | [] -> false
    | b :: l -> (equal a b) || (has_same a l)

274 275
  (* split removes redundant subtrees from the positive and negative
   * branch if they are present in the lazy union branch *)
276 277 278 279 280 281 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
  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
320

321 322
    | `Split (_,`Atm x1, `True,`False,`False), `Split (_,`Atm x2, `True,`False,`False) ->
        split (`Atm (T.cup x1 x2)) `True `False `False
323

Pietro Abate's avatar
Pietro Abate committed
324 325
    | `Split (_,`Atm x1, `False,`False,`True), `Split (_,`Atm x2, `False,`False,`True)
    | `Split (_,`Atm x1, `True,`False,`False), `Split (_,`Atm x2, `False,`False,`True)
326 327 328 329 330 331 332 333
    | `Split (_,`Atm x1, `False,`False,`True), `Split (_,`Atm x2, `True,`False,`False) ->
        assert 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
334 335 336 337 338 339

(* 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
340 341
    | `True, a | a, `True -> a
    | `False, _ | _, `False -> `False
342

343 344
    | `Split (_,`Atm x1, `True,`False,`False), `Split (_,`Atm x2, `True,`False,`False) ->
        split (`Atm(T.cap x1 x2)) `True `False `False
345

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

349 350
    | `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
351

352 353
    | `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
354

355
    | `Split (_,x1, p1,i1,n1), `Split (_,x2, p2,i2,n2) ->
356 357 358 359 360 361 362 363 364 365
	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 =
366
    if a == b then a == `False
367
    else match (a,b) with
368 369 370
      | `True, a | a, `True -> a == `False
      | `False, _ | _, `False -> true
      | `Split (_,x1, p1,i1,n1), `Split (_,x2, p2,i2,n2) ->
371 372 373 374 375 376 377 378 379 380 381 382 383 384 385
	  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
386 387 388 389 390 391 392 393
    | `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))
394 395 396
	      
  let rec ( // ) a b =
    let negatm = T.diff T.full in
397
    if a == b then `False 
398
    else match (a,b) with
399 400 401
      | `False,_ | _, `True -> `False
      | a, `False -> a
      | `True, b -> neg b
402

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

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

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

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

415
      | `Split (_,x1, p1,i1,n1), `Split (_,x2, p2,i2,n2) ->
416 417
	  let c = X.compare x1 x2 in
	  if c = 0 then
418
	    if (i2 == `False) && (n2 == `False) 
419 420
	    then split x1 (p1 // p2) (i1 // p2) (n1 ++ i1)
	    else 
421
	      split x1 ((p1++i1) // (p2 ++ i2)) `False ((n1++i1) // (n2 ++ i2))
422 423 424
	  else if c < 0 then
	    split x1 (p1 // b) (i1 // b) (n1 // b) 
	  else
425
	    split x2 (a // (i2 ++ p2)) `False (a // (i2 ++ n2))
426 427 428 429 430
	      
  let cup = ( ++ )
  let cap = ( ** )
  let diff = ( // )

431
(*
432
  (* return a couple of trees (v,a)
433 434 435
   * v = only variables as leaves
   * a = only atoms as leaves
   *)
436 437 438 439 440 441 442 443 444 445 446 447 448 449 450
  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)
451
*)
Pietro Abate's avatar
Pietro Abate committed
452

453
end