Clover coverage report -
Coverage timestamp: jeu. sept. 29 2005 23:57:39 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 407   Methods: 19
NCLOC: 186   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
MaxWatchCard.java 60,3% 60,6% 42,1% 58,6%
coverage coverage
 1    /*
 2    * MiniSAT in Java, a Java based-SAT framework
 3    * Copyright (C) 2004 Daniel Le Berre
 4    *
 5    * Based on the original minisat specification from:
 6    *
 7    * An extensible SAT solver. Niklas E?n and Niklas S?rensson.
 8    * Proceedings of the Sixth International Conference on Theory
 9    * and Applications of Satisfiability Testing, LNCS 2919,
 10    * pp 502-518, 2003.
 11    *
 12    * This library is free software; you can redistribute it and/or
 13    * modify it under the terms of the GNU Lesser General Public
 14    * License as published by the Free Software Foundation; either
 15    * version 2.1 of the License, or (at your option) any later version.
 16    *
 17    * This library is distributed in the hope that it will be useful,
 18    * but WITHOUT ANY WARRANTY; without even the implied warranty of
 19    * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
 20    * Lesser General Public License for more details.
 21    *
 22    * You should have received a copy of the GNU Lesser General Public
 23    * License along with this library; if not, write to the Free Software
 24    * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
 25    *
 26    */
 27    package org.sat4j.minisat.constraints.card;
 28   
 29    import java.io.Serializable;
 30   
 31    import org.sat4j.minisat.core.Constr;
 32    import org.sat4j.minisat.core.ILits;
 33    import org.sat4j.minisat.core.Undoable;
 34    import org.sat4j.minisat.core.UnitPropagationListener;
 35    import org.sat4j.specs.ContradictionException;
 36    import org.sat4j.specs.IVecInt;
 37   
 38    public class MaxWatchCard implements Constr, Undoable, Serializable {
 39   
 40    private static final long serialVersionUID = 1L;
 41   
 42    /**
 43    * Degr? de la contrainte de cardinalit?
 44    */
 45    private int degree;
 46   
 47    /**
 48    * Liste des litt?raux de la contrainte
 49    */
 50    private int[] lits;
 51   
 52    /**
 53    * D?termine si c'est une in?galit? sup?rieure ou ?gale
 54    */
 55    private boolean moreThan;
 56   
 57    /**
 58    * Somme des coefficients des litt?raux observ?s
 59    */
 60    private int watchCumul;
 61   
 62    /**
 63    * Vocabulaire de la contrainte
 64    */
 65    private ILits voc;
 66   
 67    /**
 68    * Constructeur de base cr?ant des contraintes vides
 69    *
 70    * @param size
 71    * nombre de litt?raux de la contrainte
 72    * @param learnt
 73    * indique si la contrainte est apprise
 74    */
 75  249266 private MaxWatchCard(ILits voc, IVecInt ps, boolean moreThan, int degree) {
 76   
 77    // On met en place les valeurs
 78  249266 this.voc = voc;
 79  249266 this.degree = degree;
 80  249266 this.moreThan = moreThan;
 81   
 82    // On simplifie ps
 83  249266 int[] index = new int[voc.nVars() * 2 + 2];
 84  249266 for (int i = 0; i < index.length; i++)
 85  481099300 index[i] = 0;
 86    // On repertorie les litt?raux utiles
 87  249266 for (int i = 0; i < ps.size(); i++) {
 88  767399 if (index[ps.get(i) ^ 1] != 0) {
 89  13 index[ps.get(i) ^ 1]--;
 90    } else {
 91  767386 index[ps.get(i)]++;
 92    }
 93    }
 94    // On supprime les litt?raux inutiles
 95  249266 int ind = 0;
 96  249266 while (ind < ps.size()) {
 97  767399 if (index[ps.get(ind)] > 0) {
 98  767373 index[ps.get(ind)]--;
 99  767373 ind++;
 100    } else {
 101  26 if ((ps.get(ind) & 1) != 0)
 102  13 this.degree--;
 103  26 ps.set(ind, ps.last());
 104  26 ps.pop();
 105    }
 106    }
 107   
 108    // On copie les litt?raux de la contrainte
 109  249266 lits = new int[ps.size()];
 110  249266 ps.moveTo(lits);
 111   
 112    // On normalise la contrainte au sens de Barth
 113  249266 normalize();
 114   
 115    // Mise en place de l'observation maximale
 116  249266 watchCumul = 0;
 117   
 118    // On observe les litt?raux non falsifi?
 119  249266 for (int i = 0; i < lits.length; i++) {
 120    // Rappel: les ?l?ments falsifi?s ne seront jamais d?pil?s
 121  767373 if (!voc.isFalsified(lits[i])) {
 122  767373 watchCumul++;
 123  767373 voc.watch(lits[i] ^ 1, this);
 124    }
 125    }
 126    }
 127   
 128    /**
 129    * Calcule la cause de l'affection d'un litt?ral
 130    *
 131    * @param p
 132    * un litt?ral falsifi? (ou Lit.UNDEFINED)
 133    * @param outReason
 134    * vecteur de litt?raux ? remplir
 135    * @see Constr#calcReason(int p, IVecInt outReason)
 136    */
 137  24921589 public void calcReason(int p, IVecInt outReason) {
 138    // TODO calcReason: v?rifier par rapport ? l'article
 139    // Pour chaque litt?ral
 140  24921589 for (int i = 0; i < lits.length; i++) {
 141    // Si il est falsifi?
 142  110032976 if (voc.isFalsified(lits[i])) {
 143    // On ajoute sa n?gation au vecteur
 144  87893499 outReason.push(lits[i] ^ 1);
 145    }
 146    }
 147    }
 148   
 149    /**
 150    * Obtenir la valeur de l'activit? de la contrainte
 151    *
 152    * @return la valeur de l'activit? de la contrainte
 153    * @see Constr#getActivity()
 154    */
 155  0 public double getActivity() {
 156    // TODO getActivity
 157  0 return 0;
 158    }
 159   
 160    /**
 161    * Incr?mente la valeur de l'activit? de la contrainte
 162    *
 163    * @param claInc
 164    * incr?ment de l'activit? de la contrainte
 165    * @see Constr#incActivity(double claInc)
 166    */
 167  0 public void incActivity(double claInc) {
 168    // TODO incActivity
 169    }
 170   
 171    /**
 172    * D?termine si la contrainte est apprise
 173    *
 174    * @return true si la contrainte est apprise, false sinon
 175    * @see Constr#learnt()
 176    */
 177  24921589 public boolean learnt() {
 178    // TODO learnt
 179  24921589 return false;
 180    }
 181   
 182    /**
 183    * La contrainte est la cause d'une propagation unitaire
 184    *
 185    * @return true si c'est le cas, false sinon
 186    * @see Constr#locked()
 187    */
 188  0 public boolean locked() {
 189    // TODO locked
 190  0 return true;
 191    }
 192   
 193    /**
 194    * Permet la cr?ation de contrainte de cardinalit? ? observation minimale
 195    *
 196    * @param s
 197    * outil pour la propagation des litt?raux
 198    * @param voc
 199    * vocabulaire utilis? par la contrainte
 200    * @param ps
 201    * liste des litt?raux de la nouvelle contrainte
 202    * @param moreThan
 203    * d?termine si c'est une sup?rieure ou ?gal ? l'origine
 204    * @param degree
 205    * fournit le degr? de la contrainte
 206    * @return une nouvelle clause si tout va bien, null sinon
 207    * @throws ContradictionException
 208    */
 209  249266 public static MaxWatchCard maxWatchCardNew(UnitPropagationListener s,
 210    ILits voc, IVecInt ps, boolean moreThan, int degree)
 211    throws ContradictionException {
 212   
 213  249266 MaxWatchCard outclause = null;
 214   
 215    // La contrainte ne doit pas ?tre vide
 216  249266 if (ps.size() == 0) {
 217  0 throw new ContradictionException("Cr?ation d'une clause vide");
 218  249266 } else if (ps.size() == degree) {
 219  0 for (int i = 0; i < ps.size(); i++)
 220  0 if (!s.enqueue(ps.get(i))) {
 221  0 throw new ContradictionException(
 222    "Contradiction avec le litt?ral impliqu?.");
 223    }
 224  0 return null;
 225    }
 226   
 227    // On cree la contrainte
 228  249266 outclause = new MaxWatchCard(voc, ps, moreThan, degree);
 229   
 230    // Si le degr? est insufisant
 231  249266 if (outclause.degree <= 0)
 232  13 return null;
 233   
 234    // Si il n'y a aucune chance de satisfaire la contrainte
 235  249253 if (outclause.watchCumul < outclause.degree)
 236  0 throw new ContradictionException("Contrainte non-satisfiable");
 237   
 238    // Si les litt?raux observ?s sont impliqu?s
 239  249253 if (outclause.watchCumul == outclause.degree) {
 240  0 for (int i = 0; i < outclause.lits.length; i++) {
 241  0 if (!s.enqueue(outclause.lits[i])) {
 242  0 throw new ContradictionException(
 243    "Contradiction avec le litt?ral impliqu?.");
 244    }
 245    }
 246  0 return null;
 247    }
 248   
 249  249253 return outclause;
 250    }
 251   
 252    /**
 253    * On normalise la contrainte au sens de Barth
 254    */
 255  249266 public void normalize() {
 256    // Gestion du signe
 257  249266 if (!moreThan) {
 258    // On multiplie le degr? par -1
 259  0 this.degree = 0 - this.degree;
 260    // On r?vise chaque litt?ral
 261  0 for (int indLit = 0; indLit < lits.length; indLit++) {
 262  0 lits[indLit] = lits[indLit] ^ 1;
 263  0 this.degree++;
 264    }
 265  0 this.moreThan = true;
 266    }
 267    }
 268   
 269    /**
 270    * Propagation de la valeur de v?rit? d'un litt?ral falsifi?
 271    *
 272    * @param s
 273    * objet utilis? pour la propagation
 274    * @param p
 275    * le litt?ral propag? (il doit etre falsifie)
 276    * @return false ssi une inconsistance est d?t?ct?e
 277    */
 278  138856586 public boolean propagate(UnitPropagationListener s, int p) {
 279   
 280    // On observe toujours tous les litt?raux
 281  138856586 voc.watch(p, this);
 282    assert !voc.isFalsified(p);
 283   
 284    // Si le litt?ral p est impliqu?
 285  138856586 if (this.watchCumul == this.degree)
 286  2782150 return false;
 287   
 288    // On met en place la mise ? jour du compteur
 289  136074436 voc.undos(p).push(this);
 290  136074436 watchCumul--;
 291   
 292    // Si les litt?raux restant sont impliqu?s
 293  136074436 if (watchCumul == degree) {
 294  108259506 for (int ind = 0; ind < lits.length; ind++) {
 295  312887478 if (voc.isUnassigned(lits[ind])) {
 296  55014688 if (!s.enqueue(lits[ind], this)) {
 297  0 return false;
 298    }
 299    }
 300    }
 301    }
 302   
 303  136074436 return true;
 304    }
 305   
 306    /**
 307    * Enl?ve une contrainte du prouveur
 308    */
 309  0 public void remove() {
 310  0 for (int i = 0; i < lits.length; i++) {
 311  0 voc.watches(lits[i] ^ 1).remove(this);
 312    }
 313    }
 314   
 315    /**
 316    * Permet le r??chantillonage de l'activit? de la contrainte
 317    *
 318    * @param d
 319    * facteur d'ajustement
 320    */
 321  0 public void rescaleBy(double d) {
 322    // TODO Yann rescaleBy
 323  0 System.out.println("rescaleBy");
 324    }
 325   
 326    /**
 327    * Simplifie la contrainte(l'all?ge)
 328    *
 329    * @return true si la contrainte est satisfaite, false sinon
 330    */
 331  430072 public boolean simplify() {
 332   
 333  430072 int i = 0;
 334   
 335    // On esp?re le maximum de la somme
 336  430072 int curr = watchCumul;
 337   
 338    // Pour chaque litt?ral
 339  430072 while (i < this.lits.length) {
 340    // On d?cr?mente si l'espoir n'est pas fond?
 341  1517582 if (voc.isUnassigned(lits[i++])) {
 342  1455532 curr--;
 343  1455532 if (curr < this.degree)
 344  401171 return false;
 345    }
 346    }
 347   
 348  28901 return false;
 349    }
 350   
 351    /**
 352    * Cha?ne repr?sentant la contrainte
 353    *
 354    * @return Cha?ne repr?sentant la contrainte
 355    */
 356  0 @Override
 357    public String toString() {
 358  0 StringBuffer stb = new StringBuffer();
 359   
 360  0 if (lits.length > 0) {
 361  0 if (voc.isUnassigned(lits[0])) {
 362  0 stb.append(this.lits[0]);
 363  0 stb.append(" ");
 364    }
 365  0 for (int i = 1; i < lits.length; i++) {
 366  0 if (voc.isUnassigned(lits[i])) {
 367  0 stb.append(" + ");
 368  0 stb.append(this.lits[i]);
 369  0 stb.append(" ");
 370    }
 371    }
 372  0 stb.append(">= ");
 373  0 stb.append(this.degree);
 374    }
 375  0 return stb.toString();
 376    }
 377   
 378    /**
 379    * M?thode appel?e lors du backtrack
 380    *
 381    * @param p
 382    * le litt?ral d?saffect?
 383    */
 384  136041204 public void undo(int p) {
 385  136041204 watchCumul++;
 386    }
 387   
 388  0 public void setLearnt() {
 389  0 throw new UnsupportedOperationException();
 390    }
 391   
 392  0 public void register() {
 393  0 throw new UnsupportedOperationException();
 394    }
 395   
 396  0 public int size() {
 397  0 return lits.length;
 398    }
 399   
 400  0 public int get(int i) {
 401  0 return lits[i];
 402    }
 403   
 404  0 public void assertConstraint(UnitPropagationListener s) {
 405  0 throw new UnsupportedOperationException();
 406    }
 407    }
 
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.