smt-lib 开源项目推荐（39 个）

testsmt /yinyang

SMT求解器的模糊框架

Gbury /dolmen

Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction

formalsec /smtml

An SMT solver frontend for OCaml

touist /touist

TouIST, the IDE & Language for Logic (backed by SAT, SMT and QBF solvers)

elsoroka /Satisfiability.jl

Specify satisfiability modulo theories problems in Julia and use the SMT-LIB format to interact with SMT solvers.

uuverifiers /princess

The Princess Theorem Prover

acorrenson /modulus

A constraint solver built from scratch in OCaml

florianschanda /PyMPF

Arbitrary precision IEEE-754 implementation in Python for generating SMTLIB float benchmarks

florianschanda /smtlib_schanda

Floating-point SMTLIB benchmarks

symflower /smtfmt

An SMT-LIB formatter.

CLC-UIowa /SySLite

SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces

KarpelesLab /z3rs

Pure-Rust, no_std port of the Z3 theorem prover — SMT-LIB 2 front end, C ABI, no GMP/C/native dependencies

patrick96 /SMTransform

Find soundness bugs in SMT solvers through equivalent transformations

edoput /guile-smt

output SMT syntax from Guile

paultristanwagner /smt-rex

An SMT solver in Rust that proves its answers: QF_UF, QF_LRA, QF_LIA, QF_NRA, QF_BV, with LRAT and Alethe proofs.

soaibsafi /smt-z3-vscode

VSCode extension for SMT2 language with Z3 solver

Valendrew /vlsi-design

Combinatorial and Decision Making Optimization (CDMO) project during the A.Y. 2021/2022.

aztek /tptp2smt

A translator from TPTP to SMT-LIB

nicdard /fusion-function-generator

A generator for Semantic Fusion

maheenmatin /CRTSolver

Python algorithm extending cvc5, with up to 7.8x speedup for QF_NIA