gnu: Add stp

* gnu/packages/maths.scm (stp): New variable.

1 files changed, 29 insertions, 0 deletions

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 0d74a2a55c..e59a6ea7d7 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -6235,6 +6235,35 @@ functions.")
 solver, that can compute Craig interpolants for various theories.")
    (license license:lgpl3+)))
 
+(define-public stp
+  (package
+    (name "stp")
+    (version "2.3.3")
+    (source
+      (origin
+        (method git-fetch)
+        (uri (git-reference (url "https://github.com/stp/stp")
+                            (commit version)))
+        (file-name (git-file-name name version))
+        (sha256
+          (base32 "1yg2v4wmswh1sigk47drwsxyayr472mf4i47lqmlcgn9hhbx1q87"))))
+    (build-system cmake-build-system)
+    (native-inputs (list bison flex perl))
+    (inputs (list boost cryptominisat louvain-community minisat zlib))
+    (arguments
+      (list #:tests? #f ; FIXME: build Python interface
+            #:phases
+            #~(modify-phases %standard-phases
+                (add-before 'configure 'set-ldflags
+                  (lambda* (#:key outputs #:allow-other-keys)
+                    (setenv "LDFLAGS"
+                      (string-append
+                        "-Wl,-rpath=" (assoc-ref outputs "out") "/lib")))))))
+    (home-page "https://stp.github.io")
+    (synopsis "Efficient SMT solver for bitvectors")
+    (description "Simple Theorem Prover is a constraint solver (or SMT solver) aimed at solving constraints of bitvectors and arrays.  These types of constraints can be generated by program analysis tools, theorem provers, automated bug finders, cryptographic attack tools, intelligent fuzzers, model checkers, and by many other applications.")
+    (license license:expat)))
+
 (define-public yices
   (package
    (name "yices")