package verifier;

import java.io.*;
import java.util.*;

/************************************
 *
 * This class verifies the bfs proof of the fact that all sufficient configurations of
 * size 9 have an (11,8) or (4,3) sorting.
 *
 * Run the verifcation program as follows:
 * Go to the directory below "bfs_files" and run
 * java verifier.VerifyBFSProof
 *
 * The verfication works as a DFS search similar to the following:
 *
 * DFS_VERIFY(unoriented_interleaving_pair_file)
 * DFS_VERIFY(unoriented_intersecting_pair_file)
 *
 * DFS_VERIFY(file)
 * IF sorting file
 *      VERIFYSORTING(file)
 * ELSE
 *     FOR EACH extension in the file
 *        DFS_VERIFY(extension_file)
 *
 * At the end of this file you can find examples of
 * the files that are being verified
 *
 */

public class VerifyBFSProof  extends BaseClass {


    public static void main(String args[]){

        Configuration interleaving_pair = new Configuration("[3](0 4 2)[3](1 5 3)");
        String intleaveFileName = "[3](0_4_2)[3](1_5_3).html";
        Configuration intersecting_pair = new Configuration("[3](0 3 1)[3](2 5 4)");
        String intsectFileName = "[3](0_3_1)[3](2_5_4).html";

        try{

            if ( !verifyFile(interleaving_pair, intleaveFileName) )
                System.exit(1);
            
            if ( !verifyFile(intersecting_pair, intsectFileName) )
                System.exit(1);
                 
        }catch(IOException exc){
            exc.printStackTrace();
        }
        System.out.println();
        System.out.println("proof verified");
        System.out.println("checkedFiles: " + checkedFiles.size());
    }


    // The file names of the files that have been verified
    // with respect to the configuration inside the file.
    private static HashSet checkedFiles = new HashSet();
    
    /************************************
     * VERIFY FILE
     * Verify that the file is a correct sorting file
     * or extension file.
     */
    static int filesVerfied = 0;
    private static boolean verifyFile(Configuration conf, String fileName) throws IOException{

        DEBUG("VERIFYING " + fileName);
        
        if ( conf.getNumBlackEdges() > 9*3 ){
            stackTrace();
            printERR("Configuration bigger than it should proof incorrect");
            return false;
        }
        
        BufferedReader in
            = new BufferedReader(new FileReader("bfs_files/"+fileName));

        in.readLine();//just skip the header

        //Check if a sorting file or extension file
        String l = in.readLine();
        boolean correct;
        if ( l.indexOf("HAS") != -1 )
            correct = verifySortingFile(conf, in,fileName);
        else
            correct = verifyExtensionFile(conf, in,fileName);

        
        in.close();

        if ( ! correct ){
            printERR("There was an error in the file");
            printERR(fileName);
        }
        else{
            filesVerfied++;
            System.out.print("files verified = " + filesVerfied +"\r");
            System.out.flush();
        }
        return correct;
    }

