Clover coverage report -
Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 186   Methods: 9
NCLOC: 84   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
PuebloMinWatchPb.java 70% 75,7% 66,7% 73,2%
coverage coverage
 1    /*
 2    * MiniSAT in Java, a Java based-SAT framework Copyright (C) 2004 Daniel Le
 3    * Berre
 4    *
 5    * Based on the original minisat specification from:
 6    *
 7    * An extensible SAT solver. Niklas E???n and Niklas S???rensson. Proceedings of
 8    * the Sixth International Conference on Theory and Applications of
 9    * Satisfiability Testing, LNCS 2919, pp 502-518, 2003.
 10    *
 11    * This library is free software; you can redistribute it and/or modify it under
 12    * the terms of the GNU Lesser General Public License as published by the Free
 13    * Software Foundation; either version 2.1 of the License, or (at your option)
 14    * any later version.
 15    *
 16    * This library is distributed in the hope that it will be useful, but WITHOUT
 17    * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
 18    * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
 19    * details.
 20    *
 21    * You should have received a copy of the GNU Lesser General Public License
 22    * along with this library; if not, write to the Free Software Foundation, Inc.,
 23    * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
 24    *
 25    */
 26    package org.sat4j.minisat.constraints.pb;
 27   
 28    import java.io.Serializable;
 29    import java.math.BigInteger;
 30   
 31    import org.sat4j.core.Vec;
 32    import org.sat4j.core.VecInt;
 33    import org.sat4j.minisat.core.ILits;
 34    import org.sat4j.minisat.core.UnitPropagationListener;
 35    import org.sat4j.specs.ContradictionException;
 36    import org.sat4j.specs.IVec;
 37    import org.sat4j.specs.IVecInt;
 38   
 39    public class PuebloMinWatchPb extends MinWatchPb implements Serializable {
 40   
 41    private static final long serialVersionUID = 1L;
 42   
 43    /**
 44    * Constructeur de base des contraintes
 45    *
 46    * @param voc
 47    * Informations sur le vocabulaire employ???
 48    * @param ps
 49    * Liste des litt???raux
 50    * @param coefs
 51    * Liste des coefficients
 52    * @param moreThan
 53    * Indication sur le comparateur
 54    * @param degree
 55    * Stockage du degr??? de la contrainte
 56    */
 57  305863 private PuebloMinWatchPb(ILits voc, IDataStructurePB mpb) {
 58   
 59  305863 super(voc, mpb);
 60    }
 61   
 62    /**
 63    * @param s
 64    * outil pour la propagation des litt???raux
 65    * @param ps
 66    * liste des litt???raux de la nouvelle contrainte
 67    * @param coefs
 68    * liste des coefficients des litt???raux de la contrainte
 69    * @param moreThan
 70    * d???termine si c'est une sup???rieure ou ???gal ??? l'origine
 71    * @param degree
 72    * fournit le degr??? de la contrainte
 73    * @return une nouvelle clause si tout va bien, ou null si un conflit est
 74    * d???tect???
 75    */
 76  830 public static PuebloMinWatchPb minWatchPbNew(UnitPropagationListener s,
 77    ILits voc, IVecInt ps, IVecInt coefs, boolean moreThan, int degree)
 78    throws ContradictionException {
 79  830 return minWatchPbNew(s, voc, ps, toVecBigInt(coefs), moreThan,
 80    toBigInt(degree));
 81    }
 82   
 83    /**
 84    * @param s
 85    * outil pour la propagation des litt???raux
 86    * @param ps
 87    * liste des litt???raux de la nouvelle contrainte
 88    * @param coefs
 89    * liste des coefficients des litt???raux de la contrainte
 90    * @param moreThan
 91    * d???termine si c'est une sup???rieure ou ???gal ??? l'origine
 92    * @param degree
 93    * fournit le degr??? de la contrainte
 94    * @return une nouvelle clause si tout va bien, ou null si un conflit est
 95    * d???tect???
 96    */
 97  279814 public static PuebloMinWatchPb minWatchPbNew(UnitPropagationListener s,
 98    ILits voc, IVecInt ps, IVec<BigInteger> coefs, boolean moreThan,
 99    BigInteger degree) throws ContradictionException {
 100    // Il ne faut pas modifier les param?tres
 101  279814 VecInt litsVec = new VecInt(ps.size());
 102  279814 IVec<BigInteger> coefsVec = new Vec<BigInteger>(coefs.size());
 103  279814 ps.copyTo(litsVec);
 104  279814 coefs.copyTo(coefsVec);
 105   
 106    // Ajouter les simplifications quand la structure sera d???finitive
 107  279814 IDataStructurePB mpb = niceParameters(litsVec, coefsVec, moreThan,
 108    degree, voc);
 109  279812 PuebloMinWatchPb outclause = new PuebloMinWatchPb(voc, mpb);
 110   
 111  279812 if (outclause.degree.signum() <= 0) {
 112  0 return null;
 113    }
 114   
 115  279812 outclause.computeWatches();
 116   
 117  279797 outclause.computePropagation(s);
 118   
 119  279797 return outclause;
 120   
 121    }
 122   
 123  0 public static PuebloMinWatchPb minWatchPbNew(UnitPropagationListener s,
 124    ILits voc, IDataStructurePB mpb) throws ContradictionException {
 125  0 PuebloMinWatchPb outclause = new PuebloMinWatchPb(voc, mpb);
 126   
 127  0 if (outclause.degree.signum() <= 0) {
 128  0 return null;
 129    }
 130   
 131  0 outclause.computeWatches();
 132   
 133  0 outclause.computePropagation(s);
 134   
 135  0 return outclause;
 136   
 137    }
 138   
 139    /**
 140    *
 141    */
 142  0 public static WatchPb watchPbNew(ILits voc, IVecInt lits, IVecInt coefs,
 143    boolean moreThan, int degree) {
 144  0 return watchPbNew(voc, lits, toVecBigInt(coefs), moreThan,
 145    toBigInt(degree));
 146    }
 147   
 148    /**
 149    *
 150    */
 151  26051 public static WatchPb watchPbNew(ILits voc, IVecInt lits,
 152    IVec<BigInteger> coefs, boolean moreThan, BigInteger degree) {
 153  26051 IDataStructurePB mpb = null;
 154  26051 mpb = niceCheckedParameters(lits, coefs, moreThan, degree, voc);
 155  26051 return new PuebloMinWatchPb(voc, mpb);
 156    }
 157   
 158  0 public static WatchPb normalizedWatchPbNew(ILits voc, IDataStructurePB mpb) {
 159  0 return new PuebloMinWatchPb(voc, mpb);
 160    }
 161   
 162  92349748 protected BigInteger maximalCoefficient(int pIndice) {
 163  92349748 return coefs[0];
 164    }
 165   
 166  92349748 protected BigInteger updateWatched(BigInteger mc, int pIndice) {
 167  92349748 BigInteger maxCoef = mc;
 168  92349748 if (watchingCount < size()) {
 169  76454880 BigInteger upWatchCumul = watchCumul.subtract(coefs[pIndice]);
 170  76454880 BigInteger borneSup = degree.add(maxCoef);
 171  76454880 for (int ind = 0; ind < lits.length
 172    && upWatchCumul.compareTo(borneSup) < 0; ind++) {
 173  720574903 if (!voc.isFalsified(lits[ind]) && !watched[ind]) {
 174  54010629 upWatchCumul = upWatchCumul.add(coefs[ind]);
 175  54010629 watched[ind] = true;
 176    assert watchingCount < size();
 177  54010629 watching[watchingCount++] = ind;
 178  54010629 voc.watch(lits[ind] ^ 1, this);
 179    }
 180    }
 181  76454880 watchCumul = upWatchCumul.add(coefs[pIndice]);
 182    }
 183  92349748 return maxCoef;
 184    }
 185   
 186    }
 
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.