mirror of
https://github.com/Ponce/slackbuilds
synced 2024-11-25 10:03:03 +01:00
12 lines
561 B
Text
12 lines
561 B
Text
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
|