Clover coverage report -
Coverage timestamp: dim. nov. 12 2006 12:21:31 CET
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 425   Methods: 18
NCLOC: 292   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
ConflictMapIncrementEtParcours.java 97,1% 98,8% 100% 98,4%
coverage coverage
 1    package org.sat4j.minisat.constraints.pb;
 2   
 3    /*
 4    * Created on Jan 17, 2005
 5    *
 6    * TODO To change the template for this generated file go to
 7    * Window - Preferences - Java - Code Style - Code Templates
 8    */
 9   
 10    import java.math.BigInteger;
 11    import java.util.HashMap;
 12    import java.util.Map;
 13   
 14    import org.sat4j.minisat.core.ILits;
 15    import org.sat4j.minisat.core.VarActivityListener;
 16   
 17    /**
 18    * @author parrain TODO To change the template for this generated type comment
 19    * go to Window - Preferences - Java - Code Style - Code Templates
 20    */
 21    public class ConflictMapIncrementEtParcours extends MapPb implements IConflict {
 22   
 23    private final ILits voc;
 24   
 25    protected BigInteger currentSlack;
 26   
 27    protected int currentLevel;
 28   
 29  56660 public static IConflict createConflict(PBConstr cpb, int level) {
 30  56660 Map<Integer, BigInteger> m = new HashMap<Integer, BigInteger>();
 31  56660 int lit;
 32  56660 BigInteger coefLit;
 33  56660 for (int i = 0; i < cpb.size(); i++) {
 34  1111628 lit = cpb.get(i);
 35  1111628 coefLit = cpb.getCoef(i);
 36    assert cpb.get(i) != 0;
 37    assert cpb.getCoef(i).signum() > 0;
 38  1111628 m.put(lit, coefLit);
 39    }
 40  56660 return new ConflictMapIncrementEtParcours(m, cpb.getDegree(), cpb
 41    .getVocabulary(), level);
 42    }
 43   
 44  56660 ConflictMapIncrementEtParcours(Map<Integer, BigInteger> m, BigInteger d,
 45    ILits voc, int level) {
 46  56660 super(m, d);
 47  56660 this.voc = voc;
 48  56660 this.currentLevel = level;
 49  56660 initCurrentSlack();
 50    }
 51   
 52  56660 private void initCurrentSlack() {
 53  56660 currentSlack = BigInteger.ZERO;
 54  56660 int ilit;
 55  56660 BigInteger tmp;
 56  56660 for (Integer lit : coefs.keySet()) {
 57  1111628 ilit = lit.intValue();
 58  1111628 tmp = coefs.get(lit);
 59  1111628 if ((tmp.signum() > 0)
 60    && (((!voc.isFalsified(ilit)) || voc.getLevel(ilit) == currentLevel)))
 61  207867 currentSlack = currentSlack.add(tmp);
 62    }
 63    }
 64   
 65    /*
 66    * coefficient to be computed.
 67    *
 68    */
 69    private BigInteger coefMult = BigInteger.ZERO;
 70   
 71    private BigInteger coefMultCons = BigInteger.ZERO;
 72   
 73    /**
 74    * Effectue une resolution avec une contrainte PB. Met a jour le Conflict.
 75    *
 76    * @param cpb
 77    * contrainte avec laquelle on va faire la resolution
 78    * @param litImplied
 79    * litteral devant etre resolu
 80    * @return la mise a jour du degre
 81    */
 82  772454 public BigInteger resolve(PBConstr cpb, int litImplied,
 83    VarActivityListener val) {
 84    assert litImplied > 1;
 85  772454 if (!coefs.containsKey(litImplied ^ 1)) {
 86    // logger.fine("pas de resolution");
 87  417373 return degree;
 88    }
 89   
 90    assert slackConflict().signum() <= 0;
 91    assert degree.signum() >= 0;
 92   
 93    // copie des coeffs de la contrainte pour pouvoir effectuer
 94    // des operations de reductions
 95  355081 BigInteger[] coefsCons = null;
 96  355081 BigInteger degreeCons = cpb.getDegree();
 97   
 98    // Recherche de l'indice du litteral implique
 99  355081 int ind = 0;
 100  355081 while (cpb.get(ind) != litImplied)
 101  656043 ind++;
 102   
 103    assert cpb.get(ind) == litImplied;
 104    assert cpb.getCoef(ind) != BigInteger.ZERO;
 105   
 106  355081 if (cpb.getCoef(ind).equals(BigInteger.ONE)) {
 107    // la r???solvante sera conflictuelle (Dixon)
 108  354195 coefMultCons = coefs.get(litImplied ^ 1);
 109  354195 coefMult = BigInteger.ONE;
 110    // mise-a-jour du degre du conflit
 111  354195 degreeCons = (degreeCons.multiply(coefMultCons));
 112    } else {
 113  886 if (coefs.get(litImplied ^ 1).equals(BigInteger.ONE)) {
 114    // la r???solvante sera conflictuelle (Dixon)
 115  185 coefMult = cpb.getCoef(ind);
 116  185 coefMultCons = BigInteger.ONE;
 117    // mise-a-jour du degre du conflit
 118  185 degree = degree.multiply(coefMult);
 119    } else {
 120    // Reduction de la contrainte
 121    // jusqu'a obtenir une resolvante conflictuelle
 122  701 WatchPb wpb = (WatchPb) cpb;
 123  701 coefsCons = wpb.getCoefs();
 124    assert positiveCoefs(coefsCons);
 125  701 degreeCons = reduceUntilConflict(litImplied, ind, coefsCons,
 126    wpb);
 127    // mise-a-jour du degre du conflit
 128  701 degreeCons = (degreeCons.multiply(coefMultCons));
 129  701 degree = degree.multiply(coefMult);
 130    }
 131    // multiplication par coefMult des coefficients du conflit
 132  886 for (Integer i : coefs.keySet()) {
 133    //coefs.put(i, coefs.get(i).multiply(coefMult));
 134  96611 setCoef(i,coefs.get(i).multiply(coefMult));
 135    }
 136    }
 137   
 138    // On effectue la resolution
 139  355081 degree = cuttingPlane(cpb, degreeCons, coefsCons, coefMultCons, val);
 140    assert !coefs.containsKey(litImplied);
 141    assert !coefs.containsKey(litImplied ^ 1);
 142    assert degree.signum() > 0;
 143   
 144    // Saturation
 145  355081 degree = saturation();
 146    assert slackConflict().signum() <= 0;
 147   
 148  355081 return degree;
 149    }
 150   
 151  701 private BigInteger reduceUntilConflict(int litImplied, int ind,
 152    BigInteger[] reducedCoefs, WatchPb wpb) {
 153  701 BigInteger slackResolve = BigInteger.ONE.negate();
 154  701 BigInteger slackThis = BigInteger.ZERO;
 155  701 BigInteger slackIndex = BigInteger.ZERO;
 156  701 BigInteger ppcm;
 157  701 BigInteger reducedDegree = wpb.getDegree();
 158   
 159  701 do {
 160  21262 if (slackResolve.signum() >= 0) {
 161    assert slackThis.signum() > 0;
 162  20561 BigInteger tmp = reduceInConstraint(wpb, reducedCoefs, ind,
 163    reducedDegree);
 164    assert ((tmp.compareTo(reducedDegree) < 0) && (tmp
 165    .compareTo(BigInteger.ONE) >= 0));
 166  20561 reducedDegree = tmp;
 167    }
 168    // Recherche d es coefficients multiplicateurs
 169    assert coefs.get(litImplied ^ 1).signum() > 0;
 170    assert reducedCoefs[ind].signum() > 0;
 171   
 172  21262 BigInteger coefLitImplied = coefs.get(litImplied ^ 1);
 173  21262 ppcm = ppcm(reducedCoefs[ind], coefLitImplied);
 174    assert ppcm.signum() > 0;
 175  21262 coefMult = ppcm.divide(coefLitImplied);
 176  21262 coefMultCons = ppcm.divide(reducedCoefs[ind]);
 177   
 178    assert coefMultCons.signum() > 0;
 179    assert coefMult.signum() > 0;
 180    assert coefMult.multiply(coefLitImplied).equals(
 181    coefMultCons.multiply(reducedCoefs[ind]));
 182   
 183    // calcul des marges (poss) de chaque contrainte
 184  21262 slackThis = wpb.slackConstraint(reducedCoefs, reducedDegree)
 185    .multiply(coefMultCons);
 186  21262 slackIndex = slackConflict().multiply(coefMult);
 187   
 188    assert slackIndex.signum() <= 0;
 189   
 190    // calcul (approximation) de la marge de la resolvante
 191  21262 slackResolve = slackThis.add(slackIndex);
 192  21262 } while (slackResolve.signum() >= 0);
 193    assert coefMult.multiply(coefs.get(litImplied ^ 1)).equals(
 194    coefMultCons.multiply(reducedCoefs[ind]));
 195  701 return reducedDegree;
 196   
 197    }
 198   
 199  1560538 public BigInteger slackConflict() {
 200  1560538 BigInteger poss = BigInteger.ZERO;
 201  1560538 BigInteger tmp;
 202    // Pour chaque litteral
 203  1560538 for (Integer i : coefs.keySet()) {
 204  70873207 tmp = coefs.get(i);
 205  70873207 if (tmp.signum() != 0 && !voc.isFalsified(i))
 206  10824272 poss = poss.add(tmp);
 207    }
 208  1560538 return poss.subtract(degree);
 209    }
 210   
 211  1919231 public boolean oldIsAssertive(int dl) {
 212  1919231 BigInteger tmp;
 213  1919231 BigInteger slack = computeSlack(dl).subtract(degree);
 214  1919231 if (slack.signum() < 0)
 215  0 return false;
 216  1919231 for (Integer i : coefs.keySet()) {
 217  147424093 tmp = coefs.get(i);
 218  147424093 if ((tmp.signum() > 0)
 219    && (voc.isUnassigned(i) || voc.getLevel(i) >= dl)
 220    && (slack.compareTo(tmp) < 0))
 221  933 return true;
 222    }
 223  1918298 return false;
 224    }
 225   
 226  1919231 private BigInteger computeSlack(int dl){
 227  1919231 BigInteger slack = BigInteger.ZERO;
 228  1919231 BigInteger tmp;
 229  1919231 for (Integer i : coefs.keySet()) {
 230  147758011 tmp = coefs.get(i);
 231  147758011 if ((tmp.signum() > 0)
 232    && (((!voc.isFalsified(i)) || voc.getLevel(i) >= dl)))
 233  101278594 slack = slack.add(tmp);
 234    }
 235  1919231 return slack;
 236    }
 237   
 238  899224 public boolean isAssertive(int dl) {
 239    assert dl <= currentLevel;
 240  899224 BigInteger tmp;
 241  899224 if (dl < currentLevel) {
 242  13464 currentSlack = BigInteger.ZERO;
 243  13464 int ilit;
 244  13464 for (Integer lit : coefs.keySet()) {
 245  8356527 ilit = lit.intValue();
 246  8356527 tmp = coefs.get(lit);
 247  8356527 if ((tmp.signum() > 0)
 248    && (!voc.isFalsified(ilit) || voc.getLevel(ilit) >= dl))
 249  3519112 currentSlack = currentSlack.add(tmp);
 250    }
 251    }
 252  899224 currentLevel = dl;
 253  899224 BigInteger slack = currentSlack.subtract(degree);
 254  899224 if (slack.signum() < 0)
 255  33238 return false;
 256  865986 int ilit;
 257  865986 for (Integer lit : coefs.keySet()) {
 258  29451704 ilit = lit.intValue();
 259  29451704 tmp = coefs.get(lit);
 260  29451704 if ((tmp.signum() > 0)
 261    && (voc.isUnassigned(ilit) || voc.getLevel(ilit) >= dl)
 262    && (slack.compareTo(tmp) < 0))
 263  113292 return true;
 264    }
 265  752694 return false;
 266    }
 267   
 268    /**
 269    * Calcule le ppcm de deux nombres
 270    *
 271    * @param a
 272    * premier nombre de l'op?ration
 273    * @param b
 274    * second nombre de l'op?ration
 275    * @return le ppcm en question
 276    */
 277  21262 protected static BigInteger ppcm(BigInteger a, BigInteger b) {
 278  21262 return a.divide(a.gcd(b)).multiply(b);
 279    }
 280   
 281    /**
 282    * Reduction d'une contrainte On supprime un litteral non assigne
 283    * prioritairement, vrai sinon. En aucun cas on ne supprime litImplied.
 284    *
 285    * @return mise a jour du degre
 286    */
 287  20561 public BigInteger reduceInConstraint(WatchPb wpb,
 288    final BigInteger[] coefsBis, final int indLitImplied,
 289    final BigInteger degreeBis) {
 290    // logger.entering(this.getClass().getName(),"reduceInConstraint");
 291    assert degreeBis.compareTo(BigInteger.ONE) > 0;
 292    // Recherche d'un litt?ral non assign?
 293  20561 int lit = -1;
 294  20561 for (int ind = 0; (ind < wpb.size()) && (lit == -1); ind++)
 295  3583457 if (coefsBis[ind].signum() != 0 && voc.isUnassigned(wpb.get(ind))) {
 296    assert coefsBis[ind].compareTo(degreeBis) < 0;
 297  3963 lit = ind;
 298    }
 299   
 300    // Sinon, recherche d'un litteral satisfait
 301  20561 if (lit == -1)
 302  16598 for (int ind = 0; (ind < wpb.size()) && (lit == -1); ind++)
 303  1962217 if ((coefsBis[ind].signum() != 0)
 304    && (voc.isSatisfied(wpb.get(ind)))
 305    && (ind != indLitImplied))
 306  16598 lit = ind;
 307   
 308    // on a trouve un litteral
 309    assert lit != -1;
 310   
 311    assert lit != indLitImplied;
 312    // logger.finer("Found literal "+Lits.toString(lits[lit]));
 313    // on reduit la contrainte
 314  20561 BigInteger degUpdate = degreeBis.subtract(coefsBis[lit]);
 315  20561 coefsBis[lit] = BigInteger.ZERO;
 316   
 317    // saturation de la contrainte
 318    assert degUpdate.signum() > 0;
 319  20561 BigInteger minimum = degUpdate;
 320  20561 for (int i = 0; i < coefsBis.length; i++) {
 321  3781574 if (coefsBis[i].signum() > 0)
 322  3127653 minimum = minimum.min(coefsBis[i]);
 323  3781574 coefsBis[i] = degUpdate.min(coefsBis[i]);
 324    }
 325  20561 if (minimum.equals(degUpdate) && !degUpdate.equals(BigInteger.ONE)) {
 326    // on a obtenu une clause
 327    // plus de reduction possible
 328  12 degUpdate = BigInteger.ONE;
 329  12 for (int i = 0; i < coefsBis.length; i++)
 330  2106 if (coefsBis[i].signum() > 0)
 331  1679 coefsBis[i] = degUpdate;
 332    }
 333   
 334    assert coefsBis[indLitImplied].signum() > 0;
 335    assert degreeBis.compareTo(degUpdate) > 0;
 336  20561 return degUpdate;
 337    }
 338   
 339  701 private boolean positiveCoefs(final BigInteger[] coefsCons) {
 340  701 for (int i = 0; i < coefsCons.length; i++) {
 341  67335 if (coefsCons[i].signum() <= 0)
 342  0 return false;
 343    }
 344  701 return true;
 345    }
 346   
 347    /**
 348    * retourne le niveau de backtrack : c'est-?-dire le niveau le plus haut
 349    * pour lequel la contrainte est assertive
 350    *
 351    * @param maxLevel
 352    * le plus bas niveau pour lequel la contrainte est assertive
 353    * @return the highest level (smaller int) for which the constraint is
 354    * assertive.
 355    */
 356  56646 public int getBacktrackLevel(int maxLevel) {
 357  56646 int litLevel;
 358  56646 int borneMax = maxLevel;
 359    // System.out.println(this);
 360    // System.out.println("assertive au niveau : " + maxLevel);
 361    // assert oldIsAssertive(borneMax);
 362  56646 int borneMin = -1;
 363    // on calcule borneMax,
 364    // le niveau le plus haut dans l'arbre ou la contrainte est assertive
 365  56646 for (int lit : coefs.keySet()) {
 366  1986840 litLevel = voc.getLevel(lit);
 367  1986840 if (litLevel < borneMax && litLevel > borneMin && oldIsAssertive(litLevel))
 368  933 borneMax = litLevel;
 369    // else
 370    // borneMin = litLevel;
 371    }
 372    // on retourne le niveau immediatement inferieur ? borneMax
 373    // pour lequel la contrainte possede un literal
 374  56646 int retour = 0;
 375  56646 for (int lit : coefs.keySet()) {
 376  1986840 litLevel = voc.getLevel(lit);
 377  1986840 if (litLevel > retour && litLevel < borneMax)
 378  159387 retour = litLevel;
 379    }
 380  56646 return retour;
 381    }
 382   
 383  13464 public void updateSlack(int level) {
 384   
 385    }
 386   
 387  2795148 @Override
 388    void increaseCoef(Integer lit, BigInteger incCoef) {
 389  2795148 int ilit = lit.intValue();
 390  2795148 if ((!voc.isFalsified(ilit)) || voc.getLevel(ilit) == currentLevel) {
 391  442224 currentSlack = currentSlack.add(incCoef);
 392    }
 393  2795148 super.increaseCoef(lit, incCoef);
 394    }
 395   
 396  1414 @Override
 397    void decreaseCoef(Integer lit, BigInteger decCoef) {
 398  1414 int ilit = lit.intValue();
 399  1414 if ((!voc.isFalsified(ilit)) || voc.getLevel(ilit) == currentLevel) {
 400  646 currentSlack = currentSlack.subtract(decCoef);
 401    }
 402  1414 super.decreaseCoef(lit, decCoef);
 403    }
 404   
 405  4110309 @Override
 406    void setCoef(Integer lit, BigInteger newValue) {
 407  4110309 int ilit = lit.intValue();
 408  4110309 if ((!voc.isFalsified(ilit)) || voc.getLevel(ilit) == currentLevel) {
 409  772474 if (coefs.containsKey(lit))
 410  462852 currentSlack = currentSlack.subtract(coefs.get(lit));
 411  772474 currentSlack = currentSlack.add(newValue);
 412    }
 413  4110309 super.setCoef(lit, newValue);
 414    }
 415   
 416  386518 @Override
 417    void removeCoef(Integer lit) {
 418  386518 int ilit = lit.intValue();
 419  386518 if ((!voc.isFalsified(ilit)) || voc.getLevel(ilit) == currentLevel) {
 420  383728 currentSlack = currentSlack.subtract(coefs.get(lit));
 421    }
 422  386518 super.removeCoef(lit);
 423    }
 424   
 425    }
 
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.