#solver #smt-solver #smt-lib #smt #sat #satisfiability

rsmt2-zz

Wrapper for SMT-LIB 2 compliant SMT solvers. With ZZ downstream fixes

2 releases

0.11.1 Feb 6, 2020
0.11.0 Jan 5, 2020

#532 in Science

MIT/Apache

185KB
3K SLoC

rsmt2

linux windows
Build Status Build status Latest Version codecov

A generic library to interact with SMT-LIB 2 compliant solvers running in a separate system process, such as Z3.

Crate.io documentation.

If you use this library consider contacting us on the repository so that we can add your project to the readme.

See CHANGES.md for the list of changes.

Future features (if requested)

  • support for more solvers
  • get-proof

Known projects using rsmt2

  • kinō, a model-checker for transition systems (abandoned)
  • hoice, a machine-learning-based predicate synthesizer for horn clauses

License

MIT/Apache-2.0

Dependencies

~2.5–3.5MB
~73K SLoC