Add initial support for FP.

Author: abdoo8080

Leanwuzla.lean

@@ -111,8 +111,8 @@ where
     match expr with
     | .var idx => push s!"x_{idx}"
     | .const val =>
-      let s := (Nat.toDigits 2 val.toNat).asString
-      let t := (List.replicate (w - s.length) '0').asString
+      let s := String.ofList (Nat.toDigits 2 val.toNat)
+      let t := String.ofList (List.replicate (w - s.length) '0')
       let binStr := t ++ s
       push "#b"
       push binStr
@@ -384,7 +384,7 @@ where
         let msg ← msg.toString
         let pref := "solving_context::time_solve: "
         if msg.startsWith pref then
-          let msg := (msg.splitOn " ")[1]!.dropRight 2
+          let msg := (msg.splitOn " ")[1]!.dropEnd 2
           set <| Float.ofInt msg.toNat!
         parseBitwuzlaTrace children
       | .withContext _ msg => parseBitwuzlaTrace #[msg]

Leanwuzla/NoKernel.lean

@@ -26,7 +26,7 @@ def runSolver (cnf : CNF Nat) (solver : System.FilePath) (lratPath : System.File
     return .ok lratProof
 
 def decideSmtNoKernel (type : Expr) : SolverM UInt8 := do
-  let solver ← TacticContext.new.determineSolver
+  let solver ← determineSolver
   let g := (← Meta.mkFreshExprMVar type).mvarId!
   let (_, g) ← g.introsP
   trace[Meta.Tactic.bv] m!"Working on goal: {g}"
@@ -86,3 +86,15 @@ def decideSmtNoKernel (type : Expr) : SolverM UInt8 := do
     else
       logError m!"Error: {e.toMessageData}"
       return (1 : UInt8)
+where
+  determineSolver : CoreM System.FilePath := do
+    let opts ← getOptions
+    let option := sat.solver.get opts
+    if option == "" then
+      let cadicalPath := (← IO.appPath).parent.get! / "cadical" |>.withExtension System.FilePath.exeExtension
+      if ← cadicalPath.pathExists then
+        return cadicalPath
+      else
+        return "cadical"
+    else
+      return option

Leanwuzla/Parser.lean

@@ -19,8 +19,8 @@ def generalIdent : Parser :=
   withAntiquot (mkAntiquot "generalIdent" `generalIdent) {
     fn := fun c s =>
       let startPos := s.pos
-      let s := takeWhile1Fn (fun c => !("(){}[].".contains c) ∧ !c.isWhitespace) "expected generalized identifier" c s
-      mkNodeToken `generalIdent startPos c s }
+      let s := takeWhile1Fn (fun c => !("(){}⦃⦄".contains c) ∧ !c.isWhitespace) "expected generalized identifier" c s
+      mkNodeToken `generalIdent startPos true c s }
 
 def Lean.TSyntax.getGeneralId : TSyntax `generalIdent → String
   | ⟨.node _ `generalIdent args⟩ => args[0]!.getAtomVal
@@ -43,18 +43,18 @@ syntax "(" slist ")" : sexp
 syntax "{" term "}" : sexp
 
 syntax sexp : slist
-syntax "...{" term "}" : slist
+syntax "⦃" term "⦄" : slist
 syntax sexp slist : slist
-syntax "...{" term "}" slist : slist
+syntax "⦃" term "⦄" slist : slist
 
 syntax "sexp!{" sexp "}" : term
 syntax "slist!{" slist "}" : term
 
 macro_rules
   | `(slist| $s:sexp) => `([sexp!{$s}])
-  | `(slist| ...{ $t:term }) => `(($t : List Sexp))
+  | `(slist| ⦃ $t:term ⦄) => `(($t : List Sexp))
   | `(slist| $s:sexp $ss:slist) => `(sexp!{$s} :: slist!{$ss})
-  | `(slist| ...{ $t:term } $ss:slist) => `(($t : List Sexp) ++ slist!{$ss})
+  | `(slist| ⦃ $t:term ⦄ $ss:slist) => `(($t : List Sexp) ++ slist!{$ss})
 
 macro_rules
   | `(sexp| $a:generalIdent) => `(Sexp.atom $(Lean.quote a.getGeneralId))
@@ -91,13 +91,15 @@ instance : Repr Sexp where
 /-- info: sexp!{(foo bar)} -/
 #guard_msgs in #eval sexp!{({Sexp.atom "foo"} bar)}
 /-- info: sexp!{(foo bar)} -/
-#guard_msgs in #eval sexp!{(foo ...{[Sexp.atom "bar"]})}
+#guard_msgs in #eval sexp!{(foo ⦃[Sexp.atom "bar"]⦄)}
 /-- info: sexp!{(foo bar)} -/
-#guard_msgs in #eval sexp!{(...{[Sexp.atom "foo"]} bar)}
+#guard_msgs in #eval sexp!{(foo ⦃[Sexp.atom "bar"]⦄)}
 /-- info: sexp!{(foo bar)} -/
-#guard_msgs in #eval sexp!{(...{[Sexp.atom "foo"]} ...{[Sexp.atom "bar"]})}
+#guard_msgs in #eval sexp!{(⦃[Sexp.atom "foo"]⦄ bar)}
 /-- info: sexp!{(foo bar)} -/
-#guard_msgs in #eval sexp!{(...{[Sexp.atom "foo", Sexp.atom "bar"]})}
+#guard_msgs in #eval sexp!{(⦃[Sexp.atom "foo"]⦄ ⦃[Sexp.atom "bar"]⦄)}
+/-- info: sexp!{(foo bar)} -/
+#guard_msgs in #eval sexp!{(⦃[Sexp.atom "foo", Sexp.atom "bar"]⦄)}
 /-- info: sexp!{(foo bar)} -/
 #guard_msgs in #eval sexp!{{Sexp.expr [Sexp.atom "foo", Sexp.atom "bar"]}}
 /-- info: [] -/

Leanwuzla/Sexp/Dsl.lean

@@ -58,6 +58,37 @@ def typeCheck (e : Expr) : SolverM UInt8 := do
     logError m!"Error: {e.toMessageData}"
     return 1
 
+/--
+Reports messages on stdout and returns the new total number of errors reported.
+If `json` is true, prints messages as JSON (one per line).
+If a message's kind is in `severityOverrides`, it will be reported with
+the specified severity.
+-/
+private def reportMessages (msgLog : MessageLog) (opts : Options)
+    (json : Bool) (severityOverrides : NameMap MessageSeverity) (numErrors : Nat) : IO Nat := do
+  let includeEndPos := Lean.Language.printMessageEndPos.get opts
+  msgLog.unreported.foldlM (init := numErrors) fun numErrors msg => do
+    let numErrors := numErrors + (if msg.severity matches .error then 1 else 0)
+    let maxErrorsReached := Lean.Language.maxErrors.get opts != 0 && numErrors > Lean.Language.maxErrors.get opts
+    let msg : Message :=
+      if maxErrorsReached then { msg with
+        data := s!"maximum number of errors ({Lean.Language.maxErrors.get opts}; from option `maxErrors`) reached, exiting"
+        severity := .error
+      } else if let some severity := severityOverrides.find? msg.kind then
+        {msg with severity}
+      else
+        msg
+    unless msg.isSilent do
+      if json then
+        let j ← msg.toJson
+        IO.println j.compress
+      else
+        let s ← msg.toString includeEndPos
+        IO.print s
+    if maxErrorsReached then
+      IO.Process.exit 1
+    return numErrors
+
 def parseAndDecideSmt2File : SolverM UInt8 := do
   try
     let goalType ← parseSmt2File (← SolverM.getInput)
@@ -71,7 +102,7 @@ def parseAndDecideSmt2File : SolverM UInt8 := do
         decideSmt goalType
   finally
     printTraces
-    Lean.Language.reportMessages (← Core.getMessageLog) (← getOptions)
+    reportMessages (← Core.getMessageLog) (← getOptions) false {} 0
 
 section Cli
 

Main.lean

@@ -1,14 +1,24 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/lean4-cli",
+ [{"url": "https://github.com/opencompl/fp-lean",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "a781e29cc715279a45f1c11022b774a09e13da5f",
+   "name": "«fp-lean»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "1604206fcd0462da9a241beeac0e2df471647435",
+   "rev": "d9fc8ae23024be37424a189982c92356e37935c8",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "nightly-testing",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "leanwuzla",

lake-manifest.json

@@ -17,4 +17,9 @@ supportInterpreter = true
 [[require]]
 scope = "leanprover"
 name = "Cli"
+rev = "nightly-testing"
+
+[[require]]
+git = "https://github.com/opencompl/fp-lean"
+name = "fp-lean"
 rev = "main"

lakefile.toml

@@ -1 +1 @@
-nightly-2025-06-27
+leanprover/lean4:nightly-2025-11-23