#!/bin/bash -f
########################################################################
#
# File  : eproof_ram
#
# Author: Stephan Schulz
#
# Contents
# 
#   Shell script for automatic proof generation with E. See the help
#   text below for more information and copyright status.
# 
# Changes
#
# <1> Distant past
#     New
# <2> Sun Feb 22 14:05:04 CET 2009
#     Added this header and --help function.
# <3> Fri Jul 15 22:30:55 CEST 2011
#     Create from eproof
#
########################################################################

EXECPATH=/Users/schulz/SOURCES/Projects/E/PROVER

VERSION=`$EXECPATH/eprover --version|cut -d' ' -f2-`

pid=$$
host=`hostname`


print_help ()
{
    echo "eproof " $VERSION
    sed -e 's/\\n/\
/g' <<EOF
\n\
Usage: eproof_ram [options] <file1> ...\n\
\n\
Eproof_ram is a wrapper around E and epclextract. It will run E with\n\
output level 4 (full output of all potentially proof-relevant\n\
inferences) and pipe the output through epclextract to provide a\n\
proof derivation or a derivation of all clauses in the saturated\n\
proof state.\n\
\n\
Eproof_ram will intercept the command line arguments and interpret\n\
certain options as described below. All other options and arguments\n\
are  passed on to eprover or epclextract, as appropriate. See those\n\
tools help pages for the supported options.\n\
\n\
In particular, eproof_ram will automatically do a close approximation\n\
of 'the right thing' (tm) with the options describing input- and output\n\
formats. \n\
\n\
Options:
\n\
   -h\n\
  --help\n\
    Print a short description of program usage and options.\n\
\n\
  --version\n\
    Print the version numbers of eprover and epclextract used by this\n\
    instance of eproof. Please include this with all bug reports (if\n\
    any).\n\
\n\
Copyright (C) 1998-2011 by Stephan Schulz, schulz@eprover.org\n\
\n\
You can find the latest version of E and additional information at\n\
http://www.eprover.org\n\
\n\
This program is free software; you can redistribute it and/or modify\n\
it under the terms of the GNU General Public License as published by\n\
the Free Software Foundation; either version 2 of the License, or\n\
(at your option) any later version.\n\
\n\
This program is distributed in the hope that it will be useful,\n\
but WITHOUT ANY WARRANTY; without even the implied warranty of\n\
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the\n\
GNU General Public License for more details.\n\
\n\
You should have received a copy of the GNU General Public License\n\
along with this program (it should be contained in the top level\n\
directory of the distribution in the file COPYING); if not, write to\n\
the Free Software Foundation, Inc., 59 Temple Place, Suite 330,\n\
Boston, MA  02111-1307 USA\n\
\n\
The original copyright holder can be contacted as\n\
\n\
Stephan Schulz (I4)\n\
Technische Universitaet Muenchen\n\
Institut fuer Informatik\n\
Boltzmannstrasse 3\n\
85748 Garching bei Muenchen\n\
Germany\n\

EOF
}



outfile=""

newargs=""
format=""


for argument in  "$@"; do
    if [ "$argument" = "-V" -o "$argument" = "--version" ] ; then
        echo $0 $VERSION
        exit $?
    elif [ "$argument" = "-h" -o "$argument" = "--help" ] ; then
        print_help
        exit $?
    else
	head=`echo "$argument"|cut -d= -f1`
	head1=`echo "$argument"|cut -c1-2`
	if [ "$head" = "--cpu-limit" ] ; then
	    timelimit=`echo $argument|cut -d= -f2`
	fi    
	if [ "$head1" = "-o" ] ; then
	    echo "Short option -o not supported by eproof, use --output-file=<file>"
	    exit 1
	fi    
	if [ "$head" = "--output-file" ] ; then
	    outfile=`echo $argument|cut -d= -f2`
	    cat /dev/null > $outfile
	    argument=""
	fi
	if  [ "$argument" = "--tstp-out" ] ; then
	    argument=""
	    format="--tstp-out"
	fi
	if  [ "$argument" = "--tstp-format" ] ; then
	    argument="--tstp-in"
	    format="--tstp-out"
	fi
	if  [ "$argument" = "--tptp3-out" ] ; then
	    argument=""
	    format="--tstp-out"
	fi
	if  [ "$argument" = "--tptp3-format" ] ; then
	    argument="--tstp-in"
	    format="--tstp-out"
	fi
    fi
    if [ "$argument" ] ; then        
        newargs=$newargs" "$argument
    fi
done

$EXECPATH/eprover $newargs -l4 -o- --pcl-terms-compressed --pcl-compact|$EXECPATH/epclextract $format -f -C --competition-framing