Clover coverage report -
Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 324   Methods: 10
NCLOC: 203   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
ConflictMap.java 0% 0% 0% 0%
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   
 11    import java.math.BigInteger;
 12    import java.util.HashMap;
 13    import java.util.Map;
 14   
 15    import org.sat4j.minisat.core.ILits;
 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 ConflictMap extends MapPb implements IConflict{
 22   
 23    private final ILits voc;
 24   
 25  0 public static IConflict createConflict(PBConstr cpb) {
 26  0 Map<Integer, BigInteger> m = new HashMap<Integer, BigInteger>();
 27  0 for (int i = 0; i < cpb.size(); i++) {
 28    assert cpb.get(i) != 0;
 29    assert cpb.getCoef(i).signum() > 0;
 30  0 m.put(cpb.get(i), cpb.getCoef(i));
 31    }
 32  0 return new ConflictMap(m, cpb.getDegree(), cpb.getVocabulary());
 33    }
 34   
 35   
 36  0 ConflictMap(Map<Integer, BigInteger> m, BigInteger d, ILits voc) {
 37  0 super(m, d);
 38  0 this.voc = voc;
 39    }
 40   
 41    /*
 42    * coefficient to be computed.
 43    *
 44    */
 45    private BigInteger coefMult = BigInteger.ZERO;
 46   
 47    private BigInteger coefMultCons = BigInteger.ZERO;
 48   
 49    /**
 50    * Effectue une resolution avec une contrainte PB. Met a jour le Conflict.
 51    *
 52    * @param cpb
 53    * contrainte avec laquelle on va faire la resolution
 54    * @param litImplied
 55    * litteral devant etre resolu
 56    * @return la mise a jour du degre
 57    */
 58  0 public BigInteger resolve(PBConstr cpb, int litImplied) {
 59    assert litImplied > 1;
 60  0 if (!coefs.containsKey(litImplied ^ 1)) {
 61    // logger.fine("pas de resolution");
 62  0 return degree;
 63    }
 64   
 65    assert slackConflict().signum() <= 0;
 66    assert degree.signum() >= 0;
 67   
 68    // copie des coeffs de la contrainte pour pouvoir effectuer
 69    // des operations de reductions
 70  0 BigInteger[] coefsCons = null;
 71  0 BigInteger degreeCons = cpb.getDegree();
 72   
 73    // Recherche de l'indice du litteral implique
 74  0 int ind = 0;
 75  0 while (cpb.get(ind) != litImplied)
 76  0 ind++;
 77   
 78    assert cpb.get(ind) == litImplied;
 79    assert cpb.getCoef(ind) != BigInteger.ZERO;
 80   
 81  0 if (cpb.getCoef(ind).equals(BigInteger.ONE)) {
 82    // la rŽsolvante sera conflictuelle (Dixon)
 83  0 coefMultCons = coefs.get(litImplied ^ 1);
 84  0 coefMult = BigInteger.ONE;
 85    // mise-a-jour du degre du conflit
 86  0 degreeCons = (degreeCons.multiply(coefMultCons));
 87    } else {
 88  0 if (coefs.get(litImplied ^ 1).equals(BigInteger.ONE)) {
 89    // la rŽsolvante sera conflictuelle (Dixon)
 90  0 coefMult = cpb.getCoef(ind);
 91  0 coefMultCons = BigInteger.ONE;
 92    // mise-a-jour du degre du conflit
 93  0 degree = degree.multiply(coefMult);
 94    } else {
 95    // Reduction de la contrainte
 96    // jusqu'a obtenir une resolvante conflictuelle
 97  0 WatchPb wpb = (WatchPb) cpb;
 98  0 coefsCons = wpb.getCoefs();
 99    assert positiveCoefs(coefsCons);
 100  0 degreeCons = reduceUntilConflict(litImplied, ind, coefsCons,
 101    wpb);
 102    // mise-a-jour du degre du conflit
 103  0 degreeCons = (degreeCons.multiply(coefMultCons));
 104  0 degree = degree.multiply(coefMult);
 105    }
 106    // multiplication par coefMult des coefficients du conflit
 107  0 for (Integer i : coefs.keySet()) {
 108  0 coefs.put(i, coefs.get(i).multiply(coefMult));
 109    }
 110    }
 111   
 112    // On effectue la resolution
 113  0 degree = cuttingPlane(cpb, degreeCons, coefsCons, coefMultCons);
 114    assert !coefs.containsKey(litImplied);
 115    assert !coefs.containsKey(litImplied ^ 1);
 116    assert degree.signum() > 0;
 117   
 118    // Saturation
 119  0 degree = saturation();
 120    assert slackConflict().signum() <= 0;
 121   
 122  0 return degree;
 123    }
 124   
 125  0 private BigInteger reduceUntilConflict(int litImplied, int ind,
 126    BigInteger[] reducedCoefs, WatchPb wpb) {
 127  0 BigInteger slackResolve = BigInteger.ONE.negate();
 128  0 BigInteger slackThis = BigInteger.ZERO;
 129  0 BigInteger slackIndex = BigInteger.ZERO;
 130  0 BigInteger ppcm;
 131  0 BigInteger reducedDegree = wpb.getDegree();
 132   
 133  0 do {
 134  0 if (slackResolve.signum() >= 0) {
 135    assert slackThis.signum() > 0;
 136  0 BigInteger tmp = reduceInConstraint(wpb, reducedCoefs, ind,
 137    reducedDegree);
 138    assert ((tmp.compareTo(reducedDegree) < 0) && (tmp
 139    .compareTo(BigInteger.ONE) >= 0));
 140  0 reducedDegree = tmp;
 141    }
 142    // Recherche des coefficients multiplicateurs
 143    assert coefs.get(litImplied ^ 1).signum() > 0;
 144    assert reducedCoefs[ind].signum() > 0;
 145   
 146  0 BigInteger coefLitImplied = coefs.get(litImplied ^ 1);
 147  0 ppcm = ppcm(reducedCoefs[ind], coefLitImplied);
 148    assert ppcm.signum() > 0;
 149  0 coefMult = ppcm.divide(coefLitImplied);
 150  0 coefMultCons = ppcm.divide(reducedCoefs[ind]);
 151   
 152    assert coefMultCons.signum() > 0;
 153    assert coefMult.signum() > 0;
 154    assert coefMult.multiply(coefLitImplied).equals(
 155    coefMultCons.multiply(reducedCoefs[ind]));
 156   
 157    // calcul des marges (poss) de chaque contrainte
 158  0 slackThis = wpb.slackConstraint(reducedCoefs, reducedDegree)
 159    .multiply(coefMultCons);
 160  0 slackIndex = slackConflict().multiply(coefMult);
 161   
 162    assert slackIndex.signum() <= 0;
 163   
 164    // calcul (approximation) de la marge de la resolvante
 165  0 slackResolve = slackThis.add(slackIndex);
 166  0 } while (slackResolve.signum() >= 0);
 167    assert coefMult.multiply(coefs.get(litImplied ^ 1)).equals(
 168    coefMultCons.multiply(reducedCoefs[ind]));
 169  0 return reducedDegree;
 170   
 171    }
 172   
 173  0 public BigInteger slackConflict() {
 174  0 BigInteger poss = BigInteger.ZERO;
 175  0 BigInteger tmp;
 176    // Pour chaque litteral
 177  0 for (Integer i : coefs.keySet()){
 178  0 tmp = coefs.get(i);
 179  0 if (tmp.signum() != 0 && !voc.isFalsified(i))
 180  0 poss = poss.add(tmp);
 181    }
 182  0 return poss.subtract(degree);
 183    }
 184   
 185  0 public boolean isAssertive(int dl) {
 186  0 BigInteger slack = BigInteger.ZERO;
 187  0 BigInteger tmp;
 188  0 for (Integer i : coefs.keySet()) {
 189  0 tmp = coefs.get(i);
 190  0 if ((tmp.signum() > 0)
 191    && (((!voc.isFalsified(i)) || voc.getLevel(i) >= dl)))
 192  0 slack = slack.add(tmp);
 193    }
 194  0 slack = slack.subtract(degree);
 195  0 if (slack.signum() < 0)
 196  0 return false;
 197  0 for (Integer i : coefs.keySet()) {
 198  0 tmp = coefs.get(i);
 199  0 if ((tmp.signum() > 0)
 200    && (voc.isUnassigned(i) || voc.getLevel(i) >= dl)
 201    && (slack.subtract(tmp).signum() < 0))
 202  0 return true;
 203    }
 204  0 return false;
 205    }
 206   
 207    /**
 208    * Calcule le ppcm de deux nombres
 209    *
 210    * @param a
 211    * premier nombre de l'op?ration
 212    * @param b
 213    * second nombre de l'op?ration
 214    * @return le ppcm en question
 215    */
 216  0 protected static BigInteger ppcm(BigInteger a, BigInteger b) {
 217  0 return a.divide(a.gcd(b)).multiply(b);
 218    }
 219   
 220    /**
 221    * Reduction d'une contrainte On supprime un litteral non assigne
 222    * prioritairement, vrai sinon. En aucun cas on ne supprime litImplied.
 223    *
 224    * @return mise a jour du degre
 225    */
 226  0 public BigInteger reduceInConstraint(WatchPb wpb,
 227    final BigInteger[] coefsBis, final int indLitImplied,
 228    final BigInteger degreeBis) {
 229    // logger.entering(this.getClass().getName(),"reduceInConstraint");
 230    assert degreeBis.compareTo(BigInteger.ONE) > 0;
 231    // Recherche d'un litt?ral non assign?
 232  0 int lit = -1;
 233  0 for (int ind = 0; (ind < wpb.size()) && (lit == -1); ind++)
 234  0 if (coefsBis[ind].signum() != 0 && voc.isUnassigned(wpb.get(ind))) {
 235    assert coefsBis[ind].compareTo(degreeBis) < 0;
 236  0 lit = ind;
 237    }
 238   
 239    // Sinon, recherche d'un litteral satisfait
 240  0 if (lit == -1)
 241  0 for (int ind = 0; (ind < wpb.size()) && (lit == -1); ind++)
 242  0 if ((coefsBis[ind].signum() != 0)
 243    && (voc.isSatisfied(wpb.get(ind)))
 244    && (ind != indLitImplied))
 245  0 lit = ind;
 246   
 247    // on a trouve un litteral
 248    assert lit != -1;
 249   
 250    assert lit != indLitImplied;
 251    // logger.finer("Found literal "+Lits.toString(lits[lit]));
 252    // on reduit la contrainte
 253  0 BigInteger degUpdate = degreeBis.subtract(coefsBis[lit]);
 254  0 coefsBis[lit] = BigInteger.ZERO;
 255   
 256    // saturation de la contrainte
 257    assert degUpdate.signum() > 0;
 258  0 BigInteger minimum = degUpdate;
 259  0 for (int i = 0; i < coefsBis.length; i++) {
 260  0 if (coefsBis[i].signum() > 0)
 261  0 minimum = minimum.min(coefsBis[i]);
 262  0 coefsBis[i] = degUpdate.min(coefsBis[i]);
 263    }
 264  0 if (minimum.equals(degUpdate) && !degUpdate.equals(BigInteger.ONE)) {
 265    // on a obtenu une clause
 266    // plus de reduction possible
 267  0 degUpdate = BigInteger.ONE;
 268  0 for (int i = 0; i < coefsBis.length; i++)
 269  0 if (coefsBis[i].signum() > 0)
 270  0 coefsBis[i] = degUpdate;
 271    }
 272   
 273    assert coefsBis[indLitImplied].signum() > 0;
 274    assert degreeBis.compareTo(degUpdate) > 0;
 275  0 return degUpdate;
 276    }
 277   
 278  0 private boolean positiveCoefs(final BigInteger[] coefsCons) {
 279  0 for (int i = 0; i < coefsCons.length; i++) {
 280  0 if (coefsCons[i].signum() <= 0)
 281  0 return false;
 282    }
 283  0 return true;
 284    }
 285   
 286    /**
 287    * retourne le niveau de backtrack : c'est-?-dire le niveau le plus haut
 288    * pour lequel la contrainte est assertive
 289    *
 290    * @param maxLevel
 291    * le plus bas niveau pour lequel la contrainte est assertive
 292    * @return the highest level (smaller int) for which the constraint is assertive.
 293    */
 294  0 public int getBacktrackLevel(int maxLevel) {
 295  0 int litLevel;
 296  0 int borneMax = maxLevel;
 297    // System.out.println(this);
 298    // System.out.println("assertive au niveau : " + maxLevel);
 299    assert isAssertive(borneMax);
 300  0 int borneMin = -1;
 301    // on calcule borneMax,
 302    // le niveau le plus haut dans l'arbre ou la contrainte est assertive
 303  0 for (int lit : coefs.keySet()) {
 304  0 litLevel = voc.getLevel(lit);
 305  0 if (litLevel < borneMax && litLevel > borneMin)
 306  0 if (isAssertive(litLevel))
 307  0 borneMax = litLevel;
 308    else
 309  0 borneMin = litLevel;
 310    }
 311    // on retourne le niveau immediatement inferieur ? borneMax
 312    // pour lequel la contrainte possede un literal
 313  0 int retour = 0;
 314  0 for (int lit : coefs.keySet()) {
 315  0 litLevel = voc.getLevel(lit);
 316  0 if (litLevel > retour && litLevel < borneMax)
 317  0 retour = litLevel;
 318    }
 319  0 return retour;
 320    }
 321   
 322    }
 323   
 324   
 
CloverReport generated by Clover Code Coverage v1.3.9
jeu. juin 15 2006 08:24:39 CEST.		   Open Source License registered to the OpenSAT Project. This license of Clover is provided to support the development of OpenSAT only.