    /**********************************
     * VERIFY SORTING FILE
     * This method is called from verfiyFile()
     * The first two lines of the file have allready been read.
     * So the file looks like this:
     * Configuration    numBE = 9   numOCy = 3  hVal = 1395330
     * [3](1 7 4)[3](0 5 2)[3](3 8 6)
     * 0:   a = 0   b = 2   c = 5   move_type = 0
     * Configuration    numBE = 9   numOCy = 3  hVal = 461256
     * [3](4 7 2)[3](0 5 3)[3](1 8 6)
     * 1:   a = 2   b = 4   c = 7   move_type = 2
     * Configuration    numBE = 9   numOCy = 5  hVal = 1617691
     * [1](2)[3](0 3 6)[3](1 8 4)[1](7)[1](5)
     * 2:   a = 0   b = 3   c = 6   move_type = 2
     * Configuration    numBE = 9   numOCy = 7  hVal = 656848
     * [1](5)[1](0)[3](4 8 1)[1](7)[1](2)[1](6)[1](3)
     * 3:   a = 1   b = 4   c = 8   move_type = 2
     * Configuration    numBE = 9   numOCy = 9  hVal = 1888127
     * [1](2)[1](0)[1](1)[1](4)[1](6)[1](3)[1](7)[1](8)[1](5)
     * </pre></body></html>
     */
    private static boolean verifySortingFile(Configuration conf, BufferedReader in, String fileName)  throws IOException{
        DEBUG("sorting file: " + fileName);
        in.readLine();//skip the info line
        
        Configuration readConf = new Configuration(in.readLine());//read the configuration line

        //Check that the read configuration actually is the one that this file
        //gives a sorting for.
        if ( !readConf.equals(conf) ){
            stackTrace();
            printERR("The read configuration is not the same as the one that should be in this file");
            printERR("readConf: " + readConf);
            printERR("inputConf: " + conf);
            return false;
        }

        //If the file all read has been check
        if ( checkedFiles.contains(fileName) )
            return true;
        checkedFiles.add(fileName);

        // START VERIFYING THE SORTING
        Configuration currentConf = readConf;
        int num2moves = 0;
        int num0moves = 0;
        while ( true ){
            //0:   a = 0   b = 2   c = 5   move_type = 0
            String transLine = in.readLine(); // the transposition
            DEBUG(transLine);
            if ( transLine.indexOf("</HTML>") != -1 )
                break; //if end of the sorting
            StringTokenizer tok = new StringTokenizer(transLine);
            tok.nextToken();//skip the index of the sorting
            tok.nextToken();tok.nextToken();//skip 'a'  and skip '='
            int a = Integer.parseInt(tok.nextToken());
            tok.nextToken();tok.nextToken();//skip 'b'  and skip '='
            int b = Integer.parseInt(tok.nextToken());
            tok.nextToken();tok.nextToken();//skip 'c'  and skip '='
            int c = Integer.parseInt(tok.nextToken());
            tok.nextToken();tok.nextToken();//skip 'move_type'  and skip '='
            int move_type = Integer.parseInt(tok.nextToken());

            // Configuration    numBE = 9   numOCy = 3  hVal = 461256
            // [3](4 7 2)[3](0 5 3)[3](1 8 6)
            
            in.readLine();//skip the info line
            Configuration nextConf = new Configuration(in.readLine());

            //Perform the transposition
            int oddCyclesBefore = currentConf.getNumOddCycles();
            currentConf.transpose(a,b,c);
            int oddCyclesDiff = currentConf.getNumOddCycles() - oddCyclesBefore;
            if ( oddCyclesDiff == 2 )
                num2moves++;
            else
                num0moves++;

            //CHECK THE TRANSPOSITION
            // Check that the move_type is correct (we only allow 0 and 2 moves)
            if ( move_type != oddCyclesDiff ||
                 (oddCyclesDiff != 0 && oddCyclesDiff != 2)){
                stackTrace();
                printERR("Move type not correct");
                printERR("transLine = " + transLine);
                printERR("performed type = " + oddCyclesDiff);
                printERR("read move_type = " + move_type);
                return false;
            }

            //check that the configuration after the transposition is as stated
            if ( !currentConf.equals(nextConf) ){
                stackTrace();
                printERR("The next configuration is not the one after transposition");
                printERR("transLine = " + transLine);
                printERR("nextConf: " + nextConf);
                printERR("currentConf: " + currentConf);
                return false;
            }
        }

        //VERIFY THAT THE SORTING IS (4,3) (8,6) (11,8)
        //Remember that a (6,5) and (5,4) sequence per definition is a (4,3) sequence
        //and that the resulting configuration is simple

        if ( num0moves == 0 ){
            stackTrace();
            printERR("UNEXPECTED SORTING there can't be a sorting without 0moves");
            return false;
        }
        if ( num0moves == 1 && num2moves < 3 ){
            stackTrace();
            printERR("Not a (4,3) sequence");
            printERR("num0moves = " + num0moves);
            printERR("num2moves = " + num2moves);
            return false;
        }
        if ( num0moves == 2 && num2moves < 6 ){
            stackTrace();
            printERR("Not an (8,6) sequence");
            printERR("num0moves = " + num0moves);
            printERR("num2moves = " + num2moves);
            return false;
        }
        if ( num0moves == 3 && num2moves < 8 ){
            stackTrace();
            printERR("Not an (11,8) sequence");
            printERR("num0moves = " + num0moves);
            printERR("num2moves = " + num2moves);
            return false;
        }

        if ( !currentConf.isSimplePermutation() ){
            stackTrace();
            printERR("Last configuration not simpe");
            printERR("last configuration is  " + currentConf);
            return false;       
        }

        
        // THE FILE IS A CORRECT SORTING FILE
        return true;
    }

