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.
This requires: zulu-openjdk8, libantlr3c, python2-toml
Maintained by: Nick Smallbone
Keywords: prover,first-order,logic,smt
ChangeLog: cvc4
Homepage:
https://cvc4.cs.stanford.edu/
Download SlackBuild:
cvc4.tar.gz
cvc4.tar.gz.asc (FAQ)
(the SlackBuild does not include the source)
Individual Files: |
README |
cvc4.SlackBuild |
cvc4.info |
run-antlr |
slack-desc |
© 2006-2025 SlackBuilds.org Project. All rights reserved.
Slackware® is a registered trademark of
Patrick Volkerding
Linux® is a registered trademark of
Linus Torvalds