#include "solve.hpp"

#include "cryptominisat.h"
#include <assert.h>

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



#define ENABLE_INPUT_VAR_DIVIED 0
#define DIVEDED_VAR_NUM 48

#define ENABLE_MERGE_NODE 1

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

using namespace CMSat;
using std::vector;

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;

        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<aiger->num_inputs; i++) {
        aiger_add_input(result_aiger, aiger->inputs[i].lit, std::to_string(aiger->inputs[i].lit).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");

    //printf("aiger maxvar %d\n", result_aiger->maxvar);

    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 = ipasir_init();

    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;
            ipasir_add(solver, var);
            ipasir_add(solver, 0);
        }
    #endif

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

        can_del++;

        if(inputs.count(u)) 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;

        ipasir_add(solver, -u), ipasir_add(solver,  a), ipasir_add(solver, 0);
        ipasir_add(solver, -u), ipasir_add(solver,  b), ipasir_add(solver, 0);
        ipasir_add(solver, -a), ipasir_add(solver, -b), ipasir_add(solver, u), ipasir_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;
    }

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

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

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

    int result = ipasir_solve(solver);

    ipasir_release(solver);

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

    return result == 20;
}

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) {    

    solver = ipasir_init();

    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;
        }


        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;
        

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

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

        ipasir_add(solver, -a);
        ipasir_add(solver, -b);
        ipasir_add(solver, u);
        ipasir_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;

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

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

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

    int result = ipasir_solve(solver);

    //ipasir_set_conflict_limit(solver, 100000);

    ipasir_release(solver);

    printf("c final: %d\n", result);

    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[]) {

    
    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)]);

    
    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

    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] == -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");
    }

    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;

    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;
}





========================
#include "solve.hpp"

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

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 cal_topo_index(aiger *aiger) {

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

//     int cnt = 0;

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

//     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);
//                 topo_index[v] = ++cnt;
//             }
//         }
//     }
// }

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

    std::queue<int> q;

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

    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 = aiger_var2lit(rhs0_edge.to);

                Graph::Edge rhs1_edge = graph.redge[v][1];
                int rhs1 = aiger_var2lit(rhs1_edge.to);

                result[aiger_var2lit(v)] = result[rhs0 + rhs0_edge.neg] & result[rhs1 + rhs1_edge.neg];
                result[aiger_var2lit(v)+1] = !result[aiger_var2lit(v)];

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

            }
        }
    }
}


aiger* get_lit_as_output_aiger(aiger* aiger, unsigned lit) {

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

    q.push(aiger_lit2var(lit));
    used[aiger_lit2var(lit)] = 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;

        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<aiger->num_inputs; i++) {
        aiger_add_input(result_aiger, aiger->inputs[i].lit, std::to_string(aiger->inputs[i].lit).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, lit, "238901893");

    //printf("aiger maxvar %d\n", result_aiger->maxvar);

    return result_aiger;
}

bool check_var_equal(aiger* aiger, int x, int y) {

    //return true;


    solver = ipasir_init();

    //ipasir_reserve(solver, aiger->maxvar);


    // for(int i=0; i<150; i++) {
    //     int var =  aiger_lit2var(aiger->inputs[i].lit);
    //     if(rand() % 2) var = -var;
    //     ipasir_add(solver, var);
    //     ipasir_add(solver, 0);
    // }

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

    x = x & 1 ? -aiger_lit2var(x) : aiger_lit2var(x);
    y = y & 1 ? -aiger_lit2var(y) : aiger_lit2var(y);

    q.push(abs(x));
    q.push(abs(y));
    int can_del = 2;
    used[abs(x)] = true;
    used[abs(y)] = 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(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;
        

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

        //aiger_add_and(aiger, aiger_var2lit(u), aiger_var2lit(a) + graph.redge[u][0].neg, aiger_var2lit(b) + graph.redge[u][1].neg);
        //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(graph.redge[u][0].neg) a = -a;
        if(graph.redge[u][1].neg) b = -b;

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

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

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

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

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

    for(auto& pair : eqs) {
        int a = pair.first;
        int b = pair.second;
        // if (used[abs(a)] && used[abs(b)]) {
            ipasir_add(solver, -a), ipasir_add(solver,  b), ipasir_add(solver, 0);
            ipasir_add(solver,  a), ipasir_add(solver, -b), ipasir_add(solver, 0);
        // }
        // else printf("no used\n");
    }

    //ipasir_set_option(solver, "--time", 1);
    //ipasir_set_conflict_limit(solver, 10000);

    int result = ipasir_solve(solver);

    printf("result is %d\n", result);

    ipasir_release(solver);
    if (result == 20) printf("can delete %d vars\n", can_del);
    // printf("==============\n");
    return result == 20;
}


int fa[100000];
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;

    std::cout << "merge " << father(x) << " " << father(y) << std::endl;

    x = aiger_lit2var(father(x));
    y = aiger_lit2var(father(y));
    
    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;
        }
    }

    fa[y] = x;

    graph.edge[y].clear();
}

