smtlib-tools

 1# smt-tools
 2
 3Various self-contained programs for working with [SMT-LIB] files.
 4Lousy research-grade code without documentation and lots of limitations and bugs.
 5Without modifications, they will likely not work for your use-case.
 6
 7## The Tools
 8
 9* `smt-analyze`: Analyzes the composition of `QF_BV` SMT-LIB files
10* `smt-normalize`: Normalizes SMT-LIB expression (e.g. removing incremental solving)
11* `smt-depth`: Calculates the maximum nesting depth as a complexity metric
12* `smt-simplify`: Simplifies selected expressions (e.g. all `bvadd`) using [Z3]
13
14## See also
15
16Some other tools I found useful:
17
18* [`smtfmt`]: Formats SMT-LIB expressions for human readability
19* [`diff-sexp`]: A tool for diffing SMT-LIB expressions
20* [`ddSMT`]: A delta debugger for SMT-LIB, can minimize SMT-LIB expressions
21* …
22
23[SMT-LIB]: https://smt-lib.org
24[`smtfmt`]: https://github.com/symflower/smtfmt
25[`diff-sexp`]: https://github.com/yav/simple-smt/blob/1.0.1/exe/DiffSExp.hs
26[`ddSMT`]: https://github.com/ddsmt/ddSMT
27[Z3]: https://github.com/Z3Prover/z3