sat-solvers 0.1.1

Unified interface to multiple SAT solvers (CaDiCaL, MiniSat, Glucose, Lingeling, Kissat) with automatic source compilation
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

#include "internal.hpp"

namespace CaDiCaL {

void Internal::reset_subsume_bits () {
  LOG ("marking all variables as not subsume");
  for (auto idx : vars)
    flags (idx).subsume = false;
}

void Internal::check_var_stats () {
#ifndef NDEBUG
  int64_t fixed = 0, eliminated = 0, substituted = 0, pure = 0, unused = 0;
  for (auto idx : vars) {
    Flags &f = flags (idx);
    if (f.active ())
      continue;
    if (f.fixed ())
      fixed++;
    if (f.eliminated ())
      eliminated++;
    if (f.substituted ())
      substituted++;
    if (f.unused ())
      unused++;
    if (f.pure ())
      pure++;
  }
  assert (stats.now.fixed == fixed);
  assert (stats.now.eliminated == eliminated);
  assert (stats.now.substituted == substituted);
  assert (stats.now.pure == pure);
  int64_t inactive = unused + fixed + eliminated + substituted + pure;
  assert (stats.inactive == inactive);
  assert (max_var == stats.active + stats.inactive);
#endif
}

} // namespace CaDiCaL