Gentoo Packages

Search

Package Information

Description:

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:

https://cvc4.github.io/

License:

GPL-2

Versions

Metadata

Description

• 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.

Maintainers

• Tupone Alfredo (tupone@gentoo.org) - Type: person

Upstream

• Remote IDs:
  • github: CVC4/CVC4-archived

<pkgmetadata>
	<maintainer type="person">
		<email>tupone@gentoo.org</email>
		<name>Tupone Alfredo</name>
	</maintainer>
	<longdescription lang="en">
		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.
	</longdescription>
	<use>
		<flag name="cln">Use <pkg>sci-libs/cln</pkg></flag>
		<flag name="statistics">Include statistics</flag>
		<flag name="proofs">Support for proof generation</flag>
	</use>
	<upstream>
		<remote-id type="github">CVC4/CVC4-archived</remote-id>
	</upstream>
</pkgmetadata>

Lint Warnings

• [Warning] Ebuild 1.8-r7 uses IUSE flag 'readline' which is not documented in metadata.xml. Add the flag to metadata.xml <use> section.
• [Warning] Missing md5-cache for version 1.8-r7. Run 'ebuild <ebuild_file> manifest' or 'egencache' to generate it.

USE Flags

Files

• cvc4-1.8-bash-5.2-fix.patch
• cvc4-1.8-cmake4.patch
• cvc4-1.8-destdir.patch
• cvc4-1.8-gentoo.patch
• cvc4-1.8-gnuinstalldirs.patch
• cvc4-1.8-musl.patch
• cvc4-1.8-size_t.patch
• cvc4-1.8-toml.patch

Manifest