solver在internal.h中定义
下面从使用的角度来了解solver个主要数据成员
assign.c中几个函数 | |
static inline void kissat_assign (kissat * solver, #ifdef INLINE_ASSIGN value * values, assigned * assigned, #endif unsigned lit, bool binary, bool redundant, unsigned level, unsigned reason) { assert (binary || !redundant); const unsigned not_lit = NOT (lit); #ifndef INLINE_ASSIGN value *values = solver->values; assigned *assigned = solver->assigned; #endif assert (!values[lit]); assert (!values[not_lit]); values[lit] = 1; values[not_lit] = -1; assert (solver->unassigned > 0); solver->unassigned--; const unsigned idx = IDX (lit); struct assigned *a = assigned + idx; if (level) { a->level = level; a->binary = binary; a->redundant = redundant; a->reason = reason; } else { a->level = 0; a->binary = false; a->redundant = false; a->reason = UNIT; } if (!solver->probing) { const bool negated = NEGATED (lit); //文字是否为负文字,为真表示是负文字,为假表示为正文字 const value value = BOOL_TO_VALUE (negated); SAVED (idx) = value; //变元的取值 来自于文字取值为真时对应变元的值 } PUSH_STACK (solver->trail, lit); if (!level) { kissat_mark_fixed_literal (solver, lit); assert (solver->unflushed < UINT_MAX); solver->unflushed++; } watches *watches = &WATCHES (not_lit); if (!watches->size) { watch *w = BEGIN_WATCHES (*watches); __builtin_prefetch (w, 0, 1); } }
|
|