k ssat数据成员的列传1

数据成员solver->clause

是一个文字序列，以一个工作栈的方式管理一部分文字；

主要包括在以下文件中：

internal.h

internal.c

主要的操作包括：

1.  RELEASE_STACK (solver->clause);

EMPTY_STACK (solver->clause),

2.

for (all_stack (unsigned, lit, solver->clause))
MARK (lit) = MARK (NOT (lit)) = 0;

CLEAR_STACK (solver->clause);

solver->clause_satisfied = false;
solver->clause_trivial = false;
solver->clause_shrink = false;

3.

assert (SIZE_STACK (solver->clause) < UINT_MAX);
PUSH_STACK (solver->clause, ilit);

//clause.c

4.

reference kissat_new_original_clause (kissat *solver) {
const unsigned size = SIZE_STACK (solver->clause);
unsigned *lits = BEGIN_STACK (solver->clause);
kissat_sort_literals (solver, size, lits);
reference res = new_clause (solver, true, false, 0, size, lits);
return res;
}

reference kissat_new_irredundant_clause (kissat *solver) {
const unsigned size = SIZE_STACK (solver->clause);
unsigned *lits = BEGIN_STACK (solver->clause);
return new_clause (solver, false, false, 0, size, lits);
}

reference kissat_new_redundant_clause (kissat *solver, unsigned glue) {
const unsigned size = SIZE_STACK (solver->clause);
unsigned *lits = BEGIN_STACK (solver->clause);
return new_clause (solver, false, true, glue, size, lits);
}

//analyze.c

5.

(1)

for (all_stack (unsigned, lit, solver->clause))

　　assert (all_assigned[IDX (lit)].analyzed);

(2)

for (all_stack (unsigned, lit, solver->clause)) {
　　analyze_reason_side_literal (solver, limit, arena, all_assigned, lit);
　　if (SIZE_STACK (solver->analyzed) > limit)
　　　　break;
}