437 lines
16 KiB
C++
437 lines
16 KiB
C++
#include <bits/stdc++.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);
|
|
|
|
|
|
// 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");
|