#!/usr/bin/perl

#----Program: tptp2T
#----Selects Problems and Solutions satisfying given constraints
#----Alex Roederer, based on the tptp1T script by Geoff Sutcliffe
#----V2.3 Feb 17th, 2008

use strict "vars"; 
#------------------------------------------------------------------------------
#----Defines default TPTP home directory
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/tptp2T_$$";
my $StatisticsFileName = 
"$TPTPDirectory/Documents/ProblemAndSolutionStatistics";
#------------------------------------------------------------------------------
#----Define hashes that will represent the formated problem and solution
    my %ProblemIndexHash;
    my %SolutionIndexHash; 
    my %AbbreviationHash; 

#----Set indexes into array and file names
#----Indices
    %ProblemIndexHash = (
        'Problem' => 0,
        'Version' => 1,
        'Status' => 2,
        'Rating' => 3,
        'Formulae' => 4, 
        'Clauses' => 4,
        'NonHornClauses' => 5,
        'UnitFormulae' => 6, 
        'UnitClauses' => 6,
        'TypeFormulae' => 7,
        'DefnFormulae' => 8,
        'RRClauses' => 9,
        'Atoms' => 10,
        'EqualityAtoms' => 11,
        'VariableAtoms' => 12,
        'MaxFormulaDepth' => 13,
        'AvFormulaDepth' => 14,
        'AvLiterals' => 14,
        'Symbols' => 15,
        'Predicates' => 15,
        'Propositions' => 16,
        'PredicateArities' => 17,
        'Connectives' => 18,
        'TypeConnectives' => 19,
        'Variables' => 20,
        'Singletons' => 21,
        'Universals' => 22,
        'Existentials' => 23,
        'Lambdas' => 24,
        'MaxTermDepth' => 25,
        'AvTermDepth' => 26,
        'Functions' => 27,
        'Constants' => 28,
        'FunctionArities' => 29, 
        'ArithmeticSymbols' => 30,
#----These are extra computed statistics, not taken from the data file
        'Domain' => 31, 
#----The final number of statistics
        'SupType' => 32, 
#----Number of statistics from data file
        'NumberOfStatistics' => 31,
    );

    %SolutionIndexHash = (
        'SystemName' => 0,
        'Result' => 1,
        'ResultTime' => 2, 
        'Output' => 3,
        'OutputTime' => 4, 
        'SolutionFormulae' => 5,
        'SolutionClauses' => 6,
        'SolutionLeaves' => 7,
        'SolutionDepth' => 8,
        'SolutionAtoms' => 9,
        'SolutionEqualityAtoms' => 10,
        'MaximalFormulaDepth' => 11,
        'MaximalClauseSize' => 12,
        'MaximalTermDepth' => 13, 
#----These are extra computed statistics, not taken from the data file
        'SOLNumberOfStatistics' => 14, #----Number from data file
    );

#----Converts full words into ontology abbreviations
    %AbbreviationHash = (
        'Success' => 'SUC',
        'Theorem' => 'THM',
        'CounterSatisfiable' => 'CSA',
        'Satisfiable' => 'SAT',
        'Unsatisfiable' => 'UNS',

        'NoSuccess' => 'NOS',
        'Open' => 'OPN',
        'Timeout' => 'TMO',
        'GaveUp' => 'GUP',
        'Error' => 'ERR',
        'Unknown' => 'UNK',

        'Solution' => 'Sol',
        'Proof' => 'Prf',
        'Refutation' => 'Ref',
        'CNFRefutation' => 'CRf',
        'Model' => 'Mod',
        'FiniteModel' => 'FMo',
        'Saturation' => 'Sat',
        'Assurance' => 'Ass',
        'None' => 'Non',
    );

#----Call Main Function
    DoMain();
