feat: add support for parsing Lean options

Leanwuzla/Parser.lean

@@ -152,7 +152,7 @@ where
       have w : Q(Nat) := (← parseTerm x).fst.appArg!
       let (_, (x : Q(BitVec $w))) ← parseTerm x
       let (_, (y : Q(BitVec $w))) ← parseTerm y
-      return (q(BitVec $w), q(BitVec.smtUDiv $x $y))
+      return (q(BitVec $w), q($x / $y))
     | sexp!{(bvurem {x} {y})} =>
       have w : Q(Nat) := (← parseTerm x).fst.appArg!
       let (_, (x : Q(BitVec $w))) ← parseTerm x

Main.lean

@@ -63,10 +63,25 @@ open Elab Command in
 def elabParseAndDecideSmt2File (path : System.FilePath) : CommandElabM Unit := do
   runTermElabM fun _ => parseAndDecideSmt2File path
 
+def parseOptions (args : List String) : IO (Options × List String) := do
+  let (opts, args) := go {} args
+  return (← Lean.Language.Lean.reparseOptions opts, args)
+where
+  go (opts : Options) : List String → (Options × List String)
+    | "-D" :: arg :: args =>
+      if let [name, value] := arg.splitOn "=" then
+          let opts := opts.set name.toName value
+          go opts args
+      else
+        (opts, args)
+    | args => (opts, args)
+
 unsafe def main (args : List String) : IO Unit := do
   Lean.initSearchPath (← Lean.findSysroot)
-  let some (path : String) := args[0]?
-    | throw (.userError "usage: lake exe leanwuzla /path/to/file.smt2")
-  withImportModules #[`Std.Tactic.BVDecide] Options.empty 0 fun env => do
+  let (opts, args) ← parseOptions args
+  IO.println opts
+  let [path] := args
+    | throw (.userError "usage: lake exe leanwuzla [-D name=value] /path/to/file.smt2")
+  withImportModules #[`Std.Tactic.BVDecide] {} 0 fun env => do
     _ ← Meta.MetaM.toIO (parseAndDecideSmt2File path)
-      { fileName := "leanwuzla", fileMap := default, options := Options.empty } { env := env }
+      { fileName := "leanwuzla", fileMap := default, options := opts } { env := env }

README.md

@@ -14,11 +14,11 @@ Alternatively to compare `bv_decide` and `bv_bitwuzla` directly run:
 bv_compare "/path/to/bitwuzla"
 ```
 
-## Terminal Frontend
+## SMT-LIB v2 Terminal Frontend
 This provides the ability to call `bv_decide` with QF_BV SMT-LIB v2 problems. You can call it like
 this:
 ```
-lake exe leanwuzla /path/to/file.smt2
+lake exe leanwuzla [-D name=value] /path/to/file.smt2
 ```
 
 ## Quality and Stability