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

Refactor the Bool/BoolVar code so that they share the same interface. Give...

Refactor the Bool/BoolVar code so that they share the same interface. Give access to the underlying atom module in BoolVar.
parent 6ee6ef2e
...@@ -42,8 +42,10 @@ types/var.cmo : misc/utils.cmo types/sortedList.cmi types/ident.cmo \ ...@@ -42,8 +42,10 @@ types/var.cmo : misc/utils.cmo types/sortedList.cmi types/ident.cmo \
misc/custom.cmo types/var.cmi misc/custom.cmo types/var.cmi
types/var.cmx : misc/utils.cmx types/sortedList.cmx types/ident.cmx \ types/var.cmx : misc/utils.cmx types/sortedList.cmx types/ident.cmx \
misc/custom.cmx types/var.cmi misc/custom.cmx types/var.cmi
types/boolVar.cmo : types/var.cmi misc/custom.cmo types/boolVar.cmi types/boolVar.cmo : types/var.cmi misc/custom.cmo misc/bool.cmi \
types/boolVar.cmx : types/var.cmx misc/custom.cmx types/boolVar.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/types.cmo : types/var.cmi misc/utils.cmo misc/stats.cmi \
types/sortedList.cmi misc/pretty.cmi misc/ns.cmi types/normal.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/intervals.cmi types/ident.cmo misc/encodings.cmi misc/custom.cmo \
...@@ -367,12 +369,13 @@ misc/html.cmi : ...@@ -367,12 +369,13 @@ misc/html.cmi :
types/compunit.cmi : types/compunit.cmi :
types/sortedList.cmi : misc/custom.cmo types/sortedList.cmi : misc/custom.cmo
misc/bool.cmi : misc/custom.cmo misc/bool.cmi : misc/custom.cmo
types/intervals.cmi : misc/custom.cmo types/intervals.cmi : misc/custom.cmo misc/bool.cmi
types/chars.cmi : misc/custom.cmo types/chars.cmi : misc/custom.cmo misc/bool.cmi
types/atoms.cmi : misc/ns.cmi misc/encodings.cmi misc/custom.cmo types/atoms.cmi : misc/ns.cmi misc/encodings.cmi misc/custom.cmo \
misc/bool.cmi
types/normal.cmi : types/normal.cmi :
types/var.cmi : types/sortedList.cmi misc/custom.cmo types/var.cmi : types/sortedList.cmi misc/custom.cmo
types/boolVar.cmi : types/var.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/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 types/boolVar.cmi \
types/atoms.cmi types/atoms.cmi
......
...@@ -8,7 +8,6 @@ sig ...@@ -8,7 +8,6 @@ sig
include Custom.T include Custom.T
val get: t -> (elem list * elem list) list val get: t -> (elem list * elem list) list
val get': t -> (elem list * (elem list) list) list
val empty : t val empty : t
val full : t val full : t
......
...@@ -4,7 +4,6 @@ sig ...@@ -4,7 +4,6 @@ sig
type elem type elem
val get: t -> (elem list * elem list) list val get: t -> (elem list * elem list) list
val get': t -> (elem list * (elem list) list) list
val empty : t val empty : t
val full : t val full : t
...@@ -19,11 +18,6 @@ sig ...@@ -19,11 +18,6 @@ sig
-> cap:('b -> 'b -> 'b) -> diff:('b -> 'b -> 'b) -> -> cap:('b -> 'b -> 'b) -> diff:('b -> 'b -> 'b) ->
atom:(elem -> 'b) -> t -> 'b atom:(elem -> 'b) -> t -> 'b
(*
val print: string -> (Format.formatter -> elem -> unit) -> t ->
(Format.formatter -> unit) list
*)
val trivially_disjoint : t -> t -> bool val trivially_disjoint : t -> t -> bool
end end
......
...@@ -74,7 +74,7 @@ val get_field_ascii : t -> string -> t ...@@ -74,7 +74,7 @@ val get_field_ascii : t -> string -> t
val get_variant : t -> string * t option val get_variant : t -> string * t option
val abstract : Types.Abstracts.abs -> 'a -> t val abstract : Types.Abstracts.T.t -> 'a -> t
val get_abstract : t -> 'a val get_abstract : t -> 'a
val mk_ref : Types.t -> t -> t val mk_ref : Types.t -> t -> t
......
...@@ -478,7 +478,7 @@ let int_type (name,min,max) = ...@@ -478,7 +478,7 @@ let int_type (name,min,max) =
let min = Intervals.V.mk min in let min = Intervals.V.mk min in
Intervals.right min Intervals.right min
| None, None -> | None, None ->
Intervals.any Intervals.full
in in
ignore (primitive name (Types.interval ival) (validate_interval ival name)) ignore (primitive name (Types.interval ival) (validate_interval ival name))
...@@ -695,5 +695,3 @@ let validate (_,_,v) = v ...@@ -695,5 +695,3 @@ let validate (_,_,v) = v
let of_st = function let of_st = function
| { st_name = Some n } -> get n | { st_name = Some n } -> get n
| _ -> assert false | _ -> assert false
...@@ -108,3 +108,9 @@ let contains_sample s t = ...@@ -108,3 +108,9 @@ let contains_sample s t =
| None, `Finite _ -> false | None, `Finite _ -> false
| Some (_,Some tag),_ -> contains tag t | Some (_,Some tag),_ -> contains tag t
| Some (ns, None),_ -> is_empty (diff (any_in_ns ns) t) | Some (ns, None),_ -> is_empty (diff (any_in_ns ns) t)
let trivially_disjoint = disjoint
let compute ~empty ~full ~cup ~cap ~diff ~atom b = assert false
let get _ = assert false
let iter _ = assert false
...@@ -13,11 +13,9 @@ module V : sig ...@@ -13,11 +13,9 @@ module V : sig
val to_string: t -> string val to_string: t -> string
end end
include Custom.T include Bool.S with type elem = V.t
val print : t -> (Format.formatter -> unit) list val print : t -> (Format.formatter -> unit) list
type elem = V.t
val empty : t val empty : t
val any : t val any : t
val full : t (* same as any *) val full : t (* same as any *)
......
...@@ -2,51 +2,17 @@ let (<) : int -> int -> bool = (<) ...@@ -2,51 +2,17 @@ let (<) : int -> int -> bool = (<)
let (>) : int -> int -> bool = (>) let (>) : int -> int -> bool = (>)
let (=) : int -> int -> bool = (=) let (=) : int -> int -> bool = (=)
(* this is the the of the Constructor container *)
module type E = sig
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
module type S = sig module type S = sig
type s module Atom : Bool.S
type elem = s Var.var_or_atom
include Custom.T
(* returns the union of all leaves in the BDD *)
val leafconj: t -> s
val get: t -> (elem list * elem list) list
(* val build : (elem list * elem list) list -> t*)
val empty : t
val full : t
(* same as full, but we keep it for the moment to avoid chaging
* the code everywhere *)
val any : t
val cup : t -> t -> t
val cap : t -> t -> t
val diff : t -> t -> t
val atom : elem -> t
val trivially_disjoint: t -> t -> bool include Bool.S with type elem = Atom.t Var.var_or_atom
(* vars a : return a bdd that is ( Any ^ Var a ) *) val var : Var.t -> t
val vars : Var.var -> t
val iter: (elem -> unit) -> t -> unit (** returns the union of all leaves in the BDD *)
val leafconj: t -> Atom.t
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 val is_empty : t -> bool
...@@ -54,13 +20,8 @@ module type S = sig ...@@ -54,13 +20,8 @@ module type S = sig
val print : ?f:(Format.formatter -> elem -> unit) -> t -> (Format.formatter -> unit) list val print : ?f:(Format.formatter -> elem -> unit) -> t -> (Format.formatter -> unit) list
(*
val extractvars : t -> [> `Var of Var.t ] bdd * t
*)
end end
module type MAKE = functor (T : E) -> S with type s = T.t
(* ternary BDD (* ternary BDD
* where the nodes are Atm of X.t | Var of String.t * where the nodes are Atm of X.t | Var of String.t
* Variables are always before Values * Variables are always before Values
...@@ -79,26 +40,26 @@ module type MAKE = functor (T : E) -> S with type s = T.t ...@@ -79,26 +40,26 @@ module type MAKE = functor (T : E) -> S with type s = T.t
* *
* *) * *)
module Make (T : E) : S with type s = T.t = struct module Make (T : Bool.S) : S with module Atom = T and type elem = T.t Var.var_or_atom = struct
(* ternary decision trees . cf section 11.3.3 Frish PhD *) (* ternary decision trees . cf section 11.3.3 Frish PhD *)
(* plus variables *) (* plus variables *)
(* `Atm are containers (Atoms, Chars, Intervals, Pairs ... ) (* `Atm are containers (Atoms, Chars, Intervals, Pairs ... )
* `Var are String * `Var are String
*) *)
type s = T.t module Atom = T
type elem = s Var.var_or_atom type elem = T.t Var.var_or_atom
module X : Custom.T with type t = elem = Var.Make(T) module X : Custom.T with type t = elem = Var.Make(T)
type 'a bdd = type 'a bdd = False
[ `True | True
| `False | Split of int * 'a * ('a bdd) * ('a bdd) * ('a bdd)
| `Split of int * 'a * ('a bdd) * ('a bdd) * ('a bdd) ]
type t = elem bdd type t = elem bdd
let rec equal_aux eq a b = let rec equal_aux eq a b =
(a == b) || (a == b) ||
match (a,b) with match (a,b) with
| `Split (h1,x1,p1,i1,n1), `Split (h2,x2,p2,i2,n2) -> | Split (h1,x1,p1,i1,n1), Split (h2,x2,p2,i2,n2) ->
(h1 == h2) && (h1 == h2) &&
(equal_aux eq p1 p2) && (equal_aux eq i1 i2) && (equal_aux eq p1 p2) && (equal_aux eq i1 i2) &&
(equal_aux eq n1 n2) && (eq x1 x2) (equal_aux eq n1 n2) && (eq x1 x2)
...@@ -112,55 +73,55 @@ module Make (T : E) : S with type s = T.t = struct ...@@ -112,55 +73,55 @@ module Make (T : E) : S with type s = T.t = struct
let rec compare a b = let rec compare a b =
if (a == b) then 0 if (a == b) then 0
else match (a,b) with else match (a,b) with
| `Split (h1,x1, p1,i1,n1), `Split (h2,x2, p2,i2,n2) -> | Split (h1,x1, p1,i1,n1), Split (h2,x2, p2,i2,n2) ->
if h1 < h2 then -1 else if h1 > h2 then 1 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 = 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 p1 p2 in if c <> 0 then c
else let c = compare i1 i2 in if c <> 0 then c else let c = compare i1 i2 in if c <> 0 then c
else compare n1 n2 else compare n1 n2
| `True,_ -> -1 | True,_ -> -1
| _, `True -> 1 | _, True -> 1
| `False,_ -> -1 | False,_ -> -1
| _,`False -> 1 | _,False -> 1
let rec hash = function let rec hash = function
| `True -> 1 | True -> 1
| `False -> 0 | False -> 0
| `Split(h,_,_,_,_) -> h | Split(h,_,_,_,_) -> h
let compute_hash x p i n = let compute_hash x p i n =
(X.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 let rec check = function
| `True -> () | True -> ()
| `False -> () | False -> ()
| `Split (h,x,p,i,n) -> | Split (h,x,p,i,n) ->
assert (h = compute_hash x p i n); assert (h = compute_hash x p i n);
(match p with `Split (_,y,_,_,_) -> assert (X.compare x y < 0) | _ -> ()); (match p with Split (_,y,_,_,_) -> assert (X.compare x y < 0) | _ -> ());
(match i 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) | _ -> ()); (match n with Split (_,y,_,_,_) -> assert (X.compare x y < 0) | _ -> ());
X.check x; check p; check i; check n X.check x; check p; check i; check n
let atom x = let atom x =
let h = X.hash x + 17 in (* partial evaluation of compute_hash... *) let h = X.hash x + 17 in (* partial evaluation of compute_hash... *)
`Split (h, x,`True,`False,`False) Split (h, x,True,False,False)
let vars v = let var v =
let compute_hash x p i n = let compute_hash x p i n =
(Var.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n) (Var.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)
in in
let a = atom (`Atm T.full) in let a = atom (`Atm T.full) in
let h = compute_hash v a `False `False in let h = compute_hash v a False False in
( `Split (h,`Var v,a,`False,`False) :> t ) ( Split (h,`Var v,a,False,False) :> t )
let rec iter f = function let rec iter f = function
| `Split (_, x, p,i,n) -> f x; iter f p; iter f i; iter f n | Split (_, x, p,i,n) -> f x; iter f p; iter f i; iter f n
| _ -> () | _ -> ()
let rec dump ppf = function let rec dump ppf = function
| `True -> Format.fprintf ppf "⫧" | True -> Format.fprintf ppf "⫧"
| `False -> Format.fprintf ppf "⫨" | False -> Format.fprintf ppf "⫨"
| `Split (_,x, p,i,n) -> | Split (_,x, p,i,n) ->
let fmt = format_of_string ( let fmt = format_of_string (
match x with match x with
`Var _ -> `Var _ ->
...@@ -173,51 +134,52 @@ module Make (T : E) : S with type s = T.t = struct ...@@ -173,51 +134,52 @@ module Make (T : E) : S with type s = T.t = struct
X.dump x dump p dump i dump n X.dump x dump p dump i dump n
let rec print f ppf = function let rec print f ppf = function
| `True -> Format.fprintf ppf "Any" | True -> Format.fprintf ppf "Any"
| `False -> Format.fprintf ppf "Empty" | False -> Format.fprintf ppf "Empty"
| `Split (_, x, p,i, n) -> | Split (_, x, p,i, n) ->
let flag = ref false in let flag = ref false in
let b () = if !flag then Format.fprintf ppf " | " else flag := true in let b () = if !flag then Format.fprintf ppf " | " else flag := true in
(match p with (match p with
| `True -> b(); Format.fprintf ppf "%a" f x | True -> b(); Format.fprintf ppf "%a" f x
| `False -> () | False -> ()
| _ -> b (); Format.fprintf ppf "%a & @[(%a)@]" f x (print f) p ); | _ -> b (); Format.fprintf ppf "%a & @[(%a)@]" f x (print f) p );
(match i with (match i with
| `True -> assert false; | True -> assert false;
| `False -> () | False -> ()
| _ -> b(); print f ppf i); | _ -> b(); print f ppf i);
(match n with (match n with
| `True -> b (); Format.fprintf ppf "@[~%a@]" f x | True -> b (); Format.fprintf ppf "@[~%a@]" f x
| `False -> () | False -> ()
| _ -> b (); Format.fprintf ppf "@[~%a@] & @[(%a)@]" f x (print f) n) | _ -> b (); Format.fprintf ppf "@[~%a@] & @[(%a)@]" f x (print f) n)
let pp_print = print X.dump let pp_print = print X.dump
let print ?(f=X.dump) = function let print ?(f=X.dump) = function
| `True -> assert false (* [] a bdd cannot be of this type *) | True -> assert false (* [] a bdd cannot be of this type *)
| `False -> [ fun ppf -> Format.fprintf ppf "Empty" ] | False -> [ fun ppf -> Format.fprintf ppf "Empty" ]
| c -> [ fun ppf -> print f ppf c ] | c -> [ fun ppf -> print f ppf c ]
(* return a list of pairs, where each pair holds the list (* return a list of pairs, where each pair holds the list
* of positive and negative elements on a branch *) * of positive and negative elements on a branch *)
let get x = let get x =
let rec aux accu pos neg = function let rec aux accu pos neg = function
| `True -> (List.rev pos, List.rev neg) :: accu | True -> (List.rev pos, List.rev neg) :: accu
| `False -> accu | False -> accu
| `Split (_,x, p,i,n) -> | Split (_,x, p,i,n) ->
let accu = aux accu (x::pos) neg p in let accu = aux accu (x::pos) neg p in
let accu = aux accu pos (x::neg) n in let accu = aux accu pos (x::neg) n in
let accu = aux accu pos neg i in let accu = aux accu pos neg i in
accu accu
in aux [] [] [] x in aux [] [] [] x
let leafconj x = let leafconj x =
let rec aux accu = function let rec aux accu = function
| `True -> accu | True -> accu
| `False -> accu | False -> accu
| `Split (_,`Atm x, `True,`False,`False) -> x :: accu | Split (_,`Atm x, True,False,False) -> x :: accu
| `Split (_,`Atm x, _,_,_) -> assert false | Split (_,`Atm x, _,_,_) -> assert false
| `Split (_,`Var x, p,i,n) -> | Split (_,`Var x, p,i,n) ->
let accu = aux accu p in let accu = aux accu p in
let accu = aux accu n in let accu = aux accu n in
let accu = aux accu i in let accu = aux accu i in
...@@ -227,11 +189,11 @@ module Make (T : E) : S with type s = T.t = struct ...@@ -227,11 +189,11 @@ module Make (T : E) : S with type s = T.t = struct
let compute ~empty ~full ~cup ~cap ~diff ~atom b = let compute ~empty ~full ~cup ~cap ~diff ~atom b =
let rec aux = function let rec aux = function
| `True -> full | True -> full
| `False -> empty | False -> empty
| `Split (_,`Atm x,`True,_,_) when T.equal x T.empty -> empty | Split (_,`Atm x,True,_,_) when T.equal x T.empty -> empty
| `Split (_,`Atm x,`True,_,_) when T.equal x T.full -> full | Split (_,`Atm x,True,_,_) when T.equal x T.full -> full
| `Split(_,x, p,i,n) -> | Split(_,x, p,i,n) ->
let x1 = atom x in let x1 = atom x in
let p = cap x1 (aux p) in let p = cap x1 (aux p) in
let i = aux i in let i = aux i in
...@@ -243,21 +205,20 @@ module Make (T : E) : S with type s = T.t = struct ...@@ -243,21 +205,20 @@ module Make (T : E) : S with type s = T.t = struct
(* Invariant: correct hash value *) (* Invariant: correct hash value *)
let split0 x pos ign neg = let split0 x pos ign neg =
`Split (compute_hash x pos ign neg, x, pos, ign, neg) Split (compute_hash x pos ign neg, x, pos, ign, neg)
let empty = `False let empty = False
let full = split0 (`Atm T.full) `True `False `False let full = split0 (`Atm T.full) True False False
let any = full
let is_empty t = (t == empty) let is_empty t = (t == empty)
(* Invariants: (* Invariants:
`Split (x, pos,ign,neg) ==> (ign <> `True), (pos <> neg) Split (x, pos,ign,neg) ==> (ign <> True), (pos <> neg)
*) *)
let rec has_true = function let rec has_true = function
| [] -> false | [] -> false
| `True :: _ -> true | True :: _ -> true
| _ :: l -> has_true l | _ :: l -> has_true l
let rec has_same a = function let rec has_same a = function
...@@ -267,9 +228,9 @@ module Make (T : E) : S with type s = T.t = struct ...@@ -267,9 +228,9 @@ module Make (T : E) : S with type s = T.t = struct
(* split removes redundant subtrees from the positive and negative (* split removes redundant subtrees from the positive and negative
* branch if they are present in the lazy union branch *) * branch if they are present in the lazy union branch *)
let rec split x p i n = let rec split x p i n =
if X.equal (`Atm T.empty) x then `False if X.equal (`Atm T.empty) x then False
(* 0?p:i:n -> 0 *) (* 0?p:i:n -> 0 *)
else if i == `True then `True else if i == True then True
(* x?p:1:n -> 1 *) (* x?p:1:n -> 1 *)
else if equal p n then p ++ i else if equal p n then p ++ i
else let p = simplify p [i] and n = simplify n [i] in else let p = simplify p [i] and n = simplify n [i] in
...@@ -280,12 +241,12 @@ module Make (T : E) : S with type s = T.t = struct ...@@ -280,12 +241,12 @@ module Make (T : E) : S with type s = T.t = struct
(* simplify t l -> bdd of ( t // l ) *) (* simplify t l -> bdd of ( t // l ) *)
and simplify a l = and simplify a l =
match a with match a with
| `False -> `False | False -> False
| `True -> if has_true l then `False else `True | True -> if has_true l then False else True
| `Split (_,`Atm x, `False,`False,`True) -> | Split (_,`Atm x, False,False,True) ->
split (`Atm(T.diff T.full x)) `True `False `False split (`Atm(T.diff T.full x)) True False False
| `Split (_,x,p,i,n) -> | Split (_,x,p,i,n) ->
if (has_true l) || (has_same a l) then `False if (has_true l) || (has_same a l) then False
else s_aux2 a x p i n [] [] [] l else s_aux2 a x p i n [] [] [] l
and s_aux2 a x p i n ap ai an = function and s_aux2 a x p i n ap ai an = function
| [] -> | [] ->
...@@ -295,10 +256,10 @@ module Make (T : E) : S with type s = T.t = struct ...@@ -295,10 +256,10 @@ module Make (T : E) : S with type s = T.t = struct
if equal p n then p ++ i else split0 x p i n 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 | 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 and s_aux3 a x p i n ap ai an l = function