SMT names that match Lean names #26

dranov · 2024-05-16T08:20:45Z

This is a draft PR addressing #7. I am still working on this, but want some feedback early.

As of now, sorts and terms in SMT-LIB get names that are derived from the Lean names. There are a few remaining hiccups:

etoms are still named stmi_<N>
inductive data types have constructors named cifvar_<N>– I'm not sure what is going on there
disposable names, used for quantifier binders, still have uninformative names, e.g. stmd_80

See the test case in Test/SmtTranslation/Names.lean for a large example.

As part of this PR, I also want to give the valid_fact_<N> assertions (part of unsat cores) potentially more user-readable names, matching the hypothesis in the Lean context where auto is called. That seems more straightforward.

dranov · 2024-05-16T08:27:33Z

@PratherConid I'm not sure where to get etom names. What do they correspond to on the Lean side? Could you please point me in the right direction?

dranov · 2024-05-16T09:30:53Z

Auto/Tactic.lean

  let lamEVarTy ← LamReif.getLamEVarTy
+  trace[auto.lamReif.printValuation] "lamEVarTy: {lamEVarTy}"


One thing I'm confused about is also that printValuation (in LamReif.lean) doesn't print any Etom lines (suggesting lamEVarTy is empty), but this prints lamEVarTy: [#0, #1, #1, #2] on the Names.lean example.

Is printValuation called too early?

etoms do not correspond to Lean expressions, but they have types, so printValuation only prints lamEVarTy.

etoms are created by skolemization. Maybe we can use names like sk_<num>.

Some automated theorem provers use sk for skolems, but other names are also ok.

dranov · 2024-05-16T09:32:40Z

Auto/Translation/Assumptions.lean

+inductive Origin where
+  /-- The `<num>`-th definitional equality associated with def `<name>` -/
+  | defEq : Name → Nat → Origin
+  /-- Lemmas hard-wired into Lean-auto -/
+  | hwLem : Name → Origin
+  /-- Lemma from local context -/
+  | lctxLem : Name → Origin
+  /-- User-provided lemma, with the string being a serialisation of the term -/
+  | userLem : String → Origin
+  /-- Lemma from lemma database -/
+  | lemDbLem : Name → Name → Origin
+  /-- Inhabitation fact from local context -/
+  | lctxInh : Name → Origin
+  /-- Inhabitation instance synthesized for canonicalized type -/
+  | tyCanInh : Origin
+  /-- Inductive type recursor -/
+  | recursor : Name → Origin
+  /-- Rewrite -/
+  | rewrite : Origin
+  /-- Lemma proved by native prover -/
+  | byNative : Name → Origin
+  /-- Catch-all for string-based origins -/
+  | generic : String → Origin


I've begun to add some structure to the stringly-typed proof trees. The goal is to eventually extract a user-readable lemma name from the DTr of assertions in the unsat core.

dranov · 2024-05-16T09:35:07Z

Auto/Tactic.lean

+  -- GEORGE: do we need to pass more of `LamReif:State` to `lamFOL2SMT`?
+  let lamVarTy ← LamReif.getVarVal
+  trace[auto.lamReif.printValuation] "lamVarTy: {lamVarTy}"
  let lamEVarTy ← LamReif.getLamEVarTy
+  trace[auto.lamReif.printValuation] "lamEVarTy: {lamEVarTy}"
+  let tyVal ← LamReif.getTyVal
+  trace[auto.lamReif.printValuation] "tyVal: {tyVal}"
  let exportLamTerms ← exportFacts.mapM (fun re => do
    match re with
    | .valid [] t => return t
    | _ => throwError "runAuto :: Unexpected error")
-  let commands ← (lamFOL2SMT lamVarTy lamEVarTy exportLamTerms exportInds).run'
+  let commands ← (lamFOL2SMT lamVarTy lamEVarTy tyVal exportLamTerms exportInds).run'


We're threading a lot of the LamReif State into lamFOL2SMT and associated functions. Would it be cleaner to make this part of relevant monad?

If yes, could you suggest how to do that? I haven't worked with monads in Lean before.

Your approach looks good to me. Using a monad might make things cleaner, but I'm not sure. Anyways, I'll clean up the code when you're done, so you can keep going for now.

dranov · 2024-05-17T04:36:37Z

With regards to disposableName (used in lamQuantified2STerm), is the original Lean name of the binder kept anywhere?

PratherConid · 2024-05-17T04:53:53Z

No, Lean-auto does not keep the name of the original binder. I did not include it in LamTerm because it might affect the performance of the checker.

PratherConid · 2024-05-17T04:56:55Z

I think you can also ignore this for now. Supporting SMT binder names that correspond to Lean binder names will require systematic changes to the codebase. An easier approach would be giving binders names like a, b, c.

dranov · 2024-05-17T05:55:59Z

Alright, that's fair. For now I've settled on taking the binder names from the associated sorts, so for instance you now get n<idx> for a binder of sort node rather than smtd_<idx>.

We thread `tyVal` through the functions in `LamFOL2SMT.lean`, to get access to the mapping from sort/type IDs to Lean types, so we can give informative names. It might be better to roll this into a monad?

See `Test/SmtTranslation/Names.lean` for an example.

Rather than `stmd_<idx>`, we now get a hint from the sort of the binder, using the first character of the sort name, so instead of `stmd_55` we now have something like `n55` for a binder of sort `node`.

dranov · 2024-05-17T06:44:04Z

I've removed the unrelated commit making DTr less stringly-typed. I will probably make a separate PR containing that commit to give assertions names closer to the Lean names.

dranov · 2024-05-17T06:46:11Z

@PratherConid I guess this is good enough for now. Could you please take a look, clean-up as necessary, and merge?

PratherConid · 2024-05-17T12:19:22Z

ok

Auto/IR/SMT.lean

PratherConid · 2024-05-18T12:09:03Z

Auto/Translation/LamFOL2SMT.lean

@@ -429,21 +453,23 @@ def termAuxDecls : Array IR.SMT.Command :=
  `valid_fact_{i}` corresponds to the `i`-th entry in `facts`
 -/
 def lamFOL2SMT
-  (lamVarTy lamEVarTy : Array LamSort)
+  (lamVarTy : Array (Expr × LamSort))


Inappropriate naming across entire file! Should be named varVal because it contains the valuation of the term.

Valuation for term atoms should be eta-reduced. This is likely an issue irrelevent to this pull request.

PratherConid · 2024-05-18T12:16:55Z

← PrettyPrinter.formatTerm (← PrettyPrinter.delab e).raw might also be used to pretty-print DTr.

PratherConid · 2024-05-18T12:32:05Z

Auto/IR/SMT.lean

+def SMTReservedWords : HashSet String :=
+  let reserved := #[ "as", "let", "exists", "forall", "match", "par",
+    "assert", "check-sat", "check-sat-assuming",
+    "declare-const", "declare-datatype", "declare-datatypes",
+    "declare-fun", "declare-sort", "define-fun", "define-fun-rec", "define-funs-rec",
+    "define-sort", "echo", "exit", "get-assertions", "get-info",
+    "get-model", "get-option", "get-proof", "get-unsat-assumptions",
+    "get-unsat-core", "get-value", "pop", "push", "reset", "reset-assertions",
+    "set-info", "set-logic", "set-option"]
+  reserved.foldl (fun hs s => hs.insert s) {}


