Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
106   289   10   8,15
22   155   0,21   13
13     1,69  
1    
 
  GateTranslator       Line # 38 106 10 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    * Utility class to easily feed a SAT solver using logical gates.
34    *
35    * @author leberre
36    *
37    */
 
38    public class GateTranslator extends SolverDecorator {
39   
40    /**
41    *
42    */
43    private static final long serialVersionUID = 1L;
44   
 
45  0 toggle public GateTranslator(ISolver solver) {
46  0 super(solver);
47    }
48   
49    /**
50    * translate y <=> FALSE into a clause.
51    * @param y a variable to falsify
52    * @throws ContradictionException iff a trivial inconsistency is found.
53    */
 
54  0 toggle public void gateFalse(int y)
55    throws ContradictionException {
56  0 IVecInt clause = new VecInt(1);
57  0 clause.push(-y);
58  0 processClause(clause);
59    }
60   
61    /**
62    * translate y <=> TRUE into a clause.
63    * @param y a variable to falsify
64    * @throws ContradictionException
65    */
 
66  0 toggle public void gateTrue(int y)
67    throws ContradictionException {
68  0 IVecInt clause = new VecInt(1);
69  0 clause.push(y);
70  0 processClause(clause);
71    }
72   
73    /**
74    * translate y <=> if x1 then x2 else x3 into clauses.
75    * @param y
76    * @param x1 the selector variable
77    * @param x2
78    * @param x3
79    * @throws ContradictionException
80    */
 
81  0 toggle public void ite(int y, int x1, int x2, int x3) throws ContradictionException {
82  0 IVecInt clause = new VecInt(2);
83    // y <=> (x1 -> x2) and (not x1 -> x3)
84    // y -> (x1 -> x2) and (not x1 -> x3)
85  0 clause.push(-y).push(-x1).push(x2);
86  0 processClause(clause);
87  0 clause.clear();
88  0 clause.push(-y).push(x1).push(x3);
89  0 processClause(clause);
90    // y <- (x1 -> x2) and (not x1 -> x3)
91    // not(x1 -> x2) or not(not x1 -> x3) or y
92    // x1 and not x2 or not x1 and not x3 or y
93    // (x1 and not x2) or ((not x1 or y) and (not x3 or y))
94    // (x1 or not x1 or y) and (not x2 or not x1 or y) and (x1 or not x3 or
95    // y) and (not x2 or not x3 or y)
96    // not x1 or not x2 or y and x1 or not x3 or y and not x2 or not x3 or y
97  0 clause.clear();
98  0 clause.push(-x1).push(-x2).push(y);
99  0 processClause(clause);
100  0 clause.clear();
101  0 clause.push(x1).push(-x3).push(y);
102  0 processClause(clause);
103  0 clause.clear();
104  0 clause.push(-x2).push(-x3).push(y);
105  0 processClause(clause);
106    // taken from Niklas Een et al SAT 2007 paper
107    // Adding the following redundant clause will improve unit propagation
108    // y -> x2 or x3
109  0 clause.clear();
110  0 clause.push(y).push(x2).push(x3);
111  0 processClause(clause);
112    }
113   
114    /**
115    * Translate y <=> x1 /\ x2 /\ ... /\ xn into clauses.
116    *
117    * @param y
118    * @param literals the x1 ... xn literals.
119    * @throws ContradictionException
120    */
 
121  0 toggle public void and(int y, IVecInt literals) throws ContradictionException {
122    // y <=> AND x1 ... xn
123   
124    // y <= x1 .. xn
125  0 IVecInt clause = new VecInt(literals.size() + 1);
126  0 clause.push(y);
127  0 for (int i = 0; i < literals.size(); i++) {
128  0 clause.push(-literals.get(i));
129    }
130  0 processClause(clause);
131  0 clause.clear();
132  0 for (int i = 0; i < literals.size(); i++) {
133    // y => xi
134  0 clause.clear();
135  0 clause.push(-y);
136  0 clause.push(literals.get(i));
137  0 processClause(clause);
138    }
139    }
140   
141    /**
142    * Translate y <=> x1 /\ x2
143    * @param y
144    * @param x1
145    * @param x2
146    * @throws ContradictionException
147    */
 
148  0 toggle public void and(int y, int x1, int x2) throws ContradictionException {
149  0 IVecInt clause = new VecInt();
150  0 clause.push(-y);
151  0 clause.push(x1);
152  0 addClause(clause);
153  0 clause.clear();
154  0 clause.push(-y);
155  0 clause.push(x2);
156  0 addClause(clause);
157  0 clause.clear();
158  0 clause.push(y);
159  0 clause.push(-x1);
160  0 clause.push(-x2);
161  0 addClause(clause);
162    }
163   
164    /**
165    * translate y <=> x1 \/ x2 \/ ... \/ xn into clauses.
166    *
167    * @param y
168    * @param literals
169    * @throws ContradictionException
170    */
 
171  0 toggle public void or(int y, IVecInt literals) throws ContradictionException {
172    // y <=> OR x1 x2 ...xn
173    // y => x1 x2 ... xn
174  0 IVecInt clause = new VecInt(literals.size() + 1);
175  0 literals.copyTo(clause);
176  0 clause.push(-y);
177  0 processClause(clause);
178  0 clause.clear();
179  0 for (int i = 0; i < literals.size(); i++) {
180    // xi => y
181  0 clause.clear();
182  0 clause.push(y);
183  0 clause.push(-literals.get(i));
184  0 processClause(clause);
185    }
186    }
187   
 
188  0 toggle private void processClause(IVecInt clause) throws ContradictionException {
189  0 addClause(clause);
190    }
191   
192    /**
193    * Translate y <=> not x into clauses.
194    *
195    * @param y
196    * @param x
197    * @throws ContradictionException
198    */
 
199  0 toggle public void not(int y, int x) throws ContradictionException {
200  0 IVecInt clause = new VecInt(2);
201    // y <=> not x
202    // y => not x = not y or not x
203  0 clause.push(-y).push(-x);
204  0 processClause(clause);
205    // y <= not x = y or x
206  0 clause.clear();
207  0 clause.push(y).push(x);
208  0 processClause(clause);
209    }
210   
211    /**
212    * translate y <=> x1 xor x2 xor ... xor xn into clauses.
213    * @param y
214    * @param literals
215    * @throws ContradictionException
216    */
 
217  0 toggle public void xor(int y, IVecInt literals) throws ContradictionException {
218  0 literals.push(-y);
219  0 int[] f = new int[literals.size()];
220  0 literals.copyTo(f);
221  0 xor2Clause(f, 0, false);
222    }
223   
224    /**
225    * translate y <=> (x1 <=> x2 <=> ... <=> xn) into clauses.
226    * @param y
227    * @param literals
228    * @throws ContradictionException
229    */
 
230  0 toggle public void iff(int y, IVecInt literals) throws ContradictionException {
231  0 literals.push(y);
232  0 int[] f = new int[literals.size()];
233  0 literals.copyTo(f);
234  0 iff2Clause(f, 0, false);
235    }
236   
 
237  0 toggle private void xor2Clause(int[] f, int prefix, boolean negation)
238    throws ContradictionException {
239  0 if (prefix == f.length - 1) {
240  0 IVecInt clause = new VecInt(f.length);
241  0 for (int i = 0; i < f.length - 1; ++i) {
242  0 clause.push(f[i]);
243    }
244  0 clause.push(f[f.length - 1] * (negation ? -1 : 1));
245  0 processClause(clause);
246  0 return;
247    }
248   
249  0 if (negation) {
250  0 f[prefix] = -f[prefix];
251  0 xor2Clause(f, prefix + 1, false);
252  0 f[prefix] = -f[prefix];
253   
254  0 xor2Clause(f, prefix + 1, true);
255    } else {
256  0 xor2Clause(f, prefix + 1, false);
257   
258  0 f[prefix] = -f[prefix];
259  0 xor2Clause(f, prefix + 1, true);
260  0 f[prefix] = -f[prefix];
261    }
262    }
263   
 
264  0 toggle private void iff2Clause(int[] f, int prefix, boolean negation)
265    throws ContradictionException {
266  0 if (prefix == f.length - 1) {
267  0 IVecInt clause = new VecInt(f.length);
268  0 for (int i = 0; i < f.length - 1; ++i) {
269  0 clause.push(f[i]);
270    }
271  0 clause.push(f[f.length - 1] * (negation ? -1 : 1));
272  0 processClause(clause);
273  0 return;
274    }
275   
276  0 if (negation) {
277  0 iff2Clause(f, prefix + 1, false);
278  0 f[prefix] = -f[prefix];
279  0 iff2Clause(f, prefix + 1, true);
280  0 f[prefix] = -f[prefix];
281    } else {
282  0 f[prefix] = -f[prefix];
283  0 iff2Clause(f, prefix + 1, false);
284  0 f[prefix] = -f[prefix];
285  0 iff2Clause(f, prefix + 1, true);
286    }
287    }
288   
289    }
 
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.