Clover coverage report -
Coverage timestamp: jeu. sept. 29 2005 23:57:39 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 324   Methods: 24
NCLOC: 240   Classes: 5
 
 Source file Conditionals Statements Methods TOTAL
CSPReader.java 0% 0,9% 4,2% 1,1%
coverage coverage
 1    package org.sat4j.reader;
 2   
 3    import java.io.FileInputStream;
 4    import java.io.FileNotFoundException;
 5    import java.io.FileReader;
 6    import java.io.IOException;
 7    import java.io.InputStreamReader;
 8    import java.io.LineNumberReader;
 9    import java.util.HashMap;
 10    import java.util.Map;
 11    import java.util.Scanner;
 12    import java.util.zip.GZIPInputStream;
 13   
 14    import org.sat4j.core.VecInt;
 15    import org.sat4j.specs.ContradictionException;
 16    import org.sat4j.specs.IProblem;
 17    import org.sat4j.specs.ISolver;
 18    import org.sat4j.specs.IVecInt;
 19   
 20    /**
 21    * This class is a CSP to SAT translator that is able to read
 22    * a CSP problem using the First CSP solver competition input
 23    * format and that translates it into clausal and cardinality
 24    * (equality) constraints.
 25    *
 26    * That code has not been tested very thoroughtly yet and was
 27    * written very quickly to meet the competition deadline :=))
 28    * There is plenty of room for improvement.
 29    *
 30    * @author leberre
 31    *
 32    */
 33    public class CSPReader implements Reader {
 34   
 35    private final ISolver solver;
 36   
 37    private int[][] domains;
 38   
 39    private Var[] vars;
 40   
 41    protected Relation[] relations;
 42   
 43  4052 public CSPReader(ISolver solver) {
 44  4052 this.solver = solver;
 45    }
 46   
 47  0 public IProblem parseInstance(String filename)
 48    throws FileNotFoundException, ParseFormatException, IOException,
 49    ContradictionException {
 50  0 if (filename.endsWith(".gz")) {
 51  0 parseInstance(new LineNumberReader(new InputStreamReader(
 52    new GZIPInputStream(new FileInputStream(filename)))));
 53    } else {
 54  0 parseInstance(new LineNumberReader(new FileReader(filename)));
 55    }
 56  0 return solver;
 57    }
 58   
 59  0 public void parseInstance(LineNumberReader in) throws ParseFormatException,
 60    ContradictionException {
 61  0 solver.reset();
 62  0 try {
 63  0 readProblem(in);
 64    } catch (NumberFormatException e) {
 65  0 throw new ParseFormatException("integer value expected on line "
 66    + in.getLineNumber(), e);
 67    }
 68    }
 69   
 70  0 public String decode(int[] model) {
 71  0 StringBuilder stb = new StringBuilder();
 72  0 for (int i = 0; i < vars.length; i++) {
 73  0 stb.append(vars[i].findValue(model));
 74  0 stb.append(" ");
 75    }
 76  0 return stb.toString();
 77    }
 78   
 79  0 private void readProblem(LineNumberReader in) throws ContradictionException {
 80  0 Scanner input = new Scanner(in);
 81    // discard problem name
 82  0 System.out.println("c reading problem "+input.nextLine());
 83    // read number of domain
 84  0 System.out.println("c reading domains");
 85  0 int nbdomain = input.nextInt();
 86  0 domains = new int[nbdomain][];
 87  0 for (int i = 0; i < nbdomain; i++) {
 88    // read domain number
 89  0 int dnum = input.nextInt();
 90    assert dnum == i;
 91   
 92    // read domain
 93  0 domains[dnum] = readArrayOfInt(input);
 94    }
 95  0 System.out.println("c reading variables");
 96  0 int nbvar = input.nextInt();
 97  0 vars = new Var[nbvar];
 98  0 int nbvarstocreate=0;
 99  0 for (int i = 0; i < nbvar; i++) {
 100    // read var number
 101  0 int varnum = input.nextInt();
 102    assert varnum==i;
 103    // read var domain
 104  0 int vardom = input.nextInt();
 105  0 vars[varnum] = new Var(domains[vardom], nbvarstocreate);
 106  0 nbvarstocreate+=domains[vardom].length;
 107    }
 108  0 solver.newVar(nbvarstocreate);
 109  0 for (int i = 0; i < nbvar; i++) {
 110  0 vars[i].toClause(solver);
 111    }
 112  0 System.out.println("c reading relations");
 113    // relation definition
 114    // read number of relations
 115  0 int nbrel = input.nextInt();
 116  0 relations = new Relation[nbrel];
 117  0 for (int i = 0; i < nbrel; i++) {
 118    // read relation number
 119  0 int relnum = input.nextInt();
 120    assert relnum == i;
 121   
 122  0 boolean forbidden = input.nextInt() == 1 ? false : true;
 123  0 int[] domains = readArrayOfInt(input);
 124   
 125  0 int nbtuples = input.nextInt();
 126  0 if (forbidden) {
 127  0 relations[relnum] = new ForbiddenRelation(domains, nbtuples);
 128    } else {
 129  0 manageAllowedTuples(relnum, domains, nbtuples);
 130    }
 131    // allowed/forbidden tuples
 132  0 for (int j = 0; j < nbtuples; j++) {
 133  0 int[] tuple = readArrayOfInt(input, relations[relnum].arity());
 134    // do something with tuple
 135  0 relations[relnum].addTuple(j, tuple);
 136    }
 137    }
 138  0 System.out.println("c reading constraints");
 139    // constraint definition
 140  0 int nbconstr = input.nextInt();
 141  0 for (int i = 0; i < nbconstr; i++) {
 142  0 int[] variables = readArrayOfInt(input);
 143  0 int relnum = input.nextInt();
 144    // manage constraint
 145  0 relations[relnum].toClause(solver, intToVar(variables));
 146    }
 147    }
 148   
 149  0 protected void manageAllowedTuples(int relnum, int[] domains, int nbtuples) {
 150  0 relations[relnum] = new AllowedRelation(domains, nbtuples);
 151    }
 152   
 153  0 private Var[] intToVar(int[] variables) {
 154  0 Var[] nvars = new Var[variables.length];
 155  0 for (int i = 0; i < variables.length; i++)
 156  0 nvars[i] = vars[variables[i]];
 157  0 return nvars;
 158    }
 159   
 160  0 private int[] readArrayOfInt(Scanner input) {
 161  0 int size = input.nextInt();
 162  0 return readArrayOfInt(input, size);
 163    }
 164   
 165  0 private int[] readArrayOfInt(Scanner input, int size) {
 166  0 int[] tab = new int[size];
 167  0 for (int i = 0; i < size; i++)
 168  0 tab[i] = input.nextInt();
 169  0 return tab;
 170    }
 171    }
 172   
 173   
 174   
 175    class Var {
 176   
 177    Map<Integer, Integer> mapping = new HashMap<Integer, Integer>();
 178   
 179    private final int[] domain;
 180   
 181  0 Var(int[] domain, int startid) {
 182  0 this.domain = domain;
 183  0 for (int i = 0; i < domain.length; i++)
 184  0 mapping.put(domain[i], ++startid);
 185    }
 186   
 187  0 int[] domain() {
 188  0 return domain;
 189    }
 190   
 191  0 int translate(int key) {
 192  0 return mapping.get(key);
 193    }
 194   
 195  0 void toClause(ISolver solver) throws ContradictionException {
 196  0 IVecInt clause = new VecInt();
 197  0 for (int key : mapping.keySet())
 198  0 clause.push(mapping.get(key));
 199    // System.err.println("Adding clause: # " + clause + " = 1 ");
 200  0 solver.addClause(clause);
 201  0 solver.addAtMost(clause, 1);
 202    }
 203   
 204  0 int findValue(int[] model) {
 205  0 for (Map.Entry<Integer, Integer> entry : mapping.entrySet()) {
 206  0 if ( model[entry.getValue()-1]==entry.getValue())
 207  0 return entry.getKey();
 208    }
 209  0 throw new RuntimeException("BIG PROBLEM: no value for a var!");
 210    }
 211    }
 212   
 213    interface Relation {
 214    void addTuple(int index, int[] tuple);
 215   
 216    public void toClause(ISolver solver, Var[] vars)
 217    throws ContradictionException;
 218   
 219    int arity();
 220    }
 221   
 222    class AllowedRelation implements Relation {
 223   
 224    protected final int[] domains;
 225   
 226    protected int[][] tuples;
 227   
 228    private IVecInt clause;
 229   
 230  0 AllowedRelation(int[] domains, int nbtuples) {
 231  0 this.domains = domains;
 232  0 tuples = new int[nbtuples][];
 233    }
 234   
 235  0 public void addTuple(int index, int[] tuple) {
 236  0 tuples[index] = tuple;
 237    }
 238   
 239  0 public void toClause(ISolver solver, Var[] vars)
 240    throws ContradictionException {
 241    // need to find all the tuples that are not expressed here.
 242  0 clause = new VecInt();
 243  0 int[] tuple = new int[vars.length];
 244  0 find(tuple, 0, vars, solver);
 245    }
 246   
 247  0 private void find(int[] tuple, int n, Var[] vars, ISolver solver)
 248    throws ContradictionException {
 249  0 if (n == vars.length) {
 250  0 if (notPresent(tuple)) {
 251  0 clause.clear();
 252  0 for (int j = 0; j < vars.length; j++) {
 253  0 clause.push(-vars[j].translate(tuple[j]));
 254    }
 255    // System.err.println("Adding clause:" + clause);
 256  0 solver.addClause(clause);
 257    }
 258    } else {
 259  0 int[] domain = vars[n].domain();
 260  0 for (int i = 0; i < domain.length; i++) {
 261  0 tuple[n] = domain[i];
 262  0 find(tuple, n + 1, vars, solver);
 263    }
 264   
 265    }
 266   
 267    }
 268   
 269  0 private boolean notPresent(int[] tuple) {
 270    // System.out.println("Checking:" + Arrays.asList(tuple));
 271    // find the first tuple begining with the same
 272    // initial number
 273  0 int i = 0;
 274  0 int j = 0;
 275  0 while (i<tuples.length&&j < tuple.length) {
 276  0 if (tuples[i][j] < tuple[j]) {
 277  0 i++;
 278  0 j = 0;
 279  0 continue;
 280    }
 281  0 if (tuples[i][j] > tuple[j])
 282  0 return true;
 283  0 j++;
 284    }
 285  0 return (j!=tuple.length);
 286    }
 287   
 288  0 public int arity() {
 289  0 return domains.length;
 290    }
 291    }
 292   
 293    class ForbiddenRelation implements Relation {
 294   
 295    private final int[] domains;
 296   
 297    private int[][] tuples;
 298   
 299  0 ForbiddenRelation(int[] domains, int nbtuples) {
 300  0 this.domains = domains;
 301  0 tuples = new int[nbtuples][];
 302    }
 303   
 304  0 public void addTuple(int index, int[] tuple) {
 305  0 tuples[index] = tuple;
 306    }
 307   
 308  0 public void toClause(ISolver solver, Var[] vars)
 309    throws ContradictionException {
 310  0 IVecInt clause = new VecInt();
 311  0 for (int i = 0; i < tuples.length; i++) {
 312  0 clause.clear();
 313  0 for (int j = 0; j < domains.length; j++) {
 314  0 clause.push(-vars[j].translate(tuples[i][j]));
 315    }
 316    // System.err.println("Adding clause (EZ) :" + clause);
 317  0 solver.addClause(clause);
 318    }
 319    }
 320   
 321  0 public int arity() {
 322  0 return domains.length;
 323    }
 324    }
 
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.