You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

70 lines
2.1 KiB

  1. # coding: utf-8
  2. import os, sys
  3. from z3 import *
  4. # get the playground information
  5. if len(sys.argv) != 2:
  6. print("Usage: python3 square.py <test-file>")
  7. sys.exit(0)
  8. with open(sys.argv[1]) as f:
  9. playground = f.read()
  10. rows = playground.strip().split("\n")
  11. playground = [[None if x == "_" else int(x) for x in r.split()] for r in rows]
  12. # get the playground size
  13. size_y = len(playground)
  14. assert(size_y != 0)
  15. size_x = len(playground[0])
  16. assert(size_x != 0)
  17. assert(size_x == size_y)
  18. #################################### Square ####################################
  19. # create the solver
  20. solver = Solver()
  21. # todo: create an integer variable for each playground cell
  22. # hint: use something like the coordinates as part of the variable name
  23. numbers = [[None for _j in range(size_x)] for _j in range(size_y)]
  24. for i in range(size_y):
  25. for j in range(size_x):
  26. pass # ... replace this with your code ...
  27. # todo: assign each known number the corresponding value from playground
  28. for i in range(size_y):
  29. for j in range(size_x):
  30. pass # ... replace this with your code ...
  31. # todo: declare a variable for the sum of all columns, rows and diagonals
  32. # ... your code goes here ...
  33. # todo: enfoce that each column sums up to the declared variable
  34. for j in range(size_x):
  35. pass # ... replace this with your code ...
  36. # todo: enfoce that each row sums up to the declared variable
  37. for i in range(size_y):
  38. pass # ... replace this with your code ...
  39. # todo: enfoce that both diagonals sum up to the declared variable
  40. # ... your code goes here ...
  41. diag1 = [numbers[i][i] for i in range(size_y)]
  42. diag2 = [numbers[i][size_y - i - 1] for i in range(size_y)]
  43. # call the solver and check satisfiability
  44. res = solver.check()
  45. if res != sat:
  46. print("unsat")
  47. sys.exit(1)
  48. # print the model
  49. m = solver.model()
  50. for i in range(size_y):
  51. results = []
  52. for j in range(size_x):
  53. num = numbers[i][j]
  54. results.append("_" if num is None else m[num].as_long())
  55. print(("%4s" * len(results)) % tuple(results))
  56. ################################################################################