#! /usr/bin/perl

#**************************************************************
#* ********************************************************** *
#* *                                                        * *
#* *          Manages the correctness tests                 * *
#* *                                                        * *
#* *                                                        * *
#* $Revision: 0.48 $                                        * *
#* $State: Exp $                                            * *
#* $Date: 2001/02/08 11:17:00 $                             * *
#* $Author: weidenb $                                       * *
#* *                                                        * *
#* *             Contact:                                   * *
#* *             Christoph Weidenbach                       * *
#* *             MPI fuer Informatik                        * *
#* *             Stuhlsatzenhausweg 85                      * *
#* *             66123 Saarbruecken                         * *
#* *             Email: weidenb@mpi-sb.mpg.de               * *
#* *             Germany                                    * *
#* *                                                        * *
#* ********************************************************** *
#**************************************************************


# $RCSfile: pcs,v $


#############################################################
#
#
# Perl script for checking proofs in DFG format (.prf files)
#
# Usage:
# pcs [options] Filename
#
#
# Options:
#
# -c continue on failure to prove proof line correct (default false)
# -r clean up at end if no proof incorrect (default false)
# -f force: delete and re-create working directory if it exists
#
# -d (name) suffix of created working directory
#           (default "_SubProofs")
# -t time limit for proof attempt (default 3 (seconds))
# -v print out some comments while proofs are checked
#
# -s suffix of generated proof files (handed over to pgen)
# -q quiet: do not print program paths, which is useful
#           inside checkstat
# -o take SPASS instead of otter
# -p path of DFG prover
# -w path of DFG converter
#
# extra:
# -x print debugging infos
# -C
#
##############################################################

use strict;
use File::Copy;
use File::Path;     # for rmtree
use Getopt::Std;

#########################################################
# Flag for: Also take paths of pgen, otter, dfg2otter
# from same-name environment variables
#########################################################
my $envpaths = 1;

#########################################################
#  Globals
#########################################################
my $sep = "---------------------------------------------------------------\n"; # formatting

############################################
# Get program paths from environment:
# SPASS, otter, dfg2otter, pgen
############################################

my $SPASS = "SPASS";
if (defined($ENV{'SPASS'})) {
  $SPASS = $ENV{'SPASS'};
}

# proof file generator
my $PGEN = "pgen";
if ($envpaths) {
  if (defined($ENV{'PGEN'})) {
    $PGEN = $ENV{'PGEN'};
  }
}

my $OTTER = "otter";
if ($envpaths) {
  if (defined($ENV{'OTTER'})) {
    $OTTER = $ENV{'OTTER'};
  }
}

my $DFG2OTTER_PL = "dfg2otter.pl";
if ($envpaths) {
  if (defined($ENV{'DFG2OTTER_PL'})) {
    $DFG2OTTER_PL = $ENV{'DFG2OTTER_PL'};
  }
}

my $DFGPROVER = "";		# possibly another prover (not OTTER or SPASS)

# default SPASS options
my $SPASS_flags = "-Memory=0 -Splits=0 -PProblem=0 -PGiven=0";

#################################################
# Constants associated with proof file generator
#################################################
# messages from proof file generator
my $PGEN_OKMSG       = "All files generated"; # everything ok
my $PGEN_FAILMSG     = "Proof not correct"; # some error occured

my $PCS_VALIDMSG     = "Proof valid.";
my $PCS_INVALIDMSG   = "Proof not correct.";
my $PCS_UNDECIDEDMSG = "Correctness of proof not decided";

############################################
# temporary files
############################################
my $TMPDIR = "/tmp/";
my @TOREMOVE = ();

############################################
# Results of theorem prover
# (return values of procedure that evaluates
#  the prover output)
############################################
my $sat_stat       = "satisfiable";
my $unsat_stat     = "unsatisfiable";
my $undecided_stat = "undecided";
my $outoftime_stat = "out of time";
my $outofmem_stat  = "out of mem";
my $error_stat     = "error";