void check_entire_problem(aiger* aiger) {    

    solver = ipasir_init();

    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;
        }


        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;
        

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

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

        ipasir_add(solver, -a);
        ipasir_add(solver, -b);
        ipasir_add(solver, u);
        ipasir_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;

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

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

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

    int result = ipasir_solve(solver);

    //ipasir_set_conflict_limit(solver, 100000);

    ipasir_release(solver);

    printf("c final: %d\n", result);

    return;
}

bool check_var_equal_new(aiger* aiger, int x, int y) {
    auto aiger0 = get_lit_as_output_aiger(aiger, x);
    auto aiger1 = get_lit_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;
}

bool check_left_graph(aiger* aiger, std::map<int, int> &new_inputs, std::vector<std::vector<int>> &clauses) {
    std::queue<int> q;
    static int* used = new int[aiger->maxvar + 1];
    memset(used, 0, (aiger->maxvar + 1) * sizeof(int));

    solver = ipasir_init();

    for(auto& pair : new_inputs) {
        q.push(pair.first);
        used[pair.first] = true;
    }

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

        if(graph.redge[u].size() < 2) {
            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;

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

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

        ipasir_add(solver, -a);
        ipasir_add(solver, -b);
        ipasir_add(solver, u);
        ipasir_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;

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

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

    for(auto& pair : new_inputs) {
        ipasir_assume(solver, pair.second ? pair.first : -pair.first);
    }

    int res = ipasir_solve(solver);

    std::vector<int> failed_list;

    if(res == 20) {
        for(auto& pair : new_inputs) {
            int lit = pair.second ? pair.first : -pair.first;
            if(ipasir_failed(solver, lit)) {
                failed_list.push_back(-lit);
            }
        }
        classes.push_back(failed_list);

        // printf("failed list: ");
        // for(auto &v : failed_list) {
        //     printf("%d ", v);
        // }
        // printf("\n");
    }

    ipasir_release(solver);

    // printf("left result: %d\n", res);

    return true;
}

bool check_right_graph(aiger* aiger, std::map<int, int> &new_inputs, std::vector<std::vector<int>> &clauses) {
    std::queue<int> q;
    static int* used = new int[aiger->maxvar + 1];
    memset(used, 0, (aiger->maxvar + 1) * sizeof(int));

    solver = ipasir_init();

    for(auto&vec : classes) {
        for(auto &v : vec) {
            ipasir_add(solver, v);
        }
        ipasir_add(solver, 0);
    }
    
    int x = aiger_lit2var(aiger->outputs[0].lit);

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

    while(!q.empty()) {
        int u = q.front();
        q.pop();
 
        if(new_inputs.count(u)) {
            continue;
        }

        if(graph.redge[u].size() < 2) {
            printf("ERROR point %d has fanin size %d\n", u << 1, graph.redge[u].size());
            exit(-1);
        }

        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;

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

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

        ipasir_add(solver, -a);
        ipasir_add(solver, -b);
        ipasir_add(solver, u);
        ipasir_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;

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

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

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

    int res = ipasir_solve(solver);

    if(res == 20) {
        ipasir_release(solver);
        return true;
    }
    else if(res == 10) {
        for(auto& input : new_inputs) {
            new_inputs[input.first] = ipasir_val(solver, input.first) >= 0 ? 1 : 0;
            //printf("input[%d]=%d\n", input.first, ipasir_val(solver, input.first));
        }
        ipasir_release(solver);
        return false;
    } else {
        ipasir_release(solver);
        printf("UNKOWN ERROR\n");
        exit(-1);
    }
}

void topo_cut(aiger* aiger, int cut_topo) {
    printf("c trying cut by topo_index......\n");
    std::map<int, int> new_inputs;

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

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

        if(pr.first > cut_topo + 2) break;

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

        if(check_var_equal(aiger, a, b)) {
            printf("result is eq: %d %d\n", a, b);
            int x = a & 1 ? -aiger_lit2var(a) : aiger_lit2var(a);
            int y = b & 1 ? -aiger_lit2var(b) : aiger_lit2var(b);
            eqs.push_back(std::make_pair(x, y));
        }
    }

    for(int i=1; i<=aiger->maxvar; i++) {
        if(topo_index[i] == cut_topo - 2) {
            new_inputs[i] = -1;
        }
    }

    std::vector<std::vector<int>> clauses;

    while(!check_right_graph(aiger, new_inputs, clauses)) {
        for(auto& pair : new_inputs) {
            printf("%d ", pair.second);
        }
        printf("\n");
        
        check_left_graph(aiger, new_inputs, clauses);
    }

    printf("c cut points: %d\n", new_inputs.size());

    //printf("c final: %d\n", check_right_graph(aiger, new_inputs));

    return;
}


int main(int argv, char* args[]) {
    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)]);

    
    classes.push_back(std::vector<int>());
    for(int i=2; i<=aiger->maxvar*2+1; i+=2) {
        classes[0].push_back(i);
    }

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

    int tinput = 0;

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

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

        // if(tinput == (1 << aiger->num_inputs)) {
        //     cout << "simulate end!" << endl;
        //     break;
        // }
        // if(tinput % 1000 == 0) {
        //     cout << "simulate " << tinput << endl;
        // }
        // int tt = tinput;
        // for(int i=0; i<aiger->num_inputs; i++) {
        //     input_vector[i] = tt & 1;
        //     tt >>= 1;
        // }
        // tinput++;
        for(int i=0; i<aiger->num_inputs; i++) {
            input_vector[i] = rand() % 2;
        }
        memset(result, -1, (2 * aiger->maxvar + 2) * sizeof(int));

        simulate(aiger, input_vector, result);

        for(int i=2; i<(2 * aiger->maxvar + 2); i++) {
            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;

        // cout << "classes: " << endl;
        // for(auto& clas : classes) {
        //     cout << "[ ";
        //     for(auto &v : clas) {
        //         cout << v << " ";
        //     }
        //     cout << "]" << endl;
        // }
    }
    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");
    }

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

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

    for(auto& clas : classes) {
        //if(clas.size() != 2) continue;
        std::vector<int> tmp;

        for(int i=0; i<clas.size(); i++) {
            for(int j=i+1; j<clas.size(); j++) {          
                int vara =  aiger_lit2var(clas[i]);
                int varb =  aiger_lit2var(clas[j]);
                pairs.push_back(std::make_pair(std::max(topo_index[vara], topo_index[varb]), std::make_pair(clas[i], clas[j])));
            }
        }
    }

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

    // test(aiger);
    // exit(0);

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

    // for(auto& pr : pairs) {
    //     printf("%d ", pr.first);
    // }
    // puts("");

    // topo_cut(aiger, topo_index[aiger_lit2var(aiger->outputs[0].lit)] / 2);
    // return 0;

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

    int pair_cnt = 0;

    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(check_var_equal(aiger, a, b)) {
            printf("result is eq: %d %d\n", a, b);
            ++s;
            int x = a & 1 ? -aiger_lit2var(a) : aiger_lit2var(a);
            int y = b & 1 ? -aiger_lit2var(b) : aiger_lit2var(b);
            eqs.push_back(std::make_pair(x, y));
        }
    }
    printf("c Number of equivalent pairs: %d\n", s);
    printf("checking entire graph...\n");

    check_entire_problem(aiger);

    return 0;
}









