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.ObjectInputStream;
31 import java.io.PrintStream;
32 import java.io.PrintWriter;
33 import java.util.Map;
34
35 import org.sat4j.specs.ContradictionException;
36 import org.sat4j.specs.IConstr;
37 import org.sat4j.specs.ISolver;
38 import org.sat4j.specs.IVec;
39 import org.sat4j.specs.IVecInt;
40 import org.sat4j.specs.IteratorInt;
41 import org.sat4j.specs.SearchListener;
42 import org.sat4j.specs.TimeoutException;
43
44
45
46
47
48
49
50
51
52 public class DimacsOutputSolver implements ISolver {
53
54
55
56
57 private static final long serialVersionUID = 1L;
58
59 private transient PrintWriter out;
60
61 private int nbvars;
62
63 private int nbclauses;
64
65 private boolean fixedNbClauses = false;
66
67 private boolean firstConstr = true;
68
69 public DimacsOutputSolver() {
70 this(new PrintWriter(System.out, true));
71 }
72
73 public DimacsOutputSolver(PrintWriter pw) {
74 out = pw;
75 }
76
77 private void readObject(ObjectInputStream stream) {
78 out = new PrintWriter(System.out, true);
79 }
80
81 public int newVar() {
82 return 0;
83 }
84
85 public int newVar(int howmany) {
86 out.print("p cnf " + howmany);
87 nbvars = howmany;
88 return 0;
89 }
90
91 public void setExpectedNumberOfClauses(int nb) {
92 out.println(" " + nb);
93 nbclauses = nb;
94 fixedNbClauses = true;
95 }
96
97 public IConstr addClause(IVecInt literals) throws ContradictionException {
98 if (firstConstr) {
99 if (!fixedNbClauses) {
100 out.println(" XXXXXX");
101 }
102 firstConstr = false;
103 }
104 for (IteratorInt iterator = literals.iterator(); iterator.hasNext();)
105 out.print(iterator.next() + " ");
106 out.println("0");
107 return null;
108 }
109
110 public boolean removeConstr(IConstr c) {
111 throw new UnsupportedOperationException();
112 }
113
114 public void addAllClauses(IVec<IVecInt> clauses)
115 throws ContradictionException {
116 throw new UnsupportedOperationException();
117 }
118
119 public IConstr addAtMost(IVecInt literals, int degree)
120 throws ContradictionException {
121 if (degree > 1) {
122 throw new UnsupportedOperationException(
123 "Not a clausal problem! degree " + degree);
124 }
125 assert degree == 1;
126 if (firstConstr) {
127 if (!fixedNbClauses) {
128 out.println("XXXXXX");
129 }
130 firstConstr = false;
131 }
132 for (int i = 0; i <= literals.size(); i++) {
133 for (int j = i + 1; j < literals.size(); j++) {
134 out.println("" + (-literals.get(i)) + " " + (-literals.get(j))
135 + " 0");
136 }
137 }
138 return null;
139 }
140
141 public IConstr addAtLeast(IVecInt literals, int degree)
142 throws ContradictionException {
143 if (degree > 1) {
144 throw new UnsupportedOperationException(
145 "Not a clausal problem! degree " + degree);
146 }
147 assert degree == 1;
148 return addClause(literals);
149 }
150
151 public void setTimeout(int t) {
152
153 }
154
155 public void setTimeoutMs(long t) {
156
157 }
158
159 public int getTimeout() {
160 return 0;
161 }
162
163
164
165
166 public long getTimeoutMs() {
167 return 0L;
168 }
169
170 public void reset() {
171 fixedNbClauses = false;
172 firstConstr = true;
173
174 }
175
176 public void printStat(PrintStream output, String prefix) {
177
178
179 }
180
181 public void printStat(PrintWriter output, String prefix) {
182
183
184 }
185
186 public Map<String, Number> getStat() {
187
188 return null;
189 }
190
191 public String toString(String prefix) {
192 return "Dimacs output solver";
193 }
194
195 public void clearLearntClauses() {
196
197
198 }
199
200 public int[] model() {
201 throw new UnsupportedOperationException();
202 }
203
204 public boolean model(int var) {
205 throw new UnsupportedOperationException();
206 }
207
208 public boolean isSatisfiable() throws TimeoutException {
209 throw new TimeoutException("There is no real solver behind!");
210 }
211
212 public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
213 throw new TimeoutException("There is no real solver behind!");
214 }
215
216 public int[] findModel() throws TimeoutException {
217 throw new UnsupportedOperationException();
218 }
219
220 public int[] findModel(IVecInt assumps) throws TimeoutException {
221 throw new UnsupportedOperationException();
222 }
223
224 public int nConstraints() {
225 return nbclauses;
226 }
227
228 public int nVars() {
229 return nbvars;
230 }
231
232 public void expireTimeout() {
233
234
235 }
236
237 public boolean isSatisfiable(IVecInt assumps, boolean global)
238 throws TimeoutException {
239 throw new TimeoutException("There is no real solver behind!");
240 }
241
242 public boolean isSatisfiable(boolean global) throws TimeoutException {
243 throw new TimeoutException("There is no real solver behind!");
244 }
245
246 public void printInfos(PrintWriter output, String prefix) {
247 }
248
249 public void setTimeoutOnConflicts(int count) {
250 }
251
252 public boolean isDBSimplificationAllowed() {
253 return false;
254 }
255
256 public void setDBSimplificationAllowed(boolean status) {
257 }
258
259
260
261
262 public void setSearchListener(SearchListener sl) {
263 }
264
265
266
267
268 public int nextFreeVarId(boolean reserve) {
269 throw new UnsupportedOperationException();
270 }
271
272
273
274
275 public boolean removeSubsumedConstr(IConstr c) {
276 return false;
277 }
278
279
280
281
282 public IConstr addBlockingClause(IVecInt literals)
283 throws ContradictionException {
284 throw new UnsupportedOperationException();
285 }
286
287
288
289
290 public SearchListener getSearchListener() {
291 throw new UnsupportedOperationException();
292 }
293
294
295
296
297 public boolean isVerbose() {
298 return true;
299 }
300
301
302
303
304 public void setVerbose(boolean value) {
305
306 }
307
308
309
310
311 public void setLogPrefix(String prefix) {
312
313
314 }
315
316
317
318
319 public String getLogPrefix() {
320 return "";
321 }
322
323
324
325
326 public IVecInt unsatExplanation() {
327 throw new UnsupportedOperationException();
328 }
329 }