#!/usr/bin/perl

#----This program selects the problems from the specified file which satisfy
#----the given constraints
use strict "vars";
#--------------------------------------------------------------------------
#----These need to be installed
my $TPTPDirectory = '/home/graph/tptp/TPTP';

#----Replaces default with user defined
if (exists($ENV{TPTP})) {
    $TPTPDirectory = $ENV{TPTP};
}

#----Other directories, file names, etc
my $SortedProblemFileName = "/tmp/tptp1T_$$";
my $FOFStatisticsFileName = "$TPTPDirectory/Documents/FOFProblemStatistics";
my $CNFStatisticsFileName = "$TPTPDirectory/Documents/CNFProblemStatistics";
#--------------------------------------------------------------------------
    my $ProblemType;
    my $StatisticsFileName;
    my %IndexHash;

#---STDERR to STDOUT
    close(STDERR);
    open(STDERR,">&STDOUT") || die("Cannot redirect STDERR to STDOUT\n");
#----Flush output
    $| = 1;

#----Check arguments
    if (@ARGV == 0 || ($ARGV[0] ne "CNF" && $ARGV[0] ne "FOF")) { 
        die("ERROR: Usage -

tptp1T CNF|FOF [-f <FileName>] {[-]<Constraint> {or [-]<Constraint>}}

<FileName> names a file containing a list of problem names to consider

- negates the meaning of any constraint. A <Constraint> is selected from: 

    Theorem, CounterSatisfiable
    Unsatisfiable, Satisfiable
    Unknown, Open

    Predicates _ _
    Propositional
    Variables
    MinimalPredicateArity _ _, MaximalPredicateArity _ _
    Equality, PureEquality
    Functions _ _
    MinimalFunctionArity _ _, MaximalFunctionArity _ _

    Horn, NonHorn (CNF only)
    RangeRestricted (CNF only)
    AverageLiterals _ _ (CNF only)
    UnitEquality (CNF only)

    Domains ALG, ANA, ... TOP
    Standard, Incomplete, Augmented, Especial, Biased
    Rating _ _
        \n");
    } 

#----Get and delete the problem type
    $ProblemType = shift @ARGV;

#----Set indexes into array and file names for CNF or FOF
    if ($ProblemType eq "FOF") {
#----File names
        $StatisticsFileName = $FOFStatisticsFileName;
#----Indices
        %IndexHash = (
            'Problem' => 0,
            'Version' => 1,
            'Status'  => 2,
            'Rating'  => 3,
#           'Formulae' => 4,
#           'UnitFormulae' => 5,
            'AtomsOrLiterals' => 6,
            'EqAtomsOrLiterals' => 7,
#           'MaxFormulaDepth' => 8,
#           'AvFormulaDepth' => 9,
            'Predicates' => 10,
            'Propositions' => 11,
            'PredicateArities' => 12,
#           'Connectives' => 13,
#           'NOTs' => 14,
#           'ORs' => 15,
#           'ANDs' => 16,
#           'EQUIVs' => 17,
#           'IMPLYs' => 18,
#           'IMPLIEDs' => 19,
#           'XORs' => 20,
#           'NORs' => 21,
#           'NANDs' => 22,
            'Variables' => 23,
#           'Singletons' => 24,
#           'Universals' => 25,
#           'Existentials' => 26,
#           'MaxTermDepth' => 27,
#           'AvTermDepth' => 28,
            'Functions' => 29,
#           'Constants' => 30,
            'FunctionArities' => 31, 
#----Number of statistics for command line version
            'NumberOfStatistics' => 32,
            );
    } else {    
#----File names
        $StatisticsFileName = $CNFStatisticsFileName;
#----Indices
            %IndexHash = (
            'Problem' => 0,
            'Version' => 1,
            'Status'  => 2,
            'Rating'  => 3,
            'Clauses' => 4,
            'NonHornClauses' => 5,
            'UnitClauses' => 6,
            'RRClauses' => 7,
            'AtomsOrLiterals' => 8,
            'EqAtomsOrLiterals' => 9,
#           'MaxLiterals' => 10,
            'AvLiterals' => 11,
            'Predicates' => 12,
            'Propositions' => 13,
            'PredicateArities' => 14,
            'Variables' => 15,
#           'Singletons' => 16,
#           'MaxDepth' => 17,
#           'AvDepth' => 18,
            'Functions' => 19,
#           'Constants' => 20,
            'FunctionArities' => 21, 
#----Number of statistics for command line version
            'NumberOfStatistics' => 22,
            );
    }

#----Look if the data is to be taken from the files, or from the arguments
    if (@ARGV >= 2 && $ARGV[0] eq "-d") { 
#----Delete the -d
        shift @ARGV;
        CheckProblemFromCommandLineData($ProblemType,@ARGV);
    } else {
        ListProblemsFromStatistics($ProblemType,@ARGV);
    }
#--------------------------------------------------------------------------
sub CheckProblemFromCommandLineData {
    my ($ProblemType,@StatisticsAndConstraints) = @_;

    my @Statistics;
    my $Statistic;
    my $StatisticNumber;

#----Extract the constraints into arrays, first all into @Statistics
    @Statistics = split(/[ \t\n]+/,shift(@StatisticsAndConstraints));
#----Check that the next one is the -c flag
    if (@Statistics != $IndexHash{'NumberOfStatistics'} ||
shift(@StatisticsAndConstraints) ne "-c") {
        die("ERROR: Incorrect number of statistics\n");
    }

#----Check the constraints and print an answer
    if (CheckConstraints($ProblemType,\@StatisticsAndConstraints,
\@Statistics)) {
        print("yes\n");
    } else {
        print("no\n");
    }
}
#--------------------------------------------------------------------------
sub ListProblemsFromStatistics {
    my ($ProblemType,@Constraints) = @_;

    my $ProblemListFileHandle = "ProblemListFileHandle";
    my $StatisticsFileHandle = "StatisticsFileHandle";
    my $ProblemListLine;
    my $StatisticsLine;
    my $ProblemName;
    my @Statistics;

#----If a file specified for problems to consider, use it
    if (@Constraints >= 2 && $Constraints[0] eq "-f") { 
#----Delete the -f
        shift @Constraints;
#----Sort the problem list so it has the same order as the statistics files
        system(
"sort -o $SortedProblemFileName +0.0 -0.6 +0.7 -0.9n $Constraints[0]");
        open ($ProblemListFileHandle,"<$SortedProblemFileName") || 
die "ERROR: Cannot open and sort $Constraints[0]";
#----Delete the file name
        shift @Constraints; 
#----Otherwise use the Statistics (all problems considered)
    } else {
        open ($ProblemListFileHandle, "<$StatisticsFileName") || 
die "ERROR: Cannot open $StatisticsFileName";
    }

#----Open the statistics files
    open($StatisticsFileHandle,"<$StatisticsFileName") || 
die "ERROR: Cannot open $StatisticsFileName";

#----Look at each problem named in the problem list
    while ($ProblemListLine = <$ProblemListFileHandle>) {
        chomp($ProblemListLine);
#----If its a line that specifies a problem
        if ($ProblemListLine =~ /^[A-Z][A-Z][A-Z][0-9][0-9][0-9]/) {
#----Extract the problem name (must be first Argument)
            ($ProblemName) = ($ProblemListLine =~ /^([^ ]*) /);
#----Extract the corresponding statistics lines from the statistics files
            while (defined($StatisticsLine = <$StatisticsFileHandle>) &&
$StatisticsLine !~ /\Q${ProblemName}\E/) {
            }
            if (!defined ($StatisticsLine)) {
                die("ERROR: No statistics for $ProblemName\n");
            }
#----Split up the statistics lines
            @Statistics = split (/\s+/, $StatisticsLine);
#----Check the problem against each constraint
            if (CheckConstraints($ProblemType,\@Constraints,\@Statistics)) {
                print("$ProblemListLine\n");
            }
        }
    }
#----Close all the files
    close($StatisticsFileHandle); 
    close($ProblemListFileHandle);
    system("rm -f $SortedProblemFileName");

}
#------------------------------------------------------------------------------
sub CheckConstraints {
    my ($ProblemType,$ConstraintsArrayRef,$StatisticsArrayRef) = @_;

    my @Constraints = @$ConstraintsArrayRef;
    my $ConstraintsUsed;
    my $Result;
    my $ORResult;
    my $FinalResult = 1;
    my $ShiftIndex;

    while ($FinalResult && @Constraints) {
        ($ConstraintsUsed,$Result) = CheckConstraint($ProblemType,
$StatisticsArrayRef,@Constraints);
#----Shift off the arguments used
        foreach $ShiftIndex (1..$ConstraintsUsed) {
            shift(@Constraints);
        }
#----If the next is alternation then deal with it. Cannot short circuit because
#----all the parameters need to be chewed off.
        while (defined($Constraints[0]) && $Constraints[0] eq "or") {
#----Get rid of the or
            shift(@Constraints);
            ($ConstraintsUsed,$ORResult) = CheckConstraint($ProblemType,
$StatisticsArrayRef,@Constraints);
#----Shift off the arguments used
            foreach $ShiftIndex (1..$ConstraintsUsed) {
                shift(@Constraints);
            }
            if (!$Result) {
                $Result = $ORResult;
            }
        }
       
#----AND with running result
        $FinalResult *= $Result;
    }

    return($FinalResult);
}
#------------------------------------------------------------------------------
#----Return TRUE or FALSE based on these arguments
sub CheckConstraint {
    my ($ProblemType,$StatisticsArrayRef,$Constraint,@RestOfConstraints) = @_;

    my $Negated;
    my $ConstraintsUsed;
    my $Result;

#----See if it's negated
    if ($Constraint =~ /^-/) {
        $Constraint = substr($Constraint,1);
        $Negated = 1;
    } else {
        $Negated = 0;
    }

    ($ConstraintsUsed,$Result) = CheckUnnegatedConstraint($ProblemType,
$StatisticsArrayRef,$Constraint,@RestOfConstraints);

    return($ConstraintsUsed,abs($Result - $Negated));
}
#------------------------------------------------------------------------------
sub CheckUnnegatedConstraint {
    my ($ProblemType,$StatisticsArrayRef,$Constraint,@RestOfConstraints) = @_;

    my $ArgumentsUsed;

#----Return number of arguments used and result
    if ($Constraint =~ /^dom/i) { 
        $ArgumentsUsed = Domains($ProblemType,$StatisticsArrayRef,
@RestOfConstraints);
        return(abs($ArgumentsUsed)+1,$ArgumentsUsed > 0);
    }
    if ($Constraint =~ /^stan/i) { 
        return(1,Standard($ProblemType,$StatisticsArrayRef)); 
    }
    if ($Constraint =~ /^incom/i) {
        return(1,Incomplete($ProblemType,$StatisticsArrayRef));
    }
    if ($Constraint =~ /^aug/i) {
        return(1,Augmented($ProblemType,$StatisticsArrayRef));
    }
    if ($Constraint =~ /^espec/i) {
        return(1,Especial($ProblemType,$StatisticsArrayRef));
    }
    if ($Constraint =~ /^bias/i) {
        return(1,Biased($ProblemType,$StatisticsArrayRef));
    }
    if ($Constraint =~ /^rat/i)            { 
        return(3,Rating($ProblemType,$StatisticsArrayRef,$RestOfConstraints[0],
$RestOfConstraints[1])); 
    }
    if ($Constraint =~ /^Theorem/i) {
        return(1,Theorem($ProblemType,$StatisticsArrayRef));
    }
    if ($Constraint =~ /^CounterSat/i) {
        return(1,CounterSatisfiable($ProblemType,$StatisticsArrayRef));
    }
    if ($Constraint =~ /^Unknown/i) {
        return(1,Unknown($ProblemType,$StatisticsArrayRef));
    }
    if ($Constraint =~ /^Sat/i) {
        return(1,Satisfiable($ProblemType,$StatisticsArrayRef));
    }
    if ($Constraint =~ /^Unsat/i) {
        return(1,Unsatisfiable($ProblemType,$StatisticsArrayRef));
    }
    if ($Constraint =~ /^open/i) {
        return(1,Open($ProblemType,$StatisticsArrayRef));
    }
    if ($Constraint =~ /^pred/i)            { 
        return(3,Predicates($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1])); 
    }
    if ($Constraint =~ /^prop/i) {
        return(1,Propositional($ProblemType,$StatisticsArrayRef));
    }
    if ($Constraint =~ /^var/i) {
        return(1,Variables($ProblemType,$StatisticsArrayRef));
    }
    if ($Constraint =~ /^min.*pred.*ar/i) {
        return(3,MinimalPredicateArity($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1]));
    }
    if ($Constraint =~ /^max.*pred.*ar/i) {
        return(3,MaximalPredicateArity($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1]));
    }
    if ($Constraint =~ /^Eq/i) {
        return(1,Equality($ProblemType,$StatisticsArrayRef));
    }
    if ($Constraint =~ /^pureEq/i) {
        return(1,PureEquality($ProblemType,$StatisticsArrayRef));
    }
    if ($Constraint =~ /^func/i)            { 
        return(3,Functions($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1])); 
    }
    if ($Constraint =~ /^min.*fun.*ar/i) {
        return(3,MinimalFunctionArity($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1]));
    }
    if ($Constraint =~ /^max.*fun.*ar/i) {
        return(3,MaximalFunctionArity($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1]));
    }
    if ($Constraint =~ /^horn/i) {
        return(1,Horn($ProblemType,$StatisticsArrayRef));
    }
    if ($Constraint =~ /^nonh/i) {
        return(1,NonHorn($ProblemType,$StatisticsArrayRef));
    }
    if ($Constraint =~ /^ran.*re/i) {
        return(1,RangeRestricted($ProblemType,$StatisticsArrayRef));
    }
    if ($Constraint =~ /^av*lit/i) {
        return(3,AverageLiterals($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1]));
    }
    if ($Constraint =~ /^unitEq/i) {
        return(1,UnitEquality($ProblemType,$StatisticsArrayRef));
    }

