diff options
author | Ying-Chieh Liao <ijliao@FreeBSD.org> | 2006-09-20 01:42:03 +0000 |
---|---|---|
committer | Ying-Chieh Liao <ijliao@FreeBSD.org> | 2006-09-20 01:42:03 +0000 |
commit | d15a699539cd70ffb4677c0945536f1b1b590ab6 (patch) | |
tree | 57faa90de1164c2011c4f221016905860e89b3f2 /math | |
parent | Make fetchable (diff) |
add cvcl 2.5.1
An automatic theorem prover for the SMT problem
PR: 103412
Submitted by: Li-Wen Hsu <lwhsu@lwhsu.org>
Notes
Notes:
svn path=/head/; revision=173419
Diffstat (limited to 'math')
-rw-r--r-- | math/Makefile | 1 | ||||
-rw-r--r-- | math/cvcl/Makefile | 30 | ||||
-rw-r--r-- | math/cvcl/distinfo | 3 | ||||
-rw-r--r-- | math/cvcl/pkg-descr | 8 | ||||
-rw-r--r-- | math/cvcl/pkg-plist | 81 |
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 |