Clover coverage report -
Coverage timestamp: dim. nov. 12 2006 12:21:31 CET
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 398   Methods: 15
NCLOC: 256   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
ConflictArray.java 97,7% 98,6% 100% 98,3%
coverage coverage
 1    /*
 2    * Created on Jan 17, 2005
 3    *
 4    * TODO To change the template for this generated file go to
 5    * Window - Preferences - Java - Code Style - Code Templates
 6    */
 7    package org.sat4j.minisat.constraints.pb;
 8   
 9    import java.math.BigInteger;
 10    import java.util.ArrayList;
 11    import java.util.List;
 12   
 13    import org.sat4j.minisat.core.ILits;
 14    import org.sat4j.minisat.core.VarActivityListener;
 15   
 16    /**
 17    * @author parrain TODO To change the template for this generated type comment
 18    * go to Window - Preferences - Java - Code Style - Code Templates
 19    */
 20    class ConflictArray extends ArrayPb implements IConflict {
 21   
 22  24794 public static IConflict createConflict(PBConstr cpb, int level) {
 23  24794 return new ConflictArray(cpb.getLits(), cpb.getCoefs(),
 24    cpb.getDegree(), cpb.getVocabulary(), level);
 25    }
 26   
 27  48014 ConflictArray(int[] lits, BigInteger[] coefs, BigInteger d, ILits voc,
 28    int level) {
 29  48014 super(lits, coefs, d, voc, level);
 30    }
 31   
 32    /*
 33    * coefficient to be computed.
 34    *
 35    */
 36    protected BigInteger coefMult = BigInteger.ZERO;
 37   
 38    protected BigInteger coefMultCons = BigInteger.ZERO;
 39   
 40    /**
 41    * Effectue une resolution avec une contrainte PB. Met a jour le Conflict.
 42    *
 43    * @param cpb
 44    * contrainte avec laquelle on va faire la resolution
 45    * @param litImplied
 46    * litteral devant etre resolu
 47    * @return la mise a jour du degre
 48    */
 49  642730 public BigInteger resolve(PBConstr cpb, int litImplied,
 50    VarActivityListener val) {
 51    assert litImplied > 1;
 52   
 53  642730 if (coefs[litImplied ^ 1] == null) {
 54    // logger.fine("pas de resolution");
 55  350952 return degree;
 56    }
 57   
 58    assert slackConflict().signum() <= 0;
 59    assert degree.signum() >= 0;
 60   
 61    // copie des coeffs de la contrainte pour pouvoir effectuer
 62    // des operations de reductions
 63  291778 BigInteger[] coefsCons = null;
 64  291778 BigInteger degreeCons = cpb.getDegree();
 65   
 66    // Recherche de l'indice du litteral implique
 67  291778 int ind = 0;
 68  291778 while (cpb.get(ind) != litImplied)
 69  569969 ind++;
 70   
 71    assert cpb.get(ind) == litImplied;
 72    assert cpb.getCoef(ind) != BigInteger.ZERO;
 73   
 74  291778 if (cpb.getCoef(ind).equals(BigInteger.ONE)) {
 75    // la rï¿œsolvante sera conflictuelle (Dixon)
 76  291172 coefMultCons = coefs[litImplied ^ 1];
 77  291172 coefMult = BigInteger.ONE;
 78    // mise-a-jour du degre du conflit
 79  291172 degreeCons = (degreeCons.multiply(coefMultCons));
 80    } else {
 81  606 if (coefs[litImplied ^ 1].equals(BigInteger.ONE)) {
 82    // la rï¿œsolvante sera conflictuelle (Dixon)
 83  173 coefMult = cpb.getCoef(ind);
 84  173 coefMultCons = BigInteger.ONE;
 85    // mise-a-jour du degre du conflit
 86  173 degree = degree.multiply(coefMult);
 87    } else {
 88    // Reduction de la contrainte
 89    // jusqu'a obtenir une resolvante conflictuelle
 90  433 WatchPb wpb = (WatchPb) cpb;
 91  433 coefsCons = wpb.getCoefs();
 92    assert positiveCoefs(coefsCons);
 93  433 degreeCons = reduceUntilConflict(litImplied, ind, coefsCons,
 94    wpb);
 95    // mise-a-jour du degre du conflit
 96  433 degreeCons = degreeCons.multiply(coefMultCons);
 97  433 degree = degree.multiply(coefMult);
 98    }
 99    // multiplication par coefMult des coefficients du conflit
 100  606 if (!coefMult.equals(BigInteger.ONE))
 101  178 for (int i = 2; i < coefs.length; i++) {
 102  499968 if (coefs[i] != null)
 103    // coefs[i] = coefs[i].multiply(coefMult);
 104  7449 setCoef(i, coefs[i].multiply(coefMult));
 105    }
 106    }
 107   
 108    // On effectue la resolution
 109  291778 degree = cuttingPlane(cpb, degreeCons, coefsCons, coefMultCons, val);
 110    assert coefs[litImplied] == null;
 111    assert coefs[litImplied ^ 1] == null;
 112    assert degree.signum() > 0;
 113   
 114    // Saturation
 115  291778 degree = saturation();
 116    assert slackConflict().signum() <= 0;
 117  291778 return degree;
 118    }
 119   
 120    /**
 121    * reduces the constraint defined by wpb until the result of the cutting
 122    * plane is a conflict. this reduction returns as much as poaaible a
 123    * constraint which is still a pseudo-boolean constraint.
 124    *
 125    * @param litImplied
 126    * @param ind
 127    * @param reducedCoefs
 128    * @param wpb
 129    * @return
 130    */
 131  433 protected BigInteger reduceUntilConflict(int litImplied, int ind,
 132    BigInteger[] reducedCoefs, WatchPb wpb) {
 133  433 BigInteger slackResolve = BigInteger.ONE.negate();
 134  433 BigInteger slackThis = BigInteger.ZERO;
 135  433 BigInteger slackIndex = BigInteger.ZERO;
 136  433 BigInteger ppcm;
 137  433 BigInteger reducedDegree = wpb.getDegree();
 138   
 139  433 do {
 140  10561 if (slackResolve.signum() >= 0) {
 141    assert slackThis.signum() > 0;
 142  10128 BigInteger tmp = reduceInConstraint(wpb, reducedCoefs, ind,
 143    reducedDegree);
 144    assert ((tmp.compareTo(reducedDegree) < 0) && (tmp
 145    .compareTo(BigInteger.ONE) >= 0));
 146  10128 reducedDegree = tmp;
 147    }
 148    // Recherche des coefficients multiplicateurs
 149    assert coefs[litImplied ^ 1].signum() > 0;
 150    assert reducedCoefs[ind].signum() > 0;
 151   
 152  10561 ppcm = ppcm(reducedCoefs[ind], coefs[litImplied ^ 1]);
 153    assert ppcm.signum() > 0;
 154  10561 coefMult = ppcm.divide(coefs[litImplied ^ 1]);
 155  10561 coefMultCons = ppcm.divide(reducedCoefs[ind]);
 156   
 157    assert coefMultCons.signum() > 0;
 158    assert coefMult.signum() > 0;
 159    assert coefMult.multiply(coefs[litImplied ^ 1]).equals(
 160    coefMultCons.multiply(reducedCoefs[ind]));
 161   
 162    // calcul des marges (poss) de chaque contrainte
 163  10561 slackThis = wpb.slackConstraint(reducedCoefs, reducedDegree)
 164    .multiply(coefMultCons);
 165  10561 slackIndex = slackConflict().multiply(coefMult);
 166   
 167    assert slackIndex.signum() <= 0;
 168   
 169    // calcul (approximation) de la marge de la resolvante
 170  10561 slackResolve = slackThis.add(slackIndex);
 171  10561 } while (slackResolve.signum() >= 0);
 172    assert coefMult.multiply(coefs[litImplied ^ 1]).equals(
 173    coefMultCons.multiply(reducedCoefs[ind]));
 174  433 return reducedDegree;
 175   
 176    }
 177   
 178  1284861 public BigInteger slackConflict() {
 179  1284861 BigInteger poss = BigInteger.ZERO;
 180    // Pour chaque litteral
 181  1284861 for (int i = 2; i < coefs.length; i++)
 182  819466180 if (coefs[i] != null && coefs[i].signum() != 0
 183    && !voc.isFalsified(i)) {
 184  9083466 poss = poss.add(coefs[i]);
 185    }
 186  1284861 return poss.subtract(degree);
 187    }
 188   
 189    /**
 190    * Calcule le ppcm de deux nombres
 191    *
 192    * @param a
 193    * premier nombre de l'op?ration
 194    * @param b
 195    * second nombre de l'op?ration
 196    * @return le ppcm en question
 197    */
 198  10561 protected static BigInteger ppcm(BigInteger a, BigInteger b) {
 199  10561 return a.divide(a.gcd(b)).multiply(b);
 200    }
 201   
 202    /**
 203    * Reduction d'une contrainte On supprime un litteral non assigne
 204    * prioritairement, vrai sinon. En aucun cas on ne supprime litImplied.
 205    *
 206    *
 207    * @return mise a jour du degre
 208    */
 209  10128 public BigInteger reduceInConstraint(WatchPb wpb,
 210    final BigInteger[] coefsBis, final int indLitImplied,
 211    final BigInteger degreeBis) {
 212    // logger.entering(this.getClass().getName(),"reduceInConstraint");
 213    assert degreeBis.compareTo(BigInteger.ONE) > 0;
 214    // Recherche d'un litt?ral non assign?
 215  10128 int lit = -1;
 216  10128 for (int ind = 0; (ind < wpb.size()) && (lit == -1); ind++)
 217  1240970 if (coefsBis[ind].signum() != 0 && voc.isUnassigned(wpb.get(ind))) {
 218    assert coefsBis[ind].compareTo(degreeBis) < 0;
 219  2148 lit = ind;
 220    }
 221   
 222    // Sinon, recherche d'un litteral satisfait
 223  10128 if (lit == -1)
 224  7980 for (int ind = 0; (ind < wpb.size()) && (lit == -1); ind++)
 225  624664 if ((coefsBis[ind].signum() != 0)
 226    && (voc.isSatisfied(wpb.get(ind)))
 227    && (ind != indLitImplied))
 228  7980 lit = ind;
 229   
 230    // on a trouve un litteral
 231    assert lit != -1;
 232   
 233    assert lit != indLitImplied;
 234    // logger.finer("Found literal "+Lits.toString(lits[lit]));
 235    // on reduit la contrainte
 236  10128 BigInteger degUpdate = degreeBis.subtract(coefsBis[lit]);
 237  10128 coefsBis[lit] = BigInteger.ZERO;
 238   
 239    // saturation de la contrainte
 240    assert degUpdate.signum() > 0;
 241  10128 BigInteger minimum = degUpdate;
 242  10128 for (int i = 0; i < coefsBis.length; i++) {
 243  1329014 if (coefsBis[i].signum() > 0)
 244  1067853 minimum = minimum.min(coefsBis[i]);
 245  1329014 coefsBis[i] = degUpdate.min(coefsBis[i]);
 246    }
 247  10128 if (minimum.equals(degUpdate) && !degUpdate.equals(BigInteger.ONE)) {
 248    // on a obtenu une clause
 249    // plus de reduction possible
 250  2 degUpdate = BigInteger.ONE;
 251  2 for (int i = 0; i < coefsBis.length; i++)
 252  255 if (coefsBis[i].signum() > 0)
 253  174 coefsBis[i] = degUpdate;
 254    }
 255   
 256    assert coefsBis[indLitImplied].signum() > 0;
 257    assert degreeBis.compareTo(degUpdate) > 0;
 258  10128 return degUpdate;
 259    }
 260   
 261  433 private boolean positiveCoefs(final BigInteger[] coefsCons) {
 262  433 for (int i = 0; i < coefsCons.length; i++) {
 263  27591 if (coefsCons[i].signum() <= 0)
 264  0 return false;
 265    }
 266  433 return true;
 267    }
 268   
 269  1362821 public boolean oldIsAssertive(int dl) {
 270  1362821 BigInteger slack = computeSlack(dl);
 271  1362821 slack = slack.subtract(degree);
 272  1362821 if (slack.signum() < 0)
 273  0 return false;
 274  1362821 for (int i = 2; i < coefs.length; i++) {
 275  1191200449 if (coefs[i] != null && (coefs[i].signum() > 0)
 276    && (voc.isUnassigned(i) || voc.getLevel(i) >= dl)
 277    && (slack.compareTo(coefs[i]) < 0))
 278  51678 return true;
 279    }
 280  1311143 return false;
 281    }
 282   
 283  2166801 private BigInteger computeSlack(int dl) {
 284  2166801 BigInteger slack = BigInteger.ZERO;
 285  2166801 for (int i = 2; i < coefs.length; i++) {
 286  1935778116 if (coefs[i] != null && (coefs[i].signum() > 0)
 287    && (((!voc.isFalsified(i)) || voc.getLevel(i) >= dl)))
 288  96359992 slack = slack.add(coefs[i]);
 289    }
 290  2166801 return slack;
 291    }
 292   
 293  13377 public void updateSlack(int dl) {
 294  13377 if (byLevel.containsKey(dl))
 295  6758 for (int lit : byLevel.get(dl)) {
 296  9958 if (voc.isFalsified(lit) && voc.getLevel(lit) == dl)
 297    // elle pourrait avoir ï¿œtï¿œ dï¿œsassignï¿œe
 298  9566 currentSlack = currentSlack.add(coefs[lit]);
 299    }
 300    }
 301   
 302  752121 public boolean isAssertive(int dl) {
 303    assert dl <= currentLevel;
 304   
 305  752121 currentLevel = dl;
 306    assert currentSlack.equals(computeSlack(dl));
 307  752121 BigInteger slack = currentSlack.subtract(degree);
 308  752121 if (slack.signum() < 0)
 309  32579 return false;
 310  719542 return isImplyingLiteral(dl, slack);
 311    }
 312   
 313  771401 private boolean isImplyingLiteral(int dl, BigInteger slack) {
 314    // on regarde les non assignï¿œs
 315  771401 if (byLevel.containsKey(-1)) {
 316  24573 for (int lit : byLevel.get(-1))
 317  73280 if (slack.compareTo(coefs[lit]) < 0)
 318  129 return true;
 319    }
 320    // on regarde tous les littï¿œraux de niveau >=dl
 321  771272 for (int level : byLevel.tailMap(dl).keySet()) {
 322  908162 for (int lit : byLevel.get(level))
 323  3694270 if (coefs[lit] != null && slack.compareTo(coefs[lit]) < 0)
 324  99826 return true;
 325    }
 326  671446 return false;
 327    }
 328   
 329    /**
 330    * retourne le niveau de backtrack : c'est-?-dire le niveau le plus haut
 331    * pour lequel la contrainte est assertive
 332    *
 333    * @param maxLevel
 334    * le plus bas niveau pour lequel la contrainte est assertive
 335    * @return the highest level (smaller int) for which the constraint is
 336    * assertive.
 337    */
 338  48000 public int getBacktrackLevel(int maxLevel) {
 339  48000 BigInteger slack = currentSlack.subtract(degree);
 340    // on cherche borneMax,
 341    // le niveau le plus haut dans l'arbre ou la contrainte est assertive
 342  48000 int borneMax = 0;
 343    // on va parcourir tous les niveaux infï¿œrieurs ï¿œ maxLevel
 344    // dans l'ordre dï¿œcroissant (ï¿œ partir de maxLevel)
 345    // jusqu'ï¿œ ce que le contrainte ne soit plus assertive
 346  48000 List<Integer> tmp = new ArrayList<Integer>(byLevel.headMap(maxLevel)
 347    .keySet());
 348  48000 int level;
 349  48000 for (int i = tmp.size() - 1; i >= 0; i--) {
 350  51927 level = tmp.get(i);
 351  51927 if (level <= 0) {
 352  68 borneMax = 0;
 353  68 break;
 354    }
 355    // calcul/correction de la nouvelle slack
 356  51859 for (Integer lit : byLevel.get(level)) {
 357  232708 if (voc.isFalsified(lit))
 358  227172 slack = slack.add(coefs[lit]);
 359    }
 360    assert computeSlack(level).subtract(degree).equals(slack);
 361  51859 if (!isImplyingLiteral(level, slack)) {
 362  47904 borneMax = level;
 363  47904 break;
 364    }
 365    }
 366    assert borneMax == oldGetBacktrackLevel(maxLevel);
 367  48000 return borneMax;
 368    }
 369   
 370  48000 public int oldGetBacktrackLevel(int maxLevel) {
 371  48000 int litLevel;
 372  48000 int borneMax = maxLevel;
 373    assert oldIsAssertive(borneMax);
 374  48000 int borneMin = -1;
 375  48000 for (int lit = 2; lit < coefs.length; lit++) {
 376  13831790 if (coefs[lit] != null) {
 377  1369853 litLevel = voc.getLevel(lit);
 378  1369853 if (litLevel < borneMax && litLevel > borneMin && oldIsAssertive(litLevel))
 379  3678 borneMax = litLevel;
 380    // else
 381    // borneMin = litLevel;
 382    }
 383    }
 384    // on retourne le niveau immediatement inferieur ? borneMax
 385    // pour lequel la contrainte possede un literal
 386  48000 int retour = 0;
 387  48000 for (int lit = 2; lit < coefs.length; lit++) {
 388  13831790 if (coefs[lit] != null) {
 389  1369853 litLevel = voc.getLevel(lit);
 390  1369853 if (litLevel > retour && litLevel < borneMax) {
 391  106732 retour = litLevel;
 392    }
 393    }
 394    }
 395  48000 return retour;
 396    }
 397   
 398    }
 
CloverReport generated by Clover Code Coverage v1.3.9
dim. nov. 12 2006 12:21:42 CET.		   Open Source License registered to the OpenSAT Project. This license of Clover is provided to support the development of OpenSAT only.