[Matryoshka-devel] first release of SMBC, a tool for finding models in computational logic

Simon Cruanes simon.cruanes at inria.fr
Wed Jan 11 17:35:10 CET 2017


I have the pleasure to announce the release of SMBC [1] version 0.2.

SMBC ("satisfiability modulo bounded checking") is a solver for
a fragment of TIP [2] composed of algebraic datatypes and (terminating)
recursive functions. Given a boolean expression with unknowns in it,
SMBC tries to find values for those unknowns values such that the
expression reduces to true. For example, looking for a list `l`
such that `reverse l = l && length l=2 && sum l=10` (using Peano
arithmetic) will return `l=[5,5]`.

SMBC is being integrated into Nunchaku to complement the other solvers
(CVC4, Kodkod) on more computational problems. I also plan to submit a
paper on SMBC at CADE.

The software can be found at https://github.com/c-cube/smbc/releases/tag/0.2.
It is written in OCaml [3] and installable via opam [4]:
  $ opam install smbc


[1] https://github.com/c-cube/smbc
[2] http://tip-org.github.io/
[3] http://ocaml.org/
[4] http://opam.ocaml.org/

Simon Cruanes

key 49AA62B6, fingerprint 949F EB87 8F06 59C6 D7D3  7D8D 4AC0 1D08 49AA 62B6
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/matryoshka-devel/attachments/20170111/1ee35c02/attachment.sig>

More information about the matryoshka-devel mailing list