Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

refactor(sat): remove useless argument of [Decided] #11413

Merged
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions src/sat/sat.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand All @@ -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
Expand Down Expand Up @@ -232,9 +232,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
Expand Down Expand Up @@ -329,7 +329,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
;;

Expand Down Expand Up @@ -874,7 +874,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
Expand Down
Loading