SMT (Z3) bindings

Stream: Program verification

[Alcides Fonseca]

I understand at some point there was a smt tactic in lean. Is there any documentation on how to use an smt solver (z3 would be ideal for me) from Lean?

[Johan Commelin]

There is still a bunch of smt stuff in core

[Johan Commelin]

I've never used it

[Bryan Gin-ge Chen]

I remember Mario recently saying that nobody has ever used it.

If you figure it out, please let us know!

[Alcides Fonseca]

There is just a tactic that provides debugging for seeing the SMT state. But as far as I know, SMT is only used inside the c++ core.

-- This tactic is just a placeholder, designed to be modified for specific performance experiments

[Simon Hudon]

I think @Jesse Michael Han uses it frequently

[Gabriel Ebner]

There are two different questions here:

1. About the internal SMT state (i.e. begin[smt] ... end, by cc): calling this SMT is a bit of a stretch. There is no SAT solver, and it only knows about congruence closure (with AC) and heuristic instantiation. At least by cc is used somewhat often in mathlib.
2. Interfacing with external SMT solvers. Jared had an unverified interface to Z3 at one point: https://github.com/leanprover/smt2_interface This allows you to call Z3 on Lean goals (including some arithmetic), but it doesn't do proofs.

[Gabriel Ebner]

The Z3 interface is completely unused, AFAIK.

[Alcides Fonseca]

Thanks! I was looking for that second one!

[Bryan Gin-ge Chen]

#1083 is related, but uses Vampire, not Z3.

[Jesse Michael Han]

any invocation of finish dips into the internal SMT state (via heuristic instantiation + congruence closure)

[Joe Hendrix]

I used the lean3 SMT tactic for congruence-closure type-problems -- it worked fine, but as noted it's not really the same as an SMT solver.