cvc4
Automatic theorem prover for satisfiability modulo theories (SMT) problems
CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination.
homepage ↗ github: CVC4/CVC4-archived
Available in
| Overlay | Newest | Ebuilds | Last activity | |
|---|---|---|---|---|
| gentoo gitweb ↗ | 1.8-r7 | 1 | 17 h | details › |
Versions & arches
Use flags of 1.8-r7
- +cln Use sci-libs/cln
- proofs Support for proof generation
- readline Enable support for libreadline, a GNU line-editing library that almost everyone wants
- +statistics Include statistics
Runtime dependencies of 1.8-r7
show 12 lines
readline?
(
)
cln?
(
)
!cln?
(
)