#include "solve.hpp"

#include <assert.h>
#include "src/kissat.h"

extern "C" {
    #include "aiger.h"
}

#define ENABLE_INPUT_VAR_DIVIED 0
#define DIVEDED_VAR_NUM 48

#define ENABLE_MERGE_NODE 0

#if ENABLE_INPUT_VAR_DIVIED
std::map<int, int> init_inputs;
#endif

using std::vector;

bool match_equal(aiger* aiger, int var) {
    if(graph.redge[var].size() != 2) return false;
    int x = graph.redge[var][0].to;
    int y = graph.redge[var][1].to;

    if(!graph.redge[var][0].neg) return false;
    if(!graph.redge[var][1].neg) return false;

    if(graph.redge[x].size() != 2) return false;
    if(graph.redge[y].size() != 2) return false;

    Graph::Edge ex0 = graph.redge[x][0];
    Graph::Edge ex1 = graph.redge[x][1];
    if(ex0.to > ex1.to) std::swap(ex0, ex1);

    Graph::Edge ey0 = graph.redge[y][0];
    Graph::Edge ey1 = graph.redge[y][1];
    if(ey0.to > ey1.to) std::swap(ey0, ey1);

    if(ex0.to != ey0.to || ex1.to != ey1.to) return false;

    if(ex0.neg + ex1.neg != 1) return false;
    if(ey0.neg + ey1.neg != 1) return false;
    if(ex0.neg + ey0.neg != 1) return false;

    // for(auto& e : graph.edge[var]) {
    //     if(!e.neg) return false;
    // }

    return true;
}

bool match_xor(aiger* aiger, int var) {
    if(graph.redge[var].size() != 2) return false;
    int x = graph.redge[var][0].to;
    int y = graph.redge[var][1].to;

    if(!graph.redge[var][0].neg) return false;
    if(!graph.redge[var][1].neg) return false;

    if(graph.redge[x].size() != 2) return false;
    if(graph.redge[y].size() != 2) return false;

    Graph::Edge ex0 = graph.redge[x][0];
    Graph::Edge ex1 = graph.redge[x][1];
    if(ex0.to > ex1.to) std::swap(ex0, ex1);

    Graph::Edge ey0 = graph.redge[y][0];
    Graph::Edge ey1 = graph.redge[y][1];
    if(ey0.to > ey1.to) std::swap(ey0, ey1);

    if(ex0.to != ey0.to || ex1.to != ey1.to) return false;

    if(ex0.neg != ex1.neg) return false;
    if(ey0.neg != ey1.neg) return false;
    if(ex0.neg == ey0.neg) return false;

    return true;
}

void cal_topo_index(aiger *aiger) {

    static int* used = new int[aiger->maxvar + 1];
    memset(used, 0, (aiger->maxvar + 1) * sizeof(int));

    std::queue<int> q;
    for(int i=0; i<aiger->num_inputs; i++) {
        int input = aiger_lit2var(aiger->inputs[i].lit);
        topo_index[input] = 1;
        q.push(input);
    }

    while(!q.empty()) {
        int cur = q.front();
        q.pop();
        for(auto& edge : graph.edge[cur]) {
            int v = edge.to;
            if(!used[v]) {
                used[v] = true;
                q.push(v);
                topo_index[v] = topo_index[cur] + 1;
            }
        }
    }
}

void simulate(aiger* aiger, int* input, int* result) {

    std::queue<int> q;

    for(int i=0; i<aiger->num_inputs; i++) {
        int var = aiger_lit2var(aiger->inputs[i].lit);
        result[var] = input[i];
        q.push(var);
    }

    static int* topo_counter = new int[aiger->maxvar + 1];
    memset(topo_counter, 0, (aiger->maxvar + 1) * sizeof(int));

    while(!q.empty()) {
        int cur = q.front();
        q.pop();
        for(auto& edge : graph.edge[cur]) {
            int v = edge.to;
            topo_counter[v]++;

            if(topo_counter[v] == 2) {
                q.push(v);

                //cout << "redge: " << v << " " << graph.redge[v][0].to << " " << graph.redge[v][1].to << endl;

                Graph::Edge rhs0_edge = graph.redge[v][0];
                int rhs0 = rhs0_edge.neg ? !result[rhs0_edge.to] : result[rhs0_edge.to];

                Graph::Edge rhs1_edge = graph.redge[v][1];
                int rhs1 = rhs1_edge.neg ? !result[rhs1_edge.to] : result[rhs1_edge.to];

                result[v] = rhs0 & rhs1;

                //cout << "var: " << aiger_var2lit(v) << " = " << rhs0 + rhs0_edge.neg << " " << rhs1 + rhs1_edge.neg << " : " <<  result[aiger_var2lit(v)] << endl;

            }
        }
    }
}

