Help needed on using Z3 in Lean, with smt2_interface

Stream: general

[Dongwei Jiang]

I've been working on a prover of my own, and I'm keen on comparing its performance against Z3 using the same formalizations. I came across the smt2_interface in Lean, but I've found its documentation to be quite limited.

Would anyone be kind enough to guide me on how to use it effectively? Specifically, I'm looking for an example that demonstrates how to employ smt2_interface to solve simple problems, perhaps something akin to:

constant A : Prop
constant B : Prop
theorem test : ¬ (A ∨ B) → ¬ A ∧ ¬ B :=
begin

end

[Mario Carneiro]

smt2_interface is very old, it hasn't been updated since early lean 3 days

[Mario Carneiro]

A more recent project in the same vein is https://github.com/ufmg-smite/lean-smt

[Dongwei Jiang]

Mario Carneiro said:

A more recent project in the same vein is https://github.com/ufmg-smite/lean-smt

Thanks for your answer! But this repo seems be built with Lake. I'm mostly familiar with Lean 3 and leanpkg, is there some manual on what to change to make it useable in Lean 3?

[Mario Carneiro]

lean 3 is EOL, and downgrading is not supported. I highly recommend switching at this point, because otherwise there aren't any good options for making this work in lean 3 other than doing it yourself