mirror/freebsd-ports
1
0
Fork 0
mirror of https://git.FreeBSD.org/ports.git synced 2024-12-22 04:17:44 +00:00
Code Issues Releases Activity
f2647c6573
freebsd-ports/math/cvc4/Makefile

99 lines
2.8 KiB
Makefile
Raw Normal View History

New port: math/cvc4 An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination. WWW: https://cvc4.cs.stanford.edu/web/ PR: 227702 Submitted by: Greg V <greg@unrelenting.technology>
2018-06-21 11:06:10 +00:00
# $FreeBSD$
PORTNAME= cvc4
math/cvc4: update to 1.7 ChangeLog: https://github.com/CVC4/CVC4/releases/tag/1.7 * New Features: Proofs: Support for bit-vector proofs with eager bitblasting Strings: Support for str.replaceall operator. New option --re-elim SyGuS: Support for abduction (--sygus-abduct) * Improvements: Strings: Significantly better performance * Changes: API change: Expr::iffExpr() is renamed to Expr::eqExpr() Compiling the language bindings now requires SWIG 3 instead of SWIG 2. The CVC3 compatibility layer has been removed. The build system now uses CMake instead of Autotools
2019-08-01 15:20:28 +00:00
DISTVERSION= 1.7
math/cryptominisat and math/py-cryptominisat: Update to 5.7.1 Bump PORTREVISIONs of consumer ports.
2020-07-09 15:44:39 +00:00
PORTREVISION= 4
New port: math/cvc4 An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination. WWW: https://cvc4.cs.stanford.edu/web/ PR: 227702 Submitted by: Greg V <greg@unrelenting.technology>
2018-06-21 11:06:10 +00:00
CATEGORIES= math java
math/cvc4: update to 1.7 ChangeLog: https://github.com/CVC4/CVC4/releases/tag/1.7 * New Features: Proofs: Support for bit-vector proofs with eager bitblasting Strings: Support for str.replaceall operator. New option --re-elim SyGuS: Support for abduction (--sygus-abduct) * Improvements: Strings: Significantly better performance * Changes: API change: Expr::iffExpr() is renamed to Expr::eqExpr() Compiling the language bindings now requires SWIG 3 instead of SWIG 2. The CVC3 compatibility layer has been removed. The build system now uses CMake instead of Autotools
2019-08-01 15:20:28 +00:00
MASTER_SITES+= http://www.antlr3.org/download/:antlr3
DISTFILES+= antlr-3.4-complete.jar:antlr3
EXTRACT_ONLY= ${DISTNAME}${EXTRACT_SUFX}
PATCH_SITES= https://github.com/${GH_ACCOUNT}/${GH_PROJECT}/commit/
PATCHFILES+= fc8907afc08d.patch:-p1 # Install Java bindings
New port: math/cvc4 An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination. WWW: https://cvc4.cs.stanford.edu/web/ PR: 227702 Submitted by: Greg V <greg@unrelenting.technology>
2018-06-21 11:06:10 +00:00
MAINTAINER= greg@unrelenting.technology
COMMENT= Automatic theorem prover for SMT (Satisfiability Modulo Theories)
LICENSE= BSD3CLAUSE
LICENSE_FILE= ${WRKSRC}/COPYING
math/cvc4: update to 1.7 ChangeLog: https://github.com/CVC4/CVC4/releases/tag/1.7 * New Features: Proofs: Support for bit-vector proofs with eager bitblasting Strings: Support for str.replaceall operator. New option --re-elim SyGuS: Support for abduction (--sygus-abduct) * Improvements: Strings: Significantly better performance * Changes: API change: Expr::iffExpr() is renamed to Expr::eqExpr() Compiling the language bindings now requires SWIG 3 instead of SWIG 2. The CVC3 compatibility layer has been removed. The build system now uses CMake instead of Autotools
2019-08-01 15:20:28 +00:00
BUILD_DEPENDS= bash:shells/bash
New port: math/cvc4 An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination. WWW: https://cvc4.cs.stanford.edu/web/ PR: 227702 Submitted by: Greg V <greg@unrelenting.technology>
2018-06-21 11:06:10 +00:00
LIB_DEPENDS= libantlr3c.so:devel/libantlr3c \
libboost_system.so:devel/boost-libs
math/cvc4: update to 1.7 ChangeLog: https://github.com/CVC4/CVC4/releases/tag/1.7 * New Features: Proofs: Support for bit-vector proofs with eager bitblasting Strings: Support for str.replaceall operator. New option --re-elim SyGuS: Support for abduction (--sygus-abduct) * Improvements: Strings: Significantly better performance * Changes: API change: Expr::iffExpr() is renamed to Expr::eqExpr() Compiling the language bindings now requires SWIG 3 instead of SWIG 2. The CVC3 compatibility layer has been removed. The build system now uses CMake instead of Autotools
2019-08-01 15:20:28 +00:00
USES= cmake ncurses compiler:c++17-lang \
math/cvc4: Remove llvm60 build dependency It was added for FreeBSD 10.x/i386 and is no longer needed. PR: 238162 Approved by: greg@unrelenting.technology (maintainer)
2019-05-27 10:10:15 +00:00
pkgconfig python:3.5+,build shebangfix
math/cvc4: update to 1.7 ChangeLog: https://github.com/CVC4/CVC4/releases/tag/1.7 * New Features: Proofs: Support for bit-vector proofs with eager bitblasting Strings: Support for str.replaceall operator. New option --re-elim SyGuS: Support for abduction (--sygus-abduct) * Improvements: Strings: Significantly better performance * Changes: API change: Expr::iffExpr() is renamed to Expr::eqExpr() Compiling the language bindings now requires SWIG 3 instead of SWIG 2. The CVC3 compatibility layer has been removed. The build system now uses CMake instead of Autotools
2019-08-01 15:20:28 +00:00
SHEBANG_FILES= src/base/mktagheaders \
src/base/mktags
USE_GITHUB= yes
GH_ACCOUNT= CVC4
GH_PROJECT= CVC4
New port: math/cvc4 An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination. WWW: https://cvc4.cs.stanford.edu/web/ PR: 227702 Submitted by: Greg V <greg@unrelenting.technology>
2018-06-21 11:06:10 +00:00
USE_JAVA= yes
JAVA_BUILD= yes
USE_LDCONFIG= yes
math/cvc4: update to 1.7 ChangeLog: https://github.com/CVC4/CVC4/releases/tag/1.7 * New Features: Proofs: Support for bit-vector proofs with eager bitblasting Strings: Support for str.replaceall operator. New option --re-elim SyGuS: Support for abduction (--sygus-abduct) * Improvements: Strings: Significantly better performance * Changes: API change: Expr::iffExpr() is renamed to Expr::eqExpr() Compiling the language bindings now requires SWIG 3 instead of SWIG 2. The CVC3 compatibility layer has been removed. The build system now uses CMake instead of Autotools
2019-08-01 15:20:28 +00:00
CMAKE_BUILD_TYPE= Production
CMAKE_ARGS+= -DANTLR_BINARY=${WRKDIR}/antlr3
OPTIONS_DEFINE= CRYPTOMINISAT JAVA PYTHON READLINE
New port: math/cvc4 An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination. WWW: https://cvc4.cs.stanford.edu/web/ PR: 227702 Submitted by: Greg V <greg@unrelenting.technology>
2018-06-21 11:06:10 +00:00
OPTIONS_RADIO= NUMLIB
OPTIONS_RADIO_NUMLIB= GMP CLN
math/cvc4: update to 1.7 ChangeLog: https://github.com/CVC4/CVC4/releases/tag/1.7 * New Features: Proofs: Support for bit-vector proofs with eager bitblasting Strings: Support for str.replaceall operator. New option --re-elim SyGuS: Support for abduction (--sygus-abduct) * Improvements: Strings: Significantly better performance * Changes: API change: Expr::iffExpr() is renamed to Expr::eqExpr() Compiling the language bindings now requires SWIG 3 instead of SWIG 2. The CVC3 compatibility layer has been removed. The build system now uses CMake instead of Autotools
2019-08-01 15:20:28 +00:00
OPTIONS_DEFAULT= CRYPTOMINISAT JAVA PYTHON READLINE GMP
New port: math/cvc4 An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination. WWW: https://cvc4.cs.stanford.edu/web/ PR: 227702 Submitted by: Greg V <greg@unrelenting.technology>
2018-06-21 11:06:10 +00:00
OPTIONS_SUB= yes
math/cvc4: Update 1.5 -> 1.6 Port changes: * Add dependency on cryptominisat, and the corresponding port option * Add USES=autoreconf, the suplied configure fails, see https://github.com/CVC4/CVC4/issues/2192 * Now build depends on python * Force clang-60 to prevent build failures on 10 PR: 229780 Submitted by: Greg V <greg@unrelenting.technology>
2018-07-22 18:30:29 +00:00
CRYPTOMINISAT_DESC= Use CryptoMiniSat as the SAT solver
New port: math/cvc4 An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination. WWW: https://cvc4.cs.stanford.edu/web/ PR: 227702 Submitted by: Greg V <greg@unrelenting.technology>
2018-06-21 11:06:10 +00:00
GMP_DESC= Use GMP numeric library
CLN_DESC= Use CLN numeric library (disables portfolio mode)
math/cvc4: update to 1.7 ChangeLog: https://github.com/CVC4/CVC4/releases/tag/1.7 * New Features: Proofs: Support for bit-vector proofs with eager bitblasting Strings: Support for str.replaceall operator. New option --re-elim SyGuS: Support for abduction (--sygus-abduct) * Improvements: Strings: Significantly better performance * Changes: API change: Expr::iffExpr() is renamed to Expr::eqExpr() Compiling the language bindings now requires SWIG 3 instead of SWIG 2. The CVC3 compatibility layer has been removed. The build system now uses CMake instead of Autotools
2019-08-01 15:20:28 +00:00
CRYPTOMINISAT_CMAKE_BOOL= USE_CRYPTOMINISAT
math/cvc4: Update 1.5 -> 1.6 Port changes: * Add dependency on cryptominisat, and the corresponding port option * Add USES=autoreconf, the suplied configure fails, see https://github.com/CVC4/CVC4/issues/2192 * Now build depends on python * Force clang-60 to prevent build failures on 10 PR: 229780 Submitted by: Greg V <greg@unrelenting.technology>
2018-07-22 18:30:29 +00:00
CRYPTOMINISAT_LIB_DEPENDS= libcryptominisat5.so:math/cryptominisat
math/cvc4: update to 1.7 ChangeLog: https://github.com/CVC4/CVC4/releases/tag/1.7 * New Features: Proofs: Support for bit-vector proofs with eager bitblasting Strings: Support for str.replaceall operator. New option --re-elim SyGuS: Support for abduction (--sygus-abduct) * Improvements: Strings: Significantly better performance * Changes: API change: Expr::iffExpr() is renamed to Expr::eqExpr() Compiling the language bindings now requires SWIG 3 instead of SWIG 2. The CVC3 compatibility layer has been removed. The build system now uses CMake instead of Autotools
2019-08-01 15:20:28 +00:00
JAVA_CMAKE_BOOL= BUILD_BINDINGS_JAVA
JAVA_CMAKE_ON= -DJAVA_INCLUDE_PATH:PATH=${JAVA_HOME}/include \
-DJAVA_AWT_LIBRARY:PATH=${JAVA_HOME}/jre/lib/${ARCH}/libjawt.so \
-DJAVA_JVM_LIBRARY:PATH=${JAVA_HOME}/jre/lib/${ATCH}/libjava.so
Move devel/swig30 to devel/swig and update to 4.0.1 - Do not silence installation message - Update dependent ports: - Fix build with swig 4.0.1 - Update *_DEPENDS - Remove BINARY_ALIAS Changes: http://www.swig.org/news.php PR: 246613 Exp-run by: antoine
2020-06-17 18:17:45 +00:00
JAVA_BUILD_DEPENDS= swig:devel/swig
New port: math/cvc4 An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination. WWW: https://cvc4.cs.stanford.edu/web/ PR: 227702 Submitted by: Greg V <greg@unrelenting.technology>
2018-06-21 11:06:10 +00:00
math/cvc4: update to 1.7 ChangeLog: https://github.com/CVC4/CVC4/releases/tag/1.7 * New Features: Proofs: Support for bit-vector proofs with eager bitblasting Strings: Support for str.replaceall operator. New option --re-elim SyGuS: Support for abduction (--sygus-abduct) * Improvements: Strings: Significantly better performance * Changes: API change: Expr::iffExpr() is renamed to Expr::eqExpr() Compiling the language bindings now requires SWIG 3 instead of SWIG 2. The CVC3 compatibility layer has been removed. The build system now uses CMake instead of Autotools
2019-08-01 15:20:28 +00:00
PYTHON_CMAKE_BOOL= BUILD_BINDINGS_PYTHON USE_PYTHON3
Move devel/swig30 to devel/swig and update to 4.0.1 - Do not silence installation message - Update dependent ports: - Fix build with swig 4.0.1 - Update *_DEPENDS - Remove BINARY_ALIAS Changes: http://www.swig.org/news.php PR: 246613 Exp-run by: antoine
2020-06-17 18:17:45 +00:00
PYTHON_BUILD_DEPENDS= swig:devel/swig
New port: math/cvc4 An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination. WWW: https://cvc4.cs.stanford.edu/web/ PR: 227702 Submitted by: Greg V <greg@unrelenting.technology>
2018-06-21 11:06:10 +00:00
math/cvc4: update to 1.7 ChangeLog: https://github.com/CVC4/CVC4/releases/tag/1.7 * New Features: Proofs: Support for bit-vector proofs with eager bitblasting Strings: Support for str.replaceall operator. New option --re-elim SyGuS: Support for abduction (--sygus-abduct) * Improvements: Strings: Significantly better performance * Changes: API change: Expr::iffExpr() is renamed to Expr::eqExpr() Compiling the language bindings now requires SWIG 3 instead of SWIG 2. The CVC3 compatibility layer has been removed. The build system now uses CMake instead of Autotools
2019-08-01 15:20:28 +00:00
READLINE_CMAKE_BOOL= USE_READLINE
READLINE_USES= readline:port
New port: math/cvc4 An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination. WWW: https://cvc4.cs.stanford.edu/web/ PR: 227702 Submitted by: Greg V <greg@unrelenting.technology>
2018-06-21 11:06:10 +00:00
math/cvc4: update to 1.7 ChangeLog: https://github.com/CVC4/CVC4/releases/tag/1.7 * New Features: Proofs: Support for bit-vector proofs with eager bitblasting Strings: Support for str.replaceall operator. New option --re-elim SyGuS: Support for abduction (--sygus-abduct) * Improvements: Strings: Significantly better performance * Changes: API change: Expr::iffExpr() is renamed to Expr::eqExpr() Compiling the language bindings now requires SWIG 3 instead of SWIG 2. The CVC3 compatibility layer has been removed. The build system now uses CMake instead of Autotools
2019-08-01 15:20:28 +00:00
GMP_CMAKE_BOOL= ENABLE_PORTFOLIO
GMP_CMAKE_ON= -DENABLE_DUMPING=OFF
GMP_LIB_DEPENDS= libgmp.so:math/gmp \
libboost_thread.so:devel/boost-libs
# note: CVC4 already depends on boost-libs, so portfolio mode is "free" in terms of pkg dependencies
New port: math/cvc4 An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination. WWW: https://cvc4.cs.stanford.edu/web/ PR: 227702 Submitted by: Greg V <greg@unrelenting.technology>
2018-06-21 11:06:10 +00:00
math/cvc4: update to 1.7 ChangeLog: https://github.com/CVC4/CVC4/releases/tag/1.7 * New Features: Proofs: Support for bit-vector proofs with eager bitblasting Strings: Support for str.replaceall operator. New option --re-elim SyGuS: Support for abduction (--sygus-abduct) * Improvements: Strings: Significantly better performance * Changes: API change: Expr::iffExpr() is renamed to Expr::eqExpr() Compiling the language bindings now requires SWIG 3 instead of SWIG 2. The CVC3 compatibility layer has been removed. The build system now uses CMake instead of Autotools
2019-08-01 15:20:28 +00:00
CLN_CMAKE_BOOL= USE_CLN
CLN_LIB_DEPENDS= libcln.so:math/cln \
libgmp.so:math/gmp
New port: math/cvc4 An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination. WWW: https://cvc4.cs.stanford.edu/web/ PR: 227702 Submitted by: Greg V <greg@unrelenting.technology>
2018-06-21 11:06:10 +00:00
.include <bsd.port.options.mk>
.if ${PORT_OPTIONS:MREADLINE} || ${PORT_OPTIONS:MCLN}
LICENSE= GPLv3
math/cvc4: update to 1.7 ChangeLog: https://github.com/CVC4/CVC4/releases/tag/1.7 * New Features: Proofs: Support for bit-vector proofs with eager bitblasting Strings: Support for str.replaceall operator. New option --re-elim SyGuS: Support for abduction (--sygus-abduct) * Improvements: Strings: Significantly better performance * Changes: API change: Expr::iffExpr() is renamed to Expr::eqExpr() Compiling the language bindings now requires SWIG 3 instead of SWIG 2. The CVC3 compatibility layer has been removed. The build system now uses CMake instead of Autotools
2019-08-01 15:20:28 +00:00
CMAKE_ARGS+= -DENABLE_GPL:BOOL=ON
New port: math/cvc4 An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination. WWW: https://cvc4.cs.stanford.edu/web/ PR: 227702 Submitted by: Greg V <greg@unrelenting.technology>
2018-06-21 11:06:10 +00:00
.endif
math/cvc4: update to 1.7 ChangeLog: https://github.com/CVC4/CVC4/releases/tag/1.7 * New Features: Proofs: Support for bit-vector proofs with eager bitblasting Strings: Support for str.replaceall operator. New option --re-elim SyGuS: Support for abduction (--sygus-abduct) * Improvements: Strings: Significantly better performance * Changes: API change: Expr::iffExpr() is renamed to Expr::eqExpr() Compiling the language bindings now requires SWIG 3 instead of SWIG 2. The CVC3 compatibility layer has been removed. The build system now uses CMake instead of Autotools
2019-08-01 15:20:28 +00:00
post-extract:
@${CP} ${DISTDIR}/antlr-3.4-complete.jar ${WRKDIR}/antlr3.jar
@${ECHO_CMD} "#!/bin/sh" > ${WRKDIR}/antlr3
Clean up after java/openjdk6 and java/openjdk6-jre removal java/openjdk6 support was removed from Mk/bsd.java.mk (r512662) and java/openjdk6 and java/openjdk6-jre were removed from the ports tree (r512663). Now this patch completely removes remaining stuff from the ports tree. PR: 241953 (exp-run) Reviewed by: glewis Approved by: portmgr (antoine) Differential Revision: https://reviews.freebsd.org/D22342
2019-11-26 21:46:12 +00:00
@${ECHO_CMD} "exec \"${LOCALBASE}/bin/java\" -classpath \"${WRKDIR}/antlr3.jar\" org.antlr.Tool \"\$$@\"" >> ${WRKDIR}/antlr3
math/cvc4: update to 1.7 ChangeLog: https://github.com/CVC4/CVC4/releases/tag/1.7 * New Features: Proofs: Support for bit-vector proofs with eager bitblasting Strings: Support for str.replaceall operator. New option --re-elim SyGuS: Support for abduction (--sygus-abduct) * Improvements: Strings: Significantly better performance * Changes: API change: Expr::iffExpr() is renamed to Expr::eqExpr() Compiling the language bindings now requires SWIG 3 instead of SWIG 2. The CVC3 compatibility layer has been removed. The build system now uses CMake instead of Autotools
2019-08-01 15:20:28 +00:00
@${CHMOD} +x ${WRKDIR}/antlr3
math/cvc4: Fix headers Fix headers so other programs can include them safely. This unbreaks lang/maude and lang/solidity PR: 238376 Reported by: jbeich@
2019-08-05 16:59:25 +00:00
post-patch:
math/cvc4: simplify post-patch * Bump PORTREVISION * Unbreak lang/maude and lang/solidity (broken in r508058 and r508059) Reported by: jbeich@ Reviewed by: jbeich@ Differential Revision: https://reviews.freebsd.org/D21170
2019-08-06 17:36:36 +00:00
@${REINPLACE_CMD} -e "s|sed -i 's|sed -i '' 's|g" \
math/cvc4: Fix headers Fix headers so other programs can include them safely. This unbreaks lang/maude and lang/solidity PR: 238376 Reported by: jbeich@
2019-08-05 16:59:25 +00:00
${WRKSRC}/src/fix-install-headers.sh
math/cvc4: update to 1.7 ChangeLog: https://github.com/CVC4/CVC4/releases/tag/1.7 * New Features: Proofs: Support for bit-vector proofs with eager bitblasting Strings: Support for str.replaceall operator. New option --re-elim SyGuS: Support for abduction (--sygus-abduct) * Improvements: Strings: Significantly better performance * Changes: API change: Expr::iffExpr() is renamed to Expr::eqExpr() Compiling the language bindings now requires SWIG 3 instead of SWIG 2. The CVC3 compatibility layer has been removed. The build system now uses CMake instead of Autotools
2019-08-01 15:20:28 +00:00
# make a relative symlink instead of absolute to build dir
post-install-JAVA-on:
@${LN} -sf CVC4-1.7.0.jar ${STAGEDIR}${PREFIX}/share/java/cvc4/CVC4.jar
New port: math/cvc4 An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination. WWW: https://cvc4.cs.stanford.edu/web/ PR: 227702 Submitted by: Greg V <greg@unrelenting.technology>
2018-06-21 11:06:10 +00:00
.include <bsd.port.mk>
Reference in New Issue Copy Permalink