Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
211   664   65   6,21
104   370   0,46   34
34     2,88  
1    
 
  OPBReader2005       Line # 51 211 65 0% 0.0
 
No Tests
 
1    /*
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le Berre
3    *
4    * Based on the original minisat specification from:
5    *
6    * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
7    * Sixth International Conference on Theory and Applications of Satisfiability
8    * Testing, LNCS 2919, pp 502-518, 2003.
9    *
10    * This library is free software; you can redistribute it and/or modify it under
11    * the terms of the GNU Lesser General Public License as published by the Free
12    * Software Foundation; either version 2.1 of the License, or (at your option)
13    * any later version.
14    *
15    * This library is distributed in the hope that it will be useful, but WITHOUT
16    * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
17    * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
18    * details.
19    *
20    * You should have received a copy of the GNU Lesser General Public License
21    * along with this library; if not, write to the Free Software Foundation, Inc.,
22    * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
23    *
24    */
25    package org.sat4j.reader;
26   
27    import java.io.BufferedReader;
28    import java.io.IOException;
29    import java.io.LineNumberReader;
30    import java.io.PrintWriter;
31    import java.io.Serializable;
32    import java.math.BigInteger;
33   
34    import org.sat4j.core.Vec;
35    import org.sat4j.core.VecInt;
36    import org.sat4j.specs.ContradictionException;
37    import org.sat4j.specs.IConstr;
38    import org.sat4j.specs.IProblem;
39    import org.sat4j.specs.ISolver;
40    import org.sat4j.specs.IVec;
41    import org.sat4j.specs.IVecInt;
42    import org.sat4j.minisat.constraints.pb.PBConstr;
43   
44    /**
45    * "Official" reader for the Pseudo Boolean evaluation 2005.
46    *
47    * @author leberre
48    * @author or
49    * @author mederic baron
50    */
 
