Use the Heap of Alt-Ergo

Author: Halbaroth

alt-ergo-lib.opam

@@ -31,7 +31,6 @@ depends: [
   "odoc" {with-doc}
   "ppx_deriving"
   "stdcompat"
-  "bheap"
 ]
 conflicts: [
   "ppxlib" {< "0.30.0"}

alt-ergo-lib.opam.locked

@@ -62,7 +62,6 @@ depends: [
   "uutf" {= "1.0.3"}
   "yojson" {= "2.1.1"}
   "zarith" {= "1.13"}
-  "bheap" {= "2.0.0"}
 ]
 build: [
   ["dune" "subst"] {dev}

dune-project

@@ -91,7 +91,6 @@ See more details on http://alt-ergo.ocamlpro.com/"
   (odoc :with-doc)
   ppx_deriving
   stdcompat
-  bheap
  )
  (conflicts
   (ppxlib (< 0.30.0))

shell.nix

@@ -43,6 +43,5 @@ pkgs.mkShell {
     stdcompat
     landmarks
     landmarks-ppx
-    bheap
   ];
 }

src/lib/dune

@@ -25,7 +25,6 @@
     alt_ergo_prelude
     fmt
     stdcompat
-    bheap
   )
   (preprocess
     (pps

src/lib/frontend/typechecker.ml

@@ -2567,11 +2567,6 @@ let rec type_decl (acc, env) d assertion_stack =
   | TypeDecl l ->
     let not_rec, are_rec = partition_non_rec l in
 
-    let not_rec, are_rec =
-      if Lists.is_empty are_rec then not_rec, are_rec
-      else [], List.rev_append not_rec are_rec
-    in
-
     (* A. Typing types that are not recursive *)
     let acc, env =
       List.fold_left

src/lib/reasoners/satml.ml

@@ -143,7 +143,7 @@ end
 module MFF = FF.Map
 module SFF = FF.Set
 
-module Vheap = Heap.Make(struct
+module Vheap = Heap.MakeRanked(struct
     type t = Atom.var
 
     let index (a : t) = a.hindex
@@ -478,7 +478,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
 
       simpDB_props = 0;
 
-      order = Vheap.make 0 Atom.dummy_var; (* sera mis a jour dans solve *)
+      order = Vheap.create 0 Atom.dummy_var; (* sera mis a jour dans solve *)
 
       progress_estimate = 0.;
 
@@ -1827,7 +1827,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
           env.next_split <- None;
           pick_branch_aux env atom
         | None ->
-          match Vheap.remove_min env.order with
+          match Vheap.pop_minimum env.order with
           | v -> pick_branch_aux env v.na
           | exception Not_found ->
             if Options.get_cdcl_tableaux_inst () then

src/lib/util/heap.ml

@@ -35,41 +35,15 @@ module type RankedType = sig
   val compare : t -> t -> int
 end
 
-module type S = sig
-  type elt
-
-  type t
-
-  val make : int -> elt -> t
-
-  val in_heap : elt -> bool
-
-  val decrease : t -> elt -> unit
-
-  val increase : t -> elt -> unit
-
-  val size : t -> int
-
-  val is_empty : t -> bool
-
-  val insert : t -> elt -> unit
-
-  val grow_to_by_double : t -> int -> unit
-
-  val remove_min : t -> elt
-
-  val filter : t -> (elt -> bool) -> unit
-end
-
-module Make(Rank : RankedType) = struct
+module MakeRanked(Rank : RankedType) = struct
   type elt = Rank.t
 
   type t = { heap : elt Vec.t } [@@unboxed]
 
   (* Negative value; used to indicate an element is not in the heap *)
   let absent = -1
 
-  let make sz dummy = { heap = Vec.make ~dummy sz }
+  let create sz dummy = { heap = Vec.make ~dummy sz }
 
   let[@inline] left i = (i lsl 1) + 1 (* i*2 + 1 *)
   let[@inline] right i = (i + 1) lsl 1 (* (i + 1) * 2*)
@@ -148,7 +122,7 @@ module Make(Rank : RankedType) = struct
   let[@inline] grow_to_by_double { heap } sz =
     Vec.grow_to_by_double heap sz
 
-  let remove_min ({ heap } as s) =
+  let pop_minimum ({ heap } as s) =
     match Vec.size heap with
     | 0 -> raise Not_found
     | 1 ->
@@ -165,3 +139,36 @@ module Make(Rank : RankedType) = struct
       if Vec.size s.heap > 1 then percolate_down s y;
       x
 end
+
+module type OrderedTypeDefault = sig
+  type t
+
+  val compare : t -> t -> int
+
+  val default : t
+end
+
+module MakeOrdered(V : OrderedTypeDefault) = struct
+  type entry = { value : V.t ; mutable index : int }
+  type elt = V.t
+
+  module H = MakeRanked
+      (struct
+        type t = entry
+
+        let index e = e.index
+
+        let set_index e i = e.index <- i
+
+        let compare x y = V.compare x.value y.value
+      end)
+
+  let entry value = { value ; index = -1 }
+
+  type t = H.t
+
+  let create n = H.create n (entry V.default)
+  let is_empty = H.is_empty
+  let insert h v = H.insert h (entry v)
+  let pop_minimum h = (H.pop_minimum h).value
+end

src/lib/util/heap.mli

@@ -62,13 +62,14 @@ end
 
 (** {2 Priority heaps} *)
 
-module type S = sig
-  type elt
+module MakeRanked(Rank : RankedType) : sig
+  type elt = Rank.t
+  (** The type of elements of the heap. *)
 
   type t
   (** The type of heaps. *)
 
-  val make : int -> elt -> t
+  val create : int -> elt -> t
   (** Create a heap with the given initial size and dummy element. *)
 
   val in_heap : elt -> bool
@@ -87,13 +88,13 @@ module type S = sig
   (** Is the heap empty ? *)
 
   val insert : t -> elt -> unit
-  (** Inset a new element in the heap. *)
+  (** Insert a new element in the heap. *)
 
   val grow_to_by_double: t -> int -> unit
   (** Grow the size of the heap by multiplying it by 2
       until it is at least the size specified. *)
 
-  val remove_min : t -> elt
+  val pop_minimum : t -> elt
   (** Remove the minimum element from the heap and return it.
 
       @raise Not_found if the heap is empty. *)
@@ -102,4 +103,35 @@ module type S = sig
   (** Filter elements in the heap. *)
 end
 
-module Make(Rank : RankedType) : S with type elt = Rank.t
+(** {2 Ordered priority heaps} *)
+
+module type OrderedTypeDefault = sig
+  type t
+
+  val compare : t -> t -> int
+
+  val default : t
+  (** Dummy value used in the heap. *)
+end
+
+module MakeOrdered(V : OrderedTypeDefault) : sig
+  type elt = V.t
+  (** The type of elements of the heap. *)
+
+  type t
+  (** The type of heaps. *)
+
+  val create : int -> t
+  (** Create a heap with the given initial size. *)
+
+  val is_empty : t -> bool
+  (** Is the heap empty ? *)
+
+  val insert : t -> elt -> unit
+  (** Insert a new element in the heap. *)
+
+  val pop_minimum : t -> elt
+  (** Remove the minimum element from the heap and return it.
+
+      @raise Not_found if the heap is empty. *)
+end

src/lib/util/nest.ml

@@ -74,24 +74,21 @@ type node = {
 (* Type of a hyperedge. *)
 and edge = node list ref
 
-module Heap = struct
-  include Binary_heap.Make
-      (struct
-        type t = node
-        let compare { weight = w1; _ } { weight = w2; _ } = w1 - w2
-      end)
-
-  let create =
-    let dummy_edge : node list ref = ref [] in
-    let dummy = {
-      id = Term.Const.Int.int "0" (* dummy *);
-      outgoing = dummy_edge;
-      in_degree = -1;
-      weight = -1;
-    }
-    in
-    create ~dummy
-end
+module Hp =
+  Heap.MakeOrdered
+    (struct
+      type t = node
+      let compare { weight = w1; _ } { weight = w2; _ } = w1 - w2
+
+      let default =
+        let dummy_edge : node list ref = ref [] in
+        {
+          id = Term.Const.Int.int "0" (* dummy *);
+          outgoing = dummy_edge;
+          in_degree = -1;
+          weight = -1;
+        }
+    end)
 
 let (let*) = Option.bind
 
@@ -117,9 +114,9 @@ let def_of_dstr dstr =
 
    @return a heap that contains all the nodes of this graph without ingoing
    hyperedges. *)
-let build_graph (defs : ty_def list) : Heap.t =
+let build_graph (defs : ty_def list) : Hp.t =
   let map : (ty_def, edge) Hashtbl.t = Hashtbl.create 17 in
-  let hp : Heap.t = Heap.create 17 in
+  let hp : Hp.t = Hp.create 17 in
   List.iter (fun d -> Hashtbl.add map d (ref [])) defs;
   List.iter
     (fun def ->
@@ -152,7 +149,7 @@ let build_graph (defs : ty_def list) : Heap.t =
                   ) 0 dstrs
               in
               node.in_degree <- in_degree;
-              if in_degree = 0 then Heap.add hp node
+              if in_degree = 0 then Hp.insert hp node
            ) cases
     ) defs;
   hp
@@ -182,10 +179,10 @@ let add_cstr, find_weight, reinit =
    Kahn's algorithm. *)
 let add_nest n =
   let hp = build_graph n in
-  while not @@ Heap.is_empty hp do
+  while not @@ Hp.is_empty hp do
     (* Loop invariant: the set of nodes in heap [hp] is exactly
        the set of the nodes of the graph without ingoing hyperedge. *)
-    let { id; outgoing; in_degree; _ } = Heap.pop_minimum hp in
+    let { id; outgoing; in_degree; _ } = Hp.pop_minimum hp in
     add_cstr @@ Uid.of_dolmen id;
     assert (in_degree = 0);
     outgoing :=
@@ -194,7 +191,7 @@ let add_nest n =
            assert (node.in_degree > 0);
            let node = { node with in_degree = node.in_degree - 1 } in
            if node.in_degree = 0 then (
-             Heap.add hp node;
+             Hp.insert hp node;
              None
            ) else (
              Some node