Stevia - Satisfiability Modulo Theories (SMT) Solver
| Linux | Windows | Chat | Coveralls | Codecov | Metrics |
|---|---|---|---|---|---|
 |
 |
 |
 |
This is a brave attempt to write a simple SMT solver in the Rust (github) programming language.
It is based on the design of:
Currently the solver is in very early development phase.
Supported Theories (SMT)
- Bitvectors of fixed bit-width and modulo-two arithmetics.
- Non-extensional arrays, indexed by bitvectors with bitvector values.
- Only supports quantifier-free inputs.
The combined theory in SMT notation is called QF_ABV.
Future Goals
- Support inputs specified in SMTLib 2.6.
- Comprehensive documentation for all important parts of the code.
- Eventually be able to keep up with efficient SMT solvers like STP.
- C API to enable bindings for other languages.
- Use an efficient SAT solver under the hood, like candy and JamSAT.
Simplifications
Stevia supports word-level transformations, called simplifications, that it applies throughout the solving process. In the following is an example of what is possible with the WIP implementation of the simplifier.
The arithmetic expression in LISP syntax:
(+ x 42 (- x y) (* y (-5)) (- (+ x 10 y)))Is simplified to:
(+ 32 (* -7 y) x)This output can then be further processed by other simplification and solving processes.
Unstable Features Used
These features need to be stabilized before this crate can be used on the stable channel.
Current State: Rust version 1.26
-
Simplifier
-
Bitblaster
License
Licensed under either of
- Apache license, Version 2.0, (LICENSE-APACHE or http://www.apache.org/licenses/LICENSE-2.0)
- MIT license (LICENSE-MIT or http://opensource.org/licenses/MIT)
at your option.
Dual licence: 
Contribution
Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in the work by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any additional terms or conditions.