Feature addition and issue fixes

chinmaydd commented 7 years ago

Aims to achieve the following:

Adds support for Boolector backend. Boolector is a SMT Solver which won 3 out of 6 tracks in the SMT Contest 2016. This is specifically interesting to us since it is observed to be extremely fast for Quantifier Free BitVector(QF_BV) logic. This can be helpful in getting faster results for rune. Also, it supports SMTLibv2 format for input so it becomes all the more easier to integrate. This requires you to have the boolector binary in your PATH variable. The source for the library can be found here.
Adds a dummy function proc_specific_read(), due to the z3 buffering issue.
Adds function get_node_info() for the solver instance which exposes an API to get node data so that it becomes a bit easier for debugging in other libraries(such as for example, once again, rune/radeco).

Tests failing since we don't have boolector installed.

chinmaydd commented 7 years ago

@sushant94 have a look when free.

chinmaydd commented 7 years ago

Merging this for now. Can be reverted later if modifications are needed.

sushant94 / libsmt.rs