    /***********************************************
     * VERIFY EXTENSION FILE
     * This method verifies an extension file and all linkes from it
     * in a depth first manner.
     *
     * This method is called from verifyFile() so the first
     * two lines have been read. Hence the stream starts with:
     * [3](0 4 2)[3](1 5 3)
     * FULL CONF
     *
     * or
     * [3](0 3 1)[3](2 5 4)
     * OPEN GATES: #2 {1,5}
     */
    public static boolean verifyExtensionFile(Configuration conf, BufferedReader in, String fileName) throws IOException{
        DEBUG("extension file: " + fileName);
        Configuration readConf = new Configuration(in.readLine());//read the configuration line
        DEBUG();

        //Check that the read configuration actually is the one that this file
        //gives extensions of.
        if ( !readConf.equals(conf) ){
            stackTrace();
            printERR("The read configuration is not the same as the one that should be in this file");
            printERR("readConf: " + readConf);
            printERR("inputConf: " + conf);
            return false;
        }

        //If the file all read has been check
        if ( checkedFiles.contains(fileName) )
            return true;
        checkedFiles.add(fileName);


        LinkedList extensionList;
        
        String fullOrOpenStr = in.readLine();//read the FULL CONF or OPEN GATES lines
        if ( fullOrOpenStr.indexOf("FULL") != -1 ){
            int openGates[] = conf.getOpenGates();
            if ( openGates.length != 0 ){
                stackTrace();
                printERR("Not a full confinguration");
                printERR("openGates.length = " + openGates.length);
                return false;
            }
            
            extensionList = computeSufficientExtensionIndices(new int[0], conf.getNumBlackEdges());
        }
        else {// OPEN GATES: #2 {1,5}
            //read the open gates
            int parindex = fullOrOpenStr.indexOf('#');
            String arrayStr = fullOrOpenStr.substring(parindex);//i.e the substring "#2 {1,5}"
            StringTokenizer tok = new StringTokenizer(arrayStr,"#{,} ");
            int readNumOpen = Integer.parseInt(tok.nextToken());
            int openGates[] = conf.getOpenGates();
            if ( openGates.length != readNumOpen || openGates.length > 2){
                stackTrace();
                printERR("Incorrect number of open gates read");
                printERR("openGates.length = " + openGates.length);
                printERR("readString : " + fullOrOpenStr);
                return false;
            }
            int readOpenGates[] = new int[readNumOpen];
            for ( int i = 0 ; i < readNumOpen ; i++ ){
                readOpenGates[i] = Integer.parseInt(tok.nextToken());
                if ( openGates[i] != readOpenGates[i] ){
                    stackTrace();
                    printERR("Incorrect  open gate read");
                    printERR("openGates[i] = " + openGates[i]);
                    printERR("readString : " + fullOrOpenStr);
                    return false;
                }
            }

            extensionList = computeSufficientExtensionIndices(openGates, conf.getNumBlackEdges());
        }

        //------------------------
        // CHECK EXTENSIONS
        // Now the extensions are computed and they should be in the same order
        // as in the file. So we start checking each extension.
        in.readLine(); //skip blank line
        in.readLine(); //skip black line
        in.readLine(); // skip the line with THE EXTENSIONS ARE:

        // Every time around the for loop the file should read:
        // ------------
        //  a = 0 b = 0 c = 1
        // Configuration    numBE = 9   numOCy = 3  hVal = 1915539
        // [3](0 3 1)[3](2 7 5)[3](4 8 6)
        // canonical representation
        // Configuration    numBE = 9   numOCy = 3  hVal = 446082
        // [3](0 8 6)[3](7 4 2)[3](5 3 1)
        // BAD EXTENSION
        // View Canonical Extension <a href="[3](0_8_6)[3](1_5_3)[3](2_7_4).html">[3](0_8_6)[3](1_5_3)[3](2_7_4).html</a>
        //...
        while ( !extensionList.isEmpty() ){
            int extensionIndices[] = (int[]) extensionList.removeFirst();
            in.readLine();//skip ------------
            String exindices = in.readLine();//skip indices line  a = 0 b = 0 c = 1
            DEBUG("extension: " + exindices);
            in.readLine();//skip conf info line
            String origExtStr = in.readLine();//skip the conf (we only need to check equivalence with the canonical representation)
            in.readLine();//skip "canonical representation"
            in.readLine();//skip conf info line
            Configuration readExtension = new Configuration(in.readLine());

            Configuration extension = new Configuration(conf);
            extension.addUnoriented3Cycle(extensionIndices[0],extensionIndices[1],extensionIndices[2]);

            //check that the read extension is the right extension;
            if ( ! extension.equivalentEquals(readExtension) ){
                stackTrace();
                printERR("The extensions do not match");
                printERR("readCanoExtension = " + readExtension);
                printERR("uncanonicalExtension = " + origExtStr);
                printERR("expected extension = " + extension );
                return false;
            } 

            in.readLine();//skip BAD EXTENSION or GOOD EXTENSION

            //RECURSIVE CALL
            // DFS call recursively to check that the extension is correct
            String linkLine = in.readLine();
            int startLink = linkLine.indexOf('"');
            int endLink = linkLine.lastIndexOf('"');
            String extensionFileName = linkLine.substring(startLink+1,endLink);

            boolean correct = verifyFile(readExtension,extensionFileName);

            if ( ! correct ){
                printERR("Extension of conf not correct " + conf);
                return false;
            }
        }
        

        // ALL EXTENSION HAVE BEEN VERIFIED
        return true;
    }



