blob: ed00fa62b8bc10cd95059e9666cad7f04aea0db4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
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.
|
