sudoku.py

gistfile1.txt

from copy import deepcopy
from types import SimpleNamespace

from hypothesis import note, settings
from hypothesis.stateful import (invariant, precondition, rule,
                                 RuleBasedStateMachine)

DIM = 3
SIZE = DIM * DIM


class GuessError(Exception):
    pass


class Sudoku2(RuleBasedStateMachine):

    def __init__(self):
        super().__init__()
        self.possibilities = []
        self.board = []
        for i in range(SIZE):
            self.board.append([])
            self.possibilities.append([])
        for i in range(SIZE):
            for j in range(SIZE):
                self.board[i].append(0)
                self.possibilities[i].append([])
        self.start()
        self.setup()

    def printb(self):
        for i in range(SIZE):
            print(self.possibilities[i])

    def start(self):
        self.board[0] = [0, 5, 0, 9, 0, 0, 0, 0, 0]
        self.board[1] = [0, 0, 9, 0, 0, 0, 0, 3, 0]
        self.board[2] = [0, 0, 0, 0, 1, 0, 0, 4, 0]
        self.board[3] = [6, 0, 0, 0, 0, 0, 0, 0, 0]
        self.board[4] = [8, 0, 0, 4, 0, 0, 0, 6, 0]
        self.board[5] = [7, 0, 0, 5, 0, 0, 9, 2, 8]
        self.board[6] = [9, 0, 6, 0, 3, 2, 1, 0, 0]
        self.board[7] = [0, 2, 0, 0, 0, 5, 0, 0, 0]
        self.board[8] = [0, 0, 0, 0, 0, 0, 0, 0, 4]

    def setup(self):
        self.progress = True
        self.guess_error = False
        self.context = []
        for i in range(SIZE):
            for j in range(SIZE):
                if not self.board[i][j]:
                    self.possibilities[i][j] = list(range(1, SIZE + 1))
                else:
                    self.possibilities[i][j] = [self.board[i][j]]

    def check4(self, pos):
        # print('+++++ check4 ++++++', pos)
        # self.print_board()
        for i in range(SIZE):
            if len(self.possibilities[pos[i][0]][pos[i][1]]) == 1:
                target = self.possibilities[pos[i][0]][pos[i][1]][0]
                for j in range(SIZE):
                    if i == j:
                        continue
                    if target in self.possibilities[pos[j][0]][pos[j][1]]:
                        # print('--- removing %d from %d,%d' % (target, pos[j][0], pos[j][1]))
                        self.possibilities[pos[j][0]][pos[j][1]].remove(target)
                        if len(self.possibilities[pos[j][0]][pos[j][1]]) <= 0:
                            raise GuessError
                        self.progress = True
        for j in range(1, SIZE + 1):
            count = 0
            for i in range(SIZE):
                if j in self.possibilities[pos[i][0]][pos[i][1]]:
                    count += 1
            if count <= 0:
                raise GuessError
            if count == 1:
                for i in range(SIZE):
                    if len(self.possibilities[pos[i][0]][pos[i][1]]) > 1 and \
                            j in self.possibilities[pos[i][0]][pos[i][1]]:
                        self.possibilities[pos[i][0]][pos[i][1]] = [j]
                        # print('--- setting to %d from %d,%d' % (j, pos[i][0], pos[i][1]))
                        self.progress = True
        # self.print_board()

    @precondition(lambda self: not self.progress and self.guess_error)
    @rule()
    def reguess(self):
        # go to next guess on stack
        print('+++++ RE-GUESS ++++++')
        # self.print_board()
        last_context = self.context[-1]
        while last_context.guess <= 0:
            print('+++++ LOOPING IN RE-GUESS ++++++')
            self.context.pop()
            last_context = self.context[-1]
        self.possibilities = deepcopy(last_context.data)
        pos = last_context.pos
        i = pos // SIZE
        j = pos % SIZE
        last_context.guess -= 1
        # print('--- reguess %d of %s' % (last_context.guess, self.possibilities[i][j]))
        self.possibilities[i][j] = [self.possibilities[i][j][last_context.guess]]
        self.progress = True
        self.guess_error = False
        # self.print_board()

    def get_next_pos(self, cur_pos):
        while True:
            cur_pos += 1
            i = cur_pos // SIZE
            j = cur_pos % SIZE
            if i >= SIZE:
                assert False
            len1 = len(self.possibilities[i][j])
            if len1 > 1:
                return cur_pos, len1 - 1

    @precondition(lambda self: not self.progress and not self.guess_error)
    @rule()
    def guess(self):
        # import pdb; pdb.set_trace()
        print('+++++ GUESS ++++++')
        # self.print_board()
        # push new guess on stack
        # check if last guess
        # if so, pop from stack and move on to next guess
        last_pos = self.context[-1].pos if self.context else 0
        pos, guess = self.get_next_pos(last_pos)
        i = pos // SIZE
        j = pos % SIZE
        data = deepcopy(self.possibilities)
        # print('--- guess %d of %s' % (guess, self.possibilities[i][j]))
        self.possibilities[i][j] = [self.possibilities[i][j][guess]]
        new_context = SimpleNamespace()
        new_context.pos = pos
        new_context.guess = guess
        new_context.data = data
        self.context.append(new_context)
        self.progress = True
        # self.print_board()

    @precondition(lambda self: self.progress)
    @rule()
    def reduce(self):
        self.print_board()
        while self.progress:
            self.progress = False
            try:
                for y in range(SIZE):
                    self.check4([(y, x) for x in range(SIZE)])
                    self.check4([(x, y) for x in range(SIZE)])
                for z1 in range(DIM):
                    for z2 in range(DIM):
                        sq1 = [(x + z1 * DIM, y + z2 * DIM) for x in range(
                            DIM) for y in range(DIM)]
                        self.check4(sq1)
                # self.print_board()
            except GuessError:
                self.progress = False
                self.guess_error = True
            items = [y for x in self.possibilities for y in x if len(y) > 1]
            if not items:
                break
            self.print_board()

    @invariant()
    def all_done(self):
        items = [y for x in self.possibilities for y in x if len(y) > 1]
        if len(items) == 0:
            self.write_notes()
            assert False

    def print_board(self):
        for x in self.possibilities:
            for y in range(SIZE):
                print(' ' if len(x[y]) > 1 else x[y][0], end=' ')
            print(' ')
        print('----------------')

    def write_notes(self):
        for x in self.possibilities:
            note([x[y][0] for y in range(SIZE)])


# The default of 200 is sometimes not enough for Hypothesis to find
# a falsifying example.
Sudoku2.TestCase.settings = settings(stateful_step_count=9999999)
DieHardTest = Sudoku2.TestCase