<commit_before># SMT Kit

SMT Kit is (an optionally type-safe) C++11 domain-specific language
to create [SMT-LIB][smt-lib] 2.0 formulas for Z3, MathSAT5 and CVC4.

[smt-lib]: http://www.smt-lib.org/

## Prerequisite

For SMT Kit to work, SMT solvers must be installed separately.
Read their software licences carefully.

Currently, SMT Kit supports [Z3][z3], [MathSAT5][msat] and [CVC4][cvc4].
Installation instructions can be found in the `solvers` directory.

[z3]: http://z3.codeplex.com/
[msat]: http://mathsat.fbk.eu/
[cvc4]: http://cvc4.cs.nyu.edu/

## Installation

To build SMT Kit on a (mostly) POSIX-compliant operating system,
execute the following commands from the `smt-kit` folder:

    $ ./autogen.sh
    $ ./configure
    $ make
    $ make test
    $ make install

If `./configure` fails, you may have to set environment variables
such as `CXX` and `CXXFLAGS`. For example, to compile on OS X with
LLVM use the command `./configure CXX=clang++ CXXFLAGS=-stdlib=libc++`.
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][autoconf].

[autoconf]: http://www.gnu.org/software/autoconf/

## API Usage

First, `#include <smt>`. An example with built-in operators follows:

```C++
// Symbol names 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;

smt::Z3Solver z3_solver;
z3_solver.add(lhs != rhs);
assert(smt::unsat != z3_solver.check());

// Should always explicitly specify the logic!
smt::MsatSolver msat_solver(smt::QF_BV_LOGIC);
msat_solver.add(lhs != rhs);
assert(smt::unsat == msat_solver.check());
```

The compiler will check the arguments of SMT functions at compile-time.
For example, the above example will not compile if the SMT constant `y`
were to be an integer. However, these compile-time checks do not apply to
logic signatures. For example, when `smt::QF_BV_LOGIC` is specified but
arrays are 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][api].

If Doxygen is installed on your system, SMT Kit's documentation can also
be automatically generated by the command `make doc`.

[api]: https://github.com/ahorn/smt-kit/blob/master/test/smt_functional_test.cpp

## Troubleshooting

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 and clang++ 4.2.
But the choice of compiler also depends on the underlying SMT solvers.
In particular, MathSAT5 on OS X does not currently link with clang++
and LLVM's C++11 standard library (libc++). As a workaround, g++ from
Mac Ports works fine. This compiler portability issue has been reported
to <EMAIL>.

## Bug Reports

Please submit patches as Github pull request, formatted according to the
existing coding style.<commit_msg>Sharpen API usage description in README<commit_after># SMT Kit

SMT Kit is (an optionally type-safe) C++11 domain-specific language
to create [SMT-LIB][smt-lib] 2.0 formulas for Z3, MathSAT5 and CVC4.

[smt-lib]: http://www.smt-lib.org/

## Prerequisite

For SMT Kit to work, SMT solvers must be installed separately.
Read their software licences carefully.

Currently, SMT Kit supports [Z3][z3], [MathSAT5][msat] and [CVC4][cvc4].
Installation instructions can be found in the `solvers` directory.

[z3]: http://z3.codeplex.com/
[msat]: http://mathsat.fbk.eu/
[cvc4]: http://cvc4.cs.nyu.edu/

## Installation

To build SMT Kit on a (mostly) POSIX-compliant operating system,
execute the following commands from the `smt-kit` folder:

    $ ./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][autoconf].

[autoconf]: http://www.gnu.org/software/autoconf/

## API Usage

First, `#include <smt>`. An example with built-in operators follows:

```C++
// 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;

smt::Z3Solver z3_solver;
z3_solver.add(lhs != rhs);
assert(smt::unsat != z3_solver.check());

// Should always explicitly specify the logic!
smt::MsatSolver msat_solver(smt::QF_BV_LOGIC);
msat_solver.add(lhs != rhs);
assert(smt::unsat == msat_solver.check());
```

The compiler will check the arguments of SMT functions at compile-time.
For example, the above example will not compile if `y` is a `smt::Int`.
However, these compile-time checks do not apply to logic signatures.
For example, when `smt::QF_BV_LOGIC` is specified but `smt::Array`s are
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][api].

If Doxygen is installed on your system, SMT Kit's documentation can also
be automatically generated by the command `make doc`.

[api]: https://github.com/ahorn/smt-kit/blob/master/test/smt_functional_test.cpp

## Troubleshooting

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 and clang++ 4.2.
But the choice of compiler also depends on the underlying SMT solvers.
In particular, MathSAT5 on OS X does not currently link with clang++
and LLVM's C++11 standard library (libc++). As a workaround, g++ from
Mac Ports works fine. This compiler portability issue has been reported
to <EMAIL>.

## Bug Reports

Please submit patches as Github pull request, formatted according to the
existing coding style.
{'fraction_non_alphanumeric': 0.10595219972598569, 'fraction_numerical': 0.009133810321205664, 'mean_word_length': 4.534962089300758, 'pattern_counts': {'":': 0, '<': 11, '<?xml version=': 0, '>': 11, 'https://': 2, 'lorem ipsum': 0, 'www.': 4, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '999197', 'n_tokens_mistral': 2118, 'n_tokens_neox': 2039, 'n_words': 848}