summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorTheodoros Foradis <theodoros.for@openmailbox.org>2017-07-25 19:11:12 +0300
committerLudovic Courtès <ludo@gnu.org>2017-07-29 23:03:47 +0200
commit313844d9dc098b44cd27dcfa1a26de306c9a8fe2 (patch)
tree0c747eaebd49d40882e3c076171cc2433f957497
parenta4078acf4ab7d694e86ffcaef2073d71e58508f1 (diff)
downloadgnu-guix-313844d9dc098b44cd27dcfa1a26de306c9a8fe2.tar
gnu-guix-313844d9dc098b44cd27dcfa1a26de306c9a8fe2.tar.gz
gnu: Add z3.
* gnu/packages/maths.scm (z3): New variable. Signed-off-by: Ludovic Courtès <ludo@gnu.org>
-rw-r--r--gnu/packages/maths.scm35
1 files changed, 35 insertions, 0 deletions
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 7d4cb45b18..6566d750b2 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -18,6 +18,7 @@
;;; Copyright © 2017 Paul Garlick <pgarlick@tourbillion-technology.com>
;;; Copyright © 2017 ng0 <contact.ng0@cryptolab.net>
;;; Copyright © 2017 Ben Woodcroft <donttrustben@gmail.com>
+;;; Copyright © 2017 Theodoros Foradis <theodoros.for@openmailbox.org>
;;;
;;; 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)))