commit 9c88f730d5e8e99bf0ceea3ed8fbf5add2df4baf Author: David Baer Date: Sat Apr 22 15:35:18 2017 -0400 Initial check in. diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..2891f44 --- /dev/null +++ b/.gitignore @@ -0,0 +1,52 @@ +#### joe made this: http://goel.io/joe + +#####=== Autotools ===##### + +# http://www.gnu.org/software/automake + +Makefile.in + +# http://www.gnu.org/software/autoconf + +/autom4te.cache +/aclocal.m4 +/compile +/configure +/depcomp +/install-sh +/missing +/stamp-h1 + +#####=== C++ ===##### + +# Compiled Object files +*.slo +*.lo +*.o +*.obj + +# Precompiled Headers +*.gch +*.pch + +# Compiled Dynamic libraries +*.so +*.dylib +*.dll + +# Fortran module files +*.mod + +# Compiled Static libraries +*.lai +*.la +*.a +*.lib + +# Executables +*.exe +*.out +*.app + +/scratch +/src/.deps diff --git a/COPYING b/COPYING new file mode 100644 index 0000000..3c1b715 --- /dev/null +++ b/COPYING @@ -0,0 +1,33 @@ +Lionheart +Copyright © 2000 David A. Baer +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + +1. Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + +2. Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + +3. All advertising materials mentioning features or use of this software + must display the following acknowledgement: + This product includes software developed by the organization. + +4. Neither the name of the organization nor the + names of its contributors may be used to endorse or promote products + derived from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY David A. Baer ''AS IS'' AND ANY +EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED +WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL David A. Baer BE LIABLE FOR ANY +DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES +(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; +LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND +ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + diff --git a/INSTALL b/INSTALL new file mode 120000 index 0000000..601bc09 --- /dev/null +++ b/INSTALL @@ -0,0 +1 @@ +/usr/local/share/automake-1.15/INSTALL \ No newline at end of file diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..af57a91 --- /dev/null +++ b/Makefile @@ -0,0 +1,823 @@ +# Makefile.in generated by automake 1.15 from Makefile.am. +# Makefile. Generated from Makefile.in by configure. + +# Copyright (C) 1994-2014 Free Software Foundation, Inc. + +# This Makefile.in is free software; the Free Software Foundation +# gives unlimited permission to copy and/or distribute it, +# with or without modifications, as long as this notice is preserved. + +# This program is distributed in the hope that it will be useful, +# but WITHOUT ANY WARRANTY, to the extent permitted by law; without +# even the implied warranty of MERCHANTABILITY or FITNESS FOR A +# PARTICULAR PURPOSE. + + + + +am__is_gnu_make = { \ + if test -z '$(MAKELEVEL)'; then \ + false; \ + elif test -n '$(MAKE_HOST)'; then \ + true; \ + elif test -n '$(MAKE_VERSION)' && test -n '$(CURDIR)'; then \ + true; \ + else \ + false; \ + fi; \ +} +am__make_running_with_option = \ + case $${target_option-} in \ + ?) ;; \ + *) echo "am__make_running_with_option: internal error: invalid" \ + "target option '$${target_option-}' specified" >&2; \ + exit 1;; \ + esac; \ + has_opt=no; \ + sane_makeflags=$$MAKEFLAGS; \ + if $(am__is_gnu_make); then \ + sane_makeflags=$$MFLAGS; \ + else \ + case $$MAKEFLAGS in \ + *\\[\ \ ]*) \ + bs=\\; \ + sane_makeflags=`printf '%s\n' "$$MAKEFLAGS" \ + | sed "s/$$bs$$bs[$$bs $$bs ]*//g"`;; \ + esac; \ + fi; \ + skip_next=no; \ + strip_trailopt () \ + { \ + flg=`printf '%s\n' "$$flg" | sed "s/$$1.*$$//"`; \ + }; \ + for flg in $$sane_makeflags; do \ + test $$skip_next = yes && { skip_next=no; continue; }; \ + case $$flg in \ + *=*|--*) continue;; \ + -*I) strip_trailopt 'I'; skip_next=yes;; \ + -*I?*) strip_trailopt 'I';; \ + -*O) strip_trailopt 'O'; skip_next=yes;; \ + -*O?*) strip_trailopt 'O';; \ + -*l) strip_trailopt 'l'; skip_next=yes;; \ + -*l?*) strip_trailopt 'l';; \ + -[dEDm]) skip_next=yes;; \ + -[JT]) skip_next=yes;; \ + esac; \ + case $$flg in \ + *$$target_option*) has_opt=yes; break;; \ + esac; \ + done; \ + test $$has_opt = yes +am__make_dryrun = (target_option=n; $(am__make_running_with_option)) +am__make_keepgoing = (target_option=k; $(am__make_running_with_option)) +pkgdatadir = $(datadir)/lionheart +pkgincludedir = $(includedir)/lionheart +pkglibdir = $(libdir)/lionheart +pkglibexecdir = $(libexecdir)/lionheart +am__cd = CDPATH="$${ZSH_VERSION+.}$(PATH_SEPARATOR)" && cd +install_sh_DATA = $(install_sh) -c -m 644 +install_sh_PROGRAM = $(install_sh) -c +install_sh_SCRIPT = $(install_sh) -c +INSTALL_HEADER = $(INSTALL_DATA) +transform = $(program_transform_name) +NORMAL_INSTALL = : +PRE_INSTALL = : +POST_INSTALL = : +NORMAL_UNINSTALL = : +PRE_UNINSTALL = : +POST_UNINSTALL = : +subdir = . +ACLOCAL_M4 = $(top_srcdir)/aclocal.m4 +am__aclocal_m4_deps = $(top_srcdir)/configure.ac +am__configure_deps = $(am__aclocal_m4_deps) $(CONFIGURE_DEPENDENCIES) \ + $(ACLOCAL_M4) +DIST_COMMON = $(srcdir)/Makefile.am $(top_srcdir)/configure \ + $(am__configure_deps) $(dist_doc_DATA) $(am__DIST_COMMON) +am__CONFIG_DISTCLEAN_FILES = config.status config.cache config.log \ + configure.lineno config.status.lineno +mkinstalldirs = $(install_sh) -d +CONFIG_HEADER = config.h +CONFIG_CLEAN_FILES = +CONFIG_CLEAN_VPATH_FILES = +AM_V_P = $(am__v_P_$(V)) +am__v_P_ = $(am__v_P_$(AM_DEFAULT_VERBOSITY)) +am__v_P_0 = false +am__v_P_1 = : +AM_V_GEN = $(am__v_GEN_$(V)) +am__v_GEN_ = $(am__v_GEN_$(AM_DEFAULT_VERBOSITY)) +am__v_GEN_0 = @echo " GEN " $@; +am__v_GEN_1 = +AM_V_at = $(am__v_at_$(V)) +am__v_at_ = $(am__v_at_$(AM_DEFAULT_VERBOSITY)) +am__v_at_0 = @ +am__v_at_1 = +SOURCES = +DIST_SOURCES = +RECURSIVE_TARGETS = all-recursive check-recursive cscopelist-recursive \ + ctags-recursive dvi-recursive html-recursive info-recursive \ + install-data-recursive install-dvi-recursive \ + install-exec-recursive install-html-recursive \ + install-info-recursive install-pdf-recursive \ + install-ps-recursive install-recursive installcheck-recursive \ + installdirs-recursive pdf-recursive ps-recursive \ + tags-recursive uninstall-recursive +am__can_run_installinfo = \ + case $$AM_UPDATE_INFO_DIR in \ + n|no|NO) false;; \ + *) (install-info --version) >/dev/null 2>&1;; \ + esac +am__vpath_adj_setup = srcdirstrip=`echo "$(srcdir)" | sed 's|.|.|g'`; +am__vpath_adj = case $$p in \ + $(srcdir)/*) f=`echo "$$p" | sed "s|^$$srcdirstrip/||"`;; \ + *) f=$$p;; \ + esac; +am__strip_dir = f=`echo $$p | sed -e 's|^.*/||'`; +am__install_max = 40 +am__nobase_strip_setup = \ + srcdirstrip=`echo "$(srcdir)" | sed 's/[].[^$$\\*|]/\\\\&/g'` +am__nobase_strip = \ + for p in $$list; do echo "$$p"; done | sed -e "s|$$srcdirstrip/||" +am__nobase_list = $(am__nobase_strip_setup); \ + for p in $$list; do echo "$$p $$p"; done | \ + sed "s| $$srcdirstrip/| |;"' / .*\//!s/ .*/ ./; s,\( .*\)/[^/]*$$,\1,' | \ + $(AWK) 'BEGIN { files["."] = "" } { files[$$2] = files[$$2] " " $$1; \ + if (++n[$$2] == $(am__install_max)) \ + { print $$2, files[$$2]; n[$$2] = 0; files[$$2] = "" } } \ + END { for (dir in files) print dir, files[dir] }' +am__base_list = \ + sed '$$!N;$$!N;$$!N;$$!N;$$!N;$$!N;$$!N;s/\n/ /g' | \ + sed '$$!N;$$!N;$$!N;$$!N;s/\n/ /g' +am__uninstall_files_from_dir = { \ + test -z "$$files" \ + || { test ! -d "$$dir" && test ! -f "$$dir" && test ! -r "$$dir"; } \ + || { echo " ( cd '$$dir' && rm -f" $$files ")"; \ + $(am__cd) "$$dir" && rm -f $$files; }; \ + } +am__installdirs = "$(DESTDIR)$(docdir)" +DATA = $(dist_doc_DATA) +RECURSIVE_CLEAN_TARGETS = mostlyclean-recursive clean-recursive \ + distclean-recursive maintainer-clean-recursive +am__recursive_targets = \ + $(RECURSIVE_TARGETS) \ + $(RECURSIVE_CLEAN_TARGETS) \ + $(am__extra_recursive_targets) +AM_RECURSIVE_TARGETS = $(am__recursive_targets:-recursive=) TAGS CTAGS \ + cscope distdir dist dist-all distcheck +am__tagged_files = $(HEADERS) $(SOURCES) $(TAGS_FILES) \ + $(LISP)config.h.in +# Read a list of newline-separated strings from the standard input, +# and print each of them once, without duplicates. Input order is +# *not* preserved. +am__uniquify_input = $(AWK) '\ + BEGIN { nonempty = 0; } \ + { items[$$0] = 1; nonempty = 1; } \ + END { if (nonempty) { for (i in items) print i; }; } \ +' +# Make sure the list of sources is unique. This is necessary because, +# e.g., the same source file might be shared among _SOURCES variables +# for different programs/libraries. +am__define_uniq_tagged_files = \ + list='$(am__tagged_files)'; \ + unique=`for i in $$list; do \ + if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \ + done | $(am__uniquify_input)` +ETAGS = etags +CTAGS = ctags +CSCOPE = cscope +DIST_SUBDIRS = $(SUBDIRS) +am__DIST_COMMON = $(srcdir)/Makefile.in $(srcdir)/config.h.in COPYING \ + INSTALL README compile depcomp install-sh missing +DISTFILES = $(DIST_COMMON) $(DIST_SOURCES) $(TEXINFOS) $(EXTRA_DIST) +distdir = $(PACKAGE)-$(VERSION) +top_distdir = $(distdir) +am__remove_distdir = \ + if test -d "$(distdir)"; then \ + find "$(distdir)" -type d ! -perm -200 -exec chmod u+w {} ';' \ + && rm -rf "$(distdir)" \ + || { sleep 5 && rm -rf "$(distdir)"; }; \ + else :; fi +am__post_remove_distdir = $(am__remove_distdir) +am__relativize = \ + dir0=`pwd`; \ + sed_first='s,^\([^/]*\)/.*$$,\1,'; \ + sed_rest='s,^[^/]*/*,,'; \ + sed_last='s,^.*/\([^/]*\)$$,\1,'; \ + sed_butlast='s,/*[^/]*$$,,'; \ + while test -n "$$dir1"; do \ + first=`echo "$$dir1" | sed -e "$$sed_first"`; \ + if test "$$first" != "."; then \ + if test "$$first" = ".."; then \ + dir2=`echo "$$dir0" | sed -e "$$sed_last"`/"$$dir2"; \ + dir0=`echo "$$dir0" | sed -e "$$sed_butlast"`; \ + else \ + first2=`echo "$$dir2" | sed -e "$$sed_first"`; \ + if test "$$first2" = "$$first"; then \ + dir2=`echo "$$dir2" | sed -e "$$sed_rest"`; \ + else \ + dir2="../$$dir2"; \ + fi; \ + dir0="$$dir0"/"$$first"; \ + fi; \ + fi; \ + dir1=`echo "$$dir1" | sed -e "$$sed_rest"`; \ + done; \ + reldir="$$dir2" +DIST_ARCHIVES = $(distdir).tar.gz +GZIP_ENV = --best +DIST_TARGETS = dist-gzip +distuninstallcheck_listfiles = find . -type f -print +am__distuninstallcheck_listfiles = $(distuninstallcheck_listfiles) \ + | sed 's|^\./|$(prefix)/|' | grep -v '$(infodir)/dir$$' +distcleancheck_listfiles = find . -type f -print +ACLOCAL = ${SHELL} /home/david/devel/cpp/lionheart000916/missing aclocal-1.15 +AMTAR = $${TAR-tar} +AM_DEFAULT_VERBOSITY = 1 +AUTOCONF = ${SHELL} /home/david/devel/cpp/lionheart000916/missing autoconf +AUTOHEADER = ${SHELL} /home/david/devel/cpp/lionheart000916/missing autoheader +AUTOMAKE = ${SHELL} /home/david/devel/cpp/lionheart000916/missing automake-1.15 +AWK = gawk +CC = gcc +CCDEPMODE = depmode=gcc3 +CFLAGS = -g -O2 +CPP = gcc -E +CPPFLAGS = +CXX = g++ +CXXDEPMODE = depmode=gcc3 +CXXFLAGS = -g -O2 +CYGPATH_W = echo +DEFS = -DHAVE_CONFIG_H +DEPDIR = .deps +ECHO_C = +ECHO_N = -n +ECHO_T = +EGREP = /usr/bin/grep -E +EXEEXT = +GREP = /usr/bin/grep +INSTALL = /usr/bin/install -c +INSTALL_DATA = ${INSTALL} -m 644 +INSTALL_PROGRAM = ${INSTALL} +INSTALL_SCRIPT = ${INSTALL} +INSTALL_STRIP_PROGRAM = $(install_sh) -c -s +LDFLAGS = +LIBOBJS = +LIBS = +LTLIBOBJS = +MAKEINFO = ${SHELL} /home/david/devel/cpp/lionheart000916/missing makeinfo +MKDIR_P = /usr/local/bin/gmkdir -p +OBJEXT = o +PACKAGE = lionheart +PACKAGE_BUGREPORT = +PACKAGE_NAME = lionheart +PACKAGE_STRING = lionheart 20000916 +PACKAGE_TARNAME = lionheart +PACKAGE_URL = +PACKAGE_VERSION = 20000916 +PATH_SEPARATOR = : +SET_MAKE = +SHELL = /bin/sh +STRIP = +VERSION = 20000916 +abs_builddir = /home/david/devel/cpp/lionheart000916 +abs_srcdir = /home/david/devel/cpp/lionheart000916 +abs_top_builddir = /home/david/devel/cpp/lionheart000916 +abs_top_srcdir = /home/david/devel/cpp/lionheart000916 +ac_ct_CC = gcc +ac_ct_CXX = g++ +am__include = include +am__leading_dot = . +am__quote = +am__tar = $${TAR-tar} chof - "$$tardir" +am__untar = $${TAR-tar} xf - +bindir = ${exec_prefix}/bin +build_alias = +builddir = . +datadir = ${datarootdir} +datarootdir = ${prefix}/share +docdir = ${datarootdir}/doc/${PACKAGE_TARNAME} +dvidir = ${docdir} +exec_prefix = ${prefix} +host_alias = +htmldir = ${docdir} +includedir = ${prefix}/include +infodir = ${datarootdir}/info +install_sh = ${SHELL} /home/david/devel/cpp/lionheart000916/install-sh +libdir = ${exec_prefix}/lib +libexecdir = ${exec_prefix}/libexec +localedir = ${datarootdir}/locale +localstatedir = ${prefix}/var +mandir = ${datarootdir}/man +mkdir_p = $(MKDIR_P) +oldincludedir = /usr/include +pdfdir = ${docdir} +prefix = /usr/local +program_transform_name = s,x,x, +psdir = ${docdir} +sbindir = ${exec_prefix}/sbin +sharedstatedir = ${prefix}/com +srcdir = . +sysconfdir = ${prefix}/etc +target_alias = +top_build_prefix = +top_builddir = . +top_srcdir = . +SUBDIRS = src +dist_doc_DATA = README +all: config.h + $(MAKE) $(AM_MAKEFLAGS) all-recursive + +.SUFFIXES: +am--refresh: Makefile + @: +$(srcdir)/Makefile.in: $(srcdir)/Makefile.am $(am__configure_deps) + @for dep in $?; do \ + case '$(am__configure_deps)' in \ + *$$dep*) \ + echo ' cd $(srcdir) && $(AUTOMAKE) --foreign'; \ + $(am__cd) $(srcdir) && $(AUTOMAKE) --foreign \ + && exit 0; \ + exit 1;; \ + esac; \ + done; \ + echo ' cd $(top_srcdir) && $(AUTOMAKE) --foreign Makefile'; \ + $(am__cd) $(top_srcdir) && \ + $(AUTOMAKE) --foreign Makefile +Makefile: $(srcdir)/Makefile.in $(top_builddir)/config.status + @case '$?' in \ + *config.status*) \ + echo ' $(SHELL) ./config.status'; \ + $(SHELL) ./config.status;; \ + *) \ + echo ' cd $(top_builddir) && $(SHELL) ./config.status $@ $(am__depfiles_maybe)'; \ + cd $(top_builddir) && $(SHELL) ./config.status $@ $(am__depfiles_maybe);; \ + esac; + +$(top_builddir)/config.status: $(top_srcdir)/configure $(CONFIG_STATUS_DEPENDENCIES) + $(SHELL) ./config.status --recheck + +$(top_srcdir)/configure: $(am__configure_deps) + $(am__cd) $(srcdir) && $(AUTOCONF) +$(ACLOCAL_M4): $(am__aclocal_m4_deps) + $(am__cd) $(srcdir) && $(ACLOCAL) $(ACLOCAL_AMFLAGS) +$(am__aclocal_m4_deps): + +config.h: stamp-h1 + @test -f $@ || rm -f stamp-h1 + @test -f $@ || $(MAKE) $(AM_MAKEFLAGS) stamp-h1 + +stamp-h1: $(srcdir)/config.h.in $(top_builddir)/config.status + @rm -f stamp-h1 + cd $(top_builddir) && $(SHELL) ./config.status config.h +$(srcdir)/config.h.in: $(am__configure_deps) + ($(am__cd) $(top_srcdir) && $(AUTOHEADER)) + rm -f stamp-h1 + touch $@ + +distclean-hdr: + -rm -f config.h stamp-h1 +install-dist_docDATA: $(dist_doc_DATA) + @$(NORMAL_INSTALL) + @list='$(dist_doc_DATA)'; test -n "$(docdir)" || list=; \ + if test -n "$$list"; then \ + echo " $(MKDIR_P) '$(DESTDIR)$(docdir)'"; \ + $(MKDIR_P) "$(DESTDIR)$(docdir)" || exit 1; \ + fi; \ + for p in $$list; do \ + if test -f "$$p"; then d=; else d="$(srcdir)/"; fi; \ + echo "$$d$$p"; \ + done | $(am__base_list) | \ + while read files; do \ + echo " $(INSTALL_DATA) $$files '$(DESTDIR)$(docdir)'"; \ + $(INSTALL_DATA) $$files "$(DESTDIR)$(docdir)" || exit $$?; \ + done + +uninstall-dist_docDATA: + @$(NORMAL_UNINSTALL) + @list='$(dist_doc_DATA)'; test -n "$(docdir)" || list=; \ + files=`for p in $$list; do echo $$p; done | sed -e 's|^.*/||'`; \ + dir='$(DESTDIR)$(docdir)'; $(am__uninstall_files_from_dir) + +# This directory's subdirectories are mostly independent; you can cd +# into them and run 'make' without going through this Makefile. +# To change the values of 'make' variables: instead of editing Makefiles, +# (1) if the variable is set in 'config.status', edit 'config.status' +# (which will cause the Makefiles to be regenerated when you run 'make'); +# (2) otherwise, pass the desired values on the 'make' command line. +$(am__recursive_targets): + @fail=; \ + if $(am__make_keepgoing); then \ + failcom='fail=yes'; \ + else \ + failcom='exit 1'; \ + fi; \ + dot_seen=no; \ + target=`echo $@ | sed s/-recursive//`; \ + case "$@" in \ + distclean-* | maintainer-clean-*) list='$(DIST_SUBDIRS)' ;; \ + *) list='$(SUBDIRS)' ;; \ + esac; \ + for subdir in $$list; do \ + echo "Making $$target in $$subdir"; \ + if test "$$subdir" = "."; then \ + dot_seen=yes; \ + local_target="$$target-am"; \ + else \ + local_target="$$target"; \ + fi; \ + ($(am__cd) $$subdir && $(MAKE) $(AM_MAKEFLAGS) $$local_target) \ + || eval $$failcom; \ + done; \ + if test "$$dot_seen" = "no"; then \ + $(MAKE) $(AM_MAKEFLAGS) "$$target-am" || exit 1; \ + fi; test -z "$$fail" + +ID: $(am__tagged_files) + $(am__define_uniq_tagged_files); mkid -fID $$unique +tags: tags-recursive +TAGS: tags + +tags-am: $(TAGS_DEPENDENCIES) $(am__tagged_files) + set x; \ + here=`pwd`; \ + if ($(ETAGS) --etags-include --version) >/dev/null 2>&1; then \ + include_option=--etags-include; \ + empty_fix=.; \ + else \ + include_option=--include; \ + empty_fix=; \ + fi; \ + list='$(SUBDIRS)'; for subdir in $$list; do \ + if test "$$subdir" = .; then :; else \ + test ! -f $$subdir/TAGS || \ + set "$$@" "$$include_option=$$here/$$subdir/TAGS"; \ + fi; \ + done; \ + $(am__define_uniq_tagged_files); \ + shift; \ + if test -z "$(ETAGS_ARGS)$$*$$unique"; then :; else \ + test -n "$$unique" || unique=$$empty_fix; \ + if test $$# -gt 0; then \ + $(ETAGS) $(ETAGSFLAGS) $(AM_ETAGSFLAGS) $(ETAGS_ARGS) \ + "$$@" $$unique; \ + else \ + $(ETAGS) $(ETAGSFLAGS) $(AM_ETAGSFLAGS) $(ETAGS_ARGS) \ + $$unique; \ + fi; \ + fi +ctags: ctags-recursive + +CTAGS: ctags +ctags-am: $(TAGS_DEPENDENCIES) $(am__tagged_files) + $(am__define_uniq_tagged_files); \ + test -z "$(CTAGS_ARGS)$$unique" \ + || $(CTAGS) $(CTAGSFLAGS) $(AM_CTAGSFLAGS) $(CTAGS_ARGS) \ + $$unique + +GTAGS: + here=`$(am__cd) $(top_builddir) && pwd` \ + && $(am__cd) $(top_srcdir) \ + && gtags -i $(GTAGS_ARGS) "$$here" +cscope: cscope.files + test ! -s cscope.files \ + || $(CSCOPE) -b -q $(AM_CSCOPEFLAGS) $(CSCOPEFLAGS) -i cscope.files $(CSCOPE_ARGS) +clean-cscope: + -rm -f cscope.files +cscope.files: clean-cscope cscopelist +cscopelist: cscopelist-recursive + +cscopelist-am: $(am__tagged_files) + list='$(am__tagged_files)'; \ + case "$(srcdir)" in \ + [\\/]* | ?:[\\/]*) sdir="$(srcdir)" ;; \ + *) sdir=$(subdir)/$(srcdir) ;; \ + esac; \ + for i in $$list; do \ + if test -f "$$i"; then \ + echo "$(subdir)/$$i"; \ + else \ + echo "$$sdir/$$i"; \ + fi; \ + done >> $(top_builddir)/cscope.files + +distclean-tags: + -rm -f TAGS ID GTAGS GRTAGS GSYMS GPATH tags + -rm -f cscope.out cscope.in.out cscope.po.out cscope.files + +distdir: $(DISTFILES) + $(am__remove_distdir) + test -d "$(distdir)" || mkdir "$(distdir)" + @srcdirstrip=`echo "$(srcdir)" | sed 's/[].[^$$\\*]/\\\\&/g'`; \ + topsrcdirstrip=`echo "$(top_srcdir)" | sed 's/[].[^$$\\*]/\\\\&/g'`; \ + list='$(DISTFILES)'; \ + dist_files=`for file in $$list; do echo $$file; done | \ + sed -e "s|^$$srcdirstrip/||;t" \ + -e "s|^$$topsrcdirstrip/|$(top_builddir)/|;t"`; \ + case $$dist_files in \ + */*) $(MKDIR_P) `echo "$$dist_files" | \ + sed '/\//!d;s|^|$(distdir)/|;s,/[^/]*$$,,' | \ + sort -u` ;; \ + esac; \ + for file in $$dist_files; do \ + if test -f $$file || test -d $$file; then d=.; else d=$(srcdir); fi; \ + if test -d $$d/$$file; then \ + dir=`echo "/$$file" | sed -e 's,/[^/]*$$,,'`; \ + if test -d "$(distdir)/$$file"; then \ + find "$(distdir)/$$file" -type d ! -perm -700 -exec chmod u+rwx {} \;; \ + fi; \ + if test -d $(srcdir)/$$file && test $$d != $(srcdir); then \ + cp -fpR $(srcdir)/$$file "$(distdir)$$dir" || exit 1; \ + find "$(distdir)/$$file" -type d ! -perm -700 -exec chmod u+rwx {} \;; \ + fi; \ + cp -fpR $$d/$$file "$(distdir)$$dir" || exit 1; \ + else \ + test -f "$(distdir)/$$file" \ + || cp -p $$d/$$file "$(distdir)/$$file" \ + || exit 1; \ + fi; \ + done + @list='$(DIST_SUBDIRS)'; for subdir in $$list; do \ + if test "$$subdir" = .; then :; else \ + $(am__make_dryrun) \ + || test -d "$(distdir)/$$subdir" \ + || $(MKDIR_P) "$(distdir)/$$subdir" \ + || exit 1; \ + dir1=$$subdir; dir2="$(distdir)/$$subdir"; \ + $(am__relativize); \ + new_distdir=$$reldir; \ + dir1=$$subdir; dir2="$(top_distdir)"; \ + $(am__relativize); \ + new_top_distdir=$$reldir; \ + echo " (cd $$subdir && $(MAKE) $(AM_MAKEFLAGS) top_distdir="$$new_top_distdir" distdir="$$new_distdir" \\"; \ + echo " am__remove_distdir=: am__skip_length_check=: am__skip_mode_fix=: distdir)"; \ + ($(am__cd) $$subdir && \ + $(MAKE) $(AM_MAKEFLAGS) \ + top_distdir="$$new_top_distdir" \ + distdir="$$new_distdir" \ + am__remove_distdir=: \ + am__skip_length_check=: \ + am__skip_mode_fix=: \ + distdir) \ + || exit 1; \ + fi; \ + done + -test -n "$(am__skip_mode_fix)" \ + || find "$(distdir)" -type d ! -perm -755 \ + -exec chmod u+rwx,go+rx {} \; -o \ + ! -type d ! -perm -444 -links 1 -exec chmod a+r {} \; -o \ + ! -type d ! -perm -400 -exec chmod a+r {} \; -o \ + ! -type d ! -perm -444 -exec $(install_sh) -c -m a+r {} {} \; \ + || chmod -R a+r "$(distdir)" +dist-gzip: distdir + tardir=$(distdir) && $(am__tar) | GZIP=$(GZIP_ENV) gzip -c >$(distdir).tar.gz + $(am__post_remove_distdir) + +dist-bzip2: distdir + tardir=$(distdir) && $(am__tar) | BZIP2=$${BZIP2--9} bzip2 -c >$(distdir).tar.bz2 + $(am__post_remove_distdir) + +dist-lzip: distdir + tardir=$(distdir) && $(am__tar) | lzip -c $${LZIP_OPT--9} >$(distdir).tar.lz + $(am__post_remove_distdir) + +dist-xz: distdir + tardir=$(distdir) && $(am__tar) | XZ_OPT=$${XZ_OPT--e} xz -c >$(distdir).tar.xz + $(am__post_remove_distdir) + +dist-tarZ: distdir + @echo WARNING: "Support for distribution archives compressed with" \ + "legacy program 'compress' is deprecated." >&2 + @echo WARNING: "It will be removed altogether in Automake 2.0" >&2 + tardir=$(distdir) && $(am__tar) | compress -c >$(distdir).tar.Z + $(am__post_remove_distdir) + +dist-shar: distdir + @echo WARNING: "Support for shar distribution archives is" \ + "deprecated." >&2 + @echo WARNING: "It will be removed altogether in Automake 2.0" >&2 + shar $(distdir) | GZIP=$(GZIP_ENV) gzip -c >$(distdir).shar.gz + $(am__post_remove_distdir) + +dist-zip: distdir + -rm -f $(distdir).zip + zip -rq $(distdir).zip $(distdir) + $(am__post_remove_distdir) + +dist dist-all: + $(MAKE) $(AM_MAKEFLAGS) $(DIST_TARGETS) am__post_remove_distdir='@:' + $(am__post_remove_distdir) + +# This target untars the dist file and tries a VPATH configuration. Then +# it guarantees that the distribution is self-contained by making another +# tarfile. +distcheck: dist + case '$(DIST_ARCHIVES)' in \ + *.tar.gz*) \ + GZIP=$(GZIP_ENV) gzip -dc $(distdir).tar.gz | $(am__untar) ;;\ + *.tar.bz2*) \ + bzip2 -dc $(distdir).tar.bz2 | $(am__untar) ;;\ + *.tar.lz*) \ + lzip -dc $(distdir).tar.lz | $(am__untar) ;;\ + *.tar.xz*) \ + xz -dc $(distdir).tar.xz | $(am__untar) ;;\ + *.tar.Z*) \ + uncompress -c $(distdir).tar.Z | $(am__untar) ;;\ + *.shar.gz*) \ + GZIP=$(GZIP_ENV) gzip -dc $(distdir).shar.gz | unshar ;;\ + *.zip*) \ + unzip $(distdir).zip ;;\ + esac + chmod -R a-w $(distdir) + chmod u+w $(distdir) + mkdir $(distdir)/_build $(distdir)/_build/sub $(distdir)/_inst + chmod a-w $(distdir) + test -d $(distdir)/_build || exit 0; \ + dc_install_base=`$(am__cd) $(distdir)/_inst && pwd | sed -e 's,^[^:\\/]:[\\/],/,'` \ + && dc_destdir="$${TMPDIR-/tmp}/am-dc-$$$$/" \ + && am__cwd=`pwd` \ + && $(am__cd) $(distdir)/_build/sub \ + && ../../configure \ + $(AM_DISTCHECK_CONFIGURE_FLAGS) \ + $(DISTCHECK_CONFIGURE_FLAGS) \ + --srcdir=../.. --prefix="$$dc_install_base" \ + && $(MAKE) $(AM_MAKEFLAGS) \ + && $(MAKE) $(AM_MAKEFLAGS) dvi \ + && $(MAKE) $(AM_MAKEFLAGS) check \ + && $(MAKE) $(AM_MAKEFLAGS) install \ + && $(MAKE) $(AM_MAKEFLAGS) installcheck \ + && $(MAKE) $(AM_MAKEFLAGS) uninstall \ + && $(MAKE) $(AM_MAKEFLAGS) distuninstallcheck_dir="$$dc_install_base" \ + distuninstallcheck \ + && chmod -R a-w "$$dc_install_base" \ + && ({ \ + (cd ../.. && umask 077 && mkdir "$$dc_destdir") \ + && $(MAKE) $(AM_MAKEFLAGS) DESTDIR="$$dc_destdir" install \ + && $(MAKE) $(AM_MAKEFLAGS) DESTDIR="$$dc_destdir" uninstall \ + && $(MAKE) $(AM_MAKEFLAGS) DESTDIR="$$dc_destdir" \ + distuninstallcheck_dir="$$dc_destdir" distuninstallcheck; \ + } || { rm -rf "$$dc_destdir"; exit 1; }) \ + && rm -rf "$$dc_destdir" \ + && $(MAKE) $(AM_MAKEFLAGS) dist \ + && rm -rf $(DIST_ARCHIVES) \ + && $(MAKE) $(AM_MAKEFLAGS) distcleancheck \ + && cd "$$am__cwd" \ + || exit 1 + $(am__post_remove_distdir) + @(echo "$(distdir) archives ready for distribution: "; \ + list='$(DIST_ARCHIVES)'; for i in $$list; do echo $$i; done) | \ + sed -e 1h -e 1s/./=/g -e 1p -e 1x -e '$$p' -e '$$x' +distuninstallcheck: + @test -n '$(distuninstallcheck_dir)' || { \ + echo 'ERROR: trying to run $@ with an empty' \ + '$$(distuninstallcheck_dir)' >&2; \ + exit 1; \ + }; \ + $(am__cd) '$(distuninstallcheck_dir)' || { \ + echo 'ERROR: cannot chdir into $(distuninstallcheck_dir)' >&2; \ + exit 1; \ + }; \ + test `$(am__distuninstallcheck_listfiles) | wc -l` -eq 0 \ + || { echo "ERROR: files left after uninstall:" ; \ + if test -n "$(DESTDIR)"; then \ + echo " (check DESTDIR support)"; \ + fi ; \ + $(distuninstallcheck_listfiles) ; \ + exit 1; } >&2 +distcleancheck: distclean + @if test '$(srcdir)' = . ; then \ + echo "ERROR: distcleancheck can only run from a VPATH build" ; \ + exit 1 ; \ + fi + @test `$(distcleancheck_listfiles) | wc -l` -eq 0 \ + || { echo "ERROR: files left in build directory after distclean:" ; \ + $(distcleancheck_listfiles) ; \ + exit 1; } >&2 +check-am: all-am +check: check-recursive +all-am: Makefile $(DATA) config.h +installdirs: installdirs-recursive +installdirs-am: + for dir in "$(DESTDIR)$(docdir)"; do \ + test -z "$$dir" || $(MKDIR_P) "$$dir"; \ + done +install: install-recursive +install-exec: install-exec-recursive +install-data: install-data-recursive +uninstall: uninstall-recursive + +install-am: all-am + @$(MAKE) $(AM_MAKEFLAGS) install-exec-am install-data-am + +installcheck: installcheck-recursive +install-strip: + if test -z '$(STRIP)'; then \ + $(MAKE) $(AM_MAKEFLAGS) INSTALL_PROGRAM="$(INSTALL_STRIP_PROGRAM)" \ + install_sh_PROGRAM="$(INSTALL_STRIP_PROGRAM)" INSTALL_STRIP_FLAG=-s \ + install; \ + else \ + $(MAKE) $(AM_MAKEFLAGS) INSTALL_PROGRAM="$(INSTALL_STRIP_PROGRAM)" \ + install_sh_PROGRAM="$(INSTALL_STRIP_PROGRAM)" INSTALL_STRIP_FLAG=-s \ + "INSTALL_PROGRAM_ENV=STRIPPROG='$(STRIP)'" install; \ + fi +mostlyclean-generic: + +clean-generic: + +distclean-generic: + -test -z "$(CONFIG_CLEAN_FILES)" || rm -f $(CONFIG_CLEAN_FILES) + -test . = "$(srcdir)" || test -z "$(CONFIG_CLEAN_VPATH_FILES)" || rm -f $(CONFIG_CLEAN_VPATH_FILES) + +maintainer-clean-generic: + @echo "This command is intended for maintainers to use" + @echo "it deletes files that may require special tools to rebuild." +clean: clean-recursive + +clean-am: clean-generic mostlyclean-am + +distclean: distclean-recursive + -rm -f $(am__CONFIG_DISTCLEAN_FILES) + -rm -f Makefile +distclean-am: clean-am distclean-generic distclean-hdr distclean-tags + +dvi: dvi-recursive + +dvi-am: + +html: html-recursive + +html-am: + +info: info-recursive + +info-am: + +install-data-am: install-dist_docDATA + +install-dvi: install-dvi-recursive + +install-dvi-am: + +install-exec-am: + +install-html: install-html-recursive + +install-html-am: + +install-info: install-info-recursive + +install-info-am: + +install-man: + +install-pdf: install-pdf-recursive + +install-pdf-am: + +install-ps: install-ps-recursive + +install-ps-am: + +installcheck-am: + +maintainer-clean: maintainer-clean-recursive + -rm -f $(am__CONFIG_DISTCLEAN_FILES) + -rm -rf $(top_srcdir)/autom4te.cache + -rm -f Makefile +maintainer-clean-am: distclean-am maintainer-clean-generic + +mostlyclean: mostlyclean-recursive + +mostlyclean-am: mostlyclean-generic + +pdf: pdf-recursive + +pdf-am: + +ps: ps-recursive + +ps-am: + +uninstall-am: uninstall-dist_docDATA + +.MAKE: $(am__recursive_targets) all install-am install-strip + +.PHONY: $(am__recursive_targets) CTAGS GTAGS TAGS all all-am \ + am--refresh check check-am clean clean-cscope clean-generic \ + cscope cscopelist-am ctags ctags-am dist dist-all dist-bzip2 \ + dist-gzip dist-lzip dist-shar dist-tarZ dist-xz dist-zip \ + distcheck distclean distclean-generic distclean-hdr \ + distclean-tags distcleancheck distdir distuninstallcheck dvi \ + dvi-am html html-am info info-am install install-am \ + install-data install-data-am install-dist_docDATA install-dvi \ + install-dvi-am install-exec install-exec-am install-html \ + install-html-am install-info install-info-am install-man \ + install-pdf install-pdf-am install-ps install-ps-am \ + install-strip installcheck installcheck-am installdirs \ + installdirs-am maintainer-clean maintainer-clean-generic \ + mostlyclean mostlyclean-generic pdf pdf-am ps ps-am tags \ + tags-am uninstall uninstall-am uninstall-dist_docDATA + +.PRECIOUS: Makefile + + +# Tell versions [3.59,3.63) of GNU make to not export all variables. +# Otherwise a system limit (for SysV at least) may be exceeded. +.NOEXPORT: diff --git a/Makefile.am b/Makefile.am new file mode 100644 index 0000000..38bdf12 --- /dev/null +++ b/Makefile.am @@ -0,0 +1,2 @@ +SUBDIRS = src +dist_doc_DATA = README diff --git a/README b/README new file mode 100644 index 0000000..f160f90 --- /dev/null +++ b/README @@ -0,0 +1,275 @@ + +Lionheart + +A Refinement Logic Theorem Prover for Propositional Logic + + +In this paper, I propose a simple heuristic algorithm for deciding +logical propositions. The correctness and completeness of the system +are discussed. + +II. Formula Representation + +I use Smullyan's definition of propositional formulas as the basis of +the data structure. Smullyan defines propositional formulas as +follows: + +A. Every propositional variable is a formula +B. If X is a formula so is ~X. +C. If X, Y are formulas, then for each of the binary connectives b, +the expression (X b Y) is a formula. + +The conditions A, B, and C correspond roughly to the classes Var, Not, +and BinOp, three subclasses of PropFormula in Lionheart's C++ +representation. In addition, I introduce the ConstFormula type, +corresponding to the following rule: + +D. true is a formula and false is a formula. + +In the prover's structure, however, this additional type, and then +only F, serves as a placeholder on the right-hand side of the +turnstile and is not manipulated at all. Thus the additional +condition does not affect the completeness or correctness of the +system. + +Each of the formula classes includes a print method, which displays +the representation of that formula. Formulas of type B and C are +printed recursively. The representation of formulas is as stated in +the rules above. + +The formula classes also support an equals method to determine the +equivalence of two formulas X and Y using the following rules: + +1. The formulas must be of the same type. +2. Any immediate subformulas must be equivalent. + +III. Parsing of Formulas + +The C++ source file parser.cc contains a recursive-descent parser for +the formulas described above. The parser recognizes the following +operators, listed in order of increasing precedence: + +A. ~ : NOT +B. & : AND +C. | : OR +D. ==> : IMPLIES + +The last three are binary operators and are left associative. The +parser does not require parentheses around a subexpression containing +a binary operator--the precedence and associativity rules are used to +decide semantic meaning. Thus the input + +p | q | r & t + +corresponds to the following Smullyan-style formula: + +((p v q) v (r ^ t)) + +The parser ignores any spaces and encodes any contiguous alphabetic +text as a variable. Parentheses are supported and function as in the +Smullyan definition, overriding precedence. + +IV. Decision Procedure + +The automatic prover attempts to achieve a proof of the given formula +using the rules of refinement logic. A refinement logic proof step, +or sequent, has the following form: + +H1, H2, H3, ... , Hn |- G + +where Hi is a formula, G is a formula. If a refinement-logic proof of +the sequent exists, then we say G is true given H1, ... , Hn. + +The refinement logic system is isomorphic and equivalent to the +analytic tableau system presented in Smullyan, and is therefore +correct and complete. A propositional formula X is a tautology if and +only if the sequent + + |- X + +has a refinement-logic proof. The rules of refinement logic are +summarized in the appendix. + +One difficulty with refinement logic is that many possible rules may +be legally applied to a given sequent. For example, one might +repeatedly apply notR and notL, moving one formula from right to left, +without making any progress in the proof. For this reason, the prover +makes use of a set of heuristics to determine when to apply a rule: + +A. If the formula on the right of the turnstile is a variable and is +not equal to any formula on the left side, notR. + +B. If the formula on the right of the turnstile is a variable and is +equal to a formula on the left side, hyp. + +C. If the formula on the right of the turnstile is a binary formula +with &, andR. + +D. If the formula on the right of the turnstile is a binary formula +with ==>, impL. + +E. If the formula on the right of the turnstile is a binary formula +with |, and one of its immediate subformulas is the logical conjugate +of the other, magic. + +F. If the formula on the right of the turnstile is a logical conjugate, +notR. + +Let a formula be called basic if it is either a variable or the +logical conjugate of a binary formula with |. + +G. If the formula on the right of the turnstile is a binary formula +with | and all formulas on the left are basic, then attempt a proof after +applying an orR1. If unsuccessful, attempt a proof after applying an +orR2. + +H. If the formula on the right of the turnstile is a binary formula +with | and there are non-basic formulas on the left, notR. + +I. If there is some non-basic formula on the left, apply one of orL, +andL, impL, notL, in that order of precedence. + +J. If a variable and its logical conjugate are on the left hand side, +apply notL to the conjugate. (Note that this is followed immediately by +rule B). + +K. Give up and fail to find a proof. + +The prover attempts to use A through K in that order, so the earlier +rules take precedence over the later rules. + +Claim: (Correctness) Any formula proved by this system is a tautology. + +Proof: The system is constrained by the rules of refinement logic, +which has been proved correct. + +For the proof of correctness I must introduce a measure of the +progress of the prover. Construct a function height which maps the +propositional formulas to the natural numbers. Define + +height(p) = 0, for all propositional variables p +height(~X) = height(X), for all propositional formulas X +height(X b Y) = height(X) + height(Y) + 1, for all formulas X, Y, and +all binary connectives b. + +Further, construct seqheight, mapping refinement logic sequents to the +natural numbers, such that if S is the sequent + +H1, ... , Hn |- G + +seqheight(S) = sum(i=1..n)height(Hi) + height(G) + +Let us say that sequent S dominates T if T is generated by one of the +subgoals of S. Note that this is not a strict ordering, since S may +have up to two subgoals. + +Lemma: Let the sequent S contain a formula with a binary connective. +Then each subgoal of S contains a sequent T generated by the system +such that seqheight(T) < seqheight(S). + +Proof: + +If the binary formula is on the right-hand side of S: + + If it is an AND formula, apply andR, decreasing the height of the + right side for both subgoals. + + If it is an IMPL formula, apply impR on X==>Y. This decreases the + height of the sequent by one, since Y remains on the right side and + X joins the left side. + + If it is an OR formula, assume there are no binary formulas on the + left side (since this case is handled separately). Then apply + orR1/orR2, decreasing the height of the right side. + + If it is the logical conjugate of a binary formula, apply notR. + The binary formula is then on the left side. (Note that the system + does not generate formulas of the form ~~X, although this is legal + by Smullyan's definition). The system now applies left-hand-side + rules. + +If the binary formula is on the left-hand side of S: + + If it is an AND or OR formula, apply andL or orL. The loss of the + connective decreases seqheight by at least 1. + + If it is an IMPL formula, apply impL. The two subgoals have height + decreased by at least 1 for loss of the connective. + + If it is the logical conjugate of a binary formula, apply notL to + bring a binary formula to the right side. The system now applies + right-hand-side rules. + +Claim: (Completeness) Every tautology is proved by the system. + +Proof: From the lemma above we obtain the result that the system +decreases the height of sequents until there are no more binary +connectives. So the only formulas left are of the form p and ~p, +where p is a propositional variable. Consider the 3 cases: + +1) There is some variable p such that p and ~p are on the left side of + the sequent. In this case, rule A is employed to apply notL to + ~p. This yields case 2: + +2) There is some variable p such that p is on both sides of the + sequent. In this case, the hyp rule is used, so the proof of the + subgoal succeeds. + +3) Neither of the above conditions holds. The pseudo-rule giveup is + used, so the proof of the subgoal fails. + +By the completeness and correctness result of refinement logic, a +sequent is true iff its subgoals are true. + +The only means of losing information from a sequent is by applying +orR1 or orR2, but the above system tries both cases. Therefore, the +Lionheart system is complete. + +V. Testing + +A number of propositional logic tautologies from Smullyan were used to +test the Lionheart prover. A portion of the results are found below: + + |- (((p ==> q) & (q ==> r)) ==> (p ==> r)) by impR +((p ==> q) & (q ==> r)) |- (p ==> r) by impR +((p ==> q) & (q ==> r)), p |- r by notR +((p ==> q) & (q ==> r)), p, ~r |- false by andL +p, ~r, (p ==> q), (q ==> r) |- false by impL + p, ~r, (q ==> r) |- p by hyp + + p, ~r, (q ==> r), q |- false by impL + p, ~r, q |- q by hyp + + p, ~r, q, r |- false by notL + p, q, r |- r by hyp + + + |- ((((p ==> r) & (q ==> r)) & (p | q)) ==> r) by impR +(((p ==> r) & (q ==> r)) & (p | q)) |- r by notR +(((p ==> r) & (q ==> r)) & (p | q)), ~r |- false by andL +~r, ((p ==> r) & (q ==> r)), (p | q) |- false by andL +~r, (p | q), (p ==> r), (q ==> r) |- false by orL + ~r, (p ==> r), (q ==> r), p |- false by impL + ~r, (q ==> r), p |- p by hyp + + ~r, (q ==> r), p, r |- false by impL + ~r, p, r |- q by notR + ~r, p, r, ~q |- false by notL + p, r, ~q |- r by hyp + + ~r, p, r, r |- false by notL + p, r, r |- r by hyp + + ~r, (p ==> r), (q ==> r), q |- false by impL + ~r, (q ==> r), q |- p by notR + ~r, (q ==> r), q, ~p |- false by impL + ~r, q, ~p |- q by hyp + + ~r, q, ~p, r |- false by notL + q, ~p, r |- r by hyp + + ~r, (q ==> r), q, r |- false by impL + ~r, q, r |- q by hyp + + ~r, q, r, r |- false by notL + q, r, r |- r by hyp diff --git a/TODO b/TODO new file mode 100644 index 0000000..306283c --- /dev/null +++ b/TODO @@ -0,0 +1,29 @@ +- Fix memory leak. Proof.cleanup doesn't seem to work... +- Add automated proof support. This can probably be done in a series + of stages: + 1) Create a semi-automated prover that applies rules when it can + and seeks user input when it has to (inherit from UserRuleSource). + 2) Progressively refine the rule heuristic until the + semi-automated prover no longer needs human input. + 3) Rigorously test. + 4) Convert to pure automated prover. +- Finish commenting. + +- Implement auto-prover strategy + 1 ) goal is to get all formulas on the lhs with the form VAR or ~VAR + 2 ) if rhs is VAR and rhs != any lhs(i) --> notR + 2a) if rhs is VAR = some lhs(i) --> hyp + 3 ) if rhs is & --> andR + 4 ) if rhs is ~X --> notR + 5 ) if rhs is ==> --> impR + 6 ) if rhs is X|~X or ~X|X --> magic + 7 ) if rhs is X|Y and lhs contains only ~(W|Z)'s, VAR's, and ~VAR's + --> orR1, then orR2 if necessary + 8 ) if rhs is X|Y and lhs not described by 7's condition --> notR + 8 ) if rhs is constant (i.e. false)... + 8a) if lhs contains non-basic formulae only of form ~(X|Y) --> notL + 8b) if lhs contains X&Y --> andL + 8c) if lhs contains p and ~p --> notL on ~p + 8d) if lhs contains ~X where X is non-basic, non-OR --> notL + 8e) if lhs contains X==>Y, impL + diff --git a/config.h b/config.h new file mode 100644 index 0000000..0cc278a --- /dev/null +++ b/config.h @@ -0,0 +1,71 @@ +/* config.h. Generated from config.h.in by configure. */ +/* config.h.in. Generated from configure.ac by autoheader. */ + +/* Define to 1 if you have the header file. */ +#define HAVE_INTTYPES_H 1 + +/* Define to 1 if you have the header file. */ +#define HAVE_MEMORY_H 1 + +/* Define to 1 if you have the header file. */ +#define HAVE_STDINT_H 1 + +/* Define to 1 if you have the header file. */ +#define HAVE_STDLIB_H 1 + +/* Define to 1 if you have the `strcasecmp' function. */ +#define HAVE_STRCASECMP 1 + +/* Define to 1 if you have the `strdup' function. */ +#define HAVE_STRDUP 1 + +/* Define to 1 if you have the header file. */ +#define HAVE_STRINGS_H 1 + +/* Define to 1 if you have the header file. */ +#define HAVE_STRING_H 1 + +/* Define to 1 if you have the header file. */ +#define HAVE_SYS_STAT_H 1 + +/* Define to 1 if you have the header file. */ +#define HAVE_SYS_TYPES_H 1 + +/* Define to 1 if you have the header file. */ +#define HAVE_UNISTD_H 1 + +/* Define to 1 if the system has the type `_Bool'. */ +#define HAVE__BOOL 1 + +/* Name of package */ +#define PACKAGE "lionheart" + +/* Define to the address where bug reports for this package should be sent. */ +#define PACKAGE_BUGREPORT "" + +/* Define to the full name of this package. */ +#define PACKAGE_NAME "lionheart" + +/* Define to the full name and version of this package. */ +#define PACKAGE_STRING "lionheart 20000916" + +/* Define to the one symbol short name of this package. */ +#define PACKAGE_TARNAME "lionheart" + +/* Define to the home page for this package. */ +#define PACKAGE_URL "" + +/* Define to the version of this package. */ +#define PACKAGE_VERSION "20000916" + +/* Define to 1 if you have the ANSI C header files. */ +#define STDC_HEADERS 1 + +/* Version number of package */ +#define VERSION "20000916" + +/* Define to `__inline__' or `__inline' if that's what the C compiler + calls it, or to nothing if 'inline' is not supported under any name. */ +#ifndef __cplusplus +/* #undef inline */ +#endif diff --git a/config.h.in b/config.h.in new file mode 100644 index 0000000..f437db3 --- /dev/null +++ b/config.h.in @@ -0,0 +1,70 @@ +/* config.h.in. Generated from configure.ac by autoheader. */ + +/* Define to 1 if you have the header file. */ +#undef HAVE_INTTYPES_H + +/* Define to 1 if you have the header file. */ +#undef HAVE_MEMORY_H + +/* Define to 1 if you have the header file. */ +#undef HAVE_STDINT_H + +/* Define to 1 if you have the header file. */ +#undef HAVE_STDLIB_H + +/* Define to 1 if you have the `strcasecmp' function. */ +#undef HAVE_STRCASECMP + +/* Define to 1 if you have the `strdup' function. */ +#undef HAVE_STRDUP + +/* Define to 1 if you have the header file. */ +#undef HAVE_STRINGS_H + +/* Define to 1 if you have the header file. */ +#undef HAVE_STRING_H + +/* Define to 1 if you have the header file. */ +#undef HAVE_SYS_STAT_H + +/* Define to 1 if you have the header file. */ +#undef HAVE_SYS_TYPES_H + +/* Define to 1 if you have the header file. */ +#undef HAVE_UNISTD_H + +/* Define to 1 if the system has the type `_Bool'. */ +#undef HAVE__BOOL + +/* Name of package */ +#undef PACKAGE + +/* Define to the address where bug reports for this package should be sent. */ +#undef PACKAGE_BUGREPORT + +/* Define to the full name of this package. */ +#undef PACKAGE_NAME + +/* Define to the full name and version of this package. */ +#undef PACKAGE_STRING + +/* Define to the one symbol short name of this package. */ +#undef PACKAGE_TARNAME + +/* Define to the home page for this package. */ +#undef PACKAGE_URL + +/* Define to the version of this package. */ +#undef PACKAGE_VERSION + +/* Define to 1 if you have the ANSI C header files. */ +#undef STDC_HEADERS + +/* Version number of package */ +#undef VERSION + +/* Define to `__inline__' or `__inline' if that's what the C compiler + calls it, or to nothing if 'inline' is not supported under any name. */ +#ifndef __cplusplus +#undef inline +#endif diff --git a/config.h.in~ b/config.h.in~ new file mode 100644 index 0000000..3744b99 --- /dev/null +++ b/config.h.in~ @@ -0,0 +1,64 @@ +/* config.h.in. Generated from configure.ac by autoheader. */ + +/* Define to 1 if you have the header file. */ +#undef HAVE_INTTYPES_H + +/* Define to 1 if you have the header file. */ +#undef HAVE_MEMORY_H + +/* Define to 1 if you have the header file. */ +#undef HAVE_STDINT_H + +/* Define to 1 if you have the header file. */ +#undef HAVE_STDLIB_H + +/* Define to 1 if you have the `strcasecmp' function. */ +#undef HAVE_STRCASECMP + +/* Define to 1 if you have the `strdup' function. */ +#undef HAVE_STRDUP + +/* Define to 1 if you have the header file. */ +#undef HAVE_STRINGS_H + +/* Define to 1 if you have the header file. */ +#undef HAVE_STRING_H + +/* Define to 1 if you have the header file. */ +#undef HAVE_SYS_STAT_H + +/* Define to 1 if you have the header file. */ +#undef HAVE_SYS_TYPES_H + +/* Define to 1 if you have the header file. */ +#undef HAVE_UNISTD_H + +/* Define to 1 if the system has the type `_Bool'. */ +#undef HAVE__BOOL + +/* Define to the address where bug reports for this package should be sent. */ +#undef PACKAGE_BUGREPORT + +/* Define to the full name of this package. */ +#undef PACKAGE_NAME + +/* Define to the full name and version of this package. */ +#undef PACKAGE_STRING + +/* Define to the one symbol short name of this package. */ +#undef PACKAGE_TARNAME + +/* Define to the home page for this package. */ +#undef PACKAGE_URL + +/* Define to the version of this package. */ +#undef PACKAGE_VERSION + +/* Define to 1 if you have the ANSI C header files. */ +#undef STDC_HEADERS + +/* Define to `__inline__' or `__inline' if that's what the C compiler + calls it, or to nothing if 'inline' is not supported under any name. */ +#ifndef __cplusplus +#undef inline +#endif diff --git a/config.log b/config.log new file mode 100644 index 0000000..b254d5b --- /dev/null +++ b/config.log @@ -0,0 +1,572 @@ +This file contains any messages produced by compilers while +running configure, to aid debugging if configure makes a mistake. + +It was created by lionheart configure 20000916, which was +generated by GNU Autoconf 2.69. Invocation command line was + + $ ./configure + +## --------- ## +## Platform. ## +## --------- ## + +hostname = julian.amyanddavid.net +uname -m = amd64 +uname -r = 6.1 +uname -s = OpenBSD +uname -v = GENERIC.MP#7 + +/usr/bin/uname -p = amd64 +/bin/uname -X = unknown + +/bin/arch = unknown +/usr/bin/arch -k = OpenBSD.amd64 +/usr/convex/getsysinfo = unknown +/usr/bin/hostinfo = unknown +/bin/machine = unknown +/usr/bin/oslevel = unknown +/bin/universe = unknown + +PATH: /home/david/bin +PATH: /home/david/.local/bin +PATH: /home/david/.node_modules_global/bin +PATH: /bin +PATH: /sbin +PATH: /usr/bin +PATH: /usr/sbin +PATH: /usr/X11R6/bin +PATH: /usr/local/bin +PATH: /usr/local/sbin +PATH: /usr/local/jdk-1.7.0/bin/ +PATH: /usr/games + + +## ----------- ## +## Core tests. ## +## ----------- ## + +configure:2284: checking for a BSD-compatible install +configure:2352: result: /usr/bin/install -c +configure:2363: checking whether build environment is sane +configure:2418: result: yes +configure:2569: checking for a thread-safe mkdir -p +configure:2608: result: /usr/local/bin/gmkdir -p +configure:2615: checking for gawk +configure:2631: found /usr/local/bin/gawk +configure:2642: result: gawk +configure:2653: checking whether make sets $(MAKE) +configure:2675: result: yes +configure:2704: checking whether make supports nested variables +configure:2721: result: yes +configure:2911: checking for g++ +configure:2927: found /usr/bin/g++ +configure:2938: result: g++ +configure:2965: checking for C++ compiler version +configure:2974: g++ --version >&5 +g++ (GCC) 4.2.1 20070719 +Copyright (C) 2007 Free Software Foundation, Inc. +This is free software; see the source for copying conditions. There is NO +warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. + +configure:2985: $? = 0 +configure:2974: g++ -v >&5 +Reading specs from /usr/lib/gcc-lib/amd64-unknown-openbsd6.1/4.2.1/specs +Target: amd64-unknown-openbsd6.1 +Configured with: OpenBSD/amd64 system compiler +Thread model: posix +gcc version 4.2.1 20070719 +configure:2985: $? = 0 +configure:2974: g++ -V >&5 +g++: '-V' option must have argument +configure:2985: $? = 1 +configure:2974: g++ -qversion >&5 +g++: unrecognized option '-qversion' +g++: no input files +configure:2985: $? = 1 +configure:3005: checking whether the C++ compiler works +configure:3027: g++ conftest.cpp >&5 +configure:3031: $? = 0 +configure:3079: result: yes +configure:3082: checking for C++ compiler default output file name +configure:3084: result: a.out +configure:3090: checking for suffix of executables +configure:3097: g++ -o conftest conftest.cpp >&5 +configure:3101: $? = 0 +configure:3123: result: +configure:3145: checking whether we are cross compiling +configure:3153: g++ -o conftest conftest.cpp >&5 +configure:3157: $? = 0 +configure:3164: ./conftest +configure:3168: $? = 0 +configure:3183: result: no +configure:3188: checking for suffix of object files +configure:3210: g++ -c conftest.cpp >&5 +configure:3214: $? = 0 +configure:3235: result: o +configure:3239: checking whether we are using the GNU C++ compiler +configure:3258: g++ -c conftest.cpp >&5 +configure:3258: $? = 0 +configure:3267: result: yes +configure:3276: checking whether g++ accepts -g +configure:3296: g++ -c -g conftest.cpp >&5 +configure:3296: $? = 0 +configure:3337: result: yes +configure:3371: checking for style of include used by make +configure:3399: result: GNU +configure:3425: checking dependency style of g++ +configure:3536: result: gcc3 +configure:3599: checking for gcc +configure:3615: found /usr/bin/gcc +configure:3626: result: gcc +configure:3855: checking for C compiler version +configure:3864: gcc --version >&5 +gcc (GCC) 4.2.1 20070719 +Copyright (C) 2007 Free Software Foundation, Inc. +This is free software; see the source for copying conditions. There is NO +warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. + +configure:3875: $? = 0 +configure:3864: gcc -v >&5 +Reading specs from /usr/lib/gcc-lib/amd64-unknown-openbsd6.1/4.2.1/specs +Target: amd64-unknown-openbsd6.1 +Configured with: OpenBSD/amd64 system compiler +Thread model: posix +gcc version 4.2.1 20070719 +configure:3875: $? = 0 +configure:3864: gcc -V >&5 +gcc: '-V' option must have argument +configure:3875: $? = 1 +configure:3864: gcc -qversion >&5 +gcc: unrecognized option '-qversion' +gcc: no input files +configure:3875: $? = 1 +configure:3879: checking whether we are using the GNU C compiler +configure:3898: gcc -c conftest.c >&5 +configure:3898: $? = 0 +configure:3907: result: yes +configure:3916: checking whether gcc accepts -g +configure:3936: gcc -c -g conftest.c >&5 +configure:3936: $? = 0 +configure:3977: result: yes +configure:3994: checking for gcc option to accept ISO C89 +configure:4057: gcc -c -g -O2 conftest.c >&5 +configure:4057: $? = 0 +configure:4070: result: none needed +configure:4095: checking whether gcc understands -c and -o together +configure:4117: gcc -c conftest.c -o conftest2.o +configure:4120: $? = 0 +configure:4117: gcc -c conftest.c -o conftest2.o +configure:4120: $? = 0 +configure:4132: result: yes +configure:4151: checking dependency style of gcc +configure:4262: result: gcc3 +configure:4282: checking how to run the C preprocessor +configure:4313: gcc -E conftest.c +configure:4313: $? = 0 +configure:4327: gcc -E conftest.c +conftest.c:11:28: error: ac_nonexistent.h: No such file or directory +configure:4327: $? = 1 +configure: failed program was: +| /* confdefs.h */ +| #define PACKAGE_NAME "lionheart" +| #define PACKAGE_TARNAME "lionheart" +| #define PACKAGE_VERSION "20000916" +| #define PACKAGE_STRING "lionheart 20000916" +| #define PACKAGE_BUGREPORT "" +| #define PACKAGE_URL "" +| #define PACKAGE "lionheart" +| #define VERSION "20000916" +| /* end confdefs.h. */ +| #include +configure:4352: result: gcc -E +configure:4372: gcc -E conftest.c +configure:4372: $? = 0 +configure:4386: gcc -E conftest.c +conftest.c:11:28: error: ac_nonexistent.h: No such file or directory +configure:4386: $? = 1 +configure: failed program was: +| /* confdefs.h */ +| #define PACKAGE_NAME "lionheart" +| #define PACKAGE_TARNAME "lionheart" +| #define PACKAGE_VERSION "20000916" +| #define PACKAGE_STRING "lionheart 20000916" +| #define PACKAGE_BUGREPORT "" +| #define PACKAGE_URL "" +| #define PACKAGE "lionheart" +| #define VERSION "20000916" +| /* end confdefs.h. */ +| #include +configure:4420: checking for grep that handles long lines and -e +configure:4478: result: /usr/bin/grep +configure:4483: checking for egrep +configure:4545: result: /usr/bin/grep -E +configure:4550: checking for ANSI C header files +configure:4570: gcc -c -g -O2 conftest.c >&5 +configure:4570: $? = 0 +configure:4643: gcc -o conftest -g -O2 conftest.c >&5 +configure:4643: $? = 0 +configure:4643: ./conftest +configure:4643: $? = 0 +configure:4654: result: yes +configure:4667: checking for sys/types.h +configure:4667: gcc -c -g -O2 conftest.c >&5 +configure:4667: $? = 0 +configure:4667: result: yes +configure:4667: checking for sys/stat.h +configure:4667: gcc -c -g -O2 conftest.c >&5 +configure:4667: $? = 0 +configure:4667: result: yes +configure:4667: checking for stdlib.h +configure:4667: gcc -c -g -O2 conftest.c >&5 +configure:4667: $? = 0 +configure:4667: result: yes +configure:4667: checking for string.h +configure:4667: gcc -c -g -O2 conftest.c >&5 +configure:4667: $? = 0 +configure:4667: result: yes +configure:4667: checking for memory.h +configure:4667: gcc -c -g -O2 conftest.c >&5 +configure:4667: $? = 0 +configure:4667: result: yes +configure:4667: checking for strings.h +configure:4667: gcc -c -g -O2 conftest.c >&5 +configure:4667: $? = 0 +configure:4667: result: yes +configure:4667: checking for inttypes.h +configure:4667: gcc -c -g -O2 conftest.c >&5 +configure:4667: $? = 0 +configure:4667: result: yes +configure:4667: checking for stdint.h +configure:4667: gcc -c -g -O2 conftest.c >&5 +configure:4667: $? = 0 +configure:4667: result: yes +configure:4667: checking for unistd.h +configure:4667: gcc -c -g -O2 conftest.c >&5 +configure:4667: $? = 0 +configure:4667: result: yes +configure:4681: checking for string.h +configure:4681: result: yes +configure:4693: checking for stdbool.h that conforms to C99 +configure:4760: gcc -c -g -O2 conftest.c >&5 +configure:4760: $? = 0 +configure:4767: result: yes +configure:4769: checking for _Bool +configure:4769: gcc -c -g -O2 conftest.c >&5 +configure:4769: $? = 0 +configure:4769: gcc -c -g -O2 conftest.c >&5 +conftest.c: In function 'main': +conftest.c:58: error: expected expression before ')' token +configure:4769: $? = 1 +configure: failed program was: +| /* confdefs.h */ +| #define PACKAGE_NAME "lionheart" +| #define PACKAGE_TARNAME "lionheart" +| #define PACKAGE_VERSION "20000916" +| #define PACKAGE_STRING "lionheart 20000916" +| #define PACKAGE_BUGREPORT "" +| #define PACKAGE_URL "" +| #define PACKAGE "lionheart" +| #define VERSION "20000916" +| #define STDC_HEADERS 1 +| #define HAVE_SYS_TYPES_H 1 +| #define HAVE_SYS_STAT_H 1 +| #define HAVE_STDLIB_H 1 +| #define HAVE_STRING_H 1 +| #define HAVE_MEMORY_H 1 +| #define HAVE_STRINGS_H 1 +| #define HAVE_INTTYPES_H 1 +| #define HAVE_STDINT_H 1 +| #define HAVE_UNISTD_H 1 +| #define HAVE_STRING_H 1 +| /* end confdefs.h. */ +| #include +| #ifdef HAVE_SYS_TYPES_H +| # include +| #endif +| #ifdef HAVE_SYS_STAT_H +| # include +| #endif +| #ifdef STDC_HEADERS +| # include +| # include +| #else +| # ifdef HAVE_STDLIB_H +| # include +| # endif +| #endif +| #ifdef HAVE_STRING_H +| # if !defined STDC_HEADERS && defined HAVE_MEMORY_H +| # include +| # endif +| # include +| #endif +| #ifdef HAVE_STRINGS_H +| # include +| #endif +| #ifdef HAVE_INTTYPES_H +| # include +| #endif +| #ifdef HAVE_STDINT_H +| # include +| #endif +| #ifdef HAVE_UNISTD_H +| # include +| #endif +| int +| main () +| { +| if (sizeof ((_Bool))) +| return 0; +| ; +| return 0; +| } +configure:4769: result: yes +configure:4780: checking for inline +configure:4796: gcc -c -g -O2 conftest.c >&5 +configure:4796: $? = 0 +configure:4804: result: inline +configure:4827: checking for strcasecmp +configure:4827: gcc -o conftest -g -O2 conftest.c >&5 +conftest.c:46: warning: conflicting types for built-in function 'strcasecmp' +configure:4827: $? = 0 +configure:4827: result: yes +configure:4827: checking for strdup +configure:4827: gcc -o conftest -g -O2 conftest.c >&5 +conftest.c:47: warning: conflicting types for built-in function 'strdup' +configure:4827: $? = 0 +configure:4827: result: yes +configure:4948: checking that generated files are newer than configure +configure:4954: result: done +configure:4981: creating ./config.status + +## ---------------------- ## +## Running config.status. ## +## ---------------------- ## + +This file was extended by lionheart config.status 20000916, which was +generated by GNU Autoconf 2.69. Invocation command line was + + CONFIG_FILES = + CONFIG_HEADERS = + CONFIG_LINKS = + CONFIG_COMMANDS = + $ ./config.status + +on julian.amyanddavid.net + +config.status:863: creating Makefile +config.status:863: creating src/Makefile +config.status:863: creating config.h +config.status:1044: config.h is unchanged +config.status:1092: executing depfiles commands + +## ---------------- ## +## Cache variables. ## +## ---------------- ## + +ac_cv_c_compiler_gnu=yes +ac_cv_c_inline=inline +ac_cv_cxx_compiler_gnu=yes +ac_cv_env_CCC_set= +ac_cv_env_CCC_value= +ac_cv_env_CC_set= +ac_cv_env_CC_value= +ac_cv_env_CFLAGS_set= +ac_cv_env_CFLAGS_value= +ac_cv_env_CPPFLAGS_set= +ac_cv_env_CPPFLAGS_value= +ac_cv_env_CPP_set= +ac_cv_env_CPP_value= +ac_cv_env_CXXFLAGS_set= +ac_cv_env_CXXFLAGS_value= +ac_cv_env_CXX_set= +ac_cv_env_CXX_value= +ac_cv_env_LDFLAGS_set= +ac_cv_env_LDFLAGS_value= +ac_cv_env_LIBS_set= +ac_cv_env_LIBS_value= +ac_cv_env_build_alias_set= +ac_cv_env_build_alias_value= +ac_cv_env_host_alias_set= +ac_cv_env_host_alias_value= +ac_cv_env_target_alias_set= +ac_cv_env_target_alias_value= +ac_cv_func_strcasecmp=yes +ac_cv_func_strdup=yes +ac_cv_header_inttypes_h=yes +ac_cv_header_memory_h=yes +ac_cv_header_stdbool_h=yes +ac_cv_header_stdc=yes +ac_cv_header_stdint_h=yes +ac_cv_header_stdlib_h=yes +ac_cv_header_string_h=yes +ac_cv_header_strings_h=yes +ac_cv_header_sys_stat_h=yes +ac_cv_header_sys_types_h=yes +ac_cv_header_unistd_h=yes +ac_cv_objext=o +ac_cv_path_EGREP='/usr/bin/grep -E' +ac_cv_path_GREP=/usr/bin/grep +ac_cv_path_install='/usr/bin/install -c' +ac_cv_path_mkdir=/usr/local/bin/gmkdir +ac_cv_prog_AWK=gawk +ac_cv_prog_CPP='gcc -E' +ac_cv_prog_ac_ct_CC=gcc +ac_cv_prog_ac_ct_CXX=g++ +ac_cv_prog_cc_c89= +ac_cv_prog_cc_g=yes +ac_cv_prog_cxx_g=yes +ac_cv_prog_make_make_set=yes +ac_cv_type__Bool=yes +am_cv_CC_dependencies_compiler_type=gcc3 +am_cv_CXX_dependencies_compiler_type=gcc3 +am_cv_make_support_nested_variables=yes +am_cv_prog_cc_c_o=yes + +## ----------------- ## +## Output variables. ## +## ----------------- ## + +ACLOCAL='${SHELL} /home/david/devel/cpp/lionheart000916/missing aclocal-1.15' +AMDEPBACKSLASH='\' +AMDEP_FALSE='#' +AMDEP_TRUE='' +AMTAR='$${TAR-tar}' +AM_BACKSLASH='\' +AM_DEFAULT_V='$(AM_DEFAULT_VERBOSITY)' +AM_DEFAULT_VERBOSITY='1' +AM_V='$(V)' +AUTOCONF='${SHELL} /home/david/devel/cpp/lionheart000916/missing autoconf' +AUTOHEADER='${SHELL} /home/david/devel/cpp/lionheart000916/missing autoheader' +AUTOMAKE='${SHELL} /home/david/devel/cpp/lionheart000916/missing automake-1.15' +AWK='gawk' +CC='gcc' +CCDEPMODE='depmode=gcc3' +CFLAGS='-g -O2' +CPP='gcc -E' +CPPFLAGS='' +CXX='g++' +CXXDEPMODE='depmode=gcc3' +CXXFLAGS='-g -O2' +CYGPATH_W='echo' +DEFS='-DHAVE_CONFIG_H' +DEPDIR='.deps' +ECHO_C='' +ECHO_N='-n' +ECHO_T='' +EGREP='/usr/bin/grep -E' +EXEEXT='' +GREP='/usr/bin/grep' +INSTALL_DATA='${INSTALL} -m 644' +INSTALL_PROGRAM='${INSTALL}' +INSTALL_SCRIPT='${INSTALL}' +INSTALL_STRIP_PROGRAM='$(install_sh) -c -s' +LDFLAGS='' +LIBOBJS='' +LIBS='' +LTLIBOBJS='' +MAKEINFO='${SHELL} /home/david/devel/cpp/lionheart000916/missing makeinfo' +MKDIR_P='/usr/local/bin/gmkdir -p' +OBJEXT='o' +PACKAGE='lionheart' +PACKAGE_BUGREPORT='' +PACKAGE_NAME='lionheart' +PACKAGE_STRING='lionheart 20000916' +PACKAGE_TARNAME='lionheart' +PACKAGE_URL='' +PACKAGE_VERSION='20000916' +PATH_SEPARATOR=':' +SET_MAKE='' +SHELL='/bin/sh' +STRIP='' +VERSION='20000916' +ac_ct_CC='gcc' +ac_ct_CXX='g++' +am__EXEEXT_FALSE='' +am__EXEEXT_TRUE='#' +am__fastdepCC_FALSE='#' +am__fastdepCC_TRUE='' +am__fastdepCXX_FALSE='#' +am__fastdepCXX_TRUE='' +am__include='include' +am__isrc='' +am__leading_dot='.' +am__nodep='_no' +am__quote='' +am__tar='$${TAR-tar} chof - "$$tardir"' +am__untar='$${TAR-tar} xf -' +bindir='${exec_prefix}/bin' +build_alias='' +datadir='${datarootdir}' +datarootdir='${prefix}/share' +docdir='${datarootdir}/doc/${PACKAGE_TARNAME}' +dvidir='${docdir}' +exec_prefix='${prefix}' +host_alias='' +htmldir='${docdir}' +includedir='${prefix}/include' +infodir='${datarootdir}/info' +install_sh='${SHELL} /home/david/devel/cpp/lionheart000916/install-sh' +libdir='${exec_prefix}/lib' +libexecdir='${exec_prefix}/libexec' +localedir='${datarootdir}/locale' +localstatedir='${prefix}/var' +mandir='${datarootdir}/man' +mkdir_p='$(MKDIR_P)' +oldincludedir='/usr/include' +pdfdir='${docdir}' +prefix='/usr/local' +program_transform_name='s,x,x,' +psdir='${docdir}' +sbindir='${exec_prefix}/sbin' +sharedstatedir='${prefix}/com' +sysconfdir='${prefix}/etc' +target_alias='' + +## ----------- ## +## confdefs.h. ## +## ----------- ## + +/* confdefs.h */ +#define PACKAGE_NAME "lionheart" +#define PACKAGE_TARNAME "lionheart" +#define PACKAGE_VERSION "20000916" +#define PACKAGE_STRING "lionheart 20000916" +#define PACKAGE_BUGREPORT "" +#define PACKAGE_URL "" +#define PACKAGE "lionheart" +#define VERSION "20000916" +#define STDC_HEADERS 1 +#define HAVE_SYS_TYPES_H 1 +#define HAVE_SYS_STAT_H 1 +#define HAVE_STDLIB_H 1 +#define HAVE_STRING_H 1 +#define HAVE_MEMORY_H 1 +#define HAVE_STRINGS_H 1 +#define HAVE_INTTYPES_H 1 +#define HAVE_STDINT_H 1 +#define HAVE_UNISTD_H 1 +#define HAVE_STRING_H 1 +#define HAVE__BOOL 1 +#define HAVE_STRCASECMP 1 +#define HAVE_STRDUP 1 + +configure: exit 0 + +## ---------------------- ## +## Running config.status. ## +## ---------------------- ## + +This file was extended by lionheart config.status 20000916, which was +generated by GNU Autoconf 2.69. Invocation command line was + + CONFIG_FILES = + CONFIG_HEADERS = + CONFIG_LINKS = + CONFIG_COMMANDS = + $ ./config.status config.h + +on julian.amyanddavid.net + +config.status:863: creating config.h +config.status:1044: config.h is unchanged diff --git a/config.status b/config.status new file mode 100755 index 0000000..15444df --- /dev/null +++ b/config.status @@ -0,0 +1,1197 @@ +#! /bin/sh +# Generated by configure. +# Run this file to recreate the current configuration. +# Compiler output produced by configure, useful for debugging +# configure, is in config.log if it exists. + +debug=false +ac_cs_recheck=false +ac_cs_silent=false + +SHELL=${CONFIG_SHELL-/bin/sh} +export SHELL +## -------------------- ## +## M4sh Initialization. ## +## -------------------- ## + +# Be more Bourne compatible +DUALCASE=1; export DUALCASE # for MKS sh +if test -n "${ZSH_VERSION+set}" && (emulate sh) >/dev/null 2>&1; then : + emulate sh + NULLCMD=: + # Pre-4.2 versions of Zsh do word splitting on ${1+"$@"}, which + # is contrary to our usage. Disable this feature. + alias -g '${1+"$@"}'='"$@"' + setopt NO_GLOB_SUBST +else + case `(set -o) 2>/dev/null` in #( + *posix*) : + set -o posix ;; #( + *) : + ;; +esac +fi + + +as_nl=' +' +export as_nl +# Printing a long string crashes Solaris 7 /usr/bin/printf. +as_echo='\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\' +as_echo=$as_echo$as_echo$as_echo$as_echo$as_echo +as_echo=$as_echo$as_echo$as_echo$as_echo$as_echo$as_echo +# Prefer a ksh shell builtin over an external printf program on Solaris, +# but without wasting forks for bash or zsh. +if test -z "$BASH_VERSION$ZSH_VERSION" \ + && (test "X`print -r -- $as_echo`" = "X$as_echo") 2>/dev/null; then + as_echo='print -r --' + as_echo_n='print -rn --' +elif (test "X`printf %s $as_echo`" = "X$as_echo") 2>/dev/null; then + as_echo='printf %s\n' + as_echo_n='printf %s' +else + if test "X`(/usr/ucb/echo -n -n $as_echo) 2>/dev/null`" = "X-n $as_echo"; then + as_echo_body='eval /usr/ucb/echo -n "$1$as_nl"' + as_echo_n='/usr/ucb/echo -n' + else + as_echo_body='eval expr "X$1" : "X\\(.*\\)"' + as_echo_n_body='eval + arg=$1; + case $arg in #( + *"$as_nl"*) + expr "X$arg" : "X\\(.*\\)$as_nl"; + arg=`expr "X$arg" : ".*$as_nl\\(.*\\)"`;; + esac; + expr "X$arg" : "X\\(.*\\)" | tr -d "$as_nl" + ' + export as_echo_n_body + as_echo_n='sh -c $as_echo_n_body as_echo' + fi + export as_echo_body + as_echo='sh -c $as_echo_body as_echo' +fi + +# The user is always right. +if test "${PATH_SEPARATOR+set}" != set; then + PATH_SEPARATOR=: + (PATH='/bin;/bin'; FPATH=$PATH; sh -c :) >/dev/null 2>&1 && { + (PATH='/bin:/bin'; FPATH=$PATH; sh -c :) >/dev/null 2>&1 || + PATH_SEPARATOR=';' + } +fi + + +# IFS +# We need space, tab and new line, in precisely that order. Quoting is +# there to prevent editors from complaining about space-tab. +# (If _AS_PATH_WALK were called with IFS unset, it would disable word +# splitting by setting IFS to empty value.) +IFS=" "" $as_nl" + +# Find who we are. Look in the path if we contain no directory separator. +as_myself= +case $0 in #(( + *[\\/]* ) as_myself=$0 ;; + *) as_save_IFS=$IFS; IFS=$PATH_SEPARATOR +for as_dir in $PATH +do + IFS=$as_save_IFS + test -z "$as_dir" && as_dir=. + test -r "$as_dir/$0" && as_myself=$as_dir/$0 && break + done +IFS=$as_save_IFS + + ;; +esac +# We did not find ourselves, most probably we were run as `sh COMMAND' +# in which case we are not to be found in the path. +if test "x$as_myself" = x; then + as_myself=$0 +fi +if test ! -f "$as_myself"; then + $as_echo "$as_myself: error: cannot find myself; rerun with an absolute file name" >&2 + exit 1 +fi + +# Unset variables that we do not need and which cause bugs (e.g. in +# pre-3.0 UWIN ksh). But do not cause bugs in bash 2.01; the "|| exit 1" +# suppresses any "Segmentation fault" message there. '((' could +# trigger a bug in pdksh 5.2.14. +for as_var in BASH_ENV ENV MAIL MAILPATH +do eval test x\${$as_var+set} = xset \ + && ( (unset $as_var) || exit 1) >/dev/null 2>&1 && unset $as_var || : +done +PS1='$ ' +PS2='> ' +PS4='+ ' + +# NLS nuisances. +LC_ALL=C +export LC_ALL +LANGUAGE=C +export LANGUAGE + +# CDPATH. +(unset CDPATH) >/dev/null 2>&1 && unset CDPATH + + +# as_fn_error STATUS ERROR [LINENO LOG_FD] +# ---------------------------------------- +# Output "`basename $0`: error: ERROR" to stderr. If LINENO and LOG_FD are +# provided, also output the error to LOG_FD, referencing LINENO. Then exit the +# script with STATUS, using 1 if that was 0. +as_fn_error () +{ + as_status=$1; test $as_status -eq 0 && as_status=1 + if test "$4"; then + as_lineno=${as_lineno-"$3"} as_lineno_stack=as_lineno_stack=$as_lineno_stack + $as_echo "$as_me:${as_lineno-$LINENO}: error: $2" >&$4 + fi + $as_echo "$as_me: error: $2" >&2 + as_fn_exit $as_status +} # as_fn_error + + +# as_fn_set_status STATUS +# ----------------------- +# Set $? to STATUS, without forking. +as_fn_set_status () +{ + return $1 +} # as_fn_set_status + +# as_fn_exit STATUS +# ----------------- +# Exit the shell with STATUS, even in a "trap 0" or "set -e" context. +as_fn_exit () +{ + set +e + as_fn_set_status $1 + exit $1 +} # as_fn_exit + +# as_fn_unset VAR +# --------------- +# Portably unset VAR. +as_fn_unset () +{ + { eval $1=; unset $1;} +} +as_unset=as_fn_unset +# as_fn_append VAR VALUE +# ---------------------- +# Append the text in VALUE to the end of the definition contained in VAR. Take +# advantage of any shell optimizations that allow amortized linear growth over +# repeated appends, instead of the typical quadratic growth present in naive +# implementations. +if (eval "as_var=1; as_var+=2; test x\$as_var = x12") 2>/dev/null; then : + eval 'as_fn_append () + { + eval $1+=\$2 + }' +else + as_fn_append () + { + eval $1=\$$1\$2 + } +fi # as_fn_append + +# as_fn_arith ARG... +# ------------------ +# Perform arithmetic evaluation on the ARGs, and store the result in the +# global $as_val. Take advantage of shells that can avoid forks. The arguments +# must be portable across $(()) and expr. +if (eval "test \$(( 1 + 1 )) = 2") 2>/dev/null; then : + eval 'as_fn_arith () + { + as_val=$(( $* )) + }' +else + as_fn_arith () + { + as_val=`expr "$@" || test $? -eq 1` + } +fi # as_fn_arith + + +if expr a : '\(a\)' >/dev/null 2>&1 && + test "X`expr 00001 : '.*\(...\)'`" = X001; then + as_expr=expr +else + as_expr=false +fi + +if (basename -- /) >/dev/null 2>&1 && test "X`basename -- / 2>&1`" = "X/"; then + as_basename=basename +else + as_basename=false +fi + +if (as_dir=`dirname -- /` && test "X$as_dir" = X/) >/dev/null 2>&1; then + as_dirname=dirname +else + as_dirname=false +fi + +as_me=`$as_basename -- "$0" || +$as_expr X/"$0" : '.*/\([^/][^/]*\)/*$' \| \ + X"$0" : 'X\(//\)$' \| \ + X"$0" : 'X\(/\)' \| . 2>/dev/null || +$as_echo X/"$0" | + sed '/^.*\/\([^/][^/]*\)\/*$/{ + s//\1/ + q + } + /^X\/\(\/\/\)$/{ + s//\1/ + q + } + /^X\/\(\/\).*/{ + s//\1/ + q + } + s/.*/./; q'` + +# Avoid depending upon Character Ranges. +as_cr_letters='abcdefghijklmnopqrstuvwxyz' +as_cr_LETTERS='ABCDEFGHIJKLMNOPQRSTUVWXYZ' +as_cr_Letters=$as_cr_letters$as_cr_LETTERS +as_cr_digits='0123456789' +as_cr_alnum=$as_cr_Letters$as_cr_digits + +ECHO_C= ECHO_N= ECHO_T= +case `echo -n x` in #((((( +-n*) + case `echo 'xy\c'` in + *c*) ECHO_T=' ';; # ECHO_T is single tab character. + xy) ECHO_C='\c';; + *) echo `echo ksh88 bug on AIX 6.1` > /dev/null + ECHO_T=' ';; + esac;; +*) + ECHO_N='-n';; +esac + +rm -f conf$$ conf$$.exe conf$$.file +if test -d conf$$.dir; then + rm -f conf$$.dir/conf$$.file +else + rm -f conf$$.dir + mkdir conf$$.dir 2>/dev/null +fi +if (echo >conf$$.file) 2>/dev/null; then + if ln -s conf$$.file conf$$ 2>/dev/null; then + as_ln_s='ln -s' + # ... but there are two gotchas: + # 1) On MSYS, both `ln -s file dir' and `ln file dir' fail. + # 2) DJGPP < 2.04 has no symlinks; `ln -s' creates a wrapper executable. + # In both cases, we have to default to `cp -pR'. + ln -s conf$$.file conf$$.dir 2>/dev/null && test ! -f conf$$.exe || + as_ln_s='cp -pR' + elif ln conf$$.file conf$$ 2>/dev/null; then + as_ln_s=ln + else + as_ln_s='cp -pR' + fi +else + as_ln_s='cp -pR' +fi +rm -f conf$$ conf$$.exe conf$$.dir/conf$$.file conf$$.file +rmdir conf$$.dir 2>/dev/null + + +# as_fn_mkdir_p +# ------------- +# Create "$as_dir" as a directory, including parents if necessary. +as_fn_mkdir_p () +{ + + case $as_dir in #( + -*) as_dir=./$as_dir;; + esac + test -d "$as_dir" || eval $as_mkdir_p || { + as_dirs= + while :; do + case $as_dir in #( + *\'*) as_qdir=`$as_echo "$as_dir" | sed "s/'/'\\\\\\\\''/g"`;; #'( + *) as_qdir=$as_dir;; + esac + as_dirs="'$as_qdir' $as_dirs" + as_dir=`$as_dirname -- "$as_dir" || +$as_expr X"$as_dir" : 'X\(.*[^/]\)//*[^/][^/]*/*$' \| \ + X"$as_dir" : 'X\(//\)[^/]' \| \ + X"$as_dir" : 'X\(//\)$' \| \ + X"$as_dir" : 'X\(/\)' \| . 2>/dev/null || +$as_echo X"$as_dir" | + sed '/^X\(.*[^/]\)\/\/*[^/][^/]*\/*$/{ + s//\1/ + q + } + /^X\(\/\/\)[^/].*/{ + s//\1/ + q + } + /^X\(\/\/\)$/{ + s//\1/ + q + } + /^X\(\/\).*/{ + s//\1/ + q + } + s/.*/./; q'` + test -d "$as_dir" && break + done + test -z "$as_dirs" || eval "mkdir $as_dirs" + } || test -d "$as_dir" || as_fn_error $? "cannot create directory $as_dir" + + +} # as_fn_mkdir_p +if mkdir -p . 2>/dev/null; then + as_mkdir_p='mkdir -p "$as_dir"' +else + test -d ./-p && rmdir ./-p + as_mkdir_p=false +fi + + +# as_fn_executable_p FILE +# ----------------------- +# Test if FILE is an executable regular file. +as_fn_executable_p () +{ + test -f "$1" && test -x "$1" +} # as_fn_executable_p +as_test_x='test -x' +as_executable_p=as_fn_executable_p + +# Sed expression to map a string onto a valid CPP name. +as_tr_cpp="eval sed 'y%*$as_cr_letters%P$as_cr_LETTERS%;s%[^_$as_cr_alnum]%_%g'" + +# Sed expression to map a string onto a valid variable name. +as_tr_sh="eval sed 'y%*+%pp%;s%[^_$as_cr_alnum]%_%g'" + + +exec 6>&1 +## ----------------------------------- ## +## Main body of $CONFIG_STATUS script. ## +## ----------------------------------- ## +# Save the log message, to keep $0 and so on meaningful, and to +# report actual input values of CONFIG_FILES etc. instead of their +# values after options handling. +ac_log=" +This file was extended by lionheart $as_me 20000916, which was +generated by GNU Autoconf 2.69. Invocation command line was + + CONFIG_FILES = $CONFIG_FILES + CONFIG_HEADERS = $CONFIG_HEADERS + CONFIG_LINKS = $CONFIG_LINKS + CONFIG_COMMANDS = $CONFIG_COMMANDS + $ $0 $@ + +on `(hostname || uname -n) 2>/dev/null | sed 1q` +" + +# Files that config.status was made for. +config_files=" Makefile src/Makefile" +config_headers=" config.h" +config_commands=" depfiles" + +ac_cs_usage="\ +\`$as_me' instantiates files and other configuration actions +from templates according to the current configuration. Unless the files +and actions are specified as TAGs, all are instantiated by default. + +Usage: $0 [OPTION]... [TAG]... + + -h, --help print this help, then exit + -V, --version print version number and configuration settings, then exit + --config print configuration, then exit + -q, --quiet, --silent + do not print progress messages + -d, --debug don't remove temporary files + --recheck update $as_me by reconfiguring in the same conditions + --file=FILE[:TEMPLATE] + instantiate the configuration file FILE + --header=FILE[:TEMPLATE] + instantiate the configuration header FILE + +Configuration files: +$config_files + +Configuration headers: +$config_headers + +Configuration commands: +$config_commands + +Report bugs to the package provider." + +ac_cs_config="" +ac_cs_version="\ +lionheart config.status 20000916 +configured by ./configure, generated by GNU Autoconf 2.69, + with options \"$ac_cs_config\" + +Copyright (C) 2012 Free Software Foundation, Inc. +This config.status script is free software; the Free Software Foundation +gives unlimited permission to copy, distribute and modify it." + +ac_pwd='/home/david/devel/cpp/lionheart000916' +srcdir='.' +INSTALL='/usr/bin/install -c' +MKDIR_P='/usr/local/bin/gmkdir -p' +AWK='gawk' +test -n "$AWK" || AWK=awk +# The default lists apply if the user does not specify any file. +ac_need_defaults=: +while test $# != 0 +do + case $1 in + --*=?*) + ac_option=`expr "X$1" : 'X\([^=]*\)='` + ac_optarg=`expr "X$1" : 'X[^=]*=\(.*\)'` + ac_shift=: + ;; + --*=) + ac_option=`expr "X$1" : 'X\([^=]*\)='` + ac_optarg= + ac_shift=: + ;; + *) + ac_option=$1 + ac_optarg=$2 + ac_shift=shift + ;; + esac + + case $ac_option in + # Handling of the options. + -recheck | --recheck | --rechec | --reche | --rech | --rec | --re | --r) + ac_cs_recheck=: ;; + --version | --versio | --versi | --vers | --ver | --ve | --v | -V ) + $as_echo "$ac_cs_version"; exit ;; + --config | --confi | --conf | --con | --co | --c ) + $as_echo "$ac_cs_config"; exit ;; + --debug | --debu | --deb | --de | --d | -d ) + debug=: ;; + --file | --fil | --fi | --f ) + $ac_shift + case $ac_optarg in + *\'*) ac_optarg=`$as_echo "$ac_optarg" | sed "s/'/'\\\\\\\\''/g"` ;; + '') as_fn_error $? "missing file argument" ;; + esac + as_fn_append CONFIG_FILES " '$ac_optarg'" + ac_need_defaults=false;; + --header | --heade | --head | --hea ) + $ac_shift + case $ac_optarg in + *\'*) ac_optarg=`$as_echo "$ac_optarg" | sed "s/'/'\\\\\\\\''/g"` ;; + esac + as_fn_append CONFIG_HEADERS " '$ac_optarg'" + ac_need_defaults=false;; + --he | --h) + # Conflict between --help and --header + as_fn_error $? "ambiguous option: \`$1' +Try \`$0 --help' for more information.";; + --help | --hel | -h ) + $as_echo "$ac_cs_usage"; exit ;; + -q | -quiet | --quiet | --quie | --qui | --qu | --q \ + | -silent | --silent | --silen | --sile | --sil | --si | --s) + ac_cs_silent=: ;; + + # This is an error. + -*) as_fn_error $? "unrecognized option: \`$1' +Try \`$0 --help' for more information." ;; + + *) as_fn_append ac_config_targets " $1" + ac_need_defaults=false ;; + + esac + shift +done + +ac_configure_extra_args= + +if $ac_cs_silent; then + exec 6>/dev/null + ac_configure_extra_args="$ac_configure_extra_args --silent" +fi + +if $ac_cs_recheck; then + set X /bin/sh './configure' $ac_configure_extra_args --no-create --no-recursion + shift + $as_echo "running CONFIG_SHELL=/bin/sh $*" >&6 + CONFIG_SHELL='/bin/sh' + export CONFIG_SHELL + exec "$@" +fi + +exec 5>>config.log +{ + echo + sed 'h;s/./-/g;s/^.../## /;s/...$/ ##/;p;x;p;x' <<_ASBOX +## Running $as_me. ## +_ASBOX + $as_echo "$ac_log" +} >&5 + +# +# INIT-COMMANDS +# +AMDEP_TRUE="" ac_aux_dir="." + + +# Handling of arguments. +for ac_config_target in $ac_config_targets +do + case $ac_config_target in + "config.h") CONFIG_HEADERS="$CONFIG_HEADERS config.h" ;; + "depfiles") CONFIG_COMMANDS="$CONFIG_COMMANDS depfiles" ;; + "Makefile") CONFIG_FILES="$CONFIG_FILES Makefile" ;; + "src/Makefile") CONFIG_FILES="$CONFIG_FILES src/Makefile" ;; + + *) as_fn_error $? "invalid argument: \`$ac_config_target'" "$LINENO" 5;; + esac +done + + +# If the user did not use the arguments to specify the items to instantiate, +# then the envvar interface is used. Set only those that are not. +# We use the long form for the default assignment because of an extremely +# bizarre bug on SunOS 4.1.3. +if $ac_need_defaults; then + test "${CONFIG_FILES+set}" = set || CONFIG_FILES=$config_files + test "${CONFIG_HEADERS+set}" = set || CONFIG_HEADERS=$config_headers + test "${CONFIG_COMMANDS+set}" = set || CONFIG_COMMANDS=$config_commands +fi + +# Have a temporary directory for convenience. Make it in the build tree +# simply because there is no reason against having it here, and in addition, +# creating and moving files from /tmp can sometimes cause problems. +# Hook for its removal unless debugging. +# Note that there is a small window in which the directory will not be cleaned: +# after its creation but before its name has been assigned to `$tmp'. +$debug || +{ + tmp= ac_tmp= + trap 'exit_status=$? + : "${ac_tmp:=$tmp}" + { test ! -d "$ac_tmp" || rm -fr "$ac_tmp"; } && exit $exit_status +' 0 + trap 'as_fn_exit 1' 1 2 13 15 +} +# Create a (secure) tmp directory for tmp files. + +{ + tmp=`(umask 077 && mktemp -d "./confXXXXXX") 2>/dev/null` && + test -d "$tmp" +} || +{ + tmp=./conf$$-$RANDOM + (umask 077 && mkdir "$tmp") +} || as_fn_error $? "cannot create a temporary directory in ." "$LINENO" 5 +ac_tmp=$tmp + +# Set up the scripts for CONFIG_FILES section. +# No need to generate them if there are no CONFIG_FILES. +# This happens for instance with `./config.status config.h'. +if test -n "$CONFIG_FILES"; then + + +ac_cr=`echo X | tr X '\015'` +# On cygwin, bash can eat \r inside `` if the user requested igncr. +# But we know of no other shell where ac_cr would be empty at this +# point, so we can use a bashism as a fallback. +if test "x$ac_cr" = x; then + eval ac_cr=\$\'\\r\' +fi +ac_cs_awk_cr=`$AWK 'BEGIN { print "a\rb" }' /dev/null` +if test "$ac_cs_awk_cr" = "a${ac_cr}b"; then + ac_cs_awk_cr='\\r' +else + ac_cs_awk_cr=$ac_cr +fi + +echo 'BEGIN {' >"$ac_tmp/subs1.awk" && +cat >>"$ac_tmp/subs1.awk" <<\_ACAWK && +S["am__EXEEXT_FALSE"]="" +S["am__EXEEXT_TRUE"]="#" +S["LTLIBOBJS"]="" +S["LIBOBJS"]="" +S["EGREP"]="/usr/bin/grep -E" +S["GREP"]="/usr/bin/grep" +S["CPP"]="gcc -E" +S["am__fastdepCC_FALSE"]="#" +S["am__fastdepCC_TRUE"]="" +S["CCDEPMODE"]="depmode=gcc3" +S["ac_ct_CC"]="gcc" +S["CFLAGS"]="-g -O2" +S["CC"]="gcc" +S["am__fastdepCXX_FALSE"]="#" +S["am__fastdepCXX_TRUE"]="" +S["CXXDEPMODE"]="depmode=gcc3" +S["am__nodep"]="_no" +S["AMDEPBACKSLASH"]="\\" +S["AMDEP_FALSE"]="#" +S["AMDEP_TRUE"]="" +S["am__quote"]="" +S["am__include"]="include" +S["DEPDIR"]=".deps" +S["OBJEXT"]="o" +S["EXEEXT"]="" +S["ac_ct_CXX"]="g++" +S["CPPFLAGS"]="" +S["LDFLAGS"]="" +S["CXXFLAGS"]="-g -O2" +S["CXX"]="g++" +S["AM_BACKSLASH"]="\\" +S["AM_DEFAULT_VERBOSITY"]="1" +S["AM_DEFAULT_V"]="$(AM_DEFAULT_VERBOSITY)" +S["AM_V"]="$(V)" +S["am__untar"]="$${TAR-tar} xf -" +S["am__tar"]="$${TAR-tar} chof - \"$$tardir\"" +S["AMTAR"]="$${TAR-tar}" +S["am__leading_dot"]="." +S["SET_MAKE"]="" +S["AWK"]="gawk" +S["mkdir_p"]="$(MKDIR_P)" +S["MKDIR_P"]="/usr/local/bin/gmkdir -p" +S["INSTALL_STRIP_PROGRAM"]="$(install_sh) -c -s" +S["STRIP"]="" +S["install_sh"]="${SHELL} /home/david/devel/cpp/lionheart000916/install-sh" +S["MAKEINFO"]="${SHELL} /home/david/devel/cpp/lionheart000916/missing makeinfo" +S["AUTOHEADER"]="${SHELL} /home/david/devel/cpp/lionheart000916/missing autoheader" +S["AUTOMAKE"]="${SHELL} /home/david/devel/cpp/lionheart000916/missing automake-1.15" +S["AUTOCONF"]="${SHELL} /home/david/devel/cpp/lionheart000916/missing autoconf" +S["ACLOCAL"]="${SHELL} /home/david/devel/cpp/lionheart000916/missing aclocal-1.15" +S["VERSION"]="20000916" +S["PACKAGE"]="lionheart" +S["CYGPATH_W"]="echo" +S["am__isrc"]="" +S["INSTALL_DATA"]="${INSTALL} -m 644" +S["INSTALL_SCRIPT"]="${INSTALL}" +S["INSTALL_PROGRAM"]="${INSTALL}" +S["target_alias"]="" +S["host_alias"]="" +S["build_alias"]="" +S["LIBS"]="" +S["ECHO_T"]="" +S["ECHO_N"]="-n" +S["ECHO_C"]="" +S["DEFS"]="-DHAVE_CONFIG_H" +S["mandir"]="${datarootdir}/man" +S["localedir"]="${datarootdir}/locale" +S["libdir"]="${exec_prefix}/lib" +S["psdir"]="${docdir}" +S["pdfdir"]="${docdir}" +S["dvidir"]="${docdir}" +S["htmldir"]="${docdir}" +S["infodir"]="${datarootdir}/info" +S["docdir"]="${datarootdir}/doc/${PACKAGE_TARNAME}" +S["oldincludedir"]="/usr/include" +S["includedir"]="${prefix}/include" +S["localstatedir"]="${prefix}/var" +S["sharedstatedir"]="${prefix}/com" +S["sysconfdir"]="${prefix}/etc" +S["datadir"]="${datarootdir}" +S["datarootdir"]="${prefix}/share" +S["libexecdir"]="${exec_prefix}/libexec" +S["sbindir"]="${exec_prefix}/sbin" +S["bindir"]="${exec_prefix}/bin" +S["program_transform_name"]="s,x,x," +S["prefix"]="/usr/local" +S["exec_prefix"]="${prefix}" +S["PACKAGE_URL"]="" +S["PACKAGE_BUGREPORT"]="" +S["PACKAGE_STRING"]="lionheart 20000916" +S["PACKAGE_VERSION"]="20000916" +S["PACKAGE_TARNAME"]="lionheart" +S["PACKAGE_NAME"]="lionheart" +S["PATH_SEPARATOR"]=":" +S["SHELL"]="/bin/sh" +_ACAWK +cat >>"$ac_tmp/subs1.awk" <<_ACAWK && + for (key in S) S_is_set[key] = 1 + FS = "" + +} +{ + line = $ 0 + nfields = split(line, field, "@") + substed = 0 + len = length(field[1]) + for (i = 2; i < nfields; i++) { + key = field[i] + keylen = length(key) + if (S_is_set[key]) { + value = S[key] + line = substr(line, 1, len) "" value "" substr(line, len + keylen + 3) + len += length(value) + length(field[++i]) + substed = 1 + } else + len += 1 + keylen + } + + print line +} + +_ACAWK +if sed "s/$ac_cr//" < /dev/null > /dev/null 2>&1; then + sed "s/$ac_cr\$//; s/$ac_cr/$ac_cs_awk_cr/g" +else + cat +fi < "$ac_tmp/subs1.awk" > "$ac_tmp/subs.awk" \ + || as_fn_error $? "could not setup config files machinery" "$LINENO" 5 +fi # test -n "$CONFIG_FILES" + +# Set up the scripts for CONFIG_HEADERS section. +# No need to generate them if there are no CONFIG_HEADERS. +# This happens for instance with `./config.status Makefile'. +if test -n "$CONFIG_HEADERS"; then +cat >"$ac_tmp/defines.awk" <<\_ACAWK || +BEGIN { +D["PACKAGE_NAME"]=" \"lionheart\"" +D["PACKAGE_TARNAME"]=" \"lionheart\"" +D["PACKAGE_VERSION"]=" \"20000916\"" +D["PACKAGE_STRING"]=" \"lionheart 20000916\"" +D["PACKAGE_BUGREPORT"]=" \"\"" +D["PACKAGE_URL"]=" \"\"" +D["PACKAGE"]=" \"lionheart\"" +D["VERSION"]=" \"20000916\"" +D["STDC_HEADERS"]=" 1" +D["HAVE_SYS_TYPES_H"]=" 1" +D["HAVE_SYS_STAT_H"]=" 1" +D["HAVE_STDLIB_H"]=" 1" +D["HAVE_STRING_H"]=" 1" +D["HAVE_MEMORY_H"]=" 1" +D["HAVE_STRINGS_H"]=" 1" +D["HAVE_INTTYPES_H"]=" 1" +D["HAVE_STDINT_H"]=" 1" +D["HAVE_UNISTD_H"]=" 1" +D["HAVE_STRING_H"]=" 1" +D["HAVE__BOOL"]=" 1" +D["HAVE_STRCASECMP"]=" 1" +D["HAVE_STRDUP"]=" 1" + for (key in D) D_is_set[key] = 1 + FS = "" +} +/^[\t ]*#[\t ]*(define|undef)[\t ]+[_abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ][_abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789]*([\t (]|$)/ { + line = $ 0 + split(line, arg, " ") + if (arg[1] == "#") { + defundef = arg[2] + mac1 = arg[3] + } else { + defundef = substr(arg[1], 2) + mac1 = arg[2] + } + split(mac1, mac2, "(") #) + macro = mac2[1] + prefix = substr(line, 1, index(line, defundef) - 1) + if (D_is_set[macro]) { + # Preserve the white space surrounding the "#". + print prefix "define", macro P[macro] D[macro] + next + } else { + # Replace #undef with comments. This is necessary, for example, + # in the case of _POSIX_SOURCE, which is predefined and required + # on some systems where configure will not decide to define it. + if (defundef == "undef") { + print "/*", prefix defundef, macro, "*/" + next + } + } +} +{ print } +_ACAWK + as_fn_error $? "could not setup config headers machinery" "$LINENO" 5 +fi # test -n "$CONFIG_HEADERS" + + +eval set X " :F $CONFIG_FILES :H $CONFIG_HEADERS :C $CONFIG_COMMANDS" +shift +for ac_tag +do + case $ac_tag in + :[FHLC]) ac_mode=$ac_tag; continue;; + esac + case $ac_mode$ac_tag in + :[FHL]*:*);; + :L* | :C*:*) as_fn_error $? "invalid tag \`$ac_tag'" "$LINENO" 5;; + :[FH]-) ac_tag=-:-;; + :[FH]*) ac_tag=$ac_tag:$ac_tag.in;; + esac + ac_save_IFS=$IFS + IFS=: + set x $ac_tag + IFS=$ac_save_IFS + shift + ac_file=$1 + shift + + case $ac_mode in + :L) ac_source=$1;; + :[FH]) + ac_file_inputs= + for ac_f + do + case $ac_f in + -) ac_f="$ac_tmp/stdin";; + *) # Look for the file first in the build tree, then in the source tree + # (if the path is not absolute). The absolute path cannot be DOS-style, + # because $ac_f cannot contain `:'. + test -f "$ac_f" || + case $ac_f in + [\\/$]*) false;; + *) test -f "$srcdir/$ac_f" && ac_f="$srcdir/$ac_f";; + esac || + as_fn_error 1 "cannot find input file: \`$ac_f'" "$LINENO" 5;; + esac + case $ac_f in *\'*) ac_f=`$as_echo "$ac_f" | sed "s/'/'\\\\\\\\''/g"`;; esac + as_fn_append ac_file_inputs " '$ac_f'" + done + + # Let's still pretend it is `configure' which instantiates (i.e., don't + # use $as_me), people would be surprised to read: + # /* config.h. Generated by config.status. */ + configure_input='Generated from '` + $as_echo "$*" | sed 's|^[^:]*/||;s|:[^:]*/|, |g' + `' by configure.' + if test x"$ac_file" != x-; then + configure_input="$ac_file. $configure_input" + { $as_echo "$as_me:${as_lineno-$LINENO}: creating $ac_file" >&5 +$as_echo "$as_me: creating $ac_file" >&6;} + fi + # Neutralize special characters interpreted by sed in replacement strings. + case $configure_input in #( + *\&* | *\|* | *\\* ) + ac_sed_conf_input=`$as_echo "$configure_input" | + sed 's/[\\\\&|]/\\\\&/g'`;; #( + *) ac_sed_conf_input=$configure_input;; + esac + + case $ac_tag in + *:-:* | *:-) cat >"$ac_tmp/stdin" \ + || as_fn_error $? "could not create $ac_file" "$LINENO" 5 ;; + esac + ;; + esac + + ac_dir=`$as_dirname -- "$ac_file" || +$as_expr X"$ac_file" : 'X\(.*[^/]\)//*[^/][^/]*/*$' \| \ + X"$ac_file" : 'X\(//\)[^/]' \| \ + X"$ac_file" : 'X\(//\)$' \| \ + X"$ac_file" : 'X\(/\)' \| . 2>/dev/null || +$as_echo X"$ac_file" | + sed '/^X\(.*[^/]\)\/\/*[^/][^/]*\/*$/{ + s//\1/ + q + } + /^X\(\/\/\)[^/].*/{ + s//\1/ + q + } + /^X\(\/\/\)$/{ + s//\1/ + q + } + /^X\(\/\).*/{ + s//\1/ + q + } + s/.*/./; q'` + as_dir="$ac_dir"; as_fn_mkdir_p + ac_builddir=. + +case "$ac_dir" in +.) ac_dir_suffix= ac_top_builddir_sub=. ac_top_build_prefix= ;; +*) + ac_dir_suffix=/`$as_echo "$ac_dir" | sed 's|^\.[\\/]||'` + # A ".." for each directory in $ac_dir_suffix. + ac_top_builddir_sub=`$as_echo "$ac_dir_suffix" | sed 's|/[^\\/]*|/..|g;s|/||'` + case $ac_top_builddir_sub in + "") ac_top_builddir_sub=. ac_top_build_prefix= ;; + *) ac_top_build_prefix=$ac_top_builddir_sub/ ;; + esac ;; +esac +ac_abs_top_builddir=$ac_pwd +ac_abs_builddir=$ac_pwd$ac_dir_suffix +# for backward compatibility: +ac_top_builddir=$ac_top_build_prefix + +case $srcdir in + .) # We are building in place. + ac_srcdir=. + ac_top_srcdir=$ac_top_builddir_sub + ac_abs_top_srcdir=$ac_pwd ;; + [\\/]* | ?:[\\/]* ) # Absolute name. + ac_srcdir=$srcdir$ac_dir_suffix; + ac_top_srcdir=$srcdir + ac_abs_top_srcdir=$srcdir ;; + *) # Relative name. + ac_srcdir=$ac_top_build_prefix$srcdir$ac_dir_suffix + ac_top_srcdir=$ac_top_build_prefix$srcdir + ac_abs_top_srcdir=$ac_pwd/$srcdir ;; +esac +ac_abs_srcdir=$ac_abs_top_srcdir$ac_dir_suffix + + + case $ac_mode in + :F) + # + # CONFIG_FILE + # + + case $INSTALL in + [\\/$]* | ?:[\\/]* ) ac_INSTALL=$INSTALL ;; + *) ac_INSTALL=$ac_top_build_prefix$INSTALL ;; + esac + ac_MKDIR_P=$MKDIR_P + case $MKDIR_P in + [\\/$]* | ?:[\\/]* ) ;; + */*) ac_MKDIR_P=$ac_top_build_prefix$MKDIR_P ;; + esac +# If the template does not know about datarootdir, expand it. +# FIXME: This hack should be removed a few years after 2.60. +ac_datarootdir_hack=; ac_datarootdir_seen= +ac_sed_dataroot=' +/datarootdir/ { + p + q +} +/@datadir@/p +/@docdir@/p +/@infodir@/p +/@localedir@/p +/@mandir@/p' +case `eval "sed -n \"\$ac_sed_dataroot\" $ac_file_inputs"` in +*datarootdir*) ac_datarootdir_seen=yes;; +*@datadir@*|*@docdir@*|*@infodir@*|*@localedir@*|*@mandir@*) + { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: $ac_file_inputs seems to ignore the --datarootdir setting" >&5 +$as_echo "$as_me: WARNING: $ac_file_inputs seems to ignore the --datarootdir setting" >&2;} + ac_datarootdir_hack=' + s&@datadir@&${datarootdir}&g + s&@docdir@&${datarootdir}/doc/${PACKAGE_TARNAME}&g + s&@infodir@&${datarootdir}/info&g + s&@localedir@&${datarootdir}/locale&g + s&@mandir@&${datarootdir}/man&g + s&\${datarootdir}&${prefix}/share&g' ;; +esac +ac_sed_extra="/^[ ]*VPATH[ ]*=[ ]*/{ +h +s/// +s/^/:/ +s/[ ]*$/:/ +s/:\$(srcdir):/:/g +s/:\${srcdir}:/:/g +s/:@srcdir@:/:/g +s/^:*// +s/:*$// +x +s/\(=[ ]*\).*/\1/ +G +s/\n// +s/^[^=]*=[ ]*$// +} + +:t +/@[a-zA-Z_][a-zA-Z_0-9]*@/!b +s|@configure_input@|$ac_sed_conf_input|;t t +s&@top_builddir@&$ac_top_builddir_sub&;t t +s&@top_build_prefix@&$ac_top_build_prefix&;t t +s&@srcdir@&$ac_srcdir&;t t +s&@abs_srcdir@&$ac_abs_srcdir&;t t +s&@top_srcdir@&$ac_top_srcdir&;t t +s&@abs_top_srcdir@&$ac_abs_top_srcdir&;t t +s&@builddir@&$ac_builddir&;t t +s&@abs_builddir@&$ac_abs_builddir&;t t +s&@abs_top_builddir@&$ac_abs_top_builddir&;t t +s&@INSTALL@&$ac_INSTALL&;t t +s&@MKDIR_P@&$ac_MKDIR_P&;t t +$ac_datarootdir_hack +" +eval sed \"\$ac_sed_extra\" "$ac_file_inputs" | $AWK -f "$ac_tmp/subs.awk" \ + >$ac_tmp/out || as_fn_error $? "could not create $ac_file" "$LINENO" 5 + +test -z "$ac_datarootdir_hack$ac_datarootdir_seen" && + { ac_out=`sed -n '/\${datarootdir}/p' "$ac_tmp/out"`; test -n "$ac_out"; } && + { ac_out=`sed -n '/^[ ]*datarootdir[ ]*:*=/p' \ + "$ac_tmp/out"`; test -z "$ac_out"; } && + { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: $ac_file contains a reference to the variable \`datarootdir' +which seems to be undefined. Please make sure it is defined" >&5 +$as_echo "$as_me: WARNING: $ac_file contains a reference to the variable \`datarootdir' +which seems to be undefined. Please make sure it is defined" >&2;} + + rm -f "$ac_tmp/stdin" + case $ac_file in + -) cat "$ac_tmp/out" && rm -f "$ac_tmp/out";; + *) rm -f "$ac_file" && mv "$ac_tmp/out" "$ac_file";; + esac \ + || as_fn_error $? "could not create $ac_file" "$LINENO" 5 + ;; + :H) + # + # CONFIG_HEADER + # + if test x"$ac_file" != x-; then + { + $as_echo "/* $configure_input */" \ + && eval '$AWK -f "$ac_tmp/defines.awk"' "$ac_file_inputs" + } >"$ac_tmp/config.h" \ + || as_fn_error $? "could not create $ac_file" "$LINENO" 5 + if diff "$ac_file" "$ac_tmp/config.h" >/dev/null 2>&1; then + { $as_echo "$as_me:${as_lineno-$LINENO}: $ac_file is unchanged" >&5 +$as_echo "$as_me: $ac_file is unchanged" >&6;} + else + rm -f "$ac_file" + mv "$ac_tmp/config.h" "$ac_file" \ + || as_fn_error $? "could not create $ac_file" "$LINENO" 5 + fi + else + $as_echo "/* $configure_input */" \ + && eval '$AWK -f "$ac_tmp/defines.awk"' "$ac_file_inputs" \ + || as_fn_error $? "could not create -" "$LINENO" 5 + fi +# Compute "$ac_file"'s index in $config_headers. +_am_arg="$ac_file" +_am_stamp_count=1 +for _am_header in $config_headers :; do + case $_am_header in + $_am_arg | $_am_arg:* ) + break ;; + * ) + _am_stamp_count=`expr $_am_stamp_count + 1` ;; + esac +done +echo "timestamp for $_am_arg" >`$as_dirname -- "$_am_arg" || +$as_expr X"$_am_arg" : 'X\(.*[^/]\)//*[^/][^/]*/*$' \| \ + X"$_am_arg" : 'X\(//\)[^/]' \| \ + X"$_am_arg" : 'X\(//\)$' \| \ + X"$_am_arg" : 'X\(/\)' \| . 2>/dev/null || +$as_echo X"$_am_arg" | + sed '/^X\(.*[^/]\)\/\/*[^/][^/]*\/*$/{ + s//\1/ + q + } + /^X\(\/\/\)[^/].*/{ + s//\1/ + q + } + /^X\(\/\/\)$/{ + s//\1/ + q + } + /^X\(\/\).*/{ + s//\1/ + q + } + s/.*/./; q'`/stamp-h$_am_stamp_count + ;; + + :C) { $as_echo "$as_me:${as_lineno-$LINENO}: executing $ac_file commands" >&5 +$as_echo "$as_me: executing $ac_file commands" >&6;} + ;; + esac + + + case $ac_file$ac_mode in + "depfiles":C) test x"$AMDEP_TRUE" != x"" || { + # Older Autoconf quotes --file arguments for eval, but not when files + # are listed without --file. Let's play safe and only enable the eval + # if we detect the quoting. + case $CONFIG_FILES in + *\'*) eval set x "$CONFIG_FILES" ;; + *) set x $CONFIG_FILES ;; + esac + shift + for mf + do + # Strip MF so we end up with the name of the file. + mf=`echo "$mf" | sed -e 's/:.*$//'` + # Check whether this is an Automake generated Makefile or not. + # We used to match only the files named 'Makefile.in', but + # some people rename them; so instead we look at the file content. + # Grep'ing the first line is not enough: some people post-process + # each Makefile.in and add a new line on top of each file to say so. + # Grep'ing the whole file is not good either: AIX grep has a line + # limit of 2048, but all sed's we know have understand at least 4000. + if sed -n 's,^#.*generated by automake.*,X,p' "$mf" | grep X >/dev/null 2>&1; then + dirpart=`$as_dirname -- "$mf" || +$as_expr X"$mf" : 'X\(.*[^/]\)//*[^/][^/]*/*$' \| \ + X"$mf" : 'X\(//\)[^/]' \| \ + X"$mf" : 'X\(//\)$' \| \ + X"$mf" : 'X\(/\)' \| . 2>/dev/null || +$as_echo X"$mf" | + sed '/^X\(.*[^/]\)\/\/*[^/][^/]*\/*$/{ + s//\1/ + q + } + /^X\(\/\/\)[^/].*/{ + s//\1/ + q + } + /^X\(\/\/\)$/{ + s//\1/ + q + } + /^X\(\/\).*/{ + s//\1/ + q + } + s/.*/./; q'` + else + continue + fi + # Extract the definition of DEPDIR, am__include, and am__quote + # from the Makefile without running 'make'. + DEPDIR=`sed -n 's/^DEPDIR = //p' < "$mf"` + test -z "$DEPDIR" && continue + am__include=`sed -n 's/^am__include = //p' < "$mf"` + test -z "$am__include" && continue + am__quote=`sed -n 's/^am__quote = //p' < "$mf"` + # Find all dependency output files, they are included files with + # $(DEPDIR) in their names. We invoke sed twice because it is the + # simplest approach to changing $(DEPDIR) to its actual value in the + # expansion. + for file in `sed -n " + s/^$am__include $am__quote\(.*(DEPDIR).*\)$am__quote"'$/\1/p' <"$mf" | \ + sed -e 's/\$(DEPDIR)/'"$DEPDIR"'/g'`; do + # Make sure the directory exists. + test -f "$dirpart/$file" && continue + fdir=`$as_dirname -- "$file" || +$as_expr X"$file" : 'X\(.*[^/]\)//*[^/][^/]*/*$' \| \ + X"$file" : 'X\(//\)[^/]' \| \ + X"$file" : 'X\(//\)$' \| \ + X"$file" : 'X\(/\)' \| . 2>/dev/null || +$as_echo X"$file" | + sed '/^X\(.*[^/]\)\/\/*[^/][^/]*\/*$/{ + s//\1/ + q + } + /^X\(\/\/\)[^/].*/{ + s//\1/ + q + } + /^X\(\/\/\)$/{ + s//\1/ + q + } + /^X\(\/\).*/{ + s//\1/ + q + } + s/.*/./; q'` + as_dir=$dirpart/$fdir; as_fn_mkdir_p + # echo "creating $dirpart/$file" + echo '# dummy' > "$dirpart/$file" + done + done +} + ;; + + esac +done # for ac_tag + + +as_fn_exit 0 diff --git a/configure.ac b/configure.ac new file mode 100644 index 0000000..1a3d2ed --- /dev/null +++ b/configure.ac @@ -0,0 +1,30 @@ +# -*- Autoconf -*- +# Process this file with autoconf to produce a configure script. + +AC_PREREQ([2.69]) +AC_INIT([lionheart], [20000916]) +AM_INIT_AUTOMAKE([-Wall -Werror foreign]) +#AC_CONFIG_SRCDIR([main.cc]) +AC_CONFIG_SRCDIR([config.h.in]) +AC_CONFIG_HEADERS([config.h]) + +# Checks for programs. +AC_PROG_CXX +AC_PROG_CC +AC_PROG_CPP + +# Checks for libraries. + +# Checks for header files. +AC_CHECK_HEADERS([string.h]) + +# Checks for typedefs, structures, and compiler characteristics. +AC_CHECK_HEADER_STDBOOL +AC_C_INLINE + +# Checks for library functions. +AC_CHECK_FUNCS([strcasecmp strdup]) + +AC_CONFIG_FILES([Makefile + src/Makefile]) +AC_OUTPUT diff --git a/log.txt b/log.txt new file mode 100644 index 0000000..296ba4a --- /dev/null +++ b/log.txt @@ -0,0 +1,5 @@ +05/01/99 - Added "backup" pseudo-rule to allow for correcting mistakes. + - Wrote simple lexer to avoid having to use flex. This one + uses C++ input streams much more cleanly. + - Prettified some of the .h and .cc files with comments. +8/14/99, 11:02 PM -- Trying to add support for "hidden" axioms. Problem: Proof:applyRule does not properly apply axioms (add to lhs). diff --git a/src/Axiom.cc b/src/Axiom.cc new file mode 100644 index 0000000..9ef3dcf --- /dev/null +++ b/src/Axiom.cc @@ -0,0 +1,113 @@ +/* $Id: Axiom.cc,v 1.3 2000/01/24 17:42:52 david Exp $ */ + +/* Axiom.cc + by David Baer, 8/14/99 + Routines for storing and indexing a list of axioms +*/ + +#include +#include +#include "Axiom.h" +#include "parser.h" + +using namespace std; + +#ifndef NULL +#define NULL 0 +#endif + +AxiomTable::AxiomTable(unsigned sz) +{ + tblSize = sz; + data = new AxiomList[tblSize]; +} + +static inline +unsigned hashItem(char *key, unsigned modulus) +{ + unsigned result = 0, i; + + for (i = 0; i < strlen(key); i++) + result = (256 * result + (unsigned)key[i]) % modulus; + + return result; +} + +void AxiomTable::addAxiom(Axiom *ax) +{ + unsigned pos = hashItem(ax->getName(), tblSize); + data[pos].addElement(ax); +} + +void AxiomTable::addAxioms(char *filename) +{ + ifstream istr(filename); + char inbuf[1024]; + + cout << "Reading axioms from " << filename << "... " << flush; + + while (istr.getline(inbuf, 1022)) + { + if (strlen(inbuf) && (inbuf[0] != '#')) + { + char *name = strtok(inbuf, ":"), + *formstr = strtok(NULL, ":"); + + cout << name << " " << flush; + initParser(formstr); + PropFormula *form = parseFormula(); + endParser(); + + this->addAxiom(new Axiom(name, form)); + } + } + cout << endl; + +} + +void AxiomTable::printAxioms(ostream &o) +{ + unsigned i; + + for (i = 0; i < tblSize; i++) + { + unsigned j; + for (j = 0; j < data[i].size(); j++) + { + o << data[i](j)->getName() << ": "; + data[i](j)->getFormula()->println(o); + } + } +} + +Vector AxiomTable::getVector() +{ + unsigned i; + Vector result; + + for (i = 0; i < tblSize; i++) + { + unsigned j; + for (j = 0; j < data[i].size(); j++) + result.addElement(data[i](j)->getFormula()); + } + + return result; +} + +PropFormula *AxiomTable::getAxiom(char *name) +{ + unsigned key = hashItem(name, tblSize), + i; + + for (i = 0; i < data[key].size(); i++) + if (!strcmp(data[key](i)->getName(), name)) + return data[key](i)->getFormula(); + + cerr << "Error! Couldn't find axiom!" << endl; + return NULL; +} + + +AxiomTable axioms; + diff --git a/src/Axiom.h b/src/Axiom.h new file mode 100644 index 0000000..a54ddbf --- /dev/null +++ b/src/Axiom.h @@ -0,0 +1,51 @@ +/* $Id: Axiom.h,v 1.3 2000/01/24 17:42:52 david Exp $ */ + +/* Axiom.h + by David Baer, 8/14/99 + Routines for storing and indexing a list of axioms +*/ + +#ifndef _AXIOM_H +#define _AXIOM_H + +#include +#include "formula.h" +#include "Vector.h" + +using namespace std; + +class Axiom +{ + char *name; + PropFormula *formula; + public: + Axiom(char *n, PropFormula *f) { name = strdup(n); formula = f; } + + char *getName() { return name; } + PropFormula *getFormula() { return formula; } +}; + +typedef Vector AxiomList; + +/* store in hash table, resolve collisions by chaining */ +class AxiomTable +{ + AxiomList *data; + unsigned tblSize; + public: + AxiomTable(unsigned sz = 100); + + void addAxiom(Axiom *); + void addAxioms(char * /* filename */); + + PropFormula *getAxiom(char * /* name */); + + Vector getVector(); + + void printAxioms(ostream &); +}; + +extern +AxiomTable axioms; + +#endif /* !def _AXIOM_H */ diff --git a/src/FormulaRegistry.cc b/src/FormulaRegistry.cc new file mode 100644 index 0000000..012fc6e --- /dev/null +++ b/src/FormulaRegistry.cc @@ -0,0 +1,31 @@ +// $Id: FormulaRegistry.cc,v 1.4 2000/01/24 17:42:52 david Exp $ + +// FormulaRegistry.cc +// Keep track of extra generated formulae in order to facilitate +// killing them off later on. + +#include +#include "FormulaRegistry.h" + +using namespace std; + +void FormulaRegistry::annihilate() +// destroy extra formulae -- broken at present (generates a SEGV) +{ + unsigned i; + + cout << "The following excess formulas will be deleted: " << endl; + for (i = 0; i < list.size(); i++) + list(i)->println(cout); + if (!killed) + for (i = 0; i < list.size(); i++) + { + cout << "deleting: " << flush; + list(i)->println(cout); + delete list(i); + cout << "deleted." << endl; + } + + killed = 1; +} + diff --git a/src/FormulaRegistry.h b/src/FormulaRegistry.h new file mode 100644 index 0000000..b56fe54 --- /dev/null +++ b/src/FormulaRegistry.h @@ -0,0 +1,26 @@ +// $Id: FormulaRegistry.h,v 1.3 2000/01/24 17:42:52 david Exp $ + +// FormulaRegistry.h +// Definitions for a formula registry to keep track of extra +// generated formulae. These can then be deleted at convenience +// with the annhiliate() method. +// (Currently broker) + +#ifndef _FORMULAREGISTRY_H +#define _FORMULAREGISTRY_H + +#include "formula.h" +#include "Vector.h" + +class FormulaRegistry +{ + Vector list; // growable list of formulae + int killed; // set to 1 if formulae already destroyed +public: + FormulaRegistry() { killed = 0; } + void addFormula(PropFormula *f) { list.addElement(f); } + void annihilate(); +}; + +#endif /* !_FORMULAREGISTRY_H */ + diff --git a/src/Makefile b/src/Makefile new file mode 100644 index 0000000..6bd153c --- /dev/null +++ b/src/Makefile @@ -0,0 +1,582 @@ +# Makefile.in generated by automake 1.15 from Makefile.am. +# src/Makefile. Generated from Makefile.in by configure. + +# Copyright (C) 1994-2014 Free Software Foundation, Inc. + +# This Makefile.in is free software; the Free Software Foundation +# gives unlimited permission to copy and/or distribute it, +# with or without modifications, as long as this notice is preserved. + +# This program is distributed in the hope that it will be useful, +# but WITHOUT ANY WARRANTY, to the extent permitted by law; without +# even the implied warranty of MERCHANTABILITY or FITNESS FOR A +# PARTICULAR PURPOSE. + + + + +am__is_gnu_make = { \ + if test -z '$(MAKELEVEL)'; then \ + false; \ + elif test -n '$(MAKE_HOST)'; then \ + true; \ + elif test -n '$(MAKE_VERSION)' && test -n '$(CURDIR)'; then \ + true; \ + else \ + false; \ + fi; \ +} +am__make_running_with_option = \ + case $${target_option-} in \ + ?) ;; \ + *) echo "am__make_running_with_option: internal error: invalid" \ + "target option '$${target_option-}' specified" >&2; \ + exit 1;; \ + esac; \ + has_opt=no; \ + sane_makeflags=$$MAKEFLAGS; \ + if $(am__is_gnu_make); then \ + sane_makeflags=$$MFLAGS; \ + else \ + case $$MAKEFLAGS in \ + *\\[\ \ ]*) \ + bs=\\; \ + sane_makeflags=`printf '%s\n' "$$MAKEFLAGS" \ + | sed "s/$$bs$$bs[$$bs $$bs ]*//g"`;; \ + esac; \ + fi; \ + skip_next=no; \ + strip_trailopt () \ + { \ + flg=`printf '%s\n' "$$flg" | sed "s/$$1.*$$//"`; \ + }; \ + for flg in $$sane_makeflags; do \ + test $$skip_next = yes && { skip_next=no; continue; }; \ + case $$flg in \ + *=*|--*) continue;; \ + -*I) strip_trailopt 'I'; skip_next=yes;; \ + -*I?*) strip_trailopt 'I';; \ + -*O) strip_trailopt 'O'; skip_next=yes;; \ + -*O?*) strip_trailopt 'O';; \ + -*l) strip_trailopt 'l'; skip_next=yes;; \ + -*l?*) strip_trailopt 'l';; \ + -[dEDm]) skip_next=yes;; \ + -[JT]) skip_next=yes;; \ + esac; \ + case $$flg in \ + *$$target_option*) has_opt=yes; break;; \ + esac; \ + done; \ + test $$has_opt = yes +am__make_dryrun = (target_option=n; $(am__make_running_with_option)) +am__make_keepgoing = (target_option=k; $(am__make_running_with_option)) +pkgdatadir = $(datadir)/lionheart +pkgincludedir = $(includedir)/lionheart +pkglibdir = $(libdir)/lionheart +pkglibexecdir = $(libexecdir)/lionheart +am__cd = CDPATH="$${ZSH_VERSION+.}$(PATH_SEPARATOR)" && cd +install_sh_DATA = $(install_sh) -c -m 644 +install_sh_PROGRAM = $(install_sh) -c +install_sh_SCRIPT = $(install_sh) -c +INSTALL_HEADER = $(INSTALL_DATA) +transform = $(program_transform_name) +NORMAL_INSTALL = : +PRE_INSTALL = : +POST_INSTALL = : +NORMAL_UNINSTALL = : +PRE_UNINSTALL = : +POST_UNINSTALL = : +bin_PROGRAMS = lionheart$(EXEEXT) +subdir = src +ACLOCAL_M4 = $(top_srcdir)/aclocal.m4 +am__aclocal_m4_deps = $(top_srcdir)/configure.ac +am__configure_deps = $(am__aclocal_m4_deps) $(CONFIGURE_DEPENDENCIES) \ + $(ACLOCAL_M4) +DIST_COMMON = $(srcdir)/Makefile.am $(am__DIST_COMMON) +mkinstalldirs = $(install_sh) -d +CONFIG_HEADER = $(top_builddir)/config.h +CONFIG_CLEAN_FILES = +CONFIG_CLEAN_VPATH_FILES = +am__installdirs = "$(DESTDIR)$(bindir)" +PROGRAMS = $(bin_PROGRAMS) +am_lionheart_OBJECTS = lex.$(OBJEXT) main.$(OBJEXT) formula.$(OBJEXT) \ + parser.$(OBJEXT) ParamSource.$(OBJEXT) Proof.$(OBJEXT) \ + Rule.$(OBJEXT) RuleSource.$(OBJEXT) FormulaRegistry.$(OBJEXT) \ + Options.$(OBJEXT) Axiom.$(OBJEXT) copysplit.$(OBJEXT) +lionheart_OBJECTS = $(am_lionheart_OBJECTS) +lionheart_LDADD = $(LDADD) +AM_V_P = $(am__v_P_$(V)) +am__v_P_ = $(am__v_P_$(AM_DEFAULT_VERBOSITY)) +am__v_P_0 = false +am__v_P_1 = : +AM_V_GEN = $(am__v_GEN_$(V)) +am__v_GEN_ = $(am__v_GEN_$(AM_DEFAULT_VERBOSITY)) +am__v_GEN_0 = @echo " GEN " $@; +am__v_GEN_1 = +AM_V_at = $(am__v_at_$(V)) +am__v_at_ = $(am__v_at_$(AM_DEFAULT_VERBOSITY)) +am__v_at_0 = @ +am__v_at_1 = +DEFAULT_INCLUDES = -I. -I$(top_builddir) +depcomp = $(SHELL) $(top_srcdir)/depcomp +am__depfiles_maybe = depfiles +am__mv = mv -f +CXXCOMPILE = $(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \ + $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS) +AM_V_CXX = $(am__v_CXX_$(V)) +am__v_CXX_ = $(am__v_CXX_$(AM_DEFAULT_VERBOSITY)) +am__v_CXX_0 = @echo " CXX " $@; +am__v_CXX_1 = +CXXLD = $(CXX) +CXXLINK = $(CXXLD) $(AM_CXXFLAGS) $(CXXFLAGS) $(AM_LDFLAGS) $(LDFLAGS) \ + -o $@ +AM_V_CXXLD = $(am__v_CXXLD_$(V)) +am__v_CXXLD_ = $(am__v_CXXLD_$(AM_DEFAULT_VERBOSITY)) +am__v_CXXLD_0 = @echo " CXXLD " $@; +am__v_CXXLD_1 = +SOURCES = $(lionheart_SOURCES) +DIST_SOURCES = $(lionheart_SOURCES) +am__can_run_installinfo = \ + case $$AM_UPDATE_INFO_DIR in \ + n|no|NO) false;; \ + *) (install-info --version) >/dev/null 2>&1;; \ + esac +am__tagged_files = $(HEADERS) $(SOURCES) $(TAGS_FILES) $(LISP) +# Read a list of newline-separated strings from the standard input, +# and print each of them once, without duplicates. Input order is +# *not* preserved. +am__uniquify_input = $(AWK) '\ + BEGIN { nonempty = 0; } \ + { items[$$0] = 1; nonempty = 1; } \ + END { if (nonempty) { for (i in items) print i; }; } \ +' +# Make sure the list of sources is unique. This is necessary because, +# e.g., the same source file might be shared among _SOURCES variables +# for different programs/libraries. +am__define_uniq_tagged_files = \ + list='$(am__tagged_files)'; \ + unique=`for i in $$list; do \ + if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \ + done | $(am__uniquify_input)` +ETAGS = etags +CTAGS = ctags +am__DIST_COMMON = $(srcdir)/Makefile.in $(top_srcdir)/depcomp +DISTFILES = $(DIST_COMMON) $(DIST_SOURCES) $(TEXINFOS) $(EXTRA_DIST) +ACLOCAL = ${SHELL} /home/david/devel/cpp/lionheart000916/missing aclocal-1.15 +AMTAR = $${TAR-tar} +AM_DEFAULT_VERBOSITY = 1 +AUTOCONF = ${SHELL} /home/david/devel/cpp/lionheart000916/missing autoconf +AUTOHEADER = ${SHELL} /home/david/devel/cpp/lionheart000916/missing autoheader +AUTOMAKE = ${SHELL} /home/david/devel/cpp/lionheart000916/missing automake-1.15 +AWK = gawk +CC = gcc +CCDEPMODE = depmode=gcc3 +CFLAGS = -g -O2 +CPP = gcc -E +CPPFLAGS = +CXX = g++ +CXXDEPMODE = depmode=gcc3 +CXXFLAGS = -g -O2 +CYGPATH_W = echo +DEFS = -DHAVE_CONFIG_H +DEPDIR = .deps +ECHO_C = +ECHO_N = -n +ECHO_T = +EGREP = /usr/bin/grep -E +EXEEXT = +GREP = /usr/bin/grep +INSTALL = /usr/bin/install -c +INSTALL_DATA = ${INSTALL} -m 644 +INSTALL_PROGRAM = ${INSTALL} +INSTALL_SCRIPT = ${INSTALL} +INSTALL_STRIP_PROGRAM = $(install_sh) -c -s +LDFLAGS = +LIBOBJS = +LIBS = +LTLIBOBJS = +MAKEINFO = ${SHELL} /home/david/devel/cpp/lionheart000916/missing makeinfo +MKDIR_P = /usr/local/bin/gmkdir -p +OBJEXT = o +PACKAGE = lionheart +PACKAGE_BUGREPORT = +PACKAGE_NAME = lionheart +PACKAGE_STRING = lionheart 20000916 +PACKAGE_TARNAME = lionheart +PACKAGE_URL = +PACKAGE_VERSION = 20000916 +PATH_SEPARATOR = : +SET_MAKE = +SHELL = /bin/sh +STRIP = +VERSION = 20000916 +abs_builddir = /home/david/devel/cpp/lionheart000916/src +abs_srcdir = /home/david/devel/cpp/lionheart000916/src +abs_top_builddir = /home/david/devel/cpp/lionheart000916 +abs_top_srcdir = /home/david/devel/cpp/lionheart000916 +ac_ct_CC = gcc +ac_ct_CXX = g++ +am__include = include +am__leading_dot = . +am__quote = +am__tar = $${TAR-tar} chof - "$$tardir" +am__untar = $${TAR-tar} xf - +bindir = ${exec_prefix}/bin +build_alias = +builddir = . +datadir = ${datarootdir} +datarootdir = ${prefix}/share +docdir = ${datarootdir}/doc/${PACKAGE_TARNAME} +dvidir = ${docdir} +exec_prefix = ${prefix} +host_alias = +htmldir = ${docdir} +includedir = ${prefix}/include +infodir = ${datarootdir}/info +install_sh = ${SHELL} /home/david/devel/cpp/lionheart000916/install-sh +libdir = ${exec_prefix}/lib +libexecdir = ${exec_prefix}/libexec +localedir = ${datarootdir}/locale +localstatedir = ${prefix}/var +mandir = ${datarootdir}/man +mkdir_p = $(MKDIR_P) +oldincludedir = /usr/include +pdfdir = ${docdir} +prefix = /usr/local +program_transform_name = s,x,x, +psdir = ${docdir} +sbindir = ${exec_prefix}/sbin +sharedstatedir = ${prefix}/com +srcdir = . +sysconfdir = ${prefix}/etc +target_alias = +top_build_prefix = ../ +top_builddir = .. +top_srcdir = .. +lionheart_SOURCES = lex.cc main.cc formula.cc parser.cc ParamSource.cc \ + Proof.cc Rule.cc RuleSource.cc FormulaRegistry.cc \ + Options.cc Axiom.cc copysplit.cc + +all: all-am + +.SUFFIXES: +.SUFFIXES: .cc .o .obj +$(srcdir)/Makefile.in: $(srcdir)/Makefile.am $(am__configure_deps) + @for dep in $?; do \ + case '$(am__configure_deps)' in \ + *$$dep*) \ + ( cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh ) \ + && { if test -f $@; then exit 0; else break; fi; }; \ + exit 1;; \ + esac; \ + done; \ + echo ' cd $(top_srcdir) && $(AUTOMAKE) --foreign src/Makefile'; \ + $(am__cd) $(top_srcdir) && \ + $(AUTOMAKE) --foreign src/Makefile +Makefile: $(srcdir)/Makefile.in $(top_builddir)/config.status + @case '$?' in \ + *config.status*) \ + cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh;; \ + *) \ + echo ' cd $(top_builddir) && $(SHELL) ./config.status $(subdir)/$@ $(am__depfiles_maybe)'; \ + cd $(top_builddir) && $(SHELL) ./config.status $(subdir)/$@ $(am__depfiles_maybe);; \ + esac; + +$(top_builddir)/config.status: $(top_srcdir)/configure $(CONFIG_STATUS_DEPENDENCIES) + cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh + +$(top_srcdir)/configure: $(am__configure_deps) + cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh +$(ACLOCAL_M4): $(am__aclocal_m4_deps) + cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh +$(am__aclocal_m4_deps): +install-binPROGRAMS: $(bin_PROGRAMS) + @$(NORMAL_INSTALL) + @list='$(bin_PROGRAMS)'; test -n "$(bindir)" || list=; \ + if test -n "$$list"; then \ + echo " $(MKDIR_P) '$(DESTDIR)$(bindir)'"; \ + $(MKDIR_P) "$(DESTDIR)$(bindir)" || exit 1; \ + fi; \ + for p in $$list; do echo "$$p $$p"; done | \ + sed 's/$(EXEEXT)$$//' | \ + while read p p1; do if test -f $$p \ + ; then echo "$$p"; echo "$$p"; else :; fi; \ + done | \ + sed -e 'p;s,.*/,,;n;h' \ + -e 's|.*|.|' \ + -e 'p;x;s,.*/,,;s/$(EXEEXT)$$//;$(transform);s/$$/$(EXEEXT)/' | \ + sed 'N;N;N;s,\n, ,g' | \ + $(AWK) 'BEGIN { files["."] = ""; dirs["."] = 1 } \ + { d=$$3; if (dirs[d] != 1) { print "d", d; dirs[d] = 1 } \ + if ($$2 == $$4) files[d] = files[d] " " $$1; \ + else { print "f", $$3 "/" $$4, $$1; } } \ + END { for (d in files) print "f", d, files[d] }' | \ + while read type dir files; do \ + if test "$$dir" = .; then dir=; else dir=/$$dir; fi; \ + test -z "$$files" || { \ + echo " $(INSTALL_PROGRAM_ENV) $(INSTALL_PROGRAM) $$files '$(DESTDIR)$(bindir)$$dir'"; \ + $(INSTALL_PROGRAM_ENV) $(INSTALL_PROGRAM) $$files "$(DESTDIR)$(bindir)$$dir" || exit $$?; \ + } \ + ; done + +uninstall-binPROGRAMS: + @$(NORMAL_UNINSTALL) + @list='$(bin_PROGRAMS)'; test -n "$(bindir)" || list=; \ + files=`for p in $$list; do echo "$$p"; done | \ + sed -e 'h;s,^.*/,,;s/$(EXEEXT)$$//;$(transform)' \ + -e 's/$$/$(EXEEXT)/' \ + `; \ + test -n "$$list" || exit 0; \ + echo " ( cd '$(DESTDIR)$(bindir)' && rm -f" $$files ")"; \ + cd "$(DESTDIR)$(bindir)" && rm -f $$files + +clean-binPROGRAMS: + -test -z "$(bin_PROGRAMS)" || rm -f $(bin_PROGRAMS) + +lionheart$(EXEEXT): $(lionheart_OBJECTS) $(lionheart_DEPENDENCIES) $(EXTRA_lionheart_DEPENDENCIES) + @rm -f lionheart$(EXEEXT) + $(AM_V_CXXLD)$(CXXLINK) $(lionheart_OBJECTS) $(lionheart_LDADD) $(LIBS) + +mostlyclean-compile: + -rm -f *.$(OBJEXT) + +distclean-compile: + -rm -f *.tab.c + +include ./$(DEPDIR)/Axiom.Po +include ./$(DEPDIR)/FormulaRegistry.Po +include ./$(DEPDIR)/Options.Po +include ./$(DEPDIR)/ParamSource.Po +include ./$(DEPDIR)/Proof.Po +include ./$(DEPDIR)/Rule.Po +include ./$(DEPDIR)/RuleSource.Po +include ./$(DEPDIR)/copysplit.Po +include ./$(DEPDIR)/formula.Po +include ./$(DEPDIR)/lex.Po +include ./$(DEPDIR)/main.Po +include ./$(DEPDIR)/parser.Po + +.cc.o: + $(AM_V_CXX)$(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $< + $(AM_V_at)$(am__mv) $(DEPDIR)/$*.Tpo $(DEPDIR)/$*.Po +# $(AM_V_CXX)source='$<' object='$@' libtool=no \ +# DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) \ +# $(AM_V_CXX_no)$(CXXCOMPILE) -c -o $@ $< + +.cc.obj: + $(AM_V_CXX)$(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ `$(CYGPATH_W) '$<'` + $(AM_V_at)$(am__mv) $(DEPDIR)/$*.Tpo $(DEPDIR)/$*.Po +# $(AM_V_CXX)source='$<' object='$@' libtool=no \ +# DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) \ +# $(AM_V_CXX_no)$(CXXCOMPILE) -c -o $@ `$(CYGPATH_W) '$<'` + +ID: $(am__tagged_files) + $(am__define_uniq_tagged_files); mkid -fID $$unique +tags: tags-am +TAGS: tags + +tags-am: $(TAGS_DEPENDENCIES) $(am__tagged_files) + set x; \ + here=`pwd`; \ + $(am__define_uniq_tagged_files); \ + shift; \ + if test -z "$(ETAGS_ARGS)$$*$$unique"; then :; else \ + test -n "$$unique" || unique=$$empty_fix; \ + if test $$# -gt 0; then \ + $(ETAGS) $(ETAGSFLAGS) $(AM_ETAGSFLAGS) $(ETAGS_ARGS) \ + "$$@" $$unique; \ + else \ + $(ETAGS) $(ETAGSFLAGS) $(AM_ETAGSFLAGS) $(ETAGS_ARGS) \ + $$unique; \ + fi; \ + fi +ctags: ctags-am + +CTAGS: ctags +ctags-am: $(TAGS_DEPENDENCIES) $(am__tagged_files) + $(am__define_uniq_tagged_files); \ + test -z "$(CTAGS_ARGS)$$unique" \ + || $(CTAGS) $(CTAGSFLAGS) $(AM_CTAGSFLAGS) $(CTAGS_ARGS) \ + $$unique + +GTAGS: + here=`$(am__cd) $(top_builddir) && pwd` \ + && $(am__cd) $(top_srcdir) \ + && gtags -i $(GTAGS_ARGS) "$$here" +cscopelist: cscopelist-am + +cscopelist-am: $(am__tagged_files) + list='$(am__tagged_files)'; \ + case "$(srcdir)" in \ + [\\/]* | ?:[\\/]*) sdir="$(srcdir)" ;; \ + *) sdir=$(subdir)/$(srcdir) ;; \ + esac; \ + for i in $$list; do \ + if test -f "$$i"; then \ + echo "$(subdir)/$$i"; \ + else \ + echo "$$sdir/$$i"; \ + fi; \ + done >> $(top_builddir)/cscope.files + +distclean-tags: + -rm -f TAGS ID GTAGS GRTAGS GSYMS GPATH tags + +distdir: $(DISTFILES) + @srcdirstrip=`echo "$(srcdir)" | sed 's/[].[^$$\\*]/\\\\&/g'`; \ + topsrcdirstrip=`echo "$(top_srcdir)" | sed 's/[].[^$$\\*]/\\\\&/g'`; \ + list='$(DISTFILES)'; \ + dist_files=`for file in $$list; do echo $$file; done | \ + sed -e "s|^$$srcdirstrip/||;t" \ + -e "s|^$$topsrcdirstrip/|$(top_builddir)/|;t"`; \ + case $$dist_files in \ + */*) $(MKDIR_P) `echo "$$dist_files" | \ + sed '/\//!d;s|^|$(distdir)/|;s,/[^/]*$$,,' | \ + sort -u` ;; \ + esac; \ + for file in $$dist_files; do \ + if test -f $$file || test -d $$file; then d=.; else d=$(srcdir); fi; \ + if test -d $$d/$$file; then \ + dir=`echo "/$$file" | sed -e 's,/[^/]*$$,,'`; \ + if test -d "$(distdir)/$$file"; then \ + find "$(distdir)/$$file" -type d ! -perm -700 -exec chmod u+rwx {} \;; \ + fi; \ + if test -d $(srcdir)/$$file && test $$d != $(srcdir); then \ + cp -fpR $(srcdir)/$$file "$(distdir)$$dir" || exit 1; \ + find "$(distdir)/$$file" -type d ! -perm -700 -exec chmod u+rwx {} \;; \ + fi; \ + cp -fpR $$d/$$file "$(distdir)$$dir" || exit 1; \ + else \ + test -f "$(distdir)/$$file" \ + || cp -p $$d/$$file "$(distdir)/$$file" \ + || exit 1; \ + fi; \ + done +check-am: all-am +check: check-am +all-am: Makefile $(PROGRAMS) +installdirs: + for dir in "$(DESTDIR)$(bindir)"; do \ + test -z "$$dir" || $(MKDIR_P) "$$dir"; \ + done +install: install-am +install-exec: install-exec-am +install-data: install-data-am +uninstall: uninstall-am + +install-am: all-am + @$(MAKE) $(AM_MAKEFLAGS) install-exec-am install-data-am + +installcheck: installcheck-am +install-strip: + if test -z '$(STRIP)'; then \ + $(MAKE) $(AM_MAKEFLAGS) INSTALL_PROGRAM="$(INSTALL_STRIP_PROGRAM)" \ + install_sh_PROGRAM="$(INSTALL_STRIP_PROGRAM)" INSTALL_STRIP_FLAG=-s \ + install; \ + else \ + $(MAKE) $(AM_MAKEFLAGS) INSTALL_PROGRAM="$(INSTALL_STRIP_PROGRAM)" \ + install_sh_PROGRAM="$(INSTALL_STRIP_PROGRAM)" INSTALL_STRIP_FLAG=-s \ + "INSTALL_PROGRAM_ENV=STRIPPROG='$(STRIP)'" install; \ + fi +mostlyclean-generic: + +clean-generic: + +distclean-generic: + -test -z "$(CONFIG_CLEAN_FILES)" || rm -f $(CONFIG_CLEAN_FILES) + -test . = "$(srcdir)" || test -z "$(CONFIG_CLEAN_VPATH_FILES)" || rm -f $(CONFIG_CLEAN_VPATH_FILES) + +maintainer-clean-generic: + @echo "This command is intended for maintainers to use" + @echo "it deletes files that may require special tools to rebuild." +clean: clean-am + +clean-am: clean-binPROGRAMS clean-generic mostlyclean-am + +distclean: distclean-am + -rm -rf ./$(DEPDIR) + -rm -f Makefile +distclean-am: clean-am distclean-compile distclean-generic \ + distclean-tags + +dvi: dvi-am + +dvi-am: + +html: html-am + +html-am: + +info: info-am + +info-am: + +install-data-am: + +install-dvi: install-dvi-am + +install-dvi-am: + +install-exec-am: install-binPROGRAMS + +install-html: install-html-am + +install-html-am: + +install-info: install-info-am + +install-info-am: + +install-man: + +install-pdf: install-pdf-am + +install-pdf-am: + +install-ps: install-ps-am + +install-ps-am: + +installcheck-am: + +maintainer-clean: maintainer-clean-am + -rm -rf ./$(DEPDIR) + -rm -f Makefile +maintainer-clean-am: distclean-am maintainer-clean-generic + +mostlyclean: mostlyclean-am + +mostlyclean-am: mostlyclean-compile mostlyclean-generic + +pdf: pdf-am + +pdf-am: + +ps: ps-am + +ps-am: + +uninstall-am: uninstall-binPROGRAMS + +.MAKE: install-am install-strip + +.PHONY: CTAGS GTAGS TAGS all all-am check check-am clean \ + clean-binPROGRAMS clean-generic cscopelist-am ctags ctags-am \ + distclean distclean-compile distclean-generic distclean-tags \ + distdir dvi dvi-am html html-am info info-am install \ + install-am install-binPROGRAMS install-data install-data-am \ + install-dvi install-dvi-am install-exec install-exec-am \ + install-html install-html-am install-info install-info-am \ + install-man install-pdf install-pdf-am install-ps \ + install-ps-am install-strip installcheck installcheck-am \ + installdirs maintainer-clean maintainer-clean-generic \ + mostlyclean mostlyclean-compile mostlyclean-generic pdf pdf-am \ + ps ps-am tags tags-am uninstall uninstall-am \ + uninstall-binPROGRAMS + +.PRECIOUS: Makefile + + +# Tell versions [3.59,3.63) of GNU make to not export all variables. +# Otherwise a system limit (for SysV at least) may be exceeded. +.NOEXPORT: diff --git a/src/Makefile.am b/src/Makefile.am new file mode 100644 index 0000000..de2b6a4 --- /dev/null +++ b/src/Makefile.am @@ -0,0 +1,4 @@ +bin_PROGRAMS = lionheart +lionheart_SOURCES = lex.cc main.cc formula.cc parser.cc ParamSource.cc \ + Proof.cc Rule.cc RuleSource.cc FormulaRegistry.cc \ + Options.cc Axiom.cc copysplit.cc diff --git a/src/Markable.h b/src/Markable.h new file mode 100644 index 0000000..5ebfaa5 --- /dev/null +++ b/src/Markable.h @@ -0,0 +1,26 @@ +/* MarkedFormula.h + by David Baer, 7/4/2000 + + Allows us to mark formulas that persist from line 1 to line X of proof chain +*/ + +#ifndef _MARKABLE_H +#define _MARKABLE_H + +class Markable +{ + unsigned long int end; + public: + Markable(unsigned long int n = 0) + { + end = n; + } + + void setEnd(unsigned long int n) + { + end = n; + } +}; + +#endif /* !def _MARKABLE_H */ + diff --git a/src/Options.cc b/src/Options.cc new file mode 100644 index 0000000..e2ec948 --- /dev/null +++ b/src/Options.cc @@ -0,0 +1,112 @@ +/* $Id: Options.cc,v 1.6 2000/01/30 00:59:32 david Exp $ */ + +/* Options.cc + by David Baer + + Parse command line options and convert to an object +*/ + +#include +#include +#include "Options.h" +#include "parser.h" +#include "Axiom.h" + +#define APPNAME "lionheart" +#define MAJ_VER_NUM 0 +#define MIN_VER_NUM "9f" + +Options::Options(int argc, char *argv[]) +{ + form = NULL; + pause_mode = 0; + man_mode = 0; + output_file = NULL; + quiet_mode = 1; + help_req = 0; + dump_mode = 0; + max_param = 100; + use_ind = 0; + + for (int i = 1; i < argc; i++) + if (argv[i][0] != '-') + { + initParser(argv[i]); + form = parseFormula(); + endParser(); + } + else if (!strcmp(argv[i], "-ind")) + { + use_ind = 1; + } + else if (!strcmp(argv[i], "-pause")) + { + pause_mode = 1; + } + else if (!strcmp(argv[i], "-manual")) + { + man_mode = 1; + } + else if (!strncmp(argv[i], "-p", 2)) + { + if (!(i < argc - 1) || !sscanf(argv[i + 1], "%u", &max_param)) + cerr << "warning: -p needs a numerical argument" << endl; + i++; + } + else if (!strncmp(argv[i], "-o", 2)) + { + if (i < argc - 1) + output_file = strdup(argv[i + 1]); + else cerr << "warning: -o needs an argument -- ignored" << endl; + i++; + } + else if (!strncmp(argv[i], "-v", 2)) + { + quiet_mode = 0; + } + else if (!strcmp(argv[i], "-dump")) + { + dump_mode = 1; + } + else if (!strcmp(argv[i], "-a")) + { + if (i < argc - 1) + { + char *axfiles = strdup(argv[i + 1]), + *curFile = strtok(axfiles, ","); + Vector files; + + while (curFile) + { + files.addElement(curFile); + curFile = strtok(NULL, ","); + } + + for (unsigned j = 0; j < files.size(); j++) + axioms.addAxioms(files(j)); + + files.kill(); + + delete axfiles; + } + else cerr << "warning: -a needs an argument -- ignored" << endl; + i++; + } + else help_req = 1; +} + +void Options::syntax() +{ + cout << APPNAME << " " << MAJ_VER_NUM << "." << MIN_VER_NUM << endl; + cout << endl; + cout << "syntax: " << APPNAME << " [-o ] [-q] [-manual] [-dump] []" << endl; + cout << endl; + cout << " : the propositional formula to be proved" << endl; + cout << "-a [,,...] : axiom files" << endl; + cout << "-o : output proof to this text file" << endl; + cout << "-p # : maximum parameter number (default: 100)" << endl; + cout << "-manual : prompt user for proof steps" << endl; + cout << "-v : verbose mode -- all machine steps displayed " << endl; + cout << "-dump : dump proof to standard output" << endl; + cout << endl; +} diff --git a/src/Options.h b/src/Options.h new file mode 100644 index 0000000..c7e0b44 --- /dev/null +++ b/src/Options.h @@ -0,0 +1,38 @@ +/* $Id: Options.h,v 1.5 2000/01/30 00:59:32 david Exp $ */ + +/* Options.h + by David Baer + + Parse command-line options and convert to and object +*/ + +#ifndef _OPTIONS_H +#define _OPTIONS_H + +#include "formula.h" +#include "Vector.h" + +class Options +{ + int man_mode, quiet_mode, help_req, dump_mode, pause_mode, + use_ind; + unsigned max_param; + PropFormula *form; + char *output_file; +public: + Options(int argc, char *argv[]); + void syntax(); + PropFormula *getFormula() { return form; } + int pause() { return pause_mode; } + int manual() { return man_mode; } + int quiet() { return quiet_mode; } + int help() { return help_req; } + int dump() { return dump_mode; } + int induction() { return use_ind; } + char *outputFile() { return output_file; } + unsigned maxParam() { return max_param; } + +}; + +#endif /* !def _OPTIONS_H */ + diff --git a/src/ParamSource.cc b/src/ParamSource.cc new file mode 100644 index 0000000..3a109da --- /dev/null +++ b/src/ParamSource.cc @@ -0,0 +1,11 @@ +/* $Id: ParamSource.cc,v 1.3 2000/01/24 17:42:52 david Exp $ */ + +/* ParamSource.cc + by David Baer + + Object for generating parameters +*/ + +#include "ParamSource.h" + +ParamSource psource; diff --git a/src/ParamSource.h b/src/ParamSource.h new file mode 100644 index 0000000..74168ae --- /dev/null +++ b/src/ParamSource.h @@ -0,0 +1,36 @@ +/* $Id: ParamSource.h,v 1.4 2000/01/25 03:05:43 david Exp $ */ + +/* ParamSource.h + by David Baer + + Generate new (unique) parameter names +*/ + +#ifndef _PARAMSOURCE_H +#define _PARAMSOURCE_H + +#include "formula.h" + +class ParamSource +{ + unsigned count, max; + public: + ParamSource() { count = 0; } + + Var *freshParam() + { + char str[20]; + snprintf(str, 20, "p%u", count++); + + return new Var(str); + } + + void setNext(unsigned n) { if (n > count) count = n; } + unsigned viewNext() { return count; } + void setMax(unsigned m) { max = m; } + unsigned getMax() { return max; } +}; + +extern ParamSource psource; + +#endif /* !def _PARAMSOURCE_H */ diff --git a/src/Proof.cc b/src/Proof.cc new file mode 100644 index 0000000..33c2acb --- /dev/null +++ b/src/Proof.cc @@ -0,0 +1,602 @@ +/* $Id: Proof.cc,v 1.9 2000/01/29 22:33:53 david Exp $ */ + +/* Proof.cc + by David Baer + + Routines for object that applies rules as it is given them +*/ + +#include +#include "Proof.h" +#include "ParamSource.h" +#include "Axiom.h" +#include "copysplit.h" + +using namespace std; + +// constructor (for outside use) +Proof::Proof(PropFormula *f, RuleSource *g, FormulaRegistry *r) +{ + child1 = child2 = NULL; // initialize subgoals to NULL + rhs = f; // set user-specified RHS of sequent + guide = g; // initialize guide + + // if not specified, set up new formula registry + if (!r) + reg = new FormulaRegistry(); + else reg = r; +} + +// for outside use -- takes explicit LHS in addition to other params +Proof::Proof(Vectorl, PropFormula *f, RuleSource *g, + FormulaRegistry *r) +{ + child1 = child2 = NULL; + rhs = f; + lhs = l; + guide = g; + if (!r) + reg = new FormulaRegistry(); + else reg = r; +} + +static inline boolean +rightRule(RuleType r) +{ + return (r == AND_R || + r == OR_R1 || + r == OR_R2 || + r == IMP_R || + r == NOT_R || + r == MAGIC ? true : false); +} + + +ProofReturnCode Proof::prove() +{ + int ruleResult = 0; + + // the following construction requires some explanation: + // we loop endlessly until a "return" is encountered -- + // the only way we can loop is if one of the subgoals returns + // PROOF_BACKUP, meaning that the guide wishes to try a different + // rule for this sequent. Hence the 'while(1)' + while (1) + { + do // loop until an appropriate rule can be applied + { + step = guide->getRule(lhs, rhs); + if (step.getRule() == BACKUP_RULE) + return PROOF_BACKUP; + ruleResult = applyRule(step); + // ruleResult = 1 if rule successfully applied, 0 otherwise + } + while (!ruleResult); + + // did not find proof + if (ruleResult == -1) + return PROOF_FALSE; + else if (ruleResult == -2) // found proof + return PROOF_TRUE; + + // solve subgoals, if applicable + if (child1) + { + ProofReturnCode result1 = child1->prove(); + + // if backing up from subgoal, delete failed subgoal and + // re-try this sequent + if (result1 == PROOF_BACKUP) + { + delete child1; + child1 = NULL; + if (child2) { delete child2; child2 = NULL; } + continue; + } + else if (result1 == PROOF_TRUE) + if (child2) + { + // first, let's check to see whether the step that + // gave us two subgoals was superfluous. If it was, + // then we don't need to check subgoal 2, since it + // won't show up when we print the proof. + if ((step.getTarget() && !step.getTarget()->tagged()) || + (!rhs->tagged() && rightRule(step.getRule()))) + return PROOF_TRUE; + + // otherwise, we're out of luck -- we have to prove the + // second subgoal... + ProofReturnCode result2 = child2->prove(); + if (result2 == PROOF_BACKUP) + { + delete child1; + child1 = NULL; + delete child2; + child2 = NULL; + continue; + } + else if (result2 == PROOF_TRUE) + return PROOF_TRUE; // child1 & child2 are true + else return PROOF_FALSE; // child1 true, child2 false + } + else return PROOF_TRUE; // child1 true + else return PROOF_FALSE; // child1 false + } + else return PROOF_TRUE; // no children -- "hyp" applied ==> true + } +} + +// print out the proof, complete with sequents and rules +void Proof::print(ostream& o, int indent) +{ + boolean superfluous = ((step.getTarget() && + (!step.getTarget()->tagged() || + (step.getTarget()->isQuant() && !step.getTarget()->asQuant()->instantFormula()->tagged()) + )) || + (!rhs->tagged() && rightRule(step.getRule())) ? + true : false), + printed = false; // set to true once something is printed on a line + + if (!reg) + { + o << "error! excess formulas have been cleaned!" << endl; + return; + } + + if (!superfluous) + { + // do indentation + for (int i = 0; i < indent; i++) + o << " "; + + // print left-hand formulae + for (unsigned i = 0; i < lhs.size(); i++) + { + if (lhs(i)->tagged()) + { + lhs(i)->print(o); + printed = true; + } + if (printed && (i < lhs.size() - 1) && lhs(i + 1)->tagged()) + o << ", "; + } + o << " |- "; + + // print right-hand formula + if (rhs->tagged()) + rhs->print(o); + else o << "false"; + + // print rule used here + RuleType type = step.getRule(); + o << " by " << rulename[(int)type]; + + // this commented-out section doesn't work for some reason... + // ... it is an attempt to show which left-hand formulae were + // manipulated by each of the following rules + /*if ((type == AND_L) || + (type == OR_L) || + (type == IMP_L) || + (type == NOT_L)) + o << " " << step.argument() + 1;*/ + + // if we cut in a formula, say what it is! + if (type == CUT) + { + o << " "; + step.getTarget()->print(o); + } + + o << endl; + } + + // if there are two subgoals, set them off with indentation + if (child1 && child2 && + !superfluous // if this step is superflous, we don't need to + // see 2 subgoals (no info gained) + ) + { + child1->print(o, indent + 3); + o << endl; + child2->print(o, indent + 3); + } + // otherwise, just continue with the single subgoal + else if (child1) + child1->print(o, indent); +} + +static inline +QuantFormula *flipQuant(QuantFormula *qf) +// return the logical negation of a quantified formula, with the ~ on the INSIDE +{ + PropFormula *inside; + + if (qf->getFormula()->isQuant()) + inside = flipQuant(qf->getFormula()->asQuant()); + else if (qf->getFormula()->isNot()) + inside = qf->getFormula()->asNot()->notOperand(); + else inside = new Not(qf->getFormula()); + + return new QuantFormula(qf->getType() == QUANT_FORALL ? QUANT_EXISTS : QUANT_FORALL, + qf->getVariable(), inside); +} + + +// attempt to apply the given rule to the sequent +int Proof::applyRule(Rule r) +{ + PropFormula *target = r.getTarget(); // the target of the rule + // (may be a new formula [CUT] + // or an old one [AND_L, etc.] + BinOp *binop = NULL, // binop version of rhs + *binopt = NULL; // binop version of target + + if (r.isProof()) // rule supplies a proof + { + // give it the benefit of the doubt... + child1 = r.getProof(); + return -2; + } + + // do the appropriate pseudo-casts for binary expressions + // for easier access below... + if (rhs->isBinOp()) + binop = rhs->asBinOp(); + if (target) + { + if (target->isBinOp()) + binopt = target->asBinOp(); + } + + // multiplex on rule type + switch (r.getRule()) + { + case AND_L : if (binopt && (binopt->op() == BINOP_AND)) + { + Vector new_lhs = copysplitbut(lhs, target); + new_lhs.addElement(binopt->leftOperand()); + new_lhs.addElement(binopt->rightOperand()); + + // set parent info + binopt->leftOperand()->setParent(binopt); + binopt->rightOperand()->setParent(binopt); + + child1 = new Proof(new_lhs, rhs, guide, reg); + return 1; + } + break; + case AND_R : if (binop && (binop->op() == BINOP_AND)) + { + // set parent info + binop->leftOperand()->setParent(binop); + binop->rightOperand()->setParent(binop); + + child1 = new Proof(copysplit(lhs), binop->leftOperand(), + guide, reg); + child2 = new Proof(copysplit(lhs), binop->rightOperand(), + guide, reg); + return 1; + } + break; + case OR_L : if (binopt && (binopt->op() == BINOP_OR)) + { + Vector new_lhs1 = copysplitbut(lhs, target), + new_lhs2 = copysplit(new_lhs1); + new_lhs1.addElement(binopt->leftOperand()); + new_lhs2.addElement(binopt->rightOperand()); + child1 = new Proof(new_lhs1, rhs, guide, reg); + child2 = new Proof(new_lhs2, rhs, guide, reg); + + // set parent info + binopt->leftOperand()->setParent(binopt); + binopt->rightOperand()->setParent(binopt); + + return 1; + } + break; + case NOT_L : { + Vector new_lhs = copysplitbut(lhs, target); + PropFormula *new_rhs; + + if (target->isNot()) + new_rhs = target->asNot()->notOperand(); + else if (target->isQuant()) + { + /*PropFormula *inside = target->asQuant()->getFormula(); + new_rhs = new QuantFormula(target->asQuant()->getType() == QUANT_FORALL ? QUANT_EXISTS : QUANT_FORALL, + target->asQuant()->getVariable(), + inside->isNot() ? inside->asNot()->notOperand() : new Not(inside));*/ + new_rhs = flipQuant(rhs->asQuant()); + } + else new_rhs = new Not(target); + + // set parent info + new_rhs->setParent(target); + + child1 = new Proof(new_lhs, new_rhs, guide, reg); + return 1; + } + break; + case NOT_R : { + Vector new_lhs = copysplit(lhs); + PropFormula *new_elt; + + if (rhs->isNot()) + new_elt = rhs->asNot()->notOperand(); + else if (rhs->isQuant()) + { + new_elt = flipQuant(rhs->asQuant()); + } + else new_elt = new Not(rhs); + + // set parent info + new_elt->setParent(rhs); + + new_lhs.addElement(new_elt); + child1 = new Proof(new_lhs, new ConstFormula(false), guide, reg); + return 1; + } + break; + case IMP_L : if (binopt && (binopt->op() == BINOP_IMPL)) + { + Vector new_lhs1 = copysplitbut(lhs, target), + new_lhs2 = copysplit(new_lhs1); + new_lhs2.addElement(binopt->rightOperand()); + + // set parent info + binopt->leftOperand()->setParent(binopt); + binopt->rightOperand()->setParent(binopt); + + child1 = new Proof(new_lhs1, binopt->leftOperand(), + guide, reg); + child2 = new Proof(new_lhs2, rhs, guide, reg); + return 1; + } + break; + case OR_R2 : + case OR_R1 : if (binop && (binop->op() == BINOP_OR)) + { + // set parent info + PropFormula *left = binop->leftOperand()->formCopy(), + *right = binop->rightOperand()->formCopy(); + + cout << "holla!" << endl; + + left->setParent(binop); + right->setParent(binop); + + cout << "left: "; + left->print(cout); + cout << " ["; + left->getParent()->print(cout); + cout << "]" << endl; + cout << "right: "; + right->print(cout); + cout << " ["; + right->getParent()->print(cout); + cout << "]" << endl; + + child1 = new Proof(copysplit(lhs), (r.getRule() == OR_R1 ? + left + : right), + guide, reg); + return 1; + } + break; + case OR_R : if (binop && (binop->op() == BINOP_OR)) + { + Vector new_lhs = copysplit(lhs); + PropFormula *new_elt = binop->leftOperand(); + + if (new_elt->isNot()) + new_elt = new_elt->asNot()->notOperand(); + else if (new_elt->isQuant()) + { + new_elt = flipQuant(new_elt->asQuant()); + } + else new_elt = new Not(new_elt); + + // set parent info + new_elt->setParent(binop); + + new_lhs.addElement(new_elt); + + binop->rightOperand()->setParent(binop); + + child1 = new Proof(new_lhs, binop->rightOperand(), + guide, reg); + + return 1; + } + break; + case IMP_R : if (binop && (binop->op() == BINOP_IMPL)) + { + Vector new_lhs = copysplit(lhs); + new_lhs.addElement(binop->leftOperand()); + + // set parent info + binop->leftOperand()->setParent(binop); + binop->rightOperand()->setParent(binop); + + child1 = new Proof(new_lhs, binop->rightOperand(), + guide, reg); + return 1; + } + break; + case HYP : { + unsigned i, result = 0; + for (i = 0; !result && (i < lhs.size()); i++) + if (lhs(i)->equals(rhs)) + { + result = 1; + + // set tags on ancestors (this is a closed branch) + PropFormula *tempPtr = lhs(i); + // cout << "Setting tags on ancestors ... " << endl; + while (tempPtr && !tempPtr->tagged()) + { + // cout << "* "; + // tempPtr->println(cout); + tempPtr->setTag(); + tempPtr = tempPtr->getParent(); + } + + tempPtr = rhs; + while (tempPtr && !tempPtr->tagged()) + { + // cout << "* "; + // tempPtr->println(cout); + tempPtr->setTag(); + tempPtr = tempPtr->getParent(); + } + // cout << endl; + } + return result; + } + case GIVEUP: return -1; + case INSTANT:if (target->isQuant()) + { + QuantFormula *qform = target->asQuant(); + Vector new_lhs; + + if (qform->getType() == QUANT_FORALL) + { + /* cout << "instantiated formula: " << flush;*/ + char paramstr[20]; + snprintf(paramstr, 20, "p%u", r.argument()); + + PropFormula *new_elt = qform->instantiate(new Var(paramstr)); + /* new_elt->println(cout); */ + + /* cout << "old formula: " << flush; + qform->println(cout); */ + qform->incParam(); + + // need to ADD a formula to the list -- can use any parameter + new_lhs = copysplit(lhs); + new_lhs.addElement(new_elt); + + // set parent info + new_elt->setParent(qform); + + //qform->decParam(); // safe after copy + } + else // qform->getType() == QUANT_EXISTS + { + // use fresh parameter + new_lhs = copysplitbut(lhs, target); + + PropFormula *new_elt = qform->instantiate(psource.freshParam()); + + // set parent info + new_elt->setParent(qform); + + new_lhs.addElement(new_elt); + } + + child1 = new Proof(new_lhs, rhs, guide, reg); + return 1; + } + break; + case AXIOM : { + Vector new_lhs = copysplit(lhs); + PropFormula *new_ax = target; + + if (new_ax) + { + new_lhs.addElement(new_ax); + child1 = new Proof(new_lhs, rhs, guide, reg); + return 1; + } + else return 0; + } + case IND : { + Vector new_lhs1 = copysplit(lhs), + new_lhs2 = copysplit(lhs); + PropFormula *zero = r.getInductionZero(), + *succ = r.getInductionSucc(), + *new_rhs1, *new_rhs2; + Var *iV = new Var("i"), *jV = new Var("j"); + Var *zeroV = psource.freshParam(), + *lastV = psource.freshParam(), + *nextV = psource.freshParam(); + + if (!zero || !succ) + cout << "Still not fixed!" << endl; + + zero->println(cout); + succ->println(cout); + + if (zero && succ && rhs->isQuant() && (rhs->asQuant()->getType() == QUANT_FORALL)) + { + new_lhs1.addElement(zero->replace(iV, zeroV)); + new_lhs2.addElement(succ->replace(iV, lastV)-> + replace(jV, nextV)); + delete iV; + delete jV; + new_rhs1 = rhs->asQuant()->instantiate(zeroV); + new_rhs2 = rhs->asQuant()->instantiate(nextV); + new_lhs2.addElement(rhs->asQuant()->instantiate(lastV)); + + child1 = new Proof(new_lhs1, new_rhs1, guide, reg); + child2 = new Proof(new_lhs2, new_rhs2, guide, reg); + + return 1; + } + else return 0; + } + case CUT : { + Vector new_lhs = copysplit(lhs); + reg->addFormula(target); + new_lhs.addElement(target); + child1 = new Proof(target, guide, reg); + child2 = new Proof(new_lhs, rhs, guide, reg); + return 1; + } + case MAGIC : if (rhs->isBinOp() && (rhs->asBinOp()->op() == BINOP_OR)) + { + BinOp *formula = rhs->asBinOp(); + if (formula->rightOperand()->isNot()) + return formula->rightOperand()->asNot()-> + notOperand()->equals(formula->leftOperand()); + else if (formula->leftOperand()->isNot()) + return formula->leftOperand()->asNot()-> + notOperand()->equals(formula->rightOperand()); + + // set tags on ancestors (this is a closed branch) + PropFormula *tempPtr = rhs; + while (tempPtr) + { + tempPtr->setTag(); + tempPtr = tempPtr->getParent(); + } + } + break; + default : cerr << "Rule " << rulename[(int)r.getRule()] + << "not supported yet!" << endl; + } + return 0; +} + +void Proof::cleanup() +{ + if (child1) + delete child1; + if (child2) + delete child2; + if (reg) + { + reg->annihilate(); + delete reg; + reg = NULL; + } +} + +Proof::~Proof() +{ + if (child1) + delete child1; + if (child2) + delete child2; +} + diff --git a/src/Proof.h b/src/Proof.h new file mode 100644 index 0000000..03b085f --- /dev/null +++ b/src/Proof.h @@ -0,0 +1,67 @@ +// $Id: Proof.h,v 1.3 2000/01/24 17:42:52 david Exp $ + +// Proof.h +// Proof construct + +#ifndef _PROOF_H +#define _PROOF_H + +#include "Rule.h" +#include "RuleSource.h" +#include "Vector.h" +#include "FormulaRegistry.h" +#include "formula.h" + +// sometimes C++ can be braindead... +#ifndef NULL +#define NULL 0 +#endif /* !def NULL */ + +// enumerated type to encode proof results +typedef enum +{ + PROOF_FALSE = 0, + PROOF_TRUE, + PROOF_BACKUP +} ProofReturnCode; + +class Proof +{ + Vector lhs; // the lefthand side of the turnstyle + PropFormula *rhs; // the righthand side -- a single formula + Proof *child1, // proof can have 2 subgoals + *child2; + RuleSource *guide; // this abstraction supplies the rules + Rule step; // the step taken at this stage (from guide) + FormulaRegistry *reg; // the global registry of extra formulae +public: + + // constructor (for outside use) -- setup proof for a single formula + Proof(PropFormula *f, RuleSource *g, FormulaRegistry *r = NULL); + + // constructor (for internal use) -- setup a proof subgoal + Proof(Vectorl, PropFormula *f, RuleSource *g, + FormulaRegistry *r = NULL); + + // apply a given rule + int applyRule(Rule); // 0 = invalid rule, 1 = valid rule + + // try to prove this seqent with rules from guide + ProofReturnCode prove(); + + // print this sequent + void print(ostream& o, int indent = 0); + void println(ostream& o, int indent = 0) + { + print(o, indent); + o << endl; + } + + void cleanup(); // delete excess formulas + + // class destructor + ~Proof(); +}; + +#endif /* !_PROOF_H */ + diff --git a/src/Rule.cc b/src/Rule.cc new file mode 100644 index 0000000..7ba377e --- /dev/null +++ b/src/Rule.cc @@ -0,0 +1,24 @@ +// $Id: Rule.cc,v 1.4 2000/01/29 22:33:53 david Exp $ + +// Rule.cc +// Sadly, there is nothing here but the names of the rules. + +const char *rulename[] = { "andL", + "andR", + "orL", + "orR1", + "orR2", + "orR", + "impL", + "impR", + "notL", + "notR", + "cut", + "magic", + "hyp", + "instantiation", + "induction", + "axiom", + "giveup", + "backup" }; + diff --git a/src/Rule.h b/src/Rule.h new file mode 100644 index 0000000..6955d65 --- /dev/null +++ b/src/Rule.h @@ -0,0 +1,120 @@ +// $Id: Rule.h,v 1.7 2000/01/30 00:59:32 david Exp $ + +// Rule.h +// Abstraction type for refinement-logic rules + +#ifndef _RULE_H +#define _RULE_H + +#include "formula.h" +#include + +// types of rules -- the standard refinement logic set plus a few +// pseudo-rules +typedef enum +{ + AND_L, + AND_R, + OR_L, + OR_R1, + OR_R2, + OR_R, + IMP_L, + IMP_R, + NOT_L, + NOT_R, + CUT, + MAGIC, + HYP, + INSTANT, + IND, + AXIOM, + GIVEUP, // exit proof + BACKUP_RULE // backup to last subgoal +} RuleType; + +// rule names -- used for printing +extern const char *rulename[]; + +class Proof; // used in class Rule + +class Rule +{ + RuleType rule; + PropFormula *target; + PropFormula *indZero, *indSucc; + Proof *pf; + Var *var; + int arg; + char *axname; +public: + Rule() + { + rule = AND_L; + target = indZero = indSucc = NULL; + arg = 2; + pf = NULL; + var = NULL; + } + Rule(RuleType r, PropFormula *t, int a=-1, Proof *p = NULL) + { + rule = r; + target = t; + arg = a; + pf = p; + var = NULL; + indZero = indSucc = NULL; + } + Rule(RuleType r, PropFormula *t, char *name) + { + rule = r; + axname = strdup(name); + pf = NULL; + target = t; + var = NULL; + indZero = indSucc = NULL; + } + + // constructor for induction + Rule(RuleType r, PropFormula *iZ, PropFormula *iS) + { + rule = r; + indZero = iZ; + indSucc = iS; + pf = NULL; + target = NULL; + var = NULL; + } + + void setArg(int a) { arg = a; } + char *getName() { return axname; } + + Var *getVar() { return this->var; } + PropFormula *getTarget() { return target; } + PropFormula *getInductionZero() { return indZero; } + PropFormula *getInductionSucc() { return indSucc; } + RuleType getRule() { return rule; } + Rule& operator=(Rule r) + { + rule = r.rule; + target = r.target; + pf = r.pf; + arg = r.arg; + axname = r.axname; + indZero = r.indZero; + indSucc = r.indSucc; + + return *this; + } + int argument() { return arg; } + virtual boolean isProof() + { + return pf != NULL; + } + virtual Proof *getProof() + { + return pf; + } +}; + +#endif /* !_RULE_H */ diff --git a/src/RuleSource.cc b/src/RuleSource.cc new file mode 100644 index 0000000..8b898de --- /dev/null +++ b/src/RuleSource.cc @@ -0,0 +1,597 @@ +// $Id: RuleSource.cc,v 1.10 2000/01/30 00:59:32 david Exp $ + +// RuleSource.cc +// routines for supplying rules for refinement logic proofs + +#include +#include "RuleSource.h" +#include "parser.h" +#include "Proof.h" +#include "ParamSource.h" +#include "Axiom.h" + +#ifndef NULL +#define NULL 0 +#endif /* !_NULL */ + +using namespace std; + +// When the user wants to apply a left-rule, sometimes there is more +// than one possible target. This routine lists all the +// possibilities and prompts the user for his/her choice. +unsigned UserRuleSource::getFormula(Vector v, Vector possible) +{ + unsigned result, done = 0, i; + + while (!done) + { + for (i = 0; i < possible.size(); i++) + { + *ostr << possible(i) + 1 << ") "; + v(possible(i))->println(*ostr); + } + *ostr << "which formula on left? "; + *istr >> result; + for (i = 0; !done && (i < possible.size()); i++) + done = (result == (possible(i) + 1)); + } + + char nullstr[20]; + + istr->getline(nullstr, 18); + + + return result - 1; +} + +unsigned UserRuleSource::getInstantParam() +{ + char instring[100]; + unsigned num; + + *ostr << "enter a parameter for instantiation: p"; + + istr->getline(instring, 98); + + sscanf(instring, "%u", &num); + + psource.setNext(num + 1); // ensure freshness for fresh parameters + + return num; +} + +Rule UserRuleSource::getRule(Vector l, PropFormula *r) +{ + char inbuf[100]; + + while (1) // get good rule + { + for (unsigned i = 0; i < l.size(); i++) + { + l(i)->print(*ostr); + if (i < l.size() - 1) + *ostr << ", "; + } + *ostr << " |- "; + r->print(*ostr); + *ostr << " by "; + istr->getline(inbuf, 98); + if (!strcasecmp(inbuf, "andr")) + { + Rule result(AND_R, NULL); + return result; + } + else if (!strcasecmp(inbuf, "orr1")) + { + Rule result(OR_R1, NULL); + return result; + } + else if (!strcasecmp(inbuf, "orr2")) + { + Rule result(OR_R2, NULL); + return result; + } + else if (!strcasecmp(inbuf, "orr")) + { + Rule result(OR_R, NULL); + return result; + } + else if (!strcasecmp(inbuf, "impr")) + { + Rule result(IMP_R, NULL); + return result; + } + else if (!strcasecmp(inbuf, "notr")) + { + Rule result(NOT_R, NULL); + return result; + } + else if (!strcasecmp(inbuf, "andl")) + { + if (l.size() == 0) continue; // nothing on lhs! + unsigned which; + Vector possible; + for (which = 0; which < l.size(); which++) + if (l(which)->isBinOp() && (l(which)->asBinOp()->op() == BINOP_AND)) + possible.addElement(which); + if (possible.size() == 0) + which = 0; + else if (possible.size() == 1) + which = possible(0); + else which = getFormula(l, possible); + + Rule result(AND_L, l(which), which); + return result; + } + else if (!strcasecmp(inbuf, "orl")) + { + if (l.size() == 0) continue; // nothing on lhs! + unsigned which; + Vector possible; + for (which = 0; which < l.size(); which++) + if (l(which)->isBinOp() && (l(which)->asBinOp()->op() == BINOP_OR)) + possible.addElement(which); + if (possible.size() == 0) + which = 0; + else if (possible.size() == 1) + which = possible(0); + else which = getFormula(l, possible); + + Rule result(OR_L, l(which), which); + return result; + } + else if (!strcasecmp(inbuf, "impl")) + { + if (l.size() == 0) continue; // nothing on lhs! + unsigned which; + Vector possible; + for (which = 0; which < l.size(); which++) + if (l(which)->isBinOp() && (l(which)->asBinOp()->op() == BINOP_IMPL)) + possible.addElement(which); + if (possible.size() == 0) + which = 0; + else if (possible.size() == 1) + which = possible(0); + else which = getFormula(l, possible); + + Rule result(IMP_L, l(which), which); + return result; + } + else if (!strcasecmp(inbuf, "notl")) + { + if (l.size() == 0) continue; // nothing on lhs! + unsigned which; + Vector possible; + for (which = 0; which < l.size(); which++) + possible.addElement(which); + if (possible.size() == 0) + which = 0; + else if (possible.size() == 1) + which = possible(0); + else which = getFormula(l, possible); + + Rule result(NOT_L, l(which), which); + return result; + } + else if (!strcasecmp(inbuf, "instant")) + { + if (l.size() == 0) continue; + unsigned which; + Vector possible; + for (which = 0; which < l.size(); which++) + if (l(which)->isQuant()) + possible.addElement(which); + if (possible.size() == 0) + which = 0; + else if (possible.size() == 1) + which = possible(0); + else which = getFormula(l, possible); + + /*Var *p = (l(which)->asQuant()->getType() == QUANT_EXISTS ? NULL : getInstantParam());*/ + unsigned param; + if (l(which)->isQuant()) + param = (l(which)->asQuant()->getType() == QUANT_EXISTS ? 0 : getInstantParam()); + else param = 0; + + /*if (!p) + cout << "p == NULL" << endl;*/ + + Rule result(INSTANT, l(which), param); + + return result; + } + else if (!strcasecmp(inbuf, "ind")) + { + if (!r->isQuant() || (r->asQuant()->getType() != QUANT_FORALL)) + continue; + + char zeroStr[128], succStr[128]; + + *ostr << "zero(i) <==> " << flush; + *istr >> zeroStr; + initParser(zeroStr); + PropFormula * zero_pred = parseFormula(); + endParser(); + + *ostr << "succ(i, j) <==> " << flush; + *istr >> succStr; + initParser(succStr); + PropFormula * succ_pred = parseFormula(); + endParser(); + + *ostr << "Thanks!" << endl; + + Rule result(IND, zero_pred, succ_pred); + + /**ostr << "zero: " << flush; + result.getInductionZero()->println(*ostr); + *ostr << "succ: " << flush; + result.getInductionSucc()->println(*ostr);*/ + + return result; + } + else if (!strcasecmp(inbuf, "axiom")) + { + axioms.printAxioms(*ostr); + *ostr << "which one? " << flush; + char name[40]; + istr->getline(name, 38); + PropFormula *ax = axioms.getAxiom(name); + + *ostr << "New axiom: " << flush; + ax->println(*ostr); + + if (ax) + { + Rule result(AXIOM, ax, name); + return result; + } + else continue; + } + else if (!strcasecmp(inbuf, "hyp")) + { + Rule result(HYP, NULL); + return result; + } + else if (!strcasecmp(inbuf, "giveup")) + { + Rule result(GIVEUP, NULL); + return result; + } + else if (!strcasecmp(inbuf, "cut")) + { + *ostr << "Enter formula: " << flush; + initParser(*istr); + Rule result(CUT, parseFormula()); + endParser(); + return result; + } + else if (!strcasecmp(inbuf, "magic")) + { + Rule result(MAGIC, NULL); + return result; + } + else if (!strcasecmp(inbuf, "backup")) + { + Rule result(BACKUP_RULE, NULL); + return result; + } + else + { + Rule result(AND_R, NULL); + return result; + } + } +} + + +/*int order[] = { 1, 4, 3, 6, 7, 5, 2, 8, 9, 10, 11, 12, 13 };*/ +PropFormula *basicTarget = NULL; + +unsigned isBasic(Vectorlist) +{ + unsigned i, finalresult = 1, result = 1; + + //cout << "checking list..." << endl; + basicTarget = NULL; + + for (i = 0; i < list.size(); i++) + { + //list(i)->println(cout); + unsigned temp = list(i)->isNot() && + list(i)->asNot()->notOperand()->isBinOp() && + (list(i)->asNot()->notOperand()->asBinOp()->op() == BINOP_OR); + result = list(i)->isVar() || list(i)->isQuant() || + list(i)->isNot() && list(i)->asNot()->notOperand()->isVar() || + temp; + + if (result && temp && (basicTarget == NULL)) + basicTarget = list(i); + else if (!result) + if (!basicTarget) + basicTarget = list(i); + else if (basicTarget->isBinOp() && list(i)->isBinOp() && + ((unsigned)basicTarget->asBinOp()->op() > (unsigned)list(i)->asBinOp()->op())) + basicTarget = list(i); + finalresult &= result; + } + + //cout << "done, list is" << (finalresult ? " " : " not ") << "basic" << endl; + + + return finalresult; +} + +Rule AutoRuleSource::getRule(Vectorlhs, PropFormula *rhs) +{ + unsigned i, basic_lhs = isBasic(lhs); + RuleType result = GIVEUP; + PropFormula *target = NULL; + Proof *pftarget = NULL; + PropFormula *zero = NULL, *succ = NULL; + + if (rhs->isVar() || rhs->isQuant()) + { + for (i = 0; i < lhs.size(); i++) + if (lhs(i)->equals(rhs)) + result = HYP; + if (result == GIVEUP) + { + result = NOT_R; + if (induct && rhs->isQuant() && (rhs->asQuant()->getType() == QUANT_FORALL)) + { + Vector v; + v.addElement(new Var("i")); + zero = new BinOp(BINOP_AND, new Pred("Integer", v), new Pred("Zero", v)); + v.addElement(new Var("j")); + Vector w; + w.addElement(new Var("i")); + succ = new BinOp(BINOP_AND, new Pred("Integer", w), new Pred("Succ", v)); + + result = IND; + } + } + } + + if ((result == GIVEUP) && rhs->isBinOp()) + { + if (rhs->asBinOp()->op() == BINOP_AND) + result = AND_R; + if (rhs->asBinOp()->op() == BINOP_IMPL) + result = IMP_R; + if (rhs->asBinOp()->op() == BINOP_OR) + result = OR_R; + + /* This code is commented out because it used the standard */ + /* refinement-logic ORR1 and ORR2, which gets clumsy if you */ + /* can't guess which to use, and harmful as in the case of */ + /* p|~p. */ + /* + { + PropFormula *left = rhs->asBinOp()->leftOperand(), + *right = rhs->asBinOp()->rightOperand(); + + if ((left->isNot() && (left->asNot()->notOperand()->equals(right))) || + (right->isNot() && (right->asNot()->notOperand()->equals(left)))) + result = MAGIC; + } + */ + } + + if ((result == GIVEUP) && rhs->isNot()) + { + result = NOT_R; + } + + /* The new code will never get this far. OR is handled above. */ + /* + if ((result == GIVEUP) && + rhs->isBinOp() && + (rhs->asBinOp()->op() == BINOP_OR)) + { + if (basic_lhs) + { + PropFormula *new_rhs = rhs->asBinOp()->leftOperand()->formCopy(); + + new_rhs->setParent(rhs); + + Proof *attempt = new Proof(lhs, new_rhs, this); + if (attempt->prove() == PROOF_TRUE) + { + pftarget = attempt; + target = rhs; + result = OR_R1; + } + if (result == GIVEUP) + { + delete attempt; // lhs of or was unsuccessful + + new_rhs = rhs->asBinOp()->rightOperand()->formCopy(); + new_rhs->setParent(rhs); + + attempt = new Proof(lhs, new_rhs, this); + if (attempt->prove() == PROOF_TRUE) + { + pftarget = attempt; + target = rhs; + result = OR_R2; + } + if (result == GIVEUP) + delete attempt; // rhs of or was unsuccessful + } + } + if (result == GIVEUP) + { + //if (basicTarget->isNot()) + //{ + // target = basicTarget; + // result = NOT_L; + //} + if (!basic_lhs && rhs->isBinOp() && (rhs->asBinOp()->op() == BINOP_OR)) + { + result = NOT_R; + } + + if (basicTarget) + { + + if (basicTarget->isBinOp() && (basicTarget->asBinOp()->op() == BINOP_OR)) + { + target = basicTarget; + result = OR_L; + } + + if (basicTarget->isBinOp() && (basicTarget->asBinOp()->op() == BINOP_AND)) + { + target = basicTarget; + result = AND_L; + } + + if (basicTarget->isBinOp() && (basicTarget->asBinOp()->op() == BINOP_IMPL)) + { + target = basicTarget; + result = IMP_L; + } + } + + } + } + */ + + if ((result == GIVEUP) && + rhs->isConst()) + { + if (basic_lhs && basicTarget) + { + target = basicTarget; + //cout << "boo!" << basic_lhs << endl; + result = NOT_L; + } + else if (!basic_lhs && basicTarget) + { + if (basicTarget->isBinOp()) + { + if (basicTarget->asBinOp()->op() == BINOP_AND) + { + target = basicTarget; + result = AND_L; + } + if (basicTarget->asBinOp()->op() == BINOP_OR) + { + target = basicTarget; + result = OR_L; + } + + if (basicTarget->asBinOp()->op() == BINOP_IMPL) + { + target = basicTarget; + result = IMP_L; + } + } + if (basicTarget->isNot()) + { + target = basicTarget; + result = NOT_L; + } + + } + } + + if (result == GIVEUP) + { + unsigned j; + + for (i = 0; (result == GIVEUP) && (i < lhs.size()); i++) + { + for (j = i + 1; (result == GIVEUP) && (j < lhs.size()); j++) + if (lhs(i)->isNot() && + lhs(i)->asNot()->notOperand()->isVar() && + lhs(j)->isVar() && + lhs(i)->asNot()->notOperand()->equals(lhs(j))) + { + target = lhs(i); + result = NOT_L; + } + else if (lhs(j)->isNot() && + lhs(j)->asNot()->notOperand()->isVar() && + lhs(i)->isVar() && + lhs(j)->asNot()->notOperand()->equals(lhs(i))) + { + target = lhs(j); + result = NOT_L; + } + } + } + + if (result == GIVEUP) + { + for (i = 0; (result == GIVEUP) && (i < lhs.size()); i++) + { + if (lhs(i)->isQuant() && + (lhs(i)->asQuant()->getType() == QUANT_EXISTS)) + { + target = lhs(i); + if (psource.viewNext() <= psource.getMax()) + result = INSTANT; + else result = GIVEUP; + } + } + } + + if (result == GIVEUP) + { + unsigned min = 0; + target = NULL; + + for (i = 0; i < lhs.size(); i++) + if (lhs(i)->isQuant() && + (lhs(i)->asQuant()->getType() == QUANT_FORALL)) + { + if ((lhs(i)->asQuant()->nextParam() < min) || !target) + { + target = lhs(i); + result = INSTANT; + min = lhs(i)->asQuant()->nextParam(); + } + } + if ((result == INSTANT) && (min > psource.getMax())) + result = GIVEUP; + } + + if (result == GIVEUP) + { + // don't prompt user -- GIVEUP serves a useful purpose, esp. with OR + // return UserRuleSource::getRule(lhs, rhs); + } + + if (!quiet) + { + for (i = 0; i < lhs.size(); i++) + { + lhs(i)->print(*ostr); + if (i < lhs.size() - 1) *ostr << ", " << flush; + } + *ostr << " |- "; + rhs->print(*ostr); + *ostr << " by " << rulename[(unsigned)result] << flush << endl; + if (pause) + { + char strbuf[100]; + *istr >> strbuf; + } + } + if (!pftarget && (result != IND)) + if ((result == INSTANT) && (target->asQuant()->getType() == QUANT_FORALL)) + { + if (target->asQuant()->nextParam() > psource.getMax()) + result = GIVEUP; + + Rule r(result, target, target->asQuant()->nextParam()); + return r; + } + else return Rule(result, target); + else if (result == IND) + return Rule(IND, zero, succ); + else return Rule(result, target, -1, pftarget); +} + diff --git a/src/RuleSource.h b/src/RuleSource.h new file mode 100644 index 0000000..e5a9dcd --- /dev/null +++ b/src/RuleSource.h @@ -0,0 +1,46 @@ +// $Id: RuleSource.h,v 1.5 2000/01/30 00:59:32 david Exp $ + +// RuleSource.h +// An abstraction used for analyzing sequents and supplying rules. + +#ifndef _RULESOURCE_H +#define _RULESOURCE_H + +#include +#include "Rule.h" +#include "formula.h" +#include "Vector.h" + +using namespace std; + +// all we need in the abstract class is a method for returning rules +class RuleSource +{ +public: + virtual Rule getRule(Vector, PropFormula*)=0; +}; + +// A user-assisted rule source -- done +class UserRuleSource : virtual public RuleSource +{ +protected: + istream *istr; // input stream + ostream *ostr; // output stream +public: + UserRuleSource(istream &i, ostream &o) { istr = &i; ostr = &o; } + Rule getRule(Vector, PropFormula*); +private: + unsigned getFormula(Vector, Vector); + unsigned getInstantParam(); +}; + +class AutoRuleSource : virtual public UserRuleSource +{ + unsigned quiet, pause, induct; +public: + AutoRuleSource(istream &i = cin, ostream &o = cout, unsigned q = 0, unsigned p = 0, unsigned in = 0) : UserRuleSource(i, o) { quiet = q; pause = p; induct = in; } + Rule getRule(Vector, PropFormula*); +}; + +#endif /* !_RULESOURCE_H */ + diff --git a/src/Vector.h b/src/Vector.h new file mode 100644 index 0000000..33ef87b --- /dev/null +++ b/src/Vector.h @@ -0,0 +1,103 @@ +// $Id: Vector.h,v 1.3 2000/01/24 17:42:52 david Exp $ + +// Vector.h +// A growable list, somewhat like Java Vectors + +#ifndef _VECTOR_H +#define _VECTOR_H + +template +class Vector +{ + T *data; + unsigned num_elt, next; +private: + void setSize(unsigned i) + { + T *temp = new T[i]; + memcpy(temp, data, sizeof(T) * next); + delete data; + data = temp; + num_elt = i; + } +public: + Vector(unsigned len = 10) + { + data = new T[len]; + num_elt = len; + next = 0; + } + + T& operator()(unsigned i) { return data[i]; } + unsigned size() { return next; } + void addElement(T thing) + { + if (next < num_elt) + data[next++] = thing; + else + { + setSize(num_elt * 2); + addElement(thing); + } + } + + void kill() { delete data; } + + Vector operator=(Vector v) + { + data = v.data; + num_elt = v.num_elt; + next = v.next; + return *this; + } + + ~Vector() { } +}; + +template +inline Vector copy(Vector v) +{ + unsigned i; + Vector result; + + for (i = 0; i < v.size(); i++) + result.addElement(v(i)); + + return result; +} + +template +inline Vector copyBut(Vector v, T exception) +{ + unsigned i; + Vector result; + + for (i = 0; i < v.size(); i++) + if (v(i) != exception) + result.addElement(v(i)); + + return result; +} + +template +inline void vectorReplace(Vector v, T oldItem, T newItem) +{ + unsigned i; + + for (i = 0; i < v.size(); i++) + if (v(i) == oldItem) + v(i) = newItem; + +} + +template +inline void vectorAppend(Vector & v1, Vector v2) +{ + unsigned i; + + for (i = 0; i < v2.size(); i++) + v1.addElement(v2(i)); +} + + +#endif /* !_VECTOR_H */ diff --git a/src/copysplit.cc b/src/copysplit.cc new file mode 100644 index 0000000..48bfb2e --- /dev/null +++ b/src/copysplit.cc @@ -0,0 +1,33 @@ +#include "copysplit.h" + +using namespace std; + +Vector copysplit(Vector v) +{ + Vector result; + unsigned i; + + for (i = 0; i < v.size(); i++) + { + result.addElement(v(i)->formCopy()); + } + + return result; + +} + +Vector copysplitbut(Vector v, PropFormula *but) +{ + Vector result; + unsigned i; + + for (i = 0; i < v.size(); i++) + { + if (v(i) != but) + result.addElement(v(i)->formCopy()); + } + + return result; + +} + diff --git a/src/copysplit.h b/src/copysplit.h new file mode 100644 index 0000000..e748cc3 --- /dev/null +++ b/src/copysplit.h @@ -0,0 +1,13 @@ +#ifndef _COPYSPLIT_H +#define _COPYSPLIT_H + +#include "Vector.h" +#include "formula.h" + +extern Vector +copysplit(Vector); + +extern Vector +copysplitbut(Vector, PropFormula*); + +#endif /* !def _COPYSPLIT_H */ diff --git a/src/formula.cc b/src/formula.cc new file mode 100644 index 0000000..8d7fde9 --- /dev/null +++ b/src/formula.cc @@ -0,0 +1,237 @@ +// $Id: formula.cc,v 1.5 2000/01/25 03:05:43 david Exp $ + +// formula.cc +// +// mostly print methods for formula classes +#include +#include "formula.h" + +void PropFormula::println(ostream & o) +{ + print(o); + o << endl; +} + +void Var::print(ostream & o) +{ + o << name; +} + +boolean Var::equals(PropFormula *formula) +{ + if (formula->isVar() == false) + return false; + Var *v = formula->asVar(); + if (!strcmp(v->name, name)) return true; + return false; +} + +PropFormula *Var::replace(Var *v, Var *r) +{ + if (this->equals(v)) + { + PropFormula *result = r->formCopy(); + + result->setParent(this); + + return result; + } + else return this->formCopy(); +} + +void Pred::print(ostream & o) +{ + if (!strcmp(this->varName(), "Equal") && (getParams().size() == 2)) + { + o << "("; + getParams()(0)->print(o); + o << " = "; + getParams()(1)->print(o); + o << ")"; + } + else + { + Var::print(o); + o << "("; + unsigned i; + + for (i = 0; i < getParams().size(); i++) + { + getParams()(i)->print(o); + if (i < getParams().size() - 1) + o << ", "; + } + o << ")"; + } +} + +boolean Pred::equals(PropFormula *formula) +{ + if (Var::equals(formula) == false) + return false; + if (formula->asVar()->isPred() == false) + return false; + Pred *pf = formula->asVar()->asPred(); + + if (pf->getParams().size() != getParams().size()) + return false; + + unsigned i; + + for (i = 0; i < getParams().size(); i++) + if (!getParams()(i)->equals(pf->getParams()(i))) + return false; + + return true; +} + +PropFormula * Pred::replace(Var *v, Var *r) +{ + unsigned i; + Pred *temp = this->formCopy()->asVar()->asPred(); + + for (i = 0; i < temp->getParams().size(); i++) + if (temp->getParams()(i)->equals(v)) + { + //delete temp->getParams()(i); + temp->getParams()(i) = r; + } + + temp->setParent(this); + + return temp; +} + +void Not::print(ostream & o) +{ + o << "~"; + operand->print(o); + o << flush; +} + +boolean Not::equals(PropFormula *formula) +{ + if (formula->isNot() == false) + return false; + Not *v = formula->asNot(); + return operand->equals(v->operand); +} + +void BinOp::print(ostream & o) +{ + o << "("; + if ((opr == BINOP_AND) && + left->isBinOp() && + (left->asBinOp()->op() == BINOP_IMPL) && + right->isBinOp() && + (right->asBinOp()->op() == BINOP_IMPL) && + (right->asBinOp()->leftOperand()->equals(left->asBinOp()->rightOperand())) && + (right->asBinOp()->rightOperand()->equals(left->asBinOp()->leftOperand()))) + { + left->asBinOp()->leftOperand()->print(o); + o << " <==> "; + left->asBinOp()->rightOperand()->print(o); + } + else + { + left->print(o); + switch(opr) + { + case BINOP_IMPL : o << " ==> "; + break; + case BINOP_AND : o << " & "; + break; + case BINOP_OR : o << " | "; + } + right->print(o); + } + + o << ")" << flush; +} + +boolean BinOp::equals(PropFormula *formula) +{ + if (formula->isBinOp() == false) + return false; + BinOp *v = formula->asBinOp(); + return left->equals(v->left) && right->equals(v->right); +} + +void ConstFormula::print(ostream& o) +{ + o << (val ? "true" : "false") << flush; +} + +boolean ConstFormula::equals(PropFormula *formula) +{ + if (formula->isConst() == false) + return false; + ConstFormula *v = formula->asConst(); + return (v->value() == value()); +} + +void QuantFormula::print(ostream & o) +{ + switch (type) + { + case QUANT_FORALL: + o << "FORALL"; break; + case QUANT_EXISTS: + o << "EXISTS"; break; + default: + o << "?QUANT"; + } + o << "{"; + variable->print(o); + + PropFormula *f = formula; + + while (f->isQuant() && (f->asQuant()->getType() == this->getType())) + { + o << ", "; + f->asQuant()->getVariable()->print(o); + f = f->asQuant()->getFormula(); + } + + o << "}"; + f->print(o); + o << flush; +} + +boolean QuantFormula::equals(PropFormula *form) +{ + if (form->isQuant() == false) + return false; + if (form->asQuant()->getType() != getType()) + return false; + if (!form->asQuant()->getVariable()->equals(variable)) + return false; + if (!form->asQuant()->getFormula()->equals(formula)) + return false; + + return true; +} + +PropFormula * QuantFormula::instantiate(Var *sub) +{ + instantForm = formula->replace(variable, sub); + return instantForm; +} + +PropFormula * QuantFormula::replace(Var *v, Var *r) +{ + if (!this->variable->equals(v)) + { + /* handle quantifier capture -- shouldn't happen if we're well-formed */ + + + PropFormula *result = new QuantFormula(this->type, this->variable->formCopy()->asVar(), + formula->replace(v, r)); + + result->setParent(this); + + return result; + } + else return this->formCopy(); +} + diff --git a/src/formula.h b/src/formula.h new file mode 100644 index 0000000..779f982 --- /dev/null +++ b/src/formula.h @@ -0,0 +1,320 @@ +// $Id: formula.h,v 1.4 2000/01/25 03:05:43 david Exp $ + +// formula.h +// +// classes defining propositional formulas + +#ifndef _FORMULA_H +#define _FORMULA_H + +#include +#include +#include +#include "Vector.h" +#include "Markable.h" + +using namespace std; + +#ifndef boolean +#define boolean int +#define true 1 +#define false 0 +#endif /* !def _boolean */ + +// enumerated type for binary operators +typedef enum { + BINOP_AND, + BINOP_OR, + BINOP_IMPL } BooleanOperator; + +typedef enum { + QUANT_FORALL, + QUANT_EXISTS } QuantifierType; + +class Var; +class Not; +class BinOp; +class ConstFormula; +class QuantFormula; + +// supertype for propositional formulas, along with overridable +// type-determining functions. Markable superclass lets us hide irrelevant formulas +class PropFormula : public Markable +{ +private: + boolean tag; + PropFormula *_parent; +public: + // the following are pseudo-casts + virtual boolean isVar() { return false; } // overridden by Var + virtual Var *asVar() { return NULL; } + + virtual boolean isNot() { return false; } // overridden by Not + virtual Not *asNot() { return NULL; } + + virtual boolean isBinOp() { return false; } // overridden by BinOp + virtual BinOp *asBinOp() { return NULL; } + + virtual boolean isConst() { return false; } // overridden by ConstFormula + virtual ConstFormula *asConst() { return NULL; } + + virtual boolean isQuant() { return false; } + virtual QuantFormula *asQuant() { return NULL; } + + // printing routines + virtual void print(ostream&) = 0; + void println(ostream&); + + // equivalence testing routine + virtual boolean equals(PropFormula *) = 0; + + // copy formula + virtual PropFormula * formCopy() = 0; + + // instantiating quantified formulas requires... + virtual PropFormula * replace(Var * /* current */, Var * /* replacement */) = 0; + + // tag manipulation + void setTag() { tag = true; } + boolean tagged() { return tag; } + + // parent formula + void setParent(PropFormula *p) { _parent = p; } + PropFormula* getParent() { return _parent; } + + PropFormula() : Markable(0) { tag = false; _parent = NULL; } + +}; + +class Pred; + +// a formula consisting entirely of a single variable +class Var : virtual public PropFormula +{ + char *name; +public: + Var(const char *n) { name = strdup(n); } + + virtual void print(ostream&); + + virtual boolean equals(PropFormula *); + + // override the right pseudo-casts + Var *asVar() { return this; } + boolean isVar() { return true; } + + virtual boolean isPred() { return false; } + virtual Pred *asPred() { return NULL; } + + // accessor for variable name + char *varName() { return name; } + + virtual PropFormula * formCopy() + { + PropFormula *result = new Var(name); + + // set parent + result->setParent(this); + if (tagged()) result->setTag(); + + return result; + } + + virtual PropFormula * replace(Var *, Var *); +}; + +class Pred : virtual public Var +{ + Vector params; +public: + Pred(char *n, Vector p) : Var(n) { params = copy(p); } + + virtual void print(ostream &); + virtual boolean equals(PropFormula *); + + boolean isPred() { return true; } + Pred *asPred() { return this; } + + Vector &getParams() { return params; } + + PropFormula * formCopy () + { + PropFormula *result = new Pred(this->varName(), copy(params)); + + result->setParent(this); + if (tagged()) result->setTag(); + + return result; + } + + PropFormula * replace(Var *, Var *); + +}; + +// a formula consisting of the negation of another formula +class Not : virtual public PropFormula +{ + PropFormula *operand; +public: + Not(PropFormula *opnd) { operand = opnd; } + void print(ostream&); + boolean equals(PropFormula *); + + // override the appropriate pseudo-casts + Not *asNot() { return this; } + boolean isNot() { return true; } + + // accessor for operand of 'not' operator + PropFormula *notOperand() { return operand; } + + PropFormula * formCopy () + { + PropFormula *result = new Not(operand->formCopy()); + + result->setParent(this); + if (tagged()) result->setTag(); + + return result; + } + + PropFormula * replace(Var *v, Var *r) + { + PropFormula *result = new Not(operand->replace(v, r)); + + result->setParent(this); + if (tagged()) result->setTag(); + + return result; + } +}; + +// a formula encoding a binary operation on two subformulas +class BinOp : virtual public PropFormula +{ + PropFormula *left, *right; + BooleanOperator opr; +public: + BinOp(BooleanOperator o, PropFormula *l, PropFormula *r) + { + left = l; + right = r; + opr = o; + } + + boolean isBinOp() { return true; } + BinOp *asBinOp() { return this; } + + void print(ostream&); + + boolean equals(PropFormula *); + + PropFormula *leftOperand() { return left; } + PropFormula *rightOperand() { return right; } + + BooleanOperator op() { return opr; } + + PropFormula * formCopy () + { + PropFormula *result = new BinOp(opr, left->formCopy(), right->formCopy()); + + result->setParent(this); + if (tagged()) result->setTag(); + + return result; + } + + PropFormula * replace(Var *v, Var *r) + { + PropFormula *lf = left->replace(v, r), + *rf = right->replace(v, r), + *result = new BinOp(opr, lf, rf); + + result->setParent(this); + if (tagged()) result->setTag(); + + return result; + } +}; + +class ConstFormula : virtual public PropFormula +{ + boolean val; +public: + ConstFormula(boolean v) + { + val = v; + } + + boolean value() { return val; } + + boolean isConst() { return true; } + ConstFormula *asConst() { return this; } + + void print(ostream&); + + boolean equals(PropFormula *); + + PropFormula * formCopy () + { + PropFormula *result = new ConstFormula(val); + + result->setParent(this); + if (tagged()) result->setTag(); + + return result; + } + + PropFormula * replace(Var *, Var *) { return this->formCopy(); } +}; + + +class QuantFormula : virtual public PropFormula +{ + QuantifierType type; + Var *variable; + PropFormula *formula; + unsigned nextP; + + PropFormula *instantForm; // keep track of instantiated formula +public: + QuantFormula(QuantifierType t, Var *v, PropFormula *f, unsigned nP = 0) + { + type = t; + variable = v; + formula = f; + nextP = nP; + instantForm = NULL; + } + + boolean isQuant() { return true; } + QuantFormula *asQuant() { return this; } + + void print(ostream&); + boolean equals(PropFormula *); + + QuantifierType getType() { return type; } + Var *getVariable() { return variable; } + PropFormula *getFormula() { return formula; } + + unsigned nextParam() { return nextP; } + void incParam() { nextP++; } + void decParam() { nextP--; } + PropFormula *instantiate(Var *); + + PropFormula *instantFormula() { return instantForm; } + + PropFormula * formCopy () + { + PropFormula *result = new QuantFormula(type, variable->formCopy()->asVar(), formula->formCopy(), nextP); + + result->setParent(this); + if (tagged()) result->setTag(); + + return result; + } + + PropFormula * replace(Var *, Var *); +}; + +#endif /* !_FORMULA_H */ + diff --git a/src/lex.cc b/src/lex.cc new file mode 100644 index 0000000..e3fe865 --- /dev/null +++ b/src/lex.cc @@ -0,0 +1,165 @@ +// $Id: lex.cc,v 1.3 2000/01/24 17:42:52 david Exp $ + +// lex.cc +// by David Baer +// +// Lexical analyzer -- helps to parse formulas + +#include +#include +#include +#include +//#include +#include "lex.h" + +using namespace std; + +char *token_id_name = NULL; +istream *input; + +void setInput(istream& i) +{ + input = &i; +} + +// private class, local to this file +class LexBuffer +{ + char buf[256]; + int pos, end, str; +public: + LexBuffer() { pos = 0; end = -1; str = 0; do advance(); while (!strlen(buf)); } + LexBuffer(char *string) { strlcpy(buf, string, 256); pos = 0; end = strlen(string); str = 1; } + void advance() { + //cout << "buffer.advance" << endl; + if (!str && (pos > end)) + { + //cout << "buffer.advance read" << endl; + input->getline(buf, 255); + //cout << "got line: \"" << buf << "\"" << endl; + pos = 0; + end = input->gcount(); + } + else if (pos <= end) pos++; + //cout << "buffer.advance done: pos = " << pos << ", end = " << end << endl; + } + char current() { + if (pos >= end) return '\0'; + //cout << "buffer.current = " << buf[pos] << endl; + return buf[pos]; + } +} *buffer; + +void setInput(char *str) +{ + buffer = new LexBuffer(str); +} + +void illChar(char ch) +{ + cerr << "Illegal character ('" << ch << "') in input!" << endl; + exit(0); +} + +void killStr() +{ + delete token_id_name; +} + +int yylex(void) +{ + if (!buffer) buffer = new LexBuffer(); + char ch, idBuf[500]; + + // eat whitespace + while ((ch = buffer->current()) == ' ') buffer->advance(); + + switch (ch) + { + case '\r': buffer->advance(); + case '\n': buffer->advance(); + case '\0': /* cout << "end: " << (int)ch << endl; */ return -1; + case ',' : buffer->advance(); return TOKEN_COMMA; + case '{' : buffer->advance(); return TOKEN_LBRACE; + case '}' : buffer->advance(); return TOKEN_RBRACE; + case '(' : buffer->advance(); return TOKEN_LPAREN; + case ')' : buffer->advance(); return TOKEN_RPAREN; + case '&' : buffer->advance(); return TOKEN_AND; + case '|' : buffer->advance(); return TOKEN_OR; + case '=' : while (buffer->current() != '>') + { + if (buffer->current() != '=') + { + illChar(buffer->current()); + } + buffer->advance(); + } + buffer->advance(); // eat final > + return TOKEN_IMPL; + case '<' : buffer->advance(); + + while (buffer->current() != '>') + { + if (buffer->current() != '=') + illChar(buffer->current()); + buffer->advance(); + } + buffer->advance(); // eat final > + return TOKEN_IFF; + case '~' : buffer->advance(); return TOKEN_NOT; + default : if (!isalpha(ch)) + illChar(buffer->current()); + idBuf[0] = ch; + int index = 1; + buffer->advance(); + while (isalpha(ch = buffer->current())) + { + idBuf[index++] = ch; + buffer->advance(); + } + idBuf[index] = '\0'; + if (token_id_name) delete token_id_name; + token_id_name = strdup(idBuf); + if (!strcasecmp(token_id_name, "FORALL")) return TOKEN_FORALL; + else if (!strcasecmp(token_id_name, "EXISTS")) return TOKEN_EXISTS; + else return TOKEN_ID; + } + +} + +void flushInput() { +// char line[100]; +// input.getline(line, 98); + if (buffer) + { + delete buffer; + buffer = NULL; + } + +} + +static +const char *token_name[] = +{ + "TOKEN_COMMA", + "TOKEN_FORALL", + "TOKEN_EXISTS", + "TOKEN_LBRACE", + "TOKEN_RBRACE", + "TOKEN_LPAREN", + "TOKEN_RPAREN", + "TOKEN_AND", + "TOKEN_OR", + "TOKEN_IMPL", + "TOKEN_NOT", + "TOKEN_ID" +}; + +void printToken(Token t) +{ + if ((t >= TOKEN_COMMA) && (t <= TOKEN_ID)) + cout << token_name[(int)t]; + else cout << "(UNKNOWN TOKEN)"; +} + + diff --git a/src/lex.h b/src/lex.h new file mode 100644 index 0000000..72d82e0 --- /dev/null +++ b/src/lex.h @@ -0,0 +1,36 @@ +// $Id: lex.h,v 1.3 2000/01/24 17:42:52 david Exp $ + +// lex.h -- contains token types +#ifndef _LEX_H +#define _LEX_H + +#include +using std::istream; + +typedef enum { + TOKEN_ERR = -1, + TOKEN_COMMA = 0, + TOKEN_FORALL, + TOKEN_EXISTS, + TOKEN_LBRACE, + TOKEN_RBRACE, + TOKEN_LPAREN, + TOKEN_RPAREN, + TOKEN_AND, + TOKEN_OR, + TOKEN_IMPL, + TOKEN_IFF, + TOKEN_NOT, + TOKEN_ID } Token; + +#define restart setInput + +extern char *token_id_name; +extern void setInput(istream&); +extern void setInput(char*); +extern int yylex(void); +extern void flushInput(); +extern void printToken(Token); + +#endif /* !_LEX_H */ + diff --git a/src/lionheart b/src/lionheart new file mode 100755 index 0000000..726e957 Binary files /dev/null and b/src/lionheart differ diff --git a/src/main.cc b/src/main.cc new file mode 100644 index 0000000..873a923 --- /dev/null +++ b/src/main.cc @@ -0,0 +1,89 @@ +// $Id: main.cc,v 1.5 2000/01/30 00:59:32 david Exp $ + +// main.cc +// by David Baer +// +// Main module -- read formula and attempt a proof, then save if desired + +#include +#include +#include +#include +//#include +#include +#include "formula.h" +#include "Proof.h" +#include "parser.h" +#include "Options.h" +#include "Axiom.h" +#include "ParamSource.h" + +using namespace std; + +int main(int argc, char *argv[]) +{ + PropFormula *form; + char filename[200]; + Options opt(argc, argv); + + if (opt.help()) + { + opt.syntax(); + exit(0); + } + + form = opt.getFormula(); + + if (!form) + { + cout << "Formula to be proved: " << flush; + + initParser(cin); + form = parseFormula(); + endParser(); + } + + if (!form) + { + cout << "not a valid formula" << endl; + exit(0); + } + + psource.setMax(opt.maxParam()); + + //form->println(cout); + RuleSource *guide; + guide = (opt.manual() ? new UserRuleSource(cin, cout) : new AutoRuleSource(cin, cout, opt.quiet(), opt.pause(), opt.induction())); + Proof *pf = (opt.manual() ? new Proof(form, guide) : new Proof(axioms.getVector(), form, guide)); + //Proof *pf = new Proof(form); + if (pf->prove() == PROOF_TRUE) + { + if (!opt.quiet()) cout << "Theorem is a tautology" << endl; + //cin >> filename; + //cin.getline(filename, 198); // don't ask me why I have to do this... + if (!opt.dump()) + { + if (opt.outputFile()) + { + if (!opt.quiet()) cout << "Saving proof to " << opt.outputFile() << endl; + strlcpy(filename, opt.outputFile(), 200); + } + else + { + cout << "Save proof to : " << flush; + cin.getline(filename, 198); + } + if (strlen(filename)) + { + ofstream o(filename); + pf->print(o); + } + } + else pf->print(cout); + } + else cout << "Did not find a proof " << endl; + + //pf->cleanup(); + delete pf; + return 0; +} diff --git a/src/parser.cc b/src/parser.cc new file mode 100644 index 0000000..b384a9d --- /dev/null +++ b/src/parser.cc @@ -0,0 +1,263 @@ +// $Id: parser.cc,v 1.4 2000/01/25 03:05:43 david Exp $ + +// parser.cc +// by David Baer +// +// Convert text into a formula object + +#include +#include +#include +#include "lex.h" +#include "formula.h" +#include "Proof.h" +//#include "RuleSource.h" + +Token current = (Token)-1; + +inline void advance() { current = (Token)yylex(); } +inline void setup() { +// while ((current = (Token)yylex()) == -1); // eat CRLF's + while (current == -1 ) advance(); +} + +PropFormula *parseTerm(); +PropFormula *parseAnd(); +PropFormula *parseOr(); +PropFormula *parseFormula(); + +PropFormula *build(PropFormula *left, Token op) +{ + //cout << "build" << endl; + Token curOp = op; + PropFormula *result = left; + + while (curOp == op) + { + advance(); // eat operator + switch(op) + { + case TOKEN_IFF : result = new BinOp(BINOP_IMPL, result, parseOr()); + result = new BinOp(BINOP_AND, result, new BinOp(BINOP_IMPL, result->asBinOp()->rightOperand()->formCopy(), result->asBinOp()->leftOperand()->formCopy())); + break; + case TOKEN_IMPL : result = new BinOp(BINOP_IMPL, result, parseOr()); + break; + case TOKEN_OR : result = new BinOp(BINOP_OR, result, parseAnd()); + break; + case TOKEN_AND : result = new BinOp(BINOP_AND, result, parseTerm()); + break; + default : ; + } + curOp = current; + } + //cout << "done build" << endl; + return result; +} + +static inline +Vector getVarList() +{ + Vector result; + + //cout << "Variables in list: "; + while (current == TOKEN_ID) + { + result.addElement(new Var(token_id_name)); + //cout << token_id_name; + advance(); + + if (current == TOKEN_COMMA) + { + advance(); + //cout << ", "; + } + //else cout << endl; + + } + + return result; +} + +static inline +Var *handleId() +// pre: current -> TOKEN_ID +{ + Var *result; + char *str = strdup(token_id_name); + + //cout << "handleId()" << endl; + + + advance(); + if (current == TOKEN_LPAREN) + { + Vector params; + + advance(); // eat ( + params = getVarList(); + if (current != TOKEN_RPAREN) + cerr << "expected ) to close predicate parameter list" << endl; + else advance(); // eat ) + + result = new Pred(str, params); + + } + else result = new Var(str); + + delete str; + + //cout << "handleId() result: "; + //result->println(cout); + return result; +} + +static inline +QuantFormula *handleQuant() +// pre: current -> TOKEN_{FORALL,EXISTS} +{ + QuantifierType type = (current == TOKEN_FORALL ? QUANT_FORALL : QUANT_EXISTS); + + //cout << "handleQuant()" << endl; + + advance(); + // expect a { here + if (current != TOKEN_LBRACE) + // complain bitterly + cerr << "expected a { after quantifier" << endl; + else advance(); + + Vector vars = getVarList(); + + if (current != TOKEN_RBRACE) + cerr << "expected a } to close quantified variables" << endl; + else advance(); // past } to quantified formula + + int i; + PropFormula *formula = parseTerm(); // read quantified formula + + //cout << "prepending " << vars.size() << "variables" << endl; + for (i = vars.size() - 1; i >= 0; i--) + formula = new QuantFormula(type, vars(i), formula); + + //cout << "duh.." << endl; + + vars.kill(); + + //cout << "handleQuant() result: "; + //formula->println(cout); + return formula->asQuant(); +} + +PropFormula *parseTerm() +{ + //cout << "parseTerm()" << endl; + PropFormula *result; + + switch(current) + { + case -1 : cerr << "Premature end of file!" << endl; + return NULL; + case TOKEN_NOT : advance(); // eat ~ + result = new Not(parseTerm()); + break; + case TOKEN_LPAREN : advance(); // eat ( + result = parseFormula(); + if (current != TOKEN_RPAREN) + cerr << "missing right paren!" << endl; + else advance(); // eat ) + break; + case TOKEN_ID : result = handleId(); break; + case TOKEN_FORALL: + case TOKEN_EXISTS: result = handleQuant(); break; + default : return NULL; + } + + //cout << "parseTerm() result: "; + //result->println(cout); + return result; + +} + +PropFormula *parseAnd() +{ + //cout << "parseAnd" << endl; + PropFormula *result; + + switch(current) + { + case -1 : cerr << "Premature end of input!" << endl; + return NULL; + case TOKEN_NOT : + case TOKEN_LPAREN : + case TOKEN_FORALL: + case TOKEN_EXISTS: + case TOKEN_ID : result = parseTerm(); + if (current == TOKEN_AND) + return build(result, TOKEN_AND); + else return result; + default : return NULL; + } +} + +PropFormula *parseOr() +{ + //cout << "parseOr" << endl; + PropFormula *result; + + switch(current) + { + case -1 : cerr << "Premature end of input!" << endl; + return NULL; + case TOKEN_NOT : + case TOKEN_LPAREN : + case TOKEN_FORALL: + case TOKEN_EXISTS: + case TOKEN_ID : result = parseAnd(); + if (current == TOKEN_OR) + return build(result, TOKEN_OR); + else return result; + default : return NULL; + } +} + +PropFormula *parseFormula() +{ + //cout << "parseFormula" << endl; + PropFormula *result; + + switch (current) + { + case -1 : cerr << "Premature end of input!" << endl; + return NULL; + case TOKEN_NOT : + case TOKEN_LPAREN : + case TOKEN_FORALL: + case TOKEN_EXISTS: + case TOKEN_ID : // implication level + result = parseOr(); + if ((current == TOKEN_IMPL) || (current == TOKEN_IFF)) + return build(result, current); + else return result; + default : return NULL; + } +} + +void initParser(istream& i) +{ + //cout << "initParser" << endl; + restart(i); + //cout << "setup" << endl; + setup(); + //cout << "done setup" << endl; +} + +void initParser(char *str) +{ + restart(str); + setup(); +} + +void endParser() +{ + flushInput(); +} diff --git a/src/parser.h b/src/parser.h new file mode 100644 index 0000000..b7d8110 --- /dev/null +++ b/src/parser.h @@ -0,0 +1,20 @@ +// $Id: parser.h,v 1.3 2000/01/24 17:42:52 david Exp $ + +// parser.h +// by David Baer +// +// Headers for the parser + +#ifndef _PARSER_H +#define _PARSER_H + +#include +#include "formula.h" + +extern void initParser(istream&); +extern void initParser(char*); +extern PropFormula *parseFormula(); +extern void endParser(); + +#endif /* !_PARSER_H */ + diff --git a/src/predtest.cc b/src/predtest.cc new file mode 100644 index 0000000..2be3e32 --- /dev/null +++ b/src/predtest.cc @@ -0,0 +1,50 @@ +// $Id: predtest.cc,v 1.2 1999/11/17 01:47:34 david Exp $ + +// predtest.cc +// by David Baer +// +// Silly little test of predicates + +#include +#include +#include "formula.h" +#include "Vector.h" + +int main() +{ + char c; + Vector params; + + for (c = 'w'; c <= 'z'; c++) + { + char str[55] = "\0\0"; + //snprintf(str, 55, "%c", c); + str[0] = c; + params.addElement(new Var(str)); + } + Pred *test = new Pred("P", params), *test2 = new Pred("Q", params); + + cout << "Preds:" << endl; + test->println(cout); + test2->println(cout); + + test->print(cout); + if (test->equals(test2)) cout << "="; + else cout << "!="; + test2->print(cout); + cout << endl; + + QuantFormula *test3 = new QuantFormula(QUANT_FORALL, new Var("w"), + new QuantFormula(QUANT_FORALL, new Var("x"), + new QuantFormula(QUANT_FORALL, new Var("y"), + new QuantFormula(QUANT_FORALL, new Var("z"), + test)))); + + test3->println(cout); + + PropFormula *test4 = test3->instantiate(new Var("w0")); + + test4->println(cout); + + return 0; +}