svn commit: r504169 - in head/math: . boolector boolector/files

[Yuri Victorovich]

Author: yuri
Date: Fri Jun 14 07:37:00 2019
New Revision: 504169
URL: https://svnweb.freebsd.org/changeset/ports/504169

Log:
  New port: math/boolector: Satisfiability Modulo Theories (SMT) solver

Added:
  head/math/boolector/
  head/math/boolector/Makefile   (contents, props changed)
  head/math/boolector/distinfo   (contents, props changed)
  head/math/boolector/files/
  head/math/boolector/files/patch-CMakeLists.txt   (contents, props changed)
  head/math/boolector/files/patch-src_CMakeLists.txt   (contents, props changed)
  head/math/boolector/pkg-descr   (contents, props changed)
  head/math/boolector/pkg-plist   (contents, props changed)
Modified:
  head/math/Makefile

Modified: head/math/Makefile
==============================================================================
--- head/math/Makefile	Fri Jun 14 07:17:02 2019	(r504168)
+++ head/math/Makefile	Fri Jun 14 07:37:00 2019	(r504169)
@@ -148,6 +148,7 @@
     SUBDIR += blis
     SUBDIR += blitz++
     SUBDIR += blocksolve95
+    SUBDIR += boolector
     SUBDIR += bsdnt
     SUBDIR += btor2tools
     SUBDIR += cadabra2

Added: head/math/boolector/Makefile
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/boolector/Makefile	Fri Jun 14 07:37:00 2019	(r504169)
@@ -0,0 +1,30 @@
+# $FreeBSD$
+
+PORTNAME=	boolector
+DISTVERSION=	3.0.0-239
+DISTVERSIONSUFFIX=	-g0b4b8540
+CATEGORIES=	math
+
+MAINTAINER=	yuri at FreeBSD.org
+COMMENT=	Satisfiability Modulo Theories (SMT) solver
+
+LICENSE=	MIT
+LICENSE_FILE=	${WRKSRC}/COPYING
+
+BUILD_DEPENDS=	picosat>0:math/picosat
+LIB_DEPENDS=	libbtor2parser.so:math/btor2tools
+
+USES=		cmake:noninja # ninja fails to build tests
+USE_GITHUB=	yes
+GH_ACCOUNT=	Boolector
+
+CMAKE_ON=	BUILD_SHARED_LIBS
+
+do-test: # tests assume that python-3.6 is installed # some tests fail: https://github.com/Boolector/boolector/issues/53
+	@${REINPLACE_CMD} 's|#!/usr/bin/env python2|#!${LOCALBASE}/bin/python3.6|' ${WRKSRC}/contrib/btorcheckmodel.py
+	@cd ${BUILD_WRKSRC} && \
+		${SETENV} ${CONFIGURE_ENV} ${CMAKE_BIN} ${CMAKE_ARGS} -DBUILD_TESTING:BOOL=ON ${CMAKE_SOURCE_PATH} && \
+		${SETENV} ${MAKE_ENV} ${MAKE_CMD} ${MAKE_ARGS} ${ALL_TARGET} && \
+		${SETENV} ${MAKE_ENV} ${MAKE_CMD} ${MAKE_ARGS} test
+
+.include <bsd.port.mk>

Added: head/math/boolector/distinfo
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/boolector/distinfo	Fri Jun 14 07:37:00 2019	(r504169)
@@ -0,0 +1,3 @@
+TIMESTAMP = 1560489123
+SHA256 (Boolector-boolector-3.0.0-239-g0b4b8540_GH0.tar.gz) = f0de750314c8075f6adb9f88a72c7efb897e52d53dc06b41b9beceec0f163765
+SIZE (Boolector-boolector-3.0.0-239-g0b4b8540_GH0.tar.gz) = 1372029

Added: head/math/boolector/files/patch-CMakeLists.txt
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/boolector/files/patch-CMakeLists.txt	Fri Jun 14 07:37:00 2019	(r504169)
@@ -0,0 +1,18 @@
+--- CMakeLists.txt.orig	2019-05-30 02:33:58 UTC
++++ CMakeLists.txt
+@@ -402,11 +402,15 @@ configure_file(
+   ${CMAKE_CURRENT_BINARY_DIR}/src/btorconfig.h)
+ 
+ # Enable CTest
++if (BUILD_TESTING)
+ enable_testing()
++endif(BUILD_TESTING)
+ 
+ include_directories(src ${CMAKE_CURRENT_BINARY_DIR}/src)
+ add_subdirectory(src)
++if (BUILD_TESTING)
+ add_subdirectory(test)
++endif(BUILD_TESTING)
+ if(PYTHON)
+   add_subdirectory(src/api/python)
+ endif()

Added: head/math/boolector/files/patch-src_CMakeLists.txt
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/boolector/files/patch-src_CMakeLists.txt	Fri Jun 14 07:37:00 2019	(r504169)
@@ -0,0 +1,11 @@
+--- src/CMakeLists.txt.orig	2019-06-14 07:01:21 UTC
++++ src/CMakeLists.txt
+@@ -129,7 +129,7 @@ set_target_properties(boolector-bin
+   PROPERTIES
+     OUTPUT_NAME boolector
+     RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
+-if(NOT SHARED AND NOT APPLE)
++if(NOT SHARED AND NOT APPLE AND NOT ${CMAKE_SYSTEM_NAME} MATCHES "FreeBSD")
+   set_target_properties(boolector-bin
+     PROPERTIES
+       LINK_FLAGS "-static -Wl,--no-export-dynamic"

Added: head/math/boolector/pkg-descr
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/boolector/pkg-descr	Fri Jun 14 07:37:00 2019	(r504169)
@@ -0,0 +1,8 @@
+Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of
+fixed-size bit-vectors, arrays and uninterpreted functions. It supports the
+SMT-LIB logics BV, QF_ABV, QF_AUFBV, QF_BV and QF_UFBV. Boolector provides a
+rich C and Python API and supports incremental solving, both with the SMT-LIB
+commands push and pop, and as solving under assumptions. The documentation of
+its API can be found here.
+
+WWW: https://boolector.github.io/

Added: head/math/boolector/pkg-plist
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/boolector/pkg-plist	Fri Jun 14 07:37:00 2019	(r504169)
@@ -0,0 +1,9 @@
+bin/boolector
+bin/btormc
+include/boolector/boolector.h
+include/boolector/btortypes.h
+lib/cmake/Boolector/BoolectorConfig.cmake
+lib/cmake/Boolector/BoolectorConfigVersion.cmake
+lib/cmake/Boolector/BoolectorTargets-%%CMAKE_BUILD_TYPE%%.cmake
+lib/cmake/Boolector/BoolectorTargets.cmake
+lib/libboolector.a