diff options
| author | Liliana Marie Prikler <liliana.prikler@gmail.com> | 2023-02-25 09:24:58 +0100 |
|---|---|---|
| committer | Liliana Marie Prikler <liliana.prikler@gmail.com> | 2023-03-05 08:17:58 +0100 |
| commit | 367979cbff8a85a983535c6a0858f80ba36c72e2 (patch) | |
| tree | a328c3d35c41dffb18d574c2f80d340a0ec50e52 /gnu | |
| parent | 771d4f86ddb63670999a8ab47ee6888db71298f7 (diff) | |
| download | guix-367979cbff8a85a983535c6a0858f80ba36c72e2.tar.gz | |
gnu: Add yices.
* gnu/packages/maths.scm (yices): New variable.
Diffstat (limited to 'gnu')
| -rw-r--r-- | gnu/packages/maths.scm | 53 |
1 files changed, 53 insertions, 0 deletions
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index f9b050ddcb..069c2c07c2 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -123,6 +123,7 @@ #:use-module (gnu packages gd) #:use-module (gnu packages ghostscript) #:use-module (gnu packages glib) + #:use-module (gnu packages gperf) #:use-module (gnu packages graphviz) #:use-module (gnu packages gtk) #:use-module (gnu packages icu4c) @@ -6080,6 +6081,58 @@ as equations, scalars, vectors, and matrices.") (home-page "https://www.gnu.org/software/jacal/") (license license:gpl3+))) +(define-public yices + (package + (name "yices") + (version "2.6.4") + (source (origin + (method url-fetch) + (uri (string-append "https://yices.csl.sri.com/releases/" + version "/yices-" version "-src.tar.gz")) + (sha256 + (base32 + "1jvqvf35gv2dj936yzl8w98kc68d8fcdard90d6dddzc43h28fjk")))) + (build-system gnu-build-system) + (arguments + (list #:configure-flags + #~(list #$@(if (%current-target-system) + '() + (list (string-append "--build=" + (%current-system)))) + "--enable-mcsat" + ;; XXX: Ewww, static linkage + (string-append + "--with-static-libpoly=" + (search-input-file %build-inputs "lib/libpoly.a")) + (string-append + "--with-static-gmp=" + (search-input-file %build-inputs "lib/libgmp.a")) + (string-append + "--with-pic-libpoly=" + (search-input-file %build-inputs "lib/libpicpoly.a"))) + #:phases + #~(modify-phases %standard-phases + (add-after 'unpack 'fix-build-files + (lambda* (#:key outputs #:allow-other-keys) + (substitute* "Makefile.build" + (("SHELL=.*") "") + (("/sbin/ldconfig") (which "ldconfig"))) + (substitute* (find-files "etc" "install-yices.*") + (("/usr/bin/install") (which "install")) + (("/bin/ln") (which "ln")) + (("/sbin/ldconfig") (which "ldconfig")) + (("install_dir=.*") + (string-append "install_dir=" + (assoc-ref outputs "out"))))))))) + (inputs (list cudd gmp gperf libpoly)) + (native-inputs (list autoconf automake bash-minimal)) + (home-page "https://yices.csl.sri.com/") + (synopsis "Satisfiability modulo theories solver") + (description "Yices is a solver for @acronym{SMT, satisfiability modulo +theories} problems. It can process input in SMT-LIB format or its own +s-expression-based format.") + (license license:gpl3+))) + (define-public z3 (package (name "z3") |