Programming the Z3 SMT solver | Hacker News Reader

Programming the Z3 SMT solver

theory.stanford.edu

251 pointspplonski8653 comments

Aw. It's been a very long time, but I used the original Oppen-Nelson simplifier, the ancestor of all SMT solvers.[1] We used it inside the Pascal-F verifier, around 1981.

Two years ago I found the sources for that in my garage and put them on Github.[2] The section "CPC4" is the modified (by Derek Oppen) Oppen-Nelson simplifier. This was originally in Franz LISP, and I converted them to Common LISP in 2017. It's not fully debugged, but it will run the basic solvers - add, subtract, multiply by constant, equality, inequality, theory of arrays, theory of structures, booleans, conditionals. That theory is completely decidable, and it covers most of the problems that cause range and subscript errors.

[1] https://www.cs.tau.ac.il/~msagiv/courses/ATP/p245-nelson.pdf [2] https://github.com/John-Nagle/pasv

"SAT/SMT by Example" that appeared on the front page a day or two ago is also good, if you missed it.

https://yurichev.com/SAT_SMT.html

This tutorial also cites it.

Z3 is such a brilliant piece of software - we've been using it for some small scheduling problems - such a godsend.

What's the difference between using the Z3 library and using [sympy](www.sympy.org) a symbolic solving library?

SymPy is somewhat like Mathematica where it presents a wrapper around lots of underlying solvers. Z3 is one particular solver for a category of problems.

Z3 opt is like magic

I imagine that for complicated inputs, the solver will just "hang". Is this an issue in practice? Can you bound its runtime?

hmm so Z3 has a timeout option you can set.

In our experience we haven't really seen it hang or do anything out of the ordinary - unsat problems on average seem to take longer than sat problems (it probably needs to scan a lot more).

We've pushed it to about a million variables or so and it has handled it well thought we might only be a the lower end of workloads.

On the list of "cool things also happen to employ Z3", definitely check out MS Dafny programming language: https://github.com/Microsoft/dafny

How does Dafny differ from Microsoft's F* (FStar)[1]?

[1] https://www.fstar-lang.org/

It is more C# like, and was used to write one of the Singularity post OSes at MS Research.

"Automated Verification of a Type-Safe Operating System"

https://www.microsoft.com/en-us/research/wp-content/uploads/...

Thanks. I see the F#/F* synergy. Are C#/Dafny as similar to favor them over the F#/F* combo?

Ivy [1] is another research language built around Z3. Slides from a recent presentation of the language are also available [2]. The concept of exploiting modularity to obtain decidable verification conditions is quite interesting. Plus, it compiles down to C++.

[1]: http://microsoft.github.io/ivy/

[2]: http://vmcaischool19.tecnico.ulisboa.pt/~vmcaischool19.daemo... (PowerPoint slides)

Z3 is amazing. I have been working with it since 2007. We are now building program synthesizers using it. Having a solid system to do the heavy lifting is a life saver.

Z3 seems cool and I want to try but I must admit I fail to see how to use it for a real world project. Do you have a blog post talking about your Z3 use for your project?

The below were written for a semi- or non-technical audience, and only address your curiosity tangentially, but better than nothing:

* Program synthesis overview: https://medium.com/@vidiborskiy/software-writes-software-pro...

* Program synthesis to make smart contract security more accessible: https://medium.com/@vidiborskiy/program-synthesis-smart-cont...

* Synthetic Minds (that is us): https://synthetic-minds.com/

You can help by telling me what questions would be most informative to answer. Promise to write a post addressing them directly.

We at Radix Labs (S18) use Z3 (and CVC4/SyGuS) heavily as a library to solve place-and-route problems for goal directed robot path planning problems.

Its facilities for program construction over the integers, sets, bitvectors, and reals make it an ideal candidate for this, especially when leveraging nu-Z3 for optimization over these.

With Z3, we’re able to construct optimized routes for robots extremely fast (especially with extensions over the techniques described in [1]), and as a direct result, derive value for our customers as execution time is important when dealing with expensive equipment.

A couple of my friends over at trail of bits do the work that saurabh does at synthetic minds, and their code is open source so you can take a look at it. [2]

It’s a decently active field of research, with solvers trading blows in the annual SMT-COMP [3]. check out their instances to see how people really use them.

[1] https://papers.nips.cc/paper/8233-learning-to-solve-smt-form...

[2] https://www.trailofbits.com/services/blockchain-security/

[3] http://smtcomp.sourceforge.net/2018/

Trail of bits is not building anything in program synthesis.

Out of curiosity, what made you choose Z3 over other SMT solvers? Also, if you have benchmarks that you can publish, it would be really great if you could submit them to SMT-LIB/SMT-COMP [0] such that they can be used to improve SMT solvers.

[0] https://smt-comp.github.io/news/2019-01-24.html

About the benchmarks, SMT-LIB has had my instances for close to a decade now :) [1,2] We are now generating non-bitvector benchmarks, and maybe in the Fall we will submit newer instances.

Back in the day, I was foolish enough to implement my own (bitvector) solver. Hoping to outcompete with the assumption that I could encode heuristics informed by the domain (i.e., synthesis-specific). Turned out Z3's "general" heuristics were just faster. You could say, I let Nikolaj and Leonardo take it from there. For completeness, I also did experiment with a bunch of other solvers that were considered good at the time [3]. (Have to caveat with the fact that CVC3, now CVC4, has always been on my list of future-to-try.)

---

