From 61c843a3c7541bed30a4302aa8ab23cf98bd279c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Wed, 29 Jan 2025 21:47:47 +0100
Subject: [PATCH] refactor: pull out some LRAT functionality from bv_decide
 (#6856)

This PR refactors a bit of the functionality in bv_decide's frontend to
make it accessible for external users.
---
 src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean
index 7178e12d43..3b4de5ba7a 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean
@@ -54,7 +54,7 @@ def TacticContext.new (lratPath : System.FilePath) (config : BVDecideConfig) :
     config
   }
 where
-  determineSolver : Lean.Elab.TermElabM System.FilePath := do
+  determineSolver : CoreM System.FilePath := do
     let opts ← getOptions
     let option := sat.solver.get opts
     if option == "" then
@@ -96,7 +96,7 @@ instance : ToExpr LRAT.IntAction where
       mkApp3 (mkConst ``LRAT.Action.del [.zero, .zero]) beta alpha (toExpr ids)
   toTypeExpr := mkConst ``LRAT.IntAction
 
-def LratCert.ofFile (lratPath : System.FilePath) (trimProofs : Bool) : CoreM LratCert := do
+def LratCert.load (lratPath : System.FilePath) (trimProofs : Bool) : CoreM (Array LRAT.IntAction) := do
   let proofInput ← IO.FS.readBinFile lratPath
   let proof ←
     withTraceNode `sat (fun _ => return s!"Parsing LRAT file") do
@@ -118,6 +118,10 @@ def LratCert.ofFile (lratPath : System.FilePath) (trimProofs : Bool) : CoreM Lra
       pure proof
 
   trace[Meta.Tactic.sat] s!"LRAT proof has {proof.size} steps after trimming"
+  return proof
+
+def LratCert.ofFile (lratPath : System.FilePath) (trimProofs : Bool) : CoreM LratCert := do
+  let proof ← LratCert.load lratPath trimProofs
 
   -- This is necessary because the proof might be in the binary format in which case we cannot
   -- store it as a string in the environment (yet) due to missing support for binary literals.