GNU bug report logs - #61783
[PATCH 0/6] Add more SMT solvers

Previous Next

Full log

View this message in rfc822 format

From: Liliana Marie Prikler <liliana.prikler <at> gmail.com>
To: 61783 <at> debbugs.gnu.org
Subject: [bug#61783] [PATCH 2/6] gnu: Add libpoly.
Date: Sat, 25 Feb 2023 09:24:33 +0100

* gnu/packages/maths.scm (libpoly): New variable.
---
 gnu/packages/maths.scm | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 608545dda9..f9b050ddcb 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -7580,6 +7580,29 @@ (define-public cudd
 diagrams.")
    (license license:bsd-3)))
 
+(define-public libpoly
+  (package
+   (name "libpoly")
+   (version "0.1.11")
+   (source (origin
+            (method git-fetch)
+            (uri (git-reference
+                  (url "https://github.com/SRI-CSL/libpoly")
+                  (commit (string-append "v" version))))
+            (file-name (git-file-name name version))
+            (sha256
+             (base32
+              "0qylmg30rklvg00a0h1b3pb52cj9ki98yd27cylihjhq2klh3dmy"))))
+   (build-system cmake-build-system)
+   (arguments
+    (list #:configure-flags #~(list "-DLIBPOLY_BUILD_PYTHON_API=off")))
+   (inputs (list gmp))
+   (home-page "https://github.com/SRI-CSL/libpoly")
+   (synopsis "Manipulate polynomials")
+   (description "LibPoly is a C library for manipulating polynomials to support
+symbolic reasoning engines that need to reason about polynomial constraints.")
+   (license license:lgpl3+)))
+
 (define-public lingeling
   (let ((commit "72d2b13eea5fbd95557a3d0d199cd98dfbdc76ee")
         (revision "1"))
-- 
2.39.1

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.