#include <reap.hpp>

Public Member Functions
	Reap ()

void	init ()

void	release ()

bool	empty ()

size_t	size ()

void	push (unsigned)

void	clear ()

unsigned	pop ()

Detailed Description

Definition at line 11 of file reap.hpp.

Constructor & Destructor Documentation

◆ Reap()

Reap::Reap ( )

Definition at line 35 of file cadical_reap.cpp.

            {
  num_elements = 0;
  last_deleted = 0;
  min_bucket = 32;
  max_bucket = 0;
}

Member Function Documentation

◆ clear()

void Reap::clear ( )

Definition at line 132 of file cadical_reap.cpp.

                  {
  CADICAL_assert (max_bucket <= 32);
  for (unsigned i = 0; i < 33; i++)
    buckets[i].clear ();
  num_elements = 0;
  last_deleted = 0;
  min_bucket = 32;
  max_bucket = 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ empty()

bool Reap::empty ( )

inline

Definition at line 16 of file reap.hpp.

16{ return !num_elements; }

Here is the caller graph for this function:

◆ init()

ABC_NAMESPACE_IMPL_START void Reap::init ( )

Definition at line 19 of file cadical_reap.cpp.

                 {
  for (auto &bucket : buckets)
    bucket = {0};
  CADICAL_assert (!num_elements);
  CADICAL_assert (!last_deleted);
  min_bucket = 32;
  CADICAL_assert (!max_bucket);
}

◆ pop()

unsigned Reap::pop ( )

Definition at line 59 of file cadical_reap.cpp.

                    {
  CADICAL_assert (num_elements > 0);
  unsigned i = min_bucket;
  for (;;) {
    CADICAL_assert (i < 33);
    CADICAL_assert (i <= max_bucket);
    std::vector<unsigned> &s = buckets[i];
    if (s.empty ()) {
      min_bucket = ++i;
      continue;
    }
    unsigned res;
    if (i) {
      res = UINT_MAX;
      const auto begin = std::begin (s);
      const auto end = std::end (s);
      auto q = std::begin (s);
      CADICAL_assert (begin < end);
      for (auto p = begin; p != end; ++p) {
        const unsigned tmp = *p;
        if (tmp >= res)
          continue;
        res = tmp;
        q = p;
      }
 
      for (auto p = begin; p != end; ++p) {
        if (p == q)
          continue;
        const unsigned other = *p;
        const unsigned diff = other ^ res;
        CADICAL_assert (sizeof (unsigned) == 4);
        const unsigned j = 32 - leading_zeroes_of_unsigned (diff);
        CADICAL_assert (j < i);
        buckets[j].push_back (other);
        if (min_bucket > j)
          min_bucket = j;
      }
 
      s.clear ();
 
      if (i && max_bucket == i) {
#ifndef CADICAL_NDEBUG
        for (unsigned j = i + 1; j < 33; j++)
          CADICAL_assert (buckets[j].empty ());
#endif
        if (s.empty ())
          max_bucket = i - 1;
      }
    } else {
      res = last_deleted;
      CADICAL_assert (!buckets[0].empty ());
      CADICAL_assert (buckets[0].at (0) == res);
      buckets[0].pop_back ();
    }
 
    if (min_bucket == i) {
#ifndef CADICAL_NDEBUG
      for (unsigned j = 0; j < i; j++)
        CADICAL_assert (buckets[j].empty ());
#endif
      if (s.empty ())
        min_bucket = std::min ((int) (i + 1), 32);
    }
 
    --num_elements;
    CADICAL_assert (last_deleted <= res);
    last_deleted = res;
 
    return res;
  }
}

Here is the call graph for this function:

◆ push()

void Reap::push ( unsigned e )

Definition at line 46 of file cadical_reap.cpp.

                           {
  CADICAL_assert (last_deleted <= e);
  const unsigned diff = e ^ last_deleted;
  const unsigned bucket = 32 - leading_zeroes_of_unsigned (diff);
  buckets[bucket].push_back (e);
  if (min_bucket > bucket)
    min_bucket = bucket;
  if (max_bucket < bucket)
    max_bucket = bucket;
  CADICAL_assert (num_elements != UINT_MAX);
  num_elements++;
}

◆ release()

void Reap::release ( )

Definition at line 28 of file cadical_reap.cpp.

                    {
  num_elements = 0;
  last_deleted = 0;
  min_bucket = 32;
  max_bucket = 0;
}

◆ size()

size_t Reap::size ( )