I’m not sure what this is building up to, but another thing on my to-do list is to learn how to use the Z3 theorem prover. This repo is where I’m saving my experiments.
Example (1):
| ; https://stackoverflow.com/questions/30998111/executing-a-z3-script-in-command-line-prompt | |
| (declare-const a Int) | |
| (declare-fun f (Int Bool) Int) | |
| (assert (> a 10)) | |
| (assert (< (f a true) 100)) | |
| (check-sat) |
Example (2):
| ; https://stackoverflow.com/questions/13395391/z3-finding-all-satisfying-models | |
| (declare-const f Bool) | |
| (assert (or (= f true) (= f false))) | |
| (check-sat) |
Update (2019-01-17)
Added some examples.
Content © 2025 Richard Cook. All rights reserved.