From 3475c110b4c9fe38650fc689de4a7c3068edaad1 Mon Sep 17 00:00:00 2001 From: Nguyễn Gia Phong Date: Mon, 3 Jul 2023 19:48:40 +0900 Subject: gnu: Add stp * gnu/packages/maths.scm (stp): New variable. --- gnu/packages/maths.scm | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) 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") -- cgit 1.4.1