sushant94/libsmt.rs

Rust Bindings to interact with SMTLIB2 compliant solvers

libsmt.rs's Issues

Extend supported commands

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:

• set-logic
• define-fun
• declare-fun
• declare-sort
• define-sort
• assert
• get-assertions
• check-sat
• get-proof
• get-unsat-core
• get-value
• get-assignment
• push
• pop
• get-option
• set-option
• get-info
• set-info
• exit

We would like to support them all

Implement more logics

The current SMTLIB2 implementation only supports a few bitvector logic.
See here for a complete list of logics defined according to the standard.

[CI] Setup continuous integration for libsmt

• Set up Travis and testing out SMTLIB2 implementation to work with atleast two popular SMT Solvers such as Z3 and CVC4.
• Set up coveralls.io to measure test coverage

Set timeout for read()

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.

[docs] Improve usage examples

• Add more usage examples to show use of more logics
• Write blogpost showing various aspects of libsmt2 such as:
  • Implementing a new solver backend
  • Implementing a new custom logic

Full SMTLIB v2.5 support

http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.5-r2015-06-28.pdf

Publish an official crate

Cleanup warnings

• Fix up some enum variants
• Add lints to allow non_camel_cased_types in places needed
• Compile with clippy to compile with more lints and fixup

Add re-exports

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.

Move under radare namespace may be

Since @sushant94 stopped development, may be it makes sense to move it under radare namespace?

Returned output from Z3 not properly captured in Windows

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 results from Z3 are marked as "Unsat".

This same code also doesn't account for an error returned from Z3, which isn't the same as "Unsat". This would be true for any environment.

Pass options to solver

Add support to pass options to the underlying solver.

libsmt.rs should return syntax error information using certain ErrorType

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).

[docs] Improve Documentation