solver.c File Reference

#include <stdio.h>
#include <assert.h>
#include <string.h>
#include <math.h>
#include "act_clause.h"
#include "act_var.h"
#include "solver.h"
#include "utils/heap.h"
#include "utils/mem.h"
#include "utils/sort.h"
#include "misc/util/abc_global.h"

Include dependency graph for solver.c:

Go to the source code of this file.

Functions
unsigned	solver_clause_create (solver_t *s, vec_uint_t *lits, unsigned f_learnt)
void	solver_cancel_until (solver_t *s, unsigned level)
unsigned	solver_propagate (solver_t *s)
char	solver_search (solver_t *s)
void	solver_debug_check_trail (solver_t *s)
void	solver_debug_check_clauses (solver_t *s)
void	solver_debug_check (solver_t *s, int result)

Function Documentation

solver_cancel_until()

void solver_cancel_until	(	solver_t *	s,
		unsigned	level )

Definition at line 515 of file solver.c.

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

Here is the caller graph for this function:

solver_clause_create()

unsigned solver_clause_create	(	solver_t *	s,
		vec_uint_t *	lits,
		unsigned	f_learnt )

Definition at line 483 of file solver.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

solver_debug_check()

void solver_debug_check	(	solver_t *	s,
		int	result )

Definition at line 749 of file solver.c.

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

Here is the call graph for this function:

solver_debug_check_clauses()

void solver_debug_check_clauses

(

solver_t *

s

)

Definition at line 725 of file solver.c.

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

solver_debug_check_trail()

void solver_debug_check_trail

(

solver_t *

s

)

Definition at line 696 of file solver.c.

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

Here is the caller graph for this function:

solver_propagate()

unsigned solver_propagate

(

solver_t *

s

)

Definition at line 534 of file solver.c.

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

Here is the caller graph for this function:

solver_search()

char solver_search

(

solver_t *

s

)

Definition at line 627 of file solver.c.

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

Here is the call graph for this function:

Here is the caller graph for this function: