commit: ad8c6827e4f1a0a083298c9217cce9347a8621c7
Author: Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Tue Jan 10 02:49:54 2023 +0000
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Tue Jan 10 04:22:47 2023 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=ad8c6827
sci-mathematics/z3: update metadata xml
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>
sci-mathematics/z3/metadata.xml | 18 ++++++++++++++++++
1 file changed, 18 insertions(+)
diff --git a/sci-mathematics/z3/metadata.xml b/sci-mathematics/z3/metadata.xml
index b0bebabc397e..5ab7254e6517 100644
--- a/sci-mathematics/z3/metadata.xml
+++ b/sci-mathematics/z3/metadata.xml
@@ -11,11 +11,29 @@
<email>[email protected]</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>
