#!/bin/perl -w

use strict "vars";
#-----------------------------------------------------------------------------
my $EGround = "/home/tptp/Systems/GrAnDe---1.0/eground";
my $ECommandFormat = "$EGround --tptp-in --dimacs --silent --resources-info --split-tries=100 --memory-limit=400 --soft-cpu-limit=%d --add-one-instance --constraints %s";
my $ECPUFraction = 0.75;

my $DecideDir = "/home/tptp/Systems/ZChaff---2001.2.17";
my $Decide = "$DecideDir/zchaff.2001.2.17.solaris";
my $DecideCommandFormat = "$Decide %s";

my $TempFile = "/tmp/PizEAndDecide$$";
my $GlobalInterrupted;
#-----------------------------------------------------------------------------
sub InterruptHandle {
    my ($Signal) = @_;

    $GlobalInterrupted = 1;
}
#-----------------------------------------------------------------------------
    my $FromEHandle = "FromEHandle";
    my $ToFileHandle = "ToFileHandle";
    my $FromDecideHandle = "FromDecideHandle";
    my $ECommand;
    my $DecideCommand;
    my $Line;
    my $EStatusLine;
    my $DecideDone;
    my $ETime;

    if (scalar(@ARGV) != 2) {
        die("Usage: And <problem file> <time limit>\n");
    }

    $GlobalInterrupted = 0;
    $SIG{'QUIT'} = 'InterruptHandle';
    $SIG{'XCPU'} = 'InterruptHandle';

    $ETime = $ECPUFraction*$ARGV[1];
    $ETime = int($ECPUFraction*$ARGV[1]);
    if ($ETime == 0) {
        $ETime = 1;
    }
    print("$ETime of $ARGV[1] seconds allocated to grounding\n");

    $ECommand = sprintf($ECommandFormat,$ETime,$ARGV[0]);
    $DecideCommand = sprintf($DecideCommandFormat,$TempFile);

    open($FromEHandle,"$ECommand|") or die("ERROR: Cannot start $ECommand\n");
    open($ToFileHandle,">$TempFile") or die("ERROR: Cannot open $TempFile\n");

#----Echo from eground to Decide, except last line.
    while (!$GlobalInterrupted && defined($Line = <$FromEHandle>) && 
$Line !~ /^#/) {
        if ($Line =~ /^#/) {
            print("$Line");
        }
        if ($Line !~ /^c/ && $Line !~ /^ *$/) {
            print($ToFileHandle $Line);
        }
    }

    $DecideDone = 0;
    if ($Line !~ /^#/) {
        print("ERROR: Last line does not provide eground status\n");
    } else {
        $EStatusLine = $Line;
        chomp($EStatusLine);
        print("Grounding status: $EStatusLine\n");

#----Flush rest from eground
    while (!$GlobalInterrupted && defined($Line = <$FromEHandle>)) {
        if ($Line =~ /^#/) {
            print("$Line");
        }
    }
    close($FromEHandle);
    close($ToFileHandle);

#DEBUG print("Starting Decide on $TempFile\n");
        open($FromDecideHandle,"$Decide $TempFile|") or 
die("ERROR: Cannot start Decide\n");
#----Watch output from Decide
        while (!$DecideDone && defined($Line = <$FromDecideHandle>)) {
#DEBUG print(" ZChaff says: $Line");
            if ($Line =~ /Instance unsatisfiable/) {
                print("$Line");
                $DecideDone = 1;
            }
            if ($Line =~ /Instance satisfiable/) {
                if ($EStatusLine =~ /Full and complete proof state written/) {
                    print($Line);
                } else {
                    print("Decide found a model of an incomplete grounding\n");
                }
                $DecideDone = 1;
            }
            if ($Line =~ /The file is empty/) {
                print("ERROR: $Line");
                $DecideDone = 1;
            }
        }

        close($FromDecideHandle);
    }

    system("rm -f $TempFile");

    if (!$DecideDone) {
        print("ERROR: Decide did not report anything\n");
    }

#-----------------------------------------------------------------------------