Actor-based Smtlib-2 Scala Unified Malleable Package for real-Time Interaction On-demand.¶

Assumptio is an actor-based SMT lib 2.0 API written in Scala designed to allow its user to perform on the fly queries to a SMT solver, which internal state is maintained until closed by the user. As of today, only Microsoft Research's Z3 and University of Trento's MathSat 5 are supported. No matter how much the authors would like to add support for other solvers, it is very difficult to do so without proper user feedback and/or contribution. This is why Assumptio is released under the GPL license. We would like to convince Assumptio's potential users that it is easy to use, and most of all relatively easy to tweak. People wanting to participate are encouraged to send their customisations to the author in order to help Assumptio improving for the best of its users.