Packages tagged smt

23 packages have this tag.

[Merge tag] (trustees only)

Related tags: library (23), formal-methods (15), theorem-provers (14), bsd3 (12), symbolic-computation (11), gpl (6), math (6), bit-vectors (5), mit (5), logic (2), program (2), algorithms (1), ...

Name
DLs
Rating
Rev Deps
Description
Tags
Last U/L
Last Version
Maintainers
boolector180.01Haskell bindings for the Boolector SMT solver (bit-vectors, formal-methods, library, math, mit, smt, theorem-provers)2020-08-200.0.0.13DeianStefan
grisette300.01Symbolic evaluation as a library (bsd3, formal-methods, library, smt, symbolic-computation, theorem-provers)2024-11-080.9.0.0siruilu
grisette-monad-coroutine30.00Support for monad-coroutine package with Grisette (bsd3, formal-methods, library, smt, symbolic-computation, theorem-provers)2024-01-100.2.0.0siruilu
hasmtlib822.00A monad for interfacing with external SMT solvers (gpl, library, logic, smt)2024-11-292.8.1bruderj15
hz3 (deprecated)80.00Bindings for the Z3 Theorem Prover (bit-vectors, bsd3, deprecated, formal-methods, library, math, smt, theorem-provers)2019-10-0196.0.0.0
linearEqSolver30.01Use SMT solvers to solve linear systems over integers and rationals (bsd3, library, math, smt)2020-05-132.3LeventErkok
sbv3932.7512SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. (bit-vectors, bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers)2024-11-0711.0LeventErkok
sbv-program30.00Component-based program synthesis using SBV (bit-vectors, bsd3, formal-methods, library, smt, symbolic-computation)2023-01-261.1.0.0arrowd
sbvPlugin20.01Formally prove properties of Haskell programs using SBV/SMT (bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers)2024-05-229.10.1LeventErkok
smt2-parser380.01A Haskell parser for SMT-LIB version 2.6 (bsd3, formal-languages, language, library, smt)2022-10-080.1.0.1liuyuxi, haskell_github_trust
smtLib210.03A library for working with the SMTLIB format. (bsd3, library, smt)2019-01-101.1IavorDiatchki
smtlib-backends442.05Low-level functions for SMT-LIB-based interaction with SMT solvers. (library, mit, smt)2024-05-280.4FacundoDominguez
smtlib-backends-process392.02An SMT-LIB backend running solvers as external processes. (library, mit, smt)2023-02-060.3FacundoDominguez
smtlib-backends-tests32.00Testing SMT-LIB backends. (library, mit, smt, testing)2023-02-060.3FacundoDominguez, qaristote
smtlib-backends-z382.01An SMT-LIB backend implemented using Z3's C API. (library, mit, smt)2024-01-290.3.1FacundoDominguez
smtlib2102.06A type-safe interface to communicate with an SMT solver. (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)2017-01-051.0HenningGuenther
smtlib2-debug20.01Dump the communication with an SMT solver for debugging purposes. (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)2017-01-051.0HenningGuenther
smtlib2-pipe30.01A type-safe interface to communicate with an SMT solver. (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)2017-01-051.0HenningGuenther
smtlib2-quickcheck10.01Helper functions to create SMTLib expressions in QuickCheck (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)2017-01-061.0HenningGuenther
smtlib2-timing30.01Get timing informations for SMT queries (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)2017-01-071.0HenningGuenther
toysolver180.04Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc (algorithms, bsd3, constraints, formal-methods, library, logic, optimisation, optimization, program, smt, theorem-provers)2022-09-170.8.1MasahiroSakai
what4682.258Solver-agnostic symbolic values support for issuing queries (bsd3, formal-methods, library, program, smt, symbolic-computation, theorem-provers)2024-09-231.6.2RobertDockins, ryanglscott, galoisinc, mccleeary
z3362.256Bindings for the Z3 Theorem Prover (bit-vectors, bsd3, formal-methods, library, math, smt, theorem-provers)2020-08-29408.2IagoAbal