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