Commit 71ca75a5 authored by Pietro Abate's avatar Pietro Abate

Fix all problems with Tallying.merge

- all unit tests for Tallying.merge pass
- add few more functions to .ocamlinit
parent b4bd86bf
......@@ -19,3 +19,24 @@ let parse_typ s =
Types.descr nodepat
;;
type pp = P of vv * string | N of string * vv
and vv = V of string
let mk_pp = function
|P(V alpha,t) -> Tallying.CS.singleton (Tallying.Pos (`Var alpha,parse_typ t))
|N(t,V alpha) -> Tallying.CS.singleton (Tallying.Neg (parse_typ t,`Var alpha))
let mk_prod l =
List.fold_left (fun acc2 c ->
Tallying.CS.prod (mk_pp c) acc2
) Tallying.CS.sat l
let mk_union l1 l2 =
Tallying.CS.union (mk_prod l1) (mk_prod l2)
let mk_s ll =
List.fold_left (fun acc1 l ->
Tallying.CS.union (mk_prod l) acc1
) Tallying.CS.S.empty ll
......@@ -195,10 +195,11 @@ let norm_tests = [
"(`$A , Int) | (`$B , Bool))","(Int , (Int | Bool))", mk_s [
[P(V "A","Int");P(V "B","Int")]
];
(*
"(`$A1 -> `$B1) -> [ `$A1 ] -> [ `$B1 ]", "((Int -> Bool) | ((`$A \\ Int) -> (`$B \\ Int))) -> `$G", mk_s [
[P(V "A","Empty")]
];
*)
]
let test_norm =
......@@ -215,39 +216,43 @@ let test_norm =
;;
let merge_tests = [
[("`$A", "Empty");("`$B", "Empty")], Tallying.CS.prod (mk_pos ("A", "Empty")) (mk_pos ("B", "Empty"));
[("`$A", "Int | Bool");("Int","`$B");("`$B", "Empty")], Tallying.CS.unsat;
[("Bool","`$B"); ("`$B", "`$A"); ("`$A", "Empty")], Tallying.CS.unsat;
[("Bool","`$B"); ("Int","`$B"); ("`$B","`$A"); ("`$A", "Int | Bool")],
Tallying.CS.prod
(mk_neg ("`$B","A")) (
Tallying.CS.prod
(mk_pos ("A", "Int | Bool")) (
Tallying.CS.prod
(mk_neg ("Int | Bool","B"))
(mk_pos ("B","Int | Bool"))
)
);
[("`$A", "`$B")], mk_pos ("A","`$B");
[("`$B", "Empty")], mk_pos ("B","Empty");
[("`$A", "Int");("`$B", "Bool"); ("`$A", "Empty")],Tallying.CS.prod (mk_pos ("A", "Empty")) (mk_pos ("B", "Bool"));
]
"empty empty", mk_s [[P(V "A", "Empty");P(V "B", "Empty")]],
mk_s [
[P(V "A","Empty");P(V "B","Empty")]
];
"unsat 1", mk_s [[P(V "A", "Int | Bool");N("Int",V "B");P(V "B", "Empty")]], Tallying.CS.unsat;
"unsat 2", mk_s [[N("Bool",V "B"); N("`$B", V "A"); P(V "A", "Empty")]], Tallying.CS.unsat;
"quad", mk_s [[N("Bool | Int",V "B"); N("`$B",V "A"); P(V "A", "Int | Bool")]],
mk_s [
[N("`$B", V "A");P(V "A","Int | Bool");N("Int | Bool", V "B"); P(V "B","Int | Bool")]
];
"add one", mk_s [[N("`$B", V "A");P(V "A","Int | Bool")]],
mk_s [[N("`$B", V "A");P(V "A","Int | Bool");P(V "B","Int | Bool")]];
"A B", mk_s [[P(V "A", "`$B")]], mk_pp (P(V "A","`$B"));
"", mk_s [[P(V "B", "Empty")]], mk_pp (P(V "B","Empty"));
"", mk_s [[P(V "A", "Int");P(V "B", "Bool"); P(V "A", "Empty")]],
mk_s [
[P(V "A","Empty");P(V "B","Bool")]
]
];;
let test_merge =
let print_test l =
String.concat ";" (List.map (fun (s,t) -> Printf.sprintf " %s >= %s" s t) l)
in
"test tallying merge" >:::
List.map (fun (l,expected) ->
(print_test l) >:: (fun _ ->
let n = List.fold_left (fun acc (s,t) ->
let s = parse_typ s in
let t = parse_typ t in
Tallying.CS.prod acc (Tallying.norm(diff s t))) Tallying.CS.S.empty l
in
let result = Tallying.CS.S.fold (fun c acc ->
try Tallying.CS.union (Tallying.merge c) acc with Tallying.UnSatConstr -> acc
) n Tallying.CS.S.empty
List.map (fun (test,s,expected) ->
test >:: (fun _ ->
let result =
try
Tallying.CS.S.fold (fun c acc ->
Tallying.CS.union (Tallying.merge c) acc
) s Tallying.CS.S.empty
with Tallying.UnSatConstr -> Tallying.CS.unsat
in
let elem s = MSet.of_list (Tallying.CS.S.elements s) in
MSet.assert_equal (elem expected) (elem result)
......
......@@ -2403,9 +2403,9 @@ module Tallying = struct
end
let normatoms (t,_) = if Atoms.is_empty t then CS.sat else CS.unsat (* raise UnSatConstr *)
let normchars (t,_) = if Chars.is_empty t then CS.sat else CS.unsat (* raise UnSatConstr *)
let normints (t,_) = if Intervals.is_empty t then CS.sat else CS.unsat (* raise UnSatConstr *)
let normatoms (t,_) = if Atoms.is_empty t then CS.sat else CS.unsat
let normchars (t,_) = if Chars.is_empty t then CS.sat else CS.unsat
let normints (t,_) = if Intervals.is_empty t then CS.sat else CS.unsat
let single_aux constr (b,v,p,n) =
let aux f constr acc l =
......@@ -2467,15 +2467,15 @@ module Tallying = struct
|(_,[]) -> failwith "impossible3"
|_,_ -> failwith "impossible4"
(* norm generates a constraint set for the costraint t <= 0 *)
let rec norm ( (t,m) : (s * DescrSet.t)) =
Format.printf "Norm of %a\n" Print.print t;
if DescrSet.mem t m then CS.sat else begin
if DescrSet.mem t m || is_empty t then CS.sat else begin
let aux_base single norm_aux acc l =
List.fold_left (fun acc (pos,neg) ->
CS.prod acc (toplevel single norm_aux m (pos,neg))
) acc l
in
let accu = CS.sat in
let accu = CS.unsat 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
......@@ -2580,10 +2580,12 @@ module Tallying = struct
let t = CS.M.find (not b,v) m in
let x = if b then diff t s else diff s t in
if DescrSet.mem x mem then None
else
let c1 = CS.prod (CS.S.singleton m) (norm x) in
else begin
let n = let r = norm x in if CS.S.is_empty r then raise UnSatConstr else r in
let c1 = CS.prod (CS.S.singleton m) n in
let c2 = CS.S.fold (fun m1 acc -> CS.union acc (merge (m1,DescrSet.add x mem))) c1 CS.S.empty in
Some c2
end
with Not_found -> None
in
let mm =
......@@ -2652,7 +2654,7 @@ module Tallying = struct
aux (CS.E.empty,CS.E.empty) e
let tallying l =
let n = List.fold_left (fun acc (s,t) -> try CS.prod acc (norm(diff s t)) with UnSatConstr -> acc) CS.S.empty l in
let n = List.fold_left (fun acc (s,t) -> CS.prod acc (norm(diff s t))) CS.S.empty l in
if CS.S.is_empty n then raise UnSatConstr 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
if CS.ES.is_empty m then raise UnSatConstr else
......
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