aiger* get_var_as_output_aiger(aiger* aiger, unsigned var) {

    std::queue<int> q;
    
    static int* used = new int[aiger->maxvar + 1];
    memset(used, 0, (aiger->maxvar + 1) * sizeof(int));

    q.push(var);
    used[var] = true;

    std::vector<std::pair<int, std::pair<int, int>>> ands;
    std::vector<int> inputs;
    

    while(!q.empty()) {
        int u = q.front();
        q.pop();

        // if(graph.redge[u].size() == 0) {
        //     inputs.push_back(aiger_var2lit(u));
        //     continue;
        // }

        int a = graph.redge[u][0].to;
        int b = graph.redge[u][1].to;

        if(a <= aiger->num_inputs && b <= aiger->num_inputs) {
            printf("AND-START: %d (%d %d)\n", u, a, b);
            inputs.push_back(aiger_var2lit(u));
            continue;
        }
        if(a <= aiger->num_inputs || b <= aiger->num_inputs) {
            printf("FUCK!!!!!");
        }

        ands.push_back(std::make_pair(aiger_var2lit(u), std::make_pair(aiger_var2lit(a) + graph.redge[u][0].neg, aiger_var2lit(b) + graph.redge[u][1].neg)));

        if(!used[a]) q.push(a), used[a] = true;
        if(!used[b]) q.push(b), used[b] = true;
    }

    auto result_aiger = aiger_init();
    for(int i=0; i<inputs.size(); i++) {
        printf("add INPUTS: %d\n", inputs[i]);
        aiger_add_input(result_aiger, inputs[i], std::to_string(inputs[i]).c_str());
    }
    for(auto &pr : ands) {
        aiger_add_and(result_aiger, pr.first, pr.second.first, pr.second.second);
        printf("add AND: %d %d %d\n", pr.first, pr.second.first, pr.second.second);
    }
    aiger_add_output(result_aiger, aiger_var2lit(var), "238901893");

    return result_aiger;
}

void get_cone_of_points(aiger *aiger, std::vector<int> &points, std::vector<int> &result, int lmin) {
    result.clear();

    std::queue<int> q;
    static int* used = new int[aiger->maxvar + 1];
    memset(used, 0, (aiger->maxvar + 1) * sizeof(int));

    for(auto& p : points) {
        q.push(p);
        used[p] = true;
    }
    
    while(!q.empty()) {
        int u = q.front();
        q.pop();

        result.push_back(u);

        if(topo_index[u] < lmin) continue;
        if(graph.redge[u].size() == 0) continue;

        int a = graph.redge[u][0].to;
        int b = graph.redge[u][1].to;

        if(graph.redge[u][0].neg) a = -a;
        if(graph.redge[u][1].neg) b = -b;

        a = abs(a), b = abs(b);

        if(!used[a]) q.push(a), used[a] = true;
        if(!used[b]) q.push(b), used[b] = true;
    }
}

