diff --git a/.gitignore b/.gitignore index b9ee5dc..a8b4dfc 100644 --- a/.gitignore +++ b/.gitignore @@ -33,4 +33,5 @@ acec amulet2 -build \ No newline at end of file +build +.vscode \ No newline at end of file diff --git a/.vscode/settings.json b/.vscode/settings.json deleted file mode 100644 index 48cb31a..0000000 --- a/.vscode/settings.json +++ /dev/null @@ -1,8 +0,0 @@ -{ - "files.associations": { - "*.ejs": "html", - "iostream": "cpp", - "*.tcc": "cpp", - "new": "cpp" - } -} \ No newline at end of file diff --git a/acec.cpp b/acec.cpp index f1248a8..6753172 100644 --- a/acec.cpp +++ b/acec.cpp @@ -1,46 +1,8 @@ #include -#include "vec.hpp" -#include "circuit.hpp" -#include "sweep.hpp" - -//#include "libopenf4.h" -#include "src/cadical.hpp" #include "polynomial.h" -extern "C" { - #include "aiger.h" -} - -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) { @@ -87,112 +49,112 @@ bool subsitute(Polynomial* &a, Polynomial* b) { 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(); +// 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->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[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[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[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())); +// 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(); +// 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())); +// 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(); - } -} +// 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(); @@ -203,112 +165,109 @@ int main(int argv, char* args[]) { init_mpz(19260817); - S = sweep_init(argv, args); - S->solve(); + // 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; + // } - 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; - } + // std::vector polys; - std::vector polys; + // 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); + // } + // } - 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()); - 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; - } + // 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(!reserved_vars.count(i)) continue; + // //if(c->sz == 2 && abs(c->to[0]) <= 14 && abs(c->to[1]) <= 14) 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); - Polynomial *resultA, *resultB = nullptr; - getPolyOfGate(S, i, resultA, resultB); + // printf(" original:\t"); resultA->print(stdout); - 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); + // } - 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); - printf(" pos-var:\t"); resultA->print(stdout); + // for(auto subs : subsitute_vars) { + // //printf("delete: "); subs->print(stdout); + // subsitute(resultA, subs); + // } - for(auto subs : subsitute_vars) { - //printf("delete: "); subs->print(stdout); - subsitute(resultA, subs); - } + // printf(" xor-relative:\t"); resultA->print(stdout); - printf(" xor-relative:\t"); resultA->print(stdout); - - polys.push_back(resultA); + // 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)); - } + // 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()); + // printf(" = %s ( ", gate_type[c->type].c_str()); - for (int j = 0; j < c->sz; j++) { - printf("%d ", c->to[j]); - } - puts(")"); - } + // 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())); + // add_to_vstack(pvar(32)); + // push_mstack(new Monomial(one, build_term_from_stack())); - Polynomial *result = build_poly(); + // Polynomial *result = build_poly(); - std::sort(polys.begin(), polys.end(), poly_cmp); + // 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); - } + // for(auto p : polys) { + // printf("now: "); result->print(stdout); + // printf("div: "); p->print(stdout); + // subsitute(result, p); + // } return 0; } diff --git a/acec.log b/acec.log deleted file mode 100644 index e69de29..0000000 diff --git a/aiger.c b/aiger.c deleted file mode 100644 index e6e5bb6..0000000 --- a/aiger.c +++ /dev/null @@ -1,2775 +0,0 @@ -/*************************************************************************** -Copyright (c) 2011, Siert Wieringa, Aalto University, Finland. -Copyright (c) 2006-2019, Armin Biere, Johannes Kepler University. - -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. -***************************************************************************/ -#include "aiger.h" - -#include -#include -#include -#include -#include - - - -/*------------------------------------------------------------------------*/ - -// TODO move this to seperate file and sync it with git hash - -const char * -aiger_id (void) -{ - return "invalid id"; -} - -/*------------------------------------------------------------------------*/ - -const char * -aiger_version (void) -{ - return AIGER_VERSION; -} - -/*------------------------------------------------------------------------*/ - -#define GZIP "gzip -c > %s 2>/dev/null" -#define GUNZIP "gunzip -c %s 2>/dev/null" - -#define NEWN(p,n) \ - do { \ - size_t bytes = (n) * sizeof (*(p)); \ - (p) = private->malloc_callback (private->memory_mgr, bytes); \ - memset ((p), 0, bytes); \ - } while (0) - -#define REALLOCN(p,m,n) \ - do { \ - size_t mbytes = (m) * sizeof (*(p)); \ - size_t nbytes = (n) * sizeof (*(p)); \ - size_t minbytes = (mbytes < nbytes) ? mbytes : nbytes; \ - void * res = private->malloc_callback (private->memory_mgr, nbytes); \ - memcpy (res, (p), minbytes); \ - if (nbytes > mbytes) \ - memset (((char*)res) + mbytes, 0, nbytes - mbytes); \ - private->free_callback (private->memory_mgr, (p), mbytes); \ - (p) = res; \ - } while (0) - -#define FIT(p,m,n) \ - do { \ - size_t old_size = (m); \ - size_t new_size = (n); \ - if (old_size < new_size) \ - { \ - REALLOCN (p,old_size,new_size); \ - (m) = new_size; \ - } \ - } while (0) - -#define ENLARGE(p,s) \ - do { \ - size_t old_size = (s); \ - size_t new_size = old_size ? 2 * old_size : 1; \ - REALLOCN (p,old_size,new_size); \ - (s) = new_size; \ - } while (0) - -#define PUSH(p,t,s,l) \ - do { \ - if ((t) == (s)) \ - ENLARGE (p, s); \ - (p)[(t)++] = (l); \ - } while (0) - -#define DELETEN(p,n) \ - do { \ - size_t bytes = (n) * sizeof (*(p)); \ - private->free_callback (private->memory_mgr, (p), bytes); \ - (p) = 0; \ - } while (0) - -#define CLR(p) do { memset (&(p), 0, sizeof (p)); } while (0) - -#define NEW(p) NEWN (p,1) -#define DELETE(p) DELETEN (p,1) - -#define IMPORT_private_FROM(p) \ - aiger_private * private = (aiger_private*) (p) - -#define EXPORT_public_FROM(p) \ - aiger * public = &(p)->public - -typedef struct aiger_private aiger_private; -typedef struct aiger_buffer aiger_buffer; -typedef struct aiger_reader aiger_reader; -typedef struct aiger_type aiger_type; - -struct aiger_type -{ - unsigned input:1; - unsigned latch:1; - unsigned and:1; - - unsigned mark:1; - unsigned onstack:1; - - /* Index int to 'public->{inputs,latches,ands}'. - */ - unsigned idx; -}; - -struct aiger_private -{ - aiger public; - - aiger_type *types; /* [0..maxvar] */ - unsigned size_types; - - unsigned char * coi; - unsigned size_coi; - - unsigned size_inputs; - unsigned size_latches; - unsigned size_outputs; - unsigned size_ands; - unsigned size_bad; - unsigned size_constraints; - unsigned size_justice; - unsigned size_fairness; - - unsigned num_comments; - unsigned size_comments; - - void *memory_mgr; - aiger_malloc malloc_callback; - aiger_free free_callback; - - char *error; -}; - -struct aiger_buffer -{ - char *start; - char *cursor; - char *end; -}; - -struct aiger_reader -{ - void *state; - aiger_get get; - - int ch; - - unsigned lineno; - unsigned charno; - - unsigned lineno_at_last_token_start; - - int done_with_reading_header; - int looks_like_aag; - - aiger_mode mode; - unsigned maxvar; - unsigned inputs; - unsigned latches; - unsigned outputs; - unsigned ands; - unsigned bad; - unsigned constraints; - unsigned justice; - unsigned fairness; - - char *buffer; - unsigned top_buffer; - unsigned size_buffer; -}; - -aiger * -aiger_init_mem (void *memory_mgr, - aiger_malloc external_malloc, aiger_free external_free) -{ - aiger_private *private; - aiger *public; - - assert (external_malloc); - assert (external_free); - private = external_malloc (memory_mgr, sizeof (*private)); - CLR (*private); - private->memory_mgr = memory_mgr; - private->malloc_callback = external_malloc; - private->free_callback = external_free; - public = &private->public; - PUSH (public->comments, private->num_comments, private->size_comments, 0); - - return public; -} - -static void * -aiger_default_malloc (void *state, size_t bytes) -{ - return malloc (bytes); -} - -static void -aiger_default_free (void *state, void *ptr, size_t bytes) -{ - free (ptr); -} - -aiger * -aiger_init (void) -{ - return aiger_init_mem (0, aiger_default_malloc, aiger_default_free); -} - -static void -aiger_delete_str (aiger_private * private, char *str) -{ - if (str) - DELETEN (str, strlen (str) + 1); -} - -static char * -aiger_copy_str (aiger_private * private, const char *str) -{ - char *res; - - if (!str || !str[0]) - return 0; - - NEWN (res, strlen (str) + 1); - strcpy (res, str); - - return res; -} - -static unsigned -aiger_delete_symbols_aux (aiger_private * private, - aiger_symbol * symbols, unsigned size) -{ - unsigned i, res; - - res = 0; - for (i = 0; i < size; i++) - { - aiger_symbol *s = symbols + i; - if (!s->name) - continue; - - aiger_delete_str (private, s->name); - s->name = 0; - res++; - } - - return res; -} - -static void -aiger_delete_symbols (aiger_private * private, - aiger_symbol * symbols, unsigned size) -{ - aiger_delete_symbols_aux (private, symbols, size); - DELETEN (symbols, size); -} - -static unsigned -aiger_delete_comments (aiger * public) -{ - char **start = (char **) public->comments, ** end, ** p; - IMPORT_private_FROM (public); - - end = start + private->num_comments; - for (p = start; p < end; p++) - aiger_delete_str (private, *p); - - private->num_comments = 0; - public->comments[0] = 0; - - return private->num_comments; -} - -void -aiger_reset (aiger * public) -{ - unsigned i; - - IMPORT_private_FROM (public); - - aiger_delete_symbols (private, public->inputs, private->size_inputs); - aiger_delete_symbols (private, public->latches, private->size_latches); - aiger_delete_symbols (private, public->outputs, private->size_outputs); - aiger_delete_symbols (private, public->bad, private->size_bad); - aiger_delete_symbols (private, public->constraints, - private->size_constraints); - for (i = 0; i < public->num_justice; i++) - DELETEN (public->justice[i].lits, public->justice[i].size); - aiger_delete_symbols (private, public->justice, private->size_justice); - aiger_delete_symbols (private, public->fairness, private->size_fairness); - DELETEN (public->ands, private->size_ands); - - aiger_delete_comments (public); - DELETEN (public->comments, private->size_comments); - - DELETEN (private->coi, private->size_coi); - - DELETEN (private->types, private->size_types); - aiger_delete_str (private, private->error); - DELETE (private); -} - -static aiger_type * -aiger_import_literal (aiger_private * private, unsigned lit) -{ - unsigned var = aiger_lit2var (lit); - EXPORT_public_FROM (private); - - if (var > public->maxvar) - public->maxvar = var; - - while (var >= private->size_types) - ENLARGE (private->types, private->size_types); - - return private->types + var; -} - -void -aiger_add_input (aiger * public, unsigned lit, const char *name) -{ - IMPORT_private_FROM (public); - aiger_symbol symbol; - aiger_type *type; - - assert (!aiger_error (public)); - - assert (lit); - assert (!aiger_sign (lit)); - - type = aiger_import_literal (private, lit); - - assert (!type->input); - assert (!type->latch); - assert (!type->and); - - type->input = 1; - type->idx = public->num_inputs; - - CLR (symbol); - symbol.lit = lit; - symbol.name = aiger_copy_str (private, name); - - PUSH (public->inputs, public->num_inputs, private->size_inputs, symbol); -} - -void -aiger_add_latch (aiger * public, - unsigned lit, unsigned next, const char *name) -{ - IMPORT_private_FROM (public); - aiger_symbol symbol; - aiger_type *type; - - assert (!aiger_error (public)); - - assert (lit); - assert (!aiger_sign (lit)); - - type = aiger_import_literal (private, lit); - - assert (!type->input); - assert (!type->latch); - assert (!type->and); - - /* Warning: importing 'next' makes 'type' invalid. - */ - type->latch = 1; - type->idx = public->num_latches; - - aiger_import_literal (private, next); - - CLR (symbol); - symbol.lit = lit; - symbol.next = next; - symbol.name = aiger_copy_str (private, name); - - PUSH (public->latches, public->num_latches, private->size_latches, symbol); -} - -void -aiger_add_reset (aiger * public, unsigned lit, unsigned reset) -{ - IMPORT_private_FROM (public); - aiger_type * type; - assert (reset <= 1 || reset == lit); - assert (!aiger_error (public)); - assert (lit); - assert (!aiger_sign (lit)); - type = aiger_import_literal (private, lit); - assert (type->latch); - assert (type->idx < public->num_latches); - public->latches[type->idx].reset = reset; -} - -void -aiger_add_output (aiger * public, unsigned lit, const char *name) -{ - IMPORT_private_FROM (public); - aiger_symbol symbol; - aiger_import_literal (private, lit); - CLR (symbol); - symbol.lit = lit; - symbol.name = aiger_copy_str (private, name); - PUSH (public->outputs, public->num_outputs, private->size_outputs, symbol); -} - -void -aiger_add_bad (aiger * public, unsigned lit, const char *name) -{ - IMPORT_private_FROM (public); - aiger_symbol symbol; - aiger_import_literal (private, lit); - CLR (symbol); - symbol.lit = lit; - symbol.name = aiger_copy_str (private, name); - PUSH (public->bad, public->num_bad, private->size_bad, symbol); -} - -void -aiger_add_constraint (aiger * public, unsigned lit, const char *name) -{ - IMPORT_private_FROM (public); - aiger_symbol symbol; - aiger_import_literal (private, lit); - CLR (symbol); - symbol.lit = lit; - symbol.name = aiger_copy_str (private, name); - PUSH (public->constraints, - public->num_constraints, private->size_constraints, symbol); -} - -void -aiger_add_justice (aiger * public, - unsigned size, unsigned * lits, - const char * name) -{ - IMPORT_private_FROM (public); - aiger_symbol symbol; - unsigned i, lit; - CLR (symbol); - symbol.size = size; - NEWN (symbol.lits, size); - for (i = 0; i < size; i++) - { - lit = lits[i]; - aiger_import_literal (private, lit); - symbol.lits[i] = lit; - } - symbol.name = aiger_copy_str (private, name); - PUSH (public->justice, - public->num_justice, private->size_justice, symbol); -} - -void -aiger_add_fairness (aiger * public, unsigned lit, const char *name) -{ - IMPORT_private_FROM (public); - aiger_symbol symbol; - aiger_import_literal (private, lit); - CLR (symbol); - symbol.lit = lit; - symbol.name = aiger_copy_str (private, name); - PUSH (public->fairness, - public->num_fairness, private->size_fairness, symbol); -} - -void -aiger_add_and (aiger * public, unsigned lhs, unsigned rhs0, unsigned rhs1) -{ - IMPORT_private_FROM (public); - aiger_type *type; - aiger_and *and; - - assert (!aiger_error (public)); - - assert (lhs > 1); - assert (!aiger_sign (lhs)); - - type = aiger_import_literal (private, lhs); - - assert (!type->input); - assert (!type->latch); - assert (!type->and); - - type->and = 1; - type->idx = public->num_ands; - - aiger_import_literal (private, rhs0); - aiger_import_literal (private, rhs1); - - if (public->num_ands == private->size_ands) - ENLARGE (public->ands, private->size_ands); - - and = public->ands + public->num_ands; - - and->lhs = lhs; - and->rhs0 = rhs0; - and->rhs1 = rhs1; - - public->num_ands++; -} - -void -aiger_add_comment (aiger * public, const char *comment) -{ - IMPORT_private_FROM (public); - char **p; - - assert (!aiger_error (public)); - - assert (!strchr (comment, '\n')); - assert (private->num_comments); - p = public->comments + private->num_comments - 1; - assert (!*p); - *p = aiger_copy_str (private, comment); - PUSH (public->comments, private->num_comments, private->size_comments, 0); -} - -static const char * -aiger_error_s (aiger_private * private, const char *s, const char *a) -{ - unsigned tmp_len, error_len; - char *tmp; - assert (!private->error); - tmp_len = strlen (s) + strlen (a) + 1; - NEWN (tmp, tmp_len); - sprintf (tmp, s, a); - error_len = strlen (tmp) + 1; - NEWN (private->error, error_len); - memcpy (private->error, tmp, error_len); - DELETEN (tmp, tmp_len); - return private->error; -} - -static const char * -aiger_error_u (aiger_private * private, const char *s, unsigned u) -{ - unsigned tmp_len, error_len; - char *tmp; - assert (!private->error); - tmp_len = strlen (s) + sizeof (u) * 4 + 1; - NEWN (tmp, tmp_len); - sprintf (tmp, s, u); - error_len = strlen (tmp) + 1; - NEWN (private->error, error_len); - memcpy (private->error, tmp, error_len); - DELETEN (tmp, tmp_len); - return private->error; -} - -static const char * -aiger_error_uu (aiger_private * private, const char *s, unsigned a, - unsigned b) -{ - unsigned tmp_len, error_len; - char *tmp; - assert (!private->error); - tmp_len = strlen (s) + sizeof (a) * 4 + sizeof (b) * 4 + 1; - NEWN (tmp, tmp_len); - sprintf (tmp, s, a, b); - error_len = strlen (tmp) + 1; - NEWN (private->error, error_len); - memcpy (private->error, tmp, error_len); - DELETEN (tmp, tmp_len); - return private->error; -} - -static const char * -aiger_error_us (aiger_private * private, const char *s, unsigned a, - const char * b) -{ - unsigned tmp_len, error_len; - char *tmp; - assert (!private->error); - tmp_len = strlen (s) + sizeof (a) * 4 + strlen (b) + 1; - NEWN (tmp, tmp_len); - sprintf (tmp, s, a, b); - error_len = strlen (tmp) + 1; - NEWN (private->error, error_len); - memcpy (private->error, tmp, error_len); - DELETEN (tmp, tmp_len); - return private->error; -} - -static const char * -aiger_error_usu (aiger_private * private, - const char *s, unsigned a, const char *t, unsigned b) -{ - unsigned tmp_len, error_len; - char *tmp; - assert (!private->error); - tmp_len = strlen (s) + strlen (t) + sizeof (a) * 4 + sizeof (b) * 4 + 1; - NEWN (tmp, tmp_len); - sprintf (tmp, s, a, t, b); - error_len = strlen (tmp) + 1; - NEWN (private->error, error_len); - memcpy (private->error, tmp, error_len); - DELETEN (tmp, tmp_len); - return private->error; -} - -const char * -aiger_error (aiger * public) -{ - IMPORT_private_FROM (public); - return private->error; -} - -static int -aiger_literal_defined (aiger_private * private, unsigned lit) -{ - unsigned var = aiger_lit2var (lit); -#ifndef NDEBUG - EXPORT_public_FROM (private); -#endif - aiger_type *type; - - assert (var <= public->maxvar); - if (!var) - return 1; - - type = private->types + var; - - return type->and || type->input || type->latch; -} - -static void -aiger_check_next_defined (aiger_private * private) -{ - EXPORT_public_FROM (private); - unsigned i, next, latch; - aiger_symbol *symbol; - - if (private->error) - return; - - for (i = 0; !private->error && i < public->num_latches; i++) - { - symbol = public->latches + i; - latch = symbol->lit; - next = symbol->next; - - assert (!aiger_sign (latch)); - assert (private->types[aiger_lit2var (latch)].latch); - - if (!aiger_literal_defined (private, next)) - aiger_error_uu (private, - "next state function %u of latch %u undefined", - next, latch); - } -} - -static void -aiger_check_right_hand_side_defined (aiger_private * private, aiger_and * and, - unsigned rhs) -{ - if (private->error) - return; - - assert (and); - if (!aiger_literal_defined (private, rhs)) - aiger_error_uu (private, "literal %u in AND %u undefined", rhs, and->lhs); -} - -static void -aiger_check_right_hand_sides_defined (aiger_private * private) -{ - EXPORT_public_FROM (private); - aiger_and *and; - unsigned i; - - if (private->error) - return; - - for (i = 0; !private->error && i < public->num_ands; i++) - { - and = public->ands + i; - aiger_check_right_hand_side_defined (private, and, and->rhs0); - aiger_check_right_hand_side_defined (private, and, and->rhs1); - } -} - -static void -aiger_check_outputs_defined (aiger_private * private) -{ - EXPORT_public_FROM (private); - unsigned i, output; - - if (private->error) - return; - - for (i = 0; !private->error && i < public->num_outputs; i++) - { - output = public->outputs[i].lit; - output = aiger_strip (output); - if (output <= 1) - continue; - - if (!aiger_literal_defined (private, output)) - aiger_error_u (private, "output %u undefined", output); - } -} - -static void -aiger_check_bad_defined (aiger_private * private) -{ - EXPORT_public_FROM (private); - unsigned i, bad; - - if (private->error) - return; - - for (i = 0; !private->error && i < public->num_bad; i++) - { - bad = public->bad[i].lit; - bad = aiger_strip (bad); - if (bad <= 1) - continue; - - if (!aiger_literal_defined (private, bad)) - aiger_error_u (private, "bad %u undefined", bad); - } -} - -static void -aiger_check_constraints_defined (aiger_private * private) -{ - EXPORT_public_FROM (private); - unsigned i, constraint; - - if (private->error) - return; - - for (i = 0; !private->error && i < public->num_constraints; i++) - { - constraint = public->constraints[i].lit; - constraint = aiger_strip (constraint); - if (constraint <= 1) - continue; - - if (!aiger_literal_defined (private, constraint)) - aiger_error_u (private, "constraint %u undefined", constraint); - } -} - -static void -aiger_check_fairness_defined (aiger_private * private) -{ - EXPORT_public_FROM (private); - unsigned i, fairness; - - if (private->error) - return; - - for (i = 0; !private->error && i < public->num_fairness; i++) - { - fairness = public->fairness[i].lit; - fairness = aiger_strip (fairness); - if (fairness <= 1) - continue; - - if (!aiger_literal_defined (private, fairness)) - aiger_error_u (private, "fairness %u undefined", fairness); - } -} - -static void -aiger_check_justice_defined (aiger_private * private) -{ - EXPORT_public_FROM (private); - unsigned i, j, justice; - - if (private->error) - return; - - for (i = 0; !private->error && i < public->num_justice; i++) - { - for (j = 0; !private->error && j < public->justice[i].size; j++) - { - justice = public->justice[i].lits[j]; - justice = aiger_strip (justice); - if (justice <= 1) - continue; - - if (!aiger_literal_defined (private, justice)) - aiger_error_u (private, "justice %u undefined", justice); - } - } -} - -static void -aiger_check_for_cycles (aiger_private * private) -{ - unsigned i, j, *stack, size_stack, top_stack, tmp; - EXPORT_public_FROM (private); - aiger_type *type; - aiger_and *and; - - if (private->error) - return; - - stack = 0; - size_stack = top_stack = 0; - - for (i = 1; !private->error && i <= public->maxvar; i++) - { - type = private->types + i; - - if (!type->and || type->mark) - continue; - - PUSH (stack, top_stack, size_stack, i); - while (top_stack) - { - j = stack[top_stack - 1]; - - if (j) - { - type = private->types + j; - if (type->mark && type->onstack) - { - aiger_error_u (private, - "cyclic definition for and gate %u", j); - break; - } - - if (!type->and || type->mark) - { - top_stack--; - continue; - } - - /* Prefix code. - */ - type->mark = 1; - type->onstack = 1; - PUSH (stack, top_stack, size_stack, 0); - - assert (type->idx < public->num_ands); - and = public->ands + type->idx; - - tmp = aiger_lit2var (and->rhs0); - if (tmp) - PUSH (stack, top_stack, size_stack, tmp); - - tmp = aiger_lit2var (and->rhs1); - if (tmp) - PUSH (stack, top_stack, size_stack, tmp); - } - else - { - /* All descendends traversed. This is the postfix code. - */ - assert (top_stack >= 2); - top_stack -= 2; - j = stack[top_stack]; - assert (j); - type = private->types + j; - assert (type->mark); - assert (type->onstack); - type->onstack = 0; - } - } - } - - DELETEN (stack, size_stack); -} - -const char * -aiger_check (aiger * public) -{ - IMPORT_private_FROM (public); - - assert (!aiger_error (public)); - - aiger_check_next_defined (private); - aiger_check_outputs_defined (private); - aiger_check_bad_defined (private); - aiger_check_constraints_defined (private); - aiger_check_justice_defined (private); - aiger_check_fairness_defined (private); - aiger_check_right_hand_sides_defined (private); - aiger_check_for_cycles (private); - - return private->error; -} - -static int -aiger_default_get (FILE * file) -{ - return getc (file); -} - -static int -aiger_default_put (char ch, FILE * file) -{ - return putc ((unsigned char) ch, file); -} - -static int -aiger_string_put (char ch, aiger_buffer * buffer) -{ - if (buffer->cursor == buffer->end) - return EOF; - *buffer->cursor++ = ch; - return ch; -} - -static int -aiger_put_s (void *state, aiger_put put, const char *str) -{ - const char *p; - char ch; - - for (p = str; (ch = *p); p++) - if (put (ch, state) == EOF) - return EOF; - - return p - str; /* 'fputs' semantics, >= 0 is OK */ -} - -static int -aiger_put_u (void *state, aiger_put put, unsigned u) -{ - char buffer[sizeof (u) * 4]; - sprintf (buffer, "%u", u); - return aiger_put_s (state, put, buffer); -} - -static int -aiger_write_delta (void *state, aiger_put put, unsigned delta) -{ - unsigned char ch; - unsigned tmp = delta; - - while (tmp & ~0x7f) - { - ch = tmp & 0x7f; - ch |= 0x80; - - if (put (ch, state) == EOF) - return 0; - - tmp >>= 7; - } - - ch = tmp; - return put (ch, state) != EOF; -} - -static int -aiger_write_header (aiger * public, - const char *format_string, - int compact_inputs_and_latches, - void *state, aiger_put put) -{ - unsigned i, j; - - if (aiger_put_s (state, put, format_string) == EOF) return 0; - if (put (' ', state) == EOF) return 0; - if (aiger_put_u (state, put, public->maxvar) == EOF) return 0; - if (put (' ', state) == EOF) return 0; - if (aiger_put_u (state, put, public->num_inputs) == EOF) return 0; - if (put (' ', state) == EOF) return 0; - if (aiger_put_u (state, put, public->num_latches) == EOF) return 0; - if (put (' ', state) == EOF) return 0; - if (aiger_put_u (state, put, public->num_outputs) == EOF) return 0; - if (put (' ', state) == EOF) return 0; - if (aiger_put_u (state, put, public->num_ands) == EOF) return 0; - - if (public->num_bad || - public->num_constraints || - public->num_justice || - public->num_fairness) - { - if (put (' ', state) == EOF) return 0; - if (aiger_put_u (state, put, public->num_bad) == EOF) return 0; - } - - if (public->num_constraints || - public->num_justice || - public->num_fairness) - { - if (put (' ', state) == EOF) return 0; - if (aiger_put_u (state, put, public->num_constraints) == EOF) return 0; - } - - if (public->num_justice || - public->num_fairness) - { - if (put (' ', state) == EOF) return 0; - if (aiger_put_u (state, put, public->num_justice) == EOF) return 0; - } - - if (public->num_fairness) - { - if (put (' ', state) == EOF) return 0; - if (aiger_put_u (state, put, public->num_fairness) == EOF) return 0; - } - - if (put ('\n', state) == EOF) return 0; - - if (!compact_inputs_and_latches && public->num_inputs) - { - for (i = 0; i < public->num_inputs; i++) - if (aiger_put_u (state, put, public->inputs[i].lit) == EOF || - put ('\n', state) == EOF) - return 0; - } - - if (public->num_latches) - { - for (i = 0; i < public->num_latches; i++) - { - if (!compact_inputs_and_latches) - { - if (aiger_put_u (state, put, public->latches[i].lit) == EOF) - return 0; - if (put (' ', state) == EOF) return 0; - } - - if (aiger_put_u (state, put, public->latches[i].next) == EOF) - return 0; - - if (public->latches[i].reset) - { - if (put (' ', state) == EOF) return 0; - if (aiger_put_u (state, put, public->latches[i].reset) == EOF) - return 0; - } - if (put ('\n', state) == EOF) return 0; - } - } - - if (public->num_outputs) - { - for (i = 0; i < public->num_outputs; i++) - if (aiger_put_u (state, put, public->outputs[i].lit) == EOF || - put ('\n', state) == EOF) - return 0; - } - - if (public->num_bad) - { - for (i = 0; i < public->num_bad; i++) - if (aiger_put_u (state, put, public->bad[i].lit) == EOF || - put ('\n', state) == EOF) - return 0; - } - - if (public->num_constraints) - { - for (i = 0; i < public->num_constraints; i++) - if (aiger_put_u (state, put, public->constraints[i].lit) == EOF || - put ('\n', state) == EOF) - return 0; - } - - if (public->num_justice) - { - for (i = 0; i < public->num_justice; i++) - { - if (aiger_put_u (state, put, public->justice[i].size) == EOF) - return 0; - if (put ('\n', state) == EOF) return 0; - } - - for (i = 0; i < public->num_justice; i++) - { - for (j = 0; j < public->justice[i].size; j++) - { - if (aiger_put_u (state, put, public->justice[i].lits[j]) == EOF) - return 0; - if (put ('\n', state) == EOF) return 0; - } - } - } - - if (public->num_fairness) - { - for (i = 0; i < public->num_fairness; i++) - if (aiger_put_u (state, put, public->fairness[i].lit) == EOF || - put ('\n', state) == EOF) - return 0; - } - - return 1; -} - -static int -aiger_have_at_least_one_symbol_aux (aiger * public, - aiger_symbol * symbols, unsigned size) -{ - unsigned i; - - for (i = 0; i < size; i++) - if (symbols[i].name) - return 1; - - return 0; -} - -static int -aiger_have_at_least_one_symbol (aiger * public) -{ - if (aiger_have_at_least_one_symbol_aux (public, - public->inputs, public->num_inputs)) - return 1; - - if (aiger_have_at_least_one_symbol_aux (public, - public->outputs, - public->num_outputs)) - return 1; - - if (aiger_have_at_least_one_symbol_aux (public, - public->latches, - public->num_latches)) - return 1; - - if (aiger_have_at_least_one_symbol_aux (public, - public->bad, - public->num_bad)) - return 1; - - if (aiger_have_at_least_one_symbol_aux (public, - public->constraints, - public->num_constraints)) - return 1; - - if (aiger_have_at_least_one_symbol_aux (public, - public->justice, - public->num_justice)) - return 1; - - if (aiger_have_at_least_one_symbol_aux (public, - public->fairness, - public->num_fairness)) - return 1; - - return 0; -} - -static int -aiger_write_symbols_aux (aiger * public, - void *state, aiger_put put, - const char *type, - aiger_symbol * symbols, unsigned size) -{ - unsigned i; - - for (i = 0; i < size; i++) - { - if (!symbols[i].name) - continue; - - assert (symbols[i].name[0]); - - if (aiger_put_s (state, put, type) == EOF || - aiger_put_u (state, put, i) == EOF || - put (' ', state) == EOF || - aiger_put_s (state, put, symbols[i].name) == EOF || - put ('\n', state) == EOF) - return 0; - } - - return 1; -} - -static int -aiger_write_symbols (aiger * public, void *state, aiger_put put) -{ - if (!aiger_write_symbols_aux (public, state, put, - "i", public->inputs, public->num_inputs)) - return 0; - - if (!aiger_write_symbols_aux (public, state, put, - "l", public->latches, public->num_latches)) - return 0; - - if (!aiger_write_symbols_aux (public, state, put, - "o", public->outputs, public->num_outputs)) - return 0; - - if (!aiger_write_symbols_aux (public, state, put, - "b", public->bad, public->num_bad)) - return 0; - - if (!aiger_write_symbols_aux (public, state, put, - "c", public->constraints, - public->num_constraints)) - return 0; - - if (!aiger_write_symbols_aux (public, state, put, - "j", public->justice, public->num_justice)) - return 0; - - if (!aiger_write_symbols_aux (public, state, put, - "f", public->fairness, public->num_fairness)) - return 0; - - return 1; -} - -int -aiger_write_symbols_to_file (aiger * public, FILE * file) -{ - assert (!aiger_error (public)); - return aiger_write_symbols (public, file, (aiger_put) aiger_default_put); -} - -static int -aiger_write_comments (aiger * public, void *state, aiger_put put) -{ - char **p, *str; - - for (p = public->comments; (str = *p); p++) - { - if (aiger_put_s (state, put, str) == EOF) - return 0; - - if (put ('\n', state) == EOF) - return 0; - } - - return 1; -} - -int -aiger_write_comments_to_file (aiger * public, FILE * file) -{ - assert (!aiger_error (public)); - return aiger_write_comments (public, file, (aiger_put) aiger_default_put); -} - -static int -aiger_write_ascii (aiger * public, void *state, aiger_put put) -{ - aiger_and *and; - unsigned i; - - assert (!aiger_check (public)); - - if (!aiger_write_header (public, "aag", 0, state, put)) - return 0; - - for (i = 0; i < public->num_ands; i++) - { - and = public->ands + i; - if (aiger_put_u (state, put, and->lhs) == EOF || - put (' ', state) == EOF || - aiger_put_u (state, put, and->rhs0) == EOF || - put (' ', state) == EOF || - aiger_put_u (state, put, and->rhs1) == EOF || - put ('\n', state) == EOF) - return 0; - } - - return 1; -} - -static unsigned -aiger_max_input_or_latch (aiger * public) -{ - unsigned i, tmp, res; - - res = 0; - - for (i = 0; i < public->num_inputs; i++) - { - tmp = public->inputs[i].lit; - assert (!aiger_sign (tmp)); - if (tmp > res) - res = tmp; - } - - for (i = 0; i < public->num_latches; i++) - { - tmp = public->latches[i].lit; - assert (!aiger_sign (tmp)); - if (tmp > res) - res = tmp; - } - - return res; -} - -int -aiger_is_reencoded (aiger * public) -{ - unsigned i, tmp, max, lhs; - aiger_and *and; - - max = 0; - for (i = 0; i < public->num_inputs; i++) - { - max += 2; - tmp = public->inputs[i].lit; - if (max != tmp) - return 0; - } - - for (i = 0; i < public->num_latches; i++) - { - max += 2; - tmp = public->latches[i].lit; - if (max != tmp) - return 0; - } - - lhs = aiger_max_input_or_latch (public) + 2; - for (i = 0; i < public->num_ands; i++) - { - and = public->ands + i; - - if (and->lhs <= max) - return 0; - - if (and->lhs != lhs) - return 0; - - if (and->lhs < and->rhs0) - return 0; - - if (and->rhs0 < and->rhs1) - return 0; - - lhs += 2; - } - - return 1; -} - -static void -aiger_new_code (unsigned var, unsigned *new, unsigned *code) -{ - unsigned lit = aiger_var2lit (var), res; - assert (!code[lit]); - res = *new; - code[lit] = res; - code[lit + 1] = res + 1; - *new += 2; -} - -static unsigned -aiger_reencode_lit (aiger * public, unsigned lit, - unsigned *new, unsigned *code, - unsigned **stack_ptr, unsigned * size_stack_ptr) -{ - unsigned res, old, top, child0, child1, tmp, var, size_stack, * stack; - IMPORT_private_FROM (public); - aiger_type *type; - aiger_and *and; - - if (lit < 2) - return lit; - - res = code[lit]; - if (res) - return res; - - var = aiger_lit2var (lit); - assert (var <= public->maxvar); - type = private->types + var; - - if (type->and) - { - top = 0; - stack = *stack_ptr; - size_stack = *size_stack_ptr; - PUSH (stack, top, size_stack, var); - - while (top > 0) - { - old = stack[--top]; - if (old) - { - if (code[aiger_var2lit (old)]) - continue; - - assert (old <= public->maxvar); - type = private->types + old; - if (type->onstack) - continue; - - type->onstack = 1; - - PUSH (stack, top, size_stack, old); - PUSH (stack, top, size_stack, 0); - - assert (type->and); - assert (type->idx < public->num_ands); - - and = public->ands + type->idx; - assert (and); - - child0 = aiger_lit2var (and->rhs0); - child1 = aiger_lit2var (and->rhs1); - - if (child0 < child1) - { - tmp = child0; - child0 = child1; - child1 = tmp; - } - - assert (child0 >= child1); /* smaller child first */ - - if (child0) - { - type = private->types + child0; - if (!type->input && !type->latch && !type->onstack) - PUSH (stack, top, size_stack, child0); - } - - if (child1) - { - type = private->types + child1; - if (!type->input && !type->latch && !type->onstack) - PUSH (stack, top, size_stack, child1); - } - } - else - { - assert (top > 0); - old = stack[--top]; - assert (!code[aiger_var2lit (old)]); - type = private->types + old; - assert (type->onstack); - type->onstack = 0; - aiger_new_code (old, new, code); - } - } - *size_stack_ptr = size_stack; - *stack_ptr = stack; - } - else - { - assert (type->input || type->latch); - assert (lit < *new); - - code[lit] = lit; - code[aiger_not (lit)] = aiger_not (lit); - } - - assert (code[lit]); - - return code[lit]; -} - -static int -cmp_lhs (const void *a, const void *b) -{ - const aiger_and *c = a; - const aiger_and *d = b; - return ((int) c->lhs) - (int) d->lhs; -} - -void -aiger_reencode (aiger * public) -{ - unsigned *code, i, j, size_code, old, new, lhs, rhs0, rhs1, tmp; - unsigned *stack, size_stack; - IMPORT_private_FROM (public); - - assert (!aiger_error (public)); - - aiger_symbol *symbol; - aiger_type *type; - aiger_and *and; - - if (aiger_is_reencoded (public)) - return; - - size_code = 2 * (public->maxvar + 1); - if (size_code < 2) - size_code = 2; - - NEWN (code, size_code); - - code[1] = 1; /* not used actually */ - - new = 2; - - for (i = 0; i < public->num_inputs; i++) - { - old = public->inputs[i].lit; - - code[old] = new; - code[old + 1] = new + 1; - - new += 2; - } - - for (i = 0; i < public->num_latches; i++) - { - old = public->latches[i].lit; - - code[old] = new; - code[old + 1] = new + 1; - - new += 2; - } - - stack = 0; - size_stack = 0; - - for (i = 0; i < public->num_latches; i++) - { - old = public->latches[i].next; - public->latches[i].next = - aiger_reencode_lit (public, old, &new, code, &stack, &size_stack); - - old = public->latches[i].reset; - public->latches[i].reset = - aiger_reencode_lit (public, old, &new, code, &stack, &size_stack); - } - - for (i = 0; i < public->num_outputs; i++) - { - old = public->outputs[i].lit; - public->outputs[i].lit = - aiger_reencode_lit (public, old, &new, code, &stack, &size_stack); - } - - for (i = 0; i < public->num_bad; i++) - { - old = public->bad[i].lit; - public->bad[i].lit = - aiger_reencode_lit (public, old, &new, code, &stack, &size_stack); - } - - for (i = 0; i < public->num_constraints; i++) - { - old = public->constraints[i].lit; - public->constraints[i].lit = - aiger_reencode_lit (public, old, &new, code, &stack, &size_stack); - } - - for (i = 0; i < public->num_justice; i++) - { - for (j = 0; j < public->justice[i].size; j++) - { - old = public->justice[i].lits[j]; - public->justice[i].lits[j] = - aiger_reencode_lit (public, old, &new, code, &stack, &size_stack); - } - } - - for (i = 0; i < public->num_fairness; i++) - { - old = public->fairness[i].lit; - public->fairness[i].lit = - aiger_reencode_lit (public, old, &new, code, &stack, &size_stack); - } - - DELETEN (stack, size_stack); - - j = 0; - for (i = 0; i < public->num_ands; i++) - { - and = public->ands + i; - lhs = code[and->lhs]; - if (!lhs) - continue; - - rhs0 = code[and->rhs0]; - rhs1 = code[and->rhs1]; - - and = public->ands + j++; - - if (rhs0 < rhs1) - { - tmp = rhs1; - rhs1 = rhs0; - rhs0 = tmp; - } - - assert (lhs > rhs0); - assert (rhs0 >= rhs1); - - and->lhs = lhs; - and->rhs0 = rhs0; - and->rhs1 = rhs1; - } - public->num_ands = j; - - qsort (public->ands, j, sizeof (*and), cmp_lhs); - - /* Reset types. - */ - for (i = 1; i <= public->maxvar; i++) - { - type = private->types + i; - type->input = 0; - type->latch = 0; - type->and = 0; - type->idx = 0; - } - - assert (new); - assert (public->maxvar >= aiger_lit2var (new - 1)); - public->maxvar = aiger_lit2var (new - 1); - - /* Fix types for ANDs. - */ - for (i = 0; i < public->num_ands; i++) - { - and = public->ands + i; - type = private->types + aiger_lit2var (and->lhs); - type->and = 1; - type->idx = i; - } - - /* Fix types for inputs. - */ - for (i = 0; i < public->num_inputs; i++) - { - symbol = public->inputs + i; - assert (symbol->lit < size_code); - symbol->lit = code[symbol->lit]; - type = private->types + aiger_lit2var (symbol->lit); - type->input = 1; - type->idx = i; - } - - /* Fix types for latches. - */ - for (i = 0; i < public->num_latches; i++) - { - symbol = public->latches + i; - symbol->lit = code[symbol->lit]; - type = private->types + aiger_lit2var (symbol->lit); - type->latch = 1; - type->idx = i; - } - - DELETEN (code, size_code); - -#ifndef NDEBUG - for (i = 0; i <= public->maxvar; i++) - { - type = private->types + i; - assert (!(type->input && type->latch)); - assert (!(type->input && type->and)); - assert (!(type->latch && type->and)); - } -#endif - assert (aiger_is_reencoded (public)); - assert (!aiger_check (public)); -} - -const unsigned char * -aiger_coi (aiger * public) -{ - IMPORT_private_FROM (public); - private->size_coi = public->maxvar + 1; - NEWN (private->coi, private->size_coi); - memset (private->coi, 1, private->size_coi); - return private->coi; -} - -static int -aiger_write_binary (aiger * public, void *state, aiger_put put) -{ - aiger_and *and; - unsigned lhs, i; - - assert (!aiger_check (public)); - - aiger_reencode (public); - - if (!aiger_write_header (public, "aig", 1, state, put)) - return 0; - - lhs = aiger_max_input_or_latch (public) + 2; - - for (i = 0; i < public->num_ands; i++) - { - and = public->ands + i; - - assert (lhs == and->lhs); - assert (lhs > and->rhs0); - assert (and->rhs0 >= and->rhs1); - - if (!aiger_write_delta (state, put, lhs - and->rhs0)) - return 0; - - if (!aiger_write_delta (state, put, and->rhs0 - and->rhs1)) - return 0; - - lhs += 2; - } - - return 1; -} - -unsigned -aiger_strip_symbols_and_comments (aiger * public) -{ - IMPORT_private_FROM (public); - unsigned res; - - assert (!aiger_error (public)); - - res = aiger_delete_comments (public); - - res += aiger_delete_symbols_aux (private, - public->inputs, - private->size_inputs); - res += aiger_delete_symbols_aux (private, - public->latches, - private->size_latches); - res += aiger_delete_symbols_aux (private, - public->outputs, - private->size_outputs); - res += aiger_delete_symbols_aux (private, - public->bad, - private->size_bad); - res += aiger_delete_symbols_aux (private, - public->constraints, - private->size_constraints); - res += aiger_delete_symbols_aux (private, - public->justice, - private->size_justice); - res += aiger_delete_symbols_aux (private, - public->fairness, - private->size_fairness); - return res; -} - -int -aiger_write_generic (aiger * public, - aiger_mode mode, void *state, aiger_put put) -{ - assert (!aiger_error (public)); - - if ((mode & aiger_ascii_mode)) - { - if (!aiger_write_ascii (public, state, put)) - return 0; - } - else - { - if (!aiger_write_binary (public, state, put)) - return 0; - } - - if (!(mode & aiger_stripped_mode)) - { - if (aiger_have_at_least_one_symbol (public)) - { - if (!aiger_write_symbols (public, state, put)) - return 0; - } - - if (public->comments[0]) - { - if (aiger_put_s (state, put, "c\n") == EOF) - return 0; - - if (!aiger_write_comments (public, state, put)) - return 0; - } - } - - return 1; -} - -int -aiger_write_to_file (aiger * public, aiger_mode mode, FILE * file) -{ - assert (!aiger_error (public)); - return aiger_write_generic (public, - mode, file, (aiger_put) aiger_default_put); -} - -int -aiger_write_to_string (aiger * public, aiger_mode mode, char *str, size_t len) -{ - aiger_buffer buffer; - int res; - - assert (!aiger_error (public)); - - buffer.start = str; - buffer.cursor = str; - buffer.end = str + len; - res = aiger_write_generic (public, - mode, &buffer, (aiger_put) aiger_string_put); - - if (!res) - return 0; - - if (aiger_string_put (0, &buffer) == EOF) - return 0; - - return 1; -} - -static int -aiger_has_suffix (const char *str, const char *suffix) -{ - if (strlen (str) < strlen (suffix)) - return 0; - - return !strcmp (str + strlen (str) - strlen (suffix), suffix); -} - -int -aiger_open_and_write_to_file (aiger * public, const char *file_name) -{ - IMPORT_private_FROM (public); - int res, pclose_file; - char *cmd, size_cmd; - aiger_mode mode; - FILE *file; - - assert (!aiger_error (public)); - - assert (file_name); - - if (aiger_has_suffix (file_name, ".gz")) - { - size_cmd = strlen (file_name) + strlen (GZIP); - NEWN (cmd, size_cmd); - sprintf (cmd, GZIP, file_name); - file = popen (cmd, "w"); - DELETEN (cmd, size_cmd); - pclose_file = 1; - } - else - { - file = fopen (file_name, "w"); - pclose_file = 0; - } - - if (!file) - return 0; - - if (aiger_has_suffix (file_name, ".aag") || - aiger_has_suffix (file_name, ".aag.gz")) - mode = aiger_ascii_mode; - else - mode = aiger_binary_mode; - - res = aiger_write_to_file (public, mode, file); - - if (pclose_file) - pclose (file); - else - fclose (file); - - if (!res) - unlink (file_name); - - return res; -} - -static int -aiger_next_ch (aiger_reader * reader) -{ - int res; - - res = reader->get (reader->state); - - if (isspace (reader->ch) && !isspace (res)) - reader->lineno_at_last_token_start = reader->lineno; - - reader->ch = res; - - if (reader->done_with_reading_header && reader->looks_like_aag) - { - if (!isspace (res) && !isdigit (res) && res != EOF) - reader->looks_like_aag = 0; - } - - if (res == '\n') - reader->lineno++; - - if (res != EOF) - reader->charno++; - - return res; -} - -/* Read a number assuming that the current character has already been - * checked to be a digit, e.g. the start of the number to be read. - */ -static unsigned -aiger_read_number (aiger_reader * reader) -{ - unsigned res; - - assert (isdigit (reader->ch)); - res = reader->ch - '0'; - - while (isdigit (aiger_next_ch (reader))) - res = 10 * res + (reader->ch - '0'); - - return res; -} - -/* Expect and read an unsigned number followed by at least one white space - * character. The white space should either the space character or a new - * line as specified by the 'followed_by' parameter. If a number can not be - * found or there is no white space after the number, an apropriate error - * message is returned. - */ -static const char * -aiger_read_literal (aiger_private * private, - aiger_reader * reader, - const char * context, - unsigned *res_ptr, - char expected_followed_by, - char * followed_by_ptr) -{ - unsigned res; - - assert (expected_followed_by == ' ' || - expected_followed_by == '\n' || - !expected_followed_by); - - if (!isdigit (reader->ch)) - return aiger_error_us (private, - "line %u: expected %s", - reader->lineno, context); - - res = aiger_read_number (reader); - - if (expected_followed_by == ' ') - { - if (reader->ch != ' ') - return aiger_error_usu (private, - "line %u: expected space after %s %u", - reader->lineno_at_last_token_start, context, res); -} - if (expected_followed_by == '\n') - { - if (reader->ch != '\n') - return aiger_error_usu (private, - "line %u: expected new line after %s %u", - reader->lineno_at_last_token_start, context, res); -} - if (!expected_followed_by) - { - if (reader->ch != '\n' && reader->ch != ' ') - return aiger_error_usu (private, - "line %u: expected space or new line after %s %u", - reader->lineno_at_last_token_start, context, res); - } - - if (followed_by_ptr) - *followed_by_ptr = reader->ch; - - aiger_next_ch (reader); /* skip white space */ - - *res_ptr = res; - - return 0; -} - -static const char * -aiger_already_defined (aiger * public, aiger_reader * reader, unsigned lit) -{ - IMPORT_private_FROM (public); - aiger_type *type; - unsigned var; - - assert (lit); - assert (!aiger_sign (lit)); - - var = aiger_lit2var (lit); - - if (public->maxvar < var) - return 0; - - type = private->types + var; - - if (type->input) - return aiger_error_uu (private, - "line %u: literal %u already defined as input", - reader->lineno_at_last_token_start, lit); - - if (type->latch) - return aiger_error_uu (private, - "line %u: literal %u already defined as latch", - reader->lineno_at_last_token_start, lit); - - if (type->and) - return aiger_error_uu (private, - "line %u: literal %u already defined as AND", - reader->lineno_at_last_token_start, lit); - return 0; -} - -static const char * -aiger_read_header (aiger * public, aiger_reader * reader) -{ - IMPORT_private_FROM (public); - unsigned i, j, lit, next, reset; - unsigned * sizes, * lits; - const char *error; - char ch; - - aiger_next_ch (reader); - if (reader->ch != 'a') - return aiger_error_u (private, - "line %u: expected 'a' as first character", - reader->lineno); - - if (aiger_next_ch (reader) != 'i' && reader->ch != 'a') - return aiger_error_u (private, - "line %u: expected 'i' or 'a' after 'a'", - reader->lineno); - - if (reader->ch == 'a') - reader->mode = aiger_ascii_mode; - else - reader->mode = aiger_binary_mode; - - if (aiger_next_ch (reader) != 'g') - return aiger_error_u (private, - "line %u: expected 'g' after 'a[ai]'", - reader->lineno); - - if (aiger_next_ch (reader) != ' ') - return aiger_error_u (private, - "line %u: expected ' ' after 'a[ai]g'", - reader->lineno); - - aiger_next_ch (reader); - - if (aiger_read_literal (private, reader, - "maximum variable index", &reader->maxvar, ' ', 0) || - aiger_read_literal (private, reader, - "number of inputs", &reader->inputs, ' ', 0) || - aiger_read_literal (private, reader, - "number latches", &reader->latches, ' ', 0) || - aiger_read_literal (private, reader, - "number of outputs", &reader->outputs, ' ', 0) || - aiger_read_literal (private, reader, - "number of and gates", &reader->ands, 0, &ch) || - (ch == ' ' && - aiger_read_literal (private, reader, - "number of bad state constraints", &reader->bad, 0, &ch)) || - (ch == ' ' && - aiger_read_literal (private, reader, - "number of invariant constraints", - &reader->constraints, 0, &ch)) || - (ch == ' ' && - aiger_read_literal (private, reader, - "number of justice constraints", &reader->justice, 0, &ch)) || - (ch == ' ' && - aiger_read_literal (private, reader, - "number of fairness constraints", &reader->fairness, '\n', 0))) - { - assert (private->error); - return private->error; - } - - if (reader->mode == aiger_binary_mode) - { - i = reader->inputs; - i += reader->latches; - i += reader->ands; - - if (i != reader->maxvar) - return aiger_error_u (private, - "line %u: invalid maximal variable index", - reader->lineno); - } - - public->maxvar = reader->maxvar; - - FIT (private->types, private->size_types, public->maxvar + 1); - FIT (public->inputs, private->size_inputs, reader->inputs); - FIT (public->latches, private->size_latches, reader->latches); - FIT (public->outputs, private->size_outputs, reader->outputs); - FIT (public->ands, private->size_ands, reader->ands); - FIT (public->bad, private->size_bad, reader->bad); - FIT (public->constraints, private->size_constraints, reader->constraints); - FIT (public->justice, private->size_justice, reader->justice); - FIT (public->fairness, private->size_fairness, reader->fairness); - - for (i = 0; i < reader->inputs; i++) - { - if (reader->mode == aiger_ascii_mode) - { - error = aiger_read_literal (private, reader, - "input literal", &lit, '\n', 0); - if (error) - return error; - - if (!lit || aiger_sign (lit) - || aiger_lit2var (lit) > public->maxvar) - return aiger_error_uu (private, - "line %u: literal %u is not a valid input", - reader->lineno_at_last_token_start, lit); - - error = aiger_already_defined (public, reader, lit); - if (error) - return error; - } - else - lit = 2 * (i + 1); - - aiger_add_input (public, lit, 0); - } - - for (i = 0; i < reader->latches; i++) - { - if (reader->mode == aiger_ascii_mode) - { - error = aiger_read_literal (private, reader, - "latch literal", &lit, ' ', 0); - if (error) - return error; - - if (!lit || aiger_sign (lit) - || aiger_lit2var (lit) > public->maxvar) - return aiger_error_uu (private, - "line %u: literal %u is not a valid latch", - reader->lineno_at_last_token_start, lit); - - error = aiger_already_defined (public, reader, lit); - if (error) - return error; - } - else - lit = 2 * (i + reader->inputs + 1); - - error = aiger_read_literal (private, reader, - "next state literal", &next, 0, &ch); - if (error) - return error; - - if (aiger_lit2var (next) > public->maxvar) - return aiger_error_uu (private, - "line %u: literal %u is not a valid literal", - reader->lineno_at_last_token_start, next); - - aiger_add_latch (public, lit, next, 0); - - if (ch == ' ') - { - error = aiger_read_literal (private, reader, - "reset literal", &reset, '\n', 0); - if (error) - return error; - - aiger_add_reset (public, lit, reset); - } - } - - for (i = 0; i < reader->outputs; i++) - { - error = aiger_read_literal (private, reader, - "output literal", &lit, '\n', 0); - if (error) - return error; - - if (aiger_lit2var (lit) > public->maxvar) - return aiger_error_uu (private, - "line %u: literal %u is not a valid output", - reader->lineno_at_last_token_start, lit); - - aiger_add_output (public, lit, 0); - } - - for (i = 0; i < reader->bad; i++) - { - error = aiger_read_literal (private, reader, - "bad state constraint literal", &lit, '\n', 0); - if (error) - return error; - - if (aiger_lit2var (lit) > public->maxvar) - return aiger_error_uu (private, - "line %u: literal %u is not valid bad", - reader->lineno_at_last_token_start, lit); - - aiger_add_bad (public, lit, 0); - } - - for (i = 0; i < reader->constraints; i++) - { - error = aiger_read_literal (private, reader, - "invariant constraint literal", &lit, '\n', 0); - if (error) - return error; - - if (aiger_lit2var (lit) > public->maxvar) - return aiger_error_uu (private, - "line %u: literal %u is not a valid constraint", - reader->lineno_at_last_token_start, lit); - - aiger_add_constraint (public, lit, 0); - } - - if (reader->justice) - { - NEWN (sizes, reader->justice); - error = 0; - for (i = 0; !error && i < reader->justice; i++) - error = aiger_read_literal (private, reader, - "justice constraint size", sizes + i, '\n', 0); - for (i = 0; !error && i < reader->justice; i++) - { - NEWN (lits, sizes[i]); - for (j = 0; !error && j < sizes[i]; j++) - error = aiger_read_literal (private, reader, - "justice constraint literal", lits + j, '\n', 0); - if (!error) - aiger_add_justice (public, sizes[i], lits, 0); - DELETEN (lits, sizes[i]); - } - DELETEN (sizes, reader->justice); - if (error) - return error; - } - - for (i = 0; i < reader->fairness; i++) - { - error = aiger_read_literal (private, reader, - "fairness constraint literal", &lit, '\n', 0); - if (error) - return error; - - if (aiger_lit2var (lit) > public->maxvar) - return aiger_error_uu (private, - "line %u: literal %u is not valid fairness", - reader->lineno_at_last_token_start, lit); - - aiger_add_fairness (public, lit, 0); - } - - reader->done_with_reading_header = 1; - reader->looks_like_aag = 1; - - return 0; -} - -static const char * -aiger_read_ascii (aiger * public, aiger_reader * reader) -{ - IMPORT_private_FROM (public); - unsigned i, lhs, rhs0, rhs1; - const char *error; - - for (i = 0; i < reader->ands; i++) - { - error = aiger_read_literal (private, reader, - "and gate left-hand side literal", &lhs, ' ', 0); - if (error) - return error; - - if (!lhs || aiger_sign (lhs) || aiger_lit2var (lhs) > public->maxvar) - return aiger_error_uu (private, - "line %u: " - "literal %u is not a valid LHS of AND", - reader->lineno_at_last_token_start, lhs); - - error = aiger_already_defined (public, reader, lhs); - if (error) - return error; - - error = aiger_read_literal (private, reader, - "and gate first right-hand side literal", - &rhs0, ' ', 0); - if (error) - return error; - - if (aiger_lit2var (rhs0) > public->maxvar) - return aiger_error_uu (private, - "line %u: literal %u is not a valid literal", - reader->lineno_at_last_token_start, rhs0); - - error = aiger_read_literal (private, reader, - "and gate first right-hand side literal", - &rhs1, '\n', 0); - if (error) - return error; - - if (aiger_lit2var (rhs1) > public->maxvar) - return aiger_error_uu (private, - "line %u: literal %u is not a valid literal", - reader->lineno_at_last_token_start, rhs1); - - aiger_add_and (public, lhs, rhs0, rhs1); - } - - return 0; -} - -static const char * -aiger_read_delta (aiger_private * private, aiger_reader * reader, - unsigned *res_ptr) -{ - unsigned res, i, charno; - unsigned char ch; - - if (reader->ch == EOF) - UNEXPECTED_EOF: - return aiger_error_u (private, - "character %u: unexpected end of file", - reader->charno); - i = 0; - res = 0; - ch = reader->ch; - - charno = reader->charno; - - while ((ch & 0x80)) - { - assert (sizeof (unsigned) == 4); - - if (i == 5) - INVALID_CODE: - return aiger_error_u (private, "character %u: invalid code", charno); - - res |= (ch & 0x7f) << (7 * i++); - aiger_next_ch (reader); - if (reader->ch == EOF) - goto UNEXPECTED_EOF; - - ch = reader->ch; - } - - if (i == 5 && ch >= 8) - goto INVALID_CODE; - - res |= ch << (7 * i); - *res_ptr = res; - - aiger_next_ch (reader); - - return 0; -} - -static const char * -aiger_read_binary (aiger * public, aiger_reader * reader) -{ - unsigned i, lhs, rhs0, rhs1, delta, charno; - IMPORT_private_FROM (public); - const char *error; - - delta = 0; /* avoid warning with -O3 */ - - lhs = aiger_max_input_or_latch (public); - - for (i = 0; i < reader->ands; i++) - { - lhs += 2; - charno = reader->charno; - error = aiger_read_delta (private, reader, &delta); - if (error) - return error; - - if (delta > lhs) /* can at most be the same */ - INVALID_DELTA: - return aiger_error_u (private, "character %u: invalid delta", charno); - - rhs0 = lhs - delta; - - charno = reader->charno; - error = aiger_read_delta (private, reader, &delta); - if (error) - return error; - - if (delta > rhs0) /* can well be the same ! */ - goto INVALID_DELTA; - - rhs1 = rhs0 - delta; - - aiger_add_and (public, lhs, rhs0, rhs1); - } - - return 0; -} - -static void -aiger_reader_push_ch (aiger_private * private, aiger_reader * reader, char ch) -{ - PUSH (reader->buffer, reader->top_buffer, reader->size_buffer, ch); -} - -static const char * -aiger_read_comments (aiger * public, aiger_reader * reader) -{ - IMPORT_private_FROM (public); - assert( reader->ch == '\n' ); - - aiger_next_ch (reader); - - while (reader->ch != EOF) - { - while (reader->ch != '\n') - { - aiger_reader_push_ch (private, reader, reader->ch); - aiger_next_ch (reader); - - if (reader->ch == EOF) - return aiger_error_u (private, - "line %u: new line after comment missing", - reader->lineno); - } - - aiger_next_ch (reader); - aiger_reader_push_ch (private, reader, 0); - aiger_add_comment (public, reader->buffer); - reader->top_buffer = 0; - } - - return 0; -} - -static const char * -aiger_read_symbols_and_comments (aiger * public, aiger_reader * reader) -{ - IMPORT_private_FROM (public); - const char *error, *type_name, * type_pos; - unsigned pos, num, count; - aiger_symbol *symbol; - - assert (!reader->buffer); - - for (count = 0;; count++) - { - if (reader->ch == EOF) - return 0; - - if (reader->ch != 'i' && - reader->ch != 'l' && - reader->ch != 'o' && - reader->ch != 'b' && - reader->ch != 'c' && - reader->ch != 'j' && - reader->ch != 'f') - { - if (reader->looks_like_aag) - return aiger_error_u (private, - "line %u: corrupted symbol table " - "('aig' instead of 'aag' header?)", - reader->lineno); - return aiger_error_u (private, - "line %u: expected '[cilobcjf]' or EOF", - reader->lineno); - } - - /* 'c' is a special case as it may be either the start of a comment, - or the start of a constraint symbol */ - if (reader->ch == 'c') - { - if (aiger_next_ch (reader) == '\n' ) - return aiger_read_comments(public, reader); - - type_name = "constraint"; - type_pos = "constraint"; - num = public->num_constraints; - symbol = public->constraints; - - if (!num) - return aiger_error_u (private, - "line %u: " - "unexpected invariance constraint symbol entry prefix 'c ' " - "(comment sections start with 'c' without space)", - reader->lineno_at_last_token_start); - } - else - { - if (reader->ch == 'i') - { - type_name = "input"; - type_pos = "input"; - num = public->num_inputs; - symbol = public->inputs; - } - else if (reader->ch == 'l') - { - type_name = "latch"; - type_pos = "latch"; - num = public->num_latches; - symbol = public->latches; - } - else if (reader->ch == 'o') - { - type_name = "output"; - type_pos = "output"; - num = public->num_outputs; - symbol = public->outputs; - } - else if (reader->ch == 'b') - { - type_name = "bad"; - type_pos = "bad"; - num = public->num_bad; - symbol = public->bad; - } - else if (reader->ch == 'j') - { - type_name = "justice"; - type_pos = "justice"; - num = public->num_justice; - symbol = public->justice; - } - else - { - assert (reader->ch == 'f'); - type_name = "fairness"; - type_pos = "fairness"; - num = public->num_fairness; - symbol = public->fairness; - } - - aiger_next_ch (reader); - } - - error = aiger_read_literal (private, reader, - type_pos, &pos, ' ', 0); - if (error) - return error; - - if (pos >= num) - return aiger_error_usu (private, - "line %u: " - "%s symbol table entry position %u too large", - reader->lineno_at_last_token_start, type_name, pos); - - symbol += pos; - - if (symbol->name) - return aiger_error_usu (private, - "line %u: %s literal %u has multiple symbols", - reader->lineno_at_last_token_start, type_name, - symbol->lit); - - while (reader->ch != '\n' && reader->ch != EOF) - { - aiger_reader_push_ch (private, reader, reader->ch); - aiger_next_ch (reader); - } - - if (reader->ch == EOF) - return aiger_error_u (private, - "line %u: new line missing", reader->lineno); - - assert (reader->ch == '\n'); - aiger_next_ch (reader); - - aiger_reader_push_ch (private, reader, 0); - symbol->name = aiger_copy_str (private, reader->buffer); - reader->top_buffer = 0; - } -} - -const char * -aiger_read_generic (aiger * public, void *state, aiger_get get) -{ - IMPORT_private_FROM (public); - aiger_reader reader; - const char *error; - - assert (!aiger_error (public)); - - CLR (reader); - - reader.lineno = 1; - reader.state = state; - reader.get = get; - reader.ch = ' '; - - error = aiger_read_header (public, &reader); - if (error) - return error; - - if (reader.mode == aiger_ascii_mode) - error = aiger_read_ascii (public, &reader); - else - error = aiger_read_binary (public, &reader); - - if (error) - return error; - - error = aiger_read_symbols_and_comments (public, &reader); - - DELETEN (reader.buffer, reader.size_buffer); - - if (error) - return error; - - return aiger_check (public); -} - -const char * -aiger_read_from_file (aiger * public, FILE * file) -{ - assert (!aiger_error (public)); - return aiger_read_generic (public, file, (aiger_get) aiger_default_get); -} - -const char * -aiger_open_and_read_from_file (aiger * public, const char *file_name) -{ - IMPORT_private_FROM (public); - char *cmd, size_cmd; - const char *res; - int pclose_file; - FILE *file; - - assert (!aiger_error (public)); - - if (aiger_has_suffix (file_name, ".gz")) - { - size_cmd = strlen (file_name) + strlen (GUNZIP); - NEWN (cmd, size_cmd); - sprintf (cmd, GUNZIP, file_name); - file = popen (cmd, "r"); - DELETEN (cmd, size_cmd); - pclose_file = 1; - } - else - { - file = fopen (file_name, "rb"); - pclose_file = 0; - } - - if (!file) - return aiger_error_s (private, "can not read '%s'", file_name); - - res = aiger_read_from_file (public, file); - - if (pclose_file) - pclose (file); - else - fclose (file); - - return res; -} - -const char * -aiger_get_symbol (aiger * public, unsigned lit) -{ - IMPORT_private_FROM (public); - aiger_symbol *symbol; - aiger_type *type; - unsigned var; - - assert (!aiger_error (public)); - - assert (lit); - assert (!aiger_sign (lit)); - - var = aiger_lit2var (lit); - assert (var <= public->maxvar); - type = private->types + var; - - if (type->input) - symbol = public->inputs; - else if (type->latch) - symbol = public->latches; - else - return 0; - - return symbol[type->idx].name; -} - -static aiger_type * -aiger_lit2type (aiger * public, unsigned lit) -{ - IMPORT_private_FROM (public); - aiger_type *type; - unsigned var; - - var = aiger_lit2var (lit); - assert (var <= public->maxvar); - type = private->types + var; - - return type; -} - -int -aiger_lit2tag (aiger * public, unsigned lit) -{ - aiger_type * type; - lit = aiger_strip (lit); - if (!lit) return 0; - type = aiger_lit2type (public, lit); - if (type->input) return 1; - if (type->latch) return 2; - return 3; -} - -aiger_symbol * -aiger_is_input (aiger * public, unsigned lit) -{ - aiger_type *type; - aiger_symbol *res; - - assert (!aiger_error (public)); - type = aiger_lit2type (public, lit); - if (!type->input) - return 0; - - res = public->inputs + type->idx; - - return res; -} - -aiger_symbol * -aiger_is_latch (aiger * public, unsigned lit) -{ - aiger_symbol *res; - aiger_type *type; - - assert (!aiger_error (public)); - type = aiger_lit2type (public, lit); - if (!type->latch) - return 0; - - res = public->latches + type->idx; - - return res; -} - -aiger_and * -aiger_is_and (aiger * public, unsigned lit) -{ - aiger_type *type; - aiger_and *res; - - assert (!aiger_error (public)); - type = aiger_lit2type (public, lit); - if (!type->and) - return 0; - - res = public->ands + type->idx; - - return res; -} diff --git a/aiger.h b/aiger.h deleted file mode 100644 index 84437fb..0000000 --- a/aiger.h +++ /dev/null @@ -1,359 +0,0 @@ -/*************************************************************************** -Copyright (c) 2006 - 2018, Armin Biere, Johannes Kepler University. - -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. -***************************************************************************/ - -/*------------------------------------------------------------------------*/ -/* This file contains the API of the 'AIGER' library, which is a reader and - * writer for the AIGER AIG format. The code of the library - * consists of 'aiger.c' and 'aiger.h'. It is independent of 'simpaig.c' - * and 'simpaig.h'. - * library. - */ -#ifndef aiger_h_INCLUDED -#define aiger_h_INCLUDED - -#include - -/*------------------------------------------------------------------------*/ - -#define AIGER_VERSION "1.9" - -/*------------------------------------------------------------------------*/ - -typedef struct aiger aiger; -typedef struct aiger_and aiger_and; -typedef struct aiger_symbol aiger_symbol; - -/*------------------------------------------------------------------------*/ -/* AIG references are represented as unsigned integers and are called - * literals. The least significant bit is the sign. The index of a literal - * can be obtained by dividing the literal by two. Only positive indices - * are allowed, which leaves 0 for the boolean constant FALSE. The boolean - * constant TRUE is encoded as the unsigned number 1 accordingly. - */ -#define aiger_false 0 -#define aiger_true 1 - -#define aiger_is_constant(l) \ - ((l) == aiger_false || ((l) == aiger_true)) - -#define aiger_sign(l) \ - (((unsigned)(l))&1) - -#define aiger_strip(l) \ - (((unsigned)(l))&~1) - -#define aiger_not(l) \ - (((unsigned)(l))^1) - -/*------------------------------------------------------------------------*/ -/* Each literal is associated to a variable having an unsigned index. The - * variable index is obtained by deviding the literal index by two, which is - * the same as removing the sign bit. - */ -#define aiger_var2lit(i) \ - (((unsigned)(i)) << 1) - -#define aiger_lit2var(l) \ - (((unsigned)(l)) >> 1) - -/*------------------------------------------------------------------------*/ -/* Callback functions for client memory management. The 'free' wrapper will - * get as last argument the size of the memory as it was allocated. - */ -typedef void *(*aiger_malloc) (void *mem_mgr, size_t); -typedef void (*aiger_free) (void *mem_mgr, void *ptr, size_t); - -/*------------------------------------------------------------------------*/ -/* Callback function for client character stream reading. It returns an - * ASCII character or EOF. Thus is has the same semantics as the standard - * library 'getc'. See 'aiger_read_generic' for more details. - */ -typedef int (*aiger_get) (void *client_state); - -/*------------------------------------------------------------------------*/ -/* Callback function for client character stream writing. The return value - * is EOF iff writing failed and otherwise the character 'ch' casted to an - * unsigned char. It has therefore the same semantics as 'fputc' and 'putc' - * from the standard library. - */ -typedef int (*aiger_put) (char ch, void *client_state); - -/*------------------------------------------------------------------------*/ - -enum aiger_mode -{ - aiger_binary_mode = 0, - aiger_ascii_mode = 1, - aiger_stripped_mode = 2, /* can be ORed with one of the previous */ -}; - -typedef enum aiger_mode aiger_mode; - -/*------------------------------------------------------------------------*/ - -struct aiger_and -{ - unsigned lhs; /* as literal [2..2*maxvar], even */ - unsigned rhs0; /* as literal [0..2*maxvar+1] */ - unsigned rhs1; /* as literal [0..2*maxvar+1] */ -}; - -/*------------------------------------------------------------------------*/ - -struct aiger_symbol -{ - unsigned lit; /* as literal [0..2*maxvar+1] */ - unsigned next, reset; /* used only for latches */ - unsigned size, * lits; /* used only for justice */ - char *name; -}; - -/*------------------------------------------------------------------------*/ -/* This is the externally visible state of the library. The format is - * almost the same as the ASCII file format. The first part is exactly as - * in the header 'M I L O A' and optional 'B C J F' after the format identifier - * string. - */ -struct aiger -{ - /* variable not literal index, e.g. maxlit = 2*maxvar + 1 - */ - unsigned maxvar; - - unsigned num_inputs; - unsigned num_latches; - unsigned num_outputs; - unsigned num_ands; - unsigned num_bad; - unsigned num_constraints; - unsigned num_justice; - unsigned num_fairness; - - aiger_symbol *inputs; /* [0..num_inputs[ */ - aiger_symbol *latches; /* [0..num_latches[ */ - aiger_symbol *outputs; /* [0..num_outputs[ */ - aiger_symbol *bad; /* [0..num_bad[ */ - aiger_symbol *constraints; /* [0..num_constraints[ */ - aiger_symbol *justice; /* [0..num_justice[ */ - aiger_symbol *fairness; /* [0..num_fairness[ */ - - aiger_and *ands; /* [0..num_ands[ */ - - char **comments; /* zero terminated */ -}; - -/*------------------------------------------------------------------------*/ -/* Version and CVS identifier. - */ -const char *aiger_id (void); /* not working after moving to 'git' */ -const char *aiger_version (void); - -/*------------------------------------------------------------------------*/ -/* You need to initialize the library first. This generic initialization - * function uses standard 'malloc' and 'free' from the standard library for - * memory management. - */ -aiger *aiger_init (void); - -/*------------------------------------------------------------------------*/ -/* Same as previous initialization function except that a memory manager - * from the client is used for memory allocation. See the 'aiger_malloc' - * and 'aiger_free' definitions above. - */ -aiger *aiger_init_mem (void *mem_mgr, aiger_malloc, aiger_free); - -/*------------------------------------------------------------------------*/ -/* Reset and delete the library. - */ -void aiger_reset (aiger *); - -/*------------------------------------------------------------------------*/ -/* Treat the literal 'lit' as input, output, latch, bad, constraint, - * justice of fairness respectively. The - * literal of latches and inputs can not be signed nor a constant (< 2). - * You can not register latches nor inputs multiple times. An input can not - * be a latch. The last argument is the symbolic name if non zero. - * The same literal can of course be used for multiple outputs. - */ -void aiger_add_input (aiger *, unsigned lit, const char *); -void aiger_add_latch (aiger *, unsigned lit, unsigned next, const char *); -void aiger_add_output (aiger *, unsigned lit, const char *); -void aiger_add_bad (aiger *, unsigned lit, const char *); -void aiger_add_constraint (aiger *, unsigned lit, const char *); -void aiger_add_justice (aiger *, unsigned size, unsigned *, const char *); -void aiger_add_fairness (aiger *, unsigned lit, const char *); - -/*------------------------------------------------------------------------*/ -/* Add a reset value to the latch 'lit'. The 'lit' has to be a previously - * added latch and 'reset' is either '0', '1' or equal to 'lit', the latter - * means undefined. - */ -void aiger_add_reset (aiger *, unsigned lit, unsigned reset); - -/*------------------------------------------------------------------------*/ -/* Register an unsigned AND with AIGER. The arguments are signed literals - * as discussed above, e.g. the least significant bit stores the sign and - * the remaining bit the variable index. The 'lhs' has to be unsigned - * (even). It identifies the AND and can only be registered once. After - * registration an AND can be accessed through 'ands[aiger_lit2idx (lhs)]'. - */ -void aiger_add_and (aiger *, unsigned lhs, unsigned rhs0, unsigned rhs1); - -/*------------------------------------------------------------------------*/ -/* Add a line of comments. The comment may not contain a new line character. - */ -void aiger_add_comment (aiger *, const char *comment_line); - -/*------------------------------------------------------------------------*/ -/* This checks the consistency for debugging and testing purposes. In - * particular, it is checked that all 'next' literals of latches, all - * outputs, and all right hand sides of ANDs are defined, where defined - * means that the corresponding literal is a constant 0 or 1, or defined as - * an input, a latch, or AND gate. Furthermore the definitions of ANDs are - * checked to be non cyclic. If a check fails a corresponding error message - * is returned. - */ -const char *aiger_check (aiger *); - -/*------------------------------------------------------------------------*/ -/* These are the writer functions for AIGER. They return zero on failure. - * The assumptions on 'aiger_put' are the same as with 'fputc' from the - * standard library (see the 'aiger_put' definition above). Note, that - * writing in binary mode triggers 'aig_reencode' and thus destroys the - * original literal association and may even delete AND nodes. See - * 'aiger_reencode' for more details. - */ -int aiger_write_to_file (aiger *, aiger_mode, FILE *); -int aiger_write_to_string (aiger *, aiger_mode, char *str, size_t len); -int aiger_write_generic (aiger *, aiger_mode, void *state, aiger_put); - -/*------------------------------------------------------------------------*/ -/* The following function allows to write to a file. The write mode is - * determined from the suffix in the file name. The mode used is ASCII for - * a '.aag' suffix and binary mode otherwise. In addition a '.gz' suffix can - * be added which requests the file to written by piping it through 'gzip'. - * This feature assumes that the 'gzip' program is in your path and can be - * executed through 'popen'. The return value is non zero on success. - */ -int aiger_open_and_write_to_file (aiger *, const char *file_name); - -/*------------------------------------------------------------------------*/ -/* The binary format reencodes all indices. After normalization the input - * indices come first followed by the latch and then the AND indices. In - * addition the indices will be topologically sorted to respect the - * child/parent relation, e.g. child indices will always be smaller than - * their parent indices. This function can directly be called by the - * client. As a side effect, ANDs that are not in any cone of a next state - * function nor in any cone of an output function are discarded. The new - * indices of ANDs start immediately after all input and latch indices. The - * data structures are updated accordingly including 'maxvar'. The client - * data within ANDs is reset to zero. - */ -int aiger_is_reencoded (aiger *); -void aiger_reencode (aiger *); - -/*------------------------------------------------------------------------*/ -/* This function computes the cone of influence (coi). The coi contains - * those literals that may have an influence to one of the outputs. A - * variable 'v' is in the coi if the array returned as result is non zero at - * position 'v'. All other variables can be considered redundant. The array - * returned is valid until the next call to this function and will be - * deallocated on reset. - * - * TODO: this is just a stub and actually not really implemented yet. - */ -const unsigned char * aiger_coi (aiger *); /* [1..maxvar] */ - -/*------------------------------------------------------------------------*/ -/* Read an AIG from a FILE, a string, or through a generic interface. These - * functions return a non zero error message if an error occurred and - * otherwise 0. The paramater 'aiger_get' has the same return values as - * 'getc', e.g. it returns 'EOF' when done. After an error occurred the - * library becomes invalid. Only 'aiger_reset' or 'aiger_error' can be - * used. The latter returns the previously returned error message. - */ -const char *aiger_read_from_file (aiger *, FILE *); -const char *aiger_read_from_string (aiger *, const char *str); -const char *aiger_read_generic (aiger *, void *state, aiger_get); - -/*------------------------------------------------------------------------*/ -/* Returns a previously generated error message if the library is in an - * invalid state. After this function returns a non zero error message, - * only 'aiger_reset' can be called (beside 'aiger_error'). The library can - * reach an invalid through a failed read attempt, or if 'aiger_check' - * failed. - */ -const char *aiger_error (aiger *); - -/*------------------------------------------------------------------------*/ -/* Same semantics as with 'aiger_open_and_write_to_file' for reading. - */ -const char *aiger_open_and_read_from_file (aiger *, const char *); - -/*------------------------------------------------------------------------*/ -/* Write symbol table or the comments to a file. Result is zero on failure. - */ -int aiger_write_symbols_to_file (aiger *, FILE * file); -int aiger_write_comments_to_file (aiger *, FILE * file); - -/*------------------------------------------------------------------------*/ -/* Remove symbols and comments. The result is the number of symbols - * and comments removed. - */ -unsigned aiger_strip_symbols_and_comments (aiger *); - -/*------------------------------------------------------------------------*/ -/* If 'lit' is an input or a latch with a name, the symbolic name is - * returned. Note, that literals can be used for multiple outputs. - * Therefore there is no way to associate a name with a literal itself. - * Names for outputs are stored in the 'outputs' symbols and can only be - * accesed through a linear traversal of the output symbols. - */ -const char *aiger_get_symbol (aiger *, unsigned lit); - -/*------------------------------------------------------------------------*/ -/* Return tag of the literal: - * - * 0 = constant - * 1 = input - * 2 = latch - * 3 = and - */ - -int aiger_lit2tag (aiger *, unsigned lit); - -/*------------------------------------------------------------------------*/ -/* Check whether the given unsigned, e.g. even, literal was defined as - * 'input', 'latch' or 'and'. The command returns a zero pointer if the - * literal was not defined as 'input', 'latch', or 'and' respectively. - * Otherwise a pointer to the corresponding input or latch symbol is returned. - * In the case of an 'and' the AND node is returned. The returned symbol - * if non zero is in the respective array of 'inputs', 'latches' and 'ands'. - * It thus also allows to extract the position of an input or latch literal. - * For outputs this is not possible, since the same literal may be used for - * several outputs. - */ -aiger_symbol *aiger_is_input (aiger *, unsigned lit); -aiger_symbol *aiger_is_latch (aiger *, unsigned lit); -aiger_and *aiger_is_and (aiger *, unsigned lit); - -#endif diff --git a/circuit.cpp b/circuit.cpp deleted file mode 100644 index c50d477..0000000 --- a/circuit.cpp +++ /dev/null @@ -1,449 +0,0 @@ -#include "sweep.hpp" -#include "circuit.hpp" - -bool Sweep::match_xor(int x) { // check clause x, -y, -z <==> xor - int y = C[x][0], z = C[x][1]; - if (y >= 0 || z >= 0) return false; - if (del[-y] || del[-z] || !C[-y].sz || !C[-z].sz) return false; - int u1 = C[-y][0], v1 = C[-y][1]; - int u2 = C[-z][0], v2 = C[-z][1]; - if (u1 == -u2 && v1 == -v2) goto doit; - if (u1 == -v2 && v1 == -u2) goto doit; - return false; -doit: - del[x] = 1; - if (C[-y].outs <= 1) del[-y] = 2; - if (C[-z].outs <= 1) del[-z] = 2; - C[x][0] = C[-y][0], C[x][1] = C[-y][1]; - C[x].type = Xor; - - return true; -} - -bool Sweep::match_majority(int x) { - // x = -y & z - // z = -v & -w - // y = a1 & a2 - // v = a1 & a3 - // w = a2 & a3 - int y = C[x][0], z = C[x][1]; - if (y > 0) std::swap(y, z); - if (y >= 0 || z <= 0) return false; - if (del[-y] || del[z] || !C[-y].sz || !C[z].sz) return false; - int v = C[z][0], w = C[z][1]; - if (v >= 0 || w >= 0) return false; - if (del[-v] || del[-w] || !C[-v].sz || !C[-w].sz) return false; - // -y, -w, -v - int a = C[-y][0], b = C[-y][1]; - if (C[-v][1] == a || C[-v][1] == b) std::swap(C[-v][0], C[-v][1]); - if (C[-w][1] == a || C[-w][1] == b) std::swap(C[-w][0], C[-w][1]); - if (C[-v][0] != a && C[-w][0] != a) return false; - if (C[-v][0] != b && C[-w][0] != b) return false; - if (C[-v][1] != C[-w][1]) return false; - del[x] = 1; - if (C[-y].outs <= 1) del[-y] = 2; - if (C[z].outs <= 1) del[z] = 2; - 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].type = Majority; - return true; -} - -void Sweep::adjust_not() { - int *pos = new int[maxvar + 1]; - int *neg = new int[maxvar + 1]; - for (int i = 1; i <= maxvar; i++) - pos[i] = neg[i] = 0; - for (int i = 1; i <= maxvar; i++) { - if (!C[i].sz || del[i] == 2) continue; - for (int j = 0; j < C[i].sz; j++) { - int v = C[i][j]; - if (v > 0) pos[v]++; - else neg[-v]++; - } - } - for (int i = 1; i <= maxvar; i++) { - if (!C[i].sz || del[i] == 2) continue; - if (C[i].type == Xor && pos[i] == 0 && neg[i] > 0) { - for (int j = 0; j < C[i].sz; j++) - if (C[i][j] < 0 && C[-C[i][j]].neg == 0) {C[i][j] = -C[i][j]; C[i].neg = 1; break;} - } - // if (C[i].type == Xor) { - // int z = 0; - // for (int j = 0; j < C[i].sz; j++) - // if (C[i][j] < 0) {C[i][j] = -C[i][j]; z ^= 1;} - // if (z) C[i].neg = 1; - // } - } -} - -void Sweep::match_HA() { - std::map M; - int lits = maxvar << 1 | 1; - for (int i = 1; i <= maxvar; i++) { - if (!C[i].sz || del[i] == 2 || C[i].type != And) continue; - int mapid = C[i][0] * lits + C[i][1]; - M[mapid] = i; - } - for (int i = 1; i <= maxvar; i++) { - if (!C[i].sz || del[i] == 2 || C[i].type != Xor) continue; - int mapid = C[i][0] * lits + C[i][1]; - int id = M[mapid]; - if (id) { - C[i].type = HA; - C[i].carrier = id; - del[id] = 2; - continue; - } - - mapid = (-C[i][0]) * lits - C[i][1]; - id = M[mapid]; - if (id) { - C[i].type = HA; - C[i].carrier = id; - C[i][0] = -C[i][0]; - C[i][1] = -C[i][1]; - del[id] = 2; - continue; - } - - mapid = C[i][0] * lits - C[i][1]; - id = M[mapid]; - if (id) { - C[i].type = HA; - C[i].carrier = id; - C[i][1] = -C[i][1]; - C[i].neg = 1; - del[id] = 2; - continue; - } - - mapid = (-C[i][0]) * lits + C[i][1]; - id = M[mapid]; - if (id) { - C[i].type = HA; - C[i].carrier = id; - C[i][0] = -C[i][0]; - C[i].neg = 1; - del[id] = 2; - continue; - } - } -} - -bool Sweep::line_positive(int to) { - return (to < 0) == C[abs(to)].neg; -} - -void Sweep::recalculate_outs() { - for (int i = 1; i <= maxvar; i++) - C[i].outs = 0; - 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++) { - C[abs(c->to[j])].outs++; - } - } -} - -void Sweep::match_FA() { - for (int i = 1; i <= maxvar; i++) { - circuit *c = &C[i]; - if (!c->sz || del[i] == 2) continue; - if (c->type != HA) continue; - C[abs(c->carrier)].to.clear(); - C[abs(c->carrier)].to.push(i); - C[abs(c->carrier)].sz = 1; - C[abs(c->carrier)].neg = c->carrier < 0; - } - - for(int i=1; i<=maxvar; i++) { - if (!C[i].sz || del[i] == 2) continue; - - circuit *c = &C[i]; - - if(c->type != And) continue; - - if(c->sz != 2) continue; - - if(c->to[0] >= 0) continue; - if(c->to[1] >= 0) continue; - - if(C[abs(c->to[0])].sz != 1) continue; - if(C[abs(c->to[1])].sz != 1) continue; - - int ha1 = C[abs(c->to[0])][0]; - int ha2 = C[abs(c->to[1])][0]; - - ha1 = abs(ha1); - ha2 = abs(ha2); - - if(C[ha1].type != HA) continue; - if(C[ha2].type != HA) continue; - - bool check_link = true; - for(int k=0; ktype = FA; - fa->carrier = -i; - vec new_vec; - for(int k=0; kto); - fa->sz = fa->to.size(); - - C[i].to.clear(); - C[i].sz = 0; - C[i].neg = !C[i].neg; - } -} - -void Sweep::to_multi_input_gates() { - //printf("hello\n %d\n", maxvar); - std::queue q; - q.push(maxvar); - while(!q.empty()) { - int u = q.front(); - q.pop(); - - circuit *c = &C[u]; - - if(u == maxvar) { - for(int i=0; isz; i++) { - if (!C[abs(c->to[i])].sz || del[abs(c->to[i])] == 2) continue; - q.push(abs(c->to[i])); - } - continue; - } - - for(int i=0; isz; i++) { - circuit *t = &C[abs(c->to[i])]; - if(t->type != c->type) continue; - vec new_vec; - if(c->type == Xor) { - //printf("XOR: %d %d\n", u, c->to[i]); - for(int j=0; jsz; j++) { - new_vec.push(t->to[j]); - //printf("add %d\n", t->to[j]); - } - - for(int j=0; jsz; j++) { - if(i == j) { - if(!line_positive(c->to[j])) - new_vec[0] = -new_vec[0]; - } else { - new_vec.push(c->to[j]); - } - } - - if(t->outs == 1) { - del[abs(c->to[i])] = 2; - //printf("del: %d\n", c->to[i]); - } - - new_vec.copyTo(c->to); - c->sz = new_vec.size(); - - q.push(u); - break; - } - - if(c->type == And && line_positive(c->to[i])) { - if(t->to.size() == 0) continue; - - //printf("AND: %d %d\n", u, c->to[i]); - t->to.copyTo(new_vec); - //printf("new_vec %d\n", new_vec.size()); - - for(int j=0; jsz; j++) { - if(i != j) { - new_vec.push(c->to[j]); - } - } - - if(C[abs(c->to[i])].outs == 1) { - del[abs(c->to[i])] = 2; - } - - new_vec.copyTo(c->to); - c->sz = new_vec.size(); - - q.push(u); - - break; - } - } - - - - for(int i=0; isz; i++) { - if (!C[abs(c->to[i])].sz || del[abs(c->to[i])] == 2) continue; - q.push(abs(c->to[i])); - } - } -} - -void Sweep::to_dot_graph(const char* filename, int end_point) { - std::ofstream file(filename); - std::queue q; - q.push(abs(end_point)); - std::set used; - used.insert(abs(end_point)); - file << "digraph \"graph\" {\n"; - - char str[1024]; - - while(!q.empty()) { - int u = q.front(); - q.pop(); - circuit *c = &C[u]; - - if(!c->sz || del[u] == 2) continue; - - sprintf(str, "A%d[label=\"%d (%s)\"];\n", u, u, gate_type[c->type].c_str()); - file << str; - if (c->type == HA || c->type == FA) { - int a = u * (C[u].neg ? -1 : 1); - int b = c->carrier; - sprintf(str, "A%d->A%d[arrowhead=%s]\n", u, abs(b), !line_positive(b) ? "dot" : "none"); - file << str; - } - else { - int t = u * (C[u].neg ? -1 : 1); - } - for (int j = 0; j < c->sz; j++) { - /** - * 删除初始输入 - */ - 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; - } - - for(int j=0; jsz; j++) { - int x = abs(c->to[j]); - if(used.count(x)) continue; - used.insert(x); - q.push(x); - } - } - - file << "}\n"; -} - -void Sweep::identify() { - - del = new int[maxvar + 1]; - for (int i = 1; i <= maxvar; i++) del[i] = 0; - recalculate_outs(); - for (int i = 1; i <= maxvar; i++) { - if (!C[i].sz || del[i] == 2) continue; - if (match_xor(i)) continue; - } - - // recalculate_outs(); - - // 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(); - - //to_multi_input_gates(); - //match_FA(); - - // printf("digraph \"graph\" {\n"); - // for (int i = 1; i <= maxvar; i++) { - // circuit *c = &C[i]; - // if (!c->sz || del[i] == 2) continue; - - // printf("A%d[label=\"%d (%s)\"];\n", i, i, gate_type[c->type].c_str()); - - // if (c->type == HA || c->type == FA) { - // int a = i * (C[i].neg ? -1 : 1); - // int b = c->carrier; - // printf("A%d->A%d[arrowhead=%s]\n", i, abs(b), !line_positive(b) ? "dot" : "none"); - // } - // else { - // int t = i * (C[i].neg ? -1 : 1); - // } - // for (int j = 0; j < c->sz; j++) { - // if(abs(c->to[j]) <= 14) continue; - // printf("A%d->A%d[arrowhead=%s]\n", abs(c->to[j]), i, !line_positive(c->to[j]) ? "dot" : "none"); - // } - // } - // printf("}\n"); - - 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++) { - // circuit *c = &C[i]; - // if (del[i] == 2) continue; - // printf("%d : %d (outs)\n", i, c->outs); - // } - -} \ No newline at end of file diff --git a/circuit.hpp b/circuit.hpp deleted file mode 100644 index 384e563..0000000 --- a/circuit.hpp +++ /dev/null @@ -1,16 +0,0 @@ -#ifndef circuit_hpp_INCLUDED -#define circuit_hpp_INCLUDED - -enum gate_type {And, Xor, Majority, HA, FA}; -const std::string gate_type[5] = {"and", "xor", "majority", "HA", "FA"}; - -struct circuit { - vec to; - int sz, outs, type, neg, carrier; - circuit() : sz(0), outs(0), type(0), neg(0), carrier(0) {} - void push(int x) { to.push(x); sz++; } - int &operator [] (int index) { return to[index]; } - const int& operator [] (int index) const { return to[index]; } -}; - -#endif \ No newline at end of file diff --git a/cms.log b/cms.log deleted file mode 100644 index 8ae66aa..0000000 --- a/cms.log +++ /dev/null @@ -1,408 +0,0 @@ --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/fraig.cpp b/fraig.cpp deleted file mode 100644 index 1e8089f..0000000 --- a/fraig.cpp +++ /dev/null @@ -1,291 +0,0 @@ -#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 deleted file mode 100644 index 8804f3f..0000000 --- a/hCaD_V2/BUILD.md +++ /dev/null @@ -1,104 +0,0 @@ -# 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 deleted file mode 100644 index fbf1cdd..0000000 --- a/hCaD_V2/CONTRIBUTING +++ /dev/null @@ -1,4 +0,0 @@ -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 deleted file mode 100644 index 81065ff..0000000 --- a/hCaD_V2/LICENSE +++ /dev/null @@ -1,22 +0,0 @@ -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 deleted file mode 100644 index 756f3b8..0000000 --- a/hCaD_V2/README.md +++ /dev/null @@ -1,54 +0,0 @@ -[![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 deleted file mode 100644 index 347f583..0000000 --- a/hCaD_V2/VERSION +++ /dev/null @@ -1 +0,0 @@ -1.4.1 diff --git a/hCaD_V2/bin/starexec_run_default b/hCaD_V2/bin/starexec_run_default deleted file mode 100644 index d24f815..0000000 --- a/hCaD_V2/bin/starexec_run_default +++ /dev/null @@ -1,2 +0,0 @@ -#!/bin/sh -exec ./cadical --target=0 --walk=false $1 $2/proof.out diff --git a/hCaD_V2/configure b/hCaD_V2/configure deleted file mode 100755 index e761d26..0000000 --- a/hCaD_V2/configure +++ /dev/null @@ -1,494 +0,0 @@ -#!/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 [