Modify runAutoGetHints to return unsat core even when external solver…

… uses TPTP

Auto/Solver/TPTP.lean

@@ -9,6 +9,7 @@ initialize
   registerTraceClass `auto.tptp.printQuery
   registerTraceClass `auto.tptp.printProof
   registerTraceClass `auto.tptp.premiseSelection
+  registerTraceClass `auto.tptp.unsatCore.deriv
 
 register_option auto.tptp : Bool := {
   defValue := false

Auto/Tactic.lean

@@ -271,28 +271,28 @@ open Embedding.Lam in
   If TPTP fails, return none
 -/
 def queryTPTP (exportFacts : Array REntry) : LamReif.ReifM (Array Embedding.Lam.REntry) := do
-    let lamVarTy := (← LamReif.getVarVal).map Prod.snd
-    let lamEVarTy ← LamReif.getLamEVarTy
-    let exportLamTerms ← exportFacts.mapM (fun re => do
-      match re with
-      | .valid [] t => return t
-      | _ => throwError "runAuto :: Unexpected error")
-    let query ← lam2TH0 lamVarTy lamEVarTy exportLamTerms
-    trace[auto.tptp.printQuery] "\n{query}"
-    let tptpProof ← Solver.TPTP.querySolver query
-    try
-      let proofSteps ← Parser.TPTP.getProof lamVarTy lamEVarTy tptpProof
-      for step in proofSteps do
-        trace[auto.tptp.printProof] "{step}"
-    catch e =>
-      trace[auto.tptp.printProof] "TPTP proof reification failed with {e.toMessageData}"
-    let unsatCore ← Parser.TPTP.unsatCore tptpProof
-    let mut ret := #[]
-    for n in unsatCore do
-      let .some re := exportFacts[n]?
-        | throwError "queryTPTP :: Index {n} out of range"
-      ret := ret.push re
-    return ret
+  let lamVarTy := (← LamReif.getVarVal).map Prod.snd
+  let lamEVarTy ← LamReif.getLamEVarTy
+  let exportLamTerms ← exportFacts.mapM (fun re => do
+    match re with
+    | .valid [] t => return t
+    | _ => throwError "runAuto :: Unexpected error")
+  let query ← lam2TH0 lamVarTy lamEVarTy exportLamTerms
+  trace[auto.tptp.printQuery] "\n{query}"
+  let tptpProof ← Solver.TPTP.querySolver query
+  try
+    let proofSteps ← Parser.TPTP.getProof lamVarTy lamEVarTy tptpProof
+    for step in proofSteps do
+      trace[auto.tptp.printProof] "{step}"
+  catch e =>
+    trace[auto.tptp.printProof] "TPTP proof reification failed with {e.toMessageData}"
+  let unsatCore ← Parser.TPTP.unsatCore tptpProof
+  let mut ret := #[]
+  for n in unsatCore do
+    let .some re := exportFacts[n]?
+      | throwError "queryTPTP :: Index {n} out of range"
+    ret := ret.push re
+  return ret
 
 /-- Returns the longest common prefix of two substrings.
     The returned substring will use the same underlying string as `s`.
@@ -414,8 +414,11 @@ def querySMT (exportFacts : Array REntry) (exportInds : Array MutualIndInfo) : L
     - `polynomialLemmas` : List Expr
     - `rewriteFacts` : List (List Expr)
 
-    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]` -/
+    Note 1: In all fields except `selectorInfos`, there may be loose bound variables. The loose bound variable `#i` corresponds to
+    the selector indicated by `selectorInfos[i]`
+
+    Note 2: When the external solver is cvc5, all fields can be populated, but when the external solver is Zipperposition, only the
+    first field (`unsatCoreDerivLeafStrings`) will be populated -/
 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
@@ -708,9 +711,7 @@ def evalAuto : Tactic
       absurd.assign proof
 | _ => throwUnsupportedSyntax
 
-/-- 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) -/
+/-- Runs `auto`'s monomorphization and preprocessing, then returns `solverHints` determined by the external prover's output -/
 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")
@@ -726,12 +727,29 @@ def runAutoGetHints (lemmas : Array Lemma) (inhFacts : Array Lemma) : MetaM solv
     -- **Preprocessing in Verified Checker**
     let (exportFacts', exportInds) ← LamReif.preprocess exportFacts exportInds
     exportFacts := exportFacts'
-    -- runAutoGetHints only supports SMT right now
+    -- **TPTP**
+    if auto.tptp.get (← getOptions) then
+      if auto.tptp.premiseSelection.get (← getOptions) then
+        let unsatCore ← queryTPTP exportFacts
+        if unsatCore == #[] then -- This can only occur if the external solver fails to find a proof
+          throwError "runAutoGetHints :: External TPTP solver unable to solve the goal"
+        let mut unsatCoreDerivLeafStrings := #[]
+        for fact in unsatCore do
+          let factDTR ← LamReif.collectDerivFor fact
+          unsatCoreDerivLeafStrings := unsatCoreDerivLeafStrings ++ factDTR.collectLeafStrings
+          trace[auto.tptp.unsatCore.deriv] "{fact} DTR: {factDTR}"
+        -- When the external prover uses the TPTP format, only information about the unsat core can be collected
+        return (unsatCoreDerivLeafStrings, #[], [], [], [], [], [], [])
+      else
+        throwError "runAutoGetHints :: No hints to return if auto.tptp is enabled but auto.tptp.premiseSelection is disabled"
     -- **SMT**
-    if auto.smt.get (← getOptions) then
+    else if auto.smt.get (← getOptions) then
       if let .some solverHints ← querySMTForHints exportFacts exportInds then
         return solverHints
-    throwError "autoGetHints only implemented for cvc5 (enable option auto.smt)"
+      else
+        throwError "runAutoGetHints :: querySMTForHints failed to return solverHints"
+    else
+      throwError "runAutoGetHints :: Either auto.smt or auto.tptp must be enabled"
     )
   let (solverHints, _) ← Monomorphization.monomorphize lemmas inhFacts $ fun s => do
     let callAfterReify : Reif.ReifM solverHints := do