Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
247   665   98   9,15
210   427   0,5   27
27     4,59  
1    
 
  ConflictMap       Line # 40 247 98 84,9% 0.84917355
 
  (135)
 
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    package org.sat4j.minisat.constraints.pb;
26   
27    import java.math.BigInteger;
28    import java.util.HashMap;
29    import java.util.Map;
30   
31    import org.sat4j.core.VecInt;
32    import org.sat4j.minisat.constraints.cnf.Lits;
33    import org.sat4j.minisat.core.ILits;
34    import org.sat4j.minisat.core.VarActivityListener;
35   
36    /**
37    * @author parrain TODO To change the template for this generated type comment
38    * go to Window - Preferences - Java - Code Style - Code Templates
39    */
 
40    public class ConflictMap extends MapPb implements IConflict {
41   
42    private final ILits voc;
43   
44    /**
45    * to store the slack of the current resolvant
46    */
47    protected BigInteger currentSlack;
48   
49    protected int currentLevel;
50   
51    /**
52    * allows to access directly to all variables belonging to a particular
53    * level At index 0, unassigned literals are stored (usually level -1); so
54    * there is always a step between index and levels.
55    */
56    protected VecInt[] byLevel;
57   
58    /**
59    * constructs the data structure needed to perform cutting planes
60    *
61    * @param cpb
62    * pseudo-boolean constraint which rosed the conflict
63    * @param level
64    * current decision level
65    * @return a conflict on which cutting plane can be performed.
66    */
 
67  1079520 toggle public static IConflict createConflict(PBConstr cpb, int level) {
68  1079520 Map<Integer, BigInteger> m = new HashMap<Integer, BigInteger>();
69  1079520 int lit;
70  1079520 BigInteger coefLit;
71  13147107 for (int i = 0; i < cpb.size(); i++) {
72  12067587 lit = cpb.get(i);
73  12067587 coefLit = cpb.getCoef(i);
74  12067587 assert cpb.get(i) != 0;
75  12067587 assert cpb.getCoef(i).signum() > 0;
76  12067587 m.put(lit, coefLit);
77    }
78  1079520 return new ConflictMap(m, cpb.getDegree(), cpb.getVocabulary(), level);
79    }
80   
 
81  1281751 toggle ConflictMap(Map<Integer, BigInteger> m, BigInteger d, ILits voc, int level) {
82  1281751 super(m, d);
83  1281751 this.voc = voc;
84  1281751 this.currentLevel = level;
85  1281751 initStructures();
86    }
87   
 
88  1281751 toggle private void initStructures() {
89  1281751 currentSlack = BigInteger.ZERO;
90  1281751 byLevel = new VecInt[levelToIndex(currentLevel) + 1];
91  1281751 int ilit, litLevel, index;
92  1281751 BigInteger tmp;
93  1281751 for (Integer lit : coefs.keySet()) {
94  16108441 ilit = lit.intValue();
95  16108441 litLevel = voc.getLevel(ilit);
96    // eventually add to slack
97  16108441 tmp = coefs.get(lit);
98  16108441 if ((tmp.signum() > 0)
99    && (((!voc.isFalsified(ilit)) || litLevel == currentLevel)))
100  3918918 currentSlack = currentSlack.add(tmp);
101    // add to byLevel structure
102  16108441 index = levelToIndex(litLevel);
103  16108441 if (byLevel[index] == null) {
104  8072282 byLevel[index] = new VecInt();
105    }
106  16108441 byLevel[index].push(ilit);
107    }
108    }
109   
110    /**
111    * convert level into an index in the byLevel structure
112    *
113    * @param level
114    * @return
115    */
 
116  213683203 toggle private static final int levelToIndex(int level) {
117  213683203 return level + 1;
118    }
119   
120    /**
121    * convert index in the byLevel structure into a level
122    *
123    * @param indLevel
124    * @return
125    */
 
126  54934187 toggle private static final int indexToLevel(int indLevel) {
127  54934187 return indLevel - 1;
128    }
129   
130    /*
131    * coefficient to be computed.
132    *
133    */
134    protected BigInteger coefMult = BigInteger.ZERO;
135   
136    protected BigInteger coefMultCons = BigInteger.ZERO;
137   
138    /**
139    * computes a cutting plane with a pseudo-boolean constraint. this method
140    * updates the current instance (of ConflictMap).
141    *
142    * @param cpb
143    * constraint to compute with the cutting plane
144    * @param litImplied
145    * literal that must be resolved by the cutting plane
146    * @return an update of the degree of the current instance
147    */
 
148  19266524 toggle public BigInteger resolve(PBConstr cpb, int litImplied,
149    VarActivityListener val) {
150  19266524 assert litImplied > 1;
151  19266524 int nLitImplied = litImplied ^ 1;
152  19266524 if (cpb == null || !coefs.containsKey(nLitImplied)) {
153    // no resolution
154    // undo operation should be anticipated
155  9303722 int litLevel = levelToIndex(voc.getLevel(litImplied));
156  9303722 int lit = 0;
157  9303722 if (byLevel[litLevel] != null) {
158  9155673 if (byLevel[litLevel].contains(litImplied)) {
159  34221 lit = litImplied;
160  34221 assert coefs.containsKey(litImplied);
161  9121452 } else if (byLevel[litLevel].contains(nLitImplied)) {
162  52 lit = nLitImplied;
163  52 assert coefs.containsKey(nLitImplied);
164    }
165    }
166   
167  9303722 if (lit > 0) {
168  34273 byLevel[litLevel].remove(lit);
169  34273 if (byLevel[0] == null)
170  3822 byLevel[0] = new VecInt();
171  34273 byLevel[0].push(lit);
172    }
173  9303722 return degree;
174    }
175   
176  9962802 assert slackConflict().signum() <= 0;
177  9962802 assert degree.signum() >= 0;
178   
179    // coefficients of the constraint must be copied in an other structure
180    // in order to make reduction operations.
181  9962802 BigInteger[] coefsCons = null;
182  9962802 BigInteger degreeCons = cpb.getDegree();
183   
184    // search of the index of the implied literal
185  9962802 int ind = 0;
186  29674906 while (cpb.get(ind) != litImplied)
187  19712104 ind++;
188   
189  9962802 assert cpb.get(ind) == litImplied;
190  9962802 assert cpb.getCoef(ind) != BigInteger.ZERO;
191   
192  9962802 if (cpb.getCoef(ind).equals(BigInteger.ONE)) {
193    // then we know that the resolvant will still be a conflict (cf.
194    // Dixon's property)
195  9950836 coefMultCons = coefs.get(nLitImplied);
196  9950836 coefMult = BigInteger.ONE;
197    // updating of the degree of the conflict
198  9950836 degreeCons = degreeCons.multiply(coefMultCons);
199    } else {
200  11966 if (coefs.get(nLitImplied).equals(BigInteger.ONE)) {
201    // then we know that the resolvant will still be a conflict (cf.
202    // Dixon's property)
203  2257 coefMult = cpb.getCoef(ind);
204  2257 coefMultCons = BigInteger.ONE;
205    // updating of the degree of the conflict
206  2257 degree = degree.multiply(coefMult);
207    } else {
208    // pb-constraint has to be reduced
209    // to obtain a conflictual result from the cutting plane
210  9709 WatchPb wpb = (WatchPb) cpb;
211  9709 coefsCons = wpb.getCoefs();
212  9709 assert positiveCoefs(coefsCons);
213  9709 degreeCons = reduceUntilConflict(litImplied, ind, coefsCons,
214    wpb);
215    // updating of the degree of the conflict
216  9709 degreeCons = degreeCons.multiply(coefMultCons);
217  9709 degree = degree.multiply(coefMult);
218    }
219   
220    // coefficients of the conflict must be multiplied by coefMult
221  11966 if (!coefMult.equals(BigInteger.ONE))
222  3181 for (Integer i : coefs.keySet()) {
223  297640 setCoef(i, coefs.get(i).multiply(coefMult));
224    }
225    }
226   
227  9962802 assert slackConflict().signum() <= 0;
228   
229    // cutting plane
230  9962802 degree = cuttingPlane(cpb, degreeCons, coefsCons, coefMultCons, val);
231   
232    // neither litImplied nor nLitImplied is present in coefs structure
233  9962802 assert !coefs.containsKey(litImplied);
234  9962802 assert !coefs.containsKey(nLitImplied);
235    // neither litImplied nor nLitImplied is present in byLevel structure
236  9962802 assert getLevelByLevel(litImplied) == -1;
237  9962802 assert getLevelByLevel(nLitImplied) == -1;
238  9962802 assert degree.signum() > 0;
239  9962802 assert slackConflict().signum() <= 0;
240   
241    // saturation
242  9962802 degree = saturation();
243  9962802 assert slackConflict().signum() <= 0;
244   
245  9962802 return degree;
246    }
247   
 
248  9359 toggle protected BigInteger reduceUntilConflict(int litImplied, int ind,
249    BigInteger[] reducedCoefs, WatchPb wpb) {
250  9359 BigInteger slackResolve = BigInteger.ONE.negate();
251  9359 BigInteger slackThis = BigInteger.ZERO;
252  9359 BigInteger slackIndex = BigInteger.ZERO;
253  9359 BigInteger slackConflict = slackConflict();
254  9359 BigInteger ppcm;
255  9359 BigInteger reducedDegree = wpb.getDegree();
256  9359 BigInteger previousCoefLitImplied = BigInteger.ZERO;
257  9359 BigInteger tmp;
258  9359 BigInteger coefLitImplied = coefs.get(litImplied ^ 1);
259   
260  9359 do {
261  335708 if (slackResolve.signum() >= 0) {
262  326349 assert slackThis.signum() > 0;
263  326349 tmp = reduceInConstraint(wpb, reducedCoefs, ind,
264    reducedDegree);
265  326349 assert ((tmp.compareTo(reducedDegree) < 0) && (tmp.compareTo(BigInteger.ONE) >= 0));
266  326349 reducedDegree = tmp;
267    }
268    // search of the multiplying coefficients
269  335708 assert coefs.get(litImplied ^ 1).signum() > 0;
270  335708 assert reducedCoefs[ind].signum() > 0;
271   
272  335708 if (!reducedCoefs[ind].equals(previousCoefLitImplied)) {
273  89521 assert coefLitImplied.equals(coefs.get(litImplied ^ 1));
274  89521 ppcm = ppcm(reducedCoefs[ind], coefLitImplied);
275  89521 assert ppcm.signum() > 0;
276  89521 coefMult = ppcm.divide(coefLitImplied);
277  89521 coefMultCons = ppcm.divide(reducedCoefs[ind]);
278   
279  89521 assert coefMultCons.signum() > 0;
280  89521 assert coefMult.signum() > 0;
281  89521 assert coefMult.multiply(coefLitImplied).equals(
282    coefMultCons.multiply(reducedCoefs[ind]));
283  89521 previousCoefLitImplied = reducedCoefs[ind];
284    }
285   
286    // slacks computed for each constraint
287  335708 slackThis = wpb.slackConstraint(reducedCoefs, reducedDegree)
288    .multiply(coefMultCons);
289  335708 assert slackConflict.equals(slackConflict());
290  335708 slackIndex = slackConflict.multiply(coefMult);
291  335708 assert slackIndex.signum() <= 0;
292    // estimate of the slack after the cutting plane
293  335708 slackResolve = slackThis.add(slackIndex);
294  335708 } while (slackResolve.signum() >= 0);
295  9359 assert coefMult.multiply(coefs.get(litImplied ^ 1)).equals(
296    coefMultCons.multiply(reducedCoefs[ind]));
297  9359 return reducedDegree;
298   
299    }
300   
301    /**
302    * computes the slack of the current instance
303    */
 
304  60744550 toggle public BigInteger slackConflict() {
305  60744550 BigInteger poss = BigInteger.ZERO;
306  60744550 BigInteger tmp;
307    // for each literal
308  60744550 for (Integer i : coefs.keySet()) {
309  1873915020 tmp = coefs.get(i);
310  1873915020 if (tmp.signum() != 0 && !voc.isFalsified(i))
311  142288849 poss = poss.add(tmp);
312    }
313  60744550 return poss.subtract(degree);
314    }
315   
 
316  38442729 toggle public boolean oldIsAssertive(int dl) {
317  38442729 BigInteger tmp;
318  38442729 BigInteger slack = computeSlack(dl).subtract(degree);
319  38442729 if (slack.signum() < 0)
320  0 return false;
321  38442729 for (Integer i : coefs.keySet()) {
322  1975736624 tmp = coefs.get(i);
323  1975736624 if ((tmp.signum() > 0)
324    && (voc.isUnassigned(i) || voc.getLevel(i) >= dl)
325    && (slack.compareTo(tmp) < 0))
326  1291299 return true;
327    }
328  37151430 return false;
329    }
330   
331    // computes a slack with respect to a particular decision level
 
332  77421976 toggle private BigInteger computeSlack(int dl) {
333  77421976 BigInteger slack = BigInteger.ZERO;
334  77421976 BigInteger tmp;
335  77421976 for (Integer i : coefs.keySet()) {
336    tmp = coefs.get(i);
337    if ((tmp.signum() > 0)
338    && (((!voc.isFalsified(i)) || voc.getLevel(i) >= dl)))
339  2113168391 slack = slack.add(tmp);
340    }
341  77421976 return slack;
342    }
343   
344    /**
345    * tests if the conflict is assertive (allows to imply a literal) at a
346    * particular decision level
347    *
348    * @param dl
349    * the decision level
350    * @return true if the conflict is assertive at the decision level
351    */
 
352  21829774 toggle public boolean isAssertive(int dl) {
353  21829774 assert dl <= currentLevel;
354  21829774 assert dl <= currentLevel;
355   
356  21829774 currentLevel = dl;
357    // assert currentSlack.equals(computeSlack(dl));
358  21829774 BigInteger slack = currentSlack.subtract(degree);
359  21829774 if (slack.signum() < 0)
360  298904 return false;
361  21530870 return isImplyingLiteral(slack);
362    }
363   
364    // given the slack already computed, tests if a literal could be implied at
365    // a particular level
366    // uses the byLevel data structure to parse each literal by decision level
 
367  21530870 toggle private boolean isImplyingLiteral(BigInteger slack) {
368    // unassigned literals are tried first
369  21530870 int unassigned = levelToIndex(-1);
370  21530870 if (byLevel[unassigned] != null) {
371  387091 for (Integer lit : byLevel[unassigned])
372  2452721 if (slack.compareTo(coefs.get(lit)) < 0)
373  1796 return true;
374    }
375    // then we have to look at every literal at a decision level >=dl
376  21529074 BigInteger tmp;
377  21529074 int level = levelToIndex(currentLevel);
378  21529074 if (byLevel[level] != null)
379  21529074 for (Integer lit : byLevel[level]) {
380  85030925 tmp = coefs.get(lit);
381  85030925 if (tmp != null && slack.compareTo(tmp) < 0)
382  2561454 return true;
383    }
384  18967620 return false;
385    }
386   
387    // given the slack already computed, tests if a literal could be implied at
388    // a particular level
389    // uses the coefs data structure (where coefficients are decreasing ordered) to parse each literal
 
390  18431224 toggle private boolean isImplyingLiteralOrdered(int dl, BigInteger slack) {
391  18431224 int ilit, litLevel;
392  18431224 for (Integer lit : coefs.keySet()) {
393  939336977 ilit = lit.intValue();
394  939336977 litLevel = voc.getLevel(ilit);
395    // if (slack.compareTo(coefs.get(lit)) >= 0)
396    // return false;
397    // else if (litLevel >= dl || voc.isUnassigned(ilit))
398    // return true;
399  939336977 if ((litLevel >= dl || voc.isUnassigned(ilit)) && (slack.compareTo(coefs.get(lit)) < 0))
400  4109 return true;
401    }
402  18427115 return false;
403    }
404   
405    /**
406    * computes the least common factor of two integers (Plus Petit Commun
407    * Multiple in french)
408    *
409    * @param a
410    * first integer
411    * @param b
412    * second integer
413    * @return the least common factor
414    */
 
415  89521 toggle protected static BigInteger ppcm(BigInteger a, BigInteger b) {
416  89521 return a.divide(a.gcd(b)).multiply(b);
417    }
418   
419    /**
420    * constraint reduction : removes a literal of the constraint. The literal
421    * should be either unassigned or satisfied. The literal can not be the
422    * literal that should be resolved.
423    *
424    * @param wpb
425    * the initial constraint to reduce
426    * @param coefsBis
427    * the coefficients of the constraint wrt which the reduction
428    * will be proposed
429    * @param indLitImplied
430    * index in wpb of the literal that should be resolved
431    * @param degreeBis
432    * the degree of the constraint wrt which the reduction will be
433    * proposed
434    * @return new degree of the reduced constraint
435    */
 
436  326349 toggle public BigInteger reduceInConstraint(WatchPb wpb,
437    final BigInteger[] coefsBis, final int indLitImplied,
438    final BigInteger degreeBis) {
439    // logger.entering(this.getClass().getName(),"reduceInConstraint");
440  326349 assert degreeBis.compareTo(BigInteger.ONE) > 0;
441    // search of an unassigned literal
442  326349 int lit = -1;
443  58665949 for (int ind = 0; (ind < wpb.lits.length) && (lit == -1); ind++)
444  58339600 if (coefsBis[ind].signum() != 0 && voc.isUnassigned(wpb.lits[ind])) {
445  56347 assert coefsBis[ind].compareTo(degreeBis) < 0;
446  56347 lit = ind;
447    }
448   
449    // else, search of a satisfied literal
450  326349 if (lit == -1)
451  33313408 for (int ind = 0; (ind < wpb.lits.length) && (lit == -1); ind++)
452  33043406 if ((coefsBis[ind].signum() != 0)
453    && (voc.isSatisfied(wpb.lits[ind]))
454    && (ind != indLitImplied))
455  270002 lit = ind;
456   
457    // a literal has been found
458  326349 assert lit != -1;
459   
460  326349 assert lit != indLitImplied;
461    // logger.finer("Found literal "+Lits.toString(lits[lit]));
462    // reduction can be done
463  326349 BigInteger degUpdate = degreeBis.subtract(coefsBis[lit]);
464  326349 coefsBis[lit] = BigInteger.ZERO;
465   
466    // saturation of the constraint
467  326349 degUpdate = saturation(coefsBis, degUpdate);
468   
469  326349 assert coefsBis[indLitImplied].signum() > 0;
470  326349 assert degreeBis.compareTo(degUpdate) > 0;
471  326349 return degUpdate;
472    }
473   
 
474  326349 toggle static BigInteger saturation(BigInteger[] coefs, BigInteger degree) {
475  326349 assert degree.signum() > 0;
476  326349 BigInteger minimum = degree;
477  61067583 for (int i = 0; i < coefs.length; i++) {
478  60741234 if (coefs[i].signum() > 0)
479  51858570 minimum = minimum.min(coefs[i]);
480  60741234 coefs[i] = degree.min(coefs[i]);
481    }
482  326349 if (minimum.equals(degree) && !degree.equals(BigInteger.ONE)) {
483    // the result is a clause
484    // there is no more possible reduction
485  762 degree = BigInteger.ONE;
486  175483 for (int i = 0; i < coefs.length; i++)
487  174721 if (coefs[i].signum() > 0)
488  137518 coefs[i] = degree;
489    }
490  326349 return degree;
491    }
492   
 
493  9709 toggle private boolean positiveCoefs(final BigInteger[] coefsCons) {
494  1304388 for (int i = 0; i < coefsCons.length; i++) {
495  1294679 if (coefsCons[i].signum() <= 0)
496  0 return false;
497    }
498  9709 return true;
499    }
500   
501    /**
502    * computes the level for the backtrack : the highest decision level for
503    * which the conflict is assertive.
504    *
505    * @param maxLevel
506    * the lowest level for which the conflict is assertive
507    * @return the highest level (smaller int) for which the constraint is
508    * assertive.
509    */
 
510  1281625 toggle public int getBacktrackLevel(int maxLevel) {
511    // we are looking for a level higher than maxLevel
512    // where the constraint is still assertive
513  1281625 VecInt lits;
514  1281625 int level;
515  1281625 int indStop = levelToIndex(maxLevel) - 1;
516  1281625 int indStart = levelToIndex(0);
517  1281625 BigInteger slack = computeSlack(0).subtract(degree);
518  1281625 int previous = 0;
519  34196755 for (int indLevel = indStart; indLevel <= indStop; indLevel++) {
520  32919239 if (byLevel[indLevel] != null) {
521  18431224 level = indexToLevel(indLevel);
522  18431224 assert computeSlack(level).subtract(degree).equals(slack);
523  18431224 if (isImplyingLiteralOrdered(level, slack)) {
524    //if (isImplyingLiteral(level, slack)) {
525  4109 break;
526    }
527    // updating the new slack
528  18427115 lits = byLevel[indLevel];
529  18427115 for (Integer lit : lits) {
530  37151428 if (voc.isFalsified(lit)
531    && voc.getLevel(lit) == indexToLevel(indLevel))
532  36502963 slack = slack.subtract(coefs.get(lit));
533    }
534  18427115 if (!lits.isEmpty())
535  18422412 previous = level;
536    }
537    }
538  1281625 assert previous == oldGetBacktrackLevel(maxLevel);
539    // assert previous == retour;
540  1281625 return previous;
541    }
542   
 
543  1281625 toggle public int oldGetBacktrackLevel(int maxLevel) {
544  1281625 int litLevel;
545  1281625 int borneMax = maxLevel;
546  1281625 assert oldIsAssertive(borneMax);
547  1281625 int borneMin = -1;
548    // on calcule borneMax,
549    // le niveau le plus haut dans l'arbre ou la contrainte est assertive
550  1281625 for (int lit : coefs.keySet()) {
551  38539982 litLevel = voc.getLevel(lit);
552  38539982 if (litLevel < borneMax && litLevel > borneMin
553    && oldIsAssertive(litLevel))
554  9674 borneMax = litLevel;
555    }
556    // on retourne le niveau immediatement inferieur ? borneMax
557    // pour lequel la contrainte possede un literal
558  1281625 int retour = 0;
559  1281625 for (int lit : coefs.keySet()) {
560  38539982 litLevel = voc.getLevel(lit);
561  38539982 if (litLevel > retour && litLevel < borneMax) {
562  3721209 retour = litLevel;
563    }
564    }
565  1281625 return retour;
566    }
567   
 
568  121471 toggle public void updateSlack(int level) {
569  121471 int dl = levelToIndex(level);
570  121471 if (byLevel[dl] != null)
571  61139 for (int lit : byLevel[dl]) {
572  90698 if (voc.isFalsified(lit))
573  86904 currentSlack = currentSlack.add(coefs.get(lit));
574    }
575    }
576   
 
577  49412296 toggle @Override
578    void increaseCoef(Integer lit, BigInteger incCoef) {
579  49412296 int ilit = lit.intValue();
580  49412296 if ((!voc.isFalsified(ilit)) || voc.getLevel(ilit) == currentLevel) {
581  8509050 currentSlack = currentSlack.add(incCoef);
582    }
583  49412296 assert byLevel[levelToIndex(voc.getLevel(ilit))].contains(ilit);
584  49412296 super.increaseCoef(lit, incCoef);
585    }
586   
 
587  24728 toggle @Override
588    void decreaseCoef(Integer lit, BigInteger decCoef) {
589  24728 int ilit = lit.intValue();
590  24728 if ((!voc.isFalsified(ilit)) || voc.getLevel(ilit) == currentLevel) {
591  8540 currentSlack = currentSlack.subtract(decCoef);
592    }
593  24728 assert byLevel[levelToIndex(voc.getLevel(ilit))].contains(ilit);
594  24728 super.decreaseCoef(lit, decCoef);
595    }
596   
 
597  81531649 toggle @Override
598    void setCoef(Integer lit, BigInteger newValue) {
599  81531649 int ilit = lit.intValue();
600  81531649 int litLevel = voc.getLevel(ilit);
601  81531649 if ((!voc.isFalsified(ilit)) || litLevel == currentLevel) {
602  16752052 if (coefs.containsKey(lit))
603  8479812 currentSlack = currentSlack.subtract(coefs.get(lit));
604  16752052 currentSlack = currentSlack.add(newValue);
605    }
606  81531649 int indLitLevel = levelToIndex(litLevel);
607  81531649 if (!coefs.containsKey(lit)) {
608  32707492 if (byLevel[indLitLevel] == null) {
609  11735418 byLevel[indLitLevel] = new VecInt();
610    }
611  32707492 byLevel[indLitLevel].push(ilit);
612   
613    }
614  81531649 assert byLevel[indLitLevel] != null;
615  81531649 assert byLevel[indLitLevel].contains(ilit);
616  81531649 super.setCoef(lit, newValue);
617    }
618   
 
619  10275951 toggle @Override
620    void removeCoef(Integer lit) {
621  10275951 int ilit = lit.intValue();
622  10275951 int litLevel = voc.getLevel(ilit);
623  10275951 if ((!voc.isFalsified(ilit)) || litLevel == currentLevel) {
624  10241071 currentSlack = currentSlack.subtract(coefs.get(lit));
625    }
626   
627  10275951 int indLitLevel = levelToIndex(litLevel);
628  10275951 assert indLitLevel < byLevel.length;
629  10275951 assert byLevel[indLitLevel] != null;
630  10275951 assert byLevel[indLitLevel].contains(ilit);
631  10275951 byLevel[indLitLevel].remove(lit);
632  10275951 super.removeCoef(lit);
633    }
634   
 
635  19925604 toggle private int getLevelByLevel(int lit) {
636  582251000 for (int i = 0; i < byLevel.length; i++)
637  562325396 if (byLevel[i] != null && byLevel[i].contains(lit))
638  0 return i;
639  19925604 return -1;
640    }
641   
 
642  19266398 toggle public boolean slackIsCorrect(int dl) {
643  19266398 return currentSlack.equals(computeSlack(dl));
644    }
645   
 
646  0 toggle @Override
647    public String toString() {
648  0 int lit;
649  0 StringBuilder stb = new StringBuilder();
650  0 for (Map.Entry<Integer, BigInteger> entry : coefs.entrySet()) {
651  0 lit = Integer.valueOf(entry.getKey());
652  0 stb.append(entry.getValue());
653  0 stb.append(".");
654  0 stb.append(Lits.toString(lit));
655  0 stb.append(" ");
656  0 stb.append("[");
657  0 stb.append(voc.valueToString(lit));
658  0 stb.append("@");
659  0 stb.append(voc.getLevel(lit));
660  0 stb.append("]");
661    }
662  0 return stb.toString() + " >= " + degree; //$NON-NLS-1$
663    }
664   
665    }
 
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.