#----Default return 1 used, and it failed
    return(1,0);
}
#------------------------------------------------------------------------------
#==============================================================================
#----CNF and FOF constraints
#==============================================================================
#------------------------------------------------------------------------------
#----This is only used once on the first problem if a domain constraint
#----is given. After that a check is made in the main loop.
sub Domains { 
    my ($ProblemType,$StatisticsArrayRef,@Constraints) = @_;

    my $NumberOfDomains = 0;
    my @Domains = ();
    my $ProblemDomain;

#----Get domains off constraint list
    while ($Constraints[$NumberOfDomains] =~ /^[A-Z]{3}$/) {
        $Domains[$NumberOfDomains] = $Constraints[$NumberOfDomains];
        $NumberOfDomains++;
    }

    $ProblemDomain = substr($$StatisticsArrayRef[$IndexHash{'Problem'}],0,3);

    if (grep(/$ProblemDomain/,@Domains)) {
        return($NumberOfDomains);
    } else {
        return(-1 * $NumberOfDomains);
    }
#---- return($$StatisticsArrayRef[$IndexHash{'Problem'}] =~ /$Domain/);
}
#------------------------------------------------------------------------------
sub Standard { 
    my ($ProblemType,$StatisticsArrayRef) = @_;

    return($$StatisticsArrayRef[$IndexHash{'Version'}] eq "S");
}
#------------------------------------------------------------------------------
sub Incomplete { 
    my ($ProblemType,$StatisticsArrayRef) = @_;

    return($$StatisticsArrayRef[$IndexHash{'Version'}] eq "I");
}
#------------------------------------------------------------------------------
sub Augmented { 
    my ($ProblemType,$StatisticsArrayRef) = @_;

    return($$StatisticsArrayRef[$IndexHash{'Version'}] eq "A");
}
#------------------------------------------------------------------------------
sub Especial { 
    my ($ProblemType,$StatisticsArrayRef) = @_;

    return($$StatisticsArrayRef[$IndexHash{'Version'}] eq "E");
}
#------------------------------------------------------------------------------
sub Biased { 
    my ($ProblemType,$StatisticsArrayRef) = @_;

    return($$StatisticsArrayRef[$IndexHash{'Version'}] eq "B");
}
#------------------------------------------------------------------------------
sub Rating {
    my ($ProblemType,$StatisticsArrayRef,$LowerBound,$UpperBound) = @_;

    return($$StatisticsArrayRef[$IndexHash{'Rating'}] ne "?" &&
$$StatisticsArrayRef[$IndexHash{'Rating'}] >= $LowerBound && 
$$StatisticsArrayRef[$IndexHash{'Rating'}] <= $UpperBound);
}
#------------------------------------------------------------------------------
sub Theorem { 
    my ($ProblemType,$StatisticsArrayRef) = @_;

    return($ProblemType eq "FOF" && 
           $$StatisticsArrayRef[$IndexHash{'Status'}] eq "T");
}
#------------------------------------------------------------------------------
sub CounterSatisfiable { 
my ($ProblemType,$StatisticsArrayRef) = @_;

    return($ProblemType eq "FOF" && 
           $$StatisticsArrayRef[$IndexHash{'Status'}] eq "C");
}
#------------------------------------------------------------------------------
sub Unsatisfiable { 
    my ($ProblemType,$StatisticsArrayRef) = @_;
    
    return($$StatisticsArrayRef[$IndexHash{'Status'}] eq "U");
}
#------------------------------------------------------------------------------
sub Satisfiable { 
    my ($ProblemType,$StatisticsArrayRef) = @_;

    return($$StatisticsArrayRef[$IndexHash{'Status'}] eq "S");
}
#------------------------------------------------------------------------------
sub Unknown { 
    my ($ProblemType,$StatisticsArrayRef) = @_;

    return($$StatisticsArrayRef[$IndexHash{'Status'}] eq "?" ||
           Open($ProblemType,$StatisticsArrayRef));
}
#------------------------------------------------------------------------------
sub Open { 
    my ($ProblemType,$StatisticsArrayRef) = @_;

    return($$StatisticsArrayRef[$IndexHash{'Status'}] eq "O");
}
#------------------------------------------------------------------------------
sub Predicates {
    my ($ProblemType,$StatisticsArrayRef,$LowerBound,$UpperBound) = @_;

    return($$StatisticsArrayRef[$IndexHash{'Predicates'}] >= $LowerBound && 
$$StatisticsArrayRef[$IndexHash{'Predicates'}] <= $UpperBound);
}
#------------------------------------------------------------------------------
sub Propositional { 
    my ($ProblemType,$StatisticsArrayRef) = @_;

    return($$StatisticsArrayRef[$IndexHash{'Predicates'}] == 
$$StatisticsArrayRef[$IndexHash{'Propositions'}]);
}
#------------------------------------------------------------------------------
sub Variables {
    my ($ProblemType,$StatisticsArrayRef) = @_;
    
    return($$StatisticsArrayRef[$IndexHash{'Variables'}] > 0);
}
#------------------------------------------------------------------------------
sub MinimalPredicateArity {
    my ($ProblemType,$StatisticsArrayRef,$LowerBound,$UpperBound) = @_;

    my $MinimalArity;

    ($MinimalArity) = 
($$StatisticsArrayRef[$IndexHash{'PredicateArities'}] =~ /([0-9]*)\-[0-9]*/);
    return($MinimalArity >= $LowerBound && $MinimalArity <= $UpperBound);
}
#------------------------------------------------------------------------------
sub MaximalPredicateArity {
    my ($ProblemType,$StatisticsArrayRef,$LowerBound,$UpperBound) = @_;

    my $MaximalArity;

    ($MaximalArity) = 
($$StatisticsArrayRef[$IndexHash{'PredicateArities'}] =~ /[0-9]*\-([0-9]*)/);
    return($MaximalArity >= $LowerBound && $MaximalArity <= $UpperBound);
}
#------------------------------------------------------------------------------
sub Equality { 
    my ($ProblemType,$StatisticsArrayRef) = @_;

    return($$StatisticsArrayRef[$IndexHash{'EqAtomsOrLiterals'}] > 0);
}
#------------------------------------------------------------------------------
sub PureEquality { 
    my ($ProblemType,$StatisticsArrayRef) = @_;

    return(Equality($ProblemType,$StatisticsArrayRef) &&
$$StatisticsArrayRef[$IndexHash{'AtomsOrLiterals'}] == 
$$StatisticsArrayRef[$IndexHash{'EqAtomsOrLiterals'}]);
}
#------------------------------------------------------------------------------
sub Functions { 
    my ($ProblemType,$StatisticsArrayRef,$LowerBound,$UpperBound) = @_;

    return($$StatisticsArrayRef[$IndexHash{'Functions'}] >= $LowerBound && 
           $$StatisticsArrayRef[$IndexHash{'Functions'}] <= $UpperBound);
}
#------------------------------------------------------------------------------
sub MinimalFunctionArity {
    my ($ProblemType,$StatisticsArrayRef,$LowerBound,$UpperBound) = @_;

    my $MinimalArity;

    if ($$StatisticsArrayRef[$IndexHash{'FunctionArities'}] eq "---") {
        $MinimalArity = -1;
    } else {
        ($MinimalArity) = 
($$StatisticsArrayRef[$IndexHash{'FunctionArities'}] =~ /([0-9]*)\-[0-9]*/);
    }

    if ($LowerBound eq "-") {
        $LowerBound = -1;
    }

    if ($UpperBound eq "-") {
        $UpperBound = -1;
    }

    return($MinimalArity >= $LowerBound && $MinimalArity <= $UpperBound);
}
#------------------------------------------------------------------------------
sub MaximalFunctionArity {
    my ($ProblemType,$StatisticsArrayRef,$LowerBound,$UpperBound) = @_;

    my $MaximalArity;

    if ($$StatisticsArrayRef[$IndexHash{'FunctionArities'}] eq "---") {
        $MaximalArity = -1;
    } else {
        ($MaximalArity) = 
($$StatisticsArrayRef[$IndexHash{'FunctionArities'}] =~ /[0-9]*\-([0-9]*)/);
    }

    if ($LowerBound eq "-") {
        $LowerBound = -1;
    }

    if ($UpperBound eq "-") {
        $UpperBound = -1;
    }

    return($MaximalArity >= $LowerBound && $MaximalArity <= $UpperBound);
}
#------------------------------------------------------------------------------
#==============================================================================
#----CNF only constraints
#==============================================================================
#------------------------------------------------------------------------------
sub Horn { 
    my ($ProblemType,$StatisticsArrayRef) = @_;

    return($ProblemType eq "CNF" && 
$$StatisticsArrayRef[$IndexHash{'NonHornClauses'}] == 0);
}
#------------------------------------------------------------------------------
sub NonHorn { 
    my ($ProblemType,$StatisticsArrayRef) = @_;

    return($ProblemType eq "CNF" && 
$$StatisticsArrayRef[$IndexHash{'NonHornClauses'}] != 0);
}
#------------------------------------------------------------------------------
sub RangeRestricted { 
    my ($ProblemType,$StatisticsArrayRef) = @_;

    return($ProblemType eq "CNF" &&
$$StatisticsArrayRef[$IndexHash{'Clauses'}] == 
$$StatisticsArrayRef[$IndexHash{'RRClauses'}]);
}
#------------------------------------------------------------------------------
sub AverageLiterals {
    my ($ProblemType,$StatisticsArrayRef,$LowerBound,$UpperBound) = @_;

    return($$StatisticsArrayRef[$IndexHash{'AvLiterals'}] >= $LowerBound &&
           $$StatisticsArrayRef[$IndexHash{'AvLiterals'}] <= $UpperBound);
}
#------------------------------------------------------------------------------
sub UnitEquality {
    my ($ProblemType,$StatisticsArrayRef) = @_;

    return($ProblemType eq "CNF" && 
PureEquality($ProblemType,$StatisticsArrayRef) &&
$$StatisticsArrayRef[$IndexHash{'Clauses'}] == 
$$StatisticsArrayRef[$IndexHash{'UnitClauses'}]);
}
#------------------------------------------------------------------------------
