New port: math/yices: SMT solver

5 files changed, 87 insertions, 0 deletions

diff --git a/math/yices/Makefile b/math/yices/Makefile
new file mode 100644
index 000000000000..c96114cd3668
--- /dev/null
+++ b/math/yices/Makefile
@@ -0,0 +1,32 @@
+# $FreeBSD$
+
+PORTNAME=	yices
+DISTVERSION=	2.6.0
+CATEGORIES=	math
+MASTER_SITES=	http://yices.csl.sri.com/releases/${DISTVERSION}/
+DISTNAME=	${PORTNAME}-${DISTVERSION}-src
+
+MAINTAINER=	yuri@FreeBSD.org
+COMMENT=	SMT solver
+
+LICENSE=	GPLv3
+LICENSE_FILE=	${WRKSRC}/LICENSE
+
+BUILD_DEPENDS=	gperf:devel/gperf
+LIB_DEPENDS=	libgmp.so:math/gmp
+
+USES=		gmake localbase
+GNU_CONFIGURE=	yes
+CONFIGURE_ARGS=	--with-pic-gmp=${LOCALBASE}/lib/libgmp.so
+USE_LDCONFIG=	yes
+
+MAKE_ARGS=	YICES_MAKE_INCLUDE=configs/make.include.${CONFIGURE_TARGET}
+CFLAGS+=	-fPIC
+
+WRKSRC=		${WRKDIR}/${PORTNAME}-${DISTVERSION}
+
+post-install:
+	@${RM} ${STAGEDIR}${PREFIX}/lib/*.a
+	@cd ${STAGEDIR}${PREFIX}/lib && ${LN} -s libyices.so.2.6 libyices.so && ${LN} -s libyices.so.2.6 libyices.so.2
+
+.include <bsd.port.mk>
diff --git a/math/yices/distinfo b/math/yices/distinfo
new file mode 100644
index 000000000000..1ca35faa1ea3
--- /dev/null
+++ b/math/yices/distinfo
@@ -0,0 +1,3 @@
+TIMESTAMP = 1532156748
+SHA256 (yices-2.6.0-src.tar.gz) = 4712c5c4bd1d299418148c68851c023041dc16450907353bedd4c17c1e4713e4
+SIZE (yices-2.6.0-src.tar.gz) = 5539571
diff --git a/math/yices/files/patch-Makefile.build b/math/yices/files/patch-Makefile.build
new file mode 100644
index 000000000000..3ab7ed1d0580
--- /dev/null
+++ b/math/yices/files/patch-Makefile.build
@@ -0,0 +1,28 @@
+--- Makefile.build.orig	2018-06-29 04:11:11 UTC
++++ Makefile.build
+@@ -131,7 +131,7 @@ static_objsubdirs := $(srcsubdirs:%=$(st
+ # build_dir/dist: binaries + libraries with distribution not linked with GMP
+ # build_dir/static_dist: includes GMP (statically linked)
+ #
+-dist_dir = $(build_dir)/dist
++dist_dir = $(build_dir)
+ static_dist_dir = $(build_dir)/static_dist
+ 
+ 
+@@ -448,7 +448,7 @@ install-default:
+ 	$(MKDIR_P) $(DESTDIR)$(bindir)
+ 	$(MKDIR_P) $(DESTDIR)$(libdir)
+ 	$(MKDIR_P) $(DESTDIR)$(includedir)
+-	$(INSTALL) -m 664 $(dist_dir)/include/* $(DESTDIR)$(includedir)
++	$(INSTALL) -m 664 $(dist_dir)/../../src/include/* $(DESTDIR)$(includedir)
+ 	$(INSTALL) $(dist_dir)/bin/* $(DESTDIR)$(bindir)
+ 	$(INSTALL) $(dist_dir)/lib/* $(DESTDIR)$(libdir)
+ 
+@@ -467,7 +467,6 @@ install-linux install-unix: install-defa
+ # be added to the hints file.' In other words, ldconfig on FreeBSD doesn't create the symbolic link,
+ # as on Linux.
+ install-freebsd: install-default
+-	$(LDCONFIG) -m $(DESTDIR)$(libdir) && (cd $(DESTDIR)$(libdir) && $(LN_S) -f libyices.so.$(MAJOR).$(MINOR) libyices.so)
+ 
+ #
+ # cygwin and mingw install: copy the DLLs in $(bindir)
diff --git a/math/yices/pkg-descr b/math/yices/pkg-descr
new file mode 100644
index 000000000000..a2539ed6cda8
--- /dev/null
+++ b/math/yices/pkg-descr
@@ -0,0 +1,11 @@
+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.
+
+WWW: http://yices.csl.sri.com/
diff --git a/math/yices/pkg-plist b/math/yices/pkg-plist
new file mode 100644
index 000000000000..32da57a6ad50
--- /dev/null
+++ b/math/yices/pkg-plist
@@ -0,0 +1,13 @@
+bin/yices_main
+bin/yices_sat
+bin/yices_sat_new
+bin/yices_smt
+bin/yices_smt2
+bin/yices_smtcomp
+include/yices.h
+include/yices_exit_codes.h
+include/yices_limits.h
+include/yices_types.h
+lib/libyices.so
+lib/libyices.so.2
+lib/libyices.so.2.6