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 package org.sat4j.minisat.constraints.cnf;
31
32 import java.io.Serializable;
33
34 import org.sat4j.core.LiteralsUtils;
35 import org.sat4j.core.Vec;
36 import org.sat4j.minisat.core.Constr;
37 import org.sat4j.minisat.core.ILits;
38 import org.sat4j.minisat.core.Propagatable;
39 import org.sat4j.minisat.core.Undoable;
40 import org.sat4j.specs.IVec;
41
42
43
44
45
46
47 public final class Lits implements Serializable, ILits {
48
49 private static final int DEFAULT_INIT_SIZE = 128;
50
51 private static final long serialVersionUID = 1L;
52
53 private boolean pool[] = new boolean[1];
54
55 private int realnVars = 0;
56
57 @SuppressWarnings("unchecked")
58 private IVec<Propagatable>[] watches = new IVec[0];
59
60 private int[] level = new int[0];
61
62 private Constr[] reason = new Constr[0];
63
64 private int maxvarid = 0;
65
66 @SuppressWarnings("unchecked")
67 private IVec<Undoable>[] undos = new IVec[0];
68
69 private boolean[] falsified = new boolean[0];
70
71 public Lits() {
72 init(DEFAULT_INIT_SIZE);
73 }
74
75 @SuppressWarnings({ "unchecked" })
76 public final void init(int nvar) {
77 if (nvar < this.pool.length) {
78 return;
79 }
80 assert nvar >= 0;
81
82 int nvars = nvar + 1;
83 boolean[] npool = new boolean[nvars];
84 System.arraycopy(this.pool, 0, npool, 0, this.pool.length);
85 this.pool = npool;
86
87 int[] nlevel = new int[nvars];
88 System.arraycopy(this.level, 0, nlevel, 0, this.level.length);
89 this.level = nlevel;
90
91 IVec<Propagatable>[] nwatches = new IVec[2 * nvars];
92 System.arraycopy(this.watches, 0, nwatches, 0, this.watches.length);
93 this.watches = nwatches;
94
95 IVec<Undoable>[] nundos = new IVec[nvars];
96 System.arraycopy(this.undos, 0, nundos, 0, this.undos.length);
97 this.undos = nundos;
98
99 Constr[] nreason = new Constr[nvars];
100 System.arraycopy(this.reason, 0, nreason, 0, this.reason.length);
101 this.reason = nreason;
102
103 boolean[] newFalsified = new boolean[2 * nvars];
104 System.arraycopy(this.falsified, 0, newFalsified, 0,
105 this.falsified.length);
106 this.falsified = newFalsified;
107 }
108
109 public int getFromPool(int x) {
110 int var = Math.abs(x);
111 if (var >= this.pool.length) {
112 init(Math.max(var, this.pool.length << 1));
113 }
114 assert var < this.pool.length;
115 if (var > this.maxvarid) {
116 this.maxvarid = var;
117 }
118 int lit = LiteralsUtils.toInternal(x);
119 assert lit > 1;
120 if (!this.pool[var]) {
121 this.realnVars++;
122 this.pool[var] = true;
123 this.watches[var << 1] = new Vec<Propagatable>();
124 this.watches[var << 1 | 1] = new Vec<Propagatable>();
125 this.undos[var] = new Vec<Undoable>();
126 this.level[var] = -1;
127 this.falsified[var << 1] = false;
128
129 this.falsified[var << 1 | 1] = false;
130
131 }
132 return lit;
133 }
134
135 public boolean belongsToPool(int x) {
136 assert x > 0;
137 if (x >= this.pool.length) {
138 return false;
139 }
140 return this.pool[x];
141 }
142
143 public void resetPool() {
144 for (int i = 0; i < this.pool.length; i++) {
145 if (this.pool[i]) {
146 reset(i << 1);
147 }
148 }
149 this.maxvarid = 0;
150 this.realnVars = 0;
151 }
152
153 public void ensurePool(int howmany) {
154 if (howmany >= this.pool.length) {
155 init(Math.max(howmany, this.pool.length << 1));
156 }
157 this.maxvarid = howmany;
158 }
159
160 public void unassign(int lit) {
161 assert this.falsified[lit] || this.falsified[lit ^ 1];
162 this.falsified[lit] = false;
163 this.falsified[lit ^ 1] = false;
164 }
165
166 public void satisfies(int lit) {
167 assert !this.falsified[lit] && !this.falsified[lit ^ 1];
168 this.falsified[lit] = false;
169 this.falsified[lit ^ 1] = true;
170 }
171
172 public void forgets(int var) {
173 this.falsified[var << 1] = true;
174 this.falsified[var << 1 ^ 1] = true;
175 }
176
177 public boolean isSatisfied(int lit) {
178 return this.falsified[lit ^ 1];
179 }
180
181 public final boolean isFalsified(int lit) {
182 return this.falsified[lit];
183 }
184
185 public boolean isUnassigned(int lit) {
186 return !this.falsified[lit] && !this.falsified[lit ^ 1];
187 }
188
189 public String valueToString(int lit) {
190 if (isUnassigned(lit)) {
191 return "?";
192 }
193 if (isSatisfied(lit)) {
194 return "T";
195 }
196 return "F";
197 }
198
199 public int nVars() {
200
201 return this.maxvarid;
202 }
203
204 public int not(int lit) {
205 return lit ^ 1;
206 }
207
208 public static String toString(int lit) {
209 return ((lit & 1) == 0 ? "" : "-") + (lit >> 1);
210 }
211
212 public void reset(int lit) {
213 this.watches[lit].clear();
214 this.watches[lit ^ 1].clear();
215 this.level[lit >> 1] = -1;
216 this.reason[lit >> 1] = null;
217 this.undos[lit >> 1].clear();
218 this.falsified[lit] = false;
219 this.falsified[lit ^ 1] = false;
220 this.pool[lit >> 1] = false;
221 }
222
223 public int getLevel(int lit) {
224 return this.level[lit >> 1];
225 }
226
227 public void setLevel(int lit, int l) {
228 this.level[lit >> 1] = l;
229 }
230
231 public Constr getReason(int lit) {
232 return this.reason[lit >> 1];
233 }
234
235 public void setReason(int lit, Constr r) {
236 this.reason[lit >> 1] = r;
237 }
238
239 public IVec<Undoable> undos(int lit) {
240 return this.undos[lit >> 1];
241 }
242
243 public void watch(int lit, Propagatable c) {
244 this.watches[lit].push(c);
245 }
246
247 public IVec<Propagatable> watches(int lit) {
248 return this.watches[lit];
249 }
250
251 public boolean isImplied(int lit) {
252 int var = lit >> 1;
253 assert this.reason[var] == null || this.falsified[lit]
254 || this.falsified[lit ^ 1];
255
256
257 return this.pool[var]
258 && (this.reason[var] != null || this.level[var] == 0);
259 }
260
261 public int realnVars() {
262 return this.realnVars;
263 }
264
265
266
267
268
269
270
271 protected int capacity() {
272 return this.pool.length - 1;
273 }
274
275
276
277
278 public int nextFreeVarId(boolean reserve) {
279 if (reserve) {
280 ensurePool(this.maxvarid + 1);
281
282 return this.maxvarid;
283 }
284 return this.maxvarid + 1;
285 }
286 }