From cac3967b52ae44fae3962ee9eba456221e0efda3 Mon Sep 17 00:00:00 2001
From: Bruno Schmitt <bruno@oschmitt.com>
Date: Mon, 6 Feb 2017 11:34:52 -0800
Subject: =?UTF-8?q?Adding=20a=20new=20SAT=20solver=20to=20ABC.=20(Satoko)?=
 =?UTF-8?q?=20The=20command=20is=20=E2=80=98satoko=E2=80=99?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/sat/satoko/clause.h | 63 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 63 insertions(+)
 create mode 100644 src/sat/satoko/clause.h

(limited to 'src/sat/satoko/clause.h')

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 */
-- 
cgit v1.2.3