summaryrefslogtreecommitdiff
path: root/academic/cvc4/README
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.