############################################
# Options: defaults etc.
############################################
# string parameter for getopts; contains all admissible options,
# suffixed with ':' for options with arguments
my $option_names = 'fvqcrd:t:s:op:w:xC:';
# define default values
my %options = (c => 0,		  # don't continue on failure
	       r => 0,		  # don't clean up when proof incorrect
	       f => 0,		  # don't overwrite working directories
	       d => "_SubProofs", # working directory suffix
	       t => 3,		  # time limit for prover
	       v => 0,		  # not verbose
	       s => ".dfg",	  # suffix of generated proof files
	       q => 0,		  # not quiet
	       o => 0,		  # don't use SPASS as prover
	       x => 0,		  # no debugging infos
	       C => "SPASS" );	  # path of SPASS binary

# synonyms for options
my $quiet;
my $DFGCONVERTER;

# suffixes of converted files
my $conv_suffix = ".conv";
# SPASS suffix
my $spass_suffix = ".cnf";

################################
# Type of prover. Used to
# select appropriate subroutines
# for calling prover, converter etc.
#
# Values: "otter", "spass", "dfg".
# Set by SetOptions.
################################
my $prover_type = "";

################################
# Paths of prover and converters.
#
# The converter changes dfg format files
# into input files for prover.
#
# These vars are set by SetOptions.
#
# If @Converters is (), no
# converter has been specified.
#
################################
my $PROVER     = "";
my @Converters = ();


###################################################
# MAIN
###################################################

$|=1;				# set linewise buffering
$SIG{INT}  = \&catchint;	# set up interrupt handler
$SIG{TERM} = \&catchint;
&SetOptions($option_names);	# read options

###################################################
# Generate name of working directory from filename
###################################################
my ($fn_root, $in_file);

if (@ARGV > 0) {
  $in_file = $ARGV[0];
  if (!-e $in_file) {
    die "$in_file: No such file.\n";
  }
  
  # extract name root (without .extension, without path)
  # pattern: match arbitrary sequence of 'name/', then any sequence
  # of characters until '.' is reached (or end of expression)
  $in_file =~ /(.*\/)*([^\.]*)/;
  $fn_root = $2;
} else {
  &printoptions;
  die "\n";
}

my $wd = $fn_root.$options{'d'};

###################################################
# Create working directory
###################################################

if ($options{'f'} && -e $wd) {
  rmtree($wd);
}

if (-e $wd) {
  if ($options{'f'}) {
    die "\nFormer working directory $wd could not be removed.\n";
  } else {
    my $dcnt = 0;
    my $td = $wd;
    while (-e $td) {
      $dcnt++;
      $td = $wd.$dcnt;
    }
    $wd = $td;
  }
}

$wd = $wd."/";
if (!mkdir($wd, 0755)) {	# "rwxr-xr-x"
  die "\n Failed to make working directory $wd.\n$!\n";
}

###################################################
# Print program paths of:
# otter, dfg2otter, pgen
#
# This is done so lately to catch other errors before
###################################################

if (!$quiet) {
  &printpaths;
}

###################################################
# Call proof generator, get subproof tasks
###################################################

my @gen = Execute("$PGEN -q -d $wd -t $options{'t'} -s $options{'s'} $in_file");
if ($options{'x'}) {
  print "pgen returns: @gen";
}

# if proof generator failed to return anything, stop
# (this is probably a serious error)

if (!@gen) {
  &cleanup();
  die "Proof generator returned nothing on input file '$in_file'.\n";
}

# otherwise check output

if (grep(/$PGEN_FAILMSG/, @gen)) {
  &cleanup();
  print "Proof generator failed and returned:\n", @gen;
  die "\n$PCS_INVALIDMSG\n";
}

