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