Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
119   290   18   9,15
30   191   0,25   13
13     2,31  
1    
 
  ExtendedDimacsArrayReader       Line # 41 119 18 0% 0.0
 
No Tests
 
1    /*
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le Berre
3    *
4    * Based on the original minisat specification from:
5    *
6    * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
7    * Sixth International Conference on Theory and Applications of Satisfiability
8    * Testing, LNCS 2919, pp 502-518, 2003.
9    *
10    * This library is free software; you can redistribute it and/or modify it under
11    * the terms of the GNU Lesser General Public License as published by the Free
12    * Software Foundation; either version 2.1 of the License, or (at your option)
13    * any later version.
14    *
15    * This library is distributed in the hope that it will be useful, but WITHOUT
16    * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
17    * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
18    * details.
19    *
20    * You should have received a copy of the GNU Lesser General Public License
21    * along with this library; if not, write to the Free Software Foundation, Inc.,
22    * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
23    *
24    */
25    package org.sat4j.tools;
26   
27    import org.sat4j.core.VecInt;
28    import org.sat4j.specs.ContradictionException;
29    import org.sat4j.specs.ISolver;
30    import org.sat4j.specs.IVecInt;
31   
32    /**
33    * Reader for the Extended Dimacs format proposed by Fahiem Bacchus and Toby
34    * Walsh in array representation (without the terminating 0).
35    *
36    * Adaptation of org.sat4j.reader.ExtendedDimacsReader.
37    *
38    * @author leberre
39    * @author fuhs
40    */
 
