C++11 library for many-sorted logics
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 smt::Int.
However, these compile-time checks do not apply to logic signatures.
For example, when smt::QF_BV_LOGIC is specified for the solver but
an 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.
For SMT Kit to work, CVC4, MathSAT5 and Z3 must be installed
separately. Read their software licences carefully. The SMT solver's installation
instructions can be found in the solvers directory.
To build SMT Kit on a (mostly) POSIX-compliant operating system,
execute the following commands from the smt-kit directory:
$ ./autogen.sh
$ ./configure
$ make
$ make test
$ make install
If ./configure fails, you may have to set environment variables. For example,
to compile on OS X with clang++ use the command ./configure CXX=clang++.
But see also the troubleshooting section below.
If 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.
Note that 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.