Generate a skyscrapers puzzle game solver for z3
The first argument is the size of the grid
Indexes from 0 while the actual skyscraper's height starts from 1
To solve this puzzle:
Run the command:
python z3-skyscrapers.py 5 r2=2 u1=5 l1=3 d0=3 d3=4 r4c3=2
E.g. the file example.smt2 was generated with:
python z3-skyscrapers.py 5 r2=2 u1=5 l1=3 d0=3 d3=4 r4c3=2 > example.smt2
Run and uncomment (get-model) to get the solution and fill the grid!
Puzzle's images from Conceptis Puzzles