Advertisement
Guest User

Untitled

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