1#!/usr/bin/perl
    2use warnings;
    3use strict;
    4#
    5#    Copyright (C) 2004,2005,2006,2007,2008,2009
    6#    Patrick Blackburn, Johan Bos, Eric Cow and Sebastian Hinderer
    7
    8# parameterisation of the programs
    9my $tempdir = $ARGV[0];
   10my $timelimit = $ARGV[1];
   11my $mindomsize = $ARGV[2];
   12my $maxdomsize = $ARGV[3];
   13my $engines = $ARGV[4];
   14
   15# for keeping track of running programs 
   16my %pids = (); 
   17
   18# where to store results
   19my $model = "";
   20my $winner = "";
   21
   22# CPU limited time
   23my $CPULimit = "";
   24if ($timelimit > 0) {
   25    $CPULimit = "ext/bin/CPULimitedRun $timelimit";
   26} else { $timelimit = 100; }
   27
   28# how to run programs
   29my %programs = ( 
   30 otter    => "ext/bin/otter",
   31 bliksem  => "$CPULimit ext/bin/bliksem",
   32 vampire  => "ext/bin/vampire -t $timelimit -m 500 < $tempdir/vampire.in",
   33 zenon    => "ext/bin/zenon -p0 -itptp -",
   34 mace     => "$CPULimit ext/bin/mace -n$mindomsize -N$maxdomsize -P",
   35 paradox  => "$CPULimit ext/bin/paradox $tempdir/paradox.in --model"
   36);
   37
   38# run any requested processes
   39foreach my $p (keys %programs) {
   40  if ($engines =~ /$p/) {
   41    my $childPid = fork;
   42    if ($childPid==0) {
   43      # Redirect stdin, stdout and stderr
   44      open(STDIN, "< $tempdir/$p.in") or die "Can't redirect stdin to $tempdir/$p.in: $!";
   45      open(STDOUT, "> $tempdir/$p.out") or die "Can't redirect stdout to $tempdir/$p.out: $!";
   46      open(STDERR, "> /dev/null") or die "Can't redirect stderr to /dev/null: $!";
   47      # Run the inference engine
   48      exec $programs{$p}; 
   49    }
   50    # the parent process keeps track of the child process
   51    $pids{$childPid} = $p;
   52  }
   53}
   54
   55# continue looping while there are still processes running
   56# and none of them has found a result
   57while( (keys %pids) > 0) {
   58  # Waits for a process to terminate
   59  my $pid = wait;
   60  if ($pid==-1) {
   61    last;
   62  }
   63
   64  if ($pids{$pid} eq "mace") {
   65    my $readmacemodel = 0;
   66    open(OUTPUT,"$tempdir/mace.out");
   67    while (<OUTPUT>) {
   68      if (/end_of_model/) {
   69        $winner = "mace";
   70        $readmacemodel = 0;
   71      } elsif ($readmacemodel) {
   72        $model = "$model$_";
   73        $model =~ s/\$(.*?)\,/$1\,/;
   74      } elsif (/======================= Model/) {
   75        $readmacemodel = 1;
   76      }
   77    }
   78    close(OUTPUT);
   79    delete $pids{$pid};
   80    if ($winner ne "") { last; }
   81  }
   82
   83  elsif ($pids{$pid} eq "paradox") {
   84    my $readparadoxmodel = 0;
   85    open(OUTPUT,"$tempdir/paradox.out");
   86    while (<OUTPUT>) {
   87            if (/END MODEL/ && $readparadoxmodel == 1) {
   88               $model = "$model dummy\n]).\n";
   89	       $winner = "paradox";
   90	       $readparadoxmodel = 0;
   91            }
   92            elsif ($readparadoxmodel == 1) {
   93               s/<=>/:/;
   94               s/\$true/1,/;
   95               s/\$false/0,/;
   96               s/!/d/g;
   97               $model = "$model $_" if (/,$/);
   98            }
   99            elsif (/BEGIN MODEL/) {
  100               $model = "paradox([\n";
  101               $readparadoxmodel = 1;
  102            }
  103            elsif ($_ =~ /Contradiction/) {
  104               $model = "paradox([]).\n";
  105               $winner = "paradox";
  106               $readparadoxmodel = 0;
  107            }
  108    }
  109    close(OUTPUT);
  110    delete $pids{$pid};
  111    if ($winner ne "") { last; }
  112  }
  113
  114  elsif ($pids{$pid} eq "otter") {
  115    open(OUTPUT,"$tempdir/otter.out");
  116    while (<OUTPUT>) {
  117      if (/proof of the theorem/) {
  118        $winner = "otter";
  119      }
  120    }
  121    close(OUTPUT);
  122    delete $pids{$pid};
  123    if ($winner ne "") { last; }
  124  }
  125
  126  elsif ($pids{$pid} eq "bliksem") {
  127    open(OUTPUT,"$tempdir/bliksem.out");
  128    while (<OUTPUT>) {
  129      if (/found a proof/) {
  130        $winner = "bliksem";
  131      }
  132    }
  133    close(OUTPUT);
  134    delete $pids{$pid};
  135    if ($winner ne "") { last; }
  136  }
  137
  138  elsif ($pids{$pid} eq "vampire") {
  139    open(OUTPUT,"$tempdir/vampire.out");
  140    while (<OUTPUT>) {
  141      if (/Termination reason: Refutation/) {
  142#      if (/End of refutation /) {
  143        $winner = "vampire";
  144      }
  145    }
  146    close(OUTPUT);
  147    delete $pids{$pid};
  148    if ($winner ne "") { last; }
  149  }
  150
  151  elsif ($pids{$pid} eq "zenon") {
  152    open(OUTPUT,"$tempdir/zenon.out");
  153    while (<OUTPUT>) {
  154      if (/FOUND/) {
  155        $winner = "zenon";
  156      }
  157    }
  158    close(OUTPUT);
  159    delete $pids{$pid};
  160    if ($winner ne "") { last; }
  161  }
  162}
  163
  164# kill any remaining child processes (for example, any theorem
  165# provers or model builders which are still working)
  166foreach (keys %pids) {
  167  kill(15, $_);
  168}
  169
  170# write the results out to a file which will be read by application
  171open(OUTPUT,">$tempdir/tpmb.out");
  172if ($winner ne "") {
  173   my $details = "proof.\n";
  174   if ($model ne "") {
  175      $details = $model;
  176   }
  177   print OUTPUT $details;
  178   print OUTPUT "engine($winner).\n";
  179}
  180else {
  181   print OUTPUT "unknown.\n";
  182}
  183close(OUTPUT);
  184
  185exit 0;