From 85f75858ffa812ae52b42f1e70e347b5caaf67b6 Mon Sep 17 00:00:00 2001 From: Rudi Grinberg Date: Wed, 29 Jan 2025 19:18:03 +0000 Subject: [PATCH] refactor(sat): remove useless argument of [Decided] Signed-off-by: Rudi Grinberg Signed-off-by: Rudi Grinberg --- src/sat/sat.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/sat/sat.ml b/src/sat/sat.ml index 7dd099de247..5a4865bdbe5 100644 --- a/src/sat/sat.ml +++ b/src/sat/sat.ml @@ -112,7 +112,7 @@ module Make (User : USER) = struct and undo = | Undo_at_most_one of lit option ref - | Decided of t + | Decided and var = { id : VarID.t (* A unique ID, used to test identity *) @@ -130,7 +130,7 @@ module Make (User : USER) = struct and lit = sign * var - and t = + type t = { id_maker : VarID.mint ; (* Propagation *) mutable vars : var list @@ -245,9 +245,9 @@ module Make (User : USER) = struct | Neg -> Pp.text "not(" ++ User.pp var.obj ++ Pp.char ')' ;; - let undo undo lit = + let undo problem undo lit = match undo with - | Decided problem -> problem.set_to_false <- false + | Decided -> problem.set_to_false <- false | Undo_at_most_one current -> if debug then @@ -342,7 +342,7 @@ module Make (User : USER) = struct while var_info.undo <> [] do let cb = List.hd var_info.undo in var_info.undo <- List.tl var_info.undo; - undo cb lit + undo problem cb lit done ;; @@ -876,7 +876,7 @@ module Make (User : USER) = struct | None -> (* Switch to set_to_false mode (until we backtrack). *) problem.set_to_false <- true; - undecided.undo <- Decided problem :: undecided.undo; + undecided.undo <- Decided :: undecided.undo; (* Printf.printf "%s -> false\n" (name_lit undecided); *) Neg, undecided) in