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.Vec; |
33 |
| import org.sat4j.minisat.core.Constr; |
34 |
| import org.sat4j.minisat.core.ILits; |
35 |
| import org.sat4j.minisat.core.Lbool; |
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 class Lits implements Serializable, ILits { |
46 |
| |
47 |
| private static final long serialVersionUID = 1L; |
48 |
| |
49 |
| private boolean pool[] = new boolean[0]; |
50 |
| |
51 |
| private int realnVars=0; |
52 |
| |
53 |
| @SuppressWarnings("unchecked") |
54 |
| protected IVec<Propagatable>[] watches = new IVec[0]; |
55 |
| |
56 |
| private int[] level = new int[0]; |
57 |
| |
58 |
| public Lbool[] truthValue = new Lbool[1]; |
59 |
| |
60 |
| private Constr[] reason = new Constr[0]; |
61 |
| |
62 |
| @SuppressWarnings("unchecked") |
63 |
| private IVec<Undoable>[] undos = new IVec[0]; |
64 |
| |
65 |
2846
| public Lits() {
|
66 |
| } |
67 |
| |
68 |
668338
| @SuppressWarnings({"unchecked"})
|
69 |
| public void init(int nvar) { |
70 |
| assert nvar >= 0; |
71 |
| |
72 |
668338
| int nvars = nvar + 1;
|
73 |
668338
| boolean[] npool = new boolean[nvars];
|
74 |
668338
| System.arraycopy(pool, 0, npool, 0, pool.length);
|
75 |
668338
| pool = npool;
|
76 |
| |
77 |
668338
| level = new int[nvars];
|
78 |
668338
| int[] nlevel = new int[nvars];
|
79 |
668335
| System.arraycopy(level, 0, nlevel, 0, level.length);
|
80 |
668335
| level = nlevel;
|
81 |
| |
82 |
668335
| IVec<Propagatable>[] nwatches = new IVec[2 * nvars];
|
83 |
668325
| System.arraycopy(watches, 0, nwatches, 0, watches.length);
|
84 |
668325
| watches = nwatches;
|
85 |
| |
86 |
668325
| Lbool[] ntruthValue = new Lbool[nvars];
|
87 |
668324
| System.arraycopy(truthValue, 0, ntruthValue, 0, truthValue.length);
|
88 |
668324
| truthValue = ntruthValue;
|
89 |
| |
90 |
668324
| IVec<Undoable>[] nundos = new IVec[nvars];
|
91 |
668322
| System.arraycopy(undos, 0, nundos, 0, undos.length);
|
92 |
668322
| undos = nundos;
|
93 |
| |
94 |
668322
| Constr[] nreason = new Constr[nvars];
|
95 |
668322
| System.arraycopy(reason, 0, nreason, 0, reason.length);
|
96 |
668322
| reason = nreason;
|
97 |
| } |
98 |
| |
99 |
24980868
| public int getFromPool(int x) {
|
100 |
24980868
| int var = Math.abs(x);
|
101 |
| assert var < pool.length; |
102 |
| |
103 |
24980868
| int lit = ((x < 0) ? (var << 1) ^ 1 : (var << 1));
|
104 |
| assert lit > 1; |
105 |
24980868
| if (!pool[var]) {
|
106 |
1075169
| realnVars++;
|
107 |
1075169
| pool[var] = true;
|
108 |
1075169
| watches[var << 1] = new Vec<Propagatable>();
|
109 |
1075169
| watches[(var << 1) | 1] = new Vec<Propagatable>();
|
110 |
1075169
| truthValue[var] = Lbool.UNDEFINED;
|
111 |
1075169
| undos[var] = new Vec<Undoable>();
|
112 |
1075169
| level[var] = -1;
|
113 |
| |
114 |
| |
115 |
| } |
116 |
24980868
| return lit;
|
117 |
| } |
118 |
| |
119 |
1538734
| public boolean belongsToPool(int x) {
|
120 |
| assert x > 0; |
121 |
1538734
| return pool[x];
|
122 |
| } |
123 |
| |
124 |
2490
| public void resetPool() {
|
125 |
2490
| for (int i = 0; i < pool.length; i++) {
|
126 |
0
| if (pool[i]) {
|
127 |
0
| reset(i);
|
128 |
| } |
129 |
| } |
130 |
| } |
131 |
| |
132 |
668326
| public void ensurePool(int howmany) {
|
133 |
668326
| init(howmany);
|
134 |
| } |
135 |
| |
136 |
| public void unassign(int lit) { |
137 |
| assert truthValue[lit >> 1] != Lbool.UNDEFINED; |
138 |
| truthValue[lit >> 1] = Lbool.UNDEFINED; |
139 |
| } |
140 |
| |
141 |
| public void satisfies(int lit) { |
142 |
| assert truthValue[lit >> 1] == Lbool.UNDEFINED; |
143 |
| truthValue[lit >> 1] = satisfyingValue(lit); |
144 |
| } |
145 |
| |
146 |
2112944114
| private static final Lbool satisfyingValue(int lit) {
|
147 |
2112944114
| return ((lit & 1) == 0) ? Lbool.TRUE : Lbool.FALSE;
|
148 |
| } |
149 |
| |
150 |
| public boolean isSatisfied(int lit) { |
151 |
| return truthValue[lit >> 1] == satisfyingValue(lit); |
152 |
| } |
153 |
| |
154 |
1047041374
| public boolean isFalsified(int lit) {
|
155 |
1047041374
| Lbool falsified = ((lit & 1) == 0) ? Lbool.FALSE : Lbool.TRUE;
|
156 |
1047041374
| return truthValue[lit >> 1] == falsified;
|
157 |
| } |
158 |
| |
159 |
1886954653
| public boolean isUnassigned(int lit) {
|
160 |
1886954653
| return truthValue[lit >> 1] == Lbool.UNDEFINED;
|
161 |
| } |
162 |
| |
163 |
0
| public String valueToString(int lit) {
|
164 |
0
| if (isUnassigned(lit))
|
165 |
0
| return "?";
|
166 |
0
| if (isSatisfied(lit))
|
167 |
0
| return "T";
|
168 |
0
| return "F";
|
169 |
| } |
170 |
| |
171 |
36601957
| public int nVars() {
|
172 |
36601957
| return truthValue.length - 1;
|
173 |
| } |
174 |
| |
175 |
0
| public int not(int lit) {
|
176 |
0
| return lit ^ 1;
|
177 |
| } |
178 |
| |
179 |
2
| public static String toString(int lit) {
|
180 |
2
| return ((lit & 1) == 0 ? "" : "-") + (lit >> 1);
|
181 |
| } |
182 |
| |
183 |
0
| public void reset(int lit) {
|
184 |
0
| watches[lit].clear();
|
185 |
0
| watches[lit ^ 1].clear();
|
186 |
0
| level[lit >> 1] = -1;
|
187 |
0
| truthValue[lit >> 1] = Lbool.UNDEFINED;
|
188 |
0
| reason[lit >> 1] = null;
|
189 |
0
| undos[lit >> 1].clear();
|
190 |
| } |
191 |
| |
192 |
1263087438
| public int getLevel(int lit) {
|
193 |
1263087438
| return level[lit >> 1];
|
194 |
| } |
195 |
| |
196 |
| public void setLevel(int lit, int l) { |
197 |
| level[lit >> 1] = l; |
198 |
| } |
199 |
| |
200 |
| public Constr getReason(int lit) { |
201 |
| return reason[lit >> 1]; |
202 |
| } |
203 |
| |
204 |
| public void setReason(int lit, Constr r) { |
205 |
| reason[lit >> 1] = r; |
206 |
| } |
207 |
| |
208 |
1819183493
| public IVec<Undoable> undos(int lit) {
|
209 |
1819183493
| return undos[lit >> 1];
|
210 |
| } |
211 |
| |
212 |
982880609
| public void watch(int lit, Propagatable c) {
|
213 |
982880609
| watches[lit].push(c);
|
214 |
| } |
215 |
| |
216 |
| public IVec<Propagatable> watches(int lit) { |
217 |
| return watches[lit]; |
218 |
| } |
219 |
| |
220 |
0
| public boolean isImplied(int lit) {
|
221 |
0
| int var = lit >> 1;
|
222 |
| |
223 |
| assert reason[var] == null || truthValue[var] != Lbool.UNDEFINED; |
224 |
| |
225 |
| |
226 |
0
| return reason[var] != null || level[var] == 0;
|
227 |
| } |
228 |
| |
229 |
452572390
| public int realnVars() {
|
230 |
452572390
| return realnVars;
|
231 |
| } |
232 |
| } |