add cvcl 2.5.1

An automatic theorem prover for the SMT problem

PR:		103412
Submitted by:	Li-Wen Hsu <lwhsu@lwhsu.org>

5 files changed, 123 insertions, 0 deletions

diff --git a/math/Makefile b/math/Makefile
index 1146c0b75128..5e1039042d40 100644
--- a/math/Makefile
+++ b/math/Makefile
@@ -38,6 +38,7 @@
     SUBDIR += concorde
     SUBDIR += convertall
     SUBDIR += coq
+    SUBDIR += cvcl
     SUBDIR += cxsc
     SUBDIR += dcdflib
     SUBDIR += diehard
diff --git a/math/cvcl/Makefile b/math/cvcl/Makefile
new file mode 100644
index 000000000000..a085838fb9b2
--- /dev/null
+++ b/math/cvcl/Makefile
@@ -0,0 +1,30 @@
+# New ports collection makefile for:	cvcl
+# Date created:		2006-09-15
+# Whom:			Li-wen Hsu <lwhsu@lwhsu.org>
+#
+# $FreeBSD$
+#
+
+PORTNAME=	cvcl
+PORTVERSION=	2.5.1
+CATEGORIES=	math
+MASTER_SITES=	http://www.cs.nyu.edu/acsys/cvcl/download/
+
+MAINTAINER=	lwhsu@lwhsu.org
+COMMENT=	An automatic theorem prover for the SMT problem
+
+LIB_DEPENDS=	gmp.7:${PORTSDIR}/math/libgmp4
+
+USE_GMAKE=	yes
+USE_BISON=	yes
+USE_LDCONFIG=	yes
+
+GNU_CONFIGURE=	yes
+CONFIGURE_ARGS=	--with-arith=gmp \
+		--with-extra-libs=${LOCALBASE}/lib \
+		--with-extra-includes=${LOCALBASE}/include \
+		--with-build=optimized
+
+WRKSRC=	${WRKDIR}/cvcl-20060527
+
+.include <bsd.port.mk>
diff --git a/math/cvcl/distinfo b/math/cvcl/distinfo
new file mode 100644
index 000000000000..9a40b76b9e6a
--- /dev/null
+++ b/math/cvcl/distinfo
@@ -0,0 +1,3 @@
+MD5 (cvcl-2.5.1.tar.gz) = c41afb57e90438efa6e7360e330039f4
+SHA256 (cvcl-2.5.1.tar.gz) = a1a008816c170f3ddea6f513c6bbf11ed10f155b55431284ebad97dd26e61772
+SIZE (cvcl-2.5.1.tar.gz) = 689957
diff --git a/math/cvcl/pkg-descr b/math/cvcl/pkg-descr
new file mode 100644
index 000000000000..bd68d695f4d1
--- /dev/null
+++ b/math/cvcl/pkg-descr
@@ -0,0 +1,8 @@
+CVC Lite is an automatic theorem prover for the Satisfiability Modulo
+Theories (SMT) problem. Its features include: support for a variety of
+theories; interactive as well as C and C++ library interfaces; proof and
+model generation abilities; predicate subtyping; and suppport for quantifiers.
+In addition, there are essentially no limits on its use for research or
+commercial purposes (see license).
+
+WWW:	http://www.cs.nyu.edu/acsys/cvcl/
diff --git a/math/cvcl/pkg-plist b/math/cvcl/pkg-plist
new file mode 100644
index 000000000000..c82a2d7aa313
--- /dev/null
+++ b/math/cvcl/pkg-plist
@@ -0,0 +1,81 @@
+bin/cvcl
+include/cvcl/assumptions.h
+include/cvcl/assumptions_value.h
+include/cvcl/c_interface.h
+include/cvcl/c_interface_defs.h
+include/cvcl/cdflags.h
+include/cvcl/cdlist.h
+include/cvcl/cdmap.h
+include/cvcl/cdmap_ordered.h
+include/cvcl/cdo.h
+include/cvcl/circuit.h
+include/cvcl/clause.h
+include/cvcl/cnf.h
+include/cvcl/cnf_manager.h
+include/cvcl/command_line_exception.h
+include/cvcl/command_line_flags.h
+include/cvcl/common_proof_rules.h
+include/cvcl/compat_hash_map.h
+include/cvcl/compat_hash_set.h
+include/cvcl/context.h
+include/cvcl/cvclutil.h
+include/cvcl/debug.h
+include/cvcl/dpllt.h
+include/cvcl/dpllt_basic.h
+include/cvcl/eval_exception.h
+include/cvcl/exception.h
+include/cvcl/expr.h
+include/cvcl/expr_hash.h
+include/cvcl/expr_manager.h
+include/cvcl/expr_map.h
+include/cvcl/expr_op.h
+include/cvcl/expr_stream.h
+include/cvcl/expr_transform.h
+include/cvcl/expr_value.h
+include/cvcl/fdstream.h
+include/cvcl/kinds.h
+include/cvcl/lang.h
+include/cvcl/memory_manager.h
+include/cvcl/memory_manager_chunks.h
+include/cvcl/memory_manager_malloc.h
+include/cvcl/notifylist.h
+include/cvcl/parser.h
+include/cvcl/proof.h
+include/cvcl/rational.h
+include/cvcl/parser_exception.h
+include/cvcl/pretty_printer.h
+include/cvcl/queryresult.h
+include/cvcl/sat_api.h
+include/cvcl/search.h
+include/cvcl/search_impl_base.h
+include/cvcl/search_sat.h
+include/cvcl/search_simple.h
+include/cvcl/search_fast.h
+include/cvcl/smartcdo.h
+include/cvcl/smtlib_exception.h
+include/cvcl/sound_exception.h
+include/cvcl/statistics.h
+include/cvcl/theorem.h
+include/cvcl/theorem_manager.h
+include/cvcl/theorem_producer.h
+include/cvcl/theory_arith.h
+include/cvcl/theory_array.h
+include/cvcl/theory_bitvector.h
+include/cvcl/theory_core.h
+include/cvcl/type.h
+include/cvcl/theory_datatype.h
+include/cvcl/theory_datatype_lazy.h
+include/cvcl/theory.h
+include/cvcl/theory_quant.h
+include/cvcl/theory_records.h
+include/cvcl/theory_simulate.h
+include/cvcl/theory_uf.h
+include/cvcl/translator.h
+include/cvcl/typecheck_exception.h
+include/cvcl/variable.h
+include/cvcl/vc_cmd.h
+include/cvcl/vc.h
+include/cvcl/vcl.h
+lib/libcvclite.a
+lib/libcvclite.so
+@dirrm include/cvcl