[Matryoshka-devel] first release of SMBC, a tool for finding models in computational logic
simon.cruanes at inria.fr
Wed Jan 11 17:35:10 CET 2017
I have the pleasure to announce the release of SMBC  version 0.2.
SMBC ("satisfiability modulo bounded checking") is a solver for
a fragment of TIP  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  and installable via opam :
$ opam install smbc
key 49AA62B6, fingerprint 949F EB87 8F06 59C6 D7D3 7D8D 4AC0 1D08 49AA 62B6
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 833 bytes
Desc: not available
More information about the matryoshka-devel