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.039s
details
Expand
smt_stats
num checks7
arith assert lower5
arith pivots3
rlimit count1817
mk clause3
datatype occurs check21
mk bool var50
arith assert upper5
datatype splits3
decisions7
arith add rows7
propagations2
conflicts7
arith fixed eqs4
datatype accessor ax5
arith conflicts1
datatype constructor ax8
num allocs933581
final checks6
added eqs33
del clause1
arith eq adapter3
memory5.900000
max memory5.900000
Expand
  • start[0.039s]
      not (_x = []) && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
      ==> List.tl _x = []
          || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x)))
             (Ordinal.Int (Ordinal.count _x))
  • simplify
    into
    (not
     ((not (_x = []) && Ordinal.count _x >= 0) && Ordinal.count (List.tl _x) >= 0)
     || List.tl _x = [])
    || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x)))
       (Ordinal.Int (Ordinal.count _x))
    expansions
    []
    rewrite_steps
      forward_chaining
      • unroll
        expr
        (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`ty_0 list`_1098|
                                              …
        expansions
        • unroll
          expr
          (|count_`ty_0 list`_1098| (|get.::.1_1084| _x_1089))
          expansions
          • unroll
            expr
            (|count_`ty_0 list`_1098| _x_1089)
            expansions
            • unsat
              (let ((a!1 (= (|count_`ty_0 list`_1098| _x_1089)
                            (+ 1 (|count_`ty_0 list`_1098| (|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[_x <> [] && List.hd _x = [] && not (_x = [])]
            proof
            detailed proof
            ground_instances3
            definitions0
            inductions0
            search_time
            0.016s
            details
            Expand
            smt_stats
            num checks8
            arith assert lower13
            arith pivots8
            rlimit count6156
            mk clause41
            datatype occurs check36
            mk bool var128
            arith assert upper14
            datatype splits11
            decisions29
            arith add rows17
            propagations80
            conflicts13
            arith fixed eqs7
            datatype accessor ax14
            arith conflicts2
            datatype constructor ax23
            num allocs5598060
            final checks10
            added eqs104
            del clause8
            arith eq adapter10
            memory12.730000
            max memory12.730000
            Expand
            • start[0.016s]
                (_x <> [] && List.hd _x = [])
                && not (_x = [])
                   && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                ==> not
                    (((List.tl _x) <> [] && List.hd (List.tl _x) = [])
                     && not (List.tl _x = []))
                    && not
                       (not ((List.tl _x) <> [] && List.hd (List.tl _x) = [])
                        && not (List.tl _x = []))
                    || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x)))
                       (Ordinal.Int (Ordinal.count _x))
            • simplify
              into
              (not
               ((((_x <> [] && List.hd _x = []) && not (_x = [])) && Ordinal.count _x >= 0)
                && Ordinal.count (List.tl _x) >= 0)
               || not
                  (((List.tl _x) <> [] && List.hd (List.tl _x) = [])
                   && not (List.tl _x = []))
                  && not
                     (not ((List.tl _x) <> [] && List.hd (List.tl _x) = [])
                      && not (List.tl _x = [])))
              || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x)))
                 (Ordinal.Int (Ordinal.count _x))
              expansions
              []
              rewrite_steps
                forward_chaining
                • unroll
                  expr
                  (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`ty_0 list list`_1128|
                                                   …
                  expansions
                  • unroll
                    expr
                    (|count_`ty_0 list list`_1128| (|get.::.1_1111| _x_1117))
                    expansions
                    • unroll
                      expr
                      (|count_`ty_0 list list`_1128| _x_1117)
                      expansions
                      • unsat
                        (let ((a!1 (= (ite (>= (|count_`ty_0 list`_1130| |[]_2|) 0)
                                           (|count_`ty_0 list`_1…

                      call `transpose3 (List.tl _x)` from `transpose3 _x`
                      originaltranspose3 _x
                      subtranspose3 (List.tl _x)
                      original ordinalOrdinal.Int (Ordinal.count _x)
                      sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
                      path[not (_x <> [] && List.hd _x = []) && not (_x = [])]
                      proof
                      detailed proof
                      ground_instances3
                      definitions0
                      inductions0
                      search_time
                      0.016s
                      details
                      Expand
                      smt_stats
                      num checks8
                      arith assert lower11
                      arith pivots9
                      rlimit count3037
                      mk clause33
                      datatype occurs check31
                      mk bool var94
                      arith assert upper12
                      datatype splits10
                      decisions32
                      arith add rows16
                      propagations55
                      conflicts12
                      arith fixed eqs5
                      datatype accessor ax7
                      arith conflicts2
                      datatype constructor ax14
                      num allocs3068774
                      final checks8
                      added eqs62
                      del clause8
                      arith eq adapter7
                      memory9.800000
                      max memory9.800000
                      Expand
                      • start[0.016s]
                          not (_x <> [] && List.hd _x = [])
                          && not (_x = [])
                             && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                          ==> not
                              (((List.tl _x) <> [] && List.hd (List.tl _x) = [])
                               && not (List.tl _x = []))
                              && not
                                 (not ((List.tl _x) <> [] && List.hd (List.tl _x) = [])
                                  && not (List.tl _x = []))
                              || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x)))
                                 (Ordinal.Int (Ordinal.count _x))
                      • simplify
                        into
                        (not
                         (((not (_x <> [] && List.hd _x = []) && not (_x = []))
                           && Ordinal.count _x >= 0)
                          && Ordinal.count (List.tl _x) >= 0)
                         || not
                            (((List.tl _x) <> [] && List.hd (List.tl _x) = [])
                             && not (List.tl _x = []))
                            && not
                               (not ((List.tl _x) <> [] && List.hd (List.tl _x) = [])
                                && not (List.tl _x = [])))
                        || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x)))
                           (Ordinal.Int (Ordinal.count _x))
                        expansions
                        []
                        rewrite_steps
                          forward_chaining
                          • unroll
                            expr
                            (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`ty_0 list list`_1128|
                                                             …
                            expansions
                            • unroll
                              expr
                              (|count_`ty_0 list list`_1128| (|get.::.1_1111| _x_1117))
                              expansions
                              • unroll
                                expr
                                (|count_`ty_0 list list`_1128| _x_1117)
                                expansions
                                • unsat
                                  (let ((a!1 (ite (>= (|count_`ty_0 list`_1130| (|get.::.0_1110| _x_1117)) 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[_x <> [] && List.hd _x = [] && not (_x = [])]
                                proof
                                detailed proof
                                ground_instances3
                                definitions0
                                inductions0
                                search_time
                                0.013s
                                details
                                Expand
                                smt_stats
                                num checks8
                                arith assert lower13
                                arith pivots8
                                rlimit count6156
                                mk clause41
                                datatype occurs check36
                                mk bool var128
                                arith assert upper14
                                datatype splits11
                                decisions29
                                arith add rows17
                                propagations80
                                conflicts13
                                arith fixed eqs7
                                datatype accessor ax14
                                arith conflicts2
                                datatype constructor ax23
                                num allocs19437344
                                final checks10
                                added eqs104
                                del clause8
                                arith eq adapter10
                                memory13.290000
                                max memory13.290000
                                Expand
                                • start[0.013s]
                                    (_x <> [] && List.hd _x = [])
                                    && not (_x = [])
                                       && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                                    ==> not
                                        (((List.tl _x) <> [] && List.hd (List.tl _x) = [])
                                         && not (List.tl _x = []))
                                        && not
                                           (not ((List.tl _x) <> [] && List.hd (List.tl _x) = [])
                                            && not (List.tl _x = []))
                                        || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x)))
                                           (Ordinal.Int (Ordinal.count _x))
                                • simplify
                                  into
                                  (not
                                   ((((_x <> [] && List.hd _x = []) && not (_x = [])) && Ordinal.count _x >= 0)
                                    && Ordinal.count (List.tl _x) >= 0)
                                   || not
                                      (((List.tl _x) <> [] && List.hd (List.tl _x) = [])
                                       && not (List.tl _x = []))
                                      && not
                                         (not ((List.tl _x) <> [] && List.hd (List.tl _x) = [])
                                          && not (List.tl _x = [])))
                                  || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x)))
                                     (Ordinal.Int (Ordinal.count _x))
                                  expansions
                                  []
                                  rewrite_steps
                                    forward_chaining
                                    • unroll
                                      expr
                                      (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`ty_0 list list`_1159|
                                                                       …
                                      expansions
                                      • unroll
                                        expr
                                        (|count_`ty_0 list list`_1159| (|get.::.1_1142| _x_1148))
                                        expansions
                                        • unroll
                                          expr
                                          (|count_`ty_0 list list`_1159| _x_1148)
                                          expansions
                                          • unsat
                                            (let ((a!1 (= (ite (>= (|count_`ty_0 list`_1161| |[]_2|) 0)
                                                               (|count_`ty_0 list`_1…

                                          call `get_heads (List.tl _x)` from `get_heads _x`
                                          originalget_heads _x
                                          subget_heads (List.tl _x)
                                          original ordinalOrdinal.Int (Ordinal.count _x)
                                          sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
                                          path[not (_x <> [] && List.hd _x = []) && not (_x = [])]
                                          proof
                                          detailed proof
                                          ground_instances3
                                          definitions0
                                          inductions0
                                          search_time
                                          0.016s
                                          details
                                          Expand
                                          smt_stats
                                          num checks8
                                          arith assert lower11
                                          arith pivots9
                                          rlimit count3037
                                          mk clause33
                                          datatype occurs check31
                                          mk bool var94
                                          arith assert upper12
                                          datatype splits10
                                          decisions32
                                          arith add rows16
                                          propagations55
                                          conflicts12
                                          arith fixed eqs5
                                          datatype accessor ax7
                                          arith conflicts2
                                          datatype constructor ax14
                                          num allocs14647704
                                          final checks8
                                          added eqs62
                                          del clause8
                                          arith eq adapter7
                                          memory10.360000
                                          max memory12.730000
                                          Expand
                                          • start[0.016s]
                                              not (_x <> [] && List.hd _x = [])
                                              && not (_x = [])
                                                 && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                                              ==> not
                                                  (((List.tl _x) <> [] && List.hd (List.tl _x) = [])
                                                   && not (List.tl _x = []))
                                                  && not
                                                     (not ((List.tl _x) <> [] && List.hd (List.tl _x) = [])
                                                      && not (List.tl _x = []))
                                                  || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x)))
                                                     (Ordinal.Int (Ordinal.count _x))
                                          • simplify
                                            into
                                            (not
                                             (((not (_x <> [] && List.hd _x = []) && not (_x = []))
                                               && Ordinal.count _x >= 0)
                                              && Ordinal.count (List.tl _x) >= 0)
                                             || not
                                                (((List.tl _x) <> [] && List.hd (List.tl _x) = [])
                                                 && not (List.tl _x = []))
                                                && not
                                                   (not ((List.tl _x) <> [] && List.hd (List.tl _x) = [])
                                                    && not (List.tl _x = [])))
                                            || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x)))
                                               (Ordinal.Int (Ordinal.count _x))
                                            expansions
                                            []
                                            rewrite_steps
                                              forward_chaining
                                              • unroll
                                                expr
                                                (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`ty_0 list list`_1159|
                                                                                 …
                                                expansions
                                                • unroll
                                                  expr
                                                  (|count_`ty_0 list list`_1159| (|get.::.1_1142| _x_1148))
                                                  expansions
                                                  • unroll
                                                    expr
                                                    (|count_`ty_0 list list`_1159| _x_1148)
                                                    expansions
                                                    • unsat
                                                      (let ((a!1 (ite (>= (|count_`ty_0 list`_1161| (|get.::.0_1141| _x_1148)) 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 (l <> [] && List.hd l = []) && not (l = [])]
                                                    proof
                                                    detailed proof
                                                    ground_instances3
                                                    definitions0
                                                    inductions0
                                                    search_time
                                                    0.013s
                                                    details
                                                    Expand
                                                    smt_stats
                                                    num checks7
                                                    arith assert lower5
                                                    arith pivots2
                                                    rlimit count2106
                                                    mk clause5
                                                    datatype occurs check46
                                                    mk bool var68
                                                    arith assert upper3
                                                    datatype splits11
                                                    decisions15
                                                    arith add rows2
                                                    propagations4
                                                    conflicts8
                                                    arith fixed eqs1
                                                    datatype accessor ax8
                                                    arith conflicts1
                                                    datatype constructor ax16
                                                    num allocs35423793
                                                    final checks11
                                                    added eqs48
                                                    del clause5
                                                    arith eq adapter2
                                                    memory11.110000
                                                    max memory13.590000
                                                    Expand
                                                    • start[0.013s]
                                                        not (l <> [] && List.hd 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 (true && List.tl (List.hd l) = [])
                                                             && not ((List.tl (List.hd l)) :: (transpose3 …) = []))
                                                            || Ordinal.( << )
                                                               (Ordinal.Int
                                                                (if (if (List.tl (List.hd l)) :: (transpose3 …) = [] then 0
                                                                     else List.length …)
                                                                    >= 0
                                                                 then
                                                                   if (List.tl (List.hd l)) :: (transpose3 …) = [] then 0
                                                                   else List.length …
                                                                 else 0))
                                                               (Ordinal.Int
                                                                (if (if l = [] then 0 else List.length (List.hd l)) >= 0
                                                                 then if l = [] then 0 else List.length (List.hd l) else 0))
                                                    • simplify
                                                      into
                                                      (not
                                                       (((not (l <> [] && List.hd l = []) && not (l = []))
                                                         && (if (if l = [] then 0 else List.length (List.hd l)) >= 0
                                                             then if l = [] then 0 else List.length (List.hd l) else 0)
                                                            >= 0)
                                                        && (if List.length (List.tl (List.hd l)) >= 0
                                                            then List.length (List.tl (List.hd l)) else 0)
                                                           >= 0)
                                                       || List.tl (List.hd l) = [])
                                                      || Ordinal.( << )
                                                         (Ordinal.Int
                                                          (if List.length (List.tl (List.hd l)) >= 0
                                                           then List.length (List.tl (List.hd l)) else 0))
                                                         (Ordinal.Int
                                                          (if (if l = [] then 0 else List.length (List.hd l)) >= 0
                                                           then if l = [] then 0 else List.length (List.hd l) else 0))
                                                      expansions
                                                      []
                                                      rewrite_steps
                                                        forward_chaining
                                                        • unroll
                                                          expr
                                                          (let ((a!1 (>= (|List.length_1228| (|get.::.1_1202| (|get.::.0_1204| l_1221)))
                                                                         0))
                                                            …
                                                          expansions
                                                          • unroll
                                                            expr
                                                            (|List.length_1228| (|get.::.1_1202| (|get.::.0_1204| l_1221)))
                                                            expansions
                                                            • unroll
                                                              expr
                                                              (|List.length_1228| (|get.::.0_1204| l_1221))
                                                              expansions
                                                              • unsat
                                                                (let ((a!1 (+ 1 (|List.length_1228| (|get.::.1_1202| (|get.::.0_1204| l_1221)))))
                                                                      (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.023s
                                                              details
                                                              Expand
                                                              smt_stats
                                                              num checks7
                                                              arith assert lower5
                                                              arith pivots3
                                                              rlimit count2043
                                                              mk clause3
                                                              datatype occurs check30
                                                              mk bool var66
                                                              arith assert upper5
                                                              datatype splits6
                                                              decisions14
                                                              arith add rows7
                                                              propagations1
                                                              conflicts10
                                                              arith fixed eqs4
                                                              datatype accessor ax8
                                                              arith conflicts1
                                                              datatype constructor ax16
                                                              num allocs48916387
                                                              final checks6
                                                              added eqs52
                                                              del clause1
                                                              arith eq adapter3
                                                              memory11.680000
                                                              max memory13.590000
                                                              Expand
                                                              • start[0.023s]
                                                                  not (l = [])
                                                                  && not (x = Z)
                                                                     && Ordinal.count x >= 0 && Ordinal.count (Destruct(S, 0, x)) >= 0
                                                                  ==> not (not (List.tl l = []) && not (Destruct(S, 0, x) = Z))
                                                                      || Ordinal.( << ) (Ordinal.Int (Ordinal.count (Destruct(S, 0, x))))
                                                                         (Ordinal.Int (Ordinal.count x))
                                                              • simplify
                                                                into
                                                                (not
                                                                 (((not (l = []) && not (x = Z)) && Ordinal.count x >= 0)
                                                                  && Ordinal.count (Destruct(S, 0, x)) >= 0)
                                                                 || not (not (List.tl l = []) && not (Destruct(S, 0, x) = Z)))
                                                                || Ordinal.( << ) (Ordinal.Int (Ordinal.count (Destruct(S, 0, x))))
                                                                   (Ordinal.Int (Ordinal.count x))
                                                                expansions
                                                                []
                                                                rewrite_steps
                                                                  forward_chaining
                                                                  • unroll
                                                                    expr
                                                                    (|Ordinal.<<_102| (|Ordinal.Int_93| (count_nat_1260 (|get.S.0_1239| x_1249)))
                                                                                      (|Or…
                                                                    expansions
                                                                    • unroll
                                                                      expr
                                                                      (count_nat_1260 (|get.S.0_1239| x_1249))
                                                                      expansions
                                                                      • unroll
                                                                        expr
                                                                        (count_nat_1260 x_1249)
                                                                        expansions
                                                                        • unsat
                                                                          (let ((a!1 (= (count_nat_1260 x_1249)
                                                                                        (+ 1 (count_nat_1260 (|get.S.0_1239| x_1249)))))…

                                                                        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.029s
                                                                        details
                                                                        Expand
                                                                        smt_stats
                                                                        num checks7
                                                                        arith assert lower5
                                                                        arith pivots3
                                                                        rlimit count2043
                                                                        mk clause3
                                                                        datatype occurs check30
                                                                        mk bool var66
                                                                        arith assert upper5
                                                                        datatype splits6
                                                                        decisions14
                                                                        arith add rows7
                                                                        propagations1
                                                                        conflicts10
                                                                        arith fixed eqs4
                                                                        datatype accessor ax8
                                                                        arith conflicts1
                                                                        datatype constructor ax16
                                                                        num allocs64405708
                                                                        final checks6
                                                                        added eqs52
                                                                        del clause1
                                                                        arith eq adapter3
                                                                        memory12.130000
                                                                        max memory14.890000
                                                                        Expand
                                                                        • start[0.029s]
                                                                            not (y = [])
                                                                            && not (x = Z)
                                                                               && Ordinal.count x >= 0 && Ordinal.count (Destruct(S, 0, x)) >= 0
                                                                            ==> not (not (List.tl y = []) && not (Destruct(S, 0, x) = Z))
                                                                                || Ordinal.( << ) (Ordinal.Int (Ordinal.count (Destruct(S, 0, x))))
                                                                                   (Ordinal.Int (Ordinal.count x))
                                                                        • simplify
                                                                          into
                                                                          (not
                                                                           (((not (y = []) && not (x = Z)) && Ordinal.count x >= 0)
                                                                            && Ordinal.count (Destruct(S, 0, x)) >= 0)
                                                                           || not (not (List.tl y = []) && not (Destruct(S, 0, x) = Z)))
                                                                          || Ordinal.( << ) (Ordinal.Int (Ordinal.count (Destruct(S, 0, x))))
                                                                             (Ordinal.Int (Ordinal.count x))
                                                                          expansions
                                                                          []
                                                                          rewrite_steps
                                                                            forward_chaining
                                                                            • unroll
                                                                              expr
                                                                              (|Ordinal.<<_102| (|Ordinal.Int_93| (count_nat_1286 (|get.S.0_1266| x_1275)))
                                                                                                (|Or…
                                                                              expansions
                                                                              • unroll
                                                                                expr
                                                                                (count_nat_1286 (|get.S.0_1266| x_1275))
                                                                                expansions
                                                                                • unroll
                                                                                  expr
                                                                                  (count_nat_1286 x_1275)
                                                                                  expansions
                                                                                  • unsat
                                                                                    (let ((a!1 (= (count_nat_1286 x_1275)
                                                                                                  (+ 1 (count_nat_1286 (|get.S.0_1266| x_1275)))))…

                                                                                  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.019s
                                                                                  details
                                                                                  Expand
                                                                                  smt_stats
                                                                                  num checks7
                                                                                  arith assert lower5
                                                                                  arith pivots3
                                                                                  rlimit count1936
                                                                                  mk clause3
                                                                                  datatype occurs check18
                                                                                  mk bool var52
                                                                                  arith assert upper5
                                                                                  datatype splits3
                                                                                  decisions7
                                                                                  arith add rows7
                                                                                  propagations2
                                                                                  conflicts7
                                                                                  arith fixed eqs4
                                                                                  datatype accessor ax5
                                                                                  arith conflicts1
                                                                                  datatype constructor ax8
                                                                                  num allocs74418555
                                                                                  final checks5
                                                                                  added eqs33
                                                                                  del clause1
                                                                                  arith eq adapter3
                                                                                  memory15.300000
                                                                                  max memory15.300000
                                                                                  Expand
                                                                                  • start[0.019s]
                                                                                      not (x = List.hd y)
                                                                                      && not (y = []) && Ordinal.count y >= 0 && Ordinal.count (List.tl y) >= 0
                                                                                      ==> not (not (x = List.hd (List.tl y)) && not (List.tl y = []))
                                                                                          || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl y)))
                                                                                             (Ordinal.Int (Ordinal.count y))
                                                                                  • simplify
                                                                                    into
                                                                                    (not
                                                                                     (((not (x = List.hd y) && not (y = [])) && Ordinal.count y >= 0)
                                                                                      && Ordinal.count (List.tl y) >= 0)
                                                                                     || not (not (x = List.hd (List.tl y)) && not (List.tl y = [])))
                                                                                    || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl y)))
                                                                                       (Ordinal.Int (Ordinal.count y))
                                                                                    expansions
                                                                                    []
                                                                                    rewrite_steps
                                                                                      forward_chaining
                                                                                      • unroll
                                                                                        expr
                                                                                        (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`ty_0 list`_1311|
                                                                                                                              …
                                                                                        expansions
                                                                                        • unroll
                                                                                          expr
                                                                                          (|count_`ty_0 list`_1311| (|get.::.1_1294| y_1301))
                                                                                          expansions
                                                                                          • unroll
                                                                                            expr
                                                                                            (|count_`ty_0 list`_1311| y_1301)
                                                                                            expansions
                                                                                            • unsat
                                                                                              (let ((a!1 (= (|count_`ty_0 list`_1311| y_1301)
                                                                                                            (+ 1 (|count_`ty_0 list`_1311| (|get.:…

                                                                                            termination proof

                                                                                            Termination proof

                                                                                            call `unique (List.tl x)` from `unique x`
                                                                                            originalunique x
                                                                                            subunique (List.tl x)
                                                                                            original ordinalOrdinal.Int (Ordinal.count x)
                                                                                            sub ordinalOrdinal.Int (Ordinal.count (List.tl x))
                                                                                            path[not (elem (List.hd x) (List.tl x)) && not (x = [])]
                                                                                            proof
                                                                                            detailed proof
                                                                                            ground_instances4
                                                                                            definitions0
                                                                                            inductions0
                                                                                            search_time
                                                                                            0.018s
                                                                                            details
                                                                                            Expand
                                                                                            smt_stats
                                                                                            num checks9
                                                                                            arith assert lower6
                                                                                            arith pivots4
                                                                                            rlimit count2357
                                                                                            mk clause8
                                                                                            datatype occurs check21
                                                                                            mk bool var58
                                                                                            arith assert upper4
                                                                                            datatype splits3
                                                                                            decisions15
                                                                                            arith add rows5
                                                                                            propagations5
                                                                                            conflicts7
                                                                                            arith fixed eqs3
                                                                                            datatype accessor ax5
                                                                                            arith conflicts1
                                                                                            datatype constructor ax6
                                                                                            num allocs93420577
                                                                                            final checks6
                                                                                            added eqs31
                                                                                            del clause1
                                                                                            arith eq adapter3
                                                                                            memory15.790000
                                                                                            max memory15.790000
                                                                                            Expand
                                                                                            • start[0.018s]
                                                                                                not (elem (List.hd x) (List.tl x))
                                                                                                && not (x = []) && Ordinal.count x >= 0 && Ordinal.count (List.tl x) >= 0
                                                                                                ==> not
                                                                                                    (not (elem (List.hd (List.tl x)) (List.tl (List.tl x)))
                                                                                                     && not (List.tl x = []))
                                                                                                    || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl x)))
                                                                                                       (Ordinal.Int (Ordinal.count x))
                                                                                            • simplify
                                                                                              into
                                                                                              (not
                                                                                               (((not (elem (List.hd x) (List.tl x)) && not (x = []))
                                                                                                 && Ordinal.count x >= 0)
                                                                                                && Ordinal.count (List.tl x) >= 0)
                                                                                               || not
                                                                                                  (not (elem (List.hd (List.tl x)) (List.tl (List.tl x)))
                                                                                                   && not (List.tl x = [])))
                                                                                              || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl x)))
                                                                                                 (Ordinal.Int (Ordinal.count x))
                                                                                              expansions
                                                                                              []
                                                                                              rewrite_steps
                                                                                                forward_chaining
                                                                                                • unroll
                                                                                                  expr
                                                                                                  (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`ty_0 list`_1337|
                                                                                                                                        …
                                                                                                  expansions
                                                                                                  • unroll
                                                                                                    expr
                                                                                                    (elem_1323 (|get.::.0_1317| (|get.::.1_1318| x_1328))
                                                                                                               (|get.::.1_1318| (|get.::.1_1318| x…
                                                                                                    expansions
                                                                                                    • unroll
                                                                                                      expr
                                                                                                      (|count_`ty_0 list`_1337| (|get.::.1_1318| x_1328))
                                                                                                      expansions
                                                                                                      • unroll
                                                                                                        expr
                                                                                                        (|count_`ty_0 list`_1337| x_1328)
                                                                                                        expansions
                                                                                                        • unsat
                                                                                                          (let ((a!1 (= (|count_`ty_0 list`_1337| x_1328)
                                                                                                                        (+ 1 (|count_`ty_0 list`_1337| (|get.:…

                                                                                                        termination proof

                                                                                                        Termination proof

                                                                                                        call `keep_some_list (List.tl l)` from `keep_some_list l`
                                                                                                        originalkeep_some_list l
                                                                                                        subkeep_some_list (List.tl l)
                                                                                                        original ordinalOrdinal.Int (Ordinal.count l)
                                                                                                        sub ordinalOrdinal.Int (Ordinal.count (List.tl l))
                                                                                                        path[not (l = [])]
                                                                                                        proof
                                                                                                        detailed proof
                                                                                                        ground_instances3
                                                                                                        definitions0
                                                                                                        inductions0
                                                                                                        search_time
                                                                                                        0.027s
                                                                                                        details
                                                                                                        Expand
                                                                                                        smt_stats
                                                                                                        num checks7
                                                                                                        arith assert lower5
                                                                                                        arith pivots3
                                                                                                        rlimit count1978
                                                                                                        mk clause3
                                                                                                        datatype occurs check29
                                                                                                        mk bool var64
                                                                                                        arith assert upper5
                                                                                                        datatype splits9
                                                                                                        decisions16
                                                                                                        arith add rows7
                                                                                                        propagations2
                                                                                                        conflicts7
                                                                                                        arith fixed eqs4
                                                                                                        datatype accessor ax10
                                                                                                        arith conflicts1
                                                                                                        datatype constructor ax16
                                                                                                        num allocs114751115
                                                                                                        final checks8
                                                                                                        added eqs49
                                                                                                        del clause1
                                                                                                        arith eq adapter3
                                                                                                        memory16.220000
                                                                                                        max memory19.050000
                                                                                                        Expand
                                                                                                        • start[0.027s]
                                                                                                            not (l = []) && Ordinal.count l >= 0 && Ordinal.count (List.tl l) >= 0
                                                                                                            ==> List.tl l = []
                                                                                                                || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl l)))
                                                                                                                   (Ordinal.Int (Ordinal.count l))
                                                                                                        • simplify
                                                                                                          into
                                                                                                          (not
                                                                                                           ((not (l = []) && Ordinal.count l >= 0) && Ordinal.count (List.tl l) >= 0)
                                                                                                           || List.tl l = [])
                                                                                                          || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl l)))
                                                                                                             (Ordinal.Int (Ordinal.count l))
                                                                                                          expansions
                                                                                                          []
                                                                                                          rewrite_steps
                                                                                                            forward_chaining
                                                                                                            • unroll
                                                                                                              expr
                                                                                                              (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`ty_0 option list`_1366|
                                                                                                                                             …
                                                                                                              expansions
                                                                                                              • unroll
                                                                                                                expr
                                                                                                                (|count_`ty_0 option list`_1366| (|get.::.1_1347| l_1357))
                                                                                                                expansions
                                                                                                                • unroll
                                                                                                                  expr
                                                                                                                  (|count_`ty_0 option list`_1366| l_1357)
                                                                                                                  expansions
                                                                                                                  • unsat
                                                                                                                    (let ((a!1 (= (|count_`ty_0 option list`_1366| l_1357)
                                                                                                                                  (+ 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.018s
                                                                                                                  details
                                                                                                                  Expand
                                                                                                                  smt_stats
                                                                                                                  num checks8
                                                                                                                  arith assert lower15
                                                                                                                  arith pivots8
                                                                                                                  rlimit count2597
                                                                                                                  mk clause12
                                                                                                                  datatype occurs check29
                                                                                                                  mk bool var87
                                                                                                                  arith assert upper12
                                                                                                                  datatype splits9
                                                                                                                  decisions24
                                                                                                                  arith add rows12
                                                                                                                  propagations10
                                                                                                                  conflicts10
                                                                                                                  arith fixed eqs7
                                                                                                                  datatype accessor ax10
                                                                                                                  arith conflicts2
                                                                                                                  arith assert diseq1
                                                                                                                  datatype constructor ax16
                                                                                                                  num allocs128881521
                                                                                                                  final checks8
                                                                                                                  added eqs58
                                                                                                                  del clause5
                                                                                                                  arith eq adapter10
                                                                                                                  memory19.710000
                                                                                                                  max memory19.710000
                                                                                                                  Expand
                                                                                                                  • start[0.018s]
                                                                                                                      not (_x = []) && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                                                                                                                      ==> List.tl _x = []
                                                                                                                          || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x)))
                                                                                                                             (Ordinal.Int (Ordinal.count _x))
                                                                                                                  • simplify
                                                                                                                    into
                                                                                                                    (not
                                                                                                                     ((not (_x = []) && Ordinal.count _x >= 0) && Ordinal.count (List.tl _x) >= 0)
                                                                                                                     || List.tl _x = [])
                                                                                                                    || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x)))
                                                                                                                       (Ordinal.Int (Ordinal.count _x))
                                                                                                                    expansions
                                                                                                                    []
                                                                                                                    rewrite_steps
                                                                                                                      forward_chaining
                                                                                                                      • unroll
                                                                                                                        expr
                                                                                                                        (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`ty_0 list list`_1425|
                                                                                                                                                         …
                                                                                                                        expansions
                                                                                                                        • unroll
                                                                                                                          expr
                                                                                                                          (|count_`ty_0 list list`_1425| (|get.::.1_1405| _x_1416))
                                                                                                                          expansions
                                                                                                                          • unroll
                                                                                                                            expr
                                                                                                                            (|count_`ty_0 list list`_1425| _x_1416)
                                                                                                                            expansions
                                                                                                                            • unsat
                                                                                                                              (let ((a!1 (ite (>= (|count_`ty_0 list`_1427| (|get.::.0_1404| _x_1416)) 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.098s
                                                                                                                            details
                                                                                                                            Expand
                                                                                                                            smt_stats
                                                                                                                            num checks8
                                                                                                                            arith assert lower15
                                                                                                                            arith pivots8
                                                                                                                            rlimit count2597
                                                                                                                            mk clause12
                                                                                                                            datatype occurs check29
                                                                                                                            mk bool var87
                                                                                                                            arith assert upper12
                                                                                                                            datatype splits9
                                                                                                                            decisions24
                                                                                                                            arith add rows12
                                                                                                                            propagations10
                                                                                                                            conflicts10
                                                                                                                            arith fixed eqs7
                                                                                                                            datatype accessor ax10
                                                                                                                            arith conflicts2
                                                                                                                            arith assert diseq1
                                                                                                                            datatype constructor ax16
                                                                                                                            num allocs153683562
                                                                                                                            final checks8
                                                                                                                            added eqs58
                                                                                                                            del clause5
                                                                                                                            arith eq adapter10
                                                                                                                            memory20.240000
                                                                                                                            max memory20.240000
                                                                                                                            Expand
                                                                                                                            • start[0.098s]
                                                                                                                                not (_x = []) && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                                                                                                                                ==> List.tl _x = []
                                                                                                                                    || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x)))
                                                                                                                                       (Ordinal.Int (Ordinal.count _x))
                                                                                                                            • simplify
                                                                                                                              into
                                                                                                                              (not
                                                                                                                               ((not (_x = []) && Ordinal.count _x >= 0) && Ordinal.count (List.tl _x) >= 0)
                                                                                                                               || List.tl _x = [])
                                                                                                                              || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x)))
                                                                                                                                 (Ordinal.Int (Ordinal.count _x))
                                                                                                                              expansions
                                                                                                                              []
                                                                                                                              rewrite_steps
                                                                                                                                forward_chaining
                                                                                                                                • unroll
                                                                                                                                  expr
                                                                                                                                  (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`ty_0 list list`_1463|
                                                                                                                                                                   …
                                                                                                                                  expansions
                                                                                                                                  • unroll
                                                                                                                                    expr
                                                                                                                                    (|count_`ty_0 list list`_1463| (|get.::.1_1437| _x_1454))
                                                                                                                                    expansions
                                                                                                                                    • unroll
                                                                                                                                      expr
                                                                                                                                      (|count_`ty_0 list list`_1463| _x_1454)
                                                                                                                                      expansions
                                                                                                                                      • unsat
                                                                                                                                        (let ((a!1 (ite (>= (|count_`ty_0 list`_1465| (|get.::.0_1436| _x_1454)) 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.035s
                                                                                                                                      details
                                                                                                                                      Expand
                                                                                                                                      smt_stats
                                                                                                                                      num checks8
                                                                                                                                      arith assert lower15
                                                                                                                                      arith pivots8
                                                                                                                                      rlimit count2641
                                                                                                                                      mk clause12
                                                                                                                                      datatype occurs check29
                                                                                                                                      mk bool var87
                                                                                                                                      arith assert upper12
                                                                                                                                      datatype splits9
                                                                                                                                      decisions24
                                                                                                                                      arith add rows15
                                                                                                                                      propagations10
                                                                                                                                      conflicts10
                                                                                                                                      arith fixed eqs7
                                                                                                                                      datatype accessor ax10
                                                                                                                                      arith conflicts2
                                                                                                                                      arith assert diseq1
                                                                                                                                      datatype constructor ax16
                                                                                                                                      num allocs180853479
                                                                                                                                      final checks8
                                                                                                                                      added eqs58
                                                                                                                                      del clause5
                                                                                                                                      arith eq adapter10
                                                                                                                                      memory20.800000
                                                                                                                                      max memory23.570000
                                                                                                                                      Expand
                                                                                                                                      • start[0.035s]
                                                                                                                                          not (_x = []) && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                                                                                                                                          ==> List.tl _x = []
                                                                                                                                              || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x)))
                                                                                                                                                 (Ordinal.Int (Ordinal.count _x))
                                                                                                                                      • simplify
                                                                                                                                        into
                                                                                                                                        (not
                                                                                                                                         ((not (_x = []) && Ordinal.count _x >= 0) && Ordinal.count (List.tl _x) >= 0)
                                                                                                                                         || List.tl _x = [])
                                                                                                                                        || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x)))
                                                                                                                                           (Ordinal.Int (Ordinal.count _x))
                                                                                                                                        expansions
                                                                                                                                        []
                                                                                                                                        rewrite_steps
                                                                                                                                          forward_chaining
                                                                                                                                          • unroll
                                                                                                                                            expr
                                                                                                                                            (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`ty_0 list list`_1496|
                                                                                                                                                                             …
                                                                                                                                            expansions
                                                                                                                                            • unroll
                                                                                                                                              expr
                                                                                                                                              (|count_`ty_0 list list`_1496| (|get.::.1_1475| _x_1487))
                                                                                                                                              expansions
                                                                                                                                              • unroll
                                                                                                                                                expr
                                                                                                                                                (|count_`ty_0 list list`_1496| _x_1487)
                                                                                                                                                expansions
                                                                                                                                                • unsat
                                                                                                                                                  (let ((a!1 (ite (>= (|count_`ty_0 list`_1498| (|get.::.0_1474| _x_1487)) 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.077s
                                                                                                                                                details
                                                                                                                                                Expand
                                                                                                                                                smt_stats
                                                                                                                                                arith offset eqs90
                                                                                                                                                num checks26
                                                                                                                                                arith assert lower489
                                                                                                                                                arith pivots125
                                                                                                                                                rlimit count45082
                                                                                                                                                mk clause546
                                                                                                                                                datatype occurs check210
                                                                                                                                                mk bool var1201
                                                                                                                                                arith assert upper465
                                                                                                                                                datatype splits109
                                                                                                                                                decisions1043
                                                                                                                                                arith add rows600
                                                                                                                                                arith bound prop67
                                                                                                                                                propagations1328
                                                                                                                                                interface eqs19
                                                                                                                                                conflicts101
                                                                                                                                                arith fixed eqs207
                                                                                                                                                datatype accessor ax121
                                                                                                                                                minimized lits26
                                                                                                                                                arith conflicts32
                                                                                                                                                arith assert diseq164
                                                                                                                                                datatype constructor ax312
                                                                                                                                                num allocs200964948
                                                                                                                                                final checks56
                                                                                                                                                added eqs1655
                                                                                                                                                del clause277
                                                                                                                                                arith eq adapter317
                                                                                                                                                memory24.920000
                                                                                                                                                max memory24.920000
                                                                                                                                                Expand
                                                                                                                                                • start[0.077s]
                                                                                                                                                    not (List.tl (List.tl _x) = [])
                                                                                                                                                    && not (List.tl _x = [])
                                                                                                                                                       && not (_x = [])
                                                                                                                                                          && Ordinal.count _x >= 0
                                                                                                                                                             && Ordinal.count (List.tl (List.tl (List.tl _x))) >= 0
                                                                                                                                                    ==> not
                                                                                                                                                        (not (List.tl (List.tl (List.tl (List.tl (List.tl _x)))) = [])
                                                                                                                                                         && not (List.tl (List.tl (List.tl (List.tl _x))) = [])
                                                                                                                                                            && not (List.tl (List.tl (List.tl _x)) = []))
                                                                                                                                                        || Ordinal.( << )
                                                                                                                                                           (Ordinal.Int (Ordinal.count (List.tl (List.tl (List.tl _x)))))
                                                                                                                                                           (Ordinal.Int (Ordinal.count _x))
                                                                                                                                                • simplify
                                                                                                                                                  into
                                                                                                                                                  (not
                                                                                                                                                   ((((not (List.tl (List.tl _x) = []) && not (List.tl _x = []))
                                                                                                                                                      && not (_x = []))
                                                                                                                                                     && Ordinal.count _x >= 0)
                                                                                                                                                    && Ordinal.count (List.tl (List.tl (List.tl _x))) >= 0)
                                                                                                                                                   || not
                                                                                                                                                      ((not (List.tl (List.tl (List.tl (List.tl (List.tl _x)))) = [])
                                                                                                                                                        && not (List.tl (List.tl (List.tl (List.tl _x))) = []))
                                                                                                                                                       && not (List.tl (List.tl (List.tl _x)) = [])))
                                                                                                                                                  || Ordinal.( << )
                                                                                                                                                     (Ordinal.Int (Ordinal.count (List.tl (List.tl (List.tl _x)))))
                                                                                                                                                     (Ordinal.Int (Ordinal.count _x))
                                                                                                                                                  expansions
                                                                                                                                                  []
                                                                                                                                                  rewrite_steps
                                                                                                                                                    forward_chaining
                                                                                                                                                    • unroll
                                                                                                                                                      expr
                                                                                                                                                      (let ((a!1 (|count_`ty_0 list list`_1531|
                                                                                                                                                                   (|get.::.1_1508| (|get.::.1_1508| (|get.::.1_…
                                                                                                                                                      expansions
                                                                                                                                                      • unroll
                                                                                                                                                        expr
                                                                                                                                                        (|count_`ty_0 list list`_1531|
                                                                                                                                                          (|get.::.1_1508| (|get.::.1_1508| (|get.::.1_1508| _x_1522))))
                                                                                                                                                        expansions
                                                                                                                                                        • unroll
                                                                                                                                                          expr
                                                                                                                                                          (|count_`ty_0 list list`_1531| _x_1522)
                                                                                                                                                          expansions
                                                                                                                                                          • unroll
                                                                                                                                                            expr
                                                                                                                                                            (let ((a!1 (|get.::.1_1508| (|get.::.1_1508| (|get.::.1_1508| (|get.::.1_1508| _x_1522))))))
                                                                                                                                                              (|cou…
                                                                                                                                                            expansions
                                                                                                                                                            • unroll
                                                                                                                                                              expr
                                                                                                                                                              (let ((a!1 (|count_`ty_0 list list`_1531|
                                                                                                                                                                           (|get.::.1_1508| (|get.::.1_1508| (|get.::.1_…
                                                                                                                                                              expansions
                                                                                                                                                              • unroll
                                                                                                                                                                expr
                                                                                                                                                                (let ((a!1 (|get.::.0_1507| (|get.::.1_1508| (|get.::.1_1508| (|get.::.1_1508| _x_1522))))))
                                                                                                                                                                  (|cou…
                                                                                                                                                                expansions
                                                                                                                                                                • unroll
                                                                                                                                                                  expr
                                                                                                                                                                  (|count_`ty_0 list list`_1531| (|get.::.1_1508| _x_1522))
                                                                                                                                                                  expansions
                                                                                                                                                                  • unroll
                                                                                                                                                                    expr
                                                                                                                                                                    (|count_`ty_0 list`_1533| (|get.::.0_1507| _x_1522))
                                                                                                                                                                    expansions
                                                                                                                                                                    • unroll
                                                                                                                                                                      expr
                                                                                                                                                                      (let ((a!1 (|get.::.1_1508| (|get.::.1_1508| (|get.::.1_1508| (|get.::.1_1508| _x_1522))))))
                                                                                                                                                                        (|cou…
                                                                                                                                                                      expansions
                                                                                                                                                                      • unroll
                                                                                                                                                                        expr
                                                                                                                                                                        (let ((a!1 (|count_`ty_0 list list`_1531|
                                                                                                                                                                                     (|get.::.1_1508| (|get.::.1_1508| (|get.::.1_…
                                                                                                                                                                        expansions
                                                                                                                                                                        • unroll
                                                                                                                                                                          expr
                                                                                                                                                                          (let ((a!1 (|get.::.1_1508| (|get.::.1_1508| (|get.::.1_1508| (|get.::.1_1508| _x_1522))))))
                                                                                                                                                                            (|cou…
                                                                                                                                                                          expansions
                                                                                                                                                                          • unroll
                                                                                                                                                                            expr
                                                                                                                                                                            (|count_`ty_0 list list`_1531| (|get.::.1_1508| (|get.::.1_1508| _x_1522)))
                                                                                                                                                                            expansions
                                                                                                                                                                            • unsat
                                                                                                                                                                              (let ((a!1 (>= (|count_`ty_0 list`_1533|
                                                                                                                                                                                               (|get.::.0_1507| (|get.::.1_1508| _x_1522)…

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

                                                                                                                                                                                      termination proof

                                                                                                                                                                                      Termination proof

                                                                                                                                                                                      call `match_cols (List.tl y)` from `match_cols y`
                                                                                                                                                                                      originalmatch_cols y
                                                                                                                                                                                      submatch_cols (List.tl y)
                                                                                                                                                                                      original ordinalOrdinal.Int (Ordinal.count y)
                                                                                                                                                                                      sub ordinalOrdinal.Int (Ordinal.count (List.tl y))
                                                                                                                                                                                      path[(List.hd y).0 = None || (List.hd y).1 = None && not (y = [])]
                                                                                                                                                                                      proof
                                                                                                                                                                                      detailed proof
                                                                                                                                                                                      ground_instances3
                                                                                                                                                                                      definitions0
                                                                                                                                                                                      inductions0
                                                                                                                                                                                      search_time
                                                                                                                                                                                      0.014s
                                                                                                                                                                                      details
                                                                                                                                                                                      Expand
                                                                                                                                                                                      smt_stats
                                                                                                                                                                                      num checks7
                                                                                                                                                                                      arith assert lower6
                                                                                                                                                                                      arith pivots5
                                                                                                                                                                                      rlimit count5693
                                                                                                                                                                                      mk clause28
                                                                                                                                                                                      datatype occurs check66
                                                                                                                                                                                      mk bool var164
                                                                                                                                                                                      arith assert upper4
                                                                                                                                                                                      datatype splits42
                                                                                                                                                                                      decisions34
                                                                                                                                                                                      arith add rows6
                                                                                                                                                                                      propagations51
                                                                                                                                                                                      conflicts12
                                                                                                                                                                                      arith fixed eqs3
                                                                                                                                                                                      datatype accessor ax27
                                                                                                                                                                                      arith conflicts1
                                                                                                                                                                                      datatype constructor ax35
                                                                                                                                                                                      num allocs300182486
                                                                                                                                                                                      final checks14
                                                                                                                                                                                      added eqs150
                                                                                                                                                                                      del clause2
                                                                                                                                                                                      arith eq adapter3
                                                                                                                                                                                      memory30.060000
                                                                                                                                                                                      max memory30.060000
                                                                                                                                                                                      Expand
                                                                                                                                                                                      • start[0.014s]
                                                                                                                                                                                          ((List.hd y).0 = None || (List.hd y).1 = None)
                                                                                                                                                                                          && not (y = []) && Ordinal.count y >= 0 && Ordinal.count (List.tl y) >= 0
                                                                                                                                                                                          ==> not
                                                                                                                                                                                              (((List.hd (List.tl y)).0 = None || (List.hd (List.tl y)).1 = None)
                                                                                                                                                                                               && not (List.tl y = []))
                                                                                                                                                                                              && not
                                                                                                                                                                                                 (Option.get (List.hd (List.tl y)).0 =
                                                                                                                                                                                                  Option.get (List.hd (List.tl y)).1
                                                                                                                                                                                                  && not
                                                                                                                                                                                                     ((List.hd (List.tl y)).0 = None
                                                                                                                                                                                                      || (List.hd (List.tl y)).1 = None)
                                                                                                                                                                                                     && not (List.tl y = []))
                                                                                                                                                                                              || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl y)))
                                                                                                                                                                                                 (Ordinal.Int (Ordinal.count y))
                                                                                                                                                                                      • simplify
                                                                                                                                                                                        into
                                                                                                                                                                                        (not
                                                                                                                                                                                         (((((List.hd y).0 = None || (List.hd y).1 = None) && not (y = []))
                                                                                                                                                                                           && Ordinal.count y >= 0)
                                                                                                                                                                                          && Ordinal.count (List.tl y) >= 0)
                                                                                                                                                                                         || not
                                                                                                                                                                                            (((List.hd (List.tl y)).0 = None || (List.hd (List.tl y)).1 = None)
                                                                                                                                                                                             && not (List.tl y = []))
                                                                                                                                                                                            && not
                                                                                                                                                                                               ((Option.get (List.hd (List.tl y)).0 =
                                                                                                                                                                                                 Option.get (List.hd (List.tl y)).1
                                                                                                                                                                                                 && not
                                                                                                                                                                                                    ((List.hd (List.tl y)).0 = None || (List.hd (List.tl y)).1 = None))
                                                                                                                                                                                                && not (List.tl y = [])))
                                                                                                                                                                                        || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl y)))
                                                                                                                                                                                           (Ordinal.Int (Ordinal.count y))
                                                                                                                                                                                        expansions
                                                                                                                                                                                        []
                                                                                                                                                                                        rewrite_steps
                                                                                                                                                                                          forward_chaining
                                                                                                                                                                                          • unroll
                                                                                                                                                                                            expr
                                                                                                                                                                                            (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`(ty_0 option * ty_0 option) list`_1875|
                                                                                                                                                                                                           …
                                                                                                                                                                                            expansions
                                                                                                                                                                                            • unroll
                                                                                                                                                                                              expr
                                                                                                                                                                                              (|count_`(ty_0 option * ty_0 option) list`_1875| (|get.::.1_1857| y_1864))
                                                                                                                                                                                              expansions
                                                                                                                                                                                              • unroll
                                                                                                                                                                                                expr
                                                                                                                                                                                                (|count_`(ty_0 option * ty_0 option) list`_1875| y_1864)
                                                                                                                                                                                                expansions
                                                                                                                                                                                                • unsat
                                                                                                                                                                                                  (let ((a!1 (= (|count_`(ty_0 option * ty_0 option) list`_1875| y_1864)
                                                                                                                                                                                                                (+ 4
                                                                                                                                                                                                            …

                                                                                                                                                                                                call `match_cols (List.tl y)` from `match_cols y`
                                                                                                                                                                                                originalmatch_cols y
                                                                                                                                                                                                submatch_cols (List.tl y)
                                                                                                                                                                                                original ordinalOrdinal.Int (Ordinal.count y)
                                                                                                                                                                                                sub ordinalOrdinal.Int (Ordinal.count (List.tl y))
                                                                                                                                                                                                path[Option.get (List.hd y).0 = Option.get (List.hd y).1 && not ((List.hd y).0 = None || (List.hd y).1 = None) && not (y = [])]
                                                                                                                                                                                                proof
                                                                                                                                                                                                detailed proof
                                                                                                                                                                                                ground_instances3
                                                                                                                                                                                                definitions0
                                                                                                                                                                                                inductions0
                                                                                                                                                                                                search_time
                                                                                                                                                                                                0.015s
                                                                                                                                                                                                details
                                                                                                                                                                                                Expand
                                                                                                                                                                                                smt_stats
                                                                                                                                                                                                num checks7
                                                                                                                                                                                                arith assert lower5
                                                                                                                                                                                                arith pivots4
                                                                                                                                                                                                rlimit count2887
                                                                                                                                                                                                mk clause26
                                                                                                                                                                                                datatype occurs check59
                                                                                                                                                                                                mk bool var147
                                                                                                                                                                                                arith assert upper5
                                                                                                                                                                                                datatype splits26
                                                                                                                                                                                                decisions31
                                                                                                                                                                                                arith add rows7
                                                                                                                                                                                                propagations57
                                                                                                                                                                                                conflicts13
                                                                                                                                                                                                arith fixed eqs4
                                                                                                                                                                                                datatype accessor ax26
                                                                                                                                                                                                arith conflicts1
                                                                                                                                                                                                datatype constructor ax34
                                                                                                                                                                                                num allocs279674675
                                                                                                                                                                                                final checks11
                                                                                                                                                                                                added eqs148
                                                                                                                                                                                                del clause2
                                                                                                                                                                                                arith eq adapter3
                                                                                                                                                                                                memory27.140000
                                                                                                                                                                                                max memory27.140000
                                                                                                                                                                                                Expand
                                                                                                                                                                                                • start[0.015s]
                                                                                                                                                                                                    Option.get (List.hd y).0 = Option.get (List.hd y).1
                                                                                                                                                                                                    && not ((List.hd y).0 = None || (List.hd y).1 = None)
                                                                                                                                                                                                       && not (y = [])
                                                                                                                                                                                                          && Ordinal.count y >= 0 && Ordinal.count (List.tl y) >= 0
                                                                                                                                                                                                    ==> not
                                                                                                                                                                                                        (((List.hd (List.tl y)).0 = None || (List.hd (List.tl y)).1 = None)
                                                                                                                                                                                                         && not (List.tl y = []))
                                                                                                                                                                                                        && not
                                                                                                                                                                                                           (Option.get (List.hd (List.tl y)).0 =
                                                                                                                                                                                                            Option.get (List.hd (List.tl y)).1
                                                                                                                                                                                                            && not
                                                                                                                                                                                                               ((List.hd (List.tl y)).0 = None
                                                                                                                                                                                                                || (List.hd (List.tl y)).1 = None)
                                                                                                                                                                                                               && not (List.tl y = []))
                                                                                                                                                                                                        || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl y)))
                                                                                                                                                                                                           (Ordinal.Int (Ordinal.count y))
                                                                                                                                                                                                • simplify
                                                                                                                                                                                                  into
                                                                                                                                                                                                  (not
                                                                                                                                                                                                   ((((Option.get (List.hd y).0 = Option.get (List.hd y).1
                                                                                                                                                                                                       && not ((List.hd y).0 = None || (List.hd y).1 = None))
                                                                                                                                                                                                      && not (y = []))
                                                                                                                                                                                                     && Ordinal.count y >= 0)
                                                                                                                                                                                                    && Ordinal.count (List.tl y) >= 0)
                                                                                                                                                                                                   || not
                                                                                                                                                                                                      (((List.hd (List.tl y)).0 = None || (List.hd (List.tl y)).1 = None)
                                                                                                                                                                                                       && not (List.tl y = []))
                                                                                                                                                                                                      && not
                                                                                                                                                                                                         ((Option.get (List.hd (List.tl y)).0 =
                                                                                                                                                                                                           Option.get (List.hd (List.tl y)).1
                                                                                                                                                                                                           && not
                                                                                                                                                                                                              ((List.hd (List.tl y)).0 = None || (List.hd (List.tl y)).1 = None))
                                                                                                                                                                                                          && not (List.tl y = [])))
                                                                                                                                                                                                  || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl y)))
                                                                                                                                                                                                     (Ordinal.Int (Ordinal.count y))
                                                                                                                                                                                                  expansions
                                                                                                                                                                                                  []
                                                                                                                                                                                                  rewrite_steps
                                                                                                                                                                                                    forward_chaining
                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                      expr
                                                                                                                                                                                                      (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`(ty_0 option * ty_0 option) list`_1875|
                                                                                                                                                                                                                     …
                                                                                                                                                                                                      expansions
                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                        expr
                                                                                                                                                                                                        (|count_`(ty_0 option * ty_0 option) list`_1875| (|get.::.1_1857| y_1864))
                                                                                                                                                                                                        expansions
                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                          expr
                                                                                                                                                                                                          (|count_`(ty_0 option * ty_0 option) list`_1875| y_1864)
                                                                                                                                                                                                          expansions
                                                                                                                                                                                                          • unsat
                                                                                                                                                                                                            (let ((a!1 (= (|count_`(ty_0 option * ty_0 option) list`_1875| y_1864)
                                                                                                                                                                                                                          (+ 4
                                                                                                                                                                                                                      …

                                                                                                                                                                                                          termination proof

                                                                                                                                                                                                          Termination proof

                                                                                                                                                                                                          call `match_rows (List.tl x)` from `match_rows x`
                                                                                                                                                                                                          originalmatch_rows x
                                                                                                                                                                                                          submatch_rows (List.tl x)
                                                                                                                                                                                                          original ordinalOrdinal.Int (Ordinal.count x)
                                                                                                                                                                                                          sub ordinalOrdinal.Int (Ordinal.count (List.tl x))
                                                                                                                                                                                                          path[match_cols (zip (List.hd x).0 (List.hd x).1) && not (x = [])]
                                                                                                                                                                                                          proof
                                                                                                                                                                                                          detailed proof
                                                                                                                                                                                                          ground_instances5
                                                                                                                                                                                                          definitions0
                                                                                                                                                                                                          inductions0
                                                                                                                                                                                                          search_time
                                                                                                                                                                                                          0.025s
                                                                                                                                                                                                          details
                                                                                                                                                                                                          Expand
                                                                                                                                                                                                          smt_stats
                                                                                                                                                                                                          arith offset eqs5
                                                                                                                                                                                                          num checks12
                                                                                                                                                                                                          arith assert lower30
                                                                                                                                                                                                          arith pivots20
                                                                                                                                                                                                          rlimit count6702
                                                                                                                                                                                                          mk clause54
                                                                                                                                                                                                          datatype occurs check72
                                                                                                                                                                                                          mk bool var239
                                                                                                                                                                                                          arith assert upper28
                                                                                                                                                                                                          datatype splits27
                                                                                                                                                                                                          decisions92
                                                                                                                                                                                                          arith add rows31
                                                                                                                                                                                                          propagations49
                                                                                                                                                                                                          conflicts17
                                                                                                                                                                                                          arith fixed eqs11
                                                                                                                                                                                                          datatype accessor ax32
                                                                                                                                                                                                          minimized lits2
                                                                                                                                                                                                          arith conflicts6
                                                                                                                                                                                                          arith assert diseq1
                                                                                                                                                                                                          datatype constructor ax55
                                                                                                                                                                                                          num allocs356986655
                                                                                                                                                                                                          final checks11
                                                                                                                                                                                                          added eqs212
                                                                                                                                                                                                          del clause21
                                                                                                                                                                                                          arith eq adapter20
                                                                                                                                                                                                          memory27.850000
                                                                                                                                                                                                          max memory30.260000
                                                                                                                                                                                                          Expand
                                                                                                                                                                                                          • start[0.025s]
                                                                                                                                                                                                              match_cols (zip (List.hd x).0 (List.hd x).1)
                                                                                                                                                                                                              && not (x = []) && Ordinal.count x >= 0 && Ordinal.count (List.tl x) >= 0
                                                                                                                                                                                                              ==> not
                                                                                                                                                                                                                  (match_cols (zip (List.hd (List.tl x)).0 (List.hd (List.tl x)).1)
                                                                                                                                                                                                                   && not (List.tl x = []))
                                                                                                                                                                                                                  || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl x)))
                                                                                                                                                                                                                     (Ordinal.Int (Ordinal.count x))
                                                                                                                                                                                                          • simplify
                                                                                                                                                                                                            into
                                                                                                                                                                                                            (not
                                                                                                                                                                                                             (((match_cols (zip (List.hd x).0 (List.hd x).1) && not (x = []))
                                                                                                                                                                                                               && Ordinal.count x >= 0)
                                                                                                                                                                                                              && Ordinal.count (List.tl x) >= 0)
                                                                                                                                                                                                             || not
                                                                                                                                                                                                                (match_cols (zip (List.hd (List.tl x)).0 (List.hd (List.tl x)).1)
                                                                                                                                                                                                                 && not (List.tl x = [])))
                                                                                                                                                                                                            || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl x)))
                                                                                                                                                                                                               (Ordinal.Int (Ordinal.count x))
                                                                                                                                                                                                            expansions
                                                                                                                                                                                                            []
                                                                                                                                                                                                            rewrite_steps
                                                                                                                                                                                                              forward_chaining
                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                expr
                                                                                                                                                                                                                (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`(ty_0 option list * ty_0 option list) list`_1932|
                                                                                                                                                                                                                     …
                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                  (zip_1910 (|tuple_get.0_1893| (|get.::.0_1896| (|get.::.1_1897| x_1923)))
                                                                                                                                                                                                                            (|tuple_get.1_18…
                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                    (let ((a!1 (zip_1910 (|tuple_get.0_1893|
                                                                                                                                                                                                                                           (|get.::.0_1896| (|get.::.1_1897| x_…
                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                      (|count_`(ty_0 option list * ty_0 option list) list`_1932|
                                                                                                                                                                                                                        (|get.::.1_1897| x_1923))
                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                        (|count_`(ty_0 option list * ty_0 option list) list`_1932| x_1923)
                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                        • unsat
                                                                                                                                                                                                                          (let ((a!1 (>= (|count_`ty_0 option list`_1936|
                                                                                                                                                                                                                                           (|tuple_get.0_1893| (|get.::.0_1896…

                                                                                                                                                                                                                        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.341s):
                                                                                                                                                                                                                          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