#include "sweep.hpp"
#include "circuit.hpp"
#include "src/cadical.hpp"
extern "C" {
    #include "aiger.h"
}

void Sweep::propagate(int* input, int* result) {

    std::queue<int> q;

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

    static int* topo_counter = new int[maxvar + 1];
    memset(topo_counter, 0, (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;

            }
        }
    }
}

void Sweep::circuit_propagate(int *input, int* result) {
    std::queue<int> q;

    for(int i=1; i<=aig->num_inputs; i++) {
        result[i] = input[i - 1];
        q.push(i);
        // printf("%d %d\n", i, result[i]);
    }
    for (int i = 1; i <= maxvar; i++) seen[i] = 0;
    while(!q.empty()) {
        int x = q.front();
        q.pop();
        for (int i = 0; i < inv_C[x].size(); i++) {
            int v = inv_C[x][i];
            seen[v]++;
            if (seen[v] == C[v].sz) {
                q.push(v);
                if (C[v].type == And) {
                    result[v] = 1;
                    for (int j = 0; j < C[v].sz; j++) {
                        int x = C[v][j];
                        result[v] &= x > 0 ? result[abs(x)] : !result[abs(x)];
                    }
                }
                else if (C[v].type == Xor) {
                    result[v] = 0;
                    for (int j = 0; j < C[v].sz; j++) {
                        int x = C[v][j];
                        result[v] ^= x > 0 ? result[abs(x)] : !result[abs(x)];
                    }
                }
                else if (C[v].type == Majority) {
                    int s[2] = {0, 0};
                    for (int j = 0; j < C[v].sz; j++) {
                        int x = C[v][j];
                        s[x > 0 ? result[abs(x)] : !result[abs(x)]]++;
                    }
                    result[v] = s[1] > s[0] ? 1 : 0;
                }
                else if (C[v].type == HA) {
                    assert(C[v].sz == 2);
                    int s = 0;
                    for (int j = 0; j < C[v].sz; j++) {
                        int x = C[v][j];
                        s += x > 0 ? result[abs(x)] : !result[abs(x)];
                    }
                    result[v] = s % 2;
                    result[abs(C[v].carrier)] = s >> 1;
                    if (C[v].carrier < 0) result[abs(C[v].carrier)] = !result[abs(C[v].carrier)];
                    q.push(abs(C[v].carrier));
                }
                else if (C[v].type == FA) {
                    assert(C[v].sz == 3);
                    int s = 0;
                    for (int j = 0; j < C[v].sz; j++) {
                        int x = C[v][j];
                        s += x > 0 ? result[abs(x)] : !result[abs(x)];
                    }
                    result[v] = s % 2;
                    result[abs(C[v].carrier)] = s >> 1;
                    if (C[v].carrier < 0) result[abs(C[v].carrier)] = !result[abs(C[v].carrier)];
                    q.push(abs(C[v].carrier));
                }
                if (C[v].neg) result[v] = !result[v];
                // printf("%d %d\n", v, result[v]);
            }
        }
    }

}

// int  Sweep::seen_cut_points(aiger* aig, int x, int y) {
//     std::queue<int> q;
//     int *used = 

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

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

// }

bool Sweep::check_var_equal(int x, int y, int assume) {

    std::queue<int> q;

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

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

    int can_del = 2;

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

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

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

    //Assume -NV
    solver->add(-assume), solver->add(-x), solver->add(-y), solver->add(0);
    solver->add(-assume), solver->add(x), solver->add(y), solver->add(0);

    solver->assume (assume);

    int result = solver->solve ();  

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

bool Sweep::check_constant(int x, int val) {

    std::queue<int> q;
    x = x & 1 ? -aiger_lit2var(x) : aiger_lit2var(x);

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

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

        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;

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

    solver->assume (x * (val ? -1 : 1));

    int result = solver->solve();  
    return result == 20;
}

void Sweep::random_simulation() {
    
    int* result = new int[2 * maxvar + 2];
    int* circuit_res = new int[maxvar + 1];
    int* input_vector = new int[aig->num_inputs];

    for(int i=0; i<rounds; i++) 
    {
        if (i % 10000 == 0) printf("================================= %d ===========================\n", i);
        for(int i=0; i<aig->num_inputs; i++) {
            input_vector[i] = rand() % 2;
        }
        for (int i=0; i<det_v_sz; i++) {
            if (abs(det_v[i]) <= aig->num_inputs) input_vector[abs(det_v[i]) - 1] = det_v[i] > 0 ? 1 : 0;
        }
        memset(result, -1, (2 * maxvar + 2) * sizeof(int));
        memset(circuit_res, -1, (maxvar + 1) * sizeof(int));

        propagate(input_vector, result);
        circuit_propagate(input_vector, circuit_res);
        if (result[output] != !circuit_res[output >> 1]) {
            printf("wrong %d %d %d\n", output, !result[output], circuit_res[output >> 1]);
            for (int i = 1; i <= maxvar; i++) {
                if (circuit_res[i] == -1) continue;
                if (result[i * 2] != circuit_res[i]) printf("%d %d %d\n", i, result[i * 2], circuit_res[i]);
                printf("%d %d\n", i, result[i << 1]);
            }
            return;
        }
        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), sum_pos[v] += 1;
                else v0.push_back(v), sum_neg[v] += 1;
            }
            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) {
    //     int lit = clas[0];
    //     printf("[ ");
    //     for(auto &v : clas) {
    //         printf("%d ", v);
    //     }
    //     printf("] %d %d\n", sum_pos[lit], sum_neg[lit]);
    // }

}

void Sweep::simulation() {
    //printf("c =================================== detect =================================\n");    
    seen = new int[maxvar + 1];
    classes.push_back(std::vector<int>());
    for(int i=2; i<=maxvar*2+1; i++) {
        classes[0].push_back(i);
    }
   
    random_simulation();
}