41    public class ExtendedDimacsArrayReader extends DimacsArrayReader {
42   
43    public static final int FALSE = 1;
44   
45    public static final int TRUE = 2;
46   
47    public static final int NOT = 3;
48   
49    public static final int AND = 4;
50   
51    public static final int NAND = 5;
52   
53    public static final int OR = 6;
54   
55    public static final int NOR = 7;
56   
57    public static final int XOR = 8;
58   
59    public static final int XNOR = 9;
60   
61    public static final int IMPLIES = 10;
62   
63    public static final int IFF = 11;
64   
65    public static final int IFTHENELSE = 12;
66   
67    public static final int ATLEAST = 13;
68   
69    public static final int ATMOST = 14;
70   
71    public static final int COUNT = 15;
72   
73    private static final long serialVersionUID = 1L;
74   
 
75  0 toggle public ExtendedDimacsArrayReader(ISolver solver) {
76  0 super(solver);
77    }
78   
79    /**
80    * Handles a single constraint (constraint == Extended Dimacs circuit gate).
81    *
82    * @param gateType
83    * the type of the gate in question
84    * @param output
85    * the number of the output of the gate in question
86    * @param inputs
87    * the numbers of the inputs of the gates in question
88    * @return true
89    */
 
90  0 toggle @Override
91    protected boolean handleConstr(int gateType, int output, int[] inputs)
92    throws ContradictionException {
93  0 IVecInt literals = new VecInt(inputs);
94  0 switch (gateType) {
95  0 case FALSE:
96  0 gateFalse(output, literals);
97  0 break;
98  0 case TRUE:
99  0 gateTrue(output, literals);
100  0 break;
101  0 case OR:
102  0 or(output, literals);
103  0 break;
104  0 case NOT:
105  0 not(output, literals);
106  0 break;
107  0 case AND:
108  0 and(output, literals);
109  0 break;
110  0 case XOR:
111  0 xor(output, literals);
112  0 break;
113  0 case IFF:
114  0 iff(output, literals);
115  0 break;
116  0 case IFTHENELSE:
117  0 ite(output, literals);
118  0 break;
119  0 default:
120  0 throw new UnsupportedOperationException("Gate type " + gateType
121    + " not handled yet");
122    }
123  0 return true;
124    }
125   
 
126  0 toggle private void gateFalse(int y, IVecInt literals)
127    throws ContradictionException {
128  0 assert literals.size() == 0;
129  0 IVecInt clause = new VecInt(1);
130  0 clause.push(-y);
131  0 processClause(clause);
132    }
133   
 
134  0 toggle private void gateTrue(int y, IVecInt literals)
135    throws ContradictionException {
136  0 assert literals.size() == 0;
137  0 IVecInt clause = new VecInt(1);
138  0 clause.push(y);
139  0 processClause(clause);
140    }
141   
 
142  0 toggle private void ite(int y, IVecInt literals) throws ContradictionException {
143  0 assert literals.size() == 3;
144  0 IVecInt clause = new VecInt(2);
145    // y <=> (x1 -> x2) and (not x1 -> x3)
146    // y -> (x1 -> x2) and (not x1 -> x3)
147  0 clause.push(-y).push(-literals.get(0)).push(literals.get(1));
148  0 processClause(clause);
149  0 clause.clear();
150  0 clause.push(-y).push(literals.get(0)).push(literals.get(2));
151  0 processClause(clause);
152    // y <- (x1 -> x2) and (not x1 -> x3)
153    // not(x1 -> x2) or not(not x1 -> x3) or y
154    // x1 and not x2 or not x1 and not x3 or y
155    // (x1 and not x2) or ((not x1 or y) and (not x3 or y))
156    // (x1 or not x1 or y) and (not x2 or not x1 or y) and (x1 or not x3 or
157    // y) and (not x2 or not x3 or y)
158    // not x1 or not x2 or y and x1 or not x3 or y and not x2 or not x3 or y
159  0 clause.clear();
160  0 clause.push(-literals.get(0)).push(-literals.get(1)).push(y);
161  0 processClause(clause);
162  0 clause.clear();
163  0 clause.push(literals.get(0)).push(-literals.get(2)).push(y);
164  0 processClause(clause);
165  0 clause.clear();
166  0 clause.push(-literals.get(1)).push(-literals.get(2)).push(y);
167  0 processClause(clause);
168    }
169   
 
170  0 toggle private void and(int y, IVecInt literals) throws ContradictionException {
171    // y <=> AND x1 ... xn
172   
173    // y <= x1 .. xn
174  0 IVecInt clause = new VecInt(literals.size() + 1);
175  0 clause.push(y);
176  0 for (int i = 0; i < literals.size(); i++) {
177  0 clause.push(-literals.get(i));
178    }
179  0 processClause(clause);
180  0 clause.clear();
181  0 for (int i = 0; i < literals.size(); i++) {
182    // y => xi
183  0 clause.clear();
184  0 clause.push(-y);
185  0 clause.push(literals.get(i));
186  0 processClause(clause);
187    }
188    }
189   
 
190  0 toggle private void or(int y, IVecInt literals) throws ContradictionException {
191    // y <=> OR x1 x2 ...xn
192    // y => x1 x2 ... xn
193  0 IVecInt clause = new VecInt(literals.size() + 1);
194  0 literals.copyTo(clause);
195  0 clause.push(-y);
196  0 processClause(clause);
197  0 clause.clear();
198  0 for (int i = 0; i < literals.size(); i++) {
199    // xi => y
200  0 clause.clear();
201  0 clause.push(y);
202  0 clause.push(-literals.get(i));
203  0 processClause(clause);
204    }
205    }
206   
 
207  0 toggle private void processClause(IVecInt clause) throws ContradictionException {
208  0 solver.addClause(clause);
209    }
210   
 
211  0 toggle private void not(int y, IVecInt literals) throws ContradictionException {
212  0 assert literals.size() == 1;
213  0 IVecInt clause = new VecInt(2);
214    // y <=> not x
215    // y => not x = not y or not x
216  0 clause.push(-y).push(-literals.get(0));
217  0 processClause(clause);
218    // y <= not x = y or x
219  0 clause.clear();
220  0 clause.push(y).push(literals.get(0));
221  0 processClause(clause);
222    }
223   
 
224  0 toggle void xor(int y, IVecInt literals) throws ContradictionException {
225  0 literals.push(-y);
226  0 int[] f = new int[literals.size()];
227  0 literals.copyTo(f);
228  0 xor2Clause(f, 0, false);
229    }
230   
 
231  0 toggle void iff(int y, IVecInt literals) throws ContradictionException {
232  0 literals.push(y);
233  0 int[] f = new int[literals.size()];
234  0 literals.copyTo(f);
235  0 iff2Clause(f, 0, false);
236    }
237   
 
238  0 toggle void xor2Clause(int[] f, int prefix, boolean negation)
239    throws ContradictionException {
240  0 if (prefix == f.length - 1) {
241  0 IVecInt clause = new VecInt(f.length);
242  0 for (int i = 0; i < f.length - 1; ++i) {
243  0 clause.push(f[i]);
244    }
245  0 clause.push(f[f.length - 1] * (negation ? -1 : 1));
246  0 processClause(clause);
247  0 return;
248    }
249   
250  0 if (negation) {
251  0 f[prefix] = -f[prefix];
252  0 xor2Clause(f, prefix + 1, false);
253  0 f[prefix] = -f[prefix];
254   
255  0 xor2Clause(f, prefix + 1, true);
256    } else {
257  0 xor2Clause(f, prefix + 1, false);
258   
259  0 f[prefix] = -f[prefix];
260  0 xor2Clause(f, prefix + 1, true);
261  0 f[prefix] = -f[prefix];
262    }
263    }
264   
 
265  0 toggle void iff2Clause(int[] f, int prefix, boolean negation)
266    throws ContradictionException {
267  0 if (prefix == f.length - 1) {
268  0 IVecInt clause = new VecInt(f.length);
269  0 for (int i = 0; i < f.length - 1; ++i) {
270  0 clause.push(f[i]);
271    }
272  0 clause.push(f[f.length - 1] * (negation ? -1 : 1));
273  0 processClause(clause);
274  0 return;
275    }
276   
277  0 if (negation) {
278  0 iff2Clause(f, prefix + 1, false);
279  0 f[prefix] = -f[prefix];
280  0 iff2Clause(f, prefix + 1, true);
281  0 f[prefix] = -f[prefix];
282    } else {
283  0 f[prefix] = -f[prefix];
284  0 iff2Clause(f, prefix + 1, false);
285  0 f[prefix] = -f[prefix];
286  0 iff2Clause(f, prefix + 1, true);
287    }
288    }
289   
290    }
 
CloverReport generated by Clover Code Coverage v2.0a5
mer. juin 27 2007 07:27:33 CEST.		   Beta Testers License registered to clover-support@cenqua.com. This license of Clover2 is provided for beta testing only. You have 5 day(s) before your Beta Tester License expires.