Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
166   584   50   4,49
84   316   0,52   37
37     2,32  
1    
 
  WatchPb       Line # 43 166 50 60,6% 0.6062718
 
  (181)
 
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.io.Serializable;
29    import java.math.BigInteger;
30    import java.util.Random;
31   
32    import org.sat4j.core.Vec;
33    import org.sat4j.core.VecInt;
34    import org.sat4j.minisat.constraints.cnf.Lits;
35    import org.sat4j.minisat.core.Constr;
36    import org.sat4j.minisat.core.ILits;
37    import org.sat4j.minisat.core.Undoable;
38    import org.sat4j.minisat.core.UnitPropagationListener;
39    import org.sat4j.specs.ContradictionException;
40    import org.sat4j.specs.IVec;
41    import org.sat4j.specs.IVecInt;
42   
 
43    public abstract class WatchPb implements PBConstr, Undoable, Serializable {
44   
45    /**
46    * constant for the initial type of inequality less than or equal
47    */
48    public static final boolean ATMOST = false;
49   
50    /**
51    * constant for the initial type of inequality more than or equal
52    */
53    public static final boolean ATLEAST = true;
54   
55    /**
56    * variable needed for the sort method
57    */
58    private static final Random rand = new Random(91648253);
59   
60    /**
61    * constraint activity
62    */
63    protected double activity;
64   
65    /**
66    * coefficients of the literals of the constraint
67    */
68    protected BigInteger[] coefs;
69   
70    /**
71    * degree of the pseudo-boolean constraint
72    */
73    protected BigInteger degree;
74   
75    /**
76    * literals of the constraint
77    */
78    protected int[] lits;
79   
80    /**
81    * true if the constraint is a learned constraint
82    */
83    protected boolean learnt = false;
84   
85    /**
86    * true if the constraint is the origin of unit propagation
87    */
88    protected boolean locked;
89   
90    /**
91    * sum of the coefficients of the literals satisfied or unvalued
92    */
93    protected BigInteger watchCumul = BigInteger.ZERO;
94   
95    /**
96    * constraint's vocabulary
97    */
98    protected ILits voc;
99   
100    /**
101    * This constructor is only available for the serialization.
102    */
 
103  0 toggle WatchPb() {
104    }
105   
 
106  2053815 toggle WatchPb(IDataStructurePB mpb) {
107  2053815 int size = mpb.size();
108  2053815 lits = new int[size];
109  2053815 this.coefs = new BigInteger[size];
110  2053815 mpb.buildConstraintFromMapPb(lits, coefs);
111   
112  2053815 this.degree = mpb.getDegree();
113   
114    // On peut trier suivant les coefficients
115  2053815 sort();
116    }
117   
 
118  369792 toggle WatchPb(int[] lits, BigInteger[] coefs, BigInteger degree) {
119  369792 this.lits = lits;
120  369792 this.coefs = coefs;
121  369792 this.degree = degree;
122    // On peut trier suivant les coefficients
123  369792 sort();
124    }
125   
126    /**
127    * This predicate tests wether the constraint is assertive at decision level dl
128    *
129    * @param dl
130    * @return true iff the constraint is assertive at decision level dl.
131    */
 
132  0 toggle public boolean isAssertive(int dl) {
133  0 BigInteger slack = BigInteger.ZERO;
134  0 for (int i = 0; i < lits.length; i++) {
135  0 if ((coefs[i].signum() > 0)
136    && ((!voc.isFalsified(lits[i]) || voc.getLevel(lits[i]) >= dl)))
137  0 slack = slack.add(coefs[i]);
138    }
139  0 slack = slack.subtract(degree);
140  0 if (slack.signum() < 0)
141  0 return false;
142  0 for (int i = 0; i < lits.length; i++) {
143  0 if ((coefs[i].signum() > 0)
144    && (voc.isUnassigned(lits[i]) || voc.getLevel(lits[i]) >= dl)
145    && (slack.compareTo(coefs[i]) < 0)) {
146  0 return true;
147    }
148    }
149  0 return false;
150    }
151   
152    /**
153    * compute the reason for the assignment of a literal
154    *
155    * @param p
156    * a falsified literal (or Lit.UNDEFINED)
157    * @param outReason
158    * list of falsified literals for which the negation is the reason of the assignment
159    * @see Constr#calcReason(int, IVecInt)
160    */
 
161  186250858 toggle public void calcReason(int p, IVecInt outReason) {
162  186250858 for (int q : lits) {
163    if (voc.isFalsified(q)) {
164  706009647 outReason.push(q ^ 1);
165    }
166    }
167    }
168   
169    abstract protected void computeWatches() throws ContradictionException;
170   
171    abstract protected void computePropagation(UnitPropagationListener s)
172    throws ContradictionException;
173   
174    /**
175    * to obtain the i-th literal of the constraint
176    *
177    * @param i
178    * index of the literal
179    * @return the literal
180    */
 
181  52543755 toggle public int get(int i) {
182  52543755 return lits[i];
183    }
184   
185    /**
186    * to obtain the coefficient of the i-th literal of the constraint
187    *
188    * @param i
189    * index of the literal
190    * @return coefficient of the literal
191    */
 
192  21951450 toggle public BigInteger getCoef(int i) {
193  21951450 return coefs[i];
194    }
195   
196    /**
197    * to obtain the activity value of the constraint
198    *
199    * @return activity value of the constraint
200    * @see Constr#getActivity()
201    */
 
202  0 toggle public double getActivity() {
203  0 return activity;
204    }
205   
 
206  2683812 toggle public static IDataStructurePB niceParameters(IVecInt ps,
207    IVec<BigInteger> bigCoefs, boolean moreThan, BigInteger bigDeg,
208    ILits voc) throws ContradictionException {
209    // Ajouter les simplifications quand la structure sera d?finitive
210  2683812 if (ps.size() == 0) {
211  0 throw new ContradictionException("Creating Empty clause ?");
212  2683812 } else if (ps.size() != bigCoefs.size()) {
213  0 throw new IllegalArgumentException(
214    "Contradiction dans la taille des tableaux ps=" + ps.size()
215    + " coefs=" + bigCoefs.size() + ".");
216    }
217  2683812 return niceCheckedParameters(ps, bigCoefs, moreThan, bigDeg, voc);
218    }
219   
 
220  2897309 toggle public static IDataStructurePB niceCheckedParameters(IVecInt ps,
221    IVec<BigInteger> bigCoefs, boolean moreThan, BigInteger bigDeg,
222    ILits voc) {
223  2897309 assert ps.size() != 0 && ps.size() == bigCoefs.size();
224  2897309 int[] lits = new int[ps.size()];
225  2897309 ps.copyTo(lits);
226  2897309 BigInteger[] bc = new BigInteger[bigCoefs.size()];
227  2897309 bigCoefs.copyTo(bc);
228  2897309 BigInteger bigDegree = bigDeg;
229  2897309 if (!moreThan) {
230  242572 for (int i = 0; i < lits.length; i++) {
231  218646 bc[i] = bc[i].negate();
232    }
233  23926 bigDegree = bigDegree.negate();
234    }
235   
236  24340395 for (int i = 0; i < bc.length; i++)
237  21443086 if (bc[i].signum() < 0) {
238  10279806 lits[i] = lits[i] ^ 1;
239  10279806 bc[i] = bc[i].negate();
240  10279806 bigDegree = bigDegree.add(bc[i]);
241    }
242   
243  2897309 IDataStructurePB mpb = new MapPb(voc);
244  2897309 if (bigDegree.signum() > 0)
245  2897309 bigDegree = mpb.cuttingPlane(lits, bc, bigDegree);
246  2897309 if (bigDegree.signum() > 0)
247  2897309 bigDegree = mpb.saturation();
248  2897309 if (bigDegree.signum() <= 0)
249  0 return null;
250  2897309 return mpb;
251    }
252   
253    /**
254    * increase activity value of the constraint
255    *
256    * @see Constr#incActivity(double claInc)
257    */
 
258  0 toggle public void incActivity(double claInc) {
259  0 activity += claInc;
260    }
261   
262    /**
263    * compute the slack of the current constraint
264    * slack = poss - degree of the constraint
265    *
266    * @return la marge
267    */
 
268  213497 toggle public BigInteger slackConstraint() {
269  213497 return recalcLeftSide().subtract(this.degree);
270    }
271   
272    /**
273    * compute the slack of a described constraint
274    * slack = poss - degree of the constraint
275    *
276    * @param coefs
277    * coefficients of the constraint
278    * @param degree
279    * degree of the constraint
280    * @return slack of the constraint
281    */
 
282  335708 toggle public BigInteger slackConstraint(BigInteger[] coefs, BigInteger degree) {
283  335708 return recalcLeftSide(coefs).subtract(degree);
284    }
285   
286    /**
287    * compute the sum of the coefficients of the satisfied or non-assigned literals
288    * of a described constraint (usually called poss)
289    *
290    * @param coefs
291    * coefficients of the constraint
292    * @return poss
293    */
 
294  837641255 toggle public BigInteger recalcLeftSide(BigInteger[] coefs) {
295  837641255 BigInteger poss = BigInteger.ZERO;
296    // Pour chaque litteral
297  375624557 for (int i = 0; i < lits.length; i++)
298    if (!voc.isFalsified(lits[i])) {
299    assert coefs[i].signum() >= 0;
300    poss = poss.add(coefs[i]);
301    }
302  837641255 return poss;
303    }
304   
305    /**
306    * compute the sum of the coefficients of the satisfied or non-assigned literals
307    * of the current constraint (usually called poss)
308    *
309    * @return poss
310    */
 
311  837305547 toggle public BigInteger recalcLeftSide() {
312  837305547 return recalcLeftSide(this.coefs);
313    }
314   
315    /**
316    * D?termine si la contrainte est toujours satisfiable
317    *
318    * @return la contrainte est encore satisfiable
319    */
 
320  13297631 toggle protected boolean isSatisfiable() {
321  13297631 return recalcLeftSide().compareTo(degree) >= 0;
322    }
323   
324    /**
325    * is the constraint a learnt constrainte ?
326    *
327    * @return true si la contrainte est apprise, false sinon
328    * @see Constr#learnt()
329    */
 
330  186250858 toggle public boolean learnt() {
331  186250858 return learnt;
332    }
333   
334    /**
335    * The constraint is the reason of a unit propagation.
336    *
337    * @return true
338    * @see Constr#locked()
339    */
 
340  0 toggle public boolean locked() {
341  0 return true;
342    }
343   
344    /**
345    * Calcule le ppcm de deux nombres
346    *
347    * @param a
348    * premier nombre de l'op?ration
349    * @param b
350    * second nombre de l'op?ration
351    * @return le ppcm en question
352    */
 
353  0 toggle protected static BigInteger ppcm(BigInteger a, BigInteger b) {
354  0 return a.divide(a.gcd(b)).multiply(b);
355    }
356   
357    /**
358    * Permet le r??????chantillonage de l'activit??? de la contrainte
359    *
360    * @param d
361    * facteur d'ajustement
362    */
 
363  0 toggle public void rescaleBy(double d) {
364  0 activity *= d;
365    }
366   
 
367  2996433 toggle void selectionSort(int from, int to) {
368  2996433 int i, j, best_i;
369  2996433 BigInteger tmp;
370  2996433 int tmp2;
371   
372  19242230 for (i = from; i < to - 1; i++) {
373  16245797 best_i = i;
374  94259683 for (j = i + 1; j < to; j++) {
375  78013886 if (coefs[j].compareTo(coefs[best_i]) > 0)
376  1476764 best_i = j;
377    }
378  16245797 tmp = coefs[i];
379  16245797 coefs[i] = coefs[best_i];
380  16245797 coefs[best_i] = tmp;
381  16245797 tmp2 = lits[i];
382  16245797 lits[i] = lits[best_i];
383  16245797 lits[best_i] = tmp2;
384    }
385    }
386   
387    /**
388    * La contrainte est apprise
389    */
 
390  213301 toggle public void setLearnt() {
391  213301 learnt = true;
392    }
393   
394    /**
395    * Simplifie la contrainte(l'all???ge)
396    *
397    * @return true si la contrainte est satisfaite, false sinon
398    */
 
399  0 toggle public boolean simplify() {
400  0 BigInteger cumul = BigInteger.ZERO;
401   
402  0 int i = 0;
403  0 while (i < lits.length && cumul.compareTo(degree) < 0) {
404  0 if (voc.isSatisfied(lits[i])) {
405    // Mesure pessimiste
406  0 cumul = cumul.add(coefs[i]);
407    }
408  0 i++;
409    }
410   
411  0 return (cumul.compareTo(degree) >= 0);
412    }
413   
 
414  451382926 toggle public int size() {
415  451382926 return lits.length;
416    }
417   
418    /**
419    * sort coefficient and literal arrays
420    */
 
421  2423607 toggle final protected void sort() {
422  2423607 assert this.lits != null;
423  2423607 if (coefs.length > 0) {
424  2423607 this.sort(0, size());
425  2423607 BigInteger buffInt = coefs[0];
426  19242130 for (int i = 1; i < coefs.length; i++) {
427  16818523 assert buffInt.compareTo(coefs[i]) >= 0;
428  16818523 buffInt = coefs[i];
429    }
430   
431    }
432    }
433   
434    /**
435    * sort partially coefficient and literal arrays
436    *
437    * @param from
438    * index for the beginning of the sort
439    * @param to
440    * index for the end of the sort
441    */
 
442  3569259 toggle final protected void sort(int from, int to) {
443  3569259 int width = to - from;
444  3569259 if (to - from <= 15)
445  2996433 selectionSort(from, to);
446   
447    else {
448  572826 BigInteger pivot = coefs[rand.nextInt(width) + from];
449  572826 BigInteger tmp;
450  572826 int i = from - 1;
451  572826 int j = to;
452  572826 int tmp2;
453   
454  572826 for (;;) {
455  7656858 do
456  8627904 i++;
457  8627904 while (coefs[i].compareTo(pivot) > 0);
458  7656858 do
459  8686928 j--;
460  8686928 while (pivot.compareTo(coefs[j]) > 0);
461   
462  7656858 if (i >= j)
463  572826 break;
464   
465  7084032 tmp = coefs[i];
466  7084032 coefs[i] = coefs[j];
467  7084032 coefs[j] = tmp;
468  7084032 tmp2 = lits[i];
469  7084032 lits[i] = lits[j];
470  7084032 lits[j] = tmp2;
471    }
472   
473  572826 sort(from, i);
474  572826 sort(i, to);
475    }
476   
477    }
478   
 
479  0 toggle @Override
480    public String toString() {
481  0 StringBuffer stb = new StringBuffer();
482   
483  0 if (lits.length > 0) {
484  0 for (int i = 0; i < lits.length; i++) {
485    // if (voc.isUnassigned(lits[i])) {
486  0 stb.append(" + ");
487  0 stb.append(this.coefs[i]);
488  0 stb.append(".");
489  0 stb.append(Lits.toString(this.lits[i]));
490  0 stb.append("[");
491  0 stb.append(voc.valueToString(lits[i]));
492  0 stb.append("@");
493  0 stb.append(voc.getLevel(lits[i]));
494  0 stb.append("]");
495  0 stb.append(" ");
496    // }
497    }
498  0 stb.append(">= ");
499  0 stb.append(this.degree);
500    }
501  0 return stb.toString();
502    }
503   
 
504  213497 toggle public void assertConstraint(UnitPropagationListener s) {
505  213497 BigInteger tmp = slackConstraint();
506  6538313 for (int i = 0; i < lits.length; i++) {
507  6324816 if (voc.isUnassigned(lits[i]) && tmp.compareTo(coefs[i]) < 0) {
508  227404 boolean ret = s.enqueue(lits[i], this);
509  227404 assert ret;
510    }
511    }
512    }
513   
514    // protected abstract WatchPb watchPbNew(Lits voc, VecInt lits, VecInt
515    // coefs, boolean moreThan, int degree, int[] indexer);
516    /**
517    * @return Returns the degree.
518    */
 
519  1978815 toggle public BigInteger getDegree() {
520  1978815 return degree;
521    }
522   
 
523  213301 toggle public void register() {
524  213301 assert learnt;
525  213301 try {
526  213301 computeWatches();
527    } catch (ContradictionException e) {
528  0 System.out.println(this);
529    assert false;
530    }
531    }
532   
 
533  1005312 toggle public static IVec<BigInteger> toVecBigInt(IVecInt vec) {
534  1005312 IVec<BigInteger> bigVec = new Vec<BigInteger>(vec.size());
535  4092760 for (int i = 0; i < vec.size(); ++i)
536  3087448 bigVec.push(BigInteger.valueOf(vec.get(i)));
537  1005312 return bigVec;
538    }
539   
 
540  1005312 toggle public static BigInteger toBigInt(int i) {
541  1005312 return BigInteger.valueOf(i);
542    }
543   
 
544  9709 toggle public BigInteger[] getCoefs() {
545  9709 BigInteger[] coefsBis = new BigInteger[coefs.length];
546  9709 System.arraycopy(coefs, 0, coefsBis, 0, coefs.length);
547  9709 return coefsBis;
548    }
549   
 
550  0 toggle public int[] getLits() {
551  0 int[] litsBis = new int[lits.length];
552  0 System.arraycopy(lits, 0, litsBis, 0, lits.length);
553  0 return litsBis;
554    }
555   
 
556  232392 toggle public ILits getVocabulary() {
557  232392 return voc;
558    }
559   
560    /**
561    * compute an implied clause on the literals with the greater coefficients
562    */
 
563  0 toggle public IVecInt computeAnImpliedClause() {
564  0 BigInteger cptCoefs = BigInteger.ZERO;
565  0 int index = coefs.length;
566  0 while ((cptCoefs.compareTo(degree) > 0) && (index > 0)) {
567  0 cptCoefs = cptCoefs.add(coefs[--index]);
568    }
569  0 if (index > 0 && index < size() / 2) {
570    // System.out.println(this);
571    // System.out.println("index : "+index);
572  0 IVecInt literals = new VecInt(index);
573  0 for (int j = 0; j <= index; j++)
574  0 literals.push(lits[j]);
575  0 return literals;
576    }
577  0 return null;
578    }
579   
 
580  0 toggle public boolean coefficientsEqualToOne() {
581  0 return false;
582    }
583   
584    }
 
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.