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


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