Clover coverage report -
Coverage timestamp: jeu. sept. 29 2005 23:57:39 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 460   Methods: 20
NCLOC: 212   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
MinWatchCard.java 64,1% 64,2% 50% 62,8%
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.card;
 27   
 28    import java.io.Serializable;
 29   
 30    import org.sat4j.minisat.core.Constr;
 31    import org.sat4j.minisat.core.ILits;
 32    import org.sat4j.minisat.core.Undoable;
 33    import org.sat4j.minisat.core.UnitPropagationListener;
 34    import org.sat4j.specs.ContradictionException;
 35    import org.sat4j.specs.IVecInt;
 36   
 37    public class MinWatchCard implements Constr, Undoable, Serializable {
 38   
 39    private static final long serialVersionUID = 1L;
 40   
 41    public static final boolean ATLEAST = true;
 42   
 43    /**
 44    * Degr? de la contrainte de cardinalit?
 45    */
 46    private int degree;
 47   
 48    /**
 49    * Liste des litt?raux de la contrainte
 50    */
 51    private int[] lits;
 52   
 53    /**
 54    * D?termine si c'est une in?galit? sup?rieure ou ?gale
 55    */
 56    private boolean moreThan;
 57   
 58    /**
 59    * Somme des coefficients des litt?raux observ?s
 60    */
 61    private int watchCumul;
 62   
 63    /**
 64    * Vocabulaire de la contrainte
 65    */
 66    private ILits voc;
 67   
 68    /**
 69    * Constructeur de clause accessible par minWatchCard
 70    *
 71    * @param voc
 72    * vocabulaire employ? par la contrainte
 73    * @param ps
 74    * vecteur contenant la liste des litt?raux de la contrainte
 75    * @param moreThan
 76    * true si la contrainte est sup?rieure ou ?gale
 77    * @param degree
 78    * le degr? de la contrainte
 79    */
 80  249266 private MinWatchCard(ILits voc, IVecInt ps, boolean moreThan, int degree) {
 81    // On met en place les valeurs
 82  249266 this.voc = voc;
 83  249266 this.degree = degree;
 84  249266 this.moreThan = moreThan;
 85   
 86    // On simplifie ps
 87  249266 int[] index = new int[voc.nVars() * 2 + 2];
 88  249266 for (int i = 0; i < index.length; i++)
 89  481099300 index[i] = 0;
 90    // On repertorie les litt?raux utiles
 91  249266 for (int i = 0; i < ps.size(); i++) {
 92  767399 if (index[ps.get(i) ^ 1] != 0) {
 93  13 index[ps.get(i) ^ 1]--;
 94    } else {
 95  767386 index[ps.get(i)]++;
 96    }
 97    }
 98    // On supprime les litt?raux inutiles
 99  249266 int ind = 0;
 100  249266 while (ind < ps.size()) {
 101  767399 if (index[ps.get(ind)] > 0) {
 102  767373 index[ps.get(ind)]--;
 103  767373 ind++;
 104    } else {
 105  26 if ((ps.get(ind) & 1) != 0)
 106  13 this.degree--;
 107  26 ps.set(ind, ps.last());
 108  26 ps.pop();
 109    }
 110    }
 111   
 112    // On copie les litt?raux de la contrainte
 113  249266 lits = new int[ps.size()];
 114  249266 ps.moveTo(lits);
 115   
 116    // On normalise la contrainte au sens de Barth
 117  249266 normalize();
 118   
 119    }
 120   
 121    /**
 122    * Calcule la cause de l'affection d'un litt?ral
 123    *
 124    * @param p
 125    * un litt?ral falsifi? (ou Lit.UNDEFINED)
 126    * @param outReason
 127    * vecteur de litt?raux ? remplir
 128    * @see Constr#calcReason(int p, IVecInt outReason)
 129    */
 130  24416258 public void calcReason(int p, IVecInt outReason) {
 131    // TODO calcReason: v?rifier par rapport ? l'article
 132    // Pour chaque litt?ral
 133  24416258 for (int i = 0; i < lits.length; i++) {
 134    // Si il est falsifi?
 135  108752714 if (voc.isFalsified(lits[i])) {
 136    // On ajoute sa n?gation au vecteur
 137  87117107 outReason.push(lits[i] ^ 1);
 138    }
 139    }
 140    }
 141   
 142    /**
 143    * Obtenir la valeur de l'activit? de la contrainte
 144    *
 145    * @return la valeur de l'activit? de la contrainte
 146    * @see Constr#getActivity()
 147    */
 148  0 public double getActivity() {
 149    // TODO getActivity
 150  0 return 0;
 151    }
 152   
 153    /**
 154    * Incr?mente la valeur de l'activit? de la contrainte
 155    *
 156    * @param claInc
 157    * incr?ment de l'activit? de la contrainte
 158    * @see Constr#incActivity(double claInc)
 159    */
 160  0 public void incActivity(double claInc) {
 161    // TODO incActivity
 162    }
 163   
 164    /**
 165    * D?termine si la contrainte est apprise
 166    *
 167    * @return true si la contrainte est apprise, false sinon
 168    * @see Constr#learnt()
 169    */
 170  24416258 public boolean learnt() {
 171    // TODO learnt
 172  24416258 return false;
 173    }
 174   
 175    /**
 176    * Met ? jour les affectations
 177    *
 178    * @param voc
 179    * vocabulaire employ?
 180    * @param ps
 181    * liste des litt?raux concern?s
 182    * @return influence des changements sur le degr?
 183    */
 184  249266 private static int linearisation(ILits voc, IVecInt ps) {
 185    // Stockage de l'influence des modifications
 186  249266 int modif = 0;
 187   
 188  249266 for (int i = 0; i < ps.size();) {
 189    // on verifie si le litteral est affecte
 190  767399 if (!voc.isUnassigned(ps.get(i))) {
 191    // Si le litteral est satisfait,
 192    // ?a revient ? baisser le degr?
 193  0 if (voc.isSatisfied(ps.get(i))) {
 194  0 modif--;
 195    }
 196    // dans tous les cas, s'il est assign?,
 197    // on enleve le ieme litteral
 198  0 ps.set(i, ps.last());
 199  0 ps.pop();
 200    } else {
 201    // on passe au litt?ral suivant
 202  767399 i++;
 203    }
 204    }
 205   
 206    // DLB: inutile?
 207    // ps.shrinkTo(nbElement);
 208   
 209  249266 return modif;
 210    }
 211   
 212    /**
 213    * La contrainte est la cause d'une propagation unitaire
 214    *
 215    * @return true si c'est le cas, false sinon
 216    * @see Constr#locked()
 217    */
 218  0 public boolean locked() {
 219    // TODO locked
 220  0 return true;
 221    }
 222   
 223    /**
 224    * Permet la cr?ation de contrainte de cardinalit? ? observation minimale
 225    *
 226    * @param s
 227    * outil pour la propagation des litt?raux
 228    * @param voc
 229    * vocabulaire utilis? par la contrainte
 230    * @param ps
 231    * liste des litt?raux de la nouvelle contrainte
 232    * @param moreThan
 233    * d?termine si c'est une sup?rieure ou ?gal ? l'origine
 234    * @param degree
 235    * fournit le degr? de la contrainte
 236    * @return une nouvelle clause si tout va bien, null sinon
 237    * @throws ContradictionException
 238    */
 239  249266 public static MinWatchCard minWatchCardNew(UnitPropagationListener s,
 240    ILits voc, IVecInt ps, boolean moreThan, int degree)
 241    throws ContradictionException {
 242   
 243  249266 degree += linearisation(voc, ps);
 244   
 245  249266 if (ps.size() == 0) {
 246  0 throw new ContradictionException("Cr?ation d'une clause vide");
 247  249266 } else if (ps.size() == degree) {
 248  0 for (int i = 0; i < ps.size(); i++)
 249  0 if (!s.enqueue(ps.get(i))) {
 250  0 throw new ContradictionException(
 251    "Contradiction avec le litt?ral impliqu?.");
 252    }
 253  0 return null;
 254    }
 255   
 256    // La contrainte est maintenant cr??e
 257  249266 MinWatchCard retour = new MinWatchCard(voc, ps, moreThan, degree);
 258   
 259  249266 retour.normalize();
 260   
 261  249266 if (degree <= 0)
 262  0 return null;
 263   
 264    // On observe degre+1 litt?raux
 265  249266 int indSwap = retour.lits.length;
 266  249266 int tmpInt;
 267  249266 for (int i = 0; i <= retour.degree && i < indSwap; i++) {
 268  498517 while (voc.isFalsified(retour.lits[i]) && --indSwap <= i) {
 269  0 tmpInt = retour.lits[i];
 270  0 retour.lits[i] = retour.lits[indSwap];
 271  0 retour.lits[indSwap] = tmpInt;
 272    }
 273   
 274    // Si le litt?ral est observable
 275  498517 if (!voc.isFalsified(retour.lits[i])) {
 276  498517 retour.watchCumul++;
 277  498517 voc.watch(retour.lits[i] ^ 1, retour);
 278    }
 279    }
 280   
 281    // Si on observe pas suffisament
 282  249266 if (retour.watchCumul <= retour.degree) {
 283    // Si l'on a les litt?rux impliqu?s
 284  2 if (retour.watchCumul == retour.degree) {
 285  2 for (int i = 0; i < retour.lits.length; i++)
 286  0 if (!s.enqueue(retour.lits[i])) {
 287  0 throw new ContradictionException(
 288    "Contradiction avec le litt?ral impliqu?.");
 289    }
 290  2 return null;
 291    }
 292  0 throw new ContradictionException("Contrainte non-satisfiable");
 293    }
 294   
 295  249264 return retour;
 296    }
 297   
 298    /**
 299    * On normalise la contrainte au sens de Barth
 300    */
 301  498532 public void normalize() {
 302    // Gestion du signe
 303  498532 if (!moreThan) {
 304    // On multiplie le degr? par -1
 305  0 this.degree = 0 - this.degree;
 306    // On r?vise chaque litt?ral
 307  0 for (int indLit = 0; indLit < lits.length; indLit++) {
 308  0 lits[indLit] = lits[indLit] ^ 1;
 309  0 this.degree++;
 310    }
 311  0 this.moreThan = true;
 312    }
 313    }
 314   
 315    /**
 316    * Propagation de la valeur de v?rit? d'un litt?ral falsifi?
 317    *
 318    * @param s
 319    * outil pour la propagation des litt?raux
 320    * @param p
 321    * le litt?ral propag?
 322    * @return false si inconsistance d?t?ct?e, true sinon
 323    */
 324  102228277 public boolean propagate(UnitPropagationListener s, int p) {
 325   
 326    // Si la contrainte est responsable de propagation unitaire
 327  102228277 if (watchCumul == degree) {
 328  0 voc.watch(p, this);
 329  0 return false;
 330    }
 331   
 332    // Recherche du litt?ral falsifi?
 333  102228277 int indFalsified = -1;
 334  102228277 while ((lits[++indFalsified] ^ 1) != p)
 335    ;
 336   
 337    // Recherche du litt?ral swap
 338  102228277 int indSwap = degree + 1;
 339  102228277 while (indSwap < lits.length && voc.isFalsified(lits[indSwap]))
 340  130709938 indSwap++;
 341   
 342    // Mise ? jour de la contrainte
 343  102228277 if (indSwap == lits.length) {
 344    // Si aucun litt?ral n'a ?t? trouv?
 345  92275136 voc.watch(p, this);
 346    // La limite est atteinte
 347  92275136 watchCumul--;
 348    assert watchCumul == degree;
 349  92275136 voc.undos(p).push(this);
 350   
 351    // On met en queue les litt?raux impliqu?s
 352  92275136 for (int i = 0; i <= degree; i++)
 353  184350418 if ((p != (lits[i] ^ 1)) &&!s.enqueue(lits[i], this))
 354  2780692 return false;
 355   
 356  89494444 return true;
 357    }
 358    // Si un litt?ral a ?t? trouv? on les ?change
 359  9953141 int tmpInt = lits[indSwap];
 360  9953141 lits[indSwap] = lits[indFalsified];
 361  9953141 lits[indFalsified] = tmpInt;
 362   
 363    // On observe le nouveau litt?ral
 364  9953141 voc.watch(tmpInt ^ 1, this);
 365   
 366  9953141 return true;
 367    }
 368   
 369    /**
 370    * Enl?ve une contrainte du prouveur
 371    */
 372  13516 public void remove() {
 373  13516 for (int i = 0; i <= degree; i++) {
 374  27032 voc.watches(lits[i] ^ 1).remove(this);
 375    }
 376    }
 377   
 378    /**
 379    * Permet le r??chantillonage de l'activit? de la contrainte
 380    *
 381    * @param d
 382    * facteur d'ajustement
 383    */
 384  0 public void rescaleBy(double d) {
 385    // TODO rescaleBy
 386    }
 387   
 388    /**
 389    * Simplifie la contrainte
 390    *
 391    * @return true si la contrainte est satisfaite, false sinon
 392    */
 393  417164 public boolean simplify() {
 394    // Calcule de la valeur actuelle
 395  417164 for (int i = 0, count = 0; i < lits.length; i++)
 396  1405717 if (voc.isSatisfied(lits[i]))
 397  13517 if (++count == degree)
 398  13516 return true;
 399   
 400  403648 return false;
 401    }
 402   
 403    /**
 404    * Cha?ne repr?sentant la contrainte
 405    *
 406    * @return Cha?ne repr?sentant la contrainte
 407    */
 408  0 @Override
 409    public String toString() {
 410  0 StringBuffer stb = new StringBuffer();
 411   
 412  0 if (lits.length > 0) {
 413  0 if (voc.isUnassigned(lits[0])) {
 414  0 stb.append(this.lits[0]);
 415  0 stb.append(" ");
 416    }
 417  0 for (int i = 1; i < lits.length; i++) {
 418  0 if (voc.isUnassigned(lits[i])) {
 419  0 stb.append(" + ");
 420  0 stb.append(this.lits[i]);
 421  0 stb.append(" ");
 422    }
 423    }
 424  0 stb.append(">= ");
 425  0 stb.append(this.degree);
 426    }
 427  0 return stb.toString();
 428    }
 429   
 430    /**
 431    * M?thode appel?e lors du backtrack
 432    *
 433    * @param p
 434    * un litt?ral d?saffect?
 435    */
 436  92272985 public void undo(int p) {
 437    // Le litt?ral observ? et falsifi? devient non assign?
 438  92272985 watchCumul++;
 439    }
 440   
 441  0 public void setLearnt() {
 442  0 throw new UnsupportedOperationException();
 443    }
 444   
 445  0 public void register() {
 446  0 throw new UnsupportedOperationException();
 447    }
 448   
 449  0 public int size() {
 450  0 return lits.length;
 451    }
 452   
 453  0 public int get(int i) {
 454  0 return lits[i];
 455    }
 456   
 457  0 public void assertConstraint(UnitPropagationListener s) {
 458  0 throw new UnsupportedOperationException();
 459    }
 460    }
 
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.