Knuckledragger, a Semi-Automated Python Proof Assistant
philipzucker.com
philipzucker.com
Some things that I think work well for SMT solvers:
1. Bounded model checking for source code.
2. Finding solutions to constraint problems.
3. Design rule checking for hardware layout and logic gates.
Recently, I built a simple scheduling system using Z3. My wife is a librarian supervisor, and she's been spending hours each week creating schedules by hand. But, with a little Z3, one can enumerate the constraints and let it find a viable example. If the example doesn't work, add more constraints until it does.
Can you give an example of the kinds of constraints that need to get tweaked?
And do you have to tweak them in Z3 each time?
Disclaimer: I know almost nothing about Z3. I'm just picturing you trying to convince her that something like datalog has a learning curve that she'll Totally Be Glad she Powered Through, and she'll Thank you Later for Talking he Into It :)
I just hacked up a little shallow embedding via lex/yacc, using the C API. It's not pretty, but it was put together quickly to solve a problem.
As for typical constraints, there needs to be people on certain desks at certain times. People have to take breaks between N and M hours after starting. People have off-desk time that they use to perform other tasks that must be managed and must be contiguous. People have different numbers of hours they have to work, and a finite amount of time that they are allowed to be on a particular desk on a given day or week.
For instance, by default, this config sets a soft constraint that two people must be at the desk, and a hard constraint that no more than two people and at least one person must be at the desk. Likewise, there is a soft constraint that desk time must be contiguous, and a hard constraint that desk time must be at least so long to prevent continual splitting.
Numbers were such that you could only ever handle a fraction of the possible work. The throughout of a good allocation could be significantly higher than a naive one.
So you wanted to avoid to work with epsilon-delta in the reals
Question, do you use intuitionistic logic or classical logic?
If you use intuitionistic logic, why not model smooth infinitesimal analysis?
Anyway so does this mean that Z3 can't be used to prove intuitonistic arguments? That's surprising to me. What exactly makes SMT tied to classical logic?
edit: okay check out this https://dl.acm.org/doi/10.5555/1983702.1983729 the author used an embedding in order to represent intuitionistic formulas inside classical logic, so they could use Z3 anyway
I think embedding intuitionistic logic into z3 is possible in some sense and perhaps even useful. I would a priori expect a prover built from the ground up like nanoCoP-i to deal with intuitionistic logic to be better, even if it is orders of magnitude less complex than z3.
I don't think the concept of SMT is has to be tied to classical logic in some abstract sense, but the SMTlib standard is classical. And in the sense that an SMT solver is SAT solver (kind of as classical as you can get) bolted to theories. But seems reasonable to build some kind of framework bolting domain specific intuitionistic solvers to a intuitionistic fabric.
See Itauto https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.I... https://gitlab.inria.fr/fbesson/itauto which would be another interesting backend. Reusing tactics from other systems is maybe just a step too far for knuckledragger in terms of packaging and interfacing problems
Is this trying to prove things about Python code, or is it a Python interface to Z3, or something else?
It is not trying to prove things about python code.
It is building facilities and theory libraries around the pre-existing z3 python interface in a manner that can be reasonably called an interactive theorem prover. Hopefully, eventually, with a lower barrier to entry (and probably lower expressivity ceiling) than pre-existing systems like Lean, Coq, Isabelle.
I am targeting applications close to my heart, like calculus, differential equations, dynamical systems, numerical calculations, software verification. It is a tall order. No promises.
I have had a decent number of times where if I was told "write this code in this Python DSL, and then you can do interactive theorem proofs just on that bit", I would be pretty satisfied, even if it meant really cutting down what kind of objects I could use in the process.
If by "Record" you're referring to the Record helper in the blog post, that was nothing clever. Just a helper to define struct-like datatypes (record types).
I did do some experimentation using the python parser to turn python code into z3 expressions but I haven't pushed on that https://www.philipzucker.com/applicative_python/ It is a little annoying to not be able to use the nice native python if-then-else or match syntax.
https://amaranth-lang.org/docs/amaranth/latest/guide.html#co...
All of these seem to find solutions to user-provided constraint sets. They must be appropriate for different classes of problems, but it’s not obvious to me how that breaks out.
It’s, uh, been a long time since I last hand-rolled an optimization algorithm…
Prolog has some operational flavor to it. You can predict what it'll do. It can be used as "just" a programming language akin to python with fairly little logical/mathemtical content. Declarative Prolog as in constraint logic programming is in the realm of attacking similar logical problems to z3.
scipy.optimize is a grab bag of stuff. Some of it is pretty heuristic. It's all subject to floating point error, which is the devil we live with. The milp and lp solvers are relatives of how z3 handles linear inequality constraints. scipy.optimize doesn't treat logic at all really. It takes in mathematical multivariate functions and finds roots or minima.
Z3 is intended to be mathematically rigorous. It is less operational than prolog. On big combinatorial problems (SAT, bitvector problems), it is probably a superior tool. It does have an optimization interface, I haven't used it much.