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.014s
details
Expand
smt_stats
num checks7
arith assert lower5
arith pivots3
rlimit count1821
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 allocs1365196829
final checks6
added eqs33
del clause1
arith eq adapter3
memory16.080000
max memory18.750000
Expand
  • start[0.014s]
      not (_x = []) && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
      ==> List.tl _x = []
          || Ordinal.Int (Ordinal.count (List.tl _x)) Ordinal.<<
             Ordinal.Int (Ordinal.count _x)
  • simplify
    into
    (not
     ((not (_x = []) && Ordinal.count _x >= 0) && Ordinal.count (List.tl _x) >= 0)
     || List.tl _x = [])
    || Ordinal.Int (Ordinal.count (List.tl _x)) Ordinal.<<
       Ordinal.Int (Ordinal.count _x)
    expansions
    []
    rewrite_steps
      forward_chaining
      • unroll
        expr
        (|Ordinal.<<_121| (|Ordinal.Int_112|
                            (|count_`ty_0 list`_2452| (|get.::.1_2439| …
        expansions
        • unroll
          expr
          (|count_`ty_0 list`_2452| (|get.::.1_2439| _x_2443))
          expansions
          • unroll
            expr
            (|count_`ty_0 list`_2452| _x_2443)
            expansions
            • unsat
              (let ((a!1 (= (|count_`ty_0 list`_2452| _x_2443)
                            (+ 1 (|count_`ty_0 list`_2452| (|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.016s
            details
            Expand
            smt_stats
            num checks8
            arith assert lower14
            arith pivots7
            rlimit count8221
            mk clause41
            datatype occurs check32
            mk bool var127
            arith assert upper17
            datatype splits10
            decisions28
            arith add rows14
            propagations76
            conflicts12
            arith fixed eqs7
            datatype accessor ax14
            arith conflicts2
            arith assert diseq1
            datatype constructor ax22
            num allocs1477427153
            final checks9
            added eqs101
            del clause8
            arith eq adapter12
            memory16.340000
            max memory18.750000
            Expand
            • start[0.016s]
                (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.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                       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.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                 Ordinal.Int (Ordinal.count _x)
              expansions
              []
              rewrite_steps
                forward_chaining
                • unroll
                  expr
                  (|Ordinal.<<_121| (|Ordinal.Int_112|
                                      (|count_`ty_0 list list`_2484| (|get.::.1_2…
                  expansions
                  • unroll
                    expr
                    (|count_`ty_0 list list`_2484| (|get.::.1_2471| _x_2477))
                    expansions
                    • unroll
                      expr
                      (|count_`ty_0 list list`_2484| _x_2477)
                      expansions
                      • unsat
                        (let ((a!1 (+ 1
                                      (|count_`ty_0 list list`_2484| (|get.::.1_2471| _x_2477))
                                    …

                      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.017s
                      details
                      Expand
                      smt_stats
                      num checks8
                      arith assert lower11
                      arith pivots10
                      rlimit count5164
                      mk clause34
                      datatype occurs check67
                      mk bool var143
                      arith assert upper10
                      datatype splits26
                      decisions37
                      arith add rows18
                      propagations47
                      conflicts12
                      arith fixed eqs5
                      datatype accessor ax17
                      arith conflicts2
                      datatype constructor ax29
                      num allocs1407702448
                      final checks15
                      added eqs114
                      del clause6
                      arith eq adapter7
                      memory16.380000
                      max memory18.750000
                      Expand
                      • start[0.017s]
                          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.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                                 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.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                           Ordinal.Int (Ordinal.count _x)
                        expansions
                        []
                        rewrite_steps
                          forward_chaining
                          • unroll
                            expr
                            (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                (|count_`ty_0 list list`_2484| (|get.::.1_2…
                            expansions
                            • unroll
                              expr
                              (|count_`ty_0 list list`_2484| (|get.::.1_2471| _x_2477))
                              expansions
                              • unroll
                                expr
                                (|count_`ty_0 list list`_2484| _x_2477)
                                expansions
                                • unsat
                                  (let ((a!1 (ite (>= (|count_`ty_0 list`_2486| (|get.::.0_2470| _x_2477)) 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.015s
                                details
                                Expand
                                smt_stats
                                num checks8
                                arith assert lower14
                                arith pivots8
                                rlimit count14475
                                mk clause40
                                datatype occurs check32
                                mk bool var123
                                arith assert upper13
                                datatype splits10
                                decisions24
                                arith add rows17
                                propagations75
                                conflicts12
                                arith fixed eqs7
                                datatype accessor ax14
                                arith conflicts2
                                datatype constructor ax20
                                num allocs1560762191
                                final checks9
                                added eqs97
                                del clause8
                                arith eq adapter10
                                memory19.280000
                                max memory19.280000
                                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.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                                           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.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                                     Ordinal.Int (Ordinal.count _x)
                                  expansions
                                  []
                                  rewrite_steps
                                    forward_chaining
                                    • unroll
                                      expr
                                      (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                          (|count_`ty_0 list list`_2517| (|get.::.1_2…
                                      expansions
                                      • unroll
                                        expr
                                        (|count_`ty_0 list list`_2517| (|get.::.1_2504| _x_2510))
                                        expansions
                                        • unroll
                                          expr
                                          (|count_`ty_0 list list`_2517| _x_2510)
                                          expansions
                                          • unsat
                                            (let ((a!1 (= (ite (>= (|count_`ty_0 list`_2519| |[]_2|) 0)
                                                               (|count_`ty_0 list`_2…

                                          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.016s
                                          details
                                          Expand
                                          smt_stats
                                          num checks8
                                          arith assert lower12
                                          arith pivots9
                                          rlimit count11438
                                          mk clause34
                                          datatype occurs check53
                                          mk bool var134
                                          arith assert upper9
                                          datatype splits20
                                          decisions34
                                          arith add rows16
                                          propagations50
                                          conflicts12
                                          arith fixed eqs5
                                          datatype accessor ax15
                                          arith conflicts2
                                          datatype constructor ax27
                                          num allocs1518728100
                                          final checks12
                                          added eqs105
                                          del clause6
                                          arith eq adapter7
                                          memory16.440000
                                          max memory18.750000
                                          Expand
                                          • start[0.016s]
                                              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.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                                                     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.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                                               Ordinal.Int (Ordinal.count _x)
                                            expansions
                                            []
                                            rewrite_steps
                                              forward_chaining
                                              • unroll
                                                expr
                                                (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                                    (|count_`ty_0 list list`_2517| (|get.::.1_2…
                                                expansions
                                                • unroll
                                                  expr
                                                  (|count_`ty_0 list list`_2517| (|get.::.1_2504| _x_2510))
                                                  expansions
                                                  • unroll
                                                    expr
                                                    (|count_`ty_0 list list`_2517| _x_2510)
                                                    expansions
                                                    • unsat
                                                      (let ((a!1 (ite (>= (|count_`ty_0 list`_2519| (|get.::.0_2503| _x_2510)) 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.016s
                                                    details
                                                    Expand
                                                    smt_stats
                                                    num checks7
                                                    arith assert lower5
                                                    arith pivots2
                                                    rlimit count16460
                                                    mk clause4
                                                    datatype occurs check39
                                                    mk bool var56
                                                    arith assert upper3
                                                    datatype splits6
                                                    decisions10
                                                    arith add rows2
                                                    propagations3
                                                    conflicts7
                                                    arith fixed eqs1
                                                    datatype accessor ax7
                                                    arith conflicts1
                                                    datatype constructor ax13
                                                    num allocs1670699342
                                                    final checks8
                                                    added eqs39
                                                    del clause4
                                                    arith eq adapter2
                                                    memory16.470000
                                                    max memory19.380000
                                                    Expand
                                                    • start[0.016s]
                                                        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.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.<<
                                                               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.Int
                                                         (if List.length (List.tl (List.hd l)) >= 0
                                                          then List.length (List.tl (List.hd l)) else 0)
                                                         Ordinal.<<
                                                         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_2594| (|get.::.1_2568| (|get.::.0_2570| l_2587)))
                                                                         0))
                                                            …
                                                          expansions
                                                          • unroll
                                                            expr
                                                            (|List.length_2594| (|get.::.1_2568| (|get.::.0_2570| l_2587)))
                                                            expansions
                                                            • unroll
                                                              expr
                                                              (|List.length_2594| (|get.::.0_2570| l_2587))
                                                              expansions
                                                              • unsat
                                                                (let ((a!1 (+ 1 (|List.length_2594| (|get.::.1_2568| (|get.::.0_2570| l_2587)))))
                                                                      (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.016s
                                                              details
                                                              Expand
                                                              smt_stats
                                                              num checks7
                                                              arith assert lower6
                                                              arith pivots3
                                                              rlimit count18483
                                                              mk clause3
                                                              datatype occurs check30
                                                              mk bool var64
                                                              arith assert upper4
                                                              datatype splits6
                                                              decisions13
                                                              arith add rows7
                                                              propagations1
                                                              conflicts9
                                                              arith fixed eqs4
                                                              datatype accessor ax8
                                                              arith conflicts1
                                                              datatype constructor ax15
                                                              num allocs1715162591
                                                              final checks6
                                                              added eqs49
                                                              del clause1
                                                              arith eq adapter3
                                                              memory16.530000
                                                              max memory19.380000
                                                              Expand
                                                              • start[0.016s]
                                                                  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.Int (Ordinal.count (Destruct(S, 0, x))) Ordinal.<<
                                                                         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.Int (Ordinal.count (Destruct(S, 0, x))) Ordinal.<<
                                                                   Ordinal.Int (Ordinal.count x)
                                                                expansions
                                                                []
                                                                rewrite_steps
                                                                  forward_chaining
                                                                  • unroll
                                                                    expr
                                                                    (|Ordinal.<<_121| (|Ordinal.Int_112| (count_nat_2628 (|get.S.0_2429| x_2621)))
                                                                                      (|O…
                                                                    expansions
                                                                    • unroll
                                                                      expr
                                                                      (count_nat_2628 (|get.S.0_2429| x_2621))
                                                                      expansions
                                                                      • unroll
                                                                        expr
                                                                        (count_nat_2628 x_2621)
                                                                        expansions
                                                                        • unsat
                                                                          (let ((a!1 (= (+ 1 (count_nat_2628 (|get.S.0_2429| x_2621)))
                                                                                        (count_nat_2628 x_2621)))…

                                                                        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.015s
                                                                        details
                                                                        Expand
                                                                        smt_stats
                                                                        num checks7
                                                                        arith assert lower5
                                                                        arith pivots3
                                                                        rlimit count20506
                                                                        mk clause3
                                                                        datatype occurs check31
                                                                        mk bool var64
                                                                        arith assert upper5
                                                                        datatype splits6
                                                                        decisions13
                                                                        arith add rows7
                                                                        propagations1
                                                                        conflicts9
                                                                        arith fixed eqs4
                                                                        datatype accessor ax8
                                                                        arith conflicts1
                                                                        datatype constructor ax15
                                                                        num allocs1760494117
                                                                        final checks6
                                                                        added eqs49
                                                                        del clause1
                                                                        arith eq adapter3
                                                                        memory19.360000
                                                                        max memory19.380000
                                                                        Expand
                                                                        • start[0.015s]
                                                                            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.Int (Ordinal.count (Destruct(S, 0, x))) Ordinal.<<
                                                                                   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.Int (Ordinal.count (Destruct(S, 0, x))) Ordinal.<<
                                                                             Ordinal.Int (Ordinal.count x)
                                                                          expansions
                                                                          []
                                                                          rewrite_steps
                                                                            forward_chaining
                                                                            • unroll
                                                                              expr
                                                                              (|Ordinal.<<_121| (|Ordinal.Int_112| (count_nat_2655 (|get.S.0_2429| x_2648)))
                                                                                                (|O…
                                                                              expansions
                                                                              • unroll
                                                                                expr
                                                                                (count_nat_2655 (|get.S.0_2429| x_2648))
                                                                                expansions
                                                                                • unroll
                                                                                  expr
                                                                                  (count_nat_2655 x_2648)
                                                                                  expansions
                                                                                  • unsat
                                                                                    (let ((a!1 (= (count_nat_2655 x_2648)
                                                                                                  (+ 1 (count_nat_2655 (|get.S.0_2429| x_2648)))))…

                                                                                  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.015s
                                                                                  details
                                                                                  Expand
                                                                                  smt_stats
                                                                                  num checks7
                                                                                  arith assert lower6
                                                                                  arith pivots3
                                                                                  rlimit count22422
                                                                                  mk clause3
                                                                                  datatype occurs check18
                                                                                  mk bool var50
                                                                                  arith assert upper4
                                                                                  datatype splits3
                                                                                  decisions6
                                                                                  arith add rows7
                                                                                  propagations2
                                                                                  conflicts6
                                                                                  arith fixed eqs4
                                                                                  datatype accessor ax5
                                                                                  arith conflicts1
                                                                                  datatype constructor ax7
                                                                                  num allocs1875315218
                                                                                  final checks5
                                                                                  added eqs30
                                                                                  del clause1
                                                                                  arith eq adapter3
                                                                                  memory16.590000
                                                                                  max memory19.380000
                                                                                  Expand
                                                                                  • start[0.015s]
                                                                                      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.Int (Ordinal.count (List.tl y)) Ordinal.<<
                                                                                             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.Int (Ordinal.count (List.tl y)) Ordinal.<<
                                                                                       Ordinal.Int (Ordinal.count y)
                                                                                    expansions
                                                                                    []
                                                                                    rewrite_steps
                                                                                      forward_chaining
                                                                                      • unroll
                                                                                        expr
                                                                                        (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                                                                            (|count_`ty_0 list`_2682| (|get.::.1_2669| …
                                                                                        expansions
                                                                                        • unroll
                                                                                          expr
                                                                                          (|count_`ty_0 list`_2682| (|get.::.1_2669| y_2676))
                                                                                          expansions
                                                                                          • unroll
                                                                                            expr
                                                                                            (|count_`ty_0 list`_2682| y_2676)
                                                                                            expansions
                                                                                            • unsat
                                                                                              (let ((a!1 (= (+ 1 (|count_`ty_0 list`_2682| (|get.::.1_2669| y_2676)))
                                                                                                            (|count_`ty_0 …

                                                                                            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.017s
                                                                                            details
                                                                                            Expand
                                                                                            smt_stats
                                                                                            num checks9
                                                                                            arith assert lower6
                                                                                            arith pivots4
                                                                                            rlimit count24807
                                                                                            mk clause8
                                                                                            datatype occurs check21
                                                                                            mk bool var62
                                                                                            arith assert upper4
                                                                                            datatype splits3
                                                                                            decisions17
                                                                                            arith add rows5
                                                                                            propagations5
                                                                                            conflicts9
                                                                                            arith fixed eqs3
                                                                                            datatype accessor ax5
                                                                                            arith conflicts1
                                                                                            datatype constructor ax8
                                                                                            num allocs1922395319
                                                                                            final checks6
                                                                                            added eqs37
                                                                                            del clause1
                                                                                            arith eq adapter3
                                                                                            memory16.590000
                                                                                            max memory19.380000
                                                                                            Expand
                                                                                            • start[0.017s]
                                                                                                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.Int (Ordinal.count (List.tl x)) Ordinal.<<
                                                                                                       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.Int (Ordinal.count (List.tl x)) Ordinal.<<
                                                                                                 Ordinal.Int (Ordinal.count x)
                                                                                              expansions
                                                                                              []
                                                                                              rewrite_steps
                                                                                                forward_chaining
                                                                                                • unroll
                                                                                                  expr
                                                                                                  (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                                                                                      (|count_`ty_0 list`_2709| (|get.::.1_2694| …
                                                                                                  expansions
                                                                                                  • unroll
                                                                                                    expr
                                                                                                    (elem_2699 (|get.::.0_2693| (|get.::.1_2694| x_2704))
                                                                                                               (|get.::.1_2694| (|get.::.1_2694| x…
                                                                                                    expansions
                                                                                                    • unroll
                                                                                                      expr
                                                                                                      (|count_`ty_0 list`_2709| (|get.::.1_2694| x_2704))
                                                                                                      expansions
                                                                                                      • unroll
                                                                                                        expr
                                                                                                        (|count_`ty_0 list`_2709| x_2704)
                                                                                                        expansions
                                                                                                        • unsat
                                                                                                          (let ((a!1 (= (+ 1 (|count_`ty_0 list`_2709| (|get.::.1_2694| x_2704)))
                                                                                                                        (|count_`ty_0 …

                                                                                                        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
                                                                                                        definitions2
                                                                                                        inductions0
                                                                                                        search_time
                                                                                                        0.019s
                                                                                                        details
                                                                                                        Expand
                                                                                                        smt_stats
                                                                                                        num checks7
                                                                                                        arith assert lower5
                                                                                                        arith pivots3
                                                                                                        rlimit count26743
                                                                                                        mk clause3
                                                                                                        datatype occurs check29
                                                                                                        mk bool var60
                                                                                                        arith assert upper5
                                                                                                        datatype splits9
                                                                                                        decisions13
                                                                                                        arith add rows7
                                                                                                        propagations2
                                                                                                        conflicts6
                                                                                                        arith fixed eqs4
                                                                                                        datatype accessor ax8
                                                                                                        arith conflicts1
                                                                                                        datatype constructor ax13
                                                                                                        num allocs2007978163
                                                                                                        final checks8
                                                                                                        added eqs42
                                                                                                        del clause1
                                                                                                        arith eq adapter3
                                                                                                        memory16.680000
                                                                                                        max memory19.440000
                                                                                                        Expand
                                                                                                        • start[0.019s]
                                                                                                            not (l = []) && Ordinal.count l >= 0 && Ordinal.count (List.tl l) >= 0
                                                                                                            ==> List.tl l = []
                                                                                                                || Ordinal.Int (Ordinal.count (List.tl l)) Ordinal.<<
                                                                                                                   Ordinal.Int (Ordinal.count l)
                                                                                                        • simplify
                                                                                                          into
                                                                                                          (not
                                                                                                           ((not (l = []) && Ordinal.count l >= 0) && Ordinal.count (List.tl l) >= 0)
                                                                                                           || List.tl l = [])
                                                                                                          || Ordinal.Int (Ordinal.count (List.tl l)) Ordinal.<<
                                                                                                             Ordinal.Int (Ordinal.count l)
                                                                                                          expansions
                                                                                                          []
                                                                                                          rewrite_steps
                                                                                                            forward_chaining
                                                                                                            • unroll
                                                                                                              expr
                                                                                                              (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                                                                                                  (|count_`ty_0 option list`_2741| (|get.::.1…
                                                                                                              expansions
                                                                                                              • unroll
                                                                                                                expr
                                                                                                                (|count_`ty_0 option list`_2741| (|get.::.1_2726| l_2736))
                                                                                                                expansions
                                                                                                                Ordinal.count
                                                                                                              • unroll
                                                                                                                expr
                                                                                                                (|count_`ty_0 option list`_2741| l_2736)
                                                                                                                expansions
                                                                                                                Ordinal.count
                                                                                                              • unsat
                                                                                                                (let ((a!1 (= (|count_`ty_0 option list`_2741| l_2736)
                                                                                                                              (+ 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.016s
                                                                                                              details
                                                                                                              Expand
                                                                                                              smt_stats
                                                                                                              num checks8
                                                                                                              arith assert lower15
                                                                                                              arith pivots8
                                                                                                              rlimit count29325
                                                                                                              mk clause12
                                                                                                              datatype occurs check37
                                                                                                              mk bool var86
                                                                                                              arith assert upper12
                                                                                                              datatype splits9
                                                                                                              decisions23
                                                                                                              arith add rows12
                                                                                                              propagations10
                                                                                                              conflicts10
                                                                                                              arith fixed eqs7
                                                                                                              datatype accessor ax9
                                                                                                              arith conflicts2
                                                                                                              arith assert diseq1
                                                                                                              datatype constructor ax15
                                                                                                              num allocs2055498086
                                                                                                              final checks8
                                                                                                              added eqs56
                                                                                                              del clause5
                                                                                                              arith eq adapter10
                                                                                                              memory19.460000
                                                                                                              max memory19.460000
                                                                                                              Expand
                                                                                                              • start[0.016s]
                                                                                                                  not (_x = []) && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                                                                                                                  ==> List.tl _x = []
                                                                                                                      || Ordinal.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                                                                                                                         Ordinal.Int (Ordinal.count _x)
                                                                                                              • simplify
                                                                                                                into
                                                                                                                (not
                                                                                                                 ((not (_x = []) && Ordinal.count _x >= 0) && Ordinal.count (List.tl _x) >= 0)
                                                                                                                 || List.tl _x = [])
                                                                                                                || Ordinal.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                                                                                                                   Ordinal.Int (Ordinal.count _x)
                                                                                                                expansions
                                                                                                                []
                                                                                                                rewrite_steps
                                                                                                                  forward_chaining
                                                                                                                  • unroll
                                                                                                                    expr
                                                                                                                    (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                                                                                                        (|count_`ty_0 list list`_2803| (|get.::.1_2…
                                                                                                                    expansions
                                                                                                                    • unroll
                                                                                                                      expr
                                                                                                                      (|count_`ty_0 list list`_2803| (|get.::.1_2788| _x_2798))
                                                                                                                      expansions
                                                                                                                      • unroll
                                                                                                                        expr
                                                                                                                        (|count_`ty_0 list list`_2803| _x_2798)
                                                                                                                        expansions
                                                                                                                        • unsat
                                                                                                                          (let ((a!1 (ite (>= (|count_`ty_0 list`_2805| (|get.::.0_2787| _x_2798)) 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.018s
                                                                                                                        details
                                                                                                                        Expand
                                                                                                                        smt_stats
                                                                                                                        num checks8
                                                                                                                        arith assert lower16
                                                                                                                        arith pivots8
                                                                                                                        rlimit count31876
                                                                                                                        mk clause12
                                                                                                                        datatype occurs check37
                                                                                                                        mk bool var83
                                                                                                                        arith assert upper11
                                                                                                                        datatype splits9
                                                                                                                        decisions21
                                                                                                                        arith add rows12
                                                                                                                        propagations10
                                                                                                                        conflicts9
                                                                                                                        arith fixed eqs7
                                                                                                                        datatype accessor ax8
                                                                                                                        arith conflicts2
                                                                                                                        arith assert diseq1
                                                                                                                        datatype constructor ax13
                                                                                                                        num allocs2142572935
                                                                                                                        final checks8
                                                                                                                        added eqs51
                                                                                                                        del clause5
                                                                                                                        arith eq adapter10
                                                                                                                        memory19.460000
                                                                                                                        max memory19.460000
                                                                                                                        Expand
                                                                                                                        • start[0.018s]
                                                                                                                            not (_x = []) && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                                                                                                                            ==> List.tl _x = []
                                                                                                                                || Ordinal.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                                                                                                                                   Ordinal.Int (Ordinal.count _x)
                                                                                                                        • simplify
                                                                                                                          into
                                                                                                                          (not
                                                                                                                           ((not (_x = []) && Ordinal.count _x >= 0) && Ordinal.count (List.tl _x) >= 0)
                                                                                                                           || List.tl _x = [])
                                                                                                                          || Ordinal.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                                                                                                                             Ordinal.Int (Ordinal.count _x)
                                                                                                                          expansions
                                                                                                                          []
                                                                                                                          rewrite_steps
                                                                                                                            forward_chaining
                                                                                                                            • unroll
                                                                                                                              expr
                                                                                                                              (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                                                                                                                  (|count_`ty_0 list list`_2841| (|get.::.1_2…
                                                                                                                              expansions
                                                                                                                              • unroll
                                                                                                                                expr
                                                                                                                                (|count_`ty_0 list list`_2841| (|get.::.1_2820| _x_2836))
                                                                                                                                expansions
                                                                                                                                • unroll
                                                                                                                                  expr
                                                                                                                                  (|count_`ty_0 list list`_2841| _x_2836)
                                                                                                                                  expansions
                                                                                                                                  • unsat
                                                                                                                                    (let ((a!1 (ite (>= (|count_`ty_0 list`_2843| (|get.::.0_2819| _x_2836)) 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.018s
                                                                                                                                  details
                                                                                                                                  Expand
                                                                                                                                  smt_stats
                                                                                                                                  num checks8
                                                                                                                                  arith assert lower16
                                                                                                                                  arith pivots8
                                                                                                                                  rlimit count34427
                                                                                                                                  mk clause12
                                                                                                                                  datatype occurs check37
                                                                                                                                  mk bool var83
                                                                                                                                  arith assert upper11
                                                                                                                                  datatype splits9
                                                                                                                                  decisions21
                                                                                                                                  arith add rows12
                                                                                                                                  propagations10
                                                                                                                                  conflicts9
                                                                                                                                  arith fixed eqs7
                                                                                                                                  datatype accessor ax8
                                                                                                                                  arith conflicts2
                                                                                                                                  arith assert diseq1
                                                                                                                                  datatype constructor ax13
                                                                                                                                  num allocs2229782233
                                                                                                                                  final checks8
                                                                                                                                  added eqs51
                                                                                                                                  del clause5
                                                                                                                                  arith eq adapter10
                                                                                                                                  memory19.480000
                                                                                                                                  max memory19.480000
                                                                                                                                  Expand
                                                                                                                                  • start[0.018s]
                                                                                                                                      not (_x = []) && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                                                                                                                                      ==> List.tl _x = []
                                                                                                                                          || Ordinal.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                                                                                                                                             Ordinal.Int (Ordinal.count _x)
                                                                                                                                  • simplify
                                                                                                                                    into
                                                                                                                                    (not
                                                                                                                                     ((not (_x = []) && Ordinal.count _x >= 0) && Ordinal.count (List.tl _x) >= 0)
                                                                                                                                     || List.tl _x = [])
                                                                                                                                    || Ordinal.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                                                                                                                                       Ordinal.Int (Ordinal.count _x)
                                                                                                                                    expansions
                                                                                                                                    []
                                                                                                                                    rewrite_steps
                                                                                                                                      forward_chaining
                                                                                                                                      • unroll
                                                                                                                                        expr
                                                                                                                                        (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                                                                                                                            (|count_`ty_0 list list`_2874| (|get.::.1_2…
                                                                                                                                        expansions
                                                                                                                                        • unroll
                                                                                                                                          expr
                                                                                                                                          (|count_`ty_0 list list`_2874| (|get.::.1_2858| _x_2869))
                                                                                                                                          expansions
                                                                                                                                          • unroll
                                                                                                                                            expr
                                                                                                                                            (|count_`ty_0 list list`_2874| _x_2869)
                                                                                                                                            expansions
                                                                                                                                            • unsat
                                                                                                                                              (let ((a!1 (ite (>= (|count_`ty_0 list`_2876| (|get.::.0_2857| _x_2869)) 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.053s
                                                                                                                                            details
                                                                                                                                            Expand
                                                                                                                                            smt_stats
                                                                                                                                            arith offset eqs5
                                                                                                                                            num checks26
                                                                                                                                            arith assert lower473
                                                                                                                                            arith pivots139
                                                                                                                                            rlimit count83898
                                                                                                                                            mk clause477
                                                                                                                                            datatype occurs check262
                                                                                                                                            mk bool var1427
                                                                                                                                            arith assert upper522
                                                                                                                                            datatype splits163
                                                                                                                                            decisions1295
                                                                                                                                            arith add rows656
                                                                                                                                            arith bound prop40
                                                                                                                                            propagations1228
                                                                                                                                            interface eqs5
                                                                                                                                            conflicts90
                                                                                                                                            arith fixed eqs198
                                                                                                                                            datatype accessor ax158
                                                                                                                                            minimized lits19
                                                                                                                                            arith conflicts20
                                                                                                                                            arith assert diseq149
                                                                                                                                            datatype constructor ax365
                                                                                                                                            num allocs2291912797
                                                                                                                                            final checks49
                                                                                                                                            added eqs1630
                                                                                                                                            del clause279
                                                                                                                                            arith eq adapter318
                                                                                                                                            memory20.270000
                                                                                                                                            max memory20.270000
                                                                                                                                            Expand
                                                                                                                                            • start[0.053s]
                                                                                                                                                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.Int (Ordinal.count (List.tl (List.tl (List.tl _x))))
                                                                                                                                                       Ordinal.<< 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.Int (Ordinal.count (List.tl (List.tl (List.tl _x)))) Ordinal.<<
                                                                                                                                                 Ordinal.Int (Ordinal.count _x)
                                                                                                                                              expansions
                                                                                                                                              []
                                                                                                                                              rewrite_steps
                                                                                                                                                forward_chaining
                                                                                                                                                • unroll
                                                                                                                                                  expr
                                                                                                                                                  (let ((a!1 (|count_`ty_0 list list`_2914|
                                                                                                                                                               (|get.::.1_2895| (|get.::.1_2895| (|get.::.1_…
                                                                                                                                                  expansions
                                                                                                                                                  • unroll
                                                                                                                                                    expr
                                                                                                                                                    (|count_`ty_0 list list`_2914|
                                                                                                                                                      (|get.::.1_2895| (|get.::.1_2895| (|get.::.1_2895| _x_2909))))
                                                                                                                                                    expansions
                                                                                                                                                    • unroll
                                                                                                                                                      expr
                                                                                                                                                      (|count_`ty_0 list list`_2914| _x_2909)
                                                                                                                                                      expansions
                                                                                                                                                      • unroll
                                                                                                                                                        expr
                                                                                                                                                        (let ((a!1 (|get.::.1_2895| (|get.::.1_2895| (|get.::.1_2895| (|get.::.1_2895| _x_2909))))))
                                                                                                                                                          (|cou…
                                                                                                                                                        expansions
                                                                                                                                                        • unroll
                                                                                                                                                          expr
                                                                                                                                                          (let ((a!1 (|count_`ty_0 list list`_2914|
                                                                                                                                                                       (|get.::.1_2895| (|get.::.1_2895| (|get.::.1_…
                                                                                                                                                          expansions
                                                                                                                                                          • unroll
                                                                                                                                                            expr
                                                                                                                                                            (let ((a!1 (|get.::.0_2894| (|get.::.1_2895| (|get.::.1_2895| (|get.::.1_2895| _x_2909))))))
                                                                                                                                                              (|cou…
                                                                                                                                                            expansions
                                                                                                                                                            • unroll
                                                                                                                                                              expr
                                                                                                                                                              (|count_`ty_0 list list`_2914| (|get.::.1_2895| _x_2909))
                                                                                                                                                              expansions
                                                                                                                                                              • unroll
                                                                                                                                                                expr
                                                                                                                                                                (|count_`ty_0 list`_2916| (|get.::.0_2894| _x_2909))
                                                                                                                                                                expansions
                                                                                                                                                                • unroll
                                                                                                                                                                  expr
                                                                                                                                                                  (let ((a!1 (|get.::.1_2895| (|get.::.1_2895| (|get.::.1_2895| (|get.::.1_2895| _x_2909))))))
                                                                                                                                                                    (|cou…
                                                                                                                                                                  expansions
                                                                                                                                                                  • unroll
                                                                                                                                                                    expr
                                                                                                                                                                    (let ((a!1 (|count_`ty_0 list list`_2914|
                                                                                                                                                                                 (|get.::.1_2895| (|get.::.1_2895| (|get.::.1_…
                                                                                                                                                                    expansions
                                                                                                                                                                    • unroll
                                                                                                                                                                      expr
                                                                                                                                                                      (let ((a!1 (|get.::.1_2895| (|get.::.1_2895| (|get.::.1_2895| (|get.::.1_2895| _x_2909))))))
                                                                                                                                                                        (|cou…
                                                                                                                                                                      expansions
                                                                                                                                                                      • unroll
                                                                                                                                                                        expr
                                                                                                                                                                        (|count_`ty_0 list list`_2914| (|get.::.1_2895| (|get.::.1_2895| _x_2909)))
                                                                                                                                                                        expansions
                                                                                                                                                                        • unsat
                                                                                                                                                                          (let ((a!1 (ite (>= (|count_`ty_0 list`_2916| (|get.::.0_2894| _x_2909)) 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.016s
                                                                                                                                                                        details
                                                                                                                                                                        Expand
                                                                                                                                                                        smt_stats
                                                                                                                                                                        num checks7
                                                                                                                                                                        arith assert lower6
                                                                                                                                                                        arith pivots3
                                                                                                                                                                        rlimit count85955
                                                                                                                                                                        mk clause3
                                                                                                                                                                        datatype occurs check30
                                                                                                                                                                        mk bool var70
                                                                                                                                                                        arith assert upper4
                                                                                                                                                                        datatype splits6
                                                                                                                                                                        decisions15
                                                                                                                                                                        arith add rows7
                                                                                                                                                                        propagations1
                                                                                                                                                                        conflicts11
                                                                                                                                                                        arith fixed eqs4
                                                                                                                                                                        datatype accessor ax8
                                                                                                                                                                        arith conflicts1
                                                                                                                                                                        datatype constructor ax17
                                                                                                                                                                        num allocs2347835098
                                                                                                                                                                        final checks6
                                                                                                                                                                        added eqs57
                                                                                                                                                                        del clause1
                                                                                                                                                                        arith eq adapter3
                                                                                                                                                                        memory20.140000
                                                                                                                                                                        max memory20.500000
                                                                                                                                                                        Expand
                                                                                                                                                                        • start[0.016s]
                                                                                                                                                                            not (l1 = [] || l2 = [])
                                                                                                                                                                            && Ordinal.count l1 >= 0 && Ordinal.count (List.tl l1) >= 0
                                                                                                                                                                            ==> (List.tl l1 = [] || List.tl l2 = [])
                                                                                                                                                                                || Ordinal.Int (Ordinal.count (List.tl l1)) Ordinal.<<
                                                                                                                                                                                   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.Int (Ordinal.count (List.tl l1)) Ordinal.<<
                                                                                                                                                                             Ordinal.Int (Ordinal.count l1)
                                                                                                                                                                          expansions
                                                                                                                                                                          []
                                                                                                                                                                          rewrite_steps
                                                                                                                                                                            forward_chaining
                                                                                                                                                                            • unroll
                                                                                                                                                                              expr
                                                                                                                                                                              (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                                                                                                                                                                  (|count_`ty_0 list`_3151| (|get.::.1_3126| …
                                                                                                                                                                              expansions
                                                                                                                                                                              • unroll
                                                                                                                                                                                expr
                                                                                                                                                                                (|count_`ty_0 list`_3151| (|get.::.1_3126| l1_3144))
                                                                                                                                                                                expansions
                                                                                                                                                                                • unroll
                                                                                                                                                                                  expr
                                                                                                                                                                                  (|count_`ty_0 list`_3151| l1_3144)
                                                                                                                                                                                  expansions
                                                                                                                                                                                  • unsat
                                                                                                                                                                                    (let ((a!1 (= (+ 1 (|count_`ty_0 list`_3151| (|get.::.1_3126| l1_3144)))
                                                                                                                                                                                                  (|count_`ty_0…

                                                                                                                                                                                  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
                                                                                                                                                                                  definitions2
                                                                                                                                                                                  inductions0
                                                                                                                                                                                  search_time
                                                                                                                                                                                  0.016s
                                                                                                                                                                                  details
                                                                                                                                                                                  Expand
                                                                                                                                                                                  smt_stats
                                                                                                                                                                                  num checks7
                                                                                                                                                                                  arith assert lower5
                                                                                                                                                                                  arith pivots4
                                                                                                                                                                                  rlimit count91834
                                                                                                                                                                                  mk clause29
                                                                                                                                                                                  datatype occurs check69
                                                                                                                                                                                  mk bool var158
                                                                                                                                                                                  arith assert upper5
                                                                                                                                                                                  datatype splits36
                                                                                                                                                                                  decisions34
                                                                                                                                                                                  arith add rows7
                                                                                                                                                                                  propagations66
                                                                                                                                                                                  conflicts13
                                                                                                                                                                                  arith fixed eqs4
                                                                                                                                                                                  datatype accessor ax24
                                                                                                                                                                                  arith conflicts1
                                                                                                                                                                                  datatype constructor ax32
                                                                                                                                                                                  num allocs2502469415
                                                                                                                                                                                  final checks14
                                                                                                                                                                                  added eqs145
                                                                                                                                                                                  del clause2
                                                                                                                                                                                  arith eq adapter3
                                                                                                                                                                                  memory23.030000
                                                                                                                                                                                  max memory23.030000
                                                                                                                                                                                  Expand
                                                                                                                                                                                  • start[0.016s]
                                                                                                                                                                                      ((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.Int (Ordinal.count (List.tl y)) Ordinal.<<
                                                                                                                                                                                             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.Int (Ordinal.count (List.tl y)) Ordinal.<<
                                                                                                                                                                                       Ordinal.Int (Ordinal.count y)
                                                                                                                                                                                    expansions
                                                                                                                                                                                    []
                                                                                                                                                                                    rewrite_steps
                                                                                                                                                                                      forward_chaining
                                                                                                                                                                                      • unroll
                                                                                                                                                                                        expr
                                                                                                                                                                                        (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                                                                                                                                                                            (|count_`(ty_0 option * ty_0 option) list`_…
                                                                                                                                                                                        expansions
                                                                                                                                                                                        • unroll
                                                                                                                                                                                          expr
                                                                                                                                                                                          (|count_`(ty_0 option * ty_0 option) list`_3185| (|get.::.1_3171| y_3178))
                                                                                                                                                                                          expansions
                                                                                                                                                                                          Ordinal.count
                                                                                                                                                                                        • unroll
                                                                                                                                                                                          expr
                                                                                                                                                                                          (|count_`(ty_0 option * ty_0 option) list`_3185| y_3178)
                                                                                                                                                                                          expansions
                                                                                                                                                                                          Ordinal.count
                                                                                                                                                                                        • unsat
                                                                                                                                                                                          (let ((a!1 (= (+ 4
                                                                                                                                                                                                           (|count_`(ty_0 option * ty_0 option) list`_3185|
                                                                                                                                                                                                         …

                                                                                                                                                                                        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
                                                                                                                                                                                        definitions2
                                                                                                                                                                                        inductions0
                                                                                                                                                                                        search_time
                                                                                                                                                                                        0.022s
                                                                                                                                                                                        details
                                                                                                                                                                                        Expand
                                                                                                                                                                                        smt_stats
                                                                                                                                                                                        num checks7
                                                                                                                                                                                        arith assert lower5
                                                                                                                                                                                        arith pivots4
                                                                                                                                                                                        rlimit count88957
                                                                                                                                                                                        mk clause26
                                                                                                                                                                                        datatype occurs check67
                                                                                                                                                                                        mk bool var157
                                                                                                                                                                                        arith assert upper5
                                                                                                                                                                                        datatype splits31
                                                                                                                                                                                        decisions36
                                                                                                                                                                                        arith add rows7
                                                                                                                                                                                        propagations62
                                                                                                                                                                                        conflicts14
                                                                                                                                                                                        arith fixed eqs4
                                                                                                                                                                                        datatype accessor ax27
                                                                                                                                                                                        arith conflicts1
                                                                                                                                                                                        datatype constructor ax36
                                                                                                                                                                                        num allocs2446445293
                                                                                                                                                                                        final checks12
                                                                                                                                                                                        added eqs155
                                                                                                                                                                                        del clause2
                                                                                                                                                                                        arith eq adapter3
                                                                                                                                                                                        memory20.170000
                                                                                                                                                                                        max memory23.010000
                                                                                                                                                                                        Expand
                                                                                                                                                                                        • start[0.022s]
                                                                                                                                                                                            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.Int (Ordinal.count (List.tl y)) Ordinal.<<
                                                                                                                                                                                                   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.Int (Ordinal.count (List.tl y)) Ordinal.<<
                                                                                                                                                                                             Ordinal.Int (Ordinal.count y)
                                                                                                                                                                                          expansions
                                                                                                                                                                                          []
                                                                                                                                                                                          rewrite_steps
                                                                                                                                                                                            forward_chaining
                                                                                                                                                                                            • unroll
                                                                                                                                                                                              expr
                                                                                                                                                                                              (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                                                                                                                                                                                  (|count_`(ty_0 option * ty_0 option) list`_…
                                                                                                                                                                                              expansions
                                                                                                                                                                                              • unroll
                                                                                                                                                                                                expr
                                                                                                                                                                                                (|count_`(ty_0 option * ty_0 option) list`_3185| (|get.::.1_3171| y_3178))
                                                                                                                                                                                                expansions
                                                                                                                                                                                                Ordinal.count
                                                                                                                                                                                              • unroll
                                                                                                                                                                                                expr
                                                                                                                                                                                                (|count_`(ty_0 option * ty_0 option) list`_3185| y_3178)
                                                                                                                                                                                                expansions
                                                                                                                                                                                                Ordinal.count
                                                                                                                                                                                              • unsat
                                                                                                                                                                                                (let ((a!1 (= (+ 4
                                                                                                                                                                                                                 (|count_`(ty_0 option * ty_0 option) list`_3185|
                                                                                                                                                                                                               …

                                                                                                                                                                                              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
                                                                                                                                                                                              definitions2
                                                                                                                                                                                              inductions0
                                                                                                                                                                                              search_time
                                                                                                                                                                                              0.024s
                                                                                                                                                                                              details
                                                                                                                                                                                              Expand
                                                                                                                                                                                              smt_stats
                                                                                                                                                                                              arith offset eqs5
                                                                                                                                                                                              num checks12
                                                                                                                                                                                              arith assert lower31
                                                                                                                                                                                              arith pivots20
                                                                                                                                                                                              rlimit count98671
                                                                                                                                                                                              mk clause54
                                                                                                                                                                                              datatype occurs check88
                                                                                                                                                                                              mk bool var239
                                                                                                                                                                                              arith assert upper27
                                                                                                                                                                                              datatype splits27
                                                                                                                                                                                              decisions90
                                                                                                                                                                                              arith add rows40
                                                                                                                                                                                              propagations51
                                                                                                                                                                                              conflicts17
                                                                                                                                                                                              arith fixed eqs11
                                                                                                                                                                                              datatype accessor ax32
                                                                                                                                                                                              minimized lits2
                                                                                                                                                                                              arith conflicts6
                                                                                                                                                                                              arith assert diseq1
                                                                                                                                                                                              datatype constructor ax55
                                                                                                                                                                                              num allocs2603618836
                                                                                                                                                                                              final checks11
                                                                                                                                                                                              added eqs212
                                                                                                                                                                                              del clause21
                                                                                                                                                                                              arith eq adapter20
                                                                                                                                                                                              memory23.040000
                                                                                                                                                                                              max memory23.040000
                                                                                                                                                                                              Expand
                                                                                                                                                                                              • start[0.024s]
                                                                                                                                                                                                  match_cols (zip (List.hd …).0 (List.hd …).1)
                                                                                                                                                                                                  && not (… = [])
                                                                                                                                                                                                     && Ordinal.count … >= 0 && Ordinal.count (List.tl …) >= 0
                                                                                                                                                                                                  ==> not
                                                                                                                                                                                                      (match_cols (zip (List.hd (List.tl …)).0 (List.hd (List.tl …)).1)
                                                                                                                                                                                                       && not (List.tl … = []))
                                                                                                                                                                                                      || Ordinal.Int (Ordinal.count (List.tl …)) Ordinal.<<
                                                                                                                                                                                                         Ordinal.Int (Ordinal.count …)
                                                                                                                                                                                              • simplify
                                                                                                                                                                                                into
                                                                                                                                                                                                (not
                                                                                                                                                                                                 (((match_cols (zip (List.hd …).0 (List.hd …).1) && not (… = []))
                                                                                                                                                                                                   && Ordinal.count … >= 0)
                                                                                                                                                                                                  && Ordinal.count (List.tl …) >= 0)
                                                                                                                                                                                                 || not
                                                                                                                                                                                                    (match_cols (zip (List.hd (List.tl …)).0 (List.hd (List.tl …)).1)
                                                                                                                                                                                                     && not (List.tl … = [])))
                                                                                                                                                                                                || Ordinal.Int (Ordinal.count (List.tl …)) Ordinal.<<
                                                                                                                                                                                                   Ordinal.Int (Ordinal.count …)
                                                                                                                                                                                                expansions
                                                                                                                                                                                                []
                                                                                                                                                                                                rewrite_steps
                                                                                                                                                                                                  forward_chaining
                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                    expr
                                                                                                                                                                                                    (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                                                                                                                                                                                        (|count_`(ty_0 option list * ty_0 option li…
                                                                                                                                                                                                    expansions
                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                      expr
                                                                                                                                                                                                      (zip_3226 (|tuple_get.0_3209| (|get.::.0_3212| (|get.::.1_3213| x_3239)))
                                                                                                                                                                                                                (|tuple_get.1_32…
                                                                                                                                                                                                      expansions
                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                        expr
                                                                                                                                                                                                        (let ((a!1 (zip_3226 (|tuple_get.0_3209|
                                                                                                                                                                                                                               (|get.::.0_3212| (|get.::.1_3213| x_…
                                                                                                                                                                                                        expansions
                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                          expr
                                                                                                                                                                                                          (|count_`(ty_0 option list * ty_0 option list) list`_3244|
                                                                                                                                                                                                            (|get.::.1_3213| x_3239))
                                                                                                                                                                                                          expansions
                                                                                                                                                                                                          Ordinal.count
                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                          expr
                                                                                                                                                                                                          (|count_`(ty_0 option list * ty_0 option list) list`_3244| x_3239)
                                                                                                                                                                                                          expansions
                                                                                                                                                                                                          Ordinal.count
                                                                                                                                                                                                        • unsat
                                                                                                                                                                                                          (let ((a!1 (>= (|count_`ty_0 option list`_3248|
                                                                                                                                                                                                                           (|tuple_get.0_3209| (|get.::.0_3212…

                                                                                                                                                                                                        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, 2.870s):
                                                                                                                                                                                                          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