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