51    public class OPBReader2005 extends Reader implements Serializable {
52   
53    /**
54    * Comment for <code>serialVersionUID</code>
55    */
56    private static final long serialVersionUID = 1L;
57   
58    protected final ISolver solver;
59   
60    private final IVecInt lits;
61   
62    private final IVec<BigInteger> coeffs;
63   
64    private BigInteger d;
65   
66    private String operator;
67   
68    private final IVecInt objectiveVars = new VecInt();
69   
70    private final IVec<BigInteger> objectiveCoeffs = new Vec<BigInteger>();
71   
72    // does the instance have an objective function?
73    private boolean hasObjFunc = false;
74   
75    protected int nbVars, nbConstr; // MetaData: #Variables and #Constraints in
76    // file.
77    protected int nbConstraintsRead;
78    /**
79    * callback called when we get the number of variables and the expected
80    * number of constraints
81    *
82    * @param nbvar:
83    * the number of variables
84    * @param nbconstr:
85    * the number of contraints
86    */
 
87  0 toggle protected void metaData(int nbvar, int nbconstr) {
88  0 solver.newVar(nbvar);
89    }
90   
91    /**
92    * callback called before we read the objective function
93    */
 
94  0 toggle protected void beginObjective() {
95    }
96   
97    /**
98    * callback called after we've read the objective function
99    */
 
100  0 toggle protected void endObjective() {
101  0 assert lits.size() == coeffs.size();
102  0 assert lits.size() == coeffs.size();
103  0 for (int i = 0; i < lits.size(); i++) {
104  0 objectiveVars.push(lits.get(i));
105  0 objectiveCoeffs.push(coeffs.get(i));
106    }
107    }
108   
109    /**
110    * callback called before we read a constraint
111    */
 
112  0 toggle protected void beginConstraint() {
113  0 lits.clear();
114  0 coeffs.clear();
115  0 assert lits.size() == 0;
116  0 assert coeffs.size() == 0;
117    }
118   
119    /**
120    * callback called after we've read a constraint
121    */
122    /**
123    * @throws ContradictionException
124    */
 
125  0 toggle protected void endConstraint() throws ContradictionException {
126   
127  0 assert !(lits.size() == 0);
128  0 assert !(coeffs.size() == 0);
129  0 assert lits.size() == coeffs.size();
130   
131  0 if ("<=".equals(operator) || "=".equals(operator)){
132  0 solver.addPseudoBoolean(lits, coeffs, false, d);
133    }
134  0 if (">=".equals(operator) || "=".equals(operator)){
135  0 solver.addPseudoBoolean(lits, coeffs, true, d);
136    }
137  0 nbConstraintsRead++;
138    }
139   
140    /**
141    * callback called when we read a term of a constraint
142    *
143    * @param coeff:
144    * the coefficient of the term
145    * @param var:
146    * the identifier of the variable
147    */
 
148  0 toggle private void constraintTerm(BigInteger coeff, String var) {
149  0 coeffs.push(coeff);
150  0 lits.push(translateVarToId(var));
151    }
152   
 
153  0 toggle protected int translateVarToId(String var) {
154  0 int id = Integer.parseInt(var.substring(1));
155  0 return ((savedChar == '-') ? -1 : 1) * id;
156    }
157   
158    /**
159    * callback called when we read the relational operator of a constraint
160    *
161    * @param relop:
162    * the relational oerator (>= or =)
163    */
 
164  0 toggle protected void constraintRelOp(String relop) {
165  0 operator = relop;
166    }
167   
168    /**
169    * callback called when we read the right term of a constraint (also known
170    * as the degree)
171    *
172    * @param val:
173    * the degree of the constraint
174    */
 
175  0 toggle protected void constraintRightTerm(BigInteger val) {
176  0 d = val;
177    }
178   
179    transient BufferedReader in; // the stream we're reading from
180   
181    char savedChar; // a character read from the file but not yet consumed
182   
183    boolean charAvailable = false; // true iff savedChar contains a character
184   
185    boolean eofReached = false; // true iff we've reached EOF
186   
187    /**
188    * get the next character from the stream
189    *
190    * @throws IOException
191    */
 
192  0 toggle protected char get() throws IOException {
193  0 int c;
194   
195  0 if (charAvailable) {
196  0 charAvailable = false;
197  0 return savedChar;
198    }
199   
200  0 c = in.read();
201  0 if (c == -1)
202  0 eofReached = true;
203   
204  0 return (char) c;
205    }
206   
 
207  0 toggle public IVecInt getVars() {
208  0 return objectiveVars;
209    }
210   
 
211  0 toggle public IVec<BigInteger> getCoeffs() {
212  0 return objectiveCoeffs;
213    }
214   
215    /**
216    * put back a character into the stream (only one chr can be put back)
217    */
 
218  0 toggle private void putback(char c) {
219  0 savedChar = c;
220  0 charAvailable = true;
221    }
222   
223    /**
224    * return true iff we've reached EOF
225    */
 
226  0 toggle protected boolean eof() {
227  0 return eofReached;
228    }
229   
230    /**
231    * skip white spaces
232    *
233    * @throws IOException
234    */
 
235  0 toggle protected void skipSpaces() throws IOException {
236  0 char c;
237   
238  0 while (Character.isWhitespace(c = get()))
239  0 ;
240   
241  0 putback(c);
242    }
243   
244    /**
245    * read a word from file
246    *
247    * @return the word we read
248    * @throws IOException
249    */
 
250  0 toggle public String readWord() throws IOException {
251  0 StringBuffer s = new StringBuffer();
252  0 char c;
253   
254  0 skipSpaces();
255   
256  0 while (!Character.isWhitespace(c = get()) && !eof())
257  0 s.append(c);
258   
259  0 return s.toString();
260    }
261   
262    /**
263    * read a integer from file
264    *
265    * @param s
266    * a StringBuffer to store the integer that was read
267    * @throws IOException
268    */
 
269  0 toggle public void readInteger(StringBuffer s) throws IOException {
270  0 char c;
271   
272  0 skipSpaces();
273  0 s.setLength(0);
274   
275  0 c = get();
276  0 if (c == '-' || Character.isDigit(c))
277  0 s.append(c);
278    // note: BigInteger don't like a '+' before the number, we just skip it
279   
280  0 while (Character.isDigit(c = get()) && !eof())
281  0 s.append(c);
282   
283  0 putback(c);
284    }
285   
286    /**
287    * read an identifier from stream and store it in s
288    *
289    * @return the identifier we read or null
290    * @throws IOException
291    * @throws ParseFormatException
292    */
 
293  0 toggle protected boolean readIdentifier(StringBuffer s) throws IOException,
294    ParseFormatException {
295  0 char c;
296   
297  0 s.setLength(0);
298   
299  0 skipSpaces();
300   
301    // first char (must be a letter or underscore)
302  0 c = get();
303  0 if (eof())
304  0 return false;
305   
306  0 if (!isGoodFirstCharacter(c)) {
307  0 putback(c);
308  0 return false;
309    }
310   
311  0 s.append(c);
312   
313    // next chars (must be a letter, a digit or an underscore)
314  0 while (true) {
315  0 c = get();
316  0 if (eof())
317  0 break;
318   
319  0 if (isGoodFollowingCharacter(c))
320  0 s.append(c);
321    else {
322  0 putback(c);
323  0 break;
324    }
325    }
326  0 checkId(s);
327  0 return true;
328    }
329   
 
330  0 toggle protected boolean isGoodFirstCharacter(char c){
331  0 return Character.isLetter(c) || c == '_';
332    }
333   
 
334  0 toggle protected boolean isGoodFollowingCharacter(char c){
335  0 return Character.isLetter(c) || Character.isDigit(c) || c == '_';
336    }
337   
 
338  0 toggle protected void checkId(StringBuffer s) throws ParseFormatException{
339    // Small check on the coefficient ID to make sure everything is ok
340  0 int varID = Integer.parseInt(s.substring(1));
341  0 if (varID > nbVars) {
342  0 throw new ParseFormatException(
343    "Variable identifier larger than #variables in metadata.");
344    }
345    }
346    /**
347    * read a relational operator from stream and store it in s
348    *
349    * @return the relational operator we read or null
350    * @throws IOException
351    */
 
352  0 toggle private String readRelOp() throws IOException {
353  0 char c;
354   
355  0 skipSpaces();
356   
357  0 c = get();
358  0 if (eof())
359  0 return null;
360   
361  0 if (c == '=')
362  0 return "=";
363   
364  0 if (c == '>' && get() == '=')
365  0 return ">=";
366   
367  0 return null;
368    }
369   
370    /**
371    * read the first comment line to get the number of variables and the number
372    * of constraints in the file calls metaData with the data that was read
373    *
374    * @throws IOException
375    * @throws ParseException
376    */
 
377  0 toggle protected void readMetaData() throws IOException, ParseFormatException {
378  0 char c;
379  0 String s;
380   
381    // get the number of variables and constraints
382  0 c = get();
383  0 if (c != '*')
384  0 throw new ParseFormatException(
385    "First line of input file should be a comment");
386   
387  0 s = readWord();
388  0 if (eof() || !"#variable=".equals(s))
389  0 throw new ParseFormatException(
390    "First line should contain #variable= as first keyword");
391   
392  0 nbVars = Integer.parseInt(readWord());
393   
394  0 s = readWord();
395  0 if (eof() || !"#constraint=".equals(s))
396  0 throw new ParseFormatException(
397    "First line should contain #constraint= as second keyword");
398   
399  0 nbConstr = Integer.parseInt(readWord());
400   
401    // skip the rest of the line
402  0 in.readLine();
403   
404    // callback to transmit the data
405  0 metaData(nbVars, nbConstr);
406    }
407   
408    /**
409    * skip the comments at the beginning of the file
410    *
411    * @throws IOException
412    */
 
413  0 toggle private void skipComments() throws IOException {
414  0 char c = ' ';
415   
416    // skip further comments
417   
418  0 while (!eof() && (c = get()) == '*') {
419  0 in.readLine();
420    }
421   
422  0 putback(c);
423    }
424   
425    /**
426    * read a term into coeff and var
427    *
428    * @param coeff:
429    * the coefficient of the variable
430    * @param var:
431    * the indentifier we read
432    * @throws IOException
433    * @throws ParseException
434    */
 
435  0 toggle protected void readTerm(StringBuffer coeff, StringBuffer var)
436    throws IOException, ParseFormatException, ContradictionException {
437  0 char c;
438   
439  0 readInteger(coeff);
440   
441  0 skipSpaces();
442  0 c = get();
443  0 if (c != '*')
444  0 throw new ParseFormatException(
445    "'*' expected between a coefficient and a variable");
446   
447  0 if (!readIdentifier(var))
448  0 throw new ParseFormatException("identifier expected");
449    }
450   
451    /**
452    * read the objective line (if any) calls beginObjective, objectiveTerm and
453    * endObjective
454    *
455    * @throws IOException
456    * @throws ParseException
457    */
 
458  0 toggle private void readObjective() throws IOException, ParseFormatException {
459  0 char c;
460  0 StringBuffer var = new StringBuffer();
461  0 StringBuffer coeff = new StringBuffer();
462   
463    // read objective line (if any)
464   
465  0 skipSpaces();
466  0 c = get();
467  0 if (c != 'm') {
468    // no objective line
469  0 putback(c);
470  0 return;
471    }
472   
473  0 hasObjFunc = true;
474  0 if (get() == 'i' && get() == 'n' && get() == ':') {
475  0 beginObjective(); // callback
476   
477  0 while (!eof()) {
478  0 try {
479  0 readTerm(coeff, var);
480    } catch (ContradictionException e) {
481    // TODO Auto-generated catch block
482  0 e.printStackTrace();
483    }
484  0 constraintTerm(new BigInteger(coeff.toString()), var.toString()); // callback
485   
486  0 skipSpaces();
487  0 c = get();
488  0 if (c == ';')
489  0 break; // end of objective
490   
491  0 else if (c == '-' || c == '+' || Character.isDigit(c))
492  0 putback(c);
493    else
494  0 throw new ParseFormatException(
495    "unexpected character in objective function");
496    }
497   
498  0 endObjective();
499    } else
500  0 throw new ParseFormatException(
501    "input format error: 'min:' expected");
502    }
503   
504    /**
505    * read a constraint calls beginConstraint, constraintTerm and endConstraint
506    *
507    * @throws ParseException
508    * @throws IOException
509    * @throws ContradictionException
510    */
 
511  0 toggle private void readConstraint() throws IOException, ParseFormatException,
512    ContradictionException {
513  0 StringBuffer var = new StringBuffer();
514  0 StringBuffer coeff = new StringBuffer();
515  0 char c;
516   
517  0 beginConstraint();
518   
519  0 while (!eof()) {
520  0 readTerm(coeff, var);
521  0 constraintTerm(new BigInteger(coeff.toString()), var.toString());
522   
523  0 skipSpaces();
524  0 c = get();
525  0 if (c == '>' || c == '=') {
526    // relational operator found
527  0 putback(c);
528  0 break;
529  0 } else if (c == '-' || c == '+' || Character.isDigit(c))
530  0 putback(c);
531    else {
532  0 throw new ParseFormatException(
533    "unexpected character in constraint");
534    }
535    }
536   
537  0 if (eof())
538  0 throw new ParseFormatException(
539    "unexpected EOF before end of constraint");
540   
541  0 String relop;
542  0 if ((relop = readRelOp()) == null) {
543  0 throw new ParseFormatException(
544    "unexpected relational operator in constraint");
545   
546    }
547  0 constraintRelOp(relop);
548  0 readInteger(coeff);
549  0 constraintRightTerm(new BigInteger(coeff.toString()));
550   
551  0 skipSpaces();
552  0 c = get();
553  0 if (eof() || c != ';')
554  0 throw new ParseFormatException(
555    "semicolon expected at end of constraint");
556   
557  0 endConstraint();
558    }
559   
 
560  0 toggle public OPBReader2005(ISolver solver) {
561  0 this.solver = solver;
562  0 lits = new VecInt();
563  0 coeffs = new Vec<BigInteger>();
564    }
565   
566    /**
567    * parses the file and uses the callbacks to send to send the data back to
568    * the program
569    *
570    * @throws IOException
571    * @throws ParseException
572    * @throws ContradictionException
573    */
 
574  0 toggle public void parse() throws IOException, ParseFormatException,
575    ContradictionException {
576  0 readMetaData();
577   
578  0 skipComments();
579   
580  0 readObjective();
581   
582    // read constraints
583  0 nbConstraintsRead = 0;
584  0 char c;
585  0 while (!eof()) {
586  0 skipSpaces();
587  0 if (eof())
588  0 break;
589   
590  0 c = get();
591  0 putback(c);
592  0 if (c == '*')
593  0 skipComments();
594   
595  0 if (eof())
596  0 break;
597   
598  0 readConstraint();
599    //nbConstraintsRead++;
600    }
601    // Small check on the number of constraints
602  0 if (nbConstraintsRead != nbConstr) {
603  0 throw new ParseFormatException(
604    "Number of constraints read is different from metadata.");
605    }
606    }
607   
 
608  0 toggle @Override
609    public final IProblem parseInstance(final java.io.Reader in)
610    throws ParseFormatException, ContradictionException {
611  0 return parseInstance(new LineNumberReader(in));
612    }
613   
 
614  0 toggle private IProblem parseInstance(LineNumberReader in)
615    throws ParseFormatException, ContradictionException {
616  0 solver.reset();
617  0 this.in = in;
618  0 try {
619  0 parse();
620  0 return solver;
621    } catch (IOException e) {
622  0 throw new ParseFormatException(e);
623    }
624    }
625   
 
626  0 toggle @Override
627    public String decode(int[] model) {
628  0 StringBuffer stb = new StringBuffer();
629   
630  0 for (int i = 0; i < model.length; i++) {
631  0 if (model[i] < 0) {
632  0 stb.append("-x");
633  0 stb.append(-model[i]);
634    } else {
635  0 stb.append("x");
636  0 stb.append(model[i]);
637    }
638  0 stb.append(" ");
639    }
640  0 return stb.toString();
641    }
642   
 
643  0 toggle @Override
644    public void decode(int[] model, PrintWriter out) {
645  0 for (int i = 0; i < model.length; i++) {
646  0 if (model[i] < 0) {
647  0 out.print("-x");
648  0 out.print(-model[i]);
649    } else {
650  0 out.print("x");
651  0 out.print(model[i]);
652    }
653  0 out.print(" ");
654    }
655    }
656   
 
657  0 toggle public ObjectiveFunction getObjectiveFunction() {
658  0 if (hasObjFunc){
659  0 return new ObjectiveFunction(getVars(), getCoeffs());
660    }
661  0 return null;
662    }
663   
664    }
 
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.