diff options
| author | Heinz Wiesinger <pprkut@liwjatan.at> | 2010-05-13 00:20:07 +0200 |
|---|---|---|
| committer | Erik Hanson <erik@slackbuilds.org> | 2010-05-13 00:20:07 +0200 |
| commit | 060d2498f52279d67d50754863fe0f6d0191ef4e (patch) | |
| tree | 62264dcd8d552eb79b1bf039ed261d3d972f713c | |
| parent | fbbff75475642643a58cf8be8d0d576e81a61339 (diff) | |
academic/ladr: Updated for version 2009_11A
| -rw-r--r-- | academic/ladr/ladr-libtoolize.diff | 161 | ||||
| -rw-r--r-- | academic/ladr/ladr.SlackBuild | 19 | ||||
| -rw-r--r-- | academic/ladr/ladr.info | 12 | ||||
| -rw-r--r-- | academic/ladr/slack-desc | 4 |
4 files changed, 113 insertions, 83 deletions
diff --git a/academic/ladr/ladr-libtoolize.diff b/academic/ladr/ladr-libtoolize.diff index 9eddee96d94bc..015de6d8303b2 100644 --- a/academic/ladr/ladr-libtoolize.diff +++ b/academic/ladr/ladr-libtoolize.diff @@ -1,6 +1,6 @@ -diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/Makefile LADR-2008-09A/Makefile ---- LADR-2008-09A-orig/Makefile 2007-10-22 23:33:12.000000000 +0200 -+++ LADR-2008-09A/Makefile 2008-10-19 15:55:32.270034513 +0200 +diff -U 3 -H -b -E -d -r -N -- LADR-2009-11A.orig/Makefile LADR-2009-11A/Makefile +--- LADR-2009-11A.orig/Makefile 2007-10-22 23:33:12.000000000 +0200 ++++ LADR-2009-11A/Makefile 2009-12-26 13:50:32.285406118 +0100 @@ -2,7 +2,7 @@ @echo See README.make @@ -19,9 +19,9 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/Makefile LADR-2008-09A/Make test1: bin/prover9 -f prover9.examples/x2.in | bin/prooftrans parents_only -diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/apps.src/Makefile LADR-2008-09A/apps.src/Makefile ---- LADR-2008-09A-orig/apps.src/Makefile 2008-07-10 00:45:29.000000000 +0200 -+++ LADR-2008-09A/apps.src/Makefile 2008-10-19 15:55:32.330034747 +0200 +diff -U 3 -H -b -E -d -r -N -- LADR-2009-11A.orig/apps.src/Makefile LADR-2009-11A/apps.src/Makefile +--- LADR-2009-11A.orig/apps.src/Makefile 2009-04-17 16:46:39.000000000 +0200 ++++ LADR-2009-11A/apps.src/Makefile 2009-12-26 13:50:32.335405804 +0100 @@ -16,16 +16,16 @@ all: ladr apps install realclean @@ -43,7 +43,7 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/apps.src/Makefile LADR-2008 tags: etags *.c ../ladr/*.c -@@ -33,73 +33,73 @@ +@@ -33,85 +33,85 @@ apps: $(PROGRAMS) test: test.o @@ -66,6 +66,14 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/apps.src/Makefile LADR-2008 - $(CC) $(CFLAGS) -o test_clause_eval test_clause_eval.o ../ladr/libladr.a + libtool --mode=link $(CC) $(CFLAGS) -o test_clause_eval test_clause_eval.o ../ladr/libladr.la + test_complex: test_complex.o +- $(CC) $(CFLAGS) -o test_complex test_complex.o ../ladr/libladr.a ++ libtool --mode=link $(CC) $(CFLAGS) -o test_complex test_complex.o ../ladr/libladr.la + + complex: complex.o +- $(CC) $(CFLAGS) -o complex complex.o ../ladr/libladr.a ++ libtool --mode=link $(CC) $(CFLAGS) -o complex complex.o ../ladr/libladr.la + latfilter: latfilter.o - $(CC) $(CFLAGS) -o latfilter latfilter.o ../ladr/libladr.a + libtool --mode=link $(CC) $(CFLAGS) -o latfilter latfilter.o ../ladr/libladr.la @@ -138,11 +146,19 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/apps.src/Makefile LADR-2008 - $(CC) $(CFLAGS) -o sigtest sigtest.o ../ladr/libladr.a + libtool --mode=link $(CC) $(CFLAGS) -o sigtest sigtest.o ../ladr/libladr.la + rewriter2: rewriter2.o +- $(CC) $(CFLAGS) -o rewriter2 rewriter2.o ../ladr/libladr.a ++ libtool --mode=link $(CC) $(CFLAGS) -o rewriter2 rewriter2.o ../ladr/libladr.la + + gen_trc_defs: gen_trc_defs.o +- $(CC) $(CFLAGS) -o gen_trc_defs gen_trc_defs.o ../ladr/libladr.a ++ libtool --mode=link $(CC) $(CFLAGS) -o gen_trc_defs gen_trc_defs.o ../ladr/libladr.la + -diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/ladr/Makefile LADR-2008-09A/ladr/Makefile ---- LADR-2008-09A-orig/ladr/Makefile 2008-08-15 02:11:36.000000000 +0200 -+++ LADR-2008-09A/ladr/Makefile 2008-10-19 15:55:32.435034921 +0200 +diff -U 3 -H -b -E -d -r -N -- LADR-2009-11A.orig/ladr/Makefile LADR-2009-11A/ladr/Makefile +--- LADR-2009-11A.orig/ladr/Makefile 2009-10-28 15:22:04.000000000 +0100 ++++ LADR-2009-11A/ladr/Makefile 2009-12-26 13:50:32.453408456 +0100 @@ -11,46 +11,49 @@ # CFLAGS = $(XFLAGS) -pg -O -Wall # CFLAGS = $(XFLAGS) -Wall -pedantic @@ -160,8 +176,8 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/ladr/Makefile LADR-2008-09A - pindex.o compress.o\ - maximal.o lindex.o weight.o weight2.o\ - int_code.o features.o di_tree.o fastparse.o\ -- random.o subsume.o clause_misc.o clause_eval.o --INFE_OBJ = flatdemod.o demod.o clash.o resolve.o paramod.o\ +- random.o subsume.o clause_misc.o clause_eval.o complex.o +-INFE_OBJ = dollar.o flatdemod.o demod.o clash.o resolve.o paramod.o\ - backdemod.o\ - hints.o ac_redun.o xproofs.o ivy.o -MODL_OBJ = interp.o @@ -179,8 +195,8 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/ladr/Makefile LADR-2008-09A + pindex.lo compress.lo\ + maximal.lo lindex.lo weight.lo weight2.lo\ + int_code.lo features.lo di_tree.lo fastparse.lo\ -+ random.lo subsume.lo clause_misc.lo clause_eval.lo -+INFE_OBJ = flatdemod.lo demod.lo clash.lo resolve.lo paramod.lo\ ++ random.lo subsume.lo clause_misc.lo clause_eval.lo complex.lo ++INFE_OBJ = dollar.lo flatdemod.lo demod.lo clash.lo resolve.lo paramod.lo\ + backdemod.lo\ + hints.lo ac_redun.lo xproofs.lo ivy.lo +MODL_OBJ = interp.lo @@ -217,7 +233,7 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/ladr/Makefile LADR-2008-09A protos: util/make_protos $(OBJECTS) -@@ -67,150 +70,150 @@ +@@ -67,156 +70,156 @@ # The rest of the file is generated automatically by util/make_dep @@ -287,47 +303,47 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/ladr/Makefile LADR-2008-09A -accanon.o: accanon.h termflag.h termorder.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h +accanon.lo: accanon.h termflag.h termorder.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h --unify.o: unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h -+unify.lo: unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h +-unify.o: unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h ++unify.lo: unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h -fpalist.o: fpalist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h +fpalist.lo: fpalist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h --fpa.o: fpa.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h -+fpa.lo: fpa.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h +-fpa.o: fpa.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h ++fpa.lo: fpa.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h --discrim.o: discrim.h unify.h index.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h -+discrim.lo: discrim.h unify.h index.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h +-discrim.o: discrim.h unify.h index.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h ++discrim.lo: discrim.h unify.h index.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h --discrimb.o: discrimb.h discrim.h unify.h index.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h -+discrimb.lo: discrimb.h discrim.h unify.h index.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h +-discrimb.o: discrimb.h discrim.h unify.h index.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h ++discrimb.lo: discrimb.h discrim.h unify.h index.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h --discrimw.o: discrimw.h discrim.h unify.h index.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h -+discrimw.lo: discrimw.h discrim.h unify.h index.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h +-discrimw.o: discrimw.h discrim.h unify.h index.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h ++discrimw.lo: discrimw.h discrim.h unify.h index.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h -dioph.o: dioph.h +dioph.lo: dioph.h --btu.o: btu.h dioph.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h -+btu.lo: btu.h dioph.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h +-btu.o: btu.h dioph.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h ++btu.lo: btu.h dioph.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h --btm.o: btm.h unify.h accanon.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h termflag.h termorder.h flatterm.h -+btm.lo: btm.h unify.h accanon.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h termflag.h termorder.h flatterm.h +-btm.o: btm.h unify.h accanon.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h termorder.h flatterm.h ++btm.lo: btm.h unify.h accanon.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h termorder.h flatterm.h --mindex.o: mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h -+mindex.lo: mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h +-mindex.o: mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h ++mindex.lo: mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h -basic.o: basic.h unify.h termflag.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h +basic.lo: basic.h unify.h termflag.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h --attrib.o: attrib.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h -+attrib.lo: attrib.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h +-attrib.o: attrib.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h ++attrib.lo: attrib.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h --formula.o: formula.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h -+formula.lo: formula.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h +-formula.o: formula.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h ++formula.lo: formula.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h --definitions.o: definitions.h formula.h topform.h clauseid.h just.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h literals.h maximal.h termflag.h parse.h -+definitions.lo: definitions.h formula.h topform.h clauseid.h just.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h literals.h maximal.h termflag.h parse.h +-definitions.o: definitions.h formula.h topform.h clauseid.h just.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h literals.h maximal.h parse.h ++definitions.lo: definitions.h formula.h topform.h clauseid.h just.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h literals.h maximal.h parse.h -literals.o: literals.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h +literals.lo: literals.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h @@ -347,8 +363,8 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/ladr/Makefile LADR-2008-09A -just.o: just.h clauseid.h parse.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h +just.lo: just.h clauseid.h parse.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h --cnf.o: cnf.h formula.h clock.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h -+cnf.lo: cnf.h formula.h clock.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h +-cnf.o: cnf.h formula.h clock.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h ++cnf.lo: cnf.h formula.h clock.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h -clausify.o: clausify.h topform.h cnf.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h clock.h +clausify.lo: clausify.h topform.h cnf.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h clock.h @@ -365,12 +381,15 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/ladr/Makefile LADR-2008-09A -maximal.o: maximal.h literals.h termorder.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h +maximal.lo: maximal.h literals.h termorder.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h --lindex.o: lindex.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h -+lindex.lo: lindex.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h +-lindex.o: lindex.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h ++lindex.lo: lindex.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h -weight.o: weight.h literals.h unify.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h listterm.h +weight.lo: weight.h literals.h unify.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h listterm.h +-weight2.o: weight2.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h ++weight2.lo: weight2.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h + -int_code.o: int_code.h just.h ibuffer.h clauseid.h parse.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h +int_code.lo: int_code.h just.h ibuffer.h clauseid.h parse.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h @@ -386,8 +405,8 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/ladr/Makefile LADR-2008-09A -random.o: random.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h +random.lo: random.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h --subsume.o: subsume.h parautil.h lindex.h features.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h -+subsume.lo: subsume.h parautil.h lindex.h features.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h +-subsume.o: subsume.h parautil.h lindex.h features.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h ++subsume.lo: subsume.h parautil.h lindex.h features.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h -clause_misc.o: clause_misc.h clist.h mindex.h just.h basic.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h parse.h +clause_misc.lo: clause_misc.h clist.h mindex.h just.h basic.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h parse.h @@ -395,26 +414,32 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/ladr/Makefile LADR-2008-09A -clause_eval.o: clause_eval.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h +clause_eval.lo: clause_eval.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h --flatdemod.o: flatdemod.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h -+flatdemod.lo: flatdemod.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h +-complex.o: complex.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h ++complex.lo: complex.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h + +-dollar.o: dollar.h clist.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h ++dollar.lo: dollar.h clist.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h + +-flatdemod.o: flatdemod.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h ++flatdemod.lo: flatdemod.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h --demod.o: demod.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h -+demod.lo: demod.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h +-demod.o: demod.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h ++demod.lo: demod.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h --clash.o: clash.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h -+clash.lo: clash.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h +-clash.o: clash.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h ++clash.lo: clash.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h --resolve.o: resolve.h clash.h lindex.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h maximal.h topform.h literals.h tlist.h attrib.h formula.h hash.h -+resolve.lo: resolve.h clash.h lindex.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h maximal.h topform.h literals.h tlist.h attrib.h formula.h hash.h +-resolve.o: resolve.h clash.h lindex.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h maximal.h topform.h literals.h tlist.h attrib.h formula.h hash.h ++resolve.lo: resolve.h clash.h lindex.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h maximal.h topform.h literals.h tlist.h attrib.h formula.h hash.h --paramod.o: paramod.h resolve.h basic.h clash.h lindex.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h maximal.h topform.h literals.h tlist.h attrib.h formula.h hash.h -+paramod.lo: paramod.h resolve.h basic.h clash.h lindex.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h maximal.h topform.h literals.h tlist.h attrib.h formula.h hash.h +-paramod.o: paramod.h resolve.h basic.h clash.h lindex.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h maximal.h topform.h literals.h tlist.h attrib.h formula.h hash.h ++paramod.lo: paramod.h resolve.h basic.h clash.h lindex.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h maximal.h topform.h literals.h tlist.h attrib.h formula.h hash.h --backdemod.o: backdemod.h demod.h clist.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h topform.h literals.h attrib.h formula.h maximal.h tlist.h hash.h -+backdemod.lo: backdemod.h demod.h clist.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h topform.h literals.h attrib.h formula.h maximal.h tlist.h hash.h +-backdemod.o: backdemod.h demod.h clist.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h topform.h literals.h attrib.h formula.h maximal.h tlist.h hash.h ++backdemod.lo: backdemod.h demod.h clist.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h topform.h literals.h attrib.h formula.h maximal.h tlist.h hash.h --hints.o: hints.h subsume.h clist.h backdemod.h resolve.h parautil.h lindex.h features.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h demod.h clash.h -+hints.lo: hints.h subsume.h clist.h backdemod.h resolve.h parautil.h lindex.h features.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h demod.h clash.h +-hints.o: hints.h subsume.h clist.h backdemod.h resolve.h parautil.h lindex.h features.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h demod.h clash.h ++hints.lo: hints.h subsume.h clist.h backdemod.h resolve.h parautil.h lindex.h features.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h demod.h clash.h -ac_redun.o: ac_redun.h parautil.h accanon.h termflag.h termorder.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h +ac_redun.lo: ac_redun.h parautil.h accanon.h termflag.h termorder.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h @@ -442,10 +467,10 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/ladr/Makefile LADR-2008-09A -top_input.o: top_input.h ioutil.h std_options.h tptp_trans.h parse.h fastparse.h ivy.h clausify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h unify.h termorder.h hash.h flatterm.h xproofs.h clauses.h clause_misc.h paramod.h subsume.h clist.h mindex.h just.h basic.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h resolve.h clash.h lindex.h parautil.h features.h cnf.h clock.h options.h +top_input.lo: top_input.h ioutil.h std_options.h tptp_trans.h parse.h fastparse.h ivy.h clausify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h unify.h termorder.h hash.h flatterm.h xproofs.h clauses.h clause_misc.h paramod.h subsume.h clist.h mindex.h just.h basic.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h resolve.h clash.h lindex.h parautil.h features.h cnf.h clock.h options.h -diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/mace4.src/Makefile LADR-2008-09A/mace4.src/Makefile ---- LADR-2008-09A-orig/mace4.src/Makefile 2008-07-10 00:38:20.000000000 +0200 -+++ LADR-2008-09A/mace4.src/Makefile 2008-10-19 15:55:32.376034420 +0200 -@@ -25,11 +25,11 @@ +diff -U 3 -H -b -E -d -r -N -- LADR-2009-11A.orig/mace4.src/Makefile LADR-2009-11A/mace4.src/Makefile +--- LADR-2009-11A.orig/mace4.src/Makefile 2009-04-17 16:46:46.000000000 +0200 ++++ LADR-2009-11A/mace4.src/Makefile 2009-12-26 13:50:32.373406096 +0100 +@@ -26,11 +26,11 @@ $(MAKE) libmace4.a ladr: @@ -459,7 +484,7 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/mace4.src/Makefile LADR-200 $(OBJECTS): estack.h syms.h ground.h propagate.h mstate.h msearch.h -@@ -37,10 +37,10 @@ +@@ -38,10 +38,10 @@ etags *.c ../ladr/*.c clean: @@ -473,9 +498,9 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/mace4.src/Makefile LADR-200 install: - /bin/mv mace4 ../bin + libtool --mode=install /bin/cp mace4 `pwd`/../bin -diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/provers.src/Makefile LADR-2008-09A/provers.src/Makefile ---- LADR-2008-09A-orig/provers.src/Makefile 2008-08-18 21:12:56.000000000 +0200 -+++ LADR-2008-09A/provers.src/Makefile 2008-10-19 15:55:32.434034496 +0200 +diff -U 3 -H -b -E -d -r -N -- LADR-2009-11A.orig/provers.src/Makefile LADR-2009-11A/provers.src/Makefile +--- LADR-2009-11A.orig/provers.src/Makefile 2009-10-28 15:22:15.000000000 +0100 ++++ LADR-2009-11A/provers.src/Makefile 2009-12-26 13:50:32.420530288 +0100 @@ -41,13 +41,13 @@ $(MAKE) clean @@ -538,9 +563,9 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/provers.src/Makefile LADR-2 prover9.o mprover.o iterate4.o autosketches4.o fof-prover9.o: search.h utilities.h forward_subsume.h giv_select.h white_black.h demodulate.h actions.h index_lits.h pred_elim.h unfold.h provers.h -diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/test.src/Makefile LADR-2008-09A/test.src/Makefile ---- LADR-2008-09A-orig/test.src/Makefile 2007-03-06 21:27:59.000000000 +0100 -+++ LADR-2008-09A/test.src/Makefile 2008-10-19 15:55:32.425034393 +0200 +diff -U 3 -H -b -E -d -r -N -- LADR-2009-11A.orig/test.src/Makefile LADR-2009-11A/test.src/Makefile +--- LADR-2009-11A.orig/test.src/Makefile 2007-03-06 21:27:59.000000000 +0100 ++++ LADR-2009-11A/test.src/Makefile 2009-12-26 13:50:32.416531165 +0100 @@ -17,13 +17,13 @@ ladr: diff --git a/academic/ladr/ladr.SlackBuild b/academic/ladr/ladr.SlackBuild index 2b88462210ac6..352f01c14dca0 100644 --- a/academic/ladr/ladr.SlackBuild +++ b/academic/ladr/ladr.SlackBuild @@ -2,7 +2,7 @@ # Slackware build script for ladr -# Copyright 2007-2008 Heinz Wiesinger <pprkut@liwjatan.at> +# Copyright 2007-2010 Heinz Wiesinger, Amsterdam, The Netherlands # All rights reserved. # # Redistribution and use of this script, with or without modification, is @@ -23,7 +23,7 @@ # ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. PRGNAM=ladr -VERSION=2008_09A +VERSION=2009_11A ARCH=${ARCH:-i486} BUILD=${BUILD:-1} TAG=${TAG:-_SBo} @@ -38,10 +38,13 @@ SRC_VERSION=$(echo $VERSION | tr _ -) if [ "$ARCH" = "i486" ]; then SLKCFLAGS="-O2 -march=i486 -mtune=i686" + LIBDIRSUFFIX="" elif [ "$ARCH" = "i686" ]; then SLKCFLAGS="-O2 -march=i686 -mtune=i686" + LIBDIRSUFFIX="" elif [ "$ARCH" = "x86_64" ]; then SLKCFLAGS="-O2 -fPIC" + LIBDIRSUFFIX="64" fi set -e @@ -65,12 +68,12 @@ patch -p1 -i $CWD/ladr-libtoolize.diff XFLAGS="$SLKCFLAGS" make all MAKEFLAGS="-j1" -mkdir -p $PKG/usr/{bin,lib} +mkdir -p $PKG/usr/{bin,lib$LIBDIRSUFFIX} install -m 0755 ./bin/* $PKG/usr/bin/ -install -m 0755 ./ladr/libladr.la $PKG/usr/lib/ -install -m 0755 ./ladr/.libs/libladr.so.4.0.0 $PKG/usr/lib/ -ln -s /usr/lib/libladr.so.4.0.0 $PKG/usr/lib/libladr.so.4 -ln -s /usr/lib/libladr.so.4.0.0 $PKG/usr/lib/libladr.so +install -m 0755 ./ladr/libladr.la $PKG/usr/lib$LIBDIRSUFFIX/ +install -m 0755 ./ladr/.libs/libladr.so.4.0.0 $PKG/usr/lib$LIBDIRSUFFIX/ +ln -s /usr/lib$LIBDIRSUFFIX/libladr.so.4.0.0 $PKG/usr/lib$LIBDIRSUFFIX/libladr.so.4 +ln -s /usr/lib$LIBDIRSUFFIX/libladr.so.4.0.0 $PKG/usr/lib$LIBDIRSUFFIX/libladr.so rm -f $PKG/usr/bin/proof3fo.xsl chmod 755 $PKG/usr/bin/gvizify @@ -94,4 +97,4 @@ mkdir -p $PKG/install cat $CWD/slack-desc > $PKG/install/slack-desc cd $PKG -/sbin/makepkg -l y -c n $OUTPUT/$PRGNAM-$VERSION-$ARCH-$BUILD$TAG.tgz +/sbin/makepkg -l y -c n $OUTPUT/$PRGNAM-$VERSION-$ARCH-$BUILD$TAG.${PKGTYPE:-tgz} diff --git a/academic/ladr/ladr.info b/academic/ladr/ladr.info index 8c7a1ae4cdc25..e3b7be7be0d3f 100644 --- a/academic/ladr/ladr.info +++ b/academic/ladr/ladr.info @@ -1,8 +1,10 @@ PRGNAM="ladr" -VERSION="2008_09A" +VERSION="2009_11A" HOMEPAGE="http://www.cs.unm.edu/~mccune/prover9/" -DOWNLOAD="http://www.cs.unm.edu/~mccune/prover9/download/LADR-2008-09A.tar.gz" -MD5SUM="96cc67eae8f485c22d01449fd2639dae" -MAINTAINER="ppr:kut" +DOWNLOAD="http://www.cs.unm.edu/~mccune/prover9/download/LADR-2009-11A.tar.gz" +MD5SUM="ab409f31ecbb4410b1c7d75deadea2c6" +DOWNLOAD_x86_64="" +MD5SUM_x86_64="" +MAINTAINER="Heinz Wiesinger" EMAIL="pprkut@liwjatan.at" -APPROVED="Michiel" +APPROVED="Erik Hanson" diff --git a/academic/ladr/slack-desc b/academic/ladr/slack-desc index 0e9a2a4d73c80..7939499621c03 100644 --- a/academic/ladr/slack-desc +++ b/academic/ladr/slack-desc @@ -5,11 +5,11 @@ # make exactly 11 lines for the formatting to be correct. It's also # customary to leave one space after the ':'. - |-----handy-ruler------------------------------------------------------| + |-----handy-ruler-------------------------------------------------------| ladr: ladr (Mathematical Programs) ladr: ladr: LADR includes some mathematical programs like -ladr: - prover 9 (automated theorem prover for first-order and equational +ladr: - prover 9 (automated theorem prover for first-order and equational ladr: logic) ladr: - mace4 (search for finite models and counterexamples) ladr: |