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