#------------------------------------------------------------------------------
#----DoMain Function determines if data is to be taken from arguments or files-
#------------------------------------------------------------------------------
sub DoMain {

#---Pushes STDERR to STDOUT
    close(STDERR);
    open(STDERR,">&STDOUT") || 
die("ERROR: Cannot redirect STDERR to STDOUT\n");

#----Flush output make pipes hot!
    $| = 1;

#----Check arguments, if none, given or -h is called, print help
    if (@ARGV == 0 || ($ARGV[0] eq "-h") || ($ARGV[0] eq "--h")) { 
        Usage();
        die("\n");
    }

#----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;
#DEBUG print("OUT CMND Statistics: @ARGV\n");
        CheckProblemFromCommandLineData(@ARGV);
    } else {
#DEBUG print("OUT LIST Statistics: @ARGV\n"); 
        ListProblemsFromStatistics(@ARGV);
    }
}
#------------------------------------------------------------------------------
#----Usage prints instructions for use if insufficient arguments provided
#------------------------------------------------------------------------------
sub Usage {

    print("Adapted from the tptp1T script by Alex Roederer, University of Miami, 2007

Usage -

tptp2T [-f <FileName>] [-q1 or -q2 or -q3] [-pp or -ps or -pps] {[-]<Constraint> {[and/or] [-]<Constraint>}}

<FileName> lists the problems to be considered (default is all).
-q sets quietness: 1=continuous update, 2=final count, 3=quiet
-pp prints problem lines, -ps prints solution lines, -pps prints both 
(Defaults: Only Problem Constraints = -pp
           Only Solution Constraints = -ps
           Both types of Constraints = -pps)
- negates the meaning of any constraint. 
or allows for logical or between constraints.
and allows for logical and between constraints.
a space between constraints is treated as an and. 
Curley braces {} allow for grouping of terms.  

For constraints in which an upper and lower bound are required,
a dash (-) may be used to indicate don't care. 

A <Constraint> is selected from: 
    
    Problem Constraints:

    Form _ (THF, TFF, FOF, CNF, ANY - default is ANY)
    Version _ (Standard, Incomplete, Augmented, Especial, Biased)
    Status _ (Theorem, CounterSatisfiable, Unknown, 
              Unsatisfiable, Satisfiable, Open)
    Rating _ _
    Formulae _ _ (THF, TFF, FOF)
    Clauses _ _ (CNF)
    NonHorn (CNF)
    NonHornClauses _ _ (CNF)
    UnitFormulae _ _ (THF, TFF, FOF)
    UnitClauses _ _ (CNF)
    RangeRestricted (CNF)
    RRClauses _ _ (CNF)
    Atoms _ _
    Equality
    EqualityAtoms _ _
    PureEquality
    UnitEquality (CNF)
    Arithmetic (THF and TFF)
    ArithmeticSymbols _ _ (THF and TFF)
    Symbols _ _ (THF)
    MinimalSymbolArity _ _ (THF)
    MaximalSymbolArity _ _ (THF)
    Predicates _ _ (TFF, FOF, CNF)
    Propositional (TFF, FOF, CNF)
    MinimalPredicateArity _ _ (TFF, FOF, CNF)
    MaximalPredicateArity _ _ (TFF, FOF, CNF)
    Variables
    Functions _ _ (FOF, TFF, CNF)
    MinimalFunctionArity _ _ (TFF, FOF, CNF)
    MaximalFunctionArity _ _ (TFF, FOF, CNF)
    AverageLiterals _ _ (CNF)
    Domains ALG ANA ... TOP

    Solution Constraints (multiple sets allowed): 
    
    System Name[---Version] (System ANY for any system)
    Result _ (SZS value, e.g., THM) 
    ResultTime _ _
    Output _ (SZS value, e.g., Ref)
    SolutionFormulae _ _ (THF, TFF, FOF)
    SolutionClauses _ _  (CNF)
    SolutionDepth _ _
    SolutionLeaves _ _
    Equality
    SolutionEqualityAtoms _ _
    PureEquality
    Selectivity _ _
    Girth _ _
");
}
#------------------------------------------------------------------------------
#----CheckProblemFromCommandLineData
#------------------------------------------------------------------------------
#---This is antiquated and probably no longer supported. Use at your own peril.
#------------------------------------------------------------------------------
sub CheckProblemFromCommandLineData {
    my (@StatisticsAndConstraints) = @_;

    my @Statistics;
    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 (scalar(@Statistics) != $ProblemIndexHash{'NumberOfStatistics'} ||
shift(@StatisticsAndConstraints) ne "-c") {
        die("ERROR: Incorrect number of statistics\n");
    }

#----Check the constraints and print an answer
#    if (CheckConstraints(\@StatisticsAndConstraints,\@Statistics)) {
#        print("yes\n");
#    } else {
        print("Sorry, this feature is not currently supported.\n");
#    }
}
#------------------------------------------------------------------------------
#----ListProblemsFromStatistics------------------------------------------------
#------------------------------------------------------------------------------
sub ListProblemsFromStatistics {
    my (@Constraints) = @_;

    my $PrintOption;
    my $QuietnessOption; 
    my $ProblemListFileHandle = "ProblemListFileHandle";
    my $StatisticsFileHandle = "StatisticsFileHandle";
    my $StatisticsLine;
    my $ProblemName;
    my @Statistics;
    my @TempStats; 
    my $ProblemType; 
    my $GoodProblem; 

    my @SolutionStatistics;
    my @SolutionLines; 

    my @ProblemStatistics;
    my $ProblemLine;  
    my $indexThroughProblems;
    my $SomeSolutionExists; 
    my $SystemChecksIndex; 
   
    my $Garbage; 
 
    my $FinalResultHolder; 
    my $ConstraintsStackArrayRef; 

    my $SystemChecksResults;         
    my $NumberOfSystems; 

    my $PrintFlag; 
    my $Counter;
    my $ProblemCounter = 0;
    my $SolutionCounter = 0; 
    my $IdleFlag = 0;
    my $CurrentDomain = "???"; 
    my $LastDomain = "???"; 

    my @GoodSolutions; 
    my @SolutionNamesNotToPrint;  
    my $SolutionNameNotToPrint; 

    my $CurrentConstraint = 0; 
    my @ConstraintsStack; 
    my @ConstraintsStackSave; 
    my $ConstraintsStackRef; 
    my @ConstraintsStackSaveForPrinting; 
    my $ResultValuePushedThrough = 1; 
    my $SystemAnyChosen; 

#----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 -k 1.1,1.6 -k 1.7,1.7r -k 1.8n $Constraints[0]");
#----Delete the file name
        shift @Constraints; 
        open($ProblemListFileHandle,"<$SortedProblemFileName") || 
die("ERROR: Cannot open and sort $Constraints[0]\n");

#----Otherwise use the Statistics (all problems considered)
    } else {
        open($ProblemListFileHandle, "<$StatisticsFileName") || 
die "ERROR: Cannot open $StatisticsFileName";
    }

#----Look for quietness flag
    if ($Constraints[0] =~ /^-q/) {
        $QuietnessOption = shift(@Constraints); 
    } else {
        $QuietnessOption = "-q2"; 
    }

#----Look for print options flag
    if ($Constraints[0] =~ /^-p/) {
        $PrintOption = shift(@Constraints);
    } else {

        $PrintFlag = 0; 
        $Counter = 0;
        $PrintOption = "-pps"; 

        while (defined ($Constraints[$Counter])) {
            if (($Constraints[$Counter]) =~ /syst/i) {
                    $PrintFlag = 1;
            }
            $Counter++; 
        }
        if ($PrintFlag == 0) {
            $PrintOption = "-pp"; 
        } 
    }

#----Here we create @ConstraintsStack, that contains the system names and 
#----logical operators. This will be filled in to later check that the 
#----entire logical systems onstruct has been satisfied, before the problem 
#----is printed. 

    @ConstraintsStack = (); 
    $ConstraintsStackRef = CreateConstraintsStack(\@Constraints,
\@ConstraintsStack); 
    @ConstraintsStack = @$ConstraintsStackRef; 
    @ConstraintsStackSave = @ConstraintsStack; 
#DEGBUG print("ConstraintsStack: @ConstraintsStack\n"); 

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

#----Print appropriate headers - get them from the statistics file
    $StatisticsLine = <$StatisticsFileHandle>;
    chomp($StatisticsLine);
    if ($StatisticsLine !~ /Problem/) {
        die("ERROR: No Problem header in statistics file\n");
    }
    if ($QuietnessOption le "-q2") {
        if ($PrintOption =~ /^-pp/) {
            print("$StatisticsLine\n");
        }
        if ($PrintOption =~ /s/) {
            $StatisticsLine = <$StatisticsFileHandle>;
            chomp($StatisticsLine);
            if ($StatisticsLine !~ /Solution/) {
                die("ERROR: No Problem header in statistics file\n");
            }
            print("   $StatisticsLine\n");
        }
    }

#----Look at each problem named in the "problem list"
    while (defined($ProblemName = GetNextProblemName($ProblemListFileHandle))) {
#----Extract the corresponding statistics lines from the statistics files
#DEBUG print("ProblemName block: $ProblemName\n");
        $StatisticsLine = <$StatisticsFileHandle>;
        chomp($StatisticsLine);
        while (defined($StatisticsLine) && 
$StatisticsLine !~ /^\Q${ProblemName}\E/) {
            $StatisticsLine = <$StatisticsFileHandle>;
            chomp($StatisticsLine);
        }
        if (!defined($StatisticsLine)) {
            die("ERROR: No statistics for $ProblemName\n");
        }

#----Erase any information in these two arrays: 
#----These will be used to hold the statistics lines. 
        @SolutionStatistics = (); 
        @SolutionLines = ();

#----For each statistics line (skipping blank lines)
        while (defined($StatisticsLine) && $StatisticsLine !~ /^ *$/) {
#----Split up the statistics line
            @Statistics = split (/\s+/, $StatisticsLine);
#----Check if length is "correct" (fits one of the three formats)
            if ($StatisticsLine =~ /^[A-Za-z]{3}[0-9]{3}\^/) {
                $ProblemType = "THF";
            } elsif ($StatisticsLine =~ /^[A-Za-z]{3}[0-9]{3}[_=]/) {
                $ProblemType = "TFF";
            } elsif ($StatisticsLine =~ /^[A-Za-z]{3}[0-9]{3}\+/) {
                $ProblemType = "FOF";
            } elsif ($StatisticsLine =~ /^[A-Za-z]{3}[0-9]{3}-/) {
                $ProblemType = "CNF";
            } elsif ($StatisticsLine =~ /^.+---.+/)  {
                $ProblemType = "SOL";
            } else {
                die("ERROR: Cannot work out type for \"$StatisticsLine\"\n"); 
            }

#----Space Statistics Out According Type of Problem
            if ($ProblemType eq "THF" || $ProblemType eq "TFF" ||
$ProblemType eq "FOF" || $ProblemType eq "CNF") {
                $ProblemLine = $StatisticsLine; 
                $Statistics[$ProblemIndexHash{'Domain'}] = substr($Statistics[0],0,3); 
                $Statistics[$ProblemIndexHash{'SupType'}] = $ProblemType; 
                $#Statistics = $ProblemIndexHash{'SupType'};
#----Save the problem statistics (@Statistics now gets used for each solution)
                @ProblemStatistics = @Statistics;
            } elsif ($ProblemType eq "SOL") {
                push (@SolutionLines, $StatisticsLine); 
                $Statistics[$ProblemIndexHash{'SupType'}] = $ProblemType; 
                $#Statistics = $ProblemIndexHash{'SupType'};
#----Make a reference to a copy of the statistics and save in list
                push (@SolutionStatistics, [ @Statistics ]);
            } else {
                die("ERROR: Not THF, TFF, FOF, CNF, or SOL\n");
            }
            $StatisticsLine = <$StatisticsFileHandle>;
            chomp($StatisticsLine);
        }

#----Get the Current Domain for Idleprinter...
        $CurrentDomain = $ProblemStatistics[$ProblemIndexHash{'Domain'}]; 

#----Call CheckConstraints on the Problem to determine Goodness. 
        ($GoodProblem,$Garbage) = CheckConstraints(
$ProblemStatistics[$ProblemIndexHash{'SupType'}],\@ConstraintsStack,
\@Constraints,\@ProblemStatistics,\@ProblemStatistics);
#DEBUG print("Good Problem: $GoodProblem\n");

#----IMMEDIATE ABORT: We've passed our last domain of interest
        if ($GoodProblem == -99) {
#----If required, print the prob and sol counts
            if ($QuietnessOption le "-q2") {
                print(
"\n\% $ProblemCounter problems and $SolutionCounter solutions found\n"); 
            }
#----Close the files, and exit back to main.
            close($StatisticsFileHandle); 
            close($ProblemListFileHandle);
            system("rm -f $SortedProblemFileName");
            return(1); 
        }
#----END OF IMMEDIATE ABORT

#----If we've found a good problem, start processing the solutions
        if ($GoodProblem) {
            @ConstraintsStack = @ConstraintsStackSave;
            $SomeSolutionExists = 0; 
            $indexThroughProblems = 0;
            @GoodSolutions = (); 

#----Go through the statistics lines,
#----Each time through the loop, CheckConstraints is called.
#----It returns a Result and the Constraints Stack
#----The result is put into @GoodSolutions. The Stack is captured.
 
            while (defined($SolutionStatistics[$indexThroughProblems])) {
                ($FinalResultHolder,$ConstraintsStackArrayRef) = 
CheckConstraints("SOL",\@ConstraintsStack,\@Constraints,
$SolutionStatistics[$indexThroughProblems],\@ProblemStatistics);
                @ConstraintsStack = @$ConstraintsStackArrayRef; 
                $GoodSolutions[$indexThroughProblems] = $FinalResultHolder; 
                $indexThroughProblems++; 
            }
#DEBUG print("GoodSolutions: @GoodSolutions and @ConstraintsStack\n"); 
#DEBUG print("ConstraintsStack before changes: @ConstraintsStack\n");

            $CurrentConstraint = 0; 
            $SystemChecksIndex = 0;

#----All solution lines are finished, and the Constraints Stack is finished. 
#----If any of the S: markers in the ConstraintsStack don't have any
#----RES:* after them, we assume it's because that system constraint 
#----failed for all lines, so we set it to RES:0 
            while (defined($CurrentConstraint = 
$ConstraintsStack[$SystemChecksIndex])) {
                if ($CurrentConstraint =~ m/^S/ && 
$CurrentConstraint !~ m/RES:[0-9]+$/) {
                    $ConstraintsStack[$SystemChecksIndex] .= "RES:0";
                }
                $SystemChecksIndex++;  
            }
#DEBUG print("ConstraintsStack After First Sub: @ConstraintsStack\n"); 

            @ConstraintsStackSaveForPrinting = @ConstraintsStack; 
            $ResultValuePushedThrough = 1; 
            $SystemChecksIndex = 0;
           
#----Now, go through the ConstraintsStack, and mark off any 
#----lines that, while true, contribute nothing to the answer ( for example, 
#----1 and 0 would evaluate to 0, and the first solution line, while true
#----in regards to its system constraint, does not make the entire 
#----expression true, so it shouldn't be printed).
 
            while (defined($CurrentConstraint = 
$ConstraintsStackSaveForPrinting[$SystemChecksIndex])) {
                if ($CurrentConstraint =~ /^S.*0$/) {
                    $ResultValuePushedThrough = 0; 
                } elsif (($CurrentConstraint =~ /^S.*1$/ || 
$CurrentConstraint =~ /^S.*7$/) && $ResultValuePushedThrough == 0) {
                    $ConstraintsStackSaveForPrinting[$SystemChecksIndex] =~ 
s/1$/0/; 
                } elsif ($CurrentConstraint =~ /or/) {
                    $ResultValuePushedThrough = 1; 
                }
            $SystemChecksIndex++; 
            }

            $ResultValuePushedThrough = 1; 
            $SystemChecksIndex--;
            
#----And go through in the other direction, right to left, to catch any that 
#----were located at the beginning of a clause. 
            while ($SystemChecksIndex > -1 && defined($CurrentConstraint = 
$ConstraintsStackSaveForPrinting[$SystemChecksIndex])) {
                if ($CurrentConstraint =~ /^S.*0$/) {
                    $ResultValuePushedThrough = 0; 
                } elsif (($CurrentConstraint =~ /^S.*1$/ || 
$CurrentConstraint =~ /^S.*7$/)  && $ResultValuePushedThrough == 0) {
                    $ConstraintsStackSaveForPrinting[$SystemChecksIndex] =~ 
s/1$/0/; 
                } elsif ($CurrentConstraint =~ /or/) {
                    $ResultValuePushedThrough = 1; 
                }
            $SystemChecksIndex--; 
            }
#DEBUG print("Printing Save After: @ConstraintsStackSaveForPrinting\n");

            @SolutionNamesNotToPrint = (); 
            $SystemAnyChosen = 0; 

#----Now that the string is fixed up, go through the ConstraintsStack, 
#----and pull out the names for systems that are RES:0 so we don't print them. 

            $SystemChecksIndex = 0; 
            while (defined($CurrentConstraint = 
$ConstraintsStackSaveForPrinting[$SystemChecksIndex])) {
#DEBUG print("Current: $CurrentConstraint!\n");
                if ($CurrentConstraint =~ /^S.*0$/ && 
$CurrentConstraint !~ /^S:ANY/) {
                    $CurrentConstraint =~ s/^S://; 
                    $CurrentConstraint =~ s/RES:0$//; 
                    push(@SolutionNamesNotToPrint,$CurrentConstraint); 
                } elsif ($CurrentConstraint =~ /^S:ANY/ && 
$CurrentConstraint =~ /RES:7$/) {
                    $SystemAnyChosen = 1; 
                }
                $SystemChecksIndex++; 
            }
#DEBUG print("SolutionNamesNotToPrint : @SolutionNamesNotToPrint\n"); 
#DEBUG print("GoodSolutions: @GoodSolutions\n"); 

#----Get each name that shouldn't be printed, and find the corresponding
#----entry in the GoodSolutions array, and set it to 0.
             foreach $SolutionNameNotToPrint (@SolutionNamesNotToPrint) {
                 $indexThroughProblems = 0;
                 while (defined($SolutionLines[$indexThroughProblems])) {
                     if ($SolutionLines[$indexThroughProblems] =~ 
/^$SolutionNameNotToPrint/) {
                         $GoodSolutions[$indexThroughProblems] = 0; 
                     }
                     $indexThroughProblems++; 
                 }
             }

#DEBUG print("GoodSolutions After: @GoodSolutions\n"); 

#----Pass through GoodSolutions Array, and check to see that something 
#----is nonzero, and set SomeSolutionExists
            $SomeSolutionExists=0; 
            $indexThroughProblems = 0; 

            while(defined($GoodSolutions[$indexThroughProblems])) { 
                if ($GoodSolutions[$indexThroughProblems] > 0) {
                    $SomeSolutionExists = 1; 
                }
                $indexThroughProblems++; 
            }
#DEBUG print("Stack After: @ConstraintsStack\n");

#----In preparation for the meta-check (to see if the block, as a whole, 
#----satisfies the constraints), change every instance of "S:SystemNameRes:X"
#----to the value of X, so it may be passed to the LogicParser. 
            $SystemChecksResults = 1; 
            $SystemChecksIndex = 0;
            while (defined($CurrentConstraint = 
$ConstraintsStack[$SystemChecksIndex])) {
                 if ($CurrentConstraint =~ m/^S/) {
                     if ($CurrentConstraint =~ m/RES:0$/) {
                         $ConstraintsStack[$SystemChecksIndex] = 0;
                     } elsif ($CurrentConstraint =~ m/RES:[1-9][0-9]*$/) {
                         $ConstraintsStack[$SystemChecksIndex] = 1;
                     }
                 }
                 $SystemChecksIndex++; 
            }
#DEBUG print("Send to parser: @ConstraintsStack\n");            

#----Check the ConstraintsStack now for truthiness. 
            ($SystemChecksResults,$Garbage) = 
LogicParser("SOL",\@ConstraintsStack);

#----If some solution remains to be printed, and the solution block as a whole
#----satisfies the set of solution constraints provided, print:
            if (scalar(@GoodSolutions) == 0 || 
($SomeSolutionExists && $SystemChecksResults)) {
                if ($PrintOption eq "-pp" || $PrintOption eq "-pps") {
#----This prints the line before we tear it up into pieces
                    if (defined($ProblemLine)) {
                        if ($IdleFlag > 0 && $QuietnessOption le "-q1") {
                            print("\n"); 
                        }
                        print("$ProblemLine\n"); 
                        $IdleFlag = 0; 
                        $ProblemCounter++; 
                    }
                }
#----If solution lines are desired, go through the GoodSolutions array. 
#----For each entry that is nonzero, print the corresponding line. 
                if ($PrintOption eq "-ps" || $PrintOption eq "-pps") {
                    $indexThroughProblems = 0;

                    while (defined($GoodSolutions[$indexThroughProblems])) {
                        if ($GoodSolutions[$indexThroughProblems] > 0) {
                           print("   $SolutionLines[$indexThroughProblems]\n"); 
                           $IdleFlag = 0; 
                           $SolutionCounter++; 
                        }
                        $indexThroughProblems++; 
                    }    
                }   
            }                 
        }
#----Otherwise, if the problem was bad, or the solution block failed to meet
#----the desired constraints, we are not printing, so we sit idle. 
        if (!$GoodProblem || !$SystemChecksResults || !$SomeSolutionExists) {
            if ($QuietnessOption le "-q1") {
                if ($IdleFlag == 0) {
                    print("\%"); 
                }
                if ($IdleFlag > 0 && $IdleFlag % 200 == 0) {
                    if ($CurrentDomain ne $LastDomain) {
                        print("$CurrentDomain"); 
                        $LastDomain = $CurrentDomain; 
                    }
                        print("."); 
                } 
                $IdleFlag++; 
            }
        }
    }   


    if ($QuietnessOption le "-q2") {
        print(
"\n\% $ProblemCounter problems and $SolutionCounter solutions found\n"); 
    }

#----Close all the files
    close($StatisticsFileHandle); 
    close($ProblemListFileHandle);
    system("rm -f $SortedProblemFileName");
}
#------------------------------------------------------------------------------
#----GetNextProbleName gets the next problem name. Seriously.------------------
#------------------------------------------------------------------------------
sub GetNextProblemName {
    my ($ProblemListFileHandle) = @_;

    my $ProblemListLine;
    my $ProblemName;

    while (defined($ProblemListLine = <$ProblemListFileHandle>)) {
        chomp($ProblemListLine);
#DEBUG print("Looking at name line $ProblemListLine\n");
#----If its a line that specifies a problem or solution
        if ($ProblemListLine =~ /^[A-Z][A-Z][A-Z][0-9][0-9][0-9]/) {
#----Extract the problem name (this RE is real - no space at end for my file
#----lists)
            ($ProblemName) = ($ProblemListLine =~ /^([^ ]*)/);
#DEBUG print("Found name $ProblemName\n");
            return($ProblemName);
        }
    }
    return(undef);
}
#------------------------------------------------------------------------------
#----CreateConstraintsStack: Creates Logical Systems Construct-----------------
#------------------------------------------------------------------------------
sub CreateConstraintsStack {

    my ($ConstraintsRef,$ConstraintsStackRef) = @_; 
    my @ConstraintsArrayFROZEN = @$ConstraintsRef; 
    my @Constraints = @ConstraintsArrayFROZEN; 
    my @ConstraintsStack = @$ConstraintsStackRef; 

    my $ConstraintIndex; 

    my $LeftParen;
    my $RightParen; 

#----Go through the constraints provided. 
#----When you find a logical connector, just push it onto the stack. 
#----When you find a system constraint, prepend S: to the name of the system,
#----Then push it on the stack. 
#----If you find anything else, throw it away. 
    while (@Constraints) {
#DEBUG print ("Constraints Array: @Constraints\n"); 
        if (@Constraints[0] eq "and" || @Constraints[0] eq "or" ||
        @Constraints[0] eq "{" || @Constraints[0] eq "}") {
            push(@ConstraintsStack, shift(@Constraints)); 
        } elsif ($Constraints[0] =~ /system/i) {
            push(@ConstraintsStack, "S:@Constraints[1]"); 
            shift(@Constraints); 
        } else {
            shift(@Constraints);
        } 
   }

    $LeftParen = 0; 
    $RightParen = 0; 

    $ConstraintIndex = 0; 

#----Count the parenthesis, make sure they match. (This may be handled
#----by the shell...?)
    foreach $ConstraintIndex (@ConstraintsStack) {
        if ($ConstraintIndex eq "{") {
            $LeftParen++; 
        } elsif ($ConstraintIndex eq "}") {
            $RightParen++;
        }
    }

    unless ($LeftParen == $RightParen) {
        print("ERROR- USAGE: MISSMATCHED PARENTHESIS!"); 
        return(-99); 
    }

#DEBUG print("Important Systemchecks: @ConstraintsStack\n");

return(\@ConstraintsStack);  

}
#------------------------------------------------------------------------------
#----CheckConstraints Checks a set of Statistics against Constraints-----------
#------------------------------------------------------------------------------
sub CheckConstraints {
    my ($ProblemType,$SystemChecksArrayRef,$ConstraintsArrayRef,$StatisticsArrayRef,$ProblemStatisticsArrayRef) = @_;

    my @Constraints = @$ConstraintsArrayRef;
    my @SystemChecks = @$SystemChecksArrayRef;
    my $ConstraintsUsed;
    my $Result;
    my $ResultSave; 
    my $TempResult; 
    my $FinalResult = 0;
    my $ShiftIndex;
    my $GottenPastProblemConstraints = 0; 
    my $SystemChecksIndex = 0; 

    my $Garbage; 

    my @ConstraintsResultsStack; 
    my $ConstraintsResult;
    my @ConstraintsResultsStackTemp; 

#DEBUG print ("Statistics: @$StatisticsArrayRef\n"); 
    while (@Constraints) {
#DEBUG print ("Constraints Array: @Constraints\n"); 

#----For each constraint on the stack, if it's a logical constraint, just
#----Push it onto the new Constraints Results Stack. 
#----If it's a system constraint, push the name of the system with S: prepnded.
        while (@Constraints[0] eq "and" || @Constraints[0] eq "or" ||
        @Constraints[0] eq "{" || @Constraints[0] eq "}") {
            push(@ConstraintsResultsStack, shift(@Constraints)); 
        }
        if ($Constraints[0] =~ /system/i) {
            push(@ConstraintsResultsStack, "S:@Constraints[1]") or 
            die("Unmatched System Constraint");  
        } elsif (!@Constraints) {
#----CHANGE! Added a colon
            push(@ConstraintsResultsStack, "S:"); 
        }

#----Otherwise, check the constraint using CheckConstraint. 
        if (@Constraints) {
            ($ConstraintsUsed,$Result) = CheckConstraint(
$ProblemStatisticsArrayRef,$ProblemType,$StatisticsArrayRef,@Constraints);
#DEBUG print("ConstraintsUsed = $ConstraintsUsed Result = $Result\n");

#----Shift off the arguments used, then push the result onto the ResultsStack. 
            foreach $ShiftIndex (1..$ConstraintsUsed) {
                shift(@Constraints);
            }
            push(@ConstraintsResultsStack, $Result); 
        }
    }

#DEBUG print("Stack: @ConstraintsResultsStack\n"); 
#----Now that all the Constraints have been processed, if this is problem line,
    if ($ProblemType ne "SOL") { 
        @ConstraintsResultsStackTemp = (); 
        $Result = shift(@ConstraintsResultsStack); 

#----Go through the array, get rid of all the System Constraints (set to 1).
        if ($Result =~ m/^S:/) {
            push(@ConstraintsResultsStackTemp,"1"); 
        } else {
            while ($Result !~ m/^S:/ && defined($Result)) {
                push(@ConstraintsResultsStackTemp,$Result); 
                $Result = shift(@ConstraintsResultsStack); 
            }
        }
#DEBUG print("Thing to check for logic: @ConstraintsResultsStackTemp\n"); 
        ($FinalResult,$Garbage) = LogicParser($ProblemType,\@ConstraintsResultsStackTemp);
#DEBUG print("FinalResult on that: $FinalResult\n"); 
#----Otherwise, we're at a system line
    } else {

        $ResultSave = 0; 
#DEBUG print("ConstraintsResults Before anything: @ConstraintsResultsStack\n");  

        $Result = shift(@ConstraintsResultsStack);
        while ($Result !~ m/^S/ && @ConstraintsResultsStack) {
            $Result = shift(@ConstraintsResultsStack); 
        }
#DEBUG print("ConstraintsResults sans problem stuff: @ConstraintsResultsStack and Res is $Result\n");  

#----If there are no solution constraints, then we print everything.
        if (!@ConstraintsResultsStack) {
            return(1,\@SystemChecks); 
        }

        $ResultSave = $Result; 
        $Result = shift(@ConstraintsResultsStack);  

#---Otherwise, we start consoldating the Results
        while (defined($Result)) {

            @ConstraintsResultsStackTemp = (); 
            
            while ($Result !~ /^S/ && ~(($Result eq "and" || $Result eq "or" || $Result eq "{" || $Result eq "}") && $ConstraintsResultsStack[0] =~ /^S/) && @ConstraintsResultsStack) {
                push(@ConstraintsResultsStackTemp,$Result); 
                $Result = shift(@ConstraintsResultsStack); 
            }

            if (!@ConstraintsResultsStack) {
                push(@ConstraintsResultsStackTemp,$Result); 
            }

            if ($ResultSave) {

#DEBUG print("Piece of Stack in focus: @ConstraintsResultsStackTemp\n"); 
                $Garbage = pop(@ConstraintsResultsStackTemp); 

                while (($Garbage eq "and" || $Garbage eq "or" || $Garbage eq "{" || $Garbage eq "}" || $Garbage eq "S") && @ConstraintsResultsStackTemp) {
#DEBUG print("Found some garbage at end of stack: $Garbage\n"); 
                    $Garbage = pop(@ConstraintsResultsStackTemp); 
                }

                push(@ConstraintsResultsStackTemp,$Garbage); 

#DEBUG print("Const: @ConstraintsResultsStackTemp\n");                 
#----Once you've found everything up to the next System Constraint, 
#----Pass it to the Logic Parser, and save the result. 
                ($TempResult,$Garbage) = LogicParser($ProblemType,\@ConstraintsResultsStackTemp); 
                if ($TempResult) {
                    $FinalResult = $TempResult; 
                }

                $SystemChecksIndex = 0; 
                while (defined(@SystemChecks[$SystemChecksIndex])) {
#DEBUG print("SysChecks: @SystemChecks,Ressave is  $ResultSave and $TempResult\n"); 
                    if (@SystemChecks[$SystemChecksIndex] eq $ResultSave && $TempResult > 0) {
                        @SystemChecks[$SystemChecksIndex] = $ResultSave."RES:".$TempResult; 
                    }
                    $SystemChecksIndex++; 
                }
#DEBUG print("Check for logic: @ConstraintsResultsStackTemp , match to $ResultSave in SysChecks\n");
#DEBUG print("ResultTemp: $TempResult and Finalresult: $FinalResult\n");  
            }
            $ResultSave = $Result; 
            $Result = shift(@ConstraintsResultsStack);  
        }
    }
#DEBUG print("Stack: @ConstraintsResultsStack\n"); 
#DEBUG print("SystemChecks: @SystemChecks\n"); 
#DEBUG print("FinalResult = $FinalResult\n"); 

    if ($FinalResult == -99) {
        return(-99,\@SystemChecks); 
    } elsif ($FinalResult == 7) {
        return(7,\@SystemChecks); 
    } elsif ($FinalResult >= 1) {
        $FinalResult = 1; 
    }    

#DEBUG print("Final: $FinalResult\n"); 

    return($FinalResult,\@SystemChecks);
}
#------------------------------------------------------------------------------
#----LogicParser: Parse a stack of logical operators and parethesis
#------------------------------------------------------------------------------
sub LogicParser {
    my ($ProblemType,$ConstraintsResultsStackRef) = @_; 

    my @ConstraintsResultsStack = @$ConstraintsResultsStackRef;  
    my $FinalResult = 1; 
    my $CurrentResult; 
    my $FinalResultHolder; 
    my $ConstraintsResultsStackRef; 

    while(@ConstraintsResultsStack) {
#DEBUG print("Current Results Stack:@ConstraintsResultsStack\n"); 
        $CurrentResult = shift(@ConstraintsResultsStack); 
#DEBUG print("Current Result : $CurrentResult\n"); 
#DEBUG print("At the top: Look: $CurrentResult\n"); 

        if ($CurrentResult eq "or") {
#DEBUG print("In the or\n"); 
            $CurrentResult = shift(@ConstraintsResultsStack); 
#DEBUG print("Grab next: $CurrentResult\n"); 
            if ($CurrentResult =~ /^[+-]?\d+$/) {
                if ($CurrentResult == -99) {
                    $FinalResult += 0; 
                } else {
                    $FinalResult += $CurrentResult; 
                }
            } elsif ($CurrentResult eq "{") {
                ($FinalResultHolder,$ConstraintsResultsStackRef) = LogicParser($ProblemType,\@ConstraintsResultsStack);
                @ConstraintsResultsStack = @$ConstraintsResultsStackRef; 
                $FinalResult += $FinalResultHolder; 
#DEBUG print("After recursing, here's where we're at: @ConstraintsResultsStack , and CurrentRes is $CurrentResult\n"); 
            } elsif ($CurrentResult eq "}") {
                return ($FinalResult); 
            }
        } elsif ($CurrentResult eq "and") {
            $CurrentResult = shift(@ConstraintsResultsStack); 
           if ($CurrentResult =~ /^[+-]?\d+$/) {
                if ($CurrentResult == -99) {
                    $FinalResult = -99; 
                } else {
                    $FinalResult *= $CurrentResult; 
                }
            } elsif ($CurrentResult eq "{") {
                ($FinalResultHolder,$ConstraintsResultsStackRef) = LogicParser($ProblemType,\@ConstraintsResultsStack);
                @ConstraintsResultsStack = @$ConstraintsResultsStackRef; 
                $FinalResult *= $FinalResultHolder; 
#DEBUG print("After recursing, here's where we're at: @ConstraintsResultsStack , and CurrentRes is $CurrentResult\n"); 
            } elsif ($CurrentResult eq "}") {
                return ($FinalResult); 
            } 
        } elsif ($CurrentResult eq "{") {
            ($FinalResultHolder,$ConstraintsResultsStackRef) = LogicParser($ProblemType,\@ConstraintsResultsStack); 
            @ConstraintsResultsStack = @$ConstraintsResultsStackRef; 
            $FinalResult *= $FinalResultHolder; 
#DEBUG print("After recursing, here's where we're at: @ConstraintsResultsStack , and CurrentRes is $CurrentResult\n"); 

        } elsif ($CurrentResult eq "}") {
            return ($FinalResult,\@ConstraintsResultsStack); 
        } else {
            $FinalResult *= $CurrentResult; 
        }

#DEBUG print("End of function: $FinalResult\n"); 
    } 
#DEBUG print("End of sub: $FinalResult\n"); 
    return ($FinalResult,\@ConstraintsResultsStack); 
}
#------------------------------------------------------------------------------
#----CheckConstraint: Remove negation
#------------------------------------------------------------------------------
sub CheckConstraint {
    my ($ProblemStatisticsArrayRef,$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(
$ProblemStatisticsArrayRef,$ProblemType,$StatisticsArrayRef,$Constraint,
@RestOfConstraints);
#DEBUG print("Result: $Result, where Constraint was $Constraint\n"); 
    if ($Result < 0) {
        if ($Result == -99) {
            if ($Negated) {
                return($ConstraintsUsed,1); 
            } else {
                return($ConstraintsUsed,-99); 
            }
        }
        return($ConstraintsUsed,1); 
    } elsif ($Result == 7) { 
        if ($Negated) {
            return($ConstraintsUsed,0); 
        } else { 
            return($ConstraintsUsed,7); 
        }
    } else {
        return($ConstraintsUsed,abs($Result - $Negated));
    }
}
#------------------------------------------------------------------------------
#----CheckUnnegatedConstraint: Return TRUE or FALSE to query based on stats. 
#------------------------------------------------------------------------------
sub CheckUnnegatedConstraint {
    my ($ProblemStatisticsArrayRef,$ProblemType,$StatisticsArrayRef,$Constraint,@RestOfConstraints) = @_;

    my $ArgumentsUsed;
    my @ArgumentsUsedArray; 

#DEBUG print("Constraint: $Constraint\n");
#DEBUG print("    Values: @RestOfConstraints\n");
#DEBUG print("Statistics: @$StatisticsArrayRef\n");
#DEBUG print("ProbStats : @$ProblemStatisticsArrayRef\n");
#----Return number of arguments used and result. Always need number used.

    if ($Constraint =~ /^Form$/i) {
        return(2,CheckForm($ProblemType,$StatisticsArrayRef,$RestOfConstraints[0])); 
    }
    if ($Constraint =~ /^Domain/i) {
        @ArgumentsUsedArray = Domains($ProblemType,$StatisticsArrayRef,
@RestOfConstraints);        
        return(($ArgumentsUsedArray[0])+1,$ArgumentsUsedArray[1]);
    }
    if ($Constraint =~ /^Version/i) {
        return(2,CheckVersion($ProblemType,$StatisticsArrayRef,$RestOfConstraints[0])); 
    }
    if ($Constraint =~ /^Rating/i)            { 
        return(3,Rating($ProblemType,$StatisticsArrayRef,$RestOfConstraints[0],
$RestOfConstraints[1])); 
    }
    if ($Constraint =~ /^Status/i) {
        return(2,CheckStatus($ProblemType,$StatisticsArrayRef,$RestOfConstraints[0])); 
    }
    if ($Constraint =~ /^Clause/i) {
        return(3,Clauses($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1]));
    }
    if ($Constraint =~ /^UnitFormula/i) {
        return(3,UnitFormulae($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1])); 
    }
    if ($Constraint =~ /^UnitClause/i) {
        return(3,UnitClauses($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1])); 
    }
    if ($Constraint =~ /^Atoms/i) {
        return(3,Atoms($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1]));
    }
    if ($Constraint =~ /^Eq.*Atoms/i) {
        return(3,EqualityAtoms($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1]));
    }
    if ($Constraint =~ /^Ari.*Sym/i) {
        return(3,ArithmeticSymbols($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1]));
    }
    if ($Constraint =~ /^Formula/i) {
        return(3,Formulae($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1])); 
    }
    if ($Constraint =~ /^NonHornClause/i) {
        return(3,NonHornClauses($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1]));
    }
    if ($Constraint =~ /^Predicate/i || $Constraint =~ /^Symbol/i)            { 
        return(3,Predicates($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1])); 
    }
    if ($Constraint =~ /^Propositional/i) {
        return(1,Propositional($ProblemType,$StatisticsArrayRef));
    }
    if ($Constraint =~ /^Variables/i) {
        return(1,Variables($ProblemType,$StatisticsArrayRef));
    }
    if ($Constraint =~ /^Min.*Pred.*Arity/i ||
$Constraint =~ /^Min.*Symb.*Arity/i) {
        return(3,MinimalPredicateArity($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1]));
    }
    if ($Constraint =~ /^Max.*Pred.*Arity/i ||
$Constraint =~ /^Max.*Symb.*Arity/i) {
        return(3,MaximalPredicateArity($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1]));
    }
    if ($Constraint =~ /^Av.*Atoms/i) {
        return(3,AverageAtoms($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1]));
    }
    if ($ProblemType ne "SOL" && $Constraint =~ /^Equality/i) {
        return(1,Equality($ProblemType,$StatisticsArrayRef));
    }
    if ($ProblemType ne "SOL" && $Constraint =~ /^Arithmetic/i) {
        return(1,Arithmetic($ProblemType,$StatisticsArrayRef));
    }
    if ($ProblemType ne "SOL" && $Constraint =~ /^PureEq/i) {
        return(1,PureEquality($ProblemType,$StatisticsArrayRef));
    }
    if ($Constraint =~ /^Function/i)            { 
        return(3,Functions($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1])); 
    }
    if ($Constraint =~ /^Min.*Func.*Arity/i) {
        return(3,MinimalFunctionArity($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1]));
    }
    if ($Constraint =~ /^Max.*Func.*Arity/i) {
        return(3,MaximalFunctionArity($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1]));
    }
    if ($Constraint =~ /^Horn/i) {
        return(1,Horn($ProblemType,$StatisticsArrayRef));
    }
    if ($Constraint =~ /^NonHorn$/i) {
        return(1,NonHorn($ProblemType,$StatisticsArrayRef));
    }
    if ($Constraint =~ /^RangeRestricted/i) {
        return(1,RangeRestricted($ProblemType,$StatisticsArrayRef));
    }
    if ($Constraint =~ /^RRClause/i) {
        return(3,RRClauses($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1])); 
    }
    if ($Constraint =~ /^Av.*Literal/i) {
        return(3,AverageLiterals($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1]));
    }
    if ($Constraint =~ /^UnitEq/i) {
        return(1,UnitEquality($ProblemType,$StatisticsArrayRef));
    }

