Date: Wed, 20 Sep 2006 08:13:02 +0800 (CST) From: Li-Wen Hsu <lwhsu@lwhsu.org> To: FreeBSD-gnats-submit@FreeBSD.org Cc: lwhsu@lwhsu.org Subject: ports/103412: [NEW PORT] math/cvcl: An automatic theorem prover for the SMT problem Message-ID: <200609200013.k8K0D2AL055180@knight.lwhsu.ckefgisc.org> Resent-Message-ID: <200609200020.k8K0KLe8062961@freefall.freebsd.org>
next in thread | raw e-mail | index | archive | help
>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@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@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@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:
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?200609200013.k8K0D2AL055180>