#include "misc.h"
#include "export.h"
#include "import.h"
#include "function.h"

#include <stdio.h>
#include <ctime>


void print_help_and_exit(void)
{
    cout << "Collapsing tool (c) January 2007 by Premysl Rucky" << endl << endl;
    cout << "syntax: collapse [options] [input_file] [output_file]" << endl << endl;
    cout << "available options: " << endl;
    cout << "-m ... turns on minimization of the output truth table" << endl;
    cout << "-s ... turns on the subsets enhancement of the minimization algorithm" << endl;
    cout << "-a ... turns on automatic dynamic variables reordering" << endl;
    cout << "-t ... turns on the cpu time measurement" << endl;
    exit(1);
}

int main(int argc, char *argv[])
{
    DdManager *manager;
    Import *im_bench;
    Function *funct;
    Export *ex_pla;
    clock_t start, end;
    bool time_meas = false, min = false, sub = false;
    int par = 0;

//     kontrola spravneho poctu parametru
    if (argc < 3){
        print_help_and_exit();
    }
    
    switch(argc){
        case 3:
            manager = Cudd_Init(0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
            im_bench = new Import(argv[1]);
            ex_pla = new Export(argv[2]);
            funct = new Function(manager, min, sub);
            break;
        
        // ZADAN JEDEN PARAMETR
        case 4:
            manager = Cudd_Init(0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
            im_bench = new Import(argv[2]);
            ex_pla = new Export(argv[3]);
            
            if (strcmp(argv[1], "-m") == 0){
                min = true;
            }
            else
                if (strcmp(argv[1], "-a") == 0){
                    Cudd_AutodynEnable(manager, CUDD_REORDER_SIFT);
                }
                else
                    if (strcmp(argv[1], "-s") == 0){
                        sub = true;
                    }
                    else 
                        if (strcmp(argv[1], "-t") == 0){
                            start = clock();
                            time_meas = true;
                        }
                        else
                            print_help_and_exit();

            funct = new Function(manager, min, sub);
            break;
            
        // ZADANY DVA PARAMETRY
        case 5:
            manager = Cudd_Init(0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
            if (strcmp(argv[1], "-m") == 0){
                min = true;
                if (strcmp(argv[2], "-m") == 0){
                    cout << "haha, very funny..." << endl;
                }
                else
                    if (strcmp(argv[2], "-a") == 0){
                    Cudd_AutodynEnable(manager, CUDD_REORDER_SIFT);
                    }
                    else
                        if (strcmp(argv[2], "-s") == 0){
                            sub = true;
                        }
                        else 
                            if (strcmp(argv[2], "-t") == 0){
                                start = clock();
                                time_meas = true;
                            }
                            else
                                print_help_and_exit();
            }
            else
                if (strcmp(argv[1], "-a") == 0){
                Cudd_AutodynEnable(manager, CUDD_REORDER_SIFT);
                    if (strcmp(argv[2], "-m") == 0){
                        min = true;
                    }
                    else
                        if (strcmp(argv[2], "-a") == 0){
                            cout << "don't try to pull my leg..." << endl;
                        }
                        else
                            if (strcmp(argv[2], "-s") == 0){
                                sub = true;
                            }
                            else 
                                if (strcmp(argv[2], "-t") == 0){
                                    start = clock();
                                    time_meas = true;
                                }
                                else
                                    print_help_and_exit();
                }
                else
                    if (strcmp(argv[1], "-s") == 0){
                        sub = true;
                        if (strcmp(argv[2], "-m") == 0){
                            min = true;
                        }
                        else
                            if (strcmp(argv[2], "-a") == 0){
                                Cudd_AutodynEnable(manager, CUDD_REORDER_SIFT);
                            }
                            else
                                if (strcmp(argv[2], "-s") == 0){
                                    cout << "don't try to break my balls..." << endl;
                                }
                                else 
                                    if (strcmp(argv[2], "-t") == 0){
                                        start = clock();
                                        time_meas = true;
                                    }
                                    else
                                        print_help_and_exit();
                    }
                    else 
                        if (strcmp(argv[1], "-t") == 0){
                            start = clock();
                            time_meas = true;
                            if (strcmp(argv[2], "-m") == 0){
                                min = true;
                            }
                            else
                                if (strcmp(argv[2], "-a") == 0){
                                    Cudd_AutodynEnable(manager, CUDD_REORDER_SIFT);
                                }
                                else
                                    if (strcmp(argv[2], "-s") == 0){
                                        sub = true;
                                    }
                                    else 
                                        if (strcmp(argv[2], "-t") == 0){
                                            cout << "bad boy..." << endl;
                                        }
                                        else
                                            print_help_and_exit();
                        }
                        else
                            print_help_and_exit();
                        
            im_bench = new Import(argv[3]);
            ex_pla = new Export(argv[4]);
            funct = new Function(manager, min, sub);
            break;
        
        // ZADANY 3 PARAMETRY
        case 6:
            manager = Cudd_Init(0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
            if ((strcmp(argv[1], "-m")==0) || (strcmp(argv[2], "-m")==0) || (strcmp(argv[3], "-m")==0)){
                min = true;
                par++;
            }
            if ((strcmp(argv[1], "-s")==0) || (strcmp(argv[2], "-s")==0) || (strcmp(argv[3], "-s")==0)){
                sub = true;
                par++;
            }
            if ((strcmp(argv[1], "-a")==0) || (strcmp(argv[2], "-a")==0) || (strcmp(argv[3], "-a")==0)){
                Cudd_AutodynEnable(manager, CUDD_REORDER_SIFT);
                par++;
            }
            if ((strcmp(argv[1], "-t")==0) || (strcmp(argv[2], "-t")==0) || (strcmp(argv[3], "-t")==0)){
                start = clock();
                time_meas = true;
                par++;
            }
            if (par == 3){
                im_bench = new Import(argv[4]);
                ex_pla = new Export(argv[5]);
                funct = new Function(manager, min, sub);
            }
            else
                print_help_and_exit();
            break;

       // ZADANY 4 PARAMETRY
        case 7:
            manager = Cudd_Init(0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
            if ((strcmp(argv[1], "-m")==0) || (strcmp(argv[2], "-m")==0) || 
                (strcmp(argv[3], "-m")==0) || (strcmp(argv[4], "-m")==0))
                min = true;
            else
                print_help_and_exit();
            
            if ((strcmp(argv[1], "-s")==0) || (strcmp(argv[2], "-s")==0) || 
                 (strcmp(argv[3], "-s")==0) || (strcmp(argv[4], "-s")==0))
                sub = true;
            else
                print_help_and_exit();
            
            if ((strcmp(argv[1], "-a")==0) || (strcmp(argv[2], "-a")==0) || 
                 (strcmp(argv[3], "-a")==0) || (strcmp(argv[4], "-a")==0))
                Cudd_AutodynEnable(manager, CUDD_REORDER_SIFT);
            else
                print_help_and_exit();
            
            if ((strcmp(argv[1], "-t")==0) || (strcmp(argv[2], "-t")==0) || 
                 (strcmp(argv[3], "-t")==0) || (strcmp(argv[4], "-t")==0)){
                start = clock();
                time_meas = true;
            }
            else
                print_help_and_exit();

            im_bench = new Import(argv[5]);
            ex_pla = new Export(argv[6]);
            funct = new Function(manager, min, sub);
            break;
 
        default:
            print_help_and_exit();
    }

    //-------------------- import bench souboru ---------------------
    if (im_bench->import_bench())
        cout << "import ok" << endl;
    else
        exit(1);
    //---------------------------------------------------------------

    //-------------------- postaveni bdd a optimalizace ------------------
    if (funct->run(im_bench->get_var_list(), ex_pla, im_bench->get_output_num()))
        cout << "export ok" << endl;
    else
        exit(1);
    //---------------------------------------------------------------

    end = clock();
    if (time_meas)
        cout << "collapsing finished in "<< difftime(end, start)/CLOCKS_PER_SEC << " secs" << endl;

    Cudd_Quit(manager);

    delete im_bench;
    delete ex_pla;
    delete funct;

//     koncime bez chyby - snad
    return 0;
}
