From 60073210ce226abf8b6e3f8f28e25c97f47a63e0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Mon, 19 Aug 2024 14:52:33 +0200 Subject: [PATCH] Rename schedule constructors --- src/lib/reasoners/bitv_rel.ml | 80 +++++++++++++++++------------------ 1 file changed, 40 insertions(+), 40 deletions(-) diff --git a/src/lib/reasoners/bitv_rel.ml b/src/lib/reasoners/bitv_rel.ml index 90240cf53..9537eb49c 100644 --- a/src/lib/reasoners/bitv_rel.ml +++ b/src/lib/reasoners/bitv_rel.ml @@ -1662,6 +1662,7 @@ end = struct let push q k p = Q.push q (B (k, p)) + (* Returns [false] if no propagation was performed (empty queue). *) let run1 st q = match Q.pop q with | B ({ run ; _ }, p) -> run st p; true @@ -2002,40 +2003,40 @@ let state uf idom bdom = ; bitlist_variables = bvars ; bitlist_changed = HX.create 17 } -(* Schedule specifications *) -type schedule = - | Single of Any_propagator.Queue.t - (** Propagate a single constraint from the given queue. *) - | Round_robin of (schedule * int) array - (** Performs [n] propagations from the provided schedules in round-robin - fashion the coefficient adjusts how many propagations are performed - before moving on to the next schedule. *) - | Repeat of schedule - (** Repeat the given schedule to completion. *) - -let rec run_schedule state schedule = - match schedule with - | Single queue -> Any_propagator.Queue.run1 state queue - | Round_robin schedules -> - Array.fold_left (fun did_run (schedule, niter) -> - run_many state schedule false niter || did_run - ) false schedules - | Repeat schedule -> - run_repeatedly state schedule false - -and run_many state schedule did_run n = - if n <= 0 then did_run - else - if run_schedule state schedule then - run_many state schedule true (n - 1) - else - did_run +module Schedule = struct + (* Schedule specifications *) + type t = + | Single of Any_propagator.Queue.t + (** Propagate a single constraint from the given queue. *) + | Sequence of t array + (** Performs propagations from the provided schedules in sequence. *) + | Repeat of t + (** Repeat the given schedule to completion. *) + + (* Returns [false] if no propagation was performed. *) + let rec run state schedule = + match schedule with + | Single queue -> + Any_propagator.Queue.run1 state queue + | Sequence schedules -> + Array.fold_left (fun did_run schedule -> + run state schedule || did_run + ) false schedules + | Repeat schedule -> + run_repeatedly state schedule false + + and run_repeatedly state schedule did_run = + if run state schedule then + run_repeatedly state schedule true + else + did_run -and run_repeatedly state schedule did_run = - if run_schedule state schedule then - run_repeatedly state schedule true - else - did_run + let queue q = Single q + + let sequence scheds = Sequence scheds + + let repeat s = Repeat s +end let rec propagate_all uf eqs bdom idom = (* Optimization to avoid unnecessary allocations *) @@ -2047,14 +2048,13 @@ let rec propagate_all uf eqs bdom idom = (* We run all propagations over a single domain to completion, then run the consistency propagators to perform cross-domain propagations. *) - ignore ( - run_schedule state @@ Repeat ( - Round_robin - [| (Repeat (Single queues.propagation_queue), 1) - ; (Repeat (Single queues.consistency_queue), 1) + ignore Schedule.( + run state @@ repeat @@ + sequence + [| repeat @@ queue queues.propagation_queue + ; repeat @@ queue queues.consistency_queue |] - ) - ); + ); let bdom = state.bitlists in let idom = state.intervals in