[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[bug#61783] [PATCH 3/6] gnu: Add yices.
From: |
Liliana Marie Prikler |
Subject: |
[bug#61783] [PATCH 3/6] gnu: Add yices. |
Date: |
Sat, 25 Feb 2023 09:24:58 +0100 |
* gnu/packages/maths.scm (yices): New variable.
---
gnu/packages/maths.scm | 53 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 53 insertions(+)
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 @@ (define-module (gnu packages maths)
#: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 @@ (define-public jacal
(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")
--
2.39.1
- [bug#61783] [PATCH 0/6] Add more SMT solvers, Liliana Marie Prikler, 2023/02/25
- [bug#61783] [PATCH 2/6] gnu: Add libpoly., Liliana Marie Prikler, 2023/02/25
- [bug#61783] [PATCH 3/6] gnu: Add yices.,
Liliana Marie Prikler <=
- [bug#61783] [PATCH 4/6] gnu: Add btor2tools., Liliana Marie Prikler, 2023/02/25
- [bug#61783] [PATCH 5/6] gnu: Add boolector., Liliana Marie Prikler, 2023/02/25
- [bug#61783] [PATCH 1/6] gnu: Add cudd., Liliana Marie Prikler, 2023/02/25
- [bug#61783] [PATCH 6/6] gnu: Add java-smtinterpol., Liliana Marie Prikler, 2023/02/25