Clover coverage report -
Coverage timestamp: mer. avr. 19 2006 16:27:14 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 257   Methods: 8
NCLOC: 151   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
Conflict.java 100% 100% 100% 100%
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.Map;
 11   
 12    import org.sat4j.minisat.core.ILits;
 13   
 14    /**
 15    * @author parrain TODO To change the template for this generated type comment
 16    * go to Window - Preferences - Java - Code Style - Code Templates
 17    */
 18    class Conflict extends MapPb {
 19   
 20    private final ILits voc;
 21   
 22  112328 Conflict(Map<Integer, BigInteger> m, BigInteger d, ILits voc) {
 23  112328 super(m, d);
 24  112328 this.voc = voc;
 25    }
 26   
 27    /*
 28    * coefficient to be computed.
 29    *
 30    */
 31    private BigInteger coefMult = BigInteger.ZERO;
 32   
 33    private BigInteger coefMultCons = BigInteger.ZERO;
 34   
 35    /**
 36    * Effectue une resolution avec une contrainte PB. Met a jour le Conflict.
 37    *
 38    * @param wpb
 39    * contrainte avec laquelle on va faire la resolution
 40    * @param litImplied
 41    * litteral devant etre resolu
 42    * @return la mise a jour du degre
 43    */
 44  2858011 BigInteger resolve(WatchPb wpb, int litImplied) {
 45    assert litImplied > 1;
 46  2858011 if (!coefs.containsKey(litImplied ^ 1)) {
 47    // logger.fine("pas de resolution");
 48  1977505 return degree;
 49    }
 50   
 51    assert slackConflict().signum() <= 0;
 52    assert degree.signum() >= 0;
 53   
 54    // copie des coeffs de la contrainte pour pouvoir effectuer
 55    // des operations de reductions
 56  880506 BigInteger[] coefsCons = wpb.getCoefs();
 57  880506 BigInteger degreeCons = wpb.getDegree();
 58  880506 int[] litsCons = wpb.getLits();
 59   
 60  880506 for (int i = 0; i < coefsCons.length; i++)
 61    assert coefsCons[i].signum() > 0;
 62   
 63    // Recherche de l'indice du litteral implique
 64  880506 int ind = -1;
 65  880506 while (litsCons[++ind] != litImplied)
 66    ;
 67   
 68    assert litsCons[ind] == litImplied;
 69    assert coefsCons[ind] != BigInteger.ZERO;
 70    // 1- Reduction de la contrainte
 71    // jusqu'a obtenir une resolvante conflictuelle
 72  880506 degreeCons = reduceUntilConflict(litImplied, ind, litsCons, coefsCons,
 73    degreeCons, wpb);
 74   
 75    // 2- multiplication par coefMult des coefficients du conflit
 76    // mise-a-jour du degre du conflit
 77  880506 degreeCons = (degreeCons.multiply(coefMultCons));
 78  880506 degree = degree.multiply(coefMult);
 79   
 80  880506 if (coefMult.compareTo(BigInteger.ONE) > 0) {
 81  1262 for (Integer i : coefs.keySet()) {
 82  94063 coefs.put(i, coefs.get(i).multiply(coefMult));
 83    }
 84    }
 85   
 86    // 3- On ajoute les informations de la contrainte courante
 87    // On effectue la resolution
 88  880506 degree = addCoeffNewConstraint(litsCons, coefsCons, degreeCons,
 89    coefMultCons);
 90    assert !coefs.containsKey(litImplied);
 91    assert !coefs.containsKey(litImplied ^ 1);
 92    assert degree.signum() > 0;
 93   
 94    // 4- Saturation
 95  880506 degree = saturation();
 96    assert slackConflict().signum() <= 0;
 97   
 98  880506 return degree;
 99    }
 100   
 101  880506 private BigInteger reduceUntilConflict(int litImplied, int ind, int[] lits,
 102    BigInteger[] coefsBis, BigInteger degreeBis, WatchPb wpb) {
 103  880506 BigInteger slackResolve = BigInteger.ONE.negate();
 104  880506 BigInteger slackThis = BigInteger.ZERO;
 105  880506 BigInteger slackIndex = BigInteger.ZERO;
 106  880506 BigInteger ppcm;
 107   
 108    // int cpt = -1;
 109   
 110  880506 do {
 111    // cpt++;
 112    // logger.fine("Compteur de passages : "+cpt);
 113  1012771 if (slackResolve.signum() >= 0) {
 114    assert slackThis.signum() > 0;
 115    // r?duction de la contrainte
 116  132265 BigInteger tmp = reduceInConstraint(coefsBis, lits, ind,
 117    degreeBis);
 118    assert ((tmp.compareTo(degreeBis) < 0) && (tmp
 119    .compareTo(BigInteger.ONE) >= 0));
 120  132265 degreeBis = tmp;
 121    }
 122    // Recherche des coefficients multiplicateurs
 123    assert coefs.get(litImplied ^ 1).signum() > 0;
 124    assert coefsBis[ind].signum() > 0;
 125   
 126  1012771 ppcm = ppcm(coefsBis[ind], coefs.get(litImplied ^ 1));
 127    assert ppcm.signum() > 0;
 128  1012771 coefMult = ppcm.divide(coefs.get(litImplied ^ 1));
 129  1012771 coefMultCons = ppcm.divide(coefsBis[ind]);
 130   
 131    assert coefMultCons.signum() > 0;
 132    assert coefMult.signum() > 0;
 133    assert coefMult.multiply(coefs.get(litImplied ^ 1)).equals(
 134    coefMultCons.multiply(coefsBis[ind]));
 135   
 136    // calcul des marges (poss) de chaque contrainte
 137  1012771 slackThis = wpb.slackConstraint(coefsBis, degreeBis).multiply(
 138    coefMultCons);
 139  1012771 slackIndex = slackConflict().multiply(coefMult);
 140   
 141    assert slackIndex.signum() <= 0;
 142   
 143    // calcul (approximation) de la marge de la resolvante
 144  1012771 slackResolve = slackThis.add(slackIndex);
 145  1012771 } while (slackResolve.signum() >= 0);
 146    assert coefMult.multiply(coefs.get(litImplied ^ 1)).equals(
 147    coefMultCons.multiply(coefsBis[ind]));
 148  880506 return degreeBis;
 149   
 150    }
 151   
 152  5744122 BigInteger slackConflict() {
 153  5744122 BigInteger poss = BigInteger.ZERO;
 154    // Pour chaque litteral
 155  5744122 for (Integer i : coefs.keySet())
 156  226760267 if (coefs.get(i).signum() != 0 && !voc.isFalsified(i))
 157  42094325 poss = poss.add(coefs.get(i));
 158  5744122 return poss.subtract(degree);
 159    }
 160   
 161  112328 BigInteger getDegree() {
 162  112328 return degree;
 163    }
 164   
 165  3123241 boolean isAssertive(int dl) {
 166  3123241 BigInteger slack = BigInteger.ZERO;
 167  3123241 for (Integer i : coefs.keySet()) {
 168  156180377 if ((coefs.get(i).signum() > 0)
 169    && (((!voc.isFalsified(i)) || voc.getLevel(i) >= dl)))
 170  53876803 slack = slack.add(coefs.get(i));
 171    }
 172  3123241 slack = slack.subtract(degree);
 173  3123241 if (slack.signum() < 0)
 174  100987 return false;
 175  3022254 for (Integer i : coefs.keySet()) {
 176  91252362 if ((coefs.get(i).signum() > 0)
 177    && (voc.isUnassigned(i) || voc.getLevel(i) >= dl)
 178    && (slack.subtract(coefs.get(i)).signum() < 0))
 179  224572 return true;
 180    }
 181  2797682 return false;
 182    }
 183   
 184    /**
 185    * Calcule le ppcm de deux nombres
 186    *
 187    * @param a
 188    * premier nombre de l'op?ration
 189    * @param b
 190    * second nombre de l'op?ration
 191    * @return le ppcm en question
 192    */
 193  1012771 protected static BigInteger ppcm(BigInteger a, BigInteger b) {
 194  1012771 return a.divide(a.gcd(b)).multiply(b);
 195    }
 196   
 197    /**
 198    * Reduction d'une contrainte On supprime un litteral non assigne
 199    * prioritairement, vrai sinon. En aucun cas on ne supprime litImplied.
 200    *
 201    * @param cycle
 202    * on reduira par le cyclieme litteral
 203    * @return mise a jour du degre
 204    */
 205  132265 public BigInteger reduceInConstraint(final BigInteger[] coefsBis,
 206    final int[] lits, final int indLitImplied,
 207    final BigInteger degreeBis) {
 208    // logger.entering(this.getClass().getName(),"reduceInConstraint");
 209    assert degreeBis.compareTo(BigInteger.ONE) > 0;
 210    // Recherche d'un litt?ral non assign?
 211  132265 int lit = -1;
 212  132265 for (int ind = 0; (ind < lits.length) && (lit == -1); ind++)
 213  18097036 if (coefsBis[ind].signum() != 0 && voc.isUnassigned(lits[ind])) {
 214    assert coefsBis[ind].compareTo(degreeBis) < 0;
 215  21501 lit = ind;
 216    }
 217   
 218    // Sinon, recherche d'un litteral satisfait
 219  132265 if (lit == -1)
 220  110764 for (int ind = 0; (ind < lits.length) && (lit == -1); ind++)
 221  9475012 if ((coefsBis[ind].signum() != 0)
 222    && (voc.isSatisfied(lits[ind]))
 223    && (ind != indLitImplied))
 224  110764 lit = ind;
 225   
 226    // on a trouve un litteral
 227    assert lit != -1;
 228   
 229    assert lit != indLitImplied;
 230    // logger.finer("Found literal "+Lits.toString(lits[lit]));
 231    // on reduit la contrainte
 232  132265 BigInteger degUpdate = degreeBis.subtract(coefsBis[lit]);
 233  132265 coefsBis[lit] = BigInteger.ZERO;
 234   
 235    // saturation de la contrainte
 236    assert degUpdate.signum() > 0;
 237  132265 BigInteger minimum = degUpdate;
 238  132265 for (int i = 0; i < coefsBis.length; i++) {
 239  19101497 if (coefsBis[i].signum() > 0)
 240  15694865 minimum = minimum.min(coefsBis[i]);
 241  19101497 coefsBis[i] = degUpdate.min(coefsBis[i]);
 242    }
 243  132265 if (minimum.equals(degUpdate) && !degUpdate.equals(BigInteger.ONE)) {
 244    // on a obtenu une clause
 245    // plus de reduction possible
 246  134 degUpdate = BigInteger.ONE;
 247  134 for (int i = 0; i < coefsBis.length; i++)
 248  20642 if (coefsBis[i].signum() > 0)
 249  15376 coefsBis[i] = degUpdate;
 250    }
 251   
 252    assert coefsBis[indLitImplied].signum() > 0;
 253    assert degreeBis.compareTo(degUpdate) > 0;
 254  132265 return degUpdate;
 255    }
 256   
 257    }
 
CloverReport generated by Clover Code Coverage v1.3.9
mer. avr. 19 2006 16:27:19 CEST.		   Open Source License registered to the OpenSAT Project. This license of Clover is provided to support the development of OpenSAT only.