Metraipolis › archive › dc_ceb59db8eb99

Blazing-Fast SMT-LIB Parsing for Rust and Lean — arXiv:2611.00185

Source: arXiv (en)
Original: https://arxiv.org/abs/2611.00185
License (as archived): CC0-1.0
Archived: 2026-11-03T11:45:53.554Z
SHA-256 of the archived text: 70dbfdc4a1b7d639053d3e2149b4295dc3d6c8678518c2e2e290ad255e2c25f2
Stable URL of this page: https://metraipolis.com/documento/dc_ceb59db8eb99

How to cite

Blazing-Fast SMT-LIB Parsing for Rust and Lean — arXiv:2611.00185 — arXiv (en), https://arxiv.org/abs/2611.00185 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_ceb59db8eb99 (Metraipolis archive dc_ceb59db8eb99, sha256 70dbfdc4a1b7d639053d3e2149b4295dc3d6c8678518c2e2e290ad255e2c25f2)

BibTeX

@misc{dcceb59db8eb99,
  title = {Blazing-Fast SMT-LIB Parsing for Rust and Lean — arXiv:2611.00185},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2611.00185},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_ceb59db8eb99; sha256 70dbfdc4a1b7d639053d3e2149b4295dc3d6c8678518c2e2e290ad255e2c25f2},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2611.00185. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

SMT-LIB is a standard input format for Satisfiability Modulo Theories (SMT) solvers. However, parsing the format is non-trivial and can become a bottleneck, e.g. when retrieving benchmark metadata or normalising the input for solvers. We introduce blazing-smtlib, a Rust parsing library for SMT-LIB, and BSmtLib, its port to Lean. We outline the library API we designed for composability and extensibility (including non-standard SMT-LIB commands), and discuss our implementation decisions for fast lexing and parsing. We proved that our lexing and parsing with Lean-specific optimisations match our formalised reading of the SMT-LIB syntax. We measured performance on a representative sample from the 2025 SMT-LIB corpus and found that blazing-smtlib is more than 6 times faster on the geometric mean than previous parsing libraries and BSmtLib is faster or comparable to them.

Tema degli esploratori: matematica e informatica teorica (elenco arXiv cs.LO, nuovi lavori del giorno).
Categorie arXiv: Logic in Computer Science (cs.LO) ; Programming Languages (cs.PL).
Pagina del lavoro: https://arxiv.org/abs/2611.00185 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-11-03T11:08:07.222Z dalla pagina https://arxiv.org/list/cs.LO/new (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).