Clover coverage report -
Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 308   Methods: 12
NCLOC: 146   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
MaxWatchPb.java 67,6% 79,2% 75% 75,4%
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  1214677 private MaxWatchPb(ILits voc, IDataStructurePB mpb) {
 58   
 59  1214677 super(mpb);
 60  1214677 this.voc = voc;
 61   
 62  1214677 activity = 0;
 63  1214677 watchCumul = BigInteger.ZERO;
 64  1214677 locked = false;
 65    }
 66   
 67    /**
 68    * Permet l'observation de tous les litt???raux
 69    *
 70    * @see org.sat4j.minisat.constraints.WatchPb#computeWatches()
 71    */
 72  1214587 @Override
 73    protected void computeWatches() throws ContradictionException {
 74    assert watchCumul.equals(BigInteger.ZERO);
 75  1214587 for (int i = 0; i < lits.length; i++) {
 76  12023495 if (voc.isFalsified(lits[i])) {
 77  4726222 if (learnt)
 78  4726091 voc.undos(lits[i] ^ 1).push(this);
 79    } else {
 80    // Mise ? jour de la possibilit? initiale
 81  7297273 voc.watch(lits[i] ^ 1, this);
 82  7297273 watchCumul = watchCumul.add(coefs[i]);
 83    }
 84    }
 85   
 86    assert watchCumul.compareTo(recalcLeftSide()) >= 0;
 87  1214587 if (!learnt && watchCumul.compareTo(degree) < 0) {
 88  17 throw new ContradictionException("non satisfiable constraint");
 89    }
 90    }
 91   
 92    /*
 93    * (non-Javadoc)
 94    *
 95    * @see org.sat4j.minisat.constraints.WatchPb#computePropagation()
 96    */
 97  1025312 @Override
 98    protected void computePropagation(UnitPropagationListener s)
 99    throws ContradictionException {
 100    // On propage
 101  1025312 int ind = 0;
 102  1025312 while (ind < coefs.length
 103    && watchCumul.subtract(coefs[ind]).compareTo(degree) < 0) {
 104  266 if (voc.isUnassigned(lits[ind]) && !s.enqueue(lits[ind], this)) {
 105  0 throw new ContradictionException("non satisfiable constraint");
 106    }
 107  266 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  778801 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  778801 VecInt litsVec = new VecInt();
 153  778801 IVec<BigInteger> coefsVec = new Vec<BigInteger>();
 154  778801 ps.copyTo(litsVec);
 155  778801 coefs.copyTo(coefsVec);
 156   
 157  778801 IDataStructurePB mpb = niceParameters(litsVec, coefsVec, moreThan,
 158    degree, voc);
 159   
 160  778801 if (mpb == null) {
 161  0 return null;
 162    }
 163  778801 MaxWatchPb outclause = new MaxWatchPb(voc, mpb);
 164   
 165  778801 if (outclause.degree.signum() <= 0)
 166  0 return null;
 167  778801 outclause.computeWatches();
 168  778784 outclause.computePropagation(s);
 169   
 170  778784 return outclause;
 171   
 172    }
 173   
 174  0 public static MaxWatchPb normalizedMaxWatchPbNew(UnitPropagationListener s,
 175    ILits voc, ArrayPb mpb) throws ContradictionException {
 176  0 MaxWatchPb outclause = new MaxWatchPb(voc, mpb);
 177   
 178  0 if (outclause.degree.signum() <= 0)
 179  0 return null;
 180  0 outclause.computeWatches();
 181  0 outclause.computePropagation(s);
 182   
 183  0 return outclause;
 184    }
 185   
 186    /**
 187    * Propagation de la valeur de v?rit? d'un litt?ral falsifi?
 188    *
 189    * @param s
 190    * un prouveur
 191    * @param p
 192    * le litt?ral propag? (il doit etre falsifie)
 193    * @return false ssi une inconsistance est d?tect?e
 194    */
 195  327296634 public boolean propagate(UnitPropagationListener s, int p) {
 196  327296634 voc.watch(p, this);
 197   
 198    assert watchCumul.compareTo(recalcLeftSide()) >= 0 : "" + watchCumul
 199    + "/" + recalcLeftSide() + ":" + learnt;
 200   
 201    // Si le litt?ral est impliqu? il y a un conflit
 202  327296634 int indiceP = 0;
 203  327296634 while ((lits[indiceP] ^ 1) != p)
 204    indiceP++;
 205   
 206  327296634 BigInteger coefP = coefs[indiceP];
 207   
 208  327296634 BigInteger newcumul = watchCumul.subtract(coefP);
 209  327296634 if (newcumul.compareTo(degree) < 0) {
 210    // System.out.println(this.analyse(new ConstrHandle()));
 211   
 212    assert !isSatisfiable();
 213  3579899 return false;
 214    }
 215   
 216    // On met en place la mise ? jour du compteur
 217  323716735 voc.undos(p).push(this);
 218  323716735 watchCumul = newcumul;
 219   
 220    // On propage
 221  323716735 int ind = 0;
 222  323716735 BigInteger limit = watchCumul.subtract(degree);
 223  323716735 while (ind < coefs.length
 224    && limit.compareTo(coefs[ind]) < 0) {
 225  460383117 if (voc.isUnassigned(lits[ind]) && (!s.enqueue(lits[ind], this))) {
 226    assert !isSatisfiable();
 227  0 return false;
 228    }
 229  460383117 ind++;
 230    }
 231   
 232    assert learnt || watchCumul.compareTo(recalcLeftSide()) >= 0;
 233    assert watchCumul.compareTo(recalcLeftSide()) >= 0;
 234  323716735 return true;
 235    }
 236   
 237    /**
 238    * Enl???ve une contrainte du prouveur
 239    */
 240  0 public void remove() {
 241  0 for (int i = 0; i < lits.length; i++) {
 242  0 if (!voc.isFalsified(lits[i]))
 243  0 voc.watches(lits[i] ^ 1).remove(this);
 244    }
 245    }
 246   
 247    /**
 248    * M?thode appel?e lors du backtrack
 249    *
 250    * @param p
 251    * un litt?ral d?saffect?
 252    */
 253  328334175 public void undo(int p) {
 254  328334175 int indiceP = 0;
 255  328334175 while ((lits[indiceP] ^ 1) != p)
 256    indiceP++;
 257   
 258    assert coefs[indiceP].signum() > 0;
 259   
 260  328334175 watchCumul = watchCumul.add(coefs[indiceP]);
 261    }
 262   
 263    /**
 264    *
 265    */
 266  0 public static WatchPb watchPbNew(ILits voc, IVecInt lits, IVecInt coefs,
 267    boolean moreThan, int degree) {
 268  0 return watchPbNew(voc, lits, toVecBigInt(coefs), moreThan,
 269    toBigInt(degree));
 270    }
 271   
 272    /**
 273    *
 274    */
 275  189348 public static WatchPb watchPbNew(ILits voc, IVecInt lits,
 276    IVec<BigInteger> coefs, boolean moreThan, BigInteger degree) {
 277  189348 IDataStructurePB mpb = null;
 278  189348 mpb = niceCheckedParameters(lits, coefs, moreThan, degree, voc);
 279  189348 return new MaxWatchPb(voc, mpb);
 280    }
 281   
 282    /**
 283    * @param s
 284    * a unit propagation listener
 285    * @param voc
 286    * the vocabulary
 287    * @param mpb
 288    * the PB constraint to normalize.
 289    * @return a new PB contraint or null if a trivial inconsistency is detected.
 290    */
 291  246528 public static MaxWatchPb normalizedMaxWatchPbNew(UnitPropagationListener s,
 292    ILits voc, IDataStructurePB mpb) throws ContradictionException {
 293    // Il ne faut pas modifier les param?tres
 294  246528 MaxWatchPb outclause = new MaxWatchPb(voc, mpb);
 295   
 296  246528 if (outclause.degree.signum() <= 0) {
 297  0 return null;
 298    }
 299   
 300  246528 outclause.computeWatches();
 301   
 302  246528 outclause.computePropagation(s);
 303   
 304  246528 return outclause;
 305   
 306    }
 307   
 308    }
 
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.