Homework 7A starter

cook-levin.py

from z3 import *

# Must specify a single-tape deterministic Turing machine.


class Tm:

  def __init__(self):
    self.states = set(["s", "r00", "r11", "r01", "r10", "l", "lx", "qA", "qR"])
    self.start_state = "s"
    self.accept_state = "qA"
    self.reject_state = "qR"
    self.delta = [
      ("s", "0", "r00", "x", "R"),
      ("s", "1", "r11", "x", "R"),
      ("s", "x", "qA", "x", "R"),
      ("s", "_", "qR", "_", "R"),
      ("r00", "0", "r00", "0", "R"),
      ("r00", "1", "r01", "1", "R"),
      ("r00", "x", "lx", "x", "R"),
      ("r00", "_", "lx", "_", "L"),
      ("r01", "0", "r00", "0", "R"),
      ("r01", "1", "r01", "1", "R"),
      ("r01", "x", "qR", "1", "R"),
      ("r01", "_", "qR", "1", "R"),
      ("r10", "0", "r10", "0", "R"),
      ("r10", "1", "r11", "1", "R"),
      ("r10", "x", "qR", "1", "R"),
      ("r10", "_", "qR", "1", "R"),
      ("r11", "0", "r10", "0", "R"),
      ("r11", "1", "r11", "1", "R"),
      ("r11", "x", "lx", "x", "L"),
      ("r11", "_", "lx", "_", "L"),
      ("lx", "0", "l", "x", "L"),
      ("lx", "1", "l", "x", "L"),
      ("lx", "x", "qA", "x", "L"),
      ("lx", "_", "qR", "x", "L"),
      ("l", "0", "l", "0", "L"),
      ("l", "1", "l", "1", "L"),
      ("l", "x", "s", "x", "R"),
      ("l", "_", "qR", "x", "R"),
    ]

    self.input_alphabet = ["_", "0", "1"]
    self.tape_alphabet = ["_", "0", "1", "x"]
    self.state = None
    self.input = []


# Our verifier.
tm = Tm()

### 1. Variables ###

# max of p(n) time steps / tape cells
pn = 16

# The main Z3 solver object. Add constraints to this.
s = Solver()

# Q_{q,t} for each q \in Q and 0 <= t < p(n).
Q = dict()
for q in tm.states:
  Q[q] = []
  for t in range(pn):
    Q[q].append(Bool(f"{q}_{t}"))

# TODO: H_{i,t} for each 0 <= i < pn, 0 <= t < pn
# TODO: X

# 1. The machine starts off in its start state.
s.add(Q[tm.start_state][0])

# TODO: 2. The head starts off at the left edge

# TODO: 3. Each tape cell has some symbol in it at each point in time.

# TODO: At time 0, only input symbols allowed.

# TODO: At time 1+, any tape symbols allowed

# TODO: 4. You end up in an accept state.

# TODO: Never enter a reject state

# TODO: 5. Each step of the machine is computed according to the transition.
#       Right, Left
#       If the head is not in the immediate vicinity, copy.

# TODO: 6a. If you're in one state, you're not in another.
for q in tm.states:
  for r in tm.states:
    if q == r:
      continue
    for t in range(pn):
      clause = Implies(Q[q][t], Not(Q[r][t]))
      s.add(clause)


# TODO: 6b. If your head is somewhere, it's not somewhere else.

# TODO: Head must be somewhere at each time step.

# TODO: 6c. If something is written on a tape cell, nothing else is written there.

print(s.check())
m = s.model()
print(m)

# TODO: Output