simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

refactor: fix sudoku example

Browse source
This commit is contained in:
Simon Cruanes 2022-10-12 22:20:43 -04:00
parent a6d3ed259f
commit 032be221a3
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
examples/sudoku/sudoku_solve.ml
View file

@ -1,6 +1,7 @@
(** simple sudoku solver *)
open Sidekick_util
module Proof = Sidekick_proof
let errorf msg = Fmt.kasprintf failwith msg
@ -214,7 +215,7 @@ end = struct
mk_cell_lit self.tst x y (Cell.make (c + 1)))
in
Log.debugf 4 (fun k -> k "(@[add-clause@ %a@])" pp_c_ c);
A.add_clause ~keep:true c Proof_trace.dummy_step_id
A.add_clause ~keep:true c @@ fun () -> Proof.Pterm.dummy
))
(* check constraints *)
@ -242,7 +243,7 @@ end = struct
in
Stat.incr self.stat_conflict;
logs_conflict c_kind c;
A.raise_conflict c Proof_trace.dummy_step_id
A.raise_conflict c @@ fun () -> Proof.Pterm.dummy
))
in
all_diff "rows" Grid.rows;
@ -274,7 +275,7 @@ end = struct
]
in
logs_conflict "at-most-one" c;
A.raise_conflict c Proof_trace.dummy_step_id
A.raise_conflict c @@ fun () -> Proof.Pterm.dummy
)
| _ -> ())
@ -334,7 +335,7 @@ end = struct
let plugin : Sat.plugin = Theory.to_plugin theory in
{
tst;
solver = Sat.create ~stat ~proof:Proof_trace.dummy plugin;
solver = Sat.create ~stat ~tracer:Sat.Tracer.dummy plugin;
theory;
grid0 = g;
}