#include "solve.hpp"

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

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 cal_topo_index(aiger *aiger) {

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

//     int cnt = 0;

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

//     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);
//                 topo_index[v] = ++cnt;
//             }
//         }
//     }
// }

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

    std::queue<int> q;

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

    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 = aiger_var2lit(rhs0_edge.to);

                Graph::Edge rhs1_edge = graph.redge[v][1];
                int rhs1 = aiger_var2lit(rhs1_edge.to);

                result[aiger_var2lit(v)] = result[rhs0 + rhs0_edge.neg] & result[rhs1 + rhs1_edge.neg];
                result[aiger_var2lit(v)+1] = !result[aiger_var2lit(v)];

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

            }
        }
    }
}


aiger* get_lit_as_output_aiger(aiger* aiger, unsigned lit) {

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

    q.push(aiger_lit2var(lit));
    used[aiger_lit2var(lit)] = 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;

        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<aiger->num_inputs; i++) {
        aiger_add_input(result_aiger, aiger->inputs[i].lit, std::to_string(aiger->inputs[i].lit).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, lit, "238901893");

    //printf("aiger maxvar %d\n", result_aiger->maxvar);

    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) {
        int var = aiger_lit2var(p);
        q.push(var);
        used[var] = 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) {
    solver = ipasir_init();

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

    x = x & 1 ? -aiger_lit2var(x) : aiger_lit2var(x);
    y = y & 1 ? -aiger_lit2var(y) : aiger_lit2var(y);

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

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

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

        can_del++;

        if(inputs.count(u)) continue;
        // if(graph.redge[u].size() == 0) {
        //     //printf("eeeeeeee %d\n", u);
        //     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;

        ipasir_add(solver, -u), ipasir_add(solver,  a), ipasir_add(solver, 0);
        ipasir_add(solver, -u), ipasir_add(solver,  b), ipasir_add(solver, 0);
        ipasir_add(solver, -a), ipasir_add(solver, -b), ipasir_add(solver, u), ipasir_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;
    }

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

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

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

    int result = ipasir_solve(solver);

    ipasir_release(solver);

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

    return result == 20;
}
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);
    }

    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);
                printf("insert %d\n", 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;
}


