Clover coverage report -
Coverage timestamp: jeu. sept. 29 2005 23:57:39 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 268   Methods: 10
NCLOC: 122   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
MaxWatchPb.java 90% 92,6% 90% 91,5%
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 the
 8    * Sixth International Conference on Theory and Applications of Satisfiability
 9    * 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 MaxWatchPb extends WatchPb implements Serializable {
 40   
 41    private static final long serialVersionUID = 1L;
 42   
 43    /**
 44    * Constructeur de base cr?ant des contraintes vides
 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  809035 private MaxWatchPb(ILits voc, IVecInt ps, IVec<BigInteger> bigCoefs,
 58    boolean moreThan, BigInteger bigDeg) {
 59   
 60  809035 super(ps, bigCoefs, moreThan, bigDeg);
 61  809035 this.voc = voc;
 62   
 63  809035 activity = 0;
 64  809035 watchCumul = BigInteger.ZERO;
 65  809035 locked = false;
 66    }
 67   
 68    /**
 69    * Permet l'observation de tous les litt???raux
 70    *
 71    * @see org.sat4j.minisat.constraints.WatchPb#computeWatches()
 72    */
 73  808947 @Override
 74    protected void computeWatches() throws ContradictionException {
 75    assert watchCumul.equals(BigInteger.ZERO);
 76  808947 for (int i = 0; i < lits.length; i++) {
 77    // Mise ? jour de la possibilit? initiale
 78  4445701 voc.watch(lits[i] ^ 1, this);
 79  4445701 watchCumul = watchCumul.add(coefs[i]);
 80    }
 81    assert watchCumul.compareTo(recalcLeftSide()) >= 0;
 82  808947 if (!learnt) {
 83  779799 if (watchCumul.compareTo(degree) < 0) {
 84  16 throw new ContradictionException("non satisfiable constraint");
 85    }
 86    }
 87    }
 88   
 89    /*
 90    * (non-Javadoc)
 91    *
 92    * @see org.sat4j.minisat.constraints.WatchPb#computePropagation()
 93    */
 94  779783 @Override
 95    protected void computePropagation(UnitPropagationListener s)
 96    throws ContradictionException {
 97    // On propage
 98  779783 int ind = 0;
 99  779783 while (ind < coefs.length
 100    && watchCumul.subtract(coefs[ind]).compareTo(degree) < 0) {
 101  274 if (voc.isUnassigned(lits[ind])) {
 102  209 if (!s.enqueue(lits[ind], this)) {
 103  0 throw new ContradictionException(
 104    "non satisfiable constraint");
 105    }
 106    }
 107  274 ind++;
 108    }
 109    assert watchCumul.compareTo(recalcLeftSide()) >= 0;
 110    }
 111   
 112    /**
 113    * @param s
 114    * outil pour la propagation des litt?raux
 115    * @param ps
 116    * liste des litt?raux de la nouvelle contrainte
 117    * @param coefs
 118    * liste des coefficients des litt?raux de la contrainte
 119    * @param moreThan
 120    * d?termine si c'est une sup?rieure ou ?gal ? l'origine
 121    * @param degree
 122    * fournit le degr? de la contrainte
 123    * @return une nouvelle clause si tout va bien, ou null si un conflit est
 124    * d?tect?
 125    */
 126  499336 public static MaxWatchPb maxWatchPbNew(UnitPropagationListener s,
 127    ILits voc, IVecInt ps, IVecInt coefs, boolean moreThan, int degree)
 128    throws ContradictionException {
 129  499336 return maxWatchPbNew(s, voc, ps, toVecBigInt(coefs), moreThan,
 130    toBigInt(degree));
 131    }
 132   
 133    /**
 134    * @param s
 135    * outil pour la propagation des litt?raux
 136    * @param ps
 137    * liste des litt?raux de la nouvelle contrainte
 138    * @param coefs
 139    * liste des coefficients des litt?raux de la contrainte
 140    * @param moreThan
 141    * d?termine si c'est une sup?rieure ou ?gal ? l'origine
 142    * @param degree
 143    * fournit le degr? de la contrainte
 144    * @return une nouvelle clause si tout va bien, ou null si un conflit est
 145    * d?tect?
 146    */
 147  779799 public static MaxWatchPb maxWatchPbNew(UnitPropagationListener s,
 148    ILits voc, IVecInt ps, IVec<BigInteger> coefs, boolean moreThan,
 149    BigInteger degree) throws ContradictionException {
 150   
 151    // Il ne faut pas modifier les param?tres
 152  779799 VecInt litsVec = new VecInt();
 153  779799 IVec<BigInteger> coefsVec = new Vec<BigInteger>();
 154  779799 ps.copyTo(litsVec);
 155  779799 coefs.copyTo(coefsVec);
 156   
 157  779799 niceParameter(litsVec, coefsVec);
 158   
 159  779799 MaxWatchPb outclause = new MaxWatchPb(voc, litsVec, coefsVec, moreThan,
 160    degree);
 161   
 162  779799 if (outclause.degree.signum() <= 0)
 163  0 return null;
 164  779799 outclause.computeWatches();
 165  779783 outclause.computePropagation(s);
 166   
 167  779783 return outclause;
 168   
 169    }
 170   
 171    /**
 172    * Propagation de la valeur de v?rit? d'un litt?ral falsifi?
 173    *
 174    * @param s
 175    * un prouveur
 176    * @param p
 177    * le litt?ral propag? (il doit etre falsifie)
 178    * @return false ssi une inconsistance est d?tect?e
 179    */
 180  260273874 public boolean propagate(UnitPropagationListener s, int p) {
 181  260273874 voc.watch(p, this);
 182   
 183    assert watchCumul.compareTo(recalcLeftSide()) >= 0;
 184   
 185    // Si le litt?ral est impliqu? il y a un conflit
 186  260273874 int indiceP = 0;
 187  260273874 while ((lits[indiceP] ^ 1) != p)
 188  1951799705 indiceP++;
 189   
 190  260273874 BigInteger coefP = coefs[indiceP];
 191   
 192  260273874 if (watchCumul.subtract(coefP).compareTo(degree) < 0) {
 193    // System.out.println(this.analyse(new ConstrHandle()));
 194   
 195    assert !isSatisfiable();
 196  5214729 return false;
 197    }
 198   
 199    // On met en place la mise ? jour du compteur
 200  255059145 voc.undos(p).push(this);
 201  255059145 watchCumul = watchCumul.subtract(coefP);
 202   
 203    // On propage
 204  255059145 int ind = 0;
 205  255059145 while (ind < coefs.length
 206    && watchCumul.subtract(coefs[ind]).compareTo(degree) < 0) {
 207  701865992 if (voc.isUnassigned(lits[ind])) {
 208  170216664 if (!s.enqueue(lits[ind], this)) {
 209    // lastConfl = p;
 210    // System.out.println(this.analyse(new ConstrHandle()));
 211    assert !isSatisfiable();
 212  0 return false;
 213    }
 214    // logger.fine("littï¿œral impliquï¿œ " +
 215    // Lits.toString(lits[ind]));
 216    // logger.fine(" par la contrainte " + this);
 217    }
 218  701865992 ind++;
 219    }
 220   
 221    assert learnt || watchCumul.compareTo(recalcLeftSide()) >= 0;
 222    assert watchCumul.compareTo(recalcLeftSide()) >= 0;
 223  255059145 return true;
 224    }
 225   
 226    /**
 227    * Enl???ve une contrainte du prouveur
 228    */
 229  31916 public void remove() {
 230  31916 for (int i = 0; i < lits.length; i++) {
 231  206495 if (!voc.isFalsified(lits[i]))
 232  176759 voc.watches(lits[i] ^ 1).remove(this);
 233    }
 234    }
 235   
 236    /**
 237    * M?thode appel?e lors du backtrack
 238    *
 239    * @param p
 240    * un litt?ral d?saffect?
 241    */
 242  254984678 public void undo(int p) {
 243  254984678 int indiceP = 0;
 244  254984678 while ((lits[indiceP] ^ 1) != p)
 245  1923729045 indiceP++;
 246   
 247    assert coefs[indiceP].signum() > 0;
 248   
 249  254984678 watchCumul = watchCumul.add(coefs[indiceP]);
 250    }
 251   
 252    /**
 253    *
 254    */
 255  0 public static WatchPb watchPbNew(ILits voc, IVecInt lits, IVecInt coefs,
 256    boolean moreThan, int degree) {
 257  0 return new MaxWatchPb(voc, lits, toVecBigInt(coefs), moreThan,
 258    toBigInt(degree));
 259    }
 260   
 261    /**
 262    *
 263    */
 264  29236 public static WatchPb watchPbNew(ILits voc, IVecInt lits,
 265    IVec<BigInteger> coefs, boolean moreThan, BigInteger degree) {
 266  29236 return new MaxWatchPb(voc, lits, coefs, moreThan, degree);
 267    }
 268    }
 
CloverReport generated by Clover Code Coverage v1.3.9
jeu. sept. 29 2005 23:57:47 CEST.		   Open Source License registered to the OpenSAT Project. This license of Clover is provided to support the development of OpenSAT only.