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