academic/z3: Added (theorem solver).

Signed-off-by: Willy Sudiarto Raharjo <willysr@slackbuilds.org>

1 files changed, 19 insertions, 0 deletions

diff --git a/academic/z3/slack-desc b/academic/z3/slack-desc
new file mode 100644
index 000000000000..c8a8e4c2c2b7
--- /dev/null
+++ b/academic/z3/slack-desc
@@ -0,0 +1,19 @@
+# HOW TO EDIT THIS FILE:
+# The "handy ruler" below makes it easier to edit a package description.
+# Line up the first '|' above the ':' following the base package name, and
+# the '|' on the right side marks the last column you can put a character in.
+# You must make exactly 11 lines for the formatting to be correct.  It's also
+# customary to leave one space after the ':' except on otherwise blank lines.
+
+  |-----handy-ruler------------------------------------------------------|
+z3: z3 (a first-order theorem prover and SMT solver)
+z3:
+z3: Z3 is an automated theorem prover and satisfiability modulo theories
+z3: (SMT) solver. Given a formula in first-order logic, it attempts to
+z3: either prove the formula or find a counterexample. Z3 supports
+z3: arithmetic, reasoning about arrays, and several other built-in
+z3: theories. Input problems are written in SMT-LIB format.
+z3: 
+z3: This package includes the z3 program as well as C++ and Python APIs.
+z3: 
+z3: Homepage: https://github.com/Z3Prover/z3/wiki