Sudoku

In this notebook we're going to use Imandra to reason about the classic kind of puzzle that you can find everywhere.

(note: this example was adapted from code from Koen Claessen and Dan Rosén)

We're going to define what a sudoku puzzle is, and how to check if a given sudoku is a solution. From that we can get Imandra to find solutions for us, without actually writing a sudoku solver.

Helpers

We're going to define a sudoku as a 9×9 grid.

Numbers

However, for now, the bounded model checker that comes along with Imandra doesn't handle numbers. We do not need much here besides length, so a unary notation (classic Peano arithmetic) will do.

In [1]:
type nat = Z | S of nat;;

(* readability matters, so we write a pretty-printer for nats *)
let rec int_of_nat = function Z -> 0i | S n -> Caml.Int.(1i + int_of_nat n) [@@program]
let pp_nat out n = Format.fprintf out "%d" (int_of_nat n) [@@program];;
#install_printer pp_nat;;
Out[1]:
type nat = Z | S of nat
val int_of_nat : nat -> int/2 = <fun>
val pp_nat : Format.formatter -> nat -> unit = <fun>
In [2]:
let rec length = function
  | [] -> Z
  | _ :: tl -> S (length tl)

let n3 = S (S (S Z));;
let n6 = S (S (S n3));;
let n9 = S (S (S n6));;
Out[2]:
val length : 'a list -> nat = <fun>
val n3 : nat = 3
val n6 : nat = 6
val n9 : nat = 9
termination proof

Termination proof

