Move dischargeObligationIncremental to SMTUtils for Imperative reuse

Author: MikaelMayer

Strata/DL/Imperative/SMTUtils.lean

@@ -292,6 +292,79 @@ def addLocationInfo {P : PureExpr} [BEq P.Ident]
       Strata.SMT.Solver.setInfoString message.fst message.snd
     | .none => pure ()
 
+/-- Result of encoding a proof obligation against an `AbstractSolver`.
+    Returned by the encoder callback passed to `dischargeObligationIncremental`,
+    consumed by the check-sat orchestration. -/
+structure EncodedObligation where
+  obligationId : Strata.SMT.Term
+  assumptionIds : List String
+  estate : Strata.SMT.EncoderState
+
+/-- Discharge a proof obligation using a live (incremental) SMT solver.
+    The encoder callback runs against the spawned solver to emit declarations
+    and assertions; this helper orchestrates check-sat calls and model parsing. -/
+def dischargeObligationIncremental {P : PureExpr} [ToFormat P.Ident] [BEq P.Ident]
+    (encodeDecl : Strata.SMT.AbstractSolver Strata.SMT.Term Strata.SMT.TermType
+                    Strata.SMT.IncrementalSolverM →
+                  Strata.SMT.IncrementalSolverM EncodedObligation)
+    (typedVarToSMTFn : P.Ident → P.Ty → Except Format (String × Strata.SMT.TermType))
+    (vars : List P.TypedIdent)
+    (smtsolver : String) (solverFlags : Array String)
+    (satisfiabilityCheck validityCheck : Bool) :
+    IO (Except SolverError (Result P.Ident × Result P.Ident × Strata.SMT.EncoderState)) := do
+  let solverState ← Strata.SMT.IncrementalSolver.spawn smtsolver solverFlags
+  let action : Strata.SMT.IncrementalSolverM
+      (Except SolverError (Result P.Ident × Result P.Ident × Strata.SMT.EncoderState)) := do
+    let solver := Strata.SMT.IncrementalSolver.mkIncrementalSolver
+    let { obligationId, assumptionIds, estate } ← encodeDecl solver
+    let varIds := assumptionIds.map fun id => Strata.SMT.Term.var ⟨id, .bool⟩
+    let getModelForVars : Strata.SMT.IncrementalSolverM (Model P.Ident) := do
+      if varIds.isEmpty then return []
+      try
+        match ← solver.getValue varIds with
+        | .ok pairs =>
+          match pairs with
+          | [(.prim (.string rawOutput), _)] =>
+            let rawModel ← parseModelDDM rawOutput
+            match processModel typedVarToSMTFn vars rawModel estate with
+            | .ok model => return model
+            | .error _ => return []
+          | _ => return []
+        | .error _ => return []
+      catch _ => return []
+    let decisionToResult (decision : Except String Strata.SMT.Decision) :
+        Strata.SMT.IncrementalSolverM (Result P.Ident) := do
+      match decision with
+      | .ok .sat => return .sat (← getModelForVars)
+      | .ok .unknown =>
+        let model ← getModelForVars
+        return if model.isEmpty then .unknown else .unknown (some model)
+      | .ok .unsat => return .unsat
+      | .error msg => return .err msg
+    let unwrap {α : Type} (label : String) (r : Except String α) : Strata.SMT.IncrementalSolverM α :=
+      match r with
+      | .ok a => return a
+      | .error msg => throw (IO.userError s!"{label}: {msg}")
+    let bothChecks := satisfiabilityCheck && validityCheck
+    let mut satResult : Result P.Ident := .unknown
+    let mut valResult : Result P.Ident := .unknown
+    if bothChecks then
+      satResult ← decisionToResult (← solver.checkSatAssuming [obligationId])
+      let negObligation ← unwrap "mkNot" (← solver.mkNot obligationId)
+      valResult ← decisionToResult (← solver.checkSatAssuming [negObligation])
+    else
+      if satisfiabilityCheck then
+        unwrap "assert" (← solver.assert obligationId)
+        satResult ← decisionToResult (← solver.checkSat)
+      else if validityCheck then
+        let negObligation ← unwrap "mkNot" (← solver.mkNot obligationId)
+        unwrap "assert" (← solver.assert negObligation)
+        valResult ← decisionToResult (← solver.checkSat)
+    solver.close
+    return .ok (satResult, valResult, estate)
+  let (result, _) ← action.run solverState
+  return result
+
 /--
 Writes the proof obligation to file, discharge the obligation using SMT solver,
 and parse the output of the SMT solver.

Strata/Languages/Core/Verifier.lean

@@ -557,8 +557,7 @@ def dischargeObligationIncremental
   (_label : String)
   (varDefinitions : List VarDefinition := [])
   (varDeclarations : List VarDeclaration := [])
-  : IO (Except Imperative.SMT.SolverError (SMT.Result × SMT.Result × EncoderState)) :=
-  open _root_.Strata.SMT.IncrementalSolver in do
+  : IO (Except Imperative.SMT.SolverError (SMT.Result × SMT.Result × EncoderState)) := do
   let baseFlags := getSolverFlags options
   let needsIncremental := satisfiabilityCheck && validityCheck
   let solverSpecificFlags := match options.solver with
@@ -567,68 +566,25 @@ def dischargeObligationIncremental
       if needsIncremental && !baseFlags.contains "--incremental" then
         base ++ #["--incremental"]
       else base
-    | "z3" => #["-in"]  -- z3 reads from stdin with -in
+    | "z3" => #["-in"]
     | _ => #[]
   let allFlags := solverSpecificFlags ++ baseFlags
-  let solverState ← spawn options.solver allFlags
-  let action : _root_.Strata.SMT.IncrementalSolverM (Except Imperative.SMT.SolverError (SMT.Result × SMT.Result × EncoderState)) := do
-    let solver := _root_.Strata.SMT.IncrementalSolver.mkIncrementalSolver
-    -- Solver-specific prelude (options like smt.mbqi, auto_config)
-    let prelude : _root_.Strata.SMT.IncrementalSolverM Unit := match options.solver with
+  let encodeDecl (solver : Strata.SMT.AbstractSolver Term TermType
+                            Strata.SMT.IncrementalSolverM) :
+      Strata.SMT.IncrementalSolverM Imperative.SMT.EncodedObligation := do
+    let prelude : Strata.SMT.IncrementalSolverM Unit := match options.solver with
       | "z3" => do
         solver.setOption "smt.mbqi" "false"
         solver.setOption "auto_config" "false"
       | _ => pure ()
-    -- Encode all declarations and assertions through the AbstractSolver API.
     let (obligationId, ids, estate) ←
       _root_.Strata.SMT.Encoder.encodeDeclarationsAbstract solver ctx prelude
         assumptionTerms obligationTerm
         (varDefinitions := varDefinitions) (varDeclarations := varDeclarations)
-    -- Variable terms for getValue
-    let varIds := ids.map fun id => Term.var ⟨id, .bool⟩
-    -- Helper to get model via solver.getValue and parse it.
-    -- Called only when the decision is SAT or UNKNOWN.
-    let getModelForVars : _root_.Strata.SMT.IncrementalSolverM (Imperative.SMT.Model Expression.Ident) := do
-      if varIds.isEmpty then return []
-      match ← solver.getValue varIds with
-      | .ok pairs =>
-        match pairs with
-        | [(.prim (.string rawOutput), _)] =>
-          let rawModel ← Imperative.SMT.parseModelDDM rawOutput
-          match Imperative.SMT.processModel (typedVarToSMTFn ctx) vars rawModel estate with
-          | .ok model => return model
-          | .error _ => return []
-        | _ => return []
-      | .error _ => return []
-    -- Issue check-sat commands through the AbstractSolver API.
-    let decisionToResult (decision : Except String Decision)
-        : _root_.Strata.SMT.IncrementalSolverM (Imperative.SMT.Result Expression.Ident) := do
-      match decision with
-      | .ok .sat => return .sat (← getModelForVars)
-      | .ok .unknown =>
-        let model ← getModelForVars
-        return if model.isEmpty then .unknown else .unknown (some model)
-      | .ok .unsat => return .unsat
-      | .error msg => return .err msg
-    let bothChecks := satisfiabilityCheck && validityCheck
-    let mut satResult : Imperative.SMT.Result Expression.Ident := .unknown
-    let mut valResult : Imperative.SMT.Result Expression.Ident := .unknown
-    if bothChecks then
-      satResult ← decisionToResult (← solver.checkSatAssuming [obligationId])
-      let negObligation ← _root_.Strata.SMT.Encoder.unwrap "mkNot" (← solver.mkNot obligationId)
-      valResult ← decisionToResult (← solver.checkSatAssuming [negObligation])
-    else
-      if satisfiabilityCheck then
-        _root_.Strata.SMT.Encoder.unwrap "assert" (← solver.assert obligationId)
-        satResult ← decisionToResult (← solver.checkSat)
-      else if validityCheck then
-        let negObligation ← _root_.Strata.SMT.Encoder.unwrap "mkNot" (← solver.mkNot obligationId)
-        _root_.Strata.SMT.Encoder.unwrap "assert" (← solver.assert negObligation)
-        valResult ← decisionToResult (← solver.checkSat)
-    solver.close
-    return .ok (satResult, valResult, estate)
-  let (result, _) ← action.run solverState
-  return result
+    return { obligationId, assumptionIds := ids, estate }
+  Imperative.SMT.dischargeObligationIncremental (P := Core.Expression)
+    encodeDecl (typedVarToSMTFn ctx) vars options.solver allFlags
+    satisfiabilityCheck validityCheck
 
 end -- public section
 end Core.SMT