diff --git a/.vscode/settings.json b/.vscode/settings.json index 379d8e4..48cb31a 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -1,6 +1,8 @@ { "files.associations": { "*.ejs": "html", - "iostream": "cpp" + "iostream": "cpp", + "*.tcc": "cpp", + "new": "cpp" } } \ No newline at end of file diff --git a/acec.cpp b/acec.cpp index d45d392..f1248a8 100644 --- a/acec.cpp +++ b/acec.cpp @@ -4,86 +4,362 @@ #include "circuit.hpp" #include "sweep.hpp" -#include "libopenf4.h" +//#include "libopenf4.h" +#include "src/cadical.hpp" + +#include "polynomial.h" extern "C" { #include "aiger.h" } -#define pvar(i) ((string((i) < 0 ? "N" : "") + "A" + std::to_string(abs(i))).c_str()) +Sweep *S; Sweep* sweep_init(int argv, char* args[]) { Sweep *S = new Sweep(); S->aig = aiger_init(); + S->solver = new CaDiCaL::Solver; S->det_v_sz = 0; S->file = fopen(args[1], "r"); + // S->rounds = atoi(args[2]); + // if (argv > 3) { + // S->det_v = new int[argv -3]; + // for (int i = 3; i < argv; i++) + // S->det_v[S->det_v_sz++] = atoi(args[i]); + // } return S; } +Var* pvar(int id) { + static std::map 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 ? S->topo_index[id] : (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; isize(); 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; isz; 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; isz; 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 another; int main(int argv, char* args[]) { - Sweep *S = sweep_init(argv, args); + + init_mpz(19260817); + + S = sweep_init(argv, args); + S->solve(); - using namespace std; - //using namespace F4; - - // Create polynomial array. - vector polynomialArray; - - // Create variable name array. - vector variableName; + std::map 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; + } - set vars; + std::vector polys; - int t = S->maxvar; + std::set reserved_vars; + std::vector 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; jsz; 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(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; isz; 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; isz-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(!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) { - 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; isz; i++) { - sprintf(term, "%s+%s", term, pvar(c->to[i])); - } - polynomialArray.push_back(term); - printf("%s\n", term); + printf("( %d %d )", i * (S->C[i].neg ? -1 : 1), c->carrier); + } + else { + printf("%d", i * (S->C[i].neg ? -1 : 1)); } - 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; isz; i++) { - sprintf(term, "%s+%s", term, pvar(c->to[i])); - } - polynomialArray.push_back(term); - printf("%s\n", term); + 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; isz; 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; isz-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; isz; 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; isz; 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); @@ -98,24 +374,24 @@ int main(int argv, char* args[]) { // 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); - } + // 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); + // 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++) // { @@ -131,17 +407,72 @@ int main(int argv, char* args[]) { // polynomialArray.emplace_back("x0*x1*x2*x3*x4*x5-1"); // Compute a reduce groebner basis. - vector basis = groebnerBasisF4(7, variableName.size(), variableName, polynomialArray, 1, 0); + //vector basis = groebnerBasisF4(7, variableName.size(), variableName, polynomialArray, 1, 0); - for(size_t i = 0; i < basis.size(); i++) - { - cout << basis[i] << endl; - } + // for(size_t i = 0; i < basis.size(); i++) + // { + // cout << basis[i] << endl; + // } - for(int i=t; i>=1; i--) { - printf("(declare-fun %s () Bool)", pvar(i)); - printf("(declare-fun %s () Bool)", pvar(-i)); - } - - return 0; -} \ No newline at end of file +// 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; isz; i++) { + // clause += " " + pvar(c->to[i]); + // } + // clause += ")))"; + // cout << clause << endl; + // } + // if(c->type == Xor) { + // string clause = "(assert (= " + pvar(var) + " (xor"; + // for(int i=0; isz; 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; isz; 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"); \ No newline at end of file diff --git a/acec.log b/acec.log new file mode 100644 index 0000000..e69de29 diff --git a/circuit.cpp b/circuit.cpp index 7cb6c89..c50d477 100644 --- a/circuit.cpp +++ b/circuit.cpp @@ -46,8 +46,8 @@ bool Sweep::match_majority(int x) { if (C[-v].outs <= 1) del[-v] = 2; if (C[-w].outs <= 1) del[-w] = 2; - C[x][0] = a; C[x][1] = b; - C[x].push(C[-w][1]); + C[x][0] = -a; C[x][1] = -b; + C[x].push(-C[-w][1]); C[x].type = Majority; return true; } @@ -163,7 +163,6 @@ void Sweep::match_FA() { for(int i=1; i<=maxvar; i++) { if (!C[i].sz || del[i] == 2) continue; - //printf("X: %d\n", i); circuit *c = &C[i]; @@ -347,7 +346,7 @@ void Sweep::to_dot_graph(const char* filename, int end_point) { /** * 删除初始输入 */ - if(abs(c->to[j]) <= num_inputs) continue; + if(abs(c->to[j]) <= 14) continue; sprintf(str, "A%d->A%d[arrowhead=%s]\n", abs(c->to[j]), u, !line_positive(c->to[j]) ? "dot" : "none"); file << str; @@ -365,6 +364,7 @@ void Sweep::to_dot_graph(const char* filename, int end_point) { } void Sweep::identify() { + del = new int[maxvar + 1]; for (int i = 1; i <= maxvar; i++) del[i] = 0; recalculate_outs(); @@ -373,21 +373,19 @@ void Sweep::identify() { if (match_xor(i)) continue; } - recalculate_outs(); + // recalculate_outs(); - for (int i = 1; i <= maxvar; i++) { - if (!C[i].sz || del[i] == 2) continue; - if (match_majority(i)) continue; - } + // for (int i = 1; i <= maxvar; i++) { + // if (!C[i].sz || del[i] == 2) continue; + // if (match_majority(i)) continue; + // } recalculate_outs(); - - adjust_not(); - match_HA(); + //adjust_not(); + //match_HA(); - to_multi_input_gates(); - - match_FA(); + //to_multi_input_gates(); + //match_FA(); // printf("digraph \"graph\" {\n"); // for (int i = 1; i <= maxvar; i++) { @@ -411,8 +409,35 @@ void Sweep::identify() { // } // printf("}\n"); - //to_dot_graph("graph1.dot", abs(C[maxvar].to[0])); - //to_dot_graph("graph2.dot", abs(C[maxvar].to[1])); + recalculate_outs(); + // for (int i = 1; i <= maxvar; i++) { + // circuit *c = &C[i]; + // if (!c->sz || del[i] == 2) continue; + + // if (c->type == HA || c->type == FA) + // printf("( %d %d )", i * (C[i].neg ? -1 : 1), c->carrier); + // else + // printf("%d", i * (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(")"); + // } + + inv_C = new vec[maxvar + 1]; + for (int i = 1; i <= maxvar; i++) { + circuit *c = &C[i]; + if (!c->sz || del[i] == 2) continue; + for (int j = 0; j < c->sz; j++) { + inv_C[abs(c->to[j])].push(i); + } + } + // to_dot_graph("graph1.dot", 291); + // to_dot_graph("graph2.dot", 175); // recalculate_outs(); // for (int i = 1; i <= maxvar; i++) { @@ -420,7 +445,5 @@ void Sweep::identify() { // if (del[i] == 2) continue; // printf("%d : %d (outs)\n", i, c->outs); // } - - - + } \ No newline at end of file diff --git a/cms.log b/cms.log new file mode 100644 index 0000000..8ae66aa --- /dev/null +++ b/cms.log @@ -0,0 +1,408 @@ +-293 -292 0 +-293 176 0 +292 -176 293 0 +-294 292 0 +-294 -176 0 +-292 176 294 0 +289 231 292 0 +-173 154 176 0 +-289 -288 0 +-289 287 0 +288 -287 289 0 +228 197 231 0 +-173 172 0 +-173 -157 0 +-172 157 173 0 +-151 124 154 0 +-288 -285 0 +-288 -242 0 +285 242 288 0 +-287 -286 0 +-287 -249 0 +286 249 287 0 +225 208 228 0 +-197 -196 0 +-197 195 0 +196 -195 197 0 +-172 171 0 +-172 -160 0 +-171 160 172 0 +-150 127 157 0 +-151 150 0 +-151 -127 0 +-150 127 151 0 +121 88 124 0 +-285 -284 0 +-285 283 0 +284 -283 285 0 +-242 -241 0 +-242 240 0 +241 -240 242 0 +-286 -285 0 +-286 -248 0 +285 248 286 0 +-249 -248 0 +-249 -242 0 +248 242 249 0 +222 216 225 0 +205 200 208 0 +-196 -193 0 +-196 -180 0 +193 180 196 0 +-195 -194 0 +-195 -187 0 +194 187 195 0 +-171 170 0 +-171 -163 0 +-170 163 171 0 +149 130 160 0 +-150 -149 0 +-150 -130 0 +149 130 150 0 +-119 116 127 0 +-121 -120 0 +-121 -115 0 +120 115 121 0 +85 78 88 0 +-284 -281 0 +-284 -255 0 +281 255 284 0 +-283 -282 0 +-283 -262 0 +282 262 283 0 +-241 -238 0 +-241 97 0 +238 -97 241 0 +-240 -239 0 +-240 -232 0 +239 232 240 0 +245 193 248 0 +-219 42 222 0 +213 20 216 0 +-205 -204 0 +-205 203 0 +204 -203 205 0 +-41 27 200 0 +190 31 193 0 +-180 179 0 +-180 -116 0 +-179 116 180 0 +-194 -193 0 +-194 -186 0 +193 186 194 0 +-187 -186 0 +-187 -180 0 +186 180 187 0 +-170 169 0 +-170 -166 0 +-169 166 170 0 +-147 144 163 0 +-149 -148 0 +-149 -143 0 +148 143 149 0 +112 109 130 0 +114 91 119 0 +-116 106 0 +-116 105 0 +-106 -105 116 0 +-120 -119 0 +-120 116 0 +119 -116 120 0 +-115 -114 0 +-115 -91 0 +114 91 115 0 +-82 81 85 0 +75 48 78 0 +-281 -280 0 +-281 279 0 +280 -279 281 0 +-255 -254 0 +-255 253 0 +254 -253 255 0 +-282 -281 0 +-282 -261 0 +281 261 282 0 +-262 -261 0 +-262 -255 0 +261 255 262 0 +-235 105 238 0 +-97 96 0 +-97 95 0 +-96 -95 97 0 +-239 -238 0 +-239 -58 0 +238 58 239 0 +-232 97 0 +-232 -58 0 +-97 58 232 0 +186 180 245 0 +82 21 219 0 +-42 5 0 +-42 4 0 +-5 -4 42 0 +-213 -212 0 +-213 211 0 +212 -211 213 0 +17 16 20 0 +-204 63 0 +-204 -31 0 +-63 31 204 0 +-203 -202 0 +-203 -201 0 +202 201 203 0 +38 37 41 0 +-27 26 0 +-27 25 0 +-26 -25 27 0 +63 54 190 0 +26 25 31 0 +-179 -178 0 +-179 -177 0 +178 177 179 0 +-183 62 186 0 +-169 168 0 +-169 167 0 +-168 -167 169 0 +-140 137 166 0 +142 133 147 0 +-144 12 0 +-144 6 0 +-12 -6 144 0 +-148 -147 0 +-148 144 0 +147 -144 148 0 +-143 -142 0 +-143 -133 0 +142 133 143 0 +103 94 112 0 +106 105 109 0 +-114 -113 0 +-114 -104 0 +113 104 114 0 +73 70 91 0 +-106 12 0 +-106 2 0 +-12 -2 106 0 +-105 6 0 +-105 5 0 +-6 -5 105 0 +-82 12 0 +-82 9 0 +-12 -9 82 0 +-81 -80 0 +-81 -79 0 +80 79 81 0 +-75 -74 0 +-75 -61 0 +74 61 75 0 +45 36 48 0 +-280 -277 0 +-280 -101 0 +277 101 280 0 +-279 -278 0 +-279 -269 0 +278 269 279 0 +-254 251 0 +-254 144 0 +-251 -144 254 0 +-253 -252 0 +-253 -250 0 +252 250 253 0 +258 238 261 0 +106 55 235 0 +-96 15 0 +-96 8 0 +-15 -8 96 0 +-95 13 0 +-95 3 0 +-13 -3 95 0 +53 52 58 0 +-21 11 0 +-21 7 0 +-11 -7 21 0 +-212 67 0 +-212 62 0 +-67 -62 212 0 +-211 -210 0 +-211 -209 0 +210 209 211 0 +-17 10 0 +-17 8 0 +-10 -8 17 0 +-16 14 0 +-16 13 0 +-14 -13 16 0 +-63 5 0 +-63 2 0 +-5 -2 63 0 +-202 54 0 +-202 -31 0 +-54 31 202 0 +-201 63 0 +-201 54 0 +-63 -54 201 0 +-38 15 0 +-38 2 0 +-15 -2 38 0 +-37 6 0 +-37 3 0 +-6 -3 37 0 +-26 8 0 +-26 7 0 +-8 -7 26 0 +-25 13 0 +-25 10 0 +-13 -10 25 0 +-54 53 0 +-54 52 0 +-53 -52 54 0 +-178 105 0 +-178 55 0 +-105 -55 178 0 +-177 106 0 +-177 55 0 +-106 -55 177 0 +67 28 183 0 +-62 15 0 +-62 6 0 +-15 -6 62 0 +-168 12 0 +-168 8 0 +-12 -8 168 0 +-167 13 0 +-167 5 0 +-13 -5 167 0 +135 134 140 0 +-137 12 0 +-137 11 0 +-12 -11 137 0 +-142 -141 0 +-142 -136 0 +141 136 142 0 +-101 98 133 0 +-103 -102 0 +-103 -97 0 +102 97 103 0 +-58 55 94 0 +-113 -112 0 +-113 -109 0 +112 109 113 0 +-104 -103 0 +-104 -94 0 +103 94 104 0 +60 51 73 0 +-67 66 70 0 +-80 67 0 +-80 -66 0 +-67 66 80 0 +-79 63 0 +-79 62 0 +-63 -62 79 0 +-74 -73 0 +-74 -70 0 +73 70 74 0 +-61 -60 0 +-61 -51 0 +60 51 61 0 +-42 41 45 0 +33 24 36 0 +-277 -276 0 +-277 275 0 +276 -275 277 0 +96 95 101 0 +-278 -277 0 +-278 -268 0 +277 268 278 0 +-269 -268 0 +-269 -101 0 +268 101 269 0 +-251 137 0 +-251 135 0 +-137 -135 251 0 +-252 251 0 +-252 98 0 +-251 -98 252 0 +-250 144 0 +-250 98 0 +-144 -98 250 0 +-97 58 258 0 +-55 15 0 +-55 11 0 +-15 -11 55 0 +-53 8 0 +-53 3 0 +-8 -3 53 0 +-52 13 0 +-52 7 0 +-13 -7 52 0 +-67 12 0 +-67 4 0 +-12 -4 67 0 +-210 62 0 +-210 28 0 +-62 -28 210 0 +-209 67 0 +-209 28 0 +-67 -28 209 0 +-28 11 0 +-28 3 0 +-11 -3 28 0 +-135 8 0 +-135 5 0 +-8 -5 135 0 +-134 15 0 +-134 13 0 +-15 -13 134 0 +-141 -140 0 +-141 137 0 +140 -137 141 0 +-136 135 0 +-136 134 0 +-135 -134 136 0 +-98 11 0 +-98 5 0 +-11 -5 98 0 +-102 -101 0 +-102 98 0 +101 -98 102 0 +-60 -59 0 +-60 -54 0 +59 54 60 0 +-31 28 51 0 +63 62 66 0 +-33 -32 0 +-33 -27 0 +32 27 33 0 +-21 20 24 0 +-276 -273 0 +-276 134 0 +273 -134 276 0 +-275 -274 0 +-275 -270 0 +274 270 275 0 +-265 251 268 0 +-59 -58 0 +-59 55 0 +58 -55 59 0 +-32 -31 0 +-32 28 0 +31 -28 32 0 +137 135 273 0 +-274 -273 0 +-274 169 0 +273 -169 274 0 +-270 169 0 +-270 134 0 +-169 -134 270 0 +144 98 265 0 +-293 -294 0 +293 294 0 +-251 252 0 +251 -252 0 +-253 255 0 +253 -255 0 +-254 266 0 +254 -266 0 +-176 292 0 +176 -292 0 +c Solver::solve( ) diff --git a/f4cpp b/f4cpp deleted file mode 160000 index 645458c..0000000 --- a/f4cpp +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 645458ca02450215bd0e891fc3081d8cbc79c51f diff --git a/fraig.cpp b/fraig.cpp new file mode 100644 index 0000000..1e8089f --- /dev/null +++ b/fraig.cpp @@ -0,0 +1,291 @@ +#include "sweep.hpp" +#include "circuit.hpp" +#include "src/cadical.hpp" +extern "C" { + #include "aiger.h" +} + +void Sweep::propagate(int* input, int* result) { + + std::queue q; + + for(int i=0; inum_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 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 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 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 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; inum_inputs; i++) { + input_vector[i] = rand() % 2; + } + for (int i=0; inum_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> tmp; + for(auto& clas : classes) { + std::vector v0; + std::vector 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()); + for(int i=2; i<=maxvar*2+1; i++) { + classes[0].push_back(i); + } + + random_simulation(); +} \ No newline at end of file diff --git a/hCaD_V2/BUILD.md b/hCaD_V2/BUILD.md new file mode 100644 index 0000000..8804f3f --- /dev/null +++ b/hCaD_V2/BUILD.md @@ -0,0 +1,104 @@ +# CaDiCaL Build + +Use `./configure && make` to configure and build `cadical` in the default +`build` sub-directory. + +This will also build the library `libcadical.a` as well as the model based +tester `mobical`: + + build/cadical + build/mobical + build/libcadical.a + +The header file of the library is in + + src/cadical.hpp + +The build process requires GNU make. Using the generated `makefile` with +GNU make compiles separate object files, which can be cached (for instance +with `ccache`). In order to force parallel build you can use the '-j' +option either for 'configure' or with 'make'. If the environment variable +'MAKEFLAGS' is set, e.g., 'MAKEFLAGS=-j ./configure', the same effect +is achieved and the generated makefile will use those flags. + +Options +------- + +You might want to check out options of `./configure -h`, such as + + ./configure -c # include assertion checking code + + ./configure -l # include code to really see what the solver is doing + + ./configure -a # both above and in addition `-g` for debugging. + +You can easily use multiple build directories, e.g., + + mkdir debug; cd debug; ../configure -g; make + +which compiles and builds a debugging version in the sub-directory `debug`, +since `-g` was specified as parameter to `configure`. The object files, +the library and the binaries are all independent of those in the default +build directory `build`. + +All source files reside in the `src` directory. The library `libcadical.a` +is compiled from all the `.cpp` files except `cadical.cpp` and +`mobical.cpp`, which provide the applications, i.e., the stand alone solver +`cadical` and the model based tester `mobical`. + +Manual Build +------------ + +If you can not or do not want to rely on our `configure` script nor on our +build system based on GNU `make`, then this is easily doable as follows. + + mkdir build + cd build + for f in ../src/*.cpp; do g++ -O3 -DNDEBUG -DNBUILD -c $f; done + ar rc libcadical.a `ls *.o | grep -v ical.o` + g++ -o cadical cadical.o -L. -lcadical + g++ -o mobical mobical.o -L. -lcadical + +Note that application object files are excluded from the library. +Of course you can use different compilation options as well. + +Since `build.hpp` is not generated in this flow the `-DNBUILD` flag is +necessary though, which avoids dependency of `version.cpp` on `build.hpp`. +Consequently you will only get very basic version information compiled into +the library and binaries (guaranteed is in essence just the version number +of the library). + +And if you really do not care about compilation time nor caching and just +want to build the solver once manually then the following also works. + + g++ -O3 -DNDEBUG -DNBUILD -o cadical `ls *.cpp | grep -v mobical` + +Further note that the `configure` script provides some feature checks and +might generate additional compiler flags necessary for compilation. You +might need to set those yourself or just use a modern C++11 compiler. + +This manual build process using object files is fast enough in combination +with caching solutions such as `ccache`. But it lacks the ability of our +GNU make solution to run compilation in parallel without additional parallel +process scheduling solutions. + +Cross-Compilation +----------------- + +We have preliminary support for cross-compilation using MinGW32 (only +tested for a Linux compilation host and Windows-64 target host at this +point). + +There are two steps necessary to make this work. First make +sure to be able to execute binaries compiled with the cross-compiler +directly. For instance in order to use `wine` to execute the binaries +on Linux you might want to look into the `binfmt_misc` module and +registering the appropriate interpreter for `DOSWin`. As second step +you simply tell the `configure` script to use the cross-compiler. + + CXXFLAGS=-static CXX=i686-w64-mingw32-g++ ./configure + +Note the use of '-static', which was necessary for me since by default +`wine` did not find `libstdc++` if dynamically linked. + + diff --git a/hCaD_V2/CONTRIBUTING b/hCaD_V2/CONTRIBUTING new file mode 100644 index 0000000..fbf1cdd --- /dev/null +++ b/hCaD_V2/CONTRIBUTING @@ -0,0 +1,4 @@ +At this point we want to keep complete ownership in one hand +to particularly avoid any additional co-authorship claims. +Thus please refrain from generating pull requests. Use the issue +tracker or send email to 'biere@jku.at' instead. diff --git a/hCaD_V2/LICENSE b/hCaD_V2/LICENSE new file mode 100644 index 0000000..81065ff --- /dev/null +++ b/hCaD_V2/LICENSE @@ -0,0 +1,22 @@ +MIT License + +Copyright (c) 2016-2021 Armin Biere, Johannes Kepler University Linz, Austria +Copyright (c) 2020-2021 Mathias Fleury, Johannes Kepler University Linz, Austria + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. diff --git a/hCaD_V2/README.md b/hCaD_V2/README.md new file mode 100644 index 0000000..756f3b8 --- /dev/null +++ b/hCaD_V2/README.md @@ -0,0 +1,54 @@ +[![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](https://opensource.org/licenses/MIT) +[![Build Status](https://travis-ci.com/arminbiere/cadical.svg?branch=master)](https://travis-ci.com/arminbiere/cadical) + + +CaDiCaL Simplified Satisfiability Solver +=============================================================================== + +The goal of the development of CaDiCaL was to obtain a CDCL solver, +which is easy to understand and change, while at the same time not being +much slower than other state-of-the-art CDCL solvers. + +Originally we wanted to also radically simplify the design and internal data +structures, but that goal was only achieved partially, at least for instance +compared to Lingeling. + +However, the code is much better documented and CaDiCaL actually became in +general faster than Lingeling even though it is missing some preprocessors +(mostly parity and cardinality constraint reasoning), which would be crucial +to solve certain instances. + +Use `./configure && make` to configure and build `cadical` and the library +`libcadical.a` in the default `build` sub-directory. The header file of +the library is [`src/cadical.hpp`](src/cadical.hpp) and includes an example +for API usage. + +See [`BUILD.md`](BUILD.md) for options and more details related to the build +process and [`test/README.md`](test/README.md) for testing the library and +the solver. + +The solver has the following usage `cadical [ dimacs [ proof ] ]`. +See `cadical -h` for more options. + +If you want to cite CaDiCaL please use the solver description in the +latest SAT competition proceedings: + +
+  @inproceedings{BiereFazekasFleuryHeisinger-SAT-Competition-2020-solvers,
+    author    = {Armin Biere and Katalin Fazekas and Mathias Fleury and Maximillian Heisinger},
+    title     = {{CaDiCaL}, {Kissat}, {Paracooba}, {Plingeling} and {Treengeling}
+		 Entering the {SAT Competition 2020}},
+    pages     = {51--53},
+    editor    = {Tomas Balyo and Nils Froleyks and Marijn Heule and 
+		 Markus Iser and Matti J{\"a}rvisalo and Martin Suda},
+    booktitle = {Proc.~of {SAT Competition} 2020 -- Solver and Benchmark Descriptions},
+    volume    = {B-2020-1},
+    series    = {Department of Computer Science Report Series B},
+    publisher = {University of Helsinki},
+    year      = 2020,
+  }
+
+ +You might also find more information on CaDiCaL at . + +Armin Biere diff --git a/hCaD_V2/VERSION b/hCaD_V2/VERSION new file mode 100644 index 0000000..347f583 --- /dev/null +++ b/hCaD_V2/VERSION @@ -0,0 +1 @@ +1.4.1 diff --git a/hCaD_V2/bin/starexec_run_default b/hCaD_V2/bin/starexec_run_default new file mode 100644 index 0000000..d24f815 --- /dev/null +++ b/hCaD_V2/bin/starexec_run_default @@ -0,0 +1,2 @@ +#!/bin/sh +exec ./cadical --target=0 --walk=false $1 $2/proof.out diff --git a/hCaD_V2/configure b/hCaD_V2/configure new file mode 100755 index 0000000..e761d26 --- /dev/null +++ b/hCaD_V2/configure @@ -0,0 +1,494 @@ +#!/bin/sh + +#--------------------------------------------------------------------------# + +# Run './configure' to produce a 'makefile' in the 'build' sub-directory or +# in any immediate sub-directory different from the 'src', 'scripts' and +# 'test' directories. + +#--------------------------------------------------------------------------# + +rm -f configure.log + +#--------------------------------------------------------------------------# + +# Common default options. + +all=no +debug=no +logging=no +check=no +competition=no +coverage=no +profile=no +contracts=yes +tracing=yes +unlocked=yes +pedantic=no +options="" +quiet=no +m32=no + +#--------------------------------------------------------------------------# + +if [ -f ./scripts/colors.sh ] +then + . ./scripts/colors.sh +elif [ -f ../scripts/colors.sh ] +then + . ../scripts/colors.sh +else + BAD="" + HILITE="" + BOLD="" + NORMAL="" +fi + +die () { + if [ -f configure.log ] + then + checklog=" (check also 'configure.log')" + else + checklog="" + fi + cecho "${BOLD}configure:${NORMAL} ${BAD}error:${NORMAL} $*${checklog}" + exit 1 +} + +msg () { + cecho "${BOLD}configure:${NORMAL} $*" +} + +# if we can find the 'color.sh' script source it and overwrite color codes + +for dir in . .. +do + [ -f $dir/scripts/colors.sh ] || continue + . $dir/scripts/colors.sh || exit 1 + break +done + +#--------------------------------------------------------------------------# + +# Parse and handle command line options. + +usage () { +cat << EOF +usage: configure [