kissat分析01_基本数据结构02_solver

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