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
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
#ifndef _flags_hpp_INCLUDED
#define _flags_hpp_INCLUDED
namespace CaDiCaL {
struct Flags { // Variable flags.
// The first set of flags is related to 'analyze' and 'minimize'.
//
bool seen : 1; // seen in generating first UIP clause in 'analyze'
bool keep : 1; // keep in learned clause in 'minimize'
bool poison : 1; // can not be removed in 'minimize'
bool removable : 1; // can be removed in 'minimize'
bool shrinkable : 1; // can be removed in 'shrink'
bool added : 1; // has already been added to lrat_chain (in 'minimize')
// These three variable flags are used to schedule clauses in subsumption
// ('subsume'), variables in bounded variable elimination ('elim') and in
// hyper ternary resolution ('ternary').
//
bool elim : 1; // removed since last 'elim' round (*)
bool subsume : 1; // added since last 'subsume' round (*)
bool ternary : 1; // added in ternary clause since last 'ternary' (*)
bool sweep : 1;
bool blockable : 1;
unsigned char
marked_signed : 2; // generate correct LRAT chains in decompose
unsigned char factor : 2;
// These literal flags are used by blocked clause elimination ('block').
//
unsigned char block : 2; // removed since last 'block' round (*)
unsigned char skip : 2; // skip this literal as blocking literal
bool backbone1, backbone0;
// Bits for handling assumptions.
//
unsigned char assumed : 2;
unsigned char failed : 2; // 0 if not part of failure
// 1 if positive lit is in failure
// 2 if negated lit is in failure
bool factored_but_on_reconstruction_stack : 1;
enum {
UNUSED = 0,
ACTIVE = 1,
FIXED = 2,
ELIMINATED = 3,
SUBSTITUTED = 4,
PURE = 5
};
unsigned char status : 3;
// Initialized explicitly in 'Internal::init' through this function.
//
Flags () {
seen = keep = poison = removable = shrinkable = added = sweep =
backbone1 = backbone0 = false;
subsume = elim = ternary = true;
block = 3u;
skip = assumed = failed = marked_signed = factor = 0;
status = UNUSED;
}
bool unused () const { return status == UNUSED; }
bool active () const { return status == ACTIVE; }
bool fixed () const { return status == FIXED; }
bool eliminated () const { return status == ELIMINATED; }
bool substituted () const { return status == SUBSTITUTED; }
bool pure () const { return status == PURE; }
// The flags marked with '(*)' are copied during 'External::copy_flags',
// which in essence means they are reset in the copy if they were clear.
// This avoids the effort of fruitless preprocessing the copy.
void copy (Flags &dst) const {
dst.elim = elim;
dst.subsume = subsume;
dst.ternary = ternary;
dst.block = block;
dst.sweep = sweep;
dst.backbone0 = backbone0;
dst.backbone1 = backbone1;
dst.added = added;
dst.factor = factor;
// seen, keep, poison, removable, shrinkable are unused
}
};
} // namespace CaDiCaL
#endif