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
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
|
/*****************************************************************************
SatELite -- (C) Niklas Een, Niklas Sorensson, 2004
CryptoMiniSat -- Copyright (c) 2009 Mate Soos
Original code by SatELite authors are under an MIT licence.
Modifications for CryptoMiniSat are under GPLv3.
******************************************************************************/
#ifndef XORSIMPLIFIER_H
#define XORSIMPLIFIER_H
#include "Solver.h"
#include "Vec.h"
#include "XSet.h"
namespace CMSat {
class ClauseCleaner;
/**
@brief Handles xor-subsumption and variable elimination at the XOR level
This class achieves three things:
1) it removes variables though XOR-ing of two xors thereby removing their common
variable. If that variable is not used anywere else, the variable is now removed
from the problem
2) It tries to XOR clauses together to get 1-long or 2-long XOR clauses. These
force variables to certain values or replace variables with other variables,
respectively
3) It tries to subsume XOR clauses with other XOR clauses (making 2 XOR clauses
in the process, but one of them is going to be much smaller than it was originally)
*/
class XorSubsumer
{
public:
XorSubsumer(Solver& S2);
bool simplifyBySubsumption();
void unlinkModifiedClause(vec<Lit>& origClause, XorClauseSimp c);
void unlinkModifiedClauseNoDetachNoNULL(vec<Lit>& origClause, XorClauseSimp c);
void unlinkClause(XorClauseSimp cc, Var elim = var_Undef);
XorClauseSimp linkInClause(XorClause& cl);
void linkInAlreadyClause(XorClauseSimp& c);
void newVar();
void extendModel(Solver& solver2);
uint32_t getNumElimed() const;
const vec<char>& getVarElimed() const;
bool unEliminate(const Var var);
bool checkElimedUnassigned() const;
double getTotalTime() const;
struct XorElimedClause
{
vector<Lit> lits;
bool xorEqualFalse;
void plainPrint(FILE* to = stdout) const
{
fprintf(to, "x");
if (xorEqualFalse) fprintf(to, "-");
for (size_t i = 0; i < lits.size(); i++) {
assert(!lits[i].sign());
fprintf(to, "%d ", lits[i].var() + 1);
}
fprintf(to, "0\n");
}
};
const map<Var, vector<XorElimedClause> >& getElimedOutVar() const;
private:
friend class ClauseCleaner;
friend class ClauseAllocator;
//Main
vec<XorClauseSimp> clauses;
vec<vec<XorClauseSimp> > occur; // 'occur[index(lit)]' is a list of constraints containing 'lit'.
Solver& solver; // The Solver
// Temporaries (to reduce allocation overhead):
//
vec<char> seen_tmp; // (used in various places)
//Start-up
void addFromSolver(vec<XorClause*>& cs);
void addBackToSolver();
// Subsumption:
void findSubsumed(XorClause& ps, vec<XorClauseSimp>& out_subsumed);
bool isSubsumed(XorClause& ps);
void subsume0(XorClauseSimp ps);
template<class T1, class T2>
bool subset(const T1& A, const T2& B);
bool subsetAbst(uint32_t A, uint32_t B);
template<class T>
void findUnMatched(const T& A, const T& B, vec<Lit>& unmatchedPart);
//helper
void testAllClauseAttach() const;
//dependent removal
bool removeDependent();
void fillCannotEliminate();
vec<char> cannot_eliminate;
void addToCannotEliminate(Clause* it);
void removeWrong(vec<Clause*>& cs);
void removeWrongBins();
void removeAssignedVarsFromEliminated();
//Global stats
double totalTime;
map<Var, vector<XorElimedClause> > elimedOutVar;
vec<char> var_elimed;
uint32_t numElimed;
//Heule-process
template<class T>
void xorTwoClauses(const T& c1, const T& c2, vec<Lit>& xored);
bool localSubstitute();
uint32_t localSubstituteUseful;
uint32_t clauses_subsumed;
uint32_t clauses_cut;
uint32_t origNClauses;
uint32_t clauseID;
};
inline bool XorSubsumer::subsetAbst(uint32_t A, uint32_t B)
{
return !(A & ~B);
}
// Assumes 'seen' is cleared (will leave it cleared)
template<class T1, class T2>
bool XorSubsumer::subset(const T1& A, const T2& B)
{
for (uint32_t i = 0; i != B.size(); i++)
seen_tmp[B[i].var()] = 1;
for (uint32_t i = 0; i != A.size(); i++) {
if (!seen_tmp[A[i].var()]) {
for (uint32_t i = 0; i != B.size(); i++)
seen_tmp[B[i].var()] = 0;
return false;
}
}
for (uint32_t i = 0; i != B.size(); i++)
seen_tmp[B[i].var()] = 0;
return true;
}
inline void XorSubsumer::newVar()
{
occur .push();
seen_tmp .push(0);
cannot_eliminate.push(0);
var_elimed.push(0);
}
inline const vec<char>& XorSubsumer::getVarElimed() const
{
return var_elimed;
}
inline uint32_t XorSubsumer::getNumElimed() const
{
return numElimed;
}
inline double XorSubsumer::getTotalTime() const
{
return totalTime;
}
inline const map<Var, vector<XorSubsumer::XorElimedClause> >& XorSubsumer::getElimedOutVar() const
{
return elimedOutVar;
}
}
#endif //XORSIMPLIFIER_H
|