#----SOLUTION CONDITIONS---------------------------------------
    if ($Constraint =~ /^System/i) {
        return(2,System($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0])); 
    }
    if ($Constraint =~ /^ResultTime/i) {
        return(3,ResultTime($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1])); 
    }
    if ($Constraint =~ /^Result$/i) {
        return(2,Result($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0])); 
    }
    if ($Constraint =~ /^Output/i) {
        return(2,Output($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0])); 
    }
    if ($Constraint =~ /^Sol.*Depth/i) {
        return(3,SolutionDepth($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1])); 
    }
    if ($Constraint =~ /^Sol.*Formul/i) {
        return(3,SolutionFormulae($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1])); 
    }
    if ($Constraint =~ /^Sol.*Clauses/i) {
        return(3,SolutionClauses($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1])); 
    }
    if ($Constraint =~ /^Sol.*Leave/i) {
        return(3,SolutionLeaves($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1])); 
    }
    if ($ProblemType eq "SOL" && $Constraint =~ /^Equality/i) {
        return(1,SolutionEquality($ProblemType,$StatisticsArrayRef));
    }
    if ($ProblemType eq "SOL" && $Constraint =~ /^PureEq/i) {
        return(1,SolutionPureEquality($ProblemType,$StatisticsArrayRef));
    }
    if ($Constraint =~ /^Sol.*Eq.*Atoms/i) {
        return(3,SolutionEqualityAtoms($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1]));
    }
    if ($Constraint =~ /^Selectivity/i) {
        return(3,Selectivity($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1],$ProblemStatisticsArrayRef)); 
    }
    if ($Constraint =~ /^Girth/i) {
        return(3,Girth($ProblemType,$StatisticsArrayRef,
$RestOfConstraints[0],$RestOfConstraints[1])); 
    }

