5 files changed, 144 insertions, 0 deletions

diff --git a/math/Makefile b/math/Makefile
index 8f434e38951e..6d5dbbe7fe8f 100644
--- a/math/Makefile
+++ b/math/Makefile
@@ -38,6 +38,7 @@
     SUBDIR += concorde
     SUBDIR += convertall
     SUBDIR += coq
+    SUBDIR += cvc3
     SUBDIR += cvcl
     SUBDIR += cxsc
     SUBDIR += dcdflib
diff --git a/math/cvc3/Makefile b/math/cvc3/Makefile
new file mode 100644
index 000000000000..3428e2113e44
--- /dev/null
+++ b/math/cvc3/Makefile
@@ -0,0 +1,31 @@
+# New ports collection makefile for:	cvc3
+# Date created:		Mar. 24, 2007
+# Whom:			Li-Wen Hsu <lwhsu@lwhsu.org>
+#
+# $FreeBSD$
+#
+
+PORTNAME=	cvc3
+PORTVERSION=	1.0
+CATEGORIES=	math
+MASTER_SITES=	http://www.cs.nyu.edu/acsys/cvc3/download/${PORTVERSION}/ \
+		http://www.cs.nctu.edu.tw/~lwhsu/ports/distfiles/
+
+MAINTAINER=	lwhsu@lwhsu.org
+COMMENT=	An automatic theorem prover for the SMT problem
+
+LIB_DEPENDS=	gmp:${PORTSDIR}/math/libgmp4
+
+CONFIGURE_ARGS=	--enable-dynamic \
+		--with-arith=gmp \
+		--with-build=optimized \
+		--with-extra-includes=${LOCALBASE}/include \
+		--with-extra-libs=${LOCALBASE}/lib
+CXXFLAGS+=	-fPIC
+GNU_CONFIGURE=	yes
+USE_BISON=	yes
+USE_GMAKE=	yes
+USE_LDCONFIG=	yes
+USE_PERL5=	yes
+
+.include <bsd.port.mk>
diff --git a/math/cvc3/distinfo b/math/cvc3/distinfo
new file mode 100644
index 000000000000..f537a0307d66
--- /dev/null
+++ b/math/cvc3/distinfo
@@ -0,0 +1,3 @@
+MD5 (cvc3-1.0.tar.gz) = afe2e56b3002fd4dda73e68acda2e4a1
+SHA256 (cvc3-1.0.tar.gz) = 9a027f209471303751536133cc4643a3b14b975784e4c56cc47ca3c57ac15d0c
+SIZE (cvc3-1.0.tar.gz) = 756035
diff --git a/math/cvc3/pkg-descr b/math/cvc3/pkg-descr
new file mode 100644
index 000000000000..bba0e1374585
--- /dev/null
+++ b/math/cvc3/pkg-descr
@@ -0,0 +1,24 @@
+CVC3 is an automatic theorem prover for Satisfiability Modulo Theories (SMT)
+problems. It can be used to prove the validity (or, dually, the
+satisfiability) of first-order formulas in a large number of built-in logical
+theories and their combination.
+
+CVC3 is the last offspring of a series of popular SMT provers, which originated
+at Stanford University with the SVC system. In particular, it builds on the
+code base of CVC Lite, its most recent predecessor. Its high level design
+follows that of the Sammy prover.
+
+CVC3 works with a version of first-order logic with polymorphic types and has
+a wide variety of features including:
+  * several built-in base theories: rational and integer linear arithmetic,
+    arrays, tuples, records, inductive data types, bit vectors, and equality
+    over uninterpreted function symbols;
+  * support for quantifiers;
+  * an interactive text-based interface;
+  * a rich C and C++ API for embedding in other systems;
+  * proof and model generation abilities;
+  * predicate subtyping;
+  * essentially no limit on its use for research or commercial purposes
+    (see license). 
+
+WWW:	http://www.cs.nyu.edu/acsys/cvc3/
diff --git a/math/cvc3/pkg-plist b/math/cvc3/pkg-plist
new file mode 100644
index 000000000000..460675b1409e
--- /dev/null
+++ b/math/cvc3/pkg-plist
@@ -0,0 +1,85 @@
+bin/cvc3
+include/cvc3/assumptions.h
+include/cvc3/c_interface.h
+include/cvc3/c_interface_defs.h
+include/cvc3/cdflags.h
+include/cvc3/cdlist.h
+include/cvc3/cdmap.h
+include/cvc3/cdmap_ordered.h
+include/cvc3/cdo.h
+include/cvc3/circuit.h
+include/cvc3/clause.h
+include/cvc3/cnf.h
+include/cvc3/cnf_manager.h
+include/cvc3/command_line_exception.h
+include/cvc3/command_line_flags.h
+include/cvc3/common_proof_rules.h
+include/cvc3/compat_hash_map.h
+include/cvc3/compat_hash_set.h
+include/cvc3/context.h
+include/cvc3/cvc_util.h
+include/cvc3/debug.h
+include/cvc3/dpllt.h
+include/cvc3/dpllt_basic.h
+include/cvc3/dpllt_minisat.h
+include/cvc3/eval_exception.h
+include/cvc3/exception.h
+include/cvc3/expr.h
+include/cvc3/expr_hash.h
+include/cvc3/expr_manager.h
+include/cvc3/expr_map.h
+include/cvc3/expr_op.h
+include/cvc3/expr_stream.h
+include/cvc3/expr_transform.h
+include/cvc3/expr_value.h
+include/cvc3/fdstream.h
+include/cvc3/hash_fun.h
+include/cvc3/hash_map.h
+include/cvc3/hash_set.h
+include/cvc3/hash_table.h
+include/cvc3/kinds.h
+include/cvc3/lang.h
+include/cvc3/memory_manager.h
+include/cvc3/memory_manager_chunks.h
+include/cvc3/memory_manager_context.h
+include/cvc3/memory_manager_malloc.h
+include/cvc3/notifylist.h
+include/cvc3/parser.h
+include/cvc3/parser_exception.h
+include/cvc3/pretty_printer.h
+include/cvc3/proof.h
+include/cvc3/queryresult.h
+include/cvc3/rational.h
+include/cvc3/sat_api.h
+include/cvc3/search.h
+include/cvc3/search_fast.h
+include/cvc3/search_impl_base.h
+include/cvc3/search_sat.h
+include/cvc3/search_simple.h
+include/cvc3/smartcdo.h
+include/cvc3/smtlib_exception.h
+include/cvc3/sound_exception.h
+include/cvc3/statistics.h
+include/cvc3/theorem.h
+include/cvc3/theorem_manager.h
+include/cvc3/theorem_producer.h
+include/cvc3/theory.h
+include/cvc3/theory_arith.h
+include/cvc3/theory_array.h
+include/cvc3/theory_bitvector.h
+include/cvc3/theory_core.h
+include/cvc3/theory_datatype.h
+include/cvc3/theory_datatype_lazy.h
+include/cvc3/theory_quant.h
+include/cvc3/theory_records.h
+include/cvc3/theory_simulate.h
+include/cvc3/theory_uf.h
+include/cvc3/translator.h
+include/cvc3/type.h
+include/cvc3/typecheck_exception.h
+include/cvc3/variable.h
+include/cvc3/vc.h
+include/cvc3/vc_cmd.h
+include/cvc3/vcl.h
+lib/libcvc3.so
+@dirrm include/cvc3