Commit 79ce2417 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Re-factor the BoolVar module. Move it to bool.ml and factor as much code as possible with Bool

parent 5cace08c
......@@ -161,9 +161,9 @@ OBJECTS = \
driver/cduce_config.cmo misc/stats.cmo misc/custom.cmo misc/encodings.cmo \
misc/upool.cmo misc/pretty.cmo misc/ns.cmo misc/imap.cmo misc/html.cmo misc/utils.cmo \
\
types/compunit.cmo types/sortedList.cmo misc/bool.cmo types/ident.cmo \
types/compunit.cmo types/sortedList.cmo types/ident.cmo types/var.cmo misc/bool.cmo \
types/intervals.cmo types/chars.cmo types/atoms.cmo types/normal.cmo \
types/var.cmo types/boolVar.cmo types/types.cmo compile/auto_pat.cmo \
types/types.cmo compile/auto_pat.cmo \
types/sequence.cmo types/builtin_defs.cmo \
\
runtime/value.cmo \
......@@ -347,9 +347,6 @@ misc/q_symbol.cmo: misc/q_symbol.ml
$(HIDE) $(CAMLC) -c -pp camlp4orf $<
types/boolVar.cmo: SYNTAX_PARSER=
types/boolVar.cmi: SYNTAX_PARSER=
types/boolVar.cmx: SYNTAX_PARSER=
parser/parser.$(EXTENSION): PACKAGES += camlp4.extend
.ml.cmo:
......
......@@ -22,12 +22,16 @@ types/compunit.cmo : types/compunit.cmi
types/compunit.cmx : types/compunit.cmi
types/sortedList.cmo : misc/custom.cmo types/sortedList.cmi
types/sortedList.cmx : misc/custom.cmx types/sortedList.cmi
misc/bool.cmo : misc/custom.cmo misc/bool.cmi
misc/bool.cmx : misc/custom.cmx misc/bool.cmi
types/ident.cmo : misc/utils.cmo types/sortedList.cmi misc/ns.cmi \
misc/encodings.cmi
types/ident.cmx : misc/utils.cmx types/sortedList.cmx misc/ns.cmx \
misc/encodings.cmx
types/var.cmo : misc/utils.cmo types/sortedList.cmi types/ident.cmo \
misc/custom.cmo types/var.cmi
types/var.cmx : misc/utils.cmx types/sortedList.cmx types/ident.cmx \
misc/custom.cmx types/var.cmi
misc/bool.cmo : types/var.cmi misc/custom.cmo misc/bool.cmi
misc/bool.cmx : types/var.cmx misc/custom.cmx misc/bool.cmi
types/intervals.cmo : types/intervals.cmi
types/intervals.cmx : types/intervals.cmi
types/chars.cmo : misc/custom.cmo types/chars.cmi
......@@ -38,24 +42,16 @@ types/atoms.cmx : misc/upool.cmx types/sortedList.cmx misc/ns.cmx \
misc/imap.cmx misc/encodings.cmx types/atoms.cmi
types/normal.cmo : types/normal.cmi
types/normal.cmx : types/normal.cmi
types/var.cmo : misc/utils.cmo types/sortedList.cmi types/ident.cmo \
misc/custom.cmo types/var.cmi
types/var.cmx : misc/utils.cmx types/sortedList.cmx types/ident.cmx \
misc/custom.cmx types/var.cmi
types/boolVar.cmo : types/var.cmi misc/custom.cmo misc/bool.cmi \
types/boolVar.cmi
types/boolVar.cmx : types/var.cmx misc/custom.cmx misc/bool.cmx \
types/boolVar.cmi
types/types.cmo : types/var.cmi misc/utils.cmo misc/stats.cmi \
types/sortedList.cmi misc/pretty.cmi misc/ns.cmi types/normal.cmi \
types/intervals.cmi types/ident.cmo misc/encodings.cmi misc/custom.cmo \
types/compunit.cmi types/chars.cmi types/boolVar.cmi misc/bool.cmi \
types/atoms.cmi types/types.cmi
types/compunit.cmi types/chars.cmi misc/bool.cmi types/atoms.cmi \
types/types.cmi
types/types.cmx : types/var.cmx misc/utils.cmx misc/stats.cmx \
types/sortedList.cmx misc/pretty.cmx misc/ns.cmx types/normal.cmx \
types/intervals.cmx types/ident.cmx misc/encodings.cmx misc/custom.cmx \
types/compunit.cmx types/chars.cmx types/boolVar.cmx misc/bool.cmx \
types/atoms.cmx types/types.cmi
types/compunit.cmx types/chars.cmx misc/bool.cmx types/atoms.cmx \
types/types.cmi
compile/auto_pat.cmo : types/types.cmi types/ident.cmo types/chars.cmi \
types/atoms.cmi compile/auto_pat.cmi
compile/auto_pat.cmx : types/types.cmx types/ident.cmx types/chars.cmx \
......@@ -368,16 +364,15 @@ misc/imap.cmi :
misc/html.cmi :
types/compunit.cmi :
types/sortedList.cmi : misc/custom.cmo
misc/bool.cmi : misc/custom.cmo
types/var.cmi : types/sortedList.cmi misc/custom.cmo
misc/bool.cmi : types/var.cmi misc/custom.cmo
types/intervals.cmi : misc/custom.cmo misc/bool.cmi
types/chars.cmi : misc/custom.cmo misc/bool.cmi
types/atoms.cmi : misc/ns.cmi misc/encodings.cmi misc/custom.cmo \
misc/bool.cmi
types/normal.cmi :
types/var.cmi : types/sortedList.cmi misc/custom.cmo
types/boolVar.cmi : types/var.cmi misc/custom.cmo misc/bool.cmi
types/types.cmi : types/var.cmi misc/ns.cmi types/intervals.cmi \
types/ident.cmo misc/custom.cmo types/chars.cmi types/boolVar.cmi \
types/ident.cmo misc/custom.cmo types/chars.cmi misc/bool.cmi \
types/atoms.cmi
compile/auto_pat.cmi : types/types.cmi types/ident.cmo types/chars.cmi \
types/atoms.cmi
......
......@@ -18,20 +18,17 @@ sig
val iter: (elem-> unit) -> t -> unit
val compute: empty:'b -> full:'b -> cup:('b -> 'b -> 'b)
-> cap:('b -> 'b -> 'b) -> diff:('b -> 'b -> 'b) ->
val compute:
empty:'b -> full:'b ->
cup:('b -> 'b -> 'b) ->
cap:('b -> 'b -> 'b) ->
diff:('b -> 'b -> 'b) ->
atom:(elem -> 'b) -> t -> 'b
(*
val print: string -> (Format.formatter -> elem -> unit) -> t ->
(Format.formatter -> unit) list
*)
val trivially_disjoint: t -> t -> bool
end
module type MAKE = functor (X : Custom.T) -> S with type elem = X.t
module Make(X : Custom.T) =
struct
......@@ -314,548 +311,244 @@ struct
let cap = ( ** )
let diff = ( // )
(*
let rec cap_atom x pos a = (* Assume that x does not appear in a *)
match a with
| False -> False
| True -> if pos then atom x else neg_atom x
| Split (_,y,p,i,n) ->
let c = X.compare x y in
assert (c <> 0);
if (c < 0) then
if pos then split x a False False
else split x False False a
else split y (cap_atom x pos p) (cap_atom x pos i) (cap_atom x pos n)
*)
end
module type V =
sig
(*
let not_triv = function
| True | False -> false
| _ -> true
let diff x y =
let d = diff x y in
if (not_triv x) && (not_triv y) then
Format.fprintf Format.std_formatter "X = %a@\nY = %a@\nX\\Z = %a@\n"
dump x dump y dump d;
d
let cap x y =
let d = cap x y in
if (not_triv x) && (not_triv y) then
Format.fprintf Format.std_formatter "X = %a@\nY = %a@\nX**Z = %a@\n"
dump x dump y dump d;
d
let cup x y =
let d = cup x y in
if (not_triv x) && (not_triv y) then
Format.fprintf Format.std_formatter "X = %a@\nY = %a@\nX++Z = %a@\n"
dump x dump y dump d;
d
*)
end
module Atom : S
include S with type elem = Atom.t Var.var_or_atom
val var : Var.t -> t
(** returns the union of all leaves in the BDD *)
val leafconj: t -> Atom.t
val is_empty : t -> bool
val extract : t -> [ `Empty | `Full | `Split of (elem * t * t * t) ]
(*
module type S' = sig
include S
type bdd = False | True | Br of elem * t * t
val br: t -> bdd
end
module MakeBdd(X : Custom.T) =
module MakeVar (T : S) =
struct
type elem = X.t
type t =
| Zero
| One
| Branch of elem * t * t * int * t
type node = t
let neg = function
| Zero -> One | One -> Zero
| Branch (_,_,_,_,neg) -> neg
let id = function
| Zero -> 0
| One -> 1
| Branch (_,_,_,id,_) -> id
(* Internalization + detection of useless branching *)
let max_id = ref 2 (* Must be >= 2 *)
module W = Weak(*Myweak*).Make(
struct
type t = node
let hash = function
| Zero | One -> assert false
| Branch (v,yes,no,_,_) ->
1 + 17*X.hash v + 257*(id yes) + 65537*(id no)
let equal x y = (x == y) || match x,y with
| Branch (v1,yes1,no1,id1,_), Branch (v2,yes2,no2,id2,_) ->
(id1 == 0 || id2 == 0) && X.equal v1 v2 &&
(yes1 == yes2) && (no1 == no2)
| _ -> assert false
end)
let table = W.create 16383
type branch =
{ v : X.t; yes : node; no : node; mutable id : int; neg : branch }
let mk v yes no =
if yes == no then yes
else
let rec pos = Branch (v,yes,no,0,Branch (v,neg yes,neg no,0,pos)) in
let x = W.merge table pos in
let pos : branch = Obj.magic x in
if (pos.id == 0)
then (let n = !max_id in
max_id := succ n;
pos.id <- n;
pos.neg.id <- (-n));
x
let atom v = mk v One Zero
let dummy = Obj.magic (ref 0)
let memo_size = 16383
let memo_keys = Array.make memo_size (Obj.magic dummy)
let memo_vals = Array.make memo_size (Obj.magic dummy)
let memo_occ = Array.make memo_size 0
let eg2 (x1,y1) (x2,y2) = x1 == x2 && y1 == y2
let rec cup x1 x2 = if (x1 == x2) then x1 else match x1,x2 with
| One, x | x, One -> One
| Zero, x | x, Zero -> x
| Branch (v1,yes1,no1,id1,neg1), Branch (v2,yes2,no2,id2,neg2) ->
if (x1 == neg2) then One
else
let k,h =
if id1<id2 then (x1,x2),id1+65537*id2 else (x2,x1),id2+65537*id1 in
let h = (h land max_int) mod memo_size in
let i = memo_occ.(h) in
let k' = memo_keys.(h) in
if (k' != dummy) && (eg2 k k')
then (memo_occ.(h) <- succ i; memo_vals.(h))
else
let r =
let c = X.compare v1 v2 in
if (c = 0) then mk v1 (cup yes1 yes2) (cup no1 no2)
else if (c < 0) then mk v1 (cup yes1 x2) (cup no1 x2)
else mk v2 (cup yes2 x1) (cup no2 x1) in
if (i = 0) then (memo_keys.(h) <- k; memo_vals.(h) <- r;
memo_occ.(h) <- 1)
else memo_occ.(h) <- pred i;
r
module Atom = T
module X = Var.Make(Atom)
include Make(X)
let rec dump ppf = function
| One -> Format.fprintf ppf "+"
| Zero -> Format.fprintf ppf "-"
| Branch (x,p,n,id,_) ->
Format.fprintf ppf "%i:%a(@[%a,%a@])"
id
X.dump x dump p dump n
(*
let cup x y =
let d = cup x y in
Format.fprintf Format.std_formatter "X = %a@\nY = %a@\nX+Z = %a@\n"
dump x dump y dump d;
d
*)
let var v =
let compute_hash x p i n =
(Var.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)
in
let a = atom (`Atm T.full) in
let h = compute_hash v a False False in
(Split (h,`Var v, a, False, False) :> t )
let get x =
let rec aux accu pos neg = function
| True -> (List.rev pos, List.rev neg) :: accu
| 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)
let compute ~empty ~full ~cup ~cap ~diff ~atom b =
let rec aux = function
| True -> full
| False -> empty
| Split (_,`Atm x,True,_,_) when T.equal x T.empty -> empty
| Split (_,`Atm x,True,_,_) when T.equal x T.full -> full
| Split(_,x, p,i,n) ->
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
in
aux b
let cap x1 x2 = neg (cup (neg x1) (neg x2))
let diff x1 x2 = neg (cup (neg x1) x2)
let empty = False
let full = split0 (`Atm T.full) True False False
let is_empty = function False -> true | _ -> false
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
let rec iter f = function
| Branch (x,p,n,_,_) -> f x; iter f p; iter f 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
| Split (_,`Atm x1, True,False,False), Split (_,`Atm x2, True,False,False) ->
split (`Atm (T.cup x1 x2)) True False False
| Split (_,`Atm x1, False,False,True), Split (_,`Atm x2, False,False,True)
| Split (_,`Atm x1, True,False,False), Split (_,`Atm x2, False,False,True)
| Split (_,`Atm x1, False,False,True), Split (_,`Atm x2, True,False,False) ->
assert false
let rec print f ppf = function
| One -> Format.fprintf ppf "Any"
| Zero -> Format.fprintf ppf "Empty"
| Branch (x,p,n,_,_) ->
let flag = ref false in
let b () = if !flag then Format.fprintf ppf " | " else flag := true in
(match p with
| One -> b(); Format.fprintf ppf "%a" f x
| Zero -> ()
| _ -> b (); Format.fprintf ppf "%a & @[(%a)@]" f x (print f) p );
(match n with
| One -> b (); Format.fprintf ppf "@[~%a@]" f x
| Zero -> ()
| _ -> b (); Format.fprintf ppf "@[~%a@] & @[(%a)@]" f x (print f) n)
| 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
let print a f = function
| One -> [ fun ppf -> Format.fprintf ppf "%s" a ]
| Zero -> []
| c -> [ fun ppf -> print f ppf c ]
(* seems better not to make ++ and this split mutually recursive;
is the invariant still inforced ? *)
let rec get accu pos neg = function
| One -> (pos,neg) :: accu
| Zero -> accu
| Branch (x,p,n,_,_) ->
(*OPT: can avoid creating this list cell when pos or neg =False *)
let accu = get accu (x::pos) neg p in
let accu = get accu pos (x::neg) n in
accu
(* intersection *)
let rec ( ** ) a b = if a == b then a else match (a,b) with
| True, a | a, True -> a
| False, _ | _, False -> False
let get x = get [] [] [] x
| Split (_,`Atm x1, True,False,False), Split (_,`Atm x2, True,False,False) ->
split (`Atm(T.cap x1 x2)) True False False
let compute ~empty ~full ~cup ~cap ~diff ~atom b =
let rec aux = function
| One -> full
| Zero -> empty
| Branch(x,p,n,_,_) ->
let p = cap (atom x) (aux p)
and n = diff (aux n) (atom x) in
cup p n
in
aux b
| 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
let empty = Zero
let full = One
let rec serialize t = function
| (Zero | One) as b ->
Serialize.Put.bool t true; Serialize.Put.bool t (b == One)
| Branch (x,p,n,_,_) ->
Serialize.Put.bool t false;
X.serialize t x;
serialize t p;
serialize t n
let rec deserialize t =
if Serialize.Get.bool t then
if Serialize.Get.bool t then One else Zero
else
let x = X.deserialize t in
let p = deserialize t in
let n = deserialize t in
let x = atom x in
cup (cap x p) (cap (neg x) n)
(* mk x p n is not ok, because order of keys might have changed!
OPT TODO: detect when this is ok *)
let trivially_disjoint x y = neg x == y
let compare x y = compare (id x) (id y)
let equal x y = x == y
let hash x = id x
let check x = ()
type bdd = False | True | Br of elem * t * t
let br = function
| Zero -> False | One -> True | Branch (x,p,n,_,_) -> Br (x,p,n)
end
| 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
| 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
module Make2(X : Custom.T) = struct
module XSet = Hashset.MakeSet(X)
type 'a s = {
pos : XSet.t;
neg : XSet.t;
sub : 'a;
(* vars : XSet.t; *)
hash : int;
}
let tset_equal = ref ()
let tset_compare = ref ()
module rec TSet : Hashset.SET with type elt = TSet.t s =
Hashset.MakeSet(
struct
type t = TSet.t s
let compare t1 t2 =
if (t1 == t2) then 0
else let x = t1.hash and y = t2.hash in
if x < y then (-1) else if x > y then 1
else let c = XSet.compare t1.pos t2.pos in if c <> 0 then c
else let c = XSet.compare t1.neg t2.neg in if c <> 0 then c
else (Obj.magic !tset_compare) t1.sub t2.sub
let equal t1 t2 =
(t1 == t2) ||
(t1.hash == t2.hash &&
XSet.equal t1.pos t2.pos &&
XSet.equal t1.neg t2.neg &&
(Obj.magic !tset_equal) t1.sub t2.sub)
let hash t = t.hash
end)
let () =
tset_compare := Obj.magic TSet.compare;
tset_equal := Obj.magic TSet.equal
| 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 ++ 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)
type elem = X.t
type t = TSet.t s
let compare t1 t2 =
if (t1 == t2) then 0
else let x = t1.hash and y = t2.hash in
if x < y then (-1) else if x > y then 1
else let c = XSet.compare t1.pos t2.pos in if c <> 0 then c
else let c = XSet.compare t1.neg t2.neg in if c <> 0 then c
else TSet.compare t1.sub t2.sub
let equal t1 t2 =
(t1 == t2) ||
(t1.hash == t2.hash &&
XSet.equal t1.pos t2.pos &&
XSet.equal t1.neg t2.neg &&
TSet.equal t1.sub t2.sub)
let hash t = t.hash
let rec print f ppf t =
Format.fprintf ppf "(";
let first = ref true in
let sep () = if !first then first := false else Format.fprintf ppf "&" in
XSet.iter (fun x -> sep (); f ppf x) t.pos;
XSet.iter (fun x -> sep (); Format.fprintf ppf "~"; f ppf x) t.neg;
TSet.iter (fun t -> sep (); Format.fprintf ppf "~"; print f ppf t) t.sub;
Format.fprintf ppf ")"
let make pos neg sub =
(* let vars =
TSet.fold (fun t accu -> XSet.union t.vars accu) sub (XSet.union pos neg)
in *)
{ pos = pos;
neg = neg;
sub = sub;
(* vars = vars; *)
hash = XSet.hash pos + 17 * XSet.hash neg + 257 * TSet.hash sub }
let any = make XSet.empty XSet.empty TSet.empty
let empty = make XSet.empty XSet.empty (TSet.singleton any)
let atom x = make (XSet.singleton x) XSet.empty TSet.empty
let compl t =
if t == any then empty else if t == empty then any
else
match XSet.is_empty t.pos, XSet.is_empty t.neg, TSet.is_empty t.sub with
| true,true,false ->
(match TSet.is_singleton t.sub with
| Some t -> t
| None -> make XSet.empty XSet.empty (TSet.singleton t))
| false,true,true ->
(match XSet.is_singleton t.pos with
| Some _ -> make XSet.empty t.pos TSet.empty
| None -> make XSet.empty XSet.empty (TSet.singleton t))
| true,false,true ->
(match XSet.is_singleton t.neg with
| Some _ -> make t.neg XSet.empty TSet.empty
| None -> make XSet.empty XSet.empty (TSet.singleton t))
| _ -> make XSet.empty XSet.empty (TSet.singleton t)
let triv_subset t1 t2 =
XSet.subset t2.pos t1.pos &&
XSet.subset t2.neg t1.neg &&
TSet.subset t2.sub t1.sub
let can_factor t1 t2 =
not (XSet.disjoint t1.pos t2.pos &&
XSet.disjoint t1.neg t2.neg &&
TSet.disjoint t1.sub t2.sub)
let cap t1 t2 =
if (t1 == any) || (equal t1 t2) || (triv_subset t2 t1) then t2
else if (t2 == any) || (triv_subset t1 t2) then t1
else if (t1 == empty || t2 == empty)