#include <bits/stdc++.h>

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


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 getPolyOfGate(Sweep* s, int gateid, Polynomial* &resultA, Polynomial* &resultB) {
//     circuit *c = &(s->C[abs(gateid)]);
//     gateid = abs(gateid) * (c->neg ? -1 : 1);
//     if(c->type == And) {
//         add_to_vstack(pvar(gateid));
//         push_mstack(new Monomial(minus_one, build_term_from_stack()));
//         for(int i=0; i<c->sz; i++) {
//             add_to_vstack(pvar(c->to[i]));
//         }
//         push_mstack(new Monomial(one, build_term_from_stack()));
//         resultA = build_poly();
//     } else if(c->type == Xor) {
//         add_to_vstack(pvar(gateid));
//         push_mstack(new Monomial(minus_one, build_term_from_stack()));
//         add_to_vstack(pvar(c->to[0]));
//         add_to_vstack(pvar(c->to[1]));
//         push_mstack(new Monomial(minus_two, build_term_from_stack()));
//         add_to_vstack(pvar(c->to[0]));
//         push_mstack(new Monomial(one, build_term_from_stack()));
//         add_to_vstack(pvar(c->to[1]));
//         push_mstack(new Monomial(one, build_term_from_stack()));
//         resultA = build_poly();
//     } else if(c->type == HA) {
//         add_to_vstack(pvar(gateid));
//         push_mstack(new Monomial(minus_one, build_term_from_stack()));
//         add_to_vstack(pvar(c->to[0]));
//         add_to_vstack(pvar(c->to[1]));
//         push_mstack(new Monomial(minus_two, build_term_from_stack()));
//         add_to_vstack(pvar(c->to[0]));
//         push_mstack(new Monomial(one, build_term_from_stack()));
//         add_to_vstack(pvar(c->to[1]));
//         push_mstack(new Monomial(one, build_term_from_stack()));
//         resultA = build_poly();

//         add_to_vstack(pvar(c->carrier));
//         push_mstack(new Monomial(minus_one, build_term_from_stack()));
//         for(int i=0; i<c->sz; i++) {
//             add_to_vstack(pvar(c->to[i]));
//         }
//         push_mstack(new Monomial(one, build_term_from_stack()));
//         resultB = build_poly();
//     } else if(c->type == FA) {
//         add_to_vstack(pvar(gateid));
//         push_mstack(new Monomial(minus_one, build_term_from_stack()));
//         add_to_vstack(pvar(c->to[0]));
//         push_mstack(new Monomial(one, build_term_from_stack()));
//         add_to_vstack(pvar(c->to[1]));
//         push_mstack(new Monomial(one, build_term_from_stack()));
//         add_to_vstack(pvar(c->to[2]));
//         push_mstack(new Monomial(one, build_term_from_stack()));

//         add_to_vstack(pvar(c->to[0]));
//         add_to_vstack(pvar(c->to[1]));
//         push_mstack(new Monomial(minus_two, build_term_from_stack()));

//         add_to_vstack(pvar(c->to[1]));
//         add_to_vstack(pvar(c->to[2]));
//         push_mstack(new Monomial(minus_two, build_term_from_stack()));

//         add_to_vstack(pvar(c->to[0]));
//         add_to_vstack(pvar(c->to[2]));
//         push_mstack(new Monomial(minus_two, build_term_from_stack()));

//         add_to_vstack(pvar(c->to[0]));
//         add_to_vstack(pvar(c->to[1]));
//         add_to_vstack(pvar(c->to[2]));
//         push_mstack(new Monomial(four, build_term_from_stack()));
        
//         resultA = build_poly();

//         add_to_vstack(pvar(c->carrier));
//         push_mstack(new Monomial(minus_one, build_term_from_stack()));
//         add_to_vstack(pvar(c->to[0]));
//         add_to_vstack(pvar(c->to[1]));
//         push_mstack(new Monomial(one, build_term_from_stack()));
//         add_to_vstack(pvar(c->to[0]));
//         add_to_vstack(pvar(c->to[2]));
//         push_mstack(new Monomial(one, build_term_from_stack()));
//         add_to_vstack(pvar(c->to[1]));
//         add_to_vstack(pvar(c->to[2]));
//         push_mstack(new Monomial(one, build_term_from_stack()));
//         add_to_vstack(pvar(c->to[0]));
//         add_to_vstack(pvar(c->to[1]));
//         add_to_vstack(pvar(c->to[2]));
//         push_mstack(new Monomial(minus_two, build_term_from_stack()));
        
//         resultB = build_poly();
//     } else if(c->type == Majority) {
//         add_to_vstack(pvar(gateid));
//         push_mstack(new Monomial(minus_one, build_term_from_stack()));
//         add_to_vstack(pvar(c->to[0]));
//         add_to_vstack(pvar(c->to[1]));
//         push_mstack(new Monomial(one, build_term_from_stack()));
//         add_to_vstack(pvar(c->to[0]));
//         add_to_vstack(pvar(c->to[2]));
//         push_mstack(new Monomial(one, build_term_from_stack()));
//         add_to_vstack(pvar(c->to[1]));
//         add_to_vstack(pvar(c->to[2]));
//         push_mstack(new Monomial(one, build_term_from_stack()));
//         add_to_vstack(pvar(c->to[0]));
//         add_to_vstack(pvar(c->to[1]));
//         add_to_vstack(pvar(c->to[2]));
//         push_mstack(new Monomial(minus_two, build_term_from_stack()));
//         resultA = 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");

    // std::map<std::string, Polynomial*> nas;
    // for(int i=1; i<=S->maxvar; 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;

    // std::set<int> reserved_vars;
    // std::vector<Polynomial*> subsitute_vars;
    // for (int i = 1; i <= S->maxvar; i++) {
    //     circuit *c = &(S->C[i]);
    //     if (!c->sz || S->del[i] == 2) continue;
    //     if(c->type == Xor) {
    //         reserved_vars.insert(i);
    //         // for(int j=0; j<c->sz; j++)
    //         //     reserved_vars.insert(abs(c->to[j]));
    //     }
    // }
    // for (int i = 1; i <= S->maxvar; i++) {
    //     circuit *c = &(S->C[i]);
    //     if (!c->sz || S->del[i] == 2) continue;
    //     if(!reserved_vars.count(i)) {
    //         Polynomial *p, *q;
    //         getPolyOfGate(S, i, p, q);
    //         while(p->get_lt()->get_var_name()[0] == 'N') {
    //             Polynomial *to_div = nas[p->get_lt()->get_var_name()];
    //             subsitute(p, to_div);
    //         }
    //         subsitute_vars.push_back(p);
    //     }
    // }

    // printf("reserved: %d ; subsitute: %d\n", reserved_vars.size(), subsitute_vars.size());

    // for (int i = 1; i <= S->maxvar; i++) {
    //     circuit *c = &(S->C[i]);
    //     if (!c->sz || S->del[i] == 2) continue;
    // }

    // for (int i = 1; i <= S->maxvar; i++) {
    //     circuit *c = &(S->C[i]);
    //     if (!c->sz || S->del[i] == 2) continue;

    //     if(!reserved_vars.count(i)) continue;

    //     //if(c->sz == 2 && abs(c->to[0]) <= 14 && abs(c->to[1]) <= 14) continue;

    //     Polynomial *resultA, *resultB = nullptr;
    //     getPolyOfGate(S, i, resultA, resultB);

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

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

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

    //     for(auto subs : subsitute_vars) {
    //         //printf("delete: "); subs->print(stdout);
    //         subsitute(resultA, subs);
    //     }

    //     printf("  xor-relative:\t"); resultA->print(stdout);

    //     polys.push_back(resultA);
        
    //     if (c->type == HA || c->type == FA) {
    //         printf("( %d %d )", i * (S->C[i].neg ? -1 : 1), c->carrier); 
    //     }
    //     else {
    //         printf("%d", i * (S->C[i].neg ? -1 : 1));
    //     }

    //     printf(" = %s ( ", gate_type[c->type].c_str());

    //     for (int j = 0; j < c->sz; j++) {
    //         printf("%d ", c->to[j]);
    //     }
    //     puts(")");
    // }

    // add_to_vstack(pvar(32));
    // 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);
    // }
    
    return 0;
}

