Commit 58c7c621 authored by Pietro Abate's avatar Pietro Abate
Browse files

[r2005-06-13 15:20:13 by afrisch] Simplifications

Original author: afrisch
Date: 2005-06-13 15:20:14+00:00
parent 3cd1a52f
......@@ -145,6 +145,7 @@ OBJECTS = \
misc/state.cmo misc/pool.cmo misc/encodings.cmo \
misc/pretty.cmo misc/ns.cmo misc/inttbl.cmo misc/imap.cmo \
misc/html.cmo \
misc/ptmap.cmo misc/hashset.cmo \
\
types/sortedList.cmo misc/bool.cmo types/boolean.cmo types/ident.cmo \
types/intervals.cmo \
......
......@@ -26,11 +26,13 @@ misc/imap.cmo: misc/imap.cmi
misc/imap.cmx: misc/imap.cmi
misc/html.cmo: misc/html.cmi
misc/html.cmx: misc/html.cmi
misc/ptmap.cmo: misc/ptmap.cmi
misc/ptmap.cmx: misc/ptmap.cmi
types/sortedList.cmo: misc/serialize.cmi misc/custom.cmo types/sortedList.cmi
types/sortedList.cmx: misc/serialize.cmx misc/custom.cmx types/sortedList.cmi
misc/bool.cmo: types/sortedList.cmi misc/serialize.cmi misc/custom.cmo \
misc/bool.cmo: misc/serialize.cmi misc/hashset.cmo misc/custom.cmo \
misc/bool.cmi
misc/bool.cmx: types/sortedList.cmx misc/serialize.cmx misc/custom.cmx \
misc/bool.cmx: misc/serialize.cmx misc/hashset.cmx misc/custom.cmx \
misc/bool.cmi
types/boolean.cmo: types/sortedList.cmi misc/custom.cmo types/boolean.cmi
types/boolean.cmx: types/sortedList.cmx misc/custom.cmx types/boolean.cmi
......
......@@ -200,7 +200,7 @@ let debug ppf tenv cenv = function
Format.fprintf ppf "[DEBUG:compile]@.";
let t = Typer.typ tenv t
and pl = List.map (Typer.pat tenv) pl in
Patterns.Compile2.debug_compile ppf t pl;
Patterns.Compile.debug_compile ppf t pl;
Format.fprintf ppf "@.";
(*
......
......@@ -8,6 +8,7 @@ sig
include Custom.T
val get: t -> (elem list * elem list) list
val get': t -> (elem list * (elem list) list) list
val empty : t
val full : t
......@@ -142,6 +143,24 @@ struct
accu
let get x = get [] [] [] 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 ->
(* if (List.length l > 1) then (print_int (List.length l); flush stdout); *)
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
......@@ -157,7 +176,7 @@ struct
(* Invariant: correct hash value *)
let split x pos ign neg =
let split0 x pos ign neg =
Split (compute_hash x pos ign neg, x, pos, ign, neg)
......@@ -168,135 +187,81 @@ struct
let full = True
(* Invariants:
Split (x, pos,ign,neg) ==> (ign <> True);
(pos <> False or neg <> False)
Split (x, pos,ign,neg) ==> (ign <> True), (pos <> neg)
*)
let split x pos ign neg =
if ign == True then True
else if (pos == False) && (neg == False) then ign
else split x pos ign neg
let rec has_true = function
| [] -> false
| True :: _ -> true
| _ :: l -> has_true l
(* Invariant:
- no ``subsumption'
*)
let rec has_same a = function
| [] -> false
| b :: l -> (equal a b) || (has_same a l)
(*
let rec simplify a b =
if equal a b then False
else match (a,b) with
| False,_ | _, True -> False
| a, False -> a
| True, _ -> True
| Split (_,x1,p1,i1,n1), Split (_,x2,p2,i2,n2) ->
let c = X.compare x1 x2 in
if c = 0 then
let p1' = simplify (simplify p1 i2) p2
and i1' = simplify i1 i2
and n1' = simplify (simplify n1 i2) n2 in
if (p1 != p1') || (n1 != n1') || (i1 != i1')
then split x1 p1' i1' n1'
else a
else if c > 0 then
simplify a i2
else
let p1' = simplify p1 b
and i1' = simplify i1 b
and n1' = simplify n1 b in
if (p1 != p1') || (n1 != n1') || (i1 != i1')
then split x1 p1' i1' n1'
else a
*)
let rec split x p i n =
if i == True then True
else if equal p n then p ++ i
else let p = simplify p [i] and n = simplify n [i] in
if equal p n then p ++ i
else split0 x p i n
let rec simplify a l =
if (a == False) then False else simpl_aux1 a [] l
and simpl_aux1 a accu = function
and simplify a l =
match 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
| [] ->
if accu == [] then a else
(match a with
| True -> True
| False -> assert false
| Split (_,x,p,i,n) -> simpl_aux2 x p i n [] [] [] accu)
| False :: l -> simpl_aux1 a accu l
| True :: l -> False
| b :: l -> if a == b then False else simpl_aux1 a (b::accu) l
and simpl_aux2 x p i n ap ai an = function
| [] -> split x (simplify p ap) (simplify i ai) (simplify n an)
| (Split (_,x2,p2,i2,n2) as b) :: l ->
let c = X.compare x2 x in
if c < 0 then
simpl_aux3 x p i n ap ai an l i2
else if c > 0 then
simpl_aux2 x p i n (b :: ap) (b :: ai) (b :: an) l
else
simpl_aux2 x p i n (p2 :: i2 :: ap) (i2 :: ai) (n2 :: i2 :: an) l
| _ -> assert false
and simpl_aux3 x p i n ap ai an l = function
| False -> simpl_aux2 x p i n ap ai an l
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 ->
let c = X.compare x2 x in
if c < 0 then
simpl_aux3 x p i n ap ai an l i2
else if c > 0 then
simpl_aux2 x p i n (b :: ap) (b :: ai) (b :: an) l
else
simpl_aux2 x p i n (p2 :: i2 :: ap) (i2 :: ai) (n2 :: i2 :: an) l
let split x p i n =
split x (simplify p [i]) i (simplify n [i])
let rec ( ++ ) a b =
(* if equal a b then a *)
if a == b then a
else match (a,b) with
| True, _ | _, True -> True
| False, a | a, False -> a
| 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
(* Pseudo-Invariant:
- pos <> neg
*)
let split x pos ign neg =
if equal pos neg then (neg ++ ign) else split x pos ign neg
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
and ( ++ ) a b = if a == b then a
else match (a,b) with
| True, _ | _, True -> True
| False, a | a, False -> a
| 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 ? *)
let rec ( ** ) a b =
(* if equal a b then a *)
if a == b then a
else match (a,b) with
| True, a | a, True -> a
| False, _ | _, 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 ++ i2) ++ (p2 ** i1))
(i1 ** i2)
(n1 ** (n2 ++ i2) ++ (n2 ** i1)) *)
split x1
((p1 ++ i1) ** (p2 ++ i2))
False
((n1 ++ i1) ** (n2 ++ i2))
else if c < 0 then
split x1 (p1 ** b) (i1 ** b) (n1 ** b)
else
split x2 (p2 ** a) (i2 ** a) (n2 ** a)
let rec ( ** ) a b = if a == b then a else match (a,b) with
| True, a | a, True -> a
| False, _ | _, 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 ++ i2) ++ (p2 ** i1))
(i1 ** i2)
(n1 ** (n2 ++ i2) ++ (n2 ** i1))
(* if (p2 == True) && (n2 == False)
then split x1 (p1 ++ i1) (i1 ** i2) (n1 ** i2)
else if (p2 == False) && (n2 == True)
then split x1 (p1 ** i2) (i1 ** i2) (n1 ++ i1)
else
split x1 ((p1++i1) ** (p2 ++ i2)) False ((n1 ++ i1) ** (n2 ++ i2))
*)
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 =
if a == b then a == False
......@@ -321,9 +286,12 @@ struct
let rec neg = function
| True -> False
| False -> True
(* | Split (_,x, p,i,False) -> split x False (neg (i ++ p)) (neg i)
| 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,False,n) -> split x (neg p) (neg (p ++ n)) (neg n)
(* | Split (_,x, p, False, False) ->
split x False (neg p) True
| Split (_,x, False, False, n) -> split x True (neg n) False *)
| Split (_,x, p,i,n) -> split x (neg (i ++ p)) False (neg (i ++ n))
let rec ( // ) a b =
......@@ -336,10 +304,12 @@ struct
| Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
let c = X.compare x1 x2 in
if c = 0 then
split x1
((p1 ++ i1) // (p2 ++ i2))
False
((n1 ++ i1) // (n2 ++ i2))
if (i2 == False) && (n2 == False)
then split x1 (p1 // p2) (i1 // p2) (n1 ++ i1)
(* else if (i2 == False) && (p2 == False)
then split x1 (p1 ++ i1) (i1 // n2) (n1 // n2) *)
else
split x1 ((p1++i1) // (p2 ++ i2)) False ((n1++i1) // (n2 ++ i2))
else if c < 0 then
split x1 (p1 // b) (i1 // b) (n1 // b)
(* split x1 ((p1 ++ i1)// b) False ((n1 ++i1) // b) *)
......@@ -386,7 +356,7 @@ struct
(cap_atom x true p) ++ i ++ (cap_atom x false n)
(* split x p i n is not ok, because order of keys might have changed! *)
(*
(*
let not_triv = function
| True | False -> false
| _ -> true
......@@ -404,10 +374,18 @@ struct
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 type S' = sig
include S
type bdd = False | True | Br of elem * t * t
......@@ -603,904 +581,308 @@ struct
| Zero -> False | One -> True | Branch (x,p,n,_,_) -> Br (x,p,n)
end
(*
module Simplify(X : Custom.T) = struct
type elem = X.t
module V = SortedList.Make(X)
module Make2(X : Custom.T) = struct
module XSet = Hashset.MakeSet(X)
type tree = Split of elem list * elem list * tree list option
type f = {
pos: V.t;
neg: V.t;
subs: fset;
mutable id: int; (* unique id for hash consing *)
mutable dnf: (V.t * V.t) list option;
mutable dnf_neg: (V.t * V.t) list option;
type 'a s = {
pos : XSet.t;
neg : XSet.t;
sub : 'a;
(* vars : XSet.t; *)
hash : int;
}
and fset =
| Empty
| Leaf of f
| Branch of int * int * fset * fset
type t = PosF of f | NegF of f | PosV of X.t | NegV of X.t | Zero | One
let id k = k.id
module F = struct
let empty = Empty
let is_empty = function Empty -> true | _ -> false
let singleton k = Leaf k
let zero_bit k m = (k land m) == 0
let rec mem k = function
| Empty -> false
| Leaf j -> k == j
| Branch (_, m, l, r) -> mem k (if zero_bit (id k) m then l else r)
let lowest_bit x = x land (-x)
let branching_bit p0 p1 = lowest_bit (p0 lxor p1)
let mask p m = p land (m-1)
let join (p0,t0,p1,t1) =
let m = branching_bit p0 p1 in
if zero_bit p0 m then Branch (mask p0 m, m, t0, t1)
else Branch (mask p0 m, m, t1, t0)
let match_prefix k p m = (mask k m) == p
let add k t =
let rec ins = function
| Empty -> Leaf k
| Leaf j as t -> if j == k then t else join (id k, Leaf k, id j, t)
| Branch (p,m,t0,t1) as t ->
if match_prefix (id k) p m then
if zero_bit (id k) m then Branch (p, m, ins t0, t1)
else Branch (p, m, t0, ins t1)
else join (id k, Leaf k, p, t)
in
ins t
let rec union s t = match s,t with
| Empty, t -> t
| t, Empty -> t
| Leaf k, t -> add k t
| t, Leaf k -> add k t
| (Branch (p,m,s0,s1) as s), (Branch (q,n,t0,t1) as t) ->
if m == n && match_prefix q p m then
Branch (p, m, union s0 t0, union s1 t1)
else if m < n && match_prefix q p m then
if zero_bit q m then Branch (p, m, union s0 t, s1)
else Branch (p, m, s0, union s1 t)
else if m > n && match_prefix p q n then
if zero_bit p n then Branch (q, n, union s t0, t1)
else Branch (q, n, t0, union s t1)
else join (p, s, q, t)
let rec subset s1 s2 = match s1,s2 with
| Empty, _ -> true
| _, Empty -> false
| Leaf k1, _ -> mem k1 s2
| Branch _, Leaf _ -> false
| Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
if m1 == m2 && p1 == p2 then subset l1 l2 && subset r1 r2
else if m1 > m2 && match_prefix p1 p2 m2 then
if zero_bit p1 m2 then subset l1 l2 && subset r1 l2
else subset l1 r2 && subset r1 r2
else
false
let branch = function
| (_,_,Empty,t) -> t
| (_,_,t,Empty) -> t
| (p,m,t0,t1) -> Branch (p,m,t0,t1)
let rec remove k = function
| Empty -> Empty
| Leaf j as t -> if k == j then Empty else t
| Branch (p,m,t0,t1) as t ->
if match_prefix (id k) p m then
if zero_bit (id k) m then branch (p, m, remove k t0, t1)
else branch (p, m, t0, remove k t1)
else t
let rec inter s1 s2 = match s1,s2 with
| Empty, _ -> Empty
| _, Empty -> Empty
| Leaf k1, _ -> if mem k1 s2 then s1 else Empty
| _, Leaf k2 -> if mem k2 s1 then s2 else Empty
| Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
if m1 == m2 && p1 == p2 then union (inter l1 l2) (inter r1 r2)
else if m1 < m2 && match_prefix p2 p1 m1 then
inter (if zero_bit p2 m1 then l1 else r1) s2
else if m1 > m2 && match_prefix p1 p2 m2 then
inter s1 (if zero_bit p1 m2 then l2 else r2)
else Empty
let rec split s1 s2 = match s1,s2 with
| Empty, _ -> Empty,Empty,s2
| _, Empty -> s1,Empty,Empty
| Leaf k1, _ -> if mem k1 s2 then Empty,s1,(remove k1 s2) else s1,Empty,s2
| _, Leaf k2 -> if mem k2 s1 then (remove k2 s1),s2,Empty else s1,Empty,s2
| Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
if m1 == m2 && p1 == p2 then
let x1,x12,x2 = split l1 l2
and y1,y12,y2 = split r1 r2 in
union x1 y1, union x12 y12, union x2 y2
else if m1 < m2 && match_prefix p2 p1 m1 then
if zero_bit p2 m1
then let x1,x12,x2 = split l1 s2 in union x1 r1, x12, x2
else let x1,x12,x2 = split r1 s2 in union l1 x1, x12, x2
else if m2 < m1 && match_prefix p1 p2 m1 then
if zero_bit p1 m2
then let x1,x12,x2 = split l2 s1 in x1, x12, union x2 r2
else let x1,x12,x2 = split r1 s2 in x1, x12, union l2 x2
else (s1,Empty,s2)
let rec diff s1 s2 = match s1,s2 with
| Empty, _ -> Empty
| _, Empty -> s1
| Leaf k1, _ -> if mem k1 s2 then Empty else s1
| _, Leaf k2 -> remove k2 s1
| Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
if m1 == m2 && p1 == p2 then union (diff l1 l2) (diff r1 r2)
else if m1 < m2 && match_prefix p2 p1 m1 then
if zero_bit p2 m1 then union (diff l1 s2) r1
else union l1 (diff r1 s2)
else if m1 > m2 && match_prefix p1 p2 m2 then
if zero_bit p1 m2 then diff s1 l2 else diff s1 r2
else s1
let rec intersect s1 s2 = match s1,s2 with
| Empty, _ -> false
| _, Empty -> false
| Leaf k1, _ -> mem k1 s2
| _, Leaf k2 -> mem k2 s1
| Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
if m1 == m2 && p1 == p2 then intersect l1 l2 || intersect r1 r2
else if m1 < m2 && match_prefix p2 p1 m1 then
intersect (if zero_bit p2 m1 then l1 else r1) s2
else if m1 > m2 && match_prefix p1 p2 m2 then
intersect s1 (if zero_bit p1 m2 then l2 else r2)
else false
let disjoint s1 s2 = not (intersect s1 s2)
let rec equal x y = x == y || match x,y with
| Leaf k1, Leaf k2 -> k1 == k2
| Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
p1 == p2 && m1 == m2 && (equal l1 l2) && (equal r1 r2)
| _ -> false
let rec compare x y = match x,y with
| Empty, Empty -> 0
| Leaf k1, Leaf k2 -> id k1 - id k2
| Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
if (p1 < p2) then (-1) else if (p1 > p2) then 1
else if (m1 < m2) then (-1) else if (m1 > m2) then 1
else let c = compare l1 l2 in if c != 0 then c
else compare r1 r2
| Empty, _ -> -1 | _, Empty -> 1
| Leaf _, _ -> -1 | _, Leaf _ -> 1
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)
(* 3,19,65599,1048577 *)
let z1 = 3 (* int_of_string (Sys.getenv "Z1") *)
let z2 = 19 (* int_of_string (Sys.getenv "Z2") *)
let z3 = 65599 (* int_of_string (Sys.getenv "Z3") *)
let z4 = 1048577 (* int_of_string (Sys.getenv "Z4") *)
let rec hash = function
| Empty -> 0
| Leaf k -> 1 + z1 * (id k)
| Branch (p,m,l,r) ->
2 + z1 * p + z2 * m + z3 * (hash l) + z4 * (hash r)
let rec iter f = function
| Empty -> ()
| Leaf k -> f k
| Branch (_,_,t0,t1) -> iter f t0; iter f t1
let rec exists f = function
| Empty -> false
| Leaf k -> f k
| Branch (_,_,t0,t1) -> exists f t0 || exists f t1
let rec fold f s accu = match s with
| Empty -> accu
| Leaf k -> f k accu
| Branch (_,_,t0,t1) -> fold f t0 (fold f t1 accu)
let rec card f s accu = match s with
| Empty -> accu
| Leaf k -> f k accu
| Branch (_,_,t0,t1) -> fold f t0 (fold f t1 accu)
let rec cardinal = function
| Empty -> 0
| Leaf _ -> 1
| Branch (_,_,t0,t1) -> cardinal t0 + cardinal t1
let rec elements accu = function
| Empty -> accu
| Leaf k -> k :: accu
| Branch (_,_,t0,t1) -> elements (elements accu t0) t1
end
let print_f px =
let rec aux ppf f =
let first = ref true in
let sep () = if !first then first := false else Format.fprintf ppf "." in
V.iter (fun x -> sep (); Format.fprintf ppf "%a" px x) f.pos;
V.iter (fun x -> sep (); Format.fprintf ppf "~%a" px x) f.neg;
F.iter (fun f -> sep (); Format.fprintf ppf "~(@[%a@])" aux f) f.subs;
if !first then Format.fprintf ppf "."
in
fun ppf f -> (*allvars ppf f; *) aux ppf f
let print_t px ppf = function
| PosV f -> Format.fprintf ppf "%a" px f
| NegV f -> Format.fprintf ppf "~%a" px f
| PosF f -> Format.fprintf ppf "%a" (print_f px) f
| NegF f -> Format.fprintf ppf "~(%a)" (print_f px) f
| Zero -> Format.fprintf ppf "0"
| One -> Format.fprintf ppf "1"
let () =
tset_compare := Obj.magic TSet.compare;
tset_equal := Obj.magic TSet.equal
let dump = print_t
(fun ppf i -> Format.fprintf ppf "%i" (X.hash i))
type elem = X.t
type t = TSet.t s
(*
let dump_vars ppf v =
let first = ref true in
let sep () = if !first then first := false else Format.fprintf ppf "|" in
V.iter (fun x -> sep (); Format.fprintf ppf "%i" (X.hash x)) v