#ifndef _vivify_hpp_INCLUDED
#define _vivify_hpp_INCLUDED

#include "global.h"

#include "util.hpp"

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

ABC_NAMESPACE_CXX_HEADER_START

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

ABC_NAMESPACE_CXX_HEADER_END

#endif