bool check_var_equal_with_input_set(aiger *aiger, int x, int y, std::set<int> &inputs) {



    SATSolver solver;
    solver.set_max_time(10);
    solver.new_vars(aiger->maxvar + 1);
    solver.log_to_file("cms.log");

    std::queue<int> q;
    static int* used = new int[aiger->maxvar + 1];
    memset(used, 0, (aiger->maxvar + 1) * sizeof(int));

    q.push(x);
    q.push(y);
    int can_del = 0;
    used[x] = true;
    used[y] = true;

    // printf("[%d]inputs: ", inputs.size());
    // for(auto& in : inputs) {
    //     printf("%d ", inputs);
    // }
    // printf("\n");

    #if ENABLE_INPUT_VAR_DIVIED
        for(auto& p : init_inputs) {
            int var = aiger_lit2var(p.first);
            if(!p.second) var = -var;
            cms_add(solver, var);
            cms_add(solver, 0);
        }
    #endif

    while(!q.empty()) {
        int u = q.front();
        q.pop();

        can_del++;

        if(inputs.count(u)) continue;

        if(match_xor(aiger, u) || match_equal(aiger, u)) {
            //printf("FUCK %d\n", u);
            std::vector<unsigned> vars;
            int x = graph.redge[graph.redge[u][0].to][0].to;
            int y = graph.redge[graph.redge[u][0].to][1].to;
            vars.push_back(x);
            vars.push_back(y);
            vars.push_back(u);
            solver.add_xor_clause(vars, match_equal(aiger, u));
            //printf("x: %d %d %d (%d)\n", x, y, u, match_equal(aiger, u));

            if(!used[x]) q.push(x), used[x] = true;
            if(!used[y]) q.push(y), used[y] = true;
            
            continue;
        }

        int a = graph.redge[u][0].to;
        int b = graph.redge[u][1].to;

        if(graph.redge[u][0].neg) a = -a;
        if(graph.redge[u][1].neg) b = -b;

        cms_add(solver, -u), cms_add(solver,  a), cms_add(solver, 0);
        cms_add(solver, -u), cms_add(solver,  b), cms_add(solver, 0);
        cms_add(solver, -a), cms_add(solver, -b), cms_add(solver, u), cms_add(solver, 0);

        a = abs(a), b = abs(b);

        if(!used[a])
            q.push(a), used[a] = true;

        if(!used[b])
            q.push(b), used[b] = true;
    }

    cms_add(solver, -x), cms_add(solver, -y), cms_add(solver, 0);
    cms_add(solver,  x), cms_add(solver,  y), cms_add(solver, 0);

    for(auto& pair : eqs) {
        int a = pair.first;
        int b = pair.second;
        cms_add(solver, -a), cms_add(solver,  b), cms_add(solver, 0);
        cms_add(solver,  a), cms_add(solver, -b), cms_add(solver, 0);
    }

    // printf("2one %d\n", can_del);

    // printf("##### %d\n", result);

    // printf("FIND XOR: %d\n",);

    auto result = solver.solve();

    return result == l_False;
}

bool check_var_equal(aiger* aiger, int x, int y) {
    std::vector<int> cone;
    std::vector<int> points;
    points.push_back(x);
    points.push_back(y);

    get_cone_of_points(aiger, points, cone, 0);

    printf("cone %d\n", cone.size());

    std::set<int> inputs;
    for(auto& p : cone) {
        // if(eqn.count(p) || graph.redge[p].size() == 0)
        //     inputs.insert(p);
        if(graph.redge[p].size() == 0)
            inputs.insert(p);
    }

    while(!check_var_equal_with_input_set(aiger, x, y, inputs)) {
        std::vector<std::pair<int, int>> vec;
        for(auto& p : inputs) {
            vec.push_back(std::make_pair(topo_index[p], p));
        }
        std::sort(vec.begin(), vec.end());

        int p = vec[vec.size()-1].second;

        //printf("max-topo: %d\n", topo_index[p]);

        if(topo_index[p] == 1) return false;

        std::queue<int> q;
        static int* used = new int[aiger->maxvar + 1];
        memset(used, 0, (aiger->maxvar + 1) * sizeof(int));

        q.push(p);
        used[p] = true;
        
        while(!q.empty()) {
            int u = q.front();
            q.pop();

            if(graph.redge[u].size() == 0 || (eqn.count(u) && u != p)) {
                inputs.insert(u);
                continue;
            }

            int a = graph.redge[u][0].to;
            int b = graph.redge[u][1].to;

            if(!used[a]) q.push(a), used[a] = true;
            if(!used[b]) q.push(b), used[b] = true;
        }

        inputs.erase(p);
    }

    return true;
}

