Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
77   331   24   5,92
52   151   0,47   13
13     2,77  
1    
 
  MaxWatchPb       Line # 38 77 24 69,7% 0.6971831
 
  (177)
 
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 MaxWatchPb extends WatchPb {
39   
40    private static final long serialVersionUID = 1L;
41   
42    /**
43    * Constructeur de base cr?ant des contraintes vides
44    *
45    * @param voc
46    * Informations sur le vocabulaire employ?
47    * @param ps
48    * Liste des litt?raux
49    * @param coefs
50    * Liste des coefficients
51    * @param moreThan
52    * Indication sur le comparateur
53    * @param degree
54    * Stockage du degr? de la contrainte
55    */
 
56  905007 toggle private MaxWatchPb(ILits voc, IDataStructurePB mpb) {
57   
58  905007 super(mpb);
59  905007 this.voc = voc;
60   
61  905007 activity = 0;
62  905007 watchCumul = BigInteger.ZERO;
63  905007 locked = false;
64    }
65   
 
66  246528 toggle private MaxWatchPb(ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree) {
67   
68  246528 super(lits, coefs, degree);
69  246528 this.voc = voc;
70   
71  246528 activity = 0;
72  246528 watchCumul = BigInteger.ZERO;
73  246528 locked = false;
74    }
75   
76    /**
77    * Permet l'observation de tous les litt???raux
78    *
79    * @see org.sat4j.minisat.constraints.WatchPb#computeWatches()
80    */
 
81  1151442 toggle @Override
82    protected void computeWatches() throws ContradictionException {
83  1151442 assert watchCumul.equals(BigInteger.ZERO);
84  10061266 for (int i = 0; i < lits.length; i++) {
85  8909824 if (voc.isFalsified(lits[i])) {
86  2541637 if (learnt)
87  2541506 voc.undos(lits[i] ^ 1).push(this);
88    } else {
89    // Mise ? jour de la possibilit? initiale
90  6368187 voc.watch(lits[i] ^ 1, this);
91  6368187 watchCumul = watchCumul.add(coefs[i]);
92    }
93    }
94   
95  1151442 assert watchCumul.compareTo(recalcLeftSide()) >= 0;
96  1151442 if (!learnt && watchCumul.compareTo(degree) < 0) {
97  17 throw new ContradictionException("non satisfiable constraint");
98    }
99    }
100   
101    /*
102    * (non-Javadoc)
103    *
104    * @see org.sat4j.minisat.constraints.WatchPb#computePropagation()
105    */
 
106  1026121 toggle @Override
107    protected void computePropagation(UnitPropagationListener s)
108    throws ContradictionException {
109    // On propage
110  1026121 int ind = 0;
111  1026387 while (ind < coefs.length
112    && watchCumul.subtract(coefs[ind]).compareTo(degree) < 0) {
113  266 if (voc.isUnassigned(lits[ind]) && !s.enqueue(lits[ind], this))
114  0 throw new ContradictionException("non satisfiable constraint");
115  266 ind++;
116    }
117  1026121 assert watchCumul.compareTo(recalcLeftSide()) >= 0;
118    }
119   
120    /**
121    * @param s
122    * outil pour la propagation des litt?raux
123    * @param ps
124    * liste des litt?raux de la nouvelle contrainte
125    * @param coefs
126    * liste des coefficients des litt?raux de la contrainte
127    * @param moreThan
128    * d?termine si c'est une sup?rieure ou ?gal ? l'origine
129    * @param degree
130    * fournit le degr? de la contrainte
131    * @return une nouvelle clause si tout va bien, ou null si un conflit est
132    * d?tect?
133    */
 
134  499336 toggle public static MaxWatchPb maxWatchPbNew(UnitPropagationListener s,
135    ILits voc, IVecInt ps, IVecInt coefs, boolean moreThan, int degree)
136    throws ContradictionException {
137  499336 return maxWatchPbNew(s, voc, ps, toVecBigInt(coefs), moreThan,
138    toBigInt(degree));
139    }
140   
141    /**
142    * @param s
143    * outil pour la propagation des litt?raux
144    * @param ps
145    * liste des litt?raux de la nouvelle contrainte
146    * @param coefs
147    * liste des coefficients des litt?raux de la contrainte
148    * @param moreThan
149    * d?termine si c'est une sup?rieure ou ?gal ? l'origine
150    * @param degree
151    * fournit le degr? de la contrainte
152    * @return une nouvelle clause si tout va bien, ou null si un conflit est
153    * d?tect?
154    */
 
155  779610 toggle public static MaxWatchPb maxWatchPbNew(UnitPropagationListener s,
156    ILits voc, IVecInt ps, IVec<BigInteger> coefs, boolean moreThan,
157    BigInteger degree) throws ContradictionException {
158   
159    // Il ne faut pas modifier les param?tres
160  779610 VecInt litsVec = new VecInt();
161  779610 IVec<BigInteger> coefsVec = new Vec<BigInteger>();
162  779610 ps.copyTo(litsVec);
163  779610 coefs.copyTo(coefsVec);
164   
165  779610 IDataStructurePB mpb = niceParameters(litsVec, coefsVec, moreThan,
166    degree, voc);
167   
168  779610 if (mpb == null) {
169  0 return null;
170    }
171  779610 MaxWatchPb outclause = new MaxWatchPb(voc, mpb);
172   
173  779610 if (outclause.degree.signum() <= 0)
174  0 return null;
175  779610 outclause.computeWatches();
176  779593 outclause.computePropagation(s);
177   
178  779593 return outclause;
179   
180    }
181   
182    /**
183    * Propagation de la valeur de v?rit? d'un litt?ral falsifi?
184    *
185    * @param s
186    * un prouveur
187    * @param p
188    * le litt?ral propag? (il doit etre falsifie)
189    * @return false ssi une inconsistance est d?tect?e
190    */
 
191  335673260 toggle public boolean propagate(UnitPropagationListener s, int p) {
192  335673260 voc.watch(p, this);
193   
194  335673260 assert watchCumul.compareTo(recalcLeftSide()) >= 0 : "" + watchCumul
195    + "/" + recalcLeftSide() + ":" + learnt;
196   
197    // Si le litt?ral est impliqu? il y a un conflit
198  335673260 int indiceP = 0;
199    while ((lits[indiceP] ^ 1) != p)
200    indiceP++;
201   
202  335673260 BigInteger coefP = coefs[indiceP];
203   
204  335673260 BigInteger newcumul = watchCumul.subtract(coefP);
205  335673260 if (newcumul.compareTo(degree) < 0) {
206    // System.out.println(this.analyse(new ConstrHandle()));
207   
208  4874569 assert !isSatisfiable();
209  4874569 return false;
210    }
211   
212    // On met en place la mise ? jour du compteur
213  330798691 voc.undos(p).push(this);
214  330798691 watchCumul = newcumul;
215   
216    // On propage
217  330798691 int ind = 0;
218  330798691 BigInteger limit = watchCumul.subtract(degree);
219  954826504 while (ind < coefs.length && limit.compareTo(coefs[ind]) < 0) {
220  624027813 if (voc.isUnassigned(lits[ind]) && (!s.enqueue(lits[ind], this))) {
221  0 assert !isSatisfiable();
222  0 return false;
223    }
224  624027813 ind++;
225    }
226   
227  330798691 assert learnt || watchCumul.compareTo(recalcLeftSide()) >= 0;
228  330798691 assert watchCumul.compareTo(recalcLeftSide()) >= 0;
229  330798691 return true;
230    }
231   
232    /**
233    * Enl???ve une contrainte du prouveur
234    */
 
235  0 toggle public void remove() {
236  0 for (int i = 0; i < lits.length; i++) {
237  0 if (!voc.isFalsified(lits[i]))
238  0 voc.watches(lits[i] ^ 1).remove(this);
239    }
240    }
241   
242    /**
243    * M?thode appel?e lors du backtrack
244    *
245    * @param p
246    * un litt?ral d?saffect?
247    */
 
248  333241869 toggle public void undo(int p) {
249  333241869 int indiceP = 0;
250    while ((lits[indiceP] ^ 1) != p)
251    indiceP++;
252   
253  333241869 assert coefs[indiceP].signum() > 0;
254   
255  333241869 watchCumul = watchCumul.add(coefs[indiceP]);
256    }
257   
258    /**
259    *
260    */
 
261  0 toggle public static WatchPb watchPbNew(ILits voc, IVecInt lits, IVecInt coefs,
262    boolean moreThan, int degree) {
263  0 return watchPbNew(voc, lits, toVecBigInt(coefs), moreThan,
264    toBigInt(degree));
265    }
266   
267    /**
268    *
269    */
 
270  125397 toggle public static WatchPb watchPbNew(ILits voc, IVecInt lits,
271    IVec<BigInteger> coefs, boolean moreThan, BigInteger degree) {
272  125397 IDataStructurePB mpb = null;
273  125397 mpb = niceCheckedParameters(lits, coefs, moreThan, degree, voc);
274  125397 return new MaxWatchPb(voc, mpb);
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  0 toggle public static MaxWatchPb normalizedMaxWatchPbNew(UnitPropagationListener s,
288    ILits voc, IDataStructurePB mpb) throws ContradictionException {
289    // Il ne faut pas modifier les param?tres
290  0 MaxWatchPb outclause = new MaxWatchPb(voc, mpb);
291   
292  0 if (outclause.degree.signum() <= 0) {
293  0 return null;
294    }
295   
296  0 outclause.computeWatches();
297   
298  0 outclause.computePropagation(s);
299   
300  0 return outclause;
301   
302    }
303   
304    /**
305    * @param s
306    * a unit propagation listener
307    * @param voc
308    * the vocabulary
309    * @param mpb
310    * the PB constraint to normalize.
311    * @return a new PB contraint or null if a trivial inconsistency is
312    * detected.
313    */
 
314  246528 toggle public static MaxWatchPb normalizedMaxWatchPbNew(UnitPropagationListener s,
315    ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree) throws ContradictionException {
316    // Il ne faut pas modifier les param?tres
317  246528 MaxWatchPb outclause = new MaxWatchPb(voc, lits, coefs, degree);
318   
319  246528 if (outclause.degree.signum() <= 0) {
320  0 return null;
321    }
322   
323  246528 outclause.computeWatches();
324   
325  246528 outclause.computePropagation(s);
326   
327  246528 return outclause;
328   
329    }
330   
331    }
 
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.