SMTLIB generation and semantics

Stream: general

[Joe Hendrix]

Is there a library for representing and rendering SMTLIB 2 expressions that is compatible with Lean 3? I'd like to have a library where I can generate SMTLIB (specifically the uninterpreted functions/sorts, bitvectors, and arrays), and express semantically what it means for a set of SMTLIB assertions to be satisfiable from a model-theoretic definition. I can start one, but don't want to duplicate existing work.

[Sebastian Ullrich]

We have https://github.com/leanprover/smt2_interface. It should still work, hopefully

[Joe Hendrix]

Thanks, it looks like this has most of what I'd want. Is this intended to be ported to be compatible with Lean4? I'd like to also define a model theory for SMTLIB. Is that something that you think would be welcome in this repo?

[Sebastian Ullrich]

I don't think we have any specific plans for this package, but hopefully it should be quick to port. I don't have any specific thoughts about what should go in the package either, but perhaps it could be a separate package on top of smt2_interface?