olooney3 days ago
I like Z3 a lot. I think it's criminally underappreciated and underused. Here is a fairly interesting use I put it to a few years ago:
https://www.oranlooney.com/post/playfair/#known-plaintext-at...
Slightly more complicated than the toy examples shown in the documentation above, and hints at one of the real world use cases for Z3 - red teaming cryptography.
That said, I'm not sure the documentation linked above is really doing it any favors in terms of helping popularizing it.
lloydatkinson3 days ago
How does it compare to the others? I started trying to use Zinc but I get lost in all the vocabulary and literature which assumes you already have a background in it.
Bluesteinop3 days ago
There's also a neat shm library by that name. Namespace's getting crowded :)
greatgib3 days ago
If anyone wondering, because it took me a few hops to find out:
Z3 is a high-performance theorem prover being developed at Microsoft Research.
1122333 days ago
oh, something new! I thought Z3 is SAT/SMT solver, they must have added something.
Jaxan3 days ago
Sometimes you can use SMT for “theorem proving”. It is a rather broad term. I don’t think they added something much different than what they already had.
baq3 days ago
well a SAT solver is kinda sorta a theorem prover right...?
IshKebab3 days ago
It is. Look up what SMT stands for.
NooneAtAll33 days ago
SMT is SAT+arithmetic, no?
IshKebab3 days ago
Satisfiability Modulo Theories
mcphage3 days ago
Shin Megami Tensei?
Bluesteinop3 days ago
Or a BMW, or a groundbreaking electro mechanical computer, depending :)
number63 days ago
I was hoping for the mechanical computer...
okokwhatever3 days ago
nailed!
ascent8173 days ago
I’m working on a DO-178C compliant verification suite for avionics software with Z3 at work, criminally underrated