runAutoGetHints now also returns unsatCoreDerivLeafStrings

Auto/Tactic.lean

@@ -154,7 +154,7 @@ def collectLctxLemmas (lctxhyps : Bool) (ngoalAndBinders : Array FVarId) : Tacti
         continue
       if ¬ decl.isAuxDecl ∧ (← Meta.isProp type) then
         let name ← fVarId.getUserName
-        lemmas := lemmas.push ⟨⟨mkFVar fVarId, type, .leaf s!"lctxLem {name}"⟩, #[]⟩
+        lemmas := lemmas.push ⟨⟨mkFVar fVarId, type, .leaf s!"lctxLem {name} (fvarId: {fVarId.name})"⟩, #[]⟩
     return lemmas
 
 def collectUserLemmas (terms : Array Term) : TacticM (Array Lemma) :=
@@ -418,7 +418,7 @@ def querySMT (exportFacts : Array REntry) (exportInds : Array MutualIndInfo) : L
 abbrev solverLemmas := Array (String × Expr × Nat × Expr) × List Expr × List Expr × List Expr × List Expr × List Expr × List (List Expr)
 
 open Embedding.Lam in
-def querySMTForHints (exportFacts : Array REntry) (exportInds : Array MutualIndInfo) : LamReif.ReifM (Option solverLemmas) := do
+def querySMTForHints (exportFacts : Array REntry) (exportInds : Array MutualIndInfo) : LamReif.ReifM (Option (Array String × solverLemmas)) := do
   let lamVarTy := (← LamReif.getVarVal).map Prod.snd
   let lamEVarTy ← LamReif.getLamEVarTy
   let exportLamTerms ← exportFacts.mapM (fun re => do
@@ -454,11 +454,14 @@ def querySMTForHints (exportFacts : Array REntry) (exportInds : Array MutualIndI
       let e ← Lam2D.interpLamTermAsUnlifted tyValMap varValMap etomValMap 0 t
       trace[auto.smt.unsatCore.leanExprs] "|valid_fact_{id}| : {← Core.betaReduce e}"
     )
-  -- **Print derivation of unsatCore**
+  -- **Print derivation of unsatCore and collect unsatCore derivation leaves**
+  -- `unsatCoreDerivLeafStrings` contains all of the strings that appear as leaves in any derivation for any fact in the unsat core
+  let mut unsatCoreDerivLeafStrings := #[]
   for id in unsatCoreIds do
     let .some t := exportLamTerms[id]?
       | throwError "runAuto :: Index {id} of `exportLamTerm` out of range"
     let vderiv ← LamReif.collectDerivFor (.valid [] t)
+    unsatCoreDerivLeafStrings := unsatCoreDerivLeafStrings ++ vderiv.collectLeafStrings
     trace[auto.smt.unsatCore.deriv] "|valid_fact_{id}| : {vderiv}"
   -- **Build symbolPrecMap using l2hMap and selInfos**
   let (preprocessFacts, theoryLemmas, instantiations, computationLemmas, polynomialLemmas, rewriteFacts) := solverHints
@@ -516,7 +519,7 @@ def querySMTForHints (exportFacts : Array REntry) (exportInds : Array MutualIndI
           | none => ruleInstances.mapM (fun lemTerm => Parser.SMTTerm.parseTermAndAbstractSelectors lemTerm symbolMap selectorMVars)
       )
     let solverLemmas := (selectorArr, preprocessFacts, theoryLemmas, instantiations, computationLemmas, polynomialLemmas, rewriteFacts)
-    return some solverLemmas
+    return some (unsatCoreDerivLeafStrings, solverLemmas)
   else
     let preprocessFacts ← preprocessFacts.mapM (fun lemTerm => Parser.SMTTerm.tryParseTermAndAbstractSelectors lemTerm symbolMap selectorMVars)
     let theoryLemmas ← theoryLemmas.mapM (fun lemTerm => Parser.SMTTerm.tryParseTermAndAbstractSelectors lemTerm symbolMap selectorMVars)
@@ -542,7 +545,7 @@ def querySMTForHints (exportFacts : Array REntry) (exportInds : Array MutualIndI
     let polynomialLemmas := polynomialLemmas.filterMap id
     let rewriteFacts := rewriteFacts.map (fun rwFacts => rwFacts.filterMap id)
     let solverLemmas := (selectorArr, preprocessFacts, theoryLemmas, instantiations, computationLemmas, polynomialLemmas, rewriteFacts)
-    return some solverLemmas
+    return some (unsatCoreDerivLeafStrings, solverLemmas)
 
 open LamReif Embedding.Lam in
 /--
@@ -706,16 +709,18 @@ def evalAuto : Tactic
       absurd.assign proof
 | _ => throwUnsupportedSyntax
 
-/-- Run `auto`'s monomorphization and preprocessing, then return the list of preprocessing and theory lemmas output
-    by the SMT solver. -/
-def runAutoGetHints (lemmas : Array Lemma) (inhFacts : Array Lemma) : MetaM solverLemmas := do
+/-- Runs `auto`'s monomorphization and preprocessing, then returns:
+    - `unsatCoreDerivLeafStrings` which contains the String of every leaf node in every derivation of a fact in the unsat core
+    - `lemmas` which contains all of the extra lemmas generated by the SMT solver (that were used in the final proof) -/
+def runAutoGetHints (lemmas : Array Lemma) (inhFacts : Array Lemma) : MetaM (Array String × solverLemmas) := do
   -- Simplify `ite`
   let ite_simp_lem ← Lemma.ofConst ``Auto.Bool.ite_simp (.leaf "hw Auto.Bool.ite_simp")
   let lemmas ← lemmas.mapM (fun lem => Lemma.rewriteUPolyRigid lem ite_simp_lem)
   -- Simplify `decide`
   let decide_simp_lem ← Lemma.ofConst ``Auto.Bool.decide_simp (.leaf "hw Auto.Bool.decide_simp")
   let lemmas ← lemmas.mapM (fun lem => Lemma.rewriteUPolyRigid lem decide_simp_lem)
-  let afterReify (uvalids : Array UMonoFact) (uinhs : Array UMonoFact) (minds : Array (Array SimpleIndVal)) : LamReif.ReifM solverLemmas := (do
+  let afterReify (uvalids : Array UMonoFact) (uinhs : Array UMonoFact) (minds : Array (Array SimpleIndVal))
+    : LamReif.ReifM (Array String × solverLemmas) := (do
     let exportFacts ← LamReif.reifFacts uvalids
     let mut exportFacts := exportFacts.map (Embedding.Lam.REntry.valid [])
     let _ ← LamReif.reifInhabitations uinhs
@@ -726,17 +731,17 @@ def runAutoGetHints (lemmas : Array Lemma) (inhFacts : Array Lemma) : MetaM solv
     -- runAutoGetHints only supports SMT right now
     -- **SMT**
     if auto.smt.get (← getOptions) then
-      if let .some lemmas ← querySMTForHints exportFacts exportInds then
-        return lemmas
+      if let .some (unsatCoreDerivLeafStrings, lemmas) ← querySMTForHints exportFacts exportInds then
+        return (unsatCoreDerivLeafStrings, lemmas)
     throwError "autoGetHints only implemented for cvc5 (enable option auto.smt)"
     )
-  let (lemmas, _) ← Monomorphization.monomorphize lemmas inhFacts $ fun s => do
-    let callAfterReify : Reif.ReifM solverLemmas := do
+  let ((unsatCoreDerivLeafStrings, lemmas), _) ← Monomorphization.monomorphize lemmas inhFacts $ fun s => do
+    let callAfterReify : Reif.ReifM (Array String × solverLemmas) := do
       let u ← computeMaxLevel s.facts
       (afterReify s.facts s.inhTys s.inds).run' {u := u}
     callAfterReify.run s
   trace[auto.tactic] "Auto found preprocessing and theory lemmas: {lemmas}"
-  return lemmas
+  return (unsatCoreDerivLeafStrings, lemmas)
 
 syntax (name := autoGetHints) "autoGetHints" autoinstr hints (uord)* : tactic
 
@@ -868,7 +873,7 @@ def evalAutoGetHints : Tactic
     match instr with
     | .none =>
       let (lemmas, inhFacts) ← collectAllLemmas hints uords (goalBinders.push ngoal)
-      let (selectorInfos, lemmas) ← runAutoGetHints lemmas inhFacts
+      let (_, selectorInfos, lemmas) ← runAutoGetHints lemmas inhFacts
       IO.println s!"Auto found hints. Time spent by auto : {(← IO.monoMsNow) - startTime}ms"
       let allLemmas :=
         lemmas.1 ++ lemmas.2.1 ++ lemmas.2.2.1 ++ lemmas.2.2.2.1 ++ lemmas.2.2.2.2.1 ++

Auto/Translation/Assumptions.lean

@@ -23,6 +23,10 @@ partial def DTr.toString : DTr → String
 instance : ToString DTr where
   toString := DTr.toString
 
+partial def DTr.collectLeafStrings : DTr → Array String
+| .node _ dtrs => dtrs.foldl (fun acc l => acc ++ l.collectLeafStrings) #[]
+| .leaf s => #[s]
+
 /--
   Universe monomprphic facts
   User-supplied facts should have their universe level parameters