add cvcl 2.5.1

An automatic theorem prover for the SMT problem

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

math/Makefile

@@ -38,6 +38,7 @@
     SUBDIR += concorde
     SUBDIR += convertall
     SUBDIR += coq
+    SUBDIR += cvcl
     SUBDIR += cxsc
     SUBDIR += dcdflib
     SUBDIR += diehard

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>

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

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/

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