diff --git a/docs/changelog.rst b/docs/changelog.rst index 6d7a2b9..773319f 100644 --- a/docs/changelog.rst +++ b/docs/changelog.rst @@ -10,6 +10,8 @@ v0.1 (not yet released) - GHack (`solver`) - Glucose 4.1 (`solver`) - ABC bsat2 (`solver`) + - ABC bmcg (`solver`) + - ABC satoko (`solver`) * Types: - Wrapper for variables (`var_type`) - Wrapper for literals (`lit_type`) diff --git a/include/bill/sat/solver.hpp b/include/bill/sat/solver.hpp index 6559cca..31a0b3e 100644 --- a/include/bill/sat/solver.hpp +++ b/include/bill/sat/solver.hpp @@ -31,7 +31,9 @@ #define ABC_USE_NAMESPACE pabc #define ABC_NAMESPACE pabc #define ABC_USE_NO_READLINE +#define SATOKO_NAMESPACE satoko #include "sat_solvers/abc.hpp" +#include "sat_solvers/satoko.hpp" #endif #pragma GCC diagnostic pop #endif @@ -135,6 +137,7 @@ enum class solvers { maple, bsat2, bmcg, + satoko, #endif ghack, }; @@ -909,4 +912,159 @@ class solver { }; #endif +#if !defined(BILL_WINDOWS_PLATFORM) +template<> +class solver { +public: + using solver_type = satoko::satoko_t; + +#pragma region Constructors + solver() + { + solver_ = satoko::satoko_create(); + } + + ~solver() + { + satoko::satoko_destroy(solver_); + solver_ = nullptr; + } + + /* disallow copying */ + solver(solver const&) = delete; + solver& operator=(const solver&) = delete; +#pragma endregion + +#pragma region Modifiers + void restart() + { + satoko::satoko_reset(solver_); + state_ = result::states::undefined; + } + + var_type add_variable() + { + return satoko::satoko_add_variable(solver_, 0); + } + + void add_variables(uint32_t num_variables = 1) + { + for (auto i = 0u; i < num_variables; ++i) { + satoko::satoko_add_variable(solver_, 0); + } + } + + auto add_clause(std::vector::const_iterator it, + std::vector::const_iterator ie) + { + auto counter = 0u; + while (it != ie) { + literals[counter++] = pabc::Abc_Var2Lit(it->variable(), + it->is_complemented()); + ++it; + } + auto const result = satoko::satoko_add_clause(solver_, literals, counter); + state_ = result ? result::states::dirty : result::states::unsatisfiable; + return result; + } + + auto add_clause(std::vector const& clause) + { + return add_clause(clause.begin(), clause.end()); + } + + auto add_clause(lit_type lit) + { + return add_clause(std::vector{lit}); + } + + result get_model() const + { + assert(state_ == result::states::satisfiable); + result::model_type model; + for (auto i = 0u; i < num_variables(); ++i) { + auto const value = satoko::satoko_read_cex_varvalue(solver_, i); + if (value == 1) { + model.emplace_back(lbool_type::true_); + } else { + model.emplace_back(lbool_type::false_); + } + } + return result(model); + } + + result get_result() const + { + assert(state_ != result::states::dirty); + if (state_ == result::states::satisfiable) { + return get_model(); + } else { + return result(); + } + } + + result::states solve(std::vector const& assumptions = {}, + uint32_t conflict_limit = 0) + { + /* special case: empty solver state */ + if (num_variables() == 0u) + return result::states::undefined; + + int result; + if (assumptions.size() > 0u) { + /* solve with assumptions */ + uint32_t counter = 0u; + auto it = assumptions.begin(); + while (it != assumptions.end()) { + literals[counter++] = pabc::Abc_Var2Lit(it->variable(), + it->is_complemented()); + ++it; + } + result = satoko::satoko_solve_assumptions_limit(solver_, literals, counter, + conflict_limit); + } else { + /* solve without assumptions */ + result = satoko::satoko_solve_assumptions_limit(solver_, 0, 0, + conflict_limit); + } + + if (result == satoko::SATOKO_SAT) { + state_ = result::states::satisfiable; + } else if (result == satoko::SATOKO_UNSAT) { + state_ = result::states::unsatisfiable; + } else { + state_ = result::states::undefined; + } + + return state_; + } +#pragma endregion + +#pragma region Properties + uint32_t num_variables() const + { + return satoko::satoko_varnum(solver_); + } + + uint32_t num_clauses() const + { + return satoko::satoko_clausenum(solver_); + } +#pragma endregion + +private: + /*! \brief Backend solver */ + solver_type* solver_ = nullptr; + + /*! \brief Current state of the solver */ + result::states state_ = result::states::undefined; + + /*! \brief Temporary storage for one clause */ + pabc::lit literals[2048]; + + /*! \brief Count the number of variables */ + uint32_t variable_counter_ = 0u; +}; +#endif + } // namespace bill diff --git a/libs/sat_solvers/sat_solvers/satoko.hpp b/libs/sat_solvers/sat_solvers/satoko.hpp new file mode 100644 index 0000000..960ab99 --- /dev/null +++ b/libs/sat_solvers/sat_solvers/satoko.hpp @@ -0,0 +1,1455 @@ +#pragma once + +/*** solver_api.cpp ***/ +//===--- 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 +#include +#include + +#include +SATOKO_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) == SATOKO_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]) == SATOKO_LIT_TRUE) + return SATOKO_OK; + return SATOKO_ERR; +} + +static inline void solver_clean_stats(solver_t *s) +{ + long n_conflicts_all = s->stats.n_conflicts_all; + long n_propagations_all = s->stats.n_propagations_all; + memset(&(s->stats), 0, sizeof(struct satoko_stats)); + s->stats.n_conflicts_all = n_conflicts_all; + s->stats.n_propagations_all = n_propagations_all; +} + +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 : %10ld\n", s->stats.n_conflicts); + printf("decisions : %10ld\n", s->stats.n_decisions); + printf("propagations : %10ld\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); + s->status = SATOKO_OK; + /* 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); + /* 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_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); + if (s->marks) + vec_char_free(s->marks); + satoko_free(s); +} + +void satoko_default_opts(satoko_opts_t *opts) +{ + memset(opts, 0, sizeof(satoko_opts_t)); + opts->verbose = 0; + opts->no_simplify = 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; + opts->learnt_ratio = 0.5; + /* VSIDS heuristic */ + opts->var_act_limit = VAR_ACT_LIMIT; + opts->var_act_rescale = VAR_ACT_RESCALE; + opts->var_decay = 0.95; + opts->clause_decay = (clause_act_t) 0.995; + /* Binary resolution */ + opts->clause_max_sz_bin_resol = 30; + opts->clause_min_lbd_bin_resol = 6; + + opts->garbage_max_ratio = (float) 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_fetch(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_setnvars(solver_t *s, int nvars) +{ + int i; + for (i = satoko_varnum(s); i < nvars; i++) + satoko_add_variable(s, 0); +} + +int satoko_add_variable(solver_t *s, char sign) +{ + unsigned var = vec_act_size(s->activity); + 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, SATOKO_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); + if (s->marks) + vec_char_push_back(s->marks, 0); + return var; +} + +int satoko_add_clause(solver_t *s, int *lits, int size) +{ + unsigned i, j; + unsigned prev_lit; + unsigned max_var; + unsigned cref; + + qsort((void *) lits, size, sizeof(unsigned), stk_uint_compare); + max_var = lit2var(lits[size - 1]); + while (max_var >= vec_act_size(s->activity)) + satoko_add_variable(s, SATOKO_LIT_FALSE); + + vec_uint_clear(s->temp_lits); + j = 0; + prev_lit = UNDEF; + for (i = 0; i < (unsigned)size; i++) { + if ((unsigned)lits[i] == lit_compl(prev_lit) || lit_value(s, lits[i]) == SATOKO_LIT_TRUE) + return SATOKO_OK; + else if ((unsigned)lits[i] != prev_lit && var_value(s, lit2var(lits[i])) == SATOKO_VAR_UNASSING) { + prev_lit = lits[i]; + vec_uint_push_back(s->temp_lits, lits[i]); + } + } + + if (vec_uint_size(s->temp_lits) == 0) { + s->status = SATOKO_ERR; + return SATOKO_ERR; + } if (vec_uint_size(s->temp_lits) == 1) { + solver_enqueue(s, vec_uint_at(s->temp_lits, 0), UNDEF); + return (s->status = (solver_propagate(s) == UNDEF)); + } + if ( 0 ) { + for ( i = 0; i < vec_uint_size(s->temp_lits); i++ ) { + int lit = vec_uint_at(s->temp_lits, i); + printf( "%s%d ", lit&1 ? "!":"", lit>>1 ); + } + printf( "\n" ); + } + cref = solver_clause_create(s, s->temp_lits, 0); + clause_watch(s, cref); + return SATOKO_OK; +} + +void satoko_assump_push(solver_t *s, int lit) +{ + assert(lit2var(lit) < (unsigned)satoko_varnum(s)); + // printf("[Satoko] Push assumption: %d\n", lit); + vec_uint_push_back(s->assumptions, lit); + vec_char_assign(s->polarity, lit2var(lit), lit_polarity(lit)); +} + +void satoko_assump_pop(solver_t *s) +{ + assert(vec_uint_size(s->assumptions) > 0); + // printf("[Satoko] Pop assumption: %d\n", vec_uint_pop_back(s->assumptions)); + vec_uint_pop_back(s->assumptions); + solver_cancel_until(s, vec_uint_size(s->assumptions)); +} + +int satoko_solve(solver_t *s) +{ + int status = SATOKO_UNDEC; + + assert(s); + solver_clean_stats(s); + //if (s->opts.verbose) + // print_opts(s); + if (s->status == SATOKO_ERR) { + printf("Satoko in inconsistent state\n"); + return SATOKO_UNDEC; + } + + if (!s->opts.no_simplify) + if (satoko_simplify(s) != SATOKO_OK) + return SATOKO_UNDEC; + + while (status == SATOKO_UNDEC) { + status = solver_search(s); + if (solver_check_limits(s) == 0 || solver_stop(s)) + break; + if (s->nRuntimeLimit && pabc::Abc_Clock() > s->nRuntimeLimit) + break; + if (s->pFuncStop && s->pFuncStop(s->RunId)) + break; + } + if (s->opts.verbose) + print_stats(s); + + solver_cancel_until(s, vec_uint_size(s->assumptions)); + return status; +} + +int satoko_solve_assumptions(solver_t *s, int * plits, int nlits) +{ + int i, status; + // printf("\n[Satoko] Solve with assumptions.. (%d)\n", vec_uint_size(s->assumptions)); + // printf("[Satoko] + Variables: %d\n", satoko_varnum(s)); + // printf("[Satoko] + Clauses: %d\n", satoko_clausenum(s)); + // printf("[Satoko] + Trail size: %d\n", vec_uint_size(s->trail)); + // printf("[Satoko] + Queue head: %d\n", s->i_qhead); + // solver_debug_check_trail(s); + for ( i = 0; i < nlits; i++ ) + satoko_assump_push( s, plits[i] ); + status = satoko_solve( s ); + for ( i = 0; i < nlits; i++ ) + satoko_assump_pop( s ); + return status; +} + +int satoko_solve_assumptions_limit(satoko_t *s, int * plits, int nlits, int nconflim) +{ + int temp = s->opts.conf_limit, status; + s->opts.conf_limit = nconflim ? s->stats.n_conflicts + nconflim : 0; + status = satoko_solve_assumptions(s, plits, nlits); + s->opts.conf_limit = temp; + return status; +} +int satoko_minimize_assumptions(satoko_t * s, int * plits, int nlits, int nconflim) +{ + int i, nlitsL, nlitsR, nresL, nresR, status; + if ( nlits == 1 ) + { + // since the problem is UNSAT, we try to solve it without assuming the last literal + // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed + status = satoko_solve_assumptions_limit( s, NULL, 0, nconflim ); + return (int)(status != SATOKO_UNSAT); // return 1 if the problem is not UNSAT + } + assert( nlits >= 2 ); + nlitsL = nlits / 2; + nlitsR = nlits - nlitsL; + // assume the left lits + for ( i = 0; i < nlitsL; i++ ) + satoko_assump_push(s, plits[i]); + // solve with these assumptions + status = satoko_solve_assumptions_limit( s, NULL, 0, nconflim ); + if ( status == SATOKO_UNSAT ) // these are enough + { + for ( i = 0; i < nlitsL; i++ ) + satoko_assump_pop(s); + return satoko_minimize_assumptions( s, plits, nlitsL, nconflim ); + } + // these are not enoguh + // solve for the right lits + nresL = nlitsR == 1 ? 1 : satoko_minimize_assumptions( s, plits + nlitsL, nlitsR, nconflim ); + for ( i = 0; i < nlitsL; i++ ) + satoko_assump_pop(s); + // swap literals + vec_uint_clear(s->temp_lits); + for ( i = 0; i < nlitsL; i++ ) + vec_uint_push_back(s->temp_lits, plits[i]); + for ( i = 0; i < nresL; i++ ) + plits[i] = plits[nlitsL+i]; + for ( i = 0; i < nlitsL; i++ ) + plits[nresL+i] = vec_uint_at(s->temp_lits, i); + // assume the right lits + for ( i = 0; i < nresL; i++ ) + satoko_assump_push(s, plits[i]); + // solve with these assumptions + status = satoko_solve_assumptions_limit( s, NULL, 0, nconflim ); + if ( status == SATOKO_UNSAT ) // these are enough + { + for ( i = 0; i < nresL; i++ ) + satoko_assump_pop(s); + return nresL; + } + // solve for the left lits + nresR = nlitsL == 1 ? 1 : satoko_minimize_assumptions( s, plits + nresL, nlitsL, nconflim ); + for ( i = 0; i < nresL; i++ ) + satoko_assump_pop(s); + return nresL + nresR; +} + +int satoko_final_conflict(solver_t *s, int **out) +{ + *out = (int *)vec_uint_data(s->final_conflict); + return vec_uint_size(s->final_conflict); +} + +satoko_stats_t * satoko_stats(satoko_t *s) +{ + return &s->stats; +} + +satoko_opts_t * satoko_options(satoko_t *s) +{ + return &s->opts; +} + +void satoko_bookmark(satoko_t *s) +{ + // printf("[Satoko] Bookmark.\n"); + assert(s->status == SATOKO_OK); + assert(solver_dlevel(s) == 0); + s->book_cl_orig = vec_uint_size(s->originals); + s->book_cl_lrnt = vec_uint_size(s->learnts); + s->book_vars = vec_char_size(s->assigns); + s->book_trail = vec_uint_size(s->trail); + // s->book_qhead = s->i_qhead; + s->opts.no_simplify = 1; +} + +void satoko_unbookmark(satoko_t *s) +{ + // printf("[Satoko] Unbookmark.\n"); + assert(s->status == SATOKO_OK); + s->book_cl_orig = 0; + s->book_cl_lrnt = 0; + s->book_cdb = 0; + s->book_vars = 0; + s->book_trail = 0; + // s->book_qhead = 0; + s->opts.no_simplify = 0; +} + +void satoko_reset(satoko_t *s) +{ + // printf("[Satoko] Reset.\n"); + vec_uint_clear(s->assumptions); + vec_uint_clear(s->final_conflict); + cdb_clear(s->all_clauses); + vec_uint_clear(s->originals); + vec_uint_clear(s->learnts); + vec_wl_clean(s->watches); + vec_act_clear(s->activity); + heap_clear(s->var_order); + vec_uint_clear(s->levels); + vec_uint_clear(s->reasons); + vec_char_clear(s->assigns); + vec_char_clear(s->polarity); + vec_uint_clear(s->trail); + vec_uint_clear(s->trail_lim); + b_queue_clean(s->bq_lbd); + b_queue_clean(s->bq_trail); + vec_uint_clear(s->temp_lits); + vec_char_clear(s->seen); + vec_uint_clear(s->tagged); + vec_uint_clear(s->stack); + vec_uint_clear(s->last_dlevel); + vec_uint_clear(s->stamps); + s->status = SATOKO_OK; + s->var_act_inc = VAR_ACT_INIT_INC; + s->clause_act_inc = CLAUSE_ACT_INIT_INC; + s->n_confl_bfr_reduce = s->opts.n_conf_fst_reduce; + s->RC1 = 1; + s->RC2 = s->opts.n_conf_fst_reduce; + s->book_cl_orig = 0; + s->book_cl_lrnt = 0; + s->book_cdb = 0; + s->book_vars = 0; + s->book_trail = 0; + s->i_qhead = 0; +} + +void satoko_rollback(satoko_t *s) +{ + unsigned i, cref; + unsigned n_originals = vec_uint_size(s->originals) - s->book_cl_orig; + unsigned n_learnts = vec_uint_size(s->learnts) - s->book_cl_lrnt; + struct clause **cl_to_remove; + + // printf("[Satoko] rollback.\n"); + assert(s->status == SATOKO_OK); + assert(solver_dlevel(s) == 0); + if (!s->book_vars) { + satoko_reset(s); + return; + } + cl_to_remove = satoko_alloc(struct clause *, n_originals + n_learnts); + /* Mark clauses */ + vec_uint_foreach_start(s->originals, cref, i, s->book_cl_orig) + cl_to_remove[i] = clause_fetch(s, cref); + vec_uint_foreach_start(s->learnts, cref, i, s->book_cl_lrnt) + cl_to_remove[n_originals + i] = clause_fetch(s, cref); + for (i = 0; i < n_originals + n_learnts; i++) { + clause_unwatch(s, cdb_cref(s->all_clauses, (unsigned *)cl_to_remove[i])); + cl_to_remove[i]->f_mark = 1; + } + satoko_free(cl_to_remove); + vec_uint_shrink(s->originals, s->book_cl_orig); + vec_uint_shrink(s->learnts, s->book_cl_lrnt); + /* Shrink variable related vectors */ + for (i = s->book_vars; i < 2 * vec_char_size(s->assigns); i++) { + vec_wl_at(s->watches, i)->size = 0; + vec_wl_at(s->watches, i)->n_bin = 0; + } + // s->i_qhead = s->book_qhead; + s->watches->size = s->book_vars; + vec_act_shrink(s->activity, s->book_vars); + vec_uint_shrink(s->levels, s->book_vars); + vec_uint_shrink(s->reasons, s->book_vars); + vec_uint_shrink(s->stamps, s->book_vars); + vec_char_shrink(s->assigns, s->book_vars); + vec_char_shrink(s->seen, s->book_vars); + vec_char_shrink(s->polarity, s->book_vars); + solver_rebuild_order(s); + /* Rewind solver and cancel level 0 assignments to the trail */ + solver_cancel_until(s, 0); + vec_uint_shrink(s->trail, s->book_trail); + if (s->book_cdb) + s->all_clauses->size = s->book_cdb; + s->book_cl_orig = 0; + s->book_cl_lrnt = 0; + s->book_vars = 0; + s->book_trail = 0; + // s->book_qhead = 0; +} + +void satoko_mark_cone(satoko_t *s, int * pvars, int n_vars) +{ + int i; + if (!solver_has_marks(s)) + s->marks = vec_char_init(satoko_varnum(s), 0); + for (i = 0; i < n_vars; i++) { + var_set_mark(s, pvars[i]); + vec_sdbl_assign(s->activity, pvars[i], 0); + if (!heap_in_heap(s->var_order, pvars[i])) + heap_insert(s->var_order, pvars[i]); + } +} + +void satoko_unmark_cone(satoko_t *s, int *pvars, int n_vars) +{ + int i; + assert(solver_has_marks(s)); + for (i = 0; i < n_vars; i++) + var_clean_mark(s, pvars[i]); +} + +void satoko_write_dimacs(satoko_t *s, char *fname, int wrt_lrnt, int zero_var) +{ + FILE *file; + unsigned i; + unsigned n_vars = vec_act_size(s->activity); + unsigned n_orig = vec_uint_size(s->originals) + vec_uint_size(s->trail); + unsigned n_lrnts = vec_uint_size(s->learnts); + unsigned *array; + + assert(wrt_lrnt == 0 || wrt_lrnt == 1); + assert(zero_var == 0 || zero_var == 1); + if (fname != NULL) + file = fopen(fname, "w"); + else + file = stdout; + + if (file == NULL) { + printf( "Error: Cannot open output file.\n"); + return; + } + fprintf(file, "p cnf %d %d\n", n_vars, wrt_lrnt ? n_orig + n_lrnts : n_orig); + for (i = 0; i < vec_char_size(s->assigns); i++) { + if ( var_value(s, i) != SATOKO_VAR_UNASSING ) { + if (zero_var) + fprintf(file, "%d\n", var_value(s, i) == SATOKO_LIT_FALSE ? -(int)(i) : i); + else + fprintf(file, "%d 0\n", var_value(s, i) == SATOKO_LIT_FALSE ? -(int)(i + 1) : i + 1); + } + } + array = vec_uint_data(s->originals); + for (i = 0; i < vec_uint_size(s->originals); i++) + clause_dump(file, clause_fetch(s, array[i]), !zero_var); + + if (wrt_lrnt) { + array = vec_uint_data(s->learnts); + for (i = 0; i < n_lrnts; i++) + clause_dump(file, clause_fetch(s, array[i]), !zero_var); + } + fclose(file); + +} + +int satoko_varnum(satoko_t *s) +{ + return vec_char_size(s->assigns); +} + +int satoko_clausenum(satoko_t *s) +{ + return vec_uint_size(s->originals); +} + +int satoko_learntnum(satoko_t *s) +{ + return vec_uint_size(s->learnts); +} + +int satoko_conflictnum(satoko_t *s) +{ + return satoko_stats(s)->n_conflicts_all; +} + +void satoko_set_stop(satoko_t *s, int * pstop) +{ + s->pstop = pstop; +} + +void satoko_set_stop_func(satoko_t *s, int (*fnct)(int)) +{ + s->pFuncStop = fnct; +} + +void satoko_set_runid(satoko_t *s, int id) +{ + s->RunId = id; +} + +int satoko_read_cex_varvalue(satoko_t *s, int ivar) +{ + return satoko_var_polarity(s, ivar) == SATOKO_LIT_TRUE; +} + +pabc::abctime satoko_set_runtime_limit(satoko_t* s, pabc::abctime Limit) +{ + pabc::abctime nRuntimeLimit = s->nRuntimeLimit; + s->nRuntimeLimit = Limit; + return nRuntimeLimit; +} + +char satoko_var_polarity(satoko_t *s, unsigned var) +{ + return vec_char_at(s->polarity, var); +} + +ABC_NAMESPACE_IMPL_END + +/*** solver.cpp ***/ + +//===--- solver.c -----------------------------------------------------------=== +// +// satoko: Satisfiability solver +// +// This file is distributed under the BSD 2-Clause License. +// See LICENSE for details. +// +//===------------------------------------------------------------------------=== +#include +#include +#include +#include + +#include +#include +#include +#include +#include +#include + +#include + +SATOKO_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_fetch(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]) == SATOKO_LIT_FALSE) { + assert(lit_value(s, lits[1]) == SATOKO_LIT_TRUE); + stk_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_compl(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_bin(s->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) == SATOKO_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) { + stk_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) != SATOKO_VAR_UNASSING) { + if (heap_size(s->var_order) == 0) { + next_var = UNDEF; + return UNDEF; + } + next_var = heap_remove_min(s->var_order); + if (solver_has_marks(s) && !var_mark(s, next_var)) + next_var = UNDEF; + } + return var2lit(next_var, satoko_var_polarity(s, next_var)); +} + +static inline void solver_new_decision(solver_t *s, unsigned lit) +{ + if (solver_has_marks(s) && !var_mark(s, lit2var(lit))) + return; + assert(var_value(s, lit2var(lit)) == SATOKO_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_fetch(s, cref); + lits = &(clause->data[0].lit); + + if (p != UNDEF && clause->size == 2 && lit_value(s, lits[0]) == SATOKO_LIT_FALSE) { + assert(lit_value(s, lits[1]) == SATOKO_LIT_TRUE); + stk_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_fetch(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_compl(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_fetch(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)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 > (int)s->opts.fst_block_rst && + b_queue_is_valid(s->bq_lbd) && + ((long)vec_uint_size(s->trail) > (s->opts.b_rst * (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; + + // printf("[Satoko] Analize final..\n"); + // printf("[Satoko] Conflicting lit: %d\n", lit); + vec_uint_clear(s->final_conflict); + 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); i --> vec_uint_at(s->trail_lim, 0);) { + 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_compl(vec_uint_at(s->trail, i))); + } else { + unsigned j; + struct clause *clause = clause_fetch(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); + // solver_debug_check_unsat(s); +} + +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)); + + if (s->book_cdb) + s->book_cdb = 0; + + 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)); + } + + /* Update CREFS */ + 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_start(s->learnts, cref, i, s->book_cl_lrnt) + learnts_cls[i] = clause_fetch(s, cref); + + limit = (unsigned)(n_learnts * s->opts.learnt_ratio); + + 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_fetch(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) +{ + unsigned i; + + if (solver_dlevel(s) <= level) + return; + for (i = vec_uint_size(s->trail); i --> vec_uint_at(s->trail_lim, level);) { + unsigned var = lit2var(vec_uint_at(s->trail, i)); + + vec_char_assign(s->assigns, var, SATOKO_VAR_UNASSING); + vec_uint_assign(s->reasons, var, UNDEF); + 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_bin(s->watches, i, p) { + if (solver_has_marks(s) && !var_mark(s, lit2var(i->blocker))) + continue; + if (var_value(s, lit2var(i->blocker)) == SATOKO_VAR_UNASSING) + solver_enqueue(s, i->blocker, i->cref); + else if (lit_value(s, i->blocker) == SATOKO_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 + ws->n_bin; i < end;) { + struct clause *clause; + struct watcher w; + + if (solver_has_marks(s) && !var_mark(s, lit2var(i->blocker))) { + *j++ = *i++; + continue; + } + if (lit_value(s, i->blocker) == SATOKO_LIT_TRUE) { + *j++ = *i++; + continue; + } + + clause = clause_fetch(s, i->cref); + lits = &(clause->data[0].lit); + + // Make sure the false literal is data[1]: + neg_lit = lit_compl(p); + if (lits[0] == neg_lit) + stk_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]) == SATOKO_LIT_TRUE) + *j++ = w; + else { + /* Look for new watch */ + unsigned k; + for (k = 2; k < clause->size; k++) { + if (lit_value(s, lits[k]) != SATOKO_LIT_FALSE) { + lits[1] = lits[k]; + lits[k] = neg_lit; + watch_list_push(vec_wl_at(s->watches, lit_compl(lits[1])), w, 0); + goto next; + } + } + + *j++ = w; + + /* Clause becomes unit under this assignment */ + if (lit_value(s, lits[0]) == SATOKO_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->stats.n_propagations_all += 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++; + s->stats.n_conflicts_all++; + 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 { + // solver_debug_check_clauses(s); + /* No conflict */ + unsigned next_lit; + + if (solver_rst(s) || solver_check_limits(s) == 0 || solver_stop(s) || + (s->nRuntimeLimit && (s->stats.n_conflicts & 63) == 0 && pabc::Abc_Clock() > s->nRuntimeLimit)) { + b_queue_clean(s->bq_lbd); + solver_cancel_until(s, 0); + return SATOKO_UNDEC; + } + if (!s->opts.no_simplify && solver_dlevel(s) == 0) + satoko_simplify(s); + + /* Reduce the set of learnt clauses */ + if (s->opts.learnt_ratio && vec_uint_size(s->learnts) > 100 && + 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) == SATOKO_LIT_TRUE) { + vec_uint_push_back(s->trail_lim, vec_uint_size(s->trail)); + } else if (lit_value(s, lit) == SATOKO_LIT_FALSE) { + solver_analyze_final(s, lit_compl(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) { + // solver_debug_check(s, SATOKO_SAT); + return SATOKO_SAT; + } + } + solver_new_decision(s, next_lit); + } + } +} + +//===------------------------------------------------------------------------=== +// Debug procedures +//===------------------------------------------------------------------------=== +void solver_debug_check_trail(solver_t *s) +{ + unsigned i; + unsigned *array; + vec_uint_t *trail_dup = vec_uint_alloc(0); + fprintf(stdout, "[Satoko] Checking for trail(%u) inconsistencies...\n", vec_uint_size(s->trail)); + vec_uint_duplicate(trail_dup, s->trail); + vec_uint_sort(trail_dup, 1); + array = vec_uint_data(trail_dup); + for (i = 1; i < vec_uint_size(trail_dup); i++) { + if (array[i - 1] == lit_compl(array[i])) { + fprintf(stdout, "[Satoko] Inconsistent trail: %u %u\n", array[i - 1], array[i]); + assert(0); + return; + } + } + for (i = 0; i < vec_uint_size(trail_dup); i++) { + if (var_value(s, lit2var(array[i])) != lit_polarity(array[i])) { + fprintf(stdout, "[Satoko] Inconsistent trail assignment: %u, %u\n", vec_char_at(s->assigns, lit2var(array[i])), array[i]); + assert(0); + return; + } + } + fprintf(stdout, "[Satoko] Trail OK.\n"); + vec_uint_print(trail_dup); + vec_uint_free(trail_dup); + +} + +void solver_debug_check_clauses(solver_t *s) +{ + unsigned cref, i; + + fprintf(stdout, "[Satoko] Checking clauses (%d)...\n", vec_uint_size(s->originals)); + vec_uint_foreach(s->originals, cref, i) { + unsigned j; + struct clause *clause = clause_fetch(s, cref); + for (j = 0; j < clause->size; j++) { + if (vec_uint_find(s->trail, lit_compl(clause->data[j].lit))) { + continue; + } + break; + } + if (j == clause->size) { + vec_uint_print(s->trail); + fprintf(stdout, "[Satoko] FOUND UNSAT CLAUSE]: (%d) ", i); + clause_print(clause); + assert(0); + } + } + fprintf(stdout, "[Satoko] All SAT - OK\n"); +} + +void solver_debug_check(solver_t *s, int result) +{ + unsigned cref, i; + solver_debug_check_trail(s); + fprintf(stdout, "[Satoko] Checking clauses (%d)... \n", vec_uint_size(s->originals)); + vec_uint_foreach(s->originals, cref, i) { + unsigned j; + struct clause *clause = clause_fetch(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) { + fprintf(stdout, "[Satoko] FOUND UNSAT CLAUSE: (%d) ", i); + clause_print(clause); + assert(0); + } + } + fprintf(stdout, "[Satoko] All SAT - OK\n"); +} + +ABC_NAMESPACE_IMPL_END diff --git a/libs/sat_solvers/sat_solvers/satoko/act_clause.h b/libs/sat_solvers/sat_solvers/satoko/act_clause.h new file mode 100644 index 0000000..362ac56 --- /dev/null +++ b/libs/sat_solvers/sat_solvers/satoko/act_clause.h @@ -0,0 +1,43 @@ +//===--- 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 +SATOKO_NAMESPACE_HEADER_START + +static inline void clause_act_rescale(solver_t *s) +{ + unsigned i, cref; + struct clause *clause; + + vec_uint_foreach(s->learnts, cref, i) { + clause = clause_fetch(s, cref); + clause->data[clause->size].act >>= 10; + } + s->clause_act_inc = stk_uint_max((s->clause_act_inc >> 10), (1 << 11)); +} + +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); +} + +SATOKO_NAMESPACE_HEADER_END +#endif /* satoko__act_clause_h */ diff --git a/libs/sat_solvers/sat_solvers/satoko/act_var.h b/libs/sat_solvers/sat_solvers/satoko/act_var.h new file mode 100644 index 0000000..9fea962 --- /dev/null +++ b/libs/sat_solvers/sat_solvers/satoko/act_var.h @@ -0,0 +1,53 @@ +//===--- 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 "heap.h" +#include "sdbl.h" + +#include +SATOKO_NAMESPACE_HEADER_START + +/** Re-scale the activity value for all variables. + */ +static inline void var_act_rescale(solver_t *s) +{ + unsigned i; + act_t *activity = vec_act_data(s->activity); + + for (i = 0; i < vec_sdbl_size(s->activity); i++) + activity[i] = sdbl_div(activity[i], s->opts.var_act_rescale); + s->var_act_inc = sdbl_div(s->var_act_inc, s->opts.var_act_rescale); +} + +/** Increment the activity value of one variable ('var') + */ +static inline void var_act_bump(solver_t *s, unsigned var) +{ + act_t *activity = vec_act_data(s->activity); + + activity[var] = sdbl_add(activity[var], s->var_act_inc); + if (activity[var] > s->opts.var_act_limit) + 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 = sdbl_mult(s->var_act_inc, double2sdbl(1 /s->opts.var_decay)); +} + +SATOKO_NAMESPACE_HEADER_END +#endif /* satoko__act_var_h */ diff --git a/libs/sat_solvers/sat_solvers/satoko/b_queue.h b/libs/sat_solvers/sat_solvers/satoko/b_queue.h new file mode 100644 index 0000000..0e88cbe --- /dev/null +++ b/libs/sat_solvers/sat_solvers/satoko/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 +SATOKO_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 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) 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; +} + +SATOKO_NAMESPACE_HEADER_END +#endif /* satoko__utils__b_queue_h */ diff --git a/libs/sat_solvers/sat_solvers/satoko/cdb.h b/libs/sat_solvers/sat_solvers/satoko/cdb.h new file mode 100644 index 0000000..945dd69 --- /dev/null +++ b/libs/sat_solvers/sat_solvers/satoko/cdb.h @@ -0,0 +1,106 @@ +//===--- 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 +SATOKO_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 void cdb_clear(struct cdb *p) +{ + p->wasted = 0; + p->size = 0; +} + +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; +} + +SATOKO_NAMESPACE_HEADER_END +#endif /* satoko__cdb_h */ diff --git a/libs/sat_solvers/sat_solvers/satoko/clause.h b/libs/sat_solvers/sat_solvers/satoko/clause.h new file mode 100644 index 0000000..de8d3cb --- /dev/null +++ b/libs/sat_solvers/sat_solvers/satoko/clause.h @@ -0,0 +1,77 @@ +//===--- 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 +SATOKO_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"); +} + +static inline void clause_dump(FILE *file, struct clause *clause, int no_zero_var) +{ + unsigned i; + for (i = 0; i < clause->size; i++) { + int var = (clause->data[i].lit >> 1); + char pol = (clause->data[i].lit & 1); + fprintf(file, "%d ", pol ? -(var + no_zero_var) : (var + no_zero_var)); + } + if (no_zero_var) + fprintf(file, "0\n"); + else + fprintf(file, "\n"); +} + +SATOKO_NAMESPACE_HEADER_END +#endif /* satoko__clause_h */ diff --git a/libs/sat_solvers/sat_solvers/satoko/heap.h b/libs/sat_solvers/sat_solvers/satoko/heap.h new file mode 100644 index 0000000..5325f75 --- /dev/null +++ b/libs/sat_solvers/sat_solvers/satoko/heap.h @@ -0,0 +1,178 @@ +//===--- 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_sdbl.h" +#include "vec/vec_int.h" +#include "vec/vec_uint.h" + +#include +SATOKO_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) +{ + vec_int_clear(p->indices); + 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; +} + +SATOKO_NAMESPACE_HEADER_END +#endif /* satoko__utils__heap_h */ diff --git a/libs/sat_solvers/sat_solvers/satoko/mem.h b/libs/sat_solvers/sat_solvers/satoko/mem.h new file mode 100644 index 0000000..db79a81 --- /dev/null +++ b/libs/sat_solvers/sat_solvers/satoko/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 +SATOKO_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) + +SATOKO_NAMESPACE_HEADER_END +#endif diff --git a/libs/sat_solvers/sat_solvers/satoko/misc.h b/libs/sat_solvers/sat_solvers/satoko/misc.h new file mode 100644 index 0000000..2375d61 --- /dev/null +++ b/libs/sat_solvers/sat_solvers/satoko/misc.h @@ -0,0 +1,35 @@ +//===--- 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 +SATOKO_NAMESPACE_HEADER_START + +#define stk_swap(type, a, b) { type t = a; a = b; b = t; } + +static inline unsigned stk_uint_max(unsigned a, unsigned b) +{ + return a > b ? a : b; +} + +static inline int stk_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; +} + +SATOKO_NAMESPACE_HEADER_END +#endif /* satoko__utils__misc_h */ diff --git a/libs/sat_solvers/sat_solvers/satoko/satoko.h b/libs/sat_solvers/sat_solvers/satoko/satoko.h new file mode 100644 index 0000000..6cf43a1 --- /dev/null +++ b/libs/sat_solvers/sat_solvers/satoko/satoko.h @@ -0,0 +1,148 @@ +//===--- 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 "types.h" +#include +SATOKO_NAMESPACE_HEADER_START + +/** Return valeus */ +enum { + SATOKO_ERR = 0, + SATOKO_OK = 1 +}; + +enum { + SATOKO_UNDEC = 0, /* Undecided */ + SATOKO_SAT = 1, + SATOKO_UNSAT = -1 +}; + +enum { + SATOKO_LIT_FALSE = 1, + SATOKO_LIT_TRUE = 0, + SATOKO_VAR_UNASSING = 3 +}; + +struct solver_t_; +typedef struct solver_t_ satoko_t; + +typedef struct satoko_opts satoko_opts_t; +struct satoko_opts { + /* Limits */ + long conf_limit; /* Limit on the n.of conflicts */ + long prop_limit; /* Limit on the n.of propagations */ + + /* 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 clause databese reduction */ + unsigned inc_reduce; /* Increment to reduce */ + unsigned inc_special_reduce; /* Special increment to reduce */ + unsigned lbd_freeze_clause; + float learnt_ratio; /* Percentage of learned clauses to remove */ + + /* VSIDS heuristic */ + double var_decay; + float clause_decay; + unsigned var_act_rescale; + act_t var_act_limit; + + + /* Binary resolution */ + unsigned clause_max_sz_bin_resol; + unsigned clause_min_lbd_bin_resol; + float garbage_max_ratio; + char verbose; + char no_simplify; +}; + +typedef struct satoko_stats satoko_stats_t; +struct satoko_stats { + unsigned n_starts; + unsigned n_reduce_db; + + long n_decisions; + long n_propagations; + long n_propagations_all; + long n_inspects; + long n_conflicts; + long n_conflicts_all; + + long n_original_lits; + long n_learnt_lits; +}; + + +//===------------------------------------------------------------------------=== +extern satoko_t *satoko_create(void); +extern void satoko_destroy(satoko_t *); +extern void satoko_reset(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_setnvars(satoko_t *, int); +extern int satoko_add_variable(satoko_t *, char); +extern int satoko_add_clause(satoko_t *, int *, int); +extern void satoko_assump_push(satoko_t *s, int); +extern void satoko_assump_pop(satoko_t *s); +extern int satoko_simplify(satoko_t *); +extern int satoko_solve(satoko_t *); +extern int satoko_solve_assumptions(satoko_t *s, int * plits, int nlits); +extern int satoko_solve_assumptions_limit(satoko_t *s, int * plits, int nlits, int nconflim); +extern int satoko_minimize_assumptions(satoko_t *s, int * plits, int nlits, int nconflim); +extern void satoko_mark_cone(satoko_t *, int *, int); +extern void satoko_unmark_cone(satoko_t *, int *, int); + +extern void satoko_rollback(satoko_t *); +extern void satoko_bookmark(satoko_t *); +extern void satoko_unbookmark(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 an array where clause + * is stored. The memory for the clause is managed by the solver. + * - 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 *, int **); + +/* Procedure to dump a DIMACS file. + * - It receives as input the solver, a file name string and two integers. + * - If the file name string is NULL the solver will dump in stdout. + * - The first argument can be either 0 or 1 and is an option to dump learnt + * clauses. (value 1 will dump them). + * - The seccond argument can be either 0 or 1 and is an option to use 0 as a + * variable ID or not. Keep in mind that if 0 is used as an ID the generated + * file will not be a DIMACS. (value 1 will use 0 as ID). + */ +extern void satoko_write_dimacs(satoko_t *, char *, int, int); +extern satoko_stats_t * satoko_stats(satoko_t *); +extern satoko_opts_t * satoko_options(satoko_t *); + +extern int satoko_varnum(satoko_t *); +extern int satoko_clausenum(satoko_t *); +extern int satoko_learntnum(satoko_t *); +extern int satoko_conflictnum(satoko_t *); +extern void satoko_set_stop(satoko_t *, int *); +extern void satoko_set_stop_func(satoko_t *s, int (*fnct)(int)); +extern void satoko_set_runid(satoko_t *, int); +extern int satoko_read_cex_varvalue(satoko_t *, int); +extern pabc::abctime satoko_set_runtime_limit(satoko_t *, pabc::abctime); +extern char satoko_var_polarity(satoko_t *, unsigned); + + +SATOKO_NAMESPACE_HEADER_END +#endif /* satoko__satoko_h */ diff --git a/libs/sat_solvers/sat_solvers/satoko/sdbl.h b/libs/sat_solvers/sat_solvers/satoko/sdbl.h new file mode 100644 index 0000000..9f68605 --- /dev/null +++ b/libs/sat_solvers/sat_solvers/satoko/sdbl.h @@ -0,0 +1,133 @@ +//===--- sdbl.h -------------------------------------------------------------=== +// +// satoko: Satisfiability solver +// +// This file is distributed under the BSD 2-Clause License. +// See LICENSE for details. +// +//===------------------------------------------------------------------------=== +// by Alan Mishchenko +#ifndef satoko__utils__sdbl_h +#define satoko__utils__sdbl_h + +#include +SATOKO_NAMESPACE_HEADER_START +/* + The sdbl_t floating-point number is represented as a 64-bit unsigned int. + The number is (2^expt)*mnt, where expt is a 16-bit exponent and mnt is a + 48-bit mantissa. The decimal point is located between the MSB of mnt, + which is always 1, and the remaining 15 digits of mnt. + + Currently, only positive numbers are represented. + + The range of possible values is [1.0; 2^(2^16-1)*1.111111111111111] + that is, the smallest possible number is 1.0 and the largest possible + number is 2^(---16 ones---).(1.---47 ones---) + + Comparison of numbers can be done by comparing the underlying unsigned ints. + + Only addition, multiplication, and division by 2^n are currently implemented. +*/ + +typedef pabc::word sdbl_t; + +static sdbl_t SDBL_CONST1 = ABC_CONST(0x0000800000000000); +static sdbl_t SDBL_MAX = ~(sdbl_t)(0); + +union ui64_dbl { pabc::word ui64; double dbl; }; + +static inline pabc::word sdbl_exp(sdbl_t a) { return a >> 48; } +static inline pabc::word sdbl_mnt(sdbl_t a) { return (a << 16) >> 16; } + +static inline double sdbl2double(sdbl_t a) { + union ui64_dbl temp; + assert(sdbl_exp(a) < 1023); + temp.ui64 = ((sdbl_exp(a) + 1023) << 52) | (((a << 17) >> 17) << 5); + return temp.dbl; +} + +static inline sdbl_t double2sdbl(double value) +{ + union ui64_dbl temp; + sdbl_t expt, mnt; + assert(value >= 1.0); + temp.dbl = value; + expt = (temp.ui64 >> 52) - 1023; + mnt = SDBL_CONST1 | ((temp.ui64 << 12) >> 17); + return (expt << 48) + mnt; +} + +static inline sdbl_t sdbl_add(sdbl_t a, sdbl_t b) +{ + sdbl_t expt, mnt; + if (a < b) { + a ^= b; + b ^= a; + a ^= b; + } + assert(a >= b); + expt = sdbl_exp(a); + mnt = sdbl_mnt(a) + (sdbl_mnt(b) >> (sdbl_exp(a) - sdbl_exp(b))); + /* Check for carry */ + if (mnt >> 48) { + expt++; + mnt >>= 1; + } + if (expt >> 16) /* overflow */ + return SDBL_MAX; + return (expt << 48) + mnt; +} + +static inline sdbl_t sdbl_mult(sdbl_t a, sdbl_t b) +{ + sdbl_t expt, mnt; + sdbl_t a_mnt, a_mnt_hi, a_mnt_lo; + sdbl_t b_mnt, b_mnt_hi, b_mnt_lo; + if (a < b) { + a ^= b; + b ^= a; + a ^= b; + } + assert( a >= b ); + a_mnt = sdbl_mnt(a); + b_mnt = sdbl_mnt(b); + a_mnt_hi = a_mnt>>32; + b_mnt_hi = b_mnt>>32; + a_mnt_lo = (a_mnt<<32)>>32; + b_mnt_lo = (b_mnt<<32)>>32; + mnt = ((a_mnt_hi * b_mnt_hi) << 17) + + ((a_mnt_lo * b_mnt_lo) >> 47) + + ((a_mnt_lo * b_mnt_hi) >> 15) + + ((a_mnt_hi * b_mnt_lo) >> 15); + expt = sdbl_exp(a) + sdbl_exp(b); + /* Check for carry */ + if (mnt >> 48) { + expt++; + mnt >>= 1; + } + if (expt >> 16) /* overflow */ + return SDBL_MAX; + return (expt << 48) + mnt; +} + +static inline sdbl_t sdbl_div(sdbl_t a, unsigned deg2) +{ + if (sdbl_exp(a) >= (pabc::word)deg2) + return ((sdbl_exp(a) - deg2) << 48) + sdbl_mnt(a); + return SDBL_CONST1; +} + +static inline void sdbl_test() +{ + sdbl_t ten100_ = ABC_CONST(0x014c924d692ca61b); + printf("%f\n", sdbl2double(ten100_)); + printf("%016lX\n", double2sdbl(1 /0.95)); + printf("%016lX\n", SDBL_CONST1); + printf("%f\n", sdbl2double(SDBL_CONST1)); + printf("%f\n", sdbl2double(ABC_CONST(0x000086BCA1AF286B))); + +} + +SATOKO_NAMESPACE_HEADER_END + +#endif /* satoko__utils__sdbl_h */ diff --git a/libs/sat_solvers/sat_solvers/satoko/solver.h b/libs/sat_solvers/sat_solvers/satoko/solver.h new file mode 100644 index 0000000..e21fcca --- /dev/null +++ b/libs/sat_solvers/sat_solvers/satoko/solver.h @@ -0,0 +1,259 @@ +//===--- 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 "b_queue.h" +#include "heap.h" +#include "mem.h" +#include "misc.h" +#include "vec/vec_char.h" +#include "vec/vec_sdbl.h" +#include "vec/vec_uint.h" + +#include +SATOKO_NAMESPACE_HEADER_START + + + +#define UNDEF 0xFFFFFFFF + +typedef struct solver_t_ solver_t; +struct solver_t_ { + int status; + /* 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; + + /* 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 n_props_simplify; /* Remaining number of propagations that + must be made before next execution of + 'simplify()'. */ + + /* 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; + + /* Temporary data used by Search method */ + b_queue_t *bq_trail; + b_queue_t *bq_lbd; + long RC1; + long RC2; + long n_confl_bfr_reduce; + float sum_lbd; + + /* Misc temporary */ + unsigned cur_stamp; /* Used for marking literals and levels of interest */ + vec_uint_t *stamps; /* Multipurpose stamp used to calculate LBD and + * clauses minimization with binary resolution */ + + /* Bookmark */ + unsigned book_cl_orig; /* Bookmark for orignal problem clauses vector */ + unsigned book_cl_lrnt; /* Bookmark for learnt clauses vector */ + unsigned book_cdb; /* Bookmark clause database size */ + unsigned book_vars; /* Bookmark number of variables */ + unsigned book_trail; /* Bookmark trail size */ + // unsigned book_qhead; /* Bookmark propagation queue head */ + + /* Temporary data used for solving cones */ + vec_char_t *marks; + + /* Callbacks to stop the solver */ + pabc::abctime nRuntimeLimit; + int *pstop; + int RunId; + int (*pFuncStop)(int); + + 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 *); + +/* Debuging */ +extern void solver_debug_check(solver_t *, int); +extern void solver_debug_check_trail(solver_t *); +extern void solver_debug_check_clauses(solver_t *); + +//===------------------------------------------------------------------------=== +// 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); +} +static inline int var_mark(solver_t *s, unsigned var) +{ + return (int)vec_char_at(s->marks, var); +} +static inline void var_set_mark(solver_t *s, unsigned var) +{ + vec_char_assign(s->marks, var, 1); +} +static inline void var_clean_mark(solver_t *s, unsigned var) +{ + vec_char_assign(s->marks, var, 0); +} +//===------------------------------------------------------------------------=== +// Inline lit functions +//===------------------------------------------------------------------------=== +static inline unsigned lit_compl(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_char_assign(s->polarity, 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; +} + +static inline int solver_has_marks(satoko_t *s) +{ + return (int)(s->marks != NULL); +} + +static inline int solver_stop(satoko_t *s) +{ + return s->pstop && *s->pstop; +} + +//===------------------------------------------------------------------------=== +// Inline clause functions +//===------------------------------------------------------------------------=== +static inline struct clause *clause_fetch(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; + watch_list_push(vec_wl_at(s->watches, lit_compl(clause->data[0].lit)), w1, (clause->size == 2)); + watch_list_push(vec_wl_at(s->watches, lit_compl(clause->data[1].lit)), w2, (clause->size == 2)); +} + +static inline void clause_unwatch(solver_t *s, unsigned cref) +{ + struct clause *clause = cdb_handler(s->all_clauses, cref); + watch_list_remove(vec_wl_at(s->watches, lit_compl(clause->data[0].lit)), cref, (clause->size == 2)); + watch_list_remove(vec_wl_at(s->watches, lit_compl(clause->data[1].lit)), cref, (clause->size == 2)); +} + +SATOKO_NAMESPACE_HEADER_END +#endif /* satoko__solver_h */ diff --git a/libs/sat_solvers/sat_solvers/satoko/sort.h b/libs/sat_solvers/sat_solvers/satoko/sort.h new file mode 100644 index 0000000..7a58280 --- /dev/null +++ b/libs/sat_solvers/sat_solvers/satoko/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 +SATOKO_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); + } +} + +SATOKO_NAMESPACE_HEADER_END +#endif /* satoko__utils__sort_h */ diff --git a/libs/sat_solvers/sat_solvers/satoko/types.h b/libs/sat_solvers/sat_solvers/satoko/types.h new file mode 100644 index 0000000..4edfcd2 --- /dev/null +++ b/libs/sat_solvers/sat_solvers/satoko/types.h @@ -0,0 +1,39 @@ +//===--- 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 "sdbl.h" +#include "vec/vec_sdbl.h" + +#include +SATOKO_NAMESPACE_HEADER_START + +/* In Satoko ABC version this file is useless */ + +#define VAR_ACT_INIT_INC SDBL_CONST1 +#define VAR_ACT_LIMIT ABC_CONST(0x014c924d692ca61b) +#define VAR_ACT_RESCALE 200 +typedef sdbl_t act_t; +typedef vec_sdbl_t vec_act_t ; +#define vec_act_alloc(size) vec_sdbl_alloc(size) +#define vec_act_free(vec) vec_sdbl_free(vec) +#define vec_act_size(vec) vec_sdbl_size(vec) +#define vec_act_data(vec) vec_sdbl_data(vec) +#define vec_act_clear(vec) vec_sdbl_clear(vec) +#define vec_act_shrink(vec, size) vec_sdbl_shrink(vec, size) +#define vec_act_at(vec, idx) vec_sdbl_at(vec, idx) +#define vec_act_push_back(vec, value) vec_sdbl_push_back(vec, value) + + +#define CLAUSE_ACT_INIT_INC (1 << 11) +typedef unsigned clause_act_t; + +SATOKO_NAMESPACE_HEADER_END +#endif /* satoko__types_h */ diff --git a/libs/sat_solvers/sat_solvers/satoko/vec/vec_char.h b/libs/sat_solvers/sat_solvers/satoko/vec/vec_char.h new file mode 100644 index 0000000..3f5737c --- /dev/null +++ b/libs/sat_solvers/sat_solvers/satoko/vec/vec_char.h @@ -0,0 +1,260 @@ +//===--- 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 +SATOKO_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) +{ + 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"); +} + +SATOKO_NAMESPACE_HEADER_END +#endif /* satoko__utils__vec__vec_char_h */ diff --git a/libs/sat_solvers/sat_solvers/satoko/vec/vec_flt.h b/libs/sat_solvers/sat_solvers/satoko/vec/vec_flt.h new file mode 100644 index 0000000..47f2273 --- /dev/null +++ b/libs/sat_solvers/sat_solvers/satoko/vec/vec_flt.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_flt_h +#define satoko__utils__vec__vec_flt_h + +#include +#include +#include + +#include "../mem.h" + +#include "misc/util/abc_global.h" +SATOKO_NAMESPACE_HEADER_START + +typedef struct vec_flt_t_ vec_flt_t; +struct vec_flt_t_ { + unsigned cap; + unsigned size; + float *data; +}; + +//===------------------------------------------------------------------------=== +// Vector Macros +//===------------------------------------------------------------------------=== +#define vec_flt_foreach(vec, entry, i) \ + for (i = 0; (i < vec->size) && (((entry) = vec_flt_at(vec, i)), 1); i++) + +#define vec_flt_foreach_start(vec, entry, i, start) \ + for (i = start; (i < vec_flt_size(vec)) && (((entry) = vec_flt_at(vec, i)), 1); i++) + +#define vec_flt_foreach_stop(vec, entry, i, stop) \ + for (i = 0; (i < stop) && (((entry) = vec_flt_at(vec, i)), 1); i++) + +//===------------------------------------------------------------------------=== +// Vector API +//===------------------------------------------------------------------------=== +static inline vec_flt_t *vec_flt_alloc(unsigned cap) +{ + vec_flt_t* p = satoko_alloc(vec_flt_t, 1); + + if (cap > 0 && cap < 16) + cap = 16; + p->size = 0; + p->cap = cap; + p->data = p->cap ? satoko_alloc(float, p->cap) : NULL; + return p; +} + +static inline vec_flt_t *vec_flt_alloc_exact(unsigned cap) +{ + vec_flt_t* p = satoko_alloc(vec_flt_t, 1); + + p->size = 0; + p->cap = cap; + p->data = p->cap ? satoko_alloc(float, p->cap) : NULL; + return p; +} + +static inline vec_flt_t *vec_flt_init(unsigned size, float value) +{ + vec_flt_t* p = satoko_alloc(vec_flt_t, 1); + + p->cap = size; + p->size = size; + p->data = p->cap ? satoko_alloc(float, p->cap) : NULL; + memset(p->data, value, sizeof(float) * p->size); + return p; +} + +static inline void vec_flt_free(vec_flt_t *p) +{ + if (p->data != NULL) + satoko_free(p->data); + satoko_free(p); +} + +static inline unsigned vec_flt_size(vec_flt_t *p) +{ + return p->size; +} + +static inline void vec_flt_resize(vec_flt_t *p, unsigned new_size) +{ + p->size = new_size; + if (p->cap >= new_size) + return; + p->data = satoko_realloc(float, p->data, new_size); + assert(p->data != NULL); + p->cap = new_size; +} + +static inline void vec_flt_reserve(vec_flt_t *p, unsigned new_cap) +{ + if (p->cap >= new_cap) + return; + p->data = satoko_realloc(float, p->data, new_cap); + assert(p->data != NULL); + p->cap = new_cap; +} + +static inline unsigned vec_flt_capacity(vec_flt_t *p) +{ + return p->cap; +} + +static inline int vec_flt_empty(vec_flt_t *p) +{ + return p->size ? 0 : 1; +} + +static inline void vec_flt_erase(vec_flt_t *p) +{ + satoko_free(p->data); + p->size = 0; + p->cap = 0; +} + +static inline float vec_flt_at(vec_flt_t *p, unsigned i) +{ + assert(i >= 0 && i < p->size); + return p->data[i]; +} + +static inline float *vec_flt_at_ptr(vec_flt_t *p, unsigned i) +{ + assert(i >= 0 && i < p->size); + return p->data + i; +} + +static inline float *vec_flt_data(vec_flt_t *p) +{ + assert(p); + return p->data; +} + +static inline void vec_flt_duplicate(vec_flt_t *dest, const vec_flt_t *src) +{ + assert(dest != NULL && src != NULL); + vec_flt_resize(dest, src->cap); + memcpy(dest->data, src->data, sizeof(float) * src->cap); + dest->size = src->size; +} + +static inline void vec_flt_copy(vec_flt_t *dest, const vec_flt_t *src) +{ + assert(dest != NULL && src != NULL); + vec_flt_resize(dest, src->size); + memcpy(dest->data, src->data, sizeof(float) * src->size); + dest->size = src->size; +} + +static inline void vec_flt_push_back(vec_flt_t *p, float value) +{ + if (p->size == p->cap) { + if (p->cap < 16) + vec_flt_reserve(p, 16); + else + vec_flt_reserve(p, 2 * p->cap); + } + p->data[p->size] = value; + p->size++; +} + +static inline void vec_flt_assign(vec_flt_t *p, unsigned i, float value) +{ + assert((i >= 0) && (i < vec_flt_size(p))); + p->data[i] = value; +} + +static inline void vec_flt_insert(vec_flt_t *p, unsigned i, float value) +{ + assert((i >= 0) && (i < vec_flt_size(p))); + vec_flt_push_back(p, 0); + memmove(p->data + i + 1, p->data + i, (p->size - i - 2) * sizeof(float)); + p->data[i] = value; +} + +static inline void vec_flt_drop(vec_flt_t *p, unsigned i) +{ + assert((i >= 0) && (i < vec_flt_size(p))); + memmove(p->data + i, p->data + i + 1, (p->size - i - 1) * sizeof(float)); + p->size -= 1; +} + +static inline void vec_flt_clear(vec_flt_t *p) +{ + p->size = 0; +} + +static inline int vec_flt_asc_compare(const void *p1, const void *p2) +{ + const float *pp1 = (const float *) p1; + const float *pp2 = (const float *) p2; + + if (*pp1 < *pp2) + return -1; + if (*pp1 > *pp2) + return 1; + return 0; +} + +static inline int vec_flt_desc_compare(const void* p1, const void* p2) +{ + const float *pp1 = (const float *) p1; + const float *pp2 = (const float *) p2; + + if (*pp1 > *pp2) + return -1; + if (*pp1 < *pp2) + return 1; + return 0; +} + +static inline void vec_flt_sort(vec_flt_t* p, int ascending) +{ + if (ascending) + qsort((void *) p->data, p->size, sizeof(float), + (int (*)(const void*, const void*)) vec_flt_asc_compare); + else + qsort((void *) p->data, p->size, sizeof(float), + (int (*)(const void*, const void*)) vec_flt_desc_compare); +} + +static inline long vec_flt_memory(vec_flt_t *p) +{ + return p == NULL ? 0 : sizeof(float) * p->cap + sizeof(vec_flt_t); +} + +static inline void vec_flt_print(vec_flt_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"); +} + +SATOKO_NAMESPACE_HEADER_END +#endif /* satoko__utils__vec__vec_flt_h */ diff --git a/libs/sat_solvers/sat_solvers/satoko/vec/vec_int.h b/libs/sat_solvers/sat_solvers/satoko/vec/vec_int.h new file mode 100644 index 0000000..b142405 --- /dev/null +++ b/libs/sat_solvers/sat_solvers/satoko/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 +SATOKO_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"); +} + +SATOKO_NAMESPACE_HEADER_END +#endif /* satoko__utils__vec__vec_int_h */ diff --git a/libs/sat_solvers/sat_solvers/satoko/vec/vec_sdbl.h b/libs/sat_solvers/sat_solvers/satoko/vec/vec_sdbl.h new file mode 100644 index 0000000..3457d68 --- /dev/null +++ b/libs/sat_solvers/sat_solvers/satoko/vec/vec_sdbl.h @@ -0,0 +1,253 @@ +//===--- 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_sdbl_h +#define satoko__utils__vec__vec_sdbl_h + +#include +#include +#include + +#include "../mem.h" +#include "../sdbl.h" + +#include +SATOKO_NAMESPACE_HEADER_START + +typedef struct vec_sdbl_t_ vec_sdbl_t; +struct vec_sdbl_t_ { + unsigned cap; + unsigned size; + sdbl_t *data; +}; + +//===------------------------------------------------------------------------=== +// Vector Macros +//===------------------------------------------------------------------------=== +#define vec_sdbl_foreach(vec, entry, i) \ + for (i = 0; (i < vec->size) && (((entry) = vec_sdbl_at(vec, i)), 1); i++) + +#define vec_sdbl_foreach_start(vec, entry, i, start) \ + for (i = start; (i < vec_sdbl_size(vec)) && (((entry) = vec_sdbl_at(vec, i)), 1); i++) + +#define vec_sdbl_foreach_stop(vec, entry, i, stop) \ + for (i = 0; (i < stop) && (((entry) = vec_sdbl_at(vec, i)), 1); i++) + +//===------------------------------------------------------------------------=== +// Vector API +//===------------------------------------------------------------------------=== +static inline vec_sdbl_t *vec_sdbl_alloc(unsigned cap) +{ + vec_sdbl_t* p = satoko_alloc(vec_sdbl_t, 1); + + if (cap > 0 && cap < 16) + cap = 16; + p->size = 0; + p->cap = cap; + p->data = p->cap ? satoko_alloc(sdbl_t, p->cap) : NULL; + return p; +} + +static inline vec_sdbl_t *vec_sdbl_alloc_exact(unsigned cap) +{ + vec_sdbl_t* p = satoko_alloc(vec_sdbl_t, 1); + + p->size = 0; + p->cap = cap; + p->data = p->cap ? satoko_alloc(sdbl_t, p->cap) : NULL; + return p; +} + +static inline vec_sdbl_t *vec_sdbl_init(unsigned size, sdbl_t value) +{ + vec_sdbl_t* p = satoko_alloc(vec_sdbl_t, 1); + + p->cap = size; + p->size = size; + p->data = p->cap ? satoko_alloc(sdbl_t, p->cap) : NULL; + memset(p->data, value, sizeof(sdbl_t) * p->size); + return p; +} + +static inline void vec_sdbl_free(vec_sdbl_t *p) +{ + if (p->data != NULL) + satoko_free(p->data); + satoko_free(p); +} + +static inline unsigned vec_sdbl_size(vec_sdbl_t *p) +{ + return p->size; +} + +static inline void vec_sdbl_shrink(vec_sdbl_t *p, unsigned new_size) +{ + assert(new_size <= p->cap); + p->size = new_size; +} + +static inline void vec_sdbl_resize(vec_sdbl_t *p, unsigned new_size) +{ + p->size = new_size; + if (p->cap >= new_size) + return; + p->data = satoko_realloc(sdbl_t, p->data, new_size); + assert(p->data != NULL); + p->cap = new_size; +} + +static inline void vec_sdbl_reserve(vec_sdbl_t *p, unsigned new_cap) +{ + if (p->cap >= new_cap) + return; + p->data = satoko_realloc(sdbl_t, p->data, new_cap); + assert(p->data != NULL); + p->cap = new_cap; +} + +static inline unsigned vec_sdbl_capacity(vec_sdbl_t *p) +{ + return p->cap; +} + +static inline int vec_sdbl_empty(vec_sdbl_t *p) +{ + return p->size ? 0 : 1; +} + +static inline void vec_sdbl_erase(vec_sdbl_t *p) +{ + satoko_free(p->data); + p->size = 0; + p->cap = 0; +} + +static inline sdbl_t vec_sdbl_at(vec_sdbl_t *p, unsigned i) +{ + assert(i >= 0 && i < p->size); + return p->data[i]; +} + +static inline sdbl_t *vec_sdbl_at_ptr(vec_sdbl_t *p, unsigned i) +{ + assert(i >= 0 && i < p->size); + return p->data + i; +} + +static inline sdbl_t *vec_sdbl_data(vec_sdbl_t *p) +{ + assert(p); + return p->data; +} + +static inline void vec_sdbl_duplicate(vec_sdbl_t *dest, const vec_sdbl_t *src) +{ + assert(dest != NULL && src != NULL); + vec_sdbl_resize(dest, src->cap); + memcpy(dest->data, src->data, sizeof(sdbl_t) * src->cap); + dest->size = src->size; +} + +static inline void vec_sdbl_copy(vec_sdbl_t *dest, const vec_sdbl_t *src) +{ + assert(dest != NULL && src != NULL); + vec_sdbl_resize(dest, src->size); + memcpy(dest->data, src->data, sizeof(sdbl_t) * src->size); + dest->size = src->size; +} + +static inline void vec_sdbl_push_back(vec_sdbl_t *p, sdbl_t value) +{ + if (p->size == p->cap) { + if (p->cap < 16) + vec_sdbl_reserve(p, 16); + else + vec_sdbl_reserve(p, 2 * p->cap); + } + p->data[p->size] = value; + p->size++; +} + +static inline void vec_sdbl_assign(vec_sdbl_t *p, unsigned i, sdbl_t value) +{ + assert((i >= 0) && (i < vec_sdbl_size(p))); + p->data[i] = value; +} + +static inline void vec_sdbl_insert(vec_sdbl_t *p, unsigned i, sdbl_t value) +{ + assert((i >= 0) && (i < vec_sdbl_size(p))); + vec_sdbl_push_back(p, 0); + memmove(p->data + i + 1, p->data + i, (p->size - i - 2) * sizeof(sdbl_t)); + p->data[i] = value; +} + +static inline void vec_sdbl_drop(vec_sdbl_t *p, unsigned i) +{ + assert((i >= 0) && (i < vec_sdbl_size(p))); + memmove(p->data + i, p->data + i + 1, (p->size - i - 1) * sizeof(sdbl_t)); + p->size -= 1; +} + +static inline void vec_sdbl_clear(vec_sdbl_t *p) +{ + p->size = 0; +} + +static inline int vec_sdbl_asc_compare(const void *p1, const void *p2) +{ + const sdbl_t *pp1 = (const sdbl_t *) p1; + const sdbl_t *pp2 = (const sdbl_t *) p2; + + if (*pp1 < *pp2) + return -1; + if (*pp1 > *pp2) + return 1; + return 0; +} + +static inline int vec_sdbl_desc_compare(const void* p1, const void* p2) +{ + const sdbl_t *pp1 = (const sdbl_t *) p1; + const sdbl_t *pp2 = (const sdbl_t *) p2; + + if (*pp1 > *pp2) + return -1; + if (*pp1 < *pp2) + return 1; + return 0; +} + +static inline void vec_sdbl_sort(vec_sdbl_t* p, int ascending) +{ + if (ascending) + qsort((void *) p->data, p->size, sizeof(sdbl_t), + (int (*)(const void*, const void*)) vec_sdbl_asc_compare); + else + qsort((void *) p->data, p->size, sizeof(sdbl_t), + (int (*)(const void*, const void*)) vec_sdbl_desc_compare); +} + +static inline long vec_sdbl_memory(vec_sdbl_t *p) +{ + return p == NULL ? 0 : sizeof(sdbl_t) * p->cap + sizeof(vec_sdbl_t); +} + +static inline void vec_sdbl_print(vec_sdbl_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", sdbl2double(p->data[i])); + fprintf(stdout, " }\n"); +} + +SATOKO_NAMESPACE_HEADER_END +#endif /* satoko__utils__vec__vec_sdbl_h */ diff --git a/libs/sat_solvers/sat_solvers/satoko/vec/vec_uint.h b/libs/sat_solvers/sat_solvers/satoko/vec/vec_uint.h new file mode 100644 index 0000000..0d0b3d0 --- /dev/null +++ b/libs/sat_solvers/sat_solvers/satoko/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 +SATOKO_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"); +} + +SATOKO_NAMESPACE_HEADER_END +#endif /* satoko__utils__vec__vec_uint_h */ diff --git a/libs/sat_solvers/sat_solvers/satoko/watch_list.h b/libs/sat_solvers/sat_solvers/satoko/watch_list.h new file mode 100644 index 0000000..04ae65e --- /dev/null +++ b/libs/sat_solvers/sat_solvers/satoko/watch_list.h @@ -0,0 +1,203 @@ +//===--- 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 "mem.h" +#include "misc.h" + +#include +SATOKO_NAMESPACE_HEADER_START + +struct watcher { + unsigned cref; + unsigned blocker; +}; + +struct watch_list { + unsigned cap; + unsigned size; + unsigned n_bin; + 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++) + +#define watch_list_foreach_bin(vec, watch, lit) \ + for (watch = watch_list_array(vec_wl_at(vec, lit)); \ + watch < watch_list_array(vec_wl_at(vec, lit)) + vec_wl_at(vec, lit)->n_bin; \ + 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_grow(struct watch_list *wl) +{ + 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; +} + +static inline void watch_list_push(struct watch_list *wl, struct watcher w, unsigned is_bin) +{ + assert(wl); + if (wl->size == wl->cap) + watch_list_grow(wl); + wl->watchers[wl->size++] = w; + if (is_bin && wl->size > wl->n_bin) { + stk_swap(struct watcher, wl->watchers[wl->n_bin], wl->watchers[wl->size - 1]); + wl->n_bin++; + } +} + +static inline struct watcher *watch_list_array(struct watch_list *wl) +{ + return wl->watchers; +} + +/* TODO: I still have mixed feelings if this change should be done, keeping the + * old code commented after it. */ +static inline void watch_list_remove(struct watch_list *wl, unsigned cref, unsigned is_bin) +{ + struct watcher *watchers = watch_list_array(wl); + unsigned i; + if (is_bin) { + for (i = 0; watchers[i].cref != cref; i++); + assert(i < watch_list_size(wl)); + wl->n_bin--; + memmove((wl->watchers + i), (wl->watchers + i + 1), + (wl->size - i - 1) * sizeof(struct watcher)); + } else { + for (i = wl->n_bin; watchers[i].cref != cref; i++); + assert(i < watch_list_size(wl)); + stk_swap(struct watcher, wl->watchers[i], wl->watchers[wl->size - 1]); + } + wl->size -= 1; +} + +/* +static inline void watch_list_remove(struct watch_list *wl, unsigned cref, unsigned is_bin) +{ + struct watcher *watchers = watch_list_array(wl); + unsigned i; + if (is_bin) { + for (i = 0; watchers[i].cref != cref; i++); + wl->n_bin--; + } else + for (i = wl->n_bin; 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) +{ + unsigned i; + for (i = 0; i < vec_wl->cap; i++) + watch_list_free(vec_wl->watch_lists + i); + satoko_free(vec_wl->watch_lists); + satoko_free(vec_wl); +} + +static inline void vec_wl_clean(vec_wl_t *vec_wl) +{ + unsigned i; + for (i = 0; i < vec_wl->size; i++) { + vec_wl->watch_lists[i].size = 0; + vec_wl->watch_lists[i].n_bin = 0; + } + vec_wl->size = 0; +} + +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; +} + +SATOKO_NAMESPACE_HEADER_END +#endif /* satoko__watch_list_h */ diff --git a/tests/sat/sat.cpp b/tests/sat/sat.cpp index 3c9e43a..c152c88 100644 --- a/tests/sat/sat.cpp +++ b/tests/sat/sat.cpp @@ -17,7 +17,7 @@ using namespace bill; #else #define SOLVER_TYPES \ solver, solver, solver, \ - solver, solver + solver, solver, solver #endif TEMPLATE_TEST_CASE("Simple SAT", "[sat][template]", SOLVER_TYPES)