|0.16.2||Sep 12, 2022|
|0.16.0||Apr 19, 2022|
|0.14.1||Nov 18, 2021|
|0.12.0||Apr 5, 2021|
|0.2.0||Sep 15, 2016|
#50 in Science
563 downloads per month
Used in 2 crates (via mikino_api)
A generic library to interact with SMT-LIB 2 compliant solvers running in a separate system process, such as z3 and CVC4.
If you use this library consider contacting us on the repository so that we can add your project to the readme.
changes.md for the list of changes.
- support main solvers (z3, CVC4, Yices 2)
- all basic declaration/definition/assertion/model/values commands
check-sat-assuming, with dedicated actlit API
- the commands to run each solver can be passed through environment variables, see the
Known projects using
- kinō, a model-checker for transition systems (abandoned)
- hoice, a machine-learning-based predicate synthesizer for horn clauses