9 ms·
Programming the Z3 SMT solver
- euske 8y agoFantastic! Does anyone know the LaTeX source of this? I want to make a translation.
- rezahandzalah 8y agoThe end of the page says Created with https://www.madoko.net/ https://www.madoko.net/ Try contacting the authors?
- jononor 8y agoIt looks to be available at https://github.com/Z3Prover/doc/tree/master/programmingz3 https://github.com/Z3Prover/doc/tree/master/programmingz3 - see the programmingz3.mdk
- jononor 8y agoThis looks great. Have been playing with Z3py for component selection for electronics, which has been a bit hard with currently available documentation.
- shriphani 8y agoZ3 is such a brilliant piece of software - we've been using it for some small scheduling problems - such a godsend.
- vitaminCPP 8y agoWhat's the difference between using the Z3 library and using [sympy](www.sympy.org) a symbolic solving library?
- jahewson 8y agoSymPy is somewhat like Mathematica where it presents a wrapper around lots of underlying solvers. Z3 is one particular solver for a category of problems.
- whazor 8y agoZ3 opt is like magic
- amelius 8y agoI imagine that for complicated inputs, the solver will just "hang". Is this an issue in practice? Can you bound its runtime?
- shriphani 8y agohmm 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.
- jaunkst 8y agoCan I get a lam ns example of what z3 is and what it is?
- currymj 8y agoBasically, 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-with-z3-c2efe5051c8f https://medium.com/@ahelwer/checking-firewall-equivalence-wi...
- schoen 8y agoYou could be a little more precise and say that it's NP-complete. :-)
- OxO4 8y agoThat 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 http://smt2012.loria.fr/paper7.pdf
- schoen 8y agoThanks for the clarification! What do Z3 and other SMT solvers do if you ask them about undecidable questions? Do they potentially run forever?
- patsplat 8y agoFound these links helpful: https://en.m.wikipedia.org/wiki/Satisfiability_modulo_theories#Applications https://en.m.wikipedia.org/wiki/Satisfiability_modulo_theori... https://github.com/Z3Prover/z3/wiki/Slides https://github.com/Z3Prover/z3/wiki/Slides Appears to be useful for static analysis and verification of a program.
- vonuebelgarten 8y agoThis 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.
- msla 8y ago> 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.
- nickpsecurity 8y agoOn 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.
- fizixer 8y agoI thought Z3 is some cousin of the Z80 microprocessor.
- NikolaNovak 8y agoOh, I just assumed that it was about re-programming the manufacturer Engine Control Unit [ECU] of a BMW Z3 :-)
- dang 8y agoOk, we changed the title to that from "Programming Z3".
- Profan 8y agoOn the list of "cool things also happen to employ Z3", definitely check out MS Dafny programming language: https://github.com/Microsoft/dafny https://github.com/Microsoft/dafny
- eggy 8y agoHow does Dafny differ from Microsoft's F* (FStar)[1]? [1] https://www.fstar-lang.org/ https://www.fstar-lang.org/
- pjmlp 8y agoIt 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/2016/02/pldi117-yang.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/...
- eggy 8y agoThanks. I see the F#/F* synergy. Are C#/Dafny as similar to favor them over the F#/F* combo?
- lou1306 8y agoIvy [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/ http://microsoft.github.io/ivy/ [2]: http://vmcaischool19.tecnico.ulisboa.pt/~vmcaischool19.daemon/wp/wordpress/wp-content/uploads/2019/01/winterschool19.pptx http://vmcaischool19.tecnico.ulisboa.pt/~vmcaischool19.daemo... (PowerPoint slides)
- sudeepj 8y agoCan someone help to explain whether this is similar to TLA+?
- benbjohnson 8y agoZ3 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.
- sevensor 8y agoI 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.
- lou1306 8y agoIt seems to be fairly new. The bibliography includes lots of papers published last year.
- sigstoat 8y ago"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 https://yurichev.com/SAT_SMT.html
- mogambo097 8y agoThis tutorial also cites it.
- microcolonel 8y agoBeen trying out Souper, which uses Z3 underneath. It is pretty spectacular, what it is able to do.
- jononor 8y agoI struggled to find it on my phone, so here is a link. Souper is a LLVM optimizer; https://github.com/google/souper https://github.com/google/souper
- saurabh20n 8y agoZ3 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.
- enz 8y agoZ3 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?
- saurabh20n 8y agoThe 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-program-synthesis-101-294a9a35177 https://medium.com/@vidiborskiy/software-writes-software-pro... * Program synthesis to make smart contract security more accessible: https://medium.com/@vidiborskiy/program-synthesis-smart-contract-security-101-d708002b2198 https://medium.com/@vidiborskiy/program-synthesis-smart-cont... * Synthetic Minds (that is us): https://synthetic-minds.com/ 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.
- dhash 8y agoWe 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-formulas.pdf https://papers.nips.cc/paper/8233-learning-to-solve-smt-form... [2] https://www.trailofbits.com/services/blockchain-security/ https://www.trailofbits.com/services/blockchain-security/ [3] http://smtcomp.sourceforge.net/2018/ http://smtcomp.sourceforge.net/2018/
- 00N8 8y agoI even thought it might've been about the model BMW used to make (maybe it had pioneered something by having a more programmable ECU?)
- coffeetree 8y agoIs this still useful for managed languages? What is a practical use case for this for a Java/python web app?
- dons 8y agoSolving NP hard problems efficiently.
- amelius 8y agoI know that every NP problem can be written as an SMT problem, theoretically speaking. But is that actually practical?
- KirinDave 8y agoThe 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.
- spawarotti 8y agoZ3 is used by IntelliTest: https://docs.microsoft.com/en-us/visualstudio/test/generate-unit-tests-for-your-code-with-intellitest?view=vs-2017 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/deconstructing-dynamic-symbolic-execution/ 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/2013/06/paper_tap13.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/...
- Animats 8y agoAw. 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 https://www.cs.tau.ac.il/~msagiv/courses/ATP/p245-nelson.pdf [2] https://github.com/John-Nagle/pasv https://github.com/John-Nagle/pasv
- zimpenfish 8y agoOh, 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.)
- nullc 8y agoFWIW, 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.
- zimpenfish 8y ago> 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.
- evancox100 8y agoWhy are types called sorts in this field? Or is there a difference I'm missing?