smt.scm
1 | ;;; GNU Guix --- Functional package management for GNU |
2 | ;;; Copyright © 2017 Julien Lepiller <julien@lepiller.eu> |
3 | ;;; |
4 | ;;; This file is part of GNU Guix. |
5 | ;;; |
6 | ;;; GNU Guix is free software; you can redistribute it and/or modify it |
7 | ;;; under the terms of the GNU General Public License as published by |
8 | ;;; the Free Software Foundation; either version 3 of the License, or (at |
9 | ;;; your option) any later version. |
10 | ;;; |
11 | ;;; GNU Guix is distributed in the hope that it will be useful, but |
12 | ;;; WITHOUT ANY WARRANTY; without even the implied warranty of |
13 | ;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
14 | ;;; GNU General Public License for more details. |
15 | ;;; |
16 | ;;; You should have received a copy of the GNU General Public License |
17 | ;;; along with GNU Guix. If not, see <http://www.gnu.org/licenses/>. |
18 | |
19 | (define-module (more packages smt) |
20 | #:use-module (guix packages) |
21 | #:use-module (guix download) |
22 | #:use-module (guix build-system gnu) |
23 | #:use-module (guix build-system python) |
24 | #:use-module ((guix licenses) #:prefix license:) |
25 | #:use-module (gnu packages) |
26 | #:use-module (gnu packages python)) |
27 | |
28 | (define-public z3-solver |
29 | (package |
30 | (name "z3-solver") |
31 | (version "4.5.0") |
32 | (source (origin |
33 | (method url-fetch) |
34 | (uri (string-append "https://github.com/Z3Prover/z3/archive/z3-" |
35 | version ".tar.gz")) |
36 | (sha256 |
37 | (base32 |
38 | "032a5lvji2liwmc25jv52bdrhimqflvqbpg77ccaq1jykhiivbmf")) |
39 | (file-name (string-append name "-" version ".tar.gz")))) |
40 | (build-system gnu-build-system) |
41 | (arguments |
42 | `(#:phases |
43 | (modify-phases %standard-phases |
44 | (delete 'configure) |
45 | (add-before 'build 'generate-make |
46 | (lambda _ |
47 | (system* "python" "scripts/mk_make.py") |
48 | (chdir "build")))) |
49 | #:test-target "test" |
50 | #:make-flags |
51 | (list (string-append "PREFIX=" (assoc-ref %outputs "out"))))) |
52 | (native-inputs |
53 | `(("python" ,python-2))) |
54 | (home-page "https://github.com/Z3Prover/z3") |
55 | (synopsis "SMT solver library") |
56 | (description "Z3 is a theorem prover from Microsoft Research.") |
57 | (license license:expat))) |
58 | |
59 | ;; Not reproducible and tests fail. |
60 | (define-public python-z3-solver |
61 | (package |
62 | (inherit z3-solver) |
63 | (name "python-z3-solver") |
64 | (build-system python-build-system) |
65 | (propagated-inputs |
66 | `(("z3" ,z3-solver))) |
67 | (arguments |
68 | `(#:phases |
69 | (modify-phases %standard-phases |
70 | (add-before 'build 'prepare |
71 | (lambda* (#:key inputs #:allow-other-keys) |
72 | (system* "python" "scripts/mk_make.py") |
73 | (copy-file "build/python/z3/z3core.py" "src/api/python/z3/z3core.py") |
74 | (copy-file "build/python/z3/z3consts.py" "src/api/python/z3/z3consts.py") |
75 | (chdir "src/api/python") |
76 | (substitute* "z3/z3core.py" |
77 | (("_dirs = \\[") |
78 | (string-append "_dirs = ['" (assoc-ref inputs "z3") |
79 | "/lib', "))) |
80 | (substitute* "MANIFEST.in" |
81 | ((".*") "")) |
82 | (substitute* "setup.py" |
83 | (("self.execute\\(.*") "\n") |
84 | (("scripts=.*") "\n"))))))))) |
85 | |
86 | (define-public python2-z3-solver |
87 | (package-with-python2 python-z3-solver)) |
88 | |
89 | (define-public python-claripy |
90 | (package |
91 | (name "python-claripy") |
92 | (version "6.7.1.13.post2") |
93 | (source (origin |
94 | (method url-fetch) |
95 | (uri (pypi-uri "claripy" version)) |
96 | (sha256 |
97 | (base32 |
98 | "0qcp6c7shyl4hs14yhnymcanr87i8hbp6af35avzphjq7jw33rrc")))) |
99 | (build-system python-build-system) |
100 | (propagated-inputs |
101 | `(("ana" ,python-ana))) |
102 | (home-page "https://github.com/angr/claripy") |
103 | (synopsis "Claripy is a abstracted constraint-solving wrapper") |
104 | (description "Claripy is a abstracted constraint-solving wrapper.") |
105 | (license license:bsd-2))) |
106 | |
107 | (define-public python2-claripy |
108 | (package-with-python2 python-claripy)) |
109 |