From 313844d9dc098b44cd27dcfa1a26de306c9a8fe2 Mon Sep 17 00:00:00 2001 From: Theodoros Foradis Date: Tue, 25 Jul 2017 19:11:12 +0300 Subject: gnu: Add z3. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * gnu/packages/maths.scm (z3): New variable. Signed-off-by: Ludovic Courtès --- gnu/packages/maths.scm | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) (limited to 'gnu/packages/maths.scm') 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 ;;; Copyright © 2017 ng0 ;;; Copyright © 2017 Ben Woodcroft +;;; Copyright © 2017 Theodoros Foradis ;;; ;;; 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))) -- cgit 1.4.1