diff options
| author | B. Watson <yalhcru@gmail.com> | 2022-03-23 15:08:34 -0400 |
|---|---|---|
| committer | Willy Sudiarto Raharjo <willysr@slackbuilds.org> | 2022-03-26 01:20:12 +0700 |
| commit | f34f3ac21ba5a9c942d7be7522c3e0852cf4a463 (patch) | |
| tree | d789ae33f7cd9a79caf9c03a8dfeef495a7fc7a8 /academic/z3/README | |
| parent | 6ba9f7f3752fdeaf587e6a26a6b2765628506b58 (diff) | |
academic/z3: Updated for version 4.8.12.
Signed-off-by: B. Watson <yalhcru@gmail.com>
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, 4 insertions, 8 deletions
diff --git a/academic/z3/README b/academic/z3/README index a1f132277a05e..a1c4c5a806233 100644 --- a/academic/z3/README +++ b/academic/z3/README @@ -1,12 +1,8 @@ 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 +(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 +This package includes the z3 program as well as the C++, Python2, and +Python3 APIs. |