Packages tagged smt
25 packages have this tag.
[Merge tag] (trustees only)Related tags: library (25), formal-methods (16), theorem-provers (15), bsd3 (14), symbolic-computation (12), gpl (6), math (6), bit-vectors (5), mit (5), language (2), logic (2), program (2), ...
Name |
DLs |
Rating |
Rev Deps |
Description |
Tags |
Last U/L |
Last Version |
Maintainers |
|---|---|---|---|---|---|---|---|---|
| boolector | 28 | 0.0 | 1 | Haskell bindings for the Boolector SMT solver | (bit-vectors, formal-methods, library, math, mit, smt, theorem-provers) | 2020-08-20 | 0.0.0.13 | DeianStefan |
| grisette | 42 | 0.0 | 1 | Symbolic evaluation as a library | (bsd3, formal-methods, library, smt, symbolic-computation, theorem-provers) | 2025-07-16 | 0.13.0.1 | siruilu |
| grisette-monad-coroutine | 4 | 0.0 | 0 | Support for monad-coroutine package with Grisette | (bsd3, formal-methods, library, smt, symbolic-computation, theorem-provers) | 2024-01-10 | 0.2.0.0 | siruilu |
| hasmtlib | 41 | 2.0 | 0 | A monad for interfacing with external SMT solvers | (gpl, library, logic, smt) | 2024-11-29 | 2.8.1 | bruderj15 |
| hz3 (deprecated) | 4 | 0.0 | 0 | Bindings for the Z3 Theorem Prover | (bit-vectors, bsd3, deprecated, formal-methods, library, math, smt, theorem-provers) | 2019-10-01 | 96.0.0.0 | |
| language-smtlib | 5 | 0.0 | 1 | Parsing, printing and incremental I/O for the SMT-LIB 2 format | (bsd3, language, library, smt) | 2026-07-06 | 0.2.0.0 | MasahiroSakai |
| linearEqSolver | 10 | 0.0 | 1 | Use SMT solvers to solve linear systems over integers and rationals | (bsd3, library, math, smt) | 2024-12-23 | 2.4 | LeventErkok |
| sbv | 422 | 2.75 | 15 | SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. | (bit-vectors, bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers) | 2026-08-31 | 14.7 | LeventErkok |
| sbv-program | 4 | 0.0 | 0 | Component-based program synthesis using SBV | (bit-vectors, bsd3, formal-methods, library, smt, symbolic-computation) | 2023-01-26 | 1.1.0.0 | arrowd |
| sbvPlugin | 27 | 0.0 | 1 | Formally prove properties of Haskell programs using SBV/SMT | (bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers) | 2026-01-12 | 9.14.1 | LeventErkok |
| smt2-parser | 4 | 0.0 | 1 | A Haskell parser for SMT-LIB version 2.6 | (bsd3, formal-languages, language, library, smt) | 2022-10-08 | 0.1.0.1 | liuyuxi, haskell_github_trust |
| smtLib | 30 | 0.0 | 3 | A library for working with the SMTLIB format. | (bsd3, library, smt) | 2019-01-10 | 1.1 | IavorDiatchki |
| smtlib-backends | 6 | 2.0 | 5 | Low-level functions for SMT-LIB-based interaction with SMT solvers. | (library, mit, smt) | 2024-05-28 | 0.4 | FacundoDominguez |
| smtlib-backends-process | 6 | 2.0 | 2 | An SMT-LIB backend running solvers as external processes. | (library, mit, smt) | 2023-02-06 | 0.3 | FacundoDominguez |
| smtlib-backends-tests | 3 | 2.0 | 0 | Testing SMT-LIB backends. | (library, mit, smt, testing) | 2023-02-06 | 0.3 | FacundoDominguez, qaristote |
| smtlib-backends-z3 | 4 | 2.0 | 1 | An SMT-LIB backend implemented using Z3's C API. | (library, mit, smt) | 2024-01-29 | 0.3.1 | FacundoDominguez |
| smtlib2 | 11 | 2.0 | 6 | A type-safe interface to communicate with an SMT solver. | (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers) | 2017-01-05 | 1.0 | HenningGuenther |
| smtlib2-debug | 2 | 0.0 | 1 | Dump the communication with an SMT solver for debugging purposes. | (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers) | 2017-01-05 | 1.0 | HenningGuenther |
| smtlib2-pipe | 2 | 0.0 | 1 | A type-safe interface to communicate with an SMT solver. | (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers) | 2017-01-05 | 1.0 | HenningGuenther |
| smtlib2-quickcheck | 3 | 0.0 | 1 | Helper functions to create SMTLib expressions in QuickCheck | (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers) | 2017-01-06 | 1.0 | HenningGuenther |
| smtlib2-timing | 4 | 0.0 | 1 | Get timing informations for SMT queries | (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers) | 2017-01-07 | 1.0 | HenningGuenther |
| toysolver | 76 | 0.0 | 4 | Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc | (algorithms, bsd3, constraints, formal-methods, library, logic, optimisation, optimization, program, smt, theorem-provers) | 2026-07-20 | 0.10.0 | MasahiroSakai |
| what4 | 60 | 2.25 | 11 | Solver-agnostic symbolic values support for issuing queries | (bsd3, formal-methods, library, program, smt, symbolic-computation, theorem-provers) | 2026-09-01 | 1.8 | RobertDockins, ryanglscott, galoisinc, mccleeary, sauclovian_g, aschwerdfeger_galois |
| what4-domains | 5 | 0.0 | 1 | Abstract domains for What4 term simplification | (bsd3, formal-methods, library, smt, symbolic-computation, theorem-provers) | 2026-09-01 | 0.1 | ryanglscott, galoisinc, sauclovian_g, aschwerdfeger_galois |
| z3 | 17 | 2.25 | 6 | Bindings for the Z3 Theorem Prover | (bit-vectors, bsd3, formal-methods, library, math, smt, theorem-provers) | 2020-08-29 | 408.2 | IagoAbal |