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

Recursively check in the global normalisation hash table whether the

type has already been normalized. Without this patch, in the following usage:

norm(T1, delta)
norm(<a>[ T1 ], delta)

the fact that T1 has already been normalized against some delta is not taken into
account while normalizin <a>[T1].
parent 7932c071
...@@ -3233,55 +3233,60 @@ module Tallying = struct ...@@ -3233,55 +3233,60 @@ module Tallying = struct
module NormMemoHash = Hashtbl.Make(Custom.Pair(Descr)(Var.Set)) module NormMemoHash = Hashtbl.Make(Custom.Pair(Descr)(Var.Set))
let memo_norm = NormMemoHash.create 17
let rec norm (t,delta,mem) = let rec norm (t,delta,mem) =
if is_empty t then CS.sat try
else (* If we find it in the global hashtable, we are finished *)
try NormMemoHash.find memo_norm (t, delta)
let finished, cst = NormMemoHash.find mem (t, delta) in with
if finished then cst else CS.sat Not_found ->
with try
Not_found -> let finished, cst = NormMemoHash.find mem (t, delta) in
begin if finished then cst else CS.sat
let res = with
if is_var t then Not_found ->
begin begin
let res =
(* base cases *)
if is_empty t then CS.sat (* empty type is sat *)
else if no_var t then CS.unsat (* if the type has no variable and is not empty, unsat *)
else if is_var t then (* a single top_level variable *)
begin
(* if there is only one variable then is it A <= 0 or 1 <= A *) (* if there is only one variable then is it A <= 0 or 1 <= A *)
let (v,p) = extract_variable t in let (v,p) = extract_variable t in
if Var.Set.mem v delta then CS.unsat if Var.Set.mem v delta then CS.unsat (* if it is monomorphic, unsat *)
else else
let s = if p then (Pos (v,empty)) else (Neg (any,v)) in (* otherwise, create a single constraint according to its polarity *)
CS.singleton s let s = if p then (Pos (v,empty)) else (Neg (any,v)) in
(* if there are no vars, and it is not empty then unsat *) CS.singleton s
end end
else if no_var t then CS.unsat else begin (* type is not empty and is not a variable *)
else begin let mem = NormMemoHash.add mem (t,delta) (false, CS.sat); mem in
let mem = NormMemoHash.add mem (t,delta) (false, CS.sat); mem in let aux single norm_aux acc l =
let aux single norm_aux acc l = big_prod delta (toplevel delta single norm_aux mem) acc l
big_prod delta (toplevel delta single norm_aux mem) acc l in
in let acc = aux single_atoms normatoms CS.sat (BoolAtoms.get t.atoms) 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_chars normchars acc (BoolChars.get t.chars) in let acc = aux single_ints normints acc (BoolIntervals.get t.ints) in
let acc = aux single_ints normints acc (BoolIntervals.get t.ints) in let acc = aux single_times normpair acc (BoolPair.get t.times) 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
let acc = aux single_xml normpair acc (BoolPair.get t.xml) in let acc = aux single_arrow normarrow acc (BoolPair.get t.arrow) in
let acc = aux single_arrow normarrow acc (BoolPair.get t.arrow) in let acc = aux single_abstract normabstract acc (BoolAbstracts.get t.abstract) in
let acc = aux single_abstract normabstract acc (BoolAbstracts.get t.abstract) in
(* XXX normrec is not tested at all !!! *) (* XXX normrec is not tested at all !!! *)
let acc = aux single_record normrec acc (BoolRec.get t.record) in let acc = aux single_record normrec acc (BoolRec.get t.record) in
let acc = (* Simplify the constraints on that type *) let acc = (* Simplify the constraints on that type *)
CS.S.filter CS.S.filter
(fun m -> CS.M.for_all (fun v (s, t) -> not (Var.Set.mem v delta) || (fun m -> CS.M.for_all (fun v (s, t) -> not (Var.Set.mem v delta) ||
let x = var v in subtype s x && subtype x t let x = var v in subtype s x && subtype x t
) m) ) m)
acc acc
in in
acc acc
end end
in in
NormMemoHash.replace mem (t, delta) (true,res); res NormMemoHash.replace mem (t, delta) (true,res); res
end end
(* Format.printf "Normalizing %a yields %a\n%!" Print.pp_type t CS.pp_s res; *)
(* (t1,t2) = intersection of all (fst pos,snd pos) \in P (* (t1,t2) = intersection of all (fst pos,snd pos) \in P
* (s1,s2) \in N * (s1,s2) \in N
...@@ -3376,7 +3381,6 @@ module Tallying = struct ...@@ -3376,7 +3381,6 @@ module Tallying = struct
in in
big_prod delta norm_arrow CS.sat (Pair.get t) big_prod delta norm_arrow CS.sat (Pair.get t)
let memo_norm = NormMemoHash.create 17
let norm delta t = let norm delta t =
......
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