Advertisement
Guest User

Untitled

a guest
May 27th, 2018
67
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 2.89 KB | None | 0 0
  1. import sys
  2. from z3 import *
  3.  
  4.  
  5.  
  6. # Find evaluation of formula.
  7. # Return answer YES with machine's steps or NO
  8. def printEvaluation(phi, B, width, height, SX, SY):
  9. s = Solver()
  10. s.add(phi)
  11.  
  12. # TODO if many evaluations x != model[x]
  13. if s.check() == sat:
  14. model = s.model()
  15.  
  16. printNanogram(s.model(), B, width, height)
  17. else:
  18. print "unsolvable"
  19.  
  20.  
  21.  
  22. # Print machine steps for input word
  23. def printNanogram(model, B, width, height):
  24. for r in range(height):
  25. s = ""
  26. for c in range(width):
  27. if model[B[r][c]]:
  28. s += '#'
  29. else:
  30. s += '.'
  31. print(s)
  32.  
  33.  
  34.  
  35. # Print machine configuration
  36. def starts(index, n, ivals, S):
  37. last = len(ivals) - 1
  38. ands = []
  39. ands.append(0 <= S[index][0])
  40. ands.append(S[index][last] + ivals[last] <= n)
  41.  
  42. for i in range(last):
  43. ands.append(S[index][i] + ivals[i] < S[index][i+1])
  44.  
  45. return ands
  46.  
  47.  
  48.  
  49. def fieldType(c, r, x, y, SX, SY, B):
  50. if len(SX[c]) == 0 or len(SY[r]) == 0:
  51. return (Not(B[r][c]))
  52.  
  53. subphi = And(intervalphi(r, c, x[c], SX), intervalphi(c, r, y[r], SY))
  54. return (And(Implies(B[r][c], subphi), Implies(subphi, B[r][c])))
  55.  
  56.  
  57.  
  58. def intervalphi(inElem, fixElem, ivals, S):
  59. if len(ivals) == 1:
  60. return And(S[fixElem][0] <= inElem, inElem < S[fixElem][0] + ivals[0])
  61. else:
  62. return Or([ And(S[fixElem][i] <= inElem, inElem < S[fixElem][i] + ivals[i]) for i in range(len(ivals)) ])
  63.  
  64.  
  65.  
  66. # Parse input
  67. def parseInitInfo():
  68. width, height = map(int, sys.stdin.readline().split())
  69. return width, height
  70.  
  71.  
  72.  
  73. def parseRows(n):
  74. rows = []
  75. for i in range(0,n):
  76. row = map(int, sys.stdin.readline().split())[:-1]
  77. rows.append(row)
  78. return rows
  79.  
  80.  
  81.  
  82. # ==================== MAIN ==================
  83.  
  84. # ============ Read from input =============
  85. width, height = parseInitInfo()
  86. y = parseRows(height)
  87. x = parseRows(width)
  88.  
  89.  
  90. # ========= Create variables for formula ===============
  91. SX = [ [ Int('SX_' + str(i) + '_' + str(k)) for k in range(len(x[i])) ] for i in range(width) ]
  92. SY = [ [ Int('SY_' + str(i) + '_' + str(k)) for k in range(len(y[i])) ] for i in range(height) ]
  93. B = [ [ Bool('B_' + str(i) + '_' + str(k)) for k in range(width) ] for i in range(height) ]
  94.  
  95.  
  96. print(SX)
  97. print(SY)
  98.  
  99. # ============== Create formula ============
  100. ands = []
  101.  
  102. # Create starts for intervals in rows and columns
  103. for i in range(height):
  104. if (len(y[i]) > 0):
  105. ands.extend(starts(i, width, y[i], SY))
  106.  
  107. for i in range(width):
  108. if (len(x[i]) > 0):
  109. ands.extend(starts(i, height, x[i], SX))
  110.  
  111. # Create every field
  112. for r in range(height):
  113. for c in range(width):
  114. ands.append(fieldType(c, r, x, y, SX, SY, B))
  115.  
  116. print(ands)
  117.  
  118.  
  119. # ========= Calculate formula ===========
  120. printEvaluation(And(ands), B, width, height, SX, SY)
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement