From f69a5ede640bba3faa2072c5c80e7961fb9da8cf Mon Sep 17 00:00:00 2001
From: Sören Tempel <soeren@soeren-tempel.net>
Date: Thu, 11 Jul 2024 23:27:16 +0200
Subject: gnu: Add python-pysmt.

* gnu/packages/patches/python-pysmt-fix-pow-return-type.patch:
New patch.
* gnu/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch:
New patch.
* gnu/local.mk (dist_patch_DATA): Add them.
* gnu/packages/python-xyz.scm (python-pysmt): New variable.

Signed-off-by: jgart <jgart@dismail.de>
---
 gnu/packages/python-xyz.scm | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)

(limited to 'gnu/packages/python-xyz.scm')

diff --git a/gnu/packages/python-xyz.scm b/gnu/packages/python-xyz.scm
index 8ffe795a69..a5db502364 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -33790,6 +33790,39 @@ instructions up to AVX-512 and SHA (including 3dnow!+, XOP, FMA3, FMA4, TBM
 and BMI2).")
       (license license:bsd-2))))
 
+(define-public python-pysmt
+  (package
+    (name "python-pysmt")
+    (version "0.9.5")
+    (source
+     (origin
+       ;; Fetching from Git as pypi release doesn't include all test files.
+       (method git-fetch)
+       (patches (search-patches "python-pysmt-fix-pow-return-type.patch"
+                 "python-pysmt-fix-smtlib-serialization-test.patch"))
+       (uri (git-reference
+             (url "https://github.com/pysmt/pysmt")
+             (commit (string-append "v" version))))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32 "0hrxv23y5ip4ijfx5pvbwc2fq4zg9jz42wc9zqgqm0g0mjc9ckvh"))))
+    (build-system pyproject-build-system)
+    (arguments
+     `(#:phases (modify-phases %standard-phases
+                  (add-before 'check 'set-pysmt-solver
+                    (lambda _
+                      (setenv "PYSMT_SOLVER" "z3"))))))
+    (native-inputs (list python-pytest))
+    (propagated-inputs (list z3))
+    (home-page "https://github.com/pysmt/pysmt")
+    (synopsis
+     "Solver-agnostic library for SMT formula manipulation and solving")
+    (description
+     "This Python module provides a solver-agnostic abstraction for
+working with @acronym{SMT, Satisfiability Modulo Theory} formulas.  For example,
+it allows manipulation and solving such formulas.")
+    (license license:asl2.0)))
+
 (define-public python-rpyc
   (package
     (name "python-rpyc")
-- 
cgit v1.2.3