From owner-svn-ports-head@freebsd.org Fri Jun 14 07:37:02 2019 Return-Path: Delivered-To: svn-ports-head@mailman.ysv.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2610:1c1:1:606c::19:1]) by mailman.ysv.freebsd.org (Postfix) with ESMTP id 64F7E15C9222; Fri, 14 Jun 2019 07:37:02 +0000 (UTC) (envelope-from yuri@FreeBSD.org) Received: from mxrelay.nyi.freebsd.org (mxrelay.nyi.freebsd.org [IPv6:2610:1c1:1:606c::19:3]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) server-signature RSA-PSS (4096 bits) client-signature RSA-PSS (4096 bits) client-digest SHA256) (Client CN "mxrelay.nyi.freebsd.org", Issuer "Let's Encrypt Authority X3" (verified OK)) by mx1.freebsd.org (Postfix) with ESMTPS id 0A0DC87F46; Fri, 14 Jun 2019 07:37:02 +0000 (UTC) (envelope-from yuri@FreeBSD.org) Received: from repo.freebsd.org (repo.freebsd.org [IPv6:2610:1c1:1:6068::e6a:0]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by mxrelay.nyi.freebsd.org (Postfix) with ESMTPS id D7463CBEC; Fri, 14 Jun 2019 07:37:01 +0000 (UTC) (envelope-from yuri@FreeBSD.org) Received: from repo.freebsd.org ([127.0.1.37]) by repo.freebsd.org (8.15.2/8.15.2) with ESMTP id x5E7b1Bk092086; Fri, 14 Jun 2019 07:37:01 GMT (envelope-from yuri@FreeBSD.org) Received: (from yuri@localhost) by repo.freebsd.org (8.15.2/8.15.2/Submit) id x5E7b0eY092080; Fri, 14 Jun 2019 07:37:00 GMT (envelope-from yuri@FreeBSD.org) Message-Id: <201906140737.x5E7b0eY092080@repo.freebsd.org> X-Authentication-Warning: repo.freebsd.org: yuri set sender to yuri@FreeBSD.org using -f From: Yuri Victorovich Date: Fri, 14 Jun 2019 07:37:00 +0000 (UTC) To: ports-committers@freebsd.org, svn-ports-all@freebsd.org, svn-ports-head@freebsd.org Subject: svn commit: r504169 - in head/math: . boolector boolector/files X-SVN-Group: ports-head X-SVN-Commit-Author: yuri X-SVN-Commit-Paths: in head/math: . boolector boolector/files X-SVN-Commit-Revision: 504169 X-SVN-Commit-Repository: ports MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-Rspamd-Queue-Id: 0A0DC87F46 X-Spamd-Bar: -- Authentication-Results: mx1.freebsd.org X-Spamd-Result: default: False [-2.97 / 15.00]; local_wl_from(0.00)[FreeBSD.org]; NEURAL_HAM_MEDIUM(-1.00)[-0.998,0]; NEURAL_HAM_LONG(-1.00)[-1.000,0]; NEURAL_HAM_SHORT(-0.97)[-0.974,0]; ASN(0.00)[asn:11403, ipnet:2610:1c1:1::/48, country:US] X-BeenThere: svn-ports-head@freebsd.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: SVN commit messages for the ports tree for head List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Fri, 14 Jun 2019 07:37:02 -0000 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@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 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