mirror of
https://github.com/Ponce/slackbuilds
synced 2024-12-01 01:00:03 +01:00
3d9cd787ed
Signed-off-by: Dave Woodfall <dave@slackbuilds.org> Signed-off-by: Willy Sudiarto Raharjo <willysr@slackbuilds.org>
11 lines
525 B
Text
11 lines
525 B
Text
CVC4 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. CVC4 supports
|
|
arithmetic, reasoning about arrays, and several other built-in
|
|
theories. Input problems are written in SMT-LIB format.
|
|
|
|
This package includes the cvc4 program, libraries, and Python 2
|
|
bindings.
|
|
|
|
Note that this SlackBuild builds CVC4 with readline support, which means
|
|
the resulting executable is licensed under the GPLv3.
|