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

#ifndef _elim_hpp_INCLUDED
#define _elim_hpp_INCLUDED

#include "heap.hpp" // Alphabetically after 'elim.hpp'.

namespace CaDiCaL {

struct Internal;

struct elim_more {
  Internal *internal;
  elim_more (Internal *i) : internal (i) {}
  bool operator() (unsigned a, unsigned b);
};

typedef heap<elim_more> ElimSchedule;

struct proof_clause {
  int64_t id;
  vector<int> literals;
  // for lrat
  unsigned cid; // kitten id
  bool learned;
  vector<int64_t> chain;
};

enum GateType { NO = 0, EQUI = 1, AND = 2, ITE = 3, XOR = 4, DEF = 5 };

struct Eliminator {

  Internal *internal;
  ElimSchedule schedule;

  Eliminator (Internal *i)
      : internal (i), schedule (elim_more (i)), definition_unit (0),
        gatetype (NO) {}
  ~Eliminator ();

  queue<Clause *> backward;

  Clause *dequeue ();
  void enqueue (Clause *);

  vector<Clause *> gates;
  unsigned definition_unit;
  vector<proof_clause> proof_clauses;
  vector<int> marked;
  GateType gatetype;
};

} // namespace CaDiCaL

#endif