Add stp , a Decision Procedure for Bitvectors and Arrays.

3 files changed, 58 insertions, 0 deletions

diff --git a/math/stp/Makefile b/math/stp/Makefile
new file mode 100644
index 000000000000..20d8e0b952c2
--- /dev/null
+++ b/math/stp/Makefile
@@ -0,0 +1,41 @@
+# New ports collection makefile for:	stp
+# Date created:		2008-06-18
+# Whom:			Li-Wen Hsu <lwhsu@FreeBSD.org>
+#
+# $FreeBSD$
+#
+
+PORTNAME=	stp
+DISTVERSIONPREFIX=	ver-
+DISTVERSION=	0.1
+DISTVERSIONSUFFIX=	-02-26-2008
+CATEGORIES=	math
+MASTER_SITES=	SF
+MASTER_SITE_SUBDIR=	stp-fast-prover
+
+MAINTAINER=	lwhsu@FreeBSD.org
+COMMENT=	A Decision Procedure for Bitvectors and Arrays
+
+USE_BISON=	build
+USE_GMAKE=	yes
+USE_PERL5_BUILD=	yes
+
+WRKSRC=	${WRKDIR}/stp
+
+PLIST_FILES=	bin/stp \
+		include/stp/c_interface.h \
+		include/stp/fdstream.h \
+		lib/libstp.a
+PLIST_DIRS=	include/stp
+
+do-configure:
+	${ECHO_CMD} "PREFIX=${PREFIX}" > ${WRKSRC}/config.info
+	${CP} ${WRKSRC}/Makefile.in ${WRKSRC}/Makefile
+
+do-install:
+	${INSTALL_PROGRAM} ${WRKSRC}/bin/stp ${PREFIX}/bin
+	${INSTALL_DATA} ${WRKSRC}/lib/libstp.a ${PREFIX}/lib
+	${MKDIR} ${PREFIX}/include/stp
+	${INSTALL_DATA} ${WRKSRC}/c_interface/*.h ${PREFIX}/include/stp
+
+.include <bsd.port.mk>
diff --git a/math/stp/distinfo b/math/stp/distinfo
new file mode 100644
index 000000000000..d8e94a163408
--- /dev/null
+++ b/math/stp/distinfo
@@ -0,0 +1,3 @@
+MD5 (stp-ver-0.1-02-26-2008.tar.gz) = a43f30af5db5baba27331842cac7f938
+SHA256 (stp-ver-0.1-02-26-2008.tar.gz) = 3c89182df8bf7878ea1e17a2ebf338a0e96f4af42d72c1a33f01800041898d15
+SIZE (stp-ver-0.1-02-26-2008.tar.gz) = 19907700
diff --git a/math/stp/pkg-descr b/math/stp/pkg-descr
new file mode 100644
index 000000000000..b8fcb3c687cb
--- /dev/null
+++ b/math/stp/pkg-descr
@@ -0,0 +1,14 @@
+STP is a constraint solver (also referred to as a decision procedure or
+automated prover) aimed at solving constraints generated by program analysis
+tools, theorem provers, automated bug finders, intelligent fuzzers and model
+checkers. STP has been used in many research projects at Stanford, Berkeley,
+MIT, CMU and other universities. It is also being used at many companies such
+as NVIDIA, some startup companies, and by certain government agencies.
+
+The input to STP are formulas over the theory of bit-vectors and arrays (This
+theory captures most expressions from languages like C/C++/Java and Verilog),
+and the output of STP is a single bit of information that indicates whether
+the formula is satisfiable or not. If the input is satisfiable, then it also
+generates a variable assignment to satisfy the input formula.
+
+WWW:	http://people.csail.mit.edu/vganesh/STP_files/stp.html