diff --git a/.gitignore b/.gitignore index 259148f..b9ee5dc 100644 --- a/.gitignore +++ b/.gitignore @@ -30,3 +30,7 @@ *.exe *.out *.app + +acec +amulet2 +build \ No newline at end of file diff --git a/.vscode/settings.json b/.vscode/settings.json new file mode 100644 index 0000000..379d8e4 --- /dev/null +++ b/.vscode/settings.json @@ -0,0 +1,6 @@ +{ + "files.associations": { + "*.ejs": "html", + "iostream": "cpp" + } +} \ No newline at end of file diff --git a/acec.cpp b/acec.cpp new file mode 100644 index 0000000..d45d392 --- /dev/null +++ b/acec.cpp @@ -0,0 +1,147 @@ +#include + +#include "vec.hpp" +#include "circuit.hpp" +#include "sweep.hpp" + +#include "libopenf4.h" + +extern "C" { + #include "aiger.h" +} + +#define pvar(i) ((string((i) < 0 ? "N" : "") + "A" + std::to_string(abs(i))).c_str()) + +Sweep* sweep_init(int argv, char* args[]) { + Sweep *S = new Sweep(); + S->aig = aiger_init(); + S->det_v_sz = 0; + S->file = fopen(args[1], "r"); + return S; +} + +int main(int argv, char* args[]) { + Sweep *S = sweep_init(argv, args); + S->solve(); + + using namespace std; + //using namespace F4; + + // Create polynomial array. + vector polynomialArray; + + // Create variable name array. + vector variableName; + + set vars; + + int t = S->maxvar; + + for (int i = 1; i <= S->maxvar; i++) { + circuit *c = &(S->C[i]); + if (!c->sz || S->del[i] == 2) continue; + + if(c->type == And) { + char term[1024]; + sprintf(term, "-%s+%s", pvar(i * (S->C[i].neg ? -1 : 1)), pvar(c->to[0])); + for(int i=1; isz; i++) { + sprintf(term, "%s*%s", term, pvar(c->to[i])); + } + polynomialArray.push_back(term); + printf("%s\n", term); + } + if(c->type == Xor) { + string last = pvar(c->to[0]); + char term[1024]; + for(int i=1; isz-1; i++) { + string tmp = pvar(++t); + sprintf(term, "-%s-2*%s*%s+%s+%s", tmp.c_str(), last.c_str(), pvar(c->to[i]), last.c_str(), pvar(c->to[i])); + polynomialArray.push_back(term); + printf("%s\n", term); + last = tmp; + } + sprintf(term, "-%s-2*%s*%s+%s+%s", pvar(i * (S->C[i].neg ? -1 : 1)), last.c_str(), pvar(c->to[c->sz-1]), last.c_str(), pvar(c->to[c->sz-1])); + polynomialArray.push_back(term); + printf("%s\n", term); + } + + if (c->type == HA || c->type == FA) { + char term[1024]; + sprintf(term, "-%s-2*%s+%s", pvar(i * (S->C[i].neg ? -1 : 1)), pvar(c->carrier), pvar(c->to[0])); + for(int i=1; isz; i++) { + sprintf(term, "%s+%s", term, pvar(c->to[i])); + } + polynomialArray.push_back(term); + printf("%s\n", term); + } + + if(c->type == Majority) { + char term[1024]; + sprintf(term, "-%s-2*%s+%s", pvar(++t), pvar(i * (S->C[i].neg ? -1 : 1)), pvar(c->to[0])); + for(int i=1; isz; i++) { + sprintf(term, "%s+%s", term, pvar(c->to[i])); + } + polynomialArray.push_back(term); + printf("%s\n", term); + } + + // if (c->type == HA || c->type == FA) { + // printf("( %d %d )", i * (S->C[i].neg ? -1 : 1), c->carrier); + // } + // else { + // printf("%d", i * (S->C[i].neg ? -1 : 1)); + // } + + // printf(" = %s ( ", gate_type[c->type].c_str()); + + // for (int j = 0; j < c->sz; j++) { + // printf("%d ", c->to[j]); + // } + // puts(")"); + } + + for(int i=t; i>=1; i--) { + variableName.push_back(pvar(i)); + variableName.push_back(pvar(-i)); + char term[1024]; + sprintf(term, "-%s+%s^2", pvar(i), pvar(i)); + polynomialArray.emplace_back(term); + printf("%s\n", term); + sprintf(term, "%s+%s", pvar(i), pvar(-i)); + polynomialArray.emplace_back(term); + printf("%s\n", term); + } + + char term[1024]; + sprintf(term, "-%s+1", pvar(S->maxvar)); + polynomialArray.emplace_back(term); + printf("%s\n", term); + + // for(int i = 0; i < 6; i++) + // { + // variableName.push_back('x'+to_string(i)); + // } + + // // Fill the polynomial array. + // polynomialArray.emplace_back("x0+x1+x2+x3+x4+x5"); + // polynomialArray.emplace_back("x0*x1+x1*x2+x2*x3+x3*x4+x0*x5+x4*x5"); + // polynomialArray.emplace_back("x0*x1*x2+x1*x2*x3+x2*x3*x4+x0*x1*x5+x0*x4*x5+x3*x4*x5"); + // polynomialArray.emplace_back("x0*x1*x2*x3+x1*x2*x3*x4+x0*x1*x2*x5+x0*x1*x4*x5+x0*x3*x4*x5+x2*x3*x4*x5"); + // polynomialArray.emplace_back("x0*x1*x2*x3*x4+x0*x1*x2*x3*x5+x0*x1*x2*x4*x5+x0*x1*x3*x4*x5+x0*x2*x3*x4*x5+x1*x2*x3*x4*x5"); + // polynomialArray.emplace_back("x0*x1*x2*x3*x4*x5-1"); + + // Compute a reduce groebner basis. + vector basis = groebnerBasisF4(7, variableName.size(), variableName, polynomialArray, 1, 0); + + for(size_t i = 0; i < basis.size(); i++) + { + cout << basis[i] << endl; + } + + for(int i=t; i>=1; i--) { + printf("(declare-fun %s () Bool)", pvar(i)); + printf("(declare-fun %s () Bool)", pvar(-i)); + } + + return 0; +} \ No newline at end of file diff --git a/aiger.c b/aiger.c new file mode 100644 index 0000000..e6e5bb6 --- /dev/null +++ b/aiger.c @@ -0,0 +1,2775 @@ +/*************************************************************************** +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 new file mode 100644 index 0000000..84437fb --- /dev/null +++ b/aiger.h @@ -0,0 +1,359 @@ +/*************************************************************************** +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 new file mode 100644 index 0000000..7cb6c89 --- /dev/null +++ b/circuit.cpp @@ -0,0 +1,426 @@ +#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; + //printf("X: %d\n", i); + + 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]) <= num_inputs) 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"); + + //to_dot_graph("graph1.dot", abs(C[maxvar].to[0])); + //to_dot_graph("graph2.dot", abs(C[maxvar].to[1])); + + // recalculate_outs(); + // for (int i = 1; i <= maxvar; i++) { + // circuit *c = &C[i]; + // if (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 new file mode 100644 index 0000000..384e563 --- /dev/null +++ b/circuit.hpp @@ -0,0 +1,16 @@ +#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/f4cpp b/f4cpp new file mode 160000 index 0000000..645458c --- /dev/null +++ b/f4cpp @@ -0,0 +1 @@ +Subproject commit 645458ca02450215bd0e891fc3081d8cbc79c51f diff --git a/lib/libopenf4.so.0 b/lib/libopenf4.so.0 new file mode 100755 index 0000000..4720866 Binary files /dev/null and b/lib/libopenf4.so.0 differ diff --git a/lib/libopenf4.so.0.0.0 b/lib/libopenf4.so.0.0.0 new file mode 100755 index 0000000..4720866 Binary files /dev/null and b/lib/libopenf4.so.0.0.0 differ diff --git a/m4gb b/m4gb new file mode 160000 index 0000000..0a166c8 --- /dev/null +++ b/m4gb @@ -0,0 +1 @@ +Subproject commit 0a166c87ab7d156ccbbff807a0ad1ec50cff8d83 diff --git a/makefile b/makefile new file mode 100644 index 0000000..6f52d4f --- /dev/null +++ b/makefile @@ -0,0 +1,38 @@ +SRCS = $(shell find . -maxdepth 1 -name "*.c*") + +BUILD_DIR = build/ + +OBJS = $(addprefix $(BUILD_DIR), $(addsuffix .o, $(basename $(SRCS)))) + +EXEC = acec + +LIBS = -lgmp -Iopenf4 -Llib -lopenf4 + +CXXFLAGS=-O3 -std=c++17 + +$(EXEC): $(OBJS) + $(CXX) -o $@ $^ $(CXXFLAGS) $(LIBS) + +$(BUILD_DIR)%.o: %.cpp + $(CXX) -c $< -o $@ $(CXXFLAGS) $(LIBS) + +$(BUILD_DIR)%.o: %.c + gcc -c $< -o $@ $(CXXFLAGS) $(LIBS) + +clean: + rm -f $(OBJS) $(EXEC) + +# CFLAGS=-O3 + +# solver: aiger.o main.o $(LIBS) +# $(CXX) $^ -o $@ + +# aiger.o: aiger.c aiger.h +# $(C) $(CFLAGS) -c $< -o $@ + +# main.o: main.cpp aiger.h +# $(CC) $(CXXFLAGS) -c $< -o $@ + +# clean: +# rm -rf *.o +# rm -rf solver \ No newline at end of file diff --git a/mathic b/mathic new file mode 160000 index 0000000..66b5d74 --- /dev/null +++ b/mathic @@ -0,0 +1 @@ +Subproject commit 66b5d74f8417459414cbf3753cfa9a0128483cbd diff --git a/openf4 b/openf4 new file mode 160000 index 0000000..7155c6e --- /dev/null +++ b/openf4 @@ -0,0 +1 @@ +Subproject commit 7155c6ec4e5f776e0e12202716dc7da58469e77b diff --git a/result.txt b/result.txt new file mode 100644 index 0000000..e69de29 diff --git a/sweep.cpp b/sweep.cpp new file mode 100644 index 0000000..ed0cc40 --- /dev/null +++ b/sweep.cpp @@ -0,0 +1,76 @@ +#include "sweep.hpp" +#include "circuit.hpp" + +extern "C" { + #include "aiger.h" +} + +int Sweep::get_time() { + return std::chrono::duration_cast(std::chrono::high_resolution_clock::now() - clk_st).count(); +} + +void Sweep::aiger_preprocess() { + aiger_read_from_file(aig, file); + maxvar = aig->maxvar; + output = aig->outputs[0].lit; + num_inputs = aig->num_inputs; + + used = new int[maxvar + 1]; + C = new circuit[maxvar + 1]; + memset(used, 0, (maxvar + 1) * sizeof(int)); + sum_pos = new int[2 * maxvar + 2]; + sum_neg = new int[2 * maxvar + 2]; + memset(sum_pos, 0, sizeof(int) * (2 * maxvar + 2)); + memset(sum_neg, 0, sizeof(int) * (2 * maxvar + 2)); + + for(int i=0; inum_ands; i++) { + auto gate = aig->ands[i]; + int o = aiger_lit2var(gate.lhs); + int i0 = aiger_lit2var(gate.rhs0); + int i1 = aiger_lit2var(gate.rhs1); + graph.add(i0, o, gate.rhs0 & 1); + graph.add(i1, o, gate.rhs1 & 1); + + assert((gate.lhs & 1) == 0); + C[o].push(i0 * (gate.rhs0 & 1 ? -1 : 1)); + C[o].push(i1 * (gate.rhs1 & 1 ? -1 : 1)); + } + + // for (int i = 1; i <= maxvar; i++) { + // circuit *c = &C[i]; + // if (!c->sz) continue; + // printf("%d = %s ( ", i, gate_type[c->type].c_str()); + // for (int j = 0; j < c->sz; j++) { + // printf("%d ", c->to[j]); + // } + // puts(")"); + // } + return; + + printf("c inputs: \nc "); + for(int i=0; inum_inputs; i++) { + printf("%d ", aig->inputs[i].lit); + } + + printf("\nc outputs: \nc "); + + for(int i=0; inum_outputs; i++) { + printf("%d ", aig->outputs[i].lit); + } + printf("\nc maxvar: \nc %d\n", maxvar); + // int x = det_v > 0 ? det_v : -det_v; + // if (x > maxvar) det_v = 0; + printf("assume:"); + for (int i = 0; i < det_v_sz; i++) { + printf(" %d", det_v[i]); + } + puts(""); + cal_topo_index(); +} + +void Sweep::solve() { + aiger_preprocess(); + printf("c preprocess finish: %.2lf s\n", 0.001 * get_time()); + identify(); + printf("c identify finish: %.2lf s\n", 0.001 * get_time()); +} diff --git a/sweep.hpp b/sweep.hpp new file mode 100644 index 0000000..5a7cb22 --- /dev/null +++ b/sweep.hpp @@ -0,0 +1,100 @@ +#ifndef sweep_hpp_INCLUDED +#define sweep_hpp_INCLUDED +#include +#include +#include +#include "vec.hpp" + +namespace CaDiCaL { + struct Solver; +} + +struct aiger; +struct circuit; + +class Graph { +public: + struct Edge { + int from; + int to; + int neg; + }; + + std::vector> edge; + std::vector> redge; + void add(int u, int v, int w) { + edge.resize(std::max(std::max(u, v)+1, (int)edge.size())); + redge.resize(std::max(std::max(u, v)+1, (int)redge.size())); + + edge[u].push_back(Edge{u, v, w}); + redge[v].push_back(Edge{v, u, w}); + } +}; + + +class Sweep { +public: + FILE* file; + Graph graph; + + int maxvar, output, num_inputs; + + int *used, *det_v, *is_cut, *sum_pos, *sum_neg, *del; + int det_v_sz = 0; + int rounds; + + std::chrono::high_resolution_clock::time_point clk_st = std::chrono::high_resolution_clock::now(); + + circuit *C; + aiger *aig; + std::map topo_index; + + void solve(); + + void aiger_preprocess(); + + void cal_topo_index(); + + void propagate(int* input, int* result); + + void random_simulation(); + + void simulation(); + + bool check_var_equal(int x, int y, int assume); + + bool check_constant(int x, int val); + + void check_entire_problem(aiger* aig); + + void check_with_SAT(); + + void identify(); + + bool match_xor(int x); + + bool match_majority(int x); + + void adjust_not(); + + void match_HA(); + + void match_FA(); + + bool line_positive(int to); + + void recalculate_outs(); + + void to_multi_input_gates(); + + void simplify(); + + void miter(); + + void to_dot_graph(const char* filename, int end_point); + + int get_time(); +}; + + +#endif \ No newline at end of file diff --git a/vec.hpp b/vec.hpp new file mode 100644 index 0000000..99b3136 --- /dev/null +++ b/vec.hpp @@ -0,0 +1,95 @@ +#ifndef _vec_hpp_INCLUDED +#define _vec_hpp_INCLUDED + +#include +#include +#include +#include +#include +#include +#include + +template +class vec { + static inline int imax (int x, int y) { int mask = (y-x) >> (sizeof(int)*8-1); return (x&mask) + (y&(~mask)); } + static inline void nextCap(int &cap) { cap += ((cap >> 1) + 2) & ~1; } + + public: + T* data; + int sz, cap; + vec() : data(NULL), sz(0), cap(0) {} + vec(int size, const T& pad) : data(NULL) , sz(0) , cap(0) { growTo(size, pad); } + explicit vec(int size) : data(NULL), sz(0), cap(0) { growTo(size); } + ~vec() { clear(true); } + + operator T* (void) { return data; } + + int size (void) const { return sz; } + int capacity (void) const { return cap; } + void capacity (int min_cap); + + void setsize (int v) { sz = v;} + void push (void) { if (sz == cap) capacity(sz + 1); new (&data[sz]) T(); sz++; } + void push (const T& elem) { if (sz == cap) capInc(sz + 1); data[sz++] = elem; } + void push_ (const T& elem) { assert(sz < cap); data[sz++] = elem; } + void pop (void) { assert(sz > 0), sz--, data[sz].~T(); } + void copyTo (vec& copy) { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; } + + void growTo (int size); + void growTo (int size, const T& pad); + void clear (bool dealloc = false); + void capInc (int to_cap); + + + T& operator [] (int index) { return data[index]; } + const T& operator [] (int index) const { return data[index]; } + + T& last (void) { return data[sz - 1]; } + const T& last (void) const { return data[sz - 1]; } + +}; + + +class OutOfMemoryException{}; + +template +void vec::clear(bool dealloc) { + if (data != NULL) { + sz = 0; + if (dealloc) free(data), data = NULL, cap = 0; + } +} + +template +void vec::capInc(int to_cap) { + if (cap >= to_cap) return; + int add = imax((to_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); + if (add > __INT_MAX__ - cap || ((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM) + throw OutOfMemoryException(); +} + +template +void vec::capacity(int min_cap) { + if (cap >= min_cap) return; + int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2 + if (add > __INT_MAX__ - cap || ((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM) + throw OutOfMemoryException(); + } + +template +void vec::growTo(int size) { + if (sz >= size) return; + capInc(size); + for (int i = 0; i < sz; i++) new (&data[i]) T(); + sz = size; +} + +template +void vec::growTo(int size, const T& pad) { + if (sz >= size) return; + capacity(size); + for (int i = sz; i < size; i++) data[i] = pad; + sz = size; } + + +#endif \ No newline at end of file diff --git a/z3 b/z3 new file mode 160000 index 0000000..e2cfc53 --- /dev/null +++ b/z3 @@ -0,0 +1 @@ +Subproject commit e2cfc53c9fe44690bf4310ad0ce8d0b6deea91f5