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 -> int/2 = <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 (_cnt _x)
sub ordinalOrdinal.Int (_cnt (List.tl _x))
path[not Is_a([], _x)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.017s
details
Expand
smt_stats
num checks7
arith-make-feasible7
arith-max-columns10
rlimit count1551
arith-cheap-eqs1
mk clause11
datatype occurs check12
mk bool var36
arith-lower4
datatype splits1
decisions4
propagations6
arith-max-rows2
conflicts3
datatype accessor ax7
datatype constructor ax5
num allocs688530
final checks4
added eqs26
del clause9
arith eq adapter3
arith-upper5
memory5.220000
max memory5.220000
Expand
  • start[0.017s]
      let (_x_0 : int) = count.list (const 0) _x in
      let (_x_1 : ty_0 list) = List.tl _x in
      let (_x_2 : int) = count.list (const 0) _x_1 in
      not Is_a([], _x) && _x_0 >= 0 && _x_2 >= 0
      ==> Is_a([], _x_1) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
  • simplify
    into
    let (_x_0 : ty_0 list) = List.tl _x in
    let (_x_1 : int) = count.list (const 0) _x_0 in
    let (_x_2 : int) = count.list (const 0) _x in
    (Is_a([], _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
    || not ((not Is_a([], _x) && _x_2 >= 0) && _x_1 >= 0)
    expansions
    []
    rewrite_steps
      forward_chaining
      • unroll
        expr
        (|`count.list (const 0)[0]`_1697| _x_1686)
        expansions
        • unroll
          expr
          (|`count.list (const 0)[0]`_1697| (|get.::.1_1680| _x_1686))
          expansions
          • unroll
            expr
            (|Ordinal.<<_126| (|Ordinal.Int_111|
                                (|`count.list (const 0)[0]`_1697| (|get.::.…
            expansions
            • Unsat

            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 -> int = <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 (_cnt _x)
            sub ordinalOrdinal.Int (_cnt (List.tl _x))
            path[Is_a([], List.hd _x) && not Is_a([], _x)]
            proof
            detailed proof
            ground_instances3
            definitions0
            inductions0
            search_time
            0.015s
            details
            Expand
            smt_stats
            num checks8
            arith-assume-eqs1
            arith-make-feasible18
            arith-max-columns19
            arith-conflicts2
            rlimit count5442
            mk clause34
            datatype occurs check24
            mk bool var97
            arith-lower11
            datatype splits6
            decisions21
            propagations29
            interface eqs1
            arith-max-rows7
            conflicts7
            datatype accessor ax14
            datatype constructor ax15
            num allocs4534453
            final checks7
            added eqs77
            del clause22
            arith eq adapter9
            arith-upper16
            memory8.690000
            max memory8.690000
            Expand
            • start[0.015s]
                let (_x_0 : int) = count.list (count.list (const 0)) _x in
                let (_x_1 : ty_0 list list) = List.tl _x in
                let (_x_2 : int) = count.list (count.list (const 0)) _x_1 in
                let (_x_3 : bool) = Is_a([], List.hd _x_1) in
                let (_x_4 : bool) = not Is_a([], _x_1) in
                Is_a([], List.hd _x) && not Is_a([], _x) && _x_0 >= 0 && _x_2 >= 0
                ==> not (_x_3 && _x_4) && not (not _x_3 && _x_4)
                    || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
            • simplify
              into
              let (_x_0 : ty_0 list list) = List.tl _x in
              let (_x_1 : bool) = Is_a([], List.hd _x_0) in
              let (_x_2 : bool) = not Is_a([], _x_0) in
              let (_x_3 : int) = count.list (count.list (const 0)) _x_0 in
              let (_x_4 : int) = count.list (count.list (const 0)) _x in
              (not (_x_1 && _x_2) && not (not _x_1 && _x_2)
               || Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_4))
              || not
                 (((Is_a([], List.hd _x) && not Is_a([], _x)) && _x_4 >= 0) && _x_3 >= 0)
              expansions
              []
              rewrite_steps
                forward_chaining
                • unroll
                  expr
                  (|`count.list clos_921831342[0]`_1755| _x_1742)
                  expansions
                  • unroll
                    expr
                    (|`count.list clos_921831342[0]`_1755| (|get.::.1_1735| _x_1742))
                    expansions
                    • unroll
                      expr
                      (|Ordinal.<<_126| (|Ordinal.Int_111|
                                          (|`count.list clos_921831342[0]`_1755|
                          …
                      expansions
                      • Unsat

                      call `transpose3 (List.tl _x)` from `transpose3 _x`
                      originaltranspose3 _x
                      subtranspose3 (List.tl _x)
                      original ordinalOrdinal.Int (_cnt _x)
                      sub ordinalOrdinal.Int (_cnt (List.tl _x))
                      path[not Is_a([], List.hd _x) && not Is_a([], _x)]
                      proof
                      detailed proof
                      ground_instances3
                      definitions0
                      inductions0
                      search_time
                      0.014s
                      details
                      Expand
                      smt_stats
                      num checks8
                      arith-assume-eqs1
                      arith-make-feasible24
                      arith-max-columns19
                      arith-conflicts2
                      rlimit count2825
                      mk clause38
                      datatype occurs check27
                      mk bool var114
                      arith-lower15
                      datatype splits9
                      decisions29
                      propagations35
                      interface eqs1
                      arith-max-rows7
                      conflicts9
                      datatype accessor ax17
                      datatype constructor ax18
                      num allocs2862188
                      final checks7
                      added eqs93
                      del clause26
                      arith eq adapter13
                      arith-upper21
                      memory6.090000
                      max memory6.090000
                      Expand
                      • start[0.014s]
                          let (_x_0 : int) = count.list (count.list (const 0)) _x in
                          let (_x_1 : ty_0 list list) = List.tl _x in
                          let (_x_2 : int) = count.list (count.list (const 0)) _x_1 in
                          let (_x_3 : bool) = Is_a([], List.hd _x_1) in
                          let (_x_4 : bool) = not Is_a([], _x_1) in
                          not Is_a([], List.hd _x) && not Is_a([], _x) && _x_0 >= 0 && _x_2 >= 0
                          ==> not (_x_3 && _x_4) && not (not _x_3 && _x_4)
                              || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                      • simplify
                        into
                        let (_x_0 : ty_0 list list) = List.tl _x in
                        let (_x_1 : bool) = Is_a([], List.hd _x_0) in
                        let (_x_2 : bool) = not Is_a([], _x_0) in
                        let (_x_3 : int) = count.list (count.list (const 0)) _x_0 in
                        let (_x_4 : int) = count.list (count.list (const 0)) _x in
                        (not (_x_1 && _x_2) && not (not _x_1 && _x_2)
                         || Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_4))
                        || not
                           (((not Is_a([], List.hd _x) && not Is_a([], _x)) && _x_4 >= 0)
                            && _x_3 >= 0)
                        expansions
                        []
                        rewrite_steps
                          forward_chaining
                          • unroll
                            expr
                            (|`count.list clos_921831342[0]`_1755| _x_1742)
                            expansions
                            • unroll
                              expr
                              (|`count.list clos_921831342[0]`_1755| (|get.::.1_1735| _x_1742))
                              expansions
                              • unroll
                                expr
                                (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                    (|`count.list clos_921831342[0]`_1755|
                                    …
                                expansions
                                • Unsat

                                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 (_cnt _x)
                                sub ordinalOrdinal.Int (_cnt (List.tl _x))
                                path[Is_a([], List.hd _x) && not Is_a([], _x)]
                                proof
                                detailed proof
                                ground_instances3
                                definitions0
                                inductions0
                                search_time
                                0.014s
                                details
                                Expand
                                smt_stats
                                num checks8
                                arith-assume-eqs1
                                arith-make-feasible18
                                arith-max-columns19
                                arith-conflicts2
                                rlimit count5442
                                mk clause34
                                datatype occurs check24
                                mk bool var97
                                arith-lower11
                                datatype splits6
                                decisions21
                                propagations29
                                interface eqs1
                                arith-max-rows7
                                conflicts7
                                datatype accessor ax14
                                datatype constructor ax15
                                num allocs13773365
                                final checks7
                                added eqs77
                                del clause22
                                arith eq adapter9
                                arith-upper16
                                memory8.990000
                                max memory8.990000
                                Expand
                                • start[0.014s]
                                    let (_x_0 : int) = count.list (count.list (const 0)) _x in
                                    let (_x_1 : ty_0 list list) = List.tl _x in
                                    let (_x_2 : int) = count.list (count.list (const 0)) _x_1 in
                                    let (_x_3 : bool) = Is_a([], List.hd _x_1) in
                                    let (_x_4 : bool) = not Is_a([], _x_1) in
                                    Is_a([], List.hd _x) && not Is_a([], _x) && _x_0 >= 0 && _x_2 >= 0
                                    ==> not (_x_3 && _x_4) && not (not _x_3 && _x_4)
                                        || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                • simplify
                                  into
                                  let (_x_0 : ty_0 list list) = List.tl _x in
                                  let (_x_1 : bool) = Is_a([], List.hd _x_0) in
                                  let (_x_2 : bool) = not Is_a([], _x_0) in
                                  let (_x_3 : int) = count.list (count.list (const 0)) _x_0 in
                                  let (_x_4 : int) = count.list (count.list (const 0)) _x in
                                  (not (_x_1 && _x_2) && not (not _x_1 && _x_2)
                                   || Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_4))
                                  || not
                                     (((Is_a([], List.hd _x) && not Is_a([], _x)) && _x_4 >= 0) && _x_3 >= 0)
                                  expansions
                                  []
                                  rewrite_steps
                                    forward_chaining
                                    • unroll
                                      expr
                                      (|`count.list clos_148560117[0]`_1865| _x_1852)
                                      expansions
                                      • unroll
                                        expr
                                        (|`count.list clos_148560117[0]`_1865| (|get.::.1_1845| _x_1852))
                                        expansions
                                        • unroll
                                          expr
                                          (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                              (|`count.list clos_148560117[0]`_1865|
                                              …
                                          expansions
                                          • Unsat

                                          call `get_heads (List.tl _x)` from `get_heads _x`
                                          originalget_heads _x
                                          subget_heads (List.tl _x)
                                          original ordinalOrdinal.Int (_cnt _x)
                                          sub ordinalOrdinal.Int (_cnt (List.tl _x))
                                          path[not Is_a([], List.hd _x) && not Is_a([], _x)]
                                          proof
                                          detailed proof
                                          ground_instances3
                                          definitions0
                                          inductions0
                                          search_time
                                          0.013s
                                          details
                                          Expand
                                          smt_stats
                                          num checks8
                                          arith-assume-eqs1
                                          arith-make-feasible24
                                          arith-max-columns19
                                          arith-conflicts2
                                          rlimit count2825
                                          mk clause38
                                          datatype occurs check27
                                          mk bool var114
                                          arith-lower15
                                          datatype splits9
                                          decisions29
                                          propagations35
                                          interface eqs1
                                          arith-max-rows7
                                          conflicts9
                                          datatype accessor ax17
                                          datatype constructor ax18
                                          num allocs10941486
                                          final checks7
                                          added eqs93
                                          del clause26
                                          arith eq adapter13
                                          arith-upper21
                                          memory6.430000
                                          max memory8.690000
                                          Expand
                                          • start[0.013s]
                                              let (_x_0 : int) = count.list (count.list (const 0)) _x in
                                              let (_x_1 : ty_0 list list) = List.tl _x in
                                              let (_x_2 : int) = count.list (count.list (const 0)) _x_1 in
                                              let (_x_3 : bool) = Is_a([], List.hd _x_1) in
                                              let (_x_4 : bool) = not Is_a([], _x_1) in
                                              not Is_a([], List.hd _x) && not Is_a([], _x) && _x_0 >= 0 && _x_2 >= 0
                                              ==> not (_x_3 && _x_4) && not (not _x_3 && _x_4)
                                                  || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                          • simplify
                                            into
                                            let (_x_0 : ty_0 list list) = List.tl _x in
                                            let (_x_1 : bool) = Is_a([], List.hd _x_0) in
                                            let (_x_2 : bool) = not Is_a([], _x_0) in
                                            let (_x_3 : int) = count.list (count.list (const 0)) _x_0 in
                                            let (_x_4 : int) = count.list (count.list (const 0)) _x in
                                            (not (_x_1 && _x_2) && not (not _x_1 && _x_2)
                                             || Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_4))
                                            || not
                                               (((not Is_a([], List.hd _x) && not Is_a([], _x)) && _x_4 >= 0)
                                                && _x_3 >= 0)
                                            expansions
                                            []
                                            rewrite_steps
                                              forward_chaining
                                              • unroll
                                                expr
                                                (|`count.list clos_148560117[0]`_1865| _x_1852)
                                                expansions
                                                • unroll
                                                  expr
                                                  (|`count.list clos_148560117[0]`_1865| (|get.::.1_1845| _x_1852))
                                                  expansions
                                                  • unroll
                                                    expr
                                                    (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                                        (|`count.list clos_148560117[0]`_1865|
                                                        …
                                                    expansions
                                                    • Unsat

                                                    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 ordinallet (_x_0 : int) = measure_transpose l in Ordinal.Int (if _x_0 >= 0 then _x_0 else 0)
                                                    sub ordinallet (_x_0 : int) = measure_transpose ((List.tl (List.hd l)) :: (transpose3 (List.tl l))) in Ordinal.Int (if _x_0 >= 0 then _x_0 else 0)
                                                    path[not Is_a([], List.hd l) && not Is_a([], l)]
                                                    proof
                                                    detailed proof
                                                    ground_instances3
                                                    definitions0
                                                    inductions0
                                                    search_time
                                                    0.013s
                                                    details
                                                    Expand
                                                    smt_stats
                                                    num checks7
                                                    arith-make-feasible7
                                                    arith-max-columns9
                                                    rlimit count1881
                                                    mk clause8
                                                    datatype occurs check13
                                                    mk bool var41
                                                    arith-lower2
                                                    datatype splits2
                                                    decisions6
                                                    propagations4
                                                    arith-max-rows2
                                                    conflicts3
                                                    datatype accessor ax11
                                                    datatype constructor ax9
                                                    num allocs23838383
                                                    final checks4
                                                    added eqs35
                                                    del clause8
                                                    arith eq adapter2
                                                    arith-upper5
                                                    memory6.770000
                                                    max memory8.990000
                                                    Expand
                                                    • start[0.013s]
                                                        let (_x_0 : ty_0 list) = List.hd l in
                                                        let (_x_1 : bool) = Is_a([], l) in
                                                        let (_x_2 : int) = if _x_1 then 0 else List.length _x_0 in
                                                        let (_x_3 : int) = if _x_2 >= 0 then _x_2 else 0 in
                                                        let (_x_4 : int) = List.length … in
                                                        let (_x_5 : int) = if _x_4 >= 0 then _x_4 else 0 in
                                                        not Is_a([], _x_0) && not _x_1 && _x_3 >= 0 && _x_5 >= 0
                                                        ==> Is_a([], List.tl _x_0)
                                                            || Ordinal.( << ) (Ordinal.Int _x_5) (Ordinal.Int _x_3)
                                                    • simplify
                                                      into
                                                      let (_x_0 : ty_0 list) = List.hd l in
                                                      let (_x_1 : ty_0 list) = List.tl _x_0 in
                                                      let (_x_2 : int) = List.length _x_1 in
                                                      let (_x_3 : int) = List.length _x_0 in
                                                      let (_x_4 : bool) = Is_a([], l) in
                                                      let (_x_5 : bool) = _x_4 || _x_3 >= 0 in
                                                      (Is_a([], _x_1)
                                                       || Ordinal.( << ) (Ordinal.Int (if _x_2 >= 0 then _x_2 else 0))
                                                          (Ordinal.Int (if _x_5 then if _x_4 then 0 else _x_3 else 0)))
                                                      || not ((not Is_a([], _x_0) && not _x_4) && (_x_5 || not _x_5))
                                                      expansions
                                                      []
                                                      rewrite_steps
                                                        forward_chaining
                                                        • unroll
                                                          expr
                                                          (|List.length_2018| (|get.::.0_1990| l_2010))
                                                          expansions
                                                          • unroll
                                                            expr
                                                            (|List.length_2018| (|get.::.1_1988| (|get.::.0_1990| l_2010)))
                                                            expansions
                                                            • unroll
                                                              expr
                                                              (let ((a!1 (>= (|List.length_2018| (|get.::.1_1988| (|get.::.0_1990| l_2010)))
                                                                             0))
                                                                …
                                                              expansions
                                                              • Unsat

                                                              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 (_cnt x)
                                                              sub ordinalOrdinal.Int (_cnt (Destruct(S, 0, x)))
                                                              path[not Is_a([], l) && not Is_a(Z, x)]
                                                              proof
                                                              detailed proof
                                                              ground_instances3
                                                              definitions0
                                                              inductions0
                                                              search_time
                                                              0.012s
                                                              details
                                                              Expand
                                                              smt_stats
                                                              num checks7
                                                              arith-make-feasible7
                                                              arith-max-columns10
                                                              rlimit count1720
                                                              arith-cheap-eqs1
                                                              mk clause11
                                                              datatype occurs check17
                                                              mk bool var48
                                                              arith-lower4
                                                              datatype splits2
                                                              decisions8
                                                              propagations5
                                                              arith-max-rows2
                                                              conflicts3
                                                              datatype accessor ax12
                                                              datatype constructor ax10
                                                              num allocs31778116
                                                              final checks4
                                                              added eqs40
                                                              del clause9
                                                              arith eq adapter3
                                                              arith-upper5
                                                              memory7.050000
                                                              max memory8.990000
                                                              Expand
                                                              • start[0.012s]
                                                                  let (_x_0 : int) = count.nat x in
                                                                  let (_x_1 : nat) = Destruct(S, 0, x) in
                                                                  let (_x_2 : int) = count.nat _x_1 in
                                                                  not Is_a([], l) && not Is_a(Z, x) && _x_0 >= 0 && _x_2 >= 0
                                                                  ==> not (not Is_a([], List.tl l) && not Is_a(Z, _x_1))
                                                                      || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                              • simplify
                                                                into
                                                                let (_x_0 : nat) = Destruct(S, 0, x) in
                                                                let (_x_1 : int) = count.nat _x_0 in
                                                                let (_x_2 : int) = count.nat x in
                                                                (not (not Is_a([], List.tl l) && not Is_a(Z, _x_0))
                                                                 || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                                                || not (((not Is_a([], l) && not Is_a(Z, x)) && _x_2 >= 0) && _x_1 >= 0)
                                                                expansions
                                                                []
                                                                rewrite_steps
                                                                  forward_chaining
                                                                  • unroll
                                                                    expr
                                                                    (|count.nat_17| x_2082)
                                                                    expansions
                                                                    • unroll
                                                                      expr
                                                                      (|count.nat_17| (|get.S.0_2072| x_2082))
                                                                      expansions
                                                                      • unroll
                                                                        expr
                                                                        (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.nat_17| (|get.S.0_2072| x_2082)))
                                                                                          (|O…
                                                                        expansions
                                                                        • Unsat

                                                                        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 (_cnt x)
                                                                        sub ordinalOrdinal.Int (_cnt (Destruct(S, 0, x)))
                                                                        path[not Is_a([], y) && not Is_a(Z, x)]
                                                                        proof
                                                                        detailed proof
                                                                        ground_instances3
                                                                        definitions0
                                                                        inductions0
                                                                        search_time
                                                                        0.012s
                                                                        details
                                                                        Expand
                                                                        smt_stats
                                                                        num checks7
                                                                        arith-make-feasible7
                                                                        arith-max-columns10
                                                                        rlimit count1720
                                                                        arith-cheap-eqs1
                                                                        mk clause11
                                                                        datatype occurs check17
                                                                        mk bool var48
                                                                        arith-lower4
                                                                        datatype splits2
                                                                        decisions8
                                                                        propagations5
                                                                        arith-max-rows2
                                                                        conflicts3
                                                                        datatype accessor ax12
                                                                        datatype constructor ax10
                                                                        num allocs40733575
                                                                        final checks4
                                                                        added eqs40
                                                                        del clause9
                                                                        arith eq adapter3
                                                                        arith-upper5
                                                                        memory7.300000
                                                                        max memory8.990000
                                                                        Expand
                                                                        • start[0.012s]
                                                                            let (_x_0 : int) = count.nat x in
                                                                            let (_x_1 : nat) = Destruct(S, 0, x) in
                                                                            let (_x_2 : int) = count.nat _x_1 in
                                                                            not Is_a([], y) && not Is_a(Z, x) && _x_0 >= 0 && _x_2 >= 0
                                                                            ==> not (not Is_a([], List.tl y) && not Is_a(Z, _x_1))
                                                                                || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                        • simplify
                                                                          into
                                                                          let (_x_0 : nat) = Destruct(S, 0, x) in
                                                                          let (_x_1 : int) = count.nat _x_0 in
                                                                          let (_x_2 : int) = count.nat x in
                                                                          (not (not Is_a([], List.tl y) && not Is_a(Z, _x_0))
                                                                           || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                                                          || not (((not Is_a([], y) && not Is_a(Z, x)) && _x_2 >= 0) && _x_1 >= 0)
                                                                          expansions
                                                                          []
                                                                          rewrite_steps
                                                                            forward_chaining
                                                                            • unroll
                                                                              expr
                                                                              (|count.nat_17| x_2132)
                                                                              expansions
                                                                              • unroll
                                                                                expr
                                                                                (|count.nat_17| (|get.S.0_2122| x_2132))
                                                                                expansions
                                                                                • unroll
                                                                                  expr
                                                                                  (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.nat_17| (|get.S.0_2122| x_2132)))
                                                                                                    (|O…
                                                                                  expansions
                                                                                  • Unsat

                                                                                  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 (_cnt y)
                                                                                  sub ordinalOrdinal.Int (_cnt (List.tl y))
                                                                                  path[not (x = List.hd y) && not Is_a([], y)]
                                                                                  proof
                                                                                  detailed proof
                                                                                  ground_instances3
                                                                                  definitions0
                                                                                  inductions0
                                                                                  search_time
                                                                                  0.012s
                                                                                  details
                                                                                  Expand
                                                                                  smt_stats
                                                                                  num checks7
                                                                                  arith-make-feasible7
                                                                                  arith-max-columns10
                                                                                  rlimit count1675
                                                                                  arith-cheap-eqs1
                                                                                  mk clause11
                                                                                  datatype occurs check12
                                                                                  mk bool var38
                                                                                  arith-lower4
                                                                                  datatype splits1
                                                                                  decisions4
                                                                                  propagations6
                                                                                  arith-max-rows2
                                                                                  conflicts3
                                                                                  datatype accessor ax7
                                                                                  datatype constructor ax5
                                                                                  num allocs51152526
                                                                                  final checks4
                                                                                  added eqs26
                                                                                  del clause9
                                                                                  arith eq adapter3
                                                                                  arith-upper5
                                                                                  memory7.540000
                                                                                  max memory8.990000
                                                                                  Expand
                                                                                  • start[0.012s]
                                                                                      let (_x_0 : int) = count.list (const 0) y in
                                                                                      let (_x_1 : ty_0 list) = List.tl y in
                                                                                      let (_x_2 : int) = count.list (const 0) _x_1 in
                                                                                      not (x = List.hd y) && not Is_a([], y) && _x_0 >= 0 && _x_2 >= 0
                                                                                      ==> not (not (x = List.hd _x_1) && not Is_a([], _x_1))
                                                                                          || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                                  • simplify
                                                                                    into
                                                                                    let (_x_0 : ty_0 list) = List.tl y in
                                                                                    let (_x_1 : int) = count.list (const 0) _x_0 in
                                                                                    let (_x_2 : int) = count.list (const 0) y in
                                                                                    (not (not (x = List.hd _x_0) && not Is_a([], _x_0))
                                                                                     || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                                                                    || not (((not (x = List.hd y) && not Is_a([], y)) && _x_2 >= 0) && _x_1 >= 0)
                                                                                    expansions
                                                                                    []
                                                                                    rewrite_steps
                                                                                      forward_chaining
                                                                                      • unroll
                                                                                        expr
                                                                                        (|`count.list (const 0)[0]`_2193| y_2181)
                                                                                        expansions
                                                                                        • unroll
                                                                                          expr
                                                                                          (|`count.list (const 0)[0]`_2193| (|get.::.1_2174| y_2181))
                                                                                          expansions
                                                                                          • unroll
                                                                                            expr
                                                                                            (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                                                                                (|`count.list (const 0)[0]`_2193| (|get.::.…
                                                                                            expansions
                                                                                            • Unsat

                                                                                            termination proof

                                                                                            Termination proof

                                                                                            call `unique (List.tl x)` from `unique x`
                                                                                            originalunique x
                                                                                            subunique (List.tl x)
                                                                                            original ordinalOrdinal.Int (_cnt x)
                                                                                            sub ordinalOrdinal.Int (_cnt (List.tl x))
                                                                                            path[not (elem (List.hd x) (List.tl x)) && not Is_a([], x)]
                                                                                            proof
                                                                                            detailed proof
                                                                                            ground_instances4
                                                                                            definitions0
                                                                                            inductions0
                                                                                            search_time
                                                                                            0.012s
                                                                                            details
                                                                                            Expand
                                                                                            smt_stats
                                                                                            num checks9
                                                                                            arith-make-feasible8
                                                                                            arith-max-columns10
                                                                                            rlimit count2055
                                                                                            arith-cheap-eqs1
                                                                                            mk clause11
                                                                                            datatype occurs check15
                                                                                            mk bool var44
                                                                                            arith-lower4
                                                                                            datatype splits1
                                                                                            decisions5
                                                                                            propagations6
                                                                                            arith-max-rows2
                                                                                            conflicts4
                                                                                            datatype accessor ax8
                                                                                            datatype constructor ax6
                                                                                            num allocs62287582
                                                                                            final checks5
                                                                                            added eqs28
                                                                                            del clause9
                                                                                            arith eq adapter3
                                                                                            arith-upper5
                                                                                            memory7.790000
                                                                                            max memory8.990000
                                                                                            Expand
                                                                                            • start[0.012s]
                                                                                                let (_x_0 : ty_0 list) = List.tl x in
                                                                                                let (_x_1 : int) = count.list (const 0) x in
                                                                                                let (_x_2 : int) = count.list (const 0) _x_0 in
                                                                                                not (elem (List.hd x) _x_0) && not Is_a([], x) && _x_1 >= 0 && _x_2 >= 0
                                                                                                ==> not (not (elem (List.hd _x_0) (List.tl _x_0)) && not Is_a([], _x_0))
                                                                                                    || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_1)
                                                                                            • simplify
                                                                                              into
                                                                                              let (_x_0 : ty_0 list) = List.tl x in
                                                                                              let (_x_1 : int) = count.list (const 0) _x_0 in
                                                                                              let (_x_2 : int) = count.list (const 0) x in
                                                                                              (not (not (elem (List.hd _x_0) (List.tl _x_0)) && not Is_a([], _x_0))
                                                                                               || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                                                                              || not
                                                                                                 (((not (elem (List.hd x) _x_0) && not Is_a([], x)) && _x_2 >= 0)
                                                                                                  && _x_1 >= 0)
                                                                                              expansions
                                                                                              []
                                                                                              rewrite_steps
                                                                                                forward_chaining
                                                                                                • unroll
                                                                                                  expr
                                                                                                  (elem_2230 (|get.::.0_2224| x_2235) (|get.::.1_2225| x_2235))
                                                                                                  expansions
                                                                                                  • unroll
                                                                                                    expr
                                                                                                    (|`count.list (const 0)[0]`_2246| x_2235)
                                                                                                    expansions
                                                                                                    • unroll
                                                                                                      expr
                                                                                                      (|`count.list (const 0)[0]`_2246| (|get.::.1_2225| x_2235))
                                                                                                      expansions
                                                                                                      • unroll
                                                                                                        expr
                                                                                                        (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                                                                                            (|`count.list (const 0)[0]`_2246| (|get.::.…
                                                                                                        expansions
                                                                                                        • Unsat

                                                                                                        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 (_cnt l)
                                                                                                        sub ordinalOrdinal.Int (_cnt (List.tl l))
                                                                                                        path[not Is_a([], l)]
                                                                                                        proof
                                                                                                        detailed proof
                                                                                                        ground_instances3
                                                                                                        definitions0
                                                                                                        inductions0
                                                                                                        search_time
                                                                                                        0.011s
                                                                                                        details
                                                                                                        Expand
                                                                                                        smt_stats
                                                                                                        num checks7
                                                                                                        arith-make-feasible7
                                                                                                        arith-max-columns11
                                                                                                        rlimit count1660
                                                                                                        arith-cheap-eqs1
                                                                                                        mk clause10
                                                                                                        datatype occurs check14
                                                                                                        mk bool var43
                                                                                                        arith-lower4
                                                                                                        datatype splits3
                                                                                                        decisions11
                                                                                                        propagations5
                                                                                                        arith-max-rows2
                                                                                                        conflicts3
                                                                                                        datatype accessor ax10
                                                                                                        datatype constructor ax11
                                                                                                        num allocs74556335
                                                                                                        final checks4
                                                                                                        added eqs36
                                                                                                        del clause8
                                                                                                        arith eq adapter3
                                                                                                        arith-upper5
                                                                                                        memory8.040000
                                                                                                        max memory8.990000
                                                                                                        Expand
                                                                                                        • start[0.011s]
                                                                                                            let (_x_0 : int) = count.list (count.option (const 0)) l in
                                                                                                            let (_x_1 : ty_0 option list) = List.tl l in
                                                                                                            let (_x_2 : int) = count.list (count.option (const 0)) _x_1 in
                                                                                                            not Is_a([], l) && _x_0 >= 0 && _x_2 >= 0
                                                                                                            ==> Is_a([], _x_1) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                                                        • simplify
                                                                                                          into
                                                                                                          let (_x_0 : ty_0 option list) = List.tl l in
                                                                                                          let (_x_1 : int) = count.list (count.option (const 0)) _x_0 in
                                                                                                          let (_x_2 : int) = count.list (count.option (const 0)) l in
                                                                                                          (Is_a([], _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                                                                                          || not ((not Is_a([], l) && _x_2 >= 0) && _x_1 >= 0)
                                                                                                          expansions
                                                                                                          []
                                                                                                          rewrite_steps
                                                                                                            forward_chaining
                                                                                                            • unroll
                                                                                                              expr
                                                                                                              (|`count.list clos_976953524[0]`_2302| l_2291)
                                                                                                              expansions
                                                                                                              • unroll
                                                                                                                expr
                                                                                                                (|`count.list clos_976953524[0]`_2302| (|get.::.1_2281| l_2291))
                                                                                                                expansions
                                                                                                                • unroll
                                                                                                                  expr
                                                                                                                  (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                                                                                                      (|`count.list clos_976953524[0]`_2302|
                                                                                                                      …
                                                                                                                  expansions
                                                                                                                  • Unsat

                                                                                                                  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 (_cnt _x)
                                                                                                                  sub ordinalOrdinal.Int (_cnt (List.tl _x))
                                                                                                                  path[not Is_a([], _x)]
                                                                                                                  proof
                                                                                                                  detailed proof
                                                                                                                  ground_instances3
                                                                                                                  definitions0
                                                                                                                  inductions0
                                                                                                                  search_time
                                                                                                                  0.028s
                                                                                                                  details
                                                                                                                  Expand
                                                                                                                  smt_stats
                                                                                                                  num checks8
                                                                                                                  arith-make-feasible19
                                                                                                                  arith-max-columns16
                                                                                                                  arith-conflicts2
                                                                                                                  rlimit count2373
                                                                                                                  mk clause21
                                                                                                                  datatype occurs check14
                                                                                                                  mk bool var69
                                                                                                                  arith-lower16
                                                                                                                  arith-diseq1
                                                                                                                  datatype splits3
                                                                                                                  decisions19
                                                                                                                  propagations15
                                                                                                                  arith-max-rows4
                                                                                                                  conflicts7
                                                                                                                  datatype accessor ax10
                                                                                                                  datatype constructor ax11
                                                                                                                  num allocs88464328
                                                                                                                  final checks4
                                                                                                                  added eqs54
                                                                                                                  del clause14
                                                                                                                  arith eq adapter11
                                                                                                                  arith-upper13
                                                                                                                  memory8.460000
                                                                                                                  max memory8.990000
                                                                                                                  Expand
                                                                                                                  • start[0.028s]
                                                                                                                      let (_x_0 : int) = count.list (count.list (const 0)) _x in
                                                                                                                      let (_x_1 : ty_0 list list) = List.tl _x in
                                                                                                                      let (_x_2 : int) = count.list (count.list (const 0)) _x_1 in
                                                                                                                      not Is_a([], _x) && _x_0 >= 0 && _x_2 >= 0
                                                                                                                      ==> Is_a([], _x_1) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                                                                  • simplify
                                                                                                                    into
                                                                                                                    let (_x_0 : ty_0 list list) = List.tl _x in
                                                                                                                    let (_x_1 : int) = count.list (count.list (const 0)) _x_0 in
                                                                                                                    let (_x_2 : int) = count.list (count.list (const 0)) _x in
                                                                                                                    (Is_a([], _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                                                                                                    || not ((not Is_a([], _x) && _x_2 >= 0) && _x_1 >= 0)
                                                                                                                    expansions
                                                                                                                    []
                                                                                                                    rewrite_steps
                                                                                                                      forward_chaining
                                                                                                                      • unroll
                                                                                                                        expr
                                                                                                                        (|`count.list clos_790807200[0]`_2390| _x_2379)
                                                                                                                        expansions
                                                                                                                        • unroll
                                                                                                                          expr
                                                                                                                          (|`count.list clos_790807200[0]`_2390| (|get.::.1_2367| _x_2379))
                                                                                                                          expansions
                                                                                                                          • unroll
                                                                                                                            expr
                                                                                                                            (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                                                                                                                (|`count.list clos_790807200[0]`_2390|
                                                                                                                                …
                                                                                                                            expansions
                                                                                                                            • Unsat

                                                                                                                            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 (_cnt _x)
                                                                                                                            sub ordinalOrdinal.Int (_cnt (List.tl _x))
                                                                                                                            path[not Is_a([], _x)]
                                                                                                                            proof
                                                                                                                            detailed proof
                                                                                                                            ground_instances3
                                                                                                                            definitions0
                                                                                                                            inductions0
                                                                                                                            search_time
                                                                                                                            0.012s
                                                                                                                            details
                                                                                                                            Expand
                                                                                                                            smt_stats
                                                                                                                            num checks8
                                                                                                                            arith-make-feasible19
                                                                                                                            arith-max-columns16
                                                                                                                            arith-conflicts2
                                                                                                                            rlimit count2373
                                                                                                                            mk clause21
                                                                                                                            datatype occurs check14
                                                                                                                            mk bool var69
                                                                                                                            arith-lower16
                                                                                                                            arith-diseq1
                                                                                                                            datatype splits3
                                                                                                                            decisions19
                                                                                                                            propagations15
                                                                                                                            arith-max-rows4
                                                                                                                            conflicts7
                                                                                                                            datatype accessor ax10
                                                                                                                            datatype constructor ax11
                                                                                                                            num allocs103363369
                                                                                                                            final checks4
                                                                                                                            added eqs54
                                                                                                                            del clause14
                                                                                                                            arith eq adapter11
                                                                                                                            arith-upper13
                                                                                                                            memory8.720000
                                                                                                                            max memory8.990000
                                                                                                                            Expand
                                                                                                                            • start[0.012s]
                                                                                                                                let (_x_0 : int) = count.list (count.list (const 0)) _x in
                                                                                                                                let (_x_1 : ty_0 list list) = List.tl _x in
                                                                                                                                let (_x_2 : int) = count.list (count.list (const 0)) _x_1 in
                                                                                                                                not Is_a([], _x) && _x_0 >= 0 && _x_2 >= 0
                                                                                                                                ==> Is_a([], _x_1) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                                                                            • simplify
                                                                                                                              into
                                                                                                                              let (_x_0 : ty_0 list list) = List.tl _x in
                                                                                                                              let (_x_1 : int) = count.list (count.list (const 0)) _x_0 in
                                                                                                                              let (_x_2 : int) = count.list (count.list (const 0)) _x in
                                                                                                                              (Is_a([], _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                                                                                                              || not ((not Is_a([], _x) && _x_2 >= 0) && _x_1 >= 0)
                                                                                                                              expansions
                                                                                                                              []
                                                                                                                              rewrite_steps
                                                                                                                                forward_chaining
                                                                                                                                • unroll
                                                                                                                                  expr
                                                                                                                                  (|`count.list clos_661142004[0]`_2458| _x_2447)
                                                                                                                                  expansions
                                                                                                                                  • unroll
                                                                                                                                    expr
                                                                                                                                    (|`count.list clos_661142004[0]`_2458| (|get.::.1_2429| _x_2447))
                                                                                                                                    expansions
                                                                                                                                    • unroll
                                                                                                                                      expr
                                                                                                                                      (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                                                                                                                          (|`count.list clos_661142004[0]`_2458|
                                                                                                                                          …
                                                                                                                                      expansions
                                                                                                                                      • Unsat

                                                                                                                                      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 (_cnt _x)
                                                                                                                                      sub ordinalOrdinal.Int (_cnt (List.tl _x))
                                                                                                                                      path[not Is_a([], _x)]
                                                                                                                                      proof
                                                                                                                                      detailed proof
                                                                                                                                      ground_instances3
                                                                                                                                      definitions0
                                                                                                                                      inductions0
                                                                                                                                      search_time
                                                                                                                                      0.023s
                                                                                                                                      details
                                                                                                                                      Expand
                                                                                                                                      smt_stats
                                                                                                                                      num checks8
                                                                                                                                      arith-make-feasible19
                                                                                                                                      arith-max-columns16
                                                                                                                                      arith-conflicts2
                                                                                                                                      rlimit count2373
                                                                                                                                      mk clause21
                                                                                                                                      datatype occurs check14
                                                                                                                                      mk bool var69
                                                                                                                                      arith-lower16
                                                                                                                                      arith-diseq1
                                                                                                                                      datatype splits3
                                                                                                                                      decisions19
                                                                                                                                      propagations15
                                                                                                                                      arith-max-rows4
                                                                                                                                      conflicts7
                                                                                                                                      datatype accessor ax10
                                                                                                                                      datatype constructor ax11
                                                                                                                                      num allocs119412594
                                                                                                                                      final checks4
                                                                                                                                      added eqs54
                                                                                                                                      del clause14
                                                                                                                                      arith eq adapter11
                                                                                                                                      arith-upper13
                                                                                                                                      memory8.980000
                                                                                                                                      max memory8.990000
                                                                                                                                      Expand
                                                                                                                                      • start[0.023s]
                                                                                                                                          let (_x_0 : int) = count.list (count.list (const 0)) _x in
                                                                                                                                          let (_x_1 : ty_0 list list) = List.tl _x in
                                                                                                                                          let (_x_2 : int) = count.list (count.list (const 0)) _x_1 in
                                                                                                                                          not Is_a([], _x) && _x_0 >= 0 && _x_2 >= 0
                                                                                                                                          ==> Is_a([], _x_1) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                                                                                      • simplify
                                                                                                                                        into
                                                                                                                                        let (_x_0 : ty_0 list list) = List.tl _x in
                                                                                                                                        let (_x_1 : int) = count.list (count.list (const 0)) _x_0 in
                                                                                                                                        let (_x_2 : int) = count.list (count.list (const 0)) _x in
                                                                                                                                        (Is_a([], _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                                                                                                                        || not ((not Is_a([], _x) && _x_2 >= 0) && _x_1 >= 0)
                                                                                                                                        expansions
                                                                                                                                        []
                                                                                                                                        rewrite_steps
                                                                                                                                          forward_chaining
                                                                                                                                          • unroll
                                                                                                                                            expr
                                                                                                                                            (|`count.list clos_388039378[0]`_2520| _x_2509)
                                                                                                                                            expansions
                                                                                                                                            • unroll
                                                                                                                                              expr
                                                                                                                                              (|`count.list clos_388039378[0]`_2520| (|get.::.1_2497| _x_2509))
                                                                                                                                              expansions
                                                                                                                                              • unroll
                                                                                                                                                expr
                                                                                                                                                (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                                                                                                                                    (|`count.list clos_388039378[0]`_2520|
                                                                                                                                                    …
                                                                                                                                                expansions
                                                                                                                                                • Unsat

                                                                                                                                                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 (_cnt _x)
                                                                                                                                                sub ordinalOrdinal.Int (_cnt (List.tl (List.tl (List.tl _x))))
                                                                                                                                                path[not Is_a([], List.tl (List.tl _x)) && not Is_a([], List.tl _x) && not Is_a([], _x)]
                                                                                                                                                proof
                                                                                                                                                detailed proof
                                                                                                                                                ground_instances8
                                                                                                                                                definitions0
                                                                                                                                                inductions0
                                                                                                                                                search_time
                                                                                                                                                0.027s
                                                                                                                                                details
                                                                                                                                                Expand
                                                                                                                                                smt_stats
                                                                                                                                                num checks18
                                                                                                                                                arith-assume-eqs8
                                                                                                                                                arith-make-feasible236
                                                                                                                                                arith-max-columns54
                                                                                                                                                arith-conflicts17
                                                                                                                                                rlimit count13124
                                                                                                                                                arith-cheap-eqs72
                                                                                                                                                mk clause321
                                                                                                                                                datatype occurs check75
                                                                                                                                                mk bool var669
                                                                                                                                                arith-lower197
                                                                                                                                                arith-diseq31
                                                                                                                                                datatype splits19
                                                                                                                                                decisions308
                                                                                                                                                arith-propagations22
                                                                                                                                                propagations322
                                                                                                                                                interface eqs8
                                                                                                                                                arith-bound-propagations-cheap22
                                                                                                                                                arith-max-rows25
                                                                                                                                                conflicts51
                                                                                                                                                datatype accessor ax52
                                                                                                                                                minimized lits7
                                                                                                                                                arith-bound-propagations-lp28
                                                                                                                                                datatype constructor ax133
                                                                                                                                                num allocs130696453
                                                                                                                                                final checks27
                                                                                                                                                added eqs716
                                                                                                                                                del clause180
                                                                                                                                                arith eq adapter170
                                                                                                                                                arith-upper227
                                                                                                                                                time0.001000
                                                                                                                                                memory12.330000
                                                                                                                                                max memory12.330000
                                                                                                                                                Expand
                                                                                                                                                • start[0.027s]
                                                                                                                                                    let (_x_0 : ty_0 list list) = List.tl _x in
                                                                                                                                                    let (_x_1 : ty_0 list list) = List.tl _x_0 in
                                                                                                                                                    let (_x_2 : int) = count.list (count.list (const 0)) _x in
                                                                                                                                                    let (_x_3 : ty_0 list list) = List.tl _x_1 in
                                                                                                                                                    let (_x_4 : int) = count.list (count.list (const 0)) _x_3 in
                                                                                                                                                    let (_x_5 : ty_0 list list) = List.tl _x_3 in
                                                                                                                                                    not Is_a([], _x_1)
                                                                                                                                                    && not Is_a([], _x_0) && not Is_a([], _x) && _x_2 >= 0 && _x_4 >= 0
                                                                                                                                                    ==> not
                                                                                                                                                        (not Is_a([], List.tl _x_5) && not Is_a([], _x_5) && not Is_a([], _x_3))
                                                                                                                                                        || Ordinal.( << ) (Ordinal.Int _x_4) (Ordinal.Int _x_2)
                                                                                                                                                • simplify
                                                                                                                                                  into
                                                                                                                                                  let (_x_0 : ty_0 list list) = List.tl _x in
                                                                                                                                                  let (_x_1 : ty_0 list list) = List.tl _x_0 in
                                                                                                                                                  let (_x_2 : ty_0 list list) = List.tl _x_1 in
                                                                                                                                                  let (_x_3 : int) = count.list (count.list (const 0)) _x_2 in
                                                                                                                                                  let (_x_4 : int) = count.list (count.list (const 0)) _x in
                                                                                                                                                  let (_x_5 : ty_0 list list) = List.tl _x_2 in
                                                                                                                                                  (Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_4)
                                                                                                                                                   || not
                                                                                                                                                      ((not Is_a([], List.tl _x_5) && not Is_a([], _x_5)) && not Is_a([], _x_2)))
                                                                                                                                                  || not
                                                                                                                                                     ((((not Is_a([], _x_1) && not Is_a([], _x_0)) && not Is_a([], _x))
                                                                                                                                                       && _x_4 >= 0)
                                                                                                                                                      && _x_3 >= 0)
                                                                                                                                                  expansions
                                                                                                                                                  []
                                                                                                                                                  rewrite_steps
                                                                                                                                                    forward_chaining
                                                                                                                                                    • unroll
                                                                                                                                                      expr
                                                                                                                                                      (|`count.list clos_592014680[0]`_2584| _x_2573)
                                                                                                                                                      expansions
                                                                                                                                                      • unroll
                                                                                                                                                        expr
                                                                                                                                                        (|`count.list clos_592014680[0]`_2584|
                                                                                                                                                          (|get.::.1_2559| (|get.::.1_2559| (|get.::.1_2559| _x_2573)…
                                                                                                                                                        expansions
                                                                                                                                                        • unroll
                                                                                                                                                          expr
                                                                                                                                                          (let ((a!1 (|`count.list clos_592014680[0]`_2584|
                                                                                                                                                                       (|get.::.1_2559| (|get.::.1_2559| (|g…
                                                                                                                                                          expansions
                                                                                                                                                          • unroll
                                                                                                                                                            expr
                                                                                                                                                            (|`count.list clos_592014680[0]`_2584| (|get.::.1_2559| _x_2573))
                                                                                                                                                            expansions
                                                                                                                                                            • unroll
                                                                                                                                                              expr
                                                                                                                                                              (|`count.list (const 0)[0]`_2588| (|get.::.0_2558| _x_2573))
                                                                                                                                                              expansions
                                                                                                                                                              • unroll
                                                                                                                                                                expr
                                                                                                                                                                (let ((a!1 (|get.::.1_2559| (|get.::.1_2559| (|get.::.1_2559| (|get.::.1_2559| _x_2573))))))
                                                                                                                                                                  (|`co…
                                                                                                                                                                expansions
                                                                                                                                                                • unroll
                                                                                                                                                                  expr
                                                                                                                                                                  (let ((a!1 (|get.::.0_2558| (|get.::.1_2559| (|get.::.1_2559| (|get.::.1_2559| _x_2573))))))
                                                                                                                                                                    (|`co…
                                                                                                                                                                  expansions
                                                                                                                                                                  • unroll
                                                                                                                                                                    expr
                                                                                                                                                                    (|`count.list clos_592014680[0]`_2584|
                                                                                                                                                                      (|get.::.1_2559| (|get.::.1_2559| _x_2573)))
                                                                                                                                                                    expansions
                                                                                                                                                                    • Unsat

                                                                                                                                                                    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 -> 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 -> 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 (_cnt l1)
                                                                                                                                                                    sub ordinalOrdinal.Int (_cnt (List.tl l1))
                                                                                                                                                                    path[not Is_a([], l2) && not Is_a([], l1)]
                                                                                                                                                                    proof
                                                                                                                                                                    detailed proof
                                                                                                                                                                    ground_instances3
                                                                                                                                                                    definitions0
                                                                                                                                                                    inductions0
                                                                                                                                                                    search_time
                                                                                                                                                                    0.026s
                                                                                                                                                                    details
                                                                                                                                                                    Expand
                                                                                                                                                                    smt_stats
                                                                                                                                                                    num checks7
                                                                                                                                                                    arith-make-feasible7
                                                                                                                                                                    arith-max-columns10
                                                                                                                                                                    rlimit count1730
                                                                                                                                                                    arith-cheap-eqs1
                                                                                                                                                                    mk clause11
                                                                                                                                                                    datatype occurs check17
                                                                                                                                                                    mk bool var50
                                                                                                                                                                    arith-lower4
                                                                                                                                                                    datatype splits2
                                                                                                                                                                    decisions8
                                                                                                                                                                    propagations5
                                                                                                                                                                    arith-max-rows2
                                                                                                                                                                    conflicts3
                                                                                                                                                                    datatype accessor ax12
                                                                                                                                                                    datatype constructor ax10
                                                                                                                                                                    num allocs155901061
                                                                                                                                                                    final checks4
                                                                                                                                                                    added eqs42
                                                                                                                                                                    del clause9
                                                                                                                                                                    arith eq adapter3
                                                                                                                                                                    arith-upper5
                                                                                                                                                                    memory13.670000
                                                                                                                                                                    max memory13.670000
                                                                                                                                                                    Expand
                                                                                                                                                                    • start[0.026s]
                                                                                                                                                                        let (_x_0 : int) = count.list (const 0) l1 in
                                                                                                                                                                        let (_x_1 : ty_0 list) = List.tl l1 in
                                                                                                                                                                        let (_x_2 : int) = count.list (const 0) _x_1 in
                                                                                                                                                                        not Is_a([], l2) && not Is_a([], l1) && _x_0 >= 0 && _x_2 >= 0
                                                                                                                                                                        ==> not (not Is_a([], List.tl l2) && not Is_a([], _x_1))
                                                                                                                                                                            || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                                                                                                                    • simplify
                                                                                                                                                                      into
                                                                                                                                                                      let (_x_0 : ty_0 list) = List.tl l1 in
                                                                                                                                                                      let (_x_1 : int) = count.list (const 0) _x_0 in
                                                                                                                                                                      let (_x_2 : int) = count.list (const 0) l1 in
                                                                                                                                                                      (not (not Is_a([], List.tl l2) && not Is_a([], _x_0))
                                                                                                                                                                       || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                                                                                                                                                      || not (((not Is_a([], l2) && not Is_a([], l1)) && _x_2 >= 0) && _x_1 >= 0)
                                                                                                                                                                      expansions
                                                                                                                                                                      []
                                                                                                                                                                      rewrite_steps
                                                                                                                                                                        forward_chaining
                                                                                                                                                                        • unroll
                                                                                                                                                                          expr
                                                                                                                                                                          (|`count.list (const 0)[0]`_2963| l1_2950)
                                                                                                                                                                          expansions
                                                                                                                                                                          • unroll
                                                                                                                                                                            expr
                                                                                                                                                                            (|`count.list (const 0)[0]`_2963| (|get.::.1_2926| l1_2950))
                                                                                                                                                                            expansions
                                                                                                                                                                            • unroll
                                                                                                                                                                              expr
                                                                                                                                                                              (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                                                                                                                                                                  (|`count.list (const 0)[0]`_2963| (|get.::.…
                                                                                                                                                                              expansions
                                                                                                                                                                              • Unsat

                                                                                                                                                                              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 (_cnt y)
                                                                                                                                                                              sub ordinalOrdinal.Int (_cnt (List.tl y))
                                                                                                                                                                              path[Is_a(None, (List.hd y).0) && not Is_a([], y)]
                                                                                                                                                                              proof
                                                                                                                                                                              detailed proof
                                                                                                                                                                              ground_instances3
                                                                                                                                                                              definitions0
                                                                                                                                                                              inductions0
                                                                                                                                                                              search_time
                                                                                                                                                                              0.016s
                                                                                                                                                                              details
                                                                                                                                                                              Expand
                                                                                                                                                                              smt_stats
                                                                                                                                                                              num checks7
                                                                                                                                                                              arith-make-feasible8
                                                                                                                                                                              arith-max-columns12
                                                                                                                                                                              rlimit count6624
                                                                                                                                                                              arith-cheap-eqs2
                                                                                                                                                                              mk clause26
                                                                                                                                                                              datatype occurs check24
                                                                                                                                                                              mk bool var86
                                                                                                                                                                              arith-lower4
                                                                                                                                                                              datatype splits6
                                                                                                                                                                              decisions16
                                                                                                                                                                              propagations23
                                                                                                                                                                              arith-max-rows3
                                                                                                                                                                              conflicts4
                                                                                                                                                                              datatype accessor ax18
                                                                                                                                                                              datatype constructor ax19
                                                                                                                                                                              num allocs199165558
                                                                                                                                                                              final checks6
                                                                                                                                                                              added eqs81
                                                                                                                                                                              del clause6
                                                                                                                                                                              arith eq adapter3
                                                                                                                                                                              arith-upper5
                                                                                                                                                                              memory19.230000
                                                                                                                                                                              max memory19.230000
                                                                                                                                                                              Expand
                                                                                                                                                                              • start[0.016s]
                                                                                                                                                                                  let (_x_0 : int) = count.list anon_fun._cnt.1 y in
                                                                                                                                                                                  let (_x_1 : (ty_0 option * ty_0 option) list) = List.tl y in
                                                                                                                                                                                  let (_x_2 : int) = count.list anon_fun._cnt.1 _x_1 in
                                                                                                                                                                                  let (_x_3 : (ty_0 option * ty_0 option)) = List.hd _x_1 in
                                                                                                                                                                                  let (_x_4 : ty_0 option) = _x_3.0 in
                                                                                                                                                                                  let (_x_5 : bool) = Is_a(None, _x_4) in
                                                                                                                                                                                  let (_x_6 : bool) = not Is_a([], _x_1) in
                                                                                                                                                                                  let (_x_7 : ty_0 option) = _x_3.1 in
                                                                                                                                                                                  let (_x_8 : bool) = Is_a(None, _x_7) in
                                                                                                                                                                                  let (_x_9 : bool) = not _x_5 && _x_6 in
                                                                                                                                                                                  Is_a(None, (List.hd y).0) && not Is_a([], y) && _x_0 >= 0 && _x_2 >= 0
                                                                                                                                                                                  ==> not (_x_5 && _x_6)
                                                                                                                                                                                      && not (_x_8 && _x_9)
                                                                                                                                                                                         && not (Option.get _x_4 = Option.get _x_7 && not _x_8 && _x_9)
                                                                                                                                                                                      || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                                                                                                                              • simplify
                                                                                                                                                                                into
                                                                                                                                                                                let (_x_0 : (ty_0 option * ty_0 option) list) = List.tl y in
                                                                                                                                                                                let (_x_1 : (ty_0 option * ty_0 option)) = List.hd _x_0 in
                                                                                                                                                                                let (_x_2 : ty_0 option) = _x_1.0 in
                                                                                                                                                                                let (_x_3 : bool) = Is_a(None, _x_2) in
                                                                                                                                                                                let (_x_4 : bool) = not Is_a([], _x_0) in
                                                                                                                                                                                let (_x_5 : ty_0 option) = _x_1.1 in
                                                                                                                                                                                let (_x_6 : bool) = Is_a(None, _x_5) in
                                                                                                                                                                                let (_x_7 : bool) = not _x_3 in
                                                                                                                                                                                let (_x_8 : int) = count.list anon_fun._cnt.1 _x_0 in
                                                                                                                                                                                let (_x_9 : int) = count.list anon_fun._cnt.1 y in
                                                                                                                                                                                ((not (_x_3 && _x_4) && not ((_x_6 && _x_7) && _x_4))
                                                                                                                                                                                 && not (((Option.get _x_2 = Option.get _x_5 && not _x_6) && _x_7) && _x_4)
                                                                                                                                                                                 || Ordinal.( << ) (Ordinal.Int _x_8) (Ordinal.Int _x_9))
                                                                                                                                                                                || not
                                                                                                                                                                                   (((Is_a(None, (List.hd y).0) && not Is_a([], y)) && _x_9 >= 0)
                                                                                                                                                                                    && _x_8 >= 0)
                                                                                                                                                                                expansions
                                                                                                                                                                                []
                                                                                                                                                                                rewrite_steps
                                                                                                                                                                                  forward_chaining
                                                                                                                                                                                  • unroll
                                                                                                                                                                                    expr
                                                                                                                                                                                    (|`count.list anon_fun._cnt.1[0]`_3078| y_3010)
                                                                                                                                                                                    expansions
                                                                                                                                                                                    • unroll
                                                                                                                                                                                      expr
                                                                                                                                                                                      (|`count.list anon_fun._cnt.1[0]`_3078| (|get.::.1_3001| y_3010))
                                                                                                                                                                                      expansions
                                                                                                                                                                                      • unroll
                                                                                                                                                                                        expr
                                                                                                                                                                                        (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                                                                                                                                                                            (|`count.list anon_fun._cnt.1[0]`_3078|
                                                                                                                                                                                           …
                                                                                                                                                                                        expansions
                                                                                                                                                                                        • Unsat

                                                                                                                                                                                        call `match_cols (List.tl y)` from `match_cols y`
                                                                                                                                                                                        originalmatch_cols y
                                                                                                                                                                                        submatch_cols (List.tl y)
                                                                                                                                                                                        original ordinalOrdinal.Int (_cnt y)
                                                                                                                                                                                        sub ordinalOrdinal.Int (_cnt (List.tl y))
                                                                                                                                                                                        path[Is_a(None, (List.hd y).1) && not Is_a(None, (List.hd y).0) && not Is_a([], y)]
                                                                                                                                                                                        proof
                                                                                                                                                                                        detailed proof
                                                                                                                                                                                        ground_instances3
                                                                                                                                                                                        definitions0
                                                                                                                                                                                        inductions0
                                                                                                                                                                                        search_time
                                                                                                                                                                                        0.016s
                                                                                                                                                                                        details
                                                                                                                                                                                        Expand
                                                                                                                                                                                        smt_stats
                                                                                                                                                                                        num checks7
                                                                                                                                                                                        arith-make-feasible8
                                                                                                                                                                                        arith-max-columns12
                                                                                                                                                                                        rlimit count4445
                                                                                                                                                                                        arith-cheap-eqs2
                                                                                                                                                                                        mk clause26
                                                                                                                                                                                        datatype occurs check21
                                                                                                                                                                                        mk bool var84
                                                                                                                                                                                        arith-lower4
                                                                                                                                                                                        datatype splits3
                                                                                                                                                                                        decisions12
                                                                                                                                                                                        propagations24
                                                                                                                                                                                        arith-max-rows3
                                                                                                                                                                                        conflicts4
                                                                                                                                                                                        datatype accessor ax19
                                                                                                                                                                                        datatype constructor ax17
                                                                                                                                                                                        num allocs187846449
                                                                                                                                                                                        final checks6
                                                                                                                                                                                        added eqs79
                                                                                                                                                                                        del clause6
                                                                                                                                                                                        arith eq adapter3
                                                                                                                                                                                        arith-upper5
                                                                                                                                                                                        memory16.620000
                                                                                                                                                                                        max memory16.620000
                                                                                                                                                                                        Expand
                                                                                                                                                                                        • start[0.016s]
                                                                                                                                                                                            let (_x_0 : (ty_0 option * ty_0 option)) = List.hd y in
                                                                                                                                                                                            let (_x_1 : int) = count.list anon_fun._cnt.1 y in
                                                                                                                                                                                            let (_x_2 : (ty_0 option * ty_0 option) list) = List.tl y in
                                                                                                                                                                                            let (_x_3 : int) = count.list anon_fun._cnt.1 _x_2 in
                                                                                                                                                                                            let (_x_4 : (ty_0 option * ty_0 option)) = List.hd _x_2 in
                                                                                                                                                                                            let (_x_5 : ty_0 option) = _x_4.0 in
                                                                                                                                                                                            let (_x_6 : bool) = Is_a(None, _x_5) in
                                                                                                                                                                                            let (_x_7 : bool) = not Is_a([], _x_2) in
                                                                                                                                                                                            let (_x_8 : ty_0 option) = _x_4.1 in
                                                                                                                                                                                            let (_x_9 : bool) = Is_a(None, _x_8) in
                                                                                                                                                                                            let (_x_10 : bool) = not _x_6 && _x_7 in
                                                                                                                                                                                            Is_a(None, _x_0.1)
                                                                                                                                                                                            && not Is_a(None, _x_0.0) && not Is_a([], y) && _x_1 >= 0 && _x_3 >= 0
                                                                                                                                                                                            ==> not (_x_6 && _x_7)
                                                                                                                                                                                                && not (_x_9 && _x_10)
                                                                                                                                                                                                   && not (Option.get _x_5 = Option.get _x_8 && not _x_9 && _x_10)
                                                                                                                                                                                                || Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_1)
                                                                                                                                                                                        • simplify
                                                                                                                                                                                          into
                                                                                                                                                                                          let (_x_0 : (ty_0 option * ty_0 option) list) = List.tl y in
                                                                                                                                                                                          let (_x_1 : (ty_0 option * ty_0 option)) = List.hd _x_0 in
                                                                                                                                                                                          let (_x_2 : ty_0 option) = _x_1.0 in
                                                                                                                                                                                          let (_x_3 : bool) = Is_a(None, _x_2) in
                                                                                                                                                                                          let (_x_4 : bool) = not Is_a([], _x_0) in
                                                                                                                                                                                          let (_x_5 : ty_0 option) = _x_1.1 in
                                                                                                                                                                                          let (_x_6 : bool) = Is_a(None, _x_5) in
                                                                                                                                                                                          let (_x_7 : bool) = not _x_3 in
                                                                                                                                                                                          let (_x_8 : int) = count.list anon_fun._cnt.1 _x_0 in
                                                                                                                                                                                          let (_x_9 : int) = count.list anon_fun._cnt.1 y in
                                                                                                                                                                                          let (_x_10 : (ty_0 option * ty_0 option)) = List.hd y in
                                                                                                                                                                                          ((not (_x_3 && _x_4) && not ((_x_6 && _x_7) && _x_4))
                                                                                                                                                                                           && not (((Option.get _x_2 = Option.get _x_5 && not _x_6) && _x_7) && _x_4)
                                                                                                                                                                                           || Ordinal.( << ) (Ordinal.Int _x_8) (Ordinal.Int _x_9))
                                                                                                                                                                                          || not
                                                                                                                                                                                             ((((Is_a(None, _x_10.1) && not Is_a(None, _x_10.0)) && not Is_a([], y))
                                                                                                                                                                                               && _x_9 >= 0)
                                                                                                                                                                                              && _x_8 >= 0)
                                                                                                                                                                                          expansions
                                                                                                                                                                                          []
                                                                                                                                                                                          rewrite_steps
                                                                                                                                                                                            forward_chaining
                                                                                                                                                                                            • unroll
                                                                                                                                                                                              expr
                                                                                                                                                                                              (|`count.list anon_fun._cnt.1[0]`_3055| y_3010)
                                                                                                                                                                                              expansions
                                                                                                                                                                                              • unroll
                                                                                                                                                                                                expr
                                                                                                                                                                                                (|`count.list anon_fun._cnt.1[0]`_3055| (|get.::.1_3001| y_3010))
                                                                                                                                                                                                expansions
                                                                                                                                                                                                • unroll
                                                                                                                                                                                                  expr
                                                                                                                                                                                                  (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                                                                                                                                                                                      (|`count.list anon_fun._cnt.1[0]`_3055|
                                                                                                                                                                                                     …
                                                                                                                                                                                                  expansions
                                                                                                                                                                                                  • Unsat

                                                                                                                                                                                                  call `match_cols (List.tl y)` from `match_cols y`
                                                                                                                                                                                                  originalmatch_cols y
                                                                                                                                                                                                  submatch_cols (List.tl y)
                                                                                                                                                                                                  original ordinalOrdinal.Int (_cnt y)
                                                                                                                                                                                                  sub ordinalOrdinal.Int (_cnt (List.tl y))
                                                                                                                                                                                                  path[let (_x_0 : (ty_0 option * ty_0 option)) = List.hd y in Option.get _x_0.0 = Option.get _x_0.1 && not Is_a(None, (List.hd y).1) && not Is_a(None, (List.hd y).0) && not Is_a([], y)]
                                                                                                                                                                                                  proof
                                                                                                                                                                                                  detailed proof
                                                                                                                                                                                                  ground_instances3
                                                                                                                                                                                                  definitions0
                                                                                                                                                                                                  inductions0
                                                                                                                                                                                                  search_time
                                                                                                                                                                                                  0.016s
                                                                                                                                                                                                  details
                                                                                                                                                                                                  Expand
                                                                                                                                                                                                  smt_stats
                                                                                                                                                                                                  num checks7
                                                                                                                                                                                                  arith-make-feasible7
                                                                                                                                                                                                  arith-max-columns12
                                                                                                                                                                                                  rlimit count2256
                                                                                                                                                                                                  arith-cheap-eqs2
                                                                                                                                                                                                  mk clause25
                                                                                                                                                                                                  datatype occurs check21
                                                                                                                                                                                                  mk bool var86
                                                                                                                                                                                                  arith-lower4
                                                                                                                                                                                                  datatype splits3
                                                                                                                                                                                                  decisions12
                                                                                                                                                                                                  propagations24
                                                                                                                                                                                                  arith-max-rows3
                                                                                                                                                                                                  conflicts4
                                                                                                                                                                                                  datatype accessor ax19
                                                                                                                                                                                                  datatype constructor ax17
                                                                                                                                                                                                  num allocs177037009
                                                                                                                                                                                                  final checks6
                                                                                                                                                                                                  added eqs81
                                                                                                                                                                                                  del clause5
                                                                                                                                                                                                  arith eq adapter3
                                                                                                                                                                                                  arith-upper5
                                                                                                                                                                                                  memory14.040000
                                                                                                                                                                                                  max memory14.040000
                                                                                                                                                                                                  Expand
                                                                                                                                                                                                  • start[0.016s]
                                                                                                                                                                                                      let (_x_0 : (ty_0 option * ty_0 option)) = List.hd y in
                                                                                                                                                                                                      let (_x_1 : ty_0 option) = _x_0.0 in
                                                                                                                                                                                                      let (_x_2 : ty_0 option) = _x_0.1 in
                                                                                                                                                                                                      let (_x_3 : int) = count.list anon_fun._cnt.1 y in
                                                                                                                                                                                                      let (_x_4 : (ty_0 option * ty_0 option) list) = List.tl y in
                                                                                                                                                                                                      let (_x_5 : int) = count.list anon_fun._cnt.1 _x_4 in
                                                                                                                                                                                                      let (_x_6 : (ty_0 option * ty_0 option)) = List.hd _x_4 in
                                                                                                                                                                                                      let (_x_7 : ty_0 option) = _x_6.0 in
                                                                                                                                                                                                      let (_x_8 : bool) = Is_a(None, _x_7) in
                                                                                                                                                                                                      let (_x_9 : bool) = not Is_a([], _x_4) in
                                                                                                                                                                                                      let (_x_10 : ty_0 option) = _x_6.1 in
                                                                                                                                                                                                      let (_x_11 : bool) = Is_a(None, _x_10) in
                                                                                                                                                                                                      let (_x_12 : bool) = not _x_8 && _x_9 in
                                                                                                                                                                                                      Option.get _x_1 = Option.get _x_2
                                                                                                                                                                                                      && not Is_a(None, _x_2)
                                                                                                                                                                                                         && not Is_a(None, _x_1) && not Is_a([], y) && _x_3 >= 0 && _x_5 >= 0
                                                                                                                                                                                                      ==> not (_x_8 && _x_9)
                                                                                                                                                                                                          && not (_x_11 && _x_12)
                                                                                                                                                                                                             && not (Option.get _x_7 = Option.get _x_10 && not _x_11 && _x_12)
                                                                                                                                                                                                          || Ordinal.( << ) (Ordinal.Int _x_5) (Ordinal.Int _x_3)
                                                                                                                                                                                                  • simplify
                                                                                                                                                                                                    into
                                                                                                                                                                                                    let (_x_0 : (ty_0 option * ty_0 option) list) = List.tl y in
                                                                                                                                                                                                    let (_x_1 : int) = count.list anon_fun._cnt.1 _x_0 in
                                                                                                                                                                                                    let (_x_2 : int) = count.list anon_fun._cnt.1 y in
                                                                                                                                                                                                    let (_x_3 : (ty_0 option * ty_0 option)) = List.hd _x_0 in
                                                                                                                                                                                                    let (_x_4 : ty_0 option) = _x_3.0 in
                                                                                                                                                                                                    let (_x_5 : bool) = Is_a(None, _x_4) in
                                                                                                                                                                                                    let (_x_6 : bool) = not Is_a([], _x_0) in
                                                                                                                                                                                                    let (_x_7 : ty_0 option) = _x_3.1 in
                                                                                                                                                                                                    let (_x_8 : bool) = Is_a(None, _x_7) in
                                                                                                                                                                                                    let (_x_9 : bool) = not _x_5 in
                                                                                                                                                                                                    let (_x_10 : (ty_0 option * ty_0 option)) = List.hd y in
                                                                                                                                                                                                    let (_x_11 : ty_0 option) = _x_10.0 in
                                                                                                                                                                                                    let (_x_12 : ty_0 option) = _x_10.1 in
                                                                                                                                                                                                    (Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
                                                                                                                                                                                                     || (not (_x_5 && _x_6) && not ((_x_8 && _x_9) && _x_6))
                                                                                                                                                                                                        && not
                                                                                                                                                                                                           (((Option.get _x_4 = Option.get _x_7 && not _x_8) && _x_9) && _x_6))
                                                                                                                                                                                                    || not
                                                                                                                                                                                                       (((((Option.get _x_11 = Option.get _x_12 && not Is_a(None, _x_12))
                                                                                                                                                                                                           && not Is_a(None, _x_11))
                                                                                                                                                                                                          && not Is_a([], y))
                                                                                                                                                                                                         && _x_2 >= 0)
                                                                                                                                                                                                        && _x_1 >= 0)
                                                                                                                                                                                                    expansions
                                                                                                                                                                                                    []
                                                                                                                                                                                                    rewrite_steps
                                                                                                                                                                                                      forward_chaining
                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                        expr
                                                                                                                                                                                                        (|`count.list anon_fun._cnt.1[0]`_3029| y_3010)
                                                                                                                                                                                                        expansions
                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                          expr
                                                                                                                                                                                                          (|`count.list anon_fun._cnt.1[0]`_3029| (|get.::.1_3001| y_3010))
                                                                                                                                                                                                          expansions
                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                            expr
                                                                                                                                                                                                            (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                                                                                                                                                                                                (|`count.list anon_fun._cnt.1[0]`_3029|
                                                                                                                                                                                                               …
                                                                                                                                                                                                            expansions
                                                                                                                                                                                                            • Unsat

                                                                                                                                                                                                            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 (_cnt x)
                                                                                                                                                                                                            sub ordinalOrdinal.Int (_cnt (List.tl x))
                                                                                                                                                                                                            path[let (_x_0 : (ty_0 option list * ty_0 option list)) = List.hd x in match_cols (zip _x_0.0 _x_0.1) && not Is_a([], x)]
                                                                                                                                                                                                            proof
                                                                                                                                                                                                            detailed proof
                                                                                                                                                                                                            ground_instances5
                                                                                                                                                                                                            definitions0
                                                                                                                                                                                                            inductions0
                                                                                                                                                                                                            search_time
                                                                                                                                                                                                            0.018s
                                                                                                                                                                                                            details
                                                                                                                                                                                                            Expand
                                                                                                                                                                                                            smt_stats
                                                                                                                                                                                                            num checks12
                                                                                                                                                                                                            arith-assume-eqs3
                                                                                                                                                                                                            arith-make-feasible59
                                                                                                                                                                                                            arith-max-columns33
                                                                                                                                                                                                            arith-conflicts4
                                                                                                                                                                                                            rlimit count7104
                                                                                                                                                                                                            arith-cheap-eqs20
                                                                                                                                                                                                            mk clause91
                                                                                                                                                                                                            datatype occurs check79
                                                                                                                                                                                                            mk bool var261
                                                                                                                                                                                                            arith-lower34
                                                                                                                                                                                                            arith-diseq3
                                                                                                                                                                                                            datatype splits23
                                                                                                                                                                                                            decisions139
                                                                                                                                                                                                            arith-propagations2
                                                                                                                                                                                                            propagations73
                                                                                                                                                                                                            interface eqs3
                                                                                                                                                                                                            arith-bound-propagations-cheap2
                                                                                                                                                                                                            arith-max-rows15
                                                                                                                                                                                                            conflicts15
                                                                                                                                                                                                            datatype accessor ax40
                                                                                                                                                                                                            minimized lits1
                                                                                                                                                                                                            datatype constructor ax68
                                                                                                                                                                                                            num allocs235790248
                                                                                                                                                                                                            final checks13
                                                                                                                                                                                                            added eqs280
                                                                                                                                                                                                            del clause44
                                                                                                                                                                                                            arith eq adapter33
                                                                                                                                                                                                            arith-upper52
                                                                                                                                                                                                            memory17.160000
                                                                                                                                                                                                            max memory19.230000
                                                                                                                                                                                                            Expand
                                                                                                                                                                                                            • start[0.018s]
                                                                                                                                                                                                                let (_x_0 : (ty_0 option list * ty_0 option list)) = List.hd x in
                                                                                                                                                                                                                let (_x_1 : int) = count.list anon_fun._cnt.1 x in
                                                                                                                                                                                                                let (_x_2 : (ty_0 option list * ty_0 option list) list) = List.tl x in
                                                                                                                                                                                                                let (_x_3 : int) = count.list anon_fun._cnt.1 _x_2 in
                                                                                                                                                                                                                let (_x_4 : (ty_0 option list * ty_0 option list)) = List.hd _x_2 in
                                                                                                                                                                                                                match_cols (zip _x_0.0 _x_0.1) && not Is_a([], x) && _x_1 >= 0 && _x_3 >= 0
                                                                                                                                                                                                                ==> not (match_cols (zip _x_4.0 _x_4.1) && not Is_a([], _x_2))
                                                                                                                                                                                                                    || Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_1)
                                                                                                                                                                                                            • simplify
                                                                                                                                                                                                              into
                                                                                                                                                                                                              let (_x_0 : (ty_0 option list * ty_0 option list) list) = List.tl x in
                                                                                                                                                                                                              let (_x_1 : (ty_0 option list * ty_0 option list)) = List.hd _x_0 in
                                                                                                                                                                                                              let (_x_2 : int) = count.list anon_fun._cnt.1 _x_0 in
                                                                                                                                                                                                              let (_x_3 : int) = count.list anon_fun._cnt.1 x in
                                                                                                                                                                                                              let (_x_4 : (ty_0 option list * ty_0 option list)) = List.hd x in
                                                                                                                                                                                                              (not (match_cols (zip _x_1.0 _x_1.1) && not Is_a([], _x_0))
                                                                                                                                                                                                               || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_3))
                                                                                                                                                                                                              || not
                                                                                                                                                                                                                 (((match_cols (zip _x_4.0 _x_4.1) && not Is_a([], x)) && _x_3 >= 0)
                                                                                                                                                                                                                  && _x_2 >= 0)
                                                                                                                                                                                                              expansions
                                                                                                                                                                                                              []
                                                                                                                                                                                                              rewrite_steps
                                                                                                                                                                                                                forward_chaining
                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                  (zip_3326 (|tuple_get.0_3308| (|get.::.0_3311| x_3343))
                                                                                                                                                                                                                            (|tuple_get.1_3309| (|get.::.0_331…
                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                    (match_cols_3335 (zip_3326 (|tuple_get.0_3308| (|get.::.0_3311| x_3343))
                                                                                                                                                                                                                                               …
                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                      (|`count.list anon_fun._cnt.1[0]`_3358| x_3343)
                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                        (|`count.list anon_fun._cnt.1[0]`_3358| (|get.::.1_3312| x_3343))
                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                          (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                                                                                                                                                                                                              (|`count.list anon_fun._cnt.1[0]`_3358|
                                                                                                                                                                                                                             …
                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                          • Unsat

                                                                                                                                                                                                                          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 283 steps, 1.635s):
                                                                                                                                                                                                                            let s =
                                                                                                                                                                                                                              let (_x_0 : cell option) = Some C8 in
                                                                                                                                                                                                                              let (_x_1 : cell option) = Some C1 in
                                                                                                                                                                                                                              let (_x_2 : cell option) = Some C2 in
                                                                                                                                                                                                                              let (_x_3 : cell option) = Some C7 in
                                                                                                                                                                                                                              let (_x_4 : cell option) = Some C5 in
                                                                                                                                                                                                                              let (_x_5 : cell option) = Some C3 in
                                                                                                                                                                                                                              let (_x_6 : cell option) = Some C6 in
                                                                                                                                                                                                                              let (_x_7 : cell option) = Some C4 in
                                                                                                                                                                                                                              let (_x_8 : cell option) = Some C9 in
                                                                                                                                                                                                                              {rows =
                                                                                                                                                                                                                               [[_x_0; _x_1; _x_2; _x_3; _x_4; _x_5; _x_6; _x_7; _x_8];
                                                                                                                                                                                                                                [_x_8; _x_7; _x_5; _x_6; _x_0; _x_2; _x_1; _x_3; _x_4];
                                                                                                                                                                                                                                [_x_6; _x_3; _x_4; _x_7; _x_8; _x_1; _x_2; _x_0; _x_5];
                                                                                                                                                                                                                                [_x_1; _x_4; _x_7; _x_2; _x_5; _x_3; _x_0; _x_8; _x_6];
                                                                                                                                                                                                                                [_x_5; _x_6; _x_8; _x_0; _x_7; _x_4; _x_3; _x_2; _x_1];
                                                                                                                                                                                                                                [_x_2; _x_0; _x_3; _x_1; _x_6; _x_8; _x_4; _x_5; _x_7];
                                                                                                                                                                                                                                [_x_4; _x_2; _x_1; _x_8; _x_3; _x_7; _x_5; _x_6; _x_0];
                                                                                                                                                                                                                                [_x_7; _x_5; _x_0; _x_4; _x_2; _x_6; _x_8; _x_1; _x_3];
                                                                                                                                                                                                                                [_x_3; _x_8; _x_6; _x_5; _x_1; _x_0; _x_7; _x_4; _x_2]]}
                                                                                                                                                                                                                          
                                                                                                                                                                                                                          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