2019-03-23 02:17:49 +01:00
|
|
|
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.
|
|
|
|
|
|
2020-09-04 04:58:10 +02:00
|
|
|
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.
|
