Commit 066ee893 authored by Pietro Abate's avatar Pietro Abate

Remove stale code and fix very nasty bug

- the bug was introduced in compute_hash a while ago
parent a5d67b36
......@@ -5,24 +5,32 @@ module type S = sig
include BoolVar.S
val mk_var : string -> t
val mk_atm : string -> t
val to_string : t -> string
end
let to_string pp t =
Format.fprintf Format.str_formatter "%a@." pp t;
Printf.sprintf "->%s<-" (Format.flush_str_formatter ())
module BoolChars : S with type s = Chars.t = struct
include BoolVar.Make(Chars)
let mk_var s = atom (`Var s)
let mk_atm c = atom (`Atm (Chars.atom (Chars.V.mk_char c.[0] )))
let to_string = to_string pp_print
end
module BoolAtoms : S with type s = Atoms.t = struct
include BoolVar.Make(Atoms)
let mk_var s = atom (`Var s)
let mk_atm s = atom (`Atm (Atoms.atom (Atoms.V.mk_ascii s)))
let to_string = to_string pp_print
end
module BoolIntervals : S with type s = Intervals.t = struct
include BoolVar.Make(Intervals)
let mk_var s = atom (`Var s)
let mk_atm s = atom (`Atm (Intervals.atom (Intervals.V.mk s)))
let to_string = to_string pp_print
end
module ExprParser (B : S) = struct
......@@ -37,9 +45,9 @@ module ExprParser (B : S) = struct
[ x = SELF; "^"; y = SELF -> B.cap x y ]
| "cup" LEFTA
[ x = SELF; "v"; y = SELF -> B.cup x y
| x = SELF; "\\/\\/"; y = SELF -> B.diff x y ]
| x = SELF; "-"; y = SELF -> B.diff x y ]
| "neg" RIGHTA
[ "-"; x = SELF-> B.diff B.full x ]
[ "~"; x = SELF-> B.diff B.full x ]
| "simple" NONA
["Any" -> B.full
|"Empty" -> B.empty
......@@ -58,58 +66,30 @@ end
module BCP = ExprParser(BoolChars)
module BAP = ExprParser(BoolAtoms)
module BIP = ExprParser(BoolIntervals)
(*
XXX this needs much more infrastructure as in types.ml
module BoolPair = BoolVar.Make(Pair)
module BoolRec = BoolVar.Make(Rec)
*)
let atoms_tests = [
"commutativity intersection", BAP.os "atm foo ^ atm bar", BAP.os "atm bar ^ atm foo";
"commutativity union", BAP.os "atm foo v atm bar", BAP.os "atm bar v atm foo";
"distributive intersection", BAP.os "(atm foo v atm bar) ^ atm baz", BAP.os "(atm foo ^ atm baz) v (atm bar ^ atm baz)";
"distributive intersection var", BAP.os "(var alpha v atm bar) ^ atm baz", BAP.os "(var alpha ^ atm baz) v (atm bar ^ atm baz)";
"associativity intersection", BAP.os "(atm foo ^ atm bar) ^ atm baz", BAP.os "atm foo ^ (atm bar ^ atm baz)";
"associativity intersection var", BAP.os "(atm foo ^ atm bar) ^ var alpha", BAP.os "atm foo ^ (atm bar ^ var alpha)";
"associativity union", BAP.os "(atm foo v atm bar) v atm baz", BAP.os "atm foo v (atm bar v atm baz)";
"difference", BAP.os "(atm foo ^ atm bar) v var alpha", BAP.os "var alpha";
"difference empty", BAP.os "atm foo ^ atm bar", BAP.os "Empty";
"associativity union var", BAP.os "(atm foo v var alpha) v atm baz", BAP.os "atm foo v (var alpha v atm baz)";
"intersection", BAP.os "(atm foo ^ atm bar) v var alpha", BAP.os "var alpha";
"intersection 2", BAP.os "(atm foo v var alpha ) ^ var alpha", BAP.os "var alpha";
"intersection empty", BAP.os "atm foo ^ atm bar", BAP.os "Empty";
"difference", BAP.os "(atm foo v var alpha) - (var alpha)", BAP.os "atm foo ^ ~ var alpha";
"difference", BAP.os "(atm foo v var alpha) - (atm foo)", BAP.os "var alpha ^ ~ atm foo";
"difference any 1", BAP.os "~ var alpha", BAP.os "Any - var alpha";
"difference any 2", BAP.os "~ var alpha", BAP.os "Any ^ ~ var alpha";
];;
let atoms_splitvar_atm =
"atoms splitvar" >:::
List.map (fun (descr, s1,s2) ->
(Printf.sprintf "test %s" descr) >:: (fun _ ->
assert_equal (BoolAtoms.equal s1 s2) true
)
) [
"atm empty", snd(BoolAtoms.extractvars (BAP.os "var alpha")), BAP.os "Empty";
"atm 1", snd(BoolAtoms.extractvars (BAP.os "var alpha v (atm foo ^ var beta) v var gamma")), BAP.os "atm foo ^ var beta";
"atm 2", snd(BoolAtoms.extractvars (BAP.os "var alpha v atm foo")), BAP.os "atm foo";
]
;;
let splitvar_mixed_union_atm =
"splitvar union" >:::
List.map (fun (descr, s1,s2,r) ->
(Printf.sprintf "test %s" descr) >:: (fun _ ->
assert_equal (BoolAtoms.equal (BoolAtoms.cup s1 s2) r) true
)
) [
"atoms/chars", snd(BoolAtoms.extractvars (BAP.os "atm foo")), fst(BoolChars.extractvars (BCP.os "var alpha v atm x")), BAP.os "var alpha v atm foo";
]
;;
let atoms_structure =
"atoms structure" >:::
List.map (fun (descr, s1,s2) ->
List.map (fun (descr, result,expected) ->
(Printf.sprintf "test %s" descr) >:: (fun _ ->
(*
List.iter (fun f -> f Format.std_formatter ) (BoolAtoms.print "Empty!" s1);
Format.printf "\n";
List.iter (fun f -> f Format.std_formatter ) (BoolAtoms.print "Empty!" s2);
Format.printf "\n";
*)
assert_equal (BoolAtoms.equal s1 s2) true
assert_equal ~cmp:BoolAtoms.equal ~printer:(BoolAtoms.to_string) expected result
)
) atoms_tests
;;
......@@ -134,8 +114,6 @@ let all =
"all tests" >::: [
atoms_structure;
atoms_contains;
atoms_splitvar_atm;
splitvar_mixed_union_atm;
]
let main () =
......
......@@ -42,6 +42,8 @@ module type S = sig
val atom : elem -> t
val neg_atom : elem -> t
val trivially_disjoint: t -> t -> bool
(* vars a : return a bdd that is ( Any ^ Var a ) *)
val vars : Var.var -> t
......@@ -53,12 +55,13 @@ module type S = sig
val is_empty : t -> bool
val print: ?f:(Format.formatter -> elem -> unit) -> t -> (Format.formatter -> unit) list
val pp_print : Format.formatter -> t -> unit
val trivially_disjoint: t -> t -> bool
val print : ?f:(Format.formatter -> elem -> unit) -> t -> (Format.formatter -> unit) list
(*
val extractvars : t -> [> `Var of Var.t ] bdd * t
*)
end
(*
......@@ -133,10 +136,10 @@ struct
| `Split(h, _,_,_,_) -> h
let compute_hash x p i n =
(Hashtbl.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)
(X.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)
let rec check = function
| `True -> assert false;
| `True -> ()
| `False -> ()
| `Split (h,x,p,i,n) ->
assert (h = compute_hash x p i n);
......@@ -187,7 +190,9 @@ struct
| `True -> b (); Format.fprintf ppf "@[~%a@]" f x
| `False -> ()
| _ -> b (); Format.fprintf ppf "@[~%a@] & @[(%a)@]" f x (print f) n)
let pp_print = print X.dump
let print ?(f=X.dump) = function
| `True -> [] (* [] a bdd cannot be of this type *)
| `False -> [ fun ppf -> Format.fprintf ppf "Empty" ]
......@@ -221,24 +226,6 @@ struct
in
List.fold_left T.cup T.empty (aux [] x)
(*
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 ->
let accu = get' accu pos (l :: neg) n in
get' accu pos neg i
in
aux [x] i
let get' x = get' [] [] [] x
*)
let compute ~empty ~full ~cup ~cap ~diff ~atom b =
let rec aux = function
| `True -> full
......@@ -271,91 +258,83 @@ struct
| `True :: _ -> true
| _ :: l -> has_true l
let rec has_same a = function
| [] -> false
| b :: l -> (equal a b) || (has_same a l)
(* split removes redundant subtrees from the positive and negative
* branch if they are present in the lazy union branch *)
let gensplit compare normalize normunion is_empty =
let equal = equal_aux (fun a b -> compare a b = 0) in
let rec has_same a = function
| [] -> false
| b :: l -> (equal a b) || (has_same a l)
in
let rec split x p i n =
if is_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 normalize 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
| [] ->
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 = 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 normunion (a,b) with
| `True, _ | _, `True -> `True
| `False, a | a, `False -> a
| `Split (_,x1, p1,i1,n1), `Split (_,x2, p2,i2,n2) ->
let c = 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
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
in split,(++)
(*
let splitvar,_ = gensplit Pervasives.compare (fun x -> x) (fun x -> x) (fun _ -> false)
*)
let split,(++) =
let norm = function
| `Split (_,`Atm x, `False,`False,`True) -> split0 (`Atm(T.diff T.full x)) `True `False `False
| x -> x
in
let normunion = function
| `Split (_,`Atm x1, `True,`False,`False), `Split (_,`Atm x2, `True,`False,`False) ->
split0 (`Atm (T.cup x1 x2)) `True `False `False,`False
| `Split (_,`Atm x1, `False,`False,`True), `Split (_,`Atm x2, `False,`False,`True) ->
split0 (`Atm (T.cup (T.diff T.full x1) (T.diff T.full x2))) `True `False `False,`False
| `Split (_,`Atm x1, `True,`False,`False), `Split (_,`Atm x2, `True,`False,`False) ->
split (`Atm (T.cup x1 x2)) `True `False `False
| `Split (_,`Atm x1, `True,`False,`False), `Split (_,`Atm x2, `False,`False,`True) ->
split0 (`Atm (T.cup x1 (T.diff T.full x2))) `True `False `False,`False
| `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
*)
| `Split (_,`Atm x1, `False,`False,`True), `Split (_,`Atm x2, `True,`False,`False) ->
split0 (`Atm (T.cup (T.diff T.full x1) x2)) `True `False `False,`False
| `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
*)
|a,b -> a,b
in
gensplit X.compare norm normunion (fun x -> X.equal (`Atm T.empty) x)
| `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
(* seems better not to make ++ and this split mutually recursive;
is the invariant still inforced ? *)
......@@ -453,6 +432,7 @@ struct
let cap = ( ** )
let diff = ( // )
(*
(* return a couple of trees (v,a)
* v = only variables as leaves
* a = only atoms as leaves
......@@ -472,5 +452,6 @@ struct
let t = split x p2 i2 n2 in
assert(v <> `True);
(v,t)
*)
end
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment