Clover coverage report -
Coverage timestamp: dim. nov. 12 2006 12:21:31 CET
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 293   Methods: 18
NCLOC: 227   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
ArrayPb.java 77,8% 70,9% 61,1% 72,5%
coverage 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    import java.util.ArrayList;
 11    import java.util.List;
 12    import java.util.SortedMap;
 13    import java.util.TreeMap;
 14   
 15    import org.sat4j.minisat.constraints.cnf.Lits;
 16    import org.sat4j.minisat.core.ILits;
 17    import org.sat4j.minisat.core.VarActivityListener;
 18    import org.sat4j.specs.IVec;
 19    import org.sat4j.specs.IVecInt;
 20   
 21    /**
 22    * @author parrain TODO To change the template for this generated type comment
 23    * go to Window - Preferences - Java - Code Style - Code Templates
 24    */
 25    public class ArrayPb implements IDataStructurePB {
 26   
 27    /*
 28    * During the process of cutting planes, pseudo-boolean constraints are
 29    * coded with a HashMap <literal, coefficient> and a BigInteger for the
 30    * degree.
 31    */
 32    protected final ILits voc;
 33   
 34    protected BigInteger[] coefs;
 35   
 36    protected BigInteger degree;
 37   
 38    protected BigInteger currentSlack = BigInteger.ZERO;
 39   
 40    protected int currentLevel;
 41   
 42  72808 ArrayPb(int[] lits, BigInteger[] coefLits, BigInteger degree, ILits voc,
 43    int level) {
 44  72808 coefs = new BigInteger[2 * voc.nVars() + 2];
 45  72808 currentLevel = level;
 46  72808 int litLevel;
 47  72808 for (int i = 0; i < lits.length; i++) {
 48  1349968 coefs[lits[i]] = coefLits[i];
 49  1349968 if ((coefs[lits[i]].signum() > 0) && (((!voc.isFalsified(lits[i])) || voc.getLevel(lits[i]) == currentLevel))) {
 50  276465 currentSlack = currentSlack.add(coefs[lits[i]]);
 51    }
 52  1349968 litLevel = voc.getLevel(lits[i]);
 53  1349968 if (byLevel.containsKey(litLevel))
 54  1026481 byLevel.get(litLevel).add(lits[i]);
 55    else {
 56  323487 List<Integer> oneLevel = new ArrayList<Integer>();
 57  323487 oneLevel.add(lits[i]);
 58  323487 byLevel.put(litLevel, oneLevel);
 59    }
 60    }
 61  72808 this.degree = degree;
 62  72808 this.voc = voc;
 63    }
 64   
 65  0 ArrayPb(ILits voc) {
 66  0 coefs = new BigInteger[2 * voc.nVars() + 2];
 67  0 degree = BigInteger.ZERO;
 68  0 this.voc = voc;
 69    }
 70   
 71    protected SortedMap<Integer, List<Integer>> byLevel = new TreeMap<Integer, List<Integer>>();
 72   
 73   
 74  444986 public BigInteger saturation() {
 75    assert degree.signum() > 0;
 76  444986 BigInteger minimum = degree;
 77  444986 for (int i = 2; i < coefs.length; i++) {
 78  177932700 if (coefs[i] != null) {
 79    assert coefs[i].signum() > 0;
 80    // modification
 81    // coefs[i] = degree.min(coefs[i]);
 82  14257207 if (degree.compareTo(coefs[i]) < 0)
 83  3558217 setCoef(i, degree);
 84    assert coefs[i].signum() > 0;
 85  14257207 minimum = minimum.min(coefs[i]);
 86    }
 87    }
 88    // on a appris une clause
 89  444986 if (minimum.equals(degree) && minimum.compareTo(BigInteger.ONE) > 0) {
 90  28 degree = BigInteger.ONE;
 91  28 for (int i = 2; i < coefs.length; i++)
 92  135200 if (coefs[i] != null)
 93    // coefs[i] = BigInteger.ONE;
 94  0 setCoef(i, BigInteger.ONE);
 95    }
 96   
 97  444986 return degree;
 98    }
 99   
 100  0 public BigInteger cuttingPlane(PBConstr cpb, BigInteger deg,
 101    BigInteger[] reducedCoefs, VarActivityListener val) {
 102  0 return cuttingPlane(cpb, deg, reducedCoefs, BigInteger.ONE, val);
 103    }
 104   
 105  444986 public BigInteger cuttingPlane(PBConstr cpb, BigInteger degreeCons,
 106    BigInteger[] reducedCoefs, BigInteger coefMult,
 107    VarActivityListener val) {
 108  444986 degree = degree.add(degreeCons);
 109    assert degree.signum() > 0;
 110   
 111  444986 if (reducedCoefs == null) {
 112  444120 for (int i = 0; i < cpb.size(); i++)
 113  5360412 cuttingPlane(cpb.get(i), multiplyCoefficient(cpb.getCoef(i),
 114    coefMult));
 115    } else
 116  866 for (int i = 0; i < cpb.size(); i++)
 117  55182 cuttingPlane(cpb.get(i), multiplyCoefficient(reducedCoefs[i],
 118    coefMult));
 119   
 120  444986 return degree;
 121    }
 122   
 123  0 public BigInteger cuttingPlane(int[] lits, BigInteger[] reducedCoefs,
 124    BigInteger deg) {
 125  0 return cuttingPlane(lits, reducedCoefs, deg, BigInteger.ONE);
 126    }
 127   
 128  0 public BigInteger cuttingPlane(int lits[], BigInteger[] reducedCoefs,
 129    BigInteger degreeCons, BigInteger coefMult) {
 130  0 degree = degree.add(degreeCons);
 131    assert degree.signum() > 0;
 132   
 133  0 for (int i = 0; i < lits.length; i++)
 134  0 cuttingPlane(lits[i], reducedCoefs[i].multiply(coefMult));
 135   
 136  0 return degree;
 137    }
 138   
 139  5415594 private void cuttingPlane(final int lit, final BigInteger coef) {
 140    assert coef.signum() >= 0;
 141  5415594 if (coef.signum() > 0) {
 142  5395338 if (coefs[lit ^ 1] == null) {
 143    assert (coefs[lit] == null) || (coefs[lit].signum() > 0);
 144  4888838 if (coefs[lit] == null)
 145    // coefs[lit] = coef;
 146  1289663 setCoef(lit, coef);
 147    else
 148    // coefs[lit] = coefs[lit].add(coef);
 149  3599175 increaseCoef(lit, coef);
 150    assert coefs[lit].signum() > 0;
 151    } else {
 152    assert coefs[lit] == null;
 153  506500 if (coefs[lit ^ 1].compareTo(coef) < 0) {
 154    // coefs[lit] = coef.subtract(coefs[lit ^ 1]);
 155  6002 setCoef(lit, coef.subtract(coefs[lit ^ 1]));
 156    assert coefs[lit].signum() > 0;
 157  6002 degree = degree.subtract(coefs[lit ^ 1]);
 158    // coefs[lit ^ 1] = null;
 159  6002 nullCoef(lit ^ 1);
 160    } else {
 161  500498 if (coefs[lit ^ 1].equals(coef)) {
 162  498494 degree = degree.subtract(coef);
 163    // coefs[lit ^ 1] = null;
 164  498494 nullCoef(lit ^ 1);
 165    } else {
 166    // coefs[lit ^ 1] = coefs[lit ^ 1].subtract(coef);
 167  2004 decreaseCoef(lit ^ 1, coef);
 168    assert coefs[lit ^ 1].signum() > 0;
 169  2004 degree = degree.subtract(coef);
 170    }
 171    }
 172    }
 173    }
 174    assert (coefs[lit ^ 1] == null) || (coefs[lit] == null);
 175    }
 176   
 177  72808 public void buildConstraintFromConflict(IVecInt resLits,
 178    IVec<BigInteger> resCoefs) {
 179  72808 resLits.clear();
 180  72808 resCoefs.clear();
 181    // On recherche tous les litt?raux concern?s
 182  72808 for (int i = 2; i < coefs.length; i++) {
 183  23619180 if (coefs[i] != null) {
 184  2141137 resLits.push(i);
 185    assert coefs[i].signum() > 0;
 186  2141137 resCoefs.push(coefs[i]);
 187    }
 188    }
 189    };
 190   
 191  0 public void buildConstraintFromMapPb(int[] resLits, BigInteger[] resCoefs) {
 192    // On recherche tous les litt?raux concern?s
 193    assert resLits.length == resCoefs.length;
 194    assert resLits.length == size();
 195  0 int ind = 0;
 196  0 for (int i = 2; i < coefs.length; i++) {
 197  0 if (coefs[i] != null) {
 198  0 resLits[ind] = i;
 199    assert coefs[i].signum() > 0;
 200  0 resCoefs[ind] = coefs[i];
 201  0 ind++;
 202    }
 203    }
 204    };
 205   
 206  72808 public BigInteger getDegree() {
 207  72808 return degree;
 208    }
 209   
 210  0 public int size() {
 211  0 int cpt = 0;
 212  0 for (int i = 2; i < coefs.length; i++)
 213  0 if (coefs[i] != null)
 214  0 cpt++;
 215  0 return cpt;
 216    }
 217   
 218    /*
 219    * (non-Javadoc)
 220    *
 221    * @see java.lang.Object#toString()
 222    */
 223  0 @Override
 224    public String toString() {
 225  0 StringBuilder stb = new StringBuilder();
 226  0 for (int i = 2; i < coefs.length; i++) {
 227  0 if (coefs[i] != null) {
 228  0 stb.append(coefs[i]);
 229  0 stb.append(".");
 230  0 stb.append(Lits.toString(i));
 231  0 stb.append(" ");
 232  0 stb.append("[");
 233  0 stb.append(voc.valueToString(i));
 234  0 stb.append("@");
 235  0 stb.append(voc.getLevel(i));
 236  0 stb.append("]");
 237   
 238    }
 239    }
 240  0 return stb.toString() + " >= " + degree; //$NON-NLS-1$
 241    }
 242   
 243  5415594 private BigInteger multiplyCoefficient(BigInteger coef, BigInteger mult) {
 244  5415594 if (mult.equals(BigInteger.ONE))
 245  5288034 return coef;
 246  127560 if (coef.equals(BigInteger.ONE))
 247  106068 return mult;
 248  21492 return coef.multiply(mult);
 249    }
 250   
 251  3599175 private void increaseCoef(int lit, BigInteger incCoef) {
 252  3599175 if ((!voc.isFalsified(lit)) || voc.getLevel(lit) == currentLevel) {
 253  789838 currentSlack = currentSlack.add(incCoef);
 254    }
 255  3599175 coefs[lit] = coefs[lit].add(incCoef);
 256    }
 257   
 258  2004 private void decreaseCoef(int lit, BigInteger decCoef) {
 259  2004 if ((!voc.isFalsified(lit)) || voc.getLevel(lit) == currentLevel) {
 260  978 currentSlack = currentSlack.subtract(decCoef);
 261    }
 262  2004 coefs[lit] = coefs[lit].subtract(decCoef);
 263    }
 264   
 265  4868780 protected void setCoef(int lit, BigInteger newValue) {
 266  4868780 if ((!voc.isFalsified(lit)) || voc.getLevel(lit) == currentLevel) {
 267  1210341 if (coefs[lit] != null)
 268  780890 currentSlack = currentSlack.subtract(coefs[lit]);
 269  1210341 currentSlack = currentSlack.add(newValue);
 270    }
 271  4868780 if (coefs[lit] == null) {
 272  1295665 int litLevel = voc.getLevel(lit);
 273  1295665 if (byLevel.containsKey(litLevel))
 274  1070043 byLevel.get(litLevel).add(lit);
 275    else {
 276  225622 List<Integer> oneLevel = new ArrayList<Integer>();
 277  225622 oneLevel.add(lit);
 278  225622 byLevel.put(litLevel, oneLevel);
 279    }
 280    }
 281  4868780 coefs[lit] = newValue;
 282    }
 283   
 284  504496 private void nullCoef(int lit) {
 285  504496 if ((!voc.isFalsified(lit)) || voc.getLevel(lit) == currentLevel) {
 286  500358 currentSlack = currentSlack.subtract(coefs[lit]);
 287    }
 288  504496 int litLevel = voc.getLevel(lit);
 289  504496 if (byLevel.containsKey(litLevel))
 290  504496 byLevel.get(litLevel).remove(Integer.valueOf(lit));
 291  504496 coefs[lit] = null;
 292    }
 293    }
 
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.