Clover coverage report -
Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 454   Methods: 16
NCLOC: 238   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
MinWatchPb.java 88,7% 90,2% 81,2% 89,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    protected boolean[] watched;
 47   
 48    /**
 49    * Sert ??? d???terminer si la clause est watched par le litt???ral
 50    */
 51    protected int[] watching;
 52   
 53    /**
 54    * Liste des indices des litt???raux regardant la contrainte
 55    */
 56    protected 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  1259049 protected MinWatchPb(ILits voc, IDataStructurePB mpb) {
 73   
 74  1259049 super(mpb);
 75  1259049 this.voc = voc;
 76   
 77  1259049 watching = new int[this.coefs.length];
 78  1259049 watched = new boolean[this.coefs.length];
 79  1259049 activity = 0;
 80  1259049 watchCumul = BigInteger.ZERO;
 81  1259049 locked = false;
 82   
 83  1259049 watchingCount = 0;
 84   
 85    }
 86   
 87    /*
 88    * (non-Javadoc)
 89    *
 90    * @see org.sat4j.minisat.constraints.WatchPb#computeWatches()
 91    */
 92  1258939 @Override
 93    protected void computeWatches() throws ContradictionException {
 94    assert watchCumul.signum() == 0;
 95    assert watchingCount == 0;
 96  1258939 for (int i = 0; i < lits.length
 97    && watchCumul.subtract(coefs[0]).compareTo(degree) < 0; i++) {
 98  6052705 if (!voc.isFalsified(lits[i])) {
 99  3268034 voc.watch(lits[i] ^ 1, this);
 100  3268034 watching[watchingCount++] = i;
 101  3268034 watched[i] = true;
 102    // Mise ??? jour de la possibilit??? initiale
 103  3268034 watchCumul = watchCumul.add(coefs[i]);
 104    }
 105    }
 106   
 107  1258939 if (learnt)
 108  77515 watchMoreForLearntConstraint();
 109   
 110  1258939 if (watchCumul.compareTo(degree) < 0) {
 111  32 throw new ContradictionException("non satisfiable constraint");
 112    }
 113    assert nbOfWatched() == watchingCount;
 114    }
 115   
 116  77515 private void watchMoreForLearntConstraint() {
 117    // chercher tous les litteraux a regarder
 118    // par ordre de niveau decroissant
 119  77515 int free = 1;
 120  77515 int maxlevel, maxi, level;
 121   
 122  77515 while ((watchCumul.subtract(coefs[0]).compareTo(degree) < 0)
 123    && (free > 0)) {
 124  78454 free = 0;
 125    // regarder le litteral falsifie au plus bas niveau
 126  78454 maxlevel = -1;
 127  78454 maxi = -1;
 128  78454 for (int i = 0; i < lits.length; i++) {
 129  3640117 if (voc.isFalsified(lits[i]) && !watched[i]) {
 130  2944254 free++;
 131  2944254 level = voc.getLevel(lits[i]);
 132  2944254 if (level > maxlevel) {
 133  203635 maxi = i;
 134  203635 maxlevel = level;
 135    }
 136    }
 137    }
 138   
 139  78454 if (free > 0) {
 140    assert maxi >= 0;
 141  78426 voc.watch(lits[maxi] ^ 1, this);
 142  78426 watching[watchingCount++] = maxi;
 143  78426 watched[maxi] = true;
 144    // Mise ??? jour de la possibilit??? initiale
 145  78426 watchCumul = watchCumul.add(coefs[maxi]);
 146  78426 free--;
 147    assert free >= 0;
 148    }
 149    }
 150    assert lits.length == 1 || watchingCount > 1;
 151    }
 152   
 153    /*
 154    * (non-Javadoc)
 155    *
 156    * @see org.sat4j.minisat.constraints.WatchPb#computePropagation(org.sat4j.minisat.UnitPropagationListener)
 157    */
 158  1181392 @Override
 159    protected void computePropagation(UnitPropagationListener s)
 160    throws ContradictionException {
 161    // On propage si n???cessaire
 162  1181392 int ind = 0;
 163  1181392 while (ind < lits.length
 164    && watchCumul.subtract(coefs[watching[ind]]).compareTo(degree) < 0) {
 165  532 if (voc.isUnassigned(lits[ind]) && !s.enqueue(lits[ind], this)) {
 166  0 throw new ContradictionException("non satisfiable constraint");
 167    }
 168  532 ind++;
 169    }
 170    }
 171   
 172    /**
 173    * @param s
 174    * outil pour la propagation des litt???raux
 175    * @param ps
 176    * liste des litt???raux de la nouvelle contrainte
 177    * @param coefs
 178    * liste des coefficients des litt???raux de la contrainte
 179    * @param moreThan
 180    * d???termine si c'est une sup???rieure ou ???gal ??? l'origine
 181    * @param degree
 182    * fournit le degr??? de la contrainte
 183    * @return une nouvelle clause si tout va bien, ou null si un conflit est
 184    * d???tect???
 185    */
 186  499336 public static MinWatchPb minWatchPbNew(UnitPropagationListener s,
 187    ILits voc, IVecInt ps, IVecInt coefs, boolean moreThan, int degree)
 188    throws ContradictionException {
 189  499336 return minWatchPbNew(s, voc, ps, toVecBigInt(coefs), moreThan,
 190    toBigInt(degree));
 191    }
 192   
 193    /**
 194    * @param s
 195    * outil pour la propagation des litt???raux
 196    * @param ps
 197    * liste des litt???raux de la nouvelle contrainte
 198    * @param coefs
 199    * liste des coefficients des litt???raux de la contrainte
 200    * @param moreThan
 201    * d???termine si c'est une sup???rieure ou ???gal ??? l'origine
 202    * @param degree
 203    * fournit le degr??? de la contrainte
 204    * @return une nouvelle clause si tout va bien, ou null si un conflit est
 205    * d???tect???
 206    */
 207  778348 public static MinWatchPb minWatchPbNew(UnitPropagationListener s,
 208    ILits voc, IVecInt ps, IVec<BigInteger> coefs, boolean moreThan,
 209    BigInteger degree) throws ContradictionException {
 210    // Il ne faut pas modifier les param?tres
 211  778348 VecInt litsVec = new VecInt(ps.size());
 212  778348 IVec<BigInteger> coefsVec = new Vec<BigInteger>(coefs.size());
 213  778348 ps.copyTo(litsVec);
 214  778348 coefs.copyTo(coefsVec);
 215   
 216    // Ajouter les simplifications quand la structure sera d???finitive
 217  778348 IDataStructurePB mpb = niceParameters(litsVec, coefsVec, moreThan,
 218    degree, voc);
 219   
 220  778348 if (mpb == null)
 221  0 return null;
 222   
 223  778348 MinWatchPb outclause = new MinWatchPb(voc, mpb);
 224   
 225  778348 if (outclause.degree.signum() <= 0) {
 226  0 return null;
 227    }
 228   
 229  778348 outclause.computeWatches();
 230   
 231  778331 outclause.computePropagation(s);
 232   
 233  778331 return outclause;
 234   
 235    }
 236   
 237    /**
 238    * @param s
 239    * a unit propagation listener
 240    * @param voc
 241    * the vocabulary
 242    * @param mpb
 243    * the PB constraint to normalize.
 244    * @return a new PB contraint or null if a trivial inconsistency is detected.
 245    */
 246  123264 public static MinWatchPb normalizedMinWatchPbNew(UnitPropagationListener s,
 247    ILits voc, IDataStructurePB mpb) throws ContradictionException {
 248    // Il ne faut pas modifier les param?tres
 249  123264 MinWatchPb outclause = new MinWatchPb(voc, mpb);
 250   
 251  123264 if (outclause.degree.signum() <= 0) {
 252  0 return null;
 253    }
 254   
 255  123264 outclause.computeWatches();
 256   
 257  123264 outclause.computePropagation(s);
 258   
 259  123264 return outclause;
 260   
 261    }
 262   
 263    /**
 264    * Nombre de litt???raux actuellement observ???
 265    *
 266    * @return nombre de litt???raux regard???s
 267    */
 268  785068731 protected int nbOfWatched() {
 269  785068731 int retour = 0;
 270  785068731 for (int ind = 0; ind < this.watched.length; ind++) {
 271  1400433737 for (int i = 0; i < watchingCount; i++)
 272  1863184644 if (watching[i] == ind)
 273    assert watched[ind];
 274  1400433737 retour += (this.watched[ind]) ? 1 : 0;
 275    }
 276  785068731 return retour;
 277    }
 278   
 279    /**
 280    * Propagation de la valeur de v???rit??? d'un litt???ral falsifi???
 281    *
 282    * @param s
 283    * un prouveur
 284    * @param p
 285    * le litt???ral propag??? (il doit etre falsifie)
 286    * @return false ssi une inconsistance est d???t???ct???e
 287    */
 288  215828087 public boolean propagate(UnitPropagationListener s, int p) {
 289    assert nbOfWatched() == watchingCount;
 290    assert watchingCount > 1;
 291   
 292    // Recherche de l'indice du litt???ral p
 293  215828087 int pIndiceWatching = 0;
 294  215828087 while (pIndiceWatching < watchingCount
 295    && (lits[watching[pIndiceWatching]] ^ 1) != p)
 296  365252625 pIndiceWatching++;
 297  215828087 int pIndice = watching[pIndiceWatching];
 298   
 299    assert p == (lits[pIndice] ^ 1);
 300    assert watched[pIndice];
 301   
 302    // Recherche du coefficient maximal parmi ceux des litt???raux
 303    // observ???s
 304  215828087 BigInteger maxCoef = maximalCoefficient(pIndice);
 305   
 306    // Recherche de la compensation
 307  215828087 maxCoef = updateWatched(maxCoef, pIndice);
 308   
 309  215828087 BigInteger upWatchCumul = watchCumul.subtract(coefs[pIndice]);
 310    assert nbOfWatched() == watchingCount;
 311   
 312    // Effectuer les propagations, return si l'une est impossible
 313  215828087 if (upWatchCumul.compareTo(degree) < 0) {
 314    // conflit
 315  0 voc.watch(p, this);
 316    assert watched[pIndice];
 317    assert !isSatisfiable();
 318  0 return false;
 319  215828087 } else if (upWatchCumul.compareTo(degree.add(maxCoef)) < 0) {
 320   
 321    assert watchingCount != 0;
 322  79853005 BigInteger limit = upWatchCumul.subtract(degree);
 323  79853005 for (int i = 0; i < watchingCount; i++) {
 324  421732184 if (limit.compareTo(coefs[watching[i]]) < 0
 325    && i != pIndiceWatching
 326    && !voc.isSatisfied(lits[watching[i]])
 327    && !s.enqueue(lits[watching[i]], this)) {
 328  7790029 voc.watch(p, this);
 329    assert !isSatisfiable();
 330  7790029 return false;
 331    }
 332    }
 333    // Si propagation ajoute la contrainte aux undos de p, conserver p
 334  72062976 voc.undos(p).push(this);
 335    }
 336   
 337    // sinon p peut sortir de la liste de watched
 338  208038058 watched[pIndice] = false;
 339  208038058 watchCumul = upWatchCumul;
 340  208038058 watching[pIndiceWatching] = watching[--watchingCount];
 341   
 342    assert watchingCount != 0;
 343    assert nbOfWatched() == watchingCount;
 344   
 345  208038058 return true;
 346    }
 347   
 348    /**
 349    * Enl???ve une contrainte du prouveur
 350    */
 351  0 public void remove() {
 352  0 for (int i = 0; i < watchingCount; i++) {
 353  0 voc.watches(lits[watching[i]] ^ 1).remove(this);
 354  0 this.watched[this.watching[i]] = false;
 355    }
 356  0 watchingCount = 0;
 357    assert nbOfWatched() == watchingCount;
 358    }
 359   
 360    /**
 361    * M???thode appel???e lors du backtrack
 362    *
 363    * @param p
 364    * un litt???ral d???saffect???
 365    */
 366  72057796 public void undo(int p) {
 367  72057796 voc.watch(p, this);
 368  72057796 int pIndice = 0;
 369  72057796 while ((lits[pIndice] ^ 1) != p)
 370  373047553 pIndice++;
 371   
 372    assert pIndice < lits.length;
 373   
 374  72057796 watchCumul = watchCumul.add(coefs[pIndice]);
 375   
 376    assert watchingCount == nbOfWatched();
 377   
 378  72057796 watched[pIndice] = true;
 379  72057796 watching[watchingCount++] = pIndice;
 380   
 381    assert watchingCount == nbOfWatched();
 382    }
 383   
 384    /**
 385    *
 386    */
 387  0 public static WatchPb watchPbNew(ILits voc, IVecInt lits, IVecInt coefs,
 388    boolean moreThan, int degree) {
 389  0 return watchPbNew(voc, lits, toVecBigInt(coefs), moreThan,
 390    toBigInt(degree));
 391    }
 392   
 393    /**
 394    *
 395    */
 396  51574 public static WatchPb watchPbNew(ILits voc, IVecInt lits,
 397    IVec<BigInteger> coefs, boolean moreThan, BigInteger degree) {
 398  51574 IDataStructurePB mpb = null;
 399  51574 mpb = niceCheckedParameters(lits, coefs, moreThan, degree, voc);
 400  51574 return new MinWatchPb(voc, mpb);
 401    }
 402   
 403    /**
 404    *
 405    */
 406  0 public static WatchPb normalizedWatchPbNew(ILits voc, IDataStructurePB mpb)
 407    throws ContradictionException {
 408  0 return new MinWatchPb(voc, mpb);
 409    }
 410   
 411    /**
 412    * returns the maximal coefficient for the watched literals
 413    *
 414    * @param pIndice
 415    * propagated literal : its coefficient is excluded from the
 416    * search of the maximal coefficient
 417    * @return
 418    */
 419  123478339 protected BigInteger maximalCoefficient(int pIndice) {
 420  123478339 BigInteger maxCoef = BigInteger.ZERO;
 421  123478339 for (int i = 0; i < watchingCount; i++)
 422  416917457 if (coefs[watching[i]].compareTo(maxCoef) > 0
 423    && watching[i] != pIndice) {
 424  124886165 maxCoef = coefs[watching[i]];
 425    }
 426   
 427    assert learnt || maxCoef.signum() != 0;
 428    // DLB assert maxCoef!=0;
 429  123478339 return maxCoef;
 430    }
 431   
 432  123478339 protected BigInteger updateWatched(BigInteger mc, int pIndice) {
 433  123478339 BigInteger maxCoef = mc;
 434  123478339 if (watchingCount < size()) {
 435  105815349 BigInteger upWatchCumul = watchCumul.subtract(coefs[pIndice]);
 436  105815349 for (int ind = 0; ind < lits.length
 437    && upWatchCumul.compareTo(degree.add(maxCoef)) < 0; ind++) {
 438  899086649 if (!voc.isFalsified(lits[ind]) && !watched[ind]) {
 439  83412385 upWatchCumul = upWatchCumul.add(coefs[ind]);
 440  83412385 watched[ind] = true;
 441    assert watchingCount < size();
 442  83412385 watching[watchingCount++] = ind;
 443  83412385 voc.watch(lits[ind] ^ 1, this);
 444    // Si on obtient un nouveau coefficient maximum
 445  83412385 if (coefs[ind].compareTo(maxCoef) > 0)
 446  71082 maxCoef = coefs[ind];
 447    }
 448    }
 449  105815349 watchCumul = upWatchCumul.add(coefs[pIndice]);
 450    }
 451  123478339 return maxCoef;
 452    }
 453   
 454    }
 
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.