SMT Kit is a C++11 library for many-sorted logics. It particularly targets quantifier-free SMT-LIB 2.0 formulas. Currently, SMT Kit supports CVC4, MathSAT5 and Z3.
To use SMT Kit,
#include <smt>. Here's an API usage example that encodes and checks De Morgan's law:
// Symbols (e.g. "x") must be globally unique! smt::Bool x = smt::any<smt::Bool>("x"); smt::Bool y = smt::any<smt::Bool>("y"); smt::Bool lhs = !(x && y); smt::Bool rhs = !x || !y; // Other solvers include smt::MsatSolver and smt::Z3Solver smt::CVC4Solver solver; solver.add(lhs != rhs); assert(smt::unsat == solver.check());
The compiler will check the arguments of SMT functions at compile-time.
For example, the above example will not compile if
x is a
However, these compile-time checks do not apply to logic signatures.
For example, when
smt::QF_BV_LOGIC is specified for the solver but
smt::Array is also used, there won't be a compile-time error.
Several more examples including incremental solving, function applications and array logic expressions can be found in the functional tests.
To build SMT Kit on a (mostly) POSIX-compliant operating system,
execute the following commands from the
$ ./autogen.sh $ ./configure $ make $ make test $ make install
./configure fails, you may have to set environment variables. For example,
to compile on OS X with clang++ use the command
But see also the troubleshooting section below.
make test fails, you can still install, but it is likely that some
features of this library will not work correctly on your system.
Proceed at your own risk.
make install may require superuser privileges.
For advanced usage information on other configure options refer to the Autoconf documentation.
Since SMT Kit uses advanced C++11 language features, older compiler versions are likely to be troublesome. To date, we have successfully compiled and tested the code on OS X with g++ 4.8.1, g++ 4.9 and clang++ 4.2. You should also always use the most recent version of the SMT solvers.
You are warmly invited to submit patches as Github pull request, formatted according to the existing coding style.