Commit 74afa407 authored by Pietro Abate's avatar Pietro Abate
Browse files

After a few iterations with Kim

parent 94b6c4a7
......@@ -142,6 +142,18 @@ let test_constraints =
(* ^ => & -- v => | *)
let norm_tests () = [
"Int", "Empty", Tallying.CS.unsat;
"(Int,Int)", "Empty", Tallying.CS.unsat;
"Int -> Int", "Empty" , Tallying.CS.unsat;
"Bool -> Bool","Int -> `$A", Tallying.CS.unsat;
"Int", "Bool", Tallying.CS.unsat;
"Int", "Empty", Tallying.CS.unsat;
"[] -> []","Int -> `$A", Tallying.CS.unsat;
"Any", "Empty", Tallying.CS.unsat;
"Empty", "Empty", Tallying.CS.sat;
"(`$A -> Bool)", "(`$B -> `$B)", mk_s [
[P(V "B","Empty")];
[N("`$B",V "A");N("Bool",V "B")]
......@@ -201,10 +213,6 @@ 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", "Empty", Tallying.CS.unsat;
"[] -> []","Int -> `$A",Tallying.CS.unsat;
"((`$A , Int) | (`$B , Bool))","(Int , (Int | Bool))", mk_s [
[P(V "A","Int");P(V "B","Int")]
......@@ -325,7 +333,10 @@ let test_tallying =
List.iter (fun sigma ->
let s_sigma = Tallying.apply_subst s sigma in
let t_sigma = Tallying.apply_subst t sigma in
assert_equal (Types.subtype s_sigma t_sigma) true
assert_equal ~pp_diff:(fun fmt _ ->
Format.fprintf fmt "s @ sigma_i = %a\n" Types.Print.print s_sigma;
Format.fprintf fmt "t @ sigma_i = %a\n" Types.Print.print t_sigma
) (Types.subtype s_sigma t_sigma) true
) result
) l
(*
......
......@@ -29,6 +29,49 @@ let test_variance =
;;
*)
let tlv_tests = [
"`$A", Types.is_var, true;
"Int", Types.is_var, false;
"Empty", Types.is_var, false;
"Any", Types.is_var, false;
"`$A & Int", Types.is_var, false;
"`$A & Any", Types.is_var, true;
"`$A | Int", Types.is_var, false;
"(`$A,Int)", Types.is_var, false;
"Int", Types.no_var, true;
"Any", Types.no_var, true;
"Empty", Types.no_var, true;
"`A", Types.no_var, true;
"`$A", Types.no_var, false;
"`$A & Int", Types.no_var, false;
"`$A | Int", Types.no_var, false;
"(`$A,Int)", Types.no_var, false;
"(Char,Int)", Types.no_var, true;
"Int", Types.has_tlv, false;
"Any", Types.has_tlv, false;
"Empty", Types.has_tlv, false;
"`A", Types.has_tlv, false;
"`$A", Types.has_tlv, true;
"`$A & Int", Types.has_tlv, true;
"`$A | Int", Types.has_tlv, true;
"(`$A,Int)", Types.has_tlv, false;
"`$B | (`$A,Int)", Types.has_tlv, false;
"`$A | (Char,Int)", Types.has_tlv, false;
]
let test_tlv_operations =
"test TLV operations" >:::
List.map (fun (t,f,e) ->
(Printf.sprintf "test %s " t) >:: (fun _ ->
let t = parse_typ t in
assert_equal ~pp_diff:(fun fmt _ -> Types.Print.print fmt t) (f t) e
)
) tlv_tests
;;
let set_op_tests = [
"Int & `$B", "`$B & Int";
"Int | `$B", "`$B | Int";
......@@ -233,6 +276,7 @@ let all =
test_subtype;
test_substitution;
test_rec_subtitutions;
test_tlv_operations;
(* test_witness; *)
]
......
......@@ -187,7 +187,6 @@ module TLV = struct
let no_variables x = (x.b == false) && (Var.Set.cardinal x.f = 0) && (Set.cardinal x.s = 0)
let no_toplevel x = (Set.cardinal x.s = 0)
let has_toplevel x = Set.cardinal x.s > 0
let print ppf x = if x.b then Set.print ";" ppf x.s
......@@ -452,6 +451,8 @@ let var a = {
let is_var t = TLV.is_single t.toplvars
let no_var t = TLV.no_variables t.toplvars
let has_tlv t = TLV.has_toplevel t.toplvars
let all_vars t = t.toplvars.TLV.f
(* XXX this function could be potentially costly. There should be
......@@ -1623,7 +1624,6 @@ struct
let add u = slot.def <- u :: slot.def in
(* variables are printed if displayvars OR if x is not a toplevel variable *)
let prepare_boolvar displayvars displayatoms get is_full print tlv bdd =
List.iter (fun (p,n) ->
let l1 =
......@@ -1649,12 +1649,38 @@ struct
|l -> add (Intersection (alloc (List.rev l)))
) (get bdd)
in
(*
(* variables are printed if displayvars OR if x is not a toplevel variable *)
let prepare_boolvar displayvars displayatoms get is_full print tlv bdd =
List.iter (fun (p,n) ->
let pp pol l =
List.fold_left (fun acc -> function
|(`Var v) as x ->
if displayvars || not(TLV.mem (x,pol) tlv) then
(Atomic (fun ppf -> Format.fprintf ppf "%s%a" (if pol then "" else "~ ") Var.print x))::acc
else acc
|`Atm bdd when is_full bdd ->
if not(displayvars) then
(print bdd) @ acc
else acc
|`Atm bdd ->
if pol then
if displayatoms then (print bdd) @ acc else acc
else
assert false
) [] l
in
match (pp p)@(pp n) with
|[] -> ()
|l -> add (Intersection (alloc (List.rev l)))
) (get bdd)
in
*)
if (non_empty seq) then add (Regexp (decompile seq));
let displayatoms = true in
let displayvars = TLV.has_toplevel not_seq.toplvars in
let bool = Atoms.cup (Atoms.atom (Atoms.V.mk_ascii "false")) (Atoms.atom (Atoms.V.mk_ascii "true")) in
(* base types *)
prepare_boolvar displayvars displayatoms BoolIntervals.get (Intervals.equal Intervals.full) (fun bdd ->
......@@ -1669,6 +1695,11 @@ struct
| None -> List.map (fun x -> (Atomic x)) (Chars.print bdd)
) not_seq.toplvars not_seq.chars;
let bool =
Atoms.cup
(Atoms.atom (Atoms.V.mk_ascii "false"))
(Atoms.atom (Atoms.V.mk_ascii "true"))
in
prepare_boolvar displayvars displayatoms BoolAtoms.get (Atoms.equal Atoms.full) (fun bdd ->
if Atoms.equal bool bdd then [Atomic (fun ppf -> Format.fprintf ppf "Bool")]
else List.map (fun x -> (Atomic x)) (Atoms.print bdd)
......@@ -2586,7 +2617,8 @@ module Tallying = struct
type m = Descr.s M.t
type e = Descr.s E.t
type es = ES.t
type sl = (Var.var * t) list list
type sigma = (Var.var * t) list
type sl = sigma list
let singleton = function
|Pos (v,s) -> S.singleton (M.singleton (true,v) s)
......@@ -2648,7 +2680,7 @@ module Tallying = struct
(* cartesian product of two sets of contraints sets where each
* resulting constraint set is than merged . If one of the two
* sets is empty the product is empty *)
* sets is empty/unsat the product is empty *)
let prod x y =
if S.is_empty x || S.is_empty y then S.empty
else
......@@ -2720,42 +2752,47 @@ module Tallying = struct
let big_prod f acc l =
List.fold_left (fun acc (pos,neg) ->
if CS.S.is_empty acc then acc else
(* 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 we already evaluated it, it is sat *)
if DescrSet.mem t mem then CS.sat else begin
(* if there is only one variable then is it A <= 0 or 1 <= A *)
(*
if is_var t then
let (v,p) = TLV.max t.toplvars in
let s = if p then (Pos (v,empty)) else (Neg (any,v)) in
CS.singleton s
else
(* if there are no vars, and it is not empty then unsat else sat *)
if no_var t then if is_empty t then CS.sat else CS.unsat
else
*)
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)
if DescrSet.mem t mem then begin
Format.printf "Sat for type %a\n%!" Print.print t;
CS.sat end else begin
(*
if is_empty t then CS.sat
(* if there is only one variable then is it A <= 0 or 1 <= A *)
else if is_var t then
let (v,p) = TLV.max t.toplvars in
let s = if p then (Pos (v,empty)) else (Neg (any,v)) in
CS.singleton s
(* if there are no vars, and it is not empty then unsat *)
else if no_var t then CS.unsat
else *) begin
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
(* XXX normrec is not tested at all !!! *)
aux single_record normrec acc (BoolRec.get t.record)
end
end
(* (t1,t2) = intersection of all (fst pos,snd pos) \in P
* (s1,s2) \in N
* [t1] ^ [t2] ^ [t1 \ s1] ^ [t2 \ s2] ^
* [t1] v [t2] v ( [t1 \ s1] ^ [t2 \ s2] ^
* [t1 \ s1 \ s1_1] ^ [t2 \ s2 \ s2_1 ] ^
* [t1 \ s1 \ s1_1 \ s1_2] ^ [t2 \ s2 \ s2_1 \ s2_2 ] ^ ...
* [t1 \ s1 \ s1_1 \ s1_2] ^ [t2 \ s2 \ s2_1 \ s2_2 ] ^ ... )
*
* prod(p,n) = [t1] v [t2] v prod'(t1,t2,n)
* prod'(t1,t2,{s1,s2} v n) = ([t1\s1] v prod'(t1\s1,t2,n)) ^
......@@ -2764,23 +2801,33 @@ module Tallying = struct
and normpair (t,mem) =
let norm_prod pos neg =
let rec aux t1 t2 = function
|[] -> CS.sat
|(s1,s2) :: rest ->
|[] -> CS.unsat
|(s1,s2) :: rest -> begin
let z1 = diff t1 (descr s1) in
let z2 = diff t2 (descr s2) in
let con1 = norm (z1, mem) in
Format.printf "*1norm[%a \\ %a] = %a\n" Print.print t1 Print.print (descr s1) CS.pp_s con1;
let con2 = norm (z2, mem) in
Format.printf "*2norm[%a \\ %a] = %a\n" Print.print t2 Print.print (descr s2) CS.pp_s con2;
let con10 = aux z1 t2 rest in
Format.printf "norm[con10] = %a\n" CS.pp_s con10;
let con20 = aux t1 z2 rest in
Format.printf "norm[con20] = %a\n" CS.pp_s con20;
let con11 = CS.union con1 con10 in
Format.printf "norm[con11] = %a\n" CS.pp_s con11;
let con22 = CS.union con2 con20 in
Format.printf "norm[con22] = %a\n" CS.pp_s con22;
CS.prod con11 con22
end
in
(* cap_product return the intersection of all (fst pos,snd pos) *)
let (t1,t2) = cap_product any any pos in
let con1 = norm (t1, mem) in
Format.printf "3norm[%a] = %a\n" Print.print t1 CS.pp_s con1;
let con2 = norm (t2, mem) in
Format.printf "4norm[%a] = %a\n" Print.print t2 CS.pp_s con2;
let con0 = aux t1 t2 neg in
Format.printf "norm[con0] = %a\n" CS.pp_s con0;
CS.union (CS.union con1 con2) con0
in
big_prod norm_prod CS.sat (Pair.get t)
......@@ -2985,7 +3032,9 @@ module Tallying = struct
exception Step2Fail
let tallying l =
let n = List.fold_left (fun acc (s,t) -> CS.prod acc (norm(diff s t))) CS.sat l in
let n = List.fold_left (fun acc (s,t) ->
let d = diff s t in
(* if is_empty d then CS.sat else *) CS.prod acc (norm d)) CS.sat l in
Format.printf "Norm : %a\n" CS.pp_s n;
if CS.S.is_empty n then raise Step1Fail else
let m = CS.S.fold (fun c acc -> try CS.ES.union (solve (merge c)) acc with UnSatConstr -> acc) n CS.ES.empty in
......
......@@ -110,8 +110,9 @@ val neg : t -> t
val empty : t
val any : t
val no_var : t -> bool
val is_var : t -> bool
val no_var : t -> bool
val is_var : t -> bool
val has_tlv : t -> bool
val any_node : Node.t
val empty_node : Node.t
......@@ -387,7 +388,8 @@ module Tallying : sig
type m = t M.t
type e = t E.t
type es = ES.t
type sl = (Var.var * t) list list
type sigma = (Var.var * t) list
type sl = sigma list
val pp_s : Format.formatter -> s -> unit
val pp_m : Format.formatter -> m -> unit
......@@ -407,7 +409,7 @@ module Tallying : sig
val solve : CS.s -> CS.es
val unify : CS.e -> CS.e
val tallying : (t * t) list -> CS.sl
val apply_subst : t -> (Var.var * t) list -> t
val apply_subst : t -> CS.sigma -> t
end
val apply : t -> t -> Tallying.CS.sl
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