From cac3967b52ae44fae3962ee9eba456221e0efda3 Mon Sep 17 00:00:00 2001 From: Bruno Schmitt Date: Mon, 6 Feb 2017 11:34:52 -0800 Subject: =?UTF-8?q?Adding=20a=20new=20SAT=20solver=20to=20ABC.=20(Satoko)?= =?UTF-8?q?=20The=20command=20is=20=E2=80=98satoko=E2=80=99?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Makefile | 2 +- src/base/abci/abc.c | 82 ++++- src/sat/satoko/LICENSE | 22 ++ src/sat/satoko/act_clause.h | 80 ++++ src/sat/satoko/act_var.h | 84 +++++ src/sat/satoko/cdb.h | 100 +++++ src/sat/satoko/clause.h | 63 ++++ src/sat/satoko/cnf_reader.c | 156 ++++++++ src/sat/satoko/module.make | 3 + src/sat/satoko/satoko.h | 85 +++++ src/sat/satoko/solver.c | 704 ++++++++++++++++++++++++++++++++++++ src/sat/satoko/solver.h | 242 +++++++++++++ src/sat/satoko/solver_api.c | 310 ++++++++++++++++ src/sat/satoko/types.h | 50 +++ src/sat/satoko/utils/b_queue.h | 81 +++++ src/sat/satoko/utils/heap.h | 181 +++++++++ src/sat/satoko/utils/mem.h | 23 ++ src/sat/satoko/utils/misc.h | 37 ++ src/sat/satoko/utils/sort.h | 65 ++++ src/sat/satoko/utils/vec/vec_char.h | 259 +++++++++++++ src/sat/satoko/utils/vec/vec_dble.h | 246 +++++++++++++ src/sat/satoko/utils/vec/vec_int.h | 240 ++++++++++++ src/sat/satoko/utils/vec/vec_uint.h | 268 ++++++++++++++ src/sat/satoko/watch_list.h | 152 ++++++++ 24 files changed, 3533 insertions(+), 2 deletions(-) create mode 100644 src/sat/satoko/LICENSE create mode 100644 src/sat/satoko/act_clause.h create mode 100644 src/sat/satoko/act_var.h create mode 100644 src/sat/satoko/cdb.h create mode 100644 src/sat/satoko/clause.h create mode 100644 src/sat/satoko/cnf_reader.c create mode 100644 src/sat/satoko/module.make create mode 100644 src/sat/satoko/satoko.h create mode 100644 src/sat/satoko/solver.c create mode 100644 src/sat/satoko/solver.h create mode 100644 src/sat/satoko/solver_api.c create mode 100644 src/sat/satoko/types.h create mode 100644 src/sat/satoko/utils/b_queue.h create mode 100644 src/sat/satoko/utils/heap.h create mode 100755 src/sat/satoko/utils/mem.h create mode 100755 src/sat/satoko/utils/misc.h create mode 100644 src/sat/satoko/utils/sort.h create mode 100644 src/sat/satoko/utils/vec/vec_char.h create mode 100755 src/sat/satoko/utils/vec/vec_dble.h create mode 100755 src/sat/satoko/utils/vec/vec_int.h create mode 100755 src/sat/satoko/utils/vec/vec_uint.h create mode 100644 src/sat/satoko/watch_list.h 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 ); @@ -23302,6 +23305,83 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + 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].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 [] @@ -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 +#include +#include +#include +#include + +#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 +#include +#include +#include + +#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 +#include +#include +#include + +#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 +#include +#include +#include + +#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 + +#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 + +#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 +#include +#include + +#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 +#include +#include + +#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 +#include +#include + +#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 +#include +#include + +#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 */ -- cgit v1.2.3