feat: provide noKernel mode

Leanwuzla/Basic.lean

@@ -0,0 +1,59 @@
+import Lean.Elab.Tactic.BVDecide.Frontend.BVDecide
+
+open Lean
+
+private partial def getIntrosSize (e : Expr) : Nat :=
+  go 0 e
+where
+  go (size : Nat) : Expr → Nat
+    | .forallE _ _ b _ => go (size + 1) b
+    | .mdata _ b       => go size b
+    | _                => size
+
+/--
+Introduce only forall binders and preserve names.
+-/
+def _root_.Lean.MVarId.introsP (mvarId : MVarId) : MetaM (Array FVarId × MVarId) := do
+  let type ← mvarId.getType
+  let type ← instantiateMVars type
+  let n := getIntrosSize type
+  if n == 0 then
+    return (#[], mvarId)
+  else
+    mvarId.introNP n
+
+structure Context where
+  acNf : Bool
+  parseOnly : Bool
+  timeout : Nat
+  input : String
+  maxSteps : Nat
+  disableAndFlatten : Bool
+  disableEmbeddedConstraintSubst : Bool
+  disableKernel : Bool
+
+abbrev SolverM := ReaderT Context MetaM
+
+namespace SolverM
+
+def getParseOnly : SolverM Bool := return (← read).parseOnly
+def getInput : SolverM String := return (← read).input
+def getKernelDisabled : SolverM Bool := return (← read).disableKernel
+
+def getBVDecideConfig : SolverM Elab.Tactic.BVDecide.Frontend.BVDecideConfig := do
+  let ctx ← read
+  return {
+    timeout := ctx.timeout
+    acNf := ctx.acNf
+    embeddedConstraintSubst := !ctx.disableEmbeddedConstraintSubst
+    andFlattening := !ctx.disableAndFlatten
+    maxSteps := ctx.maxSteps
+    structures := false,
+  }
+
+def run (x : SolverM α) (ctx : Context) (coreContext : Core.Context) (coreState : Core.State) :
+    IO α := do
+  let (res, _, _) ← ReaderT.run x ctx |> (Meta.MetaM.toIO · coreContext coreState)
+  return res
+
+end SolverM

Leanwuzla/NoKernel.lean

@@ -0,0 +1,88 @@
+import Leanwuzla.Basic
+
+open Lean Std.Sat Std.Tactic.BVDecide
+open Elab.Tactic.BVDecide
+open Elab.Tactic.BVDecide.Frontend
+
+def runSolver (cnf : CNF Nat) (solver : System.FilePath) (lratPath : System.FilePath)
+    (trimProofs : Bool) (timeout : Nat) (binaryProofs : Bool) :
+    CoreM (Except (Array (Bool × Nat)) (Array LRAT.IntAction)) := do
+  IO.FS.withTempFile fun cnfHandle cnfPath => do
+    withTraceNode `sat (fun _ => return "Serializing SAT problem to DIMACS file") do
+      -- lazyPure to prevent compiler lifting
+      cnfHandle.putStr  (← IO.lazyPure (fun _ => cnf.dimacs))
+      cnfHandle.flush
+
+    let res ←
+      withTraceNode `sat (fun _ => return "Running SAT solver") do
+        External.satQuery solver cnfPath lratPath timeout binaryProofs
+    if let .sat assignment := res then
+      return .error assignment
+
+    let lratProof ←
+      withTraceNode `sat (fun _ => return "Obtaining LRAT certificate") do
+        LratCert.load lratPath trimProofs
+
+    return .ok lratProof
+
+def decideSmtNoKernel (type : Expr) : SolverM UInt32 := do
+  let solver ← TacticContext.new.determineSolver
+  let g := (← Meta.mkFreshExprMVar type).mvarId!
+  let (_, g) ← g.introsP
+  trace[Meta.Tactic.bv] m!"Working on goal: {g}"
+  try
+    g.withContext $ IO.FS.withTempFile fun _ lratPath => do
+      let cfg ← SolverM.getBVDecideConfig
+      match ← Normalize.bvNormalize g cfg with
+      | some g =>
+        let bvExpr := (← M.run <| reflectBV g).bvExpr
+
+        let entry ←
+          withTraceNode `bv (fun _ => return "Bitblasting BVLogicalExpr to AIG") do
+            -- lazyPure to prevent compiler lifting
+            IO.lazyPure (fun _ => bvExpr.bitblast)
+        let aigSize := entry.aig.decls.size
+        trace[Meta.Tactic.bv] s!"AIG has {aigSize} nodes."
+
+        let (cnf, map) ←
+          withTraceNode `sat (fun _ => return "Converting AIG to CNF") do
+            -- lazyPure to prevent compiler lifting
+            IO.lazyPure (fun _ =>
+              let (entry, map) := entry.relabelNat'
+              let cnf := Std.Sat.AIG.toCNF entry
+              (cnf, map)
+            )
+
+        let res ←
+          withTraceNode `sat (fun _ => return "Obtaining external proof certificate") do
+            runSolver cnf solver lratPath cfg.trimProofs cfg.timeout cfg.binaryProofs
+
+        match res with
+        | .ok cert =>
+          let certFine ←
+            withTraceNode `sat (fun _ => return "Verifying LRAT certificate") do
+              -- lazyPure to prevent compiler lifting
+              IO.lazyPure (fun _ => LRAT.check cert cnf)
+          if certFine then
+            logInfo "unsat"
+            return (0 : UInt32)
+          else
+            logInfo "Error: Failed to check LRAT cert"
+            return (1 : UInt32)
+        | .error assignment =>
+          logInfo "sat"
+          return (0 : UInt32)
+      | none =>
+        logInfo "unsat"
+        return (0 : UInt32)
+  catch e =>
+    -- TODO: improve handling of sat cases. This is a temporary workaround.
+    let message ← e.toMessageData.toString
+    if message.startsWith "None of the hypotheses are in the supported BitVec fragment" then
+      -- We fully support SMT-LIB v2.6. Getting the above error message means
+      -- the goal was reduced to `False` with only `True` as an assumption.
+      logInfo "sat"
+      return (0 : UInt32)
+    else
+      logError m!"Error: {e.toMessageData}"
+      return (1 : UInt32)

Main.lean

@@ -1,67 +1,15 @@
-import Lean.Elab.Tactic.BVDecide.Frontend.BVDecide
-import Lean.Language.Lean
 import Cli
 
 import Leanwuzla.Parser
+import Leanwuzla.Basic
+import Leanwuzla.NoKernel
 
 open Lean
 
-private partial def getIntrosSize (e : Expr) : Nat :=
-  go 0 e
-where
-  go (size : Nat) : Expr → Nat
-    | .forallE _ _ b _ => go (size + 1) b
-    | .mdata _ b       => go size b
-    | _                => size
-
-/--
-Introduce only forall binders and preserve names.
--/
-def _root_.Lean.MVarId.introsP (mvarId : MVarId) : MetaM (Array FVarId × MVarId) := do
-  let type ← mvarId.getType
-  let type ← instantiateMVars type
-  let n := getIntrosSize type
-  if n == 0 then
-    return (#[], mvarId)
-  else
-    mvarId.introNP n
-
 def parseSmt2File (path : System.FilePath) : MetaM Expr := do
   let query ← IO.FS.readFile path
   ofExcept (Parser.parseSmt2Query query)
 
-structure Context where
-  acNf : Bool
-  parseOnly : Bool
-  timeout : Nat
-  input : String
-  maxSteps : Nat
-  disableAndFlatten : Bool
-  disableEmbeddedConstraintSubst : Bool
-
-abbrev SolverM := ReaderT Context MetaM
-
-namespace SolverM
-
-def getParseOnly : SolverM Bool := return (← read).parseOnly
-def getInput : SolverM String := return (← read).input
-
-def getBVDecideConfig : SolverM Elab.Tactic.BVDecide.Frontend.BVDecideConfig := do
-  let ctx ← read
-  return {
-    timeout := ctx.timeout
-    acNf := ctx.acNf
-    embeddedConstraintSubst := !ctx.disableEmbeddedConstraintSubst
-    andFlattening := !ctx.disableAndFlatten
-    maxSteps := ctx.maxSteps
-  }
-
-def run (x : SolverM α) (ctx : Context) (coreContext : Core.Context) (coreState : Core.State) :
-    IO α := do
-  let (res, _, _) ← ReaderT.run x ctx |> (Meta.MetaM.toIO · coreContext coreState)
-  return res
-
-end SolverM
 
 open Elab in
 def decideSmt (type : Expr) : SolverM UInt32 := do
@@ -86,37 +34,41 @@ def decideSmt (type : Expr) : SolverM UInt32 := do
       logError m!"Error: {e.toMessageData}"
       return (1 : UInt32)
   let value ← instantiateExprMVars mv
-  let r := (← getEnv).addDecl (← getOptions) (.thmDecl { name := ← Lean.mkAuxName `thm 1, levelParams := [], type, value })
-  match r with
-  | .error e =>
-    logError m!"Error: {e.toMessageData (← getOptions)}"
-    return 1
-  | .ok env =>
-    setEnv env
+  try
+    Lean.addDecl (.thmDecl { name := ← Lean.mkAuxName `thm 1, levelParams := [], type, value })
     logInfo "unsat"
     return 0
+  catch e =>
+    logError m!"Error: {e.toMessageData}"
+    return 1
 
 def typeCheck (e : Expr) : SolverM UInt32 := do
-  let defn := .defnDecl {
-    name := ← Lean.mkAuxName `def 1
-    levelParams := []
-    type := .sort .zero
-    value := e
-    hints := .regular 0
-    safety := .safe
-  }
-  let r := (← getEnv).addDecl (← getOptions) defn
-  let .error e := r | return 0
-  logError m!"Error: {e.toMessageData (← getOptions)}"
-  return 1
+  try
+    let defn := .defnDecl {
+      name := ← Lean.mkAuxName `def 1
+      levelParams := []
+      type := .sort .zero
+      value := e
+      hints := .regular 0
+      safety := .safe
+    }
+    Lean.addDecl defn
+    return 0
+  catch e =>
+    logError m!"Error: {e.toMessageData}"
+    return 1
 
 def parseAndDecideSmt2File : SolverM UInt32 := do
   try
     let goalType ← parseSmt2File (← SolverM.getInput)
     if ← SolverM.getParseOnly then
+      logInfo m!"Goal:\n{goalType}"
       typeCheck goalType
     else
-      decideSmt goalType
+      if ← SolverM.getKernelDisabled then
+        decideSmtNoKernel goalType
+      else
+        decideSmt goalType
   finally
     printTraces
     Lean.Language.reportMessages (← Core.getMessageLog) (← getOptions)
@@ -142,18 +94,24 @@ where
         opts
           |>.setBool `trace.Meta.Tactic.bv true
           |>.setBool `trace.Meta.Tactic.sat true
-          |>.setBool `trace.profiler true
+          --|>.setBool `trace.profiler true
 
     if p.hasFlag "vsimp" then
       opts :=
         opts
           |>.setBool `trace.Meta.Tactic.simp true
 
-    if p.hasFlag "skipLrat" then
+    if p.hasFlag "disableKernel" then
       opts :=
         opts
           |>.setBool `debug.skipKernelTC true
 
+    if p.hasFlag "parseOnly" then
+       opts :=
+        opts
+          |>.setNat `pp.maxSteps 10000000000
+          |>.setNat `pp.deepTerms.threshold 100
+
     opts := opts.setNat `maxHeartbeats <| p.flag! "maxHeartbeats" |>.as! Nat
     opts := opts.setNat `maxRecDepth <| p.flag! "maxRecDepth" |>.as! Nat
     opts := opts.setNat `trace.profiler.threshold <| p.flag! "pthreshold" |>.as! Nat
@@ -170,6 +128,7 @@ where
       maxSteps := p.flag! "maxSteps" |>.as! Nat
       disableAndFlatten := p.hasFlag "disableAndFlatten"
       disableEmbeddedConstraintSubst := p.hasFlag "disableEmbeddedConstraintSubst"
+      disableKernel := p.hasFlag "disableKernel"
     }
 
 unsafe def leanwuzlaCmd : Cmd := `[Cli|
@@ -188,9 +147,9 @@ unsafe def leanwuzlaCmd : Cmd := `[Cli|
     maxSteps : Nat; "Set the maximum number of simplification steps."
     pthreshold : Nat; "The timing threshold for profiler output."
     vsimp; "Print the profiler trace output from simp."
-    skipLrat; "Skip checking the LRAT certificate of the SAT proof."
     disableAndFlatten; "Disable the and flattening pass."
     disableEmbeddedConstraintSubst; "Disable the embedded constraints substitution pass."
+    disableKernel; "Disable the Lean kernel, that is only verify the LRAT cert, no reflection proof"
 
   ARGS:
     input : String; "Path to the smt2 file to work on"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2025-01-01
+leanprover/lean4-pr-releases:pr-release-6856