Commit b9334e65 authored by Pietro Abate's avatar Pietro Abate
Browse files

Filter out less restrictive constraints sets

parent 8b9f098a
......@@ -52,6 +52,24 @@ let norm_tests = [
)
);
(*
"([0--*] & `true)", "(`$A | Int) & ((Any \\ `$A) | Bool)",
*)
"(`$A , `$B)","(Int , Bool)",
cap
(mk_pos ("A","Int"))
(mk_pos ("B","Bool"))
(*
cup
(mk_pos ("A","Empty"))
(cup
(cap
(mk_pos ("A","Int"))
(mk_pos ("B","Bool"))
)
(mk_pos ("B","Empty"))
);
*)
]
let m_compare = Tallying.CS.M.compare Types.compare
......@@ -92,11 +110,12 @@ let merge_tests = [
);
[("`$A", "`$B")], mk_pos ("A","`$B");
[("`$B", "Empty")], mk_pos ("B","Empty");
[("`$A", "Int");("`$B", "Bool"); ("`$A", "Empty")],cap (mk_pos ("A", "Empty")) (mk_pos ("B", "Bool"));
]
let test_merge =
let print_test l =
String.concat ";" (List.map (fun (s,t) -> Printf.sprintf " %s \\ %s" s t) l)
String.concat ";" (List.map (fun (s,t) -> Printf.sprintf " %s >= %s" s t) l)
in
"test tallying merge" >:::
List.map (fun (l,expected) ->
......@@ -149,11 +168,10 @@ let mk_e ll =
let tallying_tests = [
[("((Int | Bool) -> Int)", "(`$A -> `$B)"); ("(`$A -> Bool)","(`$B -> `$B)")], mk_e [
[("A","Empty");("B","Empty")];
(* [("A","Empty");("B","Empty")]; *)
[("A","Int | Bool");("B","Int | Bool")]
];
[("(Int -> Int) | (Bool -> Bool)", "(`$A -> `$B)")], mk_e [
[("A","Empty")];
[("A","Empty");("B","Empty")];
];
[("((Int,Int) , (Int | Bool))","(`$A,Int) | ((`$B,Int),Bool)")], mk_e [[("A", "(Int,Int)"); ("B","Int")]];
......
......@@ -2263,7 +2263,7 @@ module Tallying = struct
let print_lst f ppf l =
let rec aux ppf = function
|[] -> Format.fprintf ppf "@."
|[h] -> Format.fprintf ppf "%a@." f h
|[h] -> Format.fprintf ppf "%a" f h
|h::t -> Format.fprintf ppf "%a ,%a" f h aux t
in
match l with
......@@ -2276,17 +2276,29 @@ module Tallying = struct
include Map.Make(struct
type t = (bool * Var.var)
let compare (b1,v1) (b2,v2) =
if b1 == b2 then
Var.compare v1 v2
if b1 == b2 then Var.compare v1 v2
else Pervasives.compare b1 b2
end)
(* m1 is a subset of m2 if for all elements (alpha,s) of
* m1 there is a correspoding element (alpha,t) in m2 such that
* s <= t . In this case m2 is a more restrictive constraint set
* then m1 *)
let subtype m1 m2 =
let c = compare Descr.compare m1 m2 in
if c = 0 then true
else
let m1,m2 = if c < 0 then m1,m2 else m2,m1 in
for_all (fun k1 t1 ->
exists (fun k2 t2 -> k1 == k2 && subtype t1 t2) m2
) m1
let print ppf m =
print_lst (fun ppf -> fun ((b,`Var v),s) ->
if b then
Format.fprintf ppf "(`$%s,%a)" v Print.print s
Format.fprintf ppf "(`$%s >= %a)" v Print.print s
else
Format.fprintf ppf "(%a,`$%s)" Print.print s v
Format.fprintf ppf "(%a >= `$%s)" Print.print s v
) ppf (bindings m);
end
......@@ -2321,6 +2333,7 @@ module Tallying = struct
include Set.Make(struct
type t = Descr.s M.t
let compare = M.compare Descr.compare
end)
let print ppf s = print_lst M.print ppf (elements s)
......@@ -2340,6 +2353,7 @@ module Tallying = struct
let print_m = M.print
let print_e = E.print
(* Inv : a map contains only on binding for each variable *)
let merge m1 m2 =
let f k v1 v2 = match (k,v1,v2) with
|(k,None,None) -> None
......@@ -2353,7 +2367,15 @@ module Tallying = struct
let sat = S.singleton M.empty
let unsat = S.empty
let cup = S.union
(* this is O(n^2) filter . Only more restritive constraints sets are kept *)
let cup x y =
let c = (S.cardinal x) - (S.cardinal y) in
let aux s1 s2 =
S.fold (fun m acc ->
if S.exists (M.subtype m) s2 then S.add m acc else acc
) s1 s2
in
if c <= 0 then aux x y else aux y x
(* cartesian product of two sets of contraints sets where each
* resulting constraint set is than merged *)
......
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