Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
124   297   19   9,54
32   197   0,25   13
13     2,38  
1    
 
  ExtendedDimacsArrayToDimacsConverter       Line # 41 124 19 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.IVecInt;
30   
31    /**
32    * Converter from the Extended Dimacs format proposed by Fahiem Bacchus and Toby
33    * Walsh in array representation (without the terminating 0) to the Dimacs
34    * format.
35    *
36    * Adaptation of org.sat4j.reader.ExtendedDimacsReader.
37    *
38    * @author leberre
39    * @author fuhs
40    */
 
41    public class ExtendedDimacsArrayToDimacsConverter extends
42    DimacsArrayToDimacsConverter {
43   
44    public static final int FALSE = 1;
45   
46    public static final int TRUE = 2;
47   
48    public static final int NOT = 3;
49   
50    public static final int AND = 4;
51   
52    public static final int NAND = 5;
53   
54    public static final int OR = 6;
55   
56    public static final int NOR = 7;
57   
58    public static final int XOR = 8;
59   
60    public static final int XNOR = 9;
61   
62    public static final int IMPLIES = 10;
63   
64    public static final int IFF = 11;
65   
66    public static final int IFTHENELSE = 12;
67   
68    public static final int ATLEAST = 13;
69   
70    public static final int ATMOST = 14;
71   
72    public static final int COUNT = 15;
73   
74    private static final long serialVersionUID = 1L;
75   
 
76  0 toggle public ExtendedDimacsArrayToDimacsConverter(int bufSize) {
77  0 super(bufSize);
78    }
79   
80    /**
81    * Handles a single constraint (constraint == Extended Dimacs circuit gate).
82    *
83    * @param gateType
84    * the type of the gate in question
85    * @param output
86    * the number of the output of the gate in question
87    * @param inputs
88    * the numbers of the inputs of the gates in question
89    * @return true
90    */
 
91  0 toggle @Override
92    protected boolean handleConstr(int gateType, int output, int[] inputs)
93    throws ContradictionException {
94  0 IVecInt literals = new VecInt(inputs);
95  0 switch (gateType) {
96  0 case FALSE:
97  0 gateFalse(output, literals);
98  0 break;
99  0 case TRUE:
100  0 gateTrue(output, literals);
101  0 break;
102  0 case OR:
103  0 or(output, literals);
104  0 break;
105  0 case NOT:
106  0 not(output, literals);
107  0 break;
108  0 case AND:
109  0 and(output, literals);
110  0 break;
111  0 case XOR:
112  0 xor(output, literals);
113  0 break;
114  0 case IFF:
115  0 iff(output, literals);
116  0 break;
117  0 case IFTHENELSE:
118  0 ite(output, literals);
119  0 break;
120  0 default:
121  0 throw new UnsupportedOperationException("Gate type " + gateType
122    + " not handled yet");
123    }
124  0 return true;
125    }
126   
 
127  0 toggle private void gateFalse(int y, IVecInt literals)
128    throws ContradictionException {
129  0 assert literals.size() == 0;
130  0 IVecInt clause = new VecInt(1);
131  0 clause.push(-y);
132  0 processClause(clause);
133    }
134   
 
135  0 toggle private void gateTrue(int y, IVecInt literals)
136    throws ContradictionException {
137  0 assert literals.size() == 0;
138  0 IVecInt clause = new VecInt(1);
139  0 clause.push(y);
140  0 processClause(clause);
141    }
142   
 
143  0 toggle private void ite(int y, IVecInt literals) throws ContradictionException {
144  0 assert literals.size() == 3;
145  0 IVecInt clause = new VecInt(2);
146    // y <=> (x1 -> x2) and (not x1 -> x3)
147    // y -> (x1 -> x2) and (not x1 -> x3)
148  0 clause.push(-y).push(-literals.get(0)).push(literals.get(1));
149  0 processClause(clause);
150  0 clause.clear();
151  0 clause.push(-y).push(literals.get(0)).push(literals.get(2));
152  0 processClause(clause);
153    // y <- (x1 -> x2) and (not x1 -> x3)
154    // not(x1 -> x2) or not(not x1 -> x3) or y
155    // x1 and not x2 or not x1 and not x3 or y
156    // (x1 and not x2) or ((not x1 or y) and (not x3 or y))
157    // (x1 or not x1 or y) and (not x2 or not x1 or y) and (x1 or not x3 or
158    // y) and (not x2 or not x3 or y)
159    // not x1 or not x2 or y and x1 or not x3 or y and not x2 or not x3 or y
160  0 clause.clear();
161  0 clause.push(-literals.get(0)).push(-literals.get(1)).push(y);
162  0 processClause(clause);
163  0 clause.clear();
164  0 clause.push(literals.get(0)).push(-literals.get(2)).push(y);
165  0 processClause(clause);
166  0 clause.clear();
167  0 clause.push(-literals.get(1)).push(-literals.get(2)).push(y);
168  0 processClause(clause);
169    }
170   
 
171  0 toggle private void and(int y, IVecInt literals) throws ContradictionException {
172    // y <=> AND x1 ... xn
173   
174    // y <= x1 .. xn
175  0 IVecInt clause = new VecInt(literals.size() + 1);
176  0 clause.push(y);
177  0 for (int i = 0; i < literals.size(); i++) {
178  0 clause.push(-literals.get(i));
179    }
180  0 processClause(clause);
181  0 clause.clear();
182  0 for (int i = 0; i < literals.size(); i++) {
183    // y => xi
184  0 clause.clear();
185  0 clause.push(-y);
186  0 clause.push(literals.get(i));
187  0 processClause(clause);
188    }
189    }
190   
 
191  0 toggle private void or(int y, IVecInt literals) throws ContradictionException {
192    // y <=> OR x1 x2 ...xn
193    // y => x1 x2 ... xn
194  0 IVecInt clause = new VecInt(literals.size() + 1);
195  0 literals.copyTo(clause);
196  0 clause.push(-y);
197  0 processClause(clause);
198  0 clause.clear();
199  0 for (int i = 0; i < literals.size(); i++) {
200    // xi => y
201  0 clause.clear();
202  0 clause.push(y);
203  0 clause.push(-literals.get(i));
204  0 processClause(clause);
205    }
206    }
207   
 
208  0 toggle private void processClause(IVecInt clause) throws ContradictionException {
209  0 final int length = clause.size();
210  0 for (int i = 0; i < length; ++i) {
211  0 this.dimacs.append(clause.get(i));
212  0 this.dimacs.append(" ");
213    }
214  0 this.dimacs.append("0\n");
215  0 ++this.clauses;
216    }
217   
 
218  0 toggle private void not(int y, IVecInt literals) throws ContradictionException {
219  0 assert literals.size() == 1;
220  0 IVecInt clause = new VecInt(2);
221    // y <=> not x
222    // y => not x = not y or not x
223  0 clause.push(-y).push(-literals.get(0));
224  0 processClause(clause);
225    // y <= not x = y or x
226  0 clause.clear();
227  0 clause.push(y).push(literals.get(0));
228  0 processClause(clause);
229    }
230   
 
231  0 toggle void xor(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 xor2Clause(f, 0, false);
236    }
237   
 
238  0 toggle void iff(int y, IVecInt literals) throws ContradictionException {
239  0 literals.push(y);
240  0 int[] f = new int[literals.size()];
241  0 literals.copyTo(f);
242  0 iff2Clause(f, 0, false);
243    }
244   
 
245  0 toggle void xor2Clause(int[] f, int prefix, boolean negation)
246    throws ContradictionException {
247  0 if (prefix == f.length - 1) {
248  0 IVecInt clause = new VecInt(f.length);
249  0 for (int i = 0; i < f.length - 1; ++i) {
250  0 clause.push(f[i]);
251    }
252  0 clause.push(f[f.length - 1] * (negation ? -1 : 1));
253  0 processClause(clause);
254  0 return;
255    }
256   
257  0 if (negation) {
258  0 f[prefix] = -f[prefix];
259  0 xor2Clause(f, prefix + 1, false);
260  0 f[prefix] = -f[prefix];
261   
262  0 xor2Clause(f, prefix + 1, true);
263    } else {
264  0 xor2Clause(f, prefix + 1, false);
265   
266  0 f[prefix] = -f[prefix];
267  0 xor2Clause(f, prefix + 1, true);
268  0 f[prefix] = -f[prefix];
269    }
270    }
271   
 
272  0 toggle void iff2Clause(int[] f, int prefix, boolean negation)
273    throws ContradictionException {
274  0 if (prefix == f.length - 1) {
275  0 IVecInt clause = new VecInt(f.length);
276  0 for (int i = 0; i < f.length - 1; ++i) {
277  0 clause.push(f[i]);
278    }
279  0 clause.push(f[f.length - 1] * (negation ? -1 : 1));
280  0 processClause(clause);
281  0 return;
282    }
283   
284  0 if (negation) {
285  0 iff2Clause(f, prefix + 1, false);
286  0 f[prefix] = -f[prefix];
287  0 iff2Clause(f, prefix + 1, true);
288  0 f[prefix] = -f[prefix];
289    } else {
290  0 f[prefix] = -f[prefix];
291  0 iff2Clause(f, prefix + 1, false);
292  0 f[prefix] = -f[prefix];
293  0 iff2Clause(f, prefix + 1, true);
294    }
295    }
296   
297    }
 
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.