Summary
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.
Versions
v1.7-r1 :: 0 :: gentoo
- Modified
- License
- GPL-2
- Keywords
- ~amd64 ~x86
- USE flags
- cln proofs readline replay statistics
USE flags
General
- cln
- Use sci-libs/cln
- proofs
- Support for proof generation
- readline
- Enable support for libreadline, a GNU line-editing library that almost everyone wants
- replay
- Turn on the replay feature
- statistics
- Include statistics
Dependencies
dev-java / antlr : A parser generator for many languages
dev-libs / antlr-c : The ANTLR3 C Runtime
dev-libs / boost : Boost Libraries for C++
dev-libs / gmp : Library for arbitrary-precision arithmetic on different type of numbers
Runtime Dependencies
dev-java / antlr : A parser generator for many languages
dev-libs / antlr-c : The ANTLR3 C Runtime
dev-libs / boost : Boost Libraries for C++
dev-libs / gmp : Library for arbitrary-precision arithmetic on different type of numbers
Change logs
- Repository mirror & CI · gentoo
Merge updates from master - Michał Górny · gentoo
*/*: Remove obsolete values from PYTHON_COMPAT
Signed-off-by: Michał Górny <mgorny@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Jakov Smolic · gentoo
sci-mathematics/cvc4: Remove old
Signed-off-by: Jakov Smolic <jakov.smolic@sartura.hr> Signed-off-by: David Seifert <soap@gentoo.org> - Alfredo Tupone · gentoo
sci-mathematics/cvc4: add python dep
Closes: https://bugs.gentoo.org/766099 Package-Manager: Portage-3.0.12, Repoman-3.0.2 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - David Seifert · gentoo
*/*: [QA] Use consistent function definition formatting
Signed-off-by: David Seifert <soap@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Tupone Alfredo · gentoo
sci-mathematics/cvc4: Add readline use flag
Closes: https://github.com/gentoo/gentoo/pull/12536 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> Package-Manager: Portage-2.3.66, Repoman-2.3.11 - Repository mirror & CI · gentoo
Merge updates from master - Tupone Alfredo · gentoo
sci-mathematics/cvc4: add statistics, replay and proofs use flag
Closes: https://github.com/gentoo/gentoo/pull/12520 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> Package-Manager: Portage-2.3.66, Repoman-2.3.11 - Repository mirror & CI · gentoo
Merge updates from master - Tupone Alfredo · gentoo
sci-mathematics/cvc4: Bump to 1.7
Closes: https://bugs.gentoo.org/688652 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> Package-Manager: Portage-2.3.66, Repoman-2.3.11 - Repository mirror & CI · gentoo
Merge updates from master - Tupone Alfredo · gentoo
sci-mathematics/cvc4: Add cvc4 to the tree
Package-Manager: Portage-2.3.40, Repoman-2.3.9