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