search

dferri / z3-skyscrapers

Generate a skyscrapers puzzle game solver for z3
4 stars 0 forks source link

need help,thanks #2

Open Nooo455 opened 1 month ago

Nooo455 commented 1 month ago

Hello, how should I use it, I don't know how to uncomment (get-model)

dferri commented 1 month ago

First a bit of context: this script cannot be used by itself, the output of this script is a .smt2 file, which can be used as an input file for the Z3 theorem prover. If you're not familiar with Z3, I don't think this script will be useful/interesting for you!

Back to your question. After running the script, you'll obtain a .smt2 file like this one: https://github.com/dferri/z3-skyscrapers/blob/master/example.smt2#L92 As you can see, in the last line is:

; (get-model)

To uncomment it, simply edit the file to remove the ;:

(get-model)