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 -> Caml.Int.t = <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.029s
details
Expand
smt_stats
num checks7
arith assert lower5
arith pivots3
rlimit count1817
mk clause3
datatype occurs check21
mk bool var50
arith assert upper5
datatype splits3
decisions7
arith add rows7
propagations2
conflicts7
arith fixed eqs4
datatype accessor ax5
arith conflicts1
datatype constructor ax8
num allocs902444373
final checks6
added eqs33
del clause1
arith eq adapter3
memory23.900000
max memory26.560000
Expand
  • start[0.029s]
      not (_x = []) && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
      ==> List.tl _x = []
          || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl _x)))
             (Ordinal.Int (Ordinal.count _x))
  • simplify
    into
    (not
     ((not (_x = []) && Ordinal.count _x >= 0) && Ordinal.count (List.tl _x) >= 0)
     || List.tl _x = [])
    || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl _x)))
       (Ordinal.Int (Ordinal.count _x))
    expansions
    []
    rewrite_steps
      forward_chaining
      • unroll
        expr
        (|Ordinal.<<_116| (|Ordinal.Int_107|
                            (|count_`ty_0 list`_1489| (|get.::.1_1475| …
        expansions
        • unroll
          expr
          (|count_`ty_0 list`_1489| (|get.::.1_1475| _x_1480))
          expansions
          • unroll
            expr
            (|count_`ty_0 list`_1489| _x_1480)
            expansions
            • unsat
              (let ((a!1 (= (|count_`ty_0 list`_1489| _x_1480)
                            (+ 1 (|count_`ty_0 list`_1489| (|get.…

            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 -> Z.t = <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[List.hd _x = [] && _x <> [] && not (_x = [])]
            proof
            detailed proof
            ground_instances3
            definitions0
            inductions0
            search_time
            0.015s
            details
            Expand
            smt_stats
            num checks8
            arith assert lower13
            arith pivots8
            rlimit count6369
            mk clause41
            datatype occurs check32
            mk bool var126
            arith assert upper14
            datatype splits10
            decisions25
            arith add rows17
            propagations80
            conflicts13
            arith fixed eqs7
            datatype accessor ax14
            arith conflicts2
            datatype constructor ax21
            num allocs1008227906
            final checks9
            added eqs101
            del clause8
            arith eq adapter10
            memory25.130000
            max memory26.560000
            Expand
            • start[0.015s]
                (List.hd _x = [] && _x <> [])
                && not (_x = [])
                   && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                ==> not
                    ((List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                     && not (List.tl _x = []))
                    && not
                       (not (List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                        && not (List.tl _x = []))
                    || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl _x)))
                       (Ordinal.Int (Ordinal.count _x))
            • simplify
              into
              (not
               ((((List.hd _x = [] && _x <> []) && not (_x = [])) && Ordinal.count _x >= 0)
                && Ordinal.count (List.tl _x) >= 0)
               || not
                  ((List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                   && not (List.tl _x = []))
                  && not
                     (not (List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                      && not (List.tl _x = [])))
              || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl _x)))
                 (Ordinal.Int (Ordinal.count _x))
              expansions
              []
              rewrite_steps
                forward_chaining
                • unroll
                  expr
                  (|Ordinal.<<_116| (|Ordinal.Int_107|
                                      (|count_`ty_0 list list`_1519| (|get.::.1_1…
                  expansions
                  • unroll
                    expr
                    (|count_`ty_0 list list`_1519| (|get.::.1_1502| _x_1508))
                    expansions
                    • unroll
                      expr
                      (|count_`ty_0 list list`_1519| _x_1508)
                      expansions
                      • unsat
                        (let ((a!1 (= (ite (>= (|count_`ty_0 list`_1521| |[]_2|) 0)
                                           (|count_`ty_0 list`_1…

                      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 (List.hd _x = [] && _x <> []) && not (_x = [])]
                      proof
                      detailed proof
                      ground_instances3
                      definitions0
                      inductions0
                      search_time
                      0.015s
                      details
                      Expand
                      smt_stats
                      num checks8
                      arith assert lower11
                      arith pivots6
                      rlimit count3305
                      mk clause36
                      datatype occurs check55
                      mk bool var150
                      arith assert upper14
                      datatype splits22
                      decisions39
                      arith add rows14
                      propagations67
                      conflicts14
                      arith fixed eqs7
                      datatype accessor ax16
                      arith conflicts2
                      arith assert diseq1
                      datatype constructor ax31
                      num allocs979232574
                      final checks13
                      added eqs123
                      del clause7
                      arith eq adapter10
                      memory22.220000
                      max memory26.560000
                      Expand
                      • start[0.015s]
                          not (List.hd _x = [] && _x <> [])
                          && not (_x = [])
                             && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                          ==> not
                              ((List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                               && not (List.tl _x = []))
                              && not
                                 (not (List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                  && not (List.tl _x = []))
                              || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl _x)))
                                 (Ordinal.Int (Ordinal.count _x))
                      • simplify
                        into
                        (not
                         (((not (List.hd _x = [] && _x <> []) && not (_x = []))
                           && Ordinal.count _x >= 0)
                          && Ordinal.count (List.tl _x) >= 0)
                         || not
                            ((List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                             && not (List.tl _x = []))
                            && not
                               (not (List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                && not (List.tl _x = [])))
                        || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl _x)))
                           (Ordinal.Int (Ordinal.count _x))
                        expansions
                        []
                        rewrite_steps
                          forward_chaining
                          • unroll
                            expr
                            (|Ordinal.<<_116| (|Ordinal.Int_107|
                                                (|count_`ty_0 list list`_1519| (|get.::.1_1…
                            expansions
                            • unroll
                              expr
                              (|count_`ty_0 list list`_1519| (|get.::.1_1502| _x_1508))
                              expansions
                              • unroll
                                expr
                                (|count_`ty_0 list list`_1519| _x_1508)
                                expansions
                                • unsat
                                  (let ((a!1 (ite (>= (|count_`ty_0 list`_1521| (|get.::.0_1501| _x_1508)) 0)
                                                  (|count_…

                                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[List.hd _x = [] && _x <> [] && not (_x = [])]
                                proof
                                detailed proof
                                ground_instances3
                                definitions0
                                inductions0
                                search_time
                                0.023s
                                details
                                Expand
                                smt_stats
                                num checks8
                                arith assert lower13
                                arith pivots8
                                rlimit count6369
                                mk clause41
                                datatype occurs check32
                                mk bool var126
                                arith assert upper14
                                datatype splits10
                                decisions25
                                arith add rows17
                                propagations80
                                conflicts13
                                arith fixed eqs7
                                datatype accessor ax14
                                arith conflicts2
                                datatype constructor ax21
                                num allocs1120544087
                                final checks9
                                added eqs101
                                del clause8
                                arith eq adapter10
                                memory25.660000
                                max memory26.560000
                                Expand
                                • start[0.023s]
                                    (List.hd _x = [] && _x <> [])
                                    && not (_x = [])
                                       && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                                    ==> not
                                        ((List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                         && not (List.tl _x = []))
                                        && not
                                           (not (List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                            && not (List.tl _x = []))
                                        || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl _x)))
                                           (Ordinal.Int (Ordinal.count _x))
                                • simplify
                                  into
                                  (not
                                   ((((List.hd _x = [] && _x <> []) && not (_x = [])) && Ordinal.count _x >= 0)
                                    && Ordinal.count (List.tl _x) >= 0)
                                   || not
                                      ((List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                       && not (List.tl _x = []))
                                      && not
                                         (not (List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                          && not (List.tl _x = [])))
                                  || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl _x)))
                                     (Ordinal.Int (Ordinal.count _x))
                                  expansions
                                  []
                                  rewrite_steps
                                    forward_chaining
                                    • unroll
                                      expr
                                      (|Ordinal.<<_116| (|Ordinal.Int_107|
                                                          (|count_`ty_0 list list`_1550| (|get.::.1_1…
                                      expansions
                                      • unroll
                                        expr
                                        (|count_`ty_0 list list`_1550| (|get.::.1_1533| _x_1539))
                                        expansions
                                        • unroll
                                          expr
                                          (|count_`ty_0 list list`_1550| _x_1539)
                                          expansions
                                          • unsat
                                            (let ((a!1 (= (ite (>= (|count_`ty_0 list`_1552| |[]_2|) 0)
                                                               (|count_`ty_0 list`_1…

                                          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 (List.hd _x = [] && _x <> []) && not (_x = [])]
                                          proof
                                          detailed proof
                                          ground_instances3
                                          definitions0
                                          inductions0
                                          search_time
                                          0.058s
                                          details
                                          Expand
                                          smt_stats
                                          num checks8
                                          arith assert lower11
                                          arith pivots6
                                          rlimit count3305
                                          mk clause36
                                          datatype occurs check55
                                          mk bool var150
                                          arith assert upper14
                                          datatype splits22
                                          decisions39
                                          arith add rows14
                                          propagations67
                                          conflicts14
                                          arith fixed eqs7
                                          datatype accessor ax16
                                          arith conflicts2
                                          arith assert diseq1
                                          datatype constructor ax31
                                          num allocs1089424561
                                          final checks13
                                          added eqs123
                                          del clause7
                                          arith eq adapter10
                                          memory22.750000
                                          max memory26.560000
                                          Expand
                                          • start[0.058s]
                                              not (List.hd _x = [] && _x <> [])
                                              && not (_x = [])
                                                 && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                                              ==> not
                                                  ((List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                                   && not (List.tl _x = []))
                                                  && not
                                                     (not (List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                                      && not (List.tl _x = []))
                                                  || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl _x)))
                                                     (Ordinal.Int (Ordinal.count _x))
                                          • simplify
                                            into
                                            (not
                                             (((not (List.hd _x = [] && _x <> []) && not (_x = []))
                                               && Ordinal.count _x >= 0)
                                              && Ordinal.count (List.tl _x) >= 0)
                                             || not
                                                ((List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                                 && not (List.tl _x = []))
                                                && not
                                                   (not (List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                                    && not (List.tl _x = [])))
                                            || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl _x)))
                                               (Ordinal.Int (Ordinal.count _x))
                                            expansions
                                            []
                                            rewrite_steps
                                              forward_chaining
                                              • unroll
                                                expr
                                                (|Ordinal.<<_116| (|Ordinal.Int_107|
                                                                    (|count_`ty_0 list list`_1550| (|get.::.1_1…
                                                expansions
                                                • unroll
                                                  expr
                                                  (|count_`ty_0 list list`_1550| (|get.::.1_1533| _x_1539))
                                                  expansions
                                                  • unroll
                                                    expr
                                                    (|count_`ty_0 list list`_1550| _x_1539)
                                                    expansions
                                                    • unsat
                                                      (let ((a!1 (ite (>= (|count_`ty_0 list`_1552| (|get.::.0_1532| _x_1539)) 0)
                                                                      (|count_…

                                                    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 ordinalOrdinal.Int (if measure_transpose l >= 0 then measure_transpose l else 0)
                                                    sub ordinalOrdinal.Int (if measure_transpose ((List.tl (List.hd l)) :: (transpose3 (List.tl l))) >= 0 then measure_transpose ((List.tl (List.hd l)) :: (transpose3 (List.tl l))) else 0)
                                                    path[not (List.hd l = [] && l <> []) && not (l = [])]
                                                    proof
                                                    detailed proof
                                                    ground_instances3
                                                    definitions0
                                                    inductions0
                                                    search_time
                                                    0.028s
                                                    details
                                                    Expand
                                                    smt_stats
                                                    num checks7
                                                    arith assert lower5
                                                    arith pivots2
                                                    rlimit count2047
                                                    mk clause4
                                                    datatype occurs check34
                                                    mk bool var60
                                                    arith assert upper3
                                                    datatype splits7
                                                    decisions12
                                                    arith add rows2
                                                    propagations3
                                                    conflicts8
                                                    arith fixed eqs1
                                                    datatype accessor ax7
                                                    arith conflicts1
                                                    datatype constructor ax15
                                                    num allocs1182373956
                                                    final checks9
                                                    added eqs44
                                                    del clause4
                                                    arith eq adapter2
                                                    memory26.390000
                                                    max memory26.560000
                                                    Expand
                                                    • start[0.028s]
                                                        not (List.hd l = [] && l <> [])
                                                        && not (l = [])
                                                           && (if (if l = [] then 0 else List.length (List.hd l)) >= 0
                                                               then if l = [] then 0 else List.length (List.hd l) else 0)
                                                              >= 0
                                                              && (if (if (List.tl (List.hd l)) :: (transpose3 …) = [] then 0
                                                                      else List.length …)
                                                                     >= 0
                                                                  then
                                                                    if (List.tl (List.hd l)) :: (transpose3 …) = [] then 0
                                                                    else List.length …
                                                                  else 0)
                                                                 >= 0
                                                        ==> not
                                                            (not (List.tl (List.hd l) = [] && true)
                                                             && not ((List.tl (List.hd l)) :: (transpose3 …) = []))
                                                            || Ordinal.<<
                                                               (Ordinal.Int
                                                                (if (if (List.tl (List.hd l)) :: (transpose3 …) = [] then 0
                                                                     else List.length …)
                                                                    >= 0
                                                                 then
                                                                   if (List.tl (List.hd l)) :: (transpose3 …) = [] then 0
                                                                   else List.length …
                                                                 else 0))
                                                               (Ordinal.Int
                                                                (if (if l = [] then 0 else List.length (List.hd l)) >= 0
                                                                 then if l = [] then 0 else List.length (List.hd l) else 0))
                                                    • simplify
                                                      into
                                                      (not
                                                       (((not (List.hd l = [] && l <> []) && not (l = []))
                                                         && (if (if l = [] then 0 else List.length (List.hd l)) >= 0
                                                             then if l = [] then 0 else List.length (List.hd l) else 0)
                                                            >= 0)
                                                        && (if List.length (List.tl (List.hd l)) >= 0
                                                            then List.length (List.tl (List.hd l)) else 0)
                                                           >= 0)
                                                       || List.tl (List.hd l) = [])
                                                      || Ordinal.<<
                                                         (Ordinal.Int
                                                          (if List.length (List.tl (List.hd l)) >= 0
                                                           then List.length (List.tl (List.hd l)) else 0))
                                                         (Ordinal.Int
                                                          (if (if l = [] then 0 else List.length (List.hd l)) >= 0
                                                           then if l = [] then 0 else List.length (List.hd l) else 0))
                                                      expansions
                                                      []
                                                      rewrite_steps
                                                        forward_chaining
                                                        • unroll
                                                          expr
                                                          (let ((a!1 (>= (|List.length_1619| (|get.::.1_1593| (|get.::.0_1595| l_1612)))
                                                                         0))
                                                            …
                                                          expansions
                                                          • unroll
                                                            expr
                                                            (|List.length_1619| (|get.::.1_1593| (|get.::.0_1595| l_1612)))
                                                            expansions
                                                            • unroll
                                                              expr
                                                              (|List.length_1619| (|get.::.0_1595| l_1612))
                                                              expansions
                                                              • unsat
                                                                (let ((a!1 (+ 1 (|List.length_1619| (|get.::.1_1593| (|get.::.0_1595| l_1612)))))
                                                                      (a!7 (not (a…

                                                              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.091s
                                                              details
                                                              Expand
                                                              smt_stats
                                                              num checks7
                                                              arith assert lower5
                                                              arith pivots3
                                                              rlimit count2039
                                                              mk clause3
                                                              datatype occurs check30
                                                              mk bool var66
                                                              arith assert upper5
                                                              datatype splits6
                                                              decisions14
                                                              arith add rows7
                                                              propagations1
                                                              conflicts10
                                                              arith fixed eqs4
                                                              datatype accessor ax8
                                                              arith conflicts1
                                                              datatype constructor ax16
                                                              num allocs1246375308
                                                              final checks6
                                                              added eqs52
                                                              del clause1
                                                              arith eq adapter3
                                                              memory26.930000
                                                              max memory26.930000
                                                              Expand
                                                              • start[0.091s]
                                                                  not (l = [])
                                                                  && not (x = Z)
                                                                     && Ordinal.count x >= 0 && Ordinal.count (Destruct(S, 0, x)) >= 0
                                                                  ==> not (not (List.tl l = []) && not (Destruct(S, 0, x) = Z))
                                                                      || Ordinal.<< (Ordinal.Int (Ordinal.count (Destruct(S, 0, x))))
                                                                         (Ordinal.Int (Ordinal.count x))
                                                              • simplify
                                                                into
                                                                (not
                                                                 (((not (l = []) && not (x = Z)) && Ordinal.count x >= 0)
                                                                  && Ordinal.count (Destruct(S, 0, x)) >= 0)
                                                                 || not (not (List.tl l = []) && not (Destruct(S, 0, x) = Z)))
                                                                || Ordinal.<< (Ordinal.Int (Ordinal.count (Destruct(S, 0, x))))
                                                                   (Ordinal.Int (Ordinal.count x))
                                                                expansions
                                                                []
                                                                rewrite_steps
                                                                  forward_chaining
                                                                  • unroll
                                                                    expr
                                                                    (|Ordinal.<<_116| (|Ordinal.Int_107| (count_nat_1651 (|get.S.0_1630| x_1640)))
                                                                                      (|O…
                                                                    expansions
                                                                    • unroll
                                                                      expr
                                                                      (count_nat_1651 (|get.S.0_1630| x_1640))
                                                                      expansions
                                                                      • unroll
                                                                        expr
                                                                        (count_nat_1651 x_1640)
                                                                        expansions
                                                                        • unsat
                                                                          (let ((a!1 (= (count_nat_1651 x_1640)
                                                                                        (+ 1 (count_nat_1651 (|get.S.0_1630| x_1640)))))…

                                                                        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.174s
                                                                        details
                                                                        Expand
                                                                        smt_stats
                                                                        num checks7
                                                                        arith assert lower5
                                                                        arith pivots3
                                                                        rlimit count2039
                                                                        mk clause3
                                                                        datatype occurs check30
                                                                        mk bool var66
                                                                        arith assert upper5
                                                                        datatype splits6
                                                                        decisions14
                                                                        arith add rows7
                                                                        propagations1
                                                                        conflicts10
                                                                        arith fixed eqs4
                                                                        datatype accessor ax8
                                                                        arith conflicts1
                                                                        datatype constructor ax16
                                                                        num allocs1309619977
                                                                        final checks6
                                                                        added eqs52
                                                                        del clause1
                                                                        arith eq adapter3
                                                                        memory27.280000
                                                                        max memory27.280000
                                                                        Expand
                                                                        • start[0.174s]
                                                                            not (y = [])
                                                                            && not (x = Z)
                                                                               && Ordinal.count x >= 0 && Ordinal.count (Destruct(S, 0, x)) >= 0
                                                                            ==> not (not (List.tl y = []) && not (Destruct(S, 0, x) = Z))
                                                                                || Ordinal.<< (Ordinal.Int (Ordinal.count (Destruct(S, 0, x))))
                                                                                   (Ordinal.Int (Ordinal.count x))
                                                                        • simplify
                                                                          into
                                                                          (not
                                                                           (((not (y = []) && not (x = Z)) && Ordinal.count x >= 0)
                                                                            && Ordinal.count (Destruct(S, 0, x)) >= 0)
                                                                           || not (not (List.tl y = []) && not (Destruct(S, 0, x) = Z)))
                                                                          || Ordinal.<< (Ordinal.Int (Ordinal.count (Destruct(S, 0, x))))
                                                                             (Ordinal.Int (Ordinal.count x))
                                                                          expansions
                                                                          []
                                                                          rewrite_steps
                                                                            forward_chaining
                                                                            • unroll
                                                                              expr
                                                                              (|Ordinal.<<_116| (|Ordinal.Int_107| (count_nat_1677 (|get.S.0_1657| x_1666)))
                                                                                                (|O…
                                                                              expansions
                                                                              • unroll
                                                                                expr
                                                                                (count_nat_1677 (|get.S.0_1657| x_1666))
                                                                                expansions
                                                                                • unroll
                                                                                  expr
                                                                                  (count_nat_1677 x_1666)
                                                                                  expansions
                                                                                  • unsat
                                                                                    (let ((a!1 (= (count_nat_1677 x_1666)
                                                                                                  (+ 1 (count_nat_1677 (|get.S.0_1657| x_1666)))))…

                                                                                  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.099s
                                                                                  details
                                                                                  Expand
                                                                                  smt_stats
                                                                                  num checks7
                                                                                  arith assert lower5
                                                                                  arith pivots3
                                                                                  rlimit count1932
                                                                                  mk clause3
                                                                                  datatype occurs check18
                                                                                  mk bool var52
                                                                                  arith assert upper5
                                                                                  datatype splits3
                                                                                  decisions7
                                                                                  arith add rows7
                                                                                  propagations2
                                                                                  conflicts7
                                                                                  arith fixed eqs4
                                                                                  datatype accessor ax5
                                                                                  arith conflicts1
                                                                                  datatype constructor ax8
                                                                                  num allocs1376072443
                                                                                  final checks5
                                                                                  added eqs33
                                                                                  del clause1
                                                                                  arith eq adapter3
                                                                                  memory27.830000
                                                                                  max memory30.590000
                                                                                  Expand
                                                                                  • start[0.099s]
                                                                                      not (x = List.hd y)
                                                                                      && not (y = []) && Ordinal.count y >= 0 && Ordinal.count (List.tl y) >= 0
                                                                                      ==> not (not (x = List.hd (List.tl y)) && not (List.tl y = []))
                                                                                          || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl y)))
                                                                                             (Ordinal.Int (Ordinal.count y))
                                                                                  • simplify
                                                                                    into
                                                                                    (not
                                                                                     (((not (x = List.hd y) && not (y = [])) && Ordinal.count y >= 0)
                                                                                      && Ordinal.count (List.tl y) >= 0)
                                                                                     || not (not (x = List.hd (List.tl y)) && not (List.tl y = [])))
                                                                                    || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl y)))
                                                                                       (Ordinal.Int (Ordinal.count y))
                                                                                    expansions
                                                                                    []
                                                                                    rewrite_steps
                                                                                      forward_chaining
                                                                                      • unroll
                                                                                        expr
                                                                                        (|Ordinal.<<_116| (|Ordinal.Int_107|
                                                                                                            (|count_`ty_0 list`_1702| (|get.::.1_1685| …
                                                                                        expansions
                                                                                        • unroll
                                                                                          expr
                                                                                          (|count_`ty_0 list`_1702| (|get.::.1_1685| y_1692))
                                                                                          expansions
                                                                                          • unroll
                                                                                            expr
                                                                                            (|count_`ty_0 list`_1702| y_1692)
                                                                                            expansions
                                                                                            • unsat
                                                                                              (let ((a!1 (= (|count_`ty_0 list`_1702| y_1692)
                                                                                                            (+ 1 (|count_`ty_0 list`_1702| (|get.:…

                                                                                            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.037s
                                                                                            details
                                                                                            Expand
                                                                                            smt_stats
                                                                                            num checks9
                                                                                            arith assert lower6
                                                                                            arith pivots4
                                                                                            rlimit count2353
                                                                                            mk clause8
                                                                                            datatype occurs check21
                                                                                            mk bool var58
                                                                                            arith assert upper4
                                                                                            datatype splits3
                                                                                            decisions15
                                                                                            arith add rows5
                                                                                            propagations5
                                                                                            conflicts7
                                                                                            arith fixed eqs3
                                                                                            datatype accessor ax5
                                                                                            arith conflicts1
                                                                                            datatype constructor ax6
                                                                                            num allocs1416590305
                                                                                            final checks6
                                                                                            added eqs31
                                                                                            del clause1
                                                                                            arith eq adapter3
                                                                                            memory31.080000
                                                                                            max memory31.080000
                                                                                            Expand
                                                                                            • start[0.037s]
                                                                                                not (elem (List.hd x) (List.tl x))
                                                                                                && not (x = []) && Ordinal.count x >= 0 && Ordinal.count (List.tl x) >= 0
                                                                                                ==> not
                                                                                                    (not (elem (List.hd (List.tl x)) (List.tl (List.tl x)))
                                                                                                     && not (List.tl x = []))
                                                                                                    || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl x)))
                                                                                                       (Ordinal.Int (Ordinal.count x))
                                                                                            • simplify
                                                                                              into
                                                                                              (not
                                                                                               (((not (elem (List.hd x) (List.tl x)) && not (x = []))
                                                                                                 && Ordinal.count x >= 0)
                                                                                                && Ordinal.count (List.tl x) >= 0)
                                                                                               || not
                                                                                                  (not (elem (List.hd (List.tl x)) (List.tl (List.tl x)))
                                                                                                   && not (List.tl x = [])))
                                                                                              || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl x)))
                                                                                                 (Ordinal.Int (Ordinal.count x))
                                                                                              expansions
                                                                                              []
                                                                                              rewrite_steps
                                                                                                forward_chaining
                                                                                                • unroll
                                                                                                  expr
                                                                                                  (|Ordinal.<<_116| (|Ordinal.Int_107|
                                                                                                                      (|count_`ty_0 list`_1728| (|get.::.1_1709| …
                                                                                                  expansions
                                                                                                  • unroll
                                                                                                    expr
                                                                                                    (elem_1714 (|get.::.0_1708| (|get.::.1_1709| x_1719))
                                                                                                               (|get.::.1_1709| (|get.::.1_1709| x…
                                                                                                    expansions
                                                                                                    • unroll
                                                                                                      expr
                                                                                                      (|count_`ty_0 list`_1728| (|get.::.1_1709| x_1719))
                                                                                                      expansions
                                                                                                      • unroll
                                                                                                        expr
                                                                                                        (|count_`ty_0 list`_1728| x_1719)
                                                                                                        expansions
                                                                                                        • unsat
                                                                                                          (let ((a!1 (= (|count_`ty_0 list`_1728| x_1719)
                                                                                                                        (+ 1 (|count_`ty_0 list`_1728| (|get.:…

                                                                                                        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.040s
                                                                                                        details
                                                                                                        Expand
                                                                                                        smt_stats
                                                                                                        num checks7
                                                                                                        arith assert lower5
                                                                                                        arith pivots3
                                                                                                        rlimit count1978
                                                                                                        mk clause3
                                                                                                        datatype occurs check29
                                                                                                        mk bool var64
                                                                                                        arith assert upper5
                                                                                                        datatype splits9
                                                                                                        decisions16
                                                                                                        arith add rows7
                                                                                                        propagations2
                                                                                                        conflicts7
                                                                                                        arith fixed eqs4
                                                                                                        datatype accessor ax10
                                                                                                        arith conflicts1
                                                                                                        datatype constructor ax16
                                                                                                        num allocs1485836157
                                                                                                        final checks8
                                                                                                        added eqs49
                                                                                                        del clause1
                                                                                                        arith eq adapter3
                                                                                                        memory31.430000
                                                                                                        max memory31.430000
                                                                                                        Expand
                                                                                                        • start[0.040s]
                                                                                                            not (l = []) && Ordinal.count l >= 0 && Ordinal.count (List.tl l) >= 0
                                                                                                            ==> List.tl l = []
                                                                                                                || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl l)))
                                                                                                                   (Ordinal.Int (Ordinal.count l))
                                                                                                        • simplify
                                                                                                          into
                                                                                                          (not
                                                                                                           ((not (l = []) && Ordinal.count l >= 0) && Ordinal.count (List.tl l) >= 0)
                                                                                                           || List.tl l = [])
                                                                                                          || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl l)))
                                                                                                             (Ordinal.Int (Ordinal.count l))
                                                                                                          expansions
                                                                                                          []
                                                                                                          rewrite_steps
                                                                                                            forward_chaining
                                                                                                            • unroll
                                                                                                              expr
                                                                                                              (|Ordinal.<<_116| (|Ordinal.Int_107|
                                                                                                                                  (|count_`ty_0 option list`_1757| (|get.::.1…
                                                                                                              expansions
                                                                                                              • unroll
                                                                                                                expr
                                                                                                                (|count_`ty_0 option list`_1757| (|get.::.1_1738| l_1748))
                                                                                                                expansions
                                                                                                                • unroll
                                                                                                                  expr
                                                                                                                  (|count_`ty_0 option list`_1757| l_1748)
                                                                                                                  expansions
                                                                                                                  • unsat
                                                                                                                    (let ((a!1 (= (|count_`ty_0 option list`_1757| l_1748)
                                                                                                                                  (+ 2 (|count_`ty_0 option list`…

                                                                                                                  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.099s
                                                                                                                  details
                                                                                                                  Expand
                                                                                                                  smt_stats
                                                                                                                  num checks8
                                                                                                                  arith assert lower15
                                                                                                                  arith pivots8
                                                                                                                  rlimit count2597
                                                                                                                  mk clause12
                                                                                                                  datatype occurs check29
                                                                                                                  mk bool var87
                                                                                                                  arith assert upper12
                                                                                                                  datatype splits9
                                                                                                                  decisions24
                                                                                                                  arith add rows12
                                                                                                                  propagations10
                                                                                                                  conflicts10
                                                                                                                  arith fixed eqs7
                                                                                                                  datatype accessor ax10
                                                                                                                  arith conflicts2
                                                                                                                  arith assert diseq1
                                                                                                                  datatype constructor ax16
                                                                                                                  num allocs1560635068
                                                                                                                  final checks8
                                                                                                                  added eqs58
                                                                                                                  del clause5
                                                                                                                  arith eq adapter10
                                                                                                                  memory32.080000
                                                                                                                  max memory34.890000
                                                                                                                  Expand
                                                                                                                  • start[0.099s]
                                                                                                                      not (_x = []) && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                                                                                                                      ==> List.tl _x = []
                                                                                                                          || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl _x)))
                                                                                                                             (Ordinal.Int (Ordinal.count _x))
                                                                                                                  • simplify
                                                                                                                    into
                                                                                                                    (not
                                                                                                                     ((not (_x = []) && Ordinal.count _x >= 0) && Ordinal.count (List.tl _x) >= 0)
                                                                                                                     || List.tl _x = [])
                                                                                                                    || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl _x)))
                                                                                                                       (Ordinal.Int (Ordinal.count _x))
                                                                                                                    expansions
                                                                                                                    []
                                                                                                                    rewrite_steps
                                                                                                                      forward_chaining
                                                                                                                      • unroll
                                                                                                                        expr
                                                                                                                        (|Ordinal.<<_116| (|Ordinal.Int_107|
                                                                                                                                            (|count_`ty_0 list list`_1816| (|get.::.1_1…
                                                                                                                        expansions
                                                                                                                        • unroll
                                                                                                                          expr
                                                                                                                          (|count_`ty_0 list list`_1816| (|get.::.1_1796| _x_1807))
                                                                                                                          expansions
                                                                                                                          • unroll
                                                                                                                            expr
                                                                                                                            (|count_`ty_0 list list`_1816| _x_1807)
                                                                                                                            expansions
                                                                                                                            • unsat
                                                                                                                              (let ((a!1 (ite (>= (|count_`ty_0 list`_1818| (|get.::.0_1795| _x_1807)) 0)
                                                                                                                                              (|count_…

                                                                                                                            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.042s
                                                                                                                            details
                                                                                                                            Expand
                                                                                                                            smt_stats
                                                                                                                            num checks8
                                                                                                                            arith assert lower15
                                                                                                                            arith pivots8
                                                                                                                            rlimit count2597
                                                                                                                            mk clause12
                                                                                                                            datatype occurs check29
                                                                                                                            mk bool var87
                                                                                                                            arith assert upper12
                                                                                                                            datatype splits9
                                                                                                                            decisions24
                                                                                                                            arith add rows12
                                                                                                                            propagations10
                                                                                                                            conflicts10
                                                                                                                            arith fixed eqs7
                                                                                                                            datatype accessor ax10
                                                                                                                            arith conflicts2
                                                                                                                            arith assert diseq1
                                                                                                                            datatype constructor ax16
                                                                                                                            num allocs1634841114
                                                                                                                            final checks8
                                                                                                                            added eqs58
                                                                                                                            del clause5
                                                                                                                            arith eq adapter10
                                                                                                                            memory32.620000
                                                                                                                            max memory34.890000
                                                                                                                            Expand
                                                                                                                            • start[0.042s]
                                                                                                                                not (_x = []) && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                                                                                                                                ==> List.tl _x = []
                                                                                                                                    || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl _x)))
                                                                                                                                       (Ordinal.Int (Ordinal.count _x))
                                                                                                                            • simplify
                                                                                                                              into
                                                                                                                              (not
                                                                                                                               ((not (_x = []) && Ordinal.count _x >= 0) && Ordinal.count (List.tl _x) >= 0)
                                                                                                                               || List.tl _x = [])
                                                                                                                              || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl _x)))
                                                                                                                                 (Ordinal.Int (Ordinal.count _x))
                                                                                                                              expansions
                                                                                                                              []
                                                                                                                              rewrite_steps
                                                                                                                                forward_chaining
                                                                                                                                • unroll
                                                                                                                                  expr
                                                                                                                                  (|Ordinal.<<_116| (|Ordinal.Int_107|
                                                                                                                                                      (|count_`ty_0 list list`_1854| (|get.::.1_1…
                                                                                                                                  expansions
                                                                                                                                  • unroll
                                                                                                                                    expr
                                                                                                                                    (|count_`ty_0 list list`_1854| (|get.::.1_1828| _x_1845))
                                                                                                                                    expansions
                                                                                                                                    • unroll
                                                                                                                                      expr
                                                                                                                                      (|count_`ty_0 list list`_1854| _x_1845)
                                                                                                                                      expansions
                                                                                                                                      • unsat
                                                                                                                                        (let ((a!1 (ite (>= (|count_`ty_0 list`_1856| (|get.::.0_1827| _x_1845)) 0)
                                                                                                                                                        (|count_…

                                                                                                                                      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.040s
                                                                                                                                      details
                                                                                                                                      Expand
                                                                                                                                      smt_stats
                                                                                                                                      num checks8
                                                                                                                                      arith assert lower15
                                                                                                                                      arith pivots8
                                                                                                                                      rlimit count2597
                                                                                                                                      mk clause12
                                                                                                                                      datatype occurs check29
                                                                                                                                      mk bool var87
                                                                                                                                      arith assert upper12
                                                                                                                                      datatype splits9
                                                                                                                                      decisions24
                                                                                                                                      arith add rows12
                                                                                                                                      propagations10
                                                                                                                                      conflicts10
                                                                                                                                      arith fixed eqs7
                                                                                                                                      datatype accessor ax10
                                                                                                                                      arith conflicts2
                                                                                                                                      arith assert diseq1
                                                                                                                                      datatype constructor ax16
                                                                                                                                      num allocs1708787747
                                                                                                                                      final checks8
                                                                                                                                      added eqs58
                                                                                                                                      del clause5
                                                                                                                                      arith eq adapter10
                                                                                                                                      memory33.150000
                                                                                                                                      max memory34.890000
                                                                                                                                      Expand
                                                                                                                                      • start[0.040s]
                                                                                                                                          not (_x = []) && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                                                                                                                                          ==> List.tl _x = []
                                                                                                                                              || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl _x)))
                                                                                                                                                 (Ordinal.Int (Ordinal.count _x))
                                                                                                                                      • simplify
                                                                                                                                        into
                                                                                                                                        (not
                                                                                                                                         ((not (_x = []) && Ordinal.count _x >= 0) && Ordinal.count (List.tl _x) >= 0)
                                                                                                                                         || List.tl _x = [])
                                                                                                                                        || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl _x)))
                                                                                                                                           (Ordinal.Int (Ordinal.count _x))
                                                                                                                                        expansions
                                                                                                                                        []
                                                                                                                                        rewrite_steps
                                                                                                                                          forward_chaining
                                                                                                                                          • unroll
                                                                                                                                            expr
                                                                                                                                            (|Ordinal.<<_116| (|Ordinal.Int_107|
                                                                                                                                                                (|count_`ty_0 list list`_1887| (|get.::.1_1…
                                                                                                                                            expansions
                                                                                                                                            • unroll
                                                                                                                                              expr
                                                                                                                                              (|count_`ty_0 list list`_1887| (|get.::.1_1866| _x_1878))
                                                                                                                                              expansions
                                                                                                                                              • unroll
                                                                                                                                                expr
                                                                                                                                                (|count_`ty_0 list list`_1887| _x_1878)
                                                                                                                                                expansions
                                                                                                                                                • unsat
                                                                                                                                                  (let ((a!1 (ite (>= (|count_`ty_0 list`_1889| (|get.::.0_1865| _x_1878)) 0)
                                                                                                                                                                  (|count_…

                                                                                                                                                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_instances12
                                                                                                                                                definitions0
                                                                                                                                                inductions0
                                                                                                                                                search_time
                                                                                                                                                0.223s
                                                                                                                                                details
                                                                                                                                                Expand
                                                                                                                                                smt_stats
                                                                                                                                                arith offset eqs58
                                                                                                                                                num checks26
                                                                                                                                                arith assert lower400
                                                                                                                                                arith pivots122
                                                                                                                                                rlimit count45932
                                                                                                                                                mk clause488
                                                                                                                                                datatype occurs check158
                                                                                                                                                mk bool var1053
                                                                                                                                                arith assert upper374
                                                                                                                                                datatype splits74
                                                                                                                                                decisions946
                                                                                                                                                arith add rows741
                                                                                                                                                arith bound prop59
                                                                                                                                                propagations1085
                                                                                                                                                interface eqs11
                                                                                                                                                conflicts85
                                                                                                                                                arith fixed eqs155
                                                                                                                                                datatype accessor ax106
                                                                                                                                                minimized lits21
                                                                                                                                                arith conflicts24
                                                                                                                                                arith assert diseq121
                                                                                                                                                datatype constructor ax279
                                                                                                                                                num allocs1858252579
                                                                                                                                                final checks40
                                                                                                                                                added eqs1358
                                                                                                                                                del clause246
                                                                                                                                                arith eq adapter258
                                                                                                                                                memory28.520000
                                                                                                                                                max memory34.890000
                                                                                                                                                Expand
                                                                                                                                                • start[0.223s]
                                                                                                                                                    not (List.tl (List.tl _x) = [])
                                                                                                                                                    && not (List.tl _x = [])
                                                                                                                                                       && not (_x = [])
                                                                                                                                                          && Ordinal.count _x >= 0
                                                                                                                                                             && Ordinal.count (List.tl (List.tl (List.tl _x))) >= 0
                                                                                                                                                    ==> not
                                                                                                                                                        (not (List.tl (List.tl (List.tl (List.tl (List.tl _x)))) = [])
                                                                                                                                                         && not (List.tl (List.tl (List.tl (List.tl _x))) = [])
                                                                                                                                                            && not (List.tl (List.tl (List.tl _x)) = []))
                                                                                                                                                        || Ordinal.<<
                                                                                                                                                           (Ordinal.Int (Ordinal.count (List.tl (List.tl (List.tl _x)))))
                                                                                                                                                           (Ordinal.Int (Ordinal.count _x))
                                                                                                                                                • simplify
                                                                                                                                                  into
                                                                                                                                                  (not
                                                                                                                                                   ((((not (List.tl (List.tl _x) = []) && not (List.tl _x = []))
                                                                                                                                                      && not (_x = []))
                                                                                                                                                     && Ordinal.count _x >= 0)
                                                                                                                                                    && Ordinal.count (List.tl (List.tl (List.tl _x))) >= 0)
                                                                                                                                                   || not
                                                                                                                                                      ((not (List.tl (List.tl (List.tl (List.tl (List.tl _x)))) = [])
                                                                                                                                                        && not (List.tl (List.tl (List.tl (List.tl _x))) = []))
                                                                                                                                                       && not (List.tl (List.tl (List.tl _x)) = [])))
                                                                                                                                                  || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl (List.tl (List.tl _x)))))
                                                                                                                                                     (Ordinal.Int (Ordinal.count _x))
                                                                                                                                                  expansions
                                                                                                                                                  []
                                                                                                                                                  rewrite_steps
                                                                                                                                                    forward_chaining
                                                                                                                                                    • unroll
                                                                                                                                                      expr
                                                                                                                                                      (let ((a!1 (|count_`ty_0 list list`_1922|
                                                                                                                                                                   (|get.::.1_1899| (|get.::.1_1899| (|get.::.1_…
                                                                                                                                                      expansions
                                                                                                                                                      • unroll
                                                                                                                                                        expr
                                                                                                                                                        (|count_`ty_0 list list`_1922|
                                                                                                                                                          (|get.::.1_1899| (|get.::.1_1899| (|get.::.1_1899| _x_1913))))
                                                                                                                                                        expansions
                                                                                                                                                        • unroll
                                                                                                                                                          expr
                                                                                                                                                          (|count_`ty_0 list list`_1922| _x_1913)
                                                                                                                                                          expansions
                                                                                                                                                          • unroll
                                                                                                                                                            expr
                                                                                                                                                            (let ((a!1 (|get.::.1_1899| (|get.::.1_1899| (|get.::.1_1899| (|get.::.1_1899| _x_1913))))))
                                                                                                                                                              (|cou…
                                                                                                                                                            expansions
                                                                                                                                                            • unroll
                                                                                                                                                              expr
                                                                                                                                                              (let ((a!1 (|count_`ty_0 list list`_1922|
                                                                                                                                                                           (|get.::.1_1899| (|get.::.1_1899| (|get.::.1_…
                                                                                                                                                              expansions
                                                                                                                                                              • unroll
                                                                                                                                                                expr
                                                                                                                                                                (let ((a!1 (|get.::.0_1898| (|get.::.1_1899| (|get.::.1_1899| (|get.::.1_1899| _x_1913))))))
                                                                                                                                                                  (|cou…
                                                                                                                                                                expansions
                                                                                                                                                                • unroll
                                                                                                                                                                  expr
                                                                                                                                                                  (|count_`ty_0 list list`_1922| (|get.::.1_1899| _x_1913))
                                                                                                                                                                  expansions
                                                                                                                                                                  • unroll
                                                                                                                                                                    expr
                                                                                                                                                                    (|count_`ty_0 list`_1924| (|get.::.0_1898| _x_1913))
                                                                                                                                                                    expansions
                                                                                                                                                                    • unroll
                                                                                                                                                                      expr
                                                                                                                                                                      (let ((a!1 (|get.::.1_1899| (|get.::.1_1899| (|get.::.1_1899| (|get.::.1_1899| _x_1913))))))
                                                                                                                                                                        (|cou…
                                                                                                                                                                      expansions
                                                                                                                                                                      • unroll
                                                                                                                                                                        expr
                                                                                                                                                                        (let ((a!1 (|count_`ty_0 list list`_1922|
                                                                                                                                                                                     (|get.::.1_1899| (|get.::.1_1899| (|get.::.1_…
                                                                                                                                                                        expansions
                                                                                                                                                                        • unroll
                                                                                                                                                                          expr
                                                                                                                                                                          (let ((a!1 (|get.::.1_1899| (|get.::.1_1899| (|get.::.1_1899| (|get.::.1_1899| _x_1913))))))
                                                                                                                                                                            (|cou…
                                                                                                                                                                          expansions
                                                                                                                                                                          • unroll
                                                                                                                                                                            expr
                                                                                                                                                                            (|count_`ty_0 list list`_1922| (|get.::.1_1899| (|get.::.1_1899| _x_1913)))
                                                                                                                                                                            expansions
                                                                                                                                                                            • unsat
                                                                                                                                                                              (let ((a!1 (ite (>= (|count_`ty_0 list`_1924| (|get.::.0_1898| _x_1913)) 0)
                                                                                                                                                                                              (|count_…

                                                                                                                                                                            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 -> Imandra_surface.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 -> Imandra_surface.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.097s
                                                                                                                                                                            details
                                                                                                                                                                            Expand
                                                                                                                                                                            smt_stats
                                                                                                                                                                            num checks7
                                                                                                                                                                            arith assert lower5
                                                                                                                                                                            arith pivots3
                                                                                                                                                                            rlimit count2041
                                                                                                                                                                            mk clause3
                                                                                                                                                                            datatype occurs check30
                                                                                                                                                                            mk bool var68
                                                                                                                                                                            arith assert upper5
                                                                                                                                                                            datatype splits6
                                                                                                                                                                            decisions14
                                                                                                                                                                            arith add rows7
                                                                                                                                                                            propagations1
                                                                                                                                                                            conflicts10
                                                                                                                                                                            arith fixed eqs4
                                                                                                                                                                            datatype accessor ax8
                                                                                                                                                                            arith conflicts1
                                                                                                                                                                            datatype constructor ax16
                                                                                                                                                                            num allocs2000615050
                                                                                                                                                                            final checks6
                                                                                                                                                                            added eqs54
                                                                                                                                                                            del clause1
                                                                                                                                                                            arith eq adapter3
                                                                                                                                                                            memory26.890000
                                                                                                                                                                            max memory34.890000
                                                                                                                                                                            Expand
                                                                                                                                                                            • start[0.097s]
                                                                                                                                                                                not (l1 = [] || l2 = [])
                                                                                                                                                                                && Ordinal.count l1 >= 0 && Ordinal.count (List.tl l1) >= 0
                                                                                                                                                                                ==> (List.tl l1 = [] || List.tl l2 = [])
                                                                                                                                                                                    || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl l1)))
                                                                                                                                                                                       (Ordinal.Int (Ordinal.count l1))
                                                                                                                                                                            • simplify
                                                                                                                                                                              into
                                                                                                                                                                              ((not
                                                                                                                                                                                ((not (l1 = [] || l2 = []) && Ordinal.count l1 >= 0)
                                                                                                                                                                                 && Ordinal.count (List.tl l1) >= 0)
                                                                                                                                                                                || List.tl l1 = [])
                                                                                                                                                                               || List.tl l2 = [])
                                                                                                                                                                              || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl l1)))
                                                                                                                                                                                 (Ordinal.Int (Ordinal.count l1))
                                                                                                                                                                              expansions
                                                                                                                                                                              []
                                                                                                                                                                              rewrite_steps
                                                                                                                                                                                forward_chaining
                                                                                                                                                                                • unroll
                                                                                                                                                                                  expr
                                                                                                                                                                                  (|Ordinal.<<_116| (|Ordinal.Int_107|
                                                                                                                                                                                                      (|count_`ty_0 list`_2235| (|get.::.1_2206| …
                                                                                                                                                                                  expansions
                                                                                                                                                                                  • unroll
                                                                                                                                                                                    expr
                                                                                                                                                                                    (|count_`ty_0 list`_2235| (|get.::.1_2206| l1_2224))
                                                                                                                                                                                    expansions
                                                                                                                                                                                    • unroll
                                                                                                                                                                                      expr
                                                                                                                                                                                      (|count_`ty_0 list`_2235| l1_2224)
                                                                                                                                                                                      expansions
                                                                                                                                                                                      • unsat
                                                                                                                                                                                        (let ((a!1 (= (|count_`ty_0 list`_2235| l1_2224)
                                                                                                                                                                                                      (+ 1 (|count_`ty_0 list`_2235| (|get.…

                                                                                                                                                                                      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[(List.hd y).0 = None || (List.hd y).1 = None && not (y = [])]
                                                                                                                                                                                      proof
                                                                                                                                                                                      detailed proof
                                                                                                                                                                                      ground_instances3
                                                                                                                                                                                      definitions0
                                                                                                                                                                                      inductions0
                                                                                                                                                                                      search_time
                                                                                                                                                                                      0.068s
                                                                                                                                                                                      details
                                                                                                                                                                                      Expand
                                                                                                                                                                                      smt_stats
                                                                                                                                                                                      num checks7
                                                                                                                                                                                      arith assert lower6
                                                                                                                                                                                      arith pivots5
                                                                                                                                                                                      rlimit count5705
                                                                                                                                                                                      mk clause28
                                                                                                                                                                                      datatype occurs check66
                                                                                                                                                                                      mk bool var164
                                                                                                                                                                                      arith assert upper4
                                                                                                                                                                                      datatype splits42
                                                                                                                                                                                      decisions34
                                                                                                                                                                                      arith add rows6
                                                                                                                                                                                      propagations51
                                                                                                                                                                                      conflicts12
                                                                                                                                                                                      arith fixed eqs3
                                                                                                                                                                                      datatype accessor ax27
                                                                                                                                                                                      arith conflicts1
                                                                                                                                                                                      datatype constructor ax35
                                                                                                                                                                                      num allocs2168590784
                                                                                                                                                                                      final checks14
                                                                                                                                                                                      added eqs150
                                                                                                                                                                                      del clause2
                                                                                                                                                                                      arith eq adapter3
                                                                                                                                                                                      memory27.380000
                                                                                                                                                                                      max memory34.890000
                                                                                                                                                                                      Expand
                                                                                                                                                                                      • start[0.068s]
                                                                                                                                                                                          ((List.hd y).0 = None || (List.hd y).1 = None)
                                                                                                                                                                                          && not (y = []) && Ordinal.count y >= 0 && Ordinal.count (List.tl y) >= 0
                                                                                                                                                                                          ==> not
                                                                                                                                                                                              (((List.hd (List.tl y)).0 = None || (List.hd (List.tl y)).1 = None)
                                                                                                                                                                                               && not (List.tl y = []))
                                                                                                                                                                                              && not
                                                                                                                                                                                                 (Option.get (List.hd (List.tl y)).0 =
                                                                                                                                                                                                  Option.get (List.hd (List.tl y)).1
                                                                                                                                                                                                  && not
                                                                                                                                                                                                     ((List.hd (List.tl y)).0 = None
                                                                                                                                                                                                      || (List.hd (List.tl y)).1 = None)
                                                                                                                                                                                                     && not (List.tl y = []))
                                                                                                                                                                                              || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl y)))
                                                                                                                                                                                                 (Ordinal.Int (Ordinal.count y))
                                                                                                                                                                                      • simplify
                                                                                                                                                                                        into
                                                                                                                                                                                        (not
                                                                                                                                                                                         (((((List.hd y).0 = None || (List.hd y).1 = None) && not (y = []))
                                                                                                                                                                                           && Ordinal.count y >= 0)
                                                                                                                                                                                          && Ordinal.count (List.tl y) >= 0)
                                                                                                                                                                                         || not
                                                                                                                                                                                            (((List.hd (List.tl y)).0 = None || (List.hd (List.tl y)).1 = None)
                                                                                                                                                                                             && not (List.tl y = []))
                                                                                                                                                                                            && not
                                                                                                                                                                                               ((Option.get (List.hd (List.tl y)).0 =
                                                                                                                                                                                                 Option.get (List.hd (List.tl y)).1
                                                                                                                                                                                                 && not
                                                                                                                                                                                                    ((List.hd (List.tl y)).0 = None || (List.hd (List.tl y)).1 = None))
                                                                                                                                                                                                && not (List.tl y = [])))
                                                                                                                                                                                        || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl y)))
                                                                                                                                                                                           (Ordinal.Int (Ordinal.count y))
                                                                                                                                                                                        expansions
                                                                                                                                                                                        []
                                                                                                                                                                                        rewrite_steps
                                                                                                                                                                                          forward_chaining
                                                                                                                                                                                          • unroll
                                                                                                                                                                                            expr
                                                                                                                                                                                            (|Ordinal.<<_116| (|Ordinal.Int_107|
                                                                                                                                                                                                                (|count_`(ty_0 option * ty_0 option) list`_…
                                                                                                                                                                                            expansions
                                                                                                                                                                                            • unroll
                                                                                                                                                                                              expr
                                                                                                                                                                                              (|count_`(ty_0 option * ty_0 option) list`_2266| (|get.::.1_2248| y_2255))
                                                                                                                                                                                              expansions
                                                                                                                                                                                              • unroll
                                                                                                                                                                                                expr
                                                                                                                                                                                                (|count_`(ty_0 option * ty_0 option) list`_2266| y_2255)
                                                                                                                                                                                                expansions
                                                                                                                                                                                                • unsat
                                                                                                                                                                                                  (let ((a!1 (= (|count_`(ty_0 option * ty_0 option) list`_2266| y_2255)
                                                                                                                                                                                                                (+ 4
                                                                                                                                                                                                            …

                                                                                                                                                                                                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[Option.get (List.hd y).0 = Option.get (List.hd y).1 && not ((List.hd y).0 = None || (List.hd y).1 = None) && not (y = [])]
                                                                                                                                                                                                proof
                                                                                                                                                                                                detailed proof
                                                                                                                                                                                                ground_instances3
                                                                                                                                                                                                definitions0
                                                                                                                                                                                                inductions0
                                                                                                                                                                                                search_time
                                                                                                                                                                                                0.017s
                                                                                                                                                                                                details
                                                                                                                                                                                                Expand
                                                                                                                                                                                                smt_stats
                                                                                                                                                                                                num checks7
                                                                                                                                                                                                arith assert lower5
                                                                                                                                                                                                arith pivots4
                                                                                                                                                                                                rlimit count2890
                                                                                                                                                                                                mk clause26
                                                                                                                                                                                                datatype occurs check59
                                                                                                                                                                                                mk bool var147
                                                                                                                                                                                                arith assert upper5
                                                                                                                                                                                                datatype splits26
                                                                                                                                                                                                decisions31
                                                                                                                                                                                                arith add rows7
                                                                                                                                                                                                propagations57
                                                                                                                                                                                                conflicts13
                                                                                                                                                                                                arith fixed eqs4
                                                                                                                                                                                                datatype accessor ax26
                                                                                                                                                                                                arith conflicts1
                                                                                                                                                                                                datatype constructor ax34
                                                                                                                                                                                                num allocs2051940477
                                                                                                                                                                                                final checks11
                                                                                                                                                                                                added eqs148
                                                                                                                                                                                                del clause2
                                                                                                                                                                                                arith eq adapter3
                                                                                                                                                                                                memory30.300000
                                                                                                                                                                                                max memory34.890000
                                                                                                                                                                                                Expand
                                                                                                                                                                                                • start[0.017s]
                                                                                                                                                                                                    Option.get (List.hd y).0 = Option.get (List.hd y).1
                                                                                                                                                                                                    && not ((List.hd y).0 = None || (List.hd y).1 = None)
                                                                                                                                                                                                       && not (y = [])
                                                                                                                                                                                                          && Ordinal.count y >= 0 && Ordinal.count (List.tl y) >= 0
                                                                                                                                                                                                    ==> not
                                                                                                                                                                                                        (((List.hd (List.tl y)).0 = None || (List.hd (List.tl y)).1 = None)
                                                                                                                                                                                                         && not (List.tl y = []))
                                                                                                                                                                                                        && not
                                                                                                                                                                                                           (Option.get (List.hd (List.tl y)).0 =
                                                                                                                                                                                                            Option.get (List.hd (List.tl y)).1
                                                                                                                                                                                                            && not
                                                                                                                                                                                                               ((List.hd (List.tl y)).0 = None
                                                                                                                                                                                                                || (List.hd (List.tl y)).1 = None)
                                                                                                                                                                                                               && not (List.tl y = []))
                                                                                                                                                                                                        || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl y)))
                                                                                                                                                                                                           (Ordinal.Int (Ordinal.count y))
                                                                                                                                                                                                • simplify
                                                                                                                                                                                                  into
                                                                                                                                                                                                  (not
                                                                                                                                                                                                   ((((Option.get (List.hd y).0 = Option.get (List.hd y).1
                                                                                                                                                                                                       && not ((List.hd y).0 = None || (List.hd y).1 = None))
                                                                                                                                                                                                      && not (y = []))
                                                                                                                                                                                                     && Ordinal.count y >= 0)
                                                                                                                                                                                                    && Ordinal.count (List.tl y) >= 0)
                                                                                                                                                                                                   || not
                                                                                                                                                                                                      (((List.hd (List.tl y)).0 = None || (List.hd (List.tl y)).1 = None)
                                                                                                                                                                                                       && not (List.tl y = []))
                                                                                                                                                                                                      && not
                                                                                                                                                                                                         ((Option.get (List.hd (List.tl y)).0 =
                                                                                                                                                                                                           Option.get (List.hd (List.tl y)).1
                                                                                                                                                                                                           && not
                                                                                                                                                                                                              ((List.hd (List.tl y)).0 = None || (List.hd (List.tl y)).1 = None))
                                                                                                                                                                                                          && not (List.tl y = [])))
                                                                                                                                                                                                  || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl y)))
                                                                                                                                                                                                     (Ordinal.Int (Ordinal.count y))
                                                                                                                                                                                                  expansions
                                                                                                                                                                                                  []
                                                                                                                                                                                                  rewrite_steps
                                                                                                                                                                                                    forward_chaining
                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                      expr
                                                                                                                                                                                                      (|Ordinal.<<_116| (|Ordinal.Int_107|
                                                                                                                                                                                                                          (|count_`(ty_0 option * ty_0 option) list`_…
                                                                                                                                                                                                      expansions
                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                        expr
                                                                                                                                                                                                        (|count_`(ty_0 option * ty_0 option) list`_2266| (|get.::.1_2248| y_2255))
                                                                                                                                                                                                        expansions
                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                          expr
                                                                                                                                                                                                          (|count_`(ty_0 option * ty_0 option) list`_2266| y_2255)
                                                                                                                                                                                                          expansions
                                                                                                                                                                                                          • unsat
                                                                                                                                                                                                            (let ((a!1 (= (|count_`(ty_0 option * ty_0 option) list`_2266| y_2255)
                                                                                                                                                                                                                          (+ 4
                                                                                                                                                                                                                      …

                                                                                                                                                                                                          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[match_cols (zip (List.hd x).0 (List.hd x).1) && not (x = [])]
                                                                                                                                                                                                          proof
                                                                                                                                                                                                          detailed proof
                                                                                                                                                                                                          ground_instances5
                                                                                                                                                                                                          definitions0
                                                                                                                                                                                                          inductions0
                                                                                                                                                                                                          search_time
                                                                                                                                                                                                          0.060s
                                                                                                                                                                                                          details
                                                                                                                                                                                                          Expand
                                                                                                                                                                                                          smt_stats
                                                                                                                                                                                                          arith offset eqs5
                                                                                                                                                                                                          num checks12
                                                                                                                                                                                                          arith assert lower30
                                                                                                                                                                                                          arith pivots20
                                                                                                                                                                                                          rlimit count6698
                                                                                                                                                                                                          mk clause54
                                                                                                                                                                                                          datatype occurs check72
                                                                                                                                                                                                          mk bool var239
                                                                                                                                                                                                          arith assert upper28
                                                                                                                                                                                                          datatype splits27
                                                                                                                                                                                                          decisions92
                                                                                                                                                                                                          arith add rows31
                                                                                                                                                                                                          propagations49
                                                                                                                                                                                                          conflicts17
                                                                                                                                                                                                          arith fixed eqs11
                                                                                                                                                                                                          datatype accessor ax32
                                                                                                                                                                                                          minimized lits2
                                                                                                                                                                                                          arith conflicts6
                                                                                                                                                                                                          arith assert diseq1
                                                                                                                                                                                                          datatype constructor ax55
                                                                                                                                                                                                          num allocs2259490636
                                                                                                                                                                                                          final checks11
                                                                                                                                                                                                          added eqs212
                                                                                                                                                                                                          del clause21
                                                                                                                                                                                                          arith eq adapter20
                                                                                                                                                                                                          memory28.060000
                                                                                                                                                                                                          max memory34.890000
                                                                                                                                                                                                          Expand
                                                                                                                                                                                                          • start[0.060s]
                                                                                                                                                                                                              match_cols (zip (List.hd x).0 (List.hd x).1)
                                                                                                                                                                                                              && not (x = []) && Ordinal.count x >= 0 && Ordinal.count (List.tl x) >= 0
                                                                                                                                                                                                              ==> not
                                                                                                                                                                                                                  (match_cols (zip (List.hd (List.tl x)).0 (List.hd (List.tl x)).1)
                                                                                                                                                                                                                   && not (List.tl x = []))
                                                                                                                                                                                                                  || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl x)))
                                                                                                                                                                                                                     (Ordinal.Int (Ordinal.count x))
                                                                                                                                                                                                          • simplify
                                                                                                                                                                                                            into
                                                                                                                                                                                                            (not
                                                                                                                                                                                                             (((match_cols (zip (List.hd x).0 (List.hd x).1) && not (x = []))
                                                                                                                                                                                                               && Ordinal.count x >= 0)
                                                                                                                                                                                                              && Ordinal.count (List.tl x) >= 0)
                                                                                                                                                                                                             || not
                                                                                                                                                                                                                (match_cols (zip (List.hd (List.tl x)).0 (List.hd (List.tl x)).1)
                                                                                                                                                                                                                 && not (List.tl x = [])))
                                                                                                                                                                                                            || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl x)))
                                                                                                                                                                                                               (Ordinal.Int (Ordinal.count x))
                                                                                                                                                                                                            expansions
                                                                                                                                                                                                            []
                                                                                                                                                                                                            rewrite_steps
                                                                                                                                                                                                              forward_chaining
                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                expr
                                                                                                                                                                                                                (|Ordinal.<<_116| (|Ordinal.Int_107|
                                                                                                                                                                                                                                    (|count_`(ty_0 option list * ty_0 option li…
                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                  (zip_2301 (|tuple_get.0_2284| (|get.::.0_2287| (|get.::.1_2288| x_2314)))
                                                                                                                                                                                                                            (|tuple_get.1_22…
                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                    (let ((a!1 (zip_2301 (|tuple_get.0_2284|
                                                                                                                                                                                                                                           (|get.::.0_2287| (|get.::.1_2288| x_…
                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                      (|count_`(ty_0 option list * ty_0 option list) list`_2323|
                                                                                                                                                                                                                        (|get.::.1_2288| x_2314))
                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                        (|count_`(ty_0 option list * ty_0 option list) list`_2323| x_2314)
                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                        • unsat
                                                                                                                                                                                                                          (let ((a!1 (>= (|count_`ty_0 option list`_2327|
                                                                                                                                                                                                                                           (|tuple_get.0_2284| (|get.::.0_2287…

                                                                                                                                                                                                                        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, 6.005s):
                                                                                                                                                                                                                          let s =
                                                                                                                                                                                                                            {rows =
                                                                                                                                                                                                                             [[Some C8; Some C1; Some C2; Some C7; Some C5; Some C3; Some C6;
                                                                                                                                                                                                                               Some C4; Some C9];
                                                                                                                                                                                                                              [Some C9; Some C4; Some C3; Some C6; Some C8; Some C2; Some C1;
                                                                                                                                                                                                                               Some C7; Some C5];
                                                                                                                                                                                                                              [Some C6; Some C7; Some C5; Some C4; Some C9; Some C1; Some C2;
                                                                                                                                                                                                                               Some C8; Some C3];
                                                                                                                                                                                                                              [Some C1; Some C5; Some C4; Some C2; Some C3; Some C7; Some C8;
                                                                                                                                                                                                                               Some C9; Some C6];
                                                                                                                                                                                                                              [Some C3; Some C6; Some C9; Some C8; Some C4; Some C5; Some C7;
                                                                                                                                                                                                                               Some C2; Some C1];
                                                                                                                                                                                                                              [Some C2; Some C8; Some C7; Some C1; Some C6; Some C9; Some C5;
                                                                                                                                                                                                                               Some C3; Some C4];
                                                                                                                                                                                                                              [Some C5; Some C2; Some C1; Some C9; Some C7; Some C4; Some C3;
                                                                                                                                                                                                                               Some C6; Some C8];
                                                                                                                                                                                                                              [Some C4; Some C3; Some C8; Some C5; Some C2; Some C6; Some C9;
                                                                                                                                                                                                                               Some C1; Some C7];
                                                                                                                                                                                                                              [Some C7; Some C9; Some C6; Some C3; Some C1; Some C8; Some C4;
                                                                                                                                                                                                                               Some C5; Some C2]]}
                                                                                                                                                                                                                        
                                                                                                                                                                                                                        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