initial commit

alt-ergo/DESCR

@@ -0,0 +1,6 @@
+Alt-Ergo is an automatic theorem prover dedicated to program
+verification. Alt-Ergo is based on CC(X) a congruence closure algorithm
+parameterized by an equational theory X. Currently, CC(X) can be instantiated
+by the empty equational theory and by the linear arithmetics. Alt-Ergo
+contains also a home made SAT-solver and an instantiation mechanism. Its
+architecture is summarized by the the following picture.

alt-ergo/Makefile

@@ -0,0 +1,23 @@
+# $NetBSD: Makefile,v 1.1 2011/05/21 19:14:41 marko_schuetz Exp $
+#
+
+DISTNAME=	alt-ergo-0.93
+CATEGORIES=	devel
+MASTER_SITES=	http://ergo.lri.fr/http/
+
+MAINTAINER=	MarkoSchuetz@web.de
+HOMEPAGE=	http://ergo.lri.fr/http/
+COMMENT=	Automatic theorem prover for program verification
+
+USE_TOOLS+=	gmake
+PKG_DESTDIR_SUPPORT=	user-destdir
+
+GNU_CONFIGURE=	yes
+USE_LANGUAGES=	c
+
+
+.include "../../lang/ocaml/buildlink3.mk"
+.include "../../wip/ocamlgraph/buildlink3.mk"
+.include "../../devel/nspr/buildlink3.mk"
+.include "../../x11/lablgtk/buildlink3.mk"
+.include "../../mk/bsd.pkg.mk"

alt-ergo/PLIST

@@ -0,0 +1,4 @@
+@comment $NetBSD: PLIST,v 1.1 2011/05/21 19:14:41 marko_schuetz Exp $
+bin/alt-ergo
+lib/alt-ergo/smt_prelude.mlw
+man/man1/alt-ergo.1

alt-ergo/distinfo

@@ -0,0 +1,5 @@
+$NetBSD: distinfo,v 1.1 2011/05/21 19:14:41 marko_schuetz Exp $
+
+SHA1 (alt-ergo-0.93.tar.gz) = b1ac27fab7812590e5e2fd3ee5d795b599429577
+RMD160 (alt-ergo-0.93.tar.gz) = fd1f7f1f75f0d1392343e7a73d25b391ad083bae
+Size (alt-ergo-0.93.tar.gz) = 178783 bytes