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