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
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