void check_entire_problem(aiger* aiger) {    

    SATSolver solver;
    solver.new_vars(aiger->maxvar + 1);

    std::queue<int> q;
    static int* used = new int[aiger->maxvar + 1];
    memset(used, 0, (aiger->maxvar + 1) * sizeof(int));
    
    int x = aiger_lit2var(aiger->outputs[0].lit);

    q.push(x);
    used[x] = true;

    while(!q.empty()) {
        int u = q.front();
        q.pop();

        /*
        (u => a & b) <=> ~u | (a & b) <=> (~u | a) & (~u | b)
        (u <= a & b) <=> ~(a & b) | u <=> ~a | ~b | u
        */
        // if(eqn.count(u)) {
        //     cout << "back ends " << u << endl;
        //     continue;
        // }

        if(graph.redge[u].size() == 0) {
            //cout << "oh FUCK" << endl;
            continue;
        }

        if(match_xor(aiger, u) || match_equal(aiger, u)) {
            //printf("FUCK %d\n", u);
            std::vector<unsigned> vars;
            int x = graph.redge[graph.redge[u][0].to][0].to;
            int y = graph.redge[graph.redge[u][0].to][1].to;
            vars.push_back(x);
            vars.push_back(y);
            vars.push_back(u);
            solver.add_xor_clause(vars, match_equal(aiger, u));
            //printf("x: %d %d %d (%d)\n", x, y, u, match_equal(aiger, u));

            if(!used[x]) q.push(x), used[x] = true;
            if(!used[y]) q.push(y), used[y] = true;
            
            continue;
        }


        int a = graph.redge[u][0].to;
        int b = graph.redge[u][1].to;


        int ta = aiger_var2lit(a);// + graph.redge[u][0].neg;
        int tb = aiger_var2lit(b);// + graph.redge[u][1].neg;

        //if(eqp.find(make_pair(ta, tb)) != eqp.end() || eqp.find(make_pair(tb, ta)) != eqp.end()) {
        // if(eqn.count(a) && eqn.count(b)) {
        //     cout << "SPCIAL-AND " << ta << " " << tb << endl;
        //     continue;
        // }


        // 下面找到所有的异或/等价电路
        if(graph.redge[a].size() > 0 && graph.redge[b].size() > 0) {

            //graph.redge[u][0].neg && graph.redge[u][1].neg && 

            auto ea0 = graph.redge[a][0];
            auto ea1 = graph.redge[a][1];
            if(ea0.to > ea1.to) std::swap(ea0, ea1);

            auto eb0 = graph.redge[b][0];
            auto eb1 = graph.redge[b][1];
            if(eb0.to > eb1.to) std::swap(eb0, eb1);

            // 两个与门连接的都是相同的节点
            if(ea0.to == eb0.to && ea1.to == eb1.to) {
                
                // 二个节点等价
                if(eqp.find(std::make_pair(aiger_var2lit(ea0.to), aiger_var2lit(ea1.to))) != eqp.end() || eqp.find(std::make_pair(aiger_var2lit(ea1.to), aiger_var2lit(ea0.to))) != eqp.end()) {
                    printf("c XOR %d %d\n", aiger_var2lit(ea0.to), aiger_var2lit(ea1.to));
                }
            }
        }

        //cout << "AND " << aiger_var2lit(u) << " " << (aiger_var2lit(a) + graph.redge[u][0].neg) << " " << (aiger_var2lit(b) + graph.redge[u][1].neg) << endl;

        if(graph.redge[u][0].neg) a = -a;
        if(graph.redge[u][1].neg) b = -b;
        

        cms_add(solver, -u);
        cms_add(solver, a);
        cms_add(solver, 0);

        cms_add(solver, -u);
        cms_add(solver, b);
        cms_add(solver, 0);

        cms_add(solver, -a);
        cms_add(solver, -b);
        cms_add(solver, u);
        cms_add(solver, 0);

        a = abs(a);
        b = abs(b);

        if(!used[a]) {
            q.push(a);
            used[a] = true;
        }

        if(!used[b]) {
            q.push(b);
            used[b] = true;
        }
    }

    for(auto& pair : eqs) {
        int a = pair.first;
        int b = pair.second;

        cms_add(solver, -a);
        cms_add(solver, b);
        cms_add(solver, 0);

        cms_add(solver, a);
        cms_add(solver, -b);
        cms_add(solver, 0);
    }

    if(aiger->outputs[0].lit & 1) {
        cms_add(solver, -x);
        cms_add(solver, 0);
    } else {
        cms_add(solver, x);
        cms_add(solver, 0);
    }
    //ipasir_set_conflict_limit(solver, 100000);

    printf("c final: %d\n", solver.solve());

    return;
}

