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

#ifndef _vivify_hpp_INCLUDED
#define _vivify_hpp_INCLUDED

#include "util.hpp"

#include <array>
#include <cstdint>
#include <vector>

namespace CaDiCaL {

struct Clause;

enum class Vivify_Mode { TIER1, TIER2, TIER3, IRREDUNDANT };

#define COUNTREF_COUNTS 2

struct vivify_ref {
  bool vivify;
  std::size_t size;
  uint64_t count[COUNTREF_COUNTS];
  Clause *clause;
};

// In the vivifier structure, we put the schedules in an array in order to
// be able to iterate over them, but we provide the reference to them to
// make sure that you do need to remember the order.
struct Vivifier {
  std::vector<vivify_ref> refs_schedule;
  std::array<std::vector<Clause *>, 4> schedules;
  std::vector<Clause *> &schedule_tier1, &schedule_tier2, &schedule_tier3,
      &schedule_irred;
  std::vector<int> sorted;
  Vivify_Mode tier;
  char tag;
  int tier1_limit;
  int tier2_limit;
  int64_t ticks;
  std::vector<std::tuple<int, Clause *, bool>> lrat_stack;
  Vivifier (Vivify_Mode mode_tier)
      : schedule_tier1 (schedules[0]), schedule_tier2 (schedules[1]),
        schedule_tier3 (schedules[2]), schedule_irred (schedules[3]),
        tier (mode_tier) {}

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

} // namespace CaDiCaL

#endif