call `length (List.tl _x)` from `length _x`
originallength _x
sublength (List.tl _x)
original ordinalOrdinal.Int (Ordinal.count _x)
sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
path[not (_x = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.014s
details
Expand
smt_stats
num checks7
arith-make-feasible10
arith-max-columns13
arith-conflicts1
rlimit count1912
arith-cheap-eqs2
mk clause3
datatype occurs check22
mk bool var46
arith-lower5
datatype splits3
decisions10
propagations1
arith-max-rows5
conflicts7
datatype accessor ax5
datatype constructor ax8
num allocs839886768
final checks6
added eqs33
del clause1
arith eq adapter3
arith-upper5
memory22.140000
max memory24.710000
Expand
  • start[0.014s]
      let (_x_0 : int) = Ordinal.count _x in
      let (_x_1 : ty_0 list) = List.tl _x in
      let (_x_2 : int) = Ordinal.count _x_1 in
      not (_x = []) && _x_0 >= 0 && _x_2 >= 0
      ==> _x_1 = [] || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
  • simplify
    into
    let (_x_0 : ty_0 list) = List.tl _x in
    let (_x_1 : int) = Ordinal.count _x_0 in
    let (_x_2 : int) = Ordinal.count _x in
    (_x_0 = [] || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
    || not ((not (_x = []) && _x_2 >= 0) && _x_1 >= 0)
    expansions
    []
    rewrite_steps
      forward_chaining
      • unroll
        expr
        (|count_`ty_0 list`_2447| _x_2438)
        expansions
        • unroll
          expr
          (|count_`ty_0 list`_2447| (|get.::.1_2433| _x_2438))
          expansions
          • unroll
            expr
            (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`ty_0 list`_2447|
                                                  …
            expansions
            • Unsat

            Rows, columns, blocks

            Sudokus have some constraints that work on rows, and some that work on columns. Using a transpose function we can always work on rows.

            In [3]:
            (** helper for {!transpose} *)
            let rec transpose3 = function
              | [] -> []
              | [] :: tl -> transpose3 tl
              | (_::t) :: tl -> t :: transpose3 tl
            
            let rec get_heads = function
              | [] -> []
              | [] :: tl -> get_heads tl
              | (h :: _) :: tl -> h :: get_heads tl
            ;;
            
            (** We need a custom termination function here *)
            let measure_transpose = function
            | [] -> 0
            | x :: _ -> List.length x
            ;;
            
            (** Transpose rows and columns in a list of lists *)
            let rec transpose l =
              match l with
              | [] -> []
              | [] :: _ -> []
              | (x1 :: xs) :: xss ->
                (x1 :: get_heads xss) :: transpose (xs :: transpose3 xss)
            [@@measure Ordinal.of_int (measure_transpose l)]
            ;;
            
            Out[3]:
            val transpose3 : 'a list list -> 'a list list = <fun>
            val get_heads : 'a list list -> 'a list = <fun>
            val measure_transpose : 'a list list -> int = <fun>
            val transpose : 'a list list -> 'a list list = <fun>
            
            termination proof

            Termination proof

            call `transpose3 (List.tl _x)` from `transpose3 _x`
            originaltranspose3 _x
            subtranspose3 (List.tl _x)
            original ordinalOrdinal.Int (Ordinal.count _x)
            sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
            path[_x <> [] && List.hd _x = [] && not (_x = [])]
            proof
            detailed proof
            ground_instances3
            definitions0
            inductions0
            search_time
            0.019s
            details
            Expand
            smt_stats
            num checks8
            arith-make-feasible27
            arith-max-columns19
            arith-conflicts2
            rlimit count6417
            mk clause44
            datatype occurs check46
            mk bool var122
            arith-lower19
            datatype splits11
            decisions36
            propagations77
            arith-max-rows7
            conflicts13
            datatype accessor ax13
            datatype constructor ax20
            num allocs916121284
            final checks10
            added eqs101
            del clause16
            arith eq adapter13
            arith-upper18
            memory25.580000
            max memory25.580000
            Expand
            • start[0.019s]
                let (_x_0 : int) = Ordinal.count _x in
                let (_x_1 : ty_0 list list) = List.tl _x in
                let (_x_2 : int) = Ordinal.count _x_1 in
                let (_x_3 : bool) = _x_1 <> [] && List.hd _x_1 = [] in
                let (_x_4 : bool) = not (_x_1 = []) in
                (_x <> [] && List.hd _x = []) && not (_x = []) && _x_0 >= 0 && _x_2 >= 0
                ==> not (_x_3 && _x_4) && not (not _x_3 && _x_4)
                    || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
            • simplify
              into
              let (_x_0 : ty_0 list list) = List.tl _x in
              let (_x_1 : int) = Ordinal.count _x_0 in
              let (_x_2 : int) = Ordinal.count _x in
              let (_x_3 : bool) = _x_0 <> [] && List.hd _x_0 = [] in
              let (_x_4 : bool) = not (_x_0 = []) in
              (Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
               || not (_x_3 && _x_4) && not (not _x_3 && _x_4))
              || not
                 ((((_x <> [] && List.hd _x = []) && not (_x = [])) && _x_2 >= 0)
                  && _x_1 >= 0)
              expansions
              []
              rewrite_steps
                forward_chaining
                • unroll
                  expr
                  (|count_`ty_0 list list`_2495| _x_2484)
                  expansions
                  • unroll
                    expr
                    (|count_`ty_0 list list`_2495| (|get.::.1_2478| _x_2484))
                    expansions
                    • unroll
                      expr
                      (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`ty_0 list list`_2495|
                                                       …
                      expansions
                      • Unsat

                      call `transpose3 (List.tl _x)` from `transpose3 _x`
                      originaltranspose3 _x
                      subtranspose3 (List.tl _x)
                      original ordinalOrdinal.Int (Ordinal.count _x)
                      sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
                      path[not (_x <> [] && List.hd _x = []) && not (_x = [])]
                      proof
                      detailed proof
                      ground_instances3
                      definitions0
                      inductions0
                      search_time
                      0.018s
                      details
                      Expand
                      smt_stats
                      num checks8
                      arith-make-feasible28
                      arith-max-columns19
                      arith-conflicts2
                      rlimit count3228
                      mk clause40
                      datatype occurs check43
                      mk bool var103
                      arith-lower20
                      datatype splits10
                      decisions44
                      propagations71
                      arith-max-rows7
                      conflicts14
                      datatype accessor ax7
                      datatype constructor ax14
                      num allocs892606628
                      final checks8
                      added eqs79
                      del clause15
                      arith eq adapter14
                      arith-upper20
                      memory23.030000
                      max memory24.710000
                      Expand
                      • start[0.018s]
                          let (_x_0 : int) = Ordinal.count _x in
                          let (_x_1 : ty_0 list list) = List.tl _x in
                          let (_x_2 : int) = Ordinal.count _x_1 in
                          let (_x_3 : bool) = _x_1 <> [] && List.hd _x_1 = [] in
                          let (_x_4 : bool) = not (_x_1 = []) in
                          not (_x <> [] && List.hd _x = [])
                          && not (_x = []) && _x_0 >= 0 && _x_2 >= 0
                          ==> not (_x_3 && _x_4) && not (not _x_3 && _x_4)
                              || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                      • simplify
                        into
                        let (_x_0 : ty_0 list list) = List.tl _x in
                        let (_x_1 : int) = Ordinal.count _x_0 in
                        let (_x_2 : int) = Ordinal.count _x in
                        let (_x_3 : bool) = _x_0 <> [] && List.hd _x_0 = [] in
                        let (_x_4 : bool) = not (_x_0 = []) in
                        (Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
                         || not (_x_3 && _x_4) && not (not _x_3 && _x_4))
                        || not
                           (((not (_x <> [] && List.hd _x = []) && not (_x = [])) && _x_2 >= 0)
                            && _x_1 >= 0)
                        expansions
                        []
                        rewrite_steps
                          forward_chaining
                          • unroll
                            expr
                            (|count_`ty_0 list list`_2495| _x_2484)
                            expansions
                            • unroll
                              expr
                              (|count_`ty_0 list list`_2495| (|get.::.1_2478| _x_2484))
                              expansions
                              • unroll
                                expr
                                (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`ty_0 list list`_2495|
                                                                 …
                                expansions
                                • Unsat

                                termination proof

                                Termination proof

                                call `get_heads (List.tl _x)` from `get_heads _x`
                                originalget_heads _x
                                subget_heads (List.tl _x)
                                original ordinalOrdinal.Int (Ordinal.count _x)
                                sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
                                path[_x <> [] && List.hd _x = [] && not (_x = [])]
                                proof
                                detailed proof
                                ground_instances3
                                definitions0
                                inductions0
                                search_time
                                0.037s
                                details
                                Expand
                                smt_stats
                                num checks8
                                arith-make-feasible27
                                arith-max-columns19
                                arith-conflicts2
                                rlimit count6425
                                mk clause44
                                datatype occurs check46
                                mk bool var122
                                arith-lower19
                                datatype splits11
                                decisions36
                                propagations77
                                arith-max-rows7
                                conflicts13
                                datatype accessor ax13
                                datatype constructor ax20
                                num allocs1039427428
                                final checks10
                                added eqs101
                                del clause16
                                arith eq adapter13
                                arith-upper18
                                memory23.410000
                                max memory25.900000
                                Expand
                                • start[0.037s]
                                    let (_x_0 : int) = Ordinal.count _x in
                                    let (_x_1 : ty_0 list list) = List.tl _x in
                                    let (_x_2 : int) = Ordinal.count _x_1 in
                                    let (_x_3 : bool) = _x_1 <> [] && List.hd _x_1 = [] in
                                    let (_x_4 : bool) = not (_x_1 = []) in
                                    (_x <> [] && List.hd _x = []) && not (_x = []) && _x_0 >= 0 && _x_2 >= 0
                                    ==> not (_x_3 && _x_4) && not (not _x_3 && _x_4)
                                        || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                • simplify
                                  into
                                  let (_x_0 : ty_0 list list) = List.tl _x in
                                  let (_x_1 : int) = Ordinal.count _x_0 in
                                  let (_x_2 : int) = Ordinal.count _x in
                                  let (_x_3 : bool) = _x_0 <> [] && List.hd _x_0 = [] in
                                  let (_x_4 : bool) = not (_x_0 = []) in
                                  (Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
                                   || not (_x_3 && _x_4) && not (not _x_3 && _x_4))
                                  || not
                                     ((((_x <> [] && List.hd _x = []) && not (_x = [])) && _x_2 >= 0)
                                      && _x_1 >= 0)
                                  expansions
                                  []
                                  rewrite_steps
                                    forward_chaining
                                    • unroll
                                      expr
                                      (|count_`ty_0 list list`_2586| _x_2575)
                                      expansions
                                      • unroll
                                        expr
                                        (|count_`ty_0 list list`_2586| (|get.::.1_2569| _x_2575))
                                        expansions
                                        • unroll
                                          expr
                                          (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`ty_0 list list`_2586|
                                                                           …
                                          expansions
                                          • Unsat

                                          call `get_heads (List.tl _x)` from `get_heads _x`
                                          originalget_heads _x
                                          subget_heads (List.tl _x)
                                          original ordinalOrdinal.Int (Ordinal.count _x)
                                          sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
                                          path[not (_x <> [] && List.hd _x = []) && not (_x = [])]
                                          proof
                                          detailed proof
                                          ground_instances3
                                          definitions0
                                          inductions0
                                          search_time
                                          0.033s
                                          details
                                          Expand
                                          smt_stats
                                          num checks8
                                          arith-make-feasible28
                                          arith-max-columns19
                                          arith-conflicts2
                                          rlimit count3228
                                          mk clause40
                                          datatype occurs check43
                                          mk bool var103
                                          arith-lower20
                                          datatype splits10
                                          decisions44
                                          propagations71
                                          arith-max-rows7
                                          conflicts14
                                          datatype accessor ax7
                                          datatype constructor ax14
                                          num allocs990751519
                                          final checks8
                                          added eqs79
                                          del clause15
                                          arith eq adapter14
                                          arith-upper20
                                          memory23.320000
                                          max memory25.680000
                                          Expand
                                          • start[0.033s]
                                              let (_x_0 : int) = Ordinal.count _x in
                                              let (_x_1 : ty_0 list list) = List.tl _x in
                                              let (_x_2 : int) = Ordinal.count _x_1 in
                                              let (_x_3 : bool) = _x_1 <> [] && List.hd _x_1 = [] in
                                              let (_x_4 : bool) = not (_x_1 = []) in
                                              not (_x <> [] && List.hd _x = [])
                                              && not (_x = []) && _x_0 >= 0 && _x_2 >= 0
                                              ==> not (_x_3 && _x_4) && not (not _x_3 && _x_4)
                                                  || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                          • simplify
                                            into
                                            let (_x_0 : ty_0 list list) = List.tl _x in
                                            let (_x_1 : int) = Ordinal.count _x_0 in
                                            let (_x_2 : int) = Ordinal.count _x in
                                            let (_x_3 : bool) = _x_0 <> [] && List.hd _x_0 = [] in
                                            let (_x_4 : bool) = not (_x_0 = []) in
                                            (Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
                                             || not (_x_3 && _x_4) && not (not _x_3 && _x_4))
                                            || not
                                               (((not (_x <> [] && List.hd _x = []) && not (_x = [])) && _x_2 >= 0)
                                                && _x_1 >= 0)
                                            expansions
                                            []
                                            rewrite_steps
                                              forward_chaining
                                              • unroll
                                                expr
                                                (|count_`ty_0 list list`_2586| _x_2575)
                                                expansions
                                                • unroll
                                                  expr
                                                  (|count_`ty_0 list list`_2586| (|get.::.1_2569| _x_2575))
                                                  expansions
                                                  • unroll
                                                    expr
                                                    (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`ty_0 list list`_2586|
                                                                                     …
                                                    expansions
                                                    • Unsat

                                                    termination proof

                                                    Termination proof

                                                    call `transpose ((List.tl (List.hd l)) :: (transpose3 (List.tl l)))` from `transpose l`
                                                    originaltranspose l
                                                    subtranspose ((List.tl (List.hd l)) :: (transpose3 (List.tl l)))
                                                    original ordinallet (_x_0 : int) = measure_transpose l in Ordinal.Int (if _x_0 >= 0 then _x_0 else 0)
                                                    sub ordinallet (_x_0 : int) = measure_transpose ((List.tl (List.hd l)) :: (transpose3 (List.tl l))) in Ordinal.Int (if _x_0 >= 0 then _x_0 else 0)
                                                    path[not (l <> [] && List.hd l = []) && not (l = [])]
                                                    proof
                                                    detailed proof
                                                    ground_instances3
                                                    definitions0
                                                    inductions0
                                                    search_time
                                                    0.015s
                                                    details
                                                    Expand
                                                    smt_stats
                                                    num checks7
                                                    arith-make-feasible12
                                                    arith-max-columns11
                                                    arith-conflicts1
                                                    rlimit count2507
                                                    mk clause6
                                                    datatype occurs check52
                                                    mk bool var65
                                                    arith-lower3
                                                    datatype splits11
                                                    decisions17
                                                    propagations4
                                                    arith-max-rows4
                                                    conflicts8
                                                    datatype accessor ax8
                                                    datatype constructor ax16
                                                    num allocs1068604130
                                                    final checks11
                                                    added eqs50
                                                    del clause6
                                                    arith eq adapter2
                                                    arith-upper5
                                                    memory26.410000
                                                    max memory26.410000
                                                    Expand
                                                    • start[0.015s]
                                                        let (_x_0 : ty_0 list) = List.hd l in
                                                        let (_x_1 : bool) = l = [] in
                                                        let (_x_2 : int) = if _x_1 then 0 else List.length _x_0 in
                                                        let (_x_3 : int) = if _x_2 >= 0 then _x_2 else 0 in
                                                        let (_x_4 : ty_0 list) = List.tl _x_0 in
                                                        let (_x_5 : bool) = _x_4 :: (transpose3 …) = [] in
                                                        let (_x_6 : int) = if _x_5 then 0 else List.length … in
                                                        let (_x_7 : int) = if _x_6 >= 0 then _x_6 else 0 in
                                                        not (l <> [] && _x_0 = []) && not _x_1 && _x_3 >= 0 && _x_7 >= 0
                                                        ==> not (not (true && _x_4 = []) && not _x_5)
                                                            || Ordinal.( << ) (Ordinal.Int _x_7) (Ordinal.Int _x_3)
                                                    • simplify
                                                      into
                                                      let (_x_0 : ty_0 list) = List.hd l in
                                                      let (_x_1 : ty_0 list) = List.tl _x_0 in
                                                      let (_x_2 : int) = List.length _x_1 in
                                                      let (_x_3 : int) = List.length _x_0 in
                                                      let (_x_4 : bool) = l = [] in
                                                      let (_x_5 : bool) = _x_4 || _x_3 >= 0 in
                                                      (_x_1 = []
                                                       || Ordinal.( << ) (Ordinal.Int (if _x_2 >= 0 then _x_2 else 0))
                                                          (Ordinal.Int (if _x_5 then if _x_4 then 0 else _x_3 else 0)))
                                                      || not ((not (l <> [] && _x_0 = []) && not _x_4) && (_x_5 || not _x_5))
                                                      expansions
                                                      []
                                                      rewrite_steps
                                                        forward_chaining
                                                        • unroll
                                                          expr
                                                          (|List.length_2715| (|get.::.0_2691| l_2708))
                                                          expansions
                                                          • unroll
                                                            expr
                                                            (|List.length_2715| (|get.::.1_2689| (|get.::.0_2691| l_2708)))
                                                            expansions
                                                            • unroll
                                                              expr
                                                              (let ((a!1 (>= (|List.length_2715| (|get.::.1_2689| (|get.::.0_2691| l_2708)))
                                                                             0))
                                                                …
                                                              expansions
                                                              • Unsat

                                                              Now we also need to extract 3×3 blocks for the additional constraint that none of them contains a duplicate.

                                                              This require a few helpers on lists and options, nothing too complicated.

                                                              In [4]:
                                                              let rec take (x:nat) l : _ list =
                                                                match x with
                                                                | Z -> []
                                                                | S x' ->
                                                                  match l with
                                                                  | [] -> []
                                                                  | y :: tl -> y :: take x' tl
                                                              
                                                              let rec drop x y =
                                                                match x with
                                                                | Z -> y
                                                                | S x' ->
                                                                  match y with
                                                                  | [] -> []
                                                                  | _ :: y' -> drop x' y'
                                                              
                                                              let rec elem x y =  match y with [] -> false | z :: ys -> x=z || elem x ys ;;
                                                              
                                                              (** Is the list [l] composed of unique elements (without duplicates)? *)
                                                              let rec unique x : bool =
                                                                match x with
                                                                | [] -> true
                                                                | y :: xs -> not (elem y xs) && unique xs
                                                              ;;
                                                              
                                                              (** Keep the elements that are [Some _], drop the others *)
                                                              let rec keep_some_list l =
                                                                match l with
                                                                | [] -> []
                                                                | y :: tail ->
                                                                  let tail = keep_some_list tail in
                                                                  match y with None -> tail | Some x -> x :: tail
                                                              ;;
                                                              
                                                              (** A block is valid if it doesn't contain duplicates *)
                                                              let block_satisfies_constraints x = unique (keep_some_list x) ;;
                                                              
                                                              let rec blocks_3_34 = function
                                                                | [] -> []
                                                                | y :: z -> drop n6 y :: blocks_3_34 z
                                                              ;;
                                                              
                                                              let rec blocks_3_33 = function
                                                                | [] -> []
                                                                | y :: z -> take n3 (drop n3 y) :: blocks_3_33 z
                                                              ;;
                                                              
                                                              let rec blocks_3_32 = function
                                                                | [] -> []
                                                                | y :: z -> take n3 y :: blocks_3_32 z
                                                              ;;
                                                              
                                                              (*
                                                              
                                                              let rec group3 = function
                                                                | xs1 :: xs2 :: xs3 :: xss ->
                                                                  (xs1 @ xs2 @ xs3) :: (group3 xss)
                                                                | _ -> []
                                                                ;;
                                                              *)
                                                              
                                                              let rec group3 = function
                                                                | [] -> []
                                                                | xs1 :: y ->
                                                                  match y with
                                                                  | [] -> []
                                                                  | xs2 :: z ->
                                                                    match z with
                                                                    | [] -> []
                                                                    | xs3 :: xss -> (xs1 @ xs2 @ xs3) :: (group3 xss)
                                                              ;;
                                                              
                                                              let blocks_3_3 l =
                                                                group3 (blocks_3_32 l) @
                                                                  group3 (blocks_3_33 l) @
                                                                    group3 (blocks_3_34 l)
                                                              ;;
                                                              
                                                              Out[4]:
                                                              val take : nat -> 'a list -> 'a list = <fun>
                                                              val drop : nat -> 'a list -> 'a list = <fun>
                                                              val elem : 'a -> 'a list -> bool = <fun>
                                                              val unique : 'a list -> bool = <fun>
                                                              val keep_some_list : 'a option list -> 'a list = <fun>
                                                              val block_satisfies_constraints : 'a option list -> bool = <fun>
                                                              val blocks_3_34 : 'a list list -> 'a list list = <fun>
                                                              val blocks_3_33 : 'a list list -> 'a list list = <fun>
                                                              val blocks_3_32 : 'a list list -> 'a list list = <fun>
                                                              val group3 : 'a list list -> 'a list list = <fun>
                                                              val blocks_3_3 : 'a list list -> 'a list list = <fun>
                                                              
                                                              termination proof

                                                              Termination proof

                                                              call `take (Destruct(S, 0, x)) (List.tl l)` from `take x l`
                                                              originaltake x l
                                                              subtake (Destruct(S, 0, x)) (List.tl l)
                                                              original ordinalOrdinal.Int (Ordinal.count x)
                                                              sub ordinalOrdinal.Int (Ordinal.count (Destruct(S, 0, x)))
                                                              path[not (l = []) && not (x = Z)]
                                                              proof
                                                              detailed proof
                                                              ground_instances3
                                                              definitions0
                                                              inductions0
                                                              search_time
                                                              0.014s
                                                              details
                                                              Expand
                                                              smt_stats
                                                              num checks7
                                                              arith-make-feasible10
                                                              arith-max-columns13
                                                              arith-conflicts1
                                                              rlimit count2114
                                                              mk clause3
                                                              datatype occurs check34
                                                              mk bool var62
                                                              arith-lower4
                                                              datatype splits6
                                                              decisions16
                                                              propagations2
                                                              arith-max-rows5
                                                              conflicts10
                                                              datatype accessor ax8
                                                              datatype constructor ax16
                                                              num allocs1123086517
                                                              final checks6
                                                              added eqs50
                                                              del clause1
                                                              arith eq adapter3
                                                              arith-upper6
                                                              memory26.720000
                                                              max memory26.720000
                                                              Expand
                                                              • start[0.014s]
                                                                  let (_x_0 : int) = Ordinal.count x in
                                                                  let (_x_1 : nat) = Destruct(S, 0, x) in
                                                                  let (_x_2 : int) = Ordinal.count _x_1 in
                                                                  not (l = []) && not (x = Z) && _x_0 >= 0 && _x_2 >= 0
                                                                  ==> not (not (List.tl l = []) && not (_x_1 = Z))
                                                                      || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                              • simplify
                                                                into
                                                                let (_x_0 : nat) = Destruct(S, 0, x) in
                                                                let (_x_1 : int) = Ordinal.count _x_0 in
                                                                let (_x_2 : int) = Ordinal.count x in
                                                                (not (not (List.tl l = []) && not (_x_0 = Z))
                                                                 || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                                                || not (((not (l = []) && not (x = Z)) && _x_2 >= 0) && _x_1 >= 0)
                                                                expansions
                                                                []
                                                                rewrite_steps
                                                                  forward_chaining
                                                                  • unroll
                                                                    expr
                                                                    (count_nat_2795 x_2784)
                                                                    expansions
                                                                    • unroll
                                                                      expr
                                                                      (count_nat_2795 (|get.S.0_2774| x_2784))
                                                                      expansions
                                                                      • unroll
                                                                        expr
                                                                        (|Ordinal.<<_102| (|Ordinal.Int_93| (count_nat_2795 (|get.S.0_2774| x_2784)))
                                                                                          (|Or…
                                                                        expansions
                                                                        • Unsat

                                                                        termination proof

                                                                        Termination proof

                                                                        call `drop (Destruct(S, 0, x)) (List.tl y)` from `drop x y`
                                                                        originaldrop x y
                                                                        subdrop (Destruct(S, 0, x)) (List.tl y)
                                                                        original ordinalOrdinal.Int (Ordinal.count x)
                                                                        sub ordinalOrdinal.Int (Ordinal.count (Destruct(S, 0, x)))
                                                                        path[not (y = []) && not (x = Z)]
                                                                        proof
                                                                        detailed proof
                                                                        ground_instances3
                                                                        definitions0
                                                                        inductions0
                                                                        search_time
                                                                        0.013s
                                                                        details
                                                                        Expand
                                                                        smt_stats
                                                                        num checks7
                                                                        arith-make-feasible10
                                                                        arith-max-columns13
                                                                        arith-conflicts1
                                                                        rlimit count2114
                                                                        mk clause3
                                                                        datatype occurs check34
                                                                        mk bool var62
                                                                        arith-lower4
                                                                        datatype splits6
                                                                        decisions16
                                                                        propagations2
                                                                        arith-max-rows5
                                                                        conflicts10
                                                                        datatype accessor ax8
                                                                        datatype constructor ax16
                                                                        num allocs1177796502
                                                                        final checks6
                                                                        added eqs50
                                                                        del clause1
                                                                        arith eq adapter3
                                                                        arith-upper6
                                                                        memory26.990000
                                                                        max memory26.990000
                                                                        Expand
                                                                        • start[0.013s]
                                                                            let (_x_0 : int) = Ordinal.count x in
                                                                            let (_x_1 : nat) = Destruct(S, 0, x) in
                                                                            let (_x_2 : int) = Ordinal.count _x_1 in
                                                                            not (y = []) && not (x = Z) && _x_0 >= 0 && _x_2 >= 0
                                                                            ==> not (not (List.tl y = []) && not (_x_1 = Z))
                                                                                || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                        • simplify
                                                                          into
                                                                          let (_x_0 : nat) = Destruct(S, 0, x) in
                                                                          let (_x_1 : int) = Ordinal.count _x_0 in
                                                                          let (_x_2 : int) = Ordinal.count x in
                                                                          (not (not (List.tl y = []) && not (_x_0 = Z))
                                                                           || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                                                          || not (((not (y = []) && not (x = Z)) && _x_2 >= 0) && _x_1 >= 0)
                                                                          expansions
                                                                          []
                                                                          rewrite_steps
                                                                            forward_chaining
                                                                            • unroll
                                                                              expr
                                                                              (count_nat_2839 x_2828)
                                                                              expansions
                                                                              • unroll
                                                                                expr
                                                                                (count_nat_2839 (|get.S.0_2819| x_2828))
                                                                                expansions
                                                                                • unroll
                                                                                  expr
                                                                                  (|Ordinal.<<_102| (|Ordinal.Int_93| (count_nat_2839 (|get.S.0_2819| x_2828)))
                                                                                                    (|Or…
                                                                                  expansions
                                                                                  • Unsat

                                                                                  termination proof

                                                                                  Termination proof

                                                                                  call `elem x (List.tl y)` from `elem x y`
                                                                                  originalelem x y
                                                                                  subelem x (List.tl y)
                                                                                  original ordinalOrdinal.Int (Ordinal.count y)
                                                                                  sub ordinalOrdinal.Int (Ordinal.count (List.tl y))
                                                                                  path[not (x = List.hd y) && not (y = [])]
                                                                                  proof
                                                                                  detailed proof
                                                                                  ground_instances3
                                                                                  definitions0
                                                                                  inductions0
                                                                                  search_time
                                                                                  0.014s
                                                                                  details
                                                                                  Expand
                                                                                  smt_stats
                                                                                  num checks7
                                                                                  arith-make-feasible9
                                                                                  arith-max-columns13
                                                                                  arith-conflicts1
                                                                                  rlimit count2026
                                                                                  arith-cheap-eqs2
                                                                                  mk clause3
                                                                                  datatype occurs check19
                                                                                  mk bool var48
                                                                                  arith-lower5
                                                                                  datatype splits3
                                                                                  decisions10
                                                                                  propagations1
                                                                                  arith-max-rows5
                                                                                  conflicts7
                                                                                  datatype accessor ax5
                                                                                  datatype constructor ax8
                                                                                  num allocs1232618098
                                                                                  final checks5
                                                                                  added eqs33
                                                                                  del clause1
                                                                                  arith eq adapter3
                                                                                  arith-upper5
                                                                                  memory27.140000
                                                                                  max memory27.140000
                                                                                  Expand
                                                                                  • start[0.014s]
                                                                                      let (_x_0 : int) = Ordinal.count y in
                                                                                      let (_x_1 : ty_0 list) = List.tl y in
                                                                                      let (_x_2 : int) = Ordinal.count _x_1 in
                                                                                      not (x = List.hd y) && not (y = []) && _x_0 >= 0 && _x_2 >= 0
                                                                                      ==> not (not (x = List.hd _x_1) && not (_x_1 = []))
                                                                                          || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                                  • simplify
                                                                                    into
                                                                                    let (_x_0 : ty_0 list) = List.tl y in
                                                                                    let (_x_1 : int) = Ordinal.count _x_0 in
                                                                                    let (_x_2 : int) = Ordinal.count y in
                                                                                    (not (not (x = List.hd _x_0) && not (_x_0 = []))
                                                                                     || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                                                                    || not (((not (x = List.hd y) && not (y = [])) && _x_2 >= 0) && _x_1 >= 0)
                                                                                    expansions
                                                                                    []
                                                                                    rewrite_steps
                                                                                      forward_chaining
                                                                                      • unroll
                                                                                        expr
                                                                                        (|count_`ty_0 list`_2882| y_2872)
                                                                                        expansions
                                                                                        • unroll
                                                                                          expr
                                                                                          (|count_`ty_0 list`_2882| (|get.::.1_2865| y_2872))
                                                                                          expansions
                                                                                          • unroll
                                                                                            expr
                                                                                            (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`ty_0 list`_2882|
                                                                                                                                  …
                                                                                            expansions
                                                                                            • Unsat

                                                                                            termination proof

                                                                                            Termination proof

                                                                                            call `unique (List.tl x)` from `unique x`
                                                                                            originalunique x
                                                                                            subunique (List.tl x)
                                                                                            original ordinalOrdinal.Int (Ordinal.count x)
                                                                                            sub ordinalOrdinal.Int (Ordinal.count (List.tl x))
                                                                                            path[not (elem (List.hd x) (List.tl x)) && not (x = [])]
                                                                                            proof
                                                                                            detailed proof
                                                                                            ground_instances4
                                                                                            definitions0
                                                                                            inductions0
                                                                                            search_time
                                                                                            0.020s
                                                                                            details
                                                                                            Expand
                                                                                            smt_stats
                                                                                            num checks9
                                                                                            arith-make-feasible10
                                                                                            arith-max-columns13
                                                                                            arith-conflicts1
                                                                                            rlimit count2389
                                                                                            arith-cheap-eqs2
                                                                                            mk clause3
                                                                                            datatype occurs check22
                                                                                            mk bool var52
                                                                                            arith-lower5
                                                                                            datatype splits3
                                                                                            decisions10
                                                                                            propagations1
                                                                                            arith-max-rows5
                                                                                            conflicts7
                                                                                            datatype accessor ax5
                                                                                            datatype constructor ax8
                                                                                            num allocs1315958827
                                                                                            final checks6
                                                                                            added eqs32
                                                                                            del clause1
                                                                                            arith eq adapter3
                                                                                            arith-upper5
                                                                                            memory24.940000
                                                                                            max memory27.240000
                                                                                            Expand
                                                                                            • start[0.020s]
                                                                                                let (_x_0 : ty_0 list) = List.tl x in
                                                                                                let (_x_1 : int) = Ordinal.count x in
                                                                                                let (_x_2 : int) = Ordinal.count _x_0 in
                                                                                                not (elem (List.hd x) _x_0) && not (x = []) && _x_1 >= 0 && _x_2 >= 0
                                                                                                ==> not (not (elem (List.hd _x_0) (List.tl _x_0)) && not (_x_0 = []))
                                                                                                    || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_1)
                                                                                            • simplify
                                                                                              into
                                                                                              let (_x_0 : ty_0 list) = List.tl x in
                                                                                              let (_x_1 : int) = Ordinal.count _x_0 in
                                                                                              let (_x_2 : int) = Ordinal.count x in
                                                                                              (not (not (elem (List.hd _x_0) (List.tl _x_0)) && not (_x_0 = []))
                                                                                               || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                                                                              || not
                                                                                                 (((not (elem (List.hd x) _x_0) && not (x = [])) && _x_2 >= 0) && _x_1 >= 0)
                                                                                              expansions
                                                                                              []
                                                                                              rewrite_steps
                                                                                                forward_chaining
                                                                                                • unroll
                                                                                                  expr
                                                                                                  (elem_2912 (|get.::.0_2906| x_2917) (|get.::.1_2907| x_2917))
                                                                                                  expansions
                                                                                                  • unroll
                                                                                                    expr
                                                                                                    (|count_`ty_0 list`_2926| x_2917)
                                                                                                    expansions
                                                                                                    • unroll
                                                                                                      expr
                                                                                                      (|count_`ty_0 list`_2926| (|get.::.1_2907| x_2917))
                                                                                                      expansions
                                                                                                      • unroll
                                                                                                        expr
                                                                                                        (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`ty_0 list`_2926|
                                                                                                                                              …
                                                                                                        expansions
                                                                                                        • Unsat

                                                                                                        termination proof

                                                                                                        Termination proof

                                                                                                        call `keep_some_list (List.tl l)` from `keep_some_list l`
                                                                                                        originalkeep_some_list l
                                                                                                        subkeep_some_list (List.tl l)
                                                                                                        original ordinalOrdinal.Int (Ordinal.count l)
                                                                                                        sub ordinalOrdinal.Int (Ordinal.count (List.tl l))
                                                                                                        path[not (l = [])]
                                                                                                        proof
                                                                                                        detailed proof
                                                                                                        ground_instances3
                                                                                                        definitions0
                                                                                                        inductions0
                                                                                                        search_time
                                                                                                        0.014s
                                                                                                        details
                                                                                                        Expand
                                                                                                        smt_stats
                                                                                                        num checks7
                                                                                                        arith-make-feasible10
                                                                                                        arith-max-columns13
                                                                                                        arith-conflicts1
                                                                                                        rlimit count2038
                                                                                                        mk clause3
                                                                                                        datatype occurs check36
                                                                                                        mk bool var58
                                                                                                        arith-lower5
                                                                                                        datatype splits9
                                                                                                        decisions17
                                                                                                        propagations1
                                                                                                        arith-max-rows5
                                                                                                        conflicts7
                                                                                                        datatype accessor ax8
                                                                                                        datatype constructor ax14
                                                                                                        num allocs1401021004
                                                                                                        final checks8
                                                                                                        added eqs43
                                                                                                        del clause1
                                                                                                        arith eq adapter3
                                                                                                        arith-upper5
                                                                                                        memory22.500000
                                                                                                        max memory27.240000
                                                                                                        Expand
                                                                                                        • start[0.014s]
                                                                                                            let (_x_0 : int) = Ordinal.count l in
                                                                                                            let (_x_1 : ty_0 option list) = List.tl l in
                                                                                                            let (_x_2 : int) = Ordinal.count _x_1 in
                                                                                                            not (l = []) && _x_0 >= 0 && _x_2 >= 0
                                                                                                            ==> _x_1 = [] || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                                                        • simplify
                                                                                                          into
                                                                                                          let (_x_0 : ty_0 option list) = List.tl l in
                                                                                                          let (_x_1 : int) = Ordinal.count _x_0 in
                                                                                                          let (_x_2 : int) = Ordinal.count l in
                                                                                                          (_x_0 = [] || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                                                                                          || not ((not (l = []) && _x_2 >= 0) && _x_1 >= 0)
                                                                                                          expansions
                                                                                                          []
                                                                                                          rewrite_steps
                                                                                                            forward_chaining
                                                                                                            • unroll
                                                                                                              expr
                                                                                                              (|count_`ty_0 option list`_2973| l_2964)
                                                                                                              expansions
                                                                                                              • unroll
                                                                                                                expr
                                                                                                                (|count_`ty_0 option list`_2973| (|get.::.1_2954| l_2964))
                                                                                                                expansions
                                                                                                                • unroll
                                                                                                                  expr
                                                                                                                  (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`ty_0 option list`_2973|
                                                                                                                                                 …
                                                                                                                  expansions
                                                                                                                  • Unsat

                                                                                                                  termination proof

                                                                                                                  Termination proof

                                                                                                                  call `blocks_3_34 (List.tl _x)` from `blocks_3_34 _x`
                                                                                                                  originalblocks_3_34 _x
                                                                                                                  subblocks_3_34 (List.tl _x)
                                                                                                                  original ordinalOrdinal.Int (Ordinal.count _x)
                                                                                                                  sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
                                                                                                                  path[not (_x = [])]
                                                                                                                  proof
                                                                                                                  detailed proof
                                                                                                                  ground_instances3
                                                                                                                  definitions0
                                                                                                                  inductions0
                                                                                                                  search_time
                                                                                                                  0.022s
                                                                                                                  details
                                                                                                                  Expand
                                                                                                                  smt_stats
                                                                                                                  num checks8
                                                                                                                  arith-make-feasible26
                                                                                                                  arith-max-columns19
                                                                                                                  arith-conflicts3
                                                                                                                  rlimit count2870
                                                                                                                  mk clause22
                                                                                                                  datatype occurs check52
                                                                                                                  mk bool var112
                                                                                                                  arith-lower18
                                                                                                                  arith-diseq2
                                                                                                                  datatype splits14
                                                                                                                  decisions34
                                                                                                                  propagations14
                                                                                                                  arith-max-rows7
                                                                                                                  conflicts14
                                                                                                                  datatype accessor ax12
                                                                                                                  datatype constructor ax23
                                                                                                                  num allocs1461539021
                                                                                                                  final checks11
                                                                                                                  added eqs83
                                                                                                                  del clause7
                                                                                                                  arith eq adapter15
                                                                                                                  arith-upper16
                                                                                                                  memory23.020000
                                                                                                                  max memory27.240000
                                                                                                                  Expand
                                                                                                                  • start[0.022s]
                                                                                                                      let (_x_0 : int) = Ordinal.count _x in
                                                                                                                      let (_x_1 : ty_0 list list) = List.tl _x in
                                                                                                                      let (_x_2 : int) = Ordinal.count _x_1 in
                                                                                                                      not (_x = []) && _x_0 >= 0 && _x_2 >= 0
                                                                                                                      ==> _x_1 = [] || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                                                                  • simplify
                                                                                                                    into
                                                                                                                    let (_x_0 : ty_0 list list) = List.tl _x in
                                                                                                                    let (_x_1 : int) = Ordinal.count _x_0 in
                                                                                                                    let (_x_2 : int) = Ordinal.count _x in
                                                                                                                    (_x_0 = [] || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                                                                                                    || not ((not (_x = []) && _x_2 >= 0) && _x_1 >= 0)
                                                                                                                    expansions
                                                                                                                    []
                                                                                                                    rewrite_steps
                                                                                                                      forward_chaining
                                                                                                                      • unroll
                                                                                                                        expr
                                                                                                                        (|count_`ty_0 list list`_3050| _x_3041)
                                                                                                                        expansions
                                                                                                                        • unroll
                                                                                                                          expr
                                                                                                                          (|count_`ty_0 list list`_3050| (|get.::.1_3030| _x_3041))
                                                                                                                          expansions
                                                                                                                          • unroll
                                                                                                                            expr
                                                                                                                            (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`ty_0 list list`_3050|
                                                                                                                                                             …
                                                                                                                            expansions
                                                                                                                            • Unsat

                                                                                                                            termination proof

                                                                                                                            Termination proof

                                                                                                                            call `blocks_3_33 (List.tl _x)` from `blocks_3_33 _x`
                                                                                                                            originalblocks_3_33 _x
                                                                                                                            subblocks_3_33 (List.tl _x)
                                                                                                                            original ordinalOrdinal.Int (Ordinal.count _x)
                                                                                                                            sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
                                                                                                                            path[not (_x = [])]
                                                                                                                            proof
                                                                                                                            detailed proof
                                                                                                                            ground_instances3
                                                                                                                            definitions0
                                                                                                                            inductions0
                                                                                                                            search_time
                                                                                                                            0.019s
                                                                                                                            details
                                                                                                                            Expand
                                                                                                                            smt_stats
                                                                                                                            num checks8
                                                                                                                            arith-make-feasible26
                                                                                                                            arith-max-columns19
                                                                                                                            arith-conflicts3
                                                                                                                            rlimit count2870
                                                                                                                            mk clause22
                                                                                                                            datatype occurs check52
                                                                                                                            mk bool var112
                                                                                                                            arith-lower18
                                                                                                                            arith-diseq2
                                                                                                                            datatype splits14
                                                                                                                            decisions34
                                                                                                                            propagations14
                                                                                                                            arith-max-rows7
                                                                                                                            conflicts14
                                                                                                                            datatype accessor ax12
                                                                                                                            datatype constructor ax23
                                                                                                                            num allocs1494247012
                                                                                                                            final checks11
                                                                                                                            added eqs83
                                                                                                                            del clause7
                                                                                                                            arith eq adapter15
                                                                                                                            arith-upper16
                                                                                                                            memory25.890000
                                                                                                                            max memory27.240000
                                                                                                                            Expand
                                                                                                                            • start[0.019s]
                                                                                                                                let (_x_0 : int) = Ordinal.count _x in
                                                                                                                                let (_x_1 : ty_0 list list) = List.tl _x in
                                                                                                                                let (_x_2 : int) = Ordinal.count _x_1 in
                                                                                                                                not (_x = []) && _x_0 >= 0 && _x_2 >= 0
                                                                                                                                ==> _x_1 = [] || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                                                                            • simplify
                                                                                                                              into
                                                                                                                              let (_x_0 : ty_0 list list) = List.tl _x in
                                                                                                                              let (_x_1 : int) = Ordinal.count _x_0 in
                                                                                                                              let (_x_2 : int) = Ordinal.count _x in
                                                                                                                              (_x_0 = [] || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                                                                                                              || not ((not (_x = []) && _x_2 >= 0) && _x_1 >= 0)
                                                                                                                              expansions
                                                                                                                              []
                                                                                                                              rewrite_steps
                                                                                                                                forward_chaining
                                                                                                                                • unroll
                                                                                                                                  expr
                                                                                                                                  (|count_`ty_0 list list`_3106| _x_3097)
                                                                                                                                  expansions
                                                                                                                                  • unroll
                                                                                                                                    expr
                                                                                                                                    (|count_`ty_0 list list`_3106| (|get.::.1_3080| _x_3097))
                                                                                                                                    expansions
                                                                                                                                    • unroll
                                                                                                                                      expr
                                                                                                                                      (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`ty_0 list list`_3106|
                                                                                                                                                                       …
                                                                                                                                      expansions
                                                                                                                                      • Unsat

                                                                                                                                      termination proof

                                                                                                                                      Termination proof

                                                                                                                                      call `blocks_3_32 (List.tl _x)` from `blocks_3_32 _x`
                                                                                                                                      originalblocks_3_32 _x
                                                                                                                                      subblocks_3_32 (List.tl _x)
                                                                                                                                      original ordinalOrdinal.Int (Ordinal.count _x)
                                                                                                                                      sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
                                                                                                                                      path[not (_x = [])]
                                                                                                                                      proof
                                                                                                                                      detailed proof
                                                                                                                                      ground_instances3
                                                                                                                                      definitions0
                                                                                                                                      inductions0
                                                                                                                                      search_time
                                                                                                                                      0.021s
                                                                                                                                      details
                                                                                                                                      Expand
                                                                                                                                      smt_stats
                                                                                                                                      num checks8
                                                                                                                                      arith-make-feasible26
                                                                                                                                      arith-max-columns19
                                                                                                                                      arith-conflicts3
                                                                                                                                      rlimit count2870
                                                                                                                                      mk clause22
                                                                                                                                      datatype occurs check52
                                                                                                                                      mk bool var112
                                                                                                                                      arith-lower18
                                                                                                                                      arith-diseq2
                                                                                                                                      datatype splits14
                                                                                                                                      decisions34
                                                                                                                                      propagations14
                                                                                                                                      arith-max-rows7
                                                                                                                                      conflicts14
                                                                                                                                      datatype accessor ax12
                                                                                                                                      datatype constructor ax23
                                                                                                                                      num allocs1612129825
                                                                                                                                      final checks11
                                                                                                                                      added eqs83
                                                                                                                                      del clause7
                                                                                                                                      arith eq adapter15
                                                                                                                                      arith-upper16
                                                                                                                                      memory20.850000
                                                                                                                                      max memory27.240000
                                                                                                                                      Expand
                                                                                                                                      • start[0.021s]
                                                                                                                                          let (_x_0 : int) = Ordinal.count _x in
                                                                                                                                          let (_x_1 : ty_0 list list) = List.tl _x in
                                                                                                                                          let (_x_2 : int) = Ordinal.count _x_1 in
                                                                                                                                          not (_x = []) && _x_0 >= 0 && _x_2 >= 0
                                                                                                                                          ==> _x_1 = [] || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                                                                                      • simplify
                                                                                                                                        into
                                                                                                                                        let (_x_0 : ty_0 list list) = List.tl _x in
                                                                                                                                        let (_x_1 : int) = Ordinal.count _x_0 in
                                                                                                                                        let (_x_2 : int) = Ordinal.count _x in
                                                                                                                                        (_x_0 = [] || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                                                                                                                        || not ((not (_x = []) && _x_2 >= 0) && _x_1 >= 0)
                                                                                                                                        expansions
                                                                                                                                        []
                                                                                                                                        rewrite_steps
                                                                                                                                          forward_chaining
                                                                                                                                          • unroll
                                                                                                                                            expr
                                                                                                                                            (|count_`ty_0 list list`_3157| _x_3148)
                                                                                                                                            expansions
                                                                                                                                            • unroll
                                                                                                                                              expr
                                                                                                                                              (|count_`ty_0 list list`_3157| (|get.::.1_3136| _x_3148))
                                                                                                                                              expansions
                                                                                                                                              • unroll
                                                                                                                                                expr
                                                                                                                                                (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`ty_0 list list`_3157|
                                                                                                                                                                                 …
                                                                                                                                                expansions
                                                                                                                                                • Unsat

                                                                                                                                                termination proof

                                                                                                                                                Termination proof

                                                                                                                                                call `group3 (List.tl (List.tl (List.tl _x)))` from `group3 _x`
                                                                                                                                                originalgroup3 _x
                                                                                                                                                subgroup3 (List.tl (List.tl (List.tl _x)))
                                                                                                                                                original ordinalOrdinal.Int (Ordinal.count _x)
                                                                                                                                                sub ordinalOrdinal.Int (Ordinal.count (List.tl (List.tl (List.tl _x))))
                                                                                                                                                path[not (List.tl (List.tl _x) = []) && not (List.tl _x = []) && not (_x = [])]
                                                                                                                                                proof
                                                                                                                                                detailed proof
                                                                                                                                                ground_instances8
                                                                                                                                                definitions0
                                                                                                                                                inductions0
                                                                                                                                                search_time
                                                                                                                                                0.028s
                                                                                                                                                details
                                                                                                                                                Expand
                                                                                                                                                smt_stats
                                                                                                                                                num checks18
                                                                                                                                                arith-make-feasible198
                                                                                                                                                arith-max-columns53
                                                                                                                                                arith-conflicts13
                                                                                                                                                rlimit count11790
                                                                                                                                                arith-cheap-eqs31
                                                                                                                                                mk clause188
                                                                                                                                                datatype occurs check98
                                                                                                                                                mk bool var531
                                                                                                                                                arith-lower150
                                                                                                                                                arith-diseq20
                                                                                                                                                datatype splits33
                                                                                                                                                decisions312
                                                                                                                                                arith-propagations18
                                                                                                                                                propagations203
                                                                                                                                                arith-bound-propagations-cheap18
                                                                                                                                                arith-max-rows25
                                                                                                                                                conflicts46
                                                                                                                                                datatype accessor ax31
                                                                                                                                                minimized lits5
                                                                                                                                                arith-bound-propagations-lp7
                                                                                                                                                datatype constructor ax117
                                                                                                                                                num allocs1709197558
                                                                                                                                                final checks18
                                                                                                                                                added eqs564
                                                                                                                                                del clause105
                                                                                                                                                arith eq adapter121
                                                                                                                                                arith-upper172
                                                                                                                                                memory18.960000
                                                                                                                                                max memory27.240000
                                                                                                                                                Expand
                                                                                                                                                • start[0.028s]
                                                                                                                                                    let (_x_0 : ty_0 list list) = List.tl _x in
                                                                                                                                                    let (_x_1 : ty_0 list list) = List.tl _x_0 in
                                                                                                                                                    let (_x_2 : int) = Ordinal.count _x in
                                                                                                                                                    let (_x_3 : ty_0 list list) = List.tl _x_1 in
                                                                                                                                                    let (_x_4 : int) = Ordinal.count _x_3 in
                                                                                                                                                    let (_x_5 : ty_0 list list) = List.tl _x_3 in
                                                                                                                                                    not (_x_1 = [])
                                                                                                                                                    && not (_x_0 = []) && not (_x = []) && _x_2 >= 0 && _x_4 >= 0
                                                                                                                                                    ==> not (not (List.tl _x_5 = []) && not (_x_5 = []) && not (_x_3 = []))
                                                                                                                                                        || Ordinal.( << ) (Ordinal.Int _x_4) (Ordinal.Int _x_2)
                                                                                                                                                • simplify
                                                                                                                                                  into
                                                                                                                                                  let (_x_0 : ty_0 list list) = List.tl _x in
                                                                                                                                                  let (_x_1 : ty_0 list list) = List.tl _x_0 in
                                                                                                                                                  let (_x_2 : ty_0 list list) = List.tl _x_1 in
                                                                                                                                                  let (_x_3 : int) = Ordinal.count _x_2 in
                                                                                                                                                  let (_x_4 : int) = Ordinal.count _x in
                                                                                                                                                  let (_x_5 : ty_0 list list) = List.tl _x_2 in
                                                                                                                                                  (Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_4)
                                                                                                                                                   || not ((not (List.tl _x_5 = []) && not (_x_5 = [])) && not (_x_2 = [])))
                                                                                                                                                  || not
                                                                                                                                                     ((((not (_x_1 = []) && not (_x_0 = [])) && not (_x = [])) && _x_4 >= 0)
                                                                                                                                                      && _x_3 >= 0)
                                                                                                                                                  expansions
                                                                                                                                                  []
                                                                                                                                                  rewrite_steps
                                                                                                                                                    forward_chaining
                                                                                                                                                    • unroll
                                                                                                                                                      expr
                                                                                                                                                      (|count_`ty_0 list list`_3210| _x_3201)
                                                                                                                                                      expansions
                                                                                                                                                      • unroll
                                                                                                                                                        expr
                                                                                                                                                        (|count_`ty_0 list list`_3210|
                                                                                                                                                          (|get.::.1_3187| (|get.::.1_3187| (|get.::.1_3187| _x_3201))))
                                                                                                                                                        expansions
                                                                                                                                                        • unroll
                                                                                                                                                          expr
                                                                                                                                                          (let ((a!1 (|count_`ty_0 list list`_3210|
                                                                                                                                                                       (|get.::.1_3187| (|get.::.1_3187| (|get.::.1_…
                                                                                                                                                          expansions
                                                                                                                                                          • unroll
                                                                                                                                                            expr
                                                                                                                                                            (|count_`ty_0 list list`_3210| (|get.::.1_3187| _x_3201))
                                                                                                                                                            expansions
                                                                                                                                                            • unroll
                                                                                                                                                              expr
                                                                                                                                                              (|count_`ty_0 list`_3212| (|get.::.0_3186| _x_3201))
                                                                                                                                                              expansions
                                                                                                                                                              • unroll
                                                                                                                                                                expr
                                                                                                                                                                (let ((a!1 (|get.::.1_3187| (|get.::.1_3187| (|get.::.1_3187| (|get.::.1_3187| _x_3201))))))
                                                                                                                                                                  (|cou…
                                                                                                                                                                expansions
                                                                                                                                                                • unroll
                                                                                                                                                                  expr
                                                                                                                                                                  (let ((a!1 (|get.::.0_3186| (|get.::.1_3187| (|get.::.1_3187| (|get.::.1_3187| _x_3201))))))
                                                                                                                                                                    (|cou…
                                                                                                                                                                  expansions
                                                                                                                                                                  • unroll
                                                                                                                                                                    expr
                                                                                                                                                                    (|count_`ty_0 list list`_3210| (|get.::.1_3187| (|get.::.1_3187| _x_3201)))
                                                                                                                                                                    expansions
                                                                                                                                                                    • Unsat

                                                                                                                                                                    The Sudoku type

                                                                                                                                                                    We're ready to define the sudoku as a list of lists of (possibly empty) cells.

                                                                                                                                                                    First, cells are just an enumeration of 9 distinct cases:

                                                                                                                                                                    In [5]:
                                                                                                                                                                    type cell = C1 | C2 | C3 | C4 | C5 | C6 | C7 | C8 | C9 ;;
                                                                                                                                                                    
                                                                                                                                                                    (* let us also write a nice printer for cells. We will put
                                                                                                                                                                       it to good use later. *)
                                                                                                                                                                    let doc_of_cell c =
                                                                                                                                                                      Document.s (match c with C1->"1"|C2->"2"|C3->"3"|C4->"4"|C5->"5"|C6->"6"|C7->"7"|C8->"8"|C9->"9") [@@program];;
                                                                                                                                                                    
                                                                                                                                                                    #install_doc doc_of_cell;;
                                                                                                                                                                    
                                                                                                                                                                    Out[5]:
                                                                                                                                                                    type cell = C1 | C2 | C3 | C4 | C5 | C6 | C7 | C8 | C9
                                                                                                                                                                    val doc_of_cell : cell -> Document.t = <fun>
                                                                                                                                                                    

                                                                                                                                                                    And the sudoku itself:

                                                                                                                                                                    In [6]:
                                                                                                                                                                    type sudoku = { rows: cell option list list } ;;
                                                                                                                                                                    
                                                                                                                                                                    (* now install a nice printer for sudoku grids *)
                                                                                                                                                                    let doc_of_sudoku (s:sudoku) : Document.t =
                                                                                                                                                                      let module D = Document in
                                                                                                                                                                      let d_of_c = function None -> D.s "·" | Some c -> doc_of_cell c in
                                                                                                                                                                      D.tbl_of d_of_c s.rows [@@program]
                                                                                                                                                                      ;;
                                                                                                                                                                    
                                                                                                                                                                    #install_doc doc_of_sudoku;;
                                                                                                                                                                    
                                                                                                                                                                    Out[6]:
                                                                                                                                                                    type sudoku = { rows : cell option list list; }
                                                                                                                                                                    val doc_of_sudoku : sudoku -> Document.t = <fun>
                                                                                                                                                                    

                                                                                                                                                                    We're going to solve the following instance (still from Dan Rosén and Koen Claessen's code). The custom printer we installed earlier shows the grid in a readable way.

                                                                                                                                                                    In [7]:
                                                                                                                                                                    let the_problem : sudoku =
                                                                                                                                                                      {rows=
                                                                                                                                                                        [ [ (Some C8) ; None ; None ; None ; None ; None ; None ; None ; None ];
                                                                                                                                                                        [ None ; None ; (Some C3) ; (Some C6) ; None ; None ; None ; None ; None ];
                                                                                                                                                                        [ None ; (Some C7) ; None ; None ; (Some C9) ; None ; (Some C2) ; None ; None ];
                                                                                                                                                                        [ None ; (Some C5) ; None ; None ; None ; (Some C7) ; None ; None ; None ];
                                                                                                                                                                        [ None ; None ; None ; None ; (Some C4) ; (Some C5) ; (Some C7) ; None ; None ];
                                                                                                                                                                        [ None ; None ; None ; (Some C1) ; None ; None ; None ; (Some C3) ; None ];
                                                                                                                                                                        [ None ; None ; (Some C1) ; None ; None ; None ; None ; (Some C6) ; (Some C8); ];
                                                                                                                                                                        [ None ; None ; (Some C8) ; (Some C5) ; None ; None ; None ; (Some C1) ; None ];
                                                                                                                                                                        [ None ; (Some C9) ; None ; None ; None ; None ; (Some C4) ; None ; None ];
                                                                                                                                                                      ]}
                                                                                                                                                                    ;;
                                                                                                                                                                    
                                                                                                                                                                    Out[7]:
                                                                                                                                                                    val the_problem : sudoku = <document>
                                                                                                                                                                    
                                                                                                                                                                    8········
                                                                                                                                                                    ··36·····
                                                                                                                                                                    ·7··9·2··
                                                                                                                                                                    ·5···7···
                                                                                                                                                                    ····457··
                                                                                                                                                                    ···1···3·
                                                                                                                                                                    ··1····68
                                                                                                                                                                    ··85···1·
                                                                                                                                                                    ·9····4··
                                                                                                                                                                    In [8]:
                                                                                                                                                                    (** All the relevant blocks: rows, columns, and 3×3 sub-squares *)
                                                                                                                                                                    let blocks (x:sudoku) =
                                                                                                                                                                      x.rows @ transpose x.rows @ blocks_3_3 x.rows
                                                                                                                                                                    
                                                                                                                                                                    (** Are all constraints satisfied? *)
                                                                                                                                                                    let satisfies_constraints (x:sudoku) = List.for_all block_satisfies_constraints (blocks x);;
                                                                                                                                                                    
                                                                                                                                                                    (** is a sudoku entirely defined (all cells are filled)? *)
                                                                                                                                                                    let is_solved (x:sudoku) =
                                                                                                                                                                      List.for_all (List.for_all Option.is_some) x.rows;;
                                                                                                                                                                    
                                                                                                                                                                    (** Is [x] of the correct shape, i.e. a 9×9 grid? *)
                                                                                                                                                                    let is_valid_sudoku (x:sudoku) =
                                                                                                                                                                      length x.rows = n9 &&
                                                                                                                                                                      List.for_all (fun col -> length col = n9) x.rows
                                                                                                                                                                    ;;
                                                                                                                                                                    
                                                                                                                                                                    Out[8]:
                                                                                                                                                                    val blocks : sudoku -> cell option list list = <fun>
                                                                                                                                                                    val satisfies_constraints : sudoku -> bool = <fun>
                                                                                                                                                                    val is_solved : sudoku -> bool = <fun>
                                                                                                                                                                    val is_valid_sudoku : sudoku -> bool = <fun>
                                                                                                                                                                    

                                                                                                                                                                    We have a template (the initial problem) and we want to solve it. It means the sudoku we're looking for must be:

                                                                                                                                                                    • solved (all cells are Some _ rather than None)
                                                                                                                                                                    • a solution of the template (i.e. cells defined in the template must match)
                                                                                                                                                                    In [9]:
                                                                                                                                                                    (** Combine lists together *)
                                                                                                                                                                    let rec zip l1 l2 = match l1, l2 with
                                                                                                                                                                      | [], _ | _, [] -> []
                                                                                                                                                                      | x1::tl1, x2 :: tl2 -> (x1,x2) :: zip tl1 tl2
                                                                                                                                                                    
                                                                                                                                                                    let rec match_cols y =
                                                                                                                                                                      match y with
                                                                                                                                                                      | [] -> true
                                                                                                                                                                      | z :: x2 ->
                                                                                                                                                                        match z with
                                                                                                                                                                        | None,_ | _, None -> match_cols x2
                                                                                                                                                                        | (Some n1,Some n2) -> n1=n2 && match_cols x2
                                                                                                                                                                    ;;
                                                                                                                                                                    
                                                                                                                                                                    let rec match_rows x =
                                                                                                                                                                      match x with
                                                                                                                                                                      | [] -> true
                                                                                                                                                                      | (row1,row2) :: z -> match_cols (zip row1 row2) && match_rows z
                                                                                                                                                                    ;;
                                                                                                                                                                    
                                                                                                                                                                    (** is [x] a solution of [y]? We check that each cell in each rows,
                                                                                                                                                                        if defined in [y], has the same value in [x] *)
                                                                                                                                                                    let is_solution_of (x:sudoku) (y:sudoku) : bool =
                                                                                                                                                                      is_solved x &&
                                                                                                                                                                      satisfies_constraints x &&
                                                                                                                                                                      match_rows (zip x.rows y.rows)
                                                                                                                                                                    
                                                                                                                                                                    Out[9]:
                                                                                                                                                                    val zip : 'a list -> 'b list -> ('a * 'b) list = <fun>
                                                                                                                                                                    val match_cols : ('a option * 'a option) list -> bool = <fun>
                                                                                                                                                                    val match_rows : ('a option list * 'a option list) list -> bool = <fun>
                                                                                                                                                                    val is_solution_of : sudoku -> sudoku -> bool = <fun>
                                                                                                                                                                    
                                                                                                                                                                    termination proof

                                                                                                                                                                    Termination proof

                                                                                                                                                                    call `zip (List.tl l1) (List.tl l2)` from `zip l1 l2`
                                                                                                                                                                    originalzip l1 l2
                                                                                                                                                                    subzip (List.tl l1) (List.tl l2)
                                                                                                                                                                    original ordinalOrdinal.Int (Ordinal.count l1)
                                                                                                                                                                    sub ordinalOrdinal.Int (Ordinal.count (List.tl l1))
                                                                                                                                                                    path[not (l1 = [] || l2 = [])]
                                                                                                                                                                    proof
                                                                                                                                                                    detailed proof
                                                                                                                                                                    ground_instances3
                                                                                                                                                                    definitions0
                                                                                                                                                                    inductions0
                                                                                                                                                                    search_time
                                                                                                                                                                    0.014s
                                                                                                                                                                    details
                                                                                                                                                                    Expand
                                                                                                                                                                    smt_stats
                                                                                                                                                                    num checks7
                                                                                                                                                                    arith-make-feasible10
                                                                                                                                                                    arith-max-columns13
                                                                                                                                                                    arith-conflicts1
                                                                                                                                                                    rlimit count2108
                                                                                                                                                                    mk clause3
                                                                                                                                                                    datatype occurs check34
                                                                                                                                                                    mk bool var64
                                                                                                                                                                    arith-lower4
                                                                                                                                                                    datatype splits6
                                                                                                                                                                    decisions16
                                                                                                                                                                    propagations2
                                                                                                                                                                    arith-max-rows5
                                                                                                                                                                    conflicts10
                                                                                                                                                                    datatype accessor ax8
                                                                                                                                                                    datatype constructor ax16
                                                                                                                                                                    num allocs1825142549
                                                                                                                                                                    final checks6
                                                                                                                                                                    added eqs52
                                                                                                                                                                    del clause1
                                                                                                                                                                    arith eq adapter3
                                                                                                                                                                    arith-upper6
                                                                                                                                                                    memory17.870000
                                                                                                                                                                    max memory27.240000
                                                                                                                                                                    Expand
                                                                                                                                                                    • start[0.014s]
                                                                                                                                                                        let (_x_0 : int) = Ordinal.count l1 in
                                                                                                                                                                        let (_x_1 : ty_0 list) = List.tl l1 in
                                                                                                                                                                        let (_x_2 : int) = Ordinal.count _x_1 in
                                                                                                                                                                        not (l1 = [] || l2 = []) && _x_0 >= 0 && _x_2 >= 0
                                                                                                                                                                        ==> (_x_1 = [] || List.tl l2 = [])
                                                                                                                                                                            || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                                                                                                                    • simplify
                                                                                                                                                                      into
                                                                                                                                                                      let (_x_0 : ty_0 list) = List.tl l1 in
                                                                                                                                                                      let (_x_1 : int) = Ordinal.count _x_0 in
                                                                                                                                                                      let (_x_2 : int) = Ordinal.count l1 in
                                                                                                                                                                      ((_x_0 = [] || List.tl l2 = [])
                                                                                                                                                                       || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                                                                                                                                                      || not ((not (l1 = [] || l2 = []) && _x_2 >= 0) && _x_1 >= 0)
                                                                                                                                                                      expansions
                                                                                                                                                                      []
                                                                                                                                                                      rewrite_steps
                                                                                                                                                                        forward_chaining
                                                                                                                                                                        • unroll
                                                                                                                                                                          expr
                                                                                                                                                                          (|count_`ty_0 list`_3559| l1_3548)
                                                                                                                                                                          expansions
                                                                                                                                                                          • unroll
                                                                                                                                                                            expr
                                                                                                                                                                            (|count_`ty_0 list`_3559| (|get.::.1_3530| l1_3548))
                                                                                                                                                                            expansions
                                                                                                                                                                            • unroll
                                                                                                                                                                              expr
                                                                                                                                                                              (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`ty_0 list`_3559|
                                                                                                                                                                                                                    …
                                                                                                                                                                              expansions
                                                                                                                                                                              • Unsat

                                                                                                                                                                              termination proof

                                                                                                                                                                              Termination proof

                                                                                                                                                                              call `match_cols (List.tl y)` from `match_cols y`
                                                                                                                                                                              originalmatch_cols y
                                                                                                                                                                              submatch_cols (List.tl y)
                                                                                                                                                                              original ordinalOrdinal.Int (Ordinal.count y)
                                                                                                                                                                              sub ordinalOrdinal.Int (Ordinal.count (List.tl y))
                                                                                                                                                                              path[let (_x_0 : (ty_0 option * ty_0 option)) = List.hd y in _x_0.0 = None || _x_0.1 = None && not (y = [])]
                                                                                                                                                                              proof
                                                                                                                                                                              detailed proof
                                                                                                                                                                              ground_instances3
                                                                                                                                                                              definitions0
                                                                                                                                                                              inductions0
                                                                                                                                                                              search_time
                                                                                                                                                                              0.014s
                                                                                                                                                                              details
                                                                                                                                                                              Expand
                                                                                                                                                                              smt_stats
                                                                                                                                                                              num checks7
                                                                                                                                                                              arith-make-feasible10
                                                                                                                                                                              arith-max-columns13
                                                                                                                                                                              arith-conflicts1
                                                                                                                                                                              rlimit count5750
                                                                                                                                                                              mk clause28
                                                                                                                                                                              datatype occurs check59
                                                                                                                                                                              mk bool var143
                                                                                                                                                                              arith-lower4
                                                                                                                                                                              datatype splits23
                                                                                                                                                                              decisions32
                                                                                                                                                                              propagations57
                                                                                                                                                                              arith-max-rows5
                                                                                                                                                                              conflicts12
                                                                                                                                                                              datatype accessor ax26
                                                                                                                                                                              datatype constructor ax33
                                                                                                                                                                              num allocs1924513495
                                                                                                                                                                              final checks10
                                                                                                                                                                              added eqs147
                                                                                                                                                                              del clause2
                                                                                                                                                                              arith eq adapter3
                                                                                                                                                                              arith-upper6
                                                                                                                                                                              memory20.690000
                                                                                                                                                                              max memory27.240000
                                                                                                                                                                              Expand
                                                                                                                                                                              • start[0.014s]
                                                                                                                                                                                  let (_x_0 : (ty_0 option * ty_0 option)) = List.hd y in
                                                                                                                                                                                  let (_x_1 : int) = Ordinal.count y in
                                                                                                                                                                                  let (_x_2 : (ty_0 option * ty_0 option) list) = List.tl y in
                                                                                                                                                                                  let (_x_3 : int) = Ordinal.count _x_2 in
                                                                                                                                                                                  let (_x_4 : (ty_0 option * ty_0 option)) = List.hd _x_2 in
                                                                                                                                                                                  let (_x_5 : ty_0 option) = _x_4.0 in
                                                                                                                                                                                  let (_x_6 : ty_0 option) = _x_4.1 in
                                                                                                                                                                                  let (_x_7 : bool) = _x_5 = None || _x_6 = None in
                                                                                                                                                                                  let (_x_8 : bool) = not (_x_2 = []) in
                                                                                                                                                                                  (_x_0.0 = None || _x_0.1 = None) && not (y = []) && _x_1 >= 0 && _x_3 >= 0
                                                                                                                                                                                  ==> not (_x_7 && _x_8)
                                                                                                                                                                                      && not (Option.get _x_5 = Option.get _x_6 && not _x_7 && _x_8)
                                                                                                                                                                                      || Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_1)
                                                                                                                                                                              • simplify
                                                                                                                                                                                into
                                                                                                                                                                                let (_x_0 : (ty_0 option * ty_0 option) list) = List.tl y in
                                                                                                                                                                                let (_x_1 : int) = Ordinal.count _x_0 in
                                                                                                                                                                                let (_x_2 : int) = Ordinal.count y in
                                                                                                                                                                                let (_x_3 : (ty_0 option * ty_0 option)) = List.hd _x_0 in
                                                                                                                                                                                let (_x_4 : ty_0 option) = _x_3.0 in
                                                                                                                                                                                let (_x_5 : ty_0 option) = _x_3.1 in
                                                                                                                                                                                let (_x_6 : bool) = _x_4 = None || _x_5 = None in
                                                                                                                                                                                let (_x_7 : bool) = not (_x_0 = []) in
                                                                                                                                                                                let (_x_8 : (ty_0 option * ty_0 option)) = List.hd y in
                                                                                                                                                                                (Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
                                                                                                                                                                                 || not (_x_6 && _x_7)
                                                                                                                                                                                    && not ((Option.get _x_4 = Option.get _x_5 && not _x_6) && _x_7))
                                                                                                                                                                                || not
                                                                                                                                                                                   ((((_x_8.0 = None || _x_8.1 = None) && not (y = [])) && _x_2 >= 0)
                                                                                                                                                                                    && _x_1 >= 0)
                                                                                                                                                                                expansions
                                                                                                                                                                                []
                                                                                                                                                                                rewrite_steps
                                                                                                                                                                                  forward_chaining
                                                                                                                                                                                  • unroll
                                                                                                                                                                                    expr
                                                                                                                                                                                    (|count_`(ty_0 option * ty_0 option) list`_3608| y_3597)
                                                                                                                                                                                    expansions
                                                                                                                                                                                    • unroll
                                                                                                                                                                                      expr
                                                                                                                                                                                      (|count_`(ty_0 option * ty_0 option) list`_3608| (|get.::.1_3590| y_3597))
                                                                                                                                                                                      expansions
                                                                                                                                                                                      • unroll
                                                                                                                                                                                        expr
                                                                                                                                                                                        (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`(ty_0 option * ty_0 option) list`_3608|
                                                                                                                                                                                                       …
                                                                                                                                                                                        expansions
                                                                                                                                                                                        • Unsat

                                                                                                                                                                                        call `match_cols (List.tl y)` from `match_cols y`
                                                                                                                                                                                        originalmatch_cols y
                                                                                                                                                                                        submatch_cols (List.tl y)
                                                                                                                                                                                        original ordinalOrdinal.Int (Ordinal.count y)
                                                                                                                                                                                        sub ordinalOrdinal.Int (Ordinal.count (List.tl y))
                                                                                                                                                                                        path[let (_x_0 : (ty_0 option * ty_0 option)) = List.hd y in Option.get _x_0.0 = Option.get _x_0.1 && let (_x_0 : (ty_0 option * ty_0 option)) = List.hd y in not (_x_0.0 = None || _x_0.1 = None) && not (y = [])]
                                                                                                                                                                                        proof
                                                                                                                                                                                        detailed proof
                                                                                                                                                                                        ground_instances3
                                                                                                                                                                                        definitions0
                                                                                                                                                                                        inductions0
                                                                                                                                                                                        search_time
                                                                                                                                                                                        0.015s
                                                                                                                                                                                        details
                                                                                                                                                                                        Expand
                                                                                                                                                                                        smt_stats
                                                                                                                                                                                        num checks7
                                                                                                                                                                                        arith-make-feasible11
                                                                                                                                                                                        arith-max-columns12
                                                                                                                                                                                        arith-conflicts1
                                                                                                                                                                                        rlimit count2930
                                                                                                                                                                                        mk clause26
                                                                                                                                                                                        datatype occurs check78
                                                                                                                                                                                        mk bool var139
                                                                                                                                                                                        arith-lower5
                                                                                                                                                                                        datatype splits26
                                                                                                                                                                                        decisions31
                                                                                                                                                                                        propagations57
                                                                                                                                                                                        arith-max-rows4
                                                                                                                                                                                        conflicts13
                                                                                                                                                                                        datatype accessor ax25
                                                                                                                                                                                        datatype constructor ax33
                                                                                                                                                                                        num allocs1891779689
                                                                                                                                                                                        final checks11
                                                                                                                                                                                        added eqs142
                                                                                                                                                                                        del clause2
                                                                                                                                                                                        arith eq adapter3
                                                                                                                                                                                        arith-upper5
                                                                                                                                                                                        memory18.130000
                                                                                                                                                                                        max memory27.240000
                                                                                                                                                                                        Expand
                                                                                                                                                                                        • start[0.015s]
                                                                                                                                                                                            let (_x_0 : (ty_0 option * ty_0 option)) = List.hd y in
                                                                                                                                                                                            let (_x_1 : ty_0 option) = _x_0.0 in
                                                                                                                                                                                            let (_x_2 : ty_0 option) = _x_0.1 in
                                                                                                                                                                                            let (_x_3 : int) = Ordinal.count y in
                                                                                                                                                                                            let (_x_4 : (ty_0 option * ty_0 option) list) = List.tl y in
                                                                                                                                                                                            let (_x_5 : int) = Ordinal.count _x_4 in
                                                                                                                                                                                            let (_x_6 : (ty_0 option * ty_0 option)) = List.hd _x_4 in
                                                                                                                                                                                            let (_x_7 : ty_0 option) = _x_6.0 in
                                                                                                                                                                                            let (_x_8 : ty_0 option) = _x_6.1 in
                                                                                                                                                                                            let (_x_9 : bool) = _x_7 = None || _x_8 = None in
                                                                                                                                                                                            let (_x_10 : bool) = not (_x_4 = []) in
                                                                                                                                                                                            Option.get _x_1 = Option.get _x_2
                                                                                                                                                                                            && not (_x_1 = None || _x_2 = None)
                                                                                                                                                                                               && not (y = []) && _x_3 >= 0 && _x_5 >= 0
                                                                                                                                                                                            ==> not (_x_9 && _x_10)
                                                                                                                                                                                                && not (Option.get _x_7 = Option.get _x_8 && not _x_9 && _x_10)
                                                                                                                                                                                                || Ordinal.( << ) (Ordinal.Int _x_5) (Ordinal.Int _x_3)
                                                                                                                                                                                        • simplify
                                                                                                                                                                                          into
                                                                                                                                                                                          let (_x_0 : (ty_0 option * ty_0 option) list) = List.tl y in
                                                                                                                                                                                          let (_x_1 : int) = Ordinal.count _x_0 in
                                                                                                                                                                                          let (_x_2 : int) = Ordinal.count y in
                                                                                                                                                                                          let (_x_3 : (ty_0 option * ty_0 option)) = List.hd _x_0 in
                                                                                                                                                                                          let (_x_4 : ty_0 option) = _x_3.0 in
                                                                                                                                                                                          let (_x_5 : ty_0 option) = _x_3.1 in
                                                                                                                                                                                          let (_x_6 : bool) = _x_4 = None || _x_5 = None in
                                                                                                                                                                                          let (_x_7 : bool) = not (_x_0 = []) in
                                                                                                                                                                                          let (_x_8 : (ty_0 option * ty_0 option)) = List.hd y in
                                                                                                                                                                                          let (_x_9 : ty_0 option) = _x_8.0 in
                                                                                                                                                                                          let (_x_10 : ty_0 option) = _x_8.1 in
                                                                                                                                                                                          (Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
                                                                                                                                                                                           || not (_x_6 && _x_7)
                                                                                                                                                                                              && not ((Option.get _x_4 = Option.get _x_5 && not _x_6) && _x_7))
                                                                                                                                                                                          || not
                                                                                                                                                                                             ((((Option.get _x_9 = Option.get _x_10
                                                                                                                                                                                                 && not (_x_9 = None || _x_10 = None))
                                                                                                                                                                                                && not (y = []))
                                                                                                                                                                                               && _x_2 >= 0)
                                                                                                                                                                                              && _x_1 >= 0)
                                                                                                                                                                                          expansions
                                                                                                                                                                                          []
                                                                                                                                                                                          rewrite_steps
                                                                                                                                                                                            forward_chaining
                                                                                                                                                                                            • unroll
                                                                                                                                                                                              expr
                                                                                                                                                                                              (|count_`(ty_0 option * ty_0 option) list`_3608| y_3597)
                                                                                                                                                                                              expansions
                                                                                                                                                                                              • unroll
                                                                                                                                                                                                expr
                                                                                                                                                                                                (|count_`(ty_0 option * ty_0 option) list`_3608| (|get.::.1_3590| y_3597))
                                                                                                                                                                                                expansions
                                                                                                                                                                                                • unroll
                                                                                                                                                                                                  expr
                                                                                                                                                                                                  (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`(ty_0 option * ty_0 option) list`_3608|
                                                                                                                                                                                                                 …
                                                                                                                                                                                                  expansions
                                                                                                                                                                                                  • Unsat

                                                                                                                                                                                                  termination proof

                                                                                                                                                                                                  Termination proof

                                                                                                                                                                                                  call `match_rows (List.tl x)` from `match_rows x`
                                                                                                                                                                                                  originalmatch_rows x
                                                                                                                                                                                                  submatch_rows (List.tl x)
                                                                                                                                                                                                  original ordinalOrdinal.Int (Ordinal.count x)
                                                                                                                                                                                                  sub ordinalOrdinal.Int (Ordinal.count (List.tl x))
                                                                                                                                                                                                  path[let (_x_0 : (ty_0 option list * ty_0 option list)) = List.hd x in match_cols (zip _x_0.0 _x_0.1) && not (x = [])]
                                                                                                                                                                                                  proof
                                                                                                                                                                                                  detailed proof
                                                                                                                                                                                                  ground_instances5
                                                                                                                                                                                                  definitions0
                                                                                                                                                                                                  inductions0
                                                                                                                                                                                                  search_time
                                                                                                                                                                                                  0.022s
                                                                                                                                                                                                  details
                                                                                                                                                                                                  Expand
                                                                                                                                                                                                  smt_stats
                                                                                                                                                                                                  num checks12
                                                                                                                                                                                                  arith-assume-eqs2
                                                                                                                                                                                                  arith-make-feasible59
                                                                                                                                                                                                  arith-max-columns37
                                                                                                                                                                                                  arith-conflicts5
                                                                                                                                                                                                  rlimit count8054
                                                                                                                                                                                                  arith-cheap-eqs3
                                                                                                                                                                                                  mk clause89
                                                                                                                                                                                                  datatype occurs check173
                                                                                                                                                                                                  mk bool var354
                                                                                                                                                                                                  arith-lower39
                                                                                                                                                                                                  arith-diseq4
                                                                                                                                                                                                  datatype splits61
                                                                                                                                                                                                  decisions174
                                                                                                                                                                                                  arith-propagations2
                                                                                                                                                                                                  propagations90
                                                                                                                                                                                                  interface eqs2
                                                                                                                                                                                                  arith-bound-propagations-cheap2
                                                                                                                                                                                                  arith-max-rows19
                                                                                                                                                                                                  conflicts26
                                                                                                                                                                                                  datatype accessor ax33
                                                                                                                                                                                                  minimized lits1
                                                                                                                                                                                                  datatype constructor ax92
                                                                                                                                                                                                  num allocs2029147308
                                                                                                                                                                                                  final checks17
                                                                                                                                                                                                  added eqs358
                                                                                                                                                                                                  del clause30
                                                                                                                                                                                                  arith eq adapter33
                                                                                                                                                                                                  arith-upper41
                                                                                                                                                                                                  memory18.740000
                                                                                                                                                                                                  max memory27.240000
                                                                                                                                                                                                  Expand
                                                                                                                                                                                                  • start[0.022s]
                                                                                                                                                                                                      let (_x_0 : (ty_0 option list * ty_0 option list)) = List.hd x in
                                                                                                                                                                                                      let (_x_1 : int) = Ordinal.count x in
                                                                                                                                                                                                      let (_x_2 : (ty_0 option list * ty_0 option list) list) = List.tl x in
                                                                                                                                                                                                      let (_x_3 : int) = Ordinal.count _x_2 in
                                                                                                                                                                                                      let (_x_4 : (ty_0 option list * ty_0 option list)) = List.hd _x_2 in
                                                                                                                                                                                                      match_cols (zip _x_0.0 _x_0.1) && not (x = []) && _x_1 >= 0 && _x_3 >= 0
                                                                                                                                                                                                      ==> not (match_cols (zip _x_4.0 _x_4.1) && not (_x_2 = []))
                                                                                                                                                                                                          || Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_1)
                                                                                                                                                                                                  • simplify
                                                                                                                                                                                                    into
                                                                                                                                                                                                    let (_x_0 : (ty_0 option list * ty_0 option list) list) = List.tl x in
                                                                                                                                                                                                    let (_x_1 : (ty_0 option list * ty_0 option list)) = List.hd _x_0 in
                                                                                                                                                                                                    let (_x_2 : int) = Ordinal.count _x_0 in
                                                                                                                                                                                                    let (_x_3 : int) = Ordinal.count x in
                                                                                                                                                                                                    let (_x_4 : (ty_0 option list * ty_0 option list)) = List.hd x in
                                                                                                                                                                                                    (not (match_cols (zip _x_1.0 _x_1.1) && not (_x_0 = []))
                                                                                                                                                                                                     || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_3))
                                                                                                                                                                                                    || not
                                                                                                                                                                                                       (((match_cols (zip _x_4.0 _x_4.1) && not (x = [])) && _x_3 >= 0)
                                                                                                                                                                                                        && _x_2 >= 0)
                                                                                                                                                                                                    expansions
                                                                                                                                                                                                    []
                                                                                                                                                                                                    rewrite_steps
                                                                                                                                                                                                      forward_chaining
                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                        expr
                                                                                                                                                                                                        (zip_3766 (|tuple_get.0_3749| (|get.::.0_3752| x_3779))
                                                                                                                                                                                                                  (|tuple_get.1_3750| (|get.::.0_375…
                                                                                                                                                                                                        expansions
                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                          expr
                                                                                                                                                                                                          (match_cols_3773 (zip_3766 (|tuple_get.0_3749| (|get.::.0_3752| x_3779))
                                                                                                                                                                                                                                     …
                                                                                                                                                                                                          expansions
                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                            expr
                                                                                                                                                                                                            (|count_`(ty_0 option list * ty_0 option list) list`_3788| x_3779)
                                                                                                                                                                                                            expansions
                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                              expr
                                                                                                                                                                                                              (|count_`(ty_0 option list * ty_0 option list) list`_3788|
                                                                                                                                                                                                                (|get.::.1_3753| x_3779))
                                                                                                                                                                                                              expansions
                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                expr
                                                                                                                                                                                                                (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`(ty_0 option list * ty_0 option list) list`_3788|
                                                                                                                                                                                                                     …
                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                • Unsat

                                                                                                                                                                                                                The Satisfaction of Subrepticiously Solving Sudokus using Satisfiability

                                                                                                                                                                                                                We can now, finally, ask Imandra to find a sudoku that satisfies all the constraints defined before!

                                                                                                                                                                                                                NOTE: we have to use [@@blast] because this problem is prone to combinatorial explosion and is too hard for Imandra's default unrolling algorithm.

                                                                                                                                                                                                                In [10]:
                                                                                                                                                                                                                instance (fun (s:sudoku) -> is_valid_sudoku s && is_solution_of s the_problem) [@@blast] ;;
                                                                                                                                                                                                                
                                                                                                                                                                                                                Out[10]:
                                                                                                                                                                                                                - : sudoku -> bool = <fun>
                                                                                                                                                                                                                module CX : sig val s : sudoku end
                                                                                                                                                                                                                
                                                                                                                                                                                                                Instance (after 273 steps, 3.103s):
                                                                                                                                                                                                                  let s =
                                                                                                                                                                                                                    let (_x_0 : cell option) = Some C8 in
                                                                                                                                                                                                                    let (_x_1 : cell option) = Some C1 in
                                                                                                                                                                                                                    let (_x_2 : cell option) = Some C2 in
                                                                                                                                                                                                                    let (_x_3 : cell option) = Some C7 in
                                                                                                                                                                                                                    let (_x_4 : cell option) = Some C5 in
                                                                                                                                                                                                                    let (_x_5 : cell option) = Some C3 in
                                                                                                                                                                                                                    let (_x_6 : cell option) = Some C6 in
                                                                                                                                                                                                                    let (_x_7 : cell option) = Some C4 in
                                                                                                                                                                                                                    let (_x_8 : cell option) = Some C9 in
                                                                                                                                                                                                                    {rows =
                                                                                                                                                                                                                     [[_x_0; _x_1; _x_2; _x_3; _x_4; _x_5; _x_6; _x_7; _x_8];
                                                                                                                                                                                                                      [_x_8; _x_7; _x_5; _x_6; _x_0; _x_2; _x_1; _x_3; _x_4];
                                                                                                                                                                                                                      [_x_6; _x_3; _x_4; _x_7; _x_8; _x_1; _x_2; _x_0; _x_5];
                                                                                                                                                                                                                      [_x_1; _x_4; _x_7; _x_2; _x_5; _x_3; _x_0; _x_8; _x_6];
                                                                                                                                                                                                                      [_x_5; _x_6; _x_8; _x_0; _x_7; _x_4; _x_3; _x_2; _x_1];
                                                                                                                                                                                                                      [_x_2; _x_0; _x_3; _x_1; _x_6; _x_8; _x_4; _x_5; _x_7];
                                                                                                                                                                                                                      [_x_4; _x_2; _x_1; _x_8; _x_3; _x_7; _x_5; _x_6; _x_0];
                                                                                                                                                                                                                      [_x_7; _x_5; _x_0; _x_4; _x_2; _x_6; _x_8; _x_1; _x_3];
                                                                                                                                                                                                                      [_x_3; _x_8; _x_6; _x_5; _x_1; _x_0; _x_7; _x_4; _x_2]]}
                                                                                                                                                                                                                
                                                                                                                                                                                                                Instance

                                                                                                                                                                                                                Let us look at the initial sudoku and its solution side to side:

                                                                                                                                                                                                                In [11]:
                                                                                                                                                                                                                Imandra.display (Document.tbl [[doc_of_sudoku the_problem; Document.s "-->"; doc_of_sudoku CX.s]]) ;;
                                                                                                                                                                                                                
                                                                                                                                                                                                                Out[11]:
                                                                                                                                                                                                                - : unit = ()
                                                                                                                                                                                                                
                                                                                                                                                                                                                8········
                                                                                                                                                                                                                ··36·····
                                                                                                                                                                                                                ·7··9·2··
                                                                                                                                                                                                                ·5···7···
                                                                                                                                                                                                                ····457··
                                                                                                                                                                                                                ···1···3·
                                                                                                                                                                                                                ··1····68
                                                                                                                                                                                                                ··85···1·
                                                                                                                                                                                                                ·9····4··
                                                                                                                                                                                                                -->
                                                                                                                                                                                                                812753649
                                                                                                                                                                                                                943682175
                                                                                                                                                                                                                675491283
                                                                                                                                                                                                                154237896
                                                                                                                                                                                                                369845721
                                                                                                                                                                                                                287169534
                                                                                                                                                                                                                521974368
                                                                                                                                                                                                                438526917
                                                                                                                                                                                                                796318452

                                                                                                                                                                                                                We can manipulate CX.s easily, directly in OCaml:

                                                                                                                                                                                                                In [12]:
                                                                                                                                                                                                                let transpose_sudoku (s:sudoku) : sudoku = {rows = transpose s.rows};;
                                                                                                                                                                                                                
                                                                                                                                                                                                                transpose_sudoku CX.s;;
                                                                                                                                                                                                                
                                                                                                                                                                                                                Out[12]:
                                                                                                                                                                                                                val transpose_sudoku : sudoku -> sudoku = <fun>
                                                                                                                                                                                                                - : sudoku = <document>
                                                                                                                                                                                                                
                                                                                                                                                                                                                896132547
                                                                                                                                                                                                                147568239
                                                                                                                                                                                                                235497186
                                                                                                                                                                                                                764281953
                                                                                                                                                                                                                589346721
                                                                                                                                                                                                                321759468
                                                                                                                                                                                                                612875394
                                                                                                                                                                                                                478923615
                                                                                                                                                                                                                953614872