Changed solverLemmas output to solverHints output

Auto/Tactic.lean

@@ -400,7 +400,8 @@ def querySMT (exportFacts : Array REntry) (exportInds : Array MutualIndInfo) : L
   else
     return .none
 
-/-- `solverLemmas` includes:
+/-- `solverHints` includes:
+    - `unsatCoreDerivLeafStrings` an array of Strings that appear as leaves in any derivation for any fact in the unsat core
     - `selectorInfos` which is an array of
       - The SMT selector name (String)
       - The constructor that the selector is for (Expr)
@@ -415,10 +416,10 @@ def querySMT (exportFacts : Array REntry) (exportInds : Array MutualIndInfo) : L
 
     Note: In all fields except `selectorInfos`, there may be loose bound variables. The loose bound variable `#i` corresponds to
     the selector indicated by `selectorInfos[i]` -/
-abbrev solverLemmas := Array (String × Expr × Nat × Expr) × List Expr × List Expr × List Expr × List Expr × List Expr × List (List Expr)
+abbrev solverHints := Array String × 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 (Array String × solverLemmas)) := do
+def querySMTForHints (exportFacts : Array REntry) (exportInds : Array MutualIndInfo) : LamReif.ReifM (Option solverHints) := do
   let lamVarTy := (← LamReif.getVarVal).map Prod.snd
   let lamEVarTy ← LamReif.getLamEVarTy
   let exportLamTerms ← exportFacts.mapM (fun re => do
@@ -518,8 +519,7 @@ def querySMTForHints (exportFacts : Array REntry) (exportInds : Array MutualIndI
           | some parsedRule => return [parsedRule]
           | none => ruleInstances.mapM (fun lemTerm => Parser.SMTTerm.parseTermAndAbstractSelectors lemTerm symbolMap selectorMVars)
       )
-    let solverLemmas := (selectorArr, preprocessFacts, theoryLemmas, instantiations, computationLemmas, polynomialLemmas, rewriteFacts)
-    return some (unsatCoreDerivLeafStrings, solverLemmas)
+    return some (unsatCoreDerivLeafStrings, selectorArr, preprocessFacts, theoryLemmas, instantiations, computationLemmas, polynomialLemmas, rewriteFacts)
   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)
@@ -544,8 +544,7 @@ def querySMTForHints (exportFacts : Array REntry) (exportInds : Array MutualIndI
     let computationLemmas := computationLemmas.filterMap id
     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 (unsatCoreDerivLeafStrings, solverLemmas)
+    return some (unsatCoreDerivLeafStrings, selectorArr, preprocessFacts, theoryLemmas, instantiations, computationLemmas, polynomialLemmas, rewriteFacts)
 
 open LamReif Embedding.Lam in
 /--
@@ -712,15 +711,14 @@ def evalAuto : Tactic
 /-- 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
+def runAutoGetHints (lemmas : Array Lemma) (inhFacts : Array Lemma) : MetaM solverHints := 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 (Array String × solverLemmas) := (do
+  let afterReify (uvalids : Array UMonoFact) (uinhs : Array UMonoFact) (minds : Array (Array SimpleIndVal)) : LamReif.ReifM solverHints := (do
     let exportFacts ← LamReif.reifFacts uvalids
     let mut exportFacts := exportFacts.map (Embedding.Lam.REntry.valid [])
     let _ ← LamReif.reifInhabitations uinhs
@@ -731,17 +729,17 @@ def runAutoGetHints (lemmas : Array Lemma) (inhFacts : Array Lemma) : MetaM (Arr
     -- runAutoGetHints only supports SMT right now
     -- **SMT**
     if auto.smt.get (← getOptions) then
-      if let .some (unsatCoreDerivLeafStrings, lemmas) ← querySMTForHints exportFacts exportInds then
-        return (unsatCoreDerivLeafStrings, lemmas)
+      if let .some solverHints ← querySMTForHints exportFacts exportInds then
+        return solverHints
     throwError "autoGetHints only implemented for cvc5 (enable option auto.smt)"
     )
-  let ((unsatCoreDerivLeafStrings, lemmas), _) ← Monomorphization.monomorphize lemmas inhFacts $ fun s => do
-    let callAfterReify : Reif.ReifM (Array String × solverLemmas) := do
+  let (solverHints, _) ← Monomorphization.monomorphize lemmas inhFacts $ fun s => do
+    let callAfterReify : Reif.ReifM solverHints := 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 (unsatCoreDerivLeafStrings, lemmas)
+  return solverHints
 
 syntax (name := autoGetHints) "autoGetHints" autoinstr hints (uord)* : tactic