    /*****************************************
     * COMPUTE SUFFICIENT EXTENSIONS
     *
     * This method takes and array of open gates and returns
     * a list containing all extensions (some extensions occurr more than ones).
     * Each extension is represented with an int[3] array.
     */

    private static LinkedList computeSufficientExtensionIndices(int openGates[],  int numBlack){

        //CALCULATE ALL THE SUFFICIENT EXTENSIONS
        LinkedList extensionList = new LinkedList();

        //IF FULL CONFIGURATION
        if ( openGates.length == 0 ){
                      
            //fill in the extensions
            for ( int firstPos = 0 ; firstPos < numBlack ; firstPos++ ){
                for ( int secondPos = firstPos ; secondPos < numBlack ; secondPos++ ){
                    for ( int thirdPos = secondPos ; thirdPos < numBlack ; thirdPos++ ){
                        //if thirdPos == secondPos == firstPos
                        //then there are 2 (actually 3) open gates so it is not a sufficient extension
                        if ( thirdPos == firstPos )
                            continue;
                        int extension[] = new int[]{firstPos,secondPos,thirdPos};
                        extensionList.add(extension);
                    }
                }
            }
        }
        else {// OPEN CONFIGURATION
            if ( openGates.length > 2 ){
                stackTrace();
                printERR("PROG ERROR to many open gates");
                System.exit(1);
            }

            
            //fill in the extensions
            for ( int gateIndex = 0 ; gateIndex < openGates.length ; gateIndex++ ){
                int openGate = openGates[gateIndex];
               
                for ( int secondPos = 0 ; secondPos < numBlack ; secondPos++ ){
                    for ( int thirdPos = secondPos ; thirdPos < numBlack ; thirdPos++ ){
                        if ( openGate == secondPos && openGate == thirdPos )
                            continue; //this is not a sufficient extension
                        int extension[] = new int[]{openGate,secondPos,thirdPos};
                        extensionList.add(extension);
                    } 
                }
            }

        }// END OF COMPUTING THE EXTENSION INDICES

        return extensionList;
    }
}