int fa[100000];
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;

    std::cout << "merge " << father(x) << " " << father(y) << std::endl;

    x = aiger_lit2var(father(x));
    y = aiger_lit2var(father(y));
    
    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;
        }
    }

    fa[y] = x;

    graph.edge[y].clear();
}

void check_entire_problem(aiger* aiger) {    

    solver = ipasir_init();

    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;
        }


        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;
        

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

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

        ipasir_add(solver, -a);
        ipasir_add(solver, -b);
        ipasir_add(solver, u);
        ipasir_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;

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

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

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

    int result = ipasir_solve(solver);

    //ipasir_set_conflict_limit(solver, 100000);

    ipasir_release(solver);

    printf("c final: %d\n", result);

    return;
}

bool check_var_equal_new(aiger* aiger, int x, int y) {
    auto aiger0 = get_lit_as_output_aiger(aiger, x);
    auto aiger1 = get_lit_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;
}

bool check_left_graph(aiger* aiger, std::map<int, int> &new_inputs, std::vector<std::vector<int>> &clauses) {
    std::queue<int> q;
    static int* used = new int[aiger->maxvar + 1];
    memset(used, 0, (aiger->maxvar + 1) * sizeof(int));

    solver = ipasir_init();

    for(auto& pair : new_inputs) {
        q.push(pair.first);
        used[pair.first] = true;
    }

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

        if(graph.redge[u].size() < 2) {
            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;

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

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

        ipasir_add(solver, -a);
        ipasir_add(solver, -b);
        ipasir_add(solver, u);
        ipasir_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;

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

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

    for(auto& pair : new_inputs) {
        ipasir_assume(solver, pair.second ? pair.first : -pair.first);
    }

    int res = ipasir_solve(solver);

    std::vector<int> failed_list;

    if(res == 20) {
        for(auto& pair : new_inputs) {
            int lit = pair.second ? pair.first : -pair.first;
            if(ipasir_failed(solver, lit)) {
                failed_list.push_back(-lit);
            }
        }
        classes.push_back(failed_list);

        // printf("failed list: ");
        // for(auto &v : failed_list) {
        //     printf("%d ", v);
        // }
        // printf("\n");
    }

    ipasir_release(solver);

    // printf("left result: %d\n", res);

    return true;
}

bool check_right_graph(aiger* aiger, std::map<int, int> &new_inputs, std::vector<std::vector<int>> &clauses) {
    std::queue<int> q;
    static int* used = new int[aiger->maxvar + 1];
    memset(used, 0, (aiger->maxvar + 1) * sizeof(int));

    solver = ipasir_init();

    for(auto&vec : classes) {
        for(auto &v : vec) {
            ipasir_add(solver, v);
        }
        ipasir_add(solver, 0);
    }
    
    int x = aiger_lit2var(aiger->outputs[0].lit);

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

    while(!q.empty()) {
        int u = q.front();
        q.pop();
 
        if(new_inputs.count(u)) {
            continue;
        }

        if(graph.redge[u].size() < 2) {
            printf("ERROR point %d has fanin size %d\n", u << 1, graph.redge[u].size());
            exit(-1);
        }

        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;

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

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

        ipasir_add(solver, -a);
        ipasir_add(solver, -b);
        ipasir_add(solver, u);
        ipasir_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;

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

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

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

    int res = ipasir_solve(solver);

    if(res == 20) {
        ipasir_release(solver);
        return true;
    }
    else if(res == 10) {
        for(auto& input : new_inputs) {
            new_inputs[input.first] = ipasir_val(solver, input.first) >= 0 ? 1 : 0;
            //printf("input[%d]=%d\n", input.first, ipasir_val(solver, input.first));
        }
        ipasir_release(solver);
        return false;
    } else {
        ipasir_release(solver);
        printf("UNKOWN ERROR\n");
        exit(-1);
    }
}

void topo_cut(aiger* aiger, int cut_topo) {
    printf("c trying cut by topo_index......\n");
    std::map<int, int> new_inputs;

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

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

        if(pr.first > cut_topo + 2) break;

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

        if(check_var_equal(aiger, a, b)) {
            printf("result is eq: %d %d\n", a, b);
            int x = a & 1 ? -aiger_lit2var(a) : aiger_lit2var(a);
            int y = b & 1 ? -aiger_lit2var(b) : aiger_lit2var(b);
            eqs.push_back(std::make_pair(x, y));
        }
    }

    for(int i=1; i<=aiger->maxvar; i++) {
        if(topo_index[i] == cut_topo - 2) {
            new_inputs[i] = -1;
        }
    }

    std::vector<std::vector<int>> clauses;

    while(!check_right_graph(aiger, new_inputs, clauses)) {
        for(auto& pair : new_inputs) {
            printf("%d ", pair.second);
        }
        printf("\n");
        
        check_left_graph(aiger, new_inputs, clauses);
    }

    printf("c cut points: %d\n", new_inputs.size());

    //printf("c final: %d\n", check_right_graph(aiger, new_inputs));

    return;
}


int main(int argv, char* args[]) {
    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)]);

    
    classes.push_back(std::vector<int>());
    for(int i=2; i<=aiger->maxvar*2+1; i+=2) {
        classes[0].push_back(i);
    }

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

    int tinput = 0;

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

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

        // if(tinput == (1 << aiger->num_inputs)) {
        //     cout << "simulate end!" << endl;
        //     break;
        // }
        // if(tinput % 1000 == 0) {
        //     cout << "simulate " << tinput << endl;
        // }
        // int tt = tinput;
        // for(int i=0; i<aiger->num_inputs; i++) {
        //     input_vector[i] = tt & 1;
        //     tt >>= 1;
        // }
        // tinput++;
        for(int i=0; i<aiger->num_inputs; i++) {
            input_vector[i] = rand() % 2;
        }
        memset(result, -1, (2 * aiger->maxvar + 2) * sizeof(int));

        simulate(aiger, input_vector, result);

        for(int i=2; i<(2 * aiger->maxvar + 2); i++) {
            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;

        // cout << "classes: " << endl;
        // for(auto& clas : classes) {
        //     cout << "[ ";
        //     for(auto &v : clas) {
        //         cout << v << " ";
        //     }
        //     cout << "]" << endl;
        // }
    }
    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");
    }

    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) 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());

    // test(aiger);
    // exit(0);

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

    // for(auto& pr : pairs) {
    //     printf("%d ", pr.first);
    // }
    // puts("");

    // topo_cut(aiger, topo_index[aiger_lit2var(aiger->outputs[0].lit)] / 2);
    // return 0;

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

    int pair_cnt = 0;

    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(check_var_equal(aiger, a, b)) {
            printf("result is eq: %d %d\n", a, b);
            ++s;
            int x = a & 1 ? -aiger_lit2var(a) : aiger_lit2var(a);
            int y = b & 1 ? -aiger_lit2var(b) : aiger_lit2var(b);
            eqn.insert(x);
            eqn.insert(y);
            eqs.push_back(std::make_pair(x, y));
        }
    }
    printf("c Number of equivalent pairs: %d\n", s);
    printf("checking entire graph...\n");

    check_entire_problem(aiger);

    return 0;
}