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