Skip to content

GitLab

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

Fix multiple bugs in the function Tallying.norm

parent 410fcd0c
Hide whitespace changes
Inline Side-by-side
misc/custom.ml
View file @ c18b8b05
......@@ -189,5 +189,5 @@ module Var (X : T) = struct
let equal t1 t2 = (compare t1 t2) = 0
let dump ppf = function
|`Atm x -> X.dump ppf x
|`Var x -> String.dump ppf x
|`Var x -> Format.fprintf ppf "`$%a" String.dump x
end
tests/libtest/tallyingTest.ml
View file @ c18b8b05
......@@ -9,8 +9,23 @@ let parse_typ s =
Types.descr nodepat
;;
let cup = Types.Tallying.CS.S.cup
let cap = Types.Tallying.CS.cap
let singleton = Types.Tallying.CS.singleton
let norm_tests = [
"Int \\ (`$A | `$B)", [[(false,`Var "A",parse_typ "Int \\ `$B")]];
"Int \\ (`$A | `$B)", singleton (false,`Var "A",parse_typ "Int \\ `$B");
"(`$A -> Int) \\ (`$B -> `$B)",
cup
(singleton (true,`Var "B",parse_typ "Empty"))
(cap
(singleton (false , `Var "B",parse_typ "`$A"))
(singleton (false , `Var "B",parse_typ "Int"))
);
"`$B", singleton (true,`Var "B",parse_typ "Empty");
"`$B \\ `$A", singleton (false , `Var "B",parse_typ "`$A");
"Int \\ `$B", singleton (false , `Var "B",parse_typ "Int");
"(Int & Bool -> Int) \\ (`$A -> `$B)"
]
let test_norm =
......
types/boolVar.ml
View file @ c18b8b05
......@@ -42,6 +42,7 @@ sig
val cap : t -> t -> t
val diff : t -> t -> t
val atom : elem -> t
val neg_atom : elem -> t
(* vars a : return a bdd that is ( Any ^ Var a ) *)
val vars : Custom.var -> t
......@@ -54,7 +55,7 @@ sig
val is_empty : t -> bool
val print: string -> t -> (Format.formatter -> unit) list
val print: ?f:(Format.formatter -> elem -> unit) -> t -> (Format.formatter -> unit) list
val trivially_disjoint: t -> t -> bool
......@@ -189,10 +190,10 @@ struct
| `False -> ()
| _ -> b (); Format.fprintf ppf "@[~%a@] & @[(%a)@]" f x (print f) n)
let print a = function
| `True -> [ fun ppf -> Format.fprintf ppf "%s" a ]
| `False -> []
| c -> [ fun ppf -> print X.dump ppf c ]
let print ?(f=X.dump) = function
| `True -> [] (* [] a bdd cannot be of this type *)
| `False -> [ fun ppf -> Format.fprintf ppf "Empty" ]
| c -> [ fun ppf -> print f ppf c ]
(* return a list of pairs, where each pair holds the list
* of positive and negative elements on a branch *)
......
types/types.ml
View file @ c18b8b05
......@@ -1512,13 +1512,15 @@ struct
(empty, d) in
let add u = slot.def <- u :: slot.def in
if (non_empty seq) then
add (Regexp (decompile seq));
List.iter
(fun (t1,t2) -> add (Pair (prepare t1, prepare t2)))
(Product.get not_seq);
List.iter
(fun (t1,t2) ->
if (non_empty seq) then add (Regexp (decompile seq));
(* pairs *)
List.iter (fun (t1,t2) ->
add (Pair (prepare t1, prepare t2))
) (Product.get not_seq);
(* xml pairs *)
List.iter (fun (t1,t2) ->
try
let n = DescrPairMap.find (t1,t2) !named_xml in
add (Name n)
......@@ -1532,26 +1534,30 @@ struct
(fun (ta,tb) ->
add (Xml (tag, prepare ta, prepare tb)))
(Product.get t2);
)
((*Product.merge_same_2*) (Product.get ~kind:`XML not_seq));
List.iter
(fun (r,some,none) ->
) (Product.get ~kind:`XML not_seq);
(* records *)
List.iter (fun (r,some,none) ->
let r = LabelMap.map (fun (o,t) -> (o, prepare t)) r in
add (Record (r,some,none)))
(Record.get not_seq);
add (Record (r,some,none))
) (Record.get not_seq);
(match Chars.is_char (BoolChars.leafconj not_seq.chars) with
| Some c -> add (Char c)
| None ->
List.iter (fun x -> add (Atomic x)) (BoolChars.print "" not_seq.chars));
List.iter (fun x -> add (Atomic x)) (BoolIntervals.print "" not_seq.ints);
List.iter (fun x -> add (Atomic x)) (BoolAtoms.print "" not_seq.atoms);
List.iter (fun x -> add (Atomic x)) (BoolChars.print not_seq.chars));
List.iter (fun x -> add (Atomic x)) (BoolIntervals.print not_seq.ints);
List.iter (fun x -> add (Atomic x)) (BoolAtoms.print not_seq.atoms);
List.iter (fun x -> add (Atomic x)) (Abstract.print not_seq.abstract);
List.iter
(fun (p,n) ->
let aux (t,s) = prepare (descr t), prepare (descr s) in
let p = List.map aux p and n = List.map aux n in
add (Arrows (p,n)))
(Pair.get (BoolPair.leafconj not_seq.arrow));
(* arrows *)
List.iter (fun (p,n) ->
let aux (t,s) = prepare (descr t), prepare (descr s) in
let p = List.map aux p and n = List.map aux n in
add (Arrows (p,n))
) (Pair.get (BoolPair.leafconj not_seq.arrow));
if not_seq.absent then add (Atomic (fun ppf -> Format.fprintf ppf "#ABSENT"));
slot.def <- List.rev slot.def;
slot
......@@ -1663,14 +1669,13 @@ struct
| [] -> Format.fprintf ppf "Arrow"
| (t,s)::l ->
Format.fprintf ppf "%a" (do_print_arrow pri) (t,s);
List.iter
(fun (t,s) ->
Format.fprintf ppf " &@ %a" (do_print_arrow pri) (t,s)
) l);
List.iter
(fun (t,s) ->
List.iter (fun (t,s) ->
Format.fprintf ppf " &@ %a" (do_print_arrow pri) (t,s)
) l
);
List.iter (fun (t,s) ->
Format.fprintf ppf " \\@ %a" (do_print_arrow pri) (t,s)
) n
) n
and do_print_arrow pri ppf (t,s) =
if (pri = 3) then Format.fprintf ppf "(";
Format.fprintf ppf "%a -> %a"
......@@ -2198,14 +2203,23 @@ module Tallying = struct
module CS = struct
type key = (bool * Custom.var)
(* constraint set : map to store constraints of the form (alpha,t) or (t,alpha) *)
module M = Map.Make(struct
type t = key
let compare = Pervasives.compare
end)
(* Set of constraint sets *)
module S = Set.Make(struct
type t = s M.t
let compare = M.compare Pervasives.compare
type t = Descr.s M.t
let compare = M.compare Descr.compare
end)
(* equation set : (s < alpha < t) stored as ( alpha -> (s,t) ) *)
module E = Map.Make(struct
type t = Custom.var
let compare = Pervasives.compare
end)
type cset = S.t
......@@ -2218,18 +2232,48 @@ module Tallying = struct
|(k,None,None) -> None
|(k,Some v,None) -> Some v
|(k,None,Some v) -> Some v
|((true,v),Some x,Some y) -> Some (cup x y)
|((false,v),Some x,Some y) -> Some (cap x y)
|((true,v),Some x,Some y) -> Some (cap x y)
|((false,v),Some x,Some y) -> Some (cup x y)
in
M.merge f m1 m2
let print ppf s =
let print_lst f ppf l =
let rec aux ppf = function
|[] -> Format.fprintf ppf "@."
|[h] -> Format.fprintf ppf "%a@." f h
|h::t -> Format.fprintf ppf "%a ,%a" f h aux t
in
match l with
|[] -> Format.fprintf ppf "{}"
|_ -> Format.fprintf ppf "{ %a }" aux l
in
print_lst (fun ppf -> fun m ->
print_lst (fun ppf -> fun ((b,`Var v),s) ->
if b then
Format.fprintf ppf "(`$%s,%a)" v Print.print s
else
Format.fprintf ppf "(%a,`$%s)" Print.print s v
) ppf (M.bindings m);
) ppf (S.elements s)
let sat = S.singleton M.empty
let unsat = S.empty
let cup = S.union
let cap x y =
S.fold (fun m1 acc ->
S.fold (fun m2 acc1 -> S.add (merge m1 m2) acc1) y acc
) x S.empty
match S.is_empty x,S.is_empty y with
|true,true -> S.empty
|false,true -> x
|true,false -> y
|false,false ->
let s =
S.fold (fun m1 acc ->
S.fold (fun m2 acc1 -> S.add (merge m1 m2) acc1) y acc
) x S.empty
in
s
end
(* Correct ??? *)
......@@ -2237,49 +2281,65 @@ module Tallying = struct
let normchars (t,_) = if Chars.is_empty t then CS.sat else raise UnSatConstr
let normints (t,_) = if Intervals.is_empty t then CS.sat else raise UnSatConstr
let c_aux c atom acc l =
List.fold_left (fun acc ->
function
|`Var a -> c acc (atom (`Var a))
|`Atm a -> c acc (atom (`Atm a))
) acc l
let capatoms (pos,neg) =
let auxcap = c_aux BoolAtoms.cap BoolAtoms.atom BoolAtoms.full in
let auxcup = c_aux BoolAtoms.cup BoolAtoms.atom BoolAtoms.empty in
{empty with atoms = BoolAtoms.diff (auxcap pos) (auxcup neg) }
let capchars (pos,neg) =
let auxcap = c_aux BoolChars.cap BoolChars.atom BoolChars.full in
let auxcup = c_aux BoolChars.cup BoolChars.atom BoolChars.empty in
{empty with chars = BoolChars.diff (auxcap pos) (auxcup neg) }
let capints (pos,neg) =
let auxcap = c_aux BoolIntervals.cap BoolIntervals.atom BoolIntervals.full in
let auxcup = c_aux BoolIntervals.cup BoolIntervals.atom BoolIntervals.empty in
{empty with ints = BoolIntervals.diff (auxcap pos) (auxcup neg) }
let captimes (pos,neg) =
let auxcap = c_aux BoolPair.cap BoolPair.atom BoolPair.full in
let auxcup = c_aux BoolPair.cup BoolPair.atom BoolPair.empty in
{ empty with times = BoolPair.diff (auxcap pos) (auxcup neg) }
let caparrow (pos,neg) =
let auxcap = c_aux BoolPair.cap BoolPair.atom BoolPair.full in
let auxcup = c_aux BoolPair.cup BoolPair.atom BoolPair.empty in
{ empty with arrow = BoolPair.diff (auxcap pos) (auxcup neg) }
let single_aux constr (b,v,p,n) =
let aux f constr acc l =
List.fold_left (fun acc ->
function
|`Var a -> cap acc (f(vars a))
|`Atm a -> cap acc (f(constr a))
) acc l
in
let id = (fun x -> x) in
let t = cap (aux id constr any p) (aux neg constr any n) in
if b then neg t else t
let single_atoms = single_aux atom
let single_chars = single_aux char
let single_ints = single_aux interval
let single_times = single_aux (fun p -> { empty with times = BoolPair.atom (`Atm p) })
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 cap norm_rec mem (p,n) = match (p,n) with
|([],(`Var x)::neg) -> CS.singleton (false,`Var x,cap ([],neg))
|((`Var x)::pos,[]) -> CS.singleton (true,`Var x, cap (pos,[]))
let toplevel single norm_rec mem (p,n) = match (p,n) with
|([],(`Var x)::neg) ->
(
Format.printf "single 1 = %a\n" Print.print (single (false,x,[],neg));
CS.singleton (false,`Var x,single (false,x,p,n))
)
|((`Var x)::pos,[]) ->
Format.printf "single 2 = %a\n" Print.print (single (true,x,pos,[]));
CS.singleton (true ,`Var x,single (true,x,pos,[]))
|((`Var x)::pos, (`Var y)::neg) ->
(* XXX this compare must be changed *)
if Pervasives.compare (`Var x) (`Var y) < 0 then
CS.singleton (true,`Var x,cap (pos,n))
else CS.singleton (false, `Var y, cap (p,neg))
|(_, (`Var x)::neg) -> CS.singleton (false,`Var x,cap (p,neg))
|((`Var x)::pos, _) -> CS.singleton (true,`Var x, cap (pos,n))
(
Format.printf "single 3 = %a\n" Print.print (single (true,x,pos,n));
CS.singleton (true,`Var x,single (true,x,pos,n))
)
else
(
Format.printf "single 4 = %a\n" Print.print (single (false,y,p,neg));
CS.singleton (false, `Var y,single (false,y,p,neg))
)
|([`Atm a], (`Var x)::neg) ->
(
Format.printf "!! single 5 = %a\n" Print.print (single (false,x,p,neg));
CS.singleton (false,`Var x,single (false,x,p,neg))
)
|((`Var x)::pos, [`Atm _]) -> failwith "impossible5"
(*
Format.printf "!! single = %a\n" Print.print (single (pos,[],[],n));
CS.singleton (true ,`Var x,single (pos,[],[],n))
*)
|([`Atm t], []) -> norm_rec (t,mem)
|([],[`Atm t]) -> failwith "impossible0" (* norm_rec (t,mem) *)
|([],[]) -> failwith "impossible"
......@@ -2290,22 +2350,25 @@ module Tallying = struct
let rec norm ( (t,m) : (s * DescrSet.t)) =
if DescrSet.mem t m then CS.sat else begin
try
let aux_base cap norm_aux acc l =
let aux_base single norm_aux acc l =
List.fold_left (fun acc (pos,neg) ->
CS.cup acc (toplevel cap norm_aux m (pos,neg))
(*
Format.printf "top cap = %a V %a = %a\n" CS.print acc CS.print (toplevel single norm_aux m (pos,neg)) CS.print (CS.cap acc (toplevel single norm_aux m (pos,neg)));
*)
CS.cap acc (toplevel single norm_aux m (pos,neg))
) acc l
in
let accu = CS.sat in
let accu = aux_base capatoms normatoms accu (BoolAtoms.get t.atoms) in
let accu = aux_base capchars normchars accu (BoolChars.get t.chars) in
let accu = aux_base capints normints accu (BoolIntervals.get t.ints) in
let accu = aux_base captimes normpair accu (BoolPair.get t.times) 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_times normpair accu (BoolPair.get t.times) in
let accu = aux_base single_times normpair accu (BoolPair.get t.xml) in
(*
let accu = aux_base accu subpair (BoolPair.get d.xml) in
let accu = aux_base accu subrecord (BoolRec.get d.record) in
*)
let accu = aux_base caparrow normarrow accu (BoolPair.get t.arrow) in
CS.cap CS.sat accu
let accu = aux_base single_arrow normarrow accu (BoolPair.get t.arrow) in
accu
with UnSatConstr -> CS.unsat
end
......@@ -2314,12 +2377,15 @@ module Tallying = struct
* [t1] ^ [t2] ^ [t1 \ s1] ^ [t2 \ s2] ^
* [t1 \ s1 \ s1_1] ^ [t2 \ s2 \ s2_1 ] ^
* [t1 \ s1 \ s1_1 \ s1_2] ^ [t2 \ s2 \ s2_1 \ s2_2 ] ^ ...
* prod(p,n) = [t1] ^ [t2] ^ prod'(t1,t2,n)
* prod'(t1,t2,{s1,s2} v n) = [t1\s1] ^ prod'(t1\s1,t2,n) v
* [t2\s2] ^ prod'(t1,t2\s2,n)
* *)
and normpair ( (t,mem) : (BoolPair.s * DescrSet.t) ) =
let mem = DescrSet.add { empty with times = BoolPair.atom (`Atm t) } mem in
let norm_prod pos neg =
let rec aux (t1 : s) (t2 : s ) = function
|[] -> CS.sat
|[] -> CS.S.empty
|(s1,s2) :: rest ->
let z1 = diff t1 (descr s1) in
let z2 = diff t2 (descr s2) in
......@@ -2340,26 +2406,39 @@ module Tallying = struct
in
List.fold_left (fun acc (p,n) -> CS.cap acc (norm_prod p n)) CS.sat (Pair.get t)
(* *)
(* arrow(p,{t1 -> t2}) = [t1] ^ arrow'(t1,any \\ t2,p)
* arrow'(t1,acc,p) =
([t1\s1] ^ arrow'(t1\s1,acc,p)) v
([acc ^ {s2} \ t2] ^ arrow'(t1,acc ^ {s2},p))
P(Q v {a}) = {a} v P(Q) v {X v {a} | X \in P(Q) }
*)
and normarrow ((t,mem) : (BoolPair.s * DescrSet.t) ) =
let mem = DescrSet.add { empty with arrow = BoolPair.atom (`Atm t) } mem in
let rec norm_arrow pos neg =
match neg with
|[] -> CS.sat
|(t0,s0)::rest ->
let con1 = norm (descr t0, mem) in
let con2 = aux (descr t0) any (descr s0) pos in
let con0 = norm_arrow pos rest in
|[] -> CS.S.empty
|(t1,t2) :: n ->
Format.printf "t1 = %a\n" Print.print (descr t1);
let con1 = norm (descr t1, mem) in
Format.printf "neg con1 = %a\n" CS.print con1;
let con2 = aux (descr t1) (diff any (descr t2)) pos in
Format.printf "neg con2 = %a\n" CS.print con2;
let con0 = norm_arrow pos n in
CS.cup (CS.cup con1 con2) con0
and aux (t0 : s) ( acc : s ) (s0 : s) = function
|[] -> CS.sat
|(s1,s2) :: rest ->
let t01 = diff t0 (descr s1) in
let acc1 = cup acc (descr s2) in
let con1 = norm (t01, mem) in
let con2 = norm (diff acc1 s0, mem) in
let con10 = aux t01 acc s0 rest in
let con20 = aux t0 acc1 s0 rest in
and aux t1 acc = function
|[] -> CS.S.empty
|(s1,s2) :: p ->
let t1s1 = diff t1 (descr s1) in
Format.printf "t1 \\ s1 = %a\n" Print.print t1s1;
let acc1 = cap acc (descr s2) in
let con1 = norm (t1s1, mem) in
Format.printf "pos con1 = %a\n" CS.print con1;
Format.printf "- t2 ^ acc ^ s2 = %a\n" Print.print acc1;
let con2 = norm (acc1, mem) in
Format.printf "pos con2 = %a\n" CS.print con2;
let con10 = aux t1s1 acc p in
let con20 = aux t1 acc1 p in
let con11 = CS.cup con1 con10 in
let con22 = CS.cup con2 con20 in
CS.cap con11 con22
......@@ -2368,20 +2447,53 @@ module Tallying = struct
let norm t = norm (t,DescrSet.empty)
(*
let merge (c,mem) =
CS.M.foldi (fun acc -> function
|(true,v) -> fun s ->
try
let t = CS.M.find (false,v) in
let rec merge (cs,mem) =
CS.M.fold (fun (b,v) s acc -> match (b,v) with
|(true,v) ->
begin try
let t = CS.M.find (false,v) cs in
let x = diff s t in
if mem x mem then acc
if DescrSet.mem x mem then acc
else
S.cup acc (S.cap c (norm x))
let c1 = CS.cap (CS.S.singleton cs) (norm x) in
let c2 = CS.S.fold (fun m acc -> CS.cup acc (merge (m,DescrSet.add x mem))) c1 CS.sat in
CS.cap acc c2
with Not_found -> acc end
|(false,v) -> acc
) cs CS.sat
with Not_found -> acc
|
) S.sat c
*)
let merge c = merge (c,DescrSet.empty)
(*
let solve cs =
CS.M.fold (fun (b,v) s acc -> match (b,v) with
|(true,v) ->
try
let t = CS.M.find (false,v) cs in
let b = fresh () in
CS.E.add v ((cup s b) cap t) acc
with Not_found ->
let b = fresh () in
CS.E.add v (cup s b)
|(false,v) ->
try
let t = CS.M.find (true,v) cs in
let b = fresh () in
CS.E.add v ((cup t b) cap s) acc
with Not_found ->
let b = fresh () in
CS.E.add v (cap s b)
) cs CS.E.empty
let unify e =
let aux acc e =
if CS.E.is_empty then []
else
let (a,t) = CS.E.pop e in
let e1 = CS.E.remove (a,t) e in
let x = fresh () in
(* replace in e1 all occurrences of a by ... *)
aux (t,a,x)::acc (subst e1 t a x)
*)
end
types/types.mli
View file @ c18b8b05
......@@ -355,6 +355,7 @@ module Tallying : sig
module M : Map.S with type key = key
module S : Set.S with type elt = t M.t
type cset = S.t
val print : Format.formatter -> S.t -> unit
val merge : S.elt -> S.elt -> S.elt
val singleton : constr -> cset
val sat : cset
......@@ -364,5 +365,7 @@ module Tallying : sig
end
val norm : t -> CS.cset
val merge : CS.S.elt -> CS.cset
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