satoko.h File Reference

#include "types.h"
#include "misc/util/abc_global.h"

Include dependency graph for satoko.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	satoko_opts
struct	satoko_stats

Typedefs
typedef struct solver_t_	satoko_t
typedef struct satoko_opts	satoko_opts_t
typedef struct satoko_stats	satoko_stats_t

Enumerations
enum	{ SATOKO_ERR = 0 , SATOKO_OK = 1 }
enum	{ SATOKO_UNDEC = 0 , SATOKO_SAT = 1 , SATOKO_UNSAT = -1 }
enum	{ SATOKO_LIT_FALSE = 1 , SATOKO_LIT_TRUE = 0 , SATOKO_VAR_UNASSING = 3 }

Functions
satoko_t *	satoko_create (void)
void	satoko_destroy (satoko_t *)
void	satoko_reset (satoko_t *)
void	satoko_default_opts (satoko_opts_t *)
void	satoko_configure (satoko_t *, satoko_opts_t *)
int	satoko_parse_dimacs (char *, satoko_t **)
void	satoko_setnvars (satoko_t *, int)
int	satoko_add_variable (satoko_t *, char)
int	satoko_add_clause (satoko_t *, int *, int)
void	satoko_assump_push (satoko_t *s, int)
void	satoko_assump_pop (satoko_t *s)
int	satoko_simplify (satoko_t *)
int	satoko_solve (satoko_t *)
int	satoko_solve_assumptions (satoko_t *s, int *plits, int nlits)
int	satoko_solve_assumptions_limit (satoko_t *s, int *plits, int nlits, int nconflim)
int	satoko_minimize_assumptions (satoko_t *s, int *plits, int nlits, int nconflim)
void	satoko_mark_cone (satoko_t *, int *, int)
void	satoko_unmark_cone (satoko_t *, int *, int)
void	satoko_rollback (satoko_t *)
void	satoko_bookmark (satoko_t *)
void	satoko_unbookmark (satoko_t *)
int	satoko_final_conflict (satoko_t *, int **)
void	satoko_write_dimacs (satoko_t *, char *, int, int)
satoko_stats_t *	satoko_stats (satoko_t *)
satoko_opts_t *	satoko_options (satoko_t *)
int	satoko_varnum (satoko_t *)
int	satoko_clausenum (satoko_t *)
int	satoko_learntnum (satoko_t *)
int	satoko_conflictnum (satoko_t *)
void	satoko_set_stop (satoko_t *, int *)
void	satoko_set_stop_func (satoko_t *s, int(*fnct)(int))
void	satoko_set_runid (satoko_t *, int)
int	satoko_read_cex_varvalue (satoko_t *, int)
abctime	satoko_set_runtime_limit (satoko_t *, abctime)
char	satoko_var_polarity (satoko_t *, unsigned)

Typedef Documentation

satoko_opts_t

typedef struct satoko_opts satoko_opts_t

Definition at line 37 of file satoko.h.

satoko_stats_t

typedef struct satoko_stats satoko_stats_t

Definition at line 72 of file satoko.h.

satoko_t

typedef struct solver_t_ satoko_t

Definition at line 35 of file satoko.h.

Enumeration Type Documentation

anonymous enum

anonymous enum

Return valeus

Enumerator
SATOKO_ERR
SATOKO_OK

Definition at line 17 of file satoko.h.

     {
    SATOKO_ERR = 0,
    SATOKO_OK  = 1
};

anonymous enum

anonymous enum

Enumerator
SATOKO_LIT_FALSE
SATOKO_LIT_TRUE
SATOKO_VAR_UNASSING

Definition at line 28 of file satoko.h.

     {
    SATOKO_LIT_FALSE = 1,
    SATOKO_LIT_TRUE = 0,
    SATOKO_VAR_UNASSING = 3
};

anonymous enum

anonymous enum

Enumerator
SATOKO_UNDEC
SATOKO_SAT
SATOKO_UNSAT

Definition at line 22 of file satoko.h.

     {
    SATOKO_UNDEC = 0, /* Undecided */
    SATOKO_SAT   = 1,
    SATOKO_UNSAT = -1
};

Function Documentation

satoko_add_clause()

int satoko_add_clause ( satoko_t * s, int * lits, int size )

extern

Definition at line 255 of file solver_api.c.

