sort.c

Go to the documentation of this file.

#include "internal.h"
#include "logging.h"
 
ABC_NAMESPACE_IMPL_START
 
static inline value
move_smallest_literal_to_front (kissat *solver, const value *const values,
                                const assigned *const assigned,
                                bool satisfied_is_enough, unsigned start,
                                unsigned size, unsigned *lits) {
  KISSAT_assert (1 < size);
  KISSAT_assert (start < size);
 
  unsigned a = lits[start];
 
  value u = values[a];
  if (!u || (u > 0 && satisfied_is_enough))
    return u;
 
  unsigned pos = 0, best = a;
 
  {
    const unsigned i = IDX (a);
    unsigned k = (u ? assigned[i].level : UINT_MAX);
 
    KISSAT_assert (start < UINT_MAX);
    for (unsigned i = start + 1; i < size; i++) {
      const unsigned b = lits[i];
      const value v = values[b];
 
      if (!v || (v > 0 && satisfied_is_enough)) {
        best = b;
        pos = i;
        u = v;
        break;
      }
 
      const unsigned j = IDX (b);
      const unsigned l = (v ? assigned[j].level : UINT_MAX);
 
      bool better;
 
      if (u < 0 && v > 0)
        better = true;
      else if (u > 0 && v < 0)
        better = false;
      else if (u < 0) {
        KISSAT_assert (v < 0);
        better = (k < l);
      } else {
        KISSAT_assert (u > 0);
        KISSAT_assert (v > 0);
        KISSAT_assert (!satisfied_is_enough);
        better = (k > l);
      }
 
      if (!better)
        continue;
 
      best = b;
      pos = i;
      u = v;
      k = l;
    }
  }
 
  if (!pos)
    return u;
 
  lits[start] = best;
  lits[pos] = a;
 
  LOG ("new smallest literal %s at %u swapped with %s at %u", LOGLIT (best),
       pos, LOGLIT (a), start);
#ifndef LOGGING
  (void) solver;
#endif
  return u;
}
 
#ifdef INLINE_SORT
static inline
#endif
    void
    kissat_sort_literals (kissat *solver,
#ifdef INLINE_SORT
                          const value *const values,
                          const assigned *assigned,
#endif
                          unsigned size, unsigned *lits) {
#ifndef INLINE_SORT
  const value *const values = solver->values;
  const assigned *const assigned = solver->assigned;
#endif
  value u = move_smallest_literal_to_front (solver, values, assigned, false,
                                            0, size, lits);
  if (size > 2)
    move_smallest_literal_to_front (solver, values, assigned, (u >= 0), 1,
                                    size, lits);
}
 
ABC_NAMESPACE_IMPL_END