Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
100   426   35   4,55
64   194   0,56   22
22     2,55  
1    
 
  MaxWatchCard       Line # 39 100 35 48,4% 0.48387095
 
  (101)
 
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.card;
27   
28    import java.io.Serializable;
29    import java.math.BigInteger;
30   
31    import org.sat4j.minisat.constraints.cnf.Lits;
32    import org.sat4j.minisat.core.Constr;
33    import org.sat4j.minisat.core.ILits;
34    import org.sat4j.minisat.core.Undoable;
35    import org.sat4j.minisat.core.UnitPropagationListener;
36    import org.sat4j.specs.ContradictionException;
37    import org.sat4j.specs.IVecInt;
38   
 
39    public class MaxWatchCard implements Constr, Undoable, Serializable {
40   
41    private static final long serialVersionUID = 1L;
42   
43    /**
44    * Degr? de la contrainte de cardinalit?
45    */
46    private int degree;
47   
48    /**
49    * Liste des litt?raux de la contrainte
50    */
51    private int[] lits;
52   
53    /**
54    * D?termine si c'est une in?galit? sup?rieure ou ?gale
55    */
56    private boolean moreThan;
57   
58    /**
59    * Somme des coefficients des litt?raux observ?s
60    */
61    private int watchCumul;
62   
63    /**
64    * Vocabulaire de la contrainte
65    */
66    private final ILits voc;
67   
68    /**
69    * Constructeur de base cr?ant des contraintes vides
70    *
71    * @param size
72    * nombre de litt?raux de la contrainte
73    * @param learnt
74    * indique si la contrainte est apprise
75    */
 
76  249266 toggle private MaxWatchCard(ILits voc, IVecInt ps, boolean moreThan, int degree) {
77   
78    // On met en place les valeurs
79  249266 this.voc = voc;
80  249266 this.degree = degree;
81  249266 this.moreThan = moreThan;
82   
83    // On simplifie ps
84  249266 int[] index = new int[voc.nVars() * 2 + 2];
85  481348566 for (int i = 0; i < index.length; i++)
86  481099300 index[i] = 0;
87    // On repertorie les litt?raux utiles
88  1016665 for (int i = 0; i < ps.size(); i++) {
89  767399 if (index[ps.get(i) ^ 1] == 0) {
90  767386 index[ps.get(i)]++;
91    } else {
92  13 index[ps.get(i) ^ 1]--;
93    }
94    }
95    // On supprime les litt?raux inutiles
96  249266 int ind = 0;
97  1016665 while (ind < ps.size()) {
98  767399 if (index[ps.get(ind)] > 0) {
99  767373 index[ps.get(ind)]--;
100  767373 ind++;
101    } else {
102  26 if ((ps.get(ind) & 1) != 0)
103  13 this.degree--;
104  26 ps.set(ind, ps.last());
105  26 ps.pop();
106    }
107    }
108   
109    // On copie les litt?raux de la contrainte
110  249266 lits = new int[ps.size()];
111  249266 ps.moveTo(lits);
112   
113    // On normalise la contrainte au sens de Barth
114  249266 normalize();
115   
116    // Mise en place de l'observation maximale
117  249266 watchCumul = 0;
118   
119    // On observe les litt?raux non falsifi?
120  1016639 for (int i = 0; i < lits.length; i++) {
121    // Rappel: les ?l?ments falsifi?s ne seront jamais d?pil?s
122  767373 if (!voc.isFalsified(lits[i])) {
123  767373 watchCumul++;
124  767373 voc.watch(lits[i] ^ 1, this);
125    }
126    }
127    }
128   
129    /**
130    * Calcule la cause de l'affection d'un litt?ral
131    *
132    * @param p
133    * un litt?ral falsifi? (ou Lit.UNDEFINED)
134    * @param outReason
135    * vecteur de litt?raux ? remplir
136    * @see Constr#calcReason(int p, IVecInt outReason)
137    */
 
138  46626683 toggle public void calcReason(int p, IVecInt outReason) {
139    // TODO calcReason: v?rifier par rapport ? l'article
140    // Pour chaque litt?ral
141  255519717 for (int i = 0; i < lits.length; i++) {
142    // Si il est falsifi?
143  208893034 if (voc.isFalsified(lits[i])) {
144    // On ajoute sa n?gation au vecteur
145  167447856 outReason.push(lits[i] ^ 1);
146    }
147    }
148    }
149   
150    /**
151    * Obtenir la valeur de l'activit? de la contrainte
152    *
153    * @return la valeur de l'activit? de la contrainte
154    * @see Constr#getActivity()
155    */
 
156  0 toggle public double getActivity() {
157    // TODO getActivity
158  0 return 0;
159    }
160   
161    /**
162    * Incr?mente la valeur de l'activit? de la contrainte
163    *
164    * @param claInc
165    * incr?ment de l'activit? de la contrainte
166    * @see Constr#incActivity(double claInc)
167    */
 
168  0 toggle public void incActivity(double claInc) {
169    // TODO incActivity
170    }
171   
172    /**
173    * D?termine si la contrainte est apprise
174    *
175    * @return true si la contrainte est apprise, false sinon
176    * @see Constr#learnt()
177    */
 
178  46626683 toggle public boolean learnt() {
179    // TODO learnt
180  46626683 return false;
181    }
182   
183    /**
184    * La contrainte est la cause d'une propagation unitaire
185    *
186    * @return true si c'est le cas, false sinon
187    * @see Constr#locked()
188    */
 
189  0 toggle public boolean locked() {
190    // TODO locked
191  0 return true;
192    }
193   
194    /**
195    * Permet la cr?ation de contrainte de cardinalit? ? observation minimale
196    *
197    * @param s
198    * outil pour la propagation des litt?raux
199    * @param voc
200    * vocabulaire utilis? par la contrainte
201    * @param ps
202    * liste des litt?raux de la nouvelle contrainte
203    * @param moreThan
204    * d?termine si c'est une sup?rieure ou ?gal ? l'origine
205    * @param degree
206    * fournit le degr? de la contrainte
207    * @return une nouvelle clause si tout va bien, null sinon
208    * @throws ContradictionException
209    */
 
210  249266 toggle public static MaxWatchCard maxWatchCardNew(UnitPropagationListener s,
211    ILits voc, IVecInt ps, boolean moreThan, int degree)
212    throws ContradictionException {
213   
214  249266 MaxWatchCard outclause = null;
215   
216    // La contrainte ne doit pas ?tre vide
217  249266 if (ps.size() == 0) {
218  0 throw new ContradictionException("Creating empty clause"); //$NON-NLS-1$
219  249266 } else if (ps.size() == degree) {
220  0 for (int i = 0; i < ps.size(); i++)
221  0 if (!s.enqueue(ps.get(i))) {
222  0 throw new ContradictionException(
223    "Contradiction with implied literal"); //$NON-NLS-1$
224    }
225  0 return null;
226    }
227   
228    // On cree la contrainte
229  249266 outclause = new MaxWatchCard(voc, ps, moreThan, degree);
230   
231    // Si le degr? est insufisant
232  249266 if (outclause.degree <= 0)
233  13 return null;
234   
235    // Si il n'y a aucune chance de satisfaire la contrainte
236  249253 if (outclause.watchCumul < outclause.degree)
237  0 throw new ContradictionException();
238   
239    // Si les litt?raux observ?s sont impliqu?s
240  249253 if (outclause.watchCumul == outclause.degree) {
241  0 for (int i = 0; i < outclause.lits.length; i++) {
242  0 if (!s.enqueue(outclause.lits[i])) {
243  0 throw new ContradictionException(
244    "Contradiction with implied literal"); //$NON-NLS-1$
245    }
246    }
247  0 return null;
248    }
249   
250  249253 return outclause;
251    }
252   
253    /**
254    * On normalise la contrainte au sens de Barth
255    */
 
256  249266 toggle public final void normalize() {
257    // Gestion du signe
258  249266 if (!moreThan) {
259    // On multiplie le degr? par -1
260  0 this.degree = 0 - this.degree;
261    // On r?vise chaque litt?ral
262  0 for (int indLit = 0; indLit < lits.length; indLit++) {
263  0 lits[indLit] = lits[indLit] ^ 1;
264  0 this.degree++;
265    }
266  0 this.moreThan = true;
267    }
268    }
269   
270    /**
271    * Propagation de la valeur de v?rit? d'un litt?ral falsifi?
272    *
273    * @param s
274    * objet utilis? pour la propagation
275    * @param p
276    * le litt?ral propag? (il doit etre falsifie)
277    * @return false ssi une inconsistance est d?t?ct?e
278    */
 
279  261624975 toggle public boolean propagate(UnitPropagationListener s, int p) {
280   
281    // On observe toujours tous les litt?raux
282  261624975 voc.watch(p, this);
283  261624975 assert !voc.isFalsified(p);
284   
285    // Si le litt?ral p est impliqu?
286  261624975 if (this.watchCumul == this.degree)
287  5181543 return false;
288   
289    // On met en place la mise ? jour du compteur
290  256443432 voc.undos(p).push(this);
291  256443432 watchCumul--;
292   
293    // Si les litt?raux restant sont impliqu?s
294  256443432 if (watchCumul == degree) {
295  205999452 for (int q : lits) {
296  594724585 if (voc.isUnassigned(q) && !s.enqueue(q, this)) {
297  0 return false;
298    }
299    }
300    }
301  256443432 return true;
302    }
303   
304    /**
305    * Enl?ve une contrainte du prouveur
306    */
 
307  0 toggle public void remove() {
308  0 for (int q : lits) {
309  0 voc.watches(q ^ 1).remove(this);
310    }
311    }
312   
313    /**
314    * Permet le r??chantillonage de l'activit? de la contrainte
315    *
316    * @param d
317    * facteur d'ajustement
318    */
 
319  0 toggle public void rescaleBy(double d) {
320    }
321   
322    /**
323    * Simplifie la contrainte(l'all?ge)
324    *
325    * @return true si la contrainte est satisfaite, false sinon
326    */
 
327  0 toggle public boolean simplify() {
328   
329  0 int i = 0;
330   
331    // On esp?re le maximum de la somme
332  0 int curr = watchCumul;
333   
334    // Pour chaque litt?ral
335  0 while (i < this.lits.length) {
336    // On d?cr?mente si l'espoir n'est pas fond?
337  0 if (voc.isUnassigned(lits[i++])) {
338  0 curr--;
339  0 if (curr < this.degree)
340  0 return false;
341    }
342    }
343   
344  0 return false;
345    }
346   
347    /**
348    * Cha?ne repr?sentant la contrainte
349    *
350    * @return Cha?ne repr?sentant la contrainte
351    */
 
352  0 toggle @Override
353    public String toString() {
354  0 StringBuffer stb = new StringBuffer();
355   
356  0 if (lits.length > 0) {
357  0 if (voc.isUnassigned(lits[0])) {
358  0 stb.append(Lits.toString(this.lits[0]));
359  0 stb.append(" "); //$NON-NLS-1$
360    }
361  0 for (int i = 1; i < lits.length; i++) {
362  0 if (voc.isUnassigned(lits[i])) {
363  0 stb.append(" + "); //$NON-NLS-1$
364  0 stb.append(Lits.toString(this.lits[i]));
365  0 stb.append(" "); //$NON-NLS-1$
366    }
367    }
368  0 stb.append(">= "); //$NON-NLS-1$
369  0 stb.append(this.degree);
370    }
371  0 return stb.toString();
372    }
373   
374    /**
375    * M?thode appel?e lors du backtrack
376    *
377    * @param p
378    * le litt?ral d?saffect?
379    */
 
380  256410200 toggle public void undo(int p) {
381  256410200 watchCumul++;
382    }
383   
 
384  0 toggle public void setLearnt() {
385  0 throw new UnsupportedOperationException();
386    }
387   
 
388  0 toggle public void register() {
389  0 throw new UnsupportedOperationException();
390    }
391   
 
392  0 toggle public int size() {
393  0 return lits.length;
394    }
395   
 
396  0 toggle public int get(int i) {
397  0 return lits[i];
398    }
399   
 
400  0 toggle public void assertConstraint(UnitPropagationListener s) {
401  0 throw new UnsupportedOperationException();
402    }
403   
404    /*
405    * (non-Javadoc)
406    *
407    * @see org.sat4j.minisat.constraints.pb.PBConstr#getCoefficient(int)
408    */
 
409  0 toggle public BigInteger getCoef(int literal) {
410  0 return BigInteger.ONE;
411    }
412   
413    /*
414    * (non-Javadoc)
415    *
416    * @see org.sat4j.minisat.constraints.pb.PBConstr#getDegree()
417    */
 
418  0 toggle public BigInteger getDegree() {
419  0 return BigInteger.valueOf(degree);
420    }
421   
 
422  0 toggle public ILits getVocabulary() {
423  0 return voc;
424    }
425   
426    }
 
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.