initial commit

cvc3/DESCR

@@ -0,0 +1,4 @@
+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/Makefile

@@ -0,0 +1,25 @@
+# $NetBSD: Makefile,v 1.1 2011/05/23 19:05:26 marko_schuetz Exp $
+#
+
+DISTNAME=	cvc3-2.2
+CATEGORIES=	devel
+MASTER_SITES=	http://www.cs.nyu.edu/acsys/cvc3/releases/2.2/
+
+MAINTAINER=	MarkoSchuetz@web.de
+HOMEPAGE=	http://www.cs.nyu.edu/acsys/cvc3/releases/2.2/
+COMMENT=	Automatic theorem prover for SMT problems
+
+GNU_CONFIGURE=	yes
+USE_LANGUAGES=	c c++
+
+USE_TOOLS+=	gmake bash perl
+PKG_DESTDIR_SUPPORT=	user-destdir
+
+SUBST_CLASSES+=                 fix-bash
+SUBST_STAGE.fix-bash=          	pre-configure
+SUBST_MESSAGE.fix-bash=        	Fixing hard-coded reference to bash.
+SUBST_FILES.fix-bash=          	Makefile.std
+SUBST_SED.fix-bash=            	-e 's,SHELL = /bin/bash,SHELL = ${TOOLS_PATH.bash},g'
+
+.include "../../devel/gmp/buildlink3.mk"
+.include "../../mk/bsd.pkg.mk"

cvc3/PLIST

@@ -0,0 +1,91 @@
+@comment $NetBSD: PLIST,v 1.1 2011/05/23 19:05:26 marko_schuetz Exp $
+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/formula_value.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/os.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_arith3.h
+include/cvc3/theory_arith_new.h
+include/cvc3/theory_arith_old.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.a
+lib/libcvc3.a.2.1.1

cvc3/distinfo

@@ -0,0 +1,5 @@
+$NetBSD: distinfo,v 1.1 2011/05/23 19:05:26 marko_schuetz Exp $
+
+SHA1 (cvc3-2.2.tar.gz) = acb66f5237dc98e74da2d765d3c4d36ac3817151
+RMD160 (cvc3-2.2.tar.gz) = 404c9e6d4dfb0d3e14448fcd8ad82a95b8ac8b30
+Size (cvc3-2.2.tar.gz) = 1096987 bytes