summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--math/yices2/DESCR10
-rw-r--r--math/yices2/Makefile30
-rw-r--r--math/yices2/PLIST11
-rw-r--r--math/yices2/buildlink3.mk15
-rw-r--r--math/yices2/distinfo11
-rw-r--r--math/yices2/patches/patch-Makefile.build42
-rw-r--r--math/yices2/patches/patch-autoconf_os15
-rw-r--r--math/yices2/patches/patch-configure.ac103
-rw-r--r--math/yices2/patches/patch-src_Makefile42
-rw-r--r--math/yices2/patches/patch-src_utils_bit__tricks.h82
10 files changed, 361 insertions, 0 deletions
diff --git a/math/yices2/DESCR b/math/yices2/DESCR
new file mode 100644
index 00000000000..6961674dcbc
--- /dev/null
+++ b/math/yices2/DESCR
@@ -0,0 +1,10 @@
+Yices 2 is an SMT solver that decides the satisfiability of formulas
+containing uninterpreted function symbols with equality, real and
+integer arithmetic, bitvectors, scalar types, and tuples. Yices 2
+supports both linear and nonlinear arithmetic.
+
+Yices 2 can process input written in the SMT-LIB notation (both
+versions 2.0 and 1.2 are supported). Alternatively, you can write
+specifications using Yices 2's own specification language, which
+includes tuples and scalar types. You can also use Yices 2 as a
+library in your software.
diff --git a/math/yices2/Makefile b/math/yices2/Makefile
new file mode 100644
index 00000000000..68dc445525c
--- /dev/null
+++ b/math/yices2/Makefile
@@ -0,0 +1,30 @@
+# $NetBSD: Makefile,v 1.1.1.1 2019/08/24 22:09:16 alnsn Exp $
+
+PKGNAME= yices2-2.6.1
+DISTNAME= Yices-${PKGVERSION}
+GITHUB_TAG= ${DISTNAME}
+CATEGORIES= math
+MASTER_SITES= ${MASTER_SITE_GITHUB:=SRI-CSL/}
+
+MAINTAINER= alnsn@NetBSD.org
+HOMEPAGE= https://yices.csl.sri.com/
+COMMENT= Yices 2 SMT solver
+LICENSE= gnu-gpl-v3
+
+BUILD_DEPENDS+= gperf-[0-9]*:../../devel/gperf
+
+USE_TOOLS+= autoconf gmake
+USE_LANGUAGES= c
+GNU_CONFIGURE= yes
+USE_GNU_CONFIGURE_HOST= no
+
+WRKSRC= ${WRKDIR}/yices2-${DISTNAME}
+
+pre-configure:
+ cd ${WRKSRC} && autoconf
+
+pre-install:
+ cd ${WRKSRC} && make dist
+
+.include "../../devel/gmp/buildlink3.mk"
+.include "../../mk/bsd.pkg.mk"
diff --git a/math/yices2/PLIST b/math/yices2/PLIST
new file mode 100644
index 00000000000..20426c8270b
--- /dev/null
+++ b/math/yices2/PLIST
@@ -0,0 +1,11 @@
+@comment $NetBSD: PLIST,v 1.1.1.1 2019/08/24 22:09:16 alnsn Exp $
+bin/yices
+bin/yices-sat
+bin/yices-smt
+bin/yices-smt2
+include/yices.h
+include/yices_exit_codes.h
+include/yices_limits.h
+include/yices_types.h
+lib/libyices.so
+lib/libyices.so.${PKGVERSION}
diff --git a/math/yices2/buildlink3.mk b/math/yices2/buildlink3.mk
new file mode 100644
index 00000000000..593db0b145d
--- /dev/null
+++ b/math/yices2/buildlink3.mk
@@ -0,0 +1,15 @@
+# $NetBSD: buildlink3.mk,v 1.1.1.1 2019/08/24 22:09:16 alnsn Exp $
+
+BUILDLINK_TREE+= yices2
+
+.if !defined(YICES2_BUILDLINK3_MK)
+YICES2_BUILDLINK3_MK:=
+
+BUILDLINK_API_DEPENDS.yices2+= yices2>=2.6.1
+BUILDLINK_ABI_DEPENDS.yices2+= yices2>=2.6.1
+BUILDLINK_PKGSRCDIR.yices2?= ../../math/yices2
+.endif # YICES2_BUILDLINK3_MK
+
+.include "../../devel/gmp/buildlink3.mk"
+
+BUILDLINK_TREE+= -yices2
diff --git a/math/yices2/distinfo b/math/yices2/distinfo
new file mode 100644
index 00000000000..52f29ccf8c9
--- /dev/null
+++ b/math/yices2/distinfo
@@ -0,0 +1,11 @@
+$NetBSD: distinfo,v 1.1.1.1 2019/08/24 22:09:16 alnsn Exp $
+
+SHA1 (Yices-2.6.1.tar.gz) = 472c4eb7dadc3e8de30495389f50ad3aa09baa08
+RMD160 (Yices-2.6.1.tar.gz) = 337faea5f2963998a93645f5b1abb4830f5dc1b8
+SHA512 (Yices-2.6.1.tar.gz) = 586f24a8e3da45726ee69f4b3a744f2c04c3b400304319c00667c81c6799a846906ed580a9c4dd0df87a23ddb8e4fefb0b8ab60c13c19dc29243ba116717d1f2
+Size (Yices-2.6.1.tar.gz) = 8903749 bytes
+SHA1 (patch-Makefile.build) = 64c6ae7101c6dd20f455e7575ce8c59fd518152a
+SHA1 (patch-autoconf_os) = fd055ab19f49921aece028df67668613ae089b3c
+SHA1 (patch-configure.ac) = 5c4579cfd0e6cc1d6f9a1315f0b4db28048febb0
+SHA1 (patch-src_Makefile) = 38bb8236d9eacd919c8afc3ed5ae0c9ea1b0233a
+SHA1 (patch-src_utils_bit__tricks.h) = 0abcd0244cb55e7889aab3550af6c25ae3c88850
diff --git a/math/yices2/patches/patch-Makefile.build b/math/yices2/patches/patch-Makefile.build
new file mode 100644
index 00000000000..aa4bbffe2aa
--- /dev/null
+++ b/math/yices2/patches/patch-Makefile.build
@@ -0,0 +1,42 @@
+$NetBSD: patch-Makefile.build,v 1.1.1.1 2019/08/24 22:09:16 alnsn Exp $
+
+Add NetBSD targets, pull request https://github.com/SRI-CSL/yices2/pull/134
+
+--- Makefile.build.orig 2018-10-26 21:33:09.000000000 +0000
++++ Makefile.build
+@@ -213,14 +213,14 @@ build_subdirs: $(build_dir) $(dyn_objsub
+
+ static_build_subdirs-mingw static_build_subdirs-cygwin: $(static_dll_objsubdirs)
+
+-static_build_subdirs-darwin static_build_subdirs-linux static_build_subdirs-unix static_build_subdirs-freebsd:
++static_build_subdirs-darwin static_build_subdirs-linux static_build_subdirs-unix static_build_subdirs-freebsd static_build_subdirs-netbsd:
+
+ static_build_subdirs: $(build_dir) $(static_objsubdirs) $(static_libdir) $(static_bindir) \
+ static_build_subdirs-$(POSIXOS)
+
+ .PHONY: build_subdirs static_build_subdirs static_build_subdirs-darwin static-build_subdirs-cygwin \
+ static_build_subdirs-mingw static_build_subdirs-linux static_build_subdirs-unix \
+- static_build_subdirs-freebsd
++ static_build_subdirs-freebsd static_build_subdirs-netbsd
+
+ #
+ # Compilation
+@@ -485,6 +485,9 @@ install-linux install-unix: install-defa
+ install-freebsd: install-default
+ $(LDCONFIG) -m $(DESTDIR)$(libdir) && (cd $(DESTDIR)$(libdir) && $(LN_S) -f libyices.so.$(MAJOR).$(MINOR) libyices.so)
+
++install-netbsd: install-default
++ (cd $(DESTDIR)$(libdir) && $(LN_S) -f libyices.so.$(YICES_VERSION) libyices.so)
++
+ #
+ # cygwin and mingw install: copy the DLLs in $(bindir)
+ #
+@@ -500,7 +503,7 @@ install-mingw: install-cygwin
+
+
+ .PHONY: install install-default install-darwin install-solaris \
+- install-linux install-freebsd install-unix \
++ install-linux install-freebsd install-netbsd install-unix \
+ install-cygwin install-mingw
+
+
diff --git a/math/yices2/patches/patch-autoconf_os b/math/yices2/patches/patch-autoconf_os
new file mode 100644
index 00000000000..12f973f3198
--- /dev/null
+++ b/math/yices2/patches/patch-autoconf_os
@@ -0,0 +1,15 @@
+$NetBSD: patch-autoconf_os,v 1.1.1.1 2019/08/24 22:09:16 alnsn Exp $
+
+Add NetBSD, pull request https://github.com/SRI-CSL/yices2/pull/134
+
+--- autoconf/os.orig 2018-10-26 21:33:09.000000000 +0000
++++ autoconf/os
+@@ -13,6 +13,8 @@ if eval 'uname > /dev/null 2> /dev/null'
+ echo "mingw";;
+ FreeBSD*)
+ echo "freebsd";;
++ NetBSD*)
++ echo "netbsd";;
+ *)
+ echo "unix";;
+ esac
diff --git a/math/yices2/patches/patch-configure.ac b/math/yices2/patches/patch-configure.ac
new file mode 100644
index 00000000000..6981216ba73
--- /dev/null
+++ b/math/yices2/patches/patch-configure.ac
@@ -0,0 +1,103 @@
+$NetBSD: patch-configure.ac,v 1.1.1.1 2019/08/24 22:09:16 alnsn Exp $
+
+Fix "=" comparisons, pull request https://github.com/SRI-CSL/yices2/pull/134
+
+--- configure.ac.orig 2018-10-26 21:33:09.000000000 +0000
++++ configure.ac
+@@ -191,7 +191,7 @@ dnl
+ static_libgmp=""
+ AC_ARG_WITH([static-gmp],
+ [AS_HELP_STRING([--with-static-gmp=<path>],[Full path to a static GMP library (e.g., libgmp.a)])],
+- [if test "x$withval" == x; then
++ [if test "x$withval" = x; then
+ AC_MSG_WARN([--with-static-gmp was used but no path was given. Using defaults])
+ else
+ static_libgmp=$withval
+@@ -203,7 +203,7 @@ static_includegmp=""
+ AC_ARG_WITH([static-gmp-include-dir],
+ [AS_HELP_STRING([--with-static-gmp-include-dir=<directory>],
+ [Directory of include file "gmp.h" compatible with static GMP library])],
+- [if test "x$withval" == x; then
++ [if test "x$withval" = x; then
+ AC_MSG_WARN([--with-static-gmp-include-dir was used but no directory was given. Using defaults])
+ else
+ static_includegmp=$withval
+@@ -215,7 +215,7 @@ AC_ARG_WITH([static-gmp-include-dir],
+ pic_libgmp=""
+ AC_ARG_WITH([pic-gmp],
+ [AS_HELP_STRING([--with-pic-gmp=<path>],[Full path to a relocatable GMP library (e.g., libgmp.a)])],
+- [if test "x$withval" == x; then
++ [if test "x$withval" = x; then
+ AC_MSG_WARN([--with-pic-gmp was used but no path was given. Using defaults])
+ else
+ pic_libgmp=$withval
+@@ -227,7 +227,7 @@ pic_includegmp=""
+ AC_ARG_WITH([pic-gmp-include-dir],
+ [AS_HELP_STRING([--with-pic-gmp-include-dir=<directory>],
+ [Directory of include file "gmp.h" compatible with relocatable GMP library])],
+- [if test "x$withval" == x; then
++ [if test "x$withval" = x; then
+ AC_MSG_WARN([--with-pic-gmp-include-dir was used but no directory was given. Using defaults])
+ else
+ pic_includegmp=$withval
+@@ -257,10 +257,10 @@ AC_ARG_ENABLE([mcsat],
+ static_lpoly=""
+ AC_ARG_WITH([static-libpoly],
+ [AS_HELP_STRING([--with-static-libpoly=<path>],[Full path to libpoly.a])],
+- [if test $use_mcsat == "no" ; then
++ [if test $use_mcsat = "no" ; then
+ AC_MSG_WARN([Ignoring option --with-static-libpoly since MCSAT support is disabled])
+ else
+- if test "x$withval" == x; then
++ if test "x$withval" = x; then
+ AC_MSG_WARN([--with-static-poly was used but no path was given. Using defaults])
+ else
+ static_lpoly=$withval
+@@ -273,10 +273,10 @@ static_includelpoly=""
+ AC_ARG_WITH([static-libpoly-include-dir],
+ [AS_HELP_STRING([--with-static-libpoly-include-dir=<directory>],
+ [Path to include files compatible with libpoly.a (e.g., /usr/local/include)])],
+- [if test $use_mcsat == "no" ; then
++ [if test $use_mcsat = "no" ; then
+ AC_MSG_WARN([Ignoring option --with-static-libpoly-include-dir since MCSAT support is disabled])
+ else
+- if test "x$withval" == x; then
++ if test "x$withval" = x; then
+ AC_MSG_WARN([--with-static-libpoly-include-dir was used but no directory was given. Using defaults])
+ else
+ static_includelpoly=$withval
+@@ -289,10 +289,10 @@ AC_ARG_WITH([static-libpoly-include-dir]
+ pic_lpoly=""
+ AC_ARG_WITH([pic-libpoly],
+ [AS_HELP_STRING([--with-pic-libpoly=<path>],[Full path to a relocatable libpoly.a])],
+- [if test $use_mcsat == "no" ; then
++ [if test $use_mcsat = "no" ; then
+ AC_MSG_WARN([Ignoring option --with-pic-libpoly since MCSAT support is disabled])
+ else
+- if test "x$withval" == x; then
++ if test "x$withval" = x; then
+ AC_MSG_WARN([--with-pic-libpoly was used but no path was given. Using defaults])
+ else
+ pic_lpoly=$withval
+@@ -305,10 +305,10 @@ pic_includelpoly=""
+ AC_ARG_WITH([pic-libpoly-include-dir],
+ [AS_HELP_STRING([--with-pic-libpoly-include-dir=<directory>],
+ [Path to include files compatible with the relocatable libpoly.a])],
+- [if test $use_mcsat == "no" ; then
++ [if test $use_mcsat = "no" ; then
+ AC_MSG_WARN([Ignoring option --with-pic-libpoly-include-dir since MCSAT support is disabled])
+ else
+- if test "x$withval" == x; then
++ if test "x$withval" = x; then
+ AC_MSG_WARN([--with-pic-libpoly-include-dir was used but no directory was given. Using defaults])
+ else
+ pic_includelpoly=$withval
+@@ -811,7 +811,7 @@ if test ! -d configs ; then
+ AS_MKDIR_P([configs])
+ fi
+
+-if test "x$host" == x ; then
++if test "x$host" = x ; then
+ AC_MSG_NOTICE([Moving make.include to configs/make.include.$build])
+ mv make.include "configs/make.include.$build"
+ else
diff --git a/math/yices2/patches/patch-src_Makefile b/math/yices2/patches/patch-src_Makefile
new file mode 100644
index 00000000000..ec53fae3917
--- /dev/null
+++ b/math/yices2/patches/patch-src_Makefile
@@ -0,0 +1,42 @@
+$NetBSD: patch-src_Makefile,v 1.1.1.1 2019/08/24 22:09:16 alnsn Exp $
+
+Add NetBSD targets, do not invoke static_libyices_dynamic, pull request https://github.com/SRI-CSL/yices2/pull/134
+
+--- src/Makefile.orig 2018-10-26 21:33:09.000000000 +0000
++++ src/Makefile
+@@ -624,6 +624,18 @@ ifeq ($(POSIXOS),freebsd)
+ static_libyices_dynamic=$(static_libdir)/$(libyices_so)
+
+ else
++ifeq ($(POSIXOS),netbsd)
++ PIC=-fPIC
++ STATIC=-static
++ CPPFLAGS := $(CPPFLAGS) -DNETBSD
++ CFLAGS += -fvisibility=hidden
++ BIN_LDFLAGS=
++ libyices_dynamic=$(libdir)/$(libyices_so)
++ # Dynamic library can't be built from .a files because
++ # they aren't normally built with -fPIC.
++ static_libyices_dynamic=
++
++else
+ ifeq ($(POSIXOS),unix)
+ PIC=-fPIC
+ STATIC=-static
+@@ -641,6 +653,7 @@ endif
+ endif
+ endif
+ endif
++endif
+
+ #
+ # include dirs: we want -I. first
+@@ -1102,7 +1115,7 @@ static-bin: $(static_binaries)
+ # Libraries
+ lib: $(libyices) $(libyices_dynamic)
+
+-static-lib: $(static_libyices) $(static_libyices_dynamic)
++static-lib: $(static_libyices)
+
+
+ .PHONY: obj static-obj bin static-bin lib static-lib
diff --git a/math/yices2/patches/patch-src_utils_bit__tricks.h b/math/yices2/patches/patch-src_utils_bit__tricks.h
new file mode 100644
index 00000000000..42881082365
--- /dev/null
+++ b/math/yices2/patches/patch-src_utils_bit__tricks.h
@@ -0,0 +1,82 @@
+$NetBSD: patch-src_utils_bit__tricks.h,v 1.1.1.1 2019/08/24 22:09:16 alnsn Exp $
+
+NetBSD has popcount in libc, pull request https://github.com/SRI-CSL/yices2/pull/134
+
+--- src/utils/bit_tricks.h.orig 2018-10-26 21:33:09.000000000 +0000
++++ src/utils/bit_tricks.h
+@@ -55,6 +55,11 @@
+ #include <stdint.h>
+ #include <assert.h>
+
++#ifdef NETBSD
++/* NetBSD has popcount in libc. */
++#include <strings.h>
++#endif
++
+
+ #ifdef __GNUC__
+
+@@ -101,9 +106,11 @@ static inline uint32_t clz(uint32_t x) {
+ return __builtin_clzl(x);
+ }
+
++#ifndef NETBSD
+ static inline uint32_t popcount32(uint32_t x) {
+ return __builtin_popcountl(x);
+ }
++#endif
+
+ #else
+ //#warning "ctz: uint32_t is (unsigned int)"
+@@ -118,9 +125,11 @@ static inline uint32_t clz(uint32_t x) {
+ return __builtin_clz(x);
+ }
+
++#ifndef NETBSD
+ static inline uint32_t popcount32(uint32_t x) {
+ return __builtin_popcount(x);
+ }
++#endif
+
+ #endif
+
+@@ -141,9 +150,11 @@ static inline uint32_t clz64(uint64_t x)
+ return __builtin_clzll(x);
+ }
+
++#ifndef NETBSD
+ static inline uint32_t popcount64(uint64_t x) {
+ return __builtin_popcountll(x);
+ }
++#endif
+
+ #else
+ // #warning "bit_tricks: uint64_t is (unsigned long)
+@@ -158,9 +169,11 @@ static inline uint32_t clz64(uint64_t x)
+ return __builtin_clzl(x);
+ }
+
++#ifndef NETBSD
+ static inline uint32_t popcount64(uint64_t x) {
+ return __builtin_popcountl(x);
+ }
++#endif
+
+ #endif // 64bit versions
+
+@@ -223,6 +236,7 @@ static inline uint32_t clz64(uint64_t x)
+ return i;
+ }
+
++#ifndef NETBSD
+ static inline uint32_t popcount32(uint32_t x) {
+ uint32_t c;
+
+@@ -246,6 +260,7 @@ static inline uint32_t popcount64(uint64
+
+ return c;
+ }
++#endif /* #ifndef NETBSD */
+
+ #endif
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-14 10:21:49 +0000