Clover coverage report -
Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 189   Methods: 5
NCLOC: 142   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
GoodOPBReader.java 73,9% 81,8% 80% 78,9%
coverage coverage
 1    /*
 2    * Created on 8 sept. 2004
 3    *
 4    * To change the template for this generated file go to
 5    * Window - Preferences - Java - Code Generation - Code and Comments
 6    */
 7    package org.sat4j.reader;
 8   
 9    import java.io.IOException;
 10    import java.io.LineNumberReader;
 11    import java.io.Serializable;
 12    import java.math.BigInteger;
 13    import java.util.HashMap;
 14    import java.util.Map;
 15    import java.util.Scanner;
 16   
 17    import org.sat4j.core.Vec;
 18    import org.sat4j.core.VecInt;
 19    import org.sat4j.specs.ContradictionException;
 20    import org.sat4j.specs.IProblem;
 21    import org.sat4j.specs.ISolver;
 22    import org.sat4j.specs.IVec;
 23    import org.sat4j.specs.IVecInt;
 24   
 25    /**
 26    * This class is a quick hack to read opb formatted files. The reader skip
 27    * commented lines (beginning with COMMENT_SYMBOL) and expect constraints of the
 28    * form: [name :] [[+|-]COEF] [*] [+|-]LIT >=|<=|= DEGREE where COEF and DEGREE
 29    * are plain integer and LIT is an identifier.
 30    *
 31    * @author leberre
 32    */
 33    public class GoodOPBReader extends Reader implements Serializable {
 34   
 35    /**
 36    * Comment for <code>serialVersionUID</code>
 37    */
 38    private static final long serialVersionUID = 1L;
 39   
 40    private static final String COMMENT_SYMBOL = "*";
 41   
 42    private final ISolver solver;
 43   
 44    private final Map<String, Integer> map = new HashMap<String, Integer>();
 45   
 46    private final IVec<String> decode = new Vec<String>();
 47   
 48    /**
 49    *
 50    */
 51  840 public GoodOPBReader(ISolver solver) {
 52  840 this.solver = solver;
 53    }
 54   
 55  840 @Override
 56    public final IProblem parseInstance(final java.io.Reader in)
 57    throws ParseFormatException, ContradictionException, IOException {
 58  840 return parseInstance(new LineNumberReader(in));
 59    }
 60   
 61  839 private IProblem parseInstance(LineNumberReader in)
 62    throws ContradictionException, IOException {
 63  839 solver.reset();
 64  839 String line;
 65  ? while ((line = in.readLine()) != null) {
 66    // cannot trim is line is null
 67  1657263 line = line.trim();
 68  1657263 if (line.endsWith(";")) {
 69  1656301 line = line.substring(0, line.length() - 1);
 70    }
 71  1657263 parseLine(line);
 72    }
 73  724 return solver;
 74    }
 75   
 76  1657263 void parseLine(String line) throws ContradictionException {
 77    // Skip commented line
 78  1657263 if (line.startsWith(COMMENT_SYMBOL))
 79  946 return;
 80  1656317 if (line.startsWith("p")) // ignore p cnf with pbchaff format
 81  0 return;
 82  1656317 if (line.startsWith("min:") || line.startsWith("min :"))
 83  576 return; // we will use that case later
 84  1655741 if (line.startsWith("max:") || line.startsWith("max :"))
 85  2 return; // we will use that case later
 86   
 87    // skip name of constraints:
 88  1655739 int index = line.indexOf(":");
 89  1655739 if (index != -1) {
 90  8347 line = line.substring(index + 1);
 91    }
 92   
 93  1655739 IVecInt lits = new VecInt();
 94  1655739 IVec<BigInteger> coeffs = new Vec<BigInteger>();
 95  1655739 Scanner stk = new Scanner(line)
 96    .useDelimiter("\\s*\\*\\s*|\\s*\\+\\s*|\\s+");
 97  1655739 while (stk.hasNext()) {
 98  13375601 String token = stk.next();
 99  13375601 if (token.equals(">=") || token.equals("<=") || token.equals("=")) {
 100    assert stk.hasNext();
 101  1655718 String tok = stk.next();
 102    // we need to remove + from the integer
 103  1655716 if (tok.startsWith("+")) {
 104  0 tok = tok.substring(1);
 105    }
 106  1655716 BigInteger d = new BigInteger(tok);
 107   
 108  1655716 try {
 109  1655716 if (token.equals(">=") || token.equals("=")) {
 110  1654141 solver.addPseudoBoolean(lits, coeffs, true, d);
 111    }
 112  1655625 if (token.equals("<=") || token.equals("=")) {
 113  24136 solver.addPseudoBoolean(lits, coeffs, false, d);
 114    }
 115    } catch (ContradictionException ce) {
 116  90 System.out.println("c inconsistent constraint: " + line);
 117  90 System.out.println("c lits: " + lits);
 118  90 System.out.println("c coeffs: " + coeffs);
 119  90 throw ce;
 120    }
 121    } else {
 122    // on est toujours en train de lire la partie gauche de la
 123    // contrainte
 124  11719883 if (token.equals("+")) {
 125    assert stk.hasNext();
 126  0 token = stk.next();
 127  11719883 } else if (token.equals("-")) {
 128    assert stk.hasNext();
 129  0 token = token + stk.next();
 130    }
 131  11719883 BigInteger coef;
 132    // should contain a coef and a literal
 133  11719883 try {
 134    // we need to remove + from the integer
 135  11719883 if (token.startsWith("+")) {
 136  0 token = token.substring(1);
 137    }
 138  11719883 coef = new BigInteger(token);
 139    assert stk.hasNext();
 140  11594337 token = stk.next();
 141    } catch (NumberFormatException nfe) {
 142    // its only an identifier
 143  125546 coef = BigInteger.ONE;
 144    }
 145  11719883 if (token.equals("-") || token.equals("~")) {
 146    assert stk.hasNext();
 147  4 token = token + stk.next();
 148    }
 149  11719883 boolean negative = false;
 150  11719883 if (token.startsWith("+")) {
 151  0 token = token.substring(1);
 152  11719883 } else if (token.startsWith("-")) {
 153  50763 token = token.substring(1);
 154    assert coef.equals(BigInteger.ONE);
 155  50763 coef = BigInteger.ONE.negate();
 156  11669120 } else if (token.startsWith("~")) {
 157  8 token = token.substring(1);
 158  8 negative = true;
 159    }
 160  11719883 Integer id = map.get(token);
 161  11719883 if (id == null) {
 162  666760 map.put(token, id = solver.newVar());
 163  666741 decode.push(token);
 164    assert decode.size() == id.intValue();
 165    }
 166  11719864 coeffs.push(coef);
 167  11719864 int lid = (negative ? -1 : 1) * id.intValue();
 168  11719864 lits.push(lid);
 169    assert coeffs.size() == lits.size();
 170    }
 171    }
 172    }
 173   
 174  0 @Override
 175    public String decode(int[] model) {
 176  0 StringBuffer stb = new StringBuffer();
 177  0 for (int i = 0; i < model.length; i++) {
 178  0 if (model[i] < 0) {
 179  0 stb.append("-");
 180  0 stb.append(decode.get(-model[i] - 1));
 181    } else {
 182  0 stb.append(decode.get(model[i] - 1));
 183    }
 184  0 stb.append(" ");
 185    }
 186  0 return stb.toString();
 187    }
 188   
 189    }
 
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.