Commit 6a67e7bc authored by Pietro Abate's avatar Pietro Abate

Fix bug caused by wrong memoization strategy

parent 885bd4fb
......@@ -158,12 +158,11 @@ let norm_tests = [
];
"(Int -> Int) | (Bool -> Bool)", "(`$A -> `$B)", mk_s [
[P(V "A","Empty")];
(* All these are subsumed as less general then (A <= 0)
[P(V "A","Empty")];
(* All these are subsumed as less general then (A <= 0) *)
[P(V "A","Empty");N("Int",V "B")];
[P(V "A","Empty");N("Bool",V "B")];
[P(V "A","Empty");N("Int | Bool",V "B")]
*)
];
"(`$A -> `$B)", "(Int -> Int) | (Bool -> Bool)", mk_s [
......@@ -200,11 +199,12 @@ let norm_tests = [
];
*)
"Int -> Bool", "`$A", mk_s [[N("Int -> Bool",V "A")]];
"((`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))",Tallying.CS.sat;
"Bool -> Bool","Int -> `$A", Tallying.CS.unsat;
"Int", "Bool", Tallying.CS.unsat;
"Int -> Bool", "`$A", mk_s [[N("Int -> Bool",V "A")]];
"Int", "Empty", Tallying.CS.unsat;
"[] -> []","Int -> `$A",Tallying.CS.unsat;
"((`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))",Tallying.CS.sat;
]
let test_norm =
......
......@@ -13,7 +13,7 @@ let to_string pp t =
Format.fprintf Format.str_formatter "%a@." pp t;
Format.flush_str_formatter ()
;;
(*
let variance_test = [
"`$A -> `$B", [("A",`Covariant);("B",`ContraVariant)];
]
......@@ -27,6 +27,7 @@ let test_variance =
)
) set_op_tests
;;
*)
let set_op_tests = [
"Int & `$B", "`$B & Int";
......@@ -66,7 +67,7 @@ let test_substitution =
let v = Var.mk v in
let s = parse_typ s in
let expected = parse_typ expected in
let result = Types.subst t (v,s) in
let result = Types.Positive.substitute t (v,s) in
assert_equal ~cmp:Types.equiv ~printer:(fun t ->
Format.sprintf "dump = %s\nrepr = %s\n" (to_string Types.dump t) (to_string Types.Print.print t)
) expected result
......@@ -78,7 +79,7 @@ let rec_subst_tests = [
"`$A", "A", "Empty";
"`$A", "B", "`$A";
"`$A | Int", "A", "X where X = (X | Int)";
"`$A | `$B | Int", "A", "X where X = X | `$B | Int";
"`$A | `$B | Int", "A", "X where X = (X | `$B | Int )";
"`$A -> `$B", "A", "X where X = X -> `$B";
"Bool -> `$B", "A", "Bool -> `$B";
"(`$A , `$B)", "A", "X where X = (X, `$B)";
......@@ -92,7 +93,7 @@ let test_rec_subtitutions =
let t = parse_typ t in
let v = Var.mk v in
let expected = parse_typ expected in
let result = Types.Positive.substitute t v in
let result = Types.Positive.substituterec t v in
assert_equal ~cmp:Types.equiv ~printer:(fun t ->
Format.sprintf "dump = %s\nrepr = %s\n" (to_string Types.dump t) (to_string Types.Print.print t)
) expected result
......
......@@ -210,7 +210,7 @@ struct
let pp_print = print X.dump
let print ?(f=X.dump) = function
| `True -> [] (* [] a bdd cannot be of this type *)
| `True -> assert false (* [] a bdd cannot be of this type *)
| `False -> [ fun ppf -> Format.fprintf ppf "Empty" ]
| c -> [ fun ppf -> print f ppf c ]
......@@ -221,7 +221,6 @@ struct
| `True -> (List.rev pos, List.rev neg) :: accu
| `False -> accu
| `Split (_,x, p,i,n) ->
(*OPT: can avoid creating this list cell when pos or neg =`False *)
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
......
......@@ -2609,21 +2609,20 @@ module Tallying = struct
(* norm generates a constraint set for the costraint t <= 0 *)
let rec norm (t,mem) =
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 =
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
accu
(* if is_var t then XXX else *)
(* XXX if there is only one variable then is it A <= 0 or 1 <= A *)
if is_empty t then CS.sat else (* if it empty then it is sat *)
if DescrSet.mem t mem then CS.sat else begin (* if we already evaluated it, it is sat *)
let mem = DescrSet.add t mem in
let aux single norm_aux acc l = big_prod (toplevel single norm_aux mem) acc l in
let acc = aux single_atoms normatoms CS.sat (BoolAtoms.get t.atoms) in
let acc = aux single_chars normchars acc (BoolChars.get t.chars) in
let acc = aux single_ints normints acc (BoolIntervals.get t.ints) in
let acc = aux single_arrow normarrow acc (BoolPair.get t.arrow) in
let acc = aux single_times normpair acc (BoolPair.get t.times) in
let acc = aux single_xml normpair acc (BoolPair.get t.xml) in
aux single_record normrec acc (BoolRec.get t.record)
end
(* (t1,t2) = intersection of all (fst pos,snd pos) \in P
......@@ -2694,6 +2693,7 @@ module Tallying = struct
P(Q v {a}) = {a} v P(Q) v {X v {a} | X \in P(Q) }
*)
(*
and normarrow (t,mem) =
let rec norm_arrow pos neg =
match neg with
......@@ -2717,12 +2717,38 @@ module Tallying = struct
CS.prod con11 con22
in
big_prod norm_arrow CS.sat (Pair.get t)
*)
and normarrow (t,mem) =
let rec norm_arrow pos neg =
match neg with
|[] -> CS.unsat
|(t1,t2)::n ->
let con1 = norm (descr t1, mem) in
let con2 = aux (descr t1) any (descr t2) pos in
let con0 = norm_arrow pos n in
CS.union (CS.union con1 con2) con0
and aux t1 acc t2 p =
match p with
|[] -> CS.unsat
|(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 (diff acc1 t2, mem) in
let con10 = aux t1s1 acc t2 p in
let con20 = aux t1 acc1 t2 p in
let con11 = CS.union con1 con10 in
let con22 = CS.union con2 con20 in
CS.prod con11 con22
in
big_prod norm_arrow CS.sat (Pair.get t)
let memo_norm = DescrHash.create 17
let norm t =
try DescrHash.find memo_norm t
with Not_found -> begin
let res = norm (t,DescrHash.create 17) in
let res = norm (t,DescrSet.empty) in
DescrHash.add memo_norm t res; res
end
......
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