[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
03/04: gnu: Add z3.
From: |
Ludovic Courtès |
Subject: |
03/04: gnu: Add z3. |
Date: |
Sat, 29 Jul 2017 17:03:54 -0400 (EDT) |
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)))