propdense.c File Reference

#include "propdense.h"
#include "fastassign.h"

Include dependency graph for propdense.c:

Go to the source code of this file.

Functions
bool	kissat_dense_propagate (kissat *solver)

Function Documentation

kissat_dense_propagate()

bool kissat_dense_propagate

(

kissat *

solver

)

Definition at line 88 of file propdense.c.

                                             {
  KISSAT_assert (!solver->level);
  KISSAT_assert (!solver->watching);
  KISSAT_assert (!solver->inconsistent);
  START (propagate);
  unsigned *propagate = solver->propagate;
  bool res = true;
  while (res && propagate != END_ARRAY (solver->trail))
    res = non_watching_propagate_literal (solver, *propagate++);
  const unsigned propagated = propagate - solver->propagate;
  solver->propagate = propagate;
  ADD (dense_propagations, propagated);
  ADD (propagations, propagated);
  if (!res) {
    KISSAT_assert (!solver->inconsistent);
    LOG ("inconsistent root propagation");
    CHECK_AND_ADD_EMPTY ();
    ADD_EMPTY_TO_PROOF ();
    solver->inconsistent = true;
  }
  STOP (propagate);
  return res;
}

Here is the caller graph for this function: