...
 
Commits (2)
  • Sylvain Dailler's avatar
  • Sylvain Dailler's avatar
    [WIP] TEST. Not intended to be merged. · 8511e56d
    Sylvain Dailler authored
    The idea is to change the pairing so that it is better when only axioms
    change. In the extreme case, the goal is unchanged.
    The first idea is to add a separator when printing the shape so that goal
    and hypothesis are separated.
    When pairing shape, the first sorting is done only on goals. Then, we try
    to add to the PQ all the elements that have the same goal shape. I say
    that some goals that are very close would not be directly next to each
    other with the current algorithm: we give them a chance to evaluate their
    measure (lcp) before elements are withdrawn.
    Then, we also tried to change lcp in case the goal is slightly changed but
    an hypothesis is changed too. If the goal change slightly in the same way
    for a lot of tasks, currently the (lcp Old New) value is always the same.
    The idea is to transform the lcp into a lcp_list which compare the goal
    like lcp and then compare each hypothesis like lcp. So, we hope that when
    the goal differs the same for two New goals compared to one Old, the right
    one will be taken because it differs the same way on the hypothesis.
    8511e56d
use int.Int
constant x : int
axiom h : x = 0 \/ x <> 0
axiom k : x + x + x + x + x = 0
goal g : x = 0 \/ x <> 0
axiom h : x = 1 \/ x <> 0
axiom k : x + x + x = 0
(* TODO work when both changing x = 0 to x = 1 everywhere or when removing x + x ... in k *)
goal g : x = 1 \/ x <> 0
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
<why3session shape_version="7">
<file proved="true">
<path name=".."/>
<path name="276_shape.mlw"/>
......
......@@ -16,6 +16,9 @@ open Number
(* explanations *)
(*******************************)
(* TODO replace this *)
let tag_hyp = '@'
let expl_prefixes = ref ["expl:"]
let arg_extra_expl_prefix =
......@@ -222,9 +225,9 @@ let debug = Debug.register_info_flag "session_pairing"
~desc:"Print@ debugging@ messages@ about@ reconstruction@ of@ \
session@ trees@ after@ modification@ of@ source@ files."
let current_shape_version = 6
let current_shape_version = 7
type shape_version = SV1 | SV2 | SV3 | SV4 | SV5
type shape_version = SV1 | SV2 | SV3 | SV4 | SV5 | SV6
module Shape = struct
......@@ -256,6 +259,8 @@ let tag_true = 't'
let tag_var = 'V'
let tag_wild = 'w'
let tag_as = 'z'
let tag_infix = "X"
let tag_mixfix = "Y"
exception ShapeTooLong
......@@ -272,7 +277,18 @@ let pushc c =
Buffer.add_char shape_buffer c;
check ()
let ident h id =
(* Remove infix and mixfix. (prefix should be rare enough) *)
let remove_infix s =
try
let s' = Strings.remove_prefix "infix " s in
tag_infix ^ s'
with Not_found ->
try
let s' = Strings.remove_prefix "mixfix " s in
tag_mixfix ^ s'
with Not_found -> s
let ident_v5 h id =
let x =
try Ident.Mid.find id !h
with Not_found ->
......@@ -281,6 +297,15 @@ let ident h id =
in
push x
let ident_v6 h id =
let x =
try Ident.Mid.find id !h
with Not_found ->
let s = remove_infix id.Ident.id_string in
h := Ident.Mid.add id s !h; s
in
push x
let vs_rename_alpha c h vs =
incr c;
let s = string_of_int !c in
......@@ -304,56 +329,58 @@ let const_shape v c =
let fmt = Format.formatter_of_buffer shape_buffer in
begin match v with
| SV1 | SV2 | SV3 | SV4 -> Common.const_v1 fmt c
| SV5 -> Common.const_v2 fmt c
| SV5 | SV6 -> Common.const_v2 fmt c
end;
Format.pp_print_flush fmt ();
check ()
let rec pat_shape c m p : 'a =
let rec pat_shape ~version c m p : 'a =
match p.pat_node with
| Pwild -> pushc tag_wild
| Pvar _ -> pushc tag_var
| Papp (f, l) ->
pushc tag_app;
ident m f.ls_name;
List.iter (pat_shape c m) l
| Pas (p, _) -> pat_shape c m p; pushc tag_as
(if version = SV6 then ident_v6 m f.ls_name
else ident_v5 m f.ls_name);
List.iter (pat_shape ~version c m) l
| Pas (p, _) -> pat_shape ~version c m p; pushc tag_as
| Por (p, q) ->
pat_shape c m q; pushc tag_or; pat_shape c m p
pat_shape ~version c m q; pushc tag_or; pat_shape ~version c m p
let rec t_shape ~version c m t =
let fn = t_shape ~version c m in
match t.t_node with
| Tconst c -> pushc tag_const; const_shape version c
| Tvar v -> pushc tag_var; ident m v.vs_name
| Tvar v -> pushc tag_var;
if version = SV6 then ident_v6 m v.vs_name else ident_v5 m v.vs_name
| Tapp (s,l) ->
pushc tag_app;
ident m s.ls_name;
if version = SV6 then ident_v6 m s.ls_name else ident_v5 m s.ls_name;
List.iter fn l
| Tif (f,t1,t2) ->
begin match version with
| SV1 | SV2 -> pushc tag_if; fn f; fn t1; fn t2
| SV3 | SV4 | SV5 -> pushc tag_if; fn t2; fn t1; fn f
| SV3 | SV4 | SV5 | SV6 -> pushc tag_if; fn t2; fn t1; fn f
end
| Tcase (t1,bl) ->
let br_shape b =
let p,t2 = t_open_branch b in
match version with
| SV1 | SV2 ->
pat_shape c m p;
pat_shape ~version c m p;
pat_rename_alpha c m p;
t_shape ~version c m t2
| SV3 | SV4 | SV5 ->
| SV3 | SV4 | SV5 | SV6 ->
pat_rename_alpha c m p;
t_shape ~version c m t2;
pat_shape c m p
pat_shape ~version c m p
in
begin match version with
| SV1 | SV2 ->
pushc tag_case;
fn t1;
List.iter br_shape bl
| SV3 | SV4 | SV5 ->
| SV3 | SV4 | SV5 | SV6 ->
pushc tag_case;
List.iter br_shape bl;
fn t1
......@@ -395,14 +422,14 @@ let rec t_shape ~version c m t =
match version with
| SV1 ->
pushc tag_let; fn t1; t_shape ~version c m t2
| SV2 | SV3 | SV4 | SV5 ->
| SV2 | SV3 | SV4 | SV5 | SV6 ->
(* t2 first, intentionally *)
t_shape ~version c m t2; pushc tag_let; fn t1
end
| Tnot f ->
begin match version with
| SV1 | SV2 -> fn f; pushc tag_not
| SV3 | SV4 | SV5 -> pushc tag_not; fn f
| SV3 | SV4 | SV5 | SV6 -> pushc tag_not; fn f
end
| Ttrue -> pushc tag_true
| Tfalse -> pushc tag_false
......@@ -417,20 +444,21 @@ let t_shape_task ~version ~expl t =
(* expl *)
begin match version with
| SV1 | SV2 -> ()
| SV3 | SV4 | SV5 -> push expl end;
| SV3 | SV4 | SV5 | SV6 -> push expl end;
(* goal shape *)
t_shape ~version c m f;
(* All declarations shape *)
begin match version with
| SV1 | SV2 | SV3 -> ()
| SV4 | SV5 ->
| SV4 | SV5 | SV6 ->
let open Decl in
let do_td td = match td.Theory.td_node with
| Theory.Decl d ->
begin match d.d_node with
| Dparam _ls -> ()
| Dprop (_, _pr, f) ->
t_shape ~version c m f
pushc tag_hyp;
t_shape ~version c m f
| _ -> ()
end
| _ -> () in
......@@ -449,7 +477,7 @@ let time = ref 0.0
let t_shape_task ?(version=current_shape_version) ~expl t =
let version = match version with
| 1 -> SV1 | 2 -> SV2 | 3 | 4 -> SV3 | 5 -> SV4 | 6 -> SV5
| 1 -> SV1 | 2 -> SV2 | 3 | 4 -> SV3 | 5 -> SV4 | 6 -> SV5 | 7 -> SV6
| _ -> assert false
in
(*
......@@ -764,7 +792,7 @@ let task_checksum ?(version=current_shape_version) t =
let version = match version with
| 1 | 2 | 3 -> CV1
| 4 | 5 -> CV2
| 6 -> CV3
| 6 | 7 -> CV3
| _ -> assert false
in
(*
......@@ -814,6 +842,36 @@ module Pairing(Old: S)(New: S) = struct
else if s1.[n] = s2.[n] then lcp (n+1) s1 s2 else n
let lcp = lcp 0
let rec lcp_rec l ls1 ls2 =
match ls1, ls2 with
| hd1 :: tl1, hd2 :: tl2 ->
lcp_rec (l @ [lcp hd1 hd2]) tl1 tl2
| _ -> l
let lcp_list s1 s2 =
(* TODO here we don't need the split as there is an equivalent program that
only go through the strings once. The same as for lcp. *)
let ls1 = Strings.split tag_hyp s1 in
let ls2 = Strings.split tag_hyp s2 in
let l = lcp_rec [] ls1 ls2 in
(* TODO remove debugging here. *)
Format.eprintf "l = ";
List.iter (fun x -> Format.eprintf "%d " x) l;
Format.eprintf "\n@.";
Format.eprintf "%s \n\n%s\n\n@." s1 s2;
l
let rec compare_list ls1 ls2 =
match ls1, ls2 with
| hd1 :: tl1, hd2 :: tl2 ->
let n = Pervasives.compare hd1 hd2 in
if Pervasives.compare hd1 hd2 = 0 then
compare_list tl1 tl2
else n
| _ :: _, _ -> 1 (* ls1 > ls2 *)
| _, _ :: _ -> -1 (* ls1 < ls2 *)
| _ -> 0
open Ident
type goal_index = Old of int | New of int
......@@ -854,6 +912,11 @@ module Pairing(Old: S)(New: S) = struct
else if n == x then p.next <- p (* right bound *)
else begin p.next <- n; n.prev <- p end
let compare_only_goal s1 s2 =
let hd1 = match Strings.split tag_hyp s1 with hd1 :: _ -> hd1 | _ -> assert false in
let hd2 = match Strings.split tag_hyp s2 with hd2 :: _ -> hd2 | _ -> assert false in
Pervasives.compare hd1 hd2
(* priority queues for pairs of nodes *)
let dprintf = Debug.dprintf debug
......@@ -909,24 +972,35 @@ module Pairing(Old: S)(New: S) = struct
let allgoals = Hashtbl.fold add old_checksums newgoals in
Hashtbl.clear old_checksums;
(* phase 2: pair goals according to shapes *)
let compare e1 e2 = Pervasives.compare e1.shape e2.shape in
(* TODO here the idea is to compare only goals. This is consistent with the
original idea of shapes. The idea is to add to the PQ in priority the
goals that have the same goal_shape. *)
let compare e1 e2 = compare_only_goal e1.shape e2.shape in
let allgoals = List.sort compare allgoals in
build_list allgoals;
if allgoals <> [] then begin
let module E = struct
let dummy = let n = List.hd allgoals (* safe *) in 0, (n, n)
type t = int * (node * node)
let compare (v1, _) (v2, _) = Pervasives.compare v2 v1
let dummy = let n = List.hd allgoals (* safe *) in [], (n, n)
type t = int list * (node * node)
let compare (v1, _) (v2, _) = compare_list v2 v1
end in
let module PQ = Pqueue.Make(E) in
let pq = PQ.create () in
let add x y = match x.elt, y.elt with
| Old _, New _ | New _, Old _ ->
PQ.insert (lcp x.shape y.shape, (x, y)) pq
PQ.insert (lcp_list x.shape y.shape, (x, y)) pq
| Old _, Old _ | New _, New _ -> () in
(* TODO can be made more efficient as the list is sorted *)
(* TODO this assume we can add each elements more than twice ->
should be ok. *)
List.iter (fun x -> List.iter (fun y -> if compare x y = 0 && x.elt <> y.elt then add x y) allgoals) allgoals;
iter_pairs add allgoals;
(* FIXME: exit earlier, as soon as we get min(old,new) pairs *)
while not (PQ.is_empty pq) do
(* TODO here I say that there can be several pairs which are maximum.
So, we can refine using the non-goal hypothesis because in the case,
where only an axiom was changed, it is better: *all* Old are changed
in the same way compared to New *)
let _, (x, y) = PQ.extract_min_exn pq in
if x.valid && y.valid then begin
let o, n = match x.elt, y.elt with
......