z3-rise4fun

Z3 tutorials from the rise4fun website

---

Project maintained by philzook58 Hosted on GitHub Pages — Theme by mattgraham

This is a reconstruction of the rise4fun Z3 website with a wasm compiled version of Z3 using z3-wasm. Since I originally did this, an official version has come online at https://microsoft.github.io/z3guide/ and javascript bindings are now in Z3 itself.

Tutorials

• Guide
• Fixedpoints
• Optimization
• Sequences
• Strategies

(declare-fun f (Int) Int) (declare-fun a () Int) ; a is a constant (declare-const b Int) ; syntax sugar for (declare-fun b () Int) (assert (> a 20)) (assert (> b a)) (assert (= (f 10) 1)) (check-sat) (get-model)

Resources

You may also be interested in

• https://github.com/philzook58/z3_tutorial (video)
• My Blog post about building this
• https://theory.stanford.edu/~nikolaj/programmingz3.html
• https://ericpony.github.io/z3py-tutorial/guide-examples.htm
• https://yurichev.com/writings/SAT_SMT_by_example.pdf