{
    unsigned i, j;
    unsigned prev_lit;
    unsigned max_var;
    unsigned cref;
 
    qsort((void *) lits, (size_t)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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

satoko_add_variable()

int satoko_add_variable ( satoko_t * s, char sign )

extern

Definition at line 237 of file solver_api.c.

{
    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;
}

Here is the caller graph for this function:

satoko_assump_pop()

void satoko_assump_pop ( satoko_t * s )

extern

Definition at line 306 of file solver_api.c.

{
    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));
}

Here is the call graph for this function:

Here is the caller graph for this function:

satoko_assump_push()

void satoko_assump_push ( satoko_t * s, int lit )

extern

Definition at line 298 of file solver_api.c.

{
    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));
}

Here is the call graph for this function:

Here is the caller graph for this function:

satoko_bookmark()

void satoko_bookmark ( satoko_t * s )

extern

Definition at line 443 of file solver_api.c.

{
    // 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;
}

satoko_clausenum()

int satoko_clausenum ( satoko_t * s )

extern

Definition at line 630 of file solver_api.c.

{
    return vec_uint_size(s->originals);
}

Here is the caller graph for this function:

satoko_configure()

void satoko_configure ( satoko_t * s, satoko_opts_t * user_opts )

extern

TODO: sanity check on configuration options

Definition at line 196 of file solver_api.c.

{
    assert(user_opts);
    memcpy(&s->opts, user_opts, sizeof(satoko_opts_t));
}

Here is the call graph for this function:

Here is the caller graph for this function:

satoko_conflictnum()

int satoko_conflictnum ( satoko_t * s )

extern

Definition at line 640 of file solver_api.c.

{
    return satoko_stats(s)->n_conflicts_all;
}

Here is the call graph for this function:

Here is the caller graph for this function:

satoko_create()

satoko_t * satoko_create ( void )

extern

Definition at line 88 of file solver_api.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

satoko_default_opts()

void satoko_default_opts ( satoko_opts_t * opts )

extern

Definition at line 161 of file solver_api.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

satoko_destroy()

void satoko_destroy ( satoko_t * s )

extern

Definition at line 132 of file solver_api.c.

{
    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);
}

Here is the caller graph for this function:

satoko_final_conflict()

int satoko_final_conflict ( satoko_t * s, int ** out )

extern

Definition at line 427 of file solver_api.c.

{
    *out = (int *)vec_uint_data(s->final_conflict);
    return vec_uint_size(s->final_conflict);
}

Here is the caller graph for this function:

satoko_learntnum()

int satoko_learntnum ( satoko_t * s )

extern

Definition at line 635 of file solver_api.c.

{
    return vec_uint_size(s->learnts);
}

Here is the caller graph for this function:

satoko_mark_cone()

void satoko_mark_cone ( satoko_t * s, int * pvars, int n_vars )

extern

Definition at line 562 of file solver_api.c.

{
    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]);
    }
}

Here is the call graph for this function:

satoko_minimize_assumptions()

int satoko_minimize_assumptions ( satoko_t * s, int * plits, int nlits, int nconflim )

extern

Definition at line 372 of file solver_api.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

satoko_options()

satoko_opts_t * satoko_options ( satoko_t * s )

extern

Definition at line 438 of file solver_api.c.

{
    return &s->opts;
}

Here is the caller graph for this function:

satoko_parse_dimacs()

int satoko_parse_dimacs ( char * fname, satoko_t ** solver )

extern

Start the solver and reads the DIMAC file.

Returns false upon immediate conflict.

Definition at line 108 of file cnf_reader.c.

{
    satoko_t *p = NULL;
    vec_uint_t *lits = NULL;
    int n_var;
    int n_clause;
    char *buffer = file_open(fname);
    char *token;
 
    if (buffer == NULL)
        return -1;
 
    token = buffer;
    while (1) {
        skip_spaces(&token);
        if (*token == 0)
            break;
        else if (*token == 'c')
            skip_line(&token);
        else if (*token == 'p') {
            token++;
            skip_spaces(&token);
            for(; !isspace(*token); token++); /* skip 'cnf' */
 
            n_var = read_int(&token);
            n_clause = read_int(&token);
            skip_line(&token);
            lits = vec_uint_alloc((unsigned) n_var);
            p = satoko_create();
        } else {
            if (lits == NULL) {
                printf("There is no parameter line.\n");
                satoko_free(buffer);
                return -1;
            }
            read_clause(&token, lits);
            if (!satoko_add_clause(p, (int*)vec_uint_data(lits), vec_uint_size(lits))) {
                printf("Unable to add clause: ");
                vec_uint_print(lits);
                return SATOKO_ERR;
            }
            }
    }
    vec_uint_free(lits);
    satoko_free(buffer);
    *solver = p;
    return SATOKO_OK;
}

