#include <bits/stdc++.h>

#include "circuit.h"
#include "polynomial.h"

Var* pvar(int id) {
    static std::map<int, Var*> mp;
    if(mp.count(id)) return mp[id];

    std::string name = "A" + std::to_string(abs(id));
    if(id < 0) name = "N" + name;

    Var* var = new Var(name.c_str(), id > 0 ? Gates[id].topo_index : (100000 + id) );

    return mp[id] = var;
}
bool subsitute(Polynomial* &a, Polynomial* b) {
    
    Polynomial* result = divide_by_term(a, b->get_lt());

    auto ltm = new Monomial(minus_one, b->get_lt());
    push_mstack(ltm);
    auto ltp = build_poly();

    Polynomial* to_minus = multiply_poly(result, ltp);

    Polynomial* new_result = add_poly(a, to_minus);

    for(int i=1; i<b->size(); i++) {
        push_mstack_end(b->get_mon(i));
    }
    Polynomial* tail = build_poly();
    
    Polynomial* new_tail = multiply_poly(result, tail);

    mpz_t c; mpz_init(c);
    mpz_mul(c, b->get_mon(0)->coeff, minus_one);
    Polynomial* tail_with_c = multiply_poly_with_constant(new_tail, c);

    Polynomial* done = add_poly(tail_with_c, new_result);

    // printf("=======subsitute======\n");
    // printf("a: "); a->print(stdout);
    // printf("b: "); b->print(stdout);
    // printf("result: "); result->print(stdout);
    // printf("to_minus: "); to_minus->print(stdout);
    // printf("new_result: "); new_result->print(stdout);
    // printf("tail: "); tail->print(stdout);
    // printf("new_tail: "); new_tail->print(stdout);
    // printf("tail_with_c: "); tail_with_c->print(stdout);
    // printf("done: "); done->print(stdout);

    a = done;
    return result->is_constant_zero_poly();
}

void poly_mod2(Polynomial* &p) {
    for(int i=0; i<p->num_mon; i++) {
        Monomial* m = p->get_mon(i);
        mpz_mod_ui(m->coeff, m->coeff, 2);
        mpz_add_ui(m->coeff, m->coeff, 2);
        mpz_mod_ui(m->coeff, m->coeff, 2);
        if(mpz_cmp_ui(m->coeff, 0) != 0) {
            push_mstack(m);
        }
    }
    p = build_poly();
}

Polynomial* getPolyOfGate(int id) {
    CircuitGate gate = Gates[id];
    if(gate.type == AND) {
        add_to_vstack(pvar(id));
        push_mstack(new Monomial(minus_one, build_term_from_stack()));
        for(auto& in : gate.inputs) {
            add_to_vstack(pvar(in));
        }
        push_mstack(new Monomial(one, build_term_from_stack()));
        return build_poly();
    }
    if(gate.type == XOR) {
        add_to_vstack(pvar(id));
        push_mstack(new Monomial(minus_one, build_term_from_stack()));
        for(auto& in : gate.inputs) {
            add_to_vstack(pvar(in));
            push_mstack(new Monomial(one, build_term_from_stack()));
        }
        return build_poly();
    } 
    if(gate.type == MAJ) {
        add_to_vstack(pvar(id));
        push_mstack(new Monomial(minus_one, build_term_from_stack()));
        add_to_vstack(pvar(gate.inputs[0]));
        add_to_vstack(pvar(gate.inputs[1]));
        push_mstack(new Monomial(one, build_term_from_stack()));
        add_to_vstack(pvar(gate.inputs[0]));
        add_to_vstack(pvar(gate.inputs[2]));
        push_mstack(new Monomial(one, build_term_from_stack()));
        add_to_vstack(pvar(gate.inputs[1]));
        add_to_vstack(pvar(gate.inputs[2]));
        push_mstack(new Monomial(one, build_term_from_stack()));
        return build_poly();
    }
    if(gate.type == OR) {
        assert(gate.inputs.size() == 2);
        add_to_vstack(pvar(id));
        push_mstack(new Monomial(minus_one, build_term_from_stack()));
        add_to_vstack(pvar(gate.inputs[0]));
        push_mstack(new Monomial(one, build_term_from_stack()));
        add_to_vstack(pvar(gate.inputs[1]));
        push_mstack(new Monomial(one, build_term_from_stack()));
        add_to_vstack(pvar(gate.inputs[0]));
        add_to_vstack(pvar(gate.inputs[1]));
        push_mstack(new Monomial(one, build_term_from_stack()));
        return build_poly();
    }
}

bool poly_cmp(Polynomial *a, Polynomial *b) {
    return a->get_lt()->get_var()->get_level() > b->get_lt()->get_var()->get_level();
}

std::map<Polynomial*, Polynomial*> another;
int main(int argv, char* args[]) {

    init_mpz(19260817);

    if(argv != 2) {
        printf("usage: ./acec <AIG-FILE>\n");
        return -1;
    }

    char also_cmd[1024];
    sprintf(also_cmd, "also -c \"read_aiger %s; convert --aig_to_xmg; write_verilog -x test.v\"", args[1]);
    system(also_cmd);

    read_verilog_from_file("test.v");
    print_circuit_structure();

    std::map<std::string, Polynomial*> nas;
    for(int i=1; i<=circuit_output; i++) {
        add_to_vstack(pvar(-i));
        push_mstack(new Monomial(one, build_term_from_stack()));
        add_to_vstack(pvar(i));
        push_mstack(new Monomial(one, build_term_from_stack()));
        push_mstack(new Monomial(minus_one, build_term_from_stack()));
        Polynomial *poly = build_poly();
        nas[pvar(-i)->get_name()] = poly;
        nas[pvar(i)->get_name()] = poly;
    }

    std::vector<Polynomial*> polys;

    for (int i = 1; i <= circuit_output; i++) {

        if(Gates[i].inputs.size() == 0) continue;

        Polynomial *result = getPolyOfGate(i);

        printf("  original:\t"); result->print(stdout);

        while(result->get_lt()->get_var_name()[0] == 'N') {
            Polynomial *to_div = nas[result->get_lt()->get_var_name()];
            subsitute(result, to_div);
        }

        printf("  pos-var:\t"); result->print(stdout);

        polys.push_back(result);
    }

    add_to_vstack(pvar(140));
    push_mstack(new Monomial(one, build_term_from_stack()));

    Polynomial *result = build_poly();

    std::sort(polys.begin(), polys.end(), poly_cmp);

    for(auto p : polys) {
        printf("now: "); result->print(stdout);
        printf("div: "); p->print(stdout);
        subsitute(result, p);
        poly_mod2(result);
    }

    printf("now: "); result->print(stdout);
    
    return 0;
}