#----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;
    my $domainIndex; 
    my $greaterThanEverything; 
    
#----Get domains off constraint list
    while ($Constraints[$NumberOfDomains] =~ /^[A-Z]{3}$/) {
        $Domains[$NumberOfDomains] = $Constraints[$NumberOfDomains];
        $NumberOfDomains++;
    }

    if ($ProblemType eq "SOL") {
            return($NumberOfDomains,-1);
    }

    $ProblemDomain = $$StatisticsArrayRef[$ProblemIndexHash{'Domain'}];

    if (grep(/$ProblemDomain/,@Domains)) {
        return($NumberOfDomains,1);
    } else {
        $domainIndex = 0; 
        $greaterThanEverything = 1; 
        while (defined($Domains[$domainIndex])) {
            if ($ProblemDomain lt $Domains[$domainIndex]) {
                $greaterThanEverything = 0;
            } 
            $domainIndex++; 
        }

        if ($greaterThanEverything == 0) {
            return($NumberOfDomains,0);
        } else {
           return($NumberOfDomains,-99);  
        }

    }
}
#------------------------------------------------------------------------------
sub CheckVersion {
    my ($ProblemType,$StatisticsArrayRef,$CheckString) = @_; 
    
    if ($ProblemType eq "SOL") {
        return(-1);
    }

    my $AbreviatedConstraint = $AbbreviationHash{$CheckString}; 
    if (defined($AbreviatedConstraint)) {
        $CheckString = $AbreviatedConstraint; 
    }
 
    if ($CheckString =~ /^stan/i) { 
        return(Standard($ProblemType,$StatisticsArrayRef)); 
    }
    if ($CheckString =~ /^incom/i || $CheckString =~ /^INC/i) {
        return(Incomplete($ProblemType,$StatisticsArrayRef));
    }
    if ($CheckString =~ /^augm/i) {
        return(Augmented($ProblemType,$StatisticsArrayRef));
    }
    if ($CheckString =~ /^espec/i) {
        return(Especial($ProblemType,$StatisticsArrayRef));
    }
    if ($CheckString =~ /^bias/i) {
        return(Biased($ProblemType,$StatisticsArrayRef));
    }
}
#------------------------------------------------------------------------------
sub Standard { 
    my ($ProblemType,$StatisticsArrayRef) = @_;

    if ($ProblemType eq "SOL") {
        return(-1); 
    }

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

    if ($ProblemType eq "SOL") {
        return(-1);
    }

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

    if ($ProblemType eq "SOL") {
        return(-1);
    }

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

    if ($ProblemType eq "SOL") {
        return(-1);
    }

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

    if ($ProblemType eq "SOL") {
        return(-1);
    }

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

    if ($ProblemType eq "SOL") {
        return(-1);
    }

    $Rating = $$StatisticsArrayRef[$ProblemIndexHash{'Rating'}];

    return(($Rating ne "?") && ExceptionCheck($Rating,$LowerBound,$UpperBound)); 
}
#------------------------------------------------------------------------------
sub CheckStatus {
    my ($ProblemType,$StatisticsArrayRef,$CheckString) = @_; 
    
    my $AbreviatedConstraint;

    if ($ProblemType eq "SOL") {
        return(-1);
    }

    $AbreviatedConstraint = $AbbreviationHash{$CheckString}; 
    if (defined($AbreviatedConstraint)) {
        $CheckString = $AbreviatedConstraint; 
    }
    if ($CheckString =~ /^THM/i) {
        return(Theorem($ProblemType,$StatisticsArrayRef));
    }
    if ($CheckString =~ /^CSA/i) {
        return(CounterSatisfiable($ProblemType,$StatisticsArrayRef));
    }
    if ($CheckString =~ /^SAT/i) {
        return(Satisfiable($ProblemType,$StatisticsArrayRef));
    }
    if ($CheckString =~ /^UNS/i) {
        return(Unsatisfiable($ProblemType,$StatisticsArrayRef));
    }
    if ($CheckString =~ /^UNK/i) {
        return(Unknown($ProblemType,$StatisticsArrayRef));
    }
    if ($CheckString =~ /^OPN/i) {
        return(Open($ProblemType,$StatisticsArrayRef));
    } 
}
#------------------------------------------------------------------------------
sub Theorem { 
    my ($ProblemType,$StatisticsArrayRef) = @_;

    if ($ProblemType eq "SOL") {
        return(-1);
    }

    return(($ProblemType eq "THF" || $ProblemType eq "TFF" ||
$ProblemType eq "FOF") && 
$$StatisticsArrayRef[$ProblemIndexHash{'Status'}] eq "THM");
}
#------------------------------------------------------------------------------
sub CounterSatisfiable { 
my ($ProblemType,$StatisticsArrayRef) = @_;

    if ($ProblemType eq "SOL") {
        return(-1);
    }

    return(($ProblemType eq "THF" || $ProblemType eq "TFF" ||
$ProblemType eq "FOF") && 
$$StatisticsArrayRef[$ProblemIndexHash{'Status'}] eq "CSA");
}
#------------------------------------------------------------------------------
sub Unsatisfiable { 
    my ($ProblemType,$StatisticsArrayRef) = @_;

    if ($ProblemType eq "SOL") {
        return(-1);
    }

    return($$StatisticsArrayRef[$ProblemIndexHash{'Status'}] eq "UNS");
}
#------------------------------------------------------------------------------
sub Satisfiable { 
    my ($ProblemType,$StatisticsArrayRef) = @_;

    if ($ProblemType eq "SOL") {
        return(-1);
    }

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

    if ($ProblemType eq "SOL") {
        return(-1);
    }

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

    if ($ProblemType eq "SOL") {
        return(-1);
    }

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

    if ($ProblemType eq "SOL") {
        return(-1);
    }

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

    if ($ProblemType eq "SOL") {
        return(-1);
    }

    return($$StatisticsArrayRef[$ProblemIndexHash{'Predicates'}] == 
$$StatisticsArrayRef[$ProblemIndexHash{'Propositions'}]);
}
#------------------------------------------------------------------------------
sub Variables {
    my ($ProblemType,$StatisticsArrayRef) = @_;

    if ($ProblemType eq "SOL") {
        return(-1);
    }

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

    my $MinimalArity;

    if ($ProblemType eq "SOL") {
        return(-1);
    }

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

    my $MaximalArity;

    if ($ProblemType eq "SOL") {
        return(-1);
    }

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

    if ($ProblemType eq "SOL") {
        return(-1);
    }

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

    if ($ProblemType eq "SOL") {
        return(-1);
    }

    return(Equality($ProblemType,$StatisticsArrayRef) &&
$$StatisticsArrayRef[$ProblemIndexHash{'Atoms'}] == 
$$StatisticsArrayRef[$ProblemIndexHash{'EqualityAtoms'}]);
}
#------------------------------------------------------------------------------
sub Arithmetic { 
    my ($ProblemType,$StatisticsArrayRef) = @_;

    if ($ProblemType eq "SOL") {
        return(-1);
    }

    return($$StatisticsArrayRef[$ProblemIndexHash{'ArithmeticSymbols'}] > 0);
}
#------------------------------------------------------------------------------
sub Functions { 
    my ($ProblemType,$StatisticsArrayRef,$LowerBound,$UpperBound) = @_;
    my $Functions = 0; 

    if ($ProblemType eq "SOL") {
        return(-1);
    }

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

    my $MinimalArity;

    if ($ProblemType eq "SOL") {
        return(-1);
    }

    if ($$StatisticsArrayRef[$ProblemIndexHash{'FunctionArities'}] eq "---") {
        $MinimalArity = -1;
    } else {
        ($MinimalArity) = 
($$StatisticsArrayRef[$ProblemIndexHash{'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 ($ProblemType eq "SOL") {
        return(-1);
    }

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

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

#DEBUG print("ProblemType  $ProblemType    CheckString $CheckString\n");
    if ($ProblemType eq "SOL") {
        return(-1);
    }

    if ($CheckString eq "ANY") {
        return(1); 
    }

    return ($ProblemType eq $CheckString); 
}
#------------------------------------------------------------------------------
sub Formulae {
    my ($ProblemType,$StatisticsArrayRef,$LowerBound,$UpperBound) = @_; 
    my $NoOfFormulae = 0; 

    if ($ProblemType eq "SOL") {
        return(-1);
    }

    $NoOfFormulae = $$StatisticsArrayRef[$ProblemIndexHash{'Formulae'}];
    return(ExceptionCheck($NoOfFormulae,$LowerBound,$UpperBound)); 
}
#------------------------------------------------------------------------------
sub Clauses {
    my ($ProblemType,$StatisticsArrayRef,$LowerBound,$UpperBound) = @_; 
    my $NoOfClauses = 0; 

    if ($ProblemType eq "SOL") {
        return(-1);
    }

    $NoOfClauses = $$StatisticsArrayRef[$ProblemIndexHash{'Clauses'}];
    return(ExceptionCheck($NoOfClauses,$LowerBound,$UpperBound)); 
}
#------------------------------------------------------------------------------
sub UnitFormulae {
    my ($ProblemType,$StatisticsArrayRef,$LowerBound,$UpperBound) = @_; 
    my $NoOfUnitFormulae = 0; 

    if ($ProblemType eq "SOL") {
        return(-1);
    }

    $NoOfUnitFormulae = $$StatisticsArrayRef[$ProblemIndexHash{'UnitFormulae'}];
    return(ExceptionCheck($NoOfUnitFormulae,$LowerBound,$UpperBound)); 
}
#------------------------------------------------------------------------------
sub UnitClauses {
    my ($ProblemType,$StatisticsArrayRef,$LowerBound,$UpperBound) = @_; 
    my $NoOfUnitClauses = 0; 

    if ($ProblemType eq "SOL") {
        return(-1);
    }

    $NoOfUnitClauses = $$StatisticsArrayRef[$ProblemIndexHash{'UnitClauses'}];
    return(ExceptionCheck($NoOfUnitClauses,$LowerBound,$UpperBound)); 
}
#------------------------------------------------------------------------------
sub AverageAtoms {
    my ($ProblemType,$StatisticsArrayRef,$LowerBound,$UpperBound) = @_;
    my $Atoms = 0; 
    my $Formulae = 0; 

    if ($ProblemType eq "SOL") {
        return(-1);
    }

    $Atoms = $$StatisticsArrayRef[$ProblemIndexHash{'Atoms'}];
    $Formulae = $$StatisticsArrayRef[$ProblemIndexHash{'Formulae'}]; 

    if ($Formulae < 1) {
        return(0); 
    }
    
    return(ExceptionCheck($Atoms/$Formulae,$LowerBound,$UpperBound)); 
}
#------------------------------------------------------------------------------
sub RRClauses {
    my ($ProblemType,$StatisticsArrayRef,$LowerBound,$UpperBound) = @_; 
    my $NoOfRRClauses = 0; 

    if ($ProblemType eq "SOL") {
        return(-1);
    }

    $NoOfRRClauses = $$StatisticsArrayRef[$ProblemIndexHash{'RRClauses'}];
    return(ExceptionCheck($NoOfRRClauses,$LowerBound,$UpperBound)); 
}
#------------------------------------------------------------------------------
sub Atoms {
    my ($ProblemType,$StatisticsArrayRef,$LowerBound,$UpperBound) = @_; 
    my $NoOfAtoms = 0; 

    if ($ProblemType eq "SOL") {
        return(-1);
    }

    $NoOfAtoms = $$StatisticsArrayRef[$ProblemIndexHash{'Atoms'}];
    return(ExceptionCheck($NoOfAtoms,$LowerBound,$UpperBound)); 
}
#------------------------------------------------------------------------------
sub EqualityAtoms {
    my ($ProblemType,$StatisticsArrayRef,$LowerBound,$UpperBound) = @_; 
    my $NoOfEqualityAtoms = 0; 

    if ($ProblemType eq "SOL") {
        return(-1);
    }

    $NoOfEqualityAtoms = $$StatisticsArrayRef[$ProblemIndexHash{'EqualityAtoms'}];
    return(ExceptionCheck($NoOfEqualityAtoms,$LowerBound,$UpperBound)); 
}
#------------------------------------------------------------------------------
sub ArithmeticSymbols {
    my ($ProblemType,$StatisticsArrayRef,$LowerBound,$UpperBound) = @_; 
    my $NoOfArithmeticSymbols = 0; 

    if ($ProblemType eq "SOL") {
        return(-1);
    }

    $NoOfArithmeticSymbols = 
$$StatisticsArrayRef[$ProblemIndexHash{'ArithmeticSymbols'}];
    return(ExceptionCheck($NoOfArithmeticSymbols,$LowerBound,$UpperBound)); 
}
#------------------------------------------------------------------------------
#==============================================================================
#----CNF only constraints
#==============================================================================
#------------------------------------------------------------------------------
sub Horn { 
    my ($ProblemType,$StatisticsArrayRef) = @_;

    if ($ProblemType eq "SOL") {
        return(-1);
    }

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

    if ($ProblemType eq "SOL") {
        return(-1);
    }

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

    if ($ProblemType eq "SOL") {
        return(-1);
    }

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

    if ($ProblemType eq "SOL") {
        return(-1);
    }

    $AverageLiterals = $$StatisticsArrayRef[$ProblemIndexHash{'AvLiterals'}];
    return(ExceptionCheck($AverageLiterals,$LowerBound,$UpperBound)); 
}
#------------------------------------------------------------------------------
sub UnitEquality {
    my ($ProblemType,$StatisticsArrayRef) = @_;

    if ($ProblemType eq "SOL") {
        return(-1);
    }

    return($ProblemType eq "CNF" && 
PureEquality($ProblemType,$StatisticsArrayRef) &&
$$StatisticsArrayRef[$ProblemIndexHash{'Clauses'}] == 
$$StatisticsArrayRef[$ProblemIndexHash{'UnitClauses'}]);
}
#------------------------------------------------------------------------------
sub NonHornClauses {
    my ($ProblemType,$StatisticsArrayRef,$LowerBound,$UpperBound) = @_; 
    my $NonHornClauses = 0; 

    if ($ProblemType eq "SOL") {
        return(-1);
    }

    $NonHornClauses = $$StatisticsArrayRef[$ProblemIndexHash{'NonHornClauses'}];
    return(($ProblemType eq "CNF") && (ExceptionCheck($NonHornClauses,$LowerBound,$UpperBound))); 
}
#------------------------------------------------------------------------------
#==============================================================================
#----SOL only constraints
#==============================================================================
#------------------------------------------------------------------------------
sub System {
    my ($ProblemType,$StatisticsArrayRef,$CheckString) = @_;

    my $SolutionName; 
    if ($ProblemType ne "SOL") {
        return(-1); 
    }

    $SolutionName = $$StatisticsArrayRef[$SolutionIndexHash{'SystemName'}]; 

    if ($CheckString =~ /^ANY/) {
        return(7); 
    }
#DEBUG print("$SolutionName is solution name, $CheckString is check string here. Should it return?"); 

    return($SolutionName =~ /^$CheckString/i)
}
#-----------------------------------------------------------------------------
sub Result {
    my ($ProblemType,$StatisticsArrayRef,$CheckString) = @_; 
    
    my $AbreviatedConstraint;

    if ($ProblemType ne "SOL") {
        return(-1);
    }

    $AbreviatedConstraint = $AbbreviationHash{$CheckString}; 
    if (defined($AbreviatedConstraint)) {
        $CheckString = $AbreviatedConstraint; 
    }     
    
    if ($CheckString eq "SUC") {
        return(
($$StatisticsArrayRef[$SolutionIndexHash{'Result'}] eq "SUC") ||
Result($ProblemType,$StatisticsArrayRef,"THM") ||
Result($ProblemType,$StatisticsArrayRef,"CSA") ||
Result($ProblemType,$StatisticsArrayRef,"SAT") ||
Result($ProblemType,$StatisticsArrayRef,"UNS")
        );
    } elsif ($CheckString eq "NOS") {
        return(
($$StatisticsArrayRef[$SolutionIndexHash{'Result'}] eq "NOS") ||
Result($ProblemType,$StatisticsArrayRef,"TMO") ||
Result($ProblemType,$StatisticsArrayRef,"GUP") ||
Result($ProblemType,$StatisticsArrayRef,"ERR") ||
Result($ProblemType,$StatisticsArrayRef,"UNK")
        );
    } else {
        return($$StatisticsArrayRef[$SolutionIndexHash{'Result'}] eq 
$CheckString); 
    }
}
#-----------------------------------------------------------------------------
sub ResultTime {
    my ($ProblemType,$StatisticsArrayRef,$LowerBound,$UpperBound) = @_;
    my $ResultTime = 0; 

    if ($ProblemType ne "SOL") {
        return(-1); 
    }
    
    $ResultTime = $$StatisticsArrayRef[$SolutionIndexHash{'ResultTime'}];

    return(ExceptionCheck($ResultTime,$LowerBound,$UpperBound)); 
}
#-----------------------------------------------------------------------------
sub Output {
    my ($ProblemType,$StatisticsArrayRef,$CheckString) = @_; 
    
    my $AbreviatedConstraint;

    if ($ProblemType ne "SOL") {
        return(-1); 
    }

    $AbreviatedConstraint = $AbbreviationHash{$CheckString}; 
    if (defined($AbreviatedConstraint)) {
        $CheckString = $AbreviatedConstraint; 
    }

    if ($CheckString eq "Sol") {
        return(
($$StatisticsArrayRef[$SolutionIndexHash{'Output'}] eq "Sol") ||
Output($ProblemType,$StatisticsArrayRef,"Prf") ||
Output($ProblemType,$StatisticsArrayRef,"Mod")
        );
    } elsif ($CheckString eq "Prf") {
        return(
($$StatisticsArrayRef[$SolutionIndexHash{'Output'}] eq "Prf") ||
Output($ProblemType,$StatisticsArrayRef,"Ref")
        );
    } elsif ($CheckString eq "Ref") {
        return(
($$StatisticsArrayRef[$SolutionIndexHash{'Output'}] eq "Ref") ||
Output($ProblemType,$StatisticsArrayRef,"CRf")
        );
    } elsif ($CheckString eq "Mod") {
        return(
($$StatisticsArrayRef[$SolutionIndexHash{'Output'}] eq "Mod") ||
Output($ProblemType,$StatisticsArrayRef,"FMo") ||
Output($ProblemType,$StatisticsArrayRef,"Sat") 
        );
    } else {
        return($$StatisticsArrayRef[$SolutionIndexHash{'Output'}] eq 
$CheckString); 
    }
}
#-----------------------------------------------------------------------------
sub SolutionFormulae {

    my ($ProblemType,$StatisticsArrayRef,$LowerBound,$UpperBound) = @_; 
    my $NoOfFormulae = 0; 

    if ($ProblemType ne "SOL") {
        return(-1); 
    }

    $NoOfFormulae = $$StatisticsArrayRef[$SolutionIndexHash{'SolutionFormulae'}];
    return(ExceptionCheck($NoOfFormulae,$LowerBound,$UpperBound)); 
}
#-----------------------------------------------------------------------------
sub SolutionClauses {

    my ($ProblemType,$StatisticsArrayRef,$LowerBound,$UpperBound) = @_; 
    my $NoOfClauses = 0; 

    if ($ProblemType ne "SOL") {
        return(-1); 
    }
    
    $NoOfClauses = $$StatisticsArrayRef[$SolutionIndexHash{'SolutionClauses'}];
    return(ExceptionCheck($NoOfClauses,$LowerBound,$UpperBound)); 
}
#-----------------------------------------------------------------------------
sub SolutionDepth {

    my ($ProblemType,$StatisticsArrayRef,$LowerBound,$UpperBound) = @_; 
    my $Depth = 0; 

    if ($ProblemType ne "SOL") {
        return(-1); 
    }

    $Depth = $$StatisticsArrayRef[$SolutionIndexHash{'SolutionDepth'}];
    return(ExceptionCheck($Depth,$LowerBound,$UpperBound)); 
}
#-----------------------------------------------------------------------------
sub SolutionLeaves {

    my ($ProblemType,$StatisticsArrayRef,$LowerBound,$UpperBound) = @_; 
    my $NoOfLeaves = 0; 

    if ($ProblemType ne "SOL") {
        return(-1); 
    }

    $NoOfLeaves = $$StatisticsArrayRef[$SolutionIndexHash{'SolutionLeaves'}];
    return(ExceptionCheck($NoOfLeaves,$LowerBound,$UpperBound)); 
}
#-----------------------------------------------------------------------------
sub SolutionEquality { 
    my ($ProblemType,$StatisticsArrayRef) = @_;

    if ($ProblemType ne "SOL") {
        return(-1);
    }

    return($$StatisticsArrayRef[$SolutionIndexHash{'SolutionEqualityAtoms'}] > 0);
}
#------------------------------------------------------------------------------
sub SolutionPureEquality { 
    my ($ProblemType,$StatisticsArrayRef) = @_;

    if ($ProblemType ne "SOL") {
        return(-1);
    }

    return(SolutionEquality($ProblemType,$StatisticsArrayRef) &&
$$StatisticsArrayRef[$SolutionIndexHash{'SolutionAtoms'}] == 
$$StatisticsArrayRef[$SolutionIndexHash{'SolutionEqualityAtoms'}]);
}
#------------------------------------------------------------------------------
sub SolutionEqualityAtoms {
    my ($ProblemType,$StatisticsArrayRef,$LowerBound,$UpperBound) = @_; 
    my $NoOfEqualityAtoms = 0; 

    if ($ProblemType ne "SOL") {
        return(-1);
    }

    $NoOfEqualityAtoms = $$StatisticsArrayRef[$SolutionIndexHash{'SolutionEqualityAtoms'}];
    return(ExceptionCheck($NoOfEqualityAtoms,$LowerBound,$UpperBound)); 
}
#-----------------------------------------------------------------------------
sub Selectivity {
    my ($ProblemType,$StatisticsArrayRef,$LowerBound,
$UpperBound,$ProblemStatisticsArrayRef) = @_; 

    my $Leaves;
    my $Formulae; 
    my $OriginalProblemType; 
    my $SolRatio; 

    if ($ProblemType ne "SOL") {
        return(-1); 
    }
    $OriginalProblemType = $$ProblemStatisticsArrayRef[$ProblemIndexHash{'SupType'}]; 
    $Formulae = $$ProblemStatisticsArrayRef[$ProblemIndexHash{'Formulae'}]; 
 
    $Leaves = $$StatisticsArrayRef[$SolutionIndexHash{'SolutionLeaves'}];
    if ($Leaves eq "-") {
        return(0); 
    }

    if ($Formulae == 0) {
#----Divide by zero. What should we do here? 
        return(0); 
    }
 
    $SolRatio = $Leaves/$Formulae; 
    $Leaves = ExceptionCheck($SolRatio,$LowerBound,$UpperBound);
    return(ExceptionCheck($SolRatio,$LowerBound,$UpperBound)); 
}
#-----------------------------------------------------------------------------
sub Girth {
    my ($ProblemType,$StatisticsArrayRef,$LowerBound,
$UpperBound) = @_; 

    my $Leaves;
    my $Depth;
    my $GirthRatio; 

    if ($ProblemType ne "SOL") {
        return(-1); 
    }
  
    $Leaves = $$StatisticsArrayRef[$SolutionIndexHash{'SolutionLeaves'}];
    $Depth = $$StatisticsArrayRef[$SolutionIndexHash{'SolutionDepth'}]; 

    if ($Leaves eq "-") {
        return(0);
    }

    if ($Depth == 0) {
        return(0);
    }

    $GirthRatio = $Leaves/$Depth; 
    return(ExceptionCheck($GirthRatio,$LowerBound,$UpperBound)); 
}
#-----------------------------------------------------------------------------
sub ExceptionCheck {
    my ($Statistic,$LowerBound,$UpperBound) = @_; 

    if ($UpperBound eq "-" && $LowerBound eq "-") {
        return(1); 
    } elsif ($UpperBound eq "-") {
        return($Statistic >= $LowerBound); 
    } elsif ($LowerBound eq "-") {
        return($Statistic <= $UpperBound); 
    } elsif (($Statistic >= $LowerBound) && ($Statistic <= $UpperBound)) {
        return(1);
    } else {
        return(0); 
    }
} 
#-----------------------------------------------------------------------------
