Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
156   501   33   3,39
58   347   0,5   46
46     1,7  
1    
 
  CSPReader       Line # 66 156 33 0% 0.0
 
No Tests
 
1    /*
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le
3    * Berre
4    *
5    * Based on the original minisat specification from:
6    *
7    * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
8    * Sixth International Conference on Theory and Applications of Satisfiability
9    * Testing, LNCS 2919, pp 502-518, 2003.
10    *
11    * This library is free software; you can redistribute it and/or modify it under
12    * the terms of the GNU Lesser General Public License as published by the Free
13    * Software Foundation; either version 2.1 of the License, or (at your option)
14    * any later version.
15    *
16    * This library is distributed in the hope that it will be useful, but WITHOUT
17    * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
18    * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
19    * details.
20    *
21    * You should have received a copy of the GNU Lesser General Public License
22    * along with this library; if not, write to the Free Software Foundation, Inc.,
23    * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
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    * This class is a CSP to SAT translator that is able to read a CSP problem
56    * using the First CSP solver competition input format and that translates it
57    * into clausal and cardinality (equality) constraints.
58    *
59    * That code has not been tested very thoroughtly yet and was written very
60    * quickly to meet the competition deadline :=)) There is plenty of room for
61    * improvement.
62    *
63    * @author leberre
64    *
65    */
 
