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