commit b332eab2c421adf507bc010025e25e69a7be5179 Author: YuhangQ Date: Tue Oct 25 18:36:19 2022 +0800 init commit diff --git a/.nfs00000000052e02b10000046d b/.nfs00000000052e02b10000046d new file mode 100755 index 0000000..2ed69bb Binary files /dev/null and b/.nfs00000000052e02b10000046d differ diff --git a/.vscode/settings.json b/.vscode/settings.json new file mode 100644 index 0000000..41bc480 --- /dev/null +++ b/.vscode/settings.json @@ -0,0 +1,82 @@ +{ + "files.associations": { + "*.ejs": "html", + "any": "cpp", + "array": "cpp", + "atomic": "cpp", + "bit": "cpp", + "*.tcc": "cpp", + "bitset": "cpp", + "cctype": "cpp", + "cfenv": "cpp", + "charconv": "cpp", + "chrono": "cpp", + "cinttypes": "cpp", + "clocale": "cpp", + "cmath": "cpp", + "codecvt": "cpp", + "complex": "cpp", + "condition_variable": "cpp", + "csetjmp": "cpp", + "csignal": "cpp", + "cstdarg": "cpp", + "cstddef": "cpp", + "cstdint": "cpp", + "cstdio": "cpp", + "cstdlib": "cpp", + "cstring": "cpp", + "ctime": "cpp", + "cuchar": "cpp", + "cwchar": "cpp", + "cwctype": "cpp", + "deque": "cpp", + "forward_list": "cpp", + "list": "cpp", + "map": "cpp", + "set": "cpp", + "unordered_map": "cpp", + "unordered_set": "cpp", + "vector": "cpp", + "exception": "cpp", + "fstream": "cpp", + "functional": "cpp", + "future": "cpp", + "initializer_list": "cpp", + "iomanip": "cpp", + "iosfwd": "cpp", + "iostream": "cpp", + "istream": "cpp", + "limits": "cpp", + "memory": "cpp", + "memory_resource": "cpp", + "mutex": "cpp", + "new": "cpp", + "numeric": "cpp", + "optional": "cpp", + "ostream": "cpp", + "ratio": "cpp", + "regex": "cpp", + "scoped_allocator": "cpp", + "shared_mutex": "cpp", + "sstream": "cpp", + "stdexcept": "cpp", + "streambuf": "cpp", + "string": "cpp", + "string_view": "cpp", + "system_error": "cpp", + "thread": "cpp", + "type_traits": "cpp", + "tuple": "cpp", + "typeindex": "cpp", + "typeinfo": "cpp", + "utility": "cpp", + "valarray": "cpp", + "variant": "cpp", + "random": "cpp", + "algorithm": "cpp", + "iterator": "cpp", + "strstream": "cpp" + }, + "cmake.configureOnOpen": false, + "cmake.sourceDirectory": "${workspaceFolder}/abc" +} \ No newline at end of file diff --git a/abc_result b/abc_result new file mode 100644 index 0000000..c632d48 --- /dev/null +++ b/abc_result @@ -0,0 +1,3 @@ +ABC command line: "source abc_script". + +Networks are equivalent. Time = 1139.12 sec diff --git a/abc_script b/abc_script new file mode 100644 index 0000000..9838901 --- /dev/null +++ b/abc_script @@ -0,0 +1 @@ +&cec test0.aiger test1.aiger \ 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/bash.sh b/bash.sh new file mode 100755 index 0000000..bc27985 --- /dev/null +++ b/bash.sh @@ -0,0 +1,6 @@ +#/bin/bash +cd /home/qianyh/experiments/cec/equal + +#ls + +#./abc/abc -f abc_script > abc_result \ No newline at end of file diff --git a/cms.log b/cms.log new file mode 100644 index 0000000..cf9d4f3 --- /dev/null +++ b/cms.log @@ -0,0 +1,405 @@ +-285 -284 0 +-285 283 0 +284 -283 285 0 +292 176 295 0 +-284 -281 0 +-284 -255 0 +281 255 284 0 +-283 -282 0 +-283 -262 0 +282 262 283 0 +289 231 292 0 +-173 154 176 0 +-281 -280 0 +-281 279 0 +280 -279 281 0 +-255 -254 0 +-255 253 0 +254 -253 255 0 +-282 -281 0 +-282 -261 0 +281 261 282 0 +-262 -261 0 +-262 -255 0 +261 255 262 0 +-289 -288 0 +-289 287 0 +288 -287 289 0 +228 197 231 0 +-173 172 0 +-173 -157 0 +-172 157 173 0 +-151 124 154 0 +-280 -277 0 +-280 -101 0 +277 101 280 0 +-279 -278 0 +-279 -269 0 +278 269 279 0 +-254 251 0 +-254 144 0 +-251 -144 254 0 +-253 -252 0 +-253 -250 0 +252 250 253 0 +258 238 261 0 +-288 -285 0 +-288 -242 0 +285 242 288 0 +-287 -286 0 +-287 -249 0 +286 249 287 0 +225 208 228 0 +-197 -196 0 +-197 195 0 +196 -195 197 0 +-172 171 0 +-172 -160 0 +-171 160 172 0 +-150 127 157 0 +-151 150 0 +-151 -127 0 +-150 127 151 0 +121 88 124 0 +-277 -276 0 +-277 275 0 +276 -275 277 0 +96 95 101 0 +-278 -277 0 +-278 -268 0 +277 268 278 0 +-269 -268 0 +-269 -101 0 +268 101 269 0 +-251 137 0 +-251 135 0 +-137 -135 251 0 +-144 12 0 +-144 6 0 +-12 -6 144 0 +-252 251 0 +-252 98 0 +-251 -98 252 0 +-250 144 0 +-250 98 0 +-144 -98 250 0 +-97 58 258 0 +-235 105 238 0 +-242 -241 0 +-242 240 0 +241 -240 242 0 +-286 -285 0 +-286 -248 0 +285 248 286 0 +-249 -248 0 +-249 -242 0 +248 242 249 0 +222 216 225 0 +205 200 208 0 +-196 -193 0 +-196 -180 0 +193 180 196 0 +-195 -194 0 +-195 -187 0 +194 187 195 0 +-171 170 0 +-171 -163 0 +-170 163 171 0 +149 130 160 0 +-150 -149 0 +-150 -130 0 +149 130 150 0 +-119 116 127 0 +-121 -120 0 +-121 -115 0 +120 115 121 0 +85 78 88 0 +-276 -273 0 +-276 134 0 +273 -134 276 0 +-275 -274 0 +-275 -270 0 +274 270 275 0 +-96 15 0 +-96 8 0 +-15 -8 96 0 +-95 13 0 +-95 3 0 +-13 -3 95 0 +-265 251 268 0 +-137 12 0 +-137 11 0 +-12 -11 137 0 +-135 8 0 +-135 5 0 +-8 -5 135 0 +-98 11 0 +-98 5 0 +-11 -5 98 0 +-97 96 0 +-97 95 0 +-96 -95 97 0 +53 52 58 0 +106 55 235 0 +-105 6 0 +-105 5 0 +-6 -5 105 0 +-241 -238 0 +-241 97 0 +238 -97 241 0 +-240 -239 0 +-240 -232 0 +239 232 240 0 +245 193 248 0 +-219 42 222 0 +213 20 216 0 +-205 -204 0 +-205 203 0 +204 -203 205 0 +-41 27 200 0 +190 31 193 0 +-180 179 0 +-180 -116 0 +-179 116 180 0 +-194 -193 0 +-194 -186 0 +193 186 194 0 +-187 -186 0 +-187 -180 0 +186 180 187 0 +-170 169 0 +-170 -166 0 +-169 166 170 0 +-147 144 163 0 +-149 -148 0 +-149 -143 0 +148 143 149 0 +112 109 130 0 +114 91 119 0 +-116 106 0 +-116 105 0 +-106 -105 116 0 +-120 -119 0 +-120 116 0 +119 -116 120 0 +-115 -114 0 +-115 -91 0 +114 91 115 0 +-82 81 85 0 +75 48 78 0 +137 135 273 0 +-134 15 0 +-134 13 0 +-15 -13 134 0 +-274 -273 0 +-274 169 0 +273 -169 274 0 +-270 169 0 +-270 134 0 +-169 -134 270 0 +144 98 265 0 +-53 8 0 +-53 3 0 +-8 -3 53 0 +-52 13 0 +-52 7 0 +-13 -7 52 0 +-106 12 0 +-106 2 0 +-12 -2 106 0 +-55 15 0 +-55 11 0 +-15 -11 55 0 +-239 -238 0 +-239 -58 0 +238 58 239 0 +-232 97 0 +-232 -58 0 +-97 58 232 0 +186 180 245 0 +82 21 219 0 +-42 5 0 +-42 4 0 +-5 -4 42 0 +-213 -212 0 +-213 211 0 +212 -211 213 0 +17 16 20 0 +-204 63 0 +-204 -31 0 +-63 31 204 0 +-203 -202 0 +-203 -201 0 +202 201 203 0 +38 37 41 0 +-27 26 0 +-27 25 0 +-26 -25 27 0 +63 54 190 0 +26 25 31 0 +-179 -178 0 +-179 -177 0 +178 177 179 0 +-183 62 186 0 +-169 168 0 +-169 167 0 +-168 -167 169 0 +-140 137 166 0 +142 133 147 0 +-148 -147 0 +-148 144 0 +147 -144 148 0 +-143 -142 0 +-143 -133 0 +142 133 143 0 +103 94 112 0 +106 105 109 0 +-114 -113 0 +-114 -104 0 +113 104 114 0 +73 70 91 0 +-82 12 0 +-82 9 0 +-12 -9 82 0 +-81 -80 0 +-81 -79 0 +80 79 81 0 +-75 -74 0 +-75 -61 0 +74 61 75 0 +45 36 48 0 +-21 11 0 +-21 7 0 +-11 -7 21 0 +-212 67 0 +-212 62 0 +-67 -62 212 0 +-211 -210 0 +-211 -209 0 +210 209 211 0 +-17 10 0 +-17 8 0 +-10 -8 17 0 +-16 14 0 +-16 13 0 +-14 -13 16 0 +-63 5 0 +-63 2 0 +-5 -2 63 0 +-202 54 0 +-202 -31 0 +-54 31 202 0 +-201 63 0 +-201 54 0 +-63 -54 201 0 +-38 15 0 +-38 2 0 +-15 -2 38 0 +-37 6 0 +-37 3 0 +-6 -3 37 0 +-26 8 0 +-26 7 0 +-8 -7 26 0 +-25 13 0 +-25 10 0 +-13 -10 25 0 +-54 53 0 +-54 52 0 +-53 -52 54 0 +-178 105 0 +-178 55 0 +-105 -55 178 0 +-177 106 0 +-177 55 0 +-106 -55 177 0 +67 28 183 0 +-62 15 0 +-62 6 0 +-15 -6 62 0 +-168 12 0 +-168 8 0 +-12 -8 168 0 +-167 13 0 +-167 5 0 +-13 -5 167 0 +135 134 140 0 +-142 -141 0 +-142 -136 0 +141 136 142 0 +-101 98 133 0 +-103 -102 0 +-103 -97 0 +102 97 103 0 +-58 55 94 0 +-113 -112 0 +-113 -109 0 +112 109 113 0 +-104 -103 0 +-104 -94 0 +103 94 104 0 +60 51 73 0 +-67 66 70 0 +-80 67 0 +-80 -66 0 +-67 66 80 0 +-79 63 0 +-79 62 0 +-63 -62 79 0 +-74 -73 0 +-74 -70 0 +73 70 74 0 +-61 -60 0 +-61 -51 0 +60 51 61 0 +-42 41 45 0 +33 24 36 0 +-67 12 0 +-67 4 0 +-12 -4 67 0 +-210 62 0 +-210 28 0 +-62 -28 210 0 +-209 67 0 +-209 28 0 +-67 -28 209 0 +-28 11 0 +-28 3 0 +-11 -3 28 0 +-141 -140 0 +-141 137 0 +140 -137 141 0 +-136 135 0 +-136 134 0 +-135 -134 136 0 +-102 -101 0 +-102 98 0 +101 -98 102 0 +-60 -59 0 +-60 -54 0 +59 54 60 0 +-31 28 51 0 +63 62 66 0 +-33 -32 0 +-33 -27 0 +32 27 33 0 +-21 20 24 0 +-59 -58 0 +-59 55 0 +58 -55 59 0 +-32 -31 0 +-32 28 0 +31 -28 32 0 +-285 -295 0 +285 295 0 +-251 252 0 +251 -252 0 +-253 255 0 +253 -255 0 +-254 266 0 +254 -266 0 +-176 292 0 +176 -292 0 +-293 294 0 +293 -294 0 +c Solver::solve( ) diff --git a/cut.hpp b/cut.hpp new file mode 100644 index 0000000..9d47006 --- /dev/null +++ b/cut.hpp @@ -0,0 +1,280 @@ + + +// void cal_topo_index(aiger *aiger) { + +// static int* topo_counter = new int[aiger->maxvar + 1]; +// memset(topo_counter, 0, (aiger->maxvar + 1) * sizeof(int)); + +// int cnt = 0; + +// std::queue q; +// for(int i=0; inum_inputs; i++) { +// int input = aiger_lit2var(aiger->inputs[i].lit); +// topo_index[input] = ++cnt; +// q.push(input); +// } + +// while(!q.empty()) { +// int cur = q.front(); +// q.pop(); +// for(auto& edge : graph.edge[cur]) { +// int v = edge.to; +// topo_counter[v]++; +// if(topo_counter[v] == 2) { +// q.push(v); +// topo_index[v] = ++cnt; +// } +// } +// } +// } + + +bool check_left_graph(aiger* aiger, std::map &new_inputs, std::vector> &clauses) { + std::queue q; + static int* used = new int[aiger->maxvar + 1]; + memset(used, 0, (aiger->maxvar + 1) * sizeof(int)); + + solver = ipasir_init(); + + for(auto& pair : new_inputs) { + q.push(pair.first); + used[pair.first] = true; + } + + while(!q.empty()) { + int u = q.front(); + q.pop(); + + if(graph.redge[u].size() < 2) { + continue; + } + + int a = graph.redge[u][0].to; + int b = graph.redge[u][1].to; + + if(graph.redge[u][0].neg) a = -a; + if(graph.redge[u][1].neg) b = -b; + + ipasir_add(solver, -u); + ipasir_add(solver, a); + ipasir_add(solver, 0); + + ipasir_add(solver, -u); + ipasir_add(solver, b); + ipasir_add(solver, 0); + + ipasir_add(solver, -a); + ipasir_add(solver, -b); + ipasir_add(solver, u); + ipasir_add(solver, 0); + + a = abs(a); + b = abs(b); + + if(!used[a]) { + q.push(a); + used[a] = true; + } + + if(!used[b]) { + q.push(b); + used[b] = true; + } + } + + for(auto& pair : eqs) { + int a = pair.first; + int b = pair.second; + + ipasir_add(solver, -a); + ipasir_add(solver, b); + ipasir_add(solver, 0); + + ipasir_add(solver, a); + ipasir_add(solver, -b); + ipasir_add(solver, 0); + } + + for(auto& pair : new_inputs) { + ipasir_assume(solver, pair.second ? pair.first : -pair.first); + } + + int res = ipasir_solve(solver); + + std::vector failed_list; + + if(res == 20) { + for(auto& pair : new_inputs) { + int lit = pair.second ? pair.first : -pair.first; + if(ipasir_failed(solver, lit)) { + failed_list.push_back(-lit); + } + } + classes.push_back(failed_list); + + // printf("failed list: "); + // for(auto &v : failed_list) { + // printf("%d ", v); + // } + // printf("\n"); + } + + ipasir_release(solver); + + // printf("left result: %d\n", res); + + return true; +} + +bool check_right_graph(aiger* aiger, std::map &new_inputs, std::vector> &clauses) { + std::queue q; + static int* used = new int[aiger->maxvar + 1]; + memset(used, 0, (aiger->maxvar + 1) * sizeof(int)); + + solver = ipasir_init(); + + for(auto&vec : classes) { + for(auto &v : vec) { + ipasir_add(solver, v); + } + ipasir_add(solver, 0); + } + + int x = aiger_lit2var(aiger->outputs[0].lit); + + q.push(x); + used[x] = true; + + while(!q.empty()) { + int u = q.front(); + q.pop(); + + if(new_inputs.count(u)) { + continue; + } + + if(graph.redge[u].size() < 2) { + printf("ERROR point %d has fanin size %d\n", u << 1, graph.redge[u].size()); + exit(-1); + } + + int a = graph.redge[u][0].to; + int b = graph.redge[u][1].to; + + if(graph.redge[u][0].neg) a = -a; + if(graph.redge[u][1].neg) b = -b; + + ipasir_add(solver, -u); + ipasir_add(solver, a); + ipasir_add(solver, 0); + + ipasir_add(solver, -u); + ipasir_add(solver, b); + ipasir_add(solver, 0); + + ipasir_add(solver, -a); + ipasir_add(solver, -b); + ipasir_add(solver, u); + ipasir_add(solver, 0); + + a = abs(a); + b = abs(b); + + if(!used[a]) { + q.push(a); + used[a] = true; + } + + if(!used[b]) { + q.push(b); + used[b] = true; + } + } + + for(auto& pair : eqs) { + int a = pair.first; + int b = pair.second; + + ipasir_add(solver, -a); + ipasir_add(solver, b); + ipasir_add(solver, 0); + + ipasir_add(solver, a); + ipasir_add(solver, -b); + ipasir_add(solver, 0); + } + + if(aiger->outputs[0].lit & 1) { + ipasir_add(solver, -x); + ipasir_add(solver, 0); + } else { + ipasir_add(solver, x); + ipasir_add(solver, 0); + } + + int res = ipasir_solve(solver); + + if(res == 20) { + ipasir_release(solver); + return true; + } + else if(res == 10) { + for(auto& input : new_inputs) { + new_inputs[input.first] = ipasir_val(solver, input.first) >= 0 ? 1 : 0; + //printf("input[%d]=%d\n", input.first, ipasir_val(solver, input.first)); + } + ipasir_release(solver); + return false; + } else { + ipasir_release(solver); + printf("UNKOWN ERROR\n"); + exit(-1); + } +} + +void topo_cut(aiger* aiger, int cut_topo) { + printf("c trying cut by topo_index......\n"); + std::map new_inputs; + + printf("c Number of pairs detected: %d\n", pairs.size()); + + int pair_cnt = 0; + for(auto& pr : pairs) { + int a = pr.second.first; + int b = pr.second.second; + + if(pr.first > cut_topo + 2) break; + + printf("[%d/%d] check-eq %d %d (max-topo: %d)\n",++pair_cnt, pairs.size(), a, b, pr.first);//13148 + + if(check_var_equal(aiger, a, b)) { + printf("result is eq: %d %d\n", a, b); + int x = a & 1 ? -aiger_lit2var(a) : aiger_lit2var(a); + int y = b & 1 ? -aiger_lit2var(b) : aiger_lit2var(b); + eqs.push_back(std::make_pair(x, y)); + } + } + + for(int i=1; i<=aiger->maxvar; i++) { + if(topo_index[i] == cut_topo - 2) { + new_inputs[i] = -1; + } + } + + std::vector> clauses; + + while(!check_right_graph(aiger, new_inputs, clauses)) { + for(auto& pair : new_inputs) { + printf("%d ", pair.second); + } + printf("\n"); + + check_left_graph(aiger, new_inputs, clauses); + } + + printf("c cut points: %d\n", new_inputs.size()); + + //printf("c final: %d\n", check_right_graph(aiger, new_inputs)); + + return; +} \ No newline at end of file diff --git a/hKis/CONTRIBUTING b/hKis/CONTRIBUTING new file mode 100644 index 0000000..0750b19 --- /dev/null +++ b/hKis/CONTRIBUTING @@ -0,0 +1,4 @@ +At this point we want to keep complete ownership in one hand +to particularly avoid any additional co-authorship claims. +Thus please refrain from generating pull requests. Use the issue +tracker or send email to 'armin.biere@gmail.com' instead. diff --git a/hKis/LICENSE b/hKis/LICENSE new file mode 100644 index 0000000..469f5b2 --- /dev/null +++ b/hKis/LICENSE @@ -0,0 +1,19 @@ +Copyright (c) 2019-2020 Armin Biere, Johannes Kepler University Linz, Austria + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. diff --git a/hKis/README.md b/hKis/README.md new file mode 100644 index 0000000..cf96c18 --- /dev/null +++ b/hKis/README.md @@ -0,0 +1,13 @@ +[![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](https://opensource.org/licenses/MIT) +[![Build Status](https://travis-ci.com/arminbiere/kissat.svg?branch=master)](https://travis-ci.com/arminbiere/kissat) + +The Kissat SAT Solver +===================== + +Kissat is a "keep it simple and clean bare metal SAT solver" written in C. +It is a port of CaDiCaL back to C with improved data structures, better +scheduling of inprocessing and optimized algorithms and implementation. + +Coincidentally "kissat" also means "cats" in Finnish. + +Run `./configure && make test` to configure, build and test in `build`. diff --git a/hKis/VERSION b/hKis/VERSION new file mode 100644 index 0000000..21e8796 --- /dev/null +++ b/hKis/VERSION @@ -0,0 +1 @@ +1.0.3 diff --git a/hKis/bin/kissat b/hKis/bin/kissat new file mode 100755 index 0000000..f783a66 Binary files /dev/null and b/hKis/bin/kissat differ diff --git a/hKis/bin/starexec_run_psids b/hKis/bin/starexec_run_psids new file mode 100644 index 0000000..336f38c --- /dev/null +++ b/hKis/bin/starexec_run_psids @@ -0,0 +1,2 @@ +#!/bin/sh +exec ./kissat --unsat --psids=true $1 $2/proof.out diff --git a/hKis/bin/starexec_run_sat b/hKis/bin/starexec_run_sat new file mode 100644 index 0000000..787d784 --- /dev/null +++ b/hKis/bin/starexec_run_sat @@ -0,0 +1,2 @@ +#!/bin/sh +exec ./kissat --sat --walkinitially=true $1 $2/proof.out diff --git a/hKis/bin/starexec_run_unsat b/hKis/bin/starexec_run_unsat new file mode 100644 index 0000000..cf034aa --- /dev/null +++ b/hKis/bin/starexec_run_unsat @@ -0,0 +1,2 @@ +#!/bin/sh +exec ./kissat --target=1 --walkinitially=true --chrono=true $1 $2/proof.out diff --git a/hKis/build/allocate.o b/hKis/build/allocate.o new file mode 100644 index 0000000..0e7aa6e Binary files /dev/null and b/hKis/build/allocate.o differ diff --git a/hKis/build/analyze.o b/hKis/build/analyze.o new file mode 100644 index 0000000..9243ca5 Binary files /dev/null and b/hKis/build/analyze.o differ diff --git a/hKis/build/ands.o b/hKis/build/ands.o new file mode 100644 index 0000000..bf2ccbb Binary files /dev/null and b/hKis/build/ands.o differ diff --git a/hKis/build/application.o b/hKis/build/application.o new file mode 100644 index 0000000..4b4809b Binary files /dev/null and b/hKis/build/application.o differ diff --git a/hKis/build/arena.o b/hKis/build/arena.o new file mode 100644 index 0000000..285cca7 Binary files /dev/null and b/hKis/build/arena.o differ diff --git a/hKis/build/assign.o b/hKis/build/assign.o new file mode 100644 index 0000000..b9cba51 Binary files /dev/null and b/hKis/build/assign.o differ diff --git a/hKis/build/autarky.o b/hKis/build/autarky.o new file mode 100644 index 0000000..dc42ab4 Binary files /dev/null and b/hKis/build/autarky.o differ diff --git a/hKis/build/averages.o b/hKis/build/averages.o new file mode 100644 index 0000000..740f282 Binary files /dev/null and b/hKis/build/averages.o differ diff --git a/hKis/build/backtrack.o b/hKis/build/backtrack.o new file mode 100644 index 0000000..ffde918 Binary files /dev/null and b/hKis/build/backtrack.o differ diff --git a/hKis/build/backward.o b/hKis/build/backward.o new file mode 100644 index 0000000..d612f7c Binary files /dev/null and b/hKis/build/backward.o differ diff --git a/hKis/build/build.h b/hKis/build/build.h new file mode 100644 index 0000000..0e3a334 --- /dev/null +++ b/hKis/build/build.h @@ -0,0 +1,5 @@ +#define VERSION "1.0.3" +#define COMPILER "gcc (Ubuntu 9.4.0-1ubuntu1~20.04.1) 9.4.0 -W -Wall -O3 -DCOMPACT -DNEMBEDDED -DNDEBUG -DNMETRICS -DQUIET -DNSTATISTICS" +#define ID "unknown" +#define BUILD "Tue Sep 13 15:13:37 CST 2022 Linux seed1 5.4.0-120-generic x86_64" +#define DIR "/home/chenzh/experiments/cec/equal/hKis/build" diff --git a/hKis/build/build.o b/hKis/build/build.o new file mode 100644 index 0000000..808425b Binary files /dev/null and b/hKis/build/build.o differ diff --git a/hKis/build/bump.o b/hKis/build/bump.o new file mode 100644 index 0000000..f23e1ca Binary files /dev/null and b/hKis/build/bump.o differ diff --git a/hKis/build/check.o b/hKis/build/check.o new file mode 100644 index 0000000..31043aa Binary files /dev/null and b/hKis/build/check.o differ diff --git a/hKis/build/clause.o b/hKis/build/clause.o new file mode 100644 index 0000000..2dba1d5 Binary files /dev/null and b/hKis/build/clause.o differ diff --git a/hKis/build/clueue.o b/hKis/build/clueue.o new file mode 100644 index 0000000..fa2083d Binary files /dev/null and b/hKis/build/clueue.o differ diff --git a/hKis/build/collect.o b/hKis/build/collect.o new file mode 100644 index 0000000..22afd63 Binary files /dev/null and b/hKis/build/collect.o differ diff --git a/hKis/build/colors.o b/hKis/build/colors.o new file mode 100644 index 0000000..97d0c4b Binary files /dev/null and b/hKis/build/colors.o differ diff --git a/hKis/build/compact.o b/hKis/build/compact.o new file mode 100644 index 0000000..3fdf8c0 Binary files /dev/null and b/hKis/build/compact.o differ diff --git a/hKis/build/config.o b/hKis/build/config.o new file mode 100644 index 0000000..18368bc Binary files /dev/null and b/hKis/build/config.o differ diff --git a/hKis/build/decide.o b/hKis/build/decide.o new file mode 100644 index 0000000..fec8f70 Binary files /dev/null and b/hKis/build/decide.o differ diff --git a/hKis/build/deduce.o b/hKis/build/deduce.o new file mode 100644 index 0000000..7117916 Binary files /dev/null and b/hKis/build/deduce.o differ diff --git a/hKis/build/dense.o b/hKis/build/dense.o new file mode 100644 index 0000000..881bf35 Binary files /dev/null and b/hKis/build/dense.o differ diff --git a/hKis/build/dominate.o b/hKis/build/dominate.o new file mode 100644 index 0000000..6cc1afb Binary files /dev/null and b/hKis/build/dominate.o differ diff --git a/hKis/build/dump.o b/hKis/build/dump.o new file mode 100644 index 0000000..b9d4c41 Binary files /dev/null and b/hKis/build/dump.o differ diff --git a/hKis/build/eliminate.o b/hKis/build/eliminate.o new file mode 100644 index 0000000..1a49a52 Binary files /dev/null and b/hKis/build/eliminate.o differ diff --git a/hKis/build/equivalences.o b/hKis/build/equivalences.o new file mode 100644 index 0000000..822603b Binary files /dev/null and b/hKis/build/equivalences.o differ diff --git a/hKis/build/error.o b/hKis/build/error.o new file mode 100644 index 0000000..21fdf0c Binary files /dev/null and b/hKis/build/error.o differ diff --git a/hKis/build/extend.o b/hKis/build/extend.o new file mode 100644 index 0000000..54fa98b Binary files /dev/null and b/hKis/build/extend.o differ diff --git a/hKis/build/failed.o b/hKis/build/failed.o new file mode 100644 index 0000000..d90be08 Binary files /dev/null and b/hKis/build/failed.o differ diff --git a/hKis/build/file.o b/hKis/build/file.o new file mode 100644 index 0000000..a2a99bb Binary files /dev/null and b/hKis/build/file.o differ diff --git a/hKis/build/flags.o b/hKis/build/flags.o new file mode 100644 index 0000000..268ea3c Binary files /dev/null and b/hKis/build/flags.o differ diff --git a/hKis/build/format.o b/hKis/build/format.o new file mode 100644 index 0000000..2559e4a Binary files /dev/null and b/hKis/build/format.o differ diff --git a/hKis/build/forward.o b/hKis/build/forward.o new file mode 100644 index 0000000..fa85764 Binary files /dev/null and b/hKis/build/forward.o differ diff --git a/hKis/build/frames.o b/hKis/build/frames.o new file mode 100644 index 0000000..5d1f3ed Binary files /dev/null and b/hKis/build/frames.o differ diff --git a/hKis/build/gates.o b/hKis/build/gates.o new file mode 100644 index 0000000..0e0ea93 Binary files /dev/null and b/hKis/build/gates.o differ diff --git a/hKis/build/handle.o b/hKis/build/handle.o new file mode 100644 index 0000000..1d8737e Binary files /dev/null and b/hKis/build/handle.o differ diff --git a/hKis/build/heap.o b/hKis/build/heap.o new file mode 100644 index 0000000..c4b837e Binary files /dev/null and b/hKis/build/heap.o differ diff --git a/hKis/build/ifthenelse.o b/hKis/build/ifthenelse.o new file mode 100644 index 0000000..0b21f3c Binary files /dev/null and b/hKis/build/ifthenelse.o differ diff --git a/hKis/build/import.o b/hKis/build/import.o new file mode 100644 index 0000000..db72aad Binary files /dev/null and b/hKis/build/import.o differ diff --git a/hKis/build/internal.o b/hKis/build/internal.o new file mode 100644 index 0000000..986784e Binary files /dev/null and b/hKis/build/internal.o differ diff --git a/hKis/build/kissat b/hKis/build/kissat new file mode 100755 index 0000000..f783a66 Binary files /dev/null and b/hKis/build/kissat differ diff --git a/hKis/build/learn.o b/hKis/build/learn.o new file mode 100644 index 0000000..a9fa2a5 Binary files /dev/null and b/hKis/build/learn.o differ diff --git a/hKis/build/libkissat.a b/hKis/build/libkissat.a new file mode 100644 index 0000000..6acccb6 Binary files /dev/null and b/hKis/build/libkissat.a differ diff --git a/hKis/build/limits.o b/hKis/build/limits.o new file mode 100644 index 0000000..36d9e9f Binary files /dev/null and b/hKis/build/limits.o differ diff --git a/hKis/build/logging.o b/hKis/build/logging.o new file mode 100644 index 0000000..ee5d04c Binary files /dev/null and b/hKis/build/logging.o differ diff --git a/hKis/build/main.o b/hKis/build/main.o new file mode 100644 index 0000000..57dc28c Binary files /dev/null and b/hKis/build/main.o differ diff --git a/hKis/build/makefile b/hKis/build/makefile new file mode 100644 index 0000000..f75ca75 --- /dev/null +++ b/hKis/build/makefile @@ -0,0 +1,69 @@ +CC=gcc +CFLAGS=-W -Wall -O3 -DCOMPACT -DNEMBEDDED -DNDEBUG -DNMETRICS -DQUIET -DNSTATISTICS +LD=gcc +AR=ar + +VPATH=../src:../test + +%.o: %.c ../[st]*/*.h makefile + $(CC) $(CFLAGS) -c $< + +APPSRC=application.c handle.c parse.c witness.c + +LIBSRT=$(sort $(wildcard ../src/*.c)) +LIBSUB=$(subst ../src/,,$(LIBSRT)) +LIBSRC=$(filter-out main.c,$(LIBSUB)) + +TSTSRT=$(sort $(wildcard ../test/*.c)) +TSTSUB=$(subst ../test/,,$(TSTSRT)) +TSTSRC=$(filter-out test.c,$(TSTSUB)) + +APPOBJ=$(APPSRC:.c=.o) +LIBOBJ=$(LIBSRC:.c=.o) +TSTOBJ=$(APPOBJ) $(TSTSRC:.c=.o) + +INCLUDES=-I../$(shell pwd|sed -e 's,.*/,,') + +all: libkissat.a kissat +test: all tissat + ./tissat + +REMOVE=*.gcda *.gcno *.gcov gmon.out *~ *.proof + +clean: + rm -f kissat tissat + rm -f makefile build.h *.o *.a + rm -f $(REMOVE) + cd ../src; rm -f $(REMOVE) + cd ../test; rm -f $(REMOVE) + +coverage: + @gcov -o . -s ../src/*.[ch] 2>&1 | \ + ../scripts/filter-coverage-output.sh +indent: + indent ../*/*.[ch] + +kissat: main.o $(APPOBJ) libkissat.a makefile + $(LD) -o $@ $< $(APPOBJ) -L. -lkissat -lm + +tissat: test.o $(TSTOBJ) libkissat.a makefile + $(LD) -o $@ $< $(TSTOBJ) -L. -lkissat -lm + +build.h: + ../scripts/generate-build-header.sh > $@ + +collect.o: sort.c +dense.o: sort.c +propagate.o: assign.c +watch.o: sort.c + +build.o: build.c build.h ../[st]*/*.h makefile + $(CC) $(CFLAGS) $(INCLUDES) -c $< + +test.o: test.c build.h ../[st]*/*.h makefile + $(CC) $(CFLAGS) $(INCLUDES) -c $< + +libkissat.a: $(LIBOBJ) makefile + $(AR) rc $@ $(LIBOBJ) + +.PHONY: all clean coverage indent test build.h diff --git a/hKis/build/minimize.o b/hKis/build/minimize.o new file mode 100644 index 0000000..b7baa5f Binary files /dev/null and b/hKis/build/minimize.o differ diff --git a/hKis/build/mode.o b/hKis/build/mode.o new file mode 100644 index 0000000..38f8d93 Binary files /dev/null and b/hKis/build/mode.o differ diff --git a/hKis/build/options.o b/hKis/build/options.o new file mode 100644 index 0000000..aa79d97 Binary files /dev/null and b/hKis/build/options.o differ diff --git a/hKis/build/parse.o b/hKis/build/parse.o new file mode 100644 index 0000000..7f90128 Binary files /dev/null and b/hKis/build/parse.o differ diff --git a/hKis/build/phases.o b/hKis/build/phases.o new file mode 100644 index 0000000..11bb675 Binary files /dev/null and b/hKis/build/phases.o differ diff --git a/hKis/build/print.o b/hKis/build/print.o new file mode 100644 index 0000000..a174c47 Binary files /dev/null and b/hKis/build/print.o differ diff --git a/hKis/build/probe.o b/hKis/build/probe.o new file mode 100644 index 0000000..008c7a9 Binary files /dev/null and b/hKis/build/probe.o differ diff --git a/hKis/build/profile.o b/hKis/build/profile.o new file mode 100644 index 0000000..270fb36 Binary files /dev/null and b/hKis/build/profile.o differ diff --git a/hKis/build/promote.o b/hKis/build/promote.o new file mode 100644 index 0000000..1935830 Binary files /dev/null and b/hKis/build/promote.o differ diff --git a/hKis/build/proof.o b/hKis/build/proof.o new file mode 100644 index 0000000..99c6de5 Binary files /dev/null and b/hKis/build/proof.o differ diff --git a/hKis/build/propdense.o b/hKis/build/propdense.o new file mode 100644 index 0000000..d81178c Binary files /dev/null and b/hKis/build/propdense.o differ diff --git a/hKis/build/prophyper.o b/hKis/build/prophyper.o new file mode 100644 index 0000000..f580c3c Binary files /dev/null and b/hKis/build/prophyper.o differ diff --git a/hKis/build/proprobe.o b/hKis/build/proprobe.o new file mode 100644 index 0000000..c7ae8e5 Binary files /dev/null and b/hKis/build/proprobe.o differ diff --git a/hKis/build/propsearch.o b/hKis/build/propsearch.o new file mode 100644 index 0000000..b1e9a88 Binary files /dev/null and b/hKis/build/propsearch.o differ diff --git a/hKis/build/queue.o b/hKis/build/queue.o new file mode 100644 index 0000000..2f7209f Binary files /dev/null and b/hKis/build/queue.o differ diff --git a/hKis/build/reduce.o b/hKis/build/reduce.o new file mode 100644 index 0000000..7a20d68 Binary files /dev/null and b/hKis/build/reduce.o differ diff --git a/hKis/build/reluctant.o b/hKis/build/reluctant.o new file mode 100644 index 0000000..dd33ba7 Binary files /dev/null and b/hKis/build/reluctant.o differ diff --git a/hKis/build/rephase.o b/hKis/build/rephase.o new file mode 100644 index 0000000..5232a28 Binary files /dev/null and b/hKis/build/rephase.o differ diff --git a/hKis/build/report.o b/hKis/build/report.o new file mode 100644 index 0000000..126167a Binary files /dev/null and b/hKis/build/report.o differ diff --git a/hKis/build/resize.o b/hKis/build/resize.o new file mode 100644 index 0000000..0ecda72 Binary files /dev/null and b/hKis/build/resize.o differ diff --git a/hKis/build/resolve.o b/hKis/build/resolve.o new file mode 100644 index 0000000..66ead20 Binary files /dev/null and b/hKis/build/resolve.o differ diff --git a/hKis/build/resources.o b/hKis/build/resources.o new file mode 100644 index 0000000..71c9c0a Binary files /dev/null and b/hKis/build/resources.o differ diff --git a/hKis/build/restart.o b/hKis/build/restart.o new file mode 100644 index 0000000..a2b4fba Binary files /dev/null and b/hKis/build/restart.o differ diff --git a/hKis/build/search.o b/hKis/build/search.o new file mode 100644 index 0000000..94dc3c6 Binary files /dev/null and b/hKis/build/search.o differ diff --git a/hKis/build/smooth.o b/hKis/build/smooth.o new file mode 100644 index 0000000..ca01c96 Binary files /dev/null and b/hKis/build/smooth.o differ diff --git a/hKis/build/sort.o b/hKis/build/sort.o new file mode 100644 index 0000000..ef72e27 Binary files /dev/null and b/hKis/build/sort.o differ diff --git a/hKis/build/stack.o b/hKis/build/stack.o new file mode 100644 index 0000000..0a11364 Binary files /dev/null and b/hKis/build/stack.o differ diff --git a/hKis/build/statistics.o b/hKis/build/statistics.o new file mode 100644 index 0000000..f4e6b5d Binary files /dev/null and b/hKis/build/statistics.o differ diff --git a/hKis/build/strengthen.o b/hKis/build/strengthen.o new file mode 100644 index 0000000..203025c Binary files /dev/null and b/hKis/build/strengthen.o differ diff --git a/hKis/build/substitute.o b/hKis/build/substitute.o new file mode 100644 index 0000000..59fa7e1 Binary files /dev/null and b/hKis/build/substitute.o differ diff --git a/hKis/build/terminate.o b/hKis/build/terminate.o new file mode 100644 index 0000000..b707ce7 Binary files /dev/null and b/hKis/build/terminate.o differ diff --git a/hKis/build/ternary.o b/hKis/build/ternary.o new file mode 100644 index 0000000..27ba578 Binary files /dev/null and b/hKis/build/ternary.o differ diff --git a/hKis/build/trail.o b/hKis/build/trail.o new file mode 100644 index 0000000..2193bec Binary files /dev/null and b/hKis/build/trail.o differ diff --git a/hKis/build/transitive.o b/hKis/build/transitive.o new file mode 100644 index 0000000..4453eb2 Binary files /dev/null and b/hKis/build/transitive.o differ diff --git a/hKis/build/utilities.o b/hKis/build/utilities.o new file mode 100644 index 0000000..5e44c1f Binary files /dev/null and b/hKis/build/utilities.o differ diff --git a/hKis/build/vector.o b/hKis/build/vector.o new file mode 100644 index 0000000..b49aaff Binary files /dev/null and b/hKis/build/vector.o differ diff --git a/hKis/build/vivify.o b/hKis/build/vivify.o new file mode 100644 index 0000000..68f7dcc Binary files /dev/null and b/hKis/build/vivify.o differ diff --git a/hKis/build/walk.o b/hKis/build/walk.o new file mode 100644 index 0000000..ebd8911 Binary files /dev/null and b/hKis/build/walk.o differ diff --git a/hKis/build/watch.o b/hKis/build/watch.o new file mode 100644 index 0000000..a864365 Binary files /dev/null and b/hKis/build/watch.o differ diff --git a/hKis/build/weaken.o b/hKis/build/weaken.o new file mode 100644 index 0000000..ab4ef19 Binary files /dev/null and b/hKis/build/weaken.o differ diff --git a/hKis/build/witness.o b/hKis/build/witness.o new file mode 100644 index 0000000..e28cce5 Binary files /dev/null and b/hKis/build/witness.o differ diff --git a/hKis/build/xors.o b/hKis/build/xors.o new file mode 100644 index 0000000..725c6bf Binary files /dev/null and b/hKis/build/xors.o differ diff --git a/hKis/configure b/hKis/configure new file mode 100755 index 0000000..8b208eb --- /dev/null +++ b/hKis/configure @@ -0,0 +1,586 @@ +#!/bin/sh + +asan=no +check=unknown +check_all=no +check_heap=no +check_queue=no +check_vectors=no +compact=no +coverage=no +debug=no +default=no +extreme=no +embedded=unknown +logging=unknown +metrics=unknown +m32=no +options=yes +optimize=unknown +pedantic=unknown +profile=no +proofs=yes +quiet=no +sat=no +static=no +statistics=unknown +symbols=unknown +testdefault=unknown +ultimate=no +unsat=no + +passthrough="" + +usage () { +cat < ... ] + +where