#!/usr/bin/perl
use FileHandle; 
use IPC::Open2; 
use File::Path;
use File::Spec;
use File::Basename;
use IO::Handle qw( );

$EKRHDIR = dirname(dirname(File::Spec->rel2abs(__FILE__)));

# Set to 0 to stop debug output.
$debug = 0;

# Hands off from here.
$TPTPDIR = $ENV{'TPTP'};
$| = 1;
$readycnt=0;

# initialize with args
$ltb_batch_file = @ARGV[0];
$total_time_limit = @ARGV[1];
$start_time = time();
$counter=0;

$default_selection_options = "[method=sine,queries=cq,tolerance=1.0,persistent=true]";

sub get_time_left{
	$time_left=$total_time_limit - (time() - $start_time);
	return($time_left)
}

# General strategy:
# - get full-time-limit FTL from command line arg
# Then for each batch:
# - get batch-time-limit BTL: problem time limit PTL multiplied with number of problems;
# - read and preprocess the shared include-files of the batch, allow BTL for this as actual problem handling may be fast;
# - then process problems one by one, allow PTL for each, but only attempt a problem if current time + PTL is within FTL 

# ensures that path names are in a proper form for E-KRHyper
sub make_ekrh_compatible_path {
	my $path=@_[0];
	my $prefix=@_[1];
	
# Remove wrapping 's.	
	$path=~s/^\'(.*)\'$/\1/;

# Add prefix if path is relative.			
	if (File::Spec->file_name_is_absolute($path))
		{}
	else
		{$path=$prefix."/".$path};

# Add wrapping 's.
	$path="'".$path."'";
	$path
}
	
# turn numerical argument into a float form for E-KRHyper	
sub make_ekrh_compatible_float {
	my $number=@_[0];
	my $number_float=$number;
	$number_float=~s/^(\d+)$/$1.0/;	
	$number_float=~s/^(\d+)\.(\d).*/$1.$2/;
	$number_float
}
	
# wait for ekrh output and check whether it contains timout or memoryout interrupts	
sub ekrh_success {
	my $reader=@_[0];
	my $writer=@_[1];
	my $success=1;
	my $timeout=0;
	$readycnt+=1;

	print $writer "#(write('%EKRHREADY".$readycnt."%~n')).\n";
	my $ekrh_output = "";
	while($ekrh_output!~/^(\%EKRHREADY$readycnt\%|.*EKRH-Warning\: Limit exceeded)/ms)
		{$ekrh_line=<$reader>;
		if($debug){
			print "ES1: ".$ekrh_line
		};
		$ekrh_output .= $ekrh_line};
	if($ekrh_output=~/SZS status Timeout/s)
		{$timeout=1};
# timeout or memoryout occurred, clear ekrh-command-block and return failure		
	if($ekrh_output=~/EKRH-Warning\: Limit exceeded/s)
		{$success=0;
		$ekrh_output = "";
		$readycnt+=1;
		 print $writer "#(clear_limit_block).\n";
		 print $writer "#(write('%EKRHREADY".$readycnt."%~n')).\n";
		 while($ekrh_output!~/^\%EKRHREADY$readycnt\%/ms)
			{$ekrh_line=<$reader>;
			if($debug){
				print "ES2: ".$ekrh_line
			};
			$ekrh_output .= $ekrh_line};
		};
	return($success, $timeout, $ekrh_output)
}
	
# print result for a problem
sub print_result {
	my $result_file=@_[0];
	my $result=@_[1];

	my ($file, $path) = fileparse($result_file);
	
	if(!(-d $path)){
		mkpath($path);
	};
	
	open RESULTFILE, ">$result_file" or die "% Cannot write to $result_file, aborting.\n";
	print RESULTFILE $result."\n";
	close RESULTFILE;
	
	print $result."\n";
}
	
# Process one 'run' command and evaluate its result. 		
sub single_run {
	my $includes_loaded=@_[0];
	my $includes_required=@_[1];
	my $algorithm=@_[2];
	my $complete=@_[3];
	my $reader=@_[4];
	my $writer=@_[5];
	my $compute_answer=@_[6];
	my $problem=@_[7];
	my $result="% SZS status GaveUp"; # default result: failure
	my $run_complete=0;
	my $timed_out=0;
	
	$problem=~/^\'(.+)\'$/;
	my $perl_problem=$1;
	my $problem_exists=1;
	if (!(-e $perl_problem)){
		print "% Warning: cannot find ".$perl_problem."\n";
		$problem_exists=0;
		$run_complete=1;print "RC2\n";
	};

# $includes_loaded = true iff all include-files have been loaded (or there were not any to load)	
	if($problem_exists && $includes_loaded){ 
	
		print $writer "#(save_input_state).\n";
		if($includes_required){ # only necessary if there really are includes, i.e. at least one
			print $writer "#(begin_nonpersistent_queries).\n";
		}
		else{	# Otherwise load the whole problem as selectable.
			print $writer "#(begin_selected_input(".$default_selection_options.")).\n";
		};		
		#print "LOADING PROBLEM: #(load(".$problem.")).\n";
		print $writer "#(load(".$problem.")).\n";
		($problem_loaded, $timeout, $ekrh_output)=&ekrh_success($reader, $writer);
		
		# Timeout overrides everything
		if($timeout){$timed_out=1};
	
		if($problem_loaded && $includes_required && (not $timed_out)){ # only necessary if there really are includes, i.e. at least one
			print $writer "#(end_nonpersistent_queries).\n";
			print $writer "#(select_from_input_alg([method=".$algorithm."])).\n";
		}
		else{
			if ($problem_loaded && (not $timed_out)){
				print $writer "#(end_persistent_selected_input).\n";
				print $writer "#(select_from_input_alg([method=".$algorithm."])).\n";
			}
		};
		($ready_for_run, $timeout, $ekrh_output)=&ekrh_success($reader, $writer);
		if($timeout){$timed_out=1};

		if($problem_loaded && $ready_for_run && (not $timed_out)){	
			print $writer "#(run).\n";	
			if($compute_answer>0){
				print $writer "#(print_answer_units).\n";
			}
			($proof_found, $timeout, $ekrh_output)=&ekrh_success($reader, $writer);
			if($timeout && (not $proof_found)){$timed_out=1};
			if($proof_found){
				$run_complete=1;
				if($ekrh_output=~/SZS status Theorem/s){
					$result="% SZS status Theorem";
					if($ekrh_output=~/(\% SZS answers start Formulae.*\% SZS answers end Formulae)/s){
						$result.="\n".$1;
					};
					if($ekrh_output=~/(\% SZS answers Tuple .*)/){
						$result.="\n".$1;
					}
				}
#				else{
#					if($ekrh_output=~/SZS status (\w+)/){
#						$result.="\n% SZS status ".$1;
#					}
#				}
			}
		};
		print $writer "#(load_previous_input_state).\n";
		($loaded, $timeout, $ekrh_output)=&ekrh_success($reader, $writer);
		if($timeout){$timed_out=1};
	};
	return($run_complete, $timed_out, $result);
}	
	

# read the LTB-file
open LTB_BATCH_FILE, $ltb_batch_file or die "Cannot open $ltb_batch_file\n";
$ltb_batch_data="";
while(<LTB_BATCH_FILE>){
	$line=$_;
	chomp($line); # dos to unix...
	$line=~s/\s+/ /g; # normalize whitespace
	$line=~s/^ (.*)$/$1/; # remove leading and...
	$line=~s/^(.*) $/$1/; # ...trailing blanks
	$ltb_batch_data.=$line."\n";
}

@batches=($ltb_batch_data=~/(\% SZS start BatchConfiguration.*?\% SZS end BatchProblems)/gs);

foreach $batch(@batches){
# Parse each batch.
	$batch=~/output\.required ?(.*)/;
#	@output_required=split(/ /, $1);
	$output_specs=$1;
	
	$batch=~/output\.desired ?(.*)/;
#	@output_desired=split(/ /, $1);	
	$output_specs.=" ".$1;

# Assurance is always required, there is no need for a flag.	
# If Answer-output is required or desired, compute and print answers in addition to assurance.	
	if ($output_specs=~/Answer/i)
		{$compute_answer=1}
	else
		{$compute_answer=0};
	
	$batch=~/limit\.time\.problem\.wc (\d+)/;
	$time_limit_per_problem=$1;	
		
	$batch=~/\% SZS start BatchIncludes(.*?)\% SZS end BatchIncludes/s;
	$preliminary_includes=$1;
	$includes=();
	@preliminary_includes=($preliminary_includes=~/include\((.+?)\)\./gs);
	foreach $preliminary_include(@preliminary_includes){
		$ekrh_include=&make_ekrh_compatible_path($preliminary_include, $TPTPDIR);
		$ekrh_include=~/^\'(.+)\'$/;
		$perl_include=$1;
		if (!(-e $perl_include)){
			print "% Warning: cannot find ".$perl_include."\n"
		}
		else{
			push(@includes, $ekrh_include)
		}
	};
	$includes_required=(scalar(@includes)>0);
	
	$batch=~/\% SZS start BatchProblems(.*?)\% SZS end BatchProblems/s;
	$problems_and_outputs=$1; 
	@problems_and_outputs=($problems_and_outputs=~/(\S+? \S+?)\s*\n/gs);
	
# A sub_batch is the set of problems in a batch which use the shared include files.
# The sub_batches array lists all sub_batches.
# If there are any shared include files, then sub_batches contains only one element,
# which is the list of all problems in the batch.
# If there are no shared include files, then each element of sub_batches is a list
# containing only one problem of the batch.
# The prover is restarted for each sub_batch.	
	@sub_batches=();
	if($includes_required){
		push @sub_batches, [@problems_and_outputs]
	}
	else{
		foreach $problem_and_output(@problems_and_outputs){
			push(@sub_batches, [$problem_and_output])	
		}	
	};

	if($time_limit_per_problem==0){$time_limit_per_problem=$total_time_limit / scalar(@problems_and_outputs)};
	$time_limit_per_problem_float=&make_ekrh_compatible_float($time_limit_per_problem);	
	
# time limit for the whole batch	
	$time_limit_for_batch = scalar(@problems_and_outputs) * $time_limit_per_problem;
	$time_limit_for_batch_float=&make_ekrh_compatible_float($time_limit_for_batch);
	
# time limit for reading the include-files and computing their dependencies	
# (Maybe come up with something smarter here, but at the current point the includes MUST be loaded, so there is no point in even
#  attempting one of the problems before this is done.)
	$time_limit_for_includes=$time_limit_for_batch;  
	$time_limit_for_includes_float=&make_ekrh_compatible_float($time_limit_for_includes);

	
	
	
# Process the batch problems.

foreach $sub_batch(@sub_batches){
# First, start E-KRHyper with a bidirectional pipe.
	local (*Reader, *Writer); 
	$config="/casc/config_ltb.tme";
	if($debug){
		$config="/casc/config_ltb_debug.tme";
	};
	$ekrh_pid = open2(\*Reader, \*Writer, $EKRHDIR."/../../bin/ekrh ".$EKRHDIR.$config." -"); 

#local $SIG{PIPE} =
#	sub {$restart = 1};	
	Writer->autoflush(1); 

# Flush E-KRHyper's initial output.
	$ekrh_output = "";
	while($ekrh_output!~/\%EKRHREADY\%/s)
		{$line = <Reader>;
		 if($debug){
			print $line
		};
		$ekrh_output .= $line};

# batch-specific settings		
	if($compute_answer>0){
# produce TPTP answers	
		print Writer "#(set_parameter(tptp_qa, 2)).\n";
# use tuple syntax for answers
		print Writer "#(set_parameter(tptp_qa_answer_type, 1)).\n";
	};
		
# Load the 'includes' as a static ontology.
	$includes_loaded=0;
	if($includes_required){
		print Writer "#(start_wallclock_timer(".$time_limit_for_includes_float.")).\n";
		print Writer "#(begin_selected_input(".$default_selection_options.")).\n";
		foreach $include(@includes){
			$include=&make_ekrh_compatible_path($include, $TPTPDIR);
			print Writer "#(load(".$include.")).\n";
		};
		print Writer "#(end_persistent_selected_input).\n";
		print Writer "#(stop_wallclock_timer).\n";
		($includes_loaded, $timeout, $ekrh_output)=&ekrh_success(Reader, Writer);
	}
	else{
		$includes_loaded=1;
	};

	
# Process the queries/problems one by one.		
	foreach $problem_and_output(@$sub_batch){
		if($problem_and_output=~/^(\S+) (\S+)$/){
			$original_problem=$1;
			$output=$2;
		}
		else{
			die "Cannot process ".$problem_and_output."\n";
		};
		$problem=&make_ekrh_compatible_path($original_problem, $TPTPDIR);
		print "% SZS status Started for ".$original_problem."\n";
		
#		print "#(start_wallclock_timer(".$time_limit_per_problem_float.")).\n";
		print Writer "#(start_wallclock_timer(".$time_limit_per_problem_float.")).\n";
	
		($run_complete, $timed_out, $result)=
			&single_run($includes_loaded, $includes_required, "sine", 0, Reader, Writer, $compute_answer, $problem);

		if ($run_complete && (not $timed_out)){
			if ($result!~/SZS status Theorem/s){
# No timeout, but no theorem result either - try a different selection.	
				($run_complete, $timed_out, $result)=
					&single_run($includes_loaded, $includes_required, "ekrh", 0, Reader, Writer, $compute_answer, $problem);
#				if ($run_complete && (not $timed_out)){
#					if ($result!~/SZS status Theorem/s){
## Again no timeout and no theorem, try all clauses.					
#						($run_complete, $timed_out, $result)=
#							&single_run($includes_loaded, $includes_required, "none", 1, Reader, Writer, $compute_answer, $problem);
## Nothing to do here, result is final.	If the run was not complete, the result will be 'GaveUp'. Otherwise the result will be sound due to completeness of final run.					
#					}
#				}
			}
		};
		
#		($mu, $ekrh_output)=&ekrh_success(Reader, Writer);
		$result.=" for ".$original_problem;
		print Writer "#(stop_wallclock_timer).\n";
		&print_result($output, $result);
		print "% SZS status Ended for ".$original_problem."\n";
		
	}
	
# Batch done, close E-KRHyper and pipe.
	print Writer "#(exit).\n";
#	waitpid($ekrh_pid, 0);
}
}