Gentoo Packages

sci-mathematics/z3 (gentoo)

Search

Install

Install this package:

emerge -a sci-mathematics/z3

If the package is masked, you can unmask it using the autounmask tool or standard emerge options:

autounmask sci-mathematics/z3

Or alternatively:

emerge --autounmask-write -a sci-mathematics/z3

Package Information

Description:
Z3 is an efficient Satisfiability Modulo Theories (SMT) solver from Microsoft Research. Z3 is a solver for symbolic logic, a foundation for many software engineering tools. SMT solvers rely on a tight integration of specialized engines of proof. Each engine owns a piece of the global puzzle and implements specialized algorithms. For example, Z3’s engine for arithmetic integrates Simplex, cuts and polynomial reasoning, while an engine for strings are regular expressions integrate methods for symbolic derivatives of regular languages. A theme shared among many of the algorithms is how they exploit a duality between finding satisfying solutions and finding refutation proofs. The solver also integrates engines for global and local inferences and global propagation. Z3 is used in a wide range of software engineering applications, ranging from program verification, compiler validation, testing, fuzzing using dynamic symbolic execution, model-based software development, network verification, and optimization.
Homepage:
https://github.com/Z3Prover/z3/
License:
MIT

Versions

Version EAPI Keywords Slot
4.16.0 8 amd64 arm arm64 ~loong ~mips ~ppc ppc64 ~riscv ~sparc x86 0/$(ver_cut 1-2)

Metadata

Description

Maintainers

Upstream

Raw Metadata XML 
<pkgmetadata>
	<maintainer type="person">
		<email>mgorny@gentoo.org</email>
	</maintainer>
	<maintainer type="project">
		<email>sci@gentoo.org</email>
		<name>Gentoo Science Project</name>
	</maintainer>
	<longdescription>
    Z3 is an efficient Satisfiability Modulo Theories (SMT) solver from
    Microsoft Research. Z3 is a solver for symbolic logic, a foundation for
    many software engineering tools. SMT solvers rely on a tight integration of
    specialized engines of proof. Each engine owns a piece of the global puzzle
    and implements specialized algorithms. For example, Z3’s engine for
    arithmetic integrates Simplex, cuts and polynomial reasoning, while an
    engine for strings are regular expressions integrate methods for symbolic
    derivatives of regular languages. A theme shared among many of the
    algorithms is how they exploit a duality between finding satisfying
    solutions and finding refutation proofs. The solver also integrates engines
    for global and local inferences and global propagation. Z3 is used in a
    wide range of software engineering applications, ranging from program
    verification, compiler validation, testing, fuzzing using dynamic symbolic
    execution, model-based software development, network verification, and
    optimization.
  </longdescription>
	<use>
		<flag name="isabelle">Add integration support for the Isabelle/HOL
  theorem prover.</flag>
	</use>
	<upstream>
		<bugs-to>https://github.com/Z3Prover/z3/issues/</bugs-to>
		<remote-id type="github">Z3Prover/z3</remote-id>
	</upstream>
</pkgmetadata>

Lint Warnings

USE Flags

Manage flags for this package: euse -i <flag> -p sci-mathematics/z3 | euse -E <flag> -p sci-mathematics/z3 | euse -D <flag> -p sci-mathematics/z3

Flag Description 4.16.0
doc Add extra documentation (API, Javadoc, etc). It is recommended to enable per package instead of globally ✓
examples Install examples, usually source code ✓
gmp Add support for dev-libs/gmp (GNU MP library) ✓
isabelle Add integration support for the Isabelle/HOL theorem prover. ✓
java Add support for Java ✓
python Add optional support/bindings for the Python language ✓

Manifest

Type File Size Versions
DIST z3-4.16.0.tar.gz 6136396 bytes 4.16.0
Unmatched Entries
Type File Size