Skip to content
forked from kino-mc/rsmt2

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

License

Apache-2.0, MIT licenses found

Licenses found

Apache-2.0
LICENSE-APACHE
MIT
LICENSE-MIT
Notifications You must be signed in to change notification settings

AdrienChampion/rsmt2

 
 

Repository files navigation

crates.io Documentation CI

rsmt2

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.

See changes.md for the list of changes.

Features

  • 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 conf module
  • alt-ergo
  • get-proof command

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

About

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

Resources

License

Apache-2.0, MIT licenses found

Licenses found

Apache-2.0
LICENSE-APACHE
MIT
LICENSE-MIT

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • Rust 100.0%