if (!grep/$PGEN_OKMSG/, @gen) {
  &cleanup();
  print "Cannot parse result of proof generator.";
  
  # if proofchecker result has already been printed
  # due to very verbose flag, don't print again
  print ":\n", @gen, "\n";
  
  die "\n";
}

###################################################
# MAIN LOOP: check all subproofs in the directory $wd
###################################################

my $proof_found       = 1;	# true as long as SPASS terminates with proof
my $proofs_found      = 0;	# number of proofs found so far
my $completions_found = 0;	# number of completions found so far
my $proof_num         = 0;      # number of proof tasks to check
my ($subproof, $conv, @res, $status);

# first count the number of proof files
opendir(DIR, $wd) or die "opendir $wd: $!\n";
while (defined ($subproof = readdir(DIR))) {
  if ($subproof =~ /$options{'s'}$/) {
    $proof_num++;
  }
}
rewinddir(DIR);  # reset the position within the subproof directory

# print comment
if ($options{'v'})  {
  print "\nChecking $proof_num proof steps with a maximum of ",$options{'t'}," seconds per step.\n";
}


# go while: 1) there are still subproofs and
#           2) either a proof has been found or
#              the 'continue option' $options{'c'} is active
while ($proof_found || $options{'c'}) {
  $subproof = readdir(DIR);
  last if !defined $subproof;
  next if $subproof !~ /$options{'s'}$/;
  $subproof = $wd . $subproof;   # add the directory to the filename

  # comment
  if ($options{'v'}) {
    print "\n   checking file $subproof: ";
  }
  
  ## create conversion file, if converter
  ## has been specified
  if (@Converters) {
    $conv = &convert($subproof);
  } else {
    $conv = $subproof;
  }
  
  ## call prover on file
  @res = &callprover($conv);
  
  ## extract status from prover output
  $status = &evalresult(@res);
  
  if ($status eq $error_stat) {
    die "\nProver does not terminate with proper exit message on file '$conv'.\nKeeping temporaries:\n@TOREMOVE\nfor debugging.\n";
  }
  
  ## remove temporaries
  &remove_tmps;
  
  
  if ($status eq $unsat_stat) {
    $proof_found = 1;
  } else {
    $proof_found = 0;
  }
  
  ## print comment
  if ($options{'v'}) {
    if ($status eq $unsat_stat) {
      print "Unsatisfiable.";
    } elsif ($status eq $sat_stat) {
      print "SATISFIABLE.";
    } elsif ($status eq $outofmem_stat) {
      print "Ran out of memory.";
    } elsif ($status eq $outoftime_stat) {
      print "Ran out of time.";
    } else {
      print "Not decided.";
    }
  }
  
  ## statistics
  if ($status eq $unsat_stat) {
    $proofs_found++;
  }
  if ($status eq $sat_stat) {
    $completions_found++;
  }
}
closedir(DIR) or die "closedir $wd: $!";

###################################################
#  Print result
###################################################

if ($options{'v'}) {
  print "\n\n";
}

if ($proofs_found - $proof_num == 0) {
  # Proof has been verified
  print "$PCS_VALIDMSG\n";
  rmtree($wd);
} else {
  # Proof could not be verified or has been falsified
  if ($completions_found)  {
    print "$PCS_INVALIDMSG\n\n" ;
  } else {
    print "Correctness of proof not decided:\n\n";
  }
  
  print "  Number of proof steps: $proof_num\n";
  print "  Correct proof steps  : $proofs_found\n";
  print "  Incorrect proof steps: ", $completions_found;
  print "\n  Undecided proof steps: ", $proof_num-$proofs_found-$completions_found, "\n";
  
  if (!$options{'r'}) {
    print "\nInput files are in ", $wd, "\n";
  }
}

&cleanup();

####################################################
# MAIN END
####################################################

####################################################
# EFFECTS: Clean up temporary files and working dir
####################################################
sub cleanup {
  &remove_tmps();
  
  if ($options{'r'}) {
    rmtree($wd);
  }
}

