1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19 package org.sat4j.reader;
20
21 import java.io.IOException;
22 import java.io.LineNumberReader;
23 import java.io.PrintWriter;
24 import java.util.HashMap;
25 import java.util.LinkedHashMap;
26 import java.util.Map;
27 import java.util.Scanner;
28
29 import org.sat4j.core.Vec;
30 import org.sat4j.csp.Clausifiable;
31 import org.sat4j.csp.Constant;
32 import org.sat4j.csp.Domain;
33 import org.sat4j.csp.EnumeratedDomain;
34 import org.sat4j.csp.Evaluable;
35 import org.sat4j.csp.Predicate;
36 import org.sat4j.csp.RangeDomain;
37 import org.sat4j.csp.Var;
38 import org.sat4j.csp.constraints.AllDiff;
39 import org.sat4j.csp.constraints.Nogoods;
40 import org.sat4j.csp.constraints.Relation;
41 import org.sat4j.csp.constraints.WalshSupports;
42 import org.sat4j.specs.ContradictionException;
43 import org.sat4j.specs.IProblem;
44 import org.sat4j.specs.ISolver;
45 import org.sat4j.specs.IVec;
46
47
48
49
50
51
52
53
54
55
56
57
58
59 public class CSPReader extends Reader implements org.sat4j.csp.xml.ICSPCallback {
60
61 private final ISolver solver;
62
63
64
65 protected Relation[] relations;
66
67 private int valueindex;
68
69
70
71 private int relindex;
72
73 private int[] currentdomain;
74
75 private Domain rangedomain;
76
77 private String currentdomainid;
78
79 private int currentdomainsize;
80
81 private final Map<String, Domain> domainmapping = new HashMap<String, Domain>();
82
83 private final Map<String, Var> varmapping = new LinkedHashMap<String, Var>();
84
85 private final Map<String, Integer> relmapping = new HashMap<String, Integer>();
86
87 private final Map<String, Clausifiable> predmapping = new HashMap<String, Clausifiable>();
88
89 private int nbvarstocreate;
90
91 private int tupleindex;
92
93 private Clausifiable currentclausifiable;
94
95 private Predicate currentpredicate;
96
97 private final IVec<Evaluable> variables = new Vec<Evaluable>();
98
99 private final IVec<Var> scope = new Vec<Var>();
100
101 private int nbvars;
102
103 private int nbconstraints;
104
105 private int currentconstraint;
106
107 public CSPReader(ISolver solver) {
108 this.solver = solver;
109 Clausifiable allDiff = new AllDiff();
110 predmapping.put("global:allDifferent",allDiff);
111 predmapping.put("global:alldifferent",allDiff);
112 }
113
114 @Override
115 public final IProblem parseInstance(final java.io.Reader in)
116 throws ParseFormatException, ContradictionException, IOException {
117 return parseInstance(new LineNumberReader(in));
118
119 }
120
121 private IProblem parseInstance(LineNumberReader in)
122 throws ParseFormatException {
123 solver.reset();
124 try {
125 readProblem(in);
126 return solver;
127 } catch (NumberFormatException e) {
128 throw new ParseFormatException("integer value expected on line "
129 + in.getLineNumber(), e);
130 }
131 }
132
133 @Override
134 public void decode(int[] model, PrintWriter out) {
135
136 for (Var v : varmapping.values()) {
137 out.print(v.findValue(model));
138 out.print(" ");
139 }
140 }
141
142 @Override
143 public String decode(int[] model) {
144 StringBuilder stb = new StringBuilder();
145
146 for (Var v : varmapping.values()) {
147 stb.append(v.findValue(model));
148 stb.append(" ");
149 }
150 return stb.toString();
151 }
152
153 private void readProblem(LineNumberReader in) {
154 Scanner input = new Scanner(in);
155
156 beginInstance(input.nextLine());
157
158
159 int nbdomain = input.nextInt();
160 beginDomainsSection(nbdomain);
161
162 for (int i = 0; i < nbdomain; i++) {
163
164 int dnum = input.nextInt();
165 assert dnum == i;
166
167 int[] domain = readArrayOfInt(input);
168 beginDomain("" + dnum, domain.length);
169 for (int j = 0; j < domain.length; j++) {
170 addDomainValue(domain[j]);
171 }
172 endDomain();
173 }
174 endDomainsSection();
175 int nbvar = input.nextInt();
176 beginVariablesSection(nbvar);
177 for (int i = 0; i < nbvar; i++) {
178
179 int varnum = input.nextInt();
180 assert varnum == i;
181
182 int vardom = input.nextInt();
183 addVariable("" + varnum, "" + vardom);
184 }
185 endVariablesSection();
186
187
188
189 int nbrel = input.nextInt();
190 beginRelationsSection(nbrel);
191 for (int i = 0; i < nbrel; i++) {
192
193
194 int relnum = input.nextInt();
195 assert relnum == i;
196
197 boolean forbidden = input.nextInt() == 1 ? false : true;
198 int[] rdomains = readArrayOfInt(input);
199
200 int nbtuples = input.nextInt();
201
202 beginRelation("" + relnum, rdomains.length, nbtuples, !forbidden);
203
204 for (int j = 0; j < nbtuples; j++) {
205 int[] tuple = readArrayOfInt(input, relations[relnum].arity());
206
207 addRelationTuple(tuple);
208 }
209
210 endRelation();
211 }
212 endRelationsSection();
213 int nbconstr = input.nextInt();
214 beginConstraintsSection(nbconstr);
215
216 for (int i = 0; i < nbconstr; i++) {
217 int[] theVariables = readArrayOfInt(input);
218 beginConstraint("" + i, theVariables.length);
219 int relnum = input.nextInt();
220
221 constraintReference("" + relnum);
222 for (int v : theVariables) {
223 addEffectiveParameter("" + v);
224 }
225 endConstraint();
226 }
227 endConstraintsSection();
228 endInstance();
229 }
230
231 protected void manageAllowedTuples(int relnum, int arity, int nbtuples) {
232 relations[relnum] = new WalshSupports(arity, nbtuples);
233 }
234
235
236
237
238
239
240
241
242 private int[] readArrayOfInt(Scanner input) {
243 int size = input.nextInt();
244 return readArrayOfInt(input, size);
245 }
246
247 private int[] readArrayOfInt(Scanner input, int size) {
248 int[] tab = new int[size];
249 for (int i = 0; i < size; i++)
250 tab[i] = input.nextInt();
251 return tab;
252 }
253
254 public void beginInstance(String arg0) {
255 System.out.println("c reading problem named " + arg0);
256 }
257
258 public void beginDomainsSection(int nbdomain) {
259 System.out.print("c reading domains");
260 }
261
262 public void beginDomain(String id, int size) {
263 currentdomainsize = size;
264 currentdomain = null;
265 valueindex = -1;
266 currentdomainid = id;
267 rangedomain = null;
268 }
269
270 public void addDomainValue(int arg0) {
271 if (currentdomain == null) {
272 currentdomain = new int[currentdomainsize];
273 }
274 if (rangedomain != null) {
275 for (int i = 0; i < rangedomain.size(); i++)
276 currentdomain[++valueindex] = rangedomain.get(i);
277 rangedomain = null;
278 }
279 currentdomain[++valueindex] = arg0;
280 }
281
282 public void addDomainValue(int begin, int end) {
283 if (currentdomainsize == end - begin + 1)
284 rangedomain = new RangeDomain(begin, end);
285 else {
286 if (currentdomain == null) {
287 currentdomain = new int[currentdomainsize];
288 }
289 for (int v = begin; v <= end; v++)
290 currentdomain[++valueindex] = v;
291 }
292 }
293
294 public void endDomain() {
295 assert rangedomain != null || valueindex == currentdomain.length - 1;
296 if (rangedomain == null)
297 domainmapping.put(currentdomainid, new EnumeratedDomain(
298 currentdomain));
299 else
300 domainmapping.put(currentdomainid, rangedomain);
301 }
302
303 public void endDomainsSection() {
304 System.out.println(" done.");
305 }
306
307 public void beginVariablesSection(int expectedNumberOfVariables) {
308 System.out.print("c reading variables");
309 nbvarstocreate = 0;
310 this.nbvars = expectedNumberOfVariables;
311 }
312
313 public void addVariable(String idvar, String iddomain) {
314 Domain vardom = domainmapping.get(iddomain);
315 varmapping.put(idvar, new Var(idvar, vardom, nbvarstocreate));
316 nbvarstocreate += vardom.size();
317 if (isVerbose())
318 System.out.print("\rc reading variables " + varmapping.size() + "/"
319 + nbvars);
320
321 }
322
323 public void endVariablesSection() {
324 if (isVerbose())
325 System.out.println("\rc reading variables (" + nbvars + ") done.");
326 else
327 System.out.println(" done.");
328 solver.newVar(nbvarstocreate);
329 try {
330 for (Evaluable v : varmapping.values()) {
331 v.toClause(solver);
332 }
333 } catch (ContradictionException ce) {
334 assert false;
335 }
336
337 }
338
339 public void beginRelationsSection(int nbrel) {
340 System.out.print("c reading relations");
341 relations = new Relation[nbrel];
342 relindex = -1;
343 }
344
345 public void beginRelation(String name, int arity, int nbTuples,
346 boolean isSupport) {
347 relmapping.put(name, ++relindex);
348 if (isVerbose())
349 System.out.print("\rc reading relations " + relindex + "/"
350 + relations.length);
351 if (isSupport) {
352 manageAllowedTuples(relindex, arity, nbTuples);
353 } else {
354 relations[relindex] = new Nogoods(arity, nbTuples);
355 }
356 tupleindex = -1;
357 }
358
359 public void addRelationTuple(int[] tuple) {
360 relations[relindex].addTuple(++tupleindex, tuple);
361 }
362
363 public void endRelation() {
364 }
365
366 public void endRelationsSection() {
367 if (isVerbose())
368 System.out.println("\rc reading relations (" + relations.length
369 + ") done.");
370 else
371 System.out.println(" done.");
372 }
373
374 public void beginPredicatesSection(int arg0) {
375 System.out.print("c reading predicates ");
376 }
377
378 public void beginPredicate(String name) {
379 currentpredicate = new Predicate();
380 predmapping.put(name, currentpredicate);
381 if (isVerbose())
382 System.out.print("\rc reading predicate " + predmapping.size());
383 }
384
385 public void addFormalParameter(String name, String type) {
386 currentpredicate.addVariable(name);
387
388 }
389
390 public void predicateExpression(String expr) {
391 currentpredicate.setExpression(expr);
392 }
393
394 public void endPredicate() {
395
396 }
397
398 public void endPredicatesSection() {
399 if (isVerbose())
400 System.out.println("\rc reading relations (" + predmapping.size()
401 + ") done.");
402 else
403 System.out.println(" done.");
404 }
405
406 public void beginConstraintsSection(int arg0) {
407 System.out.println("c reading constraints");
408 nbconstraints = arg0;
409 currentconstraint = 0;
410 }
411
412 public void beginConstraint(String name, int arity) {
413 variables.clear();
414 variables.ensure(arity);
415 scope.clear();
416 scope.ensure(arity);
417 if (isVerbose())
418 System.out.print("\rc grounding constraint " + name + "("
419 + (++currentconstraint * 100 / nbconstraints) + "%)");
420 }
421
422 public void constraintReference(String ref) {
423 Integer id = relmapping.get(ref);
424 if (id == null) {
425 currentclausifiable = predmapping.get(ref);
426 } else {
427 currentclausifiable = relations[id];
428 }
429 if (currentclausifiable ==null) {
430 throw new IllegalArgumentException("Reference not supported: "+ref);
431 }
432 }
433
434 public void addVariableToConstraint(String arg0) {
435 scope.push(varmapping.get(arg0));
436 }
437
438 public void addEffectiveParameter(String arg0) {
439 variables.push(varmapping.get(arg0));
440 }
441
442 public void addEffectiveParameter(int arg0) {
443 variables.push(new Constant(arg0));
444 }
445
446 public void beginParameterList() {
447 throw new UnsupportedOperationException(
448 "I do not handle parameter list yet!");
449
450 }
451
452 public void addIntegerItem(int arg0) {
453
454
455 }
456
457 public void addVariableItem(String arg0) {
458
459
460 }
461
462 public void endParamaterList() {
463
464
465 }
466
467 public void addConstantParameter(String arg0, int arg1) {
468 throw new UnsupportedOperationException(
469 "I do not handle constant parameter yet!");
470 }
471
472 public void constraintExpression(String arg0) {
473 throw new UnsupportedOperationException(
474 "I do not handle constraint expression yet!");
475 }
476
477 public void endConstraint() {
478 try {
479 currentclausifiable.toClause(solver, scope, variables);
480 } catch (ContradictionException e) {
481 System.err.println("c INSTANCE TRIVIALLY UNSAT");
482 }
483 }
484
485 public void endConstraintsSection() {
486 if (isVerbose())
487 System.out.println("\rc reading constraints done.");
488 else
489 System.out.println("c done with constraints.");
490 }
491
492 public void endInstance() {
493
494 }
495
496 IProblem getProblem() {
497 return solver;
498 }
499 }