bool check_var_equal_new(aiger* aiger, int x, int y) {
    auto aiger0 = get_var_as_output_aiger(aiger, x);
    auto aiger1 = get_var_as_output_aiger(aiger, y);

    system("rm -rf test0*");
    system("rm -rf test1*");

    FILE* f0 = fopen("test0.aiger", "w");
    FILE* f1 = fopen("test1.aiger", "w");

    aiger_write_to_file(aiger0, aiger_mode::aiger_binary_mode, f0);
    aiger_write_to_file(aiger1, aiger_mode::aiger_binary_mode, f1);

    fclose(f0);
    fclose(f1);

    aiger_reset(aiger0);
    aiger_reset(aiger1);

    system("./bash.sh");

    std::string str;
    FILE* result = fopen("abc_result", "r");
    char c;
    while((c = fgetc(result)) != EOF) str += c;

    std::cout << str << std::endl;

    static int cnt = 0;
    char cmd[100];
    sprintf(cmd, "cp test0.aiger hard1/test%d_0.aiger", cnt);
    system(cmd);
    sprintf(cmd, "cp test1.aiger hard1/test%d_1.aiger", cnt);
    system(cmd);
    cnt++;

    return str.find("equivalent") != std::string::npos;
}

int cal_input_related_size(aiger* aiger, int input) {
    
    static int* used = new int[aiger->maxvar + 1];
    memset(used, 0, (aiger->maxvar + 1) * sizeof(int));

    std::queue<int> q;
    q.push(input);
    used[input] = true;

    int result = 1;

    while(!q.empty()) {
        int cur = q.front();
        q.pop();
        for(auto& edge : graph.edge[cur]) {
            int v = edge.to;
            if(!used[v]) {
                used[v] = true;
                q.push(v);
                result++;
            }
        }
    }
    return result;
}


#if ENABLE_MERGE_NODE
std::map<int, int> fa;
int father(int x) {
	if(fa[x] == x) return x;
	return fa[x] = father(fa[x]);
}
void merge_node(aiger* aiger, int x, int y) {
    if(father(x) == father(y)) return;

    x = father(x);
    y = father(y);

    std::vector<int> cone_x;
    std::vector<int> cone_y;
    std::vector<int> points_x;
    points_x.push_back(x);
    std::vector<int> points_y;
    points_y.push_back(y);
    get_cone_of_points(aiger, points_x, cone_x, 0);
    get_cone_of_points(aiger, points_y, cone_y, 0);

    if(cone_y.size() < cone_x.size()) std::swap(x, y);

    fa[y] = x;

    std::cout << "merge " << y << " to " << x << std::endl;
    
    for(auto& edge : graph.edge[y]) {
        int v = edge.to;
        //std::cout << "v:" << v << std::endl;
        for(auto &e : graph.redge[v]) {
            if(e.to == y) e.to = x;
            else if(e.to == y) e.to = x;
        }
    }
    graph.edge[y].clear();
}
#endif

