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.
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.
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.
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++.
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.
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.
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.)
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?
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.
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.
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.
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:
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.
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:
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.
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