guix-more/more/packages/smt.scm

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
  #:use-module (more packages python))
28
29
(define-public z3-solver
30
  (package
31
    (name "z3-solver")
32
    (version "4.5.0")
33
    (source (origin
34
              (method url-fetch)
35
              (uri (string-append "https://github.com/Z3Prover/z3/archive/z3-"
36
                                  version ".tar.gz"))
37
              (sha256
38
               (base32
39
                "032a5lvji2liwmc25jv52bdrhimqflvqbpg77ccaq1jykhiivbmf"))
40
              (file-name (string-append name "-" version ".tar.gz"))))
41
    (build-system gnu-build-system)
42
    (arguments
43
     `(#:phases
44
       (modify-phases %standard-phases
45
         (delete 'configure)
46
         (add-before 'build 'generate-make
47
           (lambda _
48
             (system* "python" "scripts/mk_make.py")
49
             (chdir "build"))))
50
       #:test-target "test"
51
       #:make-flags
52
       (list (string-append "PREFIX=" (assoc-ref %outputs "out")))))
53
    (native-inputs
54
     `(("python" ,python-2)))
55
    (home-page "https://github.com/Z3Prover/z3")
56
    (synopsis "SMT solver library")
57
    (description "Z3 is a theorem prover from Microsoft Research.")
58
    (license license:expat)))
59
60
;; Not reproducible and tests fail.
61
(define-public python-z3-solver
62
  (package
63
    (inherit z3-solver)
64
    (name "python-z3-solver")
65
    (build-system python-build-system)
66
    (propagated-inputs
67
     `(("z3" ,z3-solver)))
68
    (arguments
69
     `(#:phases
70
       (modify-phases %standard-phases
71
         (add-before 'build 'prepare
72
           (lambda* (#:key inputs #:allow-other-keys)
73
             (system* "python" "scripts/mk_make.py")
74
             (copy-file "build/python/z3/z3core.py" "src/api/python/z3/z3core.py")
75
             (copy-file "build/python/z3/z3consts.py" "src/api/python/z3/z3consts.py")
76
             (chdir "src/api/python")
77
             (substitute* "z3/z3core.py"
78
               (("_dirs = \\[")
79
                (string-append "_dirs = ['" (assoc-ref inputs "z3")
80
                                            "/lib', ")))
81
             (substitute* "MANIFEST.in"
82
               ((".*") ""))
83
             (substitute* "setup.py"
84
               (("self.execute\\(.*") "\n")
85
               (("scripts=.*") "\n")))))))))
86
87
(define-public python2-z3-solver
88
  (package-with-python2 python-z3-solver))
89
 
90
(define-public python-claripy
91
  (package
92
    (name "python-claripy")
93
    (version "6.7.1.31")
94
    (source (origin
95
              (method url-fetch)
96
              (uri (pypi-uri "claripy" version))
97
              (sha256
98
               (base32
99
                "0jpnqggx40kfj9cc48aylxsaqy61isl2yb3agib8nqh9v4j1rwqa"))))
100
    (build-system python-build-system)
101
    (propagated-inputs
102
     `(("ana" ,python-ana)
103
       ("z3" ,python-z3-solver)))
104
    (home-page "https://github.com/angr/claripy")
105
    (synopsis "Claripy is a abstracted constraint-solving wrapper")
106
    (description "Claripy is a abstracted constraint-solving wrapper.")
107
    (license license:bsd-2)))
108
109
(define-public python2-claripy
110
  (package-with-python2 python-claripy))
111