diff --git a/src_colibri2/core/egraph.ml b/src_colibri2/core/egraph.ml index 29493d5bd3faa133a59693b63f527cf5bbcdc71b..0256693c365887386c726a87a249be31f620ae6d 100644 --- a/src_colibri2/core/egraph.ml +++ b/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; diff --git a/src_colibri2/core/events.ml b/src_colibri2/core/events.ml index 15f84bdcbe7b843e395d97cdeea3a2d7c779f8f7..e8091abc00541794392926685a225c5f1c32e94b 100644 --- a/src_colibri2/core/events.ml +++ b/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 diff --git a/src_colibri2/popop_lib/exthtbl.ml b/src_colibri2/popop_lib/exthtbl.ml index 79e10417d4ceb5159de7d914fbdfcad2b57c2340..d9fdb2cb0a721d36d796faef2b04563d406ef071 100644 --- a/src_colibri2/popop_lib/exthtbl.ml +++ b/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 *) } diff --git a/src_colibri2/solver/scheduler.ml b/src_colibri2/solver/scheduler.ml index d1e4faedbd2af2b9b5c4827fa4d697a2d3150c90..5c27d24d584a81a03af71962a9abd586426a0c2e 100644 --- a/src_colibri2/solver/scheduler.ml +++ b/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