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