03/04: gnu: Add z3.

[Ludovic Courtès]

civodul pushed a commit to branch master
in repository guix.

commit 313844d9dc098b44cd27dcfa1a26de306c9a8fe2
Author: Theodoros Foradis <address@hidden>
Date:   Tue Jul 25 19:11:12 2017 +0300

    gnu: Add z3.
    
    * gnu/packages/maths.scm (z3): New variable.
    
    Signed-off-by: Ludovic Courtès <address@hidden>
---
 gnu/packages/maths.scm | 35 +++++++++++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 7d4cb45..6566d75 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -18,6 +18,7 @@
 ;;; Copyright © 2017 Paul Garlick <address@hidden>
 ;;; Copyright © 2017 ng0 <address@hidden>
 ;;; Copyright © 2017 Ben Woodcroft <address@hidden>
+;;; Copyright © 2017 Theodoros Foradis <address@hidden>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -3161,3 +3162,37 @@ as equations, scalars, vectors, and matrices.")
     (home-page "https://www.gnu.org/software/jacal/";)
     (license license:gpl3+)))
 
+(define-public z3
+  (package
+    (name "z3")
+    (version "4.5.0")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append
+                    "https://github.com/Z3Prover/z3/archive/z3-";
+                    version ".tar.gz"))
+              (sha256
+               (base32
+                "032a5lvji2liwmc25jv52bdrhimqflvqbpg77ccaq1jykhiivbmf"))))
+    (build-system gnu-build-system)
+    (arguments
+     `(#:test-target "test"
+       #:phases
+       (modify-phases %standard-phases
+         (replace 'configure
+           (lambda* (#:key inputs outputs #:allow-other-keys)
+             (zero?
+              (system* "python" "scripts/mk_make.py"
+                       (string-append "--prefix="
+                                      (assoc-ref outputs "out"))))))
+         (add-after 'configure 'change-dir
+           (lambda _
+             (chdir "build")
+             #t)))))
+    (native-inputs
+     `(("python" ,python-2)))
+    (synopsis "Theorem prover")
+    (description "Z3 is a theorem prover and @dfn{satisfiability modulo
+theories} (SMT) solver.  It provides a C/C++ API.")
+    (home-page "https://github.com/Z3Prover/z3";)
+    (license license:expat)))