Solve Hatsune Miku logic paint

input.txt

1 4 2
6 1 2
3 2 1
2 1
2 2
3
3
3
2 4 1
4 4 2
10 3
6 4
2 5
6 7
7 2 1
-
3 3 3
2 3 3
2 3 2
1 3 2
1 2 2
2 2 2
1 2 1
2 1 3
1 2 2 1
2 3 2
2 3 3
2 3 3
1 4 4
3 5
4 7

mikupaint.cpp

#include <iostream>
#include <fstream>
#include <sstream>
#include <queue>
#include <string>
#include <algorithm>
#include "z3++.h"

using namespace z3;

expr markrow(bool col, const expr &paint,
             const expr &plen, int rowcol, const expr &var, int range) {
  context &c = paint.ctx();
  expr index = c.int_val(rowcol);
  
  auto index_prev = ast_vector_tpl<expr>(c);
  
  if (!col) index_prev.push_back(index);
  index_prev.push_back(var - 1);
  if (col) index_prev.push_back(index);
  expr prev_bound = !select(paint, index_prev);

  auto index_next = ast_vector_tpl<expr>(c);
  
  if (!col) index_next.push_back(index);
  index_next.push_back(var + range);
  if (col) index_next.push_back(index);
  expr next_bound = !select(paint, index_next);

  expr i = c.int_const("i");
  auto index_cont = ast_vector_tpl<expr>(c);
  if (!col) index_cont.push_back(index);
  index_cont.push_back(i);
  if (col) index_cont.push_back(index);
  expr continuous = forall(i, implies((i >= var) && (i < var + range),
                                      select(paint, index_cont)));

  auto conj = ast_vector_tpl<expr>(c);
  conj.push_back(prev_bound);
  conj.push_back(next_bound);
  conj.push_back(var >= 0);
  conj.push_back((var + range) <= plen);
  conj.push_back(continuous);
  return mk_and(conj);
}

void rowlimit(bool col, solver &s, const expr &paint,
              int bound, int rowcol, int size) {
  context &c = paint.ctx();
  expr index = c.int_val(rowcol);
  auto cells = ast_vector_tpl<expr>(c);
  for (int i = 0; i<size; ++i) {
    auto s = ast_vector_tpl<expr>(c);
    if (!col) s.push_back(index);
    s.push_back(c.int_val(i));
    if (col) s.push_back(index);
    cells.push_back(select(paint, s));
  }
  s.add(atleast(cells, bound));
  s.add(atmost(cells, bound));
}

void row_conditions(bool col, solver &s, const expr &paint,
                    const expr &plen,
                    const std::vector<expr> vars,
                    const std::vector<int> row,
                    int size, int index) {
  if (row.size() == 1)
    s.add(exists(vars[0], markrow(col, paint, plen, index, vars[0], row[0])));
  else {
    auto conj = ast_vector_tpl<expr>(s.ctx());
    auto exs = ast_vector_tpl<expr>(s.ctx());
    int i = 0;
    for (auto & elem : row) 
      {
        exs.push_back(vars[i]);
        conj.push_back(markrow(col, paint, plen, index, vars[i], elem));
        if (i > 0) conj.push_back(vars[i-1] < vars[i]);
        i++;
      }
    s.add(exists(exs, mk_and(conj)));
  }
  int sum = 0;
  for (auto& n : row) sum += n;
  rowlimit(col, s, paint, sum, index, size);
}

int mikupaint(int paint_size,
               std::queue<std::vector<int>> &rows,
               std::queue<std::vector<int>> &cols,
               int max_size) {
  context c;
  auto intint = ast_vector_tpl<sort>(c);
  intint.push_back(c.int_sort());
  intint.push_back(c.int_sort());
  expr paint = c.constant("paint", c.array_sort(intint, c.bool_sort()));
  expr plen = c.int_const("plen");

  solver s(c);
  s.add(plen == c.int_val(paint_size));

  std::vector<expr> vars;
  vars.reserve(max_size);
  for (int x = 0; x < max_size; ++x) {
    std::string sym = "x" + std::to_string(x);
    vars.push_back(c.int_const(sym.c_str()));
  }
  int n = 0;
  while (!rows.empty()) {
    auto row = rows.front();
    row_conditions(false, s, paint, plen, vars, row, paint_size, n);
    rows.pop();
    n++;
  }
  n = 0;
  while (!cols.empty()) {
    auto col = cols.front();
    row_conditions(true, s, paint, plen, vars, col, paint_size, n);
    cols.pop();
    n++;
  }
  auto result = s.check();
  std::cout << result << std::endl;
  if (result != z3::sat) return -3;
  // print result
  model m = s.get_model();
  for (int i=0;i<paint_size;++i) {
    expr row = c.int_val(i);
    std::cout << '"';
    for (int j=0;j<paint_size;++j) {
      auto s = ast_vector_tpl<expr>(c);
      s.push_back(row);
      s.push_back(c.int_val(j));
      std::cout << (m.eval(select(paint,s)).is_true() ? '#' : '.');
    }
    std::cout << '"' << std::endl;
  }
  return 0;
}

