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
54

#ifndef _factor_hpp_INCLUDED
#define _factor_hpp_INCLUDED

#include "clause.hpp"
#include "heap.hpp"

namespace CaDiCaL {

struct Internal;

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

struct Quotient {
  Quotient (int f) : factor (f) {}
  ~Quotient () {}
  int factor;
  size_t id;
  int64_t bid; // for LRAT
  Quotient *prev, *next;
  vector<Clause *> qlauses;
  vector<size_t> matches;
  size_t matched;
};

typedef heap<factor_occs_size> FactorSchedule;

struct Factoring {
  Factoring (Internal *, int64_t);
  ~Factoring ();

  // These are initialized by the constructor
  Internal *internal;
  int64_t limit;
  FactorSchedule schedule;

  int initial;
  int bound;
  vector<unsigned> count;
  vector<int> fresh;
  vector<int> counted;
  vector<int> nounted;
  vector<Clause *> flauses;
  struct {
    Quotient *first, *last;
  } quotients;
};

} // namespace CaDiCaL

#endif