Clover coverage report -
Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 412   Methods: 22
NCLOC: 194   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
MaxWatchCard.java 50% 51% 31,8% 48,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.card;
 27   
 28    import java.io.Serializable;
 29    import java.math.BigInteger;
 30   
 31    import org.sat4j.minisat.constraints.cnf.Lits;
 32    import org.sat4j.minisat.core.Constr;
 33    import org.sat4j.minisat.core.ILits;
 34    import org.sat4j.minisat.core.Undoable;
 35    import org.sat4j.minisat.core.UnitPropagationListener;
 36    import org.sat4j.specs.ContradictionException;
 37    import org.sat4j.specs.IVecInt;
 38   
 39    public class MaxWatchCard implements Constr, Undoable, Serializable {
 40   
 41    private static final long serialVersionUID = 1L;
 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 final ILits voc;
 67   
 68    /**
 69    * Constructeur de base cr?ant des contraintes vides
 70    *
 71    * @param size nombre de litt?raux de la contrainte
 72    * @param learnt indique si la contrainte est apprise
 73    */
 74  249266 private MaxWatchCard(ILits voc, IVecInt ps, boolean moreThan, int degree) {
 75   
 76    // On met en place les valeurs
 77  249266 this.voc = voc;
 78  249266 this.degree = degree;
 79  249266 this.moreThan = moreThan;
 80   
 81    // On simplifie ps
 82  249266 int[] index = new int[voc.nVars() * 2 + 2];
 83  249266 for (int i = 0; i < index.length; i++)
 84  481099300 index[i] = 0;
 85    // On repertorie les litt?raux utiles
 86  249266 for (int i = 0; i < ps.size(); i++) {
 87  767399 if (index[ps.get(i) ^ 1] == 0) {
 88  767386 index[ps.get(i)]++;
 89    } else {
 90  13 index[ps.get(i) ^ 1]--;
 91    }
 92    }
 93    // On supprime les litt?raux inutiles
 94  249266 int ind = 0;
 95  249266 while (ind < ps.size()) {
 96  767399 if (index[ps.get(ind)] > 0) {
 97  767373 index[ps.get(ind)]--;
 98  767373 ind++;
 99    } else {
 100  26 if ((ps.get(ind) & 1) != 0)
 101  13 this.degree--;
 102  26 ps.set(ind, ps.last());
 103  26 ps.pop();
 104    }
 105    }
 106   
 107    // On copie les litt?raux de la contrainte
 108  249266 lits = new int[ps.size()];
 109  249266 ps.moveTo(lits);
 110   
 111    // On normalise la contrainte au sens de Barth
 112  249266 normalize();
 113   
 114    // Mise en place de l'observation maximale
 115  249266 watchCumul = 0;
 116   
 117    // On observe les litt?raux non falsifi?
 118  249266 for (int i = 0; i < lits.length; i++) {
 119    // Rappel: les ?l?ments falsifi?s ne seront jamais d?pil?s
 120  767373 if (!voc.isFalsified(lits[i])) {
 121  767373 watchCumul++;
 122  767373 voc.watch(lits[i] ^ 1, this);
 123    }
 124    }
 125    }
 126   
 127    /**
 128    * Calcule la cause de l'affection d'un litt?ral
 129    *
 130    * @param p un litt?ral falsifi? (ou Lit.UNDEFINED)
 131    * @param outReason vecteur de litt?raux ? remplir
 132    * @see Constr#calcReason(int p, IVecInt outReason)
 133    */
 134  37326457 public void calcReason(int p, IVecInt outReason) {
 135    // TODO calcReason: v?rifier par rapport ? l'article
 136    // Pour chaque litt?ral
 137  37326457 for (int i = 0; i < lits.length; i++) {
 138    // Si il est falsifi?
 139  166589819 if (voc.isFalsified(lits[i])) {
 140    // On ajoute sa n?gation au vecteur
 141  133432466 outReason.push(lits[i] ^ 1);
 142    }
 143    }
 144    }
 145   
 146    /**
 147    * Obtenir la valeur de l'activit? de la contrainte
 148    *
 149    * @return la valeur de l'activit? de la contrainte
 150    * @see Constr#getActivity()
 151    */
 152  0 public double getActivity() {
 153    // TODO getActivity
 154  0 return 0;
 155    }
 156   
 157    /**
 158    * Incr?mente la valeur de l'activit? de la contrainte
 159    *
 160    * @param claInc incr?ment de l'activit? de la contrainte
 161    * @see Constr#incActivity(double claInc)
 162    */
 163  0 public void incActivity(double claInc) {
 164    // TODO incActivity
 165    }
 166   
 167    /**
 168    * D?termine si la contrainte est apprise
 169    *
 170    * @return true si la contrainte est apprise, false sinon
 171    * @see Constr#learnt()
 172    */
 173  37326457 public boolean learnt() {
 174    // TODO learnt
 175  37326457 return false;
 176    }
 177   
 178    /**
 179    * La contrainte est la cause d'une propagation unitaire
 180    *
 181    * @return true si c'est le cas, false sinon
 182    * @see Constr#locked()
 183    */
 184  0 public boolean locked() {
 185    // TODO locked
 186  0 return true;
 187    }
 188   
 189    /**
 190    * Permet la cr?ation de contrainte de cardinalit? ? observation minimale
 191    *
 192    * @param s outil pour la propagation des litt?raux
 193    * @param voc vocabulaire utilis? par la contrainte
 194    * @param ps liste des litt?raux de la nouvelle contrainte
 195    * @param moreThan d?termine si c'est une sup?rieure ou ?gal ? l'origine
 196    * @param degree fournit le degr? de la contrainte
 197    * @return une nouvelle clause si tout va bien, null sinon
 198    * @throws ContradictionException
 199    */
 200  249266 public static MaxWatchCard maxWatchCardNew(UnitPropagationListener s,
 201    ILits voc, IVecInt ps, boolean moreThan, int degree)
 202    throws ContradictionException {
 203   
 204  249266 MaxWatchCard outclause = null;
 205   
 206    // La contrainte ne doit pas ?tre vide
 207  249266 if (ps.size() == 0) {
 208  0 throw new ContradictionException("Creating empty clause"); //$NON-NLS-1$
 209  249266 } else if (ps.size() == degree) {
 210  0 for (int i = 0; i < ps.size(); i++)
 211  0 if (!s.enqueue(ps.get(i))) {
 212  0 throw new ContradictionException(
 213    "Contradiction with implied literal"); //$NON-NLS-1$
 214    }
 215  0 return null;
 216    }
 217   
 218    // On cree la contrainte
 219  249266 outclause = new MaxWatchCard(voc, ps, moreThan, degree);
 220   
 221    // Si le degr? est insufisant
 222  249266 if (outclause.degree <= 0)
 223  13 return null;
 224   
 225    // Si il n'y a aucune chance de satisfaire la contrainte
 226  249253 if (outclause.watchCumul < outclause.degree)
 227  0 throw new ContradictionException();
 228   
 229    // Si les litt?raux observ?s sont impliqu?s
 230  249253 if (outclause.watchCumul == outclause.degree) {
 231  0 for (int i = 0; i < outclause.lits.length; i++) {
 232  0 if (!s.enqueue(outclause.lits[i])) {
 233  0 throw new ContradictionException(
 234    "Contradiction with implied literal"); //$NON-NLS-1$
 235    }
 236    }
 237  0 return null;
 238    }
 239   
 240  249253 return outclause;
 241    }
 242   
 243    /**
 244    * On normalise la contrainte au sens de Barth
 245    */
 246  249266 public final void normalize() {
 247    // Gestion du signe
 248  249266 if (!moreThan) {
 249    // On multiplie le degr? par -1
 250  0 this.degree = 0 - this.degree;
 251    // On r?vise chaque litt?ral
 252  0 for (int indLit = 0; indLit < lits.length; indLit++) {
 253  0 lits[indLit] = lits[indLit] ^ 1;
 254  0 this.degree++;
 255    }
 256  0 this.moreThan = true;
 257    }
 258    }
 259   
 260    /**
 261    * Propagation de la valeur de v?rit? d'un litt?ral falsifi?
 262    *
 263    * @param s objet utilis? pour la propagation
 264    * @param p le litt?ral propag? (il doit etre falsifie)
 265    * @return false ssi une inconsistance est d?t?ct?e
 266    */
 267  209005906 public boolean propagate(UnitPropagationListener s, int p) {
 268   
 269    // On observe toujours tous les litt?raux
 270  209005906 voc.watch(p, this);
 271    assert !voc.isFalsified(p);
 272   
 273    // Si le litt?ral p est impliqu?
 274  209005906 if (this.watchCumul == this.degree)
 275  4169142 return false;
 276   
 277    // On met en place la mise ? jour du compteur
 278  204836764 voc.undos(p).push(this);
 279  204836764 watchCumul--;
 280   
 281    // Si les litt?raux restant sont impliqu?s
 282  204836764 if (watchCumul == degree) {
 283  164456581 for (int q : lits) {
 284  474922548 if (voc.isUnassigned(q) && !s.enqueue(q, this)) {
 285  0 return false;
 286    }
 287    }
 288    }
 289  204836764 return true;
 290    }
 291   
 292    /**
 293    * Enl?ve une contrainte du prouveur
 294    */
 295  0 public void remove() {
 296  0 for (int q : lits) {
 297  0 voc.watches(q ^ 1).remove(this);
 298    }
 299    }
 300   
 301    /**
 302    * Permet le r??chantillonage de l'activit? de la contrainte
 303    *
 304    * @param d facteur d'ajustement
 305    */
 306  0 public void rescaleBy(double d) {
 307    }
 308   
 309    /**
 310    * Simplifie la contrainte(l'all?ge)
 311    *
 312    * @return true si la contrainte est satisfaite, false sinon
 313    */
 314  0 public boolean simplify() {
 315   
 316  0 int i = 0;
 317   
 318    // On esp?re le maximum de la somme
 319  0 int curr = watchCumul;
 320   
 321    // Pour chaque litt?ral
 322  0 while (i < this.lits.length) {
 323    // On d?cr?mente si l'espoir n'est pas fond?
 324  0 if (voc.isUnassigned(lits[i++])) {
 325  0 curr--;
 326  0 if (curr < this.degree)
 327  0 return false;
 328    }
 329    }
 330   
 331  0 return false;
 332    }
 333   
 334    /**
 335    * Cha?ne repr?sentant la contrainte
 336    *
 337    * @return Cha?ne repr?sentant la contrainte
 338    */
 339  0 @Override
 340    public String toString() {
 341  0 StringBuffer stb = new StringBuffer();
 342   
 343  0 if (lits.length > 0) {
 344  0 if (voc.isUnassigned(lits[0])) {
 345  0 stb.append(Lits.toString(this.lits[0]));
 346  0 stb.append(" "); //$NON-NLS-1$
 347    }
 348  0 for (int i = 1; i < lits.length; i++) {
 349  0 if (voc.isUnassigned(lits[i])) {
 350  0 stb.append(" + "); //$NON-NLS-1$
 351  0 stb.append(Lits.toString(this.lits[i]));
 352  0 stb.append(" "); //$NON-NLS-1$
 353    }
 354    }
 355  0 stb.append(">= "); //$NON-NLS-1$
 356  0 stb.append(this.degree);
 357    }
 358  0 return stb.toString();
 359    }
 360   
 361    /**
 362    * M?thode appel?e lors du backtrack
 363    *
 364    * @param p le litt?ral d?saffect?
 365    */
 366  204803532 public void undo(int p) {
 367  204803532 watchCumul++;
 368    }
 369   
 370  0 public void setLearnt() {
 371  0 throw new UnsupportedOperationException();
 372    }
 373   
 374  0 public void register() {
 375  0 throw new UnsupportedOperationException();
 376    }
 377   
 378  0 public int size() {
 379  0 return lits.length;
 380    }
 381   
 382  0 public int get(int i) {
 383  0 return lits[i];
 384    }
 385   
 386  0 public void assertConstraint(UnitPropagationListener s) {
 387  0 throw new UnsupportedOperationException();
 388    }
 389   
 390    /*
 391    * (non-Javadoc)
 392    *
 393    * @see org.sat4j.minisat.constraints.pb.PBConstr#getCoefficient(int)
 394    */
 395  0 public BigInteger getCoef(int literal) {
 396  0 return BigInteger.ONE;
 397    }
 398   
 399    /*
 400    * (non-Javadoc)
 401    *
 402    * @see org.sat4j.minisat.constraints.pb.PBConstr#getDegree()
 403    */
 404  0 public BigInteger getDegree() {
 405  0 return new BigInteger(String.valueOf(degree));
 406    }
 407   
 408  0 public ILits getVocabulary() {
 409  0 return voc;
 410    }
 411   
 412    }
 
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.