//Example of sorting file
// <html><head><title></title></head><body><pre>
// <img src="[3](0_5_2)[3](1_7_4)[3](3_8_6).jpeg"><p>HAS SORTING
// Configuration    numBE = 9   numOCy = 3  hVal = 1395330
// [3](1 7 4)[3](0 5 2)[3](3 8 6)
// 0:   a = 0   b = 2   c = 5   move_type = 0
// Configuration    numBE = 9   numOCy = 3  hVal = 461256
// [3](4 7 2)[3](0 5 3)[3](1 8 6)
// 1:   a = 2   b = 4   c = 7   move_type = 2
// Configuration    numBE = 9   numOCy = 5  hVal = 1617691
// [1](2)[3](0 3 6)[3](1 8 4)[1](7)[1](5)
// 2:   a = 0   b = 3   c = 6   move_type = 2
// Configuration    numBE = 9   numOCy = 7  hVal = 656848
// [1](5)[1](0)[3](4 8 1)[1](7)[1](2)[1](6)[1](3)
// 3:   a = 1   b = 4   c = 8   move_type = 2
// Configuration    numBE = 9   numOCy = 9  hVal = 1888127
// [1](2)[1](0)[1](1)[1](4)[1](6)[1](3)[1](7)[1](8)[1](5)
// </pre></body></html>
    

//Example of extension file
// <html><head><title></title></head><body><pre>
// <img src="[3](0_4_2)[3](1_5_3).jpeg"><p>Configuration    numBE = 6   numOCy = 2  hVal = 1845
// [3](0 4 2)[3](1 5 3)
// FULL CONF
//
//
// THE EXTENSIONS ARE:
// ------------
//  a = 0 b = 0 c = 1
// Configuration    numBE = 9   numOCy = 3  hVal = 1915539
// [3](0 3 1)[3](2 7 5)[3](4 8 6)
// canonical representation
// Configuration    numBE = 9   numOCy = 3  hVal = 446082
// [3](0 8 6)[3](7 4 2)[3](5 3 1)
// BAD EXTENSION
// View Canonical Extension <a href="[3](0_8_6)[3](1_5_3)[3](2_7_4).html">[3](0_8_6)[3](1_5_3)[3](2_7_4).html</a>
// ------------
//  a = 0 b = 0 c = 2
// Configuration    numBE = 9   numOCy = 3  hVal = 2000139
// [3](0 4 1)[3](2 7 5)[3](3 8 6)
// canonical representation
// Configuration    numBE = 9   numOCy = 3  hVal = 368815
// [3](6 5 2)[3](4 1 8)[3](3 0 7)
// BAD EXTENSION
// View Canonical Extension <a href="[3](0_7_3)[3](1_8_4)[3](2_6_5).html">[3](0_7_3)[3](1_8_4)[3](2_6_5).html</a>
// ......
// ------------
//  a = 4 b = 5 c = 5
// Configuration    numBE = 9   numOCy = 3  hVal = 1519545
// [3](4 7 6)[3](0 5 2)[3](1 8 3)
// canonical representation
// Configuration    numBE = 9   numOCy = 3  hVal = 446082
// [3](6 0 8)[3](2 7 4)[3](3 1 5)
// BAD EXTENSION
// View Canonical Extension <a href="[3](0_8_6)[3](1_5_3)[3](2_7_4).html">[3](0_8_6)[3](1_5_3)[3](2_7_4).html</a>
// </pre></body></html>


//Example of extension file with open gates
// <html><head><title></title></head><body><pre>
// <img src="[3](0_3_1)[3](2_5_4).jpeg"><p>Configuration    numBE = 6   numOCy = 2  hVal = 658
// [3](0 3 1)[3](2 5 4)
// OPEN GATES: #2 {1,5}
//
//
// THE EXTENSIONS ARE:
// ------------
// open = 1 a = 0 b = 0
// Configuration    numBE = 9   numOCy = 3  hVal = 388438
// [3](0 3 1)[3](2 6 4)[3](5 8 7)
// canonical representation
// Configuration    numBE = 9   numOCy = 3  hVal = 358647
// [3](2 5 3)[3](4 8 6)[3](7 1 0)
// BAD EXTENSION
// View Canonical Extension <a href="[3](0_7_1)[3](2_5_3)[3](4_8_6).html">[3](0_7_1)[3](2_5_3)[3](4_8_6).html</a>