diff options
author | Li-Wen Hsu <lwhsu@FreeBSD.org> | 2008-06-19 01:52:25 +0000 |
---|---|---|
committer | Li-Wen Hsu <lwhsu@FreeBSD.org> | 2008-06-19 01:52:25 +0000 |
commit | a8dcd66e6e78ad2bc9170889993e4bb74e1c2a28 (patch) | |
tree | 6ae36e979d0e8284845ce1aafeb55bcdf75f0bba /math/stp | |
parent | - Update to 2.0.0.72 (diff) |
Add stp , a Decision Procedure for Bitvectors and Arrays.
Notes
Notes:
svn path=/head/; revision=215221
Diffstat (limited to 'math/stp')
-rw-r--r-- | math/stp/Makefile | 41 | ||||
-rw-r--r-- | math/stp/distinfo | 3 | ||||
-rw-r--r-- | math/stp/pkg-descr | 14 |
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 |