diff options
| author | Theodoros Foradis <theodoros.for@openmailbox.org> | 2017-07-25 19:11:12 +0300 |
|---|---|---|
| committer | Ludovic Courtès <ludo@gnu.org> | 2017-07-29 23:03:47 +0200 |
| commit | 313844d9dc098b44cd27dcfa1a26de306c9a8fe2 (patch) | |
| tree | 0c747eaebd49d40882e3c076171cc2433f957497 /gnu | |
| parent | a4078acf4ab7d694e86ffcaef2073d71e58508f1 (diff) | |
| download | gnu-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>
Diffstat (limited to 'gnu')
| -rw-r--r-- | gnu/packages/maths.scm | 35 |
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))) |