int main(int argv, char* args[]) {

    // SATSolver sat;
    // sat.new_vars(10);

    // vector<Lit> vec;

    // vec.clear();
    // vec.push_back(Lit(1, true));
    // vec.push_back(Lit(2, false));
    // sat.add_clause(vec);

    // vec.clear();
    // vec.push_back(Lit(2, true));
    // vec.push_back(Lit(1, false));
    // sat.add_clause(vec);

    // vector<unsigned> xor_clause;
    // xor_clause.push_back(1);
    // //xor_clause.push_back(2);
    // log

    // vec.clear();
    // vec.push_back(Lit(2, false));
    // sat.add_clause(vec);

    // printf("%d\n", sat.solve() == l_True);

    // return 0;

    
    printf("c =================================== input =================================\n");
    aiger* aiger = aiger_init();
    FILE* file = fopen(args[1], "r");
    aiger_read_from_file(aiger, file);

    for(int i=0; i<aiger->num_ands; i++) {
        auto gate = aiger->ands[i];
        //cout << gate.lhs << " " << gate.rhs0 << " " << gate.rhs1 << endl;
        graph.add(aiger_lit2var(gate.rhs0), aiger_lit2var(gate.lhs), gate.rhs0 & 1);
        graph.add(aiger_lit2var(gate.rhs1), aiger_lit2var(gate.lhs), gate.rhs1 & 1);
    }
    printf("c inputs: \nc ");

    for(int i=0; i<aiger->num_inputs; i++) {
        printf("%d ", aiger->inputs[i].lit);
    }

    printf("\nc outputs: \nc ");

    for(int i=0; i<aiger->num_outputs; i++) {
        printf("%d ", aiger->outputs[i].lit);
    }
    printf("\nc maxvar: \nc %d\n", aiger->maxvar);

    cal_topo_index(aiger);

    printf("c max-topo-level: %d\n", topo_index[aiger_lit2var(aiger->outputs[0].lit)]);

    int xor_cnt = 0;
    for(int i=1; i<=aiger->maxvar; i++) {
        if(match_xor(aiger, i) || match_equal(aiger, i)) xor_cnt++;
    }

    printf("c find xor: %d\n", xor_cnt);

    // FILE* file1 = fopen("new.aig", "w");
    // auto * aig = get_var_as_output_aiger(aiger, 156);
    // aiger_write_to_file(aig, aiger_mode::aiger_binary_mode, file1);
    // return 0;
    
    classes.push_back(std::vector<int>());
    for(int i=1; i<=aiger->maxvar; i++) {
        classes[0].push_back(i);
    }

    int* result = new int[aiger->maxvar + 1];
    int* input_vector = new int[aiger->num_inputs];

    #if ENABLE_INPUT_VAR_DIVIED
        
        std::vector<std::pair<int, int>> input_size;
        for(int i=0; i<aiger->num_inputs; i++) {
            int lit = aiger->inputs[i].lit;
            int size = cal_input_related_size(aiger, lit);
            input_size.push_back(std::make_pair(size, lit));
        }
        std::sort(input_size.begin(), input_size.end(), std::greater<std::pair<int, int>>());

        for(int i=0; i<std::min((int)input_size.size(), DIVEDED_VAR_NUM); i++) {
            init_inputs[input_size[i].second] = rand() % 2;
        }

    #endif

    #if ENABLE_MERGE_NODE
    for(int i=1; i<=aiger->maxvar; i++) fa[i] = i;
    #endif

    int const_zero[aiger->maxvar + 1];
    int const_one[aiger->maxvar + 1];
    for(int i=1; i<=aiger->maxvar; i++) {
        const_zero[i] = const_one[i] = 1;
    }

    printf("c =================================== detect =================================\n");
    for(int i=0; i<atoi(args[2]); i++) {

        if(i % 10000 == 0) printf("c simulate count: %d\n", i);

        for(int i=0; i<aiger->num_inputs; i++) {
            input_vector[i] = rand() % 2;

            #if ENABLE_INPUT_VAR_DIVIED
                if(init_inputs.count(aiger->inputs[i].lit))
                    input_vector[i] = init_inputs[aiger->inputs[i].lit];
            #endif
        }

        memset(result, -1,  (aiger->maxvar + 1) * sizeof(int));

        simulate(aiger, input_vector, result);


        for(int i=1; i<=aiger->maxvar; i++) {
            if(result[i] == 0) {
                const_one[i] = 0;
            } 
            if(result[i] == 1) {
                const_zero[i] = 0;
            }
            if(result[i] == -1) {
                printf("wrong\n");
                exit(0);
            }
        }


        std::vector<std::vector<int>> tmp;
        for(auto& clas : classes) {
            std::vector<int> v0;
            std::vector<int> v1;
            for(auto &v : clas) {
                if(result[v]) v1.push_back(v);
                else v0.push_back(v);
            }
            if(v0.size() > 1) tmp.push_back(v0);
            if(v1.size() > 1) tmp.push_back(v1);
        }
        
        classes = tmp;
    }

    printf("c Number of equivalent classes: %d\n", classes.size());
    printf("classes: \n");
    for(auto& clas : classes) {
        printf("[ ");
        for(auto &v : clas) {
            printf("%d ", v);
            eqn.insert(v);
        }
        printf("]\n");
    }

    for(int i=1; i<=aiger->maxvar; i++) {
        if(const_zero[i]) printf("const-zero: %d\n", i);
        if(const_one[i]) printf("const-one: %d\n", i);
    }
    return 0;

    printf("c =================================== some test code =================================\n");

    // test(aiger);
    // return 0;

    for(auto& clas : classes) {
        //if(clas.size() != 2) continue;
        std::vector<int> tmp;
        if(clas.size() > 100) {
            printf("classes too big!\n");
            continue;
        }

        for(int i=0; i<clas.size(); i++) {
            for(int j=i+1; j<clas.size(); j++) {          

                std::vector<int> cone;
                std::vector<int> pionts;
                pionts.push_back(clas[i]);
                pionts.push_back(clas[j]);
                get_cone_of_points(aiger, pionts, cone, 0);

                int vara =  aiger_lit2var(clas[i]);
                int varb =  aiger_lit2var(clas[j]);

                pairs.push_back(std::make_pair(cone.size(), std::make_pair(clas[i], clas[j])));
            }
        }
    }

    sort(pairs.begin(), pairs.end());

    printf("c =================================== check =================================\n");    


    int s = 0;
    printf("c Number of pairs detected: %d\n", pairs.size());

    int pair_cnt = 0;


    auto &p = pairs[pairs.size()-1];
    auto ta = get_var_as_output_aiger(aiger, p.second.first);
    auto tb = get_var_as_output_aiger(aiger, p.second.second);
    FILE* f0 = fopen("test0.aiger", "w");
    FILE* f1 = fopen("test1.aiger", "w");

    //aiger_write_to_file(ta aiger_mode::aiger_binary_mode, f0);
    //aiger_write_to_file(ta, aiger_mode::aiger_binary_mode, f1);

    for(auto& pr : pairs) {
        int a = pr.second.first;
        int b = pr.second.second;

        printf("[%d/%d] check-eq %d %d  (max-topo: %d)\n",++pair_cnt, pairs.size(), a, b, pr.first);//13148

        // bool eq1 = check_var_equal(aiger, a, b);
        // bool eq2 = check_var_equal_new(aiger, a, b);

        // if(eq1 != eq2) {
        //     printf("TEST FAILED\n");
        //     exit(0);
        // }

        #if ENABLE_MERGE_NODE

        if(father(a) != father(b) && check_var_equal(aiger, father(a), father(b))) {
            printf("result is eq: %d %d\n", a, b);
            merge_node(aiger, a, b);

            ++s;
            eqn.insert(a);
            eqn.insert(b);
            eqs.push_back(std::make_pair(a, b));
        }

        #else

        if(check_var_equal(aiger, a, b)) {
            printf("result is eq: %d %d\n", a, b);
            ++s;
            eqn.insert(a);
            eqn.insert(b);
            eqs.push_back(std::make_pair(a, b));
        }

        #endif
    }
    printf("c Number of equivalent pairs: %d\n", s);
    printf("checking entire graph...\n");

    check_entire_problem(aiger);

    return 0;
}