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