aboutsummaryrefslogtreecommitdiff
path: root/math
diff options
context:
space:
mode:
authorCheng-Lung Sung <clsung@FreeBSD.org>2007-03-25 04:04:30 +0000
committerCheng-Lung Sung <clsung@FreeBSD.org>2007-03-25 04:04:30 +0000
commit8fdb6ad4aabf8fbcf397640ad243a18645bdbe7d (patch)
treef7a85fdc470aa635a16f1f24e39d308875ffbe45 /math
parent6801c3cafc8c4968ff96d0bd41ad2876ce7f34f8 (diff)
downloadports-8fdb6ad4aabf8fbcf397640ad243a18645bdbe7d.tar.gz
ports-8fdb6ad4aabf8fbcf397640ad243a18645bdbe7d.zip
Notes
Diffstat (limited to 'math')
-rw-r--r--math/Makefile1
-rw-r--r--math/cvc3/Makefile31
-rw-r--r--math/cvc3/distinfo3
-rw-r--r--math/cvc3/pkg-descr24
-rw-r--r--math/cvc3/pkg-plist85
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