Skip to content

A simple (unfinished) SMT solver for QF_ABV.

License

Unknown, MIT licenses found

Licenses found

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

Robbepop/stevia

Repository files navigation

Stevia - Satisfiability Modulo Theories (SMT) Solver

Linux Windows Chat Coveralls Codecov Metrics
travis appveyor chat coveralls licence tokei

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

License

Licensed under either of

at your option.

Dual licence: badge badge

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.

About

A simple (unfinished) SMT solver for QF_ABV.

Topics

Resources

License

Unknown, MIT licenses found

Licenses found

Unknown
LICENSE-APACHE
MIT
LICENSE-MIT

Code of conduct

Stars

Watchers

Forks

Packages

No packages published

Languages