Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- import sys
- from z3 import *
- # Find evaluation of formula.
- # Return answer YES with machine's steps or NO
- def printEvaluation(phi, B, width, height, SX, SY):
- s = Solver()
- s.add(phi)
- # TODO if many evaluations x != model[x]
- if s.check() == sat:
- model = s.model()
- print ("SX")
- for i in range(len(SX)):
- for j in range(len(SX[i])):
- print(str(model[SX[i][j]].as_long()))
- print ("SY")
- for i in range(len(SY)):
- for j in range(len(SY[i])):
- print(str(model[SY[i][j]].as_long()))
- #model[T[i][step]].as_long()
- #if
- printNanogram(s.model(), B, width, height)
- else:
- print "unsolvable"
- # Print machine steps for input word
- def printNanogram(model, B, width, height):
- for r in range(height):
- s = ""
- for c in range(width):
- if model[B[r][c]]:
- s += '#'
- else:
- s += '.'
- print(s)
- # Print machine configuration
- def starts(index, n, ivals, S):
- last = len(ivals) - 1
- ands = []
- ands.append(0 <= S[index][0])
- ands.append(S[index][last] + ivals[last] <= n)
- for i in range(last):
- ands.append(S[index][i] + ivals[i] < S[index][i+1])
- return ands
- def fieldType(c, r, x, y, SX, SY, B):
- if len(SX[c]) == 0 or len(SY[r]) == 0:
- return (Not(B[r][c]))
- subphi = And(intervalphi(r, c, x[c], SX), intervalphi(c, r, y[r], SY))
- return (And(Implies(B[r][c], subphi), Implies(subphi, B[r][c])))
- def intervalphi(inElem, fixElem, ivals, S):
- if len(ivals) == 1:
- return And(S[fixElem][0] <= inElem, inElem < S[fixElem][0] + ivals[0])
- else:
- return Or([ And(S[fixElem][i] <= inElem, inElem < S[fixElem][i] + ivals[i]) for i in range(len(ivals)) ])
- # Parse input
- def parseInitInfo():
- width, height = map(int, sys.stdin.readline().split())
- return width, height
- def parseRows(n):
- rows = []
- for i in range(0,n):
- row = map(int, sys.stdin.readline().split())[:-1]
- rows.append(row)
- return rows
- # ==================== MAIN ==================
- # ============ Read from input =============
- width, height = parseInitInfo()
- y = parseRows(height)
- x = parseRows(width)
- # ========= Create variables for formula ===============
- SX = [ [ Int('SX_' + str(i) + '_' + str(k)) for k in range(len(x[i])) ] for i in range(width) ]
- SY = [ [ Int('SY_' + str(i) + '_' + str(k)) for k in range(len(y[i])) ] for i in range(height) ]
- B = [ [ Bool('B_' + str(i) + '_' + str(k)) for k in range(width) ] for i in range(height) ]
- print(SX)
- print(SY)
- # ============== Create formula ============
- ands = []
- # Create starts for intervals in rows and columns
- for i in range(height):
- if (len(y[i]) > 0):
- ands.extend(starts(i, width, y[i], SY))
- for i in range(width):
- if (len(x[i]) > 0):
- ands.extend(starts(i, height, x[i], SX))
- # Create every field
- for r in range(height):
- for c in range(width):
- ands.append(fieldType(c, r, x, y, SX, SY, B))
- print(ands)
- # ========= Calculate formula ===========
- printEvaluation(And(ands), B, width, height, SX, SY)
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement