diff options
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 a1f132277a..a1c4c5a806 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. |