Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
159   553   52   6,36
96   270   0,48   25
25     3,04  
1    
 
  MinWatchCard       Line # 38 159 52 62,9% 0.62857145
 
  (144)
 
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   
30    import org.sat4j.minisat.constraints.cnf.Lits;
31    import org.sat4j.minisat.core.Constr;
32    import org.sat4j.minisat.core.ILits;
33    import org.sat4j.minisat.core.Undoable;
34    import org.sat4j.minisat.core.UnitPropagationListener;
35    import org.sat4j.specs.ContradictionException;
36    import org.sat4j.specs.IVecInt;
37   
 
38    public class MinWatchCard implements Constr, Undoable, Serializable {
39   
40    private static final long serialVersionUID = 1L;
41   
42    public static final boolean ATLEAST = true;
43   
44    public static final boolean ATMOST = false;
45   
46    /**
47    * degree of the cardinality constraint
48    */
49    protected int degree;
50   
51    /**
52    * literals involved in the constraint
53    */
54    private int[] lits;
55   
56    /**
57    * contains the sign of the constraint : ATLEAT or ATMOST
58    */
59    private boolean moreThan;
60   
61    /**
62    * contains the sum of the coefficients of the watched literals
63    */
64    protected int watchCumul;
65   
66    /**
67    * Vocabulary of the constraint
68    */
69    private final ILits voc;
70   
71    /**
72    * Constructs and normalizes a cardinality constraint. used by
73    * minWatchCardNew in the non-normalized case.
74    *
75    * @param voc
76    * vocabulary used by the constraint
77    * @param ps
78    * literals involved in the constraint
79    * @param moreThan
80    * should be ATLEAST or ATMOST;
81    * @param degree
82    * degree of the constraint
83    */
 
84  250601 toggle public MinWatchCard(ILits voc, IVecInt ps, boolean moreThan, int degree) {
85    // On met en place les valeurs
86  250601 this.voc = voc;
87  250601 this.degree = degree;
88  250601 this.moreThan = moreThan;
89   
90    // On simplifie ps
91  250601 int[] index = new int[voc.nVars() * 2 + 2];
92  487474251 for (int i = 0; i < index.length; i++)
93  487223650 index[i] = 0;
94    // On repertorie les litt?raux utiles
95  1415193 for (int i = 0; i < ps.size(); i++) {
96  1164592 if (index[ps.get(i) ^ 1] == 0) {
97  1164579 index[ps.get(i)]++;
98    } else {
99  13 index[ps.get(i) ^ 1]--;
100    }
101    }
102    // On supprime les litt?raux inutiles
103  250601 int ind = 0;
104  1415193 while (ind < ps.size()) {
105  1164592 if (index[ps.get(ind)] > 0) {
106  1164566 index[ps.get(ind)]--;
107  1164566 ind++;
108    } else {
109    // ??
110  26 if ((ps.get(ind) & 1) != 0)
111  13 this.degree--;
112  26 ps.set(ind, ps.last());
113  26 ps.pop();
114    }
115    }
116   
117    // On copie les litt?raux de la contrainte
118  250601 lits = new int[ps.size()];
119  250601 ps.moveTo(lits);
120   
121    // On normalise la contrainte au sens de Barth
122  250601 normalize();
123   
124    }
125   
126    /**
127    * Constructs and normalizes a cardinality constraint. used by
128    * MinWatchCardPB.normalizedMinWatchCardNew() in the normalized case. <br />
129    * <strong>Should not be used if parameters are not already normalized</strong><br />
130    * This constraint is always an ATLEAST constraint.
131    *
132    * @param voc
133    * vocabulary used by the constraint
134    * @param ps
135    * literals involved in the constraint
136    * @param moreThan
137    * true si la contrainte est sup?rieure ou ?gale
138    * @param degree
139    * degree of the constraint
140    */
 
141  18412 toggle protected MinWatchCard(ILits voc, IVecInt ps, int degree) {
142    // On met en place les valeurs
143  18412 this.voc = voc;
144  18412 this.degree = degree;
145  18412 this.moreThan = ATLEAST;
146   
147    // On copie les litt?raux de la contrainte
148  18412 lits = new int[ps.size()];
149  18412 ps.moveTo(lits);
150   
151    }
152   
153    /**
154    * computes the reason for a literal
155    *
156    * @param p
157    * falsified literal (or Lit.UNDEFINED)
158    * @param outReason
159    * the reason to be computed. Vector of literals.
160    * @see Constr#calcReason(int p, IVecInt outReason)
161    */
 
162  48220540 toggle public void calcReason(int p, IVecInt outReason) {
163    // TODO calcReason: v?rifier par rapport ? l'article
164    // Pour chaque litt?ral
165  265540282 for (int i = 0; i < lits.length; i++) {
166    // Si il est falsifi?
167  217319742 if (voc.isFalsified(lits[i])) {
168    // On ajoute sa n?gation au vecteur
169  174564110 outReason.push(lits[i] ^ 1);
170    }
171    }
172    }
173   
174    /**
175    * Returns the activity of the constraint
176    *
177    * @return activity value of the constraint
178    * @see Constr#getActivity()
179    */
 
180  0 toggle public double getActivity() {
181    // TODO getActivity
182  0 return 0;
183    }
184   
185    /**
186    * Increments activity of the constraint
187    *
188    * @param claInc
189    * value to be added to the activity of the constraint
190    * @see Constr#incActivity(double claInc)
191    */
 
192  0 toggle public void incActivity(double claInc) {
193    // TODO incActivity
194    }
195   
196    /**
197    * Returns wether the constraint is learnt or not.
198    *
199    * @return false : a MinWatchCard cannot be learnt.
200    * @see Constr#learnt()
201    */
 
202  48469793 toggle public boolean learnt() {
203  48469793 return false;
204    }
205   
206    /**
207    * Simplifies the constraint w.r.t. the assignments of the literals
208    *
209    * @param voc
210    * vocabulary used
211    * @param ps
212    * literals involved
213    * @return value to be added to the degree. This value is less than or equal
214    * to 0.
215    */
 
216  267678 toggle protected static int linearisation(ILits voc, IVecInt ps) {
217    // Stockage de l'influence des modifications
218  267678 int modif = 0;
219   
220  1395493 for (int i = 0; i < ps.size();) {
221    // on verifie si le litteral est affecte
222  1127815 if (voc.isUnassigned(ps.get(i))) {
223  1127815 i++;
224    } else {
225    // Si le litteral est satisfait,
226    // ?a revient ? baisser le degr?
227  0 if (voc.isSatisfied(ps.get(i))) {
228  0 modif--;
229    }
230    // dans tous les cas, s'il est assign?,
231    // on enleve le ieme litteral
232  0 ps.set(i, ps.last());
233  0 ps.pop();
234    }
235    }
236   
237    // DLB: inutile?
238    // ps.shrinkTo(nbElement);
239  267678 assert modif <= 0;
240   
241  267678 return modif;
242    }
243   
244    /**
245    * Returns if the constraint is the reason for a unit propagation.
246    *
247    * @return true
248    * @see Constr#locked()
249    */
 
250  0 toggle public boolean locked() {
251    // TODO locked
252  0 return true;
253    }
254   
255    /**
256    * Constructs a cardinality constraint with a minimal set of watched
257    * literals Permet la cr?ation de contrainte de cardinalit? ? observation
258    * minimale
259    *
260    * @param s
261    * tool for propagation
262    * @param voc
263    * vocalulary used by the constraint
264    * @param ps
265    * literals involved in the constraint
266    * @param moreThan
267    * sign of the constraint. Should be ATLEAST or ATMOST.
268    * @param degree
269    * degree of the constraint
270    * @return a new cardinality constraint, null if it is a tautology
271    * @throws ContradictionException
272    */
 
273  249266 toggle public static MinWatchCard minWatchCardNew(UnitPropagationListener s,
274    ILits voc, IVecInt ps, boolean moreThan, int degree)
275    throws ContradictionException {
276   
277  249266 int mydegree = degree + linearisation(voc, ps);
278   
279  249266 if (ps.size() == 0 && mydegree > 0) {
280  0 throw new ContradictionException();
281  249266 } else if (ps.size() == mydegree || ps.size() <= 0) {
282  0 for (int i = 0; i < ps.size(); i++)
283  0 if (!s.enqueue(ps.get(i))) {
284  0 throw new ContradictionException();
285    }
286  0 return null;
287    }
288   
289    // La contrainte est maintenant cr??e
290  249266 MinWatchCard retour = new MinWatchCard(voc, ps, moreThan, mydegree);
291   
292  249266 if (retour.degree <= 0)
293  13 return null;
294   
295  249253 retour.computeWatches();
296   
297  249253 retour.computePropagation(s);
298   
299  249253 return retour;
300    }
301   
302    /**
303    * normalize the constraint (cf. P.Barth normalization)
304    */
 
305  250601 toggle public final void normalize() {
306    // Gestion du signe
307  250601 if (!moreThan) {
308    // On multiplie le degr? par -1
309  0 this.degree = 0 - this.degree;
310    // On r?vise chaque litt?ral
311  0 for (int indLit = 0; indLit < lits.length; indLit++) {
312  0 lits[indLit] = lits[indLit] ^ 1;
313  0 this.degree++;
314    }
315  0 this.moreThan = true;
316    }
317    }
318   
319    /**
320    * propagates the value of a falsified literal
321    *
322    * @param s
323    * tool for literal propagation
324    * @param p
325    * falsified literal
326    * @return false if an inconistency is detected, else true
327    */
 
328  205376142 toggle public boolean propagate(UnitPropagationListener s, int p) {
329   
330    // Si la contrainte est responsable de propagation unitaire
331  205376142 if (watchCumul == degree) {
332  0 voc.watch(p, this);
333  0 return false;
334    }
335   
336    // Recherche du litt?ral falsifi?
337  205376142 int indFalsified = 0;
338  305392185 while ((lits[indFalsified] ^ 1) != p)
339  100016043 indFalsified++;
340  205376142 assert watchCumul > degree;
341   
342    // Recherche du litt?ral swap
343  205376142 int indSwap = degree + 1;
344  466118976 while (indSwap < lits.length && voc.isFalsified(lits[indSwap]))
345  260742834 indSwap++;
346   
347    // Mise ? jour de la contrainte
348  205376142 if (indSwap == lits.length) {
349    // Si aucun litt?ral n'a ?t? trouv?
350  186258008 voc.watch(p, this);
351    // La limite est atteinte
352  186258008 watchCumul--;
353  186258008 assert watchCumul == degree;
354  186258008 voc.undos(p).push(this);
355   
356    // On met en queue les litt?raux impliqu?s
357  553968372 for (int i = 0; i <= degree; i++)
358  373176442 if ((p != (lits[i] ^ 1)) && !s.enqueue(lits[i], this))
359  5466078 return false;
360   
361  180791930 return true;
362    }
363    // Si un litt?ral a ?t? trouv? on les ?change
364  19118134 int tmpInt = lits[indSwap];
365  19118134 lits[indSwap] = lits[indFalsified];
366  19118134 lits[indFalsified] = tmpInt;
367   
368    // On observe le nouveau litt?ral
369  19118134 voc.watch(tmpInt ^ 1, this);
370   
371  19118134 return true;
372    }
373   
374    /**
375    * Removes a constraint from the solver
376    */
 
377  0 toggle public void remove() {
378  0 for (int i = 0; i <= degree; i++) {
379  0 voc.watches(lits[i] ^ 1).remove(this);
380    }
381    }
382   
383    /**
384    * Rescales the activity value of the constraint
385    *
386    * @param d
387    * rescale factor
388    */
 
389  0 toggle public void rescaleBy(double d) {
390    // TODO rescaleBy
391    }
392   
393    /**
394    * simplifies the constraint
395    *
396    * @return true if the constraint is satisfied, else false
397    */
 
398  0 toggle public boolean simplify() {
399    // Calcul de la valeur actuelle
400  0 for (int i = 0, count = 0; i < lits.length; i++)
401  0 if (voc.isSatisfied(lits[i]) && (++count == degree))
402  0 return true;
403   
404  0 return false;
405    }
406   
407    /**
408    * Returns a string representation of the constraint.
409    *
410    * @return representation of the constraint.
411    */
 
412  0 toggle @Override
413    public String toString() {
414  0 StringBuffer stb = new StringBuffer();
415  0 stb.append("Card (" + lits.length + ") : ");
416  0 if (lits.length > 0) {
417    // if (voc.isUnassigned(lits[0])) {
418  0 stb.append(Lits.toString(this.lits[0]));
419  0 stb.append("[");
420  0 stb.append(voc.valueToString(lits[0]));
421  0 stb.append("@");
422  0 stb.append(voc.getLevel(lits[0]));
423  0 stb.append("]");
424  0 stb.append(" "); //$NON-NLS-1$
425    // }
426  0 for (int i = 1; i < lits.length; i++) {
427    // if (voc.isUnassigned(lits[i])) {
428  0 stb.append(" + "); //$NON-NLS-1$
429  0 stb.append(Lits.toString(this.lits[i]));
430  0 stb.append("[");
431  0 stb.append(voc.valueToString(lits[i]));
432  0 stb.append("@");
433  0 stb.append(voc.getLevel(lits[i]));
434  0 stb.append("]");
435  0 stb.append(" "); //$NON-NLS-1$
436    // }
437    }
438  0 stb.append(">= "); //$NON-NLS-1$
439  0 stb.append(this.degree);
440    }
441  0 return stb.toString();
442    }
443   
444    /**
445    * Updates information on the constraint in case of a backtrack
446    *
447    * @param p
448    * unassigned literal
449    */
 
450  186255616 toggle public void undo(int p) {
451    // Le litt?ral observ? et falsifi? devient non assign?
452  186255616 watchCumul++;
453    }
454   
 
455  0 toggle public void setLearnt() {
456  0 throw new UnsupportedOperationException();
457    }
458   
 
459  0 toggle public void register() {
460  0 throw new UnsupportedOperationException();
461    }
462   
 
463  1446280 toggle public int size() {
464  1446280 return lits.length;
465    }
466   
 
467  2352109 toggle public int get(int i) {
468  2352109 return lits[i];
469    }
470   
 
471  0 toggle public void assertConstraint(UnitPropagationListener s) {
472  0 throw new UnsupportedOperationException();
473    }
474   
 
475  269000 toggle protected void computeWatches() {
476  269000 int indSwap = lits.length;
477  269000 int tmpInt;
478  1325554 for (int i = 0; i <= degree && i < indSwap; i++) {
479  1250067 while (voc.isFalsified(lits[i]) && --indSwap > i) {
480  193513 tmpInt = lits[i];
481  193513 lits[i] = lits[indSwap];
482  193513 lits[indSwap] = tmpInt;
483    }
484   
485    // Si le litteral est observable
486  1056554 if (!voc.isFalsified(lits[i])) {
487  1055860 watchCumul++;
488  1055860 voc.watch(lits[i] ^ 1, this);
489    }
490    }
491  269000 if (learnt()) {
492    // chercher tous les litteraux a regarder
493    // par ordre de niveau decroissant
494  1335 int free = 1;
495  2670 while ((watchCumul <= degree) && (free > 0)) {
496  1335 free = 0;
497    // regarder le litteral falsifie au plus bas niveau
498  1335 int maxlevel = -1, maxi = -1;
499  195542 for (int i = watchCumul; i < lits.length; i++) {
500  194207 if (voc.isFalsified(lits[i])) {
501  194207 free++;
502  194207 int level = voc.getLevel(lits[i]);
503  194207 if (level > maxlevel) {
504  4622 maxi = i;
505  4622 maxlevel = level;
506    }
507    }
508    }
509  1335 if (free > 0) {
510  1279 assert maxi >= 0;
511  1279 voc.watch(lits[maxi] ^ 1, this);
512  1279 tmpInt = lits[maxi];
513  1279 lits[maxi] = lits[watchCumul];
514  1279 lits[watchCumul] = tmpInt;
515  1279 watchCumul++;
516  1279 free--;
517  1279 assert free >= 0;
518    }
519    }
520  1335 assert lits.length == 1 || watchCumul > 1;
521    }
522   
523    }
524   
 
525  267665 toggle protected MinWatchCard computePropagation(UnitPropagationListener s)
526    throws ContradictionException {
527   
528    // Si on a des litteraux impliques
529  267665 if (watchCumul == degree) {
530  0 for (int i = 0; i < lits.length; i++)
531  0 if (!s.enqueue(lits[i])) {
532  0 throw new ContradictionException();
533    }
534  0 return null;
535    }
536   
537    // Si on n'observe pas suffisamment
538  267665 if (watchCumul < degree) {
539  0 throw new ContradictionException();
540    }
541  267665 return this;
542    }
543   
 
544  0 toggle public int[] getLits() {
545  0 int[] tmp = new int[size()];
546  0 System.arraycopy(lits, 0, tmp, 0, size());
547  0 return tmp;
548    }
549   
 
550  398322 toggle public ILits getVocabulary() {
551  398322 return voc;
552    }
553    }
 
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.