[1] VS3: QF_BV (bitvector benchmarks) https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_B... -- apologies for the unimaginative name. VS3 stands for "(V)erification and (S)ynthesis using (S)MT (S)olvers"

[2] Example SMT instance: https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_B...

[3] Engineering for synthesis using SMT solvers: Chapter 6 of PhD: http://saurabh-srivastava.com/pubs/saurabh-srivastava-thesis...

This looks great. Have been playing with Z3py for component selection for electronics, which has been a bit hard with currently available documentation.

Oh, this might be helpful. I tried optimising the linear typewriter (appeared on HN a couple of weeks back) using Z3 but it got nowhere useful even leaving it for a couple of hours to churn (contrast with simulated annealing which took 10 seconds per run and got good results >70% of runs).

(I suspect just because optimising 26! permutations is HARD.)

FWIW, for that kind of search problem, I've found it useful to use a solver (or simpler exhaustive searches) on small windows as a local search, while continuing to use a stochastic search at the global level.

E.g. consider a window of (say) 6 keys and ask if any of the 6! permutations of them are better, for each possible window over the keyboard. This is similar to n-opt in TSP.

Make N as big as you can before your search falls down. Also try making a random move and local searching the region around the random move. Try all ~n^2 pairs of n/2 windows to jointly optimize. etc.

You can also make the local searches small by grouping keys and then search for the best permutation of whole group rather than single keys. Then alternate to windows of single keys.

> consider a window of (say) 6 keys and ask if any of the 6! permutations of them are better

I imagined something similar - since we can reasonably assume that XJQZKV are doing to be at the outer edges, we can take it from 26! to 6!20!. But even constraining it as much as possible, we still end up with 6!6!6!8! and 29 years of searching.

But I'll definitely give the sliding window approach a go, yeah.

Can someone help to explain whether this is similar to TLA+?

Z3 is a low-level solver that tools are usually built on top of. TLA+ is a higher level language that uses an SMT solver underneath.

I could swear this didn't exist when I was learning how to use Z3. Is it new? Did I just fail to find it? At any rate, it clears up a lot of points I was confused about. Tremendously glad this was posted.

It seems to be fairly new. The bibliography includes lots of papers published last year.

Can I get a lam ns example of what z3 is and what it is?

Basically, it solves the problem of finding a setting of variables that is compatible with some set of constraints. This is NP-hard but Z3 is in practice very fast nonetheless.

A case study/glowing review from a programmer at Microsoft is here:

https://medium.com/@ahelwer/checking-firewall-equivalence-wi...

You could be a little more precise and say that it's NP-complete. :-)

That actually depends on the logic being used. Some of the logics supported by Z3 are not even decidable. In fact, even solving quantifier-free bit-vector formulas is NEXPTIME-complete [0] when using a binary encoding.

[0] http://smt2012.loria.fr/paper7.pdf

Thanks for the clarification!

What do Z3 and other SMT solvers do if you ask them about undecidable questions? Do they potentially run forever?

Found these links helpful:

https://en.m.wikipedia.org/wiki/Satisfiability_modulo_theori... https://github.com/Z3Prover/z3/wiki/Slides

Appears to be useful for static analysis and verification of a program.

Is this still useful for managed languages? What is a practical use case for this for a Java/python web app?

Solving NP hard problems efficiently.

I know that every NP problem can be written as an SMT problem, theoretically speaking. But is that actually practical?

The answer to that question is, "Yes, if your SMT solver has strategies that provide good results for the problem in question."

Unless you're implementing solvers or caught up on the particulars of a solver's implementation, the best way to gauge this is to try it.

Z3 is used by IntelliTest: https://docs.microsoft.com/en-us/visualstudio/test/generate-...

You can use it to answer questions like "I want to reach this statement in this C# method, what values this method's inputs have to have for the execution to pass all the if checks and so on to reach this statement?".

More broadly speaking, you can use Z3 as a solver for Dynamic Symbolic Execution engine, where DSE is described in:

https://www.microsoft.com/en-us/research/publication/deconst...

Source: I am the first author of "Generating Test Suites with Augmented Dynamic Symbolic Execution" leveraging Z3: https://www.microsoft.com/en-us/research/wp-content/uploads/...

Why are types called sorts in this field? Or is there a difference I'm missing?

Fantastic! Does anyone know the LaTeX source of this? I want to make a translation.

The end of the page says Created with https://www.madoko.net/

Try contacting the authors?

It looks to be available at https://github.com/Z3Prover/doc/tree/master/programmingz3 - see the programmingz3.mdk

This is an example of title that could benefit from a simple, non-editorialized, and purely factual change: "Programming the Z3 SMT solver".

I am sure I was not the first to think it was related to Konrad Zuse's Z3.

> I am sure I was not the first to think it was related to Konrad Zuse's Z3.

The Zuse Z3 is literally the only thing I know of which hooks up with the abbreviation "Z3" in the context of computers.

On contrary, there's tons of papers published today referencing Z3, Why3, and so on. I immediately knew they meant the solver since that's the Z3 people use most today.

I thought Z3 is some cousin of the Z80 microprocessor.

Oh, I just assumed that it was about re-programming the manufacturer Engine Control Unit [ECU] of a BMW Z3 :-)

Ok, we changed the title to that from "Programming Z3".

Been trying out Souper, which uses Z3 underneath. It is pretty spectacular, what it is able to do.

I struggled to find it on my phone, so here is a link. Souper is a LLVM optimizer; https://github.com/google/souper

I even thought it might've been about the model BMW used to make (maybe it had pioneered something by having a more programmable ECU?)

Reply on news.ycombinator.com