Initial import of Yices 2, version 2.6.1.

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.

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
+