rustsat-cadical 0.7.5

Interface to the SAT solver CaDiCaL for the RustSAT library.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127

#include "reap.hpp"
#include <cassert>
#include <climits>
#include <cstring>

void Reap::init () {
  for (auto &bucket : buckets)
    bucket = {0};
  assert (!num_elements);
  assert (!last_deleted);
  min_bucket = 32;
  assert (!max_bucket);
}

void Reap::release () {
  num_elements = 0;
  last_deleted = 0;
  min_bucket = 32;
  max_bucket = 0;
}

Reap::Reap () {
  num_elements = 0;
  last_deleted = 0;
  min_bucket = 32;
  max_bucket = 0;
}

static inline unsigned leading_zeroes_of_unsigned (unsigned x) {
  return x ? __builtin_clz (x) : sizeof (unsigned) * 8;
}

void Reap::push (unsigned e) {
  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;
  assert (num_elements != UINT_MAX);
  num_elements++;
}

unsigned Reap::pop () {
  assert (num_elements > 0);
  unsigned i = min_bucket;
  for (;;) {
    assert (i < 33);
    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);
      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;
        assert (sizeof (unsigned) == 4);
        const unsigned j = 32 - leading_zeroes_of_unsigned (diff);
        assert (j < i);
        buckets[j].push_back (other);
        if (min_bucket > j)
          min_bucket = j;
      }

      s.clear ();

      if (i && max_bucket == i) {
#ifndef NDEBUG
        for (unsigned j = i + 1; j < 33; j++)
          assert (buckets[j].empty ());
#endif
        if (s.empty ())
          max_bucket = i - 1;
      }
    } else {
      res = last_deleted;
      assert (!buckets[0].empty ());
      assert (buckets[0].at (0) == res);
      buckets[0].pop_back ();
    }

    if (min_bucket == i) {
#ifndef NDEBUG
      for (unsigned j = 0; j < i; j++)
        assert (buckets[j].empty ());
#endif
      if (s.empty ())
        min_bucket = std::min ((int) (i + 1), 32);
    }

    --num_elements;
    assert (last_deleted <= res);
    last_deleted = res;

    return res;
  }
}

void Reap::clear () {
  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;
}