The Z3 Theorem Prover

137 29 7 years ago

I seem to have somehow forgotten or missed the fact that it was MIT re-licensed a couple of years ago, instead of the previous "no commercial use" stuff. Thanks for the submission!

hyper_reality• 7 years ago

I've used Z3 a lot for CTF challenges, but in my day-to-day work have never encountered any problems that it would be useful for. I'm interested to know how people have used it in the course of their work?

glangdale4• 7 years ago

I have a super-optimizer for SIMD coding built out of Z3. It is not yet fit for public consumption, but I've already found some sequences faster than anything I had before, which is nice.

jfries• 7 years ago

I would be super interested in more details on how that works. What do you actually pass to z3 to solve?

microcolonel• 7 years ago

There's also souper, which is a generic superoptimizing pass for LLVM which can use Z3 (or most other popular SMT solvers).

pyb• 7 years ago

How was Z3 useful for CTFs ?

0xdada2• 7 years ago

You can solve many keygen type reverse engineering challenges with z3.

michael_fine• 7 years ago

You can implement pretty powerful type checkers as constraint based systems. I used Z3 in a project called LightDP to verify differential privacy as a property of the type system.

brians• 7 years ago

I use it for running LARPs: characterize the roles to play, survey players to elicit constraints and preferences, and meet constraints while optimizing preferences.

https://github.com/briansniffen/autocaster

I did something similar for reassigning seats in my office—loud people together, someone who needs it near the restroom, people generally near their team leads, that sort of thing. Too much personal information to share here.

thanatropism• 7 years ago

I've been wanting to write a DSL for solving room scheduling problems (and similar) with SAT (i.e. translate to DPLL). Put up a simple front-end, receives text that gets added to the constraint base.

Your thing seems so much more powerful. I wonder if this UI idea would make it more usable.

(Wait, are we reinventing expert systems?)

JohnStrangeII• 7 years ago

This is not really meant as a critique, more of a general suggestion for implementers to improve their docs. As someone who teaches logic and works with standard logics from time to time (HOL with Lambek Calculus, normal and classical modal logics, and plain old FOL), I've found it unnecessarily hard to figure out from the docs with what logics you can implement in them, whether you can just load these and use them, how to enter formulas, how to prove things, how to construct models, etc. This all seems overcomplicated in these tools, and almost all of them seem to mix up completely unrelated programming languages with logic. Couldn't this all be simpler?

I understand that the typical use cases for these solvers are different. Still, I often wish there was a tool that I can just fire up, choose modal logic EMC from a menu and check whether a certain formula is a theorem. So far, it has always turned out easier for me to do this by hand than using a theorem prover.

IvanK_net• 7 years ago

"I often wish there was a tool that I can just fire up, choose modal logic EMC from a menu and check whether a certain formula is a theorem."

We would not need any mathematicians then :D

dhash3• 7 years ago

Yeah I wish there was a better logic chart than [1], or at least one that I can give it something in MSOL and it can internally compile it to a representation in one of those logics.

[1] http://smtlib.cs.uiowa.edu/logics.shtml

tiredneurons2• 7 years ago

read this it's seriously good https://exhaustedneurons.github.io/abstractions/

gjm11• 7 years ago

It's OK, I guess, but it has rather little to do with the subject here. If you want to publicize your blog here, please do it by submitting a link rather than by barging into a largely unrelated discussion to shout about how good your own blogpost is.

tiredneurons2• 7 years ago

okay

The Z3 Theorem Prover

Related Stories