Here is the call graph for this function:

satoko_read_cex_varvalue()

int satoko_read_cex_varvalue ( satoko_t * s, int ivar )

extern

Definition at line 660 of file solver_api.c.

{
    return satoko_var_polarity(s, ivar) == SATOKO_LIT_TRUE;
}

Here is the call graph for this function:

Here is the caller graph for this function:

satoko_reset()

void satoko_reset ( satoko_t * s )

extern

Definition at line 469 of file solver_api.c.

{
    // 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;
}

Here is the caller graph for this function:

satoko_rollback()

void satoko_rollback ( satoko_t * s )

extern

Definition at line 508 of file solver_api.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

satoko_set_runid()

void satoko_set_runid ( satoko_t * s, int id )

extern

Definition at line 655 of file solver_api.c.

{
    s->RunId = id;
}

Here is the caller graph for this function:

satoko_set_runtime_limit()

abctime satoko_set_runtime_limit ( satoko_t * s, abctime Limit )

extern

Definition at line 665 of file solver_api.c.

{
    abctime nRuntimeLimit = s->nRuntimeLimit;
    s->nRuntimeLimit = Limit;
    return nRuntimeLimit;
}

Here is the caller graph for this function:

satoko_set_stop()

void satoko_set_stop ( satoko_t * s, int * pstop )

extern

Definition at line 645 of file solver_api.c.

{
    s->pstop = pstop;
}

satoko_set_stop_func()

void satoko_set_stop_func ( satoko_t * s, int(* fnct )(int) )

extern

Definition at line 650 of file solver_api.c.

{
    s->pFuncStop = fnct;
}

Here is the caller graph for this function:

satoko_setnvars()

void satoko_setnvars ( satoko_t * s, int nvars )

extern

Definition at line 230 of file solver_api.c.

{
    int i;
    for (i = satoko_varnum(s); i < nvars; i++)
        satoko_add_variable(s, 0);
}

Here is the call graph for this function:

Here is the caller graph for this function:

satoko_simplify()

int satoko_simplify ( satoko_t * s )

extern

Definition at line 202 of file solver_api.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

satoko_solve()

int satoko_solve ( satoko_t * s )

extern

Definition at line 314 of file solver_api.c.

{
    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 && 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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

satoko_solve_assumptions()

int satoko_solve_assumptions ( satoko_t * s, int * plits, int nlits )

extern

Definition at line 347 of file solver_api.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

satoko_solve_assumptions_limit()

int satoko_solve_assumptions_limit ( satoko_t * s, int * plits, int nlits, int nconflim )

extern

Definition at line 364 of file solver_api.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

satoko_stats()

satoko_stats_t * satoko_stats ( satoko_t * s )

extern

Definition at line 433 of file solver_api.c.

{
    return &s->stats;
}

Here is the caller graph for this function:

satoko_unbookmark()

void satoko_unbookmark ( satoko_t * s )

extern

Definition at line 456 of file solver_api.c.

{
    // 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;
}

satoko_unmark_cone()

void satoko_unmark_cone ( satoko_t * s, int * pvars, int n_vars )

extern

Definition at line 575 of file solver_api.c.

{
    int i;
    assert(solver_has_marks(s));
    for (i = 0; i < n_vars; i++)
        var_clean_mark(s, pvars[i]);
}

satoko_var_polarity()

char satoko_var_polarity ( satoko_t * s, unsigned var )

extern

Definition at line 672 of file solver_api.c.

{
    return vec_char_at(s->polarity, var);
}

Here is the caller graph for this function:

satoko_varnum()

int satoko_varnum ( satoko_t * s )

extern

Definition at line 625 of file solver_api.c.

{
    return vec_char_size(s->assigns);
}

Here is the caller graph for this function:

satoko_write_dimacs()

void satoko_write_dimacs ( satoko_t * s, char * fname, int wrt_lrnt, int zero_var )

extern

Definition at line 583 of file solver_api.c.

{
    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);
 
}