Clover coverage report -

Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST

FRAMES NO FRAMES

file stats:	LOC:	168		Methods:	9
	NCLOC:	123		Classes:	1

Source file

Conditionals

Statements

Methods

TOTAL

CSPReader.java

1		package org.sat4j.reader;
2
3		import java.io.IOException;
4		import java.io.LineNumberReader;
5		import java.util.Scanner;
6
7		import org.sat4j.reader.csp.Nogoods;
8		import org.sat4j.reader.csp.Relation;
9		import org.sat4j.reader.csp.SupportsDirectEncoding;
10		import org.sat4j.reader.csp.Var;
11		import org.sat4j.specs.ContradictionException;
12		import org.sat4j.specs.IProblem;
13		import org.sat4j.specs.ISolver;
14
15		/**
16		* This class is a CSP to SAT translator that is able to read
17		* a CSP problem using the First CSP solver competition input
18		* format and that translates it into clausal and cardinality
19		* (equality) constraints.
20		*
21		* That code has not been tested very thoroughtly yet and was
22		* written very quickly to meet the competition deadline :=))
23		* There is plenty of room for improvement.
24		*
25		* @author leberre
26		*
27		*/
28		public class CSPReader extends Reader {
29
30		private final ISolver solver;
31
32		private Var[] vars;
33
34		protected Relation[] relations;
35
36	0	public CSPReader(ISolver solver) {
37	0	this.solver = solver;
38		}
39
40	0	@Override
41		public final IProblem parseInstance(final java.io.Reader in)
42		throws ParseFormatException, ContradictionException, IOException {
43	0	return parseInstance(new LineNumberReader(in));
44
45		}
46
47	0	private IProblem parseInstance(LineNumberReader in) throws ParseFormatException,
48		ContradictionException {
49	0	solver.reset();
50	0	try {
51	0	readProblem(in);
52	0	return solver;
53		} catch (NumberFormatException e) {
54	0	throw new ParseFormatException("integer value expected on line "
55		+ in.getLineNumber(), e);
56		}
57		}
58
59	0	@Override
60		public String decode(int[] model) {
61	0	StringBuilder stb = new StringBuilder();
62	0	for (int i = 0; i < vars.length; i++) {
63	0	stb.append(vars[i].findValue(model));
64	0	stb.append(" ");
65		}
66	0	return stb.toString();
67		}
68
69	0	private void readProblem(LineNumberReader in) throws ContradictionException {
70	0	Scanner input = new Scanner(in);
71		// discard problem name
72	0	System.out.println("c reading problem named "+input.nextLine());
73		// read number of domain
74	0	System.out.print("c reading domains");
75	0	int nbdomain = input.nextInt();
76	0	int [] [] domains = new int[nbdomain][];
77	0	for (int i = 0; i < nbdomain; i++) {
78		// read domain number
79	0	int dnum = input.nextInt();
80		assert dnum == i;
81
82		// read domain
83	0	domains[dnum] = readArrayOfInt(input);
84		}
85	0	System.out.println(" done.");
86	0	System.out.print("c reading variables");
87	0	int nbvar = input.nextInt();
88	0	vars = new Var[nbvar];
89	0	int nbvarstocreate=0;
90	0	for (int i = 0; i < nbvar; i++) {
91		// read var number
92	0	System.out.print("\rc reading variables "+i+"/"+nbvar);
93	0	int varnum = input.nextInt();
94		assert varnum==i;
95		// read var domain
96	0	int vardom = input.nextInt();
97	0	vars[varnum] = new Var(domains[vardom], nbvarstocreate);
98	0	nbvarstocreate+=domains[vardom].length;
99		}
100	0	System.out.println("\rc reading variables ("+nbvar+") done.");
101	0	solver.newVar(nbvarstocreate);
102	0	for (int i = 0; i < nbvar; i++) {
103	0	vars[i].toClause(solver);
104		}
105	0	System.out.print("c reading relations");
106		// relation definition
107		// read number of relations
108	0	int nbrel = input.nextInt();
109	0	relations = new Relation[nbrel];
110	0	for (int i = 0; i < nbrel; i++) {
111	0	System.out.print("\rc reading relations "+i+"/"+nbrel);
112		// read relation number
113	0	int relnum = input.nextInt();
114		assert relnum == i;
115
116	0	boolean forbidden = input.nextInt() == 1 ? false : true;
117	0	int[] rdomains = readArrayOfInt(input);
118
119	0	int nbtuples = input.nextInt();
120	0	if (forbidden) {
121	0	relations[relnum] = new Nogoods(rdomains, nbtuples);
122		} else {
123	0	manageAllowedTuples(relnum, rdomains, nbtuples);
124		}
125		// allowed/forbidden tuples
126	0	for (int j = 0; j < nbtuples; j++) {
127	0	int[] tuple = readArrayOfInt(input, relations[relnum].arity());
128		// do something with tuple
129	0	relations[relnum].addTuple(j, tuple);
130		}
131		}
132	0	System.out.println("\rc reading relations ("+nbrel+") done.");
133	0	System.out.print("c reading constraints");
134		// constraint definition
135	0	int nbconstr = input.nextInt();
136	0	for (int i = 0; i < nbconstr; i++) {
137	0	System.out.print("\rc reading constraints "+i+"/"+nbconstr);
138	0	int[] variables = readArrayOfInt(input);
139	0	int relnum = input.nextInt();
140		// manage constraint
141	0	relations[relnum].toClause(solver, intToVar(variables));
142		}
143	0	System.out.println("\rc reading constraints ("+nbconstr+") done.");
144		}
145
146	0	protected void manageAllowedTuples(int relnum, int[] domains, int nbtuples) {
147	0	relations[relnum] = new SupportsDirectEncoding(domains, nbtuples);
148		}
149
150	0	private Var[] intToVar(int[] variables) {
151	0	Var[] nvars = new Var[variables.length];
152	0	for (int i = 0; i < variables.length; i++)
153	0	nvars[i] = vars[variables[i]];
154	0	return nvars;
155		}
156
157	0	private int[] readArrayOfInt(Scanner input) {
158	0	int size = input.nextInt();
159	0	return readArrayOfInt(input, size);
160		}
161
162	0	private int[] readArrayOfInt(Scanner input, int size) {
163	0	int[] tab = new int[size];
164	0	for (int i = 0; i < size; i++)
165	0	tab[i] = input.nextInt();
166	0	return tab;
167		}
168		}