From 8511e56d0f519d9a77c3be2ec4b5fc2b0681f052 Mon Sep 17 00:00:00 2001
From: Sylvain Dailler
Date: Mon, 6 May 2019 17:11:14 +0200
Subject: [PATCH] [WIP] TEST. Not intended to be merged.
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.
---
examples/bts/276_shape.mlw | 7 +--
examples/bts/276_shape/why3shapes.gz | Bin 411 -> 420 bytes
src/session/termcode.ml | 62 ++++++++++++++++++++++++---
3 files changed, 60 insertions(+), 9 deletions(-)
diff --git a/examples/bts/276_shape.mlw b/examples/bts/276_shape.mlw
index e5546e252..b1eedc78e 100644
--- a/examples/bts/276_shape.mlw
+++ b/examples/bts/276_shape.mlw
@@ -1,5 +1,6 @@
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
diff --git a/examples/bts/276_shape/why3shapes.gz b/examples/bts/276_shape/why3shapes.gz
index 16428fe33be916a655908666aa0d3edf6469af54..8e3f97fcba23f51ba78f0f957ba810623b7b6fb4 100644
GIT binary patch
literal 420
zcmV;V0bBkbiwFP!00000|Ls*xYaB5Qz4uqlIU!(KwmgOeavJC*xrtouvD^egQ?@-U
z{q>RU*=$O4XwMl&jGm&2tiRK_nTp&H_YNp`h_8
zql14D(ypJ+s~_|s#_FVCawepjsFpyk>MSU`;-_b+zos?)lwCi&e*V^vK39md$zVi^
zj}#M@Ou^Z3N)%@(IMPfHdcB;g-+DKoAFK7l(X(
zmZWrNAeC!NT9C7|!-uGWM3yq@+LDVNv(w%h=atgBR!dE#+(kSjYBp0LxCw59~Qi
zePBOKtOusDzaD&3aCLoD*Z2Y!J-*iU|T4J39gJG}(Siu|H_Y0mOFt~9bcO!KJ
zbaEe!s!LJM05=`VvA_=SI-lgks2R<~qwVQb$Q+i@4d4V{Ss(wLYkR&dUpwv(vz6ZQ
zLE?RhNzIo*Y8THGB-ZPjW ()
| Dprop (_, _pr, f) ->
- t_shape ~version c m f
+ pushc tag_hyp;
+ t_shape ~version c m f
| _ -> ()
end
| _ -> () in
@@ -838,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
@@ -878,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
@@ -933,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
--
2.22.0