Remove some warnings in 4.14

src_colibri2/core/egraph.ml

@@ -79,7 +79,6 @@ module Def = struct
       saved_repr  : Node.t Node.M.t;
       saved_rang  : int Node.M.t;
       saved_event_repr :  event_node Bag.t Node.M.t;
-      saved_event_any_repr : event_node Bag.t;
       saved_event_value : (ro delayed_t -> Node.t -> Value.t -> Events.enqueue) Bag.t Node.M.t;
       saved_event_reg : event_node Bag.t Node.M.t;
       saved_event_any_reg : event_node Bag.t;
@@ -215,7 +214,6 @@ module Hidden = Context.Make(struct
         saved_repr = t.repr;
         saved_rang = t.rang;
         saved_event_repr = t.event_repr;
-        saved_event_any_repr = t.event_any_repr;
         saved_event_value = t.event_value;
         saved_event_reg = t.event_reg;
         saved_event_any_reg = t.event_any_reg;

src_colibri2/core/events.ml

@@ -22,18 +22,6 @@
 
 module Dem = Keys.Make_key ()
 
-module Print = struct
-  (** Cutting the knot for pp *)
-
-  type pdem_runable = {
-    mutable pdem_runable : 'd. 'd Dem.t -> 'd Format.printer;
-  }
-
-  (** called too early *)
-  let pdem_runable : pdem_runable =
-    { pdem_runable = (fun _ _ _ -> assert false) }
-end
-
 type delay =
   | Immediate
   | Delayed_by of int
@@ -62,22 +50,15 @@ module Wait = struct
       type runable
 
       val print_runable : runable Format.printer
-
       val run : delayed -> runable -> unit
-
       val key : runable Dem.t
-
       val delay : delay
     end
 
     val register_dem : (module Dem with type runable = 'd) -> unit
-
     val get_dem : 'd Dem.t -> (module Dem with type runable = 'd)
-
     val get_priority : daemon_key -> delay
-
     val print_dem_runable : 'b Dem.t -> 'b Format.printer
-
     val is_well_initialized : unit -> bool
   end
 
@@ -90,11 +71,8 @@ module Wait = struct
       type runable
 
       val print_runable : runable Format.printer
-
       val run : delayed -> runable -> unit
-
       val key : runable Dem.t
-
       val delay : delay
     end
 
@@ -111,7 +89,6 @@ module Wait = struct
     end)
 
     let register_dem = Registry.register
-
     let get_dem = Registry.get
 
     let get_priority = function
@@ -120,9 +97,6 @@ module Wait = struct
           Dem.delay
 
     let print_dem_runable = Registry.print
-
-    let () = Print.pdem_runable.Print.pdem_runable <- print_dem_runable
-
     let is_well_initialized = Registry.is_well_initialized
   end
 end

src_colibri2/popop_lib/exthtbl.ml

@@ -152,7 +152,7 @@ module MakeSeeded(H: SeededHashedType) =
     type 'b t =
       { mutable size: int;                        (* number of entries *)
         mutable data: 'b bucketlist array;  (* the buckets *)
-        mutable seed: int;                        (* for randomization *)
+        seed: int;                        (* for randomization *)
         initial_size: int;                        (* initial array size *)
       }
 

src_colibri2/solver/scheduler.ml

@@ -40,26 +40,19 @@ let debug_dotgui =
     "sched_dotgui"
 
 let var_decay = 1. /. 0.95
-
 let stats_propa = Debug.register_stats_int "Scheduler.daemon"
-
 let stats_lasteffort = Debug.register_stats_int "Scheduler.lasteffort"
 
 let stats_lasteffort_propa =
   Debug.register_stats_int "Scheduler.lasteffort_propa"
 
 let stats_dec = Debug.register_stats_int "Scheduler.decision"
-
 let stats_con = Debug.register_stats_int "Scheduler.conflict"
-
 let stats_con_fix = Debug.register_stats_int "Scheduler.conflict_fix_model"
-
 let stats_step = Debug.register_stats_int "Scheduler.step"
-
 let stats_fix_model = Debug.register_stats_int "Scheduler.fix_model"
 
 exception Contradiction
-
 exception ReachStepLimit
 
 type last_effort_limit = Time of float | Steps of int
@@ -73,6 +66,8 @@ struct
   module Att = struct
     type t = { id : int; v : S.t; added_at : int }
 
+    let _f x = x.added_at
+
     type prio = float
 
     let equal_prio = ( = )
@@ -208,11 +203,10 @@ type t = {
   solve_step : solve_step Context.Ref.t;
   last_effort_limit : last_effort_limit option;
   mutable steps : int;
-  mutable stepsl : int;
   mutable last_todo : (Egraph.wt -> unit) * bp_kind;
   last_effort_learnt : Events.daemon_key Context.Clicket.t;
   allow_learning : bool;  (** Learning *)
-  mutable learning_htbl : int ThTerm.H.t;
+  learning_htbl : int ThTerm.H.t;
   mutable learning_tbl : bool array;
   (* last before contradiction *)
   mutable last_effort_made : PrioLastEffort.Att.t option;
@@ -257,7 +251,6 @@ let new_solver ~learning ?last_effort_limit
       level = 0;
       solve_step = Context.Ref.create creator Propagate;
       steps = 0;
-      stepsl = 0;
       last_todo = ((fun _ -> ()), External);
       last_effort_learnt = Context.Clicket.create creator;
       last_effort_limit;
@@ -719,7 +712,5 @@ let run ?nodec ?step_limit ?last_effort_limit ?options ~theories f =
   with Contradiction -> `Contradiction
 
 let pop_to st bp = ignore (pop_to st bp)
-
 let push st = push External st
-
 let get_context t = Context.creator t.context