From 94bf57195089baec93a112904ccfa871d089c635 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 20 Oct 2020 11:41:43 -0700 Subject: [PATCH] [sledge] Rename Fheap to FHeap for consistency Reviewed By: ngorogiannis Differential Revision: D24306064 fbshipit-source-id: b4abc661c --- sledge/nonstdlib/NS.mli | 3 ++- sledge/nonstdlib/NS0.ml | 1 + sledge/src/control.ml | 10 +++++----- 3 files changed, 8 insertions(+), 6 deletions(-) diff --git a/sledge/nonstdlib/NS.mli b/sledge/nonstdlib/NS.mli index a50791404..e91369c53 100644 --- a/sledge/nonstdlib/NS.mli +++ b/sledge/nonstdlib/NS.mli @@ -146,8 +146,9 @@ include module type of IArray.Import module Set = Set module Map = Map module Multiset = Multiset -module HashTable = HashTable +module FHeap = Fheap [@@warning "-49"] module HashSet = HashSet +module HashTable = HashTable module HashQueue = Core_kernel.Hash_queue (** Input / Output *) diff --git a/sledge/nonstdlib/NS0.ml b/sledge/nonstdlib/NS0.ml index 86a204c1e..de4d6c40e 100644 --- a/sledge/nonstdlib/NS0.ml +++ b/sledge/nonstdlib/NS0.ml @@ -125,6 +125,7 @@ module Either = struct let right v = Right v end +module FHeap = Fheap [@@warning "-49"] module HashQueue = Core_kernel.Hash_queue (** Input / Output *) diff --git a/sledge/src/control.ml b/sledge/src/control.ml index 8e250cc95..dc9429d31 100644 --- a/sledge/src/control.ml +++ b/sledge/src/control.ml @@ -196,7 +196,7 @@ module Make (Dom : Domain_intf.Dom) = struct end type priority = int * Edge.t [@@deriving compare] - type priority_queue = priority Fheap.t + type priority_queue = priority FHeap.t type waiting_states = (Dom.t * Depths.t) list Llair.Block.Map.t type t = priority_queue * waiting_states * int type x = Depths.t -> t -> t @@ -207,7 +207,7 @@ module Make (Dom : Domain_intf.Dom) = struct let pp fs pq = Format.fprintf fs "@[%a@]" (List.pp " ::@ " pp_priority) - (Fheap.to_list pq) + (FHeap.to_list pq) let skip _ w = w let seq x y d w = y d (x d w) @@ -221,7 +221,7 @@ module Make (Dom : Domain_intf.Dom) = struct [%Trace.info "prune: %i: %a" depth Edge.pp edge] ; work ) else - let pq = Fheap.add pq (depth, edge) in + let pq = FHeap.add pq (depth, edge) in [%Trace.info "@[<6>enqueue %i: %a@ | %a@]" depth Edge.pp edge pp pq] ; let depths = Depths.set depths ~key:edge ~data:depth in let ws = @@ -231,10 +231,10 @@ module Make (Dom : Domain_intf.Dom) = struct let init state curr bound = add ~retreating:false Stack.empty state curr Depths.empty - (Fheap.create ~cmp:compare_priority, empty_waiting_states, bound) + (FHeap.create ~cmp:compare_priority, empty_waiting_states, bound) let rec run ~f (pq0, ws, bnd) = - match Fheap.pop pq0 with + match FHeap.pop pq0 with | Some ((_, ({Edge.dst; stk} as edge)), pq) -> ( match Llair.Block.Map.find_and_remove ws dst with | Some (q :: qs, ws) ->