Commit 885bd4fb authored by Pietro Abate's avatar Pietro Abate
Browse files

various improvements and code clean up

parent 0cf16d9d
......@@ -170,9 +170,9 @@ module TLV = struct
}
let diff x y = {
b = x.b && y.b;
s = Set.diff x.s y.s;
f = Set.diff x.f y.f;
b = x.b && y.b
}
(* true if it contains only one variable *)
......@@ -2506,25 +2506,22 @@ module Tallying = struct
) m2
) m1
(* this is O(n^2) filter . Only more restritive constraints sets are kept *)
(* Only more restritive constraints sets are kept *)
let union x y =
match S.is_empty x,S.is_empty y with
|true,true -> S.empty
|true,true -> S.empty (* unsat *)
|false,true -> x
|true,false -> y
|false,false ->
S.fold (fun m1 acc ->
if M.is_empty m1 then S.union y acc else
S.fold (fun m2 acc1 ->
if (M.compare semantic_compare m1 m2) = 0 then S.add m1 acc1 else
if M.is_empty m1 then S.add m2 acc1 else
(* if M.is_empty m1 then S.add m2 acc1 else *)
if M.is_empty m2 then S.add m1 acc1 else
if lessgeneral m1 m2 then
S.add m1 acc1 (* equivalent or m1 < m2 ==> discard m2 *)
else
if lessgeneral m2 m1 then
S.add m2 acc1 (* m2 < m1 ==> discard m1 *)
else
S.add m1 (S.add m2 acc1) (* m1 <> m2 ==> we add both *)
if (M.compare semantic_compare m1 m2) = 0 then S.add m1 acc1 else
if lessgeneral m1 m2 then S.add m1 acc1 (* m1 < m2 ==> discard m2 *)
else if lessgeneral m2 m1 then S.add m2 acc1 (* m2 < m1 ==> discard m1 *)
else S.add m1 (S.add m2 acc1) (* m1 <> m2 ==> we add both *)
) y acc
) x S.empty
......@@ -2535,6 +2532,7 @@ module Tallying = struct
if S.is_empty x || S.is_empty y then S.empty
else
S.fold (fun m1 acc ->
if M.is_empty m1 then S.union y acc else
S.fold (fun m2 acc1 -> S.add (merge m1 m2) acc1) y acc
) x S.empty
......@@ -2579,7 +2577,7 @@ module Tallying = struct
let single_arrow = single_aux (fun p -> { empty with arrow = BoolPair.atom (`Atm p) })
(* check if there exists a toplevel varaible : fun (pos,neg) *)
let toplevel single norm_rec mem (p,n) = match (p,n) with
let toplevel single norm_rec mem p n = match (p,n) with
|([],(`Var x)::neg) ->
let t = single (false,x,[],neg) in
CS.singleton (Neg (t,`Var x))
......@@ -2601,31 +2599,30 @@ module Tallying = struct
CS.singleton (Neg (t,`Var x))
|([`Atm t], []) -> norm_rec (t,mem)
|([],[`Atm t]) -> failwith "impossible0" (* norm_rec (t,mem) *)
|((`Var x)::pos, [`Atm _]) -> failwith "impossible5"
|([],[]) -> failwith "impossible"
|([],_) -> failwith "impossible2"
|(_,[]) -> failwith "impossible3"
|_,_ -> failwith "impossible4"
|_,_ -> assert false
let big_prod f acc l =
List.fold_left (fun acc (pos,neg) ->
if CS.S.is_empty acc then acc else
CS.prod acc (f pos neg)
) acc l
(* norm generates a constraint set for the costraint t <= 0 *)
let rec norm (t,mem) =
if DescrHash.mem mem t || is_empty t then CS.sat else begin
if is_empty t then CS.sat else
if DescrHash.mem mem t then CS.sat else begin
DescrHash.add mem t ();
let aux_base single norm_aux acc l =
List.fold_left (fun acc (pos,neg) ->
if CS.S.is_empty acc then acc else (* lazy product *)
CS.prod acc (toplevel single norm_aux mem (pos,neg))
) acc l
big_prod (toplevel single norm_aux mem) acc l
in
let accu = CS.sat in
let accu = aux_base single_atoms normatoms accu (BoolAtoms.get t.atoms) in
let accu = aux_base single_chars normchars accu (BoolChars.get t.chars) in
let accu = aux_base single_ints normints accu (BoolIntervals.get t.ints) in
let accu = aux_base single_arrow normarrow accu (BoolPair.get t.arrow) in
let accu = aux_base single_times normpair accu (BoolPair.get t.times) in
let accu = aux_base single_xml normpair accu (BoolPair.get t.xml) in
let accu = aux_base single_record normrec accu (BoolRec.get t.record) in
let accu = aux_base single_arrow normarrow accu (BoolPair.get t.arrow) in
accu
end
......@@ -2661,7 +2658,7 @@ module Tallying = struct
let con0 = aux t1 t2 neg in
CS.union (CS.union con1 con2) con0
in
List.fold_left (fun acc (p,n) -> CS.prod acc (norm_prod p n)) CS.sat (Pair.get t)
big_prod norm_prod CS.sat (Pair.get t)
and normrec (t,mem) =
let norm_rec ((oleft,left),rights) =
......@@ -2680,7 +2677,9 @@ module Tallying = struct
let c = Array.fold_left (fun acc t -> CS.prod (norm (t,mem)) acc) CS.sat left in
CS.prod (aux left [] rights) c
in
List.fold_left (fun acc (_,p,n) -> CS.prod acc (norm_rec (p,n))) CS.sat (get_record t)
List.fold_left (fun acc (_,p,n) ->
if CS.S.is_empty acc then acc else CS.prod acc (norm_rec (p,n))
) CS.sat (get_record t)
(* arrow(p,{t1 -> t2}) = [t1] v arrow'(t1,any \ t2,p)
* arrow'(t1,acc,{s1 -> s2} v p) =
......@@ -2688,10 +2687,10 @@ module Tallying = struct
([acc ^ {s2}] v arrow'(t1,acc ^ {s2},p))
t1 -> t2 \ s1 -> s2 =
[t1] v (([t1\s1] v {[]}) ^ ([any\t2^s2] v {[]}))
[t1] v (([t1\s1] v {[]}) ^ ([t2\s2] v {[]}))
Bool -> Bool \ Int -> A =
[Bool] v (([Bool\Int] v {[]}) ^ ([Any\Bool^A] v {[]})
[Bool] v (([Bool\Int] v {[]}) ^ ([Bool\A] v {[]})
P(Q v {a}) = {a} v P(Q) v {X v {a} | X \in P(Q) }
*)
......@@ -2700,7 +2699,7 @@ module Tallying = struct
match neg with
|[] -> CS.unsat
|(t1,t2) :: n ->
let con1 = norm (descr t1, mem) in
let con1 = norm (descr t1, mem) in (* [t1] *)
let con2 = aux (descr t1) (diff any (descr t2)) pos in
let con0 = norm_arrow pos n in
CS.union (CS.union con1 con2) con0
......@@ -2709,15 +2708,15 @@ module Tallying = struct
|(s1,s2) :: p ->
let t1s1 = diff t1 (descr s1) in
let acc1 = cap acc (descr s2) in
let con1 = norm (t1s1, mem) in
let con2 = norm (acc1, mem) in
let con1 = norm (t1s1, mem) in (* [t1 \ s1] *)
let con2 = norm (acc1, mem) in (* [(Any \ t2) ^ s2] *)
let con10 = aux t1s1 acc p in
let con20 = aux t1 acc1 p in
let con11 = CS.union con1 con10 in
let con22 = CS.union con2 con20 in
CS.prod con11 con22
in
List.fold_left (fun acc (p,n) -> CS.prod acc (norm_arrow p n)) CS.sat (Pair.get t)
big_prod norm_arrow CS.sat (Pair.get t)
let memo_norm = DescrHash.create 17
let norm t =
......
......@@ -129,8 +129,7 @@ let deferr s = raise (Patterns.Error s)
(* x and y have been internalized; if they were equivalent,
they would be equal *)
else match x.desc,y.desc with
| IType (tx,_), IType (ty,_) when (Types.no_var tx) && (Types.no_var ty) && (Types.equal tx ty) -> link x y
| IType (tx,_), IType (ty,_) when (Types.no_var tx) && (Types.no_var ty) -> ()
| IType (tx,_), IType (ty,_) when (Types.equal tx ty) -> if (Types.no_var tx) then () else link x y
| IOr (x1,x2,_), IOr (y1,y2,_)
| IAnd (x1,x2,_), IAnd (y1,y2,_)
| IDiff (x1,x2,_), IDiff (y1,y2,_)
......
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