Clover coverage report -
Coverage timestamp: dim. nov. 12 2006 12:21:31 CET
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 265   Methods: 18
NCLOC: 200   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
ArrayPbIncrementEtParcours.java 0% 0% 0% 0%
coverage
 1    /*
 2    * Created on Jan 20, 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    import org.sat4j.minisat.core.VarActivityListener;
 14    import org.sat4j.specs.IVec;
 15    import org.sat4j.specs.IVecInt;
 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 ArrayPbIncrementEtParcours implements IDataStructurePB {
 22   
 23    /*
 24    * During the process of cutting planes, pseudo-boolean constraints are
 25    * coded with a HashMap <literal, coefficient> and a BigInteger for the
 26    * degree.
 27    */
 28    protected final ILits voc;
 29   
 30    protected BigInteger[] coefs;
 31   
 32    protected BigInteger degree;
 33   
 34    protected BigInteger currentSlack = BigInteger.ZERO;
 35   
 36    protected int currentLevel;
 37   
 38  0 ArrayPbIncrementEtParcours(int[] lits, BigInteger[] coefLits, BigInteger degree, ILits voc,
 39    int level) {
 40  0 coefs = new BigInteger[2 * voc.nVars() + 2];
 41  0 currentLevel = level;
 42  0 for (int i = 0; i < lits.length; i++) {
 43  0 coefs[lits[i]] = coefLits[i];
 44  0 if ((coefs[lits[i]].signum() > 0) && (((!voc.isFalsified(lits[i])) || voc.getLevel(lits[i]) == currentLevel))) {
 45  0 currentSlack = currentSlack.add(coefs[lits[i]]);
 46    }
 47    }
 48  0 this.degree = degree;
 49  0 this.voc = voc;
 50    }
 51   
 52  0 ArrayPbIncrementEtParcours(ILits voc) {
 53  0 coefs = new BigInteger[2 * voc.nVars() + 2];
 54  0 degree = BigInteger.ZERO;
 55  0 this.voc = voc;
 56    }
 57   
 58   
 59  0 public BigInteger saturation() {
 60    assert degree.signum() > 0;
 61  0 BigInteger minimum = degree;
 62  0 for (int i = 2; i < coefs.length; i++) {
 63  0 if (coefs[i] != null) {
 64    assert coefs[i].signum() > 0;
 65    // modification
 66    // coefs[i] = degree.min(coefs[i]);
 67  0 if (degree.compareTo(coefs[i]) < 0)
 68  0 setCoef(i, degree);
 69    assert coefs[i].signum() > 0;
 70  0 minimum = minimum.min(coefs[i]);
 71    }
 72    }
 73    // on a appris une clause
 74  0 if (minimum.equals(degree) && minimum.compareTo(BigInteger.ONE) > 0) {
 75  0 degree = BigInteger.ONE;
 76  0 for (int i = 2; i < coefs.length; i++)
 77  0 if (coefs[i] != null)
 78    // coefs[i] = BigInteger.ONE;
 79  0 setCoef(i, BigInteger.ONE);
 80    }
 81   
 82  0 return degree;
 83    }
 84   
 85  0 public BigInteger cuttingPlane(PBConstr cpb, BigInteger deg,
 86    BigInteger[] reducedCoefs, VarActivityListener val) {
 87  0 return cuttingPlane(cpb, deg, reducedCoefs, BigInteger.ONE, val);
 88    }
 89   
 90  0 public BigInteger cuttingPlane(PBConstr cpb, BigInteger degreeCons,
 91    BigInteger[] reducedCoefs, BigInteger coefMult,
 92    VarActivityListener val) {
 93  0 degree = degree.add(degreeCons);
 94    assert degree.signum() > 0;
 95   
 96  0 if (reducedCoefs == null) {
 97  0 for (int i = 0; i < cpb.size(); i++)
 98  0 cuttingPlane(cpb.get(i), multiplyCoefficient(cpb.getCoef(i),
 99    coefMult));
 100    } else
 101  0 for (int i = 0; i < cpb.size(); i++)
 102  0 cuttingPlane(cpb.get(i), multiplyCoefficient(reducedCoefs[i],
 103    coefMult));
 104   
 105  0 return degree;
 106    }
 107   
 108  0 public BigInteger cuttingPlane(int[] lits, BigInteger[] reducedCoefs,
 109    BigInteger deg) {
 110  0 return cuttingPlane(lits, reducedCoefs, deg, BigInteger.ONE);
 111    }
 112   
 113  0 public BigInteger cuttingPlane(int lits[], BigInteger[] reducedCoefs,
 114    BigInteger degreeCons, BigInteger coefMult) {
 115  0 degree = degree.add(degreeCons);
 116    assert degree.signum() > 0;
 117   
 118  0 for (int i = 0; i < lits.length; i++)
 119  0 cuttingPlane(lits[i], reducedCoefs[i].multiply(coefMult));
 120   
 121  0 return degree;
 122    }
 123   
 124  0 private void cuttingPlane(final int lit, final BigInteger coef) {
 125    assert coef.signum() >= 0;
 126  0 if (coef.signum() > 0) {
 127  0 if (coefs[lit ^ 1] == null) {
 128    assert (coefs[lit] == null) || (coefs[lit].signum() > 0);
 129  0 if (coefs[lit] == null)
 130    // coefs[lit] = coef;
 131  0 setCoef(lit, coef);
 132    else
 133    // coefs[lit] = coefs[lit].add(coef);
 134  0 increaseCoef(lit, coef);
 135    assert coefs[lit].signum() > 0;
 136    } else {
 137    assert coefs[lit] == null;
 138  0 if (coefs[lit ^ 1].compareTo(coef) < 0) {
 139    // coefs[lit] = coef.subtract(coefs[lit ^ 1]);
 140  0 setCoef(lit, coef.subtract(coefs[lit ^ 1]));
 141    assert coefs[lit].signum() > 0;
 142  0 degree = degree.subtract(coefs[lit ^ 1]);
 143    // coefs[lit ^ 1] = null;
 144  0 removeCoef(lit ^ 1);
 145    } else {
 146  0 if (coefs[lit ^ 1].equals(coef)) {
 147  0 degree = degree.subtract(coef);
 148    // coefs[lit ^ 1] = null;
 149  0 removeCoef(lit ^ 1);
 150    } else {
 151    // coefs[lit ^ 1] = coefs[lit ^ 1].subtract(coef);
 152  0 decreaseCoef(lit ^ 1, coef);
 153    assert coefs[lit ^ 1].signum() > 0;
 154  0 degree = degree.subtract(coef);
 155    }
 156    }
 157    }
 158    }
 159    assert (coefs[lit ^ 1] == null) || (coefs[lit] == null);
 160    }
 161   
 162  0 public void buildConstraintFromConflict(IVecInt resLits,
 163    IVec<BigInteger> resCoefs) {
 164  0 resLits.clear();
 165  0 resCoefs.clear();
 166    // On recherche tous les litt?raux concern?s
 167  0 for (int i = 2; i < coefs.length; i++) {
 168  0 if (coefs[i] != null) {
 169  0 resLits.push(i);
 170    assert coefs[i].signum() > 0;
 171  0 resCoefs.push(coefs[i]);
 172    }
 173    }
 174    };
 175   
 176  0 public void buildConstraintFromMapPb(int[] resLits, BigInteger[] resCoefs) {
 177    // On recherche tous les litt?raux concern?s
 178    assert resLits.length == resCoefs.length;
 179    assert resLits.length == size();
 180  0 int ind = 0;
 181  0 for (int i = 2; i < coefs.length; i++) {
 182  0 if (coefs[i] != null) {
 183  0 resLits[ind] = i;
 184    assert coefs[i].signum() > 0;
 185  0 resCoefs[ind] = coefs[i];
 186  0 ind++;
 187    }
 188    }
 189    };
 190   
 191  0 public BigInteger getDegree() {
 192  0 return degree;
 193    }
 194   
 195  0 public int size() {
 196  0 int cpt = 0;
 197  0 for (int i = 2; i < coefs.length; i++)
 198  0 if (coefs[i] != null)
 199  0 cpt++;
 200  0 return cpt;
 201    }
 202   
 203    /*
 204    * (non-Javadoc)
 205    *
 206    * @see java.lang.Object#toString()
 207    */
 208  0 @Override
 209    public String toString() {
 210  0 StringBuilder stb = new StringBuilder();
 211  0 for (int i = 2; i < coefs.length; i++) {
 212  0 if (coefs[i] != null) {
 213  0 stb.append(coefs[i]);
 214  0 stb.append(".");
 215  0 stb.append(Lits.toString(i));
 216  0 stb.append(" ");
 217  0 stb.append("[");
 218  0 stb.append(voc.valueToString(i));
 219  0 stb.append("@");
 220  0 stb.append(voc.getLevel(i));
 221  0 stb.append("]");
 222   
 223    }
 224    }
 225  0 return stb.toString() + " >= " + degree; //$NON-NLS-1$
 226    }
 227   
 228  0 private BigInteger multiplyCoefficient(BigInteger coef, BigInteger mult) {
 229  0 if (mult.equals(BigInteger.ONE))
 230  0 return coef;
 231  0 if (coef.equals(BigInteger.ONE))
 232  0 return mult;
 233  0 return coef.multiply(mult);
 234    }
 235   
 236  0 private void increaseCoef(int lit, BigInteger incCoef) {
 237  0 if ((!voc.isFalsified(lit)) || voc.getLevel(lit) >= currentLevel) {
 238  0 currentSlack = currentSlack.add(incCoef);
 239    }
 240  0 coefs[lit] = coefs[lit].add(incCoef);
 241    }
 242   
 243  0 private void decreaseCoef(int lit, BigInteger decCoef) {
 244  0 if ((!voc.isFalsified(lit)) || voc.getLevel(lit) >= currentLevel) {
 245  0 currentSlack = currentSlack.subtract(decCoef);
 246    }
 247  0 coefs[lit] = coefs[lit].subtract(decCoef);
 248    }
 249   
 250  0 protected void setCoef(int lit, BigInteger newValue) {
 251  0 if ((!voc.isFalsified(lit)) || voc.getLevel(lit) >= currentLevel) {
 252  0 if (coefs[lit] != null)
 253  0 currentSlack = currentSlack.subtract(coefs[lit]);
 254  0 currentSlack = currentSlack.add(newValue);
 255    }
 256  0 coefs[lit] = newValue;
 257    }
 258   
 259  0 private void removeCoef(int lit) {
 260  0 if ((!voc.isFalsified(lit)) || voc.getLevel(lit) >= currentLevel) {
 261  0 currentSlack = currentSlack.subtract(coefs[lit]);
 262    }
 263  0 coefs[lit] = null;
 264    }
 265    }
 
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.