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;