// for (int i = 1; i <= S->maxvar; i++) {
    //     circuit *c = &(S->C[i]);
    //     if (!c->sz || S->del[i] == 2) continue;

    //     if(c->type == And) {
    //         char term[1024];
    //         sprintf(term, "-%s+%s", pvar(i * (S->C[i].neg ? -1 : 1)), pvar(c->to[0]));
    //         for(int i=1; i<c->sz; i++) {
    //             sprintf(term, "%s*%s", term, pvar(c->to[i]));
    //         }
    //         polynomialArray.push_back(term);
    //         printf("%s\n", term);
    //     }
    //     if(c->type == Xor) {
    //         string last = pvar(c->to[0]);
    //         char term[1024];
    //         for(int i=1; i<c->sz-1; i++) {
    //             string tmp = pvar(++t);
    //             sprintf(term, "-%s-2*%s*%s+%s+%s", tmp.c_str(), last.c_str(), pvar(c->to[i]), last.c_str(), pvar(c->to[i]));
    //             polynomialArray.push_back(term);
    //             printf("%s\n", term);
    //             last = tmp;
    //         }
    //         sprintf(term, "-%s-2*%s*%s+%s+%s", pvar(i * (S->C[i].neg ? -1 : 1)), last.c_str(), pvar(c->to[c->sz-1]), last.c_str(), pvar(c->to[c->sz-1]));
    //         polynomialArray.push_back(term);
    //         printf("%s\n", term);
    //     }

    //     if (c->type == HA || c->type == FA) {
    //         char term[1024];
    //         sprintf(term, "-%s-2*%s+%s", pvar(i * (S->C[i].neg ? -1 : 1)), pvar(c->carrier), pvar(c->to[0]));
    //         for(int i=1; i<c->sz; i++) {
    //             sprintf(term, "%s+%s", term, pvar(c->to[i]));
    //         }
    //         polynomialArray.push_back(term);
    //         printf("%s\n", term);
    //     }

    //     if(c->type == Majority) {
    //         char term[1024];
    //         sprintf(term, "-%s-2*%s+%s", pvar(++t), pvar(i * (S->C[i].neg ? -1 : 1)), pvar(c->to[0]));
    //         for(int i=1; i<c->sz; i++) {
    //             sprintf(term, "%s+%s", term, pvar(c->to[i]));
    //         }
    //         polynomialArray.push_back(term);
    //         printf("%s\n", term);
    //     }
        
        // if (c->type == HA || c->type == FA) {
        //     printf("( %d %d )", i * (S->C[i].neg ? -1 : 1), c->carrier); 
        // }
        // else {
        //     printf("%d", i * (S->C[i].neg ? -1 : 1));
        // }

        // printf(" = %s ( ", gate_type[c->type].c_str());

        // for (int j = 0; j < c->sz; j++) {
        //     printf("%d ", c->to[j]);
        // }
        // puts(")");
    // }

    // for(int i=t; i>=1; i--) {
    //     variableName.push_back(pvar(i));
    //     variableName.push_back(pvar(-i));
    //     char term[1024];
    //     sprintf(term, "-%s+%s^2", pvar(i), pvar(i));
    //     polynomialArray.emplace_back(term);
    //     printf("%s\n", term);
    //     sprintf(term, "%s+%s", pvar(i), pvar(-i));
    //     polynomialArray.emplace_back(term);
    //     printf("%s\n", term);
    // }

    // char term[1024];
    // sprintf(term, "-%s+1", pvar(S->maxvar));
    // polynomialArray.emplace_back(term);
    // printf("%s\n", term);

    // for(int i = 0; i < 6; i++)
    // {
    //     variableName.push_back('x'+to_string(i));
    // }
    
    // // Fill the polynomial array.
    // polynomialArray.emplace_back("x0+x1+x2+x3+x4+x5");
    // polynomialArray.emplace_back("x0*x1+x1*x2+x2*x3+x3*x4+x0*x5+x4*x5");
    // polynomialArray.emplace_back("x0*x1*x2+x1*x2*x3+x2*x3*x4+x0*x1*x5+x0*x4*x5+x3*x4*x5");
    // polynomialArray.emplace_back("x0*x1*x2*x3+x1*x2*x3*x4+x0*x1*x2*x5+x0*x1*x4*x5+x0*x3*x4*x5+x2*x3*x4*x5");
    // polynomialArray.emplace_back("x0*x1*x2*x3*x4+x0*x1*x2*x3*x5+x0*x1*x2*x4*x5+x0*x1*x3*x4*x5+x0*x2*x3*x4*x5+x1*x2*x3*x4*x5");
    // polynomialArray.emplace_back("x0*x1*x2*x3*x4*x5-1");
    
    // Compute a reduce groebner basis.
    //vector<string> basis = groebnerBasisF4(7, variableName.size(), variableName, polynomialArray, 1, 0);
    
    // for(size_t i = 0; i < basis.size(); i++)
    // {
    //     cout << basis[i] << endl;
    // }

