Clover coverage report -
Coverage timestamp: jeu. sept. 29 2005 23:57:39 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 332   Methods: 14
NCLOC: 242   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
ExtendedDimacsReader.java 0% 0,7% 7,1% 1,1%
coverage coverage
 1    package org.sat4j.reader;
 2   
 3    import java.io.IOException;
 4    import java.io.LineNumberReader;
 5    import java.util.Scanner;
 6    import java.util.StringTokenizer;
 7   
 8    import org.sat4j.core.VecInt;
 9    import org.sat4j.specs.ContradictionException;
 10    import org.sat4j.specs.ISolver;
 11    import org.sat4j.specs.IVecInt;
 12   
 13    /**
 14    * Reader for the Extended Dimacs format proposed by Fahiem Bacchus
 15    * and Toby Walsh.
 16    *
 17    * @author leberre
 18    *
 19    */
 20    public class ExtendedDimacsReader extends DimacsReader {
 21   
 22    public static final int FALSE = 1;
 23   
 24    public static final int TRUE = 2;
 25   
 26    public static final int NOT = 3;
 27   
 28    public static final int AND = 4;
 29   
 30    public static final int NAND = 5;
 31   
 32    public static final int OR = 6;
 33   
 34    public static final int NOR = 7;
 35   
 36    public static final int XOR = 8;
 37   
 38    public static final int XNOR = 9;
 39   
 40    public static final int IMPLIES = 10;
 41   
 42    public static final int IFF = 11;
 43   
 44    public static final int IFTHENELSE = 12;
 45   
 46    public static final int ATLEAST = 13;
 47   
 48    public static final int ATMOST = 14;
 49   
 50    public static final int COUNT = 15;
 51   
 52    /**
 53    *
 54    *
 55    */
 56    private static final long serialVersionUID = 1L;
 57   
 58  2026 public ExtendedDimacsReader(ISolver solver) {
 59  2026 super(solver);
 60    }
 61   
 62    /**
 63    * @param in
 64    * the input stream
 65    * @throws IOException
 66    * iff an IO occurs
 67    * @throws ParseFormatException
 68    * if the input stream does not comply with the DIMACS format.
 69    */
 70  0 @Override
 71    protected void readProblemLine(LineNumberReader in) throws IOException,
 72    ParseFormatException {
 73   
 74  0 String line = in.readLine();
 75   
 76  0 if (line == null) {
 77  0 throw new ParseFormatException(
 78    "premature end of file: <p noncnf ...> expected on line "
 79    + in.getLineNumber());
 80    }
 81  0 StringTokenizer stk = new StringTokenizer(line);
 82   
 83  0 if (!(stk.hasMoreTokens() && stk.nextToken().equals("p")
 84    && stk.hasMoreTokens() && stk.nextToken().equals("noncnf"))) {
 85  0 throw new ParseFormatException(
 86    "problem line expected (p noncnf ...) on line "
 87    + in.getLineNumber());
 88    }
 89   
 90  0 int vars;
 91   
 92    // reads the max var id
 93  0 vars = Integer.parseInt(stk.nextToken());
 94    assert vars > 0;
 95  0 solver.newVar(vars);
 96  0 try {
 97  0 processClause(new VecInt().push(vars));
 98    } catch (ContradictionException e) {
 99    assert false;
 100  0 System.err.println("Contradiction when asserting root variable?");
 101    }
 102  0 disableNumberOfConstraintCheck();
 103    }
 104   
 105    /*
 106    * (non-Javadoc)
 107    *
 108    * @see org.sat4j.reader.DimacsReader#handleConstr(java.lang.String,
 109    * org.sat4j.specs.IVecInt)
 110    */
 111  0 @Override
 112    protected boolean handleConstr(String line, IVecInt literals)
 113    throws ContradictionException {
 114  0 boolean added = true;
 115    assert literals.size() == 0;
 116  0 Scanner scan = new Scanner(line);
 117  0 while (scan.hasNext()) {
 118  0 int gateType = scan.nextInt();
 119    assert gateType > 0;
 120  0 int nbparam = scan.nextInt();
 121    assert nbparam != 0;
 122    assert nbparam == -1 || gateType >= ATLEAST;
 123  0 int k = -1;
 124  0 for (int i = 0; i < nbparam; i++) {
 125  0 k = scan.nextInt();
 126    }
 127    // readI/O until reaching ending 0
 128  0 int y = scan.nextInt();
 129  0 int x;
 130  0 while ((x = scan.nextInt()) != 0) {
 131  0 literals.push(x);
 132    }
 133  0 switch (gateType) {
 134  0 case FALSE:
 135  0 gateFalse(y, literals);
 136  0 break;
 137  0 case TRUE:
 138  0 gateTrue(y, literals);
 139  0 break;
 140  0 case OR:
 141  0 or(y, literals);
 142  0 break;
 143  0 case NOT:
 144  0 not(y, literals);
 145  0 break;
 146  0 case AND:
 147  0 and(y, literals);
 148  0 break;
 149  0 case XOR:
 150  0 xor(y, literals);
 151  0 break;
 152  0 case IFF:
 153  0 iff(y, literals);
 154  0 break;
 155  0 case IFTHENELSE:
 156  0 ite(y, literals);
 157  0 break;
 158  0 default:
 159  0 throw new UnsupportedOperationException("Gate type "
 160    + gateType + " not handled yet");
 161    }
 162    }
 163  0 literals.clear();
 164  0 return added;
 165    }
 166   
 167  0 private void gateFalse(int y, IVecInt literals)
 168    throws ContradictionException {
 169    assert literals.size() == 0;
 170  0 IVecInt clause = new VecInt(1);
 171  0 clause.push(-y);
 172  0 processClause(clause);
 173    }
 174   
 175  0 private void gateTrue(int y, IVecInt literals)
 176    throws ContradictionException {
 177    assert literals.size() == 0;
 178  0 IVecInt clause = new VecInt(1);
 179  0 clause.push(y);
 180  0 processClause(clause);
 181    }
 182   
 183  0 private void ite(int y, IVecInt literals) throws ContradictionException {
 184    assert literals.size() == 3;
 185  0 IVecInt clause = new VecInt(2);
 186    // y <=> (x1 -> x2) and (not x1 -> x3)
 187    // y -> (x1 -> x2) and (not x1 -> x3)
 188  0 clause.push(-y).push(-literals.get(0)).push(literals.get(1));
 189  0 processClause(clause);
 190  0 clause.clear();
 191  0 clause.push(-y).push(literals.get(0)).push(literals.get(2));
 192  0 processClause(clause);
 193    // y <- (x1 -> x2) and (not x1 -> x3)
 194    // not(x1 -> x2) or not(not x1 -> x3) or y
 195    // x1 and not x2 or not x1 and not x3 or y
 196    // (x1 and not x2) or ((not x1 or y) and (not x3 or y))
 197    // (x1 or not x1 or y) and (not x2 or not x1 or y) and (x1 or not x3 or
 198    // y) and (not x2 or not x3 or y)
 199    // not x1 or not x2 or y and x1 or not x3 or y and not x2 or not x3 or y
 200  0 clause.clear();
 201  0 clause.push(-literals.get(0)).push(-literals.get(1)).push(y);
 202  0 processClause(clause);
 203  0 clause.clear();
 204  0 clause.push(literals.get(0)).push(-literals.get(2)).push(y);
 205  0 processClause(clause);
 206  0 clause.clear();
 207  0 clause.push(-literals.get(1)).push(-literals.get(2)).push(y);
 208  0 processClause(clause);
 209    }
 210   
 211  0 private void and(int y, IVecInt literals) throws ContradictionException {
 212    // y <=> AND x1 ... xn
 213   
 214    // y <= x1 .. xn
 215  0 IVecInt clause = new VecInt(literals.size() + 1);
 216  0 clause.push(y);
 217  0 for (int i = 0; i < literals.size(); i++) {
 218  0 clause.push(-literals.get(i));
 219    }
 220  0 processClause(clause);
 221  0 clause.clear();
 222  0 for (int i = 0; i < literals.size(); i++) {
 223    // y => xi
 224  0 clause.clear();
 225  0 clause.push(-y);
 226  0 clause.push(literals.get(i));
 227  0 processClause(clause);
 228    }
 229    }
 230   
 231  0 private void or(int y, IVecInt literals) throws ContradictionException {
 232    // y <=> OR x1 x2 ...xn
 233    // y => x1 x2 ... xn
 234  0 IVecInt clause = new VecInt(literals.size() + 1);
 235  0 literals.copyTo(clause);
 236  0 clause.push(-y);
 237  0 processClause(clause);
 238  0 clause.clear();
 239  0 for (int i = 0; i < literals.size(); i++) {
 240    // xi => y
 241  0 clause.clear();
 242  0 clause.push(y);
 243  0 clause.push(-literals.get(i));
 244  0 processClause(clause);
 245    }
 246    }
 247   
 248  0 private void processClause(IVecInt clause) throws ContradictionException {
 249  0 solver.addClause(clause);
 250    }
 251   
 252  0 private void not(int y, IVecInt literals) throws ContradictionException {
 253    assert literals.size() == 1;
 254  0 IVecInt clause = new VecInt(2);
 255    // y <=> not x
 256    // y => not x = not y or not x
 257  0 clause.push(-y).push(-literals.get(0));
 258  0 processClause(clause);
 259    // y <= not x = y or x
 260  0 clause.clear();
 261  0 clause.push(y).push(literals.get(0));
 262  0 processClause(clause);
 263    }
 264   
 265  0 void xor(int y, IVecInt literals) throws ContradictionException {
 266  0 literals.push(-y);
 267  0 int[] f = new int[literals.size()];
 268  0 literals.copyTo(f);
 269  0 xor2Clause(f, 0, false);
 270    }
 271   
 272  0 void iff(int y, IVecInt literals) throws ContradictionException {
 273  0 literals.push(y);
 274  0 int[] f = new int[literals.size()];
 275  0 literals.copyTo(f);
 276  0 iff2Clause(f, 0, false);
 277    }
 278   
 279  0 void xor2Clause(int[] f, int prefix, boolean negation)
 280    throws ContradictionException {
 281  0 if (prefix == f.length - 1) {
 282  0 IVecInt clause = new VecInt(f.length);
 283  0 for (int i = 0; i < f.length - 1; ++i) {
 284  0 clause.push(f[i]);
 285    }
 286  0 clause.push(f[f.length - 1] * (negation ? -1 : 1));
 287  0 processClause(clause);
 288  0 return;
 289    }
 290   
 291  0 if (negation) {
 292  0 f[prefix] = -f[prefix];
 293  0 xor2Clause(f, prefix + 1, false);
 294  0 f[prefix] = -f[prefix];
 295   
 296  0 xor2Clause(f, prefix + 1, true);
 297    } else {
 298  0 xor2Clause(f, prefix + 1, false);
 299   
 300  0 f[prefix] = -f[prefix];
 301  0 xor2Clause(f, prefix + 1, true);
 302  0 f[prefix] = -f[prefix];
 303    }
 304    }
 305   
 306  0 void iff2Clause(int[] f, int prefix, boolean negation)
 307    throws ContradictionException {
 308  0 if (prefix == f.length - 1) {
 309  0 IVecInt clause = new VecInt(f.length);
 310  0 for (int i = 0; i < f.length - 1; ++i) {
 311  0 clause.push(f[i]);
 312    }
 313  0 clause.push(f[f.length - 1] * (negation ? -1 : 1));
 314  0 processClause(clause);
 315  0 return;
 316    }
 317   
 318  0 if (!negation) {
 319  0 f[prefix] = -f[prefix];
 320  0 iff2Clause(f, prefix + 1, false);
 321  0 f[prefix] = -f[prefix];
 322  0 iff2Clause(f, prefix + 1, true);
 323    } else {
 324  0 iff2Clause(f, prefix + 1, false);
 325   
 326  0 f[prefix] = -f[prefix];
 327  0 iff2Clause(f, prefix + 1, true);
 328  0 f[prefix] = -f[prefix];
 329    }
 330    }
 331   
 332    }
 
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.