Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
67   324   19   3,72
46   141   0,54   18
18     2  
1    
 
  WLClause       Line # 46 67 19 66,4% 0.66412216
 
  (163)
 
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   
26    package org.sat4j.minisat.constraints.cnf;
27   
28    import java.io.Serializable;
29   
30    import org.sat4j.minisat.core.Constr;
31    import org.sat4j.minisat.core.ILits;
32    import org.sat4j.minisat.core.UnitPropagationListener;
33    import org.sat4j.specs.ContradictionException;
34    import org.sat4j.specs.IVecInt;
35   
36    /*
37    * Created on 16 oct. 2003 To change the template for this generated file go to
38    * Window>Preferences>Java>Code Generation>Code and Comments
39    */
40   
41    /**
42    * Lazy data structure for clause using Watched Literals.
43    *
44    * @author leberre
45    */
 
46    public abstract class WLClause implements Constr, Serializable {
47   
48    private static final long serialVersionUID = 1L;
49   
50    private double activity;
51   
52    protected final int[] lits;
53   
54    protected final ILits voc;
55   
56    /**
57    * Creates a new basic clause
58    *
59    * @param voc
60    * the vocabulary of the formula
61    * @param ps
62    * A VecInt that WILL BE EMPTY after calling that method.
63    */
 
64  173798426 toggle public WLClause(IVecInt ps, ILits voc) {
65  173798426 lits = new int[ps.size()];
66  173798426 ps.moveTo(lits);
67  173798426 assert ps.size() == 0;
68  173798426 this.voc = voc;
69  173798426 activity = 0;
70    }
71   
72    /**
73    * Perform some sanity check before constructing a clause a) if a literal is
74    * assigned true, return null (the clause is satisfied) b) if a literal is
75    * assigned false, remove it c) if a clause contains a literal and its
76    * opposite (tautology) return null d) remove duplicate literals e) if the
77    * clause is empty, return null f) if the clause if unit, transmit it to the
78    * object responsible for unit propagation
79    *
80    * @param ps
81    * the list of literals
82    * @param voc
83    * the vocabulary used
84    * @param s
85    * the object responsible for unit propagation
86    * @return null if the clause should be ignored, the (possibly modified)
87    * list of literals otherwise
88    * @throws ContradictionException
89    * if discovered by unit propagation
90    */
 
91  3709407 toggle public static IVecInt sanityCheck(IVecInt ps, ILits voc,
92    UnitPropagationListener s) throws ContradictionException {
93    // si un litt???ral de ps est vrai, retourner vrai
94    // enlever les litt???raux falsifi???s de ps
95  15394263 for (int i = 0; i < ps.size();) {
96    // on verifie si le litteral est affecte
97  11685630 if (voc.isUnassigned(ps.get(i))) {
98    // on passe au literal suivant
99  11684679 i++;
100    } else {
101    // Si le litteral est satisfait, la clause est
102    // satisfaite
103  951 if (voc.isSatisfied(ps.get(i))) {
104    // on retourne la clause
105  774 return null;
106    }
107    // on enleve le ieme litteral
108  177 ps.delete(i);
109   
110    }
111    }
112   
113    // on trie le vecteur ps
114  3708633 ps.sortUnique();
115   
116    // ???limine les clauses tautologiques
117    // deux litt???raux de signe oppos???s apparaissent dans la m???me
118    // clause
119  11684167 for (int i = 0; i < ps.size() - 1; i++) {
120  7975703 if (ps.get(i) == (ps.get(i + 1) ^ 1)) {
121    // la clause est tautologique
122  169 return null;
123    }
124    }
125   
126  3708454 if (propagationCheck(ps, s))
127  254 return null;
128   
129  3708200 return ps;
130    }
131   
132    /**
133    * Check if this clause is null or unit
134    *
135    * @param p
136    * the list of literals (supposed to be clean as after a call to
137    * sanityCheck())
138    * @param s
139    * the object responsible for unit propagation
140    * @return true iff the clause should be ignored (because it's unit)
141    * @throws ContradictionException
142    * when detected by unit propagation
143    */
 
144  3708464 toggle static boolean propagationCheck(IVecInt ps, UnitPropagationListener s)
145    throws ContradictionException {
146  3708464 if (ps.size() == 0) {
147  10 throw new ContradictionException("Creating Empty clause ?"); //$NON-NLS-1$
148  3708454 } else if (ps.size() == 1) {
149  254 if (!s.enqueue(ps.get(0))) {
150  0 throw new ContradictionException("Contradictory Unit Clauses"); //$NON-NLS-1$
151    }
152  254 return true;
153    }
154   
155  3708200 return false;
156    }
157   
158    /**
159    * Creates a brand new clause, presumably from external data. Performs all
160    * sanity checks.
161    *
162    * @param s
163    * the object responsible for unit propagation
164    * @param voc
165    * the vocabulary
166    * @param literals
167    * the literals to store in the clause
168    * @return the created clause or null if the clause should be ignored
169    * (tautology for example)
170    */
 
171  153090 toggle public static WLClause brandNewClause(UnitPropagationListener s, ILits voc,
172    IVecInt literals) {
173  153090 WLClause c = new DefaultWLClause(literals, voc);
174  153090 c.register();
175  153090 return c;
176    }
177   
178    /*
179    * (non-Javadoc)
180    *
181    * @see Constr#calcReason(Solver, Lit, Vec)
182    */
 
183  927548367 toggle public void calcReason(int p, IVecInt outReason) {
184  927548367 assert outReason.size() == 0
185    && ((p == ILits.UNDEFINED) || (p == lits[0]));
186  927548367 final int[] mylits = lits;
187    for (int i = (p == ILits.UNDEFINED) ? 0 : 1; i < mylits.length; i++) {
188  1780183692 assert voc.isFalsified(mylits[i]);
189  1780183692 outReason.push(mylits[i] ^ 1);
190    }
191    }
192   
193    /*
194    * (non-Javadoc)
195    *
196    * @see Constr#remove(Solver)
197    */
 
198  30250 toggle public void remove() {
199  30250 voc.watches(lits[0] ^ 1).remove(this);
200  30250 voc.watches(lits[1] ^ 1).remove(this);
201    // la clause peut etre effacee
202    }
203   
204    /*
205    * (non-Javadoc)
206    *
207    * @see Constr#simplify(Solver)
208    */
 
209  0 toggle public boolean simplify() {
210  0 for (int i = 0; i < lits.length; i++) {
211  0 if (voc.isSatisfied(lits[i])) {
212  0 return true;
213    }
214    }
215  0 return false;
216    }
217   
 
218  904481466 toggle public boolean propagate(UnitPropagationListener s, int p) {
219  904481466 final int[] mylits = lits;
220    // Lits[1] doit contenir le litt???ral falsifi???
221  904481466 if (mylits[0] == (p ^ 1)) {
222    mylits[0] = mylits[1];
223    mylits[1] = p ^ 1;
224    }
225  904481466 assert mylits[1] == (p ^ 1);
226    // // Si le premier litt???ral est satisfait, la clause est satisfaite
227    // The solver appears to solve more benchmarks (while being sometimes
228    // slower)
229    // if commenting those lines.
230    // if (voc.isSatisfied(lits[0])) {
231    // // reinsert la clause dans la liste des clauses surveillees
232    // voc.watch(p, this);
233    // return true;
234    // }
235   
236    // Recherche un nouveau litt???ral ??? regarder
237    for (int i = 2; i < mylits.length; i++) {
238    if (!voc.isFalsified(mylits[i])) {
239  2072262665 mylits[1] = mylits[i];
240  2072262665 mylits[i] = p ^ 1;
241  2072262665 voc.watch(mylits[1] ^ 1, this);
242  2072262665 return true;
243    }
244    }
245    assert voc.isFalsified(mylits[1]);
246    // La clause est unitaire ou nulle
247    voc.watch(p, this);
248    // avance pour la propagation
249    return s.enqueue(mylits[0], this);
250    }
251   
252    /*
253    * For learnt clauses only @author leberre
254    */
 
255  30259 toggle public boolean locked() {
256  30259 return voc.getReason(lits[0]) == this;
257    }
258   
259    /**
260    * @return the activity of the clause
261    */
 
262  171102418 toggle public double getActivity() {
263  171102418 return activity;
264    }
265   
 
266  0 toggle @Override
267    public String toString() {
268  0 StringBuffer stb = new StringBuffer();
269  0 for (int i = 0; i < lits.length; i++) {
270  0 stb.append(Lits.toString(lits[i]));
271  0 stb.append("["); //$NON-NLS-1$
272  0 stb.append(voc.valueToString(lits[i]));
273  0 stb.append("]"); //$NON-NLS-1$
274  0 stb.append(" "); //$NON-NLS-1$
275    }
276  0 return stb.toString();
277    }
278   
279    /**
280    * Retourne le ieme literal de la clause. Attention, cet ordre change durant
281    * la recherche.
282    *
283    * @param i
284    * the index of the literal
285    * @return the literal
286    */
 
287  337573821 toggle public int get(int i) {
288  337573821 return lits[i];
289    }
290   
291    /**
292    * @param claInc
293    */
 
294  168595510 toggle public void incActivity(double claInc) {
295  168595510 activity += claInc;
296    }
297   
298    /**
299    * @param d
300    */
 
301  4568942 toggle public void rescaleBy(double d) {
302  4568942 activity *= d;
303    }
304   
 
305    toggle public int size() {
306    return lits.length;
307    }
308   
 
309  170975774 toggle public void assertConstraint(UnitPropagationListener s) {
310  170975774 boolean ret = s.enqueue(lits[0], this);
311  170975774 assert ret;
312    }
313   
 
314  16689519 toggle public ILits getVocabulary() {
315  16689519 return voc;
316    }
317   
 
318  0 toggle public int[] getLits() {
319  0 int[] tmp = new int[size()];
320  0 System.arraycopy(lits, 0, tmp, 0, size());
321  0 return tmp;
322    }
323   
324    }
 
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.