Otter is an automated deduction system (theorem prover) for

first-order logic with equality developed at Argonne National
Laboratories.

WWW: http://www-unix.mcs.anl.gov/AR/otter/

PR:		ports/92834
Submitted by:	wollman

4 files changed, 385 insertions, 0 deletions

diff --git a/misc/otter/Makefile b/misc/otter/Makefile
new file mode 100644
index 00000000000..d0327233c7d
--- /dev/null
+++ b/misc/otter/Makefile
@@ -0,0 +1,38 @@
+# New ports collection makefile for:	otter
+# Date created:         2006-02-04
+# Whom:                 wollman
+#
+# $FreeBSD$
+#
+
+PORTNAME=	otter
+PORTVERSION=	3.3f
+CATEGORIES=	misc
+MASTER_SITES=	http://www-unix.mcs.anl.gov/AR/otter/dist33/
+
+MAINTAINER=	wollman@FreeBSD.org
+COMMENT=	A theorem prover and finite model searcher
+
+PROGRAMS=	anldp mace2 otter
+PORTDOCS=	README anldp.pdf mace2.pdf otter33.pdf
+
+post-patch:
+	@${REINPLACE_CMD} -e 's|CC=gcc|CC=$$(CC) CFLAGS="$$(CFLAGS)"|g' \
+		${WRKSRC}/Makefile
+
+do-install:
+.for prog in ${PROGRAMS}
+	${INSTALL_PROGRAM} ${WRKSRC}/bin/${prog} ${PREFIX}/bin
+.endfor
+.if !defined{NOPORTDOCS}
+	${MKDIR} ${DOCSDIR}
+.for doc in ${PORTDOCS}
+	${INSTALL_DATA} ${WRKSRC}/documents/${doc} ${DOCSDIR}
+.endfor
+.endif
+	${MKDIR} ${EXAMPLESDIR}
+	${MKDIR} ${PREFIX}/share/examples/mace2
+	(cd ${WRKSRC}/examples; ${PAX} -rw . ${EXAMPLESDIR})
+	(cd ${WRKSRC}/examples-mace2; ${PAX} -rw . ${PREFIX}/share/examples/mace2)
+
+.include <bsd.port.mk>
diff --git a/misc/otter/distinfo b/misc/otter/distinfo
new file mode 100644
index 00000000000..4153c4140b8
--- /dev/null
+++ b/misc/otter/distinfo
@@ -0,0 +1,3 @@
+MD5 (otter-3.3f.tar.gz) = 795711b307cc1316e08d3d4f46c998c9
+SHA256 (otter-3.3f.tar.gz) = 392c8c6557944eaf6958c199c365b43189beab836fb80c716569ea43af0dac9a
+SIZE (otter-3.3f.tar.gz) = 2554827
diff --git a/misc/otter/pkg-descr b/misc/otter/pkg-descr
new file mode 100644
index 00000000000..f121f8a3a14
--- /dev/null
+++ b/misc/otter/pkg-descr
@@ -0,0 +1,5 @@
+Otter is an automated deduction system (theorem prover) for
+first-order logic with equality developed at Argonne National
+Laboratories.
+
+WWW: http://www-unix.mcs.anl.gov/AR/otter/
diff --git a/misc/otter/pkg-plist b/misc/otter/pkg-plist
new file mode 100644
index 00000000000..1b53d7feaa3
--- /dev/null
+++ b/misc/otter/pkg-plist
@@ -0,0 +1,339 @@
+bin/anldp
+bin/mace2
+bin/otter
+%%EXAMPLESDIR%%/summary
+%%EXAMPLESDIR%%/Run_group
+%%EXAMPLESDIR%%/auto/robbins.out
+%%EXAMPLESDIR%%/auto/pigeon.in
+%%EXAMPLESDIR%%/auto/salt.in
+%%EXAMPLESDIR%%/auto/x2_quant.out
+%%EXAMPLESDIR%%/auto/lifsch.in
+%%EXAMPLESDIR%%/auto/mv25.out
+%%EXAMPLESDIR%%/auto/steam.in
+%%EXAMPLESDIR%%/auto/comm.in
+%%EXAMPLESDIR%%/auto/ring_x2.in
+%%EXAMPLESDIR%%/auto/tba_gg.in
+%%EXAMPLESDIR%%/auto/x2_quant.in
+%%EXAMPLESDIR%%/auto/w_sk.in
+%%EXAMPLESDIR%%/auto/z11.out
+%%EXAMPLESDIR%%/auto/pigeon.out
+%%EXAMPLESDIR%%/auto/comm.out
+%%EXAMPLESDIR%%/auto/salt.out
+%%EXAMPLESDIR%%/auto/lifsch.out
+%%EXAMPLESDIR%%/auto/sam.in
+%%EXAMPLESDIR%%/auto/steam.out
+%%EXAMPLESDIR%%/auto/wang1.in
+%%EXAMPLESDIR%%/auto/group.out
+%%EXAMPLESDIR%%/auto/cn19.out
+%%EXAMPLESDIR%%/auto/ec_yq.in
+%%EXAMPLESDIR%%/auto/ring_x2.out
+%%EXAMPLESDIR%%/auto/robbins.in
+%%EXAMPLESDIR%%/auto/ec_yq.out
+%%EXAMPLESDIR%%/auto/wang1.out
+%%EXAMPLESDIR%%/auto/w_sk.out
+%%EXAMPLESDIR%%/auto/group.in
+%%EXAMPLESDIR%%/auto/index.html
+%%EXAMPLESDIR%%/auto/README
+%%EXAMPLESDIR%%/auto/cn19.in
+%%EXAMPLESDIR%%/auto/z11.in
+%%EXAMPLESDIR%%/auto/sam.out
+%%EXAMPLESDIR%%/auto/tba_gg.out
+%%EXAMPLESDIR%%/auto/mv25.in
+%%EXAMPLESDIR%%/misc/sax1.in
+%%EXAMPLESDIR%%/misc/dem_alu.in
+%%EXAMPLESDIR%%/misc/sax2.in
+%%EXAMPLESDIR%%/misc/mv.in
+%%EXAMPLESDIR%%/misc/andrews.in
+%%EXAMPLESDIR%%/misc/dem_alu.out
+%%EXAMPLESDIR%%/misc/stage1.out
+%%EXAMPLESDIR%%/misc/str_bws.in.28752
+%%EXAMPLESDIR%%/misc/cn.in
+%%EXAMPLESDIR%%/misc/str_bws.in
+%%EXAMPLESDIR%%/misc/andrews.out
+%%EXAMPLESDIR%%/misc/kb_bench.in
+%%EXAMPLESDIR%%/misc/stage2.in
+%%EXAMPLESDIR%%/misc/dem_alu.in.28752
+%%EXAMPLESDIR%%/misc/andrews.in.28752
+%%EXAMPLESDIR%%/misc/cn.out
+%%EXAMPLESDIR%%/misc/stage2.out
+%%EXAMPLESDIR%%/misc/stage1.in
+%%EXAMPLESDIR%%/misc/mv.out
+%%EXAMPLESDIR%%/misc/index.html
+%%EXAMPLESDIR%%/misc/sax2.out
+%%EXAMPLESDIR%%/misc/README
+%%EXAMPLESDIR%%/misc/kb_bench.out
+%%EXAMPLESDIR%%/misc/mv.in.28752
+%%EXAMPLESDIR%%/misc/cn.in.28752
+%%EXAMPLESDIR%%/misc/str_bws.out
+%%EXAMPLESDIR%%/misc/sax1.out
+%%EXAMPLESDIR%%/misc/ec.out
+%%EXAMPLESDIR%%/misc/ec.in
+%%EXAMPLESDIR%%/Makefile
+%%EXAMPLESDIR%%/fringe/luka5h.out
+%%EXAMPLESDIR%%/fringe/lexical1.out
+%%EXAMPLESDIR%%/fringe/gl8.in
+%%EXAMPLESDIR%%/fringe/x3tricks.in
+%%EXAMPLESDIR%%/fringe/lexical2.in
+%%EXAMPLESDIR%%/fringe/if.in
+%%EXAMPLESDIR%%/fringe/lexical3.out
+%%EXAMPLESDIR%%/fringe/lexical2.out
+%%EXAMPLESDIR%%/fringe/mfl_13.out
+%%EXAMPLESDIR%%/fringe/gl8.out
+%%EXAMPLESDIR%%/fringe/mfl_13.in
+%%EXAMPLESDIR%%/fringe/gl4.out
+%%EXAMPLESDIR%%/fringe/rob_ocd.in
+%%EXAMPLESDIR%%/fringe/ec_yql.out
+%%EXAMPLESDIR%%/fringe/ec_yql.in.28897
+%%EXAMPLESDIR%%/fringe/rob_ocd.out
+%%EXAMPLESDIR%%/fringe/x3tricks.out
+%%EXAMPLESDIR%%/fringe/olsax_hints.in
+%%EXAMPLESDIR%%/fringe/bring.out
+%%EXAMPLESDIR%%/fringe/index.html
+%%EXAMPLESDIR%%/fringe/if.out
+%%EXAMPLESDIR%%/fringe/gl4.in.28897
+%%EXAMPLESDIR%%/fringe/gl4.in
+%%EXAMPLESDIR%%/fringe/README
+%%EXAMPLESDIR%%/fringe/luka5h.in
+%%EXAMPLESDIR%%/fringe/lexical1.in
+%%EXAMPLESDIR%%/fringe/bring.in
+%%EXAMPLESDIR%%/fringe/lexical3.in
+%%EXAMPLESDIR%%/fringe/ec_yql.in
+%%EXAMPLESDIR%%/fringe/olsax_hints.out
+%%EXAMPLESDIR%%/wos/grp_exp4.in
+%%EXAMPLESDIR%%/wos/grp_exp3.in
+%%EXAMPLESDIR%%/wos/cursory.in
+%%EXAMPLESDIR%%/wos/cursory.out
+%%EXAMPLESDIR%%/wos/twoval.in
+%%EXAMPLESDIR%%/wos/README.more
+%%EXAMPLESDIR%%/wos/rigorous.out
+%%EXAMPLESDIR%%/wos/grp_exp4.out
+%%EXAMPLESDIR%%/wos/rigorous.in
+%%EXAMPLESDIR%%/wos/rob_occ.in
+%%EXAMPLESDIR%%/wos/index.html
+%%EXAMPLESDIR%%/wos/rob_occ.out
+%%EXAMPLESDIR%%/wos/manyval.out
+%%EXAMPLESDIR%%/wos/README
+%%EXAMPLESDIR%%/wos/manyval.in
+%%EXAMPLESDIR%%/wos/twoval.out
+%%EXAMPLESDIR%%/wos/grp_exp3.out
+%%EXAMPLESDIR%%/Loop/temp
+%%EXAMPLESDIR%%/Loop/otter-ploop
+%%EXAMPLESDIR%%/Loop/Sheffer-mgi-without-mirrors
+%%EXAMPLESDIR%%/Loop/README
+%%EXAMPLESDIR%%/Loop/head
+%%EXAMPLESDIR%%/ivy/group-x2-refute.out
+%%EXAMPLESDIR%%/ivy/group-comm.out
+%%EXAMPLESDIR%%/ivy/lifsch.in
+%%EXAMPLESDIR%%/ivy/steam.in
+%%EXAMPLESDIR%%/ivy/group-x2.out
+%%EXAMPLESDIR%%/ivy/comb-sk-w.out
+%%EXAMPLESDIR%%/ivy/lifsch.out
+%%EXAMPLESDIR%%/ivy/p-and-not-p.in
+%%EXAMPLESDIR%%/ivy/p-and-not-p.out
+%%EXAMPLESDIR%%/ivy/steam.out
+%%EXAMPLESDIR%%/ivy/cd-cn19.out
+%%EXAMPLESDIR%%/ivy/t1.out
+%%EXAMPLESDIR%%/ivy/group-comm.in
+%%EXAMPLESDIR%%/ivy/comb-sk-w.in
+%%EXAMPLESDIR%%/ivy/group-x2-refute.in
+%%EXAMPLESDIR%%/ivy/group-x2.in
+%%EXAMPLESDIR%%/ivy/index.html
+%%EXAMPLESDIR%%/ivy/README
+%%EXAMPLESDIR%%/ivy/cd-cn19.in
+%%EXAMPLESDIR%%/ivy/t1.in
+%%EXAMPLESDIR%%/index.html
+%%EXAMPLESDIR%%/README
+%%EXAMPLESDIR%%/program/mission.in
+%%EXAMPLESDIR%%/program/jugs.out
+%%EXAMPLESDIR%%/program/queens.in
+%%EXAMPLESDIR%%/program/jugs.in
+%%EXAMPLESDIR%%/program/two_inv.in
+%%EXAMPLESDIR%%/program/two_inv.out
+%%EXAMPLESDIR%%/program/eval.out
+%%EXAMPLESDIR%%/program/mission.out
+%%EXAMPLESDIR%%/program/queens.out
+%%EXAMPLESDIR%%/program/index.html
+%%EXAMPLESDIR%%/program/README
+%%EXAMPLESDIR%%/program/eval.in
+%%EXAMPLESDIR%%/Run_all
+%%EXAMPLESDIR%%/Run_all.out
+%%EXAMPLESDIR%%/kalman/i4.in
+%%EXAMPLESDIR%%/kalman/ex_1.out
+%%EXAMPLESDIR%%/kalman/i1.in
+%%EXAMPLESDIR%%/kalman/ex_4.in
+%%EXAMPLESDIR%%/kalman/ex_3.out
+%%EXAMPLESDIR%%/kalman/ex_2.out
+%%EXAMPLESDIR%%/kalman/i3.out
+%%EXAMPLESDIR%%/kalman/ex_2.in
+%%EXAMPLESDIR%%/kalman/ex_4.out
+%%EXAMPLESDIR%%/kalman/ex_3.in
+%%EXAMPLESDIR%%/kalman/ex_1.in
+%%EXAMPLESDIR%%/kalman/i4.out
+%%EXAMPLESDIR%%/kalman/i3.in
+%%EXAMPLESDIR%%/kalman/index.html
+%%EXAMPLESDIR%%/kalman/i1.out
+%%EXAMPLESDIR%%/kalman/README
+%%EXAMPLESDIR%%/kalman/i2.in
+%%EXAMPLESDIR%%/kalman/i2.out
+%%EXAMPLESDIR%%/split/GEO010-2.in
+%%EXAMPLESDIR%%/split/wang3.out
+%%EXAMPLESDIR%%/split/group2.in
+%%EXAMPLESDIR%%/split/power.out
+%%EXAMPLESDIR%%/split/GEO036-2.out
+%%EXAMPLESDIR%%/split/zebra4.out
+%%EXAMPLESDIR%%/split/pigeon5.in
+%%EXAMPLESDIR%%/split/GEO036-2.in
+%%EXAMPLESDIR%%/split/wang3.in
+%%EXAMPLESDIR%%/split/zebra2.in
+%%EXAMPLESDIR%%/split/README.more
+%%EXAMPLESDIR%%/split/noncomm-group.out
+%%EXAMPLESDIR%%/split/pigeon5.out
+%%EXAMPLESDIR%%/split/power.in
+%%EXAMPLESDIR%%/split/GRP025-1.out
+%%EXAMPLESDIR%%/split/noncomm-group.in
+%%EXAMPLESDIR%%/split/zebra4.in
+%%EXAMPLESDIR%%/split/temp1
+%%EXAMPLESDIR%%/split/group2.out
+%%EXAMPLESDIR%%/split/index.html
+%%EXAMPLESDIR%%/split/README
+%%EXAMPLESDIR%%/split/pair.out
+%%EXAMPLESDIR%%/split/pair.in
+%%EXAMPLESDIR%%/split/zebra2.out
+%%EXAMPLESDIR%%/split/GRP025-1.in
+%%EXAMPLESDIR%%/split/GEO010-2.out
+share/examples/mace2/Run_mace
+share/examples/mace2/Makefile
+share/examples/mace2/basic/temp
+share/examples/mace2/basic/cl_sw.out
+share/examples/mace2/basic/cd.in
+share/examples/mace2/basic/tough-nut.out
+share/examples/mace2/basic/cl_ql.in
+share/examples/mace2/basic/tba.in
+share/examples/mace2/basic/noncommutative_group.in
+share/examples/mace2/basic/cd.out
+share/examples/mace2/basic/tba.out
+share/examples/mace2/basic/ordered_semi.in
+share/examples/mace2/basic/index.html
+share/examples/mace2/basic/README
+share/examples/mace2/basic/tough-nut.in
+share/examples/mace2/basic/cl_ql.out
+share/examples/mace2/basic/ring.in
+share/examples/mace2/basic/cl_sw.in
+share/examples/mace2/basic/program
+share/examples/mace2/basic/ring.out
+share/examples/mace2/basic/noncommutative_group.out
+share/examples/mace2/basic/ordered_semi.out
+share/examples/mace2/iterate/CAT019-5.out
+share/examples/mace2/iterate/PUZ001-3.in
+share/examples/mace2/iterate/LAT025-1.in
+share/examples/mace2/iterate/LCL136-1.out
+share/examples/mace2/iterate/RNG025-8.in
+share/examples/mace2/iterate/noncommutive_ring1.out
+share/examples/mace2/iterate/noncommutive_ring1.in
+share/examples/mace2/iterate/CAT019-5.in
+share/examples/mace2/iterate/cd.in
+share/examples/mace2/iterate/noncommutative_group.in
+share/examples/mace2/iterate/cd.out
+share/examples/mace2/iterate/PUZ001-3.out
+share/examples/mace2/iterate/BOO032-1.in
+share/examples/mace2/iterate/index.html
+share/examples/mace2/iterate/README
+share/examples/mace2/iterate/BOO032-1.out
+share/examples/mace2/iterate/kauer.out
+share/examples/mace2/iterate/program
+share/examples/mace2/iterate/LCL136-1.in
+share/examples/mace2/iterate/kauer.in
+share/examples/mace2/iterate/LAT025-1.out
+share/examples/mace2/iterate/RNG025-8.out
+share/examples/mace2/iterate/noncommutative_group.out
+share/examples/mace2/propositional/p8.out
+share/examples/mace2/propositional/p10.IN
+share/examples/mace2/propositional/p7.out
+share/examples/mace2/propositional/f3.out
+share/examples/mace2/propositional/p9.out
+share/examples/mace2/propositional/p6.in
+share/examples/mace2/propositional/p6.out
+share/examples/mace2/propositional/README.more
+share/examples/mace2/propositional/p9.in
+share/examples/mace2/propositional/q10.in
+share/examples/mace2/propositional/f4.out
+share/examples/mace2/propositional/f2.in
+share/examples/mace2/propositional/f2.out
+share/examples/mace2/propositional/p5.out
+share/examples/mace2/propositional/index.html
+share/examples/mace2/propositional/README
+share/examples/mace2/propositional/q10.out
+share/examples/mace2/propositional/p8.in
+share/examples/mace2/propositional/p5.in
+share/examples/mace2/propositional/f4.in
+share/examples/mace2/propositional/program
+share/examples/mace2/propositional/f3.in
+share/examples/mace2/propositional/p7.in
+share/examples/mace2/lattice/lt-ol.out
+share/examples/mace2/lattice/ml-mol.out
+share/examples/mace2/lattice/ol-e4.out
+share/examples/mace2/lattice/oml-mol.in
+share/examples/mace2/lattice/ol-oml.in
+share/examples/mace2/lattice/oml-mol.out
+share/examples/mace2/lattice/lt-ml.out
+share/examples/mace2/lattice/lt-ol.in
+share/examples/mace2/lattice/finite-lattice
+share/examples/mace2/lattice/ortholattice
+share/examples/mace2/lattice/lattice-axioms
+share/examples/mace2/lattice/ol-e1.out
+share/examples/mace2/lattice/ol-oml.out
+share/examples/mace2/lattice/ml-mol.in
+share/examples/mace2/lattice/index.html
+share/examples/mace2/lattice/README
+share/examples/mace2/lattice/mol-ba.out
+share/examples/mace2/lattice/ol-e1.in
+share/examples/mace2/lattice/mol-ba.in
+share/examples/mace2/lattice/program
+share/examples/mace2/lattice/ol-e4.in
+share/examples/mace2/lattice/lt-ml.in
+share/examples/mace2/index.html
+share/examples/mace2/README
+share/examples/mace2/quasigroup/qg7bl.in
+share/examples/mace2/quasigroup/qg6.in
+share/examples/mace2/quasigroup/qg4.out
+share/examples/mace2/quasigroup/qg1d.out
+share/examples/mace2/quasigroup/omts9.in
+share/examples/mace2/quasigroup/qg3.in
+share/examples/mace2/quasigroup/qg5l.out
+share/examples/mace2/quasigroup/qg3.out
+share/examples/mace2/quasigroup/omts9.out
+share/examples/mace2/quasigroup/qg1d.in
+share/examples/mace2/quasigroup/qg7bl.out
+share/examples/mace2/quasigroup/index.html
+share/examples/mace2/quasigroup/qg6.out
+share/examples/mace2/quasigroup/README
+share/examples/mace2/quasigroup/qg5l.in
+share/examples/mace2/quasigroup/program
+share/examples/mace2/quasigroup/qg4.in
+share/examples/mace2/quasigroup/qg2d.in
+share/examples/mace2/quasigroup/qg2d.out
+share/examples/mace2/Run_all
+share/examples/mace2/Run_all.out
+share/examples/mace2/Run_anldp
+share/examples/mace2/Perl-examples/Sheffer-mgi-without-mirrors
+share/examples/mace2/Perl-examples/commute4_filter
+share/examples/mace2/Perl-examples/index.html
+share/examples/mace2/Perl-examples/README
+share/examples/mace2/Perl-examples/candidates
+@dirrm %%EXAMPLESDIR%%/auto
+@dirrm %%EXAMPLESDIR%%/misc
+@dirrm %%EXAMPLESDIR%%/fringe
+@dirrm %%EXAMPLESDIR%%/wos
+@dirrm %%EXAMPLESDIR%%/Loop
+@dirrm %%EXAMPLESDIR%%/ivy
+@dirrm %%EXAMPLESDIR%%/program
+@dirrm %%EXAMPLESDIR%%/kalman
+@dirrm %%EXAMPLESDIR%%/split
+@dirrm %%EXAMPLESDIR%%
+@dirrm share/examples/mace2/basic
+@dirrm share/examples/mace2/iterate
+@dirrm share/examples/mace2/propositional
+@dirrm share/examples/mace2/lattice
+@dirrm share/examples/mace2/quasigroup
+@dirrm share/examples/mace2/Perl-examples
+@dirrm share/examples/mace2