Working Notes: a commonplace notebook for recording & exploring ideas.
Home. Site Map. Subscribe. More at expLog.

Z3

I've always been extremely curious about using solvers for managing software dynamics and writing fast software, because most of design (and planning) seems to be constraint solving under some forms of uncertainty and noise.

November 2025

2025-11-16

A tutorial on the Z3 api showed up on Hacker news and I decided to take some time to play with the API and take some notes along with that.

• The python package to install is z3-solver, the z3 pypi package seems to be something else.
• import z3 has pretty much everything. Types for defining variables
• expressions can parsed as well, reminds me of Python
• Solver is the class to collect constraints against
• model: solution for the set of asserted constraints
  • model is an interpretation that makes each asserted constraint true
• use statistics to see time spent
• can also model machine arithmetic
  • (maybe can also extend to quantized arithmetic?)
• formula/constraint is valid if it's true for any assignments (proof of statement)
• satisfiable if it's true for some assignment (finding a solution)
• prove command, checks if the inverse is unsatisfiable
• can use lists for matrix creation

— Kunal