#!/bin/perl -w

use strict "vars";
use FileHandle;
use IPC::Open2;
#------------------------------------------------------------------------------
my $TPTPDirectory = "/home/tptp";

my $LibraryDirectory = "$TPTPDirectory/TPTP";
my $tptp2XCommand = "$LibraryDirectory/TPTP2X/tptp2X";
my $SystemOnTPTPCommand = "$TPTPDirectory/SystemExecution/SystemOnTPTP";

my $DefaultCPUTimeLimit  = 60;
my $TemporaryProblemFileName = "/tmp/RatifyProblem_$$";
#------------------------------------------------------------------------------
    my $InputHandle = "InputHandle";
    my $CPUTimeLimit;

    $CPUTimeLimit = $DefaultCPUTimeLimit;
    if (scalar(@ARGV) > 0 && $ARGV[0] =~ /^\d+$/) {
        $CPUTimeLimit = shift(@ARGV);
    } 
#----If total time, allow a third per process (bloody rough)
    if (scalar(@ARGV) >= 2 && $ARGV[0] eq "-tt" && $ARGV[1] =~ /^\d+$/) {
        shift(@ARGV);
        $CPUTimeLimit = shift(@ARGV);
        $CPUTimeLimit = int($CPUTimeLimit/3);
    }

    if (scalar(@ARGV) > 0) {
        open($InputHandle,"<$ARGV[0]") or die("ERROR: Cannot open $ARGV[0]\n");
    } else {
        $InputHandle = STDIN;
    }

    DoMain($InputHandle,$CPUTimeLimit);
