me
/
guix
Archived
1
0
Fork 0

gnu: Add yices.

* gnu/packages/maths.scm (yices): New variable.
Liliana Marie Prikler 2023-02-25 09:24:58 +01:00
parent 771d4f86dd
commit 367979cbff
No known key found for this signature in database
GPG Key ID: 442A84B8C70E2F87
1 changed files with 53 additions and 0 deletions

View File

@ -123,6 +123,7 @@
#:use-module (gnu packages gd) #:use-module (gnu packages gd)
#:use-module (gnu packages ghostscript) #:use-module (gnu packages ghostscript)
#:use-module (gnu packages glib) #:use-module (gnu packages glib)
#:use-module (gnu packages gperf)
#:use-module (gnu packages graphviz) #:use-module (gnu packages graphviz)
#:use-module (gnu packages gtk) #:use-module (gnu packages gtk)
#:use-module (gnu packages icu4c) #:use-module (gnu packages icu4c)
@ -6080,6 +6081,58 @@ as equations, scalars, vectors, and matrices.")
(home-page "https://www.gnu.org/software/jacal/") (home-page "https://www.gnu.org/software/jacal/")
(license license:gpl3+))) (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 (define-public z3
(package (package
(name "z3") (name "z3")