int main(int argc, char *argv[]) {
  if (argc < 2) return -1;
  std::ifstream input(argv[1]);

  std::queue<std::vector<int>> rows, cols;
  std::size_t max_size = 0;
  bool col = false;
  for(std::string line; std::getline(input, line);) {
    if (line.size() > 0 && line[0] == '-') {
      col = true; continue;
    } 
    std::istringstream iss {line};
    std::vector<int> data{std::istream_iterator<int>(iss), std::istream_iterator<int>()};
    // std::cout << data.size() << std::endl;
    max_size = std::max(max_size, data.size());
    if (col) {cols.push(data); } else rows.push(data);
  }
  int paint_size = rows.size();
  if (paint_size != cols.size()) return -2;

  return mikupaint(paint_size, rows, cols, max_size);
}

mikupaint.ss

(import (chezscheme))

(define (parse-line s)
  (with-input-from-string s
    (lambda ()
      (let loop ([n (read)])
        (if (eof-object? n)
            '()
            (cons n (loop (read))))))))

(define (norm l)
  (if (and (= (length l) 1) (= (car l) 0))
      '()
      l))

(define xs '())
(define ys '())

(call-with-input-file (car (command-line-arguments))
  (lambda (p)
    (let loop ((line (get-line p))
               (acc '()))
      (cond [(eof-object? line)
             (set! ys (reverse! acc))]
            [(string=? line "-")
             (begin
               (set! xs (reverse! acc))
               (loop (get-line p) '()))]
            [else
             (let ([l (parse-line line)])
               (loop (get-line p) (if (null? l)
                                      acc
                                      (cons l acc))))]))))

(assert (= (length xs) (length ys)))
(define psize (length xs))



(define terpri (lambda () (write-char #\newline)))
(define-syntax pp
  (syntax-rules ()
    [(_) (terpri)]
    [(_ `s) (pretty-print `s)]
    [(_ s) (pretty-print (quote s))]
    [(_ s1 s2 ...)
     (begin (pp s1) (pp s2 ...))]))
(display ";; -*- mode:z3 -*-")
(pp)

(pp (declare-const paint (Array Int Int Bool)))
(pp (declare-const plen Int))

(pp
 (define-fun markrow ((row Int) (var Int) (range Int)) Bool
   (and
    (not (select paint row (- var 1)))
    (not (select paint row (+ var range)))
    (>= var 0)
    (<= (+ var range) plen)
    (forall ((i Int))
            (implies (and (>= i var) (< i (+ var range)))
                     (select paint row i)))))

 (define-fun markcol ((col Int) (var Int) (range Int)) Bool
   (and
    (not (select paint (- var 1) col))
    (not (select paint (+ var range) col))
    (>= var 0)
    (<= (+ var range) plen)
    (forall ((i Int))
            (implies (and (>= i var) (< i (+ var range)))
                     (select paint i col))))))

(pp `(assert (= plen ,psize)))

(define rels '())

(define (var . item)
  (string->symbol
   (apply string-append
          (map (lambda (x)
                 (cond
                  [(string? x) x]
                  [(symbol? x) (symbol->string x)]
                  [(number? x) (number->string x)]))
               item))))

(define-syntax push
  (syntax-rules ()
    [(_ place val) (set! place (cons val place))]))

(define (for-index fn items)
  (let loop ((i 0)
             (r items))
    (if (null? r) (void)
        (begin
          (fn i (car r))
          (loop (+ 1 i) (cdr r))))))

(define (mapi fn xs)
  (let loop ((i 0)
             (xs xs))
    (if (null? xs) '()
        (cons (fn i (car xs)) (loop (+ 1 i) (cdr xs))))))

(define (sum xs)
  (fold-left + 0 xs))

(for-index
 (lambda (idx row)
   (if (null? row)
       (push rels `(assert (forall ((i Int))
                                   (= (select paint ,idx i) false))))
       (push rels
             `(assert (exists ,(mapi (lambda (id x) `(,(var 'x id) Int)) row)
                              ,(if (> (length row) 1)
                                   `(and ,@(mapi (lambda (id n)
                                                   `(markrow ,idx
                                                             ,(var 'x id)
                                                             ,n))
                                                 row)
                                         (<
                                          ,@(map (lambda (id)
                                                   (var 'x id))
                                                 (iota (length row)))))
                                   `(markrow ,idx
                                             ,(var 'x 0)
                                             ,(car row))))))))
 xs)

(for-index
 (lambda (idx row)
   (if (null? row)
       (push rels `(assert (forall ((i Int))
                                   (= (select paint i ,idx) false))))
       (push rels
             `(assert (exists ,(mapi (lambda (id x) `(,(var 'y id) Int)) row)
                              ,(if (> (length row) 1)
                                   `(and ,@(mapi (lambda (id n)
                                                   `(markcol ,idx
                                                             ,(var 'y id)
                                                             ,n))
                                                 row)
                                         (<
                                          ,@(map (lambda (id)
                                                   (var 'y id))
                                                 (iota (length row)))))
                                   `(markcol ,idx
                                             ,(var 'y 0)
                                             ,(car row))))))))
 ys)

(for-index
 (lambda (idx row)
   (push rels `(assert ((_ at-least ,(sum row))
                        ,@(map (lambda (i)
                                 `(select paint ,idx ,i))
                               (iota psize)))))
   (push rels `(assert ((_ at-most ,(sum row))
                        ,@(map (lambda (i)
                                 `(select paint ,idx ,i))
                               (iota psize))))))
 xs)

(for-index
 (lambda (idx col)
   (push rels `(assert ((_ at-least ,(sum col))
                        ,@(map (lambda (i)
                                 `(select paint ,i ,idx))
                               (iota psize)))))
   (push rels `(assert ((_ at-most ,(sum col))
                        ,@(map (lambda (i)
                                 `(select paint ,i ,idx))
                               (iota psize))))))
 ys)

(for-each pretty-print (reverse rels))
(pp)



(pp
 (check-sat)
 ;; (get-model)
 (define-fun-rec rowtoseq ((row Int) (index Int)) (Seq Bool)
   (ite (>= index plen)
       (as seq.empty (Seq Bool))
       (seq.++ (seq.unit (select paint row index)) (rowtoseq row (+ index 1)))))
 (define-fun show ((i Int)) String
   (seq.map (lambda ((b Bool)) (ite b (_ Char 35) (_ Char 46)))
            (rowtoseq i 0))))

(for-each (lambda (x)
            (pp `(eval (show ,x))))
          (iota psize))
(pp)

output.smt

;; -*- mode:z3 -*-
(declare-const paint (Array Int Int Bool))
(declare-const plen Int)
(define-fun
  markrow
  ((row Int) (var Int) (range Int))
  Bool
  (and (not (select paint row (- var 1)))
       (not (select paint row (+ var range)))
       (>= var 0)
       (<= (+ var range) plen)
       (forall
         ((i Int))
         (implies
           (and (>= i var) (< i (+ var range)))
           (= (select paint row i) true)))))
(define-fun
  markcol
  ((col Int) (var Int) (range Int))
  Bool
  (and (not (select paint (- var 1) col))
       (not (select paint (+ var range) col))
       (>= var 0)
       (<= (+ var range) plen)
       (forall
         ((i Int))
         (implies
           (and (>= i var) (< i (+ var range)))
           (= (select paint i col) true)))))
(assert (= plen 15))
(assert
  (exists
    ((x0 Int) (x1 Int) (x2 Int))
    (and (markrow 0 x0 1)
         (markrow 0 x1 4)
         (markrow 0 x2 2)
         (< x0 x1 x2))))
(assert
  (exists
    ((x0 Int) (x1 Int) (x2 Int))
    (and (markrow 1 x0 6)
         (markrow 1 x1 1)
         (markrow 1 x2 2)
         (< x0 x1 x2))))
(assert
  (exists
    ((x0 Int) (x1 Int) (x2 Int))
    (and (markrow 2 x0 3)
         (markrow 2 x1 2)
         (markrow 2 x2 1)
         (< x0 x1 x2))))
(assert
  (exists
    ((x0 Int) (x1 Int))
    (and (markrow 3 x0 2) (markrow 3 x1 1) (< x0 x1))))
(assert
  (exists
    ((x0 Int) (x1 Int))
    (and (markrow 4 x0 2) (markrow 4 x1 2) (< x0 x1))))
(assert (exists ((x0 Int)) (markrow 5 x0 3)))
(assert (exists ((x0 Int)) (markrow 6 x0 3)))
(assert (exists ((x0 Int)) (markrow 7 x0 3)))
(assert
  (exists
    ((x0 Int) (x1 Int) (x2 Int))
    (and (markrow 8 x0 2)
         (markrow 8 x1 4)
         (markrow 8 x2 1)
         (< x0 x1 x2))))
(assert
  (exists
    ((x0 Int) (x1 Int) (x2 Int))
    (and (markrow 9 x0 4)
         (markrow 9 x1 4)
         (markrow 9 x2 2)
         (< x0 x1 x2))))
(assert
  (exists
    ((x0 Int) (x1 Int))
    (and (markrow 10 x0 10) (markrow 10 x1 3) (< x0 x1))))
(assert
  (exists
    ((x0 Int) (x1 Int))
    (and (markrow 11 x0 6) (markrow 11 x1 4) (< x0 x1))))
(assert
  (exists
    ((x0 Int) (x1 Int))
    (and (markrow 12 x0 2) (markrow 12 x1 5) (< x0 x1))))
(assert
  (exists
    ((x0 Int) (x1 Int))
    (and (markrow 13 x0 6) (markrow 13 x1 7) (< x0 x1))))
(assert
  (exists
    ((x0 Int) (x1 Int) (x2 Int))
    (and (markrow 14 x0 7)
         (markrow 14 x1 2)
         (markrow 14 x2 1)
         (< x0 x1 x2))))
(assert
  (exists
    ((y0 Int) (y1 Int) (y2 Int))
    (and (markcol 0 y0 3)
         (markcol 0 y1 3)
         (markcol 0 y2 3)
         (< y0 y1 y2))))
(assert
  (exists
    ((y0 Int) (y1 Int) (y2 Int))
    (and (markcol 1 y0 2)
         (markcol 1 y1 3)
         (markcol 1 y2 3)
         (< y0 y1 y2))))
(assert
  (exists
    ((y0 Int) (y1 Int) (y2 Int))
    (and (markcol 2 y0 2)
         (markcol 2 y1 3)
         (markcol 2 y2 2)
         (< y0 y1 y2))))
(assert
  (exists
    ((y0 Int) (y1 Int) (y2 Int))
    (and (markcol 3 y0 1)
         (markcol 3 y1 3)
         (markcol 3 y2 2)
         (< y0 y1 y2))))
(assert
  (exists
    ((y0 Int) (y1 Int) (y2 Int))
    (and (markcol 4 y0 1)
         (markcol 4 y1 2)
         (markcol 4 y2 2)
         (< y0 y1 y2))))
(assert
  (exists
    ((y0 Int) (y1 Int) (y2 Int))
    (and (markcol 5 y0 2)
         (markcol 5 y1 2)
         (markcol 5 y2 2)
         (< y0 y1 y2))))
(assert
  (exists
    ((y0 Int) (y1 Int) (y2 Int))
    (and (markcol 6 y0 1)
         (markcol 6 y1 2)
         (markcol 6 y2 1)
         (< y0 y1 y2))))
(assert
  (exists
    ((y0 Int) (y1 Int) (y2 Int))
    (and (markcol 7 y0 2)
         (markcol 7 y1 1)
         (markcol 7 y2 3)
         (< y0 y1 y2))))
(assert
  (exists
    ((y0 Int) (y1 Int) (y2 Int) (y3 Int))
    (and (markcol 8 y0 1)
         (markcol 8 y1 2)
         (markcol 8 y2 2)
         (markcol 8 y3 1)
         (< y0 y1 y2 y3))))
(assert
  (exists
    ((y0 Int) (y1 Int) (y2 Int))
    (and (markcol 9 y0 2)
         (markcol 9 y1 3)
         (markcol 9 y2 2)
         (< y0 y1 y2))))
(assert
  (exists
    ((y0 Int) (y1 Int) (y2 Int))
    (and (markcol 10 y0 2)
         (markcol 10 y1 3)
         (markcol 10 y2 3)
         (< y0 y1 y2))))
(assert
  (exists
    ((y0 Int) (y1 Int) (y2 Int))
    (and (markcol 11 y0 2)
         (markcol 11 y1 3)
         (markcol 11 y2 3)
         (< y0 y1 y2))))
(assert
  (exists
    ((y0 Int) (y1 Int) (y2 Int))
    (and (markcol 12 y0 1)
         (markcol 12 y1 4)
         (markcol 12 y2 4)
         (< y0 y1 y2))))
(assert
  (exists
    ((y0 Int) (y1 Int))
    (and (markcol 13 y0 3) (markcol 13 y1 5) (< y0 y1))))
(assert
  (exists
    ((y0 Int) (y1 Int))
    (and (markcol 14 y0 4) (markcol 14 y1 7) (< y0 y1))))
(assert
  ((_ at-least 7) (select paint 0 0) (select paint 0 1) (select paint 0 2)
    (select paint 0 3) (select paint 0 4) (select paint 0 5)
    (select paint 0 6) (select paint 0 7) (select paint 0 8)
    (select paint 0 9) (select paint 0 10) (select paint 0 11)
    (select paint 0 12) (select paint 0 13)
    (select paint 0 14)))
(assert
  ((_ at-most 7) (select paint 0 0) (select paint 0 1) (select paint 0 2)
    (select paint 0 3) (select paint 0 4) (select paint 0 5)
    (select paint 0 6) (select paint 0 7) (select paint 0 8)
    (select paint 0 9) (select paint 0 10) (select paint 0 11)
    (select paint 0 12) (select paint 0 13)
    (select paint 0 14)))
(assert
  ((_ at-least 9) (select paint 1 0) (select paint 1 1) (select paint 1 2)
    (select paint 1 3) (select paint 1 4) (select paint 1 5)
    (select paint 1 6) (select paint 1 7) (select paint 1 8)
    (select paint 1 9) (select paint 1 10) (select paint 1 11)
    (select paint 1 12) (select paint 1 13)
    (select paint 1 14)))
(assert
  ((_ at-most 9) (select paint 1 0) (select paint 1 1) (select paint 1 2)
    (select paint 1 3) (select paint 1 4) (select paint 1 5)
    (select paint 1 6) (select paint 1 7) (select paint 1 8)
    (select paint 1 9) (select paint 1 10) (select paint 1 11)
    (select paint 1 12) (select paint 1 13)
    (select paint 1 14)))
(assert
  ((_ at-least 6) (select paint 2 0) (select paint 2 1) (select paint 2 2)
    (select paint 2 3) (select paint 2 4) (select paint 2 5)
    (select paint 2 6) (select paint 2 7) (select paint 2 8)
    (select paint 2 9) (select paint 2 10) (select paint 2 11)
    (select paint 2 12) (select paint 2 13)
    (select paint 2 14)))
(assert
  ((_ at-most 6) (select paint 2 0) (select paint 2 1) (select paint 2 2)
    (select paint 2 3) (select paint 2 4) (select paint 2 5)
    (select paint 2 6) (select paint 2 7) (select paint 2 8)
    (select paint 2 9) (select paint 2 10) (select paint 2 11)
    (select paint 2 12) (select paint 2 13)
    (select paint 2 14)))
(assert
  ((_ at-least 3) (select paint 3 0) (select paint 3 1) (select paint 3 2)
    (select paint 3 3) (select paint 3 4) (select paint 3 5)
    (select paint 3 6) (select paint 3 7) (select paint 3 8)
    (select paint 3 9) (select paint 3 10) (select paint 3 11)
    (select paint 3 12) (select paint 3 13)
    (select paint 3 14)))
(assert
  ((_ at-most 3) (select paint 3 0) (select paint 3 1) (select paint 3 2)
    (select paint 3 3) (select paint 3 4) (select paint 3 5)
    (select paint 3 6) (select paint 3 7) (select paint 3 8)
    (select paint 3 9) (select paint 3 10) (select paint 3 11)
    (select paint 3 12) (select paint 3 13)
    (select paint 3 14)))
(assert
  ((_ at-least 4) (select paint 4 0) (select paint 4 1) (select paint 4 2)
    (select paint 4 3) (select paint 4 4) (select paint 4 5)
    (select paint 4 6) (select paint 4 7) (select paint 4 8)
    (select paint 4 9) (select paint 4 10) (select paint 4 11)
    (select paint 4 12) (select paint 4 13)
    (select paint 4 14)))
(assert
  ((_ at-most 4) (select paint 4 0) (select paint 4 1) (select paint 4 2)
    (select paint 4 3) (select paint 4 4) (select paint 4 5)
    (select paint 4 6) (select paint 4 7) (select paint 4 8)
    (select paint 4 9) (select paint 4 10) (select paint 4 11)
    (select paint 4 12) (select paint 4 13)
    (select paint 4 14)))
(assert
  ((_ at-least 3) (select paint 5 0) (select paint 5 1) (select paint 5 2)
    (select paint 5 3) (select paint 5 4) (select paint 5 5)
    (select paint 5 6) (select paint 5 7) (select paint 5 8)
    (select paint 5 9) (select paint 5 10) (select paint 5 11)
    (select paint 5 12) (select paint 5 13)
    (select paint 5 14)))
(assert
  ((_ at-most 3) (select paint 5 0) (select paint 5 1) (select paint 5 2)
    (select paint 5 3) (select paint 5 4) (select paint 5 5)
    (select paint 5 6) (select paint 5 7) (select paint 5 8)
    (select paint 5 9) (select paint 5 10) (select paint 5 11)
    (select paint 5 12) (select paint 5 13)
    (select paint 5 14)))
(assert
  ((_ at-least 3) (select paint 6 0) (select paint 6 1) (select paint 6 2)
    (select paint 6 3) (select paint 6 4) (select paint 6 5)
    (select paint 6 6) (select paint 6 7) (select paint 6 8)
    (select paint 6 9) (select paint 6 10) (select paint 6 11)
    (select paint 6 12) (select paint 6 13)
    (select paint 6 14)))
(assert
  ((_ at-most 3) (select paint 6 0) (select paint 6 1) (select paint 6 2)
    (select paint 6 3) (select paint 6 4) (select paint 6 5)
    (select paint 6 6) (select paint 6 7) (select paint 6 8)
    (select paint 6 9) (select paint 6 10) (select paint 6 11)
    (select paint 6 12) (select paint 6 13)
    (select paint 6 14)))
(assert
  ((_ at-least 3) (select paint 7 0) (select paint 7 1) (select paint 7 2)
    (select paint 7 3) (select paint 7 4) (select paint 7 5)
    (select paint 7 6) (select paint 7 7) (select paint 7 8)
    (select paint 7 9) (select paint 7 10) (select paint 7 11)
    (select paint 7 12) (select paint 7 13)
    (select paint 7 14)))
(assert
  ((_ at-most 3) (select paint 7 0) (select paint 7 1) (select paint 7 2)
    (select paint 7 3) (select paint 7 4) (select paint 7 5)
    (select paint 7 6) (select paint 7 7) (select paint 7 8)
    (select paint 7 9) (select paint 7 10) (select paint 7 11)
    (select paint 7 12) (select paint 7 13)
    (select paint 7 14)))
(assert
  ((_ at-least 7) (select paint 8 0) (select paint 8 1) (select paint 8 2)
    (select paint 8 3) (select paint 8 4) (select paint 8 5)
    (select paint 8 6) (select paint 8 7) (select paint 8 8)
    (select paint 8 9) (select paint 8 10) (select paint 8 11)
    (select paint 8 12) (select paint 8 13)
    (select paint 8 14)))
(assert
  ((_ at-most 7) (select paint 8 0) (select paint 8 1) (select paint 8 2)
    (select paint 8 3) (select paint 8 4) (select paint 8 5)
    (select paint 8 6) (select paint 8 7) (select paint 8 8)
    (select paint 8 9) (select paint 8 10) (select paint 8 11)
    (select paint 8 12) (select paint 8 13)
    (select paint 8 14)))
(assert
  ((_ at-least 10) (select paint 9 0) (select paint 9 1) (select paint 9 2)
    (select paint 9 3) (select paint 9 4) (select paint 9 5)
    (select paint 9 6) (select paint 9 7) (select paint 9 8)
    (select paint 9 9) (select paint 9 10) (select paint 9 11)
    (select paint 9 12) (select paint 9 13)
    (select paint 9 14)))
(assert
  ((_ at-most 10) (select paint 9 0) (select paint 9 1) (select paint 9 2)
    (select paint 9 3) (select paint 9 4) (select paint 9 5)
    (select paint 9 6) (select paint 9 7) (select paint 9 8)
    (select paint 9 9) (select paint 9 10) (select paint 9 11)
    (select paint 9 12) (select paint 9 13)
    (select paint 9 14)))
(assert
  ((_ at-least 13) (select paint 10 0) (select paint 10 1) (select paint 10 2)
    (select paint 10 3) (select paint 10 4) (select paint 10 5)
    (select paint 10 6) (select paint 10 7) (select paint 10 8)
    (select paint 10 9) (select paint 10 10)
    (select paint 10 11) (select paint 10 12)
    (select paint 10 13) (select paint 10 14)))
(assert
  ((_ at-most 13) (select paint 10 0) (select paint 10 1) (select paint 10 2)
    (select paint 10 3) (select paint 10 4) (select paint 10 5)
    (select paint 10 6) (select paint 10 7) (select paint 10 8)
    (select paint 10 9) (select paint 10 10)
    (select paint 10 11) (select paint 10 12)
    (select paint 10 13) (select paint 10 14)))
(assert
  ((_ at-least 10) (select paint 11 0) (select paint 11 1) (select paint 11 2)
    (select paint 11 3) (select paint 11 4) (select paint 11 5)
    (select paint 11 6) (select paint 11 7) (select paint 11 8)
    (select paint 11 9) (select paint 11 10)
    (select paint 11 11) (select paint 11 12)
    (select paint 11 13) (select paint 11 14)))
(assert
  ((_ at-most 10) (select paint 11 0) (select paint 11 1) (select paint 11 2)
    (select paint 11 3) (select paint 11 4) (select paint 11 5)
    (select paint 11 6) (select paint 11 7) (select paint 11 8)
    (select paint 11 9) (select paint 11 10)
    (select paint 11 11) (select paint 11 12)
    (select paint 11 13) (select paint 11 14)))
(assert
  ((_ at-least 7) (select paint 12 0) (select paint 12 1) (select paint 12 2)
    (select paint 12 3) (select paint 12 4) (select paint 12 5)
    (select paint 12 6) (select paint 12 7) (select paint 12 8)
    (select paint 12 9) (select paint 12 10)
    (select paint 12 11) (select paint 12 12)
    (select paint 12 13) (select paint 12 14)))
(assert
  ((_ at-most 7) (select paint 12 0) (select paint 12 1) (select paint 12 2)
    (select paint 12 3) (select paint 12 4) (select paint 12 5)
    (select paint 12 6) (select paint 12 7) (select paint 12 8)
    (select paint 12 9) (select paint 12 10)
    (select paint 12 11) (select paint 12 12)
    (select paint 12 13) (select paint 12 14)))
(assert
  ((_ at-least 13) (select paint 13 0) (select paint 13 1) (select paint 13 2)
    (select paint 13 3) (select paint 13 4) (select paint 13 5)
    (select paint 13 6) (select paint 13 7) (select paint 13 8)
    (select paint 13 9) (select paint 13 10)
    (select paint 13 11) (select paint 13 12)
    (select paint 13 13) (select paint 13 14)))
(assert
  ((_ at-most 13) (select paint 13 0) (select paint 13 1) (select paint 13 2)
    (select paint 13 3) (select paint 13 4) (select paint 13 5)
    (select paint 13 6) (select paint 13 7) (select paint 13 8)
    (select paint 13 9) (select paint 13 10)
    (select paint 13 11) (select paint 13 12)
    (select paint 13 13) (select paint 13 14)))
(assert
  ((_ at-least 10) (select paint 14 0) (select paint 14 1) (select paint 14 2)
    (select paint 14 3) (select paint 14 4) (select paint 14 5)
    (select paint 14 6) (select paint 14 7) (select paint 14 8)
    (select paint 14 9) (select paint 14 10)
    (select paint 14 11) (select paint 14 12)
    (select paint 14 13) (select paint 14 14)))
(assert
  ((_ at-most 10) (select paint 14 0) (select paint 14 1) (select paint 14 2)
    (select paint 14 3) (select paint 14 4) (select paint 14 5)
    (select paint 14 6) (select paint 14 7) (select paint 14 8)
    (select paint 14 9) (select paint 14 10)
    (select paint 14 11) (select paint 14 12)
    (select paint 14 13) (select paint 14 14)))
(assert
  ((_ at-least 9) (select paint 0 0) (select paint 1 0) (select paint 2 0)
    (select paint 3 0) (select paint 4 0) (select paint 5 0)
    (select paint 6 0) (select paint 7 0) (select paint 8 0)
    (select paint 9 0) (select paint 10 0) (select paint 11 0)
    (select paint 12 0) (select paint 13 0)
    (select paint 14 0)))
(assert
  ((_ at-most 9) (select paint 0 0) (select paint 1 0) (select paint 2 0)
    (select paint 3 0) (select paint 4 0) (select paint 5 0)
    (select paint 6 0) (select paint 7 0) (select paint 8 0)
    (select paint 9 0) (select paint 10 0) (select paint 11 0)
    (select paint 12 0) (select paint 13 0)
    (select paint 14 0)))
(assert
  ((_ at-least 8) (select paint 0 1) (select paint 1 1) (select paint 2 1)
    (select paint 3 1) (select paint 4 1) (select paint 5 1)
    (select paint 6 1) (select paint 7 1) (select paint 8 1)
    (select paint 9 1) (select paint 10 1) (select paint 11 1)
    (select paint 12 1) (select paint 13 1)
    (select paint 14 1)))
(assert
  ((_ at-most 8) (select paint 0 1) (select paint 1 1) (select paint 2 1)
    (select paint 3 1) (select paint 4 1) (select paint 5 1)
    (select paint 6 1) (select paint 7 1) (select paint 8 1)
    (select paint 9 1) (select paint 10 1) (select paint 11 1)
    (select paint 12 1) (select paint 13 1)
    (select paint 14 1)))
(assert
  ((_ at-least 7) (select paint 0 2) (select paint 1 2) (select paint 2 2)
    (select paint 3 2) (select paint 4 2) (select paint 5 2)
    (select paint 6 2) (select paint 7 2) (select paint 8 2)
    (select paint 9 2) (select paint 10 2) (select paint 11 2)
    (select paint 12 2) (select paint 13 2)
    (select paint 14 2)))
(assert
  ((_ at-most 7) (select paint 0 2) (select paint 1 2) (select paint 2 2)
    (select paint 3 2) (select paint 4 2) (select paint 5 2)
    (select paint 6 2) (select paint 7 2) (select paint 8 2)
    (select paint 9 2) (select paint 10 2) (select paint 11 2)
    (select paint 12 2) (select paint 13 2)
    (select paint 14 2)))
(assert
  ((_ at-least 6) (select paint 0 3) (select paint 1 3) (select paint 2 3)
    (select paint 3 3) (select paint 4 3) (select paint 5 3)
    (select paint 6 3) (select paint 7 3) (select paint 8 3)
    (select paint 9 3) (select paint 10 3) (select paint 11 3)
    (select paint 12 3) (select paint 13 3)
    (select paint 14 3)))
(assert
  ((_ at-most 6) (select paint 0 3) (select paint 1 3) (select paint 2 3)
    (select paint 3 3) (select paint 4 3) (select paint 5 3)
    (select paint 6 3) (select paint 7 3) (select paint 8 3)
    (select paint 9 3) (select paint 10 3) (select paint 11 3)
    (select paint 12 3) (select paint 13 3)
    (select paint 14 3)))
(assert
  ((_ at-least 5) (select paint 0 4) (select paint 1 4) (select paint 2 4)
    (select paint 3 4) (select paint 4 4) (select paint 5 4)
    (select paint 6 4) (select paint 7 4) (select paint 8 4)
    (select paint 9 4) (select paint 10 4) (select paint 11 4)
    (select paint 12 4) (select paint 13 4)
    (select paint 14 4)))
(assert
  ((_ at-most 5) (select paint 0 4) (select paint 1 4) (select paint 2 4)
    (select paint 3 4) (select paint 4 4) (select paint 5 4)
    (select paint 6 4) (select paint 7 4) (select paint 8 4)
    (select paint 9 4) (select paint 10 4) (select paint 11 4)
    (select paint 12 4) (select paint 13 4)
    (select paint 14 4)))
(assert
  ((_ at-least 6) (select paint 0 5) (select paint 1 5) (select paint 2 5)
    (select paint 3 5) (select paint 4 5) (select paint 5 5)
    (select paint 6 5) (select paint 7 5) (select paint 8 5)
    (select paint 9 5) (select paint 10 5) (select paint 11 5)
    (select paint 12 5) (select paint 13 5)
    (select paint 14 5)))
(assert
  ((_ at-most 6) (select paint 0 5) (select paint 1 5) (select paint 2 5)
    (select paint 3 5) (select paint 4 5) (select paint 5 5)
    (select paint 6 5) (select paint 7 5) (select paint 8 5)
    (select paint 9 5) (select paint 10 5) (select paint 11 5)
    (select paint 12 5) (select paint 13 5)
    (select paint 14 5)))
(assert
  ((_ at-least 4) (select paint 0 6) (select paint 1 6) (select paint 2 6)
    (select paint 3 6) (select paint 4 6) (select paint 5 6)
    (select paint 6 6) (select paint 7 6) (select paint 8 6)
    (select paint 9 6) (select paint 10 6) (select paint 11 6)
    (select paint 12 6) (select paint 13 6)
    (select paint 14 6)))
(assert
  ((_ at-most 4) (select paint 0 6) (select paint 1 6) (select paint 2 6)
    (select paint 3 6) (select paint 4 6) (select paint 5 6)
    (select paint 6 6) (select paint 7 6) (select paint 8 6)
    (select paint 9 6) (select paint 10 6) (select paint 11 6)
    (select paint 12 6) (select paint 13 6)
    (select paint 14 6)))
(assert
  ((_ at-least 6) (select paint 0 7) (select paint 1 7) (select paint 2 7)
    (select paint 3 7) (select paint 4 7) (select paint 5 7)
    (select paint 6 7) (select paint 7 7) (select paint 8 7)
    (select paint 9 7) (select paint 10 7) (select paint 11 7)
    (select paint 12 7) (select paint 13 7)
    (select paint 14 7)))
(assert
  ((_ at-most 6) (select paint 0 7) (select paint 1 7) (select paint 2 7)
    (select paint 3 7) (select paint 4 7) (select paint 5 7)
    (select paint 6 7) (select paint 7 7) (select paint 8 7)
    (select paint 9 7) (select paint 10 7) (select paint 11 7)
    (select paint 12 7) (select paint 13 7)
    (select paint 14 7)))
(assert
  ((_ at-least 6) (select paint 0 8) (select paint 1 8) (select paint 2 8)
    (select paint 3 8) (select paint 4 8) (select paint 5 8)
    (select paint 6 8) (select paint 7 8) (select paint 8 8)
    (select paint 9 8) (select paint 10 8) (select paint 11 8)
    (select paint 12 8) (select paint 13 8)
    (select paint 14 8)))
(assert
  ((_ at-most 6) (select paint 0 8) (select paint 1 8) (select paint 2 8)
    (select paint 3 8) (select paint 4 8) (select paint 5 8)
    (select paint 6 8) (select paint 7 8) (select paint 8 8)
    (select paint 9 8) (select paint 10 8) (select paint 11 8)
    (select paint 12 8) (select paint 13 8)
    (select paint 14 8)))
(assert
  ((_ at-least 7) (select paint 0 9) (select paint 1 9) (select paint 2 9)
    (select paint 3 9) (select paint 4 9) (select paint 5 9)
    (select paint 6 9) (select paint 7 9) (select paint 8 9)
    (select paint 9 9) (select paint 10 9) (select paint 11 9)
    (select paint 12 9) (select paint 13 9)
    (select paint 14 9)))
(assert
  ((_ at-most 7) (select paint 0 9) (select paint 1 9) (select paint 2 9)
    (select paint 3 9) (select paint 4 9) (select paint 5 9)
    (select paint 6 9) (select paint 7 9) (select paint 8 9)
    (select paint 9 9) (select paint 10 9) (select paint 11 9)
    (select paint 12 9) (select paint 13 9)
    (select paint 14 9)))
(assert
  ((_ at-least 8) (select paint 0 10) (select paint 1 10) (select paint 2 10)
    (select paint 3 10) (select paint 4 10) (select paint 5 10)
    (select paint 6 10) (select paint 7 10) (select paint 8 10)
    (select paint 9 10) (select paint 10 10)
    (select paint 11 10) (select paint 12 10)
    (select paint 13 10) (select paint 14 10)))
(assert
  ((_ at-most 8) (select paint 0 10) (select paint 1 10) (select paint 2 10)
    (select paint 3 10) (select paint 4 10) (select paint 5 10)
    (select paint 6 10) (select paint 7 10) (select paint 8 10)
    (select paint 9 10) (select paint 10 10)
    (select paint 11 10) (select paint 12 10)
    (select paint 13 10) (select paint 14 10)))
(assert
  ((_ at-least 8) (select paint 0 11) (select paint 1 11) (select paint 2 11)
    (select paint 3 11) (select paint 4 11) (select paint 5 11)
    (select paint 6 11) (select paint 7 11) (select paint 8 11)
    (select paint 9 11) (select paint 10 11)
    (select paint 11 11) (select paint 12 11)
    (select paint 13 11) (select paint 14 11)))
(assert
  ((_ at-most 8) (select paint 0 11) (select paint 1 11) (select paint 2 11)
    (select paint 3 11) (select paint 4 11) (select paint 5 11)
    (select paint 6 11) (select paint 7 11) (select paint 8 11)
    (select paint 9 11) (select paint 10 11)
    (select paint 11 11) (select paint 12 11)
    (select paint 13 11) (select paint 14 11)))
(assert
  ((_ at-least 9) (select paint 0 12) (select paint 1 12) (select paint 2 12)
    (select paint 3 12) (select paint 4 12) (select paint 5 12)
    (select paint 6 12) (select paint 7 12) (select paint 8 12)
    (select paint 9 12) (select paint 10 12)
    (select paint 11 12) (select paint 12 12)
    (select paint 13 12) (select paint 14 12)))
(assert
  ((_ at-most 9) (select paint 0 12) (select paint 1 12) (select paint 2 12)
    (select paint 3 12) (select paint 4 12) (select paint 5 12)
    (select paint 6 12) (select paint 7 12) (select paint 8 12)
    (select paint 9 12) (select paint 10 12)
    (select paint 11 12) (select paint 12 12)
    (select paint 13 12) (select paint 14 12)))
(assert
  ((_ at-least 8) (select paint 0 13) (select paint 1 13) (select paint 2 13)
    (select paint 3 13) (select paint 4 13) (select paint 5 13)
    (select paint 6 13) (select paint 7 13) (select paint 8 13)
    (select paint 9 13) (select paint 10 13)
    (select paint 11 13) (select paint 12 13)
    (select paint 13 13) (select paint 14 13)))
(assert
  ((_ at-most 8) (select paint 0 13) (select paint 1 13) (select paint 2 13)
    (select paint 3 13) (select paint 4 13) (select paint 5 13)
    (select paint 6 13) (select paint 7 13) (select paint 8 13)
    (select paint 9 13) (select paint 10 13)
    (select paint 11 13) (select paint 12 13)
    (select paint 13 13) (select paint 14 13)))
(assert
  ((_ at-least 11) (select paint 0 14) (select paint 1 14) (select paint 2 14)
    (select paint 3 14) (select paint 4 14) (select paint 5 14)
    (select paint 6 14) (select paint 7 14) (select paint 8 14)
    (select paint 9 14) (select paint 10 14)
    (select paint 11 14) (select paint 12 14)
    (select paint 13 14) (select paint 14 14)))
(assert
  ((_ at-most 11) (select paint 0 14) (select paint 1 14) (select paint 2 14)
    (select paint 3 14) (select paint 4 14) (select paint 5 14)
    (select paint 6 14) (select paint 7 14) (select paint 8 14)
    (select paint 9 14) (select paint 10 14)
    (select paint 11 14) (select paint 12 14)
    (select paint 13 14) (select paint 14 14)))

(check-sat)
(define-fun-rec
  rowtoseq
  ((row Int) (index Int))
  (Seq Bool)
  (ite (>= index plen)
       (as seq.empty (Seq Bool))
       (seq.++
         (seq.unit (select paint row index))
         (rowtoseq row (+ index 1)))))
(define-fun
  show
  ((i Int))
  String
  (seq.map
    (lambda ((b Bool)) (ite b (_ Char 35) (_ Char 46)))
    (rowtoseq i 0)))
(eval (show 0))
(eval (show 1))
(eval (show 2))
(eval (show 3))
(eval (show 4))
(eval (show 5))
(eval (show 6))
(eval (show 7))
(eval (show 8))
(eval (show 9))
(eval (show 10))
(eval (show 11))
(eval (show 12))
(eval (show 13))
(eval (show 14))