diff options
| -rw-r--r-- | math/Makefile | 1 | ||||
| -rw-r--r-- | math/cvc3/Makefile | 31 | ||||
| -rw-r--r-- | math/cvc3/distinfo | 3 | ||||
| -rw-r--r-- | math/cvc3/pkg-descr | 24 | ||||
| -rw-r--r-- | math/cvc3/pkg-plist | 85 |
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 |