// for(int i=1; i<=t; i++) {
    //     printf("(declare-fun %s () Bool)\n", pvar(i).c_str());
    // }

    // for (int i = 1; i <= S->maxvar; i++) {
    //     circuit *c = &(S->C[i]);
    //     if (!c->sz || S->del[i] == 2) continue;
    //     int var = i * (S->C[i].neg ? -1 : 1);

    //     if(c->type == And) {
    //         string clause = "(assert (= " + pvar(var) + " (and";
    //         for(int i=0; i<c->sz; i++) {
    //             clause +=  " " + pvar(c->to[i]);
    //         }
    //         clause += ")))";
    //         cout << clause << endl;
    //     }
    //     if(c->type == Xor) {
    //         string clause = "(assert (= " + pvar(var) + " (xor";
    //         for(int i=0; i<c->sz; i++) {
    //             clause +=  " " + pvar(c->to[i]);
    //         }
    //         clause += ")))";
    //         cout << clause << endl;
    //     }

    //     if (c->type == HA || c->type == FA) {
    //         string clause = "(assert (= (+ " + pvar(var) + " (* 2 "+pvar(c->carrier)+")) (+ ";
    //         for(int i=0; i<c->sz; i++) {
    //             clause +=  " " + pvar(c->to[i]);
    //         }
    //         clause += ")))";
    //         cout << clause << endl;
    //     }

    //     if(c->type == Majority) {
    //         string ta = pvar(c->to[0]);
    //         string tb = pvar(c->to[1]);
    //         string tc = pvar(c->to[2]);
    //         string clause = "(assert (= "+pvar(var)+" (or (and "+ta+" "+tb+") (and "+ta+" "+tc+") (and "+tb+" "+tc+"))))";
    //         cout << clause << endl;
    //     }
        
    //     // if (c->type == HA || c->type == FA) {
    //     //     printf("( %d %d )", i * (S->C[i].neg ? -1 : 1), c->carrier); 
    //     // }
    //     // else {
    //     //     printf("%d", i * (S->C[i].neg ? -1 : 1));
    //     // }

    //     // printf(" = %s ( ", gate_type[c->type].c_str());

    //     // for (int j = 0; j < c->sz; j++) {
    //     //     printf("%d ", c->to[j]);
    //     // }
    //     // puts(")");
    // }

    // printf("(assert (= false %s))\n", pvar(S->maxvar).c_str());

    // printf("(check-sat)\n");
    //printf("(get-model)\n");