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.tools;
29
30 import java.io.PrintStream;
31 import java.io.PrintWriter;
32 import java.util.Map;
33
34 import org.sat4j.specs.ContradictionException;
35 import org.sat4j.specs.IConstr;
36 import org.sat4j.specs.ISolver;
37 import org.sat4j.specs.IVec;
38 import org.sat4j.specs.IVecInt;
39 import org.sat4j.specs.SearchListener;
40 import org.sat4j.specs.TimeoutException;
41
42
43
44
45
46
47
48
49 public abstract class SolverDecorator<T extends ISolver> implements ISolver {
50
51
52
53
54 private static final long serialVersionUID = 1L;
55
56 public boolean isDBSimplificationAllowed() {
57 return solver.isDBSimplificationAllowed();
58 }
59
60 public void setDBSimplificationAllowed(boolean status) {
61 solver.setDBSimplificationAllowed(status);
62 }
63
64
65
66
67
68
69 public void setTimeoutOnConflicts(int count) {
70 solver.setTimeoutOnConflicts(count);
71 }
72
73
74
75
76
77
78
79 public void printInfos(PrintWriter out, String prefix) {
80 solver.printInfos(out, prefix);
81 }
82
83
84
85
86
87
88 public boolean isSatisfiable(boolean global) throws TimeoutException {
89 return solver.isSatisfiable(global);
90 }
91
92
93
94
95
96
97
98 public boolean isSatisfiable(IVecInt assumps, boolean global)
99 throws TimeoutException {
100 return solver.isSatisfiable(assumps, global);
101 }
102
103
104
105
106
107
108 public void clearLearntClauses() {
109 solver.clearLearntClauses();
110 }
111
112
113
114
115
116
117 public int[] findModel() throws TimeoutException {
118 return solver.findModel();
119 }
120
121
122
123
124
125
126 public int[] findModel(IVecInt assumps) throws TimeoutException {
127 return solver.findModel(assumps);
128 }
129
130
131
132
133
134
135 public boolean model(int var) {
136 return solver.model(var);
137 }
138
139 public void setExpectedNumberOfClauses(int nb) {
140 solver.setExpectedNumberOfClauses(nb);
141 }
142
143
144
145
146
147
148 public int getTimeout() {
149 return solver.getTimeout();
150 }
151
152
153
154
155 public long getTimeoutMs() {
156 return solver.getTimeoutMs();
157 }
158
159
160
161
162
163
164 public String toString(String prefix) {
165 return solver.toString(prefix);
166 }
167
168 @Override
169 public String toString() {
170 return solver.toString();
171 }
172
173
174
175
176
177
178
179 @Deprecated
180 public void printStat(PrintStream out, String prefix) {
181 solver.printStat(out, prefix);
182 }
183
184 public void printStat(PrintWriter out, String prefix) {
185 solver.printStat(out, prefix);
186 }
187
188 private T solver;
189
190
191
192
193 public SolverDecorator(T solver) {
194 this.solver = solver;
195 }
196
197 @Deprecated
198 public int newVar() {
199 return solver.newVar();
200 }
201
202
203
204
205
206
207 public int newVar(int howmany) {
208 return solver.newVar(howmany);
209 }
210
211
212
213
214
215
216 public IConstr addClause(IVecInt literals) throws ContradictionException {
217 return solver.addClause(literals);
218 }
219
220 public void addAllClauses(IVec<IVecInt> clauses)
221 throws ContradictionException {
222 solver.addAllClauses(clauses);
223 }
224
225
226
227
228 public IConstr addBlockingClause(IVecInt literals)
229 throws ContradictionException {
230 return solver.addBlockingClause(literals);
231 }
232
233
234
235
236
237
238 public IConstr addAtMost(IVecInt literals, int degree)
239 throws ContradictionException {
240 return solver.addAtMost(literals, degree);
241 }
242
243
244
245
246
247
248 public IConstr addAtLeast(IVecInt literals, int degree)
249 throws ContradictionException {
250 return solver.addAtLeast(literals, degree);
251 }
252
253
254
255
256
257
258 public int[] model() {
259 return solver.model();
260 }
261
262
263
264
265
266
267 public boolean isSatisfiable() throws TimeoutException {
268 return solver.isSatisfiable();
269 }
270
271
272
273
274
275
276 public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
277 return solver.isSatisfiable(assumps);
278 }
279
280
281
282
283
284
285 public void setTimeout(int t) {
286 solver.setTimeout(t);
287 }
288
289
290
291
292
293
294 public void setTimeoutMs(long t) {
295 solver.setTimeoutMs(t);
296 }
297
298
299
300
301
302
303 public void expireTimeout() {
304 solver.expireTimeout();
305 }
306
307
308
309
310
311
312 public int nConstraints() {
313 return solver.nConstraints();
314 }
315
316
317
318
319
320
321 public int nVars() {
322 return solver.nVars();
323 }
324
325
326
327
328
329
330 public void reset() {
331 solver.reset();
332 }
333
334 public T decorated() {
335 return solver;
336 }
337
338
339
340
341
342
343
344 public T clearDecorated() {
345 T decorated = solver;
346 solver = null;
347 return decorated;
348 }
349
350
351
352
353
354
355 public boolean removeConstr(IConstr c) {
356 return solver.removeConstr(c);
357 }
358
359
360
361
362
363
364 public Map<String, Number> getStat() {
365 return solver.getStat();
366 }
367
368
369
370
371 public void setSearchListener(SearchListener sl) {
372 solver.setSearchListener(sl);
373 }
374
375
376
377
378 public int nextFreeVarId(boolean reserve) {
379 return solver.nextFreeVarId(reserve);
380 }
381
382
383
384
385 public boolean removeSubsumedConstr(IConstr c) {
386 return solver.removeSubsumedConstr(c);
387 }
388
389
390
391
392 public SearchListener getSearchListener() {
393 return solver.getSearchListener();
394 }
395
396
397
398
399 public boolean isVerbose() {
400 return solver.isVerbose();
401 }
402
403
404
405
406 public void setVerbose(boolean value) {
407 solver.setVerbose(value);
408 }
409
410
411
412
413 public void setLogPrefix(String prefix) {
414 solver.setLogPrefix(prefix);
415 }
416
417
418
419
420 public String getLogPrefix() {
421 return solver.getLogPrefix();
422 }
423
424
425
426
427 public IVecInt unsatExplanation() {
428 return solver.unsatExplanation();
429 }
430
431 }