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.079s
details
Expand
smt_stats
num checks7
arith assert lower5
arith pivots3
rlimit count1821
mk clause3
datatype occurs check21
mk bool var50
arith assert upper5
datatype splits3
decisions7
arith add rows7
propagations2
conflicts7
arith fixed eqs4
datatype accessor ax5
arith conflicts1
datatype constructor ax8
num allocs1319288708
final checks6
added eqs33
del clause1
arith eq adapter3
memory25.080000
max memory27.740000
Expand
  • start[0.079s]
      not (_x = []) && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
      ==> List.tl _x = []
          || Ordinal.Int (Ordinal.count (List.tl _x)) Ordinal.<<
             Ordinal.Int (Ordinal.count _x)
  • simplify
    into
    (not
     ((not (_x = []) && Ordinal.count _x >= 0) && Ordinal.count (List.tl _x) >= 0)
     || List.tl _x = [])
    || Ordinal.Int (Ordinal.count (List.tl _x)) Ordinal.<<
       Ordinal.Int (Ordinal.count _x)
    expansions
    []
    rewrite_steps
      forward_chaining
      • unroll
        expr
        (|Ordinal.<<_121| (|Ordinal.Int_112|
                            (|count_`ty_0 list`_2452| (|get.::.1_2439| …
        expansions
        • unroll
          expr
          (|count_`ty_0 list`_2452| (|get.::.1_2439| _x_2443))
          expansions
          • unroll
            expr
            (|count_`ty_0 list`_2452| _x_2443)
            expansions
            • unsat
              (let ((a!1 (= (|count_`ty_0 list`_2452| _x_2443)
                            (+ 1 (|count_`ty_0 list`_2452| (|get.…

            Rows, columns, blocks

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

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

            Termination proof

            call `transpose3 (List.tl _x)` from `transpose3 _x`
            originaltranspose3 _x
            subtranspose3 (List.tl _x)
            original ordinalOrdinal.Int (Ordinal.count _x)
            sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
            path[List.hd _x = [] && _x <> [] && not (_x = [])]
            proof
            detailed proof
            ground_instances3
            definitions0
            inductions0
            search_time
            0.072s
            details
            Expand
            smt_stats
            num checks8
            arith assert lower13
            arith pivots7
            rlimit count8181
            mk clause40
            datatype occurs check32
            mk bool var125
            arith assert upper15
            datatype splits10
            decisions28
            arith add rows14
            propagations74
            conflicts12
            arith fixed eqs7
            datatype accessor ax14
            arith conflicts2
            arith assert diseq1
            datatype constructor ax22
            num allocs1428835298
            final checks9
            added eqs100
            del clause7
            arith eq adapter11
            memory28.150000
            max memory28.150000
            Expand
            • start[0.072s]
                (List.hd _x = [] && _x <> [])
                && not (_x = [])
                   && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                ==> not
                    ((List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                     && not (List.tl _x = []))
                    && not
                       (not (List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                        && not (List.tl _x = []))
                    || Ordinal.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                       Ordinal.Int (Ordinal.count _x)
            • simplify
              into
              (not
               ((((List.hd _x = [] && _x <> []) && not (_x = [])) && Ordinal.count _x >= 0)
                && Ordinal.count (List.tl _x) >= 0)
               || not
                  ((List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                   && not (List.tl _x = []))
                  && not
                     (not (List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                      && not (List.tl _x = [])))
              || Ordinal.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                 Ordinal.Int (Ordinal.count _x)
              expansions
              []
              rewrite_steps
                forward_chaining
                • unroll
                  expr
                  (|Ordinal.<<_121| (|Ordinal.Int_112|
                                      (|count_`ty_0 list list`_2484| (|get.::.1_2…
                  expansions
                  • unroll
                    expr
                    (|count_`ty_0 list list`_2484| (|get.::.1_2471| _x_2477))
                    expansions
                    • unroll
                      expr
                      (|count_`ty_0 list list`_2484| _x_2477)
                      expansions
                      • unsat
                        (let ((a!1 (+ 1
                                      (|count_`ty_0 list list`_2484| (|get.::.1_2471| _x_2477))
                                    …

                      call `transpose3 (List.tl _x)` from `transpose3 _x`
                      originaltranspose3 _x
                      subtranspose3 (List.tl _x)
                      original ordinalOrdinal.Int (Ordinal.count _x)
                      sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
                      path[not (List.hd _x = [] && _x <> []) && not (_x = [])]
                      proof
                      detailed proof
                      ground_instances3
                      definitions0
                      inductions0
                      search_time
                      0.121s
                      details
                      Expand
                      smt_stats
                      num checks8
                      arith assert lower11
                      arith pivots9
                      rlimit count5144
                      mk clause34
                      datatype occurs check67
                      mk bool var145
                      arith assert upper10
                      datatype splits26
                      decisions39
                      arith add rows16
                      propagations48
                      conflicts12
                      arith fixed eqs5
                      datatype accessor ax17
                      arith conflicts2
                      datatype constructor ax31
                      num allocs1389953727
                      final checks15
                      added eqs118
                      del clause6
                      arith eq adapter7
                      memory25.360000
                      max memory27.740000
                      Expand
                      • start[0.121s]
                          not (List.hd _x = [] && _x <> [])
                          && not (_x = [])
                             && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                          ==> not
                              ((List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                               && not (List.tl _x = []))
                              && not
                                 (not (List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                  && not (List.tl _x = []))
                              || Ordinal.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                                 Ordinal.Int (Ordinal.count _x)
                      • simplify
                        into
                        (not
                         (((not (List.hd _x = [] && _x <> []) && not (_x = []))
                           && Ordinal.count _x >= 0)
                          && Ordinal.count (List.tl _x) >= 0)
                         || not
                            ((List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                             && not (List.tl _x = []))
                            && not
                               (not (List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                && not (List.tl _x = [])))
                        || Ordinal.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                           Ordinal.Int (Ordinal.count _x)
                        expansions
                        []
                        rewrite_steps
                          forward_chaining
                          • unroll
                            expr
                            (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                (|count_`ty_0 list list`_2484| (|get.::.1_2…
                            expansions
                            • unroll
                              expr
                              (|count_`ty_0 list list`_2484| (|get.::.1_2471| _x_2477))
                              expansions
                              • unroll
                                expr
                                (|count_`ty_0 list list`_2484| _x_2477)
                                expansions
                                • unsat
                                  (let ((a!1 (ite (>= (|count_`ty_0 list`_2486| (|get.::.0_2470| _x_2477)) 0)
                                                  (|count_…

                                termination proof

                                Termination proof

                                call `get_heads (List.tl _x)` from `get_heads _x`
                                originalget_heads _x
                                subget_heads (List.tl _x)
                                original ordinalOrdinal.Int (Ordinal.count _x)
                                sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
                                path[List.hd _x = [] && _x <> [] && not (_x = [])]
                                proof
                                detailed proof
                                ground_instances3
                                definitions0
                                inductions0
                                search_time
                                0.103s
                                details
                                Expand
                                smt_stats
                                num checks8
                                arith assert lower14
                                arith pivots7
                                rlimit count14602
                                mk clause40
                                datatype occurs check32
                                mk bool var125
                                arith assert upper14
                                datatype splits10
                                decisions28
                                arith add rows14
                                propagations74
                                conflicts12
                                arith fixed eqs7
                                datatype accessor ax14
                                arith conflicts2
                                arith assert diseq1
                                datatype constructor ax22
                                num allocs1545304302
                                final checks9
                                added eqs100
                                del clause7
                                arith eq adapter11
                                memory31.170000
                                max memory31.170000
                                Expand
                                • start[0.103s]
                                    (List.hd _x = [] && _x <> [])
                                    && not (_x = [])
                                       && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                                    ==> not
                                        ((List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                         && not (List.tl _x = []))
                                        && not
                                           (not (List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                            && not (List.tl _x = []))
                                        || Ordinal.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                                           Ordinal.Int (Ordinal.count _x)
                                • simplify
                                  into
                                  (not
                                   ((((List.hd _x = [] && _x <> []) && not (_x = [])) && Ordinal.count _x >= 0)
                                    && Ordinal.count (List.tl _x) >= 0)
                                   || not
                                      ((List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                       && not (List.tl _x = []))
                                      && not
                                         (not (List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                          && not (List.tl _x = [])))
                                  || Ordinal.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                                     Ordinal.Int (Ordinal.count _x)
                                  expansions
                                  []
                                  rewrite_steps
                                    forward_chaining
                                    • unroll
                                      expr
                                      (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                          (|count_`ty_0 list list`_2517| (|get.::.1_2…
                                      expansions
                                      • unroll
                                        expr
                                        (|count_`ty_0 list list`_2517| (|get.::.1_2504| _x_2510))
                                        expansions
                                        • unroll
                                          expr
                                          (|count_`ty_0 list list`_2517| _x_2510)
                                          expansions
                                          • unsat
                                            (let ((a!1 (+ 1
                                                          (|count_`ty_0 list list`_2517| (|get.::.1_2504| _x_2510))
                                                        …

                                          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.097s
                                          details
                                          Expand
                                          smt_stats
                                          num checks8
                                          arith assert lower12
                                          arith pivots9
                                          rlimit count11565
                                          mk clause34
                                          datatype occurs check71
                                          mk bool var150
                                          arith assert upper9
                                          datatype splits28
                                          decisions43
                                          arith add rows16
                                          propagations51
                                          conflicts13
                                          arith fixed eqs5
                                          datatype accessor ax18
                                          arith conflicts2
                                          datatype constructor ax32
                                          num allocs1503238949
                                          final checks16
                                          added eqs124
                                          del clause6
                                          arith eq adapter7
                                          memory28.370000
                                          max memory28.370000
                                          Expand
                                          • start[0.097s]
                                              not (List.hd _x = [] && _x <> [])
                                              && not (_x = [])
                                                 && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                                              ==> not
                                                  ((List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                                   && not (List.tl _x = []))
                                                  && not
                                                     (not (List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                                      && not (List.tl _x = []))
                                                  || Ordinal.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                                                     Ordinal.Int (Ordinal.count _x)
                                          • simplify
                                            into
                                            (not
                                             (((not (List.hd _x = [] && _x <> []) && not (_x = []))
                                               && Ordinal.count _x >= 0)
                                              && Ordinal.count (List.tl _x) >= 0)
                                             || not
                                                ((List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                                 && not (List.tl _x = []))
                                                && not
                                                   (not (List.hd (List.tl _x) = [] && (List.tl _x) <> [])
                                                    && not (List.tl _x = [])))
                                            || Ordinal.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                                               Ordinal.Int (Ordinal.count _x)
                                            expansions
                                            []
                                            rewrite_steps
                                              forward_chaining
                                              • unroll
                                                expr
                                                (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                                    (|count_`ty_0 list list`_2517| (|get.::.1_2…
                                                expansions
                                                • unroll
                                                  expr
                                                  (|count_`ty_0 list list`_2517| (|get.::.1_2504| _x_2510))
                                                  expansions
                                                  • unroll
                                                    expr
                                                    (|count_`ty_0 list list`_2517| _x_2510)
                                                    expansions
                                                    • unsat
                                                      (let ((a!1 (ite (>= (|count_`ty_0 list`_2519| (|get.::.0_2503| _x_2510)) 0)
                                                                      (|count_…

                                                    termination proof

                                                    Termination proof

                                                    call `transpose ((List.tl (List.hd l)) :: (transpose3 (List.tl l)))` from `transpose l`
                                                    originaltranspose l
                                                    subtranspose ((List.tl (List.hd l)) :: (transpose3 (List.tl l)))
                                                    original ordinalOrdinal.Int (if measure_transpose l >= 0 then measure_transpose l else 0)
                                                    sub ordinalOrdinal.Int (if measure_transpose ((List.tl (List.hd l)) :: (transpose3 (List.tl l))) >= 0 then measure_transpose ((List.tl (List.hd l)) :: (transpose3 (List.tl l))) else 0)
                                                    path[not (List.hd l = [] && l <> []) && not (l = [])]
                                                    proof
                                                    detailed proof
                                                    ground_instances3
                                                    definitions0
                                                    inductions0
                                                    search_time
                                                    0.055s
                                                    details
                                                    Expand
                                                    smt_stats
                                                    num checks7
                                                    arith assert lower6
                                                    arith pivots2
                                                    rlimit count16612
                                                    mk clause4
                                                    datatype occurs check39
                                                    mk bool var59
                                                    arith assert upper2
                                                    datatype splits6
                                                    decisions11
                                                    arith add rows2
                                                    propagations3
                                                    conflicts8
                                                    arith fixed eqs1
                                                    datatype accessor ax7
                                                    arith conflicts1
                                                    datatype constructor ax14
                                                    num allocs1652445656
                                                    final checks8
                                                    added eqs43
                                                    del clause4
                                                    arith eq adapter2
                                                    memory28.360000
                                                    max memory31.170000
                                                    Expand
                                                    • start[0.055s]
                                                        not (List.hd l = [] && l <> [])
                                                        && not (l = [])
                                                           && (if (if l = [] then 0 else List.length (List.hd l)) >= 0
                                                               then if l = [] then 0 else List.length (List.hd l) else 0)
                                                              >= 0
                                                              && (if (if (List.tl (List.hd l)) :: (transpose3 …) = [] then 0
                                                                      else List.length …)
                                                                     >= 0
                                                                  then
                                                                    if (List.tl (List.hd l)) :: (transpose3 …) = [] then 0
                                                                    else List.length …
                                                                  else 0)
                                                                 >= 0
                                                        ==> not
                                                            (not (List.tl (List.hd l) = [] && true)
                                                             && not ((List.tl (List.hd l)) :: (transpose3 …) = []))
                                                            || Ordinal.Int
                                                               (if (if (List.tl (List.hd l)) :: (transpose3 …) = [] then 0
                                                                    else List.length …)
                                                                   >= 0
                                                                then
                                                                  if (List.tl (List.hd l)) :: (transpose3 …) = [] then 0
                                                                  else List.length …
                                                                else 0)
                                                               Ordinal.<<
                                                               Ordinal.Int
                                                               (if (if l = [] then 0 else List.length (List.hd l)) >= 0
                                                                then if l = [] then 0 else List.length (List.hd l) else 0)
                                                    • simplify
                                                      into
                                                      (not
                                                       (((not (List.hd l = [] && l <> []) && not (l = []))
                                                         && (if (if l = [] then 0 else List.length (List.hd l)) >= 0
                                                             then if l = [] then 0 else List.length (List.hd l) else 0)
                                                            >= 0)
                                                        && (if List.length (List.tl (List.hd l)) >= 0
                                                            then List.length (List.tl (List.hd l)) else 0)
                                                           >= 0)
                                                       || List.tl (List.hd l) = [])
                                                      || Ordinal.Int
                                                         (if List.length (List.tl (List.hd l)) >= 0
                                                          then List.length (List.tl (List.hd l)) else 0)
                                                         Ordinal.<<
                                                         Ordinal.Int
                                                         (if (if l = [] then 0 else List.length (List.hd l)) >= 0
                                                          then if l = [] then 0 else List.length (List.hd l) else 0)
                                                      expansions
                                                      []
                                                      rewrite_steps
                                                        forward_chaining
                                                        • unroll
                                                          expr
                                                          (let ((a!1 (>= (|List.length_2594| (|get.::.1_2568| (|get.::.0_2570| l_2587)))
                                                                         0))
                                                            …
                                                          expansions
                                                          • unroll
                                                            expr
                                                            (|List.length_2594| (|get.::.1_2568| (|get.::.0_2570| l_2587)))
                                                            expansions
                                                            • unroll
                                                              expr
                                                              (|List.length_2594| (|get.::.0_2570| l_2587))
                                                              expansions
                                                              • unsat
                                                                (let ((a!1 (+ 1 (|List.length_2594| (|get.::.1_2568| (|get.::.0_2570| l_2587)))))
                                                                      (a!7 (not (a…

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

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

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

                                                              Termination proof

                                                              call `take (Destruct(S, 0, x)) (List.tl l)` from `take x l`
                                                              originaltake x l
                                                              subtake (Destruct(S, 0, x)) (List.tl l)
                                                              original ordinalOrdinal.Int (Ordinal.count x)
                                                              sub ordinalOrdinal.Int (Ordinal.count (Destruct(S, 0, x)))
                                                              path[not (l = []) && not (x = Z)]
                                                              proof
                                                              detailed proof
                                                              ground_instances3
                                                              definitions0
                                                              inductions0
                                                              search_time
                                                              0.065s
                                                              details
                                                              Expand
                                                              smt_stats
                                                              num checks7
                                                              arith assert lower5
                                                              arith pivots3
                                                              rlimit count18651
                                                              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 allocs1696984548
                                                              final checks6
                                                              added eqs52
                                                              del clause1
                                                              arith eq adapter3
                                                              memory28.440000
                                                              max memory31.170000
                                                              Expand
                                                              • start[0.065s]
                                                                  not (l = [])
                                                                  && not (x = Z)
                                                                     && Ordinal.count x >= 0 && Ordinal.count (Destruct(S, 0, x)) >= 0
                                                                  ==> not (not (List.tl l = []) && not (Destruct(S, 0, x) = Z))
                                                                      || Ordinal.Int (Ordinal.count (Destruct(S, 0, x))) Ordinal.<<
                                                                         Ordinal.Int (Ordinal.count x)
                                                              • simplify
                                                                into
                                                                (not
                                                                 (((not (l = []) && not (x = Z)) && Ordinal.count x >= 0)
                                                                  && Ordinal.count (Destruct(S, 0, x)) >= 0)
                                                                 || not (not (List.tl l = []) && not (Destruct(S, 0, x) = Z)))
                                                                || Ordinal.Int (Ordinal.count (Destruct(S, 0, x))) Ordinal.<<
                                                                   Ordinal.Int (Ordinal.count x)
                                                                expansions
                                                                []
                                                                rewrite_steps
                                                                  forward_chaining
                                                                  • unroll
                                                                    expr
                                                                    (|Ordinal.<<_121| (|Ordinal.Int_112| (count_nat_2628 (|get.S.0_2429| x_2621)))
                                                                                      (|O…
                                                                    expansions
                                                                    • unroll
                                                                      expr
                                                                      (count_nat_2628 (|get.S.0_2429| x_2621))
                                                                      expansions
                                                                      • unroll
                                                                        expr
                                                                        (count_nat_2628 x_2621)
                                                                        expansions
                                                                        • unsat
                                                                          (let ((a!1 (= (+ 1 (count_nat_2628 (|get.S.0_2429| x_2621)))
                                                                                        (count_nat_2628 x_2621)))…

                                                                        termination proof

                                                                        Termination proof

                                                                        call `drop (Destruct(S, 0, x)) (List.tl y)` from `drop x y`
                                                                        originaldrop x y
                                                                        subdrop (Destruct(S, 0, x)) (List.tl y)
                                                                        original ordinalOrdinal.Int (Ordinal.count x)
                                                                        sub ordinalOrdinal.Int (Ordinal.count (Destruct(S, 0, x)))
                                                                        path[not (y = []) && not (x = Z)]
                                                                        proof
                                                                        detailed proof
                                                                        ground_instances3
                                                                        definitions0
                                                                        inductions0
                                                                        search_time
                                                                        0.101s
                                                                        details
                                                                        Expand
                                                                        smt_stats
                                                                        num checks7
                                                                        arith assert lower6
                                                                        arith pivots3
                                                                        rlimit count20706
                                                                        mk clause3
                                                                        datatype occurs check30
                                                                        mk bool var68
                                                                        arith assert upper4
                                                                        datatype splits6
                                                                        decisions15
                                                                        arith add rows7
                                                                        propagations1
                                                                        conflicts11
                                                                        arith fixed eqs4
                                                                        datatype accessor ax8
                                                                        arith conflicts1
                                                                        datatype constructor ax17
                                                                        num allocs1778024387
                                                                        final checks6
                                                                        added eqs55
                                                                        del clause1
                                                                        arith eq adapter3
                                                                        memory28.520000
                                                                        max memory31.280000
                                                                        Expand
                                                                        • start[0.101s]
                                                                            not (y = [])
                                                                            && not (x = Z)
                                                                               && Ordinal.count x >= 0 && Ordinal.count (Destruct(S, 0, x)) >= 0
                                                                            ==> not (not (List.tl y = []) && not (Destruct(S, 0, x) = Z))
                                                                                || Ordinal.Int (Ordinal.count (Destruct(S, 0, x))) Ordinal.<<
                                                                                   Ordinal.Int (Ordinal.count x)
                                                                        • simplify
                                                                          into
                                                                          (not
                                                                           (((not (y = []) && not (x = Z)) && Ordinal.count x >= 0)
                                                                            && Ordinal.count (Destruct(S, 0, x)) >= 0)
                                                                           || not (not (List.tl y = []) && not (Destruct(S, 0, x) = Z)))
                                                                          || Ordinal.Int (Ordinal.count (Destruct(S, 0, x))) Ordinal.<<
                                                                             Ordinal.Int (Ordinal.count x)
                                                                          expansions
                                                                          []
                                                                          rewrite_steps
                                                                            forward_chaining
                                                                            • unroll
                                                                              expr
                                                                              (|Ordinal.<<_121| (|Ordinal.Int_112| (count_nat_2655 (|get.S.0_2429| x_2648)))
                                                                                                (|O…
                                                                              expansions
                                                                              • unroll
                                                                                expr
                                                                                (count_nat_2655 (|get.S.0_2429| x_2648))
                                                                                expansions
                                                                                • unroll
                                                                                  expr
                                                                                  (count_nat_2655 x_2648)
                                                                                  expansions
                                                                                  • unsat
                                                                                    (let ((a!1 (= (+ 1 (count_nat_2655 (|get.S.0_2429| x_2648)))
                                                                                                  (count_nat_2655 x_2648)))…

                                                                                  termination proof

                                                                                  Termination proof

                                                                                  call `elem x (List.tl y)` from `elem x y`
                                                                                  originalelem x y
                                                                                  subelem x (List.tl y)
                                                                                  original ordinalOrdinal.Int (Ordinal.count y)
                                                                                  sub ordinalOrdinal.Int (Ordinal.count (List.tl y))
                                                                                  path[not (x = List.hd y) && not (y = [])]
                                                                                  proof
                                                                                  detailed proof
                                                                                  ground_instances3
                                                                                  definitions0
                                                                                  inductions0
                                                                                  search_time
                                                                                  0.120s
                                                                                  details
                                                                                  Expand
                                                                                  smt_stats
                                                                                  num checks7
                                                                                  arith assert lower6
                                                                                  arith pivots3
                                                                                  rlimit count22622
                                                                                  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 allocs1823038075
                                                                                  final checks5
                                                                                  added eqs30
                                                                                  del clause1
                                                                                  arith eq adapter3
                                                                                  memory31.290000
                                                                                  max memory31.290000
                                                                                  Expand
                                                                                  • start[0.120s]
                                                                                      not (x = List.hd y)
                                                                                      && not (y = []) && Ordinal.count y >= 0 && Ordinal.count (List.tl y) >= 0
                                                                                      ==> not (not (x = List.hd (List.tl y)) && not (List.tl y = []))
                                                                                          || Ordinal.Int (Ordinal.count (List.tl y)) Ordinal.<<
                                                                                             Ordinal.Int (Ordinal.count y)
                                                                                  • simplify
                                                                                    into
                                                                                    (not
                                                                                     (((not (x = List.hd y) && not (y = [])) && Ordinal.count y >= 0)
                                                                                      && Ordinal.count (List.tl y) >= 0)
                                                                                     || not (not (x = List.hd (List.tl y)) && not (List.tl y = [])))
                                                                                    || Ordinal.Int (Ordinal.count (List.tl y)) Ordinal.<<
                                                                                       Ordinal.Int (Ordinal.count y)
                                                                                    expansions
                                                                                    []
                                                                                    rewrite_steps
                                                                                      forward_chaining
                                                                                      • unroll
                                                                                        expr
                                                                                        (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                                                                            (|count_`ty_0 list`_2682| (|get.::.1_2669| …
                                                                                        expansions
                                                                                        • unroll
                                                                                          expr
                                                                                          (|count_`ty_0 list`_2682| (|get.::.1_2669| y_2676))
                                                                                          expansions
                                                                                          • unroll
                                                                                            expr
                                                                                            (|count_`ty_0 list`_2682| y_2676)
                                                                                            expansions
                                                                                            • unsat
                                                                                              (let ((a!1 (= (|count_`ty_0 list`_2682| y_2676)
                                                                                                            (+ 1 (|count_`ty_0 list`_2682| (|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.137s
                                                                                            details
                                                                                            Expand
                                                                                            smt_stats
                                                                                            num checks9
                                                                                            arith assert lower6
                                                                                            arith pivots4
                                                                                            rlimit count25007
                                                                                            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 allocs1904048909
                                                                                            final checks6
                                                                                            added eqs37
                                                                                            del clause1
                                                                                            arith eq adapter3
                                                                                            memory31.310000
                                                                                            max memory31.310000
                                                                                            Expand
                                                                                            • start[0.137s]
                                                                                                not (elem (List.hd x) (List.tl x))
                                                                                                && not (x = []) && Ordinal.count x >= 0 && Ordinal.count (List.tl x) >= 0
                                                                                                ==> not
                                                                                                    (not (elem (List.hd (List.tl x)) (List.tl (List.tl x)))
                                                                                                     && not (List.tl x = []))
                                                                                                    || Ordinal.Int (Ordinal.count (List.tl x)) Ordinal.<<
                                                                                                       Ordinal.Int (Ordinal.count x)
                                                                                            • simplify
                                                                                              into
                                                                                              (not
                                                                                               (((not (elem (List.hd x) (List.tl x)) && not (x = []))
                                                                                                 && Ordinal.count x >= 0)
                                                                                                && Ordinal.count (List.tl x) >= 0)
                                                                                               || not
                                                                                                  (not (elem (List.hd (List.tl x)) (List.tl (List.tl x)))
                                                                                                   && not (List.tl x = [])))
                                                                                              || Ordinal.Int (Ordinal.count (List.tl x)) Ordinal.<<
                                                                                                 Ordinal.Int (Ordinal.count x)
                                                                                              expansions
                                                                                              []
                                                                                              rewrite_steps
                                                                                                forward_chaining
                                                                                                • unroll
                                                                                                  expr
                                                                                                  (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                                                                                      (|count_`ty_0 list`_2709| (|get.::.1_2694| …
                                                                                                  expansions
                                                                                                  • unroll
                                                                                                    expr
                                                                                                    (elem_2699 (|get.::.0_2693| (|get.::.1_2694| x_2704))
                                                                                                               (|get.::.1_2694| (|get.::.1_2694| x…
                                                                                                    expansions
                                                                                                    • unroll
                                                                                                      expr
                                                                                                      (|count_`ty_0 list`_2709| (|get.::.1_2694| x_2704))
                                                                                                      expansions
                                                                                                      • unroll
                                                                                                        expr
                                                                                                        (|count_`ty_0 list`_2709| x_2704)
                                                                                                        expansions
                                                                                                        • unsat
                                                                                                          (let ((a!1 (= (|count_`ty_0 list`_2709| x_2704)
                                                                                                                        (+ 1 (|count_`ty_0 list`_2709| (|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
                                                                                                        definitions2
                                                                                                        inductions0
                                                                                                        search_time
                                                                                                        0.144s
                                                                                                        details
                                                                                                        Expand
                                                                                                        smt_stats
                                                                                                        num checks7
                                                                                                        arith assert lower5
                                                                                                        arith pivots3
                                                                                                        rlimit count26975
                                                                                                        mk clause3
                                                                                                        datatype occurs check29
                                                                                                        mk bool var64
                                                                                                        arith assert upper5
                                                                                                        datatype splits9
                                                                                                        decisions15
                                                                                                        arith add rows7
                                                                                                        propagations2
                                                                                                        conflicts8
                                                                                                        arith fixed eqs4
                                                                                                        datatype accessor ax8
                                                                                                        arith conflicts1
                                                                                                        datatype constructor ax15
                                                                                                        num allocs1989298578
                                                                                                        final checks8
                                                                                                        added eqs48
                                                                                                        del clause1
                                                                                                        arith eq adapter3
                                                                                                        memory31.330000
                                                                                                        max memory31.400000
                                                                                                        Expand
                                                                                                        • start[0.144s]
                                                                                                            not (l = []) && Ordinal.count l >= 0 && Ordinal.count (List.tl l) >= 0
                                                                                                            ==> List.tl l = []
                                                                                                                || Ordinal.Int (Ordinal.count (List.tl l)) Ordinal.<<
                                                                                                                   Ordinal.Int (Ordinal.count l)
                                                                                                        • simplify
                                                                                                          into
                                                                                                          (not
                                                                                                           ((not (l = []) && Ordinal.count l >= 0) && Ordinal.count (List.tl l) >= 0)
                                                                                                           || List.tl l = [])
                                                                                                          || Ordinal.Int (Ordinal.count (List.tl l)) Ordinal.<<
                                                                                                             Ordinal.Int (Ordinal.count l)
                                                                                                          expansions
                                                                                                          []
                                                                                                          rewrite_steps
                                                                                                            forward_chaining
                                                                                                            • unroll
                                                                                                              expr
                                                                                                              (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                                                                                                  (|count_`ty_0 option list`_2741| (|get.::.1…
                                                                                                              expansions
                                                                                                              • unroll
                                                                                                                expr
                                                                                                                (|count_`ty_0 option list`_2741| (|get.::.1_2726| l_2736))
                                                                                                                expansions
                                                                                                                Ordinal.count
                                                                                                              • unroll
                                                                                                                expr
                                                                                                                (|count_`ty_0 option list`_2741| l_2736)
                                                                                                                expansions
                                                                                                                Ordinal.count
                                                                                                              • unsat
                                                                                                                (let ((a!1 (= (|count_`ty_0 option list`_2741| l_2736)
                                                                                                                              (+ 2 (|count_`ty_0 option list`…

                                                                                                              termination proof

                                                                                                              Termination proof

                                                                                                              call `blocks_3_34 (List.tl _x)` from `blocks_3_34 _x`
                                                                                                              originalblocks_3_34 _x
                                                                                                              subblocks_3_34 (List.tl _x)
                                                                                                              original ordinalOrdinal.Int (Ordinal.count _x)
                                                                                                              sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
                                                                                                              path[not (_x = [])]
                                                                                                              proof
                                                                                                              detailed proof
                                                                                                              ground_instances3
                                                                                                              definitions0
                                                                                                              inductions0
                                                                                                              search_time
                                                                                                              0.083s
                                                                                                              details
                                                                                                              Expand
                                                                                                              smt_stats
                                                                                                              num checks8
                                                                                                              arith assert lower15
                                                                                                              arith pivots8
                                                                                                              rlimit count29572
                                                                                                              mk clause12
                                                                                                              datatype occurs check29
                                                                                                              mk bool var87
                                                                                                              arith assert upper12
                                                                                                              datatype splits9
                                                                                                              decisions24
                                                                                                              arith add rows12
                                                                                                              propagations10
                                                                                                              conflicts10
                                                                                                              arith fixed eqs7
                                                                                                              datatype accessor ax10
                                                                                                              arith conflicts2
                                                                                                              arith assert diseq1
                                                                                                              datatype constructor ax16
                                                                                                              num allocs2038265158
                                                                                                              final checks8
                                                                                                              added eqs58
                                                                                                              del clause5
                                                                                                              arith eq adapter10
                                                                                                              memory34.150000
                                                                                                              max memory34.150000
                                                                                                              Expand
                                                                                                              • start[0.083s]
                                                                                                                  not (_x = []) && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                                                                                                                  ==> List.tl _x = []
                                                                                                                      || Ordinal.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                                                                                                                         Ordinal.Int (Ordinal.count _x)
                                                                                                              • simplify
                                                                                                                into
                                                                                                                (not
                                                                                                                 ((not (_x = []) && Ordinal.count _x >= 0) && Ordinal.count (List.tl _x) >= 0)
                                                                                                                 || List.tl _x = [])
                                                                                                                || Ordinal.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                                                                                                                   Ordinal.Int (Ordinal.count _x)
                                                                                                                expansions
                                                                                                                []
                                                                                                                rewrite_steps
                                                                                                                  forward_chaining
                                                                                                                  • unroll
                                                                                                                    expr
                                                                                                                    (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                                                                                                        (|count_`ty_0 list list`_2803| (|get.::.1_2…
                                                                                                                    expansions
                                                                                                                    • unroll
                                                                                                                      expr
                                                                                                                      (|count_`ty_0 list list`_2803| (|get.::.1_2788| _x_2798))
                                                                                                                      expansions
                                                                                                                      • unroll
                                                                                                                        expr
                                                                                                                        (|count_`ty_0 list list`_2803| _x_2798)
                                                                                                                        expansions
                                                                                                                        • unsat
                                                                                                                          (let ((a!1 (ite (>= (|count_`ty_0 list`_2805| (|get.::.0_2787| _x_2798)) 0)
                                                                                                                                          (|count_…

                                                                                                                        termination proof

                                                                                                                        Termination proof

                                                                                                                        call `blocks_3_33 (List.tl _x)` from `blocks_3_33 _x`
                                                                                                                        originalblocks_3_33 _x
                                                                                                                        subblocks_3_33 (List.tl _x)
                                                                                                                        original ordinalOrdinal.Int (Ordinal.count _x)
                                                                                                                        sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
                                                                                                                        path[not (_x = [])]
                                                                                                                        proof
                                                                                                                        detailed proof
                                                                                                                        ground_instances3
                                                                                                                        definitions0
                                                                                                                        inductions0
                                                                                                                        search_time
                                                                                                                        0.058s
                                                                                                                        details
                                                                                                                        Expand
                                                                                                                        smt_stats
                                                                                                                        num checks8
                                                                                                                        arith assert lower15
                                                                                                                        arith pivots8
                                                                                                                        rlimit count32138
                                                                                                                        mk clause12
                                                                                                                        datatype occurs check37
                                                                                                                        mk bool var84
                                                                                                                        arith assert upper12
                                                                                                                        datatype splits9
                                                                                                                        decisions22
                                                                                                                        arith add rows12
                                                                                                                        propagations10
                                                                                                                        conflicts9
                                                                                                                        arith fixed eqs7
                                                                                                                        datatype accessor ax9
                                                                                                                        arith conflicts2
                                                                                                                        arith assert diseq1
                                                                                                                        datatype constructor ax14
                                                                                                                        num allocs2162325665
                                                                                                                        final checks8
                                                                                                                        added eqs53
                                                                                                                        del clause5
                                                                                                                        arith eq adapter10
                                                                                                                        memory31.360000
                                                                                                                        max memory34.150000
                                                                                                                        Expand
                                                                                                                        • start[0.058s]
                                                                                                                            not (_x = []) && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                                                                                                                            ==> List.tl _x = []
                                                                                                                                || Ordinal.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                                                                                                                                   Ordinal.Int (Ordinal.count _x)
                                                                                                                        • simplify
                                                                                                                          into
                                                                                                                          (not
                                                                                                                           ((not (_x = []) && Ordinal.count _x >= 0) && Ordinal.count (List.tl _x) >= 0)
                                                                                                                           || List.tl _x = [])
                                                                                                                          || Ordinal.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                                                                                                                             Ordinal.Int (Ordinal.count _x)
                                                                                                                          expansions
                                                                                                                          []
                                                                                                                          rewrite_steps
                                                                                                                            forward_chaining
                                                                                                                            • unroll
                                                                                                                              expr
                                                                                                                              (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                                                                                                                  (|count_`ty_0 list list`_2841| (|get.::.1_2…
                                                                                                                              expansions
                                                                                                                              • unroll
                                                                                                                                expr
                                                                                                                                (|count_`ty_0 list list`_2841| (|get.::.1_2820| _x_2836))
                                                                                                                                expansions
                                                                                                                                • unroll
                                                                                                                                  expr
                                                                                                                                  (|count_`ty_0 list list`_2841| _x_2836)
                                                                                                                                  expansions
                                                                                                                                  • unsat
                                                                                                                                    (let ((a!1 (ite (>= (|count_`ty_0 list`_2843| (|get.::.0_2819| _x_2836)) 0)
                                                                                                                                                    (|count_…

                                                                                                                                  termination proof

                                                                                                                                  Termination proof

                                                                                                                                  call `blocks_3_32 (List.tl _x)` from `blocks_3_32 _x`
                                                                                                                                  originalblocks_3_32 _x
                                                                                                                                  subblocks_3_32 (List.tl _x)
                                                                                                                                  original ordinalOrdinal.Int (Ordinal.count _x)
                                                                                                                                  sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
                                                                                                                                  path[not (_x = [])]
                                                                                                                                  proof
                                                                                                                                  detailed proof
                                                                                                                                  ground_instances3
                                                                                                                                  definitions0
                                                                                                                                  inductions0
                                                                                                                                  search_time
                                                                                                                                  0.125s
                                                                                                                                  details
                                                                                                                                  Expand
                                                                                                                                  smt_stats
                                                                                                                                  num checks8
                                                                                                                                  arith assert lower16
                                                                                                                                  arith pivots8
                                                                                                                                  rlimit count34765
                                                                                                                                  mk clause12
                                                                                                                                  datatype occurs check37
                                                                                                                                  mk bool var87
                                                                                                                                  arith assert upper11
                                                                                                                                  datatype splits9
                                                                                                                                  decisions23
                                                                                                                                  arith add rows15
                                                                                                                                  propagations10
                                                                                                                                  conflicts11
                                                                                                                                  arith fixed eqs7
                                                                                                                                  datatype accessor ax8
                                                                                                                                  arith conflicts2
                                                                                                                                  arith assert diseq1
                                                                                                                                  datatype constructor ax15
                                                                                                                                  num allocs2249894043
                                                                                                                                  final checks8
                                                                                                                                  added eqs57
                                                                                                                                  del clause5
                                                                                                                                  arith eq adapter10
                                                                                                                                  memory31.360000
                                                                                                                                  max memory34.150000
                                                                                                                                  Expand
                                                                                                                                  • start[0.125s]
                                                                                                                                      not (_x = []) && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                                                                                                                                      ==> List.tl _x = []
                                                                                                                                          || Ordinal.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                                                                                                                                             Ordinal.Int (Ordinal.count _x)
                                                                                                                                  • simplify
                                                                                                                                    into
                                                                                                                                    (not
                                                                                                                                     ((not (_x = []) && Ordinal.count _x >= 0) && Ordinal.count (List.tl _x) >= 0)
                                                                                                                                     || List.tl _x = [])
                                                                                                                                    || Ordinal.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                                                                                                                                       Ordinal.Int (Ordinal.count _x)
                                                                                                                                    expansions
                                                                                                                                    []
                                                                                                                                    rewrite_steps
                                                                                                                                      forward_chaining
                                                                                                                                      • unroll
                                                                                                                                        expr
                                                                                                                                        (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                                                                                                                            (|count_`ty_0 list list`_2874| (|get.::.1_2…
                                                                                                                                        expansions
                                                                                                                                        • unroll
                                                                                                                                          expr
                                                                                                                                          (|count_`ty_0 list list`_2874| (|get.::.1_2858| _x_2869))
                                                                                                                                          expansions
                                                                                                                                          • unroll
                                                                                                                                            expr
                                                                                                                                            (|count_`ty_0 list list`_2874| _x_2869)
                                                                                                                                            expansions
                                                                                                                                            • unsat
                                                                                                                                              (let ((a!1 (ite (>= (|count_`ty_0 list`_2876| (|get.::.0_2857| _x_2869)) 0)
                                                                                                                                                              (|count_…

                                                                                                                                            termination proof

                                                                                                                                            Termination proof

                                                                                                                                            call `group3 (List.tl (List.tl (List.tl _x)))` from `group3 _x`
                                                                                                                                            originalgroup3 _x
                                                                                                                                            subgroup3 (List.tl (List.tl (List.tl _x)))
                                                                                                                                            original ordinalOrdinal.Int (Ordinal.count _x)
                                                                                                                                            sub ordinalOrdinal.Int (Ordinal.count (List.tl (List.tl (List.tl _x))))
                                                                                                                                            path[not (List.tl (List.tl _x) = []) && not (List.tl _x = []) && not (_x = [])]
                                                                                                                                            proof
                                                                                                                                            detailed proof
                                                                                                                                            ground_instances12
                                                                                                                                            definitions0
                                                                                                                                            inductions0
                                                                                                                                            search_time
                                                                                                                                            0.221s
                                                                                                                                            details
                                                                                                                                            Expand
                                                                                                                                            smt_stats
                                                                                                                                            arith offset eqs67
                                                                                                                                            num checks26
                                                                                                                                            arith assert lower344
                                                                                                                                            arith pivots133
                                                                                                                                            rlimit count75274
                                                                                                                                            mk clause440
                                                                                                                                            datatype occurs check204
                                                                                                                                            mk bool var1041
                                                                                                                                            arith assert upper337
                                                                                                                                            datatype splits91
                                                                                                                                            decisions901
                                                                                                                                            arith add rows652
                                                                                                                                            arith bound prop49
                                                                                                                                            propagations894
                                                                                                                                            interface eqs5
                                                                                                                                            conflicts72
                                                                                                                                            arith fixed eqs155
                                                                                                                                            datatype accessor ax96
                                                                                                                                            minimized lits17
                                                                                                                                            arith conflicts19
                                                                                                                                            arith assert diseq98
                                                                                                                                            datatype constructor ax257
                                                                                                                                            num allocs2348592907
                                                                                                                                            final checks40
                                                                                                                                            added eqs1269
                                                                                                                                            del clause244
                                                                                                                                            arith eq adapter238
                                                                                                                                            memory32.010000
                                                                                                                                            max memory34.450000
                                                                                                                                            Expand
                                                                                                                                            • start[0.221s]
                                                                                                                                                not (List.tl (List.tl _x) = [])
                                                                                                                                                && not (List.tl _x = [])
                                                                                                                                                   && not (_x = [])
                                                                                                                                                      && Ordinal.count _x >= 0
                                                                                                                                                         && Ordinal.count (List.tl (List.tl (List.tl _x))) >= 0
                                                                                                                                                ==> not
                                                                                                                                                    (not (List.tl (List.tl (List.tl (List.tl (List.tl _x)))) = [])
                                                                                                                                                     && not (List.tl (List.tl (List.tl (List.tl _x))) = [])
                                                                                                                                                        && not (List.tl (List.tl (List.tl _x)) = []))
                                                                                                                                                    || Ordinal.Int (Ordinal.count (List.tl (List.tl (List.tl _x))))
                                                                                                                                                       Ordinal.<< Ordinal.Int (Ordinal.count _x)
                                                                                                                                            • simplify
                                                                                                                                              into
                                                                                                                                              (not
                                                                                                                                               ((((not (List.tl (List.tl _x) = []) && not (List.tl _x = []))
                                                                                                                                                  && not (_x = []))
                                                                                                                                                 && Ordinal.count _x >= 0)
                                                                                                                                                && Ordinal.count (List.tl (List.tl (List.tl _x))) >= 0)
                                                                                                                                               || not
                                                                                                                                                  ((not (List.tl (List.tl (List.tl (List.tl (List.tl _x)))) = [])
                                                                                                                                                    && not (List.tl (List.tl (List.tl (List.tl _x))) = []))
                                                                                                                                                   && not (List.tl (List.tl (List.tl _x)) = [])))
                                                                                                                                              || Ordinal.Int (Ordinal.count (List.tl (List.tl (List.tl _x)))) Ordinal.<<
                                                                                                                                                 Ordinal.Int (Ordinal.count _x)
                                                                                                                                              expansions
                                                                                                                                              []
                                                                                                                                              rewrite_steps
                                                                                                                                                forward_chaining
                                                                                                                                                • unroll
                                                                                                                                                  expr
                                                                                                                                                  (let ((a!1 (|count_`ty_0 list list`_2914|
                                                                                                                                                               (|get.::.1_2895| (|get.::.1_2895| (|get.::.1_…
                                                                                                                                                  expansions
                                                                                                                                                  • unroll
                                                                                                                                                    expr
                                                                                                                                                    (|count_`ty_0 list list`_2914|
                                                                                                                                                      (|get.::.1_2895| (|get.::.1_2895| (|get.::.1_2895| _x_2909))))
                                                                                                                                                    expansions
                                                                                                                                                    • unroll
                                                                                                                                                      expr
                                                                                                                                                      (|count_`ty_0 list list`_2914| _x_2909)
                                                                                                                                                      expansions
                                                                                                                                                      • unroll
                                                                                                                                                        expr
                                                                                                                                                        (let ((a!1 (|get.::.1_2895| (|get.::.1_2895| (|get.::.1_2895| (|get.::.1_2895| _x_2909))))))
                                                                                                                                                          (|cou…
                                                                                                                                                        expansions
                                                                                                                                                        • unroll
                                                                                                                                                          expr
                                                                                                                                                          (let ((a!1 (|count_`ty_0 list list`_2914|
                                                                                                                                                                       (|get.::.1_2895| (|get.::.1_2895| (|get.::.1_…
                                                                                                                                                          expansions
                                                                                                                                                          • unroll
                                                                                                                                                            expr
                                                                                                                                                            (let ((a!1 (|get.::.0_2894| (|get.::.1_2895| (|get.::.1_2895| (|get.::.1_2895| _x_2909))))))
                                                                                                                                                              (|cou…
                                                                                                                                                            expansions
                                                                                                                                                            • unroll
                                                                                                                                                              expr
                                                                                                                                                              (|count_`ty_0 list list`_2914| (|get.::.1_2895| _x_2909))
                                                                                                                                                              expansions
                                                                                                                                                              • unroll
                                                                                                                                                                expr
                                                                                                                                                                (|count_`ty_0 list`_2916| (|get.::.0_2894| _x_2909))
                                                                                                                                                                expansions
                                                                                                                                                                • unroll
                                                                                                                                                                  expr
                                                                                                                                                                  (let ((a!1 (|get.::.1_2895| (|get.::.1_2895| (|get.::.1_2895| (|get.::.1_2895| _x_2909))))))
                                                                                                                                                                    (|cou…
                                                                                                                                                                  expansions
                                                                                                                                                                  • unroll
                                                                                                                                                                    expr
                                                                                                                                                                    (let ((a!1 (|count_`ty_0 list list`_2914|
                                                                                                                                                                                 (|get.::.1_2895| (|get.::.1_2895| (|get.::.1_…
                                                                                                                                                                    expansions
                                                                                                                                                                    • unroll
                                                                                                                                                                      expr
                                                                                                                                                                      (let ((a!1 (|get.::.1_2895| (|get.::.1_2895| (|get.::.1_2895| (|get.::.1_2895| _x_2909))))))
                                                                                                                                                                        (|cou…
                                                                                                                                                                      expansions
                                                                                                                                                                      • unroll
                                                                                                                                                                        expr
                                                                                                                                                                        (|count_`ty_0 list list`_2914| (|get.::.1_2895| (|get.::.1_2895| _x_2909)))
                                                                                                                                                                        expansions
                                                                                                                                                                        • unsat
                                                                                                                                                                          (let ((a!1 (ite (>= (|count_`ty_0 list`_2916| (|get.::.0_2894| _x_2909)) 0)
                                                                                                                                                                                          (|count_…

                                                                                                                                                                        The Sudoku type

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

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

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

                                                                                                                                                                        And the sudoku itself:

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

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

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

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

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

                                                                                                                                                                        Termination proof

                                                                                                                                                                        call `zip (List.tl l1) (List.tl l2)` from `zip l1 l2`
                                                                                                                                                                        originalzip l1 l2
                                                                                                                                                                        subzip (List.tl l1) (List.tl l2)
                                                                                                                                                                        original ordinalOrdinal.Int (Ordinal.count l1)
                                                                                                                                                                        sub ordinalOrdinal.Int (Ordinal.count (List.tl l1))
                                                                                                                                                                        path[not (l1 = [] || l2 = [])]
                                                                                                                                                                        proof
                                                                                                                                                                        detailed proof
                                                                                                                                                                        ground_instances3
                                                                                                                                                                        definitions0
                                                                                                                                                                        inductions0
                                                                                                                                                                        search_time
                                                                                                                                                                        0.036s
                                                                                                                                                                        details
                                                                                                                                                                        Expand
                                                                                                                                                                        smt_stats
                                                                                                                                                                        num checks7
                                                                                                                                                                        arith assert lower5
                                                                                                                                                                        arith pivots3
                                                                                                                                                                        rlimit count77331
                                                                                                                                                                        mk clause3
                                                                                                                                                                        datatype occurs check30
                                                                                                                                                                        mk bool var70
                                                                                                                                                                        arith assert upper5
                                                                                                                                                                        datatype splits6
                                                                                                                                                                        decisions15
                                                                                                                                                                        arith add rows7
                                                                                                                                                                        propagations1
                                                                                                                                                                        conflicts11
                                                                                                                                                                        arith fixed eqs4
                                                                                                                                                                        datatype accessor ax8
                                                                                                                                                                        arith conflicts1
                                                                                                                                                                        datatype constructor ax17
                                                                                                                                                                        num allocs2415856974
                                                                                                                                                                        final checks6
                                                                                                                                                                        added eqs57
                                                                                                                                                                        del clause1
                                                                                                                                                                        arith eq adapter3
                                                                                                                                                                        memory35.580000
                                                                                                                                                                        max memory35.580000
                                                                                                                                                                        Expand
                                                                                                                                                                        • start[0.036s]
                                                                                                                                                                            not (l1 = [] || l2 = [])
                                                                                                                                                                            && Ordinal.count l1 >= 0 && Ordinal.count (List.tl l1) >= 0
                                                                                                                                                                            ==> (List.tl l1 = [] || List.tl l2 = [])
                                                                                                                                                                                || Ordinal.Int (Ordinal.count (List.tl l1)) Ordinal.<<
                                                                                                                                                                                   Ordinal.Int (Ordinal.count l1)
                                                                                                                                                                        • simplify
                                                                                                                                                                          into
                                                                                                                                                                          ((not
                                                                                                                                                                            ((not (l1 = [] || l2 = []) && Ordinal.count l1 >= 0)
                                                                                                                                                                             && Ordinal.count (List.tl l1) >= 0)
                                                                                                                                                                            || List.tl l1 = [])
                                                                                                                                                                           || List.tl l2 = [])
                                                                                                                                                                          || Ordinal.Int (Ordinal.count (List.tl l1)) Ordinal.<<
                                                                                                                                                                             Ordinal.Int (Ordinal.count l1)
                                                                                                                                                                          expansions
                                                                                                                                                                          []
                                                                                                                                                                          rewrite_steps
                                                                                                                                                                            forward_chaining
                                                                                                                                                                            • unroll
                                                                                                                                                                              expr
                                                                                                                                                                              (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                                                                                                                                                                  (|count_`ty_0 list`_3151| (|get.::.1_3126| …
                                                                                                                                                                              expansions
                                                                                                                                                                              • unroll
                                                                                                                                                                                expr
                                                                                                                                                                                (|count_`ty_0 list`_3151| (|get.::.1_3126| l1_3144))
                                                                                                                                                                                expansions
                                                                                                                                                                                • unroll
                                                                                                                                                                                  expr
                                                                                                                                                                                  (|count_`ty_0 list`_3151| l1_3144)
                                                                                                                                                                                  expansions
                                                                                                                                                                                  • unsat
                                                                                                                                                                                    (let ((a!1 (= (|count_`ty_0 list`_3151| l1_3144)
                                                                                                                                                                                                  (+ 1 (|count_`ty_0 list`_3151| (|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
                                                                                                                                                                                  definitions2
                                                                                                                                                                                  inductions0
                                                                                                                                                                                  search_time
                                                                                                                                                                                  0.118s
                                                                                                                                                                                  details
                                                                                                                                                                                  Expand
                                                                                                                                                                                  smt_stats
                                                                                                                                                                                  num checks7
                                                                                                                                                                                  arith assert lower6
                                                                                                                                                                                  arith pivots5
                                                                                                                                                                                  rlimit count83132
                                                                                                                                                                                  mk clause26
                                                                                                                                                                                  datatype occurs check110
                                                                                                                                                                                  mk bool var157
                                                                                                                                                                                  arith assert upper4
                                                                                                                                                                                  datatype splits39
                                                                                                                                                                                  decisions35
                                                                                                                                                                                  arith add rows6
                                                                                                                                                                                  propagations54
                                                                                                                                                                                  conflicts11
                                                                                                                                                                                  arith fixed eqs3
                                                                                                                                                                                  datatype accessor ax27
                                                                                                                                                                                  arith conflicts1
                                                                                                                                                                                  datatype constructor ax33
                                                                                                                                                                                  num allocs2573649397
                                                                                                                                                                                  final checks14
                                                                                                                                                                                  added eqs149
                                                                                                                                                                                  del clause2
                                                                                                                                                                                  arith eq adapter3
                                                                                                                                                                                  memory38.520000
                                                                                                                                                                                  max memory38.520000
                                                                                                                                                                                  Expand
                                                                                                                                                                                  • start[0.118s]
                                                                                                                                                                                      ((List.hd y).0 = None || (List.hd y).1 = None)
                                                                                                                                                                                      && not (y = []) && Ordinal.count y >= 0 && Ordinal.count (List.tl y) >= 0
                                                                                                                                                                                      ==> not
                                                                                                                                                                                          (((List.hd (List.tl y)).0 = None || (List.hd (List.tl y)).1 = None)
                                                                                                                                                                                           && not (List.tl y = []))
                                                                                                                                                                                          && not
                                                                                                                                                                                             (Option.get (List.hd (List.tl y)).0 =
                                                                                                                                                                                              Option.get (List.hd (List.tl y)).1
                                                                                                                                                                                              && not
                                                                                                                                                                                                 ((List.hd (List.tl y)).0 = None
                                                                                                                                                                                                  || (List.hd (List.tl y)).1 = None)
                                                                                                                                                                                                 && not (List.tl y = []))
                                                                                                                                                                                          || Ordinal.Int (Ordinal.count (List.tl y)) Ordinal.<<
                                                                                                                                                                                             Ordinal.Int (Ordinal.count y)
                                                                                                                                                                                  • simplify
                                                                                                                                                                                    into
                                                                                                                                                                                    (not
                                                                                                                                                                                     (((((List.hd y).0 = None || (List.hd y).1 = None) && not (y = []))
                                                                                                                                                                                       && Ordinal.count y >= 0)
                                                                                                                                                                                      && Ordinal.count (List.tl y) >= 0)
                                                                                                                                                                                     || not
                                                                                                                                                                                        (((List.hd (List.tl y)).0 = None || (List.hd (List.tl y)).1 = None)
                                                                                                                                                                                         && not (List.tl y = []))
                                                                                                                                                                                        && not
                                                                                                                                                                                           ((Option.get (List.hd (List.tl y)).0 =
                                                                                                                                                                                             Option.get (List.hd (List.tl y)).1
                                                                                                                                                                                             && not
                                                                                                                                                                                                ((List.hd (List.tl y)).0 = None || (List.hd (List.tl y)).1 = None))
                                                                                                                                                                                            && not (List.tl y = [])))
                                                                                                                                                                                    || Ordinal.Int (Ordinal.count (List.tl y)) Ordinal.<<
                                                                                                                                                                                       Ordinal.Int (Ordinal.count y)
                                                                                                                                                                                    expansions
                                                                                                                                                                                    []
                                                                                                                                                                                    rewrite_steps
                                                                                                                                                                                      forward_chaining
                                                                                                                                                                                      • unroll
                                                                                                                                                                                        expr
                                                                                                                                                                                        (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                                                                                                                                                                            (|count_`(ty_0 option * ty_0 option) list`_…
                                                                                                                                                                                        expansions
                                                                                                                                                                                        • unroll
                                                                                                                                                                                          expr
                                                                                                                                                                                          (|count_`(ty_0 option * ty_0 option) list`_3185| (|get.::.1_3171| y_3178))
                                                                                                                                                                                          expansions
                                                                                                                                                                                          Ordinal.count
                                                                                                                                                                                        • unroll
                                                                                                                                                                                          expr
                                                                                                                                                                                          (|count_`(ty_0 option * ty_0 option) list`_3185| y_3178)
                                                                                                                                                                                          expansions
                                                                                                                                                                                          Ordinal.count
                                                                                                                                                                                        • unsat
                                                                                                                                                                                          (let ((a!1 (= (|count_`(ty_0 option * ty_0 option) list`_3185| y_3178)
                                                                                                                                                                                                        (+ 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
                                                                                                                                                                                        definitions2
                                                                                                                                                                                        inductions0
                                                                                                                                                                                        search_time
                                                                                                                                                                                        0.105s
                                                                                                                                                                                        details
                                                                                                                                                                                        Expand
                                                                                                                                                                                        smt_stats
                                                                                                                                                                                        num checks7
                                                                                                                                                                                        arith assert lower6
                                                                                                                                                                                        arith pivots5
                                                                                                                                                                                        rlimit count80303
                                                                                                                                                                                        mk clause24
                                                                                                                                                                                        datatype occurs check100
                                                                                                                                                                                        mk bool var161
                                                                                                                                                                                        arith assert upper4
                                                                                                                                                                                        datatype splits36
                                                                                                                                                                                        decisions34
                                                                                                                                                                                        arith add rows6
                                                                                                                                                                                        propagations62
                                                                                                                                                                                        conflicts13
                                                                                                                                                                                        arith fixed eqs3
                                                                                                                                                                                        datatype accessor ax29
                                                                                                                                                                                        arith conflicts1
                                                                                                                                                                                        datatype constructor ax37
                                                                                                                                                                                        num allocs2515291391
                                                                                                                                                                                        final checks13
                                                                                                                                                                                        added eqs161
                                                                                                                                                                                        del clause2
                                                                                                                                                                                        arith eq adapter3
                                                                                                                                                                                        memory35.600000
                                                                                                                                                                                        max memory35.600000
                                                                                                                                                                                        Expand
                                                                                                                                                                                        • start[0.105s]
                                                                                                                                                                                            Option.get (List.hd y).0 = Option.get (List.hd y).1
                                                                                                                                                                                            && not ((List.hd y).0 = None || (List.hd y).1 = None)
                                                                                                                                                                                               && not (y = [])
                                                                                                                                                                                                  && Ordinal.count y >= 0 && Ordinal.count (List.tl y) >= 0
                                                                                                                                                                                            ==> not
                                                                                                                                                                                                (((List.hd (List.tl y)).0 = None || (List.hd (List.tl y)).1 = None)
                                                                                                                                                                                                 && not (List.tl y = []))
                                                                                                                                                                                                && not
                                                                                                                                                                                                   (Option.get (List.hd (List.tl y)).0 =
                                                                                                                                                                                                    Option.get (List.hd (List.tl y)).1
                                                                                                                                                                                                    && not
                                                                                                                                                                                                       ((List.hd (List.tl y)).0 = None
                                                                                                                                                                                                        || (List.hd (List.tl y)).1 = None)
                                                                                                                                                                                                       && not (List.tl y = []))
                                                                                                                                                                                                || Ordinal.Int (Ordinal.count (List.tl y)) Ordinal.<<
                                                                                                                                                                                                   Ordinal.Int (Ordinal.count y)
                                                                                                                                                                                        • simplify
                                                                                                                                                                                          into
                                                                                                                                                                                          (not
                                                                                                                                                                                           ((((Option.get (List.hd y).0 = Option.get (List.hd y).1
                                                                                                                                                                                               && not ((List.hd y).0 = None || (List.hd y).1 = None))
                                                                                                                                                                                              && not (y = []))
                                                                                                                                                                                             && Ordinal.count y >= 0)
                                                                                                                                                                                            && Ordinal.count (List.tl y) >= 0)
                                                                                                                                                                                           || not
                                                                                                                                                                                              (((List.hd (List.tl y)).0 = None || (List.hd (List.tl y)).1 = None)
                                                                                                                                                                                               && not (List.tl y = []))
                                                                                                                                                                                              && not
                                                                                                                                                                                                 ((Option.get (List.hd (List.tl y)).0 =
                                                                                                                                                                                                   Option.get (List.hd (List.tl y)).1
                                                                                                                                                                                                   && not
                                                                                                                                                                                                      ((List.hd (List.tl y)).0 = None || (List.hd (List.tl y)).1 = None))
                                                                                                                                                                                                  && not (List.tl y = [])))
                                                                                                                                                                                          || Ordinal.Int (Ordinal.count (List.tl y)) Ordinal.<<
                                                                                                                                                                                             Ordinal.Int (Ordinal.count y)
                                                                                                                                                                                          expansions
                                                                                                                                                                                          []
                                                                                                                                                                                          rewrite_steps
                                                                                                                                                                                            forward_chaining
                                                                                                                                                                                            • unroll
                                                                                                                                                                                              expr
                                                                                                                                                                                              (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                                                                                                                                                                                  (|count_`(ty_0 option * ty_0 option) list`_…
                                                                                                                                                                                              expansions
                                                                                                                                                                                              • unroll
                                                                                                                                                                                                expr
                                                                                                                                                                                                (|count_`(ty_0 option * ty_0 option) list`_3185| (|get.::.1_3171| y_3178))
                                                                                                                                                                                                expansions
                                                                                                                                                                                                Ordinal.count
                                                                                                                                                                                              • unroll
                                                                                                                                                                                                expr
                                                                                                                                                                                                (|count_`(ty_0 option * ty_0 option) list`_3185| y_3178)
                                                                                                                                                                                                expansions
                                                                                                                                                                                                Ordinal.count
                                                                                                                                                                                              • unsat
                                                                                                                                                                                                (let ((a!1 (= (|count_`(ty_0 option * ty_0 option) list`_3185| y_3178)
                                                                                                                                                                                                              (+ 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
                                                                                                                                                                                              definitions2
                                                                                                                                                                                              inductions0
                                                                                                                                                                                              search_time
                                                                                                                                                                                              0.158s
                                                                                                                                                                                              details
                                                                                                                                                                                              Expand
                                                                                                                                                                                              smt_stats
                                                                                                                                                                                              arith offset eqs5
                                                                                                                                                                                              num checks12
                                                                                                                                                                                              arith assert lower31
                                                                                                                                                                                              arith pivots20
                                                                                                                                                                                              rlimit count89771
                                                                                                                                                                                              mk clause54
                                                                                                                                                                                              datatype occurs check90
                                                                                                                                                                                              mk bool var236
                                                                                                                                                                                              arith assert upper27
                                                                                                                                                                                              datatype splits27
                                                                                                                                                                                              decisions85
                                                                                                                                                                                              arith add rows31
                                                                                                                                                                                              propagations53
                                                                                                                                                                                              conflicts17
                                                                                                                                                                                              arith fixed eqs11
                                                                                                                                                                                              datatype accessor ax31
                                                                                                                                                                                              minimized lits2
                                                                                                                                                                                              arith conflicts6
                                                                                                                                                                                              arith assert diseq1
                                                                                                                                                                                              datatype constructor ax52
                                                                                                                                                                                              num allocs2726959876
                                                                                                                                                                                              final checks11
                                                                                                                                                                                              added eqs203
                                                                                                                                                                                              del clause21
                                                                                                                                                                                              arith eq adapter20
                                                                                                                                                                                              memory35.860000
                                                                                                                                                                                              max memory38.520000
                                                                                                                                                                                              Expand
                                                                                                                                                                                              • start[0.158s]
                                                                                                                                                                                                  match_cols (zip (List.hd …).0 (List.hd …).1)
                                                                                                                                                                                                  && not (… = [])
                                                                                                                                                                                                     && Ordinal.count … >= 0 && Ordinal.count (List.tl …) >= 0
                                                                                                                                                                                                  ==> not
                                                                                                                                                                                                      (match_cols (zip (List.hd (List.tl …)).0 (List.hd (List.tl …)).1)
                                                                                                                                                                                                       && not (List.tl … = []))
                                                                                                                                                                                                      || Ordinal.Int (Ordinal.count (List.tl …)) Ordinal.<<
                                                                                                                                                                                                         Ordinal.Int (Ordinal.count …)
                                                                                                                                                                                              • simplify
                                                                                                                                                                                                into
                                                                                                                                                                                                (not
                                                                                                                                                                                                 (((match_cols (zip (List.hd …).0 (List.hd …).1) && not (… = []))
                                                                                                                                                                                                   && Ordinal.count … >= 0)
                                                                                                                                                                                                  && Ordinal.count (List.tl …) >= 0)
                                                                                                                                                                                                 || not
                                                                                                                                                                                                    (match_cols (zip (List.hd (List.tl …)).0 (List.hd (List.tl …)).1)
                                                                                                                                                                                                     && not (List.tl … = [])))
                                                                                                                                                                                                || Ordinal.Int (Ordinal.count (List.tl …)) Ordinal.<<
                                                                                                                                                                                                   Ordinal.Int (Ordinal.count …)
                                                                                                                                                                                                expansions
                                                                                                                                                                                                []
                                                                                                                                                                                                rewrite_steps
                                                                                                                                                                                                  forward_chaining
                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                    expr
                                                                                                                                                                                                    (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                                                                                                                                                                                        (|count_`(ty_0 option list * ty_0 option li…
                                                                                                                                                                                                    expansions
                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                      expr
                                                                                                                                                                                                      (zip_3226 (|tuple_get.0_3209| (|get.::.0_3212| (|get.::.1_3213| x_3239)))
                                                                                                                                                                                                                (|tuple_get.1_32…
                                                                                                                                                                                                      expansions
                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                        expr
                                                                                                                                                                                                        (let ((a!1 (zip_3226 (|tuple_get.0_3209|
                                                                                                                                                                                                                               (|get.::.0_3212| (|get.::.1_3213| x_…
                                                                                                                                                                                                        expansions
                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                          expr
                                                                                                                                                                                                          (|count_`(ty_0 option list * ty_0 option list) list`_3244|
                                                                                                                                                                                                            (|get.::.1_3213| x_3239))
                                                                                                                                                                                                          expansions
                                                                                                                                                                                                          Ordinal.count
                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                          expr
                                                                                                                                                                                                          (|count_`(ty_0 option list * ty_0 option list) list`_3244| x_3239)
                                                                                                                                                                                                          expansions
                                                                                                                                                                                                          Ordinal.count
                                                                                                                                                                                                        • unsat
                                                                                                                                                                                                          (let ((a!1 (>= (|count_`ty_0 option list`_3248|
                                                                                                                                                                                                                           (|tuple_get.0_3209| (|get.::.0_3212…

                                                                                                                                                                                                        The Satisfaction of Subrepticiously Solving Sudokus using Satisfiability

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

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

                                                                                                                                                                                                        In [10]:
                                                                                                                                                                                                        instance (fun (s:sudoku) -> is_valid_sudoku s && is_solution_of s the_problem) [@@blast] ;;
                                                                                                                                                                                                        
                                                                                                                                                                                                        Out[10]:
                                                                                                                                                                                                        - : sudoku -> bool = <fun>
                                                                                                                                                                                                        module CX : sig val s : sudoku end
                                                                                                                                                                                                        
                                                                                                                                                                                                        Instance (after 273 steps, 3.184s):
                                                                                                                                                                                                          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