Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
141   504   46   7,83
114   261   0,45   18
18     3,5  
1    
 
  MinWatchPb       Line # 38 141 46 75,8% 0.7582418
 
  (176)
 
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.pb;
27   
28    import java.math.BigInteger;
29   
30    import org.sat4j.core.Vec;
31    import org.sat4j.core.VecInt;
32    import org.sat4j.minisat.core.ILits;
33    import org.sat4j.minisat.core.UnitPropagationListener;
34    import org.sat4j.specs.ContradictionException;
35    import org.sat4j.specs.IVec;
36    import org.sat4j.specs.IVecInt;
37   
 
38    public class MinWatchPb extends WatchPb {
39   
40    private static final long serialVersionUID = 1L;
41   
42    /**
43    * Liste des indices des litt???raux regardant la contrainte
44    */
45    protected boolean[] watched;
46   
47    /**
48    * Sert ??? d???terminer si la clause est watched par le litt???ral
49    */
50    protected int[] watching;
51   
52    /**
53    * Liste des indices des litt???raux regardant la contrainte
54    */
55    protected int watchingCount = 0;
56   
57    /**
58    * Constructeur de base des contraintes
59    *
60    * @param voc
61    * Informations sur le vocabulaire employ???
62    * @param ps
63    * Liste des litt???raux
64    * @param coefs
65    * Liste des coefficients
66    * @param moreThan
67    * Indication sur le comparateur
68    * @param degree
69    * Stockage du degr??? de la contrainte
70    */
 
71  1148808 toggle protected MinWatchPb(ILits voc, IDataStructurePB mpb) {
72   
73  1148808 super(mpb);
74  1148808 this.voc = voc;
75   
76  1148808 watching = new int[this.coefs.length];
77  1148808 watched = new boolean[this.coefs.length];
78  1148808 activity = 0;
79  1148808 watchCumul = BigInteger.ZERO;
80  1148808 locked = false;
81   
82  1148808 watchingCount = 0;
83   
84    }
85   
 
86  123264 toggle protected MinWatchPb(ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree) {
87   
88  123264 super(lits, coefs, degree);
89  123264 this.voc = voc;
90   
91  123264 watching = new int[this.coefs.length];
92  123264 watched = new boolean[this.coefs.length];
93  123264 activity = 0;
94  123264 watchCumul = BigInteger.ZERO;
95  123264 locked = false;
96   
97  123264 watchingCount = 0;
98   
99    }
100    /*
101    * (non-Javadoc)
102    *
103    * @see org.sat4j.minisat.constraints.WatchPb#computeWatches()
104    */
 
105  1271969 toggle @Override
106    protected void computeWatches() throws ContradictionException {
107  1271969 assert watchCumul.signum() == 0;
108  1271969 assert watchingCount == 0;
109  7476969 for (int i = 0; i < lits.length
110    && watchCumul.subtract(coefs[0]).compareTo(degree) < 0; i++) {
111  6205000 if (!voc.isFalsified(lits[i])) {
112  3087120 voc.watch(lits[i] ^ 1, this);
113  3087120 watching[watchingCount++] = i;
114  3087120 watched[i] = true;
115    // Mise ??? jour de la possibilit??? initiale
116  3087120 watchCumul = watchCumul.add(coefs[i]);
117    }
118    }
119   
120  1271969 if (learnt)
121  87997 watchMoreForLearntConstraint();
122   
123  1271969 if (watchCumul.compareTo(degree) < 0) {
124  32 throw new ContradictionException("non satisfiable constraint");
125    }
126  1271937 assert nbOfWatched() == watchingCount;
127    }
128   
 
129  87997 toggle private void watchMoreForLearntConstraint() {
130    // chercher tous les litteraux a regarder
131    // par ordre de niveau decroissant
132  87997 int free = 1;
133  87997 int maxlevel, maxi, level;
134   
135  176344 while ((watchCumul.subtract(coefs[0]).compareTo(degree) < 0)
136    && (free > 0)) {
137  88347 free = 0;
138    // regarder le litteral falsifie au plus bas niveau
139  88347 maxlevel = -1;
140  88347 maxi = -1;
141  3659024 for (int i = 0; i < lits.length; i++) {
142  3570677 if (voc.isFalsified(lits[i]) && !watched[i]) {
143  3170745 free++;
144  3170745 level = voc.getLevel(lits[i]);
145  3170745 if (level > maxlevel) {
146  256257 maxi = i;
147  256257 maxlevel = level;
148    }
149    }
150    }
151   
152  88347 if (free > 0) {
153  88319 assert maxi >= 0;
154  88319 voc.watch(lits[maxi] ^ 1, this);
155  88319 watching[watchingCount++] = maxi;
156  88319 watched[maxi] = true;
157    // Mise ??? jour de la possibilit??? initiale
158  88319 watchCumul = watchCumul.add(coefs[maxi]);
159  88319 free--;
160  88319 assert free >= 0;
161    }
162    }
163  87997 assert lits.length == 1 || watchingCount > 1;
164    }
165   
166    /*
167    * (non-Javadoc)
168    *
169    * @see org.sat4j.minisat.constraints.WatchPb#computePropagation(org.sat4j.minisat.UnitPropagationListener)
170    */
 
171  1183940 toggle @Override
172    protected void computePropagation(UnitPropagationListener s)
173    throws ContradictionException {
174    // On propage si n???cessaire
175  1183940 int ind = 0;
176  1184472 while (ind < lits.length
177    && watchCumul.subtract(coefs[watching[ind]]).compareTo(degree) < 0) {
178  532 if (voc.isUnassigned(lits[ind]) && !s.enqueue(lits[ind], this)) {
179  0 throw new ContradictionException("non satisfiable constraint");
180    }
181  532 ind++;
182    }
183    }
184   
185    /**
186    * @param s
187    * outil pour la propagation des litt???raux
188    * @param ps
189    * liste des litt???raux de la nouvelle contrainte
190    * @param coefs
191    * liste des coefficients des litt???raux de la contrainte
192    * @param moreThan
193    * d???termine si c'est une sup???rieure ou ???gal ??? l'origine
194    * @param degree
195    * fournit le degr??? de la contrainte
196    * @return une nouvelle clause si tout va bien, ou null si un conflit est
197    * d???tect???
198    */
 
199  499336 toggle public static MinWatchPb minWatchPbNew(UnitPropagationListener s,
200    ILits voc, IVecInt ps, IVecInt coefs, boolean moreThan, int degree)
201    throws ContradictionException {
202  499336 return minWatchPbNew(s, voc, ps, toVecBigInt(coefs), moreThan,
203    toBigInt(degree));
204    }
205   
206    /**
207    * @param s
208    * outil pour la propagation des litt???raux
209    * @param ps
210    * liste des litt???raux de la nouvelle contrainte
211    * @param coefs
212    * liste des coefficients des litt???raux de la contrainte
213    * @param moreThan
214    * d???termine si c'est une sup???rieure ou ???gal ??? l'origine
215    * @param degree
216    * fournit le degr??? de la contrainte
217    * @return une nouvelle clause si tout va bien, ou null si un conflit est
218    * d???tect???
219    */
 
220  779609 toggle public static MinWatchPb minWatchPbNew(UnitPropagationListener s,
221    ILits voc, IVecInt ps, IVec<BigInteger> coefs, boolean moreThan,
222    BigInteger degree) throws ContradictionException {
223    // Il ne faut pas modifier les param?tres
224  779609 VecInt litsVec = new VecInt(ps.size());
225  779609 IVec<BigInteger> coefsVec = new Vec<BigInteger>(coefs.size());
226  779609 ps.copyTo(litsVec);
227  779609 coefs.copyTo(coefsVec);
228   
229    // Ajouter les simplifications quand la structure sera d???finitive
230  779609 IDataStructurePB mpb = niceParameters(litsVec, coefsVec, moreThan,
231    degree, voc);
232   
233  779609 if (mpb == null)
234  0 return null;
235   
236  779609 MinWatchPb outclause = new MinWatchPb(voc, mpb);
237   
238  779609 if (outclause.degree.signum() <= 0) {
239  0 return null;
240    }
241   
242  779609 outclause.computeWatches();
243   
244  779592 outclause.computePropagation(s);
245   
246  779592 return outclause;
247   
248    }
249   
250    /**
251    * @param s
252    * a unit propagation listener
253    * @param voc
254    * the vocabulary
255    * @param mpb
256    * the PB constraint to normalize.
257    * @return a new PB contraint or null if a trivial inconsistency is
258    * detected.
259    */
 
260  0 toggle public static MinWatchPb normalizedMinWatchPbNew(UnitPropagationListener s,
261    ILits voc, IDataStructurePB mpb) throws ContradictionException {
262    // Il ne faut pas modifier les param?tres
263  0 MinWatchPb outclause = new MinWatchPb(voc, mpb);
264   
265  0 if (outclause.degree.signum() <= 0) {
266  0 return null;
267    }
268   
269  0 outclause.computeWatches();
270   
271  0 outclause.computePropagation(s);
272   
273  0 return outclause;
274   
275    }
276   
277    /**
278    * @param s
279    * a unit propagation listener
280    * @param voc
281    * the vocabulary
282    * @param mpb
283    * the PB constraint to normalize.
284    * @return a new PB contraint or null if a trivial inconsistency is
285    * detected.
286    */
 
287  123264 toggle public static MinWatchPb normalizedMinWatchPbNew(UnitPropagationListener s,
288    ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree) throws ContradictionException {
289    // Il ne faut pas modifier les param?tres
290  123264 MinWatchPb outclause = new MinWatchPb(voc, lits, coefs, degree);
291   
292  123264 if (outclause.degree.signum() <= 0) {
293  0 return null;
294    }
295   
296  123264 outclause.computeWatches();
297   
298  123264 outclause.computePropagation(s);
299   
300  123264 return outclause;
301   
302    }
303   
304    /**
305    * Nombre de litt???raux actuellement observ???
306    *
307    * @return nombre de litt???raux regard???s
308    */
 
309  899908191 toggle protected int nbOfWatched() {
310  899908191 int retour = 0;
311    for (int ind = 0; ind < this.watched.length; ind++) {
312    for (int i = 0; i < watchingCount; i++)
313  730706930 if (watching[i] == ind)
314    assert watched[ind];
315    retour += (this.watched[ind]) ? 1 : 0;
316    }
317  899908191 return retour;
318    }
319   
320    /**
321    * Propagation de la valeur de v???rit??? d'un litt???ral falsifi???
322    *
323    * @param s
324    * un prouveur
325    * @param p
326    * le litt???ral propag??? (il doit etre falsifie)
327    * @return false ssi une inconsistance est d???t???ct???e
328    */
 
329  252317710 toggle public boolean propagate(UnitPropagationListener s, int p) {
330  252317710 assert nbOfWatched() == watchingCount;
331  252317710 assert watchingCount > 1;
332   
333    // Recherche de l'indice du litt???ral p
334  252317710 int pIndiceWatching = 0;
335  661474205 while (pIndiceWatching < watchingCount
336    && (lits[watching[pIndiceWatching]] ^ 1) != p)
337  409156495 pIndiceWatching++;
338  252317710 int pIndice = watching[pIndiceWatching];
339   
340  252317710 assert p == (lits[pIndice] ^ 1);
341  252317710 assert watched[pIndice];
342   
343    // Recherche du coefficient maximal parmi ceux des litt???raux
344    // observ???s
345  252317710 BigInteger maxCoef = maximalCoefficient(pIndice);
346   
347    // Recherche de la compensation
348  252317710 maxCoef = updateWatched(maxCoef, pIndice);
349   
350  252317710 BigInteger upWatchCumul = watchCumul.subtract(coefs[pIndice]);
351  252317710 assert nbOfWatched() == watchingCount;
352   
353    // Effectuer les propagations, return si l'une est impossible
354  252317710 if (upWatchCumul.compareTo(degree) < 0) {
355    // conflit
356  0 voc.watch(p, this);
357  0 assert watched[pIndice];
358  0 assert !isSatisfiable();
359  0 return false;
360  252317710 } else if (upWatchCumul.compareTo(degree.add(maxCoef)) < 0) {
361   
362  83481023 assert watchingCount != 0;
363  83481023 BigInteger limit = upWatchCumul.subtract(degree);
364  584318747 for (int i = 0; i < watchingCount; i++) {
365  509260786 if (limit.compareTo(coefs[watching[i]]) < 0
366    && i != pIndiceWatching
367    && !voc.isSatisfied(lits[watching[i]])
368    && !s.enqueue(lits[watching[i]], this)) {
369  8423062 voc.watch(p, this);
370  8423062 assert !isSatisfiable();
371  8423062 return false;
372    }
373    }
374    // Si propagation ajoute la contrainte aux undos de p, conserver p
375  75057961 voc.undos(p).push(this);
376    }
377   
378    // sinon p peut sortir de la liste de watched
379  243894648 watched[pIndice] = false;
380  243894648 watchCumul = upWatchCumul;
381  243894648 watching[pIndiceWatching] = watching[--watchingCount];
382   
383  243894648 assert watchingCount != 0;
384  243894648 assert nbOfWatched() == watchingCount;
385   
386  243894648 return true;
387    }
388   
389    /**
390    * Enl???ve une contrainte du prouveur
391    */
 
392  0 toggle public void remove() {
393  0 for (int i = 0; i < watchingCount; i++) {
394  0 voc.watches(lits[watching[i]] ^ 1).remove(this);
395  0 this.watched[this.watching[i]] = false;
396    }
397  0 watchingCount = 0;
398  0 assert nbOfWatched() == watchingCount;
399    }
400   
401    /**
402    * M???thode appel???e lors du backtrack
403    *
404    * @param p
405    * un litt???ral d???saffect???
406    */
 
407  75053093 toggle public void undo(int p) {
408  75053093 voc.watch(p, this);
409  75053093 int pIndice = 0;
410  550966617 while ((lits[pIndice] ^ 1) != p)
411  475913524 pIndice++;
412   
413  75053093 assert pIndice < lits.length;
414   
415  75053093 watchCumul = watchCumul.add(coefs[pIndice]);
416   
417  75053093 assert watchingCount == nbOfWatched();
418   
419  75053093 watched[pIndice] = true;
420  75053093 watching[watchingCount++] = pIndice;
421   
422  75053093 assert watchingCount == nbOfWatched();
423    }
424   
425    /**
426    *
427    */
 
428  0 toggle public static WatchPb watchPbNew(ILits voc, IVecInt lits, IVecInt coefs,
429    boolean moreThan, int degree) {
430  0 return watchPbNew(voc, lits, toVecBigInt(coefs), moreThan,
431    toBigInt(degree));
432    }
433   
434    /**
435    *
436    */
 
437  61320 toggle public static WatchPb watchPbNew(ILits voc, IVecInt lits,
438    IVec<BigInteger> coefs, boolean moreThan, BigInteger degree) {
439  61320 IDataStructurePB mpb = null;
440  61320 mpb = niceCheckedParameters(lits, coefs, moreThan, degree, voc);
441  61320 return new MinWatchPb(voc, mpb);
442    }
443   
444    /**
445    *
446    */
 
447  0 toggle public static WatchPb normalizedWatchPbNew(ILits voc, IDataStructurePB mpb) {
448  0 return new MinWatchPb(voc, mpb);
449    }
450   
451    /**
452    * returns the maximal coefficient for the watched literals
453    *
454    * @param pIndice
455    * propagated literal : its coefficient is excluded from the
456    * search of the maximal coefficient
457    * @return
458    */
 
459  151985978 toggle protected BigInteger maximalCoefficient(int pIndice) {
460  151985978 BigInteger maxCoef = BigInteger.ZERO;
461  650364228 for (int i = 0; i < watchingCount; i++)
462  498378250 if (coefs[watching[i]].compareTo(maxCoef) > 0
463    && watching[i] != pIndice) {
464  152260418 maxCoef = coefs[watching[i]];
465    }
466   
467  151985978 assert learnt || maxCoef.signum() != 0;
468    // DLB assert maxCoef!=0;
469  151985978 return maxCoef;
470    }
471   
 
472  151985978 toggle protected BigInteger updateWatched(BigInteger mc, int pIndice) {
473  151985978 BigInteger maxCoef = mc;
474  151985978 if (watchingCount < size()) {
475  133101270 BigInteger upWatchCumul = watchCumul.subtract(coefs[pIndice]);
476   
477  133101270 BigInteger degreePlusMaxCoef = degree.add(maxCoef); // dvh
478  1522138801 for (int ind = 0; ind < lits.length; ind++) {
479  1495239532 if (upWatchCumul.compareTo(degreePlusMaxCoef) >= 0) {
480    // note: logic negated to old version // dvh
481  106202001 break;
482    }
483   
484  1389037531 if (!voc.isFalsified(lits[ind]) && !watched[ind]) {
485  109336874 upWatchCumul = upWatchCumul.add(coefs[ind]);
486  109336874 watched[ind] = true;
487  109336874 assert watchingCount < size();
488  109336874 watching[watchingCount++] = ind;
489  109336874 voc.watch(lits[ind] ^ 1, this);
490    // Si on obtient un nouveau coefficient maximum
491  109336874 if (coefs[ind].compareTo(maxCoef) > 0) {
492  15962 maxCoef = coefs[ind];
493  15962 degreePlusMaxCoef = degree.add(maxCoef); // update
494    // that one
495    // too
496    }
497    }
498    }
499  133101270 watchCumul = upWatchCumul.add(coefs[pIndice]);
500    }
501  151985978 return maxCoef;
502    }
503   
504    }
 
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.