Clover coverage report -
Coverage timestamp: jeu. sept. 29 2005 23:57:39 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 398   Methods: 11
NCLOC: 217   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
MinWatchPb.java 95,2% 95,4% 90,9% 95,1%
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 MinWatchPb extends WatchPb implements Serializable {
 40   
 41    private static final long serialVersionUID = 1L;
 42   
 43    /**
 44    * Liste des indices des litt???raux regardant la contrainte
 45    */
 46    private boolean[] watched;
 47   
 48    /**
 49    * Sert ??? d???terminer si la clause est watched par le litt???ral
 50    */
 51    private int[] watching;
 52   
 53    /**
 54    * Liste des indices des litt???raux regardant la contrainte
 55    */
 56    private int watchingCount = 0;
 57   
 58    /**
 59    * Constructeur de base des contraintes
 60    *
 61    * @param voc
 62    * Informations sur le vocabulaire employ???
 63    * @param ps
 64    * Liste des litt???raux
 65    * @param coefs
 66    * Liste des coefficients
 67    * @param moreThan
 68    * Indication sur le comparateur
 69    * @param degree
 70    * Stockage du degr??? de la contrainte
 71    */
 72  812835 private MinWatchPb(ILits voc, IVecInt ps, IVec<BigInteger> bigCoefs,
 73    boolean moreThan, BigInteger bigDeg) {
 74   
 75  812835 super(ps, bigCoefs, moreThan, bigDeg);
 76  812835 this.voc = voc;
 77   
 78  812835 watching = new int[this.coefs.length];
 79  812835 watched = new boolean[this.coefs.length];
 80  812835 activity = 0;
 81  812835 watchCumul = BigInteger.ZERO;
 82  812835 locked = false;
 83  812835 undos = new VecInt();
 84   
 85  812835 watchingCount = 0;
 86   
 87    }
 88   
 89    /*
 90    * (non-Javadoc)
 91    *
 92    * @see org.sat4j.minisat.constraints.WatchPb#computeWatches()
 93    */
 94  812747 @Override
 95    protected void computeWatches() throws ContradictionException {
 96    assert watchCumul.signum() == 0;
 97    assert watchingCount == 0;
 98  812747 for (int i = 0; i < lits.length
 99    && watchCumul.subtract(coefs[0]).compareTo(degree) < 0; i++) {
 100  2796412 if (!voc.isFalsified(lits[i])) {
 101  1877399 voc.watch(lits[i] ^ 1, this);
 102  1877399 watching[watchingCount++] = i;
 103  1877399 watched[i] = true;
 104    // Mise ??? jour de la possibilit??? initiale
 105  1877399 watchCumul = watchCumul.add(coefs[i]);
 106    }
 107    }
 108   
 109  812747 if (learnt) {
 110    // chercher tous les litteraux a regarder
 111    // par ordre de niveau decroissant
 112  33138 int free = 1;
 113   
 114  33138 while ((watchCumul.subtract(coefs[0]).compareTo(degree) < 0)
 115    && (free > 0)) {
 116  33207 free = 0;
 117    // regarder le litteral falsifie au plus bas niveau
 118  33207 int maxlevel = -1, maxi = -1;
 119  33207 for (int i = 0; i < lits.length; i++) {
 120   
 121  1091356 if (voc.isFalsified(lits[i]) && !watched[i]) {
 122  934766 free++;
 123  934766 int level = voc.getLevel(lits[i]);
 124  934766 if (level > maxlevel) {
 125  75381 maxi = i;
 126  75381 maxlevel = level;
 127    }
 128    }
 129   
 130    }
 131  33207 if (free > 0) {
 132    assert maxi >= 0;
 133  33193 voc.watch(lits[maxi] ^ 1, this);
 134  33193 watching[watchingCount++] = maxi;
 135  33193 watched[maxi] = true;
 136    // Mise ??? jour de la possibilit??? initiale
 137  33193 watchCumul = watchCumul.add(coefs[maxi]);
 138  33193 free--;
 139    assert free >= 0;
 140    }
 141    }
 142    assert lits.length == 1 || watchingCount > 1;
 143    }
 144   
 145  812747 if (watchCumul.compareTo(degree) < 0) {
 146  17 throw new ContradictionException("non satisfiable constraint");
 147    }
 148    assert nbOfWatched() == watchingCount;
 149    }
 150   
 151    /*
 152    * (non-Javadoc)
 153    *
 154    * @see org.sat4j.minisat.constraints.WatchPb#computePropagation(org.sat4j.minisat.UnitPropagationListener)
 155    */
 156  779592 @Override
 157    protected void computePropagation(UnitPropagationListener s)
 158    throws ContradictionException {
 159    // On propage si n???cessaire
 160  779592 int ind = 0;
 161  779592 while (ind < lits.length
 162    && watchCumul.subtract(coefs[watching[ind]]).compareTo(degree) < 0) {
 163  266 if (voc.isUnassigned(lits[ind])) {
 164  212 if (!s.enqueue(lits[ind], this)) {
 165  0 throw new ContradictionException(
 166    "non satisfiable constraint");
 167    }
 168    }
 169  266 ind++;
 170    }
 171    }
 172   
 173    /**
 174    * @param s
 175    * outil pour la propagation des litt???raux
 176    * @param ps
 177    * liste des litt???raux de la nouvelle contrainte
 178    * @param coefs
 179    * liste des coefficients des litt???raux de la contrainte
 180    * @param moreThan
 181    * d???termine si c'est une sup???rieure ou ???gal ??? l'origine
 182    * @param degree
 183    * fournit le degr??? de la contrainte
 184    * @return une nouvelle clause si tout va bien, ou null si un conflit est
 185    * d???tect???
 186    */
 187  499336 public static MinWatchPb minWatchPbNew(UnitPropagationListener s,
 188    ILits voc, IVecInt ps, IVecInt coefs, boolean moreThan, int degree)
 189    throws ContradictionException {
 190  499336 return minWatchPbNew(s, voc, ps, toVecBigInt(coefs), moreThan,
 191    toBigInt(degree));
 192    }
 193   
 194    /**
 195    * @param s
 196    * outil pour la propagation des litt???raux
 197    * @param ps
 198    * liste des litt???raux de la nouvelle contrainte
 199    * @param coefs
 200    * liste des coefficients des litt???raux de la contrainte
 201    * @param moreThan
 202    * d???termine si c'est une sup???rieure ou ???gal ??? l'origine
 203    * @param degree
 204    * fournit le degr??? de la contrainte
 205    * @return une nouvelle clause si tout va bien, ou null si un conflit est
 206    * d???tect???
 207    */
 208  779609 public static MinWatchPb minWatchPbNew(UnitPropagationListener s,
 209    ILits voc, IVecInt ps, IVec<BigInteger> coefs, boolean moreThan,
 210    BigInteger degree) throws ContradictionException {
 211    // Il ne faut pas modifier les param?tres
 212  779609 VecInt litsVec = new VecInt(ps.size());
 213  779609 IVec<BigInteger> coefsVec = new Vec<BigInteger>(coefs.size());
 214  779609 ps.copyTo(litsVec);
 215  779609 coefs.copyTo(coefsVec);
 216   
 217    // Ajouter les simplifications quand la structure sera d???finitive
 218  779609 niceParameter(litsVec, coefsVec);
 219  779609 MinWatchPb outclause = new MinWatchPb(voc, litsVec, coefsVec, moreThan,
 220    degree);
 221   
 222  779609 if (outclause.degree.signum() <= 0) {
 223  0 return null;
 224    }
 225   
 226  779609 outclause.computeWatches();
 227   
 228  779592 outclause.computePropagation(s);
 229   
 230  779592 return outclause;
 231   
 232    }
 233   
 234    /**
 235    * Nombre de litt???raux actuellement observ???
 236    *
 237    * @return nombre de litt???raux regard???s
 238    */
 239  474473165 protected int nbOfWatched() {
 240  474473165 int retour = 0;
 241  474473165 for (int ind = 0; ind < this.watched.length; ind++) {
 242  1325056923 for (int i = 0; i < watchingCount; i++)
 243    if (watching[i] == ind)
 244    assert watched[ind];
 245  1325056923 retour += (this.watched[ind]) ? 1 : 0;
 246    }
 247  474473165 return retour;
 248    }
 249   
 250    /**
 251    * Propagation de la valeur de v???rit??? d'un litt???ral falsifi???
 252    *
 253    * @param s
 254    * un prouveur
 255    * @param p
 256    * le litt???ral propag??? (il doit etre falsifie)
 257    * @return false ssi une inconsistance est d???t???ct???e
 258    */
 259  115955700 public boolean propagate(UnitPropagationListener s, int p) {
 260    assert nbOfWatched() == watchingCount;
 261   
 262    assert watchingCount > 1;
 263    // Recherche de l'indice du litt???ral p
 264  115955700 int pIndiceWatching = 0;
 265  115955700 while (pIndiceWatching < watchingCount
 266    && (lits[watching[pIndiceWatching]] ^ 1) != p)
 267  197692266 pIndiceWatching++;
 268  115955700 int pIndice = watching[pIndiceWatching];
 269   
 270    assert p == (lits[pIndice] ^ 1);
 271    assert watched[pIndice];
 272   
 273    // Recherche du coefficient maximal parmi ceux des litt???raux
 274    // observ???s
 275  115955700 BigInteger maxCoef = BigInteger.ZERO;
 276  115955700 int maxIndice = 0;
 277  115955700 for (int i = 0; i < watchingCount; i++)
 278  432872455 if (coefs[watching[i]].compareTo(maxCoef) > 0
 279    && watching[i] != pIndice) {
 280  116315933 maxCoef = coefs[watching[i]];
 281  116315933 maxIndice = 0;
 282    }
 283   
 284    assert learnt || maxCoef.signum() != 0;
 285    // DLB assert maxCoef!=0;
 286   
 287    // Recherche de la compensation
 288  115955700 int ind;
 289  115955700 if (watchingCount >= size())
 290  35387453 ind = lits.length;
 291    else {
 292  80568247 ind = 0;
 293  80568247 while (ind < lits.length
 294    && watchCumul.subtract(coefs[pIndice]).subtract(maxCoef)
 295    .compareTo(degree) < 0) {
 296  735091195 if (!voc.isFalsified(lits[ind]) && !watched[ind]) {
 297  45778841 watchCumul = watchCumul.add(coefs[ind]);
 298  45778841 watched[ind] = true;
 299    assert watchingCount < size();
 300  45778841 watching[watchingCount++] = ind;
 301  45778841 voc.watch(lits[ind] ^ 1, this);
 302    // Si on obtient un nouveau coefficient maximum
 303  45778841 if (coefs[ind].compareTo(maxCoef) > 0)
 304  8579 maxCoef = coefs[ind];
 305    }
 306  735091195 ind++;
 307    }
 308    }
 309    assert nbOfWatched() == watchingCount;
 310   
 311    // Effectuer les propagations, return si l'une est impossible
 312  115955700 if (watchCumul.subtract(coefs[pIndice]).compareTo(degree) < 0) {
 313  0 voc.watch(p, this);
 314    assert watched[pIndice];
 315    assert !isSatisfiable();
 316  0 return false;
 317  115955700 } else if (ind >= lits.length) {
 318   
 319    assert watchingCount != 0;
 320  70644646 for (int i = 0; i < watchingCount; i++) {
 321  301999338 if (watchCumul.subtract(coefs[pIndice]).subtract(
 322    coefs[watching[i]]).compareTo(degree) < 0
 323    && i != pIndiceWatching) {
 324  222127548 if (!voc.isSatisfied(lits[watching[i]])&&!s.enqueue(lits[watching[i]], this)) {
 325  5169654 voc.watch(p, this);
 326    assert !isSatisfiable();
 327  5169654 return false;
 328    }
 329    }
 330    }
 331    // Si propagation ajoute la contrainte aux undos de p, conserver p
 332  65474992 voc.undos(p).push(this);
 333    }
 334   
 335    // sinon p peut sortir de la liste de watched
 336  110786046 watched[pIndice] = false;
 337  110786046 watchCumul = watchCumul.subtract(coefs[pIndice]);
 338  110786046 watching[pIndiceWatching] = watching[--watchingCount];
 339   
 340    assert watchingCount != 0;
 341    assert nbOfWatched() == watchingCount;
 342   
 343  110786046 return true;
 344    }
 345   
 346    /**
 347    * Enl???ve une contrainte du prouveur
 348    */
 349  34623 public void remove() {
 350  34623 for (int i = 0; i < watchingCount; i++) {
 351  70119 voc.watches(lits[watching[i]] ^ 1).remove(this);
 352  70119 this.watched[this.watching[i]] = false;
 353    }
 354  34623 watchingCount = 0;
 355    assert nbOfWatched() == watchingCount;
 356    }
 357   
 358    /**
 359    * M???thode appel???e lors du backtrack
 360    *
 361    * @param p
 362    * un litt???ral d???saffect???
 363    */
 364  65464183 public void undo(int p) {
 365  65464183 voc.watch(p, this);
 366  65464183 int pIndice = 0;
 367  65464183 while ((lits[pIndice] ^ 1) != p)
 368  278043138 pIndice++;
 369   
 370    assert pIndice < lits.length;
 371   
 372  65464183 watchCumul = watchCumul.add(coefs[pIndice]);
 373   
 374    assert watchingCount == nbOfWatched();
 375   
 376  65464183 watched[pIndice] = true;
 377  65464183 watching[watchingCount++] = pIndice;
 378   
 379    assert watchingCount == nbOfWatched();
 380    }
 381   
 382    /**
 383    *
 384    */
 385  0 public static WatchPb watchPbNew(ILits voc, IVecInt lits, IVecInt coefs,
 386    boolean moreThan, int degree) {
 387  0 return new MinWatchPb(voc, lits, toVecBigInt(coefs), moreThan,
 388    toBigInt(degree));
 389    }
 390   
 391    /**
 392    *
 393    */
 394  33226 public static WatchPb watchPbNew(ILits voc, IVecInt lits,
 395    IVec<BigInteger> coefs, boolean moreThan, BigInteger degree) {
 396  33226 return new MinWatchPb(voc, lits, coefs, moreThan, degree);
 397    }
 398    }
 
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.