init commit

.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"
+}

abc_result

@@ -0,0 +1,3 @@
+ABC command line: "source abc_script".
+
+Networks are equivalent.  Time =  1139.12 sec

abc_script

@@ -0,0 +1 @@
+&cec test0.aiger test1.aiger

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 <stdio.h>
+
+/*------------------------------------------------------------------------*/
+
+#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

bash.sh

@@ -0,0 +1,6 @@
+#/bin/bash
+cd /home/qianyh/experiments/cec/equal
+
+#ls
+
+#./abc/abc -f abc_script > abc_result

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(  )

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<int> q;
+//     for(int i=0; i<aiger->num_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<int, int> &new_inputs, std::vector<std::vector<int>> &clauses) {
+    std::queue<int> 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<int> 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<int, int> &new_inputs, std::vector<std::vector<int>> &clauses) {
+    std::queue<int> 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<int, int> 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<std::vector<int>> 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;
+}

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.

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.

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`.

hKis/VERSION

@@ -0,0 +1 @@
+1.0.3

hKis/bin/starexec_run_psids

@@ -0,0 +1,2 @@
+#!/bin/sh
+exec ./kissat --unsat --psids=true $1 $2/proof.out

hKis/bin/starexec_run_sat

@@ -0,0 +1,2 @@
+#!/bin/sh
+exec ./kissat --sat --walkinitially=true $1 $2/proof.out

hKis/bin/starexec_run_unsat

@@ -0,0 +1,2 @@
+#!/bin/sh
+exec ./kissat --target=1 --walkinitially=true --chrono=true $1 $2/proof.out

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"

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