Clover coverage report -
Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 551   Methods: 25
NCLOC: 270   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
MinWatchCard.java 64,3% 66% 60% 64,9%
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.constraints.cnf.Lits;
 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 MinWatchCard implements Constr, Undoable, Serializable {
 39   
 40    private static final long serialVersionUID = 1L;
 41   
 42    public static final boolean ATLEAST = true;
 43    public static final boolean ATMOST = false;
 44   
 45    /**
 46    * degree of the cardinality constraint
 47    */
 48    protected int degree;
 49   
 50    /**
 51    * literals involved in the constraint
 52    */
 53    private int[] lits;
 54   
 55    /**
 56    * contains the sign of the constraint : ATLEAT or ATMOST
 57    */
 58    private boolean moreThan;
 59   
 60    /**
 61    * contains the sum of the coefficients of the watched literals
 62    */
 63    protected int watchCumul;
 64   
 65    /**
 66    * Vocabulary of the constraint
 67    */
 68    private final ILits voc;
 69   
 70    /**
 71    * Constructs and normalizes a cardinality constraint.
 72    * used by minWatchCardNew in the non-normalized case.
 73    *
 74    * @param voc
 75    * vocabulary used by the constraint
 76    * @param ps
 77    * literals involved in the constraint
 78    * @param moreThan
 79    * should be ATLEAST or ATMOST;
 80    * @param degree
 81    * degree of the constraint
 82    */
 83  251810 public MinWatchCard(ILits voc, IVecInt ps, boolean moreThan, int degree) {
 84    // On met en place les valeurs
 85  251810 this.voc = voc;
 86  251810 this.degree = degree;
 87  251810 this.moreThan = moreThan;
 88   
 89    // On simplifie ps
 90  251810 int[] index = new int[voc.nVars() * 2 + 2];
 91  251810 for (int i = 0; i < index.length; i++)
 92  493911772 index[i] = 0;
 93    // On repertorie les litt?raux utiles
 94  251810 for (int i = 0; i < ps.size(); i++) {
 95  1253945 if (index[ps.get(i) ^ 1] == 0) {
 96  1253932 index[ps.get(i)]++;
 97    } else {
 98  13 index[ps.get(i) ^ 1]--;
 99    }
 100    }
 101    // On supprime les litt?raux inutiles
 102  251810 int ind = 0;
 103  251810 while (ind < ps.size()) {
 104  1253945 if (index[ps.get(ind)] > 0) {
 105  1253919 index[ps.get(ind)]--;
 106  1253919 ind++;
 107    } else {
 108    // ??
 109  26 if ((ps.get(ind) & 1) != 0)
 110  13 this.degree--;
 111  26 ps.set(ind, ps.last());
 112  26 ps.pop();
 113    }
 114    }
 115   
 116    // On copie les litt?raux de la contrainte
 117  251810 lits = new int[ps.size()];
 118  251810 ps.moveTo(lits);
 119   
 120    // On normalise la contrainte au sens de Barth
 121  251810 normalize();
 122   
 123    }
 124   
 125   
 126    /**
 127    * Constructs and normalizes a cardinality constraint.
 128    * used by MinWatchCardPB.normalizedMinWatchCardNew() in the normalized case. <br />
 129    * <strong>Should not be used if parameters are not already normalized</strong><br />
 130    * This constraint is always an ATLEAST constraint.
 131    *
 132    * @param voc
 133    * vocabulary used by the constraint
 134    * @param ps
 135    * literals involved in the constraint
 136    * @param moreThan
 137    * true si la contrainte est sup?rieure ou ?gale
 138    * @param degree
 139    * degree of the constraint
 140    */
 141  18412 protected MinWatchCard(ILits voc, IVecInt ps, int degree){
 142    // On met en place les valeurs
 143  18412 this.voc = voc;
 144  18412 this.degree = degree;
 145  18412 this.moreThan = ATLEAST;
 146   
 147    // On copie les litt?raux de la contrainte
 148  18412 lits = new int[ps.size()];
 149  18412 ps.moveTo(lits);
 150   
 151    }
 152   
 153    /**
 154    * computes the reason for a literal
 155    *
 156    * @param p
 157    * falsified literal (or Lit.UNDEFINED)
 158    * @param outReason
 159    * the reason to be computed. Vector of literals.
 160    * @see Constr#calcReason(int p, IVecInt outReason)
 161    */
 162  36282131 public void calcReason(int p, IVecInt outReason) {
 163    // TODO calcReason: v?rifier par rapport ? l'article
 164    // Pour chaque litt?ral
 165  36282131 for (int i = 0; i < lits.length; i++) {
 166    // Si il est falsifi?
 167  162856816 if (voc.isFalsified(lits[i])) {
 168    // On ajoute sa n?gation au vecteur
 169  130717796 outReason.push(lits[i] ^ 1);
 170    }
 171    }
 172    }
 173   
 174    /**
 175    * Returns the activity of the constraint
 176    *
 177    * @return activity value of the constraint
 178    * @see Constr#getActivity()
 179    */
 180  0 public double getActivity() {
 181    // TODO getActivity
 182  0 return 0;
 183    }
 184   
 185    /**
 186    * Increments activity of the constraint
 187    *
 188    * @param claInc
 189    * value to be added to the activity of the constraint
 190    * @see Constr#incActivity(double claInc)
 191    */
 192  0 public void incActivity(double claInc) {
 193    // TODO incActivity
 194    }
 195   
 196    /**
 197    * Returns wether the constraint is learnt or not.
 198    *
 199    * @return false : a MinWatchCard cannot be learnt.
 200    * @see Constr#learnt()
 201    */
 202  36531384 public boolean learnt() {
 203  36531384 return false;
 204    }
 205   
 206    /**
 207    * Simplifies the constraint w.r.t. the assignments of the literals
 208    *
 209    * @param voc
 210    * vocabulary used
 211    * @param ps
 212    * literals involved
 213    * @return value to be added to the degree. This value is less than or equal to 0.
 214    */
 215  267678 protected static int linearisation(ILits voc, IVecInt ps) {
 216    // Stockage de l'influence des modifications
 217  267678 int modif = 0;
 218   
 219  267678 for (int i = 0; i < ps.size();) {
 220    // on verifie si le litteral est affecte
 221  1127815 if (voc.isUnassigned(ps.get(i))) {
 222  1127815 i++;
 223    } else {
 224    // Si le litteral est satisfait,
 225    // ?a revient ? baisser le degr?
 226  0 if (voc.isSatisfied(ps.get(i))) {
 227  0 modif--;
 228    }
 229    // dans tous les cas, s'il est assign?,
 230    // on enleve le ieme litteral
 231  0 ps.set(i, ps.last());
 232  0 ps.pop();
 233    }
 234    }
 235   
 236    // DLB: inutile?
 237    // ps.shrinkTo(nbElement);
 238    assert modif <= 0;
 239   
 240  267678 return modif;
 241    }
 242   
 243    /**
 244    * Returns if the constraint is the reason for a unit propagation.
 245    *
 246    * @return true
 247    * @see Constr#locked()
 248    */
 249  0 public boolean locked() {
 250    // TODO locked
 251  0 return true;
 252    }
 253   
 254    /**
 255    * Constructs a cardinality constraint with a minimal set of watched literals
 256    * Permet la cr?ation de contrainte de cardinalit? ? observation minimale
 257    *
 258    * @param s
 259    * tool for propagation
 260    * @param voc
 261    * vocalulary used by the constraint
 262    * @param ps
 263    * literals involved in the constraint
 264    * @param moreThan
 265    * sign of the constraint. Should be ATLEAST or ATMOST.
 266    * @param degree
 267    * degree of the constraint
 268    * @return a new cardinality constraint, null if it is a tautology
 269    * @throws ContradictionException
 270    */
 271  249266 public static MinWatchCard minWatchCardNew(UnitPropagationListener s,
 272    ILits voc, IVecInt ps, boolean moreThan, int degree)
 273    throws ContradictionException {
 274   
 275  249266 int mydegree = degree + linearisation(voc, ps);
 276   
 277  249266 if (ps.size() == 0 && mydegree > 0) {
 278  0 throw new ContradictionException();
 279  249266 } else if (ps.size() == mydegree || ps.size() <= 0) {
 280  0 for (int i = 0; i < ps.size(); i++)
 281  0 if (!s.enqueue(ps.get(i))) {
 282  0 throw new ContradictionException();
 283    }
 284  0 return null;
 285    }
 286   
 287    // La contrainte est maintenant cr??e
 288  249266 MinWatchCard retour = new MinWatchCard(voc, ps, moreThan, mydegree);
 289   
 290  249266 if (retour.degree <= 0)
 291  13 return null;
 292   
 293  249253 retour.computeWatches();
 294   
 295  249253 retour.computePropagation(s);
 296   
 297  249253 return retour;
 298    }
 299   
 300    /**
 301    * normalize the constraint (cf. P.Barth normalization)
 302    */
 303  251810 public final void normalize() {
 304    // Gestion du signe
 305  251810 if (!moreThan) {
 306    // On multiplie le degr? par -1
 307  0 this.degree = 0 - this.degree;
 308    // On r?vise chaque litt?ral
 309  0 for (int indLit = 0; indLit < lits.length; indLit++) {
 310  0 lits[indLit] = lits[indLit] ^ 1;
 311  0 this.degree++;
 312    }
 313  0 this.moreThan = true;
 314    }
 315    }
 316   
 317    /**
 318    * propagates the value of a falsified literal
 319    *
 320    * @param s
 321    * tool for literal propagation
 322    * @param p
 323    * falsified literal
 324    * @return false if an inconistency is detected, else true
 325    */
 326  154526295 public boolean propagate(UnitPropagationListener s, int p) {
 327   
 328    // Si la contrainte est responsable de propagation unitaire
 329  154526295 if (watchCumul == degree) {
 330  0 voc.watch(p, this);
 331  0 return false;
 332    }
 333   
 334    // Recherche du litt?ral falsifi?
 335  154526295 int indFalsified = 0;
 336  154526295 while ((lits[indFalsified] ^ 1) != p)
 337  83702387 indFalsified++;
 338    assert watchCumul > degree;
 339   
 340    // Recherche du litt?ral swap
 341  154526295 int indSwap = degree + 1;
 342  154526295 while (indSwap < lits.length && voc.isFalsified(lits[indSwap]))
 343  211075869 indSwap++;
 344   
 345    // Mise ? jour de la contrainte
 346  154526295 if (indSwap == lits.length) {
 347    // Si aucun litt?ral n'a ?t? trouv?
 348  139421852 voc.watch(p, this);
 349    // La limite est atteinte
 350  139421852 watchCumul--;
 351    assert watchCumul == degree;
 352  139421852 voc.undos(p).push(this);
 353   
 354    // On met en queue les litt?raux impliqu?s
 355  139421852 for (int i = 0; i <= degree; i++)
 356  285019388 if ((p != (lits[i] ^ 1)) && !s.enqueue(lits[i], this))
 357  4151514 return false;
 358   
 359  135270338 return true;
 360    }
 361    // Si un litt?ral a ?t? trouv? on les ?change
 362  15104443 int tmpInt = lits[indSwap];
 363  15104443 lits[indSwap] = lits[indFalsified];
 364  15104443 lits[indFalsified] = tmpInt;
 365   
 366    // On observe le nouveau litt?ral
 367  15104443 voc.watch(tmpInt ^ 1, this);
 368   
 369  15104443 return true;
 370    }
 371   
 372    /**
 373    * Removes a constraint from the solver
 374    */
 375  0 public void remove() {
 376  0 for (int i = 0; i <= degree; i++) {
 377  0 voc.watches(lits[i] ^ 1).remove(this);
 378    }
 379    }
 380   
 381    /**
 382    * Rescales the activity value of the constraint
 383    *
 384    * @param d
 385    * rescale factor
 386    */
 387  0 public void rescaleBy(double d) {
 388    // TODO rescaleBy
 389    }
 390   
 391    /**
 392    * simplifies the constraint
 393    *
 394    * @return true if the constraint is satisfied, else false
 395    */
 396  0 public boolean simplify() {
 397    // Calcul de la valeur actuelle
 398  0 for (int i = 0, count = 0; i < lits.length; i++)
 399  0 if (voc.isSatisfied(lits[i]) && (++count == degree))
 400  0 return true;
 401   
 402  0 return false;
 403    }
 404   
 405    /**
 406    * Returns a string representation of the constraint.
 407    *
 408    * @return representation of the constraint.
 409    */
 410  0 @Override
 411    public String toString() {
 412  0 StringBuffer stb = new StringBuffer();
 413  0 stb.append("Card (" + lits.length + ") : ");
 414  0 if (lits.length > 0) {
 415    // if (voc.isUnassigned(lits[0])) {
 416  0 stb.append(Lits.toString(this.lits[0]));
 417  0 stb.append("[");
 418  0 stb.append(voc.valueToString(lits[0]));
 419  0 stb.append("@");
 420  0 stb.append(voc.getLevel(lits[0]));
 421  0 stb.append("]");
 422  0 stb.append(" "); //$NON-NLS-1$
 423    // }
 424  0 for (int i = 1; i < lits.length; i++) {
 425    // if (voc.isUnassigned(lits[i])) {
 426  0 stb.append(" + "); //$NON-NLS-1$
 427  0 stb.append(Lits.toString(this.lits[i]));
 428  0 stb.append("[");
 429  0 stb.append(voc.valueToString(lits[i]));
 430  0 stb.append("@");
 431  0 stb.append(voc.getLevel(lits[i]));
 432  0 stb.append("]");
 433  0 stb.append(" "); //$NON-NLS-1$
 434    // }
 435    }
 436  0 stb.append(">= "); //$NON-NLS-1$
 437  0 stb.append(this.degree);
 438    }
 439  0 return stb.toString();
 440    }
 441   
 442    /**
 443    * Updates information on the constraint in case of a backtrack
 444    *
 445    * @param p
 446    * unassigned literal
 447    */
 448  139419460 public void undo(int p) {
 449    // Le litt?ral observ? et falsifi? devient non assign?
 450  139419460 watchCumul++;
 451    }
 452   
 453  0 public void setLearnt() {
 454  0 throw new UnsupportedOperationException();
 455    }
 456   
 457  0 public void register() {
 458  0 throw new UnsupportedOperationException();
 459    }
 460   
 461  3358720 public int size() {
 462  3358720 return lits.length;
 463    }
 464   
 465  4135657 public int get(int i) {
 466  4135657 return lits[i];
 467    }
 468   
 469  0 public void assertConstraint(UnitPropagationListener s) {
 470  0 throw new UnsupportedOperationException();
 471    }
 472   
 473  270209 protected void computeWatches() {
 474  270209 int indSwap = lits.length;
 475  270209 int tmpInt;
 476  270209 for (int i = 0; i <= degree && i < indSwap; i++) {
 477  1085435 while (voc.isFalsified(lits[i]) && --indSwap > i) {
 478  253985 tmpInt = lits[i];
 479  253985 lits[i] = lits[indSwap];
 480  253985 lits[indSwap] = tmpInt;
 481    }
 482   
 483    // Si le litteral est observable
 484  1085435 if (!voc.isFalsified(lits[i])) {
 485  1084302 watchCumul++;
 486  1084302 voc.watch(lits[i] ^ 1, this);
 487    }
 488    }
 489  270209 if (learnt()) {
 490    // chercher tous les litteraux a regarder
 491    // par ordre de niveau decroissant
 492  2544 int free = 1;
 493  2544 while ((watchCumul <= degree) && (free > 0)) {
 494  2544 free = 0;
 495    // regarder le litteral falsifie au plus bas niveau
 496  2544 int maxlevel = -1, maxi = -1;
 497  2544 for (int i = watchCumul; i < lits.length; i++) {
 498  255118 if (voc.isFalsified(lits[i])) {
 499  255118 free++;
 500  255118 int level = voc.getLevel(lits[i]);
 501  255118 if (level > maxlevel) {
 502  6743 maxi = i;
 503  6743 maxlevel = level;
 504    }
 505    }
 506    }
 507  2544 if (free > 0) {
 508    assert maxi >= 0;
 509  2488 voc.watch(lits[maxi] ^ 1, this);
 510  2488 tmpInt = lits[maxi];
 511  2488 lits[maxi] = lits[watchCumul];
 512  2488 lits[watchCumul] = tmpInt;
 513  2488 watchCumul++;
 514  2488 free--;
 515    assert free >= 0;
 516    }
 517    }
 518    assert lits.length == 1 || watchCumul > 1;
 519    }
 520   
 521    }
 522   
 523  267665 protected MinWatchCard computePropagation(UnitPropagationListener s)
 524    throws ContradictionException {
 525   
 526    // Si on a des litteraux impliques
 527  267665 if (watchCumul == degree) {
 528  0 for (int i = 0; i < lits.length; i++)
 529  0 if (!s.enqueue(lits[i])) {
 530  0 throw new ContradictionException();
 531    }
 532  0 return null;
 533    }
 534   
 535    // Si on n'observe pas suffisamment
 536  267665 if (watchCumul < degree) {
 537  0 throw new ContradictionException();
 538    }
 539  267665 return this;
 540    }
 541   
 542  8362 public int[] getLits() {
 543  8362 int[] tmp = new int[size()];
 544  8362 System.arraycopy(lits, 0, tmp, 0, size());
 545  8362 return tmp;
 546    }
 547   
 548  494908 public ILits getVocabulary() {
 549  494908 return voc;
 550    }
 551    }
 
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.