Zulip Chat Archive

Stream: Program verification

Topic: SMT (Z3) bindings


view this post on Zulip Alcides Fonseca (Jun 03 2020 at 13:12):

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?

view this post on Zulip Johan Commelin (Jun 03 2020 at 13:27):

There is still a bunch of smt stuff in core

view this post on Zulip Johan Commelin (Jun 03 2020 at 13:27):

I've never used it

view this post on Zulip Bryan Gin-ge Chen (Jun 03 2020 at 13:30):

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

If you figure it out, please let us know!

view this post on Zulip Alcides Fonseca (Jun 03 2020 at 13:47):

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

view this post on Zulip Simon Hudon (Jun 03 2020 at 14:35):

I think @Jesse Michael Han uses it frequently

view this post on Zulip Gabriel Ebner (Jun 03 2020 at 14:42):

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.

view this post on Zulip Gabriel Ebner (Jun 03 2020 at 14:42):

The Z3 interface is completely unused, AFAIK.

view this post on Zulip Alcides Fonseca (Jun 03 2020 at 15:16):

Thanks! I was looking for that second one!

view this post on Zulip Bryan Gin-ge Chen (Jun 03 2020 at 15:19):

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

view this post on Zulip Jesse Michael Han (Jun 03 2020 at 18:45):

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

view this post on Zulip Joe Hendrix (Jun 18 2020 at 21:37):

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.


Last updated: May 08 2021 at 22:13 UTC