####################################################
# EFFECTS: removes all temporary file in @TOREMOVE
####################################################
sub remove_tmps {
  unlink(@TOREMOVE);
  @TOREMOVE = ();
}

####################################################
# EFFECTS: print paths of all used programs
####################################################
sub printpaths {
  my ($tmp, $converter, @converterpaths);
  
  print $sep;
  
  $tmp = safewhich($PROVER);
  if ($tmp eq "") {
    die "can't access prover by '$PROVER'\n";
  } else {
    print "Prover   : ";
    print "$tmp";
  }
  
  # gather paths of converters
  
  # print "Converters: @Converters\n";
  @converterpaths = ();
  foreach $converter (@Converters) {
    # print "converter: $converter\n";
    $tmp = safewhich($converter);
    if ($tmp eq "") {
      die "can't access converter by '$converter'\n";
    } else {
      unshift(@converterpaths, $converter);
    }
  }
  if (@Converters) {
    print "Converters: ";
    foreach $converter (@converterpaths) {
      print "$converter ";
    }
    print "\n";
  }
  
  # generator of proof tasks
  $tmp = safewhich($PGEN);
  if ($tmp eq "") {
    die "can't access file generator by '$PGEN'\n";
  } else {
    print "Generator: ";
    print "$tmp";
  }
  print $sep;
}

####################################################
# INPUT  : A file name
# EFFECTS: Calls prover on file
# RETURNS: Prover output
####################################################
sub callprover {
  my ($file) = @_;
  
  if ($prover_type eq "otter") {
    return Execute("$OTTER < $file 2>/dev/null");
  }
  if ($prover_type eq "spass") {
    return Execute("$SPASS $SPASS_flags -TimeLimit=$options{'t'} $file");
  }
  if ($prover_type eq "dfg") {
    return Execute("$DFGPROVER $file");
  }
}

####################################################
# INPUT  : The output of a prover
# RETURNS: The evaluation of this output
####################################################
sub evalresult {
  my (@res) = @_;
  
  if ($prover_type eq "otter") {
    return(eval_OTTER_result(@res));
  }
  if ($prover_type eq "spass") {
    return(eval_SPASS_result(@res));
  }
  if ($prover_type eq "dfg") {
    return(eval_DFGPROVER_result(@res));
  }
}

####################################################
# INPUT  : A SPASS result output
# RETURNS: The evaluation of the output
####################################################
sub eval_SPASS_result {
  my (@res) = @_;
  
  if ($options{'x'}) {
    print "SPASS returns:\n@res\n";
  }
  
  if (grep(/Proof found/, @res)) {
    return($unsat_stat);
  } elsif (grep(/Completion found/, @res)) {
    return($sat_stat);
  } elsif (grep(/out of time/, @res)) {
    return($outoftime_stat);
  } elsif (grep(/SPASS terminated by Memory Flag/, @res)) {
    return($outofmem_stat);
  } else {
    return($undecided_stat);
  }
}

##########################################################
# INPUT : A dfg prover output
# OUTPUT: The evaluation of this output
##########################################################
sub eval_DFGPROVER_result {
  my (@res) = @_;
  
  return(eval_SPASS_result(@res));
}

##########################################################
# INPUT : An Otter output
# OUTPUT: Its evaluation
#
# OTTER distinguishes search stop due to
#
# 1. sos empty   (Pattern: 'Search stopped because sos empty')
# 2. Proof found (Pattern: '--- PROOF ---')
# 3. other stop conditions:
#          max_given, max_gen, max_kept, max_seconds, max_mem
#          (Pattern: 'Search stopped (.*) {condition} option')
#
# NOTE: 'sos empty' is taken as sign for satisfiability.
#       This is interpretation is permissible only if otter has chosen
#       a complete set of inference rules in 'auto'-mode!
#
###########################################################
sub eval_OTTER_result {
  my (@res) = @_;
  
  if (grep(/Search stopped because sos empty/, @res)) {
    return($sat_stat);
  } elsif (grep(/--- PROOF ---/, @res)) {
    return($unsat_stat);
  } elsif (grep(/Search stopped by/, @res)) {
    return($undecided_stat);
  } else {
    return($error_stat);
  }
}