Not sufficient. Pre-defined symbols in SMT-lib like +, -, *, /, %, ... and auxiliary definitions in Lean-auto like iemod should be excluded. Individual SMT solvers also have pre-defined symbols.

Already causing issue in
example : (∀ (xs ys zs : List α), xs ++ ys ++ zs = xs ++ (ys ++ zs)) := by auto [List.append_assoc]
after previous pretty-print commit.

@dranov The reserved words also contain numeral, decimal and string, but there is no guarantee that Lean's pretty printer won't print them. I'm feeling that using absolutely no predetermined prefix (previously smti_) for Lean-auto generated names is causing too much trouble. Can we maybe add something like _ as a prefix?

PratherConid · 2024-05-18T13:26:53Z

I'll merge the pull request for now.

PratherConid · 2024-05-18T18:14:44Z

Made some significant changes in ff56bdb, behaviour on SMTTranslation/Names.lean becomes a bit different.

dranov commented May 16, 2024

View reviewed changes

dranov added 3 commits May 17, 2024 14:37

Generate informative names for terms and sorts

c8f3e76

We thread `tyVal` through the functions in `LamFOL2SMT.lean`, to get access to the mapping from sort/type IDs to Lean types, so we can give informative names. It might be better to roll this into a monad?

Projection funs and constructors print; etoms don't

9fe3345

See `Test/SmtTranslation/Names.lean` for an example.

More readable names for binders

5fbf23a

Rather than `stmd_<idx>`, we now get a hint from the sort of the binder, using the first character of the sort name, so instead of `stmd_55` we now have something like `n55` for a binder of sort `node`.

dranov force-pushed the smt-names branch from 4cbb575 to 5fbf23a Compare May 17, 2024 06:40

dranov marked this pull request as ready for review May 17, 2024 06:45

PratherConid reviewed May 18, 2024

View reviewed changes

Auto/IR/SMT.lean Show resolved Hide resolved

PratherConid reviewed May 18, 2024

View reviewed changes

Auto/IR/SMT.lean Outdated Show resolved Hide resolved

change smtNameFromExpr

8de91a0

PratherConid reviewed May 18, 2024

View reviewed changes

fix monomorphization

aaddd71

PratherConid merged commit 3d35c74 into leanprover-community:main May 18, 2024
2 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

SMT names that match Lean names #26

SMT names that match Lean names #26

dranov commented May 16, 2024 •

edited

Loading

dranov commented May 16, 2024

dranov May 16, 2024

PratherConid May 16, 2024

PratherConid May 16, 2024

PratherConid May 16, 2024

dranov May 16, 2024

dranov May 16, 2024

PratherConid May 16, 2024

dranov commented May 17, 2024

PratherConid commented May 17, 2024

PratherConid commented May 17, 2024

dranov commented May 17, 2024

dranov commented May 17, 2024 •

edited

Loading

dranov commented May 17, 2024

PratherConid commented May 17, 2024

PratherConid May 18, 2024

PratherConid May 18, 2024

PratherConid commented May 18, 2024

PratherConid May 18, 2024

PratherConid May 18, 2024

PratherConid May 18, 2024

PratherConid May 18, 2024

PratherConid commented May 18, 2024

PratherConid commented May 18, 2024

		let lamEVarTy ← LamReif.getLamEVarTy
		trace[auto.lamReif.printValuation] "lamEVarTy: {lamEVarTy}"

SMT names that match Lean names #26

SMT names that match Lean names #26

Conversation

dranov commented May 16, 2024 • edited Loading

dranov commented May 16, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

dranov commented May 17, 2024

PratherConid commented May 17, 2024

PratherConid commented May 17, 2024

dranov commented May 17, 2024

dranov commented May 17, 2024 • edited Loading

dranov commented May 17, 2024

PratherConid commented May 17, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

PratherConid commented May 18, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

PratherConid commented May 18, 2024

PratherConid commented May 18, 2024

dranov commented May 16, 2024 •

edited

Loading

dranov commented May 17, 2024 •

edited

Loading