ports/103412: [NEW PORT] math/cvcl: An automatic theorem prover for the SMT problem
Li-Wen Hsu
lwhsu at lwhsu.org
Wed Sep 20 00:20:23 UTC 2006
>Number: 103412
>Category: ports
>Synopsis: [NEW PORT] math/cvcl: An automatic theorem prover for the SMT problem
>Confidential: no
>Severity: non-critical
>Priority: low
>Responsible: freebsd-ports-bugs
>State: open
>Quarter:
>Keywords:
>Date-Required:
>Class: change-request
>Submitter-Id: current-users
>Arrival-Date: Wed Sep 20 00:20:20 GMT 2006
>Closed-Date:
>Last-Modified:
>Originator: Li-Wen Hsu
>Release: FreeBSD 6.1-STABLE i386
>Organization:
>Environment:
System: FreeBSD knight.lwhsu.ckefgisc.org 6.1-STABLE FreeBSD 6.1-STABLE #0: Thu Sep 7 14:15:03 CST
>Description:
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/
Generated with FreeBSD Port Tools 0.77
>How-To-Repeat:
>Fix:
--- cvcl-2.5.1.shar begins here ---
# This is a shell archive. Save it in a file, remove anything before
# this line, and then unpack it by entering "sh file". Note, it may
# create directories; files and directories will be owned by you and
# have default permissions.
#
# This archive contains:
#
# cvcl
# cvcl/pkg-descr
# cvcl/Makefile
# cvcl/pkg-plist
# cvcl/distinfo
#
echo c - cvcl
mkdir -p cvcl > /dev/null 2>&1
echo x - cvcl/pkg-descr
sed 's/^X//' >cvcl/pkg-descr << 'END-of-cvcl/pkg-descr'
XCVC Lite is an automatic theorem prover for the Satisfiability Modulo
XTheories (SMT) problem. Its features include: support for a variety of
Xtheories; interactive as well as C and C++ library interfaces; proof and
Xmodel generation abilities; predicate subtyping; and suppport for quantifiers.
XIn addition, there are essentially no limits on its use for research or
Xcommercial purposes (see license).
X
XWWW: http://www.cs.nyu.edu/acsys/cvcl/
END-of-cvcl/pkg-descr
echo x - cvcl/Makefile
sed 's/^X//' >cvcl/Makefile << 'END-of-cvcl/Makefile'
X# New ports collection makefile for: cvcl
X# Date created: 2006-09-15
X# Whom: Li-wen Hsu <lwhsu at lwhsu.org>
X#
X# $FreeBSD$
X#
X
XPORTNAME= cvcl
XPORTVERSION= 2.5.1
XCATEGORIES= math
XMASTER_SITES= http://www.cs.nyu.edu/acsys/cvcl/download/
X
XMAINTAINER= lwhsu at lwhsu.org
XCOMMENT= An automatic theorem prover for the SMT problem
X
XLIB_DEPENDS= gmp.7:${PORTSDIR}/math/libgmp4
X
XUSE_GMAKE= yes
XUSE_BISON= yes
XUSE_LDCONFIG= yes
X
XGNU_CONFIGURE= yes
XCONFIGURE_ARGS= --with-arith=gmp \
X --with-extra-libs=${LOCALBASE}/lib \
X --with-extra-includes=${LOCALBASE}/include \
X --with-build=optimized
X
XWRKSRC= ${WRKDIR}/cvcl-20060527
X
X.include <bsd.port.mk>
END-of-cvcl/Makefile
echo x - cvcl/pkg-plist
sed 's/^X//' >cvcl/pkg-plist << 'END-of-cvcl/pkg-plist'
Xbin/cvcl
Xinclude/cvcl/assumptions.h
Xinclude/cvcl/assumptions_value.h
Xinclude/cvcl/c_interface.h
Xinclude/cvcl/c_interface_defs.h
Xinclude/cvcl/cdflags.h
Xinclude/cvcl/cdlist.h
Xinclude/cvcl/cdmap.h
Xinclude/cvcl/cdmap_ordered.h
Xinclude/cvcl/cdo.h
Xinclude/cvcl/circuit.h
Xinclude/cvcl/clause.h
Xinclude/cvcl/cnf.h
Xinclude/cvcl/cnf_manager.h
Xinclude/cvcl/command_line_exception.h
Xinclude/cvcl/command_line_flags.h
Xinclude/cvcl/common_proof_rules.h
Xinclude/cvcl/compat_hash_map.h
Xinclude/cvcl/compat_hash_set.h
Xinclude/cvcl/context.h
Xinclude/cvcl/cvclutil.h
Xinclude/cvcl/debug.h
Xinclude/cvcl/dpllt.h
Xinclude/cvcl/dpllt_basic.h
Xinclude/cvcl/eval_exception.h
Xinclude/cvcl/exception.h
Xinclude/cvcl/expr.h
Xinclude/cvcl/expr_hash.h
Xinclude/cvcl/expr_manager.h
Xinclude/cvcl/expr_map.h
Xinclude/cvcl/expr_op.h
Xinclude/cvcl/expr_stream.h
Xinclude/cvcl/expr_transform.h
Xinclude/cvcl/expr_value.h
Xinclude/cvcl/fdstream.h
Xinclude/cvcl/kinds.h
Xinclude/cvcl/lang.h
Xinclude/cvcl/memory_manager.h
Xinclude/cvcl/memory_manager_chunks.h
Xinclude/cvcl/memory_manager_malloc.h
Xinclude/cvcl/notifylist.h
Xinclude/cvcl/parser.h
Xinclude/cvcl/proof.h
Xinclude/cvcl/rational.h
Xinclude/cvcl/parser_exception.h
Xinclude/cvcl/pretty_printer.h
Xinclude/cvcl/queryresult.h
Xinclude/cvcl/sat_api.h
Xinclude/cvcl/search.h
Xinclude/cvcl/search_impl_base.h
Xinclude/cvcl/search_sat.h
Xinclude/cvcl/search_simple.h
Xinclude/cvcl/search_fast.h
Xinclude/cvcl/smartcdo.h
Xinclude/cvcl/smtlib_exception.h
Xinclude/cvcl/sound_exception.h
Xinclude/cvcl/statistics.h
Xinclude/cvcl/theorem.h
Xinclude/cvcl/theorem_manager.h
Xinclude/cvcl/theorem_producer.h
Xinclude/cvcl/theory_arith.h
Xinclude/cvcl/theory_array.h
Xinclude/cvcl/theory_bitvector.h
Xinclude/cvcl/theory_core.h
Xinclude/cvcl/type.h
Xinclude/cvcl/theory_datatype.h
Xinclude/cvcl/theory_datatype_lazy.h
Xinclude/cvcl/theory.h
Xinclude/cvcl/theory_quant.h
Xinclude/cvcl/theory_records.h
Xinclude/cvcl/theory_simulate.h
Xinclude/cvcl/theory_uf.h
Xinclude/cvcl/translator.h
Xinclude/cvcl/typecheck_exception.h
Xinclude/cvcl/variable.h
Xinclude/cvcl/vc_cmd.h
Xinclude/cvcl/vc.h
Xinclude/cvcl/vcl.h
Xlib/libcvclite.a
Xlib/libcvclite.so
X at dirrm include/cvcl
END-of-cvcl/pkg-plist
echo x - cvcl/distinfo
sed 's/^X//' >cvcl/distinfo << 'END-of-cvcl/distinfo'
XMD5 (cvcl-2.5.1.tar.gz) = c41afb57e90438efa6e7360e330039f4
XSHA256 (cvcl-2.5.1.tar.gz) = a1a008816c170f3ddea6f513c6bbf11ed10f155b55431284ebad97dd26e61772
XSIZE (cvcl-2.5.1.tar.gz) = 689957
END-of-cvcl/distinfo
exit
--- cvcl-2.5.1.shar ends here ---
>Release-Note:
>Audit-Trail:
>Unformatted:
More information about the freebsd-ports-bugs
mailing list