Adding a new SAT solver to ABC. (Satoko)

The command is ‘satoko’

1 files changed, 63 insertions, 0 deletions

diff --git a/src/sat/satoko/clause.h b/src/sat/satoko/clause.h
new file mode 100644
index 00000000..2be18cd6
--- /dev/null
+++ b/src/sat/satoko/clause.h
@@ -0,0 +1,63 @@
+//===--- clause.h -----------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__clause_h
+#define satoko__clause_h
+
+#include "types.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+struct clause {
+    unsigned f_learnt    : 1;
+    unsigned f_mark      : 1;
+    unsigned f_reallocd  : 1;
+    unsigned f_deletable : 1;
+    unsigned lbd : 28;
+    unsigned size;
+    union {
+        unsigned lit;
+        clause_act_t act;
+    } data[0];
+};
+
+//===------------------------------------------------------------------------===
+// Clause API
+//===------------------------------------------------------------------------===
+static inline int clause_compare(const void *p1, const void *p2)
+{
+    const struct clause *c1 = (const struct clause *)p1;
+    const struct clause *c2 = (const struct clause *)p2;
+
+    if (c1->size > 2 && c2->size == 2)
+        return 1;
+    if (c1->size == 2 && c2->size > 2)
+        return 0;
+    if (c1->size == 2 && c2->size == 2)
+        return 0;
+
+    if (c1->lbd > c2->lbd)
+        return 1;
+    if (c1->lbd < c2->lbd)
+        return 0;
+
+    return c1->data[c1->size].act < c2->data[c2->size].act;
+}
+
+static inline void clause_print(struct clause *clause)
+{
+    unsigned i;
+    printf("{ ");
+    for (i = 0; i < clause->size; i++)
+        printf("%u ", clause->data[i].lit);
+    printf("}\n");
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__clause_h */