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.049s
details
Expand
smt_stats
num checks7
arith assert lower6
arith pivots3
rlimit count1805
mk clause3
datatype occurs check21
mk bool var48
arith assert upper4
datatype splits3
decisions6
arith add rows7
propagations2
conflicts6
arith fixed eqs4
datatype accessor ax5
arith conflicts1
datatype constructor ax7
num allocs1520689813
final checks6
added eqs30
del clause1
arith eq adapter3
memory18.950000
max memory21.900000
Expand
  • start[0.049s]
      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.<<_122| (|Ordinal.Int_113|
                            (|count_`ty_0 list`_2477| (|get.::.1_2464| …
        expansions
        • unroll
          expr
          (|count_`ty_0 list`_2477| (|get.::.1_2464| _x_2468))
          expansions
          • unroll
            expr
            (|count_`ty_0 list`_2477| _x_2468)
            expansions
            • unsat
              (let ((a!1 (= (|count_`ty_0 list`_2477| _x_2468)
                            (+ 1 (|count_`ty_0 list`_2477| (|get.…

            Rows, columns, blocks

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

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

            Termination proof

            call `transpose3 (List.tl _x)` from `transpose3 _x`
            originaltranspose3 _x
            subtranspose3 (List.tl _x)
            original ordinalOrdinal.Int (Ordinal.count _x)
            sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
            path[List.hd _x = [] && _x <> [] && not (_x = [])]
            proof
            detailed proof
            ground_instances3
            definitions0
            inductions0
            search_time
            0.055s
            details
            Expand
            smt_stats
            num checks8
            arith assert lower17
            arith pivots8
            rlimit count8378
            mk clause44
            datatype occurs check32
            mk bool var138
            arith assert upper19
            datatype splits10
            decisions33
            arith add rows18
            propagations97
            conflicts14
            arith fixed eqs9
            datatype accessor ax15
            arith conflicts2
            datatype constructor ax23
            num allocs1668493406
            final checks9
            added eqs116
            del clause16
            arith eq adapter13
            memory19.210000
            max memory21.900000
            Expand
            • start[0.055s]
                (List.hd _x = [] && _x <> [])
                && not (_x = [])
                   && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                ==> not
                    ((List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                     && not (List.tl _x = []))
                    && not
                       (not (List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                        && not (List.tl _x = []))
                    || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl _x)))
                       (Ordinal.Int (Ordinal.count _x))
            • simplify
              into
              (not
               ((((List.hd _x = [] && _x <> []) && not (_x = [])) && Ordinal.count _x >= 0)
                && Ordinal.count (List.tl _x) >= 0)
               || not
                  ((List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                   && not (List.tl _x = []))
                  && not
                     (not (List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                      && not (List.tl _x = [])))
              || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl _x)))
                 (Ordinal.Int (Ordinal.count _x))
              expansions
              []
              rewrite_steps
                forward_chaining
                • unroll
                  expr
                  (|Ordinal.<<_122| (|Ordinal.Int_113|
                                      (|count_`ty_0 list list`_2509| (|get.::.1_2…
                  expansions
                  • unroll
                    expr
                    (|count_`ty_0 list list`_2509| (|get.::.1_2496| _x_2502))
                    expansions
                    • unroll
                      expr
                      (|count_`ty_0 list list`_2509| _x_2502)
                      expansions
                      • unsat
                        (let ((a!1 (= (ite (>= (|count_`ty_0 list`_2511| |[]_2|) 0)
                                           (|count_`ty_0 list`_2…

                      call `transpose3 (List.tl _x)` from `transpose3 _x`
                      originaltranspose3 _x
                      subtranspose3 (List.tl _x)
                      original ordinalOrdinal.Int (Ordinal.count _x)
                      sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
                      path[not (List.hd _x = [] && _x <> []) && not (_x = [])]
                      proof
                      detailed proof
                      ground_instances3
                      definitions0
                      inductions0
                      search_time
                      0.105s
                      details
                      Expand
                      smt_stats
                      num checks8
                      arith assert lower12
                      arith pivots7
                      rlimit count5160
                      mk clause36
                      datatype occurs check69
                      mk bool var159
                      arith assert upper13
                      datatype splits26
                      decisions44
                      arith add rows13
                      propagations72
                      conflicts15
                      arith fixed eqs6
                      datatype accessor ax18
                      arith conflicts2
                      arith assert diseq1
                      datatype constructor ax32
                      num allocs1595096477
                      final checks15
                      added eqs132
                      del clause7
                      arith eq adapter10
                      memory19.250000
                      max memory21.900000
                      Expand
                      • start[0.105s]
                          not (List.hd _x = [] && _x <> [])
                          && not (_x = [])
                             && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                          ==> not
                              ((List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                               && not (List.tl _x = []))
                              && not
                                 (not (List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                  && not (List.tl _x = []))
                              || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl _x)))
                                 (Ordinal.Int (Ordinal.count _x))
                      • simplify
                        into
                        (not
                         (((not (List.hd _x = [] && _x <> []) && not (_x = []))
                           && Ordinal.count _x >= 0)
                          && Ordinal.count (List.tl _x) >= 0)
                         || not
                            ((List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                             && not (List.tl _x = []))
                            && not
                               (not (List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                && not (List.tl _x = [])))
                        || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl _x)))
                           (Ordinal.Int (Ordinal.count _x))
                        expansions
                        []
                        rewrite_steps
                          forward_chaining
                          • unroll
                            expr
                            (|Ordinal.<<_122| (|Ordinal.Int_113|
                                                (|count_`ty_0 list list`_2509| (|get.::.1_2…
                            expansions
                            • unroll
                              expr
                              (|count_`ty_0 list list`_2509| (|get.::.1_2496| _x_2502))
                              expansions
                              • unroll
                                expr
                                (|count_`ty_0 list list`_2509| _x_2502)
                                expansions
                                • unsat
                                  (let ((a!1 (ite (>= (|count_`ty_0 list`_2511| (|get.::.0_2495| _x_2502)) 0)
                                                  (|count_…

                                termination proof

                                Termination proof

                                call `get_heads (List.tl _x)` from `get_heads _x`
                                originalget_heads _x
                                subget_heads (List.tl _x)
                                original ordinalOrdinal.Int (Ordinal.count _x)
                                sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
                                path[List.hd _x = [] && _x <> [] && not (_x = [])]
                                proof
                                detailed proof
                                ground_instances3
                                definitions0
                                inductions0
                                search_time
                                0.026s
                                details
                                Expand
                                smt_stats
                                num checks8
                                arith assert lower16
                                arith pivots7
                                rlimit count14816
                                mk clause42
                                datatype occurs check42
                                mk bool var134
                                arith assert upper18
                                datatype splits10
                                decisions28
                                arith add rows15
                                propagations91
                                conflicts13
                                arith fixed eqs8
                                datatype accessor ax15
                                arith conflicts2
                                arith assert diseq1
                                datatype constructor ax22
                                num allocs1756056877
                                final checks9
                                added eqs110
                                del clause14
                                arith eq adapter13
                                memory22.160000
                                max memory22.160000
                                Expand
                                • start[0.026s]
                                    (List.hd _x = [] && _x <> [])
                                    && not (_x = [])
                                       && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                                    ==> not
                                        ((List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                         && not (List.tl _x = []))
                                        && not
                                           (not (List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                            && not (List.tl _x = []))
                                        || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl _x)))
                                           (Ordinal.Int (Ordinal.count _x))
                                • simplify
                                  into
                                  (not
                                   ((((List.hd _x = [] && _x <> []) && not (_x = [])) && Ordinal.count _x >= 0)
                                    && Ordinal.count (List.tl _x) >= 0)
                                   || not
                                      ((List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                       && not (List.tl _x = []))
                                      && not
                                         (not (List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                          && not (List.tl _x = [])))
                                  || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl _x)))
                                     (Ordinal.Int (Ordinal.count _x))
                                  expansions
                                  []
                                  rewrite_steps
                                    forward_chaining
                                    • unroll
                                      expr
                                      (|Ordinal.<<_122| (|Ordinal.Int_113|
                                                          (|count_`ty_0 list list`_2542| (|get.::.1_2…
                                      expansions
                                      • unroll
                                        expr
                                        (|count_`ty_0 list list`_2542| (|get.::.1_2529| _x_2535))
                                        expansions
                                        • unroll
                                          expr
                                          (|count_`ty_0 list list`_2542| _x_2535)
                                          expansions
                                          • unsat
                                            (let ((a!1 (+ 1
                                                          (|count_`ty_0 list list`_2542| (|get.::.1_2529| _x_2535))
                                                        …

                                          call `get_heads (List.tl _x)` from `get_heads _x`
                                          originalget_heads _x
                                          subget_heads (List.tl _x)
                                          original ordinalOrdinal.Int (Ordinal.count _x)
                                          sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
                                          path[not (List.hd _x = [] && _x <> []) && not (_x = [])]
                                          proof
                                          detailed proof
                                          ground_instances3
                                          definitions0
                                          inductions0
                                          search_time
                                          0.040s
                                          details
                                          Expand
                                          smt_stats
                                          num checks8
                                          arith assert lower12
                                          arith pivots10
                                          rlimit count11726
                                          mk clause34
                                          datatype occurs check63
                                          mk bool var140
                                          arith assert upper9
                                          datatype splits22
                                          decisions40
                                          arith add rows18
                                          propagations54
                                          conflicts13
                                          arith fixed eqs5
                                          datatype accessor ax16
                                          arith conflicts2
                                          datatype constructor ax28
                                          num allocs1711906810
                                          final checks13
                                          added eqs112
                                          del clause6
                                          arith eq adapter7
                                          memory19.330000
                                          max memory21.900000
                                          Expand
                                          • start[0.040s]
                                              not (List.hd _x = [] && _x <> [])
                                              && not (_x = [])
                                                 && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                                              ==> not
                                                  ((List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                                   && not (List.tl _x = []))
                                                  && not
                                                     (not (List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                                      && not (List.tl _x = []))
                                                  || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl _x)))
                                                     (Ordinal.Int (Ordinal.count _x))
                                          • simplify
                                            into
                                            (not
                                             (((not (List.hd _x = [] && _x <> []) && not (_x = []))
                                               && Ordinal.count _x >= 0)
                                              && Ordinal.count (List.tl _x) >= 0)
                                             || not
                                                ((List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                                 && not (List.tl _x = []))
                                                && not
                                                   (not (List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                                    && not (List.tl _x = [])))
                                            || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl _x)))
                                               (Ordinal.Int (Ordinal.count _x))
                                            expansions
                                            []
                                            rewrite_steps
                                              forward_chaining
                                              • unroll
                                                expr
                                                (|Ordinal.<<_122| (|Ordinal.Int_113|
                                                                    (|count_`ty_0 list list`_2542| (|get.::.1_2…
                                                expansions
                                                • unroll
                                                  expr
                                                  (|count_`ty_0 list list`_2542| (|get.::.1_2529| _x_2535))
                                                  expansions
                                                  • unroll
                                                    expr
                                                    (|count_`ty_0 list list`_2542| _x_2535)
                                                    expansions
                                                    • unsat
                                                      (let ((a!1 (ite (>= (|count_`ty_0 list`_2544| (|get.::.0_2528| _x_2535)) 0)
                                                                      (|count_…

                                                    termination proof

                                                    Termination proof

                                                    call `transpose ((List.tl (List.hd l)) :: (transpose3 (List.tl l)))` from `transpose l`
                                                    originaltranspose l
                                                    subtranspose ((List.tl (List.hd l)) :: (transpose3 (List.tl l)))
                                                    original ordinalOrdinal.Int (if measure_transpose l >= 0 then measure_transpose l else 0)
                                                    sub ordinalOrdinal.Int (if measure_transpose ((List.tl (List.hd l)) :: (transpose3 (List.tl l))) >= 0 then measure_transpose ((List.tl (List.hd l)) :: (transpose3 (List.tl l))) else 0)
                                                    path[not (List.hd l = [] && l <> []) && not (l = [])]
                                                    proof
                                                    detailed proof
                                                    ground_instances3
                                                    definitions0
                                                    inductions0
                                                    search_time
                                                    0.031s
                                                    details
                                                    Expand
                                                    smt_stats
                                                    num checks7
                                                    arith assert lower5
                                                    arith pivots2
                                                    rlimit count16803
                                                    mk clause4
                                                    datatype occurs check30
                                                    mk bool var56
                                                    arith assert upper3
                                                    datatype splits6
                                                    decisions10
                                                    arith add rows2
                                                    propagations3
                                                    conflicts7
                                                    arith fixed eqs1
                                                    datatype accessor ax7
                                                    arith conflicts1
                                                    datatype constructor ax13
                                                    num allocs1870179999
                                                    final checks8
                                                    added eqs39
                                                    del clause4
                                                    arith eq adapter2
                                                    memory19.370000
                                                    max memory22.160000
                                                    Expand
                                                    • start[0.031s]
                                                        not (List.hd l = [] && l <> [])
                                                        && not (l = [])
                                                           && (if (if l = [] then 0 else List.length (List.hd l)) >= 0
                                                               then if l = [] then 0 else List.length (List.hd l) else 0)
                                                              >= 0
                                                              && (if (if (List.tl (List.hd l)) :: (transpose3 …) = [] then 0
                                                                      else List.length …)
                                                                     >= 0
                                                                  then
                                                                    if (List.tl (List.hd l)) :: (transpose3 …) = [] then 0
                                                                    else List.length …
                                                                  else 0)
                                                                 >= 0
                                                        ==> not
                                                            (not (List.tl (List.hd l) = [] && true)
                                                             && not ((List.tl (List.hd l)) :: (transpose3 …) = []))
                                                            || Ordinal.<<
                                                               (Ordinal.Int
                                                                (if (if (List.tl (List.hd l)) :: (transpose3 …) = [] then 0
                                                                     else List.length …)
                                                                    >= 0
                                                                 then
                                                                   if (List.tl (List.hd l)) :: (transpose3 …) = [] then 0
                                                                   else List.length …
                                                                 else 0))
                                                               (Ordinal.Int
                                                                (if (if l = [] then 0 else List.length (List.hd l)) >= 0
                                                                 then if l = [] then 0 else List.length (List.hd l) else 0))
                                                    • simplify
                                                      into
                                                      (not
                                                       (((not (List.hd l = [] && l <> []) && not (l = []))
                                                         && (if (if l = [] then 0 else List.length (List.hd l)) >= 0
                                                             then if l = [] then 0 else List.length (List.hd l) else 0)
                                                            >= 0)
                                                        && (if List.length (List.tl (List.hd l)) >= 0
                                                            then List.length (List.tl (List.hd l)) else 0)
                                                           >= 0)
                                                       || List.tl (List.hd l) = [])
                                                      || Ordinal.<<
                                                         (Ordinal.Int
                                                          (if List.length (List.tl (List.hd l)) >= 0
                                                           then List.length (List.tl (List.hd l)) else 0))
                                                         (Ordinal.Int
                                                          (if (if l = [] then 0 else List.length (List.hd l)) >= 0
                                                           then if l = [] then 0 else List.length (List.hd l) else 0))
                                                      expansions
                                                      []
                                                      rewrite_steps
                                                        forward_chaining
                                                        • unroll
                                                          expr
                                                          (let ((a!1 (>= (|List.length_2619| (|get.::.1_2593| (|get.::.0_2595| l_2612)))
                                                                         0))
                                                            …
                                                          expansions
                                                          • unroll
                                                            expr
                                                            (|List.length_2619| (|get.::.1_2593| (|get.::.0_2595| l_2612)))
                                                            expansions
                                                            • unroll
                                                              expr
                                                              (|List.length_2619| (|get.::.0_2595| l_2612))
                                                              expansions
                                                              • unsat
                                                                (let ((a!1 (+ 1 (|List.length_2619| (|get.::.1_2593| (|get.::.0_2595| l_2612)))))
                                                                      (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.078s
                                                              details
                                                              Expand
                                                              smt_stats
                                                              num checks7
                                                              arith assert lower5
                                                              arith pivots3
                                                              rlimit count18842
                                                              mk clause3
                                                              datatype occurs check31
                                                              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 allocs1916782565
                                                              final checks6
                                                              added eqs52
                                                              del clause1
                                                              arith eq adapter3
                                                              memory19.440000
                                                              max memory22.160000
                                                              Expand
                                                              • start[0.078s]
                                                                  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.<<_122| (|Ordinal.Int_113| (count_nat_2653 (|get.S.0_2454| x_2646)))
                                                                                      (|O…
                                                                    expansions
                                                                    • unroll
                                                                      expr
                                                                      (count_nat_2653 (|get.S.0_2454| x_2646))
                                                                      expansions
                                                                      • unroll
                                                                        expr
                                                                        (count_nat_2653 x_2646)
                                                                        expansions
                                                                        • unsat
                                                                          (let ((a!1 (= (count_nat_2653 x_2646)
                                                                                        (+ 1 (count_nat_2653 (|get.S.0_2454| x_2646)))))…

                                                                        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.078s
                                                                        details
                                                                        Expand
                                                                        smt_stats
                                                                        num checks7
                                                                        arith assert lower5
                                                                        arith pivots3
                                                                        rlimit count20881
                                                                        mk clause3
                                                                        datatype occurs check32
                                                                        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 allocs2001445546
                                                                        final checks6
                                                                        added eqs52
                                                                        del clause1
                                                                        arith eq adapter3
                                                                        memory19.500000
                                                                        max memory22.270000
                                                                        Expand
                                                                        • start[0.078s]
                                                                            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.<<_122| (|Ordinal.Int_113| (count_nat_2680 (|get.S.0_2454| x_2673)))
                                                                                                (|O…
                                                                              expansions
                                                                              • unroll
                                                                                expr
                                                                                (count_nat_2680 (|get.S.0_2454| x_2673))
                                                                                expansions
                                                                                • unroll
                                                                                  expr
                                                                                  (count_nat_2680 x_2673)
                                                                                  expansions
                                                                                  • unsat
                                                                                    (let ((a!1 (= (+ 1 (count_nat_2680 (|get.S.0_2454| x_2673)))
                                                                                                  (count_nat_2680 x_2673)))…

                                                                                  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.065s
                                                                                  details
                                                                                  Expand
                                                                                  smt_stats
                                                                                  num checks7
                                                                                  arith assert lower6
                                                                                  arith pivots3
                                                                                  rlimit count22797
                                                                                  mk clause3
                                                                                  datatype occurs check18
                                                                                  mk bool var50
                                                                                  arith assert upper4
                                                                                  datatype splits3
                                                                                  decisions6
                                                                                  arith add rows7
                                                                                  propagations2
                                                                                  conflicts6
                                                                                  arith fixed eqs4
                                                                                  datatype accessor ax5
                                                                                  arith conflicts1
                                                                                  datatype constructor ax7
                                                                                  num allocs2048470070
                                                                                  final checks5
                                                                                  added eqs30
                                                                                  del clause1
                                                                                  arith eq adapter3
                                                                                  memory22.270000
                                                                                  max memory22.270000
                                                                                  Expand
                                                                                  • start[0.065s]
                                                                                      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.<<_122| (|Ordinal.Int_113|
                                                                                                            (|count_`ty_0 list`_2707| (|get.::.1_2694| …
                                                                                        expansions
                                                                                        • unroll
                                                                                          expr
                                                                                          (|count_`ty_0 list`_2707| (|get.::.1_2694| y_2701))
                                                                                          expansions
                                                                                          • unroll
                                                                                            expr
                                                                                            (|count_`ty_0 list`_2707| y_2701)
                                                                                            expansions
                                                                                            • unsat
                                                                                              (let ((a!1 (= (|count_`ty_0 list`_2707| y_2701)
                                                                                                            (+ 1 (|count_`ty_0 list`_2707| (|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.159s
                                                                                            details
                                                                                            Expand
                                                                                            smt_stats
                                                                                            num checks9
                                                                                            arith assert lower6
                                                                                            arith pivots4
                                                                                            rlimit count25182
                                                                                            mk clause8
                                                                                            datatype occurs check21
                                                                                            mk bool var62
                                                                                            arith assert upper4
                                                                                            datatype splits3
                                                                                            decisions17
                                                                                            arith add rows5
                                                                                            propagations5
                                                                                            conflicts9
                                                                                            arith fixed eqs3
                                                                                            datatype accessor ax5
                                                                                            arith conflicts1
                                                                                            datatype constructor ax8
                                                                                            num allocs2132916039
                                                                                            final checks6
                                                                                            added eqs37
                                                                                            del clause1
                                                                                            arith eq adapter3
                                                                                            memory22.310000
                                                                                            max memory22.310000
                                                                                            Expand
                                                                                            • start[0.159s]
                                                                                                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.<<_122| (|Ordinal.Int_113|
                                                                                                                      (|count_`ty_0 list`_2734| (|get.::.1_2719| …
                                                                                                  expansions
                                                                                                  • unroll
                                                                                                    expr
                                                                                                    (elem_2724 (|get.::.0_2718| (|get.::.1_2719| x_2729))
                                                                                                               (|get.::.1_2719| (|get.::.1_2719| x…
                                                                                                    expansions
                                                                                                    • unroll
                                                                                                      expr
                                                                                                      (|count_`ty_0 list`_2734| (|get.::.1_2719| x_2729))
                                                                                                      expansions
                                                                                                      • unroll
                                                                                                        expr
                                                                                                        (|count_`ty_0 list`_2734| x_2729)
                                                                                                        expansions
                                                                                                        • unsat
                                                                                                          (let ((a!1 (= (|count_`ty_0 list`_2734| x_2729)
                                                                                                                        (+ 1 (|count_`ty_0 list`_2734| (|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.057s
                                                                                                        details
                                                                                                        Expand
                                                                                                        smt_stats
                                                                                                        num checks7
                                                                                                        arith assert lower5
                                                                                                        arith pivots3
                                                                                                        rlimit count27160
                                                                                                        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 allocs2183067721
                                                                                                        final checks8
                                                                                                        added eqs49
                                                                                                        del clause1
                                                                                                        arith eq adapter3
                                                                                                        memory22.340000
                                                                                                        max memory22.340000
                                                                                                        Expand
                                                                                                        • start[0.057s]
                                                                                                            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.<<_122| (|Ordinal.Int_113|
                                                                                                                                  (|count_`ty_0 option list`_2766| (|get.::.1…
                                                                                                              expansions
                                                                                                              • unroll
                                                                                                                expr
                                                                                                                (|count_`ty_0 option list`_2766| (|get.::.1_2751| l_2761))
                                                                                                                expansions
                                                                                                                • unroll
                                                                                                                  expr
                                                                                                                  (|count_`ty_0 option list`_2766| l_2761)
                                                                                                                  expansions
                                                                                                                  • unsat
                                                                                                                    (let ((a!1 (= (|count_`ty_0 option list`_2766| l_2761)
                                                                                                                                  (+ 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.119s
                                                                                                                  details
                                                                                                                  Expand
                                                                                                                  smt_stats
                                                                                                                  num checks8
                                                                                                                  arith assert lower15
                                                                                                                  arith pivots8
                                                                                                                  rlimit count29757
                                                                                                                  mk clause12
                                                                                                                  datatype occurs check37
                                                                                                                  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 allocs2274047271
                                                                                                                  final checks8
                                                                                                                  added eqs58
                                                                                                                  del clause5
                                                                                                                  arith eq adapter10
                                                                                                                  memory22.390000
                                                                                                                  max memory25.160000
                                                                                                                  Expand
                                                                                                                  • start[0.119s]
                                                                                                                      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.<<_122| (|Ordinal.Int_113|
                                                                                                                                            (|count_`ty_0 list list`_2828| (|get.::.1_2…
                                                                                                                        expansions
                                                                                                                        • unroll
                                                                                                                          expr
                                                                                                                          (|count_`ty_0 list list`_2828| (|get.::.1_2813| _x_2823))
                                                                                                                          expansions
                                                                                                                          • unroll
                                                                                                                            expr
                                                                                                                            (|count_`ty_0 list list`_2828| _x_2823)
                                                                                                                            expansions
                                                                                                                            • unsat
                                                                                                                              (let ((a!1 (ite (>= (|count_`ty_0 list`_2830| (|get.::.0_2812| _x_2823)) 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.115s
                                                                                                                            details
                                                                                                                            Expand
                                                                                                                            smt_stats
                                                                                                                            num checks8
                                                                                                                            arith assert lower16
                                                                                                                            arith pivots8
                                                                                                                            rlimit count32354
                                                                                                                            mk clause12
                                                                                                                            datatype occurs check29
                                                                                                                            mk bool var87
                                                                                                                            arith assert upper11
                                                                                                                            datatype splits9
                                                                                                                            decisions24
                                                                                                                            arith add rows12
                                                                                                                            propagations10
                                                                                                                            conflicts10
                                                                                                                            arith fixed eqs7
                                                                                                                            datatype accessor ax10
                                                                                                                            arith conflicts2
                                                                                                                            arith assert diseq1
                                                                                                                            datatype constructor ax16
                                                                                                                            num allocs2326074884
                                                                                                                            final checks8
                                                                                                                            added eqs58
                                                                                                                            del clause5
                                                                                                                            arith eq adapter10
                                                                                                                            memory25.190000
                                                                                                                            max memory25.190000
                                                                                                                            Expand
                                                                                                                            • start[0.115s]
                                                                                                                                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.<<_122| (|Ordinal.Int_113|
                                                                                                                                                      (|count_`ty_0 list list`_2866| (|get.::.1_2…
                                                                                                                                  expansions
                                                                                                                                  • unroll
                                                                                                                                    expr
                                                                                                                                    (|count_`ty_0 list list`_2866| (|get.::.1_2845| _x_2861))
                                                                                                                                    expansions
                                                                                                                                    • unroll
                                                                                                                                      expr
                                                                                                                                      (|count_`ty_0 list list`_2866| _x_2861)
                                                                                                                                      expansions
                                                                                                                                      • unsat
                                                                                                                                        (let ((a!1 (ite (>= (|count_`ty_0 list`_2868| (|get.::.0_2844| _x_2861)) 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.101s
                                                                                                                                      details
                                                                                                                                      Expand
                                                                                                                                      smt_stats
                                                                                                                                      num checks8
                                                                                                                                      arith assert lower15
                                                                                                                                      arith pivots8
                                                                                                                                      rlimit count34981
                                                                                                                                      mk clause12
                                                                                                                                      datatype occurs check29
                                                                                                                                      mk bool var87
                                                                                                                                      arith assert upper12
                                                                                                                                      datatype splits9
                                                                                                                                      decisions23
                                                                                                                                      arith add rows15
                                                                                                                                      propagations10
                                                                                                                                      conflicts11
                                                                                                                                      arith fixed eqs7
                                                                                                                                      datatype accessor ax8
                                                                                                                                      arith conflicts2
                                                                                                                                      arith assert diseq1
                                                                                                                                      datatype constructor ax15
                                                                                                                                      num allocs2379100181
                                                                                                                                      final checks8
                                                                                                                                      added eqs57
                                                                                                                                      del clause5
                                                                                                                                      arith eq adapter10
                                                                                                                                      memory25.220000
                                                                                                                                      max memory25.290000
                                                                                                                                      Expand
                                                                                                                                      • start[0.101s]
                                                                                                                                          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.<<_122| (|Ordinal.Int_113|
                                                                                                                                                                (|count_`ty_0 list list`_2899| (|get.::.1_2…
                                                                                                                                            expansions
                                                                                                                                            • unroll
                                                                                                                                              expr
                                                                                                                                              (|count_`ty_0 list list`_2899| (|get.::.1_2883| _x_2894))
                                                                                                                                              expansions
                                                                                                                                              • unroll
                                                                                                                                                expr
                                                                                                                                                (|count_`ty_0 list list`_2899| _x_2894)
                                                                                                                                                expansions
                                                                                                                                                • unsat
                                                                                                                                                  (let ((a!1 (ite (>= (|count_`ty_0 list`_2901| (|get.::.0_2882| _x_2894)) 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.374s
                                                                                                                                                details
                                                                                                                                                Expand
                                                                                                                                                smt_stats
                                                                                                                                                arith offset eqs47
                                                                                                                                                num checks26
                                                                                                                                                arith assert lower551
                                                                                                                                                arith pivots136
                                                                                                                                                rlimit count88312
                                                                                                                                                mk clause552
                                                                                                                                                datatype occurs check214
                                                                                                                                                mk bool var1532
                                                                                                                                                arith assert upper533
                                                                                                                                                datatype splits133
                                                                                                                                                decisions1028
                                                                                                                                                arith add rows764
                                                                                                                                                arith bound prop67
                                                                                                                                                propagations1391
                                                                                                                                                interface eqs13
                                                                                                                                                conflicts96
                                                                                                                                                arith fixed eqs278
                                                                                                                                                datatype accessor ax167
                                                                                                                                                minimized lits29
                                                                                                                                                arith conflicts23
                                                                                                                                                arith assert diseq162
                                                                                                                                                datatype constructor ax369
                                                                                                                                                num allocs2485614005
                                                                                                                                                final checks51
                                                                                                                                                added eqs2158
                                                                                                                                                del clause280
                                                                                                                                                arith eq adapter361
                                                                                                                                                memory26.050000
                                                                                                                                                max memory26.050000
                                                                                                                                                Expand
                                                                                                                                                • start[0.374s]
                                                                                                                                                    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`_2939|
                                                                                                                                                                   (|get.::.1_2920| (|get.::.1_2920| (|get.::.1_…
                                                                                                                                                      expansions
                                                                                                                                                      • unroll
                                                                                                                                                        expr
                                                                                                                                                        (|count_`ty_0 list list`_2939|
                                                                                                                                                          (|get.::.1_2920| (|get.::.1_2920| (|get.::.1_2920| _x_2934))))
                                                                                                                                                        expansions
                                                                                                                                                        • unroll
                                                                                                                                                          expr
                                                                                                                                                          (|count_`ty_0 list list`_2939| _x_2934)
                                                                                                                                                          expansions
                                                                                                                                                          • unroll
                                                                                                                                                            expr
                                                                                                                                                            (let ((a!1 (|get.::.1_2920| (|get.::.1_2920| (|get.::.1_2920| (|get.::.1_2920| _x_2934))))))
                                                                                                                                                              (|cou…
                                                                                                                                                            expansions
                                                                                                                                                            • unroll
                                                                                                                                                              expr
                                                                                                                                                              (let ((a!1 (|count_`ty_0 list list`_2939|
                                                                                                                                                                           (|get.::.1_2920| (|get.::.1_2920| (|get.::.1_…
                                                                                                                                                              expansions
                                                                                                                                                              • unroll
                                                                                                                                                                expr
                                                                                                                                                                (let ((a!1 (|get.::.0_2919| (|get.::.1_2920| (|get.::.1_2920| (|get.::.1_2920| _x_2934))))))
                                                                                                                                                                  (|cou…
                                                                                                                                                                expansions
                                                                                                                                                                • unroll
                                                                                                                                                                  expr
                                                                                                                                                                  (|count_`ty_0 list list`_2939| (|get.::.1_2920| _x_2934))
                                                                                                                                                                  expansions
                                                                                                                                                                  • unroll
                                                                                                                                                                    expr
                                                                                                                                                                    (|count_`ty_0 list`_2941| (|get.::.0_2919| _x_2934))
                                                                                                                                                                    expansions
                                                                                                                                                                    • unroll
                                                                                                                                                                      expr
                                                                                                                                                                      (let ((a!1 (|get.::.1_2920| (|get.::.1_2920| (|get.::.1_2920| (|get.::.1_2920| _x_2934))))))
                                                                                                                                                                        (|cou…
                                                                                                                                                                      expansions
                                                                                                                                                                      • unroll
                                                                                                                                                                        expr
                                                                                                                                                                        (let ((a!1 (|count_`ty_0 list list`_2939|
                                                                                                                                                                                     (|get.::.1_2920| (|get.::.1_2920| (|get.::.1_…
                                                                                                                                                                        expansions
                                                                                                                                                                        • unroll
                                                                                                                                                                          expr
                                                                                                                                                                          (let ((a!1 (|get.::.1_2920| (|get.::.1_2920| (|get.::.1_2920| (|get.::.1_2920| _x_2934))))))
                                                                                                                                                                            (|cou…
                                                                                                                                                                          expansions
                                                                                                                                                                          • unroll
                                                                                                                                                                            expr
                                                                                                                                                                            (|count_`ty_0 list list`_2939| (|get.::.1_2920| (|get.::.1_2920| _x_2934)))
                                                                                                                                                                            expansions
                                                                                                                                                                            • unsat
                                                                                                                                                                              (let ((a!1 (|count_`ty_0 list`_2941|
                                                                                                                                                                                           (|get.::.0_2919| (|get.::.1_2920| (|get.::.1_2920|…

                                                                                                                                                                            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.136s
                                                                                                                                                                            details
                                                                                                                                                                            Expand
                                                                                                                                                                            smt_stats
                                                                                                                                                                            num checks7
                                                                                                                                                                            arith assert lower5
                                                                                                                                                                            arith pivots3
                                                                                                                                                                            rlimit count90353
                                                                                                                                                                            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 allocs2543992572
                                                                                                                                                                            final checks6
                                                                                                                                                                            added eqs54
                                                                                                                                                                            del clause1
                                                                                                                                                                            arith eq adapter3
                                                                                                                                                                            memory25.830000
                                                                                                                                                                            max memory26.370000
                                                                                                                                                                            Expand
                                                                                                                                                                            • start[0.136s]
                                                                                                                                                                                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.<<_122| (|Ordinal.Int_113|
                                                                                                                                                                                                      (|count_`ty_0 list`_3176| (|get.::.1_3151| …
                                                                                                                                                                                  expansions
                                                                                                                                                                                  • unroll
                                                                                                                                                                                    expr
                                                                                                                                                                                    (|count_`ty_0 list`_3176| (|get.::.1_3151| l1_3169))
                                                                                                                                                                                    expansions
                                                                                                                                                                                    • unroll
                                                                                                                                                                                      expr
                                                                                                                                                                                      (|count_`ty_0 list`_3176| l1_3169)
                                                                                                                                                                                      expansions
                                                                                                                                                                                      • unsat
                                                                                                                                                                                        (let ((a!1 (= (|count_`ty_0 list`_3176| l1_3169)
                                                                                                                                                                                                      (+ 1 (|count_`ty_0 list`_3176| (|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.041s
                                                                                                                                                                                      details
                                                                                                                                                                                      Expand
                                                                                                                                                                                      smt_stats
                                                                                                                                                                                      num checks7
                                                                                                                                                                                      arith assert lower7
                                                                                                                                                                                      arith pivots5
                                                                                                                                                                                      rlimit count96068
                                                                                                                                                                                      mk clause26
                                                                                                                                                                                      datatype occurs check74
                                                                                                                                                                                      mk bool var148
                                                                                                                                                                                      arith assert upper3
                                                                                                                                                                                      datatype splits32
                                                                                                                                                                                      decisions34
                                                                                                                                                                                      arith add rows6
                                                                                                                                                                                      propagations51
                                                                                                                                                                                      conflicts11
                                                                                                                                                                                      arith fixed eqs3
                                                                                                                                                                                      datatype accessor ax26
                                                                                                                                                                                      arith conflicts1
                                                                                                                                                                                      datatype constructor ax33
                                                                                                                                                                                      num allocs2745524076
                                                                                                                                                                                      final checks12
                                                                                                                                                                                      added eqs143
                                                                                                                                                                                      del clause2
                                                                                                                                                                                      arith eq adapter3
                                                                                                                                                                                      memory25.940000
                                                                                                                                                                                      max memory28.710000
                                                                                                                                                                                      Expand
                                                                                                                                                                                      • start[0.041s]
                                                                                                                                                                                          ((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.<<_122| (|Ordinal.Int_113|
                                                                                                                                                                                                                (|count_`(ty_0 option * ty_0 option) list`_…
                                                                                                                                                                                            expansions
                                                                                                                                                                                            • unroll
                                                                                                                                                                                              expr
                                                                                                                                                                                              (|count_`(ty_0 option * ty_0 option) list`_3210| (|get.::.1_3196| y_3203))
                                                                                                                                                                                              expansions
                                                                                                                                                                                              • unroll
                                                                                                                                                                                                expr
                                                                                                                                                                                                (|count_`(ty_0 option * ty_0 option) list`_3210| y_3203)
                                                                                                                                                                                                expansions
                                                                                                                                                                                                • unsat
                                                                                                                                                                                                  (let ((a!1 (= (|count_`(ty_0 option * ty_0 option) list`_3210| y_3203)
                                                                                                                                                                                                                (+ 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.059s
                                                                                                                                                                                                details
                                                                                                                                                                                                Expand
                                                                                                                                                                                                smt_stats
                                                                                                                                                                                                num checks7
                                                                                                                                                                                                arith assert lower7
                                                                                                                                                                                                arith pivots5
                                                                                                                                                                                                rlimit count93300
                                                                                                                                                                                                mk clause23
                                                                                                                                                                                                datatype occurs check102
                                                                                                                                                                                                mk bool var158
                                                                                                                                                                                                arith assert upper3
                                                                                                                                                                                                datatype splits41
                                                                                                                                                                                                decisions38
                                                                                                                                                                                                arith add rows6
                                                                                                                                                                                                propagations54
                                                                                                                                                                                                conflicts12
                                                                                                                                                                                                arith fixed eqs3
                                                                                                                                                                                                datatype accessor ax26
                                                                                                                                                                                                arith conflicts1
                                                                                                                                                                                                datatype constructor ax34
                                                                                                                                                                                                num allocs2644636708
                                                                                                                                                                                                final checks14
                                                                                                                                                                                                added eqs141
                                                                                                                                                                                                del clause2
                                                                                                                                                                                                arith eq adapter3
                                                                                                                                                                                                memory25.930000
                                                                                                                                                                                                max memory26.370000
                                                                                                                                                                                                Expand
                                                                                                                                                                                                • start[0.059s]
                                                                                                                                                                                                    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.<<_122| (|Ordinal.Int_113|
                                                                                                                                                                                                                          (|count_`(ty_0 option * ty_0 option) list`_…
                                                                                                                                                                                                      expansions
                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                        expr
                                                                                                                                                                                                        (|count_`(ty_0 option * ty_0 option) list`_3210| (|get.::.1_3196| y_3203))
                                                                                                                                                                                                        expansions
                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                          expr
                                                                                                                                                                                                          (|count_`(ty_0 option * ty_0 option) list`_3210| y_3203)
                                                                                                                                                                                                          expansions
                                                                                                                                                                                                          • unsat
                                                                                                                                                                                                            (let ((a!1 (= (|count_`(ty_0 option * ty_0 option) list`_3210| y_3203)
                                                                                                                                                                                                                          (+ 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.064s
                                                                                                                                                                                                          details
                                                                                                                                                                                                          Expand
                                                                                                                                                                                                          smt_stats
                                                                                                                                                                                                          arith offset eqs5
                                                                                                                                                                                                          num checks12
                                                                                                                                                                                                          arith assert lower31
                                                                                                                                                                                                          arith pivots20
                                                                                                                                                                                                          rlimit count102818
                                                                                                                                                                                                          mk clause54
                                                                                                                                                                                                          datatype occurs check76
                                                                                                                                                                                                          mk bool var234
                                                                                                                                                                                                          arith assert upper27
                                                                                                                                                                                                          datatype splits27
                                                                                                                                                                                                          decisions86
                                                                                                                                                                                                          arith add rows40
                                                                                                                                                                                                          propagations51
                                                                                                                                                                                                          conflicts16
                                                                                                                                                                                                          arith fixed eqs11
                                                                                                                                                                                                          datatype accessor ax31
                                                                                                                                                                                                          minimized lits2
                                                                                                                                                                                                          arith conflicts6
                                                                                                                                                                                                          arith assert diseq1
                                                                                                                                                                                                          datatype constructor ax51
                                                                                                                                                                                                          num allocs2805051803
                                                                                                                                                                                                          final checks11
                                                                                                                                                                                                          added eqs200
                                                                                                                                                                                                          del clause21
                                                                                                                                                                                                          arith eq adapter20
                                                                                                                                                                                                          memory28.820000
                                                                                                                                                                                                          max memory28.820000
                                                                                                                                                                                                          Expand
                                                                                                                                                                                                          • start[0.064s]
                                                                                                                                                                                                              match_cols (zip (List.hd …).0 (List.hd …).1)
                                                                                                                                                                                                              && not (… = [])
                                                                                                                                                                                                                 && Ordinal.count … >= 0 && Ordinal.count (List.tl …) >= 0
                                                                                                                                                                                                              ==> not
                                                                                                                                                                                                                  (match_cols (zip (List.hd (List.tl …)).0 (List.hd (List.tl …)).1)
                                                                                                                                                                                                                   && not (List.tl … = []))
                                                                                                                                                                                                                  || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl …)))
                                                                                                                                                                                                                     (Ordinal.Int (Ordinal.count …))
                                                                                                                                                                                                          • simplify
                                                                                                                                                                                                            into
                                                                                                                                                                                                            (not
                                                                                                                                                                                                             (((match_cols (zip (List.hd …).0 (List.hd …).1) && not (… = []))
                                                                                                                                                                                                               && Ordinal.count … >= 0)
                                                                                                                                                                                                              && Ordinal.count (List.tl …) >= 0)
                                                                                                                                                                                                             || not
                                                                                                                                                                                                                (match_cols (zip (List.hd (List.tl …)).0 (List.hd (List.tl …)).1)
                                                                                                                                                                                                                 && not (List.tl … = [])))
                                                                                                                                                                                                            || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl …)))
                                                                                                                                                                                                               (Ordinal.Int (Ordinal.count …))
                                                                                                                                                                                                            expansions
                                                                                                                                                                                                            []
                                                                                                                                                                                                            rewrite_steps
                                                                                                                                                                                                              forward_chaining
                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                expr
                                                                                                                                                                                                                (|Ordinal.<<_122| (|Ordinal.Int_113|
                                                                                                                                                                                                                                    (|count_`(ty_0 option list * ty_0 option li…
                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                  (zip_3251 (|tuple_get.0_3234| (|get.::.0_3237| (|get.::.1_3238| x_3264)))
                                                                                                                                                                                                                            (|tuple_get.1_32…
                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                    (let ((a!1 (zip_3251 (|tuple_get.0_3234|
                                                                                                                                                                                                                                           (|get.::.0_3237| (|get.::.1_3238| x_…
                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                      (|count_`(ty_0 option list * ty_0 option list) list`_3269|
                                                                                                                                                                                                                        (|get.::.1_3238| x_3264))
                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                        (|count_`(ty_0 option list * ty_0 option list) list`_3269| x_3264)
                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                        • unsat
                                                                                                                                                                                                                          (let ((a!1 (>= (|count_`ty_0 option list`_3273|
                                                                                                                                                                                                                                           (|tuple_get.0_3234| (|get.::.0_3237…

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