new pairing algorithm (not yet used)

parent 66571850
......@@ -107,7 +107,7 @@ LIBGENERATED = src/util/config.ml src/util/rc.ml src/parser/lexer.ml \
LIB_UTIL = config util opt lists strings extmap extset exthtbl weakhtbl \
hashcons stdlib exn_printer pp debug loc print_tree \
cmdline warning sysutil rc plugin number
cmdline warning sysutil rc plugin number pqueue
LIB_CORE = ident ty term pattern decl theory task pretty env trans printer
......
......@@ -693,10 +693,45 @@ end
module AssoMake2 (Old : S) (New : S) = struct
type any_goal = Old of Old.t | New of New.t
let rec lcp n s1 s2 =
if String.length s1 <= n || String.length s2 <= n then n
else if s1.[n] = s2.[n] then lcp (n+1) s1 s2 else n
let lcp = lcp 0
open Ident
type any_goal = Old of Old.t | New of New.t
(* doubly linked lists *)
type node = {
mutable prev: node;
shape: string;
elt: any_goal;
mutable valid: bool;
mutable next: node;
}
let mk_node g =
let s = match g with Old g -> Old.shape g | New g -> New.shape g in
let rec n = { prev = n; shape = s; elt = g; next = n; valid = true } in n
let rec iter_pairs f = function
| [] | [_] -> ()
| x :: (y :: _ as l) -> f x y; iter_pairs f l
let build_list = iter_pairs (fun x y -> x.next <- y; y.prev <- x)
(* priority queues for pairs of nodes *)
module E = struct
type t = int * (node * node)
let compare (v1, _) (v2, _) = Pervasives.compare v2 v1
end
module PQ = Pqueue.Make(E)
let dprintf = Debug.dprintf debug
let associate oldgoals newgoals =
(* set up an array [result] containing the solution
[new_goal_index g] returns the index of goal [g] in that array *)
......@@ -717,19 +752,41 @@ module AssoMake2 (Old : S) (New : S) = struct
try
let oldg = Hashtbl.find old_checksums c in
Hashtbl.remove old_checksums c;
result.(new_goal_index newg) <- (newg, Some oldg, true);
result.(new_goal_index newg) <- (newg, Some oldg, false);
acc
with Not_found ->
New newg :: acc
mk_node (New newg) :: acc
in
let newgoals = List.fold_left collect [] newgoals in
let _allgoals =
Hashtbl.fold (fun _ oldg acc -> Old oldg :: acc) old_checksums newgoals in
let add _ oldg acc = mk_node (Old oldg) :: acc in
let allgoals = Hashtbl.fold add old_checksums newgoals in
Hashtbl.clear old_checksums;
(* phase 2: pair goals according to shapes *)
(* let compare (sh1, _) (sh2, _) = Pervasives.compare sh1 sh2 in *)
(* let allgoals = List.sort compare allgoals in *)
(* assert false *)
let compare e1 e2 = Pervasives.compare e1.shape e2.shape in
let allgoals = List.sort compare allgoals in
build_list allgoals;
if allgoals <> [] then begin
let dummy = let n = List.hd allgoals (* safe *) in 0, (n, n) in
let pq = PQ.create ~dummy in
let add x y = match x.elt, y.elt with
| Old _, New _ | New _, Old _ -> PQ.add pq (lcp x.shape y.shape, (x, y))
| Old _, Old _ | New _, New _ -> () in
iter_pairs add allgoals;
(* FIXME: exit earlier, as soon as we get min(old,new) pairs *)
while not (PQ.is_empty pq) do
let _, (x, y) = PQ.extract_min pq in
if x.valid && y.valid then begin
x.valid <- false; y.valid <- false;
let o, n = match x.elt, y.elt with
| New n, Old o | Old o, New n -> o, n | _ -> assert false in
dprintf "[assoc] new pairing@.";
result.(new_goal_index n) <- n, Some o, true;
if x.prev != x && y.next != y then add x.prev y.next;
if x.prev != x then x.prev.next <- y.next else y.next.prev <- y.next;
if y.next != y then y.next.prev <- x.prev else x.prev.next <- x.prev
end
done
end;
Array.to_list result
end
......@@ -67,9 +67,9 @@ module AssoMake (Old : S) (New : S) : sig
val associate : Old.t list -> New.t list -> (New.t * Old.t option *bool) list
(** associate the new things {New.t} to old things {Old.t}.
(n,o,b) means if [o,b] is:
- [Some o, true] the old thing [o] have the same checksum that the new
- [Some o, false] the old thing [o] have the same checksum that the new
thing [n].
- [Some o, false] no old things have the same checksum
- [Some o, true] no old things have the same checksum
than [n]. The new thing [o] has a shape similar to [n]
- [None] no old thing were similar enough. *)
end
......
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
(* Resizable arrays *)
module RA = struct
type 'a t = { default: 'a; mutable size: int; mutable data: 'a array }
let length a = a.size
let make n d = { default = d; size = n; data = Array.make n d }
let get a i =
if i < 0 || i >= a.size then invalid_arg "RA.get";
a.data.(i)
let set a i v =
if i < 0 || i >= a.size then invalid_arg "RA.set";
a.data.(i) <- v
let resize a s =
if s <= a.size then begin
Array.fill a.data s (a.size - s) a.default
end else begin
let n = Array.length a.data in
if s > n then begin
let n' = max (2 * n) s in
let a' = Array.make n' a.default in
Array.blit a.data 0 a' 0 a.size;
a.data <- a'
end
end;
a.size <- s
end
(* Priority queue *)
(* The heap is encoded into a resizable array, where elements are stored
from [0] to [length - 1]. From an element stored at [i], the left
(resp. right) subtree, if any, is rooted at [2*i+1] (resp. [2*i+2]). *)
module Make(X: Set.OrderedType) = struct
type elt = X.t
type t = elt RA.t
let create ~dummy = RA.make 16 dummy
let is_empty h = RA.length h = 0
let clear h = RA.resize h 0
let rec move_up h x i =
if i = 0 then RA.set h i x else
let fi = (i - 1) / 2 in
let y = RA.get h fi in
if X.compare y x > 0 then begin RA.set h i y; move_up h x fi end
else RA.set h i x
let add h x =
let n = RA.length h in RA.resize h (n + 1); move_up h x n
exception Empty
let get_min h =
if RA.length h = 0 then raise Empty;
RA.get h 0
let min h l r = if X.compare (RA.get h r) (RA.get h l) < 0 then r else l
let smallest_node h x i =
let l = 2 * i + 1 in
let n = RA.length h in
if l >= n then i else
let r = l + 1 in
let j = if r < n then min h l r else l in
if X.compare (RA.get h j) x < 0 then j else i
let rec move_down h x i =
let j = smallest_node h x i in
if j = i then RA.set h i x
else begin RA.set h i (RA.get h j); move_down h x j end
let remove_min h =
let n = RA.length h - 1 in
if n < 0 then raise Empty;
let x = RA.get h n in
RA.resize h n;
if n > 0 then move_down h x 0
let extract_min h =
if RA.length h = 0 then raise Empty;
let x = RA.get h 0 in
remove_min h;
x
end
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
(* Priority queue *)
module Make(X: Set.OrderedType) : sig
type t
type elt = X.t
val create: dummy:elt -> t
(** [dummy] will never be returned *)
val is_empty: t -> bool
val add: t -> elt -> unit
(* inserts a new element *)
exception Empty
val get_min: t -> elt
(* returns the minimal element (does not remove it)
raises [Empty] if the queue is empty *)
val remove_min: t -> unit
(* removes the minimal element
raises [Empty] if the queue is empty *)
val extract_min: t -> elt
(* removes and returns the minimal element
raises [Empty] if the queue is empty *)
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