* [bug#73551] [PATCH 1/8] gnu: scasp: Update to 1.1.4.
2024-09-29 9:16 [bug#73551] [PATCH 0/8] Update some SAT/ASP solvers Liliana Marie Prikler
@ 2024-09-25 19:03 ` Liliana Marie Prikler
2024-09-25 19:03 ` [bug#73551] [PATCH 2/8] gnu: kissat: Update to 4.0.1 Liliana Marie Prikler
` (7 subsequent siblings)
8 siblings, 0 replies; 10+ messages in thread
From: Liliana Marie Prikler @ 2024-09-25 19:03 UTC (permalink / raw)
To: 73551
* gnu/packages/maths.scm (scasp): Update to 1.1.4.
---
gnu/packages/maths.scm | 62 ++++++++++++++++++++----------------------
1 file changed, 30 insertions(+), 32 deletions(-)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 5f47d5e390..581608d94d 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -2912,39 +2912,37 @@ (define-public libflame
(license license:bsd-3))))
(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
+ (package
+ (name "scasp")
+ (version "1.1.4")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/SWI-Prolog/sCASP")
+ (commit (string-append "V" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "1m4fs1ywich9cwj55miqp5zxs7c1fw9wvy7lcj5rkrgcanks5qk4"))))
+ (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))))
+ (license license:asl2.0)))
(define-public ceres
(package
--
2.46.0
^ permalink raw reply related [flat|nested] 10+ messages in thread* [bug#73551] [PATCH 2/8] gnu: kissat: Update to 4.0.1.
2024-09-29 9:16 [bug#73551] [PATCH 0/8] Update some SAT/ASP solvers Liliana Marie Prikler
2024-09-25 19:03 ` [bug#73551] [PATCH 1/8] gnu: scasp: Update to 1.1.4 Liliana Marie Prikler
@ 2024-09-25 19:03 ` Liliana Marie Prikler
2024-09-25 19:55 ` [bug#73551] [PATCH 3/8] gnu: z3: Update to 4.13.0 Liliana Marie Prikler
` (6 subsequent siblings)
8 siblings, 0 replies; 10+ messages in thread
From: Liliana Marie Prikler @ 2024-09-25 19:03 UTC (permalink / raw)
To: 73551
* gnu/packages/maths.scm (kissat): Update to 4.0.1.
[#:phases]<patch-source>: Relax regexp to fix test.
---
gnu/packages/maths.scm | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 581608d94d..6163148366 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9023,7 +9023,7 @@ (define-public minisat
(define-public kissat
(package
(name "kissat")
- (version "3.0.0")
+ (version "4.0.1")
(source
(origin
(method git-fetch)
@@ -9033,7 +9033,7 @@ (define-public kissat
(file-name (git-file-name name version))
(sha256
(base32
- "04x4w760srbdi4zci0s747qxk717x5d2x59ixraxh5104s9nyn8b"))))
+ "0acg61cfcjg13if2i375cyl4xvwmabhfhi9z8pnw971046am6bzv"))))
(build-system gnu-build-system)
(inputs (list xz gzip lzip bzip2 p7zip))
(arguments
@@ -9058,7 +9058,7 @@ (define-public kissat
"bool found = true;"))
(substitute* "test/testmain.c"
;; SIGINT is ignored inside invoke.
- (("^SIGNAL\\(SIGINT\\)") ""))))
+ (("^[ \t]*SIGNAL[ \t]*\\(SIGINT\\)") ""))))
(replace 'configure
(lambda* (#:key configure-flags #:allow-other-keys)
;; The configure script does not support standard GNU options.
--
2.46.0
^ permalink raw reply related [flat|nested] 10+ messages in thread* [bug#73551] [PATCH 3/8] gnu: z3: Update to 4.13.0.
2024-09-29 9:16 [bug#73551] [PATCH 0/8] Update some SAT/ASP solvers Liliana Marie Prikler
2024-09-25 19:03 ` [bug#73551] [PATCH 1/8] gnu: scasp: Update to 1.1.4 Liliana Marie Prikler
2024-09-25 19:03 ` [bug#73551] [PATCH 2/8] gnu: kissat: Update to 4.0.1 Liliana Marie Prikler
@ 2024-09-25 19:55 ` Liliana Marie Prikler
2024-09-25 20:02 ` [bug#73551] [PATCH 4/8] gnu: lingeling: Update to 1.0.0 Liliana Marie Prikler
` (5 subsequent siblings)
8 siblings, 0 replies; 10+ messages in thread
From: Liliana Marie Prikler @ 2024-09-25 19:55 UTC (permalink / raw)
To: 73551
* gnu/packages/maths.scm (z3): Update to 4.13.0.
---
gnu/packages/maths.scm | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 6163148366..b6dae2a721 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -7666,7 +7666,7 @@ (define-public yices
(define-public z3
(package
(name "z3")
- (version "4.8.17")
+ (version "4.13.0")
(home-page "https://github.com/Z3Prover/z3")
(source (origin
(method git-fetch)
@@ -7675,7 +7675,7 @@ (define-public z3
(file-name (git-file-name name version))
(sha256
(base32
- "1vvb09q7w7zd29qc4qjysrrhyylszm1wf6azkff004ixwn026b05"))))
+ "0j46lckf3zgx2xjay7z6nvlgh47gisbbl4s3m5zn280a13fwz1ih"))))
(build-system cmake-build-system)
(arguments
(list
--
2.46.0
^ permalink raw reply related [flat|nested] 10+ messages in thread* [bug#73551] [PATCH 4/8] gnu: lingeling: Update to 1.0.0.
2024-09-29 9:16 [bug#73551] [PATCH 0/8] Update some SAT/ASP solvers Liliana Marie Prikler
` (2 preceding siblings ...)
2024-09-25 19:55 ` [bug#73551] [PATCH 3/8] gnu: z3: Update to 4.13.0 Liliana Marie Prikler
@ 2024-09-25 20:02 ` Liliana Marie Prikler
2024-09-29 9:00 ` [bug#73551] [PATCH 5/8] gnu: Add cadical Liliana Marie Prikler
` (4 subsequent siblings)
8 siblings, 0 replies; 10+ messages in thread
From: Liliana Marie Prikler @ 2024-09-25 20:02 UTC (permalink / raw)
To: 73551
* gnu/packages/maths.scm (lingeling): Update to 1.0.0.
[#:phases]<hard-code-commit>: Adjust accordingly.
---
gnu/packages/maths.scm | 132 ++++++++++++++++++++---------------------
1 file changed, 65 insertions(+), 67 deletions(-)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index b6dae2a721..ab989e6af6 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9211,86 +9211,84 @@ (define-public libpoly
(license license:lgpl3+)))
(define-public lingeling
- (let ((commit "72d2b13eea5fbd95557a3d0d199cd98dfbdc76ee")
- (revision "1"))
- (package
- (name "lingeling")
- (version (git-version "sc2022" revision commit))
- (source (origin
+ (package
+ (name "lingeling")
+ (version "1.0.0")
+ (source (origin
(method git-fetch)
(uri (git-reference
(url "https://github.com/arminbiere/lingeling")
- (commit commit)))
+ (commit (string-append "rel-" version))))
(file-name (git-file-name name version))
(sha256
(base32
- "16s30x8s2cw6icchwm65zj56ph4qwz6i07g3hwkknvajisvjq85c"))))
- (build-system gnu-build-system)
- (arguments
- (list #:test-target "test"
- #:modules `((ice-9 match)
- ,@%default-gnu-modules)
- #:configure-flags #~(list "--aiger=.")
- #:phases
- #~(modify-phases %standard-phases
- (add-after 'unpack 'unpack-aiger
- (lambda* (#:key inputs #:allow-other-keys)
- (invoke #$(ar-for-target) "x"
- (search-input-file inputs "lib/libaiger.a")
- "aiger.o")
- (copy-file
- (search-input-file inputs "include/aiger/aiger.h")
- "aiger.h")))
- (add-after 'unpack 'hard-code-commit
- (lambda _
- (substitute* "mkconfig.sh"
- (("`\\./getgitid`") #$commit))))
- (add-after 'unpack 'patch-source
- (lambda* (#:key inputs #:allow-other-keys)
- (substitute* (list "treengeling.c" "lgldimacs.c")
- (("\"(gunzip|xz|bzcat|7z)" all cmd)
- (string-append
- "\""
- (search-input-file inputs (string-append "bin/" cmd)))))))
- (replace 'configure
- (lambda* (#:key configure-flags #:allow-other-keys)
- (apply invoke "./configure.sh" configure-flags)))
- (replace 'install
- (lambda* (#:key outputs #:allow-other-keys)
- (let ((bin (string-append (assoc-ref outputs "out")
- "/bin")))
- (mkdir-p bin)
- (for-each
- (lambda (file)
- (install-file file bin))
- '("blimc" "ilingeling" "lglddtrace" "lglmbt"
- "lgluntrace" "lingeling" "plingeling"
- "treengeling")))))
- (add-after 'install 'wrap-path
- (lambda* (#:key outputs #:allow-other-keys)
- (with-directory-excursion (string-append
- (assoc-ref outputs "out")
- "/bin")
- (for-each
- (lambda (file)
- (wrap-program
- file
+ "0hszkhyni7jcw580f41rrrnwz42x56sqvd8zpcjdagvdiag76lc1"))))
+ (build-system gnu-build-system)
+ (arguments
+ (list #:test-target "test"
+ #:modules `((ice-9 match)
+ ,@%default-gnu-modules)
+ #:configure-flags #~(list "--aiger=.")
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'unpack 'unpack-aiger
+ (lambda* (#:key inputs #:allow-other-keys)
+ (invoke #$(ar-for-target) "x"
+ (search-input-file inputs "lib/libaiger.a")
+ "aiger.o")
+ (copy-file
+ (search-input-file inputs "include/aiger/aiger.h")
+ "aiger.h")))
+ (add-after 'unpack 'hard-code-commit
+ (lambda _
+ (substitute* "mkconfig.sh"
+ (("`\\./getgitid`") ""))))
+ (add-after 'unpack 'patch-source
+ (lambda* (#:key inputs #:allow-other-keys)
+ (substitute* (list "treengeling.c" "lgldimacs.c")
+ (("\"(gunzip|xz|bzcat|7z)" all cmd)
+ (string-append
+ "\""
+ (search-input-file inputs (string-append "bin/" cmd)))))))
+ (replace 'configure
+ (lambda* (#:key configure-flags #:allow-other-keys)
+ (apply invoke "./configure.sh" configure-flags)))
+ (replace 'install
+ (lambda* (#:key outputs #:allow-other-keys)
+ (let ((bin (string-append (assoc-ref outputs "out")
+ "/bin")))
+ (mkdir-p bin)
+ (for-each
+ (lambda (file)
+ (install-file file bin))
+ '("blimc" "ilingeling" "lglddtrace" "lglmbt"
+ "lgluntrace" "lingeling" "plingeling"
+ "treengeling")))))
+ (add-after 'install 'wrap-path
+ (lambda* (#:key outputs #:allow-other-keys)
+ (with-directory-excursion (string-append
+ (assoc-ref outputs "out")
+ "/bin")
+ (for-each
+ (lambda (file)
+ (wrap-program
+ file
'("PATH" suffix
#$(map (lambda (input)
(file-append (this-package-input input) "/bin"))
'("gzip" "bzip2" "xz" "p7zip")))))
- ;; These programs use sprintf on buffers with magic
- ;; values to construct commands (yes, eww), so we
- ;; can't easily substitute* them.
- '("lglddtrace" "lgluntrace" "lingeling" "plingeling"))))))))
- (inputs (list `(,aiger "static") bash-minimal gzip bzip2 xz p7zip))
- (home-page "http://fmv.jku.at/lingeling")
- (synopsis "SAT solver")
- (description "This package provides a range of SAT solvers, including
+ ;; These programs use sprintf on buffers with magic
+ ;; values to construct commands (yes, eww), so we
+ ;; can't easily substitute* them.
+ '("lglddtrace" "lgluntrace" "lingeling" "plingeling"))))))))
+ (inputs (list `(,aiger "static") bash-minimal gzip bzip2 xz p7zip))
+ (home-page "http://fmv.jku.at/lingeling")
+ (synopsis "SAT solver")
+ (description "This package provides a range of SAT solvers, including
the sequential @command{lingeling} and its parallel variants
@command{plingeling} and @command{treengeling}. A bounded model checker is
also included.")
- (license license:expat))))
+ (license license:expat)))
(define-public louvain-community
(let ((commit "8cc5382d4844af127b1c1257373740d7e6b76f1e")
--
2.46.0
^ permalink raw reply related [flat|nested] 10+ messages in thread* [bug#73551] [PATCH 5/8] gnu: Add cadical.
2024-09-29 9:16 [bug#73551] [PATCH 0/8] Update some SAT/ASP solvers Liliana Marie Prikler
` (3 preceding siblings ...)
2024-09-25 20:02 ` [bug#73551] [PATCH 4/8] gnu: lingeling: Update to 1.0.0 Liliana Marie Prikler
@ 2024-09-29 9:00 ` Liliana Marie Prikler
2024-09-29 9:04 ` [bug#73551] [PATCH 6/8] gnu: Add cadiback Liliana Marie Prikler
` (3 subsequent siblings)
8 siblings, 0 replies; 10+ messages in thread
From: Liliana Marie Prikler @ 2024-09-29 9:00 UTC (permalink / raw)
To: 73551
* gnu/packages/patches/cadical-add-shared-library.patch: New file.
* gnu/local.mk (dist_patch_DATA): Register it here.
* gnu/packages/maths.scm (cadical): New variable.
---
gnu/local.mk | 1 +
gnu/packages/maths.scm | 52 +++++++++++++++++++
.../patches/cadical-add-shared-library.patch | 49 +++++++++++++++++
3 files changed, 102 insertions(+)
create mode 100644 gnu/packages/patches/cadical-add-shared-library.patch
diff --git a/gnu/local.mk b/gnu/local.mk
index 49660d4b3e..3d39016609 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -1027,6 +1027,7 @@ dist_patch_DATA = \
%D%/packages/patches/breezy-fix-gio.patch \
%D%/packages/patches/byobu-writable-status.patch \
%D%/packages/patches/bubblewrap-fix-locale-in-tests.patch \
+ %D%/packages/patches/cadical-add-shared-library.patch \
%D%/packages/patches/calibre-no-updates-dialog.patch \
%D%/packages/patches/calibre-remove-test-sqlite.patch \
%D%/packages/patches/calibre-remove-test-unrar.patch \
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index ab989e6af6..23015bc86a 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9290,6 +9290,58 @@ (define-public lingeling
also included.")
(license license:expat)))
+(define-public cadical
+ (package
+ (name "cadical")
+ (version "2.0.0")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/arminbiere/cadical")
+ (commit (string-append "rel-" version))))
+ (file-name (git-file-name name version))
+ (patches (search-patches "cadical-add-shared-library.patch"))
+ (sha256
+ (base32 "1dzjah3z34v89ka48hncwqkxrwl4xqn9947p0ipf39lxshrq91xa"))))
+ (build-system gnu-build-system)
+ (arguments
+ (list #:test-target "test"
+ #:modules `(((guix build copy-build-system) #:prefix copy:)
+ (guix build gnu-build-system)
+ (guix build utils)
+ (ice-9 regex))
+ #:imported-modules %copy-build-system-modules
+ #:phases
+ #~(modify-phases %standard-phases
+ (replace 'configure
+ (lambda* (#:key configure-flags #:allow-other-keys)
+ (setenv "CXXFLAGS" "-DPIC -fPIC")
+ (apply invoke "./configure" configure-flags)))
+ (replace 'check
+ (lambda args
+ ;; Tests are incorrectly linked upstream.
+ ;; Since we don't install them, just work around this in the
+ ;; check phase.
+ (setenv "LD_LIBRARY_PATH" (string-append (getcwd) "/build"))
+ (apply (assoc-ref %standard-phases 'check) args)
+ (unsetenv "LD_LIBRARY_PATH")))
+ (replace 'install
+ (lambda args
+ (apply
+ (assoc-ref copy:%standard-phases 'install)
+ #:install-plan
+ `(("build" "bin" #:include ("cadical" "mobical"))
+ ("build" "lib" #:include-regexp ("libcadical\\.(a|so)$"))
+ ("src" "include" #:include ("cadical.h"))
+ ;; Internal headers used by cadiback.
+ ("src" "include/cadical" #:include-regexp ("\\.hpp$")))
+ args))))))
+ (home-page "https://github.com/arminbiere/cadical")
+ (synopsis "SAT solver")
+ (description "This package provides a SAT solver based on conflict-driven
+clause learning.")
+ (license license:expat)))
+
(define-public louvain-community
(let ((commit "8cc5382d4844af127b1c1257373740d7e6b76f1e")
(revision "1"))
diff --git a/gnu/packages/patches/cadical-add-shared-library.patch b/gnu/packages/patches/cadical-add-shared-library.patch
new file mode 100644
index 0000000000..a1ae786d13
--- /dev/null
+++ b/gnu/packages/patches/cadical-add-shared-library.patch
@@ -0,0 +1,49 @@
+From fcb865786b524917aa9d3df8745aca66716794bf Mon Sep 17 00:00:00 2001
+From: Mate Soos <soos.mate@gmail.com>
+Date: Sun, 2 Jun 2024 21:50:06 -0400
+Subject: [PATCH] Also add a dynamic library
+
+---
+Liliana Marie Prikler <liliana.prikler@gmail.com>:
+ Added -L.
+ Squashed fix for cadical and mobical.
+
+ makefile.in | 5 ++++-
+ 1 file changed, 4 insertions(+), 1 deletion(-)
+
+diff --git a/makefile.in b/makefile.in
+index 291cb3e3..d179f591 100644
+--- a/makefile.in
++++ b/makefile.in
+@@ -34,7 +34,7 @@ COMPILE=$(CXX) $(CXXFLAGS) -I$(DIR) -I$(ROOT)/src
+
+ #--------------------------------------------------------------------------#
+
+-all: libcadical.a cadical mobical
++all: libcadical.so libcadical.a cadical mobical
+
+ #--------------------------------------------------------------------------#
+
+@@ -54,10 +54,10 @@ contrib/%.o: $(ROOT)/contrib/%.cpp $(ROOT)/contrib/%.hpp $(ROOT)/src/*.hpp makef
+ # tester 'mobical') and the library are the main build targets.
+
+ cadical: src/cadical.o libcadical.a makefile
+- $(COMPILE) -o $@ $< -L. -lcadical $(LIBS)
++ $(COMPILE) -static -o $@ $< -L. -lcadical $(LIBS)
+
+ mobical: src/mobical.o libcadical.a makefile $(LIBS)
+- $(COMPILE) -o $@ $< -L. -lcadical
++ $(COMPILE) -static -o $@ $< -L. -lcadical
+
+ libcadical.a: $(OBJ_SOLVER) $(OBJ_CONTRIB) makefile
+ ar rc $@ $(OBJ_SOLVER) $(OBJ_CONTRIB)
+@@ -62,5 +62,8 @@ mobical: src/mobical.o libcadical.a makefile $(LIBS)
+ libcadical.a: $(OBJ_SOLVER) $(OBJ_CONTRIB) makefile
+ ar rc $@ $(OBJ_SOLVER) $(OBJ_CONTRIB)
+
++libcadical.so: $(OBJ_SOLVER) $(OBJ_CONTRIB) $(LIBS) makefile
++ $(COMPILE) -shared -o $@ $(OBJ_SOLVER) $(OBJ_CONTRIB) $(LIBS)
++
+ #--------------------------------------------------------------------------#
+
+ # Note that 'build.hpp' is generated and resides in the build directory.
\ No newline at end of file
--
2.46.0
^ permalink raw reply related [flat|nested] 10+ messages in thread* [bug#73551] [PATCH 6/8] gnu: Add cadiback.
2024-09-29 9:16 [bug#73551] [PATCH 0/8] Update some SAT/ASP solvers Liliana Marie Prikler
` (4 preceding siblings ...)
2024-09-29 9:00 ` [bug#73551] [PATCH 5/8] gnu: Add cadical Liliana Marie Prikler
@ 2024-09-29 9:04 ` Liliana Marie Prikler
2024-09-29 9:04 ` [bug#73551] [PATCH 7/8] gnu: Add cadiback-for-cryptominisat Liliana Marie Prikler
` (2 subsequent siblings)
8 siblings, 0 replies; 10+ messages in thread
From: Liliana Marie Prikler @ 2024-09-29 9:04 UTC (permalink / raw)
To: 73551
* gnu/packages/maths.scm (cadiback): New variable.
---
gnu/packages/maths.scm | 58 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 58 insertions(+)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 23015bc86a..a8ae1c73a0 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9342,6 +9342,64 @@ (define-public cadical
clause learning.")
(license license:expat)))
+(define-public cadiback
+ (let ((commit "789329d8fcda851085ed72f1b07d8c3f46243b8a")
+ (revision "1"))
+ (package
+ (name "cadiback")
+ ;; Note: version taken from VERSION file
+ (version (git-version "0.2.1" revision commit))
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/arminbiere/cadiback")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "137jxf9g7c1979pcgcqgfff1mqk5hs41a84780px8gpcrh469cks"))))
+ (build-system gnu-build-system)
+ (arguments
+ (list #:test-target "test"
+ #:modules `(((guix build copy-build-system) #:prefix copy:)
+ (guix build gnu-build-system)
+ (guix build utils)
+ (ice-9 regex))
+ #:imported-modules %copy-build-system-modules
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'unpack 'patch-build-files
+ (lambda* (#:key inputs #:allow-other-keys)
+ (substitute* "configure"
+ (("\\$CADICAL/src") "$CADICAL/include/cadical")
+ (("\\$CADICAL/build") "$CADICAL/lib"))
+ (substitute* "generate"
+ (("\\[ -d .git \\]" all) (string-append ": " all))
+ (("GITID=.*") (string-append "GITID=\"" #$commit "\"")))
+ (substitute* "makefile.in"
+ (("\\.\\./cadical/build")
+ (dirname
+ (search-input-file inputs "lib/libcadical.a")))
+ (("\\.\\./cadical/src")
+ (search-input-directory inputs "include/cadical")))))
+ (replace 'configure
+ (lambda* (#:key configure-flags #:allow-other-keys)
+ (setenv "CADICAL" #$(this-package-input "cadical"))
+ (apply invoke "./configure" configure-flags)))
+ (replace 'install
+ (lambda args
+ (apply
+ (assoc-ref copy:%standard-phases 'install)
+ #:install-plan
+ `(("." "bin" #:include ("cadiback")))
+ args))))))
+ (inputs (list cadical))
+ (home-page "https://github.com/arminbiere/cadiback")
+ (synopsis "Backbone extractor for cadical")
+ (description "This package provides a tool to determine the backbone of
+a satisfiable formula. The backbone is the set of literals that are set to
+true in all models.")
+ (license license:expat))))
+
(define-public louvain-community
(let ((commit "8cc5382d4844af127b1c1257373740d7e6b76f1e")
(revision "1"))
--
2.46.0
^ permalink raw reply related [flat|nested] 10+ messages in thread* [bug#73551] [PATCH 7/8] gnu: Add cadiback-for-cryptominisat.
2024-09-29 9:16 [bug#73551] [PATCH 0/8] Update some SAT/ASP solvers Liliana Marie Prikler
` (5 preceding siblings ...)
2024-09-29 9:04 ` [bug#73551] [PATCH 6/8] gnu: Add cadiback Liliana Marie Prikler
@ 2024-09-29 9:04 ` Liliana Marie Prikler
2024-09-29 9:08 ` [bug#73551] [PATCH 8/8] gnu: cryptominisat: Update to 5.11.22 Liliana Marie Prikler
2024-10-06 14:19 ` bug#73551: [PATCH 0/8] Update some SAT/ASP solvers Liliana Marie Prikler
8 siblings, 0 replies; 10+ messages in thread
From: Liliana Marie Prikler @ 2024-09-29 9:04 UTC (permalink / raw)
To: 73551
* gnu/packages/maths.scm (cadiback-for-cryptominisat): New variable.
---
gnu/packages/maths.scm | 29 +++++++++++++++++++++++++++++
1 file changed, 29 insertions(+)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index a8ae1c73a0..e84a87db97 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9400,6 +9400,35 @@ (define-public cadiback
true in all models.")
(license license:expat))))
+(define cadiback-for-cryptominisat
+ (let ((commit "ea65a9442fc2604ee5f4ffd0f0fdd0bf481d5b42")
+ (revision "1"))
+ (package
+ (inherit cadiback)
+ (name "cadiback-for-cryptominisat")
+ (version (git-version "0.2.1" revision commit))
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/meelgroup/cadiback")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "1zznrlj4zp1mc7s4pfw11aq773q2lr9yl6pph630zg5mqijaim5g"))))
+ (arguments
+ (substitute-keyword-arguments (package-arguments cadiback)
+ ((#:phases phases)
+ #~(modify-phases #$phases
+ (add-after 'patch-build-files 'fix-prefix
+ (lambda _
+ (substitute* "makefile.in"
+ (("/usr") #$output))))
+ (replace 'install
+ (lambda args
+ (mkdir-p (string-append #$output "/include"))
+ (mkdir-p (string-append #$output "/lib"))
+ (apply (assoc-ref %standard-phases 'install) args))))))))))
+
(define-public louvain-community
(let ((commit "8cc5382d4844af127b1c1257373740d7e6b76f1e")
(revision "1"))
--
2.46.0
^ permalink raw reply related [flat|nested] 10+ messages in thread* [bug#73551] [PATCH 8/8] gnu: cryptominisat: Update to 5.11.22.
2024-09-29 9:16 [bug#73551] [PATCH 0/8] Update some SAT/ASP solvers Liliana Marie Prikler
` (6 preceding siblings ...)
2024-09-29 9:04 ` [bug#73551] [PATCH 7/8] gnu: Add cadiback-for-cryptominisat Liliana Marie Prikler
@ 2024-09-29 9:08 ` Liliana Marie Prikler
2024-10-06 14:19 ` bug#73551: [PATCH 0/8] Update some SAT/ASP solvers Liliana Marie Prikler
8 siblings, 0 replies; 10+ messages in thread
From: Liliana Marie Prikler @ 2024-09-29 9:08 UTC (permalink / raw)
To: 73551
* gnu/packages/maths.scm (cryptominisat): Update to 5.11.22.
[source]: Patch include for cadiback.
[inputs]: Add cadical, cadiback-for-cryptominisat and gmp.
---
gnu/packages/maths.scm | 19 ++++++++++++++++---
1 file changed, 16 insertions(+), 3 deletions(-)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index e84a87db97..e809c62e18 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9463,7 +9463,7 @@ (define-public louvain-community
(define-public cryptominisat
(package
(name "cryptominisat")
- (version "5.11.4")
+ (version "5.11.22")
(source
(origin
(method git-fetch)
@@ -9473,7 +9473,12 @@ (define-public cryptominisat
(file-name (git-file-name name version))
(sha256
(base32
- "1izjn44phjp9670s7bxrdx4p0r59idqwv3bm6sr0qnlqlha5z4zc"))))
+ "1c85gfqvy90yhh9jwmiiz2bz4i86prgpfyx1gbzl42hn2ixkcjgm"))
+ (modules '((guix build utils)))
+ (snippet
+ #~(begin
+ (substitute* "src/backbone.cpp"
+ (("\"\\.\\./cadiback/cadiback\\.h\"") "<cadiback.h>"))))))
(build-system cmake-build-system)
(arguments
(list
@@ -9497,7 +9502,15 @@ (define-public cryptominisat
"find_package(GTest REQUIRED)")
(("add_subdirectory\\(\\$\\{PROJECT_SOURCE_DIR\\}/utils/.*\\)")
"")))))))
- (inputs (list boost louvain-community python python-numpy sqlite zlib))
+ (inputs (list boost
+ cadical
+ cadiback-for-cryptominisat
+ gmp
+ louvain-community
+ python
+ python-numpy
+ sqlite
+ zlib))
(native-inputs (list googletest lingeling python python-wrapper python-lit))
(synopsis "Incremental SAT solver")
(description
--
2.46.0
^ permalink raw reply related [flat|nested] 10+ messages in thread* bug#73551: [PATCH 0/8] Update some SAT/ASP solvers
2024-09-29 9:16 [bug#73551] [PATCH 0/8] Update some SAT/ASP solvers Liliana Marie Prikler
` (7 preceding siblings ...)
2024-09-29 9:08 ` [bug#73551] [PATCH 8/8] gnu: cryptominisat: Update to 5.11.22 Liliana Marie Prikler
@ 2024-10-06 14:19 ` Liliana Marie Prikler
8 siblings, 0 replies; 10+ messages in thread
From: Liliana Marie Prikler @ 2024-10-06 14:19 UTC (permalink / raw)
To: 73551-done
Am Sonntag, dem 29.09.2024 um 11:16 +0200 schrieb Liliana Marie
Prikler:
> Liliana Marie Prikler (8):
> gnu: scasp: Update to 1.1.4.
> gnu: kissat: Update to 4.0.1.
> gnu: z3: Update to 4.13.0.
> gnu: lingeling: Update to 1.0.0.
> gnu: Add cadical.
> gnu: Add cadiback.
> gnu: Add cadiback-for-cryptominisat.
> gnu: cryptominisat: Update to 5.11.22.
Done and pushed.
^ permalink raw reply [flat|nested] 10+ messages in thread