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.8-r2 :: 0 :: gentoo
- Modified
- License
- GPL-2
- Keywords
- ~amd64 ~x86
- USE flags
- cln proofs readline statistics
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
Bugs
Change logs
- Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/cvc4: drop toml usage
Closes: https://bugs.gentoo.org/878679 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Sam James · gentoo
sci-mathematics/cvc4: fix PythonHasVersionUsage
Signed-off-by: Sam James <sam@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/cvc4: fix deps check
Closes: https://bugs.gentoo.org/833362 Package-Manager: Portage-3.0.30, Repoman-3.0.3 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Sam James · gentoo
sci-mathematics/cvc4: revbump for CMake config file fix
This file is installed and embeds the libdir path which will affect consumers trying to build against/detect cvc4. See: 03321382501b45387f99917ba5acf9aa627805bd Closes: https://bugs.gentoo.org/820515 Signed-off-by: Sam James <sam@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/cvc4: fix deps
Closes: https://bugs.gentoo.org/823023 Package-Manager: Portage-3.0.30, Repoman-3.0.3 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/cvc4: remove unused CMake variables
Closes: https://bugs.gentoo.org/829088 Package-Manager: Portage-3.0.30, Repoman-3.0.3 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/cvc4: PythonCompatUpdate
Package-Manager: Portage-3.0.30, Repoman-3.0.3 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/cvc4: version bump to 1.8
Package-Manager: Portage-3.0.18, Repoman-3.0.2 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Andreas Sturmlechner · gentoo
sci-mathematics/cvc4: python3_9, switch to cmake.eclass
Package-Manager: Portage-3.0.18, Repoman-3.0.3 Signed-off-by: Andreas Sturmlechner <asturm@gentoo.org> - 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