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