Package: guix-patches;
Reported by: Liliana Marie Prikler <liliana.prikler <at> gmail.com>
Date: Sat, 25 Feb 2023 09:22:02 UTC
Severity: normal
Tags: patch
Done: Liliana Marie Prikler <liliana.prikler <at> gmail.com>
Bug is archived. No further changes may be made.
To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 61783 in the body.
You can then email your comments to 61783 AT debbugs.gnu.org in the normal way.
Toggle the display of automated, internal messages from the tracker.
View this report as an mbox folder, status mbox, maintainer mbox
guix-patches <at> gnu.org:bug#61783; Package guix-patches.
(Sat, 25 Feb 2023 09:22:02 GMT) Full text and rfc822 format available.Liliana Marie Prikler <liliana.prikler <at> gmail.com>:guix-patches <at> gnu.org.
(Sat, 25 Feb 2023 09:22:02 GMT) Full text and rfc822 format available.Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):
From: Liliana Marie Prikler <liliana.prikler <at> gmail.com> To: guix-patches <at> gnu.org Subject: [PATCH 0/6] Add more SMT solvers Date: Sat, 25 Feb 2023 09:58:44 +0100
Hi Guix, while z3 is nice and all, I thought it'd be better to have some competition. So here it is. Cheers Liliana Marie Prikler (6): gnu: Add cudd. gnu: Add libpoly. gnu: Add yices. gnu: Add btor2tools. gnu: Add boolector. gnu: Add java-smtinterpol. gnu/local.mk | 1 + gnu/packages/maths.scm | 254 +++++++++++++++++- .../patches/boolector-find-googletest.patch | 204 ++++++++++++++ 3 files changed, 458 insertions(+), 1 deletion(-) create mode 100644 gnu/packages/patches/boolector-find-googletest.patch base-commit: ea2fa86f31a83195ac789a6d92bcaee8e53e4397 -- 2.39.1
guix-patches <at> gnu.org:bug#61783; Package guix-patches.
(Sat, 25 Feb 2023 09:58:01 GMT) Full text and rfc822 format available.Message #8 received at 61783 <at> debbugs.gnu.org (full text, mbox):
From: Liliana Marie Prikler <liliana.prikler <at> gmail.com> To: 61783 <at> debbugs.gnu.org Subject: [PATCH 2/6] gnu: Add libpoly. Date: Sat, 25 Feb 2023 09:24:33 +0100
* gnu/packages/maths.scm (libpoly): New variable.
---
gnu/packages/maths.scm | 23 +++++++++++++++++++++++
1 file changed, 23 insertions(+)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 608545dda9..f9b050ddcb 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -7580,6 +7580,29 @@ (define-public cudd
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"))
--
2.39.1
guix-patches <at> gnu.org:bug#61783; Package guix-patches.
(Sat, 25 Feb 2023 09:58:02 GMT) Full text and rfc822 format available.Message #11 received at 61783 <at> debbugs.gnu.org (full text, mbox):
From: Liliana Marie Prikler <liliana.prikler <at> gmail.com> To: 61783 <at> debbugs.gnu.org Subject: [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
guix-patches <at> gnu.org:bug#61783; Package guix-patches.
(Sat, 25 Feb 2023 09:58:02 GMT) Full text and rfc822 format available.Message #14 received at 61783 <at> debbugs.gnu.org (full text, mbox):
From: Liliana Marie Prikler <liliana.prikler <at> gmail.com> To: 61783 <at> debbugs.gnu.org Subject: [PATCH 4/6] gnu: Add btor2tools. Date: Sat, 25 Feb 2023 09:25:10 +0100
* gnu/packages/maths.scm (btor2tools): New variable.
---
gnu/packages/maths.scm | 30 ++++++++++++++++++++++++++++++
1 file changed, 30 insertions(+)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 069c2c07c2..507b7056a4 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -7607,6 +7607,36 @@ (define-public aiger
(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")
--
2.39.1
guix-patches <at> gnu.org:bug#61783; Package guix-patches.
(Sat, 25 Feb 2023 09:58:03 GMT) Full text and rfc822 format available.Message #17 received at 61783 <at> debbugs.gnu.org (full text, mbox):
From: Liliana Marie Prikler <liliana.prikler <at> gmail.com> To: 61783 <at> debbugs.gnu.org Subject: [PATCH 5/6] gnu: Add boolector. Date: Sat, 25 Feb 2023 09:25:34 +0100
* gnu/packages/patches/boolector-find-googletest: New file.
* gnu/local.mk (dist_patch_DATA): Register it here.
* gnu/packages/maths.scm (boolector): New variable.
---
gnu/local.mk | 1 +
gnu/packages/maths.scm | 54 +++++
.../patches/boolector-find-googletest.patch | 204 ++++++++++++++++++
3 files changed, 259 insertions(+)
create mode 100644 gnu/packages/patches/boolector-find-googletest.patch
diff --git a/gnu/local.mk b/gnu/local.mk
index 0838f66618..e1c5acfbc6 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -951,6 +951,7 @@ dist_patch_DATA = \
%D%/packages/patches/binutils-CVE-2021-45078.patch \
%D%/packages/patches/bloomberg-bde-cmake-module-path.patch \
%D%/packages/patches/bloomberg-bde-tools-fix-install-path.patch \
+ %D%/packages/patches/boolector-find-googletest.patch \
%D%/packages/patches/bpftrace-disable-bfd-disasm.patch \
%D%/packages/patches/breezy-fix-gio.patch \
%D%/packages/patches/byobu-writable-status.patch \
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 507b7056a4..28750e5f46 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -6081,6 +6081,60 @@ (define-public jacal
(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 @abbrev{SMT, satisfiability modulo theories}
+solver for the theories of fixed-size bit-vectors, arrays and uninterpreted
+functions.")
+ (license license:lgpl3+)))
+
(define-public yices
(package
(name "yices")
diff --git a/gnu/packages/patches/boolector-find-googletest.patch b/gnu/packages/patches/boolector-find-googletest.patch
new file mode 100644
index 0000000000..baa7c6cd96
--- /dev/null
+++ b/gnu/packages/patches/boolector-find-googletest.patch
@@ -0,0 +1,204 @@
+From 91533caf29a2c5b10b4912fd352e7af82c787598 Mon Sep 17 00:00:00 2001
+From: Aina Niemetz <aina.niemetz <at> gmail.com>
+Date: Wed, 16 Jun 2021 16:17:27 -0700
+Subject: [PATCH] Configure google test as external project.
+
+---
+ CMakeLists.txt | 7 ----
+ cmake/FindGoogleTest.cmake | 60 +++++++++++++++++++++++++++++++++
+ cmake/googletest-download.cmake | 28 ---------------
+ cmake/googletest.cmake | 41 ----------------------
+ test/CMakeLists.txt | 5 ++-
+ 5 files changed, 64 insertions(+), 77 deletions(-)
+ create mode 100644 cmake/FindGoogleTest.cmake
+ delete mode 100644 cmake/googletest-download.cmake
+ delete mode 100644 cmake/googletest.cmake
+
+diff --git a/CMakeLists.txt b/CMakeLists.txt
+index 38056ede6..d30475bcd 100644
+--- a/CMakeLists.txt
++++ b/CMakeLists.txt
+@@ -440,13 +440,6 @@ configure_file(
+ #-----------------------------------------------------------------------------#
+ # Regression tests
+
+-# Get and configure google test
+-include(cmake/googletest.cmake)
+-fetch_googletest(
+- ${PROJECT_SOURCE_DIR}/cmake
+- ${PROJECT_BINARY_DIR}/googletest
+- )
+-
+ enable_testing()
+
+ #-----------------------------------------------------------------------------#
+diff --git a/cmake/FindGoogleTest.cmake b/cmake/FindGoogleTest.cmake
+new file mode 100644
+index 000000000..c6eecd179
+--- /dev/null
++++ b/cmake/FindGoogleTest.cmake
+@@ -0,0 +1,60 @@
++# Boolector: Satisfiablity Modulo Theories (SMT) solver.
++#
++# Copyright (C) 2007-2021 by the authors listed in the AUTHORS file.
++#
++# This file is part of Boolector.
++# See COPYING for more information on using this software.
++#
++
++# Find GTest
++#
++# GTest_FOUND - Found GTest
++# GTest::GTest - GTest library
++
++find_package(GTest 1.10.0)
++
++if(NOT GTest_FOUND)
++ include(ExternalProject)
++
++ set(GTest_VERSION "1.10.0")
++
++ ExternalProject_Add(
++ GTest-EP
++ PREFIX "${CMAKE_BINARY_DIR}/deps"
++ URL https://github.com/google/googletest/archive/refs/tags/release-${GTest_VERSION}.tar.gz
++ URL_HASH SHA1=9c89be7df9c5e8cb0bc20b3c4b39bf7e82686770
++ DOWNLOAD_NAME gtest.tar.gz
++ CMAKE_ARGS
++ -DCMAKE_INSTALL_PREFIX=<INSTALL_DIR>
++ BUILD_COMMAND ${CMAKE_COMMAND} --build .
++ BUILD_BYPRODUCTS
++ <INSTALL_DIR>/lib/libgtest.a
++ <INSTALL_DIR>/lib/libgtest_main.a
++ LOG_DOWNLOAD ON
++ LOG_UPDATE ON
++ LOG_CONFIGURE ON
++ LOG_BUILD ON
++ LOG_INSTALL ON
++ LOG_OUTPUT_ON_FAILURE TRUE
++ )
++
++ set(GTest_INCLUDE_DIR "${CMAKE_BINARY_DIR}/deps/include/")
++ set(GTest_MAIN_LIBRARY "${CMAKE_BINARY_DIR}/deps/lib/libgtest_main.a")
++ set(GTest_LIBRARY "${CMAKE_BINARY_DIR}/deps/lib/libgtest.a")
++ file(MAKE_DIRECTORY "${GTest_INCLUDE_DIR}")
++
++ add_library(GTest::gtest_main STATIC IMPORTED GLOBAL)
++ set_target_properties(GTest::gtest_main
++ PROPERTIES
++ IMPORTED_LOCATION "${GTest_MAIN_LIBRARY}"
++ INTERFACE_INCLUDE_DIRECTORIES "${GTest_INCLUDE_DIR}"
++ INTERFACE_LINK_LIBRARIES "${GTest_LIBRARY}"
++ )
++ set(GTest_FOUND TRUE)
++ add_dependencies(GTest::gtest_main GTest-EP)
++ message(STATUS "Building GTest ${GTest_VERSION}: ${GTest_MAIN_LIBRARY}")
++
++ mark_as_advanced(GTest_FOUND)
++ mark_as_advanced(GTest_INCLUDE_DIR)
++ mark_as_advanced(GTest_LIBRARIES)
++endif()
+diff --git a/cmake/googletest-download.cmake b/cmake/googletest-download.cmake
+deleted file mode 100644
+index 8dca59539..000000000
+--- a/cmake/googletest-download.cmake
++++ /dev/null
+@@ -1,28 +0,0 @@
+-# Boolector: Satisfiablity Modulo Theories (SMT) solver.
+-#
+-# Copyright (C) 2007-2021 by the authors listed in the AUTHORS file.
+-#
+-# This file is part of Boolector.
+-# See COPYING for more information on using this software.
+-#
+-
+-# code copied from https://crascit.com/2015/07/25/cmake-gtest/
+-cmake_minimum_required(VERSION 3.5 FATAL_ERROR)
+-
+-project(googletest-download NONE)
+-
+-include(ExternalProject)
+-
+-ExternalProject_Add(
+- googletest
+- SOURCE_DIR "@GOOGLETEST_DOWNLOAD_ROOT@/googletest-src"
+- BINARY_DIR "@GOOGLETEST_DOWNLOAD_ROOT@/googletest-build"
+- GIT_REPOSITORY
+- https://github.com/google/googletest.git
+- GIT_TAG
+- release-1.10.0
+- CONFIGURE_COMMAND ""
+- BUILD_COMMAND ""
+- INSTALL_COMMAND ""
+- TEST_COMMAND ""
+- )
+diff --git a/cmake/googletest.cmake b/cmake/googletest.cmake
+deleted file mode 100644
+index af5a5bc36..000000000
+--- a/cmake/googletest.cmake
++++ /dev/null
+@@ -1,41 +0,0 @@
+-# Boolector: Satisfiablity Modulo Theories (SMT) solver.
+-#
+-# Copyright (C) 2007-2021 by the authors listed in the AUTHORS file.
+-#
+-# This file is part of Boolector.
+-# See COPYING for more information on using this software.
+-#
+-
+-# the following code to fetch googletest
+-# is inspired by and adapted after https://crascit.com/2015/07/25/cmake-gtest/
+-# download and unpack googletest at configure time
+-
+-macro(fetch_googletest _download_module_path _download_root)
+- set(GOOGLETEST_DOWNLOAD_ROOT ${_download_root})
+- configure_file(
+- ${_download_module_path}/googletest-download.cmake
+- ${_download_root}/CMakeLists.txt
+- @ONLY
+- )
+- unset(GOOGLETEST_DOWNLOAD_ROOT)
+-
+- execute_process(
+- COMMAND
+- "${CMAKE_COMMAND}" -G "${CMAKE_GENERATOR}" .
+- WORKING_DIRECTORY
+- ${_download_root}
+- )
+- execute_process(
+- COMMAND
+- "${CMAKE_COMMAND}" --build .
+- WORKING_DIRECTORY
+- ${_download_root}
+- )
+-
+- # adds the targers: gtest, gtest_main, gmock, gmock_main
+- add_subdirectory(
+- ${_download_root}/googletest-src
+- ${_download_root}/googletest-build
+- EXCLUDE_FROM_ALL
+- )
+-endmacro()
+diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
+index 13f87d5e0..f2e14fd81 100644
+--- a/test/CMakeLists.txt
++++ b/test/CMakeLists.txt
+@@ -5,6 +5,9 @@
+ # This file is part of Boolector.
+ # See COPYING for more information on using this software.
+ #
++
++find_package(GoogleTest REQUIRED)
++
+ set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin/tests)
+
+ set(test_names
+@@ -47,7 +50,7 @@ foreach(test ${test_names})
+ add_executable (test${test} test_${test}.cpp)
+ target_include_directories(test${test} PRIVATE ${PROJECT_SOURCE_DIR}/test/new_test)
+ target_link_libraries(test${test} boolector m)
+- target_link_libraries(test${test} gtest_main)
++ target_link_libraries(test${test} GTest::gtest_main)
+ set_target_properties(test${test} PROPERTIES OUTPUT_NAME test${test})
+ add_test(${test} ${CMAKE_BINARY_DIR}/bin/tests/test${test})
+ endforeach()
--
2.39.1
guix-patches <at> gnu.org:bug#61783; Package guix-patches.
(Sat, 25 Feb 2023 09:59:02 GMT) Full text and rfc822 format available.Message #20 received at 61783 <at> debbugs.gnu.org (full text, mbox):
From: Liliana Marie Prikler <liliana.prikler <at> gmail.com> To: 61783 <at> debbugs.gnu.org Subject: [PATCH 6/6] gnu: Add java-smtinterpol. Date: Sat, 25 Feb 2023 09:25:49 +0100
* gnu/packages/maths.scm (java-smtinterpol): New variable.
---
gnu/packages/maths.scm | 68 +++++++++++++++++++++++++++++++++++++++++-
1 file changed, 67 insertions(+), 1 deletion(-)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 28750e5f46..a7497f1d2f 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -87,6 +87,7 @@ (define-module (gnu packages maths)
#: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 glib-or-gtk)
#:use-module (guix build-system gnu)
@@ -6130,11 +6131,76 @@ (define-public boolector
(native-inputs (list googletest pkg-config python-wrapper))
(home-page "http://boolector.github.io/")
(synopsis "Bitvector-based theory solver")
- (description "Boolector is a @abbrev{SMT, satisfiability modulo theories}
+ (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")
--
2.39.1
guix-patches <at> gnu.org:bug#61783; Package guix-patches.
(Sat, 25 Feb 2023 09:59:02 GMT) Full text and rfc822 format available.Message #23 received at 61783 <at> debbugs.gnu.org (full text, mbox):
From: Liliana Marie Prikler <liliana.prikler <at> gmail.com> To: 61783 <at> debbugs.gnu.org Subject: [PATCH 1/6] gnu: Add cudd. Date: Sat, 25 Feb 2023 09:24:18 +0100
* gnu/packages/maths.scm (cudd): New variable.
---
gnu/packages/maths.scm | 28 +++++++++++++++++++++++++++-
1 file changed, 27 insertions(+), 1 deletion(-)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 280465e284..608545dda9 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -55,7 +55,7 @@
;;; Copyright © 2022 Philip McGrath <philip <at> philipmcgrath.com>
;;; Copyright © 2022 Marek Felšöci <marek <at> felsoci.sk>
;;; Copyright © 2022 vicvbcun <guix <at> ikherbers.com>
-;;; Copyright © 2022 Liliana Marie Prikler <liliana.prikler <at> gmail.com>
+;;; Copyright © 2022, 2023 Liliana Marie Prikler <liliana.prikler <at> gmail.com>
;;; Copyright © 2022 Maximilian Heisinger <mail <at> maxheisinger.at>
;;; Copyright © 2022 Akira Kyle <akira <at> akirakyle.com>
;;; Copyright © 2022 Roman Scherer <roman.scherer <at> burningswell.com>
@@ -7554,6 +7554,32 @@ (define-public aiger
(license (list license:expat
license:bsd-3)))) ; blif2aig
+(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 lingeling
(let ((commit "72d2b13eea5fbd95557a3d0d199cd98dfbdc76ee")
(revision "1"))
--
2.39.1
Liliana Marie Prikler <liliana.prikler <at> gmail.com>:Liliana Marie Prikler <liliana.prikler <at> gmail.com>:Message #28 received at 61783-done <at> debbugs.gnu.org (full text, mbox):
From: Liliana Marie Prikler <liliana.prikler <at> gmail.com> To: 61783-done <at> debbugs.gnu.org Subject: Re: [PATCH 0/6] Add more SMT solvers Date: Sun, 05 Mar 2023 09:49:09 +0100
Am Samstag, dem 25.02.2023 um 09:58 +0100 schrieb Liliana Marie Prikler: > Hi Guix, > > while z3 is nice and all, I thought it'd be better to have some > competition. So here it is. > > Cheers > > Liliana Marie Prikler (6): > gnu: Add cudd. > gnu: Add libpoly. > gnu: Add yices. > gnu: Add btor2tools. > gnu: Add boolector. > gnu: Add java-smtinterpol. Pushed.
Debbugs Internal Request <help-debbugs <at> gnu.org>
to internal_control <at> debbugs.gnu.org.
(Sun, 02 Apr 2023 11:24:10 GMT) Full text and rfc822 format available.
GNU bug tracking system
Copyright (C) 1999 Darren O. Benham,
1997,2003 nCipher Corporation Ltd,
1994-97 Ian Jackson.