#------------------------------------------------------------------------------
sub DoMain {
    my ($InputHandle,$CPUTimeLimit) = @_;

    my @Formulae;
    my @ConjectureFormulae;
    my @AxiomFormulae;

    @Formulae = ReadFormulae($InputHandle);
    if (scalar(@Formulae) == 0) {
        print("ERROR: No formulae to ratify\n");
        exit(-1);
    }
#DEBUG PrintFormulae(STDOUT,"Originals",@Formulae);
    @Formulae = FOFify(@Formulae);
#DEBUG PrintFormulae(STDOUT,"FOFified",@Formulae);

    @ConjectureFormulae = ExtractFormulaeWithStatus("conjecture",@Formulae);
#DEBUG PrintFormulae(STDOUT,"Conjectures",@ConjectureFormulae);
    @AxiomFormulae = ExtractFormulaeWithoutStatus("conjecture",@Formulae);
#DEBUG PrintFormulae(STDOUT,"Axioms",@AxiomFormulae);
    if (scalar(@ConjectureFormulae) + scalar(@AxiomFormulae) !=
scalar(@Formulae)) {
        print("ERROR: Conjectures plus others not them all\n");
        exit(-1);
    }

    if (scalar(@ConjectureFormulae) > 0) {
        DoWithConjecture(\@AxiomFormulae,\@ConjectureFormulae,\@Formulae);
    } else {
        DoWithoutConjecture(\@AxiomFormulae);
    }
}
#------------------------------------------------------------------------------
sub DoWithConjecture {
    my ($AxiomFormulaRef,$ConjectureFormulaeRef,$AllFormulaeRef) = @_;

    my $Result;

    print("NOTICE: There is a conjecture\n");
    if (scalar(@$AxiomFormulaRef) > 0) {
        print("NOTICE: There are some axioms, check them for consistency\n");
        if (($Result = RunSystemsFor("SAT",$CPUTimeLimit,@$AxiomFormulaRef)) eq 
"Satisfiable") {
            print("HAPPY : Axioms are $Result, check the conjecture\n");
            DoTheorem($AxiomFormulaRef,$ConjectureFormulaeRef,$AllFormulaeRef);
        } else {
            if ($Result eq "Unsatisfiable") {
                print("SAD   : Axioms are $Result - Conjecture is a vacuous theorem\n");
                print("RESULT: VacuousTheorem\n");
            } else {
                print("BLAH  : Cannot show axioms to be satisfiable, check them for unsatisfiability\n");
                DoDodgyAxiomsTheorem($AxiomFormulaRef,$ConjectureFormulaeRef,
$AllFormulaeRef);
            }
        }
    } else {
        print("NOTICE: No axioms, check the conjecture\n");
        DoTheorem($AxiomFormulaRef,$ConjectureFormulaeRef,$AllFormulaeRef);
    }
}
#------------------------------------------------------------------------------
sub DoDodgyAxiomsTheorem {
    my ($AxiomFormulaRef,$ConjectureFormulaeRef,$AllFormulaeRef) = @_;

    my $Result;

    if (($Result = RunSystemsFor("UNS",$CPUTimeLimit,@$AxiomFormulaRef)) eq 
"Unsatisfiable") {
        print("SAD   : Axioms are $Result - Conjecture is a vacuous theorem\n");
        print("RESULT: VacuousTheorem\n");
    } else {
        print("BLAH  : Cannot show axioms to be Unsatisfiable\n");
        print("BLAH  : Check the conjecture assuming the axioms are Satisfiable\n");
        DoTheorem($AxiomFormulaRef,$ConjectureFormulaeRef,$AllFormulaeRef);
    }
}
#------------------------------------------------------------------------------
sub DoTheorem {
    my ($AxiomFormulaRef,$ConjectureFormulaeRef,$AllFormulaeRef) = @_;

    my $Result;

    if (($Result = RunSystemsFor("THM",$CPUTimeLimit,@$AllFormulaeRef)) eq 
"Theorem") {
        print("HAPPY : All formulae are $Result - Conjecture is a theorem of the axioms\n");
        print("RESULT: Theorem\n");
    } else {
        print("NOTICE: Cannot prove the conjecture, check for counter satisfiability\n");
        if ($Result eq "CounterSatisfiable" ||
($Result = RunSystemsFor("CSA",$CPUTimeLimit,@$AllFormulaeRef)) eq 
"CounterSatisfiable") {
            print("SAD   : All formulae are $Result - Conjecture is not a theorem\n");
            print("RESULT: CounterSatisfiable\n");
        } else {
            print("BLAH  : All formulae are $Result\n");
            print("RESULT: GaveUp\n");
        }
    }
}
#------------------------------------------------------------------------------
sub DoWithoutConjecture {
    my ($AxiomFormulaRef) = @_;

    my $Result;

    print("NOTICE: There is no conjecture\n");
    if (($Result = RunSystemsFor("SAT",$CPUTimeLimit,@$AxiomFormulaRef)) eq 
"Satisfiable") {
        print("HAPPY : All formulae (axioms) are $Result\n");
        print("RESULT: Satisfiable\n");
    } else {
        if ($Result eq "Unsatisfiable" ||
($Result = RunSystemsFor("UNS",$CPUTimeLimit,@$AxiomFormulaRef)) eq 
"Unsatisfiable") {
            print("SAD   : All formulae (axioms) are $Result\n");
            print("RESULT: Unsatisfiable\n");
        } else {
            print("BLAH  : All formulae (axioms) are $Result\n");
            print("RESULT: GaveUp\n");
        }
    }
}
#------------------------------------------------------------------------------
sub RunSystemsFor {
    my ($WantToBe,$CPUTimeLimit,@Formulae) = @_;

    my @Systems;
    my $System;
    my $FailureResult;
    my $SuccessResult;
    my $SystemResult;

    @Systems = ChooseSystemsFor($WantToBe,$CPUTimeLimit,@Formulae);
#DEBUG PrintFormulae(STDOUT,"Want $WantToBe in $CPUTimeLimit, will use @Systems",@Formulae);
    while (!defined($SuccessResult) && defined($System = shift(@Systems))) {
        print("TRYING: To find $WantToBe with $System in ${CPUTimeLimit}s\n");
        if (($SystemResult = RunSystemOn($System,$CPUTimeLimit,@Formulae)) eq 
"Satisfiable" || $SystemResult eq "CounterSatisfiable" || 
$SystemResult eq "Unsatisfiable" || $SystemResult eq "Theorem") {
            $SuccessResult = $SystemResult;
        } else {
            if (!defined($FailureResult)) {
                $FailureResult = $SystemResult;
            } else {
                $FailureResult = "$FailureResult and $SystemResult";
            }
        }
    }
    if (defined($SuccessResult)) {
#DEBUG print("And we got something $SuccessResult\n");
        return($SuccessResult);
    } else {
#DEBUG print("And we got failure $FailureResult\n");
        return($FailureResult);
    }
}
#------------------------------------------------------------------------------
sub ChooseSystemsFor {
    my ($WantToBe,$CPUTimeLimit,@Formulae) = @_;

    if ($WantToBe eq "SAT" || $WantToBe eq "CSA") {
#        return("MACE---2.0");
        return("MACE---2.0","SPASS---2.1");
    }

    if ($WantToBe eq "THM" || $WantToBe eq "UNS") {
#        return("Otter---3.2");
#        return("Vampire---5.0");
        return("SSCPA---0.0 -x \"SSCPA -q1 -cE 2 %d %s\"");
    }

    return();
}
#------------------------------------------------------------------------------
sub RunSystemOn {
    my ($System,$CPUTimeLimit,@Formulae) = @_;

    my $ProblemFileHandle = "ProblemFileHandle";
    my @ResultLines;
    my $ResultLine;
    my $Result;

    unlink($TemporaryProblemFileName);
    open($ProblemFileHandle,">$TemporaryProblemFileName") or
die("ERROR: Cannot create temporary problem file to ratify\n");
    PrintFormulae($ProblemFileHandle,undef,@Formulae);
    close($ProblemFileHandle);
    @ResultLines = 
`$SystemOnTPTPCommand -q2 $System $CPUTimeLimit $TemporaryProblemFileName`;
    unlink($TemporaryProblemFileName);
#DEBUG print("Result lines are @ResultLines\n");
    ($ResultLine) = grep(/^RESULT:/,@ResultLines);
    if (defined($ResultLine)) {
        ($Result) = ($ResultLine =~ /.* says ([^ ]*)/);
        if (defined($Result)) {
#DEBUG print("Got a result $Result\n");
            return($Result);
        } else {
            die("ERROR: Illformed SystemOnTPTP output\n");
        }
    } else {
        die("ERROR: Missing SystemOnTPTP output\n");
    }
}
#------------------------------------------------------------------------------
sub PrintFormulae {
    my ($OutputHandle,$Title,@Formulae) = @_;

    my $Formula;

    if (defined($Title)) {
        print("$Title\n");
    }

    foreach $Formula (@Formulae) {
        print($OutputHandle "$Formula\n");
    }
}
#------------------------------------------------------------------------------
sub ExtractFormulaeWithStatus {
    my ($RequiredStatus,@Formulae) = @_;

    my @StatusFormulae;
    my $Formula;

    foreach $Formula (@Formulae) {
        if ($Formula =~ /fof\([^,]+,$RequiredStatus,/) {
            push(@StatusFormulae,($Formula));
        }
    }
    return(@StatusFormulae);
}
#------------------------------------------------------------------------------
sub ExtractFormulaeWithoutStatus {
    my ($IllegalStatus,@Formulae) = @_;

    my @StatusFormulae;
    my $Formula;
    my $Status;

    foreach $Formula (@Formulae) {
        ($Status) = ($Formula =~ /fof\([^,]+,([^,]+),/);
        if (defined($Status) && $Status ne $IllegalStatus) {
            push(@StatusFormulae,($Formula));
        }
    }
    return(@StatusFormulae);
}
#------------------------------------------------------------------------------
sub FOFify {
    my (@Formulae) = @_;

    my $ReceiveHandle = "ReceiveHandle";
    my $SendHandle = "SendHandle";
    my @FOFFormulae;

    open2($ReceiveHandle,$SendHandle,
"$tptp2XCommand -q2 -d- -t fofify:obvious -f tstp -") or
die("ERROR: Cannot start tptp2X for fofify\n");
    PrintFormulae($SendHandle,undef,@Formulae);
    close($SendHandle);
    @FOFFormulae = ReadFormulae($ReceiveHandle);
    close($ReceiveHandle);

    return(@FOFFormulae);
}
#------------------------------------------------------------------------------
sub ReadFormulae {
    my ($InputHandle) = @_;
    
    my $Line;
    my $Formula;
    my @Formulae;

    while (defined($Line = <$InputHandle>)) {
        if (($Line =~ /^fof/) || ($Line =~ /^cnf/) || 
($Line =~ /^input_formula/) || ($Line =~ /^input_clause/)) {
            $Formula = $Line;
            while ($Formula !~ /\)\. *$/ && defined($Line = <$InputHandle>)) {
                $Formula .=$Line;
            }
            if ($Formula =~ /\)\. *$/) {
                push(@Formulae,($Formula));
            }
        }
    }

    return(@Formulae);
}
#------------------------------------------------------------------------------