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.
lloydatkinson 4 hours 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.
Bluestein 4 hours ago [-]
There's also a neat shm library by that name. Namespace's getting crowded :)
ascent817 3 hours ago [-]
I’m working on a DO-178C compliant verification suite for avionics software with Z3 at work, criminally underrated
greatgib 9 hours 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.
112233 8 hours ago [-]
oh, something new!
I thought Z3 is SAT/SMT solver, they must have added something.
Jaxan 8 hours 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.
baq 4 hours ago [-]
well a SAT solver is kinda sorta a theorem prover right...?
IshKebab 8 hours ago [-]
It is. Look up what SMT stands for.
NooneAtAll3 6 hours ago [-]
SMT is SAT+arithmetic, no?
IshKebab 4 hours ago [-]
Satisfiability Modulo Theories
mcphage 6 hours ago [-]
Shin Megami Tensei?
Bluestein 9 hours ago [-]
Or a BMW, or a groundbreaking electro mechanical computer, depending :)
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.
Z3 is a high-performance theorem prover being developed at Microsoft Research.