diff options
author | Bruno Schmitt <bruno@oschmitt.com> | 2017-02-06 11:34:52 -0800 |
---|---|---|
committer | Bruno Schmitt <bruno@oschmitt.com> | 2017-02-06 11:34:52 -0800 |
commit | cac3967b52ae44fae3962ee9eba456221e0efda3 (patch) | |
tree | 47711960bec18836ec61ac30f1cd7dcd8d999483 /src/sat/satoko/clause.h | |
parent | aed9a87282bcb7937fd74e078d30ed74786abc75 (diff) | |
download | abc-cac3967b52ae44fae3962ee9eba456221e0efda3.tar.gz abc-cac3967b52ae44fae3962ee9eba456221e0efda3.tar.bz2 abc-cac3967b52ae44fae3962ee9eba456221e0efda3.zip |
Adding a new SAT solver to ABC. (Satoko)
The command is ‘satoko’
Diffstat (limited to 'src/sat/satoko/clause.h')
-rw-r--r-- | src/sat/satoko/clause.h | 63 |
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 */ |