SlackBuilds Repository

15.0 > Academic > cvc4 (1.8)

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

Note that this SlackBuild builds CVC4 with readline support, which means
the resulting executable is licensed under the GPLv3.

This requires: zulu-openjdk8, libantlr3c, python2-toml

Maintained by: Nick Smallbone
Keywords: prover,first-order,logic,smt
ChangeLog: cvc4


Source Downloads:
antlr-3.4-complete.jar (1b91dea1c7d480b3223f7c8a9aa0e172)
CVC4-1.8.tar.gz (9f7657e21fec3c4042225b0b8f513c34)

Download SlackBuild:
cvc4.tar.gz.asc (FAQ)

(the SlackBuild does not include the source)

Individual Files:

Validated for Slackware 15.0

See our HOWTO for instructions on how to use the contents of this repository.

Access to the repository is available via:
ftp git cgit http rsync

© 2006-2023 Project. All rights reserved.
Slackware® is a registered trademark of Patrick Volkerding
Linux® is a registered trademark of Linus Torvalds