search

leanprover-community / lean-auto

Experiments in automation for Lean
Apache License 2.0
72 stars 12 forks source link

Feature requests: Meaningful UNSAT cores and Models in Lean #5

Open mww-aws opened 11 months ago

mww-aws commented 11 months ago

Is it possible / meaningful to get UNSAT cores or models in a format that is meaningful in Lean?

We are representing domain models and some queries against those models. We would (if possible) like to get witnesses to proof failures expressed in a meaningful way back into Lean, and to get UNSAT cores that have meaning in Lean.

The underlying idea is that we want users to be able to "ask questions" about domain models by checking whether partially instantiated ground terms are conformant with the model and then presenting the results back in a meaningful way.

Mostly I am curious whether this is on your roadmap for any point in the future.

PratherConid commented 11 months ago

Yes! It will be one of the first features I'll implement after Jan 7th next year.

PratherConid commented 5 months ago

Now there's basic support for unsat cores. auto.smt.unsatCore.smtTerms shows the SMT terms of the unsat core, and auto.smt.printValuation prints the Lean expressions corresponding to SMT uninterpreted functions/sorts. The next step I'll implement is to directly print Lean expressions corresponding to SMT terms in the unsat core.

PratherConid commented 5 months ago

237f06ca0778fb258b2d0cb5f2d9eef6e9505344 implements Lean expression printing for SMT unsat cores. Use set_option trace.auto.smt.unsatCore.leanExprs true.