svn commit: r527904 - in head/math: . py-PySMT

[Mateusz Piotrowski]

Author: 0mp
Date: Fri Mar  6 23:41:39 2020
New Revision: 527904
URL: https://svnweb.freebsd.org/changeset/ports/527904

Log:
  New port: math/py-PySMT
  
  pySMT is a library for SMT formulae manipulation and solving, which makes
  working with Satisfiability Modulo Theory simple.
  
  Among others, the user can:
  
  - Define formulae in a solver independent way in a simple and inutitive
    way,
  - Write ad-hoc simplifiers and operators,
  - Dump your problems in the SMT-Lib format,
  - Solve them using one of the native solvers, or by wrapping any SMT-Lib
    complaint solver.
  
  pySMT provides methods to define a formula in Linear Real Arithmetic (LRA),
  Real Difference Logic (RDL), their combination (LIRA), Equalities and
  Uninterpreted Functions (EUF), Bit-Vectors (BV), and Arrays (A). The
  following solvers are supported through native APIs: MathSAT, Z3, CVC4,
  Yices, CUDD, PicoSAT, and Boolector. Additionally, you can use any SMT-LIB
  2 compliant solver.
  
  PySMT assumes that the python bindings for the SMT Solver are installed and
  accessible from your PYTHONPATH.
  
  WWW: http://www.pysmt.org
  
  PR:		244562

Added:
  head/math/py-PySMT/
  head/math/py-PySMT/Makefile   (contents, props changed)
  head/math/py-PySMT/distinfo   (contents, props changed)
  head/math/py-PySMT/pkg-descr   (contents, props changed)
Modified:
  head/math/Makefile

Modified: head/math/Makefile
==============================================================================
--- head/math/Makefile	Fri Mar  6 23:29:20 2020	(r527903)
+++ head/math/Makefile	Fri Mar  6 23:41:39 2020	(r527904)
@@ -685,6 +685,7 @@
     SUBDIR += py-PuLP
     SUBDIR += py-PyMetis
     SUBDIR += py-PySCIPOpt
+    SUBDIR += py-PySMT
     SUBDIR += py-PyWavelets
     SUBDIR += py-Pyomo
     SUBDIR += py-algopy

Added: head/math/py-PySMT/Makefile
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/py-PySMT/Makefile	Fri Mar  6 23:41:39 2020	(r527904)
@@ -0,0 +1,30 @@
+# $FreeBSD$
+
+PORTNAME=	PySMT
+DISTVERSIONPREFIX=	v
+DISTVERSION=	0.8.0
+CATEGORIES=	math python
+PKGNAMEPREFIX=	${PYTHON_PKGNAMEPREFIX}
+
+MAINTAINER=	0mp at FreeBSD.org
+COMMENT=	Solver-agnostic library for SMT formulae manipulation and solving
+
+LICENSE=	APACHE20
+LICENSE_FILE=	${WRKSRC}/LICENSE
+
+RUN_DEPENDS=	${PYTHON_PKGNAMEPREFIX}six>=0:devel/py-six@${PY_FLAVOR}
+TEST_DEPENDS=	${PYTHON_PKGNAMEPREFIX}nose>0:devel/py-nose@${PY_FLAVOR}
+
+# Supported Python versions: 2.7,3.5+
+USES=		python
+USE_GITHUB=	yes
+GH_ACCOUNT=	pysmt
+GH_PROJECT=	pysmt
+USE_PYTHON=	autoplist concurrent distutils
+
+NO_ARCH=	yes
+
+do-test:
+	@(cd ${TEST_WRKSRC} && ${SETENV} ${TEST_ENV} nosetests-${PYTHON_VER} -v)
+
+.include <bsd.port.mk>

Added: head/math/py-PySMT/distinfo
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/py-PySMT/distinfo	Fri Mar  6 23:41:39 2020	(r527904)
@@ -0,0 +1,3 @@
+TIMESTAMP = 1583537787
+SHA256 (pysmt-pysmt-v0.8.0_GH0.tar.gz) = 6a1f2ea69e97c9cecb43f9c5b3c5d786568cb26a3ebabe8c2b4e0acbd1870b94
+SIZE (pysmt-pysmt-v0.8.0_GH0.tar.gz) = 1129930

Added: head/math/py-PySMT/pkg-descr
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/py-PySMT/pkg-descr	Fri Mar  6 23:41:39 2020	(r527904)
@@ -0,0 +1,22 @@
+pySMT is a library for SMT formulae manipulation and solving, which makes
+working with Satisfiability Modulo Theory simple.
+
+Among others, the user can:
+
+- Define formulae in a solver independent way in a simple and inutitive way,
+- Write ad-hoc simplifiers and operators,
+- Dump your problems in the SMT-Lib format,
+- Solve them using one of the native solvers, or by wrapping any SMT-Lib
+  complaint solver.
+
+pySMT provides methods to define a formula in Linear Real Arithmetic (LRA),
+Real Difference Logic (RDL), their combination (LIRA), Equalities and
+Uninterpreted Functions (EUF), Bit-Vectors (BV), and Arrays (A). The following
+solvers are supported through native APIs: MathSAT, Z3, CVC4, Yices, CUDD,
+PicoSAT, and Boolector. Additionally, you can use any SMT-LIB 2 compliant
+solver.
+
+PySMT assumes that the python bindings for the SMT Solver are installed and
+accessible from your PYTHONPATH.
+
+WWW: http://www.pysmt.org