summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorBruno Schmitt <bruno@oschmitt.com>2017-02-06 11:34:52 -0800
committerBruno Schmitt <bruno@oschmitt.com>2017-02-06 11:34:52 -0800
commitcac3967b52ae44fae3962ee9eba456221e0efda3 (patch)
tree47711960bec18836ec61ac30f1cd7dcd8d999483
parentaed9a87282bcb7937fd74e078d30ed74786abc75 (diff)
downloadabc-cac3967b52ae44fae3962ee9eba456221e0efda3.tar.gz
abc-cac3967b52ae44fae3962ee9eba456221e0efda3.tar.bz2
abc-cac3967b52ae44fae3962ee9eba456221e0efda3.zip
Adding a new SAT solver to ABC. (Satoko)
The command is ‘satoko’
-rw-r--r--Makefile2
-rw-r--r--src/base/abci/abc.c82
-rw-r--r--src/sat/satoko/LICENSE22
-rw-r--r--src/sat/satoko/act_clause.h80
-rw-r--r--src/sat/satoko/act_var.h84
-rw-r--r--src/sat/satoko/cdb.h100
-rw-r--r--src/sat/satoko/clause.h63
-rw-r--r--src/sat/satoko/cnf_reader.c156
-rw-r--r--src/sat/satoko/module.make3
-rw-r--r--src/sat/satoko/satoko.h85
-rw-r--r--src/sat/satoko/solver.c704
-rw-r--r--src/sat/satoko/solver.h242
-rw-r--r--src/sat/satoko/solver_api.c310
-rw-r--r--src/sat/satoko/types.h50
-rw-r--r--src/sat/satoko/utils/b_queue.h81
-rw-r--r--src/sat/satoko/utils/heap.h181
-rwxr-xr-xsrc/sat/satoko/utils/mem.h23
-rwxr-xr-xsrc/sat/satoko/utils/misc.h37
-rw-r--r--src/sat/satoko/utils/sort.h65
-rw-r--r--src/sat/satoko/utils/vec/vec_char.h259
-rwxr-xr-xsrc/sat/satoko/utils/vec/vec_dble.h246
-rwxr-xr-xsrc/sat/satoko/utils/vec/vec_int.h240
-rwxr-xr-xsrc/sat/satoko/utils/vec/vec_uint.h268
-rw-r--r--src/sat/satoko/watch_list.h152
24 files changed, 3533 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index d45978a9..4142e1b2 100644
--- a/Makefile
+++ b/Makefile
@@ -23,7 +23,7 @@ MODULES := \
src/opt/cut src/opt/fxu src/opt/fxch src/opt/rwr src/opt/mfs src/opt/sim \
src/opt/ret src/opt/fret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt \
src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/dsc src/opt/sfm src/opt/sbd \
- src/sat/bsat src/sat/xsat src/sat/csat src/sat/msat src/sat/psat src/sat/cnf src/sat/bmc \
+ src/sat/bsat src/sat/xsat src/sat/satoko src/sat/csat src/sat/msat src/sat/psat src/sat/cnf src/sat/bmc \
src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky \
src/bool/rsb src/bool/rpo \
src/proof/pdr src/proof/abs src/proof/live src/proof/ssc src/proof/int \
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 008adbae..efb82fcc 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -43,6 +43,7 @@
#include "map/amap/amap.h"
#include "opt/ret/retInt.h"
#include "sat/xsat/xsat.h"
+#include "sat/satoko/satoko.h"
#include "sat/cnf/cnf.h"
#include "proof/cec/cec.h"
#include "proof/acec/acec.h"
@@ -308,6 +309,7 @@ static int Abc_CommandDSec ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandSat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDSat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandXSat ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSatoko ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPSat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -956,6 +958,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Verification", "sat", Abc_CommandSat, 0 );
Cmd_CommandAdd( pAbc, "Verification", "dsat", Abc_CommandDSat, 0 );
Cmd_CommandAdd( pAbc, "Verification", "xsat", Abc_CommandXSat, 0 );
+ Cmd_CommandAdd( pAbc, "Verification", "satoko", Abc_CommandSatoko, 0 );
Cmd_CommandAdd( pAbc, "Verification", "psat", Abc_CommandPSat, 0 );
Cmd_CommandAdd( pAbc, "Verification", "prove", Abc_CommandProve, 1 );
Cmd_CommandAdd( pAbc, "Verification", "iprove", Abc_CommandIProve, 1 );
@@ -23313,6 +23316,83 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandSatoko( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ abctime clk;
+ int c;
+ satoko_opts_t opts;
+
+ satoko_default_opts(&opts);
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Chv" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ opts.conf_limit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( opts.conf_limit < 0 )
+ goto usage;
+ break;
+ case 'h':
+ goto usage;
+ case 'v':
+ opts.verbose ^= 1;
+ break;
+
+ default:
+ goto usage;
+ }
+ }
+
+ if ( argc == globalUtilOptind + 1 )
+ {
+ char * pFileName = argv[globalUtilOptind];
+ satoko_t * p;
+ int status;
+
+ satoko_parse_dimacs( pFileName, &p );
+ satoko_configure(p, &opts);
+
+ clk = Abc_Clock();
+ status = satoko_solve( p );
+
+ if ( status == SATOKO_UNDEC )
+ Abc_Print( 1, "UNDECIDED " );
+ else if ( status == SATOKO_SAT )
+ Abc_Print( 1, "SATISFIABLE " );
+ else
+ Abc_Print( 1, "UNSATISFIABLE " );
+
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+
+ satoko_destroy( p );
+ return 0;
+ }
+
+usage:
+ Abc_Print( -2, "usage: satoko [-CILDE num] [-hv]<file>.cnf\n" );
+ Abc_Print( -2, "\t-C num : limit on the number of conflicts [default = %d]\n", opts.conf_limit );
+ Abc_Print( -2, "\t-v : prints verbose information [default = %s]\n", opts.verbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandPSat( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
@@ -26238,7 +26318,7 @@ usage:
Abc_Print( -2, "\t Zyad Hassan, Aaron R. Bradley, Fabio Somenzi, \"Better Generalization in IC3\", FMCAD 2013.\n");
Abc_Print( -2, "\t (http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD13/papers/85-Better-Generalization-IC3.pdf)\n");
-
+
return 1;
}
diff --git a/src/sat/satoko/LICENSE b/src/sat/satoko/LICENSE
new file mode 100644
index 00000000..51938137
--- /dev/null
+++ b/src/sat/satoko/LICENSE
@@ -0,0 +1,22 @@
+Copyright 2017, Bruno Schmitt - UC Berkeley / UFRGS (bruno@oschmitt.com)
+
+Redistribution and use in source and binary forms, with or without modification,
+are permitted provided that the following conditions are met:
+
+1. Redistributions of source code must retain the above copyright notice, this
+ list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright notice,
+ this list of conditions and the following disclaimer in the documentation
+ and/or other materials provided with the distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
+ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/src/sat/satoko/act_clause.h b/src/sat/satoko/act_clause.h
new file mode 100644
index 00000000..5a2fda2b
--- /dev/null
+++ b/src/sat/satoko/act_clause.h
@@ -0,0 +1,80 @@
+//===--- act_var.h ----------------------------------------------------------===
+//
+// satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__act_clause_h
+#define satoko__act_clause_h
+
+#include "solver.h"
+#include "types.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+#ifdef SATOKO_ACT_CLAUSE_FLOAT
+
+/** Re-scale the activity value for all clauses.
+ */
+static inline void clause_act_rescale(solver_t *s)
+{
+ unsigned i, cref;
+ struct clause *clause;
+
+ vec_uint_foreach(s->learnts, cref, i) {
+ clause = clause_read(s, cref);
+ clause->data[clause->size].act *= 1e-20;
+ }
+ s->clause_act_inc *= 1e-20;
+}
+
+/** Increment the activity value of one clause ('clause')
+ */
+static inline void clause_act_bump(solver_t *s, struct clause *clause)
+{
+ clause->data[clause->size].act += s->clause_act_inc;
+ if (clause->data[clause->size].act > 1e20)
+ clause_act_rescale(s);
+}
+
+/** Increment the value by which clauses activity values are incremented
+ */
+static inline void clause_act_decay(solver_t *s)
+{
+ s->clause_act_inc *= (1 / s->opts.clause_decay);
+}
+
+#else /* SATOKO_ACT_CLAUSE_FLOAT */
+
+static inline void clause_act_rescale(solver_t *s)
+{
+ unsigned i, cref;
+ struct clause *clause;
+
+ vec_uint_foreach(s->learnts, cref, i) {
+ clause = clause_read(s, cref);
+ clause->data[clause->size].act >>= 14;
+ }
+ s->clause_act_inc >>= 14;
+ s->clause_act_inc = mkt_uint_max(s->clause_act_inc, (1 << 10));
+}
+
+static inline void clause_act_bump(solver_t *s, struct clause *clause)
+{
+ clause->data[clause->size].act += s->clause_act_inc;
+ if (clause->data[clause->size].act & 0x80000000)
+ clause_act_rescale(s);
+}
+
+static inline void clause_act_decay(solver_t *s)
+{
+ s->clause_act_inc += (s->clause_act_inc >> 10);
+}
+
+#endif /* SATOKO_ACT_CLAUSE_FLOAT */
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__act_clause_h */
diff --git a/src/sat/satoko/act_var.h b/src/sat/satoko/act_var.h
new file mode 100644
index 00000000..161e9d9a
--- /dev/null
+++ b/src/sat/satoko/act_var.h
@@ -0,0 +1,84 @@
+//===--- act_var.h ----------------------------------------------------------===
+//
+// satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__act_var_h
+#define satoko__act_var_h
+
+#include "solver.h"
+#include "types.h"
+#include "utils/heap.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+#ifdef SATOKO_ACT_VAR_DBLE
+/** Re-scale the activity value for all variables.
+ */
+static inline void var_act_rescale(solver_t *s)
+{
+ unsigned i;
+ double *activity = vec_dble_data(s->activity);
+
+ for (i = 0; i < vec_dble_size(s->activity); i++)
+ activity[i] *= 1e-100;
+ s->var_act_inc *= 1e-100;
+}
+
+/** Increment the activity value of one variable ('var')
+ */
+static inline void var_act_bump(solver_t *s, unsigned var)
+{
+ double *activity = vec_dble_data(s->activity);
+
+ activity[var] += s->var_act_inc;
+ if (activity[var] > 1e100)
+ var_act_rescale(s);
+ if (heap_in_heap(s->var_order, var))
+ heap_decrease(s->var_order, var);
+}
+
+/** Increment the value by which variables activity values are incremented
+ */
+static inline void var_act_decay(solver_t *s)
+{
+ s->var_act_inc *= (1 / s->opts.var_decay);
+}
+
+#else /* SATOKO_ACT_VAR_DBLE */
+
+static inline void var_act_rescale(solver_t *s)
+{
+ unsigned i;
+ unsigned *activity = vec_uint_data(s->activity);
+
+ for (i = 0; i < vec_uint_size(s->activity); i++)
+ activity[i] >>= 19;
+ s->var_act_inc >>= 19;
+ s->var_act_inc = mkt_uint_max(s->var_act_inc, (1 << 5));
+}
+
+static inline void var_act_bump(solver_t *s, unsigned var)
+{
+ unsigned *activity = vec_uint_data(s->activity);
+
+ activity[var] += s->var_act_inc;
+ if (activity[var] & 0x80000000)
+ var_act_rescale(s);
+ if (heap_in_heap(s->var_order, var))
+ heap_decrease(s->var_order, var);
+}
+
+static inline void var_act_decay(solver_t *s)
+{
+ s->var_act_inc += (s->var_act_inc >> 4);
+}
+
+#endif /* SATOKO_ACT_VAR_DBLE */
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__act_var_h */
diff --git a/src/sat/satoko/cdb.h b/src/sat/satoko/cdb.h
new file mode 100644
index 00000000..28686ff2
--- /dev/null
+++ b/src/sat/satoko/cdb.h
@@ -0,0 +1,100 @@
+//===--- cdb.h --------------------------------------------------------------===
+//
+// satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__cdb_h
+#define satoko__cdb_h
+
+#include "clause.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+/* Clauses DB data structure */
+struct cdb {
+ unsigned size;
+ unsigned cap;
+ unsigned wasted;
+ unsigned *data;
+};
+
+//===------------------------------------------------------------------------===
+// Clause DB API
+//===------------------------------------------------------------------------===
+static inline struct clause *cdb_handler(struct cdb *p, unsigned cref)
+{
+ return cref != 0xFFFFFFFF ? (struct clause *)(p->data + cref) : NULL;
+}
+
+static inline unsigned cdb_cref(struct cdb *p, unsigned *clause)
+{
+ return (unsigned)(clause - &(p->data[0]));
+}
+
+static inline void cdb_grow(struct cdb *p, unsigned cap)
+{
+ unsigned prev_cap = p->cap;
+
+ if (p->cap >= cap)
+ return;
+ while (p->cap < cap) {
+ unsigned delta = ((p->cap >> 1) + (p->cap >> 3) + 2) & (unsigned)(~1);
+ p->cap += delta;
+ assert(p->cap >= prev_cap);
+ }
+ assert(p->cap > 0);
+ p->data = satoko_realloc(unsigned, p->data, p->cap);
+}
+
+static inline struct cdb *cdb_alloc(unsigned cap)
+{
+ struct cdb *p = satoko_calloc(struct cdb, 1);
+ if (cap <= 0)
+ cap = 1024 * 1024;
+ cdb_grow(p, cap);
+ return p;
+}
+
+static inline void cdb_free(struct cdb *p)
+{
+ satoko_free(p->data);
+ satoko_free(p);
+}
+
+static inline unsigned cdb_append(struct cdb *p, unsigned size)
+{
+ unsigned prev_size;
+ assert(size > 0);
+ cdb_grow(p, p->size + size);
+ prev_size = p->size;
+ p->size += size;
+ assert(p->size > prev_size);
+ return prev_size;
+}
+
+static inline void cdb_remove(struct cdb *p, struct clause *clause)
+{
+ p->wasted += clause->size;
+}
+
+static inline unsigned cdb_capacity(struct cdb *p)
+{
+ return p->cap;
+}
+
+static inline unsigned cdb_size(struct cdb *p)
+{
+ return p->size;
+}
+
+static inline unsigned cdb_wasted(struct cdb *p)
+{
+ return p->wasted;
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__cdb_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 */
diff --git a/src/sat/satoko/cnf_reader.c b/src/sat/satoko/cnf_reader.c
new file mode 100644
index 00000000..5e4b92f9
--- /dev/null
+++ b/src/sat/satoko/cnf_reader.c
@@ -0,0 +1,156 @@
+//===--- cnf_reader.h -------------------------------------------------------===
+//
+// satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#include <assert.h>
+#include <ctype.h>
+#include <stdlib.h>
+#include <stdio.h>
+#include <string.h>
+
+#include "satoko.h"
+#include "solver.h"
+#include "utils/mem.h"
+#include "utils/vec/vec_uint.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_IMPL_START
+
+/** Read the file into an internal buffer.
+ *
+ * This function will receive a file name. The return data is a string ended
+ * with '\0'.
+ *
+ */
+static char * file_open(const char *fname)
+{
+ FILE *file = fopen(fname, "rb");
+ char *buffer;
+ int sz_file;
+ int ret;
+
+ if (file == NULL) {
+ printf("Couldn't open file: %s\n", fname);
+ return NULL;
+ }
+ fseek(file, 0, SEEK_END);
+ sz_file = ftell(file);
+ rewind(file);
+ buffer = satoko_alloc(char, sz_file + 3);
+ ret = fread(buffer, sz_file, 1, file);
+ buffer[sz_file + 0] = '\n';
+ buffer[sz_file + 1] = '\0';
+ return buffer;
+}
+
+static void skip_spaces(char **pos)
+{
+ assert(pos != NULL);
+ for (; isspace(**pos); (*pos)++);
+}
+
+static void skip_line(char **pos)
+{
+ assert(pos != NULL);
+ for(; **pos != '\n' && **pos != '\r' && **pos != EOF; (*pos)++);
+ if (**pos != EOF)
+ (*pos)++;
+ return;
+}
+
+static int read_int(char **token)
+{
+ int value = 0;
+ int neg = 0;
+
+ skip_spaces(token);
+ if (**token == '-') {
+ neg = 1;
+ (*token)++;
+ } else if (**token == '+')
+ (*token)++;
+
+ if (!isdigit(**token)) {
+ printf("Parsing error. Unexpected char: %c.\n", **token);
+ exit(EXIT_FAILURE);
+ }
+ while (isdigit(**token)) {
+ value = (value * 10) + (**token - '0');
+ (*token)++;
+ }
+ return neg ? -value : value;
+}
+
+static void read_clause(char **token, vec_uint_t *lits)
+{
+ int var;
+ unsigned sign;
+
+ vec_uint_clear(lits);
+ while (1) {
+ var = read_int(token);
+ if (var == 0)
+ break;
+ sign = (var > 0);
+ var = abs(var) - 1;
+ vec_uint_push_back(lits, var2lit((unsigned) var, !sign));
+ }
+}
+
+/** Start the solver and reads the DIMAC file.
+ *
+ * Returns false upon immediate conflict.
+ */
+int satoko_parse_dimacs(char *fname, satoko_t **solver)
+{
+ satoko_t *p = NULL;
+ vec_uint_t *lits = NULL;
+ int n_var;
+ int n_clause;
+ char *buffer = file_open(fname);
+ char *token;
+
+ if (buffer == NULL)
+ return -1;
+
+ token = buffer;
+ while (1) {
+ skip_spaces(&token);
+ if (*token == 0)
+ break;
+ else if (*token == 'c')
+ skip_line(&token);
+ else if (*token == 'p') {
+ token++;
+ skip_spaces(&token);
+ for(; !isspace(*token); token++); /* skip 'cnf' */
+
+ n_var = read_int(&token);
+ n_clause = read_int(&token);
+ skip_line(&token);
+ lits = vec_uint_alloc((unsigned) n_var);
+ p = satoko_create();
+ } else {
+ if (lits == NULL) {
+ printf("There is no parameter line.\n");
+ satoko_free(buffer);
+ return -1;
+ }
+ read_clause(&token, lits);
+ if (!satoko_add_clause(p, vec_uint_data(lits), vec_uint_size(lits))) {
+ vec_uint_print(lits);
+ return 0;
+ }
+ }
+ }
+ vec_uint_free(lits);
+ satoko_free(buffer);
+ *solver = p;
+ return satoko_simplify(p);
+}
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/sat/satoko/module.make b/src/sat/satoko/module.make
new file mode 100644
index 00000000..512094ee
--- /dev/null
+++ b/src/sat/satoko/module.make
@@ -0,0 +1,3 @@
+SRC += src/sat/satoko/solver.c \
+ src/sat/satoko/solver_api.c \
+ src/sat/satoko/cnf_reader.c
diff --git a/src/sat/satoko/satoko.h b/src/sat/satoko/satoko.h
new file mode 100644
index 00000000..49c7837e
--- /dev/null
+++ b/src/sat/satoko/satoko.h
@@ -0,0 +1,85 @@
+//===--- satoko.h -----------------------------------------------------------===
+//
+// satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__satoko_h
+#define satoko__satoko_h
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+/** Return valeus */
+enum {
+ SATOKO_ERR = 0,
+ SATOKO_OK = 1
+};
+
+enum {
+ SATOKO_UNDEC = 0, /* Undecided */
+ SATOKO_SAT = 1,
+ SATOKO_UNSAT = -1
+};
+
+struct solver_t_;
+typedef struct solver_t_ satoko_t;
+
+typedef struct satoko_opts satoko_opts_t;
+struct satoko_opts {
+ /* Limits */
+ long long conf_limit; /* Limit on the n.of conflicts */
+ long long prop_limit; /* Limit on the n.of implications */
+
+ /* Constants used for restart heuristic */
+ double f_rst; /* Used to force a restart */
+ double b_rst; /* Used to block a restart */
+ unsigned fst_block_rst; /* Lower bound n.of conflicts for start blocking restarts */
+ unsigned sz_lbd_bqueue; /* Size of the moving avarege queue for LBD (force restart) */
+ unsigned sz_trail_bqueue; /* Size of the moving avarege queue for Trail size (block restart) */
+
+ /* Constants used for clause database reduction heuristic */
+ unsigned n_conf_fst_reduce; /* N.of conflicts before first reduction */
+ unsigned inc_reduce; /* Increment to reduce */
+ unsigned inc_special_reduce; /* Special increment to reduce */
+ unsigned lbd_freeze_clause;
+
+ /* VSIDS heuristic */
+ float clause_decay;
+ double var_decay;
+
+ /* Binary resolution */
+ unsigned clause_max_sz_bin_resol;
+ unsigned clause_min_lbd_bin_resol;
+ float garbage_max_ratio;
+ char verbose;
+};
+
+//===------------------------------------------------------------------------===
+extern satoko_t *satoko_create(void);
+extern void satoko_destroy(satoko_t *);
+extern void satoko_default_opts(satoko_opts_t *);
+extern void satoko_configure(satoko_t *, satoko_opts_t *);
+extern int satoko_parse_dimacs(char *, satoko_t **);
+extern void satoko_add_variable(satoko_t *, char);
+extern int satoko_add_clause(satoko_t *, unsigned *, unsigned);
+extern void satoko_assump_push(satoko_t *s, unsigned);
+extern void satoko_assump_pop(satoko_t *s);
+extern int satoko_simplify(satoko_t *);
+extern int satoko_solve(satoko_t *);
+
+/* If problem is unsatisfiable under assumptions, this function is used to
+ * obtain the final conflict clause expressed in the assumptions.
+ *
+ * - It receives as inputs the solver and a pointer to a array where clause
+ * will be copied. The memory is allocated by the solver, but must be freed by
+ * the caller.
+ * - The return value is either the size of the array or -1 in case the final
+ * conflict cluase was not generated.
+ */
+extern int satoko_final_conflict(satoko_t *, unsigned *);
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__satoko_h */
diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c
new file mode 100644
index 00000000..b2861bad
--- /dev/null
+++ b/src/sat/satoko/solver.c
@@ -0,0 +1,704 @@
+//===--- solver.c -----------------------------------------------------------===
+//
+// satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#include <stdio.h>
+#include <assert.h>
+#include <string.h>
+#include <math.h>
+
+#include "act_clause.h"
+#include "act_var.h"
+#include "solver.h"
+#include "utils/heap.h"
+#include "utils/mem.h"
+#include "utils/sort.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_IMPL_START
+
+//===------------------------------------------------------------------------===
+// Lit funtions
+//===------------------------------------------------------------------------===
+/**
+ * A literal is said to be redundant in a given clause if and only if all
+ * variables in its reason are either present in that clause or (recursevely)
+ * redundant.
+ */
+static inline int lit_is_removable(solver_t* s, unsigned lit, unsigned min_level)
+{
+ unsigned top = vec_uint_size(s->tagged);
+
+ assert(lit_reason(s, lit) != UNDEF);
+ vec_uint_clear(s->stack);
+ vec_uint_push_back(s->stack, lit2var(lit));
+ while (vec_uint_size(s->stack)) {
+ unsigned i;
+ unsigned var = vec_uint_pop_back(s->stack);
+ struct clause *c = clause_read(s, var_reason(s, var));
+ unsigned *lits = &(c->data[0].lit);
+
+ assert(var_reason(s, var) != UNDEF);
+ if (c->size == 2 && lit_value(s, lits[0]) == LIT_FALSE) {
+ assert(lit_value(s, lits[1]) == LIT_TRUE);
+ mkt_swap(unsigned, lits[0], lits[1]);
+ }
+
+ /* Check scan the literals of the reason clause.
+ * The first literal is skiped because is the literal itself. */
+ for (i = 1; i < c->size; i++) {
+ var = lit2var(lits[i]);
+
+ /* Check if the variable has already been seen or if it
+ * was assinged a value at the decision level 0. In a
+ * positive case, there is no need to look any further */
+ if (vec_char_at(s->seen, var) || var_dlevel(s, var) == 0)
+ continue;
+
+ /* If the variable has a reason clause and if it was
+ * assingned at a 'possible' level, then we need to
+ * check if it is recursively redundant, otherwise the
+ * literal being checked is not redundant */
+ if (var_reason(s, var) != UNDEF && ((1 << (var_dlevel(s, var) & 31)) & min_level)) {
+ vec_uint_push_back(s->stack, var);
+ vec_uint_push_back(s->tagged, var);
+ vec_char_assign(s->seen, var, 1);
+ } else {
+ vec_uint_foreach_start(s->tagged, var, i, top)
+ vec_char_assign(s->seen, var, 0);
+ vec_uint_shrink(s->tagged, top);
+ return 0;
+ }
+ }
+ }
+ return 1;
+}
+
+//===------------------------------------------------------------------------===
+// Clause functions
+//===------------------------------------------------------------------------===
+/* Calculate clause LBD (Literal Block Distance):
+ * - It's the number of variables in the final conflict clause that come from
+ * different decision levels
+ */
+static inline unsigned clause_clac_lbd(solver_t *s, unsigned *lits, unsigned size)
+{
+ unsigned i;
+ unsigned lbd = 0;
+
+ s->cur_stamp++;
+ for (i = 0; i < size; i++) {
+ unsigned level = lit_dlevel(s, lits[i]);
+ if (vec_uint_at(s->stamps, level) != s->cur_stamp) {
+ vec_uint_assign(s->stamps, level, s->cur_stamp);
+ lbd++;
+ }
+ }
+ return lbd;
+}
+
+static inline void clause_bin_resolution(solver_t *s, vec_uint_t *clause_lits)
+{
+ unsigned *lits = vec_uint_data(clause_lits);
+ unsigned counter, sz, i;
+ unsigned lit;
+ unsigned neg_lit = lit_neg(lits[0]);
+ struct watcher *w;
+
+ s->cur_stamp++;
+ vec_uint_foreach(clause_lits, lit, i)
+ vec_uint_assign(s->stamps, lit2var(lit), s->cur_stamp);
+
+ counter = 0;
+ watch_list_foreach(s->bin_watches, w, neg_lit) {
+ unsigned imp_lit = w->blocker;
+ if (vec_uint_at(s->stamps, lit2var(imp_lit)) == s->cur_stamp &&
+ lit_value(s, imp_lit) == LIT_TRUE) {
+ counter++;
+ vec_uint_assign(s->stamps, lit2var(imp_lit), (s->cur_stamp - 1));
+ }
+ }
+ if (counter > 0) {
+ sz = vec_uint_size(clause_lits) - 1;
+ for (i = 1; i < vec_uint_size(clause_lits) - counter; i++)
+ if (vec_uint_at(s->stamps, lit2var(lits[i])) != s->cur_stamp) {
+ mkt_swap(unsigned, lits[i], lits[sz]);
+ i--;
+ sz--;
+ }
+ vec_uint_shrink(clause_lits, vec_uint_size(clause_lits) - counter);
+ }
+}
+
+static inline void clause_minimize(solver_t *s, vec_uint_t *clause_lits)
+{
+ unsigned i, j;
+ unsigned *lits = vec_uint_data(clause_lits);
+ unsigned min_level = 0;
+ unsigned clause_size;
+
+ for (i = 1; i < vec_uint_size(clause_lits); i++) {
+ unsigned level = lit_dlevel(s, lits[i]);
+ min_level |= 1 << (level & 31);
+ }
+
+ /* Remove reduntant literals */
+ vec_uint_foreach(clause_lits, i, j)
+ vec_uint_push_back(s->tagged, lit2var(i));
+ for (i = j = 1; i < vec_uint_size(clause_lits); i++)
+ if (lit_reason(s, lits[i]) == UNDEF || !lit_is_removable(s, lits[i], min_level))
+ lits[j++] = lits[i];
+ vec_uint_shrink(clause_lits, j);
+
+ /* Binary Resolution */
+ clause_size = vec_uint_size(clause_lits);
+ if (clause_size <= s->opts.clause_max_sz_bin_resol &&
+ clause_clac_lbd(s, lits, clause_size) <= s->opts.clause_min_lbd_bin_resol)
+ clause_bin_resolution(s, clause_lits);
+}
+
+static inline void clause_realloc(struct cdb *dest, struct cdb *src, unsigned *cref)
+{
+ unsigned new_cref;
+ struct clause *new_clause;
+ struct clause *old_clause = cdb_handler(src, *cref);
+
+ if (old_clause->f_reallocd) {
+ *cref = (unsigned) old_clause->size;
+ return;
+ }
+ new_cref = cdb_append(dest, 3 + old_clause->f_learnt + old_clause->size);
+ new_clause = cdb_handler(dest, new_cref);
+ memcpy(new_clause, old_clause, (3 + old_clause->f_learnt + old_clause->size) * 4);
+ old_clause->f_reallocd = 1;
+ old_clause->size = (unsigned) new_cref;
+ *cref = new_cref;
+}
+
+//===------------------------------------------------------------------------===
+// Solver internal functions
+//===------------------------------------------------------------------------===
+static inline unsigned solver_decide(solver_t *s)
+{
+ unsigned next_var = UNDEF;
+
+ while (next_var == UNDEF || var_value(s, next_var) != VAR_UNASSING) {
+ if (heap_size(s->var_order) == 0) {
+ next_var = UNDEF;
+ return UNDEF;
+ } else
+ next_var = heap_remove_min(s->var_order);
+ }
+ return var2lit(next_var, vec_char_at(s->polarity, next_var));
+}
+
+static inline void solver_new_decision(solver_t *s, unsigned lit)
+{
+ assert(var_value(s, lit2var(lit)) == VAR_UNASSING);
+ vec_uint_push_back(s->trail_lim, vec_uint_size(s->trail));
+ solver_enqueue(s, lit, UNDEF);
+}
+
+/* Calculate Backtrack Level from the learnt clause */
+static inline unsigned solver_calc_bt_level(solver_t *s, vec_uint_t *learnt)
+{
+ unsigned i, tmp;
+ unsigned i_max = 1;
+ unsigned *lits = vec_uint_data(learnt);
+ unsigned max = lit_dlevel(s, lits[1]);
+
+ if (vec_uint_size(learnt) == 1)
+ return 0;
+ for (i = 2; i < vec_uint_size(learnt); i++) {
+ if (lit_dlevel(s, lits[i]) > max) {
+ max = lit_dlevel(s, lits[i]);
+ i_max = i;
+ }
+ }
+ tmp = lits[1];
+ lits[1] = lits[i_max];
+ lits[i_max] = tmp;
+ return lit_dlevel(s, lits[1]);
+}
+
+/**
+ * Most books and papers explain conflict analysis and the calculation of the
+ * 1UIP (first Unique Implication Point) using an implication graph. This
+ * function, however, do not explicity constructs the graph! It inspects the
+ * trail in reverse and figure out which literals should be added to the
+ * to-be-learnt clause using the reasons of each assignment.
+ *
+ * cur_lit: current literal being analyzed.
+ * n_paths: number of unprocessed paths from conlfict node to the current
+ * literal being analyzed (cur_lit).
+ *
+ * This functions performs a backward BFS (breadth-first search) for 1UIP node.
+ * The trail works as the BFS queue. The counter of unprocessed but seen
+ * variables (n_paths) allows us to identify when 'cur_lit' is the closest
+ * cause of conflict.
+ *
+ * When 'n_paths' reaches zero it means there are no unprocessed reverse paths
+ * back from the conflict node to 'cur_lit' - meaning it is the 1UIP decision
+ * variable.
+ *
+ */
+static inline void solver_analyze(solver_t *s, unsigned cref, vec_uint_t *learnt,
+ unsigned *bt_level, unsigned *lbd)
+{
+ unsigned i;
+ unsigned *trail = vec_uint_data(s->trail);
+ unsigned idx = vec_uint_size(s->trail) - 1;
+ unsigned n_paths = 0;
+ unsigned p = UNDEF;
+ unsigned var;
+
+ vec_uint_push_back(learnt, UNDEF);
+ do {
+ struct clause *clause;
+ unsigned *lits;
+ unsigned j;
+
+ assert(cref != UNDEF);
+ clause = clause_read(s, cref);
+ lits = &(clause->data[0].lit);
+
+ if (p != UNDEF && clause->size == 2 && lit_value(s, lits[0]) == LIT_FALSE) {
+ assert(lit_value(s, lits[1]) == LIT_TRUE);
+ mkt_swap(unsigned, lits[0], lits[1] );
+ }
+
+ if (clause->f_learnt)
+ clause_act_bump(s, clause);
+
+ if (clause->f_learnt && clause->lbd > 2) {
+ unsigned n_levels = clause_clac_lbd(s, lits, clause->size);
+ if (n_levels + 1 < clause->lbd) {
+ if (clause->lbd <= s->opts.lbd_freeze_clause)
+ clause->f_deletable = 0;
+ clause->lbd = n_levels;
+ }
+ }
+
+ for (j = (p == UNDEF ? 0 : 1); j < clause->size; j++) {
+ var = lit2var(lits[j]);
+ if (vec_char_at(s->seen, var) || var_dlevel(s, var) == 0)
+ continue;
+ vec_char_assign(s->seen, var, 1);
+ var_act_bump(s, var);
+ if (var_dlevel(s, var) == solver_dlevel(s)) {
+ n_paths++;
+ if (var_reason(s, var) != UNDEF && clause_read(s, var_reason(s, var))->f_learnt)
+ vec_uint_push_back(s->last_dlevel, var);
+ } else
+ vec_uint_push_back(learnt, lits[j]);
+ }
+
+ while (!vec_char_at(s->seen, lit2var(trail[idx--])));
+
+ p = trail[idx + 1];
+ cref = lit_reason(s, p);
+ vec_char_assign(s->seen, lit2var(p), 0);
+ n_paths--;
+ } while (n_paths > 0);
+
+ vec_uint_data(learnt)[0] = lit_neg(p);
+ clause_minimize(s, learnt);
+ *bt_level = solver_calc_bt_level(s, learnt);
+ *lbd = clause_clac_lbd(s, vec_uint_data(learnt), vec_uint_size(learnt));
+
+ if (vec_uint_size( s->last_dlevel) > 0) {
+ vec_uint_foreach(s->last_dlevel, var, i) {
+ if (clause_read(s, var_reason(s, var))->lbd < *lbd)
+ var_act_bump(s, var);
+ }
+ vec_uint_clear(s->last_dlevel);
+ }
+ vec_uint_foreach(s->tagged, var, i)
+ vec_char_assign(s->seen, var, 0);
+ vec_uint_clear(s->tagged);
+}
+
+static inline int solver_rst(solver_t *s)
+{
+ return b_queue_is_valid(s->bq_lbd) &&
+ (((long long)b_queue_avg(s->bq_lbd) * s->opts.f_rst) > (s->sum_lbd / s->stats.n_conflicts));
+}
+
+static inline int solver_block_rst(solver_t *s)
+{
+ return s->stats.n_conflicts > s->opts.fst_block_rst &&
+ b_queue_is_valid(s->bq_lbd) &&
+ (vec_uint_size(s->trail) > (s->opts.b_rst * (long long)b_queue_avg(s->bq_trail)));
+}
+
+static inline void solver_handle_conflict(solver_t *s, unsigned confl_cref)
+{
+ unsigned bt_level;
+ unsigned lbd;
+ unsigned cref;
+
+ vec_uint_clear(s->temp_lits);
+ solver_analyze(s, confl_cref, s->temp_lits, &bt_level, &lbd);
+ s->sum_lbd += lbd;
+ b_queue_push(s->bq_lbd, lbd);
+ solver_cancel_until(s, bt_level);
+ cref = UNDEF;
+ if (vec_uint_size(s->temp_lits) > 1) {
+ cref = solver_clause_create(s, s->temp_lits, 1);
+ clause_watch(s, cref);
+ }
+ solver_enqueue(s, vec_uint_at(s->temp_lits, 0), cref);
+ var_act_decay(s);
+ clause_act_decay(s);
+}
+
+static inline void solver_analyze_final(solver_t *s, unsigned lit)
+{
+ unsigned i;
+
+ vec_uint_push_back(s->final_conflict, lit);
+ if (solver_dlevel(s) == 0)
+ return;
+ vec_char_assign(s->seen, lit2var(lit), 1);
+ for (i = vec_uint_size(s->trail) - 1; i <= vec_uint_at(s->trail_lim, 0); i--) {
+ unsigned var = lit2var(vec_uint_at(s->trail, i));
+
+ if (vec_char_at(s->seen, var)) {
+ unsigned reason = var_reason(s, var);
+ if (reason == UNDEF) {
+ assert(var_dlevel(s, var) > 0);
+ vec_uint_push_back(s->final_conflict, lit_neg(vec_uint_at(s->trail, i)));
+ } else {
+ unsigned j;
+ struct clause *clause = clause_read(s, reason);
+ for (j = (clause->size == 2 ? 0 : 1); j < clause->size; j++) {
+ if (lit_dlevel(s, clause->data[j].lit) > 0)
+ vec_char_assign(s->seen, lit2var(clause->data[j].lit), 1);
+ }
+ }
+ vec_char_assign(s->seen, var, 0);
+ }
+ }
+ vec_char_assign(s->seen, lit2var(lit), 0);
+}
+
+static inline void solver_garbage_collect(solver_t *s)
+{
+ unsigned i;
+ unsigned *array;
+ struct cdb *new_cdb = cdb_alloc(cdb_capacity(s->all_clauses) - cdb_wasted(s->all_clauses));
+
+ for (i = 0; i < 2 * vec_char_size(s->assigns); i++) {
+ struct watcher *w;
+ watch_list_foreach(s->watches, w, i)
+ clause_realloc(new_cdb, s->all_clauses, &(w->cref));
+ watch_list_foreach(s->bin_watches, w, i)
+ clause_realloc(new_cdb, s->all_clauses, &(w->cref));
+ }
+
+ for (i = 0; i < vec_uint_size(s->trail); i++)
+ if (lit_reason(s, vec_uint_at(s->trail, i)) != UNDEF)
+ clause_realloc(new_cdb, s->all_clauses, &(vec_uint_data(s->reasons)[lit2var(vec_uint_at(s->trail, i))]));
+
+ array = vec_uint_data(s->learnts);
+ for (i = 0; i < vec_uint_size(s->learnts); i++)
+ clause_realloc(new_cdb, s->all_clauses, &(array[i]));
+
+ array = vec_uint_data(s->originals);
+ for (i = 0; i < vec_uint_size(s->originals); i++)
+ clause_realloc(new_cdb, s->all_clauses, &(array[i]));
+
+ cdb_free(s->all_clauses);
+ s->all_clauses = new_cdb;
+}
+
+static inline void solver_reduce_cdb(solver_t *s)
+{
+ unsigned i, limit;
+ unsigned n_learnts = vec_uint_size(s->learnts);
+ unsigned cref;
+ struct clause *clause;
+ struct clause **learnts_cls;
+
+ learnts_cls = satoko_alloc(struct clause *, n_learnts);
+ vec_uint_foreach(s->learnts, cref, i)
+ learnts_cls[i] = clause_read(s, cref);
+
+ limit = n_learnts / 2;
+
+ satoko_sort((void *)learnts_cls, n_learnts,
+ (int (*)(const void *, const void *)) clause_compare);
+
+ if (learnts_cls[n_learnts / 2]->lbd <= 3)
+ s->RC2 += s->opts.inc_special_reduce;
+ if (learnts_cls[n_learnts - 1]->lbd <= 6)
+ s->RC2 += s->opts.inc_special_reduce;
+
+ vec_uint_clear(s->learnts);
+ for (i = 0; i < n_learnts; i++) {
+ clause = learnts_cls[i];
+ cref = cdb_cref(s->all_clauses, (unsigned *)clause);
+ assert(clause->f_mark == 0);
+ if (clause->f_deletable && clause->lbd > 2 && clause->size > 2 && lit_reason(s, clause->data[0].lit) != cref && (i < limit)) {
+ clause->f_mark = 1;
+ s->stats.n_learnt_lits -= clause->size;
+ clause_unwatch(s, cref);
+ cdb_remove(s->all_clauses, clause);
+ } else {
+ if (!clause->f_deletable)
+ limit++;
+ clause->f_deletable = 1;
+ vec_uint_push_back(s->learnts, cref);
+ }
+ }
+ satoko_free(learnts_cls);
+
+ if (s->opts.verbose) {
+ printf("reduceDB: Keeping %7d out of %7d clauses (%5.2f %%) \n",
+ vec_uint_size(s->learnts), n_learnts,
+ 100.0 * vec_uint_size(s->learnts) / n_learnts);
+ fflush(stdout);
+ }
+ if (cdb_wasted(s->all_clauses) > cdb_size(s->all_clauses) * s->opts.garbage_max_ratio)
+ solver_garbage_collect(s);
+}
+
+//===------------------------------------------------------------------------===
+// Solver external functions
+//===------------------------------------------------------------------------===
+unsigned solver_clause_create(solver_t *s, vec_uint_t *lits, unsigned f_learnt)
+{
+ struct clause *clause;
+ unsigned cref;
+ unsigned n_words;
+
+ assert(vec_uint_size(lits) > 1);
+ assert(f_learnt == 0 || f_learnt == 1);
+
+ n_words = 3 + f_learnt + vec_uint_size(lits);
+ cref = cdb_append(s->all_clauses, n_words);
+ clause = clause_read(s, cref);
+ clause->f_learnt = f_learnt;
+ clause->f_mark = 0;
+ clause->f_reallocd = 0;
+ clause->f_deletable = f_learnt;
+ clause->size = vec_uint_size(lits);
+ memcpy(&(clause->data[0].lit), vec_uint_data(lits), sizeof(unsigned) * vec_uint_size(lits));
+
+ if (f_learnt) {
+ vec_uint_push_back(s->learnts, cref);
+ clause->lbd = clause_clac_lbd(s, vec_uint_data(lits), vec_uint_size(lits));
+ clause->data[clause->size].act = 0;
+ s->stats.n_learnt_lits += vec_uint_size(lits);
+ clause_act_bump(s, clause);
+ } else {
+ vec_uint_push_back(s->originals, cref);
+ s->stats.n_original_lits += vec_uint_size(lits);
+ }
+ return cref;
+}
+
+void solver_cancel_until(solver_t * s, unsigned level)
+{
+ int i;
+
+ if (solver_dlevel(s) <= level)
+ return;
+ for (i = (int) vec_uint_size(s->trail) - 1; i >= (int) vec_uint_at(s->trail_lim, level); i--) {
+ unsigned var = lit2var(vec_uint_at(s->trail, (unsigned) i));
+
+ vec_char_assign(s->assigns, var, VAR_UNASSING);
+ vec_uint_assign(s->reasons, var, UNDEF);
+ vec_char_assign(s->polarity, var, lit_polarity(vec_uint_at(s->trail, (unsigned) i)));
+ if (!heap_in_heap(s->var_order, var))
+ heap_insert(s->var_order, var);
+ }
+ s->i_qhead = vec_uint_at(s->trail_lim, level);
+ vec_uint_shrink(s->trail, vec_uint_at(s->trail_lim, level));
+ vec_uint_shrink(s->trail_lim, level);
+}
+
+unsigned solver_propagate(solver_t *s)
+{
+ unsigned conf_cref = UNDEF;
+ unsigned *lits;
+ unsigned neg_lit;
+ unsigned n_propagations = 0;
+
+ while (s->i_qhead < vec_uint_size(s->trail)) {
+ unsigned p = vec_uint_at(s->trail, s->i_qhead++);
+ struct watch_list *ws;
+ struct watcher *begin;
+ struct watcher *end;
+ struct watcher *i, *j;
+
+ n_propagations++;
+ watch_list_foreach(s->bin_watches, i, p) {
+ if (var_value(s, lit2var(i->blocker)) == VAR_UNASSING)
+ solver_enqueue(s, i->blocker, i->cref);
+ else if (lit_value(s, i->blocker) == LIT_FALSE)
+ return i->cref;
+ }
+
+ ws = vec_wl_at(s->watches, p);
+ begin = watch_list_array(ws);
+ end = begin + watch_list_size(ws);
+ for (i = j = begin; i < end;) {
+ struct clause *clause;
+ struct watcher w;
+
+ if (lit_value(s, i->blocker) == LIT_TRUE) {
+ *j++ = *i++;
+ continue;
+ }
+
+ clause = clause_read(s, i->cref);
+ lits = &(clause->data[0].lit);
+
+ // Make sure the false literal is data[1]:
+ neg_lit = lit_neg(p);
+ if (lits[0] == neg_lit)
+ mkt_swap(unsigned, lits[0], lits[1]);
+ assert(lits[1] == neg_lit);
+
+ w.cref = i->cref;
+ w.blocker = lits[0];
+
+ /* If 0th watch is true, then clause is already satisfied. */
+ if (lits[0] != i->blocker && lit_value(s, lits[0]) == LIT_TRUE)
+ *j++ = w;
+ else {
+ /* Look for new watch */
+ unsigned k;
+ for (k = 2; k < clause->size; k++) {
+ if (lit_value(s, lits[k]) != LIT_FALSE) {
+ lits[1] = lits[k];
+ lits[k] = neg_lit;
+ watch_list_push(vec_wl_at(s->watches, lit_neg(lits[1])), w);
+ goto next;
+ }
+ }
+
+ *j++ = w;
+
+ /* Clause becomes unit under this assignment */
+ if (lit_value(s, lits[0]) == LIT_FALSE) {
+ conf_cref = i->cref;
+ s->i_qhead = vec_uint_size(s->trail);
+ i++;
+ // Copy the remaining watches:
+ while (i < end)
+ *j++ = *i++;
+ } else
+ solver_enqueue(s, lits[0], i->cref);
+ }
+ next:
+ i++;
+ }
+
+ s->stats.n_inspects += j - watch_list_array(ws);
+ watch_list_shrink(ws, j - watch_list_array(ws));
+ }
+ s->stats.n_propagations += n_propagations;
+ s->n_props_simplify -= n_propagations;
+ return conf_cref;
+}
+
+char solver_search(solver_t *s)
+{
+ s->stats.n_starts++;
+ while (1) {
+ unsigned confl_cref = solver_propagate(s);
+ if (confl_cref != UNDEF) {
+ s->stats.n_conflicts++;
+ if (solver_dlevel(s) == 0)
+ return SATOKO_UNSAT;
+ /* Restart heuristic */
+ b_queue_push(s->bq_trail, vec_uint_size(s->trail));
+ if (solver_block_rst(s))
+ b_queue_clean(s->bq_lbd);
+ solver_handle_conflict(s, confl_cref);
+ } else {
+ /* No conflict */
+ unsigned next_lit;
+
+ if (solver_rst(s)) {
+ b_queue_clean(s->bq_lbd);
+ solver_cancel_until(s, 0);
+ return SATOKO_UNDEC;
+ }
+ if (solver_dlevel(s) == 0)
+ satoko_simplify(s);
+
+ /* Reduce the set of learnt clauses */
+ if (s->stats.n_conflicts >= s->n_confl_bfr_reduce) {
+ s->RC1 = (s->stats.n_conflicts / s->RC2) + 1;
+ solver_reduce_cdb(s);
+ s->RC2 += s->opts.inc_reduce;
+ s->n_confl_bfr_reduce = s->RC1 * s->RC2;
+ }
+
+ /* Make decisions based on user assumptions */
+ next_lit = UNDEF;
+ while (solver_dlevel(s) < vec_uint_size(s->assumptions)) {
+ unsigned lit = vec_uint_at(s->assumptions, solver_dlevel(s));
+ if (lit_value(s, lit) == LIT_TRUE) {
+ vec_uint_push_back(s->trail_lim, vec_uint_size(s->trail));
+ } else if (lit_value(s, lit) == LIT_FALSE) {
+ solver_analyze_final(s, lit_neg(lit));
+ return SATOKO_UNSAT;
+ } else {
+ next_lit = lit;
+ break;
+ }
+
+ }
+ if (next_lit == UNDEF) {
+ s->stats.n_decisions++;
+ next_lit = solver_decide(s);
+ if (next_lit == UNDEF)
+ return SATOKO_SAT;
+ }
+ solver_new_decision(s, next_lit);
+ }
+ }
+}
+
+//===------------------------------------------------------------------------===
+// Debug procedure
+//===------------------------------------------------------------------------===
+void solver_debug_check(solver_t *s, int result)
+{
+ unsigned cref, i;
+ unsigned *array;
+
+ printf("Checking for trail(%u) inconsistencies...", vec_uint_size(s->trail));
+ array = vec_uint_data(s->trail);
+ for (i = 1; i < vec_uint_size(s->trail); i++)
+ if (array[i - 1] == lit_neg(array[i])) {
+ printf("Inconsistent trail: %u %u\n", array[i - 1], array[i]);
+ return;
+ }
+ printf(" TRAIL OK\n");
+
+ printf("Checking clauses... \n");
+ vec_uint_foreach(s->originals, cref, i) {
+ unsigned j;
+ struct clause *clause = clause_read(s, cref);
+ for (j = 0; j < clause->size; j++) {
+ if (vec_uint_find(s->trail, clause->data[j].lit)) {
+ break;
+ }
+ }
+ if (result == SATOKO_SAT && j == clause->size) {
+ printf("FOUND UNSAT CLAUSE!!!!\n");
+ clause_print(clause);
+ }
+ }
+}
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/sat/satoko/solver.h b/src/sat/satoko/solver.h
new file mode 100644
index 00000000..65b86c68
--- /dev/null
+++ b/src/sat/satoko/solver.h
@@ -0,0 +1,242 @@
+//===--- solver.h -----------------------------------------------------------===
+//
+// satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__solver_h
+#define satoko__solver_h
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+
+#include "clause.h"
+#include "cdb.h"
+#include "satoko.h"
+#include "types.h"
+#include "watch_list.h"
+#include "utils/b_queue.h"
+#include "utils/heap.h"
+#include "utils/mem.h"
+#include "utils/misc.h"
+#include "utils/vec/vec_char.h"
+#include "utils/vec/vec_dble.h"
+#include "utils/vec/vec_uint.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+enum {
+ LIT_FALSE = 1,
+ LIT_TRUE = 0,
+ VAR_UNASSING = 3
+};
+
+#define UNDEF 0xFFFFFFFF
+
+struct satoko_stats {
+ unsigned n_starts;
+ unsigned n_reduce_db;
+
+ long long n_decisions;
+ long long n_propagations;
+ long long n_inspects;
+ long long n_conflicts;
+
+ long long n_original_lits;
+ long long n_learnt_lits;
+};
+
+typedef struct solver_t_ solver_t;
+struct solver_t_ {
+ /* User data */
+ vec_uint_t *assumptions;
+ vec_uint_t *final_conflict;
+
+ /* Clauses Database */
+ struct cdb *all_clauses;
+ vec_uint_t *learnts;
+ vec_uint_t *originals;
+ vec_wl_t *watches;
+ vec_wl_t *bin_watches;
+
+ /* Activity heuristic */
+ act_t var_act_inc; /* Amount to bump next variable with. */
+ clause_act_t clause_act_inc; /* Amount to bump next clause with. */
+
+ /* Variable Information */
+ vec_act_t *activity; /* A heuristic measurement of the activity of a variable. */
+ heap_t *var_order;
+ vec_uint_t *levels; /* Decision level of the current assignment */
+ vec_uint_t *reasons; /* Reason (clause) of the current assignment */
+ vec_char_t *assigns;
+ vec_char_t *polarity;
+
+ /* Assignments */
+ vec_uint_t *trail;
+ vec_uint_t *trail_lim; /* Separator indices for different decision levels in 'trail'. */
+ unsigned i_qhead; /* Head of propagation queue (as index into the trail). */
+ unsigned n_assigns_simplify; /* Number of top-level assignments since
+ last execution of 'simplify()'. */
+ long long n_props_simplify; /* Remaining number of propagations that
+ must be made before next execution of
+ 'simplify()'. */
+
+ /* Temporary data used by Search method */
+ b_queue_t *bq_trail;
+ b_queue_t *bq_lbd;
+ long RC1;
+ long RC2;
+ unsigned n_confl_bfr_reduce;
+ float sum_lbd;
+
+ /* Temporary data used by Analyze */
+ vec_uint_t *temp_lits;
+ vec_char_t *seen;
+ vec_uint_t *tagged; /* Stack */
+ vec_uint_t *stack;
+ vec_uint_t *last_dlevel;
+
+ /* Misc temporary */
+ vec_uint_t *stamps; /* Multipurpose stamp used to calculate LBD and
+ * clauses minimization with binary resolution */
+ unsigned cur_stamp; /* Used for marking literals and levels of interest */
+
+ struct satoko_stats stats;
+ struct satoko_opts opts;
+};
+
+//===------------------------------------------------------------------------===
+extern unsigned solver_clause_create(solver_t *, vec_uint_t *, unsigned);
+extern char solver_search(solver_t *);
+extern void solver_cancel_until(solver_t *, unsigned);
+extern unsigned solver_propagate(solver_t *);
+extern void solver_debug_check(solver_t *, int);
+
+//===------------------------------------------------------------------------===
+// Inline var/lit functions
+//===------------------------------------------------------------------------===
+static inline unsigned var2lit(unsigned var, char polarity)
+{
+ return var + var + ((unsigned) polarity != 0);
+}
+
+static inline unsigned lit2var(unsigned lit)
+{
+ return lit >> 1;
+}
+//===------------------------------------------------------------------------===
+// Inline var functions
+//===------------------------------------------------------------------------===
+static inline char var_value(solver_t *s, unsigned var)
+{
+ return vec_char_at(s->assigns, var);
+}
+
+static inline unsigned var_dlevel(solver_t *s, unsigned var)
+{
+ return vec_uint_at(s->levels, var);
+}
+
+static inline unsigned var_reason(solver_t *s, unsigned var)
+{
+ return vec_uint_at(s->reasons, var);
+}
+//===------------------------------------------------------------------------===
+// Inline lit functions
+//===------------------------------------------------------------------------===
+static inline unsigned lit_neg(unsigned lit)
+{
+ return lit ^ 1;
+}
+
+static inline char lit_polarity(unsigned lit)
+{
+ return (char)(lit & 1);
+}
+
+static inline char lit_value(solver_t *s, unsigned lit)
+{
+ return lit_polarity(lit) ^ vec_char_at(s->assigns, lit2var(lit));
+}
+
+static inline unsigned lit_dlevel(solver_t *s, unsigned lit)
+{
+ return vec_uint_at(s->levels, lit2var(lit));
+}
+
+static inline unsigned lit_reason(solver_t *s, unsigned lit)
+{
+ return vec_uint_at(s->reasons, lit2var(lit));
+}
+//===------------------------------------------------------------------------===
+// Inline solver minor functions
+//===------------------------------------------------------------------------===
+static inline unsigned solver_check_limits(solver_t *s)
+{
+ return (s->opts.conf_limit == 0 || s->opts.conf_limit >= s->stats.n_conflicts) &&
+ (s->opts.prop_limit == 0 || s->opts.prop_limit >= s->stats.n_propagations);
+}
+
+/** Returns current decision level */
+static inline unsigned solver_dlevel(solver_t *s)
+{
+ return vec_uint_size(s->trail_lim);
+}
+
+static inline int solver_enqueue(solver_t *s, unsigned lit, unsigned reason)
+{
+ unsigned var = lit2var(lit);
+
+ vec_char_assign(s->assigns, var, lit_polarity(lit));
+ vec_uint_assign(s->levels, var, solver_dlevel(s));
+ vec_uint_assign(s->reasons, var, reason);
+ vec_uint_push_back(s->trail, lit);
+ return SATOKO_OK;
+}
+
+//===------------------------------------------------------------------------===
+// Inline clause functions
+//===------------------------------------------------------------------------===
+static inline struct clause *clause_read(solver_t *s, unsigned cref)
+{
+ return cdb_handler(s->all_clauses, cref);
+}
+
+static inline void clause_watch(solver_t *s, unsigned cref)
+{
+ struct clause *clause = cdb_handler(s->all_clauses, cref);
+ struct watcher w1;
+ struct watcher w2;
+
+ w1.cref = cref;
+ w2.cref = cref;
+ w1.blocker = clause->data[1].lit;
+ w2.blocker = clause->data[0].lit;
+ if (clause->size == 2) {
+ watch_list_push(vec_wl_at(s->bin_watches, lit_neg(clause->data[0].lit)), w1);
+ watch_list_push(vec_wl_at(s->bin_watches, lit_neg(clause->data[1].lit)), w2);
+ } else {
+ watch_list_push(vec_wl_at(s->watches, lit_neg(clause->data[0].lit)), w1);
+ watch_list_push(vec_wl_at(s->watches, lit_neg(clause->data[1].lit)), w2);
+ }
+}
+
+static inline void clause_unwatch(solver_t *s, unsigned cref)
+{
+ struct clause *clause = cdb_handler(s->all_clauses, cref);
+ if (clause->size == 2) {
+ watch_list_remove(vec_wl_at(s->bin_watches, lit_neg(clause->data[0].lit)), cref);
+ watch_list_remove(vec_wl_at(s->bin_watches, lit_neg(clause->data[1].lit)), cref);
+ } else {
+ watch_list_remove(vec_wl_at(s->watches, lit_neg(clause->data[0].lit)), cref);
+ watch_list_remove(vec_wl_at(s->watches, lit_neg(clause->data[1].lit)), cref);
+ }
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__solver_h */
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c
new file mode 100644
index 00000000..db9a267b
--- /dev/null
+++ b/src/sat/satoko/solver_api.c
@@ -0,0 +1,310 @@
+//===--- solver_api.h -------------------------------------------------------===
+//
+// satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#include <stdio.h>
+#include <assert.h>
+#include <string.h>
+#include <math.h>
+
+#include "act_var.h"
+#include "utils/misc.h"
+#include "solver.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_IMPL_START
+
+//===------------------------------------------------------------------------===
+// Satoko internal functions
+//===------------------------------------------------------------------------===
+static inline void solver_rebuild_order(solver_t *s)
+{
+ unsigned var;
+ vec_uint_t *vars = vec_uint_alloc(vec_char_size(s->assigns));
+
+ for (var = 0; var < vec_char_size(s->assigns); var++)
+ if (var_value(s, var) == VAR_UNASSING)
+ vec_uint_push_back(vars, var);
+ heap_build(s->var_order, vars);
+ vec_uint_free(vars);
+}
+
+static inline int clause_is_satisfied(solver_t *s, struct clause *clause)
+{
+ unsigned i;
+ unsigned *lits = &(clause->data[0].lit);
+ for (i = 0; i < clause->size; i++)
+ if (lit_value(s, lits[i]) == LIT_TRUE)
+ return SATOKO_OK;
+ return SATOKO_ERR;
+}
+
+static inline void print_opts(solver_t *s)
+{
+ printf( "+-[ BLACK MAGIC - PARAMETERS ]-+\n");
+ printf( "| |\n");
+ printf( "|--> Restarts heuristic |\n");
+ printf( "| * LBD Queue = %6d |\n", s->opts.sz_lbd_bqueue);
+ printf( "| * Trail Queue = %6d |\n", s->opts.sz_trail_bqueue);
+ printf( "| * f_rst = %6.2f |\n", s->opts.f_rst);
+ printf( "| * b_rst = %6.2f |\n", s->opts.b_rst);
+ printf( "| |\n");
+ printf( "|--> Clause DB reduction: |\n");
+ printf( "| * First = %6d |\n", s->opts.n_conf_fst_reduce);
+ printf( "| * Inc = %6d |\n", s->opts.inc_reduce);
+ printf( "| * Special Inc = %6d |\n", s->opts.inc_special_reduce);
+ printf( "| * Protected (LBD) < %2d |\n", s->opts.lbd_freeze_clause);
+ printf( "| |\n");
+ printf( "|--> Binary resolution: |\n");
+ printf( "| * Clause size < %3d |\n", s->opts.clause_max_sz_bin_resol);
+ printf( "| * Clause lbd < %3d |\n", s->opts.clause_min_lbd_bin_resol);
+ printf( "+------------------------------+\n\n");
+}
+
+static inline void print_stats(solver_t *s)
+{
+ printf("starts : %10d\n", s->stats.n_starts);
+ printf("conflicts : %10lld\n", s->stats.n_conflicts);
+ printf("decisions : %10lld\n", s->stats.n_decisions);
+ printf("propagations : %10lld\n", s->stats.n_propagations);
+}
+
+//===------------------------------------------------------------------------===
+// Satoko external functions
+//===------------------------------------------------------------------------===
+solver_t * satoko_create()
+{
+ solver_t *s = satoko_calloc(solver_t, 1);
+
+ satoko_default_opts(&s->opts);
+ /* User data */
+ s->assumptions = vec_uint_alloc(0);
+ s->final_conflict = vec_uint_alloc(0);
+ /* Clauses Database */
+ s->all_clauses = cdb_alloc(0);
+ s->originals = vec_uint_alloc(0);
+ s->learnts = vec_uint_alloc(0);
+ s->watches = vec_wl_alloc(0);
+ s->bin_watches = vec_wl_alloc(0);
+ /* Activity heuristic */
+ s->var_act_inc = VAR_ACT_INIT_INC;
+ s->clause_act_inc = CLAUSE_ACT_INIT_INC;
+ /* Variable Information */
+ s->activity = vec_act_alloc(0);
+ s->var_order = heap_alloc(s->activity);
+ s->levels = vec_uint_alloc(0);
+ s->reasons = vec_uint_alloc(0);
+ s->assigns = vec_char_alloc(0);
+ s->polarity = vec_char_alloc(0);
+ /* Assignments */
+ s->trail = vec_uint_alloc(0);
+ s->trail_lim = vec_uint_alloc(0);
+ /* Temporary data used by Search method */
+ s->bq_trail = b_queue_alloc(s->opts.sz_trail_bqueue);
+ s->bq_lbd = b_queue_alloc(s->opts.sz_lbd_bqueue);
+ s->n_confl_bfr_reduce = s->opts.n_conf_fst_reduce;
+ s->RC1 = 1;
+ s->RC2 = s->opts.n_conf_fst_reduce;
+ /* Temporary data used by Analyze */
+ s->temp_lits = vec_uint_alloc(0);
+ s->seen = vec_char_alloc(0);
+ s->tagged = vec_uint_alloc(0);
+ s->stack = vec_uint_alloc(0);
+ s->last_dlevel = vec_uint_alloc(0);
+ /* Misc temporary */
+ s->stamps = vec_uint_alloc(0);
+ return s;
+}
+
+void satoko_destroy(solver_t *s)
+{
+ vec_uint_free(s->assumptions);
+ vec_uint_free(s->final_conflict);
+ cdb_free(s->all_clauses);
+ vec_uint_free(s->originals);
+ vec_uint_free(s->learnts);
+ vec_wl_free(s->watches);
+ vec_wl_free(s->bin_watches);
+ vec_act_free(s->activity);
+ heap_free(s->var_order);
+ vec_uint_free(s->levels);
+ vec_uint_free(s->reasons);
+ vec_char_free(s->assigns);
+ vec_char_free(s->polarity);
+ vec_uint_free(s->trail);
+ vec_uint_free(s->trail_lim);
+ b_queue_free(s->bq_lbd);
+ b_queue_free(s->bq_trail);
+ vec_uint_free(s->temp_lits);
+ vec_char_free(s->seen);
+ vec_uint_free(s->tagged);
+ vec_uint_free(s->stack);
+ vec_uint_free(s->last_dlevel);
+ vec_uint_free(s->stamps);
+ satoko_free(s);
+}
+
+void satoko_default_opts(satoko_opts_t *opts)
+{
+ opts->verbose = 0;
+ /* Limits */
+ opts->conf_limit = 0;
+ opts->prop_limit = 0;
+ /* Constants used for restart heuristic */
+ opts->f_rst = 0.8;
+ opts->b_rst = 1.4;
+ opts->fst_block_rst = 10000;
+ opts->sz_lbd_bqueue = 50;
+ opts->sz_trail_bqueue = 5000;
+ /* Constants used for clause database reduction heuristic */
+ opts->n_conf_fst_reduce = 2000;
+ opts->inc_reduce = 300;
+ opts->inc_special_reduce = 1000;
+ opts->lbd_freeze_clause = 30;
+ /* VSIDS heuristic */
+ opts->var_decay = 0.95;
+ opts->clause_decay = 0.995;
+ /* Binary resolution */
+ opts->clause_max_sz_bin_resol = 30;
+ opts->clause_min_lbd_bin_resol = 6;
+
+ opts->garbage_max_ratio = 0.3;
+}
+
+/**
+ * TODO: sanity check on configuration options
+ */
+void satoko_configure(satoko_t *s, satoko_opts_t *user_opts)
+{
+ assert(user_opts);
+ memcpy(&s->opts, user_opts, sizeof(satoko_opts_t));
+}
+
+int satoko_simplify(solver_t * s)
+{
+ unsigned i, j = 0;
+ unsigned cref;
+
+ assert(solver_dlevel(s) == 0);
+ if (solver_propagate(s) != UNDEF)
+ return SATOKO_ERR;
+ if (s->n_assigns_simplify == vec_uint_size(s->trail) || s->n_props_simplify > 0)
+ return SATOKO_OK;
+
+ vec_uint_foreach(s->originals, cref, i) {
+ struct clause *clause = clause_read(s, cref);
+
+ if (clause_is_satisfied(s, clause)) {
+ clause->f_mark = 1;
+ s->stats.n_original_lits -= clause->size;
+ clause_unwatch(s, cref);
+ } else
+ vec_uint_assign(s->originals, j++, cref);
+ }
+ vec_uint_shrink(s->originals, j);
+ solver_rebuild_order(s);
+ s->n_assigns_simplify = vec_uint_size(s->trail);
+ s->n_props_simplify = s->stats.n_original_lits + s->stats.n_learnt_lits;
+ return SATOKO_OK;
+}
+
+void satoko_add_variable(solver_t *s, char sign)
+{
+ unsigned var = vec_act_size(s->activity);
+ vec_wl_push(s->bin_watches);
+ vec_wl_push(s->bin_watches);
+ vec_wl_push(s->watches);
+ vec_wl_push(s->watches);
+ vec_act_push_back(s->activity, 0);
+ vec_uint_push_back(s->levels, 0);
+ vec_char_push_back(s->assigns, VAR_UNASSING);
+ vec_char_push_back(s->polarity, sign);
+ vec_uint_push_back(s->reasons, UNDEF);
+ vec_uint_push_back(s->stamps, 0);
+ vec_char_push_back(s->seen, 0);
+ heap_insert(s->var_order, var);
+}
+
+int satoko_add_clause(solver_t *s, unsigned *lits, unsigned size)
+{
+ unsigned i, j;
+ unsigned prev_lit;
+ unsigned max_var;
+ unsigned cref;
+
+ qsort((void *) lits, size, sizeof(unsigned), mkt_uint_compare);
+ max_var = lit2var(lits[size - 1]);
+ while (max_var >= vec_act_size(s->activity))
+ satoko_add_variable(s, LIT_FALSE);
+
+ vec_uint_clear(s->temp_lits);
+ j = 0;
+ prev_lit = UNDEF;
+ for (i = 0; i < size; i++) {
+ if (lits[i] == lit_neg(prev_lit) || lit_value(s, lits[i]) == LIT_TRUE)
+ return SATOKO_OK;
+ else if (lits[i] != prev_lit && var_value(s, lit2var(lits[i])) == VAR_UNASSING) {
+ prev_lit = lits[i];
+ vec_uint_push_back(s->temp_lits, lits[i]);
+ }
+ }
+
+ if (vec_uint_size(s->temp_lits) == 0)
+ return SATOKO_ERR;
+ if (vec_uint_size(s->temp_lits) == 1) {
+ solver_enqueue(s, vec_uint_at(s->temp_lits, 0), UNDEF);
+ return (solver_propagate(s) == UNDEF);
+ }
+
+ cref = solver_clause_create(s, s->temp_lits, 0);
+ clause_watch(s, cref);
+ return SATOKO_OK;
+}
+
+void satoko_assump_push(solver_t *s, unsigned lit)
+{
+ vec_uint_push_back(s->assumptions, lit);
+}
+
+void satoko_assump_pop(solver_t *s)
+{
+ assert(vec_uint_size(s->assumptions) > 0);
+ vec_uint_pop_back(s->assumptions);
+ solver_cancel_until(s, vec_uint_size(s->assumptions));
+}
+
+int satoko_solve(solver_t *s)
+{
+ char status = SATOKO_UNDEC;
+
+ assert(s);
+ if (s->opts.verbose)
+ print_opts(s);
+
+ while (status == SATOKO_UNDEC) {
+ status = solver_search(s);
+ if (solver_check_limits(s) == 0)
+ break;
+ }
+ if (s->opts.verbose)
+ print_stats(s);
+ solver_cancel_until(s, vec_uint_size(s->assumptions));
+ return status;
+}
+
+int satoko_final_conflict(solver_t *s, unsigned *out)
+{
+ if (vec_uint_size(s->final_conflict) == 0)
+ return -1;
+ out = satoko_alloc(unsigned, vec_uint_size(s->final_conflict));
+ memcpy(out, vec_uint_data(s->final_conflict),
+ sizeof(unsigned) * vec_uint_size(s->final_conflict));
+ return vec_uint_size(s->final_conflict);
+
+}
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/sat/satoko/types.h b/src/sat/satoko/types.h
new file mode 100644
index 00000000..2811c2c6
--- /dev/null
+++ b/src/sat/satoko/types.h
@@ -0,0 +1,50 @@
+//===--- types.h ------------------------------------------------------------===
+//
+// satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__types_h
+#define satoko__types_h
+
+#include "utils/vec/vec_dble.h"
+#include "utils/vec/vec_uint.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+#define SATOKO_ACT_VAR_DBLE
+#define SATOKO_ACT_CLAUSE_FLOAT
+
+#ifdef SATOKO_ACT_VAR_DBLE
+ #define VAR_ACT_INIT_INC 1.0
+ typedef double act_t;
+ typedef vec_dble_t vec_act_t ;
+ #define vec_act_alloc(size) vec_dble_alloc(size)
+ #define vec_act_free(vec) vec_dble_free(vec)
+ #define vec_act_size(vec) vec_dble_size(vec)
+ #define vec_act_at(vec, idx) vec_dble_at(vec, idx)
+ #define vec_act_push_back(vec, value) vec_dble_push_back(vec, value)
+#else
+ #define VAR_ACT_INIT_INC (1 << 5)
+ typedef unsigned act_t;
+ typedef vec_uint_t vec_act_t;
+ #define vec_act_alloc(size) vec_uint_alloc(size)
+ #define vec_act_free(vec) vec_uint_free(vec)
+ #define vec_act_size(vec) vec_uint_size(vec)
+ #define vec_act_at(vec, idx) vec_uint_at(vec, idx)
+ #define vec_act_push_back(vec, value) vec_uint_push_back(vec, value)
+#endif /* SATOKO_ACT_VAR_DBLE */
+
+#ifdef SATOKO_ACT_CLAUSE_FLOAT
+ #define CLAUSE_ACT_INIT_INC 1.0
+ typedef float clause_act_t;
+#else
+ #define CLAUSE_ACT_INIT_INC (1 << 11)
+ typedef unsigned clause_act_t;
+#endif /* SATOKO_ACT_CLAUSE_FLOAT */
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__types_h */
diff --git a/src/sat/satoko/utils/b_queue.h b/src/sat/satoko/utils/b_queue.h
new file mode 100644
index 00000000..926edf29
--- /dev/null
+++ b/src/sat/satoko/utils/b_queue.h
@@ -0,0 +1,81 @@
+//===--- b_queue.h ----------------------------------------------------------===
+//
+// satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__utils__b_queue_h
+#define satoko__utils__b_queue_h
+
+#include "mem.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+/* Bounded Queue */
+typedef struct b_queue_t_ b_queue_t;
+struct b_queue_t_ {
+ unsigned size;
+ unsigned cap;
+ unsigned i_first;
+ unsigned i_empty;
+ unsigned long long sum;
+ unsigned *data;
+};
+
+//===------------------------------------------------------------------------===
+// Bounded Queue API
+//===------------------------------------------------------------------------===
+static inline b_queue_t *b_queue_alloc(unsigned cap)
+{
+ b_queue_t *p = satoko_calloc(b_queue_t, 1);
+ p->cap = cap;
+ p->data = satoko_calloc(unsigned, cap);
+ return p;
+}
+
+static inline void b_queue_free(b_queue_t *p)
+{
+ satoko_free(p->data);
+ satoko_free(p);
+}
+
+static inline void b_queue_push(b_queue_t *p, unsigned Value)
+{
+ if (p->size == p->cap) {
+ assert(p->i_first == p->i_empty);
+ p->sum -= p->data[p->i_first];
+ p->i_first = (p->i_first + 1) % p->cap;
+ } else
+ p->size++;
+
+ p->sum += Value;
+ p->data[p->i_empty] = Value;
+ if ((++p->i_empty) == p->cap) {
+ p->i_empty = 0;
+ p->i_first = 0;
+ }
+}
+
+static inline unsigned b_queue_avg(b_queue_t *p)
+{
+ return (unsigned)(p->sum / ((unsigned long long) p->size));
+}
+
+static inline unsigned b_queue_is_valid(b_queue_t *p)
+{
+ return (p->cap == p->size);
+}
+
+static inline void b_queue_clean(b_queue_t *p)
+{
+ p->i_first = 0;
+ p->i_empty = 0;
+ p->size = 0;
+ p->sum = 0;
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__utils__b_queue_h */
diff --git a/src/sat/satoko/utils/heap.h b/src/sat/satoko/utils/heap.h
new file mode 100644
index 00000000..e1611e95
--- /dev/null
+++ b/src/sat/satoko/utils/heap.h
@@ -0,0 +1,181 @@
+//===--- heap.h ----------------------------------------------------------===
+//
+// satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__utils__heap_h
+#define satoko__utils__heap_h
+
+#include "mem.h"
+#include "../types.h"
+#include "vec/vec_dble.h"
+#include "vec/vec_int.h"
+#include "vec/vec_uint.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+typedef struct heap_t_ heap_t;
+struct heap_t_ {
+ vec_int_t *indices;
+ vec_uint_t *data;
+ vec_act_t *weights;
+};
+//===------------------------------------------------------------------------===
+// Heap internal functions
+//===------------------------------------------------------------------------===
+static inline unsigned left(unsigned i) { return 2 * i + 1; }
+static inline unsigned right(unsigned i) { return (i + 1) * 2; }
+static inline unsigned parent(unsigned i) { return (i - 1) >> 1; }
+
+static inline int compare(heap_t *p, unsigned x, unsigned y)
+{
+ return vec_act_at(p->weights, x) > vec_act_at(p->weights, y);
+}
+
+static inline void heap_percolate_up(heap_t *h, unsigned i)
+{
+ unsigned x = vec_uint_at(h->data, i);
+ unsigned p = parent(i);
+
+ while (i != 0 && compare(h, x, vec_uint_at(h->data, p))) {
+ vec_uint_assign(h->data, i, vec_uint_at(h->data, p));
+ vec_int_assign(h->indices, vec_uint_at(h->data, p), (int) i);
+ i = p;
+ p = parent(p);
+ }
+ vec_uint_assign(h->data, i, x);
+ vec_int_assign(h->indices, x, (int) i);
+}
+
+static inline void heap_percolate_down(heap_t *h, unsigned i)
+{
+ unsigned x = vec_uint_at(h->data, i);
+
+ while (left(i) < vec_uint_size(h->data)) {
+ unsigned child = right(i) < vec_uint_size(h->data) &&
+ compare(h, vec_uint_at(h->data, right(i)), vec_uint_at(h->data, left(i)))
+ ? right(i)
+ : left(i);
+
+ if (!compare(h, vec_uint_at(h->data, child), x))
+ break;
+
+ vec_uint_assign(h->data, i, vec_uint_at(h->data, child));
+ vec_int_assign(h->indices, vec_uint_at(h->data, i), (int) i);
+ i = child;
+ }
+ vec_uint_assign(h->data, i, x);
+ vec_int_assign(h->indices, x, (int) i);
+}
+
+//===------------------------------------------------------------------------===
+// Heap API
+//===------------------------------------------------------------------------===
+static inline heap_t *heap_alloc(vec_act_t *weights)
+{
+ heap_t *p = satoko_alloc(heap_t, 1);
+ p->weights = weights;
+ p->indices = vec_int_alloc(0);
+ p->data = vec_uint_alloc(0);
+ return p;
+}
+
+static inline void heap_free(heap_t *p)
+{
+ vec_int_free(p->indices);
+ vec_uint_free(p->data);
+ satoko_free(p);
+}
+
+static inline unsigned heap_size(heap_t *p)
+{
+ return vec_uint_size(p->data);
+}
+
+static inline int heap_in_heap(heap_t *p, unsigned entry)
+{
+ return (entry < vec_int_size(p->indices)) &&
+ (vec_int_at(p->indices, entry) >= 0);
+}
+
+static inline void heap_increase(heap_t *p, unsigned entry)
+{
+ assert(heap_in_heap(p, entry));
+ heap_percolate_down(p, (unsigned) vec_int_at(p->indices, entry));
+}
+
+static inline void heap_decrease(heap_t *p, unsigned entry)
+{
+ assert(heap_in_heap(p, entry));
+ heap_percolate_up(p, (unsigned) vec_int_at(p->indices, entry));
+}
+
+static inline void heap_insert(heap_t *p, unsigned entry)
+{
+ if (vec_int_size(p->indices) < entry + 1) {
+ unsigned old_size = vec_int_size(p->indices);
+ unsigned i;
+ int e;
+ vec_int_resize(p->indices, entry + 1);
+ vec_int_foreach_start(p->indices, e, i, old_size)
+ vec_int_assign(p->indices, i, -1);
+ }
+ assert(!heap_in_heap(p, entry));
+ vec_int_assign(p->indices, entry, (int) vec_uint_size(p->data));
+ vec_uint_push_back(p->data, entry);
+ heap_percolate_up(p, (unsigned) vec_int_at(p->indices, entry));
+}
+
+static inline void heap_update(heap_t *p, unsigned i)
+{
+ if (!heap_in_heap(p, i))
+ heap_insert(p, i);
+ else {
+ heap_percolate_up(p, (unsigned) vec_int_at(p->indices, i));
+ heap_percolate_down(p, (unsigned) vec_int_at(p->indices, i));
+ }
+}
+
+static inline void heap_build(heap_t *p, vec_uint_t *entries)
+{
+ int i;
+ unsigned j, entry;
+
+ vec_uint_foreach(p->data, entry, j)
+ vec_int_assign(p->indices, entry, -1);
+ vec_uint_clear(p->data);
+ vec_uint_foreach(entries, entry, j) {
+ vec_int_assign(p->indices, entry, (int) j);
+ vec_uint_push_back(p->data, entry);
+ }
+ for ((i = vec_uint_size(p->data) / 2 - 1); i >= 0; i--)
+ heap_percolate_down(p, (unsigned) i);
+}
+
+static inline void heap_clear(heap_t *p)
+{
+ unsigned i;
+ int entry;
+ vec_int_foreach(p->indices, entry, i)
+ vec_int_assign(p->indices, i, -1);
+ vec_uint_clear(p->data);
+}
+
+static inline unsigned heap_remove_min(heap_t *p)
+{
+ unsigned x = vec_uint_at(p->data, 0);
+ vec_uint_assign(p->data, 0, vec_uint_at(p->data, vec_uint_size(p->data) - 1));
+ vec_int_assign(p->indices, vec_uint_at(p->data, 0), 0);
+ vec_int_assign(p->indices, x, -1);
+ vec_uint_pop_back(p->data);
+ if (vec_uint_size(p->data) > 1)
+ heap_percolate_down(p, 0);
+ return x;
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__utils__heap_h */
diff --git a/src/sat/satoko/utils/mem.h b/src/sat/satoko/utils/mem.h
new file mode 100755
index 00000000..5ff9873d
--- /dev/null
+++ b/src/sat/satoko/utils/mem.h
@@ -0,0 +1,23 @@
+//===--- mem.h --------------------------------------------------------------===
+//
+// satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__utils__mem_h
+#define satoko__utils__mem_h
+
+#include <stdlib.h>
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+#define satoko_alloc(type, n_elements) ((type *) malloc((n_elements) * sizeof(type)))
+#define satoko_calloc(type, n_elements) ((type *) calloc((n_elements), sizeof(type)))
+#define satoko_realloc(type, ptr, n_elements) ((type *) realloc(ptr, (n_elements) * sizeof(type)))
+#define satoko_free(p) do { free(p); p = NULL; } while(0)
+
+ABC_NAMESPACE_HEADER_END
+#endif
diff --git a/src/sat/satoko/utils/misc.h b/src/sat/satoko/utils/misc.h
new file mode 100755
index 00000000..aa8bcb8c
--- /dev/null
+++ b/src/sat/satoko/utils/misc.h
@@ -0,0 +1,37 @@
+//===--- misc.h -------------------------------------------------------------===
+//
+// satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__utils__misc_h
+#define satoko__utils__misc_h
+
+#include <stdint.h>
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+#define mkt_swap(type, a, b) { type t = a; a = b; b = t; }
+
+static inline unsigned mkt_uint_max(unsigned a, unsigned b)
+{
+ return a > b ? a : b;
+}
+
+static inline int mkt_uint_compare(const void *p1, const void *p2)
+{
+ const unsigned pp1 = *(const unsigned *)p1;
+ const unsigned pp2 = *(const unsigned *)p2;
+
+ if (pp1 < pp2)
+ return -1;
+ if (pp1 > pp2)
+ return 1;
+ return 0;
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__utils__misc_h */
diff --git a/src/sat/satoko/utils/sort.h b/src/sat/satoko/utils/sort.h
new file mode 100644
index 00000000..285f4b91
--- /dev/null
+++ b/src/sat/satoko/utils/sort.h
@@ -0,0 +1,65 @@
+//===--- sort.h -------------------------------------------------------------===
+//
+// satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__utils__sort_h
+#define satoko__utils__sort_h
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+static inline void select_sort(void **data, unsigned size,
+ int (*comp_fn)(const void *, const void *))
+{
+ unsigned i, j, i_best;
+ void *temp;
+
+ for (i = 0; i < (size - 1); i++) {
+ i_best = i;
+ for (j = i + 1; j < size; j++) {
+ if (comp_fn(data[j], data[i_best]))
+ i_best = j;
+ }
+ temp = data[i];
+ data[i] = data[i_best];
+ data[i_best] = temp;
+ }
+}
+
+static void satoko_sort(void **data, unsigned size,
+ int (*comp_fn)(const void *, const void *))
+{
+ if (size <= 15)
+ select_sort(data, size, comp_fn);
+ else {
+ void *pivot = data[size / 2];
+ void *temp;
+ unsigned j = size;
+ int i = -1;
+
+ for (;;) {
+ do {
+ i++;
+ } while (comp_fn(data[i], pivot));
+ do {
+ j--;
+ } while (comp_fn(pivot, data[j]));
+
+ if ((unsigned) i >= j)
+ break;
+
+ temp = data[i];
+ data[i] = data[j];
+ data[j] = temp;
+ }
+ satoko_sort(data, (unsigned) i, comp_fn);
+ satoko_sort(data + i, (size - (unsigned) i), comp_fn);
+ }
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__utils__sort_h */
diff --git a/src/sat/satoko/utils/vec/vec_char.h b/src/sat/satoko/utils/vec/vec_char.h
new file mode 100644
index 00000000..fe88797a
--- /dev/null
+++ b/src/sat/satoko/utils/vec/vec_char.h
@@ -0,0 +1,259 @@
+//===--- vec_char.h ---------------------------------------------------------===
+//
+// satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__utils__vec__vec_char_h
+#define satoko__utils__vec__vec_char_h
+
+#include <assert.h>
+#include <stdio.h>
+#include <string.h>
+
+#include "../mem.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+typedef struct vec_char_t_ vec_char_t;
+struct vec_char_t_ {
+ unsigned cap;
+ unsigned size;
+ char *data;
+};
+
+//===------------------------------------------------------------------------===
+// Vector Macros
+//===------------------------------------------------------------------------===
+#define vec_char_foreach(vec, entry, i) \
+ for (i = 0; (i < vec_char_size(vec)) && (((entry) = vec_char_at(vec, i)), 1); i++)
+
+#define vec_char_foreach_start(vec, entry, i, start) \
+ for (i = start; (i < vec_char_size(vec)) && (((entry) = vec_char_at(vec, i)), 1); i++)
+
+#define vec_char_foreach_stop(vec, entry, i, stop) \
+ for (i = 0; (i < stop) && (((entry) = vec_char_at(vec, i)), 1); i++)
+
+//===------------------------------------------------------------------------===
+// Vector API
+//===------------------------------------------------------------------------===
+static inline vec_char_t * vec_char_alloc(unsigned cap)
+{
+ vec_char_t *p = satoko_alloc(vec_char_t, 1);
+
+ if (cap > 0 && cap < 16)
+ cap = 16;
+ p->size = 0;
+ p->cap = cap;
+ p->data = p->cap ? satoko_alloc(char, p->cap) : NULL;
+ return p;
+}
+
+static inline vec_char_t * vec_char_alloc_exact(unsigned cap)
+{
+ vec_char_t *p = satoko_alloc(vec_char_t, 1);
+
+ cap = 0;
+ p->size = 0;
+ p->cap = cap;
+ p->data = p->cap ? satoko_alloc(char, p->cap ) : NULL;
+ return p;
+}
+
+static inline vec_char_t * vec_char_init(unsigned size, char value)
+{
+ vec_char_t *p = satoko_alloc(vec_char_t, 1);
+
+ p->cap = size;
+ p->size = size;
+ p->data = p->cap ? satoko_alloc(char, p->cap) : NULL;
+ memset(p->data, value, sizeof(char) * p->size);
+ return p;
+}
+
+static inline void vec_char_free(vec_char_t *p)
+{
+ if (p->data != NULL)
+ satoko_free(p->data);
+ satoko_free(p);
+}
+
+static inline unsigned vec_char_size(vec_char_t *p)
+{
+ return p->size;
+}
+
+static inline void vec_char_resize(vec_char_t *p, unsigned new_size)
+{
+ p->size = new_size;
+ if (p->cap >= new_size)
+ return;
+ p->data = satoko_realloc(char, p->data, new_size);
+ assert(p->data != NULL);
+ p->cap = new_size;
+}
+
+static inline void vec_char_shrink(vec_char_t *p, unsigned new_size)
+{
+ assert(p->cap > new_size);
+ p->size = new_size;
+}
+
+static inline void vec_char_reserve(vec_char_t *p, unsigned new_cap)
+{
+ if (p->cap >= new_cap)
+ return;
+ p->data = satoko_realloc(char, p->data, new_cap);
+ assert(p->data != NULL);
+ p->cap = new_cap;
+}
+
+static inline unsigned vec_char_capacity(vec_char_t *p)
+{
+ return p->cap;
+}
+
+static inline int vec_char_empty(vec_char_t *p)
+{
+ return p->size ? 0 : 1;
+}
+
+static inline void vec_char_erase(vec_char_t *p)
+{
+ satoko_free(p->data);
+ p->size = 0;
+ p->cap = 0;
+}
+
+static inline char vec_char_at(vec_char_t *p, unsigned idx)
+{
+ assert(idx >= 0 && idx < p->size);
+ return p->data[idx];
+}
+
+static inline char * vec_char_at_ptr(vec_char_t *p, unsigned idx)
+{
+ assert(idx >= 0 && idx < p->size);
+ return p->data + idx;
+}
+
+static inline char * vec_char_data(vec_char_t *p)
+{
+ assert(p);
+ return p->data;
+}
+
+static inline void vec_char_duplicate(vec_char_t *dest, const vec_char_t *src)
+{
+ assert(dest != NULL && src != NULL);
+ vec_char_resize(dest, src->cap);
+ memcpy(dest->data, src->data, sizeof(char) * src->cap);
+ dest->size = src->size;
+}
+
+static inline void vec_char_copy(vec_char_t *dest, const vec_char_t *src)
+{
+ assert(dest != NULL && src != NULL);
+ vec_char_resize(dest, src->size);
+ memcpy(dest->data, src->data, sizeof(char) * src->size);
+ dest->size = src->size;
+}
+
+static inline void vec_char_push_back(vec_char_t *p, char value)
+{
+ if (p->size == p->cap) {
+ if (p->cap < 16)
+ vec_char_reserve(p, 16);
+ else
+ vec_char_reserve(p, 2 * p->cap);
+ }
+ p->data[p->size] = value;
+ p->size++;
+}
+
+static inline char vec_char_pop_back(vec_char_t *p)
+{
+ assert(p && p->size);
+ return p->data[--p->size];
+}
+
+static inline void vec_char_assign(vec_char_t *p, unsigned idx, char value)
+{
+ assert((idx >= 0) && (idx < vec_char_size(p)));
+ p->data[idx] = value;
+}
+
+static inline void vec_char_insert(vec_char_t *p, unsigned idx, char value)
+{
+ assert((idx >= 0) && (idx < vec_char_size(p)));
+ vec_char_push_back(p, 0);
+ memmove(p->data + idx + 1, p->data + idx, (p->size - idx - 2) * sizeof(char));
+ p->data[idx] = value;
+}
+
+static inline void vec_char_drop(vec_char_t *p, unsigned idx)
+{
+ assert((idx >= 0) && (idx < vec_char_size(p)));
+ memmove(p->data + idx, p->data + idx + 1, (p->size - idx - 1) * sizeof(char));
+ p->size -= 1;
+}
+
+static inline void vec_char_clear(vec_char_t *p)
+{
+ p->size = 0;
+}
+
+static inline int vec_char_asc_compare(const void *p1, const void *p2)
+{
+ const char *pp1 = (const char *)p1;
+ const char *pp2 = (const char *)p2;
+
+ if (*pp1 < *pp2)
+ return -1;
+ if (*pp1 > *pp2)
+ return 1;
+ return 0;
+}
+
+static inline int vec_char_desc_compare(const void *p1, const void *p2)
+{
+ const char *pp1 = (const char *)p1;
+ const char *pp2 = (const char *)p2;
+
+ if (*pp1 > *pp2)
+ return -1;
+ if (*pp1 < *pp2)
+ return 1;
+ return 0;
+}
+
+static inline void vec_char_sort(vec_char_t *p, int ascending)
+{
+ if (ascending)
+ qsort((void *) p->data, p->size, sizeof(char),
+ (int (*)(const void *, const void *)) vec_char_asc_compare);
+ else
+ qsort((void*) p->data, p->size, sizeof(char),
+ (int (*)(const void *, const void *)) vec_char_desc_compare);
+}
+
+
+static inline long vec_char_memory(vec_char_t *p)
+{
+ return p == NULL ? 0 : sizeof(char) * p->cap + sizeof(vec_char_t);
+}
+
+static inline void vec_char_print(vec_char_t* p)
+{
+ assert(p != NULL);
+ fprintf(stdout, "Vector has %u(%u) entries: {", p->size, p->cap);
+ for (unsigned i = 0; i < p->size; i++)
+ fprintf(stdout, " %d", p->data[i]);
+ fprintf(stdout, " }\n");
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__utils__vec__vec_char_h */
diff --git a/src/sat/satoko/utils/vec/vec_dble.h b/src/sat/satoko/utils/vec/vec_dble.h
new file mode 100755
index 00000000..50281c2a
--- /dev/null
+++ b/src/sat/satoko/utils/vec/vec_dble.h
@@ -0,0 +1,246 @@
+//===--- vec_int.h ----------------------------------------------------------===
+//
+// satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__utils__vec__vec_dble_h
+#define satoko__utils__vec__vec_dble_h
+
+#include <assert.h>
+#include <stdio.h>
+#include <string.h>
+
+#include "../mem.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+typedef struct vec_dble_t_ vec_dble_t;
+struct vec_dble_t_ {
+ unsigned cap;
+ unsigned size;
+ double *data;
+};
+
+//===------------------------------------------------------------------------===
+// Vector Macros
+//===------------------------------------------------------------------------===
+#define vec_dble_foreach(vec, entry, i) \
+ for (i = 0; (i < vec->size) && (((entry) = vec_dble_at(vec, i)), 1); i++)
+
+#define vec_dble_foreach_start(vec, entry, i, start) \
+ for (i = start; (i < vec_dble_size(vec)) && (((entry) = vec_dble_at(vec, i)), 1); i++)
+
+#define vec_dble_foreach_stop(vec, entry, i, stop) \
+ for (i = 0; (i < stop) && (((entry) = vec_dble_at(vec, i)), 1); i++)
+
+//===------------------------------------------------------------------------===
+// Vector API
+//===------------------------------------------------------------------------===
+static inline vec_dble_t *vec_dble_alloc(unsigned cap)
+{
+ vec_dble_t* p = satoko_alloc(vec_dble_t, 1);
+
+ if (cap > 0 && cap < 16)
+ cap = 16;
+ p->size = 0;
+ p->cap = cap;
+ p->data = p->cap ? satoko_alloc(double, p->cap) : NULL;
+ return p;
+}
+
+static inline vec_dble_t *vec_dble_alloc_exact(unsigned cap)
+{
+ vec_dble_t* p = satoko_alloc(vec_dble_t, 1);
+
+ p->size = 0;
+ p->cap = cap;
+ p->data = p->cap ? satoko_alloc(double, p->cap) : NULL;
+ return p;
+}
+
+static inline vec_dble_t *vec_dble_init(unsigned size, double value)
+{
+ vec_dble_t* p = satoko_alloc(vec_dble_t, 1);
+
+ p->cap = size;
+ p->size = size;
+ p->data = p->cap ? satoko_alloc(double, p->cap) : NULL;
+ memset(p->data, value, sizeof(double) * p->size);
+ return p;
+}
+
+static inline void vec_dble_free(vec_dble_t *p)
+{
+ if (p->data != NULL)
+ satoko_free(p->data);
+ satoko_free(p);
+}
+
+static inline unsigned vec_dble_size(vec_dble_t *p)
+{
+ return p->size;
+}
+
+static inline void vec_dble_resize(vec_dble_t *p, unsigned new_size)
+{
+ p->size = new_size;
+ if (p->cap >= new_size)
+ return;
+ p->data = satoko_realloc(double, p->data, new_size);
+ assert(p->data != NULL);
+ p->cap = new_size;
+}
+
+static inline void vec_dble_reserve(vec_dble_t *p, unsigned new_cap)
+{
+ if (p->cap >= new_cap)
+ return;
+ p->data = satoko_realloc(double, p->data, new_cap);
+ assert(p->data != NULL);
+ p->cap = new_cap;
+}
+
+static inline unsigned vec_dble_capacity(vec_dble_t *p)
+{
+ return p->cap;
+}
+
+static inline int vec_dble_empty(vec_dble_t *p)
+{
+ return p->size ? 0 : 1;
+}
+
+static inline void vec_dble_erase(vec_dble_t *p)
+{
+ satoko_free(p->data);
+ p->size = 0;
+ p->cap = 0;
+}
+
+static inline double vec_dble_at(vec_dble_t *p, unsigned i)
+{
+ assert(i >= 0 && i < p->size);
+ return p->data[i];
+}
+
+static inline double *vec_dble_at_ptr(vec_dble_t *p, unsigned i)
+{
+ assert(i >= 0 && i < p->size);
+ return p->data + i;
+}
+
+static inline double *vec_dble_data(vec_dble_t *p)
+{
+ assert(p);
+ return p->data;
+}
+
+static inline void vec_dble_duplicate(vec_dble_t *dest, const vec_dble_t *src)
+{
+ assert(dest != NULL && src != NULL);
+ vec_dble_resize(dest, src->cap);
+ memcpy(dest->data, src->data, sizeof(double) * src->cap);
+ dest->size = src->size;
+}
+
+static inline void vec_dble_copy(vec_dble_t *dest, const vec_dble_t *src)
+{
+ assert(dest != NULL && src != NULL);
+ vec_dble_resize(dest, src->size);
+ memcpy(dest->data, src->data, sizeof(double) * src->size);
+ dest->size = src->size;
+}
+
+static inline void vec_dble_push_back(vec_dble_t *p, double value)
+{
+ if (p->size == p->cap) {
+ if (p->cap < 16)
+ vec_dble_reserve(p, 16);
+ else
+ vec_dble_reserve(p, 2 * p->cap);
+ }
+ p->data[p->size] = value;
+ p->size++;
+}
+
+static inline void vec_dble_assign(vec_dble_t *p, unsigned i, double value)
+{
+ assert((i >= 0) && (i < vec_dble_size(p)));
+ p->data[i] = value;
+}
+
+static inline void vec_dble_insert(vec_dble_t *p, unsigned i, double value)
+{
+ assert((i >= 0) && (i < vec_dble_size(p)));
+ vec_dble_push_back(p, 0);
+ memmove(p->data + i + 1, p->data + i, (p->size - i - 2) * sizeof(double));
+ p->data[i] = value;
+}
+
+static inline void vec_dble_drop(vec_dble_t *p, unsigned i)
+{
+ assert((i >= 0) && (i < vec_dble_size(p)));
+ memmove(p->data + i, p->data + i + 1, (p->size - i - 1) * sizeof(double));
+ p->size -= 1;
+}
+
+static inline void vec_dble_clear(vec_dble_t *p)
+{
+ p->size = 0;
+}
+
+static inline int vec_dble_asc_compare(const void *p1, const void *p2)
+{
+ const double *pp1 = (const double *) p1;
+ const double *pp2 = (const double *) p2;
+
+ if (*pp1 < *pp2)
+ return -1;
+ if (*pp1 > *pp2)
+ return 1;
+ return 0;
+}
+
+static inline int vec_dble_desc_compare(const void* p1, const void* p2)
+{
+ const double *pp1 = (const double *) p1;
+ const double *pp2 = (const double *) p2;
+
+ if (*pp1 > *pp2)
+ return -1;
+ if (*pp1 < *pp2)
+ return 1;
+ return 0;
+}
+
+static inline void vec_dble_sort(vec_dble_t* p, int ascending)
+{
+ if (ascending)
+ qsort((void *) p->data, p->size, sizeof(double),
+ (int (*)(const void*, const void*)) vec_dble_asc_compare);
+ else
+ qsort((void *) p->data, p->size, sizeof(double),
+ (int (*)(const void*, const void*)) vec_dble_desc_compare);
+}
+
+static inline long vec_dble_memory(vec_dble_t *p)
+{
+ return p == NULL ? 0 : sizeof(double) * p->cap + sizeof(vec_dble_t);
+}
+
+static inline void vec_dble_print(vec_dble_t *p)
+{
+ unsigned i;
+ assert(p != NULL);
+ fprintf(stdout, "Vector has %u(%u) entries: {", p->size, p->cap);
+ for (i = 0; i < p->size; i++)
+ fprintf(stdout, " %f", p->data[i]);
+ fprintf(stdout, " }\n");
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__utils__vec__vec_dble_h */
diff --git a/src/sat/satoko/utils/vec/vec_int.h b/src/sat/satoko/utils/vec/vec_int.h
new file mode 100755
index 00000000..75c5d134
--- /dev/null
+++ b/src/sat/satoko/utils/vec/vec_int.h
@@ -0,0 +1,240 @@
+//===--- vec_int.h ----------------------------------------------------------===
+//
+// satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__utils__vec__vec_int_h
+#define satoko__utils__vec__vec_int_h
+
+#include <assert.h>
+#include <stdio.h>
+#include <string.h>
+
+#include "../mem.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+typedef struct vec_int_t_ vec_int_t;
+struct vec_int_t_ {
+ unsigned cap;
+ unsigned size;
+ int *data;
+};
+
+//===------------------------------------------------------------------------===
+// Vector Macros
+//===------------------------------------------------------------------------===
+#define vec_int_foreach(vec, entry, i) \
+ for (i = 0; (i < vec->size) && (((entry) = vec_int_at(vec, i)), 1); i++)
+
+#define vec_int_foreach_start(vec, entry, i, start) \
+ for (i = start; (i < vec_int_size(vec)) && (((entry) = vec_int_at(vec, i)), 1); i++)
+
+#define vec_int_foreach_stop(vec, entry, i, stop) \
+ for (i = 0; (i < stop) && (((entry) = vec_int_at(vec, i)), 1); i++)
+
+//===------------------------------------------------------------------------===
+// Vector API
+//===------------------------------------------------------------------------===
+static inline vec_int_t *vec_int_alloc(unsigned cap)
+{
+ vec_int_t* p = satoko_alloc(vec_int_t, 1);
+
+ if (cap > 0 && cap < 16)
+ cap = 16;
+ p->size = 0;
+ p->cap = cap;
+ p->data = p->cap ? satoko_alloc(int, p->cap) : NULL;
+ return p;
+}
+
+static inline vec_int_t *vec_int_alloc_exact(unsigned cap)
+{
+ vec_int_t* p = satoko_alloc(vec_int_t, 1);
+
+ p->size = 0;
+ p->cap = cap;
+ p->data = p->cap ? satoko_alloc(int, p->cap) : NULL;
+ return p;
+}
+
+static inline vec_int_t *vec_int_init(unsigned size, int value)
+{
+ vec_int_t* p = satoko_alloc(vec_int_t, 1);
+
+ p->cap = size;
+ p->size = size;
+ p->data = p->cap ? satoko_alloc(int, p->cap) : NULL;
+ memset(p->data, value, sizeof(int) * p->size);
+ return p;
+}
+
+static inline void vec_int_free(vec_int_t *p)
+{
+ if (p->data != NULL)
+ satoko_free(p->data);
+ satoko_free(p);
+}
+
+static inline unsigned vec_int_size(vec_int_t *p)
+{
+ return p->size;
+}
+
+static inline void vec_int_resize(vec_int_t *p, unsigned new_size)
+{
+ p->size = new_size;
+ if (p->cap >= new_size)
+ return;
+ p->data = satoko_realloc(int, p->data, new_size);
+ assert(p->data != NULL);
+ p->cap = new_size;
+}
+
+static inline void vec_int_reserve(vec_int_t *p, unsigned new_cap)
+{
+ if (p->cap >= new_cap)
+ return;
+ p->data = satoko_realloc(int, p->data, new_cap);
+ assert(p->data != NULL);
+ p->cap = new_cap;
+}
+
+static inline unsigned vec_int_capacity(vec_int_t *p)
+{
+ return p->cap;
+}
+
+static inline int vec_int_empty(vec_int_t *p)
+{
+ return p->size ? 0 : 1;
+}
+
+static inline void vec_int_erase(vec_int_t *p)
+{
+ satoko_free(p->data);
+ p->size = 0;
+ p->cap = 0;
+}
+
+static inline int vec_int_at(vec_int_t *p, unsigned i)
+{
+ assert(i >= 0 && i < p->size);
+ return p->data[i];
+}
+
+static inline int *vec_int_at_ptr(vec_int_t *p, unsigned i)
+{
+ assert(i >= 0 && i < p->size);
+ return p->data + i;
+}
+
+static inline void vec_int_duplicate(vec_int_t *dest, const vec_int_t *src)
+{
+ assert(dest != NULL && src != NULL);
+ vec_int_resize(dest, src->cap);
+ memcpy(dest->data, src->data, sizeof(int) * src->cap);
+ dest->size = src->size;
+}
+
+static inline void vec_int_copy(vec_int_t *dest, const vec_int_t *src)
+{
+ assert(dest != NULL && src != NULL);
+ vec_int_resize(dest, src->size);
+ memcpy(dest->data, src->data, sizeof(int) * src->size);
+ dest->size = src->size;
+}
+
+static inline void vec_int_push_back(vec_int_t *p, int value)
+{
+ if (p->size == p->cap) {
+ if (p->cap < 16)
+ vec_int_reserve(p, 16);
+ else
+ vec_int_reserve(p, 2 * p->cap);
+ }
+ p->data[p->size] = value;
+ p->size++;
+}
+
+static inline void vec_int_assign(vec_int_t *p, unsigned i, int value)
+{
+ assert((i >= 0) && (i < vec_int_size(p)));
+ p->data[i] = value;
+}
+
+static inline void vec_int_insert(vec_int_t *p, unsigned i, int value)
+{
+ assert((i >= 0) && (i < vec_int_size(p)));
+ vec_int_push_back(p, 0);
+ memmove(p->data + i + 1, p->data + i, (p->size - i - 2) * sizeof(int));
+ p->data[i] = value;
+}
+
+static inline void vec_int_drop(vec_int_t *p, unsigned i)
+{
+ assert((i >= 0) && (i < vec_int_size(p)));
+ memmove(p->data + i, p->data + i + 1, (p->size - i - 1) * sizeof(int));
+ p->size -= 1;
+}
+
+static inline void vec_int_clear(vec_int_t *p)
+{
+ p->size = 0;
+}
+
+static inline int vec_int_asc_compare(const void *p1, const void *p2)
+{
+ const int *pp1 = (const int *) p1;
+ const int *pp2 = (const int *) p2;
+
+ if (*pp1 < *pp2)
+ return -1;
+ if (*pp1 > *pp2)
+ return 1;
+ return 0;
+}
+
+static inline int vec_int_desc_compare(const void* p1, const void* p2)
+{
+ const int *pp1 = (const int *) p1;
+ const int *pp2 = (const int *) p2;
+
+ if (*pp1 > *pp2)
+ return -1;
+ if (*pp1 < *pp2)
+ return 1;
+ return 0;
+}
+
+static inline void vec_int_sort(vec_int_t* p, int ascending)
+{
+ if (ascending)
+ qsort((void *) p->data, p->size, sizeof(int),
+ (int (*)(const void*, const void*)) vec_int_asc_compare);
+ else
+ qsort((void *) p->data, p->size, sizeof(int),
+ (int (*)(const void*, const void*)) vec_int_desc_compare);
+}
+
+static inline long vec_int_memory(vec_int_t *p)
+{
+ return p == NULL ? 0 : sizeof(int) * p->cap + sizeof(vec_int_t);
+}
+
+static inline void vec_int_print(vec_int_t *p)
+{
+ unsigned i;
+ assert(p != NULL);
+ fprintf(stdout, "Vector has %u(%u) entries: {", p->size, p->cap);
+ for (i = 0; i < p->size; i++)
+ fprintf(stdout, " %d", p->data[i]);
+ fprintf(stdout, " }\n");
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__utils__vec__vec_int_h */
diff --git a/src/sat/satoko/utils/vec/vec_uint.h b/src/sat/satoko/utils/vec/vec_uint.h
new file mode 100755
index 00000000..e6719ca3
--- /dev/null
+++ b/src/sat/satoko/utils/vec/vec_uint.h
@@ -0,0 +1,268 @@
+//===--- vec_uint.h ---------------------------------------------------------===
+//
+// satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__utils__vec__vec_uint_h
+#define satoko__utils__vec__vec_uint_h
+
+#include <assert.h>
+#include <stdio.h>
+#include <string.h>
+
+#include "../mem.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+typedef struct vec_uint_t_ vec_uint_t;
+struct vec_uint_t_ {
+ unsigned cap;
+ unsigned size;
+ unsigned* data;
+};
+
+//===------------------------------------------------------------------------===
+// Vector Macros
+//===------------------------------------------------------------------------===
+#define vec_uint_foreach(vec, entry, i) \
+ for (i = 0; (i < vec_uint_size(vec)) && (((entry) = vec_uint_at(vec, i)), 1); i++)
+
+#define vec_uint_foreach_start(vec, entry, i, start) \
+ for (i = start; (i < vec_uint_size(vec)) && (((entry) = vec_uint_at(vec, i)), 1); i++)
+
+#define vec_uint_foreach_stop(vec, entry, i, stop) \
+ for (i = 0; (i < stop) && (((entry) = vec_uint_at(vec, i)), 1); i++)
+
+//===------------------------------------------------------------------------===
+// Vector API
+//===------------------------------------------------------------------------===
+static inline vec_uint_t * vec_uint_alloc(unsigned cap)
+{
+ vec_uint_t *p = satoko_alloc(vec_uint_t, 1);
+
+ if (cap > 0 && cap < 16)
+ cap = 16;
+ p->size = 0;
+ p->cap = cap;
+ p->data = p->cap ? satoko_alloc(unsigned, p->cap) : NULL;
+ return p;
+}
+
+static inline vec_uint_t * vec_uint_alloc_exact(unsigned cap)
+{
+ vec_uint_t *p = satoko_alloc(vec_uint_t, 1);
+
+ cap = 0;
+ p->size = 0;
+ p->cap = cap;
+ p->data = p->cap ? satoko_alloc(unsigned, p->cap ) : NULL;
+ return p;
+}
+
+static inline vec_uint_t * vec_uint_init(unsigned size, unsigned value)
+{
+ vec_uint_t *p = satoko_alloc(vec_uint_t, 1);
+
+ p->cap = size;
+ p->size = size;
+ p->data = p->cap ? satoko_alloc(unsigned, p->cap ) : NULL;
+ memset(p->data, value, sizeof(unsigned) * p->size);
+ return p;
+}
+
+static inline void vec_uint_free(vec_uint_t *p)
+{
+ if (p->data != NULL)
+ satoko_free(p->data);
+ satoko_free(p);
+}
+
+static inline unsigned vec_uint_size(vec_uint_t *p)
+{
+ return p->size;
+}
+
+static inline void vec_uint_resize(vec_uint_t *p, unsigned new_size)
+{
+ p->size = new_size;
+ if (p->cap >= new_size)
+ return;
+ p->data = satoko_realloc(unsigned, p->data, new_size);
+ assert(p->data != NULL);
+ p->cap = new_size;
+}
+
+static inline void vec_uint_shrink(vec_uint_t *p, unsigned new_size)
+{
+ assert(p->cap >= new_size);
+ p->size = new_size;
+}
+
+static inline void vec_uint_reserve(vec_uint_t *p, unsigned new_cap)
+{
+ if (p->cap >= new_cap)
+ return;
+ p->data = satoko_realloc(unsigned, p->data, new_cap);
+ assert(p->data != NULL);
+ p->cap = new_cap;
+}
+
+static inline unsigned vec_uint_capacity(vec_uint_t *p)
+{
+ return p->cap;
+}
+
+static inline int vec_uint_empty(vec_uint_t *p)
+{
+ return p->size ? 0 : 1;
+}
+
+static inline void vec_uint_erase(vec_uint_t *p)
+{
+ satoko_free(p->data);
+ p->size = 0;
+ p->cap = 0;
+}
+
+static inline unsigned vec_uint_at(vec_uint_t *p, unsigned idx)
+{
+ assert(idx >= 0 && idx < p->size);
+ return p->data[idx];
+}
+
+static inline unsigned * vec_uint_at_ptr(vec_uint_t *p, unsigned idx)
+{
+ assert(idx >= 0 && idx < p->size);
+ return p->data + idx;
+}
+
+static inline unsigned vec_uint_find(vec_uint_t *p, unsigned entry)
+{
+ unsigned i;
+ for (i = 0; i < p->size; i++)
+ if (p->data[i] == entry)
+ return 1;
+ return 0;
+}
+
+static inline unsigned * vec_uint_data(vec_uint_t *p)
+{
+ assert(p);
+ return p->data;
+}
+
+static inline void vec_uint_duplicate(vec_uint_t *dest, const vec_uint_t *src)
+{
+ assert(dest != NULL && src != NULL);
+ vec_uint_resize(dest, src->cap);
+ memcpy(dest->data, src->data, sizeof(unsigned) * src->cap);
+ dest->size = src->size;
+}
+
+static inline void vec_uint_copy(vec_uint_t *dest, const vec_uint_t *src)
+{
+ assert(dest != NULL && src != NULL);
+ vec_uint_resize(dest, src->size);
+ memcpy(dest->data, src->data, sizeof(unsigned) * src->size);
+ dest->size = src->size;
+}
+
+static inline void vec_uint_push_back(vec_uint_t *p, unsigned value)
+{
+ if (p->size == p->cap) {
+ if (p->cap < 16)
+ vec_uint_reserve(p, 16);
+ else
+ vec_uint_reserve(p, 2 * p->cap);
+ }
+ p->data[p->size] = value;
+ p->size++;
+}
+
+static inline unsigned vec_uint_pop_back(vec_uint_t *p)
+{
+ assert(p && p->size);
+ return p->data[--p->size];
+}
+
+static inline void vec_uint_assign(vec_uint_t *p, unsigned idx, unsigned value)
+{
+ assert((idx >= 0) && (idx < vec_uint_size(p)));
+ p->data[idx] = value;
+}
+
+static inline void vec_uint_insert(vec_uint_t *p, unsigned idx, unsigned value)
+{
+ assert((idx >= 0) && (idx < vec_uint_size(p)));
+ vec_uint_push_back(p, 0);
+ memmove(p->data + idx + 1, p->data + idx, (p->size - idx - 2) * sizeof(unsigned));
+ p->data[idx] = value;
+}
+
+static inline void vec_uint_drop(vec_uint_t *p, unsigned idx)
+{
+ assert((idx >= 0) && (idx < vec_uint_size(p)));
+ memmove(p->data + idx, p->data + idx + 1, (p->size - idx - 1) * sizeof(unsigned));
+ p->size -= 1;
+}
+
+static inline void vec_uint_clear(vec_uint_t *p)
+{
+ p->size = 0;
+}
+
+static inline int vec_uint_asc_compare(const void *p1, const void *p2)
+{
+ const unsigned *pp1 = (const unsigned *) p1;
+ const unsigned *pp2 = (const unsigned *) p2;
+
+ if ( *pp1 < *pp2 )
+ return -1;
+ if ( *pp1 > *pp2 )
+ return 1;
+ return 0;
+}
+
+static inline int vec_uint_desc_compare(const void *p1, const void *p2)
+{
+ const unsigned *pp1 = (const unsigned *) p1;
+ const unsigned *pp2 = (const unsigned *) p2;
+
+ if ( *pp1 > *pp2 )
+ return -1;
+ if ( *pp1 < *pp2 )
+ return 1;
+ return 0;
+}
+
+static inline void vec_uint_sort(vec_uint_t *p, int ascending)
+{
+ if (ascending)
+ qsort((void *) p->data, p->size, sizeof(unsigned),
+ (int (*)(const void *, const void *)) vec_uint_asc_compare);
+ else
+ qsort((void*) p->data, p->size, sizeof(unsigned),
+ (int (*)(const void *, const void *)) vec_uint_desc_compare);
+}
+
+static inline long vec_uint_memory(vec_uint_t *p)
+{
+ return p == NULL ? 0 : sizeof(unsigned) * p->cap + sizeof(vec_uint_t);
+}
+
+static inline void vec_uint_print(vec_uint_t* p)
+{
+ unsigned i;
+ assert(p != NULL);
+ fprintf(stdout, "Vector has %u(%u) entries: {", p->size, p->cap);
+ for (i = 0; i < p->size; i++)
+ fprintf(stdout, " %u", p->data[i]);
+ fprintf(stdout, " }\n");
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__utils__vec__vec_uint_h */
diff --git a/src/sat/satoko/watch_list.h b/src/sat/satoko/watch_list.h
new file mode 100644
index 00000000..f492904a
--- /dev/null
+++ b/src/sat/satoko/watch_list.h
@@ -0,0 +1,152 @@
+//===--- watch_list.h -------------------------------------------------------===
+//
+// satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__watch_list_h
+#define satoko__watch_list_h
+
+#include "utils/mem.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+struct watcher {
+ unsigned cref;
+ unsigned blocker;
+};
+
+struct watch_list {
+ unsigned cap;
+ unsigned size;
+ struct watcher *watchers;
+};
+
+typedef struct vec_wl_t_ vec_wl_t;
+struct vec_wl_t_ {
+ unsigned cap;
+ unsigned size;
+ struct watch_list *watch_lists;
+};
+
+//===------------------------------------------------------------------------===
+// Watch list Macros
+//===------------------------------------------------------------------------===
+#define watch_list_foreach(vec, watch, lit) \
+ for (watch = watch_list_array(vec_wl_at(vec, lit)); \
+ watch < watch_list_array(vec_wl_at(vec, lit)) + watch_list_size(vec_wl_at(vec, lit)); \
+ watch++)
+
+//===------------------------------------------------------------------------===
+// Watch list API
+//===------------------------------------------------------------------------===
+static inline void watch_list_free(struct watch_list *wl)
+{
+ if (wl->watchers)
+ satoko_free(wl->watchers);
+}
+
+static inline unsigned watch_list_size(struct watch_list *wl)
+{
+ return wl->size;
+}
+
+static inline void watch_list_shrink(struct watch_list *wl, unsigned size)
+{
+ assert(size <= wl->size);
+ wl->size = size;
+}
+
+static inline void watch_list_push(struct watch_list *wl, struct watcher w)
+{
+ assert(wl);
+ if (wl->size == wl->cap) {
+ unsigned new_size = (wl->cap < 4) ? 4 : (wl->cap / 2) * 3;
+ struct watcher *watchers =
+ satoko_realloc(struct watcher, wl->watchers, new_size);
+ if (watchers == NULL) {
+ printf("Failed to realloc memory from %.1f MB to %.1f "
+ "MB.\n",
+ 1.0 * wl->cap / (1 << 20),
+ 1.0 * new_size / (1 << 20));
+ fflush(stdout);
+ return;
+ }
+ wl->watchers = watchers;
+ wl->cap = new_size;
+ }
+ wl->watchers[wl->size++] = w;
+}
+
+static inline struct watcher *watch_list_array(struct watch_list *wl)
+{
+ return wl->watchers;
+}
+
+static inline void watch_list_remove(struct watch_list *wl, unsigned cref)
+{
+ struct watcher *watchers = watch_list_array(wl);
+ unsigned i;
+ for (i = 0; watchers[i].cref != cref; i++);
+ assert(i < watch_list_size(wl));
+ memmove((wl->watchers + i), (wl->watchers + i + 1),
+ (wl->size - i - 1) * sizeof(struct watcher));
+ wl->size -= 1;
+}
+
+static inline vec_wl_t *vec_wl_alloc(unsigned cap)
+{
+ vec_wl_t *vec_wl = satoko_alloc(vec_wl_t, 1);
+
+ if (cap == 0)
+ vec_wl->cap = 4;
+ else
+ vec_wl->cap = cap;
+ vec_wl->size = 0;
+ vec_wl->watch_lists = satoko_calloc(
+ struct watch_list, sizeof(struct watch_list) * vec_wl->cap);
+ return vec_wl;
+}
+
+static inline void vec_wl_free(vec_wl_t *vec_wl)
+{
+ for (unsigned i = 0; i < vec_wl->size; i++)
+ watch_list_free(vec_wl->watch_lists + i);
+ satoko_free(vec_wl->watch_lists);
+ satoko_free(vec_wl);
+}
+
+static inline void vec_wl_push(vec_wl_t *vec_wl)
+{
+ if (vec_wl->size == vec_wl->cap) {
+ unsigned new_size =
+ (vec_wl->cap < 4) ? vec_wl->cap * 2 : (vec_wl->cap / 2) * 3;
+
+ vec_wl->watch_lists = satoko_realloc(
+ struct watch_list, vec_wl->watch_lists, new_size);
+ memset(vec_wl->watch_lists + vec_wl->cap, 0,
+ sizeof(struct watch_list) * (new_size - vec_wl->cap));
+ if (vec_wl->watch_lists == NULL) {
+ printf("failed to realloc memory from %.1f mb to %.1f "
+ "mb.\n",
+ 1.0 * vec_wl->cap / (1 << 20),
+ 1.0 * new_size / (1 << 20));
+ fflush(stdout);
+ }
+ vec_wl->cap = new_size;
+ }
+ vec_wl->size++;
+}
+
+static inline struct watch_list *vec_wl_at(vec_wl_t *vec_wl, unsigned idx)
+{
+ assert(idx < vec_wl->cap);
+ assert(idx < vec_wl->size);
+ return vec_wl->watch_lists + idx;
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__watch_list_h */