Clover coverage report -
Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 332   Methods: 14
NCLOC: 243   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
ExtendedDimacsReader.java 0% 0% 0% 0%
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  0 public ExtendedDimacsReader(ISolver solver) {
 59  0 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    assert literals.size()==k;
 134  0 switch (gateType) {
 135  0 case FALSE:
 136  0 gateFalse(y, literals);
 137  0 break;
 138  0 case TRUE:
 139  0 gateTrue(y, literals);
 140  0 break;
 141  0 case OR:
 142  0 or(y, literals);
 143  0 break;
 144  0 case NOT:
 145  0 not(y, literals);
 146  0 break;
 147  0 case AND:
 148  0 and(y, literals);
 149  0 break;
 150  0 case XOR:
 151  0 xor(y, literals);
 152  0 break;
 153  0 case IFF:
 154  0 iff(y, literals);
 155  0 break;
 156  0 case IFTHENELSE:
 157  0 ite(y, literals);
 158  0 break;
 159  0 default:
 160  0 throw new UnsupportedOperationException("Gate type "
 161    + gateType + " not handled yet");
 162    }
 163    }
 164  0 literals.clear();
 165  0 return added;
 166    }
 167   
 168  0 private void gateFalse(int y, IVecInt literals)
 169    throws ContradictionException {
 170    assert literals.size() == 0;
 171  0 IVecInt clause = new VecInt(1);
 172  0 clause.push(-y);
 173  0 processClause(clause);
 174    }
 175   
 176  0 private void gateTrue(int y, IVecInt literals)
 177    throws ContradictionException {
 178    assert literals.size() == 0;
 179  0 IVecInt clause = new VecInt(1);
 180  0 clause.push(y);
 181  0 processClause(clause);
 182    }
 183   
 184  0 private void ite(int y, IVecInt literals) throws ContradictionException {
 185    assert literals.size() == 3;
 186  0 IVecInt clause = new VecInt(2);
 187    // y <=> (x1 -> x2) and (not x1 -> x3)
 188    // y -> (x1 -> x2) and (not x1 -> x3)
 189  0 clause.push(-y).push(-literals.get(0)).push(literals.get(1));
 190  0 processClause(clause);
 191  0 clause.clear();
 192  0 clause.push(-y).push(literals.get(0)).push(literals.get(2));
 193  0 processClause(clause);
 194    // y <- (x1 -> x2) and (not x1 -> x3)
 195    // not(x1 -> x2) or not(not x1 -> x3) or y
 196    // x1 and not x2 or not x1 and not x3 or y
 197    // (x1 and not x2) or ((not x1 or y) and (not x3 or y))
 198    // (x1 or not x1 or y) and (not x2 or not x1 or y) and (x1 or not x3 or
 199    // y) and (not x2 or not x3 or y)
 200    // not x1 or not x2 or y and x1 or not x3 or y and not x2 or not x3 or y
 201  0 clause.clear();
 202  0 clause.push(-literals.get(0)).push(-literals.get(1)).push(y);
 203  0 processClause(clause);
 204  0 clause.clear();
 205  0 clause.push(literals.get(0)).push(-literals.get(2)).push(y);
 206  0 processClause(clause);
 207  0 clause.clear();
 208  0 clause.push(-literals.get(1)).push(-literals.get(2)).push(y);
 209  0 processClause(clause);
 210    }
 211   
 212  0 private void and(int y, IVecInt literals) throws ContradictionException {
 213    // y <=> AND x1 ... xn
 214   
 215    // y <= x1 .. xn
 216  0 IVecInt clause = new VecInt(literals.size() + 1);
 217  0 clause.push(y);
 218  0 for (int i = 0; i < literals.size(); i++) {
 219  0 clause.push(-literals.get(i));
 220    }
 221  0 processClause(clause);
 222  0 clause.clear();
 223  0 for (int i = 0; i < literals.size(); i++) {
 224    // y => xi
 225  0 clause.clear();
 226  0 clause.push(-y);
 227  0 clause.push(literals.get(i));
 228  0 processClause(clause);
 229    }
 230    }
 231   
 232  0 private void or(int y, IVecInt literals) throws ContradictionException {
 233    // y <=> OR x1 x2 ...xn
 234    // y => x1 x2 ... xn
 235  0 IVecInt clause = new VecInt(literals.size() + 1);
 236  0 literals.copyTo(clause);
 237  0 clause.push(-y);
 238  0 processClause(clause);
 239  0 clause.clear();
 240  0 for (int i = 0; i < literals.size(); i++) {
 241    // xi => y
 242  0 clause.clear();
 243  0 clause.push(y);
 244  0 clause.push(-literals.get(i));
 245  0 processClause(clause);
 246    }
 247    }
 248   
 249  0 private void processClause(IVecInt clause) throws ContradictionException {
 250  0 solver.addClause(clause);
 251    }
 252   
 253  0 private void not(int y, IVecInt literals) throws ContradictionException {
 254    assert literals.size() == 1;
 255  0 IVecInt clause = new VecInt(2);
 256    // y <=> not x
 257    // y => not x = not y or not x
 258  0 clause.push(-y).push(-literals.get(0));
 259  0 processClause(clause);
 260    // y <= not x = y or x
 261  0 clause.clear();
 262  0 clause.push(y).push(literals.get(0));
 263  0 processClause(clause);
 264    }
 265   
 266  0 void xor(int y, IVecInt literals) throws ContradictionException {
 267  0 literals.push(-y);
 268  0 int[] f = new int[literals.size()];
 269  0 literals.copyTo(f);
 270  0 xor2Clause(f, 0, false);
 271    }
 272   
 273  0 void iff(int y, IVecInt literals) throws ContradictionException {
 274  0 literals.push(y);
 275  0 int[] f = new int[literals.size()];
 276  0 literals.copyTo(f);
 277  0 iff2Clause(f, 0, false);
 278    }
 279   
 280  0 void xor2Clause(int[] f, int prefix, boolean negation)
 281    throws ContradictionException {
 282  0 if (prefix == f.length - 1) {
 283  0 IVecInt clause = new VecInt(f.length);
 284  0 for (int i = 0; i < f.length - 1; ++i) {
 285  0 clause.push(f[i]);
 286    }
 287  0 clause.push(f[f.length - 1] * (negation ? -1 : 1));
 288  0 processClause(clause);
 289  0 return;
 290    }
 291   
 292  0 if (negation) {
 293  0 f[prefix] = -f[prefix];
 294  0 xor2Clause(f, prefix + 1, false);
 295  0 f[prefix] = -f[prefix];
 296   
 297  0 xor2Clause(f, prefix + 1, true);
 298    } else {
 299  0 xor2Clause(f, prefix + 1, false);
 300   
 301  0 f[prefix] = -f[prefix];
 302  0 xor2Clause(f, prefix + 1, true);
 303  0 f[prefix] = -f[prefix];
 304    }
 305    }
 306   
 307  0 void iff2Clause(int[] f, int prefix, boolean negation)
 308    throws ContradictionException {
 309  0 if (prefix == f.length - 1) {
 310  0 IVecInt clause = new VecInt(f.length);
 311  0 for (int i = 0; i < f.length - 1; ++i) {
 312  0 clause.push(f[i]);
 313    }
 314  0 clause.push(f[f.length - 1] * (negation ? -1 : 1));
 315  0 processClause(clause);
 316  0 return;
 317    }
 318   
 319  0 if (negation) {
 320  0 iff2Clause(f, prefix + 1, false);
 321  0 f[prefix] = -f[prefix];
 322  0 iff2Clause(f, prefix + 1, true);
 323  0 f[prefix] = -f[prefix];
 324    } else {
 325  0 f[prefix] = -f[prefix];
 326  0 iff2Clause(f, prefix + 1, false);
 327  0 f[prefix] = -f[prefix];
 328  0 iff2Clause(f, prefix + 1, true);
 329    }
 330    }
 331   
 332    }
 
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.