ryan77627/guix
1
0
Fork 0
mirror of https://git.in.rschanz.org/ryan77627/guix.git synced 2025-01-13 14:40:21 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

gnu: Add lingeling.

Browse source 
* gnu/packages/maths.scm (lingeling): New variable.
This commit is contained in:
Liliana Marie Prikler 2022-10-15 16:45:44 +02:00
parent fc061ce297
commit 58c24ec748
No known key found for this signature in database
GPG key ID: 442A84B8C70E2F87
1 changed files with 82 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

82
gnu/packages/maths.scm
View file

@ -7416,6 +7416,88 @@ (define-public aiger
(license (list license:expat
license:bsd-3)))) ; blif2aig
(define-public lingeling
(let ((commit "72d2b13eea5fbd95557a3d0d199cd98dfbdc76ee")
(revision "1"))
(package
(name "lingeling")
(version (git-version "sc2022" revision commit))
(source (origin
(method git-fetch)
(uri (git-reference
(url "https://github.com/arminbiere/lingeling")
(commit commit)))
(file-name (git-file-name name version))
(sha256
(base32
"16s30x8s2cw6icchwm65zj56ph4qwz6i07g3hwkknvajisvjq85c"))))
(build-system gnu-build-system)
(arguments
(list #:test-target "test"
#:modules `((ice-9 match)
,@%gnu-build-system-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
'("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") 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))))
(define-public libqalculate
(package
(name "libqalculate")