Snippet of code for cellular automata solving

cellsat.py

# This code starts at line 1045...
# Imagine 1000 lines of frankensteined Python code that implements a (bad) SAT solver here

class CellSolver:
  def __init__(this, w, h, steps=1, rule_b=(3,), rule_s=(2,3), diagonals=True):
    assert steps >= 1
    assert w >= 1
    assert h >= 1

    # XXX: Only Conway's for now
    assert set(rule_b) == set([3])
    assert set(rule_s) == set([2,3])
    assert diagonals

    this.solver = Solver()
    this.solver.noexpensive = True
    this.steps = steps
    this.w = w
    this.h = h
    this.boards = []
    for g in range(steps):
      board = [this.solver.allocate_vars(w) for y in range(h)]
      this.boards.append(board)

    # RULES
    for g in range(1, steps):
      last = this.boards[g-1]
      cur = this.boards[g]
      #Sketch:

      #(ite last[ox, oy]
      #    (= this[ox, oy] rule_s(last_neighborhood))
      #    (= this[ox, oy] rule_b(last_neighborhood)))

      # either way needs a counter
      for y in range(h):
        for x in range(w):
          ns = []
          for ox, oy in [(-1, -1), (-1, 0), (-1, 1), (0, -1), (0, 1), (1, -1), (1, 0), (1, 1)]:
            dx, dy = x + ox, y + oy
            if dx < 0 or dy < 0 or dx >= w or dy >= h:
              continue
              # outside cells are bounded dead
            else:
              ns.append(last[dy][dx])
          """
          1<2<3<4 cel
          0 0 0 0 DEAD
          1 0 0 0 DEAD
          1 1 0 0 last
          1 1 1 0 LIVE
          1 1 1 1 DEAD

          -4 -c
          -3 4 c
          2 -c
          -2 3 -c l
          -2 3 c -l
          """
          c = cur[y][x]
          l = last[y][x]
          #print("g:%d; x,y: %d,%d; l=%d, c=%d; n=%r" % (g, x, y, l, c, ns))
          if len(ns) == 5 or len(ns) == 8:
            [c1, c2, c3, c4] = make_counter(this.solver, ns, 4)
            this.solver.make_clause([-c4,     -c])
            this.solver.make_clause([ c2,     -c])
            this.solver.make_clause([-c3, c4,  c])
            this.solver.make_clause([-c2, c3, -c,  l])
            this.solver.make_clause([-c2, c3,  c, -l])
          else:
            assert len(ns) == 3
            [c1, c2, c3] = make_counter(this.solver, ns, 3)
            this.solver.make_clause([ c2,     -c])
            this.solver.make_clause([-c3,      c])
            this.solver.make_clause([-c2, c3, -c,  l])
            this.solver.make_clause([-c2, c3,  c, -l])

    # BOUNDARY
    # ensure no cells would have spawned outside of the board for simulation correctness
    for g in range(0, steps - 1):
      brd = this.boards[g]
      for x in set([0, w - 1]):
        for y in range(1, h - 1):
          this.solver.make_clause([-brd[y+o][x] for o in [-1, 0, 1]])
      for y in set([0, h - 1]):
        for x in range(1, w - 1):
          this.solver.make_clause([-brd[y][x+o] for o in [-1, 0, 1]])

    this.solver.propagate()
    this.solver.noexpensive = False

  def pretty(this):
    for g in range(this.steps):
      print("== Gen %d ==" % g)
      brd = this.boards[g]
      for row in brd:
        charmap = {
          None: "?",
          True: "#",
          False: ".",
        }
        print("".join(charmap[cell.solver.val(l)] for l in row))