refactor: use a vec for the new clauses

src/core/Internal.ml

@@ -721,8 +721,7 @@ module Make(Plugin : PLUGIN)
     clauses_learnt : clause Vec.t;
     (* learnt clauses (tautologies true at any time, whatever the user level) *)
 
-    (* TODO: make this a Vec.t *)
-    clauses_to_add : clause Stack.t;
+    clauses_to_add : clause Vec.t;
     (* Clauses either assumed or pushed by the theory, waiting to be added. *)
 
     mutable unsat_at_0: clause option;
@@ -789,7 +788,7 @@ module Make(Plugin : PLUGIN)
     clauses_hyps = Vec.create();
     clauses_learnt = Vec.create();
 
-    clauses_to_add = Stack.create ();
+    clauses_to_add = Vec.create ();
     to_clear=Vec.create();
 
     th_head = 0;
@@ -1505,13 +1504,14 @@ module Make(Plugin : PLUGIN)
       Vec.push vec init;
       Log.debugf info (fun k->k "Trivial clause ignored : @[%a@]" Clause.debug init)
 
-  let flush_clauses st =
-    if not (Stack.is_empty st.clauses_to_add) then (
-      while not (Stack.is_empty st.clauses_to_add) do
-        let c = Stack.pop st.clauses_to_add in
-        add_clause_ st c
-      done
-    )
+  let[@inline never] flush_clauses_ st =
+    while not @@ Vec.is_empty st.clauses_to_add do
+      let c = Vec.pop st.clauses_to_add in
+      add_clause_ st c
+    done
+
+  let[@inline] flush_clauses st =
+    if not @@ Vec.is_empty st.clauses_to_add then flush_clauses_ st
 
   type watch_res =
     | Watch_kept
@@ -1616,7 +1616,7 @@ module Make(Plugin : PLUGIN)
     let c = Clause.make atoms (Lemma lemma) in
     if not keep then Clause.set_learnt c true;
     Log.debugf info (fun k->k "Pushing clause %a" Clause.debug c);
-    Stack.push c st.clauses_to_add
+    Vec.push st.clauses_to_add c
 
   let slice_raise st (l:formula list) proof : 'a =
     let atoms = List.rev_map (create_atom st) l in
@@ -1634,7 +1634,7 @@ module Make(Plugin : PLUGIN)
         let c = Clause.make (p :: List.map Atom.neg l) (Lemma proof) in
         if p.is_true then ()
         else if p.neg.is_true then (
-          Stack.push c st.clauses_to_add
+          Vec.push st.clauses_to_add c
         ) else (
           insert_subterms_order st p.var;
           let level = List.fold_left (fun acc a -> max acc a.var.v_level) 0 l in
@@ -1695,6 +1695,7 @@ module Make(Plugin : PLUGIN)
       st.th_head <- st.elt_head; (* catch up *)
       match Plugin.assume st.th slice with
       | () ->
+        flush_clauses st;
         propagate st
       | exception Th_conflict c ->
         check_is_conflict_ c;
@@ -1919,15 +1920,17 @@ module Make(Plugin : PLUGIN)
             begin match Plugin.if_sat st.th (full_slice st) with
               | () ->
                 if st.elt_head = Vec.size st.trail &&
-                   Stack.is_empty st.clauses_to_add then (
+                   Vec.is_empty st.clauses_to_add then (
                   raise_notrace E_sat
                 );
                 (* otherwise, keep on *)
+                flush_clauses st;
               | exception Th_conflict c ->
                 check_is_conflict_ c;
                 Array.iter (fun a -> insert_var_order st (Elt.of_var a.var)) c.atoms;
                 Log.debugf info (fun k -> k "Theory conflict clause: %a" Clause.debug c);
-                Stack.push c st.clauses_to_add
+                Vec.push st.clauses_to_add c;
+                flush_clauses st;
             end;
         end
       done
@@ -1939,7 +1942,7 @@ module Make(Plugin : PLUGIN)
          let atoms = List.rev_map (mk_atom st) l in
          let c = Clause.make atoms Hyp in
          Log.debugf debug (fun k -> k "Assuming clause: @[<hov 2>%a@]" Clause.debug c);
-         Stack.push c st.clauses_to_add)
+         Vec.push st.clauses_to_add c)
       cnf
 
   (* Check satisfiability *)
@@ -1967,7 +1970,7 @@ module Make(Plugin : PLUGIN)
       false
 
   let check st : bool =
-    Stack.is_empty st.clauses_to_add &&
+    Vec.is_empty st.clauses_to_add &&
     check_vec st.clauses_hyps &&
     check_vec st.clauses_learnt
 

src/sudoku/dune

@@ -0,0 +1,9 @@
+
+(executable
+  (name sudoku_solve)
+  (modes native)
+  (libraries msat sequence containers)
+  (flags :standard -warn-error -a -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)
+  (ocamlopt_flags :standard -O3 -bin-annot
+                  -unbox-closures -unbox-closures-factor 20)
+)

src/sudoku/sudoku_solve.ml

@@ -0,0 +1,346 @@
+
+(** {1 simple sudoku solver} *)
+
+module Fmt = CCFormat
+module Log = Msat.Log
+module Vec = Msat.Vec
+
+let errorf msg = CCFormat.kasprintf failwith msg
+
+module Cell : sig
+  type t = private int
+  val equal : t -> t -> bool
+  val neq : t -> t -> bool
+  val hash : t -> int
+  val empty : t
+  val is_empty : t -> bool
+  val is_full : t -> bool
+  val make : int -> t
+  val pp : t Fmt.printer
+end = struct
+  type t = int
+  let empty = 0
+  let[@inline] make i = assert (i >= 0 && i <= 9); i
+  let[@inline] is_empty x = x = 0
+  let[@inline] is_full x = x > 0
+  let hash = CCHash.int
+  let[@inline] equal (a:t) b = a=b
+  let[@inline] neq (a:t) b = a<>b
+  let pp out i = if i=0 then Fmt.char out '.' else Fmt.int out i
+end
+
+module Grid : sig
+  type t
+
+  val get : t -> int -> int -> Cell.t
+  val set : t -> int -> int -> Cell.t -> t
+
+  (** A set of related cells *)
+  type set = (int*int*Cell.t) Sequence.t
+
+  val rows : t -> set Sequence.t
+  val cols : t -> set Sequence.t
+  val squares : t -> set Sequence.t
+
+  val all_cells : t -> (int*int*Cell.t) Sequence.t
+
+  val parse : string -> t
+  val is_full : t -> bool
+  val is_valid : t -> bool
+  val pp : t Fmt.printer
+end = struct
+  type t = Cell.t array
+
+  let[@inline] get (s:t) i j = s.(i*9 + j)
+
+  let[@inline] set (s:t) i j n =
+    let s' = Array.copy s in
+    s'.(i*9 + j) <- n;
+    s'
+
+  (** A set of related cells *)
+  type set = (int*int*Cell.t) Sequence.t
+
+  open Sequence.Infix
+
+  let all_cells (g:t) =
+    0 -- 8 >>= fun i ->
+    0 -- 8 >|= fun j -> (i,j,get g i j)
+
+  let rows (g:t) =
+    0 -- 8 >|= fun i ->
+    ( 0 -- 8 >|= fun j -> (i,j,get g i j))
+
+  let cols g =
+    0 -- 8 >|= fun j ->
+    ( 0 -- 8 >|= fun i -> (i,j,get g i j))
+
+  let squares g =
+    0 -- 2 >>= fun sq_i ->
+    0 -- 2 >|= fun sq_j ->
+    ( 0 -- 2 >>= fun off_i ->
+      0 -- 2 >|= fun off_j ->
+      let i = 3*sq_i + off_i in
+      let j = 3*sq_j + off_j in
+      (i,j,get g i j))
+
+  let is_full g = Array.for_all Cell.is_full g
+
+  let is_valid g =
+    let all_distinct (s:set) =
+      (s >|= fun (_,_,c) -> c)
+      |> Sequence.diagonal
+      |> Sequence.for_all (fun (c1,c2) -> Cell.neq c1 c2)
+    in
+    Sequence.for_all all_distinct @@ rows g &&
+    Sequence.for_all all_distinct @@ cols g &&
+    Sequence.for_all all_distinct @@ squares g
+
+  let pp out g =
+    Fmt.fprintf out "@[<v>";
+    Array.iteri
+      (fun i n ->
+         Cell.pp out n;
+         if i mod 9 = 8 then Fmt.fprintf out "@,")
+      g;
+    Fmt.fprintf out "@]"
+
+  let parse (s:string) : t =
+    if String.length s < 81 then (
+      errorf "line is too short, expected 81 chars, not %d" (String.length s);
+    );
+    let a = Array.make 81 Cell.empty in
+    for i = 0 to 80 do
+      let c = String.get s i in
+      let n = if c = '.' then 0 else Char.code c - Char.code '0' in
+      if n < 0 || n > 9 then errorf "invalid char %c" c;
+      a.(i) <- Cell.make n
+    done;
+    a
+end
+
+(** Backtrackable ref *)
+module B_ref : sig
+  type 'a t
+  val create : 'a -> 'a t
+  val set : 'a t -> 'a -> unit
+  val get : 'a t -> 'a
+  val update : 'a t -> ('a -> 'a) -> unit
+  val push_level : _ t -> unit
+  val pop_levels : _ t -> int -> unit
+end = struct
+  type 'a t = {
+    mutable cur: 'a;
+    stack: 'a Vec.t;
+  }
+
+  let create x: _ t = {cur=x; stack=Vec.create()}
+
+  let[@inline] get self = self.cur
+  let[@inline] set self x = self.cur <- x
+  let[@inline] update self f = self.cur <- f self.cur
+
+  let[@inline] push_level self : unit = Vec.push self.stack self.cur
+  let pop_levels self n : unit =
+    assert (n>=0 && n <= Vec.size self.stack);
+    let i = Vec.size self.stack-n in
+    let x = Vec.get self.stack i in
+    self.cur <- x;
+    Vec.shrink self.stack i;
+    ()
+end
+
+module Solver : sig
+  type t
+  val create : Grid.t -> t
+  val solve : t -> Grid.t option
+end = struct
+  open Msat.Solver_intf
+
+  (* formulas *)
+  module F = struct
+    type t = bool*int*int*Cell.t
+    let equal (sign1,x1,y1,c1)(sign2,x2,y2,c2) =
+      sign1=sign2 && x1=x2 && y1=y2 && Cell.equal c1 c2
+    let hash (sign,x,y,c) = CCHash.(combine4 (bool sign)(int x)(int y)(Cell.hash c))
+    let pp out (sign,x,y,c) =
+      Fmt.fprintf out "[@[(%d,%d) %s %a@]]" x y (if sign then "=" else "!=") Cell.pp c
+    let neg (sign,x,y,c) = (not sign,x,y,c)
+    let norm ((sign,_,_,_) as f) =
+      if sign then f, Same_sign else neg f, Negated
+
+    let make sign x y (c:Cell.t) : t = (sign,x,y,c)
+  end
+
+  module Theory = struct
+    type proof = unit
+    module Formula = F
+    type t = {
+      grid: Grid.t B_ref.t;
+    }
+
+    let create g : t = {grid=B_ref.create g}
+    let[@inline] grid self : Grid.t = B_ref.get self.grid
+    let[@inline] set_grid self g : unit = B_ref.set self.grid g
+
+    let push_level self = B_ref.push_level self.grid
+    let pop_levels self n = B_ref.pop_levels self.grid n
+
+    let pp_c_ = Fmt.(list ~sep:(return "@ ∨ ")) F.pp
+    let[@inline] logs_conflict kind c : unit =
+      Log.debugf 4 (fun k->k "(@[conflict.%s@ %a@])" kind pp_c_ c)
+
+    (* check that all cells are full *)
+    let check_full_ (self:t) acts : unit =
+      Grid.all_cells (grid self)
+        (fun (x,y,c) ->
+           if Cell.is_empty c then (
+             let c =
+               CCList.init 9
+                 (fun c -> F.make true x y (Cell.make (c+1)))
+             in
+             Log.debugf 4 (fun k->k "(@[add-clause@ %a@])" pp_c_ c);
+             acts.push ~keep:true c ();
+           ))
+
+    (* check constraints *)
+    let check_ (self:t) acts : unit =
+      Log.debugf 4 (fun k->k "(@[sudoku.check@ @[:g %a@]@])" Grid.pp (B_ref.get self.grid));
+      let[@inline] all_diff kind f =
+        let pairs =
+          f (grid self)
+          |> Sequence.flat_map
+            (fun set ->
+               set
+               |> Sequence.filter (fun (_,_,c) -> Cell.is_full c)
+               |> Sequence.diagonal)
+        in
+        pairs
+          (fun ((x1,y1,c1),(x2,y2,c2)) ->
+             if Cell.equal c1 c2 then (
+               assert (x1<>x2 || y1<>y2);
+               let c = [F.make false x1 y1 c1; F.make false x2 y2 c2] in
+               logs_conflict ("all-diff." ^ kind) c;
+               acts.raise_conflict c ()
+             ))
+      in
+      all_diff "rows" Grid.rows;
+      all_diff "cols" Grid.cols;
+      all_diff "squares" Grid.squares;
+      ()
+
+    let trail_ acts = 
+      acts.iter_assumptions
+      |> Sequence.map
+        (function
+          | Assign _ -> assert false
+          | Lit f -> f)
+
+    (* update current grid with the given slice *)
+    let add_slice (self:t) acts : unit =
+      trail_ acts
+        (function
+          | false,_,_,_ -> ()
+          | true,x,y,c ->
+            assert (Cell.is_full c);
+            let grid = grid self in
+            let c' = Grid.get grid x y in
+            if Cell.is_empty c' then (
+              set_grid self (Grid.set grid x y c);
+            ) else if Cell.neq c c' then (
+              (* conflict: at most one value *)
+              let c = [F.make false x y c; F.make false x y c'] in
+              logs_conflict "at-most-one" c;
+              acts.raise_conflict c ()
+            )
+        )
+
+    let assume (self:t) acts : unit =
+      Log.debugf 4
+        (fun k->k "(@[sudoku.assume@ :trail [@[%a@]]@])" (Fmt.seq F.pp) (trail_ acts));
+      add_slice self acts;
+      check_ self acts
+
+    let if_sat (self:t) acts : unit =
+      Log.debugf 4 (fun k->k "(@[sudoku.if-sat@])");
+      check_full_ self acts;
+      check_ self acts
+
+  end
+
+  module S = Msat.Make_cdcl_t(Theory)
+
+  type t = {
+    grid0: Grid.t;
+    solver: S.t;
+  }
+
+  let solve (self:t) : _ option =
+    let assumptions =
+      Grid.all_cells self.grid0
+      |> Sequence.filter (fun (_,_,c) -> Cell.is_full c)
+      |> Sequence.map (fun (x,y,c) -> F.make true x y c)
+      |> Sequence.map (S.make_atom self.solver)
+      |> Sequence.to_rev_list
+    in
+    Log.debugf 2
+      (fun k->k "(@[sudoku.solve@ :assumptions %a@])" (Fmt.Dump.list S.Atom.pp) assumptions);
+    let r =
+      match S.solve self.solver ~assumptions () with
+      | S.Sat _ -> Some (Theory.grid (S.theory self.solver))
+      | S.Unsat _ -> None
+    in
+    (* TODO: print some stats *)
+    r
+
+  let create g : t =
+    { solver=S.create (Theory.create g); grid0=g }
+end
+
+let solve_grid (g:Grid.t) : Grid.t option =
+  let s = Solver.create g in
+  Solver.solve s
+
+let solve_file file =
+  let grids =
+    CCIO.with_in file CCIO.read_lines_l
+    |> CCList.filter_map
+      (fun s ->
+         let s = String.trim s in
+         if s="" then None
+         else match Grid.parse s with
+           | g -> Some g
+           | exception e ->
+             errorf "cannot parse sudoku %S: %s@." s (Printexc.to_string e))
+  in
+  List.iter
+    (fun g ->
+       Format.printf "@[<v>@,#########################@,@[<2>solve grid:@ %a@]@]@." Grid.pp g;
+       let start=Sys.time() in
+       match solve_grid g with
+       | None -> Format.printf "no solution (in %.3fs)@." (Sys.time()-.start)
+       | Some g' when not @@ Grid.is_full g' ->
+         errorf "grid %a@ is not full" Grid.pp g'
+       | Some g' when not @@ Grid.is_valid g' ->
+         errorf "grid %a@ is not valid" Grid.pp g'
+       | Some g' ->
+         Format.printf "@[<v>@[<2>solution (in %.3fs):@ %a@]@,###################@]@."
+           (Sys.time()-.start) Grid.pp g')
+    grids
+
+let () =
+  Fmt.set_color_default true;
+  let files = ref [] in
+  let debug = ref 0 in
+  let opts = [
+    "--debug", Arg.Set_int debug, " debug";
+    "-d", Arg.Set_int debug, " debug";
+  ] |> Arg.align in
+  Arg.parse opts (fun f -> files := f :: !files) "sudoku_solve [options] <file>";
+  Msat.Log.set_debug !debug;
+  try
+    List.iter (fun f -> solve_file f) !files;
+  with
+  | Failure msg | Invalid_argument msg ->
+    Format.printf "@{<Red>Error@}:@.%s@." msg;
+    exit 1

sudoku_solve.sh

@@ -0,0 +1,4 @@
+#!/bin/sh
+
+#exec dune exec src/sudoku/sudoku_solve.exe -- $@
+exec dune exec --profile=release src/sudoku/sudoku_solve.exe -- $@

tests/sudoku/Makefile

@@ -0,0 +1,10 @@
+
+sudoku17.txt:
+	wget https://github.com/attractivechaos/plb/releases/download/v0/sudoku17.txt.gz -O sudoku17.txt.gz
+	gunzip -f sudoku17.txt.gz
+
+top50k.txt:
+	wget https://github.com/attractivechaos/plb/releases/download/v0/sudoku.top50k.gz -O top50k.txt.gz
+	gunzip -f top50k.txt.gz
+
+fetch-all: sudoku17.txt top50k.txt

tests/sudoku/sudoku.txt

@@ -0,0 +1,20 @@
+..............3.85..1.2.......5.7.....4...1...9.......5......73..2.1........4...9	near worst case for brute-force solver (wiki)
+.......12........3..23..4....18....5.6..7.8.......9.....85.....9...4.5..47...6...	gsf's sudoku q1 (Platinum Blonde)
+.2..5.7..4..1....68....3...2....8..3.4..2.5.....6...1...2.9.....9......57.4...9..	(Cheese)
+........3..1..56...9..4..7......9.5.7.......8.5.4.2....8..2..9...35..1..6........	(Fata Morgana)
+12.3....435....1....4........54..2..6...7.........8.9...31..5.......9.7.....6...8	(Red Dwarf)
+1.......2.9.4...5...6...7...5.9.3.......7.......85..4.7.....6...3...9.8...2.....1	(Easter Monster)
+.......39.....1..5..3.5.8....8.9...6.7...2...1..4.......9.8..5..2....6..4..7.....	Nicolas Juillerat's Sudoku explainer 1.2.1 (top 5)
+12.3.....4.....3....3.5......42..5......8...9.6...5.7...15..2......9..6......7..8
+..3..6.8....1..2......7...4..9..8.6..3..4...1.7.2.....3....5.....5...6..98.....5.
+1.......9..67...2..8....4......75.3...5..2....6.3......9....8..6...4...1..25...6.
+..9...4...7.3...2.8...6...71..8....6....1..7.....56...3....5..1.4.....9...2...7..
+....9..5..1.....3...23..7....45...7.8.....2.......64...9..1.....8..6......54....7	dukuso's suexrat9 (top 1)
+4...3.......6..8..........1....5..9..8....6...7.2........1.27..5.3....4.9........	from http://magictour.free.fr/topn87 (top 3)
+7.8...3.....2.1...5.........4.....263...8.......1...9..9.6....4....7.5...........
+3.7.4...........918........4.....7.....16.......25..........38..9....5...2.6.....
+........8..3...4...9..2..6.....79.......612...6.5.2.7...8...5...1.....2.4.5.....3	dukuso's suexratt (top 1)
+.......1.4.........2...........5.4.7..8...3....1.9....3..4..2...5.1........8.6...	first 2 from sudoku17
+.......12....35......6...7.7.....3.....4..8..1...........12.....8.....4..5....6..
+1.......2.9.4...5...6...7...5.3.4.......6........58.4...2...6...3...9.8.7.......1	2 from http://www.setbb.com/phpbb/viewtopic.php?p=10478
+.....1.2.3...4.5.....6....7..2.....1.8..9..3.4.....8..5....2....9..3.4....67.....