feat: support get-model and print SMT-LIB models

Parse the `(get-model)` command and return a flag from the parser indicating
whether a model should be printed. When the query is satisfiable, print a model
following SMT-LIB `get-model` semantics: one `define-fun` per user-declared
symbol (`declare-const`/`declare-fun`), excluding defined symbols. Since
`bv_decide`'s counterexample may be partial, missing constants are completed
with all-zeros for bitvectors and `false` for booleans; booleans are decoded
from their `BitVec.ofBool` reflection. Implemented on both the kernel and
no-kernel paths.

Along the way:
- Make `smtSymbolToName` keep the exact symbol string (`Name.mkSimple`) instead
  of splitting on `.`, so symbols round-trip faithfully and distinct symbols
  such as `a.0` and `a.00` are no longer conflated; `formatSmtSymbol` reads the
  string back directly.
- Teach `introsP` to step over leading `define-sort` `let` binders so declared
  constants are reached (and shared with `bv_decide`), and unfold sort aliases
  when printing.
- Restore the spurious-counterexample check lost when switching to `bvDecide'`:
  a shared `reportCounterExample` reports `sat`/model for genuine counterexamples
  and errors (exit 1) for spurious ones, consistently on both paths.
- Add `Test/Model.lean` covering symbol round-tripping, bitvector literal
  formatting, model printing (bitvecs, booleans, completion, sort aliases), and
  declared-vs-defined symbol selection.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: 2 people

Leanwuzla/Basic.lean

@@ -1,29 +1,168 @@
-import Lean.Meta.Tactic.BVDecide
+module
+
+public import Lean.Expr
+public import Lean.Meta.Basic
+public import Lean.Meta.Tactic.BVDecide.Counterexample
+public import Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
+public import Std.Tactic.BVDecide.Syntax
+import all Lean.Meta.Tactic.BVDecide.Counterexample
+
 
 open Lean
+open Std.Tactic.BVDecide
+
+/--
+Render a `width`-bit bitvector with the given numeric `value` as an SMT-LIB
+binary literal (e.g. `#b00000001`).
+-/
+public def formatBitVecLiteral (value : Nat) (width : Nat) : String := Id.run do
+  let mut s := "#b"
+  for i in [0:width] do
+    let bit := (value >>> (width - 1 - i)) &&& 1
+    s := s.push (if bit == 1 then '1' else '0')
+  return s
+
+/--
+Render a Lean `Name` as an SMT-LIB symbol, quoting it with `|...|` if it is not
+a valid simple symbol.
+-/
+public def formatSmtSymbol (n : Name) : String :=
+  -- `smtSymbolToName` builds every symbol as a single-component name holding the
+  -- exact string, so we read it back directly rather than relying on
+  -- `Name.toString`'s escaping/pseudo-syntax handling.
+  let s := match n with
+    | .mkSimple s => s
+    | _           => n.toString (escape := false)
+  let isSimpleChar c := Char.isAlphanum c || "~!@$%^&*_-+=<>.?/".contains c
+  let needsQuote :=
+    match s.toList with
+    | [] => true
+    | c :: cs => c.isDigit || !(c :: cs).all isSimpleChar
+  if needsQuote then "|" ++ s ++ "|" else s
+
+/--
+Unfold a chain of `let`-bound sort aliases (introduced by `define-sort`) to the
+underlying sort.
+-/
+private partial def resolveSortAlias (e : Expr) : MetaM Expr := do
+  match e with
+  | .fvar fvarId =>
+    match ← fvarId.getDecl with
+    | .ldecl (value := v) .. => resolveSortAlias v
+    | _ => return e
+  | _ => return e
 
-private partial def getIntrosSize (e : Expr) : Nat :=
-  go 0 e
+/--
+Print a model for a satisfiable query following SMT-LIB `get-model` semantics.
+
+`fvars` are the free variables corresponding to the SMT-LIB declared constants
+(in declaration order) and `equations` is the (possibly partial) assignment
+found by `bv_decide`. Booleans are reflected as one-bit bitvectors, so a boolean
+constant `b` shows up in `equations` as `BitVec.ofBool b`. Since `bv_decide`'s
+counterexample is not guaranteed to assign every declared constant, any constant
+missing from `equations` is completed with all-zeros for bitvectors and `false`
+for booleans.
+
+Must be run in a context in which `fvars` are valid (e.g. inside the goal's
+`withContext`).
+-/
+public def printModel (fvars : Array FVarId) (equations : Array (Expr × BVExpr.PackedBitVec)) :
+    MetaM Unit := do
+  -- Index the values found by `bv_decide` by the free variable they assign.
+  -- Bitvector constants appear directly as free variables, whereas boolean
+  -- constants `b` appear wrapped as `BitVec.ofBool b` with a one-bit value.
+  let mut values : Std.HashMap FVarId Nat := {}
+  for (e, pv) in equations do
+    if e.isFVar then
+      values := values.insert e.fvarId! pv.bv.toNat
+    else if let .app (.const ``BitVec.ofBool []) x := e then
+      if x.isFVar then
+        values := values.insert x.fvarId! pv.bv.toNat
+  let mut lines : Array String := #[]
+  for fvar in fvars do
+    let decl ← fvar.getDecl
+    let sym := formatSmtSymbol decl.userName
+    -- A declared constant may have a `define-sort` alias as its type, in which
+    -- case it is a `let`-bound free variable that we unfold to its definition.
+    match ← resolveSortAlias decl.type with
+    | .const ``Bool [] =>
+      -- A missing assignment is completed with `false`.
+      let value := values.getD fvar 0 == 1
+      lines := lines.push s!"  (define-fun {sym} () Bool {value})"
+    | .app (.const ``BitVec []) we =>
+      let some w := we.nat? | continue
+      let value := values.getD fvar 0
+      lines := lines.push
+        s!"  (define-fun {sym} () (_ BitVec {w}) {formatBitVecLiteral value w})"
+    | _ =>
+      -- Skip declarations outside the supported QF_BV fragment (e.g. functions
+      -- with arguments), which cannot appear in a counterexample anyway.
+      continue
+  let model :=
+    if lines.isEmpty then "(\n)"
+    else "(\n" ++ String.intercalate "\n" lines.toList ++ "\n)"
+  logInfo model
+
+open Lean.Meta.Tactic.BVDecide in
+/--
+Report the outcome of a satisfiable query from a `bv_decide` counterexample.
+
+If the counterexample is genuine, print `sat` (and, when `getModel` is set, the
+model) and return exit code `0`. If it is *spurious* -- i.e. `bv_decide`
+abstracted an unsupported subterm as an opaque variable, or did not use a
+relevant hypothesis, so the assignment may not actually satisfy the problem --
+report it as an error and return exit code `1`, mirroring `bvDecide`.
+-/
+public def reportCounterExample (fvars : Array FVarId) (getModel : Bool)
+    (counterExample : CounterExample) : MetaM UInt8 := do
+  let diagnosis ← DiagnosisM.run DiagnosisM.diagnose counterExample
+  if diagnosis.uninterpretedSymbols.isEmpty && diagnosis.unusedRelevantHypotheses.isEmpty then
+    logInfo "sat"
+    if getModel then
+      printModel fvars counterExample.equations
+    return (0 : UInt8)
+  else
+    logError (← addMessageContextFull (← explainCounterExampleQuality counterExample))
+    return (1 : UInt8)
+
+/--
+Count the leading `let` binders (introduced by `define-sort`) followed by the
+`forall` binders (introduced by `declare-fun`/`declare-const`) of `e`. Traversal
+stops at the first `let` following the foralls, which corresponds to the
+`define-fun`/`define-const` bindings of the body. Returns the number of leading
+`let`s and the number of following `forall`s, respectively.
+-/
+private partial def getIntrosSize (e : Expr) : Nat × Nat :=
+  goLets 0 e
 where
-  go (size : Nat) : Expr → Nat
-    | .forallE _ _ b _ => go (size + 1) b
-    | .mdata _ b       => go size b
-    | _                => size
+  goLets (lets : Nat) : Expr → Nat × Nat
+    | .letE _ _ _ b _ => goLets (lets + 1) b
+    | .mdata _ b      => goLets lets b
+    | e               => (lets, goForalls 0 e)
+  goForalls (foralls : Nat) : Expr → Nat
+    | .forallE _ _ b _ => goForalls (foralls + 1) b
+    | .mdata _ b       => goForalls foralls b
+    | _                => foralls
 
 /--
-Introduce only forall binders and preserve names.
+Introduce the leading `define-sort` `let` binders together with the
+`declare-fun`/`declare-const` `forall` binders, preserving names. Returns the
+free variables corresponding to the declared symbols, i.e. those coming from the
+`forall` binders only (the introduced sort definitions are excluded).
 -/
-def _root_.Lean.MVarId.introsP (mvarId : MVarId) : MetaM (Array FVarId × MVarId) := do
+public 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
+  let (numLets, numForalls) := getIntrosSize type
+  if numLets + numForalls == 0 then
     return (#[], mvarId)
   else
-    mvarId.introNP n
+    let (fvars, mvarId) ← mvarId.introNP (numLets + numForalls)
+    -- Drop the leading sort definitions; keep only the declared symbols.
+    return (fvars.extract numLets fvars.size, mvarId)
 
 open Meta.Tactic.BVDecide in
-structure Context where
+public structure Context where
   acNf : Bool
   parseOnly : Bool
   timeout : Nat
@@ -34,15 +173,15 @@ structure Context where
   disableKernel : Bool
   solverMode : Elab.Tactic.BVDecide.SolverMode
 
-abbrev SolverM := ReaderT Context MetaM
+public 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
+public def getParseOnly : SolverM Bool := return (← read).parseOnly
+public def getInput : SolverM String := return (← read).input
+public def getKernelDisabled : SolverM Bool := return (← read).disableKernel
 
-def getBVDecideConfig : SolverM Elab.Tactic.BVDecide.BVDecideConfig := do
+public def getBVDecideConfig : SolverM Elab.Tactic.BVDecide.BVDecideConfig := do
   let ctx ← read
   return {
     timeout := ctx.timeout
@@ -56,7 +195,7 @@ def getBVDecideConfig : SolverM Elab.Tactic.BVDecide.BVDecideConfig := do
     solverMode := ctx.solverMode
   }
 
-def run (x : SolverM α) (ctx : Context) (coreContext : Core.Context) (coreState : Core.State) :
+public 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

Leanwuzla/NoKernel.lean

@@ -1,4 +1,8 @@
-import Leanwuzla.Basic
+module
+
+public import Leanwuzla.Basic
+import all Lean.Meta.Tactic.BVDecide
+
 
 open Lean Std.Sat Std.Tactic.BVDecide
 open Meta.Tactic.BVDecide
@@ -24,17 +28,24 @@ def runSolver (cnf : CNF Nat) (solver : System.FilePath) (lratPath : System.File
 
     return .ok lratProof
 
-def decideSmtNoKernel (type : Expr) : SolverM UInt8 := do
+public def decideSmtNoKernel (type : Expr) (getModel : Bool) : SolverM UInt8 := do
   let solver ← determineSolver
   let g := (← Meta.mkFreshExprMVar type).mvarId!
-  let (_, g) ← g.introsP
+  let (fvars, 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
+        -- Reflect the goal and, at the same time, record the atom assignment so
+        -- that we can reconstruct a model if the query turns out to be sat.
+        let (bvExpr, atomsAssignment, unusedHypotheses) ← M.run do
+          let reflectionResult ← reflectBV g
+          let flipper := fun (expr, {width, atomNumber, synthetic}) =>
+            (atomNumber, (width, expr, synthetic))
+          let atomsAssignment := Std.HashMap.ofList ((← getThe State).atoms.toList.map flipper)
+          return (reflectionResult.bvExpr, atomsAssignment, reflectionResult.unusedHypotheses)
 
         let entry ←
           withTraceNode `bv (fun _ => return "Bitblasting BVLogicalExpr to AIG") do
@@ -43,7 +54,7 @@ def decideSmtNoKernel (type : Expr) : SolverM UInt8 := do
         let aigSize := entry.aig.decls.size
         trace[Meta.Tactic.bv] s!"AIG has {aigSize} nodes."
 
-        let (cnf, _) ←
+        let (cnf, map) ←
           withTraceNode `sat (fun _ => return "Converting AIG to CNF") do
             -- lazyPure to prevent compiler lifting
             IO.lazyPure (fun _ =>
@@ -68,19 +79,23 @@ def decideSmtNoKernel (type : Expr) : SolverM UInt8 := do
           else
             logInfo "Error: Failed to check LRAT cert"
             return (1 : UInt8)
-        | .error .. =>
-          logInfo "sat"
-          return (0 : UInt8)
+        | .error assignment =>
+          let equations := reconstructCounterExample map assignment aigSize atomsAssignment
+          reportCounterExample fvars getModel { goal := g, unusedHypotheses, equations }
       | none =>
         logInfo "unsat"
         return (0 : UInt8)
   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.
+      -- 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. Every
+      -- declared constant is then unconstrained, so the model completed entirely
+      -- with default values is a valid one.
       logInfo "sat"
+      if getModel then
+        g.withContext do printModel fvars #[]
       return (0 : UInt8)
     else
       logError m!"Error: {e.toMessageData}"

Leanwuzla/Parser.lean

@@ -110,11 +110,12 @@ private def mkBitVecShiftRight (w : Nat) : Expr :=
 
 def smtSymbolToName (s : String) : Name :=
   let s := if s.startsWith "|" && s.endsWith "|" then String.Pos.Raw.extract s (s.rawStartPos + '|') (s.rawEndPos - '|') else s
-  -- Quote the string if a natural translation to Name fails
-  if s.toName == .anonymous then
-    Name.mkSimple s
-  else
-    s.toName
+  -- SMT-LIB symbols are flat (non-hierarchical) strings, so we always build a
+  -- single-component name rather than splitting on `.`. This keeps the exact
+  -- symbol intact -- so it can be printed back faithfully (e.g. in models, see
+  -- `formatSmtSymbol`) -- and avoids conflating distinct symbols that only
+  -- differ in a way `String.toName` normalizes away, such as `a.0` and `a.00`.
+  Name.mkSimple s
 
 /-- Returns two types: the first is the canonical type and the second is the
     user-provided one (mainly for pretty-printing). -/
@@ -562,6 +563,9 @@ structure Query where
   funDecls : List Sexp := []
   funDefs : List Sexp := []
   asserts : List Sexp := []
+  /-- Whether the query contains a `(get-model)` command, in which case a model
+      should be printed when the query is satisfiable. -/
+  getModel : Bool := false
 
 def parseQuery (query : Query) : ParserM Expr := do
   withTypeDefs query.typeDefs <| withFunDecls query.funDecls <| withFunDefs query.funDefs do
@@ -587,6 +591,8 @@ where
       go { query with funDefs := sexp!{(define-fun {n} {ps} {s} {b})} :: query.funDefs } cmds
     | sexp!{(assert {p})} :: cmds =>
       go { query with asserts := sexp!{(assert {p})} :: query.asserts } cmds
+    | sexp!{(get-model)} :: cmds =>
+      go { query with getModel := true } cmds
     -- TODO: We should parse `(check-sat)` command. We currently return `sat` if
     -- `(check-sat)` command is missing.
     | _ :: cmds =>
@@ -595,14 +601,19 @@ where
       { typeDefs := query.typeDefs.reverse
         funDecls := query.funDecls.reverse
         funDefs := query.funDefs.reverse
-        asserts := query.asserts.reverse }
+        asserts := query.asserts.reverse
+        getModel := query.getModel }
 
-def parseSmt2Query (query : String) : Except MessageData Expr :=
+/-- Parse an SMT-LIB2 query, returning the goal expression together with a flag
+    indicating whether a model should be printed (i.e. whether the query
+    contained a `(get-model)` command). -/
+def parseSmt2Query (query : String) : Except MessageData (Expr × Bool) := do
   match Sexp.Parser.manySexps!.run query with
   | Except.error e =>
     .error s!"{e}"
   | Except.ok cmds =>
     let query := filterCmds cmds
-    (parseQuery query).run' {}
+    let e ← (parseQuery query).run' {}
+    return (e, query.getModel)
 
 end Parser