libsmt.rs
libsmt.rs copied to clipboard
sushant94
Rust Bindings to interact with SMTLIB2 compliant solvers
Since @sushant94 stopped development, may be it makes sense to move it under radare namespace?
http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.5-r2015-06-28.pdf
This PR aims to achieve the following: * Uses channels to add a timeout functionality for the read() function of the SMTProcess. This enables us to wait until we receive...
The current implementation waits indefinitely to read from the process pipe. It would be nice to have a configurable option to set a timeout for read from the solvers.
It currently only returns `Unsat` which does not really give the user much information. This is particularly useful for consumers other than those directly using the library(Eg.rune).
It seems that "unsat" is stored as "u" and "sat" is stored as "s", meaning that in smtlib2.rs::check_sat(), the call to &smt_proc.read() never seems to return "sat\n", and so all...
The current modules level makes it hard to use some common components of the library such as opcodes. For a better developer experience, it is better to re-export these.
The current SMTLIB2 implementation only supports a few bitvector logic. See [here](http://smtlib.cs.uiowa.edu/logics.shtml) for a complete list of logics defined according to the standard.
smtlib.rs currently only supports a few of the defined standard command. According to the SMTLIB2 standard the following functions are to be recognized and implemented for every solver: - [x]...