Ask a machine whether a claim always holds
A claim is a statement such as "a price times a quantity is never negative". A solver is a program that can say whether a claim always holds, or hand you one case where it fails.
Z3 is a free solver. Here you learn to ask it a question and to read its two answers, sat and unsat.
By the end of this lesson
Note
I can ask Z3 whether a claim always holds.
Key words
| Word | What it means | Example |
|---|---|---|
| Claim | a statement that should be true for every case | |
| Solver | a program that looks for values that fit some rules | |
| sat | short for satisfiable: some values fit the rules | |
| unsat | short for unsatisfiable: no values fit the rules | |
| Model | the values a solver found, one case that fits | |
| Assert | to hand the solver one rule | (assert (> x 3)) |
The cells students fill in are left blank in this preview.
A solver answers sat or unsat
You tell Z3 what numbers exist, then give it rules, then ask. declare-const makes a number. assert adds a rule. check-sat asks whether any values fit all the rules. get-model prints them.
Z3 writes an operation first and its inputs after: (> x 10) means x is above 10.
Find a number that fits
echo '(declare-const x Int) (assert (and (> x 10) (< x 20) (= (mod x 7) 0))) (check-sat) (get-model)' | z3 -inShown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
Ask for a number that cannot exist
echo '(declare-const x Int) (assert (and (> x 10) (< x 20) (= (mod x 7) 0) (= (mod x 3) 0))) (check-sat)' | z3 -inShown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
To prove a claim, refute its opposite
Z3 finds cases, so to prove a claim you ask for a case where the claim is false. If none exists, the claim holds for every case.
You assert the rules, then assert (not claim). The answer unsat means the opposite is impossible, so the claim is proved. The answer sat means the model is a counterexample.
Worked example: two claims about whole numbers
| Claim | Rules | Z3 answer | Meaning |
|---|---|---|---|
| x times y is above 0 | x above 0, y above 0 | unsat | Proved for all such x and y |
| x squared is above y squared | x above y | sat | Refuted: a counterexample exists |
The cells students fill in are left blank in this preview.
Prove a product is positive
echo '(declare-const x Int) (declare-const y Int) (assert (and (> x 0) (> y 0))) (assert (not (> (* x y) 0))) (check-sat)' | z3 -inShown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
Refute a claim about squares
echo '(declare-const x Int) (declare-const y Int) (assert (> x y)) (assert (not (> (* x x) (* y y)))) (check-sat) (get-model)' | z3 -inShown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
A common mistake
Warning
Many people think unsat means the claim is false. The question was about the opposite of the claim. So unsat means the opposite is impossible and the claim is true, and sat means the claim is false. Read the answer against the sentence (not claim).
Check the rules can be true at all
Rules that contradict each other have no solution. Then every claim looks proved, because the opposite of any claim is also impossible.
The next two Runs show it. Both rules and one claim give unsat. So always ask the rules alone first. If they are unsat, the proof means nothing.
Ask the rules alone
echo '(declare-const x Int) (assert (> x 5)) (assert (< x 3)) (check-sat)' | z3 -inShown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
A claim proved from nothing
echo '(declare-const x Int) (assert (> x 5)) (assert (< x 3)) (assert (not (> x 1000))) (check-sat)' | z3 -inShown here, not run. Create a free account to press Run and type it into your own lab’s terminal.