diff options
| author | Nick Smallbone <nick@smallbone.se> | 2019-03-23 07:25:53 +0700 |
|---|---|---|
| committer | Willy Sudiarto Raharjo <willysr@slackbuilds.org> | 2019-03-23 07:25:53 +0700 |
| commit | a2e13bb161cb7663a1f2ecf371e4e2c6a5fc6cf2 (patch) | |
| tree | 05fb1ecb2d857a105831dddd49639b81c67abafd /academic/z3/README | |
| parent | 2cfe3736aead301f8d4ff51117fdba1fb4134712 (diff) | |
| download | slackbuilds-a2e13bb161cb7663a1f2ecf371e4e2c6a5fc6cf2.tar.xz | |
academic/z3: Added (theorem solver).
Signed-off-by: Willy Sudiarto Raharjo <willysr@slackbuilds.org>
Diffstat (limited to 'academic/z3/README')
| -rw-r--r-- | academic/z3/README | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/academic/z3/README b/academic/z3/README new file mode 100644 index 000000000000..a1f132277a05 --- /dev/null +++ b/academic/z3/README @@ -0,0 +1,12 @@ +Z3 is an automated theorem prover and satisfiability modulo theories +(SMT) solver. Given a formula in first-order logic, it attempts to +either prove the formula or find a counterexample. Z3 supports +arithmetic, reasoning about arrays, and several other built-in +theories. Input problems are written in SMT-LIB format. + +This package includes the z3 program as well as the C++ and +Python APIs. By default the Python 2 version of the API is built; +if you also want the Python 3 version, run the SlackBuild with +PYTHON3=yes, like so: + + PYTHON3=yes ./z3.SlackBuild |