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

#ifndef _vivify_hpp_INCLUDED
#define _vivify_hpp_INCLUDED

namespace CaDiCaL {

struct Clause;

struct Vivifier {
  vector<Clause *> schedule, stack;
  vector<int> sorted;
  bool redundant_mode;
  std::vector<std::tuple<int, Clause *, bool>> lrat_stack;
  Vivifier (bool mode) : redundant_mode (mode) {}

  void erase () {
    erase_vector (schedule);
    erase_vector (sorted);
    erase_vector (stack);
  }
};

} // namespace CaDiCaL

#endif