summaryrefslogtreecommitdiff
path: root/gnu/packages/maths.scm
diff options
context:
space:
mode:
Diffstat (limited to 'gnu/packages/maths.scm')
-rw-r--r--gnu/packages/maths.scm587
1 files changed, 486 insertions, 101 deletions
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 4640237968..1853c77a14 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -55,10 +55,11 @@
;;; Copyright © 2022 Philip McGrath <philip@philipmcgrath.com>
;;; Copyright © 2022 Marek Felšöci <marek@felsoci.sk>
;;; Copyright © 2022 vicvbcun <guix@ikherbers.com>
-;;; Copyright © 2022 Liliana Marie Prikler <liliana.prikler@gmail.com>
+;;; Copyright © 2022, 2023 Liliana Marie Prikler <liliana.prikler@gmail.com>
;;; Copyright © 2022 Maximilian Heisinger <mail@maxheisinger.at>
;;; Copyright © 2022 Akira Kyle <akira@akirakyle.com>
;;; Copyright © 2022 Roman Scherer <roman.scherer@burningswell.com>
+;;; Copyright © 2023 Jake Leporte <jakeleporte@outlook.com>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -87,7 +88,9 @@
#:use-module (guix gexp)
#:use-module (guix utils)
#:use-module ((guix build utils) #:select (alist-replace))
+ #:use-module (guix build-system ant)
#:use-module (guix build-system cmake)
+ #:use-module (guix build-system copy)
#:use-module (guix build-system glib-or-gtk)
#:use-module (guix build-system gnu)
#:use-module (guix build-system meson)
@@ -103,6 +106,7 @@
#:use-module (gnu packages bash)
#:use-module (gnu packages bison)
#:use-module (gnu packages boost)
+ #:use-module (gnu packages calendar)
#:use-module (gnu packages check)
#:use-module (gnu packages cmake)
#:use-module (gnu packages compression)
@@ -123,7 +127,9 @@
#: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 groff)
#:use-module (gnu packages gtk)
#:use-module (gnu packages icu4c)
#:use-module (gnu packages image)
@@ -151,6 +157,7 @@
#:use-module (gnu packages pcre)
#:use-module (gnu packages popt)
#:use-module (gnu packages perl)
+ #:use-module (gnu packages prolog)
#:use-module (gnu packages pkg-config)
#:use-module (gnu packages pulseaudio)
#:use-module (gnu packages python)
@@ -172,6 +179,7 @@
#:use-module (gnu packages tls)
#:use-module (gnu packages version-control)
#:use-module (gnu packages wxwidgets)
+ #:use-module (gnu packages xdisorg)
#:use-module (gnu packages xml)
#:use-module (srfi srfi-1)
#:use-module (srfi srfi-26))
@@ -455,6 +463,101 @@ semiconductors.")
(license license:gpl3+)
(home-page "https://www.gnu.org/software/dionysus/")))
+(define-public dozenal
+ ;; There is no recent release, so use the latest commit.
+ (let ((revision "1")
+ (commit "328bc03ad544179f2cccda36763358c4216f188e"))
+ (package
+ (name "dozenal")
+ (version (git-version "12010904-3" revision commit))
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://codeberg.org/dgoodmaniii/dozenal")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "0knwfwjqdv854l5ny7csdpvp7r0md6a2k43a1l2lkyw9k3cglpph"))))
+ (build-system gnu-build-system)
+ (arguments
+ (list
+ ;; Some test scripts are included, but no makefile-driven
+ ;; tests, and they are all quite manual to run and check.
+ #:tests? #f
+ ;; Running with `make -j' causes the build to fail. This is likely
+ ;; because this project uses the "recursive make" structure, where
+ ;; each subdirectory contains its own make file, which is called by
+ ;; the top-level makefile.
+ #:parallel-build? #f
+ #:make-flags
+ #~(list (string-append "prefix=" #$output))
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'unpack 'chdir
+ (lambda _
+ (chdir "dozenal")))
+ (add-after 'chdir 'patch-lua-references
+ (lambda _
+ (let ((lua-name (strip-store-file-name
+ #$(this-package-input "lua"))))
+ (substitute* '("dozcal/Makefile"
+ "dozlua/Makefile")
+ (("lua52")
+ (string-take lua-name
+ (string-rindex lua-name #\.)))))))
+ (delete 'configure)
+ (add-before 'install 'make-bin-dir
+ (lambda _
+ (mkdir-p (string-append #$output "/bin"))))
+ (add-after 'install 'install-html-docs
+ (lambda _
+ (invoke "make"
+ (string-append "prefix=" #$output)
+ "installhtml")))
+ (add-after 'install-html-docs 'split-outputs
+ (lambda* (#:key inputs outputs #:allow-other-keys)
+ (for-each
+ (lambda (prog)
+ (let ((orig (string-append #$output "/bin/" prog))
+ (dst (string-append #$output:gui "/bin/" prog))
+ (man-orig (string-append #$output
+ "/share/man/man1/"
+ prog ".1"))
+ (man-dst (string-append #$output:gui
+ "/share/man/man1/"
+ prog ".1")))
+ (mkdir-p (dirname dst))
+ (rename-file orig dst)
+ (mkdir-p (dirname man-dst))
+ (rename-file man-orig man-dst)))
+ '("xdozdc" "gdozdc"))
+ (wrap-program (string-append #$output:gui "/bin/" "gdozdc")
+ `("PATH" = (,(string-append #$output "/bin")))
+ `("PERL5LIB" = (,(getenv "PERL5LIB")))))))))
+ (outputs '("out" "gui"))
+ (native-inputs (list groff pkg-config))
+ (inputs (list bash-minimal ;for wrap-program
+ libhdate
+ lua
+ ncurses
+ perl
+ perl-tk
+ perl-par
+ xforms))
+ (synopsis "Suite of dozenal programs")
+ (description
+ "The dozenal suite is a set of programs designed to assist with working
+in the dozenal (also called \"duodecimal\" or \"base twelve\") system. It
+includes number converters (dozenal-to-decimal and decimal-to-dozenal), an RPN
+calculator, a graphical calculator, a metric system converter (works with
+imperial, U.S. customary, SI metric, and the dozenal TGM), a pretty-printer
+for dozenal numbers, a date-and-time program, and a dozenal calendar programs,
+complete with events and to-dos.")
+ (home-page "https://codeberg.org/dgoodmaniii/dozenal")
+ (license license:gpl3+))))
+
(define-public dsfmt
(package
(name "dsfmt")
@@ -930,7 +1033,7 @@ large scale eigenvalue problems.")
(base32
"1155qixp26c12yrxc76z9mlfw2h3xxymxxv5znpgzh5gaykpndgj"))))
(build-system cmake-build-system)
- (home-page "http://www.netlib.org/lapack/")
+ (home-page "https://www.netlib.org/lapack/")
(inputs `(("fortran" ,gfortran)
("python" ,python-wrapper)))
(arguments
@@ -1033,7 +1136,7 @@ provide LAPACK for someone who does not have access to a Fortran compiler.")
(substitute* "TESTING/CMakeLists.txt"
(("^add_test\\(x[sd]hseqr.*" all)
(string-append "# " all "\n"))))))))
- (home-page "http://www.netlib.org/scalapack/")
+ (home-page "https://www.netlib.org/scalapack/")
(synopsis "Library for scalable numerical linear algebra")
(description
"ScaLAPACK is a Fortran 90 library of high-performance linear algebra
@@ -1655,7 +1758,7 @@ System (Grid, Point and Swath).")
"HDF-EOS5 is a software library built on HDF5 to support the construction
of data structures used in NASA's Earth Observing System (Grid, Point and
Swath).")
- (home-page "http://www.hdfeos.org/software/library.php#HDF-EOS5")
+ (home-page "https://www.hdfeos.org/software/library.php#HDF-EOS5")
;; Source files carry a permissive license header.
(license (license:non-copyleft home-page))))
@@ -1840,7 +1943,7 @@ the resulting text.")
`(("texlive" ,texlive-tiny)
("ghostscript" ,ghostscript)
("doxygen" ,doxygen)))
- (home-page "http://itpp.sourceforge.net")
+ (home-page "https://itpp.sourceforge.net")
(synopsis "C++ library of maths, signal processing and communication classes")
(description "IT++ is a C++ library of mathematical, signal processing and
communication classes and functions. Its main use is in simulation of
@@ -2703,12 +2806,20 @@ satisfiability checking (SAT).")
(package
(inherit clingo)
(name "python-clingo")
+ (version (package-version clingo)) ; for #$version in arguments
(arguments
(substitute-keyword-arguments (package-arguments clingo)
((#:configure-flags flags #~'())
#~(cons* "-DCLINGO_BUILD_WITH_PYTHON=pip"
"-DCLINGO_USE_LIB=yes"
#$flags))
+ ((#:imported-modules _ '())
+ `(,@%cmake-build-system-modules
+ (guix build python-build-system)))
+ ((#:modules _ '())
+ '((guix build cmake-build-system)
+ ((guix build python-build-system) #:prefix python:)
+ (guix build utils)))
((#:phases phases #~%standard-phases)
#~(modify-phases #$phases
(add-after 'unpack 'fix-failing-tests
@@ -2717,7 +2828,17 @@ satisfiability checking (SAT).")
(("ctl\\.solve\\(on_statistics=on_statistics\\)" all)
(string-append
all
- "; self.skipTest(\"You shall not fail.\")")))))))))
+ "; self.skipTest(\"You shall not fail.\")")))))
+ (add-after 'install 'install-distinfo
+ (lambda* (#:key inputs outputs #:allow-other-keys)
+ (with-directory-excursion (python:site-packages inputs outputs)
+ (let ((dir (string-append "clingo-" #$version ".dist-info")))
+ (mkdir-p dir)
+ (call-with-output-file (string-append dir "/METADATA")
+ (lambda (port)
+ (format port "Metadata-Version: 1.1~%")
+ (format port "Name: clingo~%")
+ (format port "Version: ~a~%" #$version)))))))))))
(inputs (list clingo python-wrapper))
(propagated-inputs (list python-cffi))
(native-inputs (modify-inputs (package-native-inputs clingo)
@@ -2727,6 +2848,41 @@ satisfiability checking (SAT).")
making it so that you can write @acronym{ASPs, Answer Set Programs} through
Python code.")))
+(define-public python-clorm
+ (package
+ (name "python-clorm")
+ (version "1.4.1")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/potassco/clorm")
+ (commit (string-append "v" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "0jx99y71mrgdicn1da5dwz5nzgvvpabrikff783sg4shbv2cf0b5"))))
+ (build-system pyproject-build-system)
+ (arguments
+ (list #:phases
+ #~(modify-phases %standard-phases
+ (add-before 'check 'fix-breaking-tests
+ (lambda _
+ ;; noclingo tests rely on this being set
+ (setenv "CLORM_NOCLINGO" "1")
+ (delete-file "tests/test_mypy_query.py")
+ (substitute* "tests/test_clingo.py"
+ (("self\\.assertTrue\\(os_called\\)" all)
+ (string-append "# " all))))))))
+ (propagated-inputs (list python-clingo))
+ (native-inputs (list python-typing-extensions))
+ (home-page "https://potassco.org")
+ (synopsis "Object relational mapping to clingo")
+ (description "@acronym{Clorm, Clingo ORM} provides an @acronym{ORM,
+Object Relational Mapping} interface to the @acronym{ASP, answer set
+programming} solver clingo. Its goal is to make integration of clingo
+into Python programs easier.")
+ (license license:expat)))
+
(define-public python-telingo
(package
(name "python-telingo")
@@ -2749,6 +2905,41 @@ Python code.")))
logic programs based on clingo.")
(license license:expat)))
+(define-public scasp
+ (let ((commit "89a427aa04ec6346425a40111c99b310901ffe51")
+ (revision "1"))
+ (package
+ (name "scasp")
+ (version (git-version "0.21.11.26" revision commit))
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/SWI-Prolog/sCASP")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "1ijqv9xr3imrdmz6nq7zqwsmmaxn638icig19m8900m7mjfpizs4"))))
+ (build-system copy-build-system)
+ (arguments
+ (list
+ #:install-plan #~`(("scasp" "bin/")
+ ("prolog" "lib/swipl/library"))
+ #:modules `((guix build copy-build-system)
+ ((guix build gnu-build-system) #:prefix gnu:)
+ (guix build utils)
+ (ice-9 regex))
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-before 'install 'build (assoc-ref gnu:%standard-phases 'build))
+ (add-after 'build 'check (assoc-ref gnu:%standard-phases 'check)))))
+ (native-inputs (list swi-prolog))
+ (home-page "https://github.com/SWI-Prolog/sCASP")
+ (synopsis "Interpreter for ASP programs with constraints")
+ (description "@code{s(CASP)} is a top-down interpreter for ASP programs
+with constraints.")
+ (license license:asl2.0))))
+
(define-public ceres
(package
(name "ceres-solver")
@@ -2968,61 +3159,6 @@ script files.")
#t))))))
(synopsis "High-level language for numerical computation (with GUI)")))
-(define-public opencascade-oce
- (package
- (name "opencascade-oce")
- (version "0.17.2")
- (source
- (origin
- (method git-fetch)
- (uri (git-reference
- (url "https://github.com/tpaviot/oce")
- (commit (string-append "OCE-" version))))
- (file-name (git-file-name name version))
- (patches (search-patches "opencascade-oce-glibc-2.26.patch"))
- (sha256
- (base32 "0rg5wzkvfmzfl6v2amyryb8dnjad0nn9kyr607wy2gch6rciah69"))))
- (build-system cmake-build-system)
- (arguments
- '(#:configure-flags
- (list "-DOCE_TESTING:BOOL=ON"
- "-DOCE_USE_TCL_TEST_FRAMEWORK:BOOL=ON"
- "-DOCE_DRAW:BOOL=ON"
- (string-append "-DOCE_INSTALL_PREFIX:PATH="
- (assoc-ref %outputs "out"))
- "-UCMAKE_INSTALL_RPATH")))
- (inputs
- (list freetype
- glu
- libxmu
- mesa
- tcl
- tk))
- (native-inputs
- `(("python" ,python-wrapper)))
- (home-page "https://github.com/tpaviot/oce")
- (synopsis "Libraries for 3D modeling and numerical simulation")
- (description
- "Open CASCADE is a set of libraries for the development of applications
-dealing with 3D CAD data or requiring industrial 3D capabilities. It includes
-C++ class libraries providing services for 3D surface and solid modeling, CAD
-data exchange, and visualization. It is used for development of specialized
-software dealing with 3D models in design (CAD), manufacturing (CAM),
-numerical simulation (CAE), measurement equipment (CMM), and quality
-control (CAQ) domains.
-
-This is the ``Community Edition'' (OCE) of Open CASCADE, which gathers
-patches, improvements, and experiments contributed by users over the official
-Open CASCADE library.")
- (license (list license:lgpl2.1; OCE libraries, with an exception for the
- ; use of header files; see
- ; OCCT_LGPL_EXCEPTION.txt
- license:public-domain; files
- ; src/Standard/Standard_StdAllocator.hxx and
- ; src/NCollection/NCollection_StdAllocator.hxx
- license:expat; file src/OpenGl/OpenGl_glext.h
- license:bsd-3)))); test framework gtest
-
(define-public opencascade-occt
(package
(name "opencascade-occt")
@@ -3179,7 +3315,7 @@ This is the certified version of the Open Cascade Technology (OCCT) library.")
(substitute* "api/gmsh.py"
(("find_library\\(\"gmsh\"\\)")
(simple-format #f "\"~a\"" libgmsh)))))))))
- (home-page "http://gmsh.info/")
+ (home-page "https://gmsh.info/")
(synopsis "3D finite element grid generator")
(description "Gmsh is a 3D finite element grid generator with a built-in
CAD engine and post-processor. Its design goal is to provide a fast, light
@@ -3239,7 +3375,7 @@ ASCII text files using Gmsh's own scripting language.")
(list ghostscript ;optional, for EPS/PS output
python-dbus
python-h5py ;optional, for HDF5 data
- python-pyqt-without-qtwebkit
+ python-pyqt
qtbase-5
qtsvg-5))
(propagated-inputs
@@ -3703,7 +3839,7 @@ bindings to almost all functions of SLEPc.")
(build-system gnu-build-system)
(native-inputs
(list autoconf automake))
- (home-page "http://us.metamath.org/")
+ (home-page "https://us.metamath.org/")
(synopsis "Proof verifier based on a minimalistic formalism")
(description
"Metamath is a tiny formal language and that can express theorems in
@@ -4382,7 +4518,7 @@ schemes.")
#:phases (modify-phases %standard-phases
(add-before 'check 'mpi-setup
,%openmpi-setup))))
- (home-page "http://www.p4est.org")
+ (home-page "https://www.p4est.org")
(synopsis "Adaptive mesh refinement on forests of octrees")
(description
"The p4est software library enables the dynamic management of a
@@ -4551,28 +4687,27 @@ point numbers.")
(define-public wxmaxima
(package
(name "wxmaxima")
- (version "22.05.0")
- (source
- (origin
- (method git-fetch)
- (uri (git-reference
- (url "https://github.com/wxMaxima-developers/wxmaxima")
- (commit (string-append "Version-" version))))
- (file-name (git-file-name name version))
- (sha256
- (base32 "1va56v9dys97yln4m1z3fz3k90lpy8i3kvcq0v1cbg36689aghm5"))))
+ (version "22.12.0")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/wxMaxima-developers/wxmaxima")
+ (commit (string-append "Version-" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "12bjadmy2mf7d8v4iszmzckahfcwjzaba8wpbigksh4brvhb4gj5"))))
(build-system cmake-build-system)
- (native-inputs
- `(("gettext" ,gettext-minimal)))
- (inputs
- (list wxwidgets
- maxima
- ;; Runtime support.
- adwaita-icon-theme
- gtk+
- shared-mime-info))
+ (native-inputs (list gettext-minimal))
+ (inputs (list bash-minimal
+ wxwidgets
+ maxima
+ ;; Runtime support.
+ adwaita-icon-theme
+ gtk+
+ shared-mime-info))
(arguments
- `(#:tests? #f ; tests fail non-deterministically
+ `(#:tests? #f ; tests fail non-deterministically
#:phases
(modify-phases %standard-phases
(add-after 'unpack 'patch-doc-path
@@ -4581,8 +4716,8 @@ point numbers.")
;; documentation. Only licensing information is placed there by
;; Guix.
(substitute* "src/Dirstructure.cpp"
- (("/doc/wxmaxima-\\%s") "/doc/wxmaxima"))
- #t))
+ (("/doc/wxmaxima-\\%s")
+ "/doc/wxmaxima"))))
(add-after 'install 'wrap-program
(lambda* (#:key inputs outputs #:allow-other-keys)
(wrap-program (string-append (assoc-ref outputs "out")
@@ -4595,15 +4730,15 @@ point numbers.")
(,(string-append (assoc-ref inputs "gtk+")
"/share/glib-2.0/schemas")))
`("XDG_DATA_DIRS" ":" prefix
- (;; Needed by gdk-pixbuf to know supported icon formats.
- ,(string-append
- (assoc-ref inputs "shared-mime-info") "/share")
+ ( ;; Needed by gdk-pixbuf to know supported icon formats.
+ ,(string-append (assoc-ref inputs "shared-mime-info")
+ "/share")
;; The default icon theme of GTK+.
- ,(string-append
- (assoc-ref inputs "adwaita-icon-theme") "/share"))))
- #t)))))
+ ,(string-append (assoc-ref inputs "adwaita-icon-theme")
+ "/share")))))))))
(home-page "https://wxmaxima-developers.github.io/wxmaxima/")
- (synopsis "Graphical user interface for the Maxima computer algebra system")
+ (synopsis
+ "Graphical user interface for the Maxima computer algebra system")
(description
"wxMaxima is a graphical user interface for the Maxima computer algebra
system. It eases the use of Maxima by making most of its commands available
@@ -4635,7 +4770,7 @@ full text searching.")
`(("openblas" ,openblas)
("lapack" ,lapack)
("arpack" ,arpack-ng)))
- (home-page "http://arma.sourceforge.net/")
+ (home-page "https://arma.sourceforge.net/")
(synopsis "C++ linear algebra library")
(description
"Armadillo is a C++ linear algebra library, aiming towards a good balance
@@ -5053,7 +5188,7 @@ Fresnel integrals, and similar related functions as well.")
(native-inputs
`(("cmake" ,cmake-minimal)
("m4" ,m4)))
- (home-page "http://faculty.cse.tamu.edu/davis/suitesparse.html")
+ (home-page "https://faculty.cse.tamu.edu/davis/suitesparse.html")
(synopsis "Suite of sparse matrix software")
(description
"SuiteSparse is a suite of sparse matrix algorithms, including: UMFPACK,
@@ -5081,7 +5216,7 @@ packages.")
(base32
"1dyjlq3fiparvm8ypwk6rsmjzmnwk81l88gkishphpvc79ryp216"))))
(build-system gnu-build-system)
- (home-page "http://math-atlas.sourceforge.net/")
+ (home-page "https://math-atlas.sourceforge.net/")
(inputs `(("gfortran" ,gfortran)
("lapack-tar" ,(package-source lapack))))
(outputs '("out" "doc"))
@@ -5337,7 +5472,7 @@ specifications.")
(install-file name include))
(find-files "." "\\.h$")))
#t))))))
- (home-page "http://lpsolve.sourceforge.net/")
+ (home-page "https://lpsolve.sourceforge.net/")
(synopsis "Mixed integer linear programming (MILP) solver")
(description
"lp_solve is a mixed integer linear programming solver based on the
@@ -5684,7 +5819,7 @@ FLANN is written in C++ and contains bindings for C, Octave and Python.")
(list mpfr readline))
(native-inputs
(list bison flex))
- (home-page "http://w-calc.sourceforge.net/index.php")
+ (home-page "https://w-calc.sourceforge.net/index.php")
(synopsis "Flexible command-line scientific calculator")
(description "Wcalc is a very capable calculator. It has standard functions
(sin, asin, and sinh for example, in either radians or degrees), many
@@ -6083,6 +6218,177 @@ as equations, scalars, vectors, and matrices.")
(home-page "https://www.gnu.org/software/jacal/")
(license license:gpl3+)))
+(define-public boolector
+ (package
+ (name "boolector")
+ (version "3.2.2")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/Boolector/boolector")
+ (commit version)))
+ (file-name (git-file-name name version))
+ (patches (search-patches "boolector-find-googletest.patch"))
+ (sha256
+ (base32
+ "07rvp3iry7a7ixwl0q7nc47fwky1s1cyia7gqrjsg46syqlxbz2c"))))
+ (build-system cmake-build-system)
+ (arguments
+ (list #:configure-flags
+ #~(list "-DBUILD_SHARED_LIBS=on"
+ (string-append
+ "-DBtor2Tools_INCLUDE_DIR="
+ (dirname (search-input-file %build-inputs
+ "include/btor2parser.h")))
+ (string-append
+ "-DBtor2Tools_LIBRARIES="
+ (search-input-file %build-inputs
+ "lib/libbtor2parser.so")))
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'unpack 'fix-cmake
+ (lambda _
+ (delete-file "cmake/FindCryptoMiniSat.cmake")
+ (substitute* (list "CMakeLists.txt" "src/CMakeLists.txt")
+ (("find_package\\(CryptoMiniSat\\)")
+ "find_package(cryptominisat5 CONFIG)
+find_package(louvain_communities)")
+ (("CryptoMiniSat_FOUND") "cryptominisat5_FOUND")
+ (("CryptoMiniSat_INCLUDE_DIR")
+ "CRYPTOMINISAT5_INCLUDE_DIRS")
+ (("CryptoMiniSat_LIBRARIES")
+ "CRYPTOMINISAT5_LIBRARIES"))))
+ (add-after 'unpack 'fix-sources
+ (lambda _
+ (substitute* (find-files "." "\\.c$")
+ (("\"btor2parser/btor2parser\\.h\"") "<btor2parser.h>")))))))
+ (inputs (list btor2tools
+ boost cryptominisat louvain-community sqlite))
+ (native-inputs (list googletest pkg-config python-wrapper))
+ (home-page "http://boolector.github.io/")
+ (synopsis "Bitvector-based theory solver")
+ (description "Boolector is a @acronym{SMT, satisfiability modulo theories}
+solver for the theories of fixed-size bit-vectors, arrays and uninterpreted
+functions.")
+ (license license:lgpl3+)))
+
+(define-public java-smtinterpol
+ (package
+ (name "java-smtinterpol")
+ (version "2.5")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/ultimate-pa/smtinterpol")
+ (commit version)))
+ (file-name (git-file-name name version))
+ (modules '((guix build utils)))
+ (snippet #~(begin
+ (delete-file-recursively "jacoco")
+ (delete-file-recursively "libs")
+ (delete-file-recursively "sonar")))
+ (sha256
+ (base32
+ "0bq5l7g830a8hxw1xyyfp2ph6jqk8ak0ichlymdglpnpngf6322f"))))
+ (build-system ant-build-system)
+ (arguments
+ (list #:build-target "dist"
+ #:test-target "runtests"
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'unpack 'fix-build.xml
+ (lambda _
+ (substitute* "build.xml"
+ (("<tstamp>") "<!--")
+ (("</tstamp>") "-->")
+ (("executable=\"git\"")
+ (string-append "executable=\""
+ (which "sh")
+ "\""))
+ (("<property file=.*/>" all)
+ (string-append all
+ "<property environment=\"env\" />"))
+ (("<classpath>" all)
+ (string-append
+ all
+ "<pathelement path=\"${env.CLASSPATH}\" />"))
+ (("<fileset file=\".*/libs/.*/>") "")
+ (("<junit")
+ "<junit haltonfailure=\"yes\""))
+ (call-with-output-file "describe"
+ (lambda (port)
+ (format port "echo ~a" #$version)))))
+ (add-before 'check 'delete-failing-tests
+ (lambda _
+ (delete-file
+ (string-append "SMTInterpolTest/src/de/uni_freiburg"
+ "/informatik/ultimate/smtinterpol/convert/"
+ "EqualityDestructorTest.java"))))
+ (replace 'install
+ (lambda* (#:key outputs #:allow-other-keys)
+ (let* ((out (assoc-ref outputs "out"))
+ (java (string-append out "/share/java")))
+ (for-each (lambda (f) (install-file f java))
+ (find-files "dist" "\\.jar$"))))))))
+ (native-inputs (list java-junit))
+ (home-page "http://ultimate.informatik.uni-freiburg.de/smtinterpol/")
+ (synopsis "Interpolating SMT solver")
+ (description "SMTInterpol is an @acronym{SMT, Satisfiability Modulo Theories}
+solver, that can compute Craig interpolants for various theories.")
+ (license license:lgpl3+)))
+
+(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")
@@ -7557,6 +7863,85 @@ generic reader and writer API.")
(license (list license:expat
license:bsd-3)))) ; blif2aig
+(define-public btor2tools
+ (let ((commit "b8456dda4780789e882f5791eb486f295ade4da4")
+ (revision "1"))
+ (package
+ (name "btor2tools")
+ (version (git-version "1.0.0-pre" revision commit))
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/Boolector/btor2tools")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "0r3cm69q5xhnbxa74yvdfrsf349s4cxmiqlb4aq8appi7yg3qhww"))))
+ (build-system cmake-build-system)
+ (arguments
+ (list #:out-of-source? #f
+ #:phases
+ #~(modify-phases %standard-phases
+ (replace 'check
+ (lambda* (#:key tests? #:allow-other-keys)
+ (when tests?
+ (invoke "sh" "test/runtests.sh")))))))
+ (home-page "http://boolector.github.io/")
+ (synopsis "Parser for BTOR2 format")
+ (description "This package provides a parser for the BTOR2 format used by
+Boolector.")
+ (license license:lgpl3+))))
+
+(define-public cudd
+ (package
+ (name "cudd")
+ (version "3.0.0")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/ivmai/cudd")
+ (commit (string-append "cudd-" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "0hyw9q42ir92vcaa7bwv6f631n85rfsxp463rnmklniq1wf6dyn9"))))
+ (build-system gnu-build-system)
+ (arguments (list #:configure-flags #~(list "--enable-shared")))
+ ;; The original home-page was lost to time, so we reference the "unofficial"
+ ;; Github mirror. For what it's worth, the author of the library appears to
+ ;; have been involved with this mirror at some point in time.
+ (home-page "https://github.com/ivmai/cudd")
+ (synopsis "Manipulate decision diagrams")
+ (description "@acronym{CUDD, Colorado University Decision Diagrams} is a
+library for manipulating decision diagrams. It supports binary decision
+diagrams, algebraic decision diagrams, and zero-suppressed binary decision
+diagrams.")
+ (license license:bsd-3)))
+
+(define-public libpoly
+ (package
+ (name "libpoly")
+ (version "0.1.11")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/SRI-CSL/libpoly")
+ (commit (string-append "v" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "0qylmg30rklvg00a0h1b3pb52cj9ki98yd27cylihjhq2klh3dmy"))))
+ (build-system cmake-build-system)
+ (arguments
+ (list #:configure-flags #~(list "-DLIBPOLY_BUILD_PYTHON_API=off")))
+ (inputs (list gmp))
+ (home-page "https://github.com/SRI-CSL/libpoly")
+ (synopsis "Manipulate polynomials")
+ (description "LibPoly is a C library for manipulating polynomials to support
+symbolic reasoning engines that need to reason about polynomial constraints.")
+ (license license:lgpl3+)))
+
(define-public lingeling
(let ((commit "72d2b13eea5fbd95557a3d0d199cd98dfbdc76ee")
(revision "1"))
@@ -7893,7 +8278,7 @@ numeric differences and differences in numeric formats.")
(invoke "make" "byte")
(invoke "make" "install-lib")
#t)))))
- (home-page "http://why3.lri.fr")
+ (home-page "https://why3.lri.fr")
(synopsis "Deductive program verification")
(description "Why3 provides a language for specification and programming,
called WhyML, and relies on external theorem provers, both automated and
@@ -7946,7 +8331,7 @@ of C, Java, or Ada programs.")
(variable "FRAMAC_LIB")
(files '("lib/frama-c"))
(separator #f))))
- (home-page "http://frama-c.com")
+ (home-page "https://frama-c.com")
(synopsis "C source code analysis platform")
(description "Frama-C is an extensible and collaborative platform dedicated
to source-code analysis of C software. The Frama-C analyzers assist you in
generated by cgit v1.2.3 (git 2.44.0) at 2024-07-02 23:24:15 +0000