66    public class CSPReader extends Reader implements org.sat4j.csp.xml.ICSPCallback {
67   
68    private final ISolver solver;
69   
70    // private Var[] vars;
71   
72    protected Relation[] relations;
73   
74    private int valueindex;
75   
76    // private int varindex;
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  0 toggle public CSPReader(ISolver solver) {
115  0 this.solver = solver;
116  0 predmapping.put("global:allDifferent", new AllDiff());
117    }
118   
 
119  0 toggle @Override
120    public final IProblem parseInstance(final java.io.Reader in)
121    throws ParseFormatException, ContradictionException, IOException {
122  0 return parseInstance(new LineNumberReader(in));
123   
124    }
125   
 
126  0 toggle private IProblem parseInstance(LineNumberReader in)
127    throws ParseFormatException, ContradictionException {
128  0 solver.reset();
129  0 try {
130  0 readProblem(in);
131  0 return solver;
132    } catch (NumberFormatException e) {
133  0 throw new ParseFormatException("integer value expected on line "
134    + in.getLineNumber(), e);
135    }
136    }
137   
 
138  0 toggle @Override
139    public void decode(int[] model, PrintWriter out) {
140    // verifier que les variables sont bien dans le bon ordre !!!!
141  0 for (Var v : varmapping.values()) {
142  0 out.print(v.findValue(model));
143  0 out.print(" ");
144    }
145    }
146   
 
147  0 toggle @Override
148    public String decode(int[] model) {
149  0 StringBuilder stb = new StringBuilder();
150    // verifier que les variables sont bien dans le bon ordre !!!!
151  0 for (Var v : varmapping.values()) {
152  0 stb.append(v.findValue(model));
153  0 stb.append(" ");
154    }
155  0 return stb.toString();
156    }
157   
 
158  0 toggle private void readProblem(LineNumberReader in) throws ContradictionException {
159  0 Scanner input = new Scanner(in);
160    // discard problem name
161  0 beginInstance(input.nextLine());
162   
163    // read number of domain
164  0 int nbdomain = input.nextInt();
165  0 beginDomainsSection(nbdomain);
166   
167  0 for (int i = 0; i < nbdomain; i++) {
168    // read domain number
169  0 int dnum = input.nextInt();
170  0 assert dnum == i;
171    // read domain
172  0 int[] domain = readArrayOfInt(input);
173  0 beginDomain("" + dnum, domain.length);
174  0 for (int j = 0; j < domain.length; j++) {
175  0 addDomainValue(domain[j]);
176    }
177  0 endDomain();
178    }
179  0 endDomainsSection();
180  0 int nbvar = input.nextInt();
181  0 beginVariablesSection(nbvar);
182  0 for (int i = 0; i < nbvar; i++) {
183    // read var number
184  0 int varnum = input.nextInt();
185  0 assert varnum == i;
186    // read var domain
187  0 int vardom = input.nextInt();
188  0 addVariable("" + varnum, "" + vardom);
189    }
190  0 endVariablesSection();
191   
192    // relation definition
193    // read number of relations
194  0 int nbrel = input.nextInt();
195  0 beginRelationsSection(nbrel);
196  0 for (int i = 0; i < nbrel; i++) {
197   
198    // read relation number
199  0 int relnum = input.nextInt();
200  0 assert relnum == i;
201   
202  0 boolean forbidden = input.nextInt() == 1 ? false : true;
203  0 int[] rdomains = readArrayOfInt(input);
204   
205  0 int nbtuples = input.nextInt();
206   
207  0 beginRelation("" + relnum, rdomains.length, nbtuples, !forbidden);
208   
209  0 for (int j = 0; j < nbtuples; j++) {
210  0 int[] tuple = readArrayOfInt(input, relations[relnum].arity());
211    // do something with tuple
212  0 addRelationTuple(tuple);
213    }
214   
215  0 endRelation();
216    }
217  0 endRelationsSection();
218  0 int nbconstr = input.nextInt();
219  0 beginConstraintsSection(nbconstr);
220    // constraint definition
221  0 for (int i = 0; i < nbconstr; i++) {
222  0 int[] variables = readArrayOfInt(input);
223  0 beginConstraint("" + i, variables.length);
224  0 int relnum = input.nextInt();
225    // manage constraint
226  0 constraintReference("" + relnum);
227  0 for (int v : variables) {
228  0 addEffectiveParameter("" + v);
229    }
230  0 endConstraint();
231    }
232  0 endConstraintsSection();
233  0 endInstance();
234    }
235   
 
236  0 toggle protected void manageAllowedTuples(int relnum, int arity, int nbtuples) {
237  0 relations[relnum] = new WalshSupports(arity, nbtuples);
238    }
239   
240    // private Var[] intToVar(int[] variables) {
241    // Var[] nvars = new Var[variables.length];
242    // for (int i = 0; i < variables.length; i++)
243    // nvars[i] = vars[variables[i]];
244    // return nvars;
245    // }
246   
 
247  0 toggle private int[] readArrayOfInt(Scanner input) {
248  0 int size = input.nextInt();
249  0 return readArrayOfInt(input, size);
250    }
251   
 
252  0 toggle private int[] readArrayOfInt(Scanner input, int size) {
253  0 int[] tab = new int[size];
254  0 for (int i = 0; i < size; i++)
255  0 tab[i] = input.nextInt();
256  0 return tab;
257    }
258   
 
259  0 toggle public void beginInstance(String arg0) {
260  0 System.out.println("c reading problem named " + arg0);
261    }
262   
 
263  0 toggle public void beginDomainsSection(int nbdomain) {
264  0 System.out.print("c reading domains");
265    }
266   
 
267  0 toggle public void beginDomain(String id, int size) {
268  0 currentdomainsize = size;
269  0 currentdomain = null;
270  0 valueindex = -1;
271  0 currentdomainid = id;
272  0 rangedomain = null;
273    }
274   
 
275  0 toggle public void addDomainValue(int arg0) {
276  0 if (currentdomain == null) {
277  0 currentdomain = new int[currentdomainsize];
278    }
279  0 if (rangedomain != null) {
280  0 for (int i = 0; i < rangedomain.size(); i++)
281  0 currentdomain[++valueindex] = rangedomain.get(i);
282  0 rangedomain = null;
283    }
284  0 currentdomain[++valueindex] = arg0;
285    }
286   
 
287  0 toggle public void addDomainValue(int begin, int end) {
288  0 if (currentdomainsize == end - begin + 1)
289  0 rangedomain = new RangeDomain(begin, end);
290    else {
291  0 if (currentdomain == null) {
292  0 currentdomain = new int[currentdomainsize];
293    }
294  0 for (int v = begin; v <= end; v++)
295  0 currentdomain[++valueindex] = v;
296    }
297    }
298   
 
299  0 toggle public void endDomain() {
300  0 assert rangedomain != null || valueindex == currentdomain.length - 1;
301  0 if (rangedomain == null)
302  0 domainmapping.put(currentdomainid, new EnumeratedDomain(
303    currentdomain));
304    else
305  0 domainmapping.put(currentdomainid, rangedomain);
306    }
307   
 
308  0 toggle public void endDomainsSection() {
309  0 System.out.println(" done.");
310    }
311   
 
312  0 toggle public void beginVariablesSection(int nbvars) {
313  0 System.out.print("c reading variables");
314  0 nbvarstocreate = 0;
315  0 this.nbvars = nbvars;
316    }
317   
 
318  0 toggle public void addVariable(String idvar, String iddomain) {
319  0 Domain vardom = domainmapping.get(iddomain);
320  0 varmapping.put(idvar, new Var(idvar, vardom, nbvarstocreate));
321  0 nbvarstocreate += vardom.size();
322  0 if (isVerbose())
323  0 System.out.print("\rc reading variables " + varmapping.size() + "/"
324    + nbvars);
325   
326    }
327   
 
328  0 toggle public void endVariablesSection() {
329  0 if (isVerbose())
330  0 System.out.println("\rc reading variables (" + nbvars + ") done.");
331    else
332  0 System.out.println(" done.");
333  0 solver.newVar(nbvarstocreate);
334  0 try {
335  0 for (Evaluable v : varmapping.values()) {
336  0 v.toClause(solver);
337    }
338    } catch (ContradictionException ce) {
339    assert false;
340    }
341   
342    }
343   
 
344  0 toggle public void beginRelationsSection(int nbrel) {
345  0 System.out.print("c reading relations");
346  0 relations = new Relation[nbrel];
347  0 relindex = -1;
348    }
349   
 
350  0 toggle public void beginRelation(String name, int arity, int nbTuples,
351    boolean isSupport) {
352  0 relmapping.put(name, ++relindex);
353  0 if (isVerbose())
354  0 System.out.print("\rc reading relations " + relindex + "/"
355    + relations.length);
356  0 if (isSupport) {
357  0 manageAllowedTuples(relindex, arity, nbTuples);
358    } else {
359  0 relations[relindex] = new Nogoods(arity, nbTuples);
360    }
361  0 tupleindex = -1;
362    }
363   
 
364  0 toggle public void addRelationTuple(int[] tuple) {
365  0 relations[relindex].addTuple(++tupleindex, tuple);
366    }
367   
 
368  0 toggle public void endRelation() {
369    }
370   
 
371  0 toggle public void endRelationsSection() {
372  0 if (isVerbose())
373  0 System.out.println("\rc reading relations (" + relations.length
374    + ") done.");
375    else
376  0 System.out.println(" done.");
377    }
378   
 
379  0 toggle public void beginPredicatesSection(int arg0) {
380  0 System.out.print("c reading predicates ");
381    }
382   
 
383  0 toggle public void beginPredicate(String name) {
384  0 currentpredicate = new Predicate();
385  0 predmapping.put(name, currentpredicate);
386  0 if (isVerbose())
387  0 System.out.print("\rc reading predicate " + predmapping.size());
388    }
389   
 
390  0 toggle public void addFormalParameter(String name, String type) {
391  0 currentpredicate.addVariable(name);
392   
393    }
394   
 
395  0 toggle public void predicateExpression(String expr) {
396  0 currentpredicate.setExpression(expr);
397    }
398   
 
399  0 toggle public void endPredicate() {
400    // TODO Auto-generated method stub
401    }
402   
 
403  0 toggle public void endPredicatesSection() {
404  0 if (isVerbose())
405  0 System.out.println("\rc reading relations (" + predmapping.size()
406    + ") done.");
407    else
408  0 System.out.println(" done.");
409    }
410   
 
411  0 toggle public void beginConstraintsSection(int arg0) {
412  0 System.out.println("c reading constraints");
413  0 nbconstraints = arg0;
414  0 currentconstraint = 0;
415    }
416   
 
417  0 toggle public void beginConstraint(String name, int arity) {
418  0 variables.clear();
419  0 variables.ensure(arity);
420  0 scope.clear();
421  0 scope.ensure(arity);
422  0 if (isVerbose())
423  0 System.out.print("\rc grounding constraint " + name + "("
424    + (++currentconstraint * 100 / nbconstraints) + "%)");
425    }
426   
 
427  0 toggle public void constraintReference(String ref) {
428  0 Integer id = relmapping.get(ref);
429  0 if (id == null) {
430  0 currentclausifiable = predmapping.get(ref);
431    } else {
432  0 currentclausifiable = relations[id];
433    }
434    }
435   
 
436  0 toggle public void addVariableToConstraint(String arg0) {
437  0 scope.push(varmapping.get(arg0));
438    }
439   
 
440  0 toggle public void addEffectiveParameter(String arg0) {
441  0 variables.push(varmapping.get(arg0));
442    }
443   
 
444  0 toggle public void addEffectiveParameter(int arg0) {
445  0 variables.push(new Constant(arg0));
446    }
447   
 
448  0 toggle public void beginParameterList() {
449  0 throw new UnsupportedOperationException(
450    "I do not handle parameter list yet!");
451   
452    }
453   
 
454  0 toggle public void addIntegerItem(int arg0) {
455    // TODO Auto-generated method stub
456   
457    }
458   
 
459  0 toggle public void addVariableItem(String arg0) {
460    // TODO Auto-generated method stub
461   
462    }
463   
 
464  0 toggle public void endParamaterList() {
465    // TODO Auto-generated method stub
466   
467    }
468   
 
469  0 toggle public void addConstantParameter(String arg0, int arg1) {
470  0 throw new UnsupportedOperationException(
471    "I do not handle constant parameter yet!");
472    }
473   
 
474  0 toggle public void constraintExpression(String arg0) {
475  0 throw new UnsupportedOperationException(
476    "I do not handle constraint expression yet!");
477    }
478   
 
479  0 toggle public void endConstraint() {
480  0 try {
481  0 currentclausifiable.toClause(solver, scope, variables);
482    } catch (ContradictionException e) {
483  0 System.err.println("c INSTANCE TRIVIALLY UNSAT");
484    }
485    }
486   
 
487  0 toggle public void endConstraintsSection() {
488  0 if (isVerbose())
489  0 System.out.println("\rc reading constraints done.");
490    else
491  0 System.out.println("c done with constraints.");
492    }
493   
 
494  0 toggle public void endInstance() {
495    // TODO Auto-generated method stub
496    }
497   
 
498  0 toggle IProblem getProblem() {
499  0 return solver;
500    }
501    }
 
CloverReport generated by Clover Code Coverage v2.0a5
mer. juin 27 2007 07:27:33 CEST.		   Beta Testers License registered to clover-support@cenqua.com. This license of Clover2 is provided for beta testing only. You have 5 day(s) before your Beta Tester License expires.