Clover coverage report -
Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 212   Methods: 14
NCLOC: 161   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
ArrayPb.java 90% 83,7% 85,7% 86,1%
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   
 11    import org.sat4j.minisat.constraints.cnf.Lits;
 12    import org.sat4j.minisat.core.ILits;
 13    import org.sat4j.specs.IVec;
 14    import org.sat4j.specs.IVecInt;
 15   
 16    /**
 17    * @author parrain TODO To change the template for this generated type comment
 18    * go to Window - Preferences - Java - Code Style - Code Templates
 19    */
 20    public class ArrayPb implements IDataStructurePB {
 21   
 22    /*
 23    * During the process of cutting planes, pseudo-boolean constraints are
 24    * coded with a HashMap <literal, coefficient> and a BigInteger for the
 25    * degree.
 26    */
 27    protected final ILits voc;
 28   
 29    protected BigInteger[] coefs;
 30   
 31    protected BigInteger degree;
 32   
 33   
 34  519135 ArrayPb(int[] lits, BigInteger[] coefLits, BigInteger degree, ILits voc) {
 35  519135 coefs = new BigInteger[2 * voc.nVars() + 2];
 36  519135 for (int i = 0; i < lits.length; i++)
 37  7495262 coefs[lits[i]] = coefLits[i];
 38  519135 this.degree = degree;
 39  519135 this.voc = voc;
 40    }
 41   
 42  2945770 ArrayPb(ILits voc) {
 43  2945770 coefs = new BigInteger[2 * voc.nVars() + 2];
 44  2945768 degree = BigInteger.ZERO;
 45  2945768 this.voc = voc;
 46    }
 47   
 48  6452273 public BigInteger saturation() {
 49    assert degree.signum() > 0;
 50  6452273 BigInteger minimum = degree;
 51  6452273 for (int i = 2; i < coefs.length; i++) {
 52    if (coefs[i] != null) {
 53    assert coefs[i].signum() > 0;
 54  150737993 coefs[i] = degree.min(coefs[i]);
 55    assert coefs[i].signum() > 0;
 56  150737993 minimum = minimum.min(coefs[i]);
 57    }
 58    }
 59    // on a appris une clause
 60  6452273 if (minimum.equals(degree) && minimum.compareTo(BigInteger.ONE) > 0) {
 61  126 degree = BigInteger.ONE;
 62  126 for (int i = 2; i < coefs.length; i++)
 63  608400 if (coefs[i] != null)
 64  0 coefs[i] = BigInteger.ONE;
 65    }
 66   
 67  6452273 return degree;
 68    }
 69   
 70  0 public BigInteger cuttingPlane(PBConstr cpb, BigInteger deg,
 71    BigInteger[] reducedCoefs) {
 72  0 return cuttingPlane(cpb, deg, reducedCoefs, BigInteger.ONE);
 73    }
 74   
 75  3506505 public BigInteger cuttingPlane(PBConstr cpb, BigInteger degreeCons,
 76    BigInteger[] reducedCoefs, BigInteger coefMult) {
 77  3506505 degree = degree.add(degreeCons);
 78    assert degree.signum() > 0;
 79   
 80  3506505 if (reducedCoefs == null) {
 81  3473158 for (int i = 0; i < cpb.size(); i++)
 82  36388565 cuttingPlane(cpb.get(i), multiplyCoefficient(cpb.getCoef(i),
 83    coefMult));
 84    } else
 85  33347 for (int i = 0; i < cpb.size(); i++)
 86  5045713 cuttingPlane(cpb.get(i), multiplyCoefficient(reducedCoefs[i],
 87    coefMult));
 88   
 89  3506505 return degree;
 90    }
 91   
 92  2945768 public BigInteger cuttingPlane(int[] lits, BigInteger[] reducedCoefs,
 93    BigInteger deg) {
 94  2945768 return cuttingPlane(lits, reducedCoefs, deg, BigInteger.ONE);
 95    }
 96   
 97  2945768 public BigInteger cuttingPlane(int lits[], BigInteger[] reducedCoefs,
 98    BigInteger degreeCons, BigInteger coefMult) {
 99  2945768 degree = degree.add(degreeCons);
 100    assert degree.signum() > 0;
 101   
 102  2945768 for (int i = 0; i < lits.length; i++)
 103  24347381 cuttingPlane(lits[i], reducedCoefs[i].multiply(coefMult));
 104   
 105  2945768 return degree;
 106    }
 107   
 108  65781659 private void cuttingPlane(final int lit, final BigInteger coef) {
 109    assert coef.signum() >= 0;
 110  65781659 if (coef.signum() > 0) {
 111  64269210 if (coefs[lit ^ 1] == null) {
 112    assert (coefs[lit] == null) || (coefs[lit].signum() > 0);
 113  60054332 if (coefs[lit] == null)
 114  37299512 coefs[lit] = coef;
 115    else
 116  22754820 coefs[lit] = coefs[lit].add(coef);
 117    assert coefs[lit].signum() > 0;
 118    } else {
 119    assert coefs[lit] == null;
 120  4214878 if (coefs[lit ^ 1].compareTo(coef) < 0) {
 121  196209 coefs[lit] = coef.subtract(coefs[lit ^ 1]);
 122    assert coefs[lit].signum() > 0;
 123  196209 degree = degree.subtract(coefs[lit ^ 1]);
 124  196209 coefs[lit ^ 1] = null;
 125    } else {
 126  4018669 if (coefs[lit ^ 1].equals(coef)) {
 127  3928686 degree = degree.subtract(coef);
 128  3928686 coefs[lit ^ 1] = null;
 129    } else {
 130  89983 coefs[lit ^ 1] = coefs[lit ^ 1].subtract(coef);
 131    assert coefs[lit ^ 1].signum() > 0;
 132  89983 degree = degree.subtract(coef);
 133    }
 134    }
 135    }
 136    }
 137    assert (coefs[lit ^ 1] == null) || (coefs[lit] == null);
 138    }
 139   
 140  519135 public void buildConstraintFromConflict(IVecInt resLits,
 141    IVec<BigInteger> resCoefs) {
 142  519135 resLits.clear();
 143  519135 resCoefs.clear();
 144    // On recherche tous les litt?raux concern?s
 145  519135 for (int i = 2; i < coefs.length; i++) {
 146  293695068 if (coefs[i] != null) {
 147  16518707 resLits.push(i);
 148    assert coefs[i].signum() > 0;
 149  16518707 resCoefs.push(coefs[i]);
 150    }
 151    }
 152    };
 153   
 154  3315560 public void buildConstraintFromMapPb(int[] resLits, BigInteger[] resCoefs) {
 155    // On recherche tous les litt?raux concern?s
 156    assert resLits.length == resCoefs.length;
 157    assert resLits.length == size();
 158  3315560 int ind = 0;
 159  3315560 for (int i = 2; i < coefs.length; i++) {
 160  1993634078 if (coefs[i] != null) {
 161  28146677 resLits[ind] = i;
 162    assert coefs[i].signum() > 0;
 163  28146677 resCoefs[ind] = coefs[i];
 164  28146677 ind++;
 165    }
 166    }
 167    };
 168   
 169  3889931 public BigInteger getDegree() {
 170  3889931 return degree;
 171    }
 172   
 173  6631120 public int size() {
 174  6631120 int cpt = 0;
 175  6631120 for (int i = 2; i < coefs.length; i++)
 176    if (coefs[i] != null)
 177  56293354 cpt++;
 178  6631120 return cpt;
 179    }
 180   
 181    /*
 182    * (non-Javadoc)
 183    *
 184    * @see java.lang.Object#toString()
 185    */
 186  0 @Override
 187    public String toString() {
 188  0 StringBuilder stb = new StringBuilder();
 189  0 for (int i = 2; i < coefs.length; i++) {
 190  0 if (coefs[i] != null) {
 191  0 stb.append(coefs[i]);
 192  0 stb.append(".");
 193  0 stb.append(Lits.toString(i));
 194  0 stb.append(" ");
 195  0 stb.append("[");
 196  0 stb.append(voc.valueToString(i));
 197  0 stb.append("]");
 198   
 199    }
 200    }
 201  0 return stb.toString() + " >= " + degree; //$NON-NLS-1$
 202    }
 203   
 204  41434278 private BigInteger multiplyCoefficient(BigInteger coef, BigInteger mult) {
 205  41434278 if (mult.equals(BigInteger.ONE))
 206  34634707 return coef;
 207  6799571 if (coef.equals(BigInteger.ONE))
 208  4688116 return mult;
 209  2111455 return coef.multiply(mult);
 210    }
 211   
 212    }
 
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.