####################################################
# INPUT : A DFG problem file
# OUTPUT: A corresponding otter file
####################################################
sub DFG_to_OTTER {
  my ($file) = @_;
  my ($spass_in, $otter_in, $pfile, @conv_res);
  
  $pfile = my_filename($file);
  # .frm to .cnf format
  $spass_in = new_tmpfile_name($TMPDIR, $pfile.$spass_suffix);
  @conv_res = Execute("$SPASS -CNFFEqR=0 -Flotter $file $spass_in");
  
  if (!-e $spass_in) {
    &cleanup();
    die "Error: SPASS failed to convert file '$file'.\n";
  } else {
    unshift(@TOREMOVE, $spass_in);
  }
  
  # SPASS to otter format
  $otter_in = new_tmpfile_name($TMPDIR, $pfile.$conv_suffix);
  @conv_res = Execute("$DFG2OTTER_PL -t $options{'t'} $spass_in $otter_in 2>&1");
  if ($options{'x'}) {
    system("more $otter_in");
  }
  
  if (!-e $otter_in || @conv_res) {
    &cleanup();
    die "\nError: converter $DFG2OTTER_PL failed on SPASS conversion\nof file '$file'.\nReturned:\n@conv_res\n";
  }
  else {
    unshift(@TOREMOVE, $otter_in);
  }
  return($otter_in);
}

####################################################
# EFFECTS: Extract options from ARGV and set
#          the appropriate variables
####################################################
sub SetOptions {
  my ($option_names) = @_;
  
  getopts($option_names, \%options);
  
  if (defined $options{'C'}) {
    $SPASS = $options{'C'};
  } else {
    $options{'C'} = $SPASS;
  }
  
  # translate some options into meaningful variable names
  $quiet = $options{'q'};
  
  #######################################
  # set $prover_type, $PROVER, @Converters
  #######################################
  # default: otter
  $prover_type = "otter";
  $PROVER = $OTTER;
  @Converters = ($DFG2OTTER_PL); # This is just for output
  
  # If -o is defined, take SPASS
  if ($options{'o'}) {
    if (defined $options{'p'}) {
      print "-o option overrides -p option.\n";
    }
    if (defined $options{'w'}) {
      print "-o option overrides -w option.\n";
    }
    $prover_type = "spass";
    $PROVER = $SPASS;
    @Converters = ();
  } elsif (defined $options{'w'} && !defined $options{'p'}) {
    # if DFG converter is specified, then DFG Prover must
    # be specified. (If it is not, no conversion is done).
    die "Converter, but no prover specified.\n";
  } elsif (defined $options{'p'}) {
    # use user-specified prover
    $prover_type = "dfg";
    $PROVER = $options{'p'};
    $DFGPROVER = $PROVER;
    if (defined $options{'w'}) {
      @Converters = ($options{'w'});
    }
    $DFGCONVERTER = $options{'w'};
  }
}

####################################################
# INPUT : A file path
# OUTPUT: The file name
####################################################
sub my_filename {
  my ($path) = @_;
  
  $path =~ m/(.*\/)*(.*)/;
  return($2);
}

####################################################
# INPUT : A command name
# OUTPUT: The full path of this command
####################################################
sub safewhich {
  my ($command) = @_;
  my (@res, $which);
  
  if (-e "/usr/bin/which") {
    $which = "/usr/bin/which";
  } else {
    $which = "which";
  }
  @res = `$which $command`;
  
  if ($? != 0) {
    print STDERR "Error: Strange result for \"$which $command\"\n";
  }
  if (@res != 1) {
    return("");
  }
  
  if (($res[0] =~ /command not found/) ||
      ($res[0] =~ /no\s.*in/)) {
    return("");
  }
  
  return($res[0]);
}

####################################################
# INPUT  : A file
# EFFECTS: Generated a new file which is in a format
#          suitable for the chosen prover
####################################################
sub convert {
  my ($file) = @_;
  
  if ($prover_type eq "otter")  {
    return(DFG_to_OTTER($file));
  }
  if ($prover_type eq "spass") {
    return($file);
  }
  if ($prover_type eq "dfg") {
    return($file);
  }
}

####################################################
# INPUT  : A signal name
# EFFECTS: Remove temporaries and reports interrupt
####################################################
sub catchint {
  my $signame = shift;
  &cleanup();			# remove tmp files
  if ($options{'r'}) {
    die "\n\npcs:caught signal $signame. Cleaning up.\n"; }
  else {
    die "\n\npcs:caught signal $signame. Cleaning up temporaries.\nKeeping working directory $wd.\n";
  }
}

####################################################
# EFFECTS: Print out all options
####################################################
sub printoptions {
  print "Usage:\n";
  print " pcs [options] filename\n";
  print "Options:\n";
  
  print " -c: continue on failure to prove proof line correct (default false)\n";
  print " -r: clean up at end (default false)\n";
  print " -f: (force) delete and re-create working directory if it exists\n";
  
  print " -d (name): suffix of created working directory (default _SubProofs)\n";
  
  print " -t (limit): time limit for proof attempt (default 3 (seconds)) \n";
  print " -v: print out some comments while proofs are checked\n";
  
  print " -s (suffix): suffix of generated proof files (handed over to pgen) \n";
  print " -q: quiet: do not print program paths\n";
  print " -o: use SPASS for proof checks (instead of otter)\n";
  print " -p (path): path of foreign prover \n";
  print " -w (path): path of foreign converter\n";
}

####################################################
# Start of filehandling stuff
####################################################


###################################################
# INPUT  : A filename <name>.<ext>
# RETURNS: The tupel (<name>, <ext>)
###################################################
sub split_by_ext {
  my ($name) = @_;
  
  $name =~ m/(.*?)\.(.*)/;
  if (defined($1)) {
    return($1, $2);
  }
  # return name if there is no extension
  return($name, "");
}


###################################################
# INPUT  : A directory path <dir>, a filename <pfile>
# RETURNS: <dir><pfile>  if <dir> ends with a backslash
#          <dir>/<pfile> otherwise
###################################################
sub makepath {
  my ($Dir, $pfile) = @_;
  
  if ($Dir =~ m/.*\/$/) {
    return($Dir.$pfile);
  }
  else {
    return($Dir.'/'.$pfile);
  }
}


###############################################
# INPUT  : A file name <pfile>, a directory <tmpdir>
# RETURNS: A file path which does not name an
#          existing file. The name is based on <pfile>
#          and located in <tmpdir>
###############################################
sub new_tmpfile_name {
  my ($tmpdir, $pfile) = @_;	# $pfile is pure filename, without path
  my ($wf, $fcnt);
  my ($name, $ext);		# for splitting filenames
  
  
  ($name, $ext) = split_by_ext($pfile);
  $fcnt = 0;
  $wf = makepath($tmpdir, $pfile);
  while (-e $wf) {
    $fcnt++;
    $wf = makepath($tmpdir, $name.$fcnt.".".$ext);
  }
  
  return($wf);
}


###############################################
# INPUT  : A string containing a command that
#          can be executed in a shell.
# RETURNS: The output of the command to stdout.
# EFFECT:  The command is printed to stdout if
#          the option '-x' is set.
###############################################
sub Execute {
  my ($cmd) = @_;
  my @result;
  
  if ($options{'x'}) {
    print "\n$cmd\n";
  }
  @result = `$cmd`;
  return @result;
}

