Clover coverage report -
Coverage timestamp: jeu. sept. 29 2005 23:57:39 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 666   Methods: 35
NCLOC: 360   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
WatchPb.java 72,9% 74,1% 80% 74,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.pb;
 27   
 28    import java.math.BigInteger;
 29    import java.util.HashMap;
 30    import java.util.Map;
 31    import java.util.Random;
 32   
 33    import org.sat4j.core.Vec;
 34    import org.sat4j.minisat.constraints.cnf.Lits;
 35    import org.sat4j.minisat.core.Constr;
 36    import org.sat4j.minisat.core.ILits;
 37    import org.sat4j.minisat.core.Undoable;
 38    import org.sat4j.minisat.core.UnitPropagationListener;
 39    import org.sat4j.specs.ContradictionException;
 40    import org.sat4j.specs.IVec;
 41    import org.sat4j.specs.IVecInt;
 42   
 43    public abstract class WatchPb implements Constr, Undoable {
 44   
 45    /**
 46    * Constante pour le type d'in?galit?
 47    */
 48    public static final boolean ATMOST = false;
 49   
 50    public static final boolean ATLEAST = true;
 51   
 52    /**
 53    * Variable pour la g?n?ration de nombre al?atoire (sort)
 54    */
 55    private static final Random rand = new Random(91648253);
 56   
 57    /**
 58    * D???termine l'activit??? de la contrainte
 59    */
 60    protected double activity;
 61   
 62    /**
 63    * Liste des coefficients des litt???raux de la contrainte
 64    */
 65    protected BigInteger[] coefs;
 66   
 67    /**
 68    * Degr??? de la contrainte pseudo-bool???enne
 69    */
 70    protected BigInteger degree;
 71   
 72    /**
 73    * Liste des litt???raux de la contrainte
 74    */
 75    protected int[] lits;
 76   
 77    /**
 78    * D???termine si la contrainte est apprise
 79    */
 80    protected boolean learnt = false;
 81   
 82    /**
 83    * D???termine si la contrainte est la cause d'une propagation unitaire
 84    */
 85    protected boolean locked;
 86   
 87    /**
 88    * Est-ce une in???galit??? sup???rieure ou ???gale
 89    */
 90    protected boolean moreThan;
 91   
 92    /**
 93    * Possibilit??? pour la satisfaction de la contrainte
 94    */
 95    protected BigInteger watchCumul = BigInteger.ZERO;
 96   
 97    /**
 98    * Indice des litt???raux dans l'ordre des propagations
 99    */
 100    protected IVecInt undos;
 101   
 102    protected int backtrackLiteral;
 103   
 104    // protected Logger logger = Logger
 105    // .getLogger("org.sat4j.minisat.constraints.pb");
 106   
 107    /**
 108    * Vocabulaire de la contrainte
 109    */
 110    protected ILits voc;
 111   
 112    /**
 113    * This constructor is only available for the serialization.
 114    */
 115  0 WatchPb() {
 116    }
 117   
 118  1621870 WatchPb(IVecInt ps, IVec<BigInteger> bigCoefs, boolean moreThan,
 119    BigInteger bigDeg) {
 120    assert ps.size() > 0;
 121    assert ps.size() == bigCoefs.size();
 122  1621870 this.moreThan = moreThan;
 123   
 124  1621870 MapPb mpb = new MapPb();
 125  1621870 lits = new int[ps.size()];
 126  1621870 ps.copyTo(lits);
 127  1621870 BigInteger[] bc = new BigInteger[bigCoefs.size()];
 128  1621870 bigCoefs.copyTo(bc);
 129  1621870 BigInteger bigDegree = bigDeg;
 130  1621870 if (!moreThan) {
 131  8067 for (int i = 0; i < lits.length; i++) {
 132  73586 bc[i] = bc[i].negate();
 133    }
 134  8067 bigDegree = bigDegree.negate();
 135    }
 136  1621870 for (int i = 0; i < bc.length; i++)
 137  9064750 if (bc[i].signum() < 0) {
 138  3437594 lits[i] = lits[i] ^ 1;
 139  3437594 bc[i] = bc[i].negate();
 140  3437594 bigDegree = bigDegree.add(bc[i]);
 141    }
 142  1621870 if (bigDegree.signum() > 0)
 143  1621870 bigDegree = mpb.addCoeffNewConstraint(lits, bc, bigDegree);
 144  1621870 if (bigDegree.signum() > 0)
 145  1621870 bigDegree = mpb.saturation();
 146  1621870 int size = mpb.size();
 147  1621870 lits = new int[size];
 148  1621870 this.coefs = new BigInteger[size];
 149  1621870 mpb.buildConstraintFromMapPb(lits, coefs);
 150   
 151  1621870 this.degree = bigDegree;
 152   
 153    // On peut trier suivant les coefficients
 154  1621870 sort();
 155    }
 156   
 157    /**
 158    * teste si la contrainte est assertive au niveau de d?cision > dl
 159    *
 160    * @param dl
 161    * @return true iff the constraint is assertive at decision level dl.
 162    */
 163  208878 public boolean isAssertive(int dl) {
 164  208878 BigInteger slack = BigInteger.ZERO;
 165  208878 for (int i = 0; i < lits.length; i++) {
 166  8607010 if ((coefs[i].signum() > 0)
 167    && ((!voc.isFalsified(lits[i]) || voc.getLevel(lits[i]) >= dl)))
 168  3599352 slack = slack.add(coefs[i]);
 169    }
 170  208878 slack = slack.subtract(degree);
 171  208878 if (slack.signum() < 0)
 172  0 return false;
 173  208878 for (int i = 0; i < lits.length; i++) {
 174  6719811 if ((coefs[i].signum() > 0)
 175    && (voc.isUnassigned(lits[i]) || voc.getLevel(lits[i]) >= dl)
 176    && (slack.subtract(coefs[i]).signum() < 0)) {
 177  64904 return true;
 178    }
 179    }
 180  143974 return false;
 181    }
 182   
 183    /**
 184    * Calcule la cause de l'affectation d'un litt???ral
 185    *
 186    * @param p
 187    * un litt???ral falsifi??? (ou Lit.UNDEFINED)
 188    * @param outReason
 189    * la liste des litt???raux falsifi???s dont la n???gation
 190    * correspond ??? la raison de l'affectation.
 191    * @see Constr#calcReason(int, IVecInt)
 192    */
 193  151001862 public void calcReason(int p, IVecInt outReason) {
 194  151001862 for (int q : lits) {
 195    if (voc.isFalsified(q)) {
 196  649628553 outReason.push(q ^ 1);
 197    }
 198    }
 199    }
 200   
 201    abstract protected void computeWatches() throws ContradictionException;
 202   
 203    abstract protected void computePropagation(UnitPropagationListener s)
 204    throws ContradictionException;
 205   
 206    /**
 207    * Permet d'obtenir le i-???me litt???ral de la contrainte
 208    *
 209    * @param i
 210    * indice du litt???ral recherch???
 211    * @return le litt???ral demand???
 212    */
 213  2021390 public int get(int i) {
 214  2021390 return lits[i];
 215    }
 216   
 217    /**
 218    * Permet d'obtenir le i-???me litt???ral de la contrainte
 219    *
 220    * @param i
 221    * indice du litt???ral recherch???
 222    * @return le litt???ral demand???
 223    */
 224  0 public BigInteger getCoef(int i) {
 225  0 return coefs[i];
 226    }
 227   
 228    /**
 229    * Obtenir la valeur de l'activit??? de la contrainte
 230    *
 231    * @return la valeur de l'activit??? de la contrainte
 232    * @see Constr#getActivity()
 233    */
 234    public double getActivity() {
 235    return activity;
 236    }
 237   
 238  1559408 protected static void niceParameter(IVecInt lits, IVec<BigInteger> coefs)
 239    throws ContradictionException {
 240    // Ajouter les simplifications quand la structure sera d?finitive
 241  1559408 if (lits.size() == 0) {
 242  0 throw new ContradictionException("Creating Empty clause ?");
 243  1559408 } else if (lits.size() != coefs.size()) {
 244  0 throw new IllegalArgumentException(
 245    "Contradiction dans la taille des tableaux ps="
 246    + lits.size() + " coefs=" + coefs.size() + ".");
 247    }
 248    }
 249   
 250    /**
 251    * Incr???mente la valeur de l'activit??? de la contrainte
 252    *
 253    * @see Constr#incActivity(double claInc)
 254    */
 255  0 public void incActivity(double claInc) {
 256  0 activity += claInc;
 257    }
 258   
 259    /**
 260    * Marge de la contrainte courante marge = poss - degre de la contrainte
 261    *
 262    * @return la marge
 263    */
 264  62462 public BigInteger slackConstraint() {
 265  62462 return recalcLeftSide().subtract(this.degree);
 266    }
 267   
 268    /**
 269    * Marge de la contrainte courante marge = poss - degre de la contrainte
 270    *
 271    * @param coefs
 272    * le tableau des coefficients de la contrainte consideree
 273    * @param degree
 274    * le degre de la contrainte consideree
 275    * @return la marge
 276    */
 277  708558 public BigInteger slackConstraint(BigInteger[] coefs, BigInteger degree) {
 278  708558 return recalcLeftSide(coefs).subtract(degree);
 279    }
 280   
 281    /**
 282    * somme des coefficients des litteraux satisfaits ou non assignes de la
 283    * resolvante
 284    *
 285    * @param coefs
 286    * le tableau des coefficients de la contrainte consid?r?e
 287    * @return cette somme (poss)
 288    */
 289  701666396 public BigInteger recalcLeftSide(BigInteger[] coefs) {
 290  701666396 BigInteger poss = BigInteger.ZERO;
 291    // Pour chaque litteral
 292  701666396 for (int i = 0; i < coefs.length; i++)
 293  1673415731 if ((coefs[i].signum() > 0) && (!voc.isFalsified(lits[i])))
 294    poss = poss.add(coefs[i]);
 295  701666396 return poss;
 296    }
 297   
 298    /**
 299    * somme des coefficients des litteraux satisfaits ou non assignes de la
 300    * resolvante
 301    *
 302    * @return cette somme (poss)
 303    */
 304  700957838 public BigInteger recalcLeftSide() {
 305  700957838 return recalcLeftSide(this.coefs);
 306    }
 307   
 308    /**
 309    * D?termine si la contrainte est toujours satisfiable
 310    *
 311    * @return la contrainte est encore satisfiable
 312    */
 313  10384383 protected boolean isSatisfiable() {
 314  10384383 BigInteger sum = BigInteger.ZERO;
 315  10384383 for (int i = 0; i < lits.length; i++) {
 316  120400914 if (!voc.isFalsified(lits[i])) {
 317    assert coefs[i].signum() > 0;
 318  71629821 sum = sum.add(coefs[i]);
 319    }
 320    }
 321  10384383 return sum.compareTo(degree) >= 0;
 322    }
 323   
 324    /**
 325    * Dit si la contrainte est apprise
 326    *
 327    * @return true si la contrainte est apprise, false sinon
 328    * @see Constr#learnt()
 329    */
 330  151001862 public boolean learnt() {
 331  151001862 return learnt;
 332    }
 333   
 334    /**
 335    * La contrainte est la cause d'une propagation unitaire
 336    *
 337    * @return true si c'est le cas, false sinon
 338    * @see Constr#locked()
 339    */
 340  115378617 public boolean locked() {
 341  115378617 return true;
 342    }
 343   
 344    /**
 345    * La contrainte est la cause d'une propagation unitaire
 346    *
 347    * @return true si c'est le cas, false sinon
 348    * @see Constr#locked()
 349    */
 350  0 protected void normalize() {
 351    // logger.entering(this.getClass().getName(), "normalize");
 352    // logger.finer("Before normalizing " + this.toString());
 353    // Translate into >= form
 354  0 if (!moreThan) {
 355  0 for (int i = 0; i < lits.length; i++) {
 356  0 coefs[i] = coefs[i].negate();
 357    }
 358  0 degree = degree.negate();
 359  0 moreThan = true;
 360    }
 361    assert moreThan == true;
 362   
 363    // Replace negative coeff
 364  0 for (int indLit = 0; indLit < this.lits.length; indLit++) {
 365  0 if (coefs[indLit].signum() < 0) {
 366  0 lits[indLit] = lits[indLit] ^ 1;
 367  0 coefs[indLit] = coefs[indLit].negate();
 368  0 degree = degree.add(coefs[indLit]);
 369    }
 370    assert coefs[indLit].signum() >= 0;
 371    }
 372    // On peut trier suivant les coefficients
 373  0 sort();
 374   
 375    // Saturation
 376  0 int indLit = 0;
 377  0 while (coefs.length > indLit && coefs[indLit].compareTo(degree) > 0) {
 378  0 coefs[indLit++] = degree;
 379    }
 380    // si tous les coefficients ont la valeur degree (et degree > 0)
 381    // alors il s'agit d'une clause
 382  0 if (indLit == coefs.length && degree.signum() > 0) {
 383  0 degree = BigInteger.ONE;
 384  0 for (int i = 0; i < coefs.length; i++)
 385  0 coefs[i] = degree;
 386    }
 387   
 388    // logger.finer("After normalizing " + this.toString());
 389    }
 390   
 391    /**
 392    * Calcule le ppcm de deux nombres
 393    *
 394    * @param a
 395    * premier nombre de l'op?ration
 396    * @param b
 397    * second nombre de l'op?ration
 398    * @return le ppcm en question
 399    */
 400  0 protected static BigInteger ppcm(BigInteger a, BigInteger b) {
 401  0 return a.divide(a.gcd(b)).multiply(b);
 402    }
 403   
 404    /**
 405    * Permet le r??????chantillonage de l'activit??? de la contrainte
 406    *
 407    * @param d
 408    * facteur d'ajustement
 409    */
 410  0 public void rescaleBy(double d) {
 411  0 activity *= d;
 412    }
 413   
 414  1848884 void selectionSort(int from, int to) {
 415  1848884 int i, j, best_i;
 416  1848884 BigInteger tmp;
 417  1848884 int tmp2;
 418   
 419  1848884 for (i = from; i < to - 1; i++) {
 420  7215889 best_i = i;
 421  7215889 for (j = i + 1; j < to; j++) {
 422  30638453 if (coefs[j].compareTo(coefs[best_i]) > 0)
 423  483981 best_i = j;
 424    }
 425  7215889 tmp = coefs[i];
 426  7215889 coefs[i] = coefs[best_i];
 427  7215889 coefs[best_i] = tmp;
 428  7215889 tmp2 = lits[i];
 429  7215889 lits[i] = lits[best_i];
 430  7215889 lits[best_i] = tmp2;
 431    }
 432    }
 433   
 434    /**
 435    * La contrainte est apprise
 436    */
 437  124748 public void setLearnt() {
 438  124748 learnt = true;
 439    }
 440   
 441    /**
 442    * Simplifie la contrainte(l'all???ge)
 443    *
 444    * @return true si la contrainte est satisfaite, false sinon
 445    */
 446  4188534 public boolean simplify() {
 447  4188534 BigInteger cumul = BigInteger.ZERO;
 448   
 449  4188534 int i = 0;
 450  4188534 while (i < lits.length && cumul.compareTo(degree) < 0) {
 451  26220961 if (voc.isSatisfied(lits[i])) {
 452    // Mesure pessimiste
 453  71962 cumul = cumul.add(coefs[i]);
 454    }
 455  26220961 i++;
 456    }
 457   
 458  4188534 return (cumul.compareTo(degree) >= 0);
 459    }
 460   
 461  176188993 public int size() {
 462  176188993 return lits.length;
 463    }
 464   
 465    /**
 466    * Tri des tableaux
 467    */
 468  1621870 protected void sort() {
 469    assert this.lits != null;
 470  1621870 if (size() > 0) {
 471  1621870 this.sort(0, size());
 472  1621870 BigInteger buffInt = coefs[0];
 473  1621870 for (int i = 1; i < size(); i++) {
 474    assert buffInt.compareTo(coefs[i]) >= 0;
 475  7442880 buffInt = coefs[i];
 476    }
 477   
 478    }
 479    }
 480   
 481    /**
 482    * Tri d'une partie des tableaux
 483    *
 484    * @param from
 485    * indice du d???but du tri
 486    * @param to
 487    * indice de fin du tri
 488    */
 489  2075898 protected void sort(int from, int to) {
 490  2075898 int width = to - from;
 491  2075898 if (to - from <= 15)
 492  1848884 selectionSort(from, to);
 493   
 494    else {
 495  227014 BigInteger pivot = coefs[rand.nextInt(width) + from];
 496  227014 BigInteger tmp;
 497  227014 int i = from - 1;
 498  227014 int j = to;
 499  227014 int tmp2;
 500   
 501  227014 for (;;) {
 502  3238008 do
 503  3578425 i++;
 504  3578425 while (coefs[i].compareTo(pivot) > 0);
 505  3238008 do
 506  3595759 j--;
 507  3595759 while (pivot.compareTo(coefs[j]) > 0);
 508   
 509  3238008 if (i >= j)
 510  227014 break;
 511   
 512  3010994 tmp = coefs[i];
 513  3010994 coefs[i] = coefs[j];
 514  3010994 coefs[j] = tmp;
 515  3010994 tmp2 = lits[i];
 516  3010994 lits[i] = lits[j];
 517  3010994 lits[j] = tmp2;
 518    }
 519   
 520  227014 sort(from, i);
 521  227014 sort(i, to);
 522    }
 523   
 524    }
 525   
 526    /**
 527    * Cha???ne repr???sentant la contrainte
 528    *
 529    * @return Cha???ne repr???sentant la contrainte
 530    */
 531  0 @Override
 532    public String toString() {
 533  0 StringBuffer stb = new StringBuffer();
 534   
 535  0 if (lits.length > 0) {
 536    // if(voc.isUnassigned(lits[0])){
 537  0 stb.append(this.coefs[0]);
 538  0 stb.append(".");
 539  0 stb.append(Lits.toString(this.lits[0]));
 540  0 stb.append("[");
 541  0 stb.append(voc.valueToString(lits[0]));
 542  0 stb.append("@");
 543  0 stb.append(voc.getLevel(lits[0]));
 544  0 stb.append("]");
 545  0 stb.append(" ");
 546    // }
 547  0 for (int i = 1; i < lits.length; i++) {
 548    // if (voc.isUnassigned(lits[i])) {
 549  0 stb.append(" + ");
 550  0 stb.append(this.coefs[i]);
 551  0 stb.append(".");
 552  0 stb.append(Lits.toString(this.lits[i]));
 553  0 stb.append("[");
 554  0 stb.append(voc.valueToString(lits[i]));
 555  0 stb.append("@");
 556  0 stb.append(voc.getLevel(lits[i]));
 557  0 stb.append("]");
 558  0 stb.append(" ");
 559    // }
 560    }
 561  0 stb.append((this.moreThan) ? ">= " : "<= ");
 562  0 stb.append(this.degree);
 563    }
 564  0 return stb.toString();
 565    }
 566   
 567    /**
 568    * retourne le niveau de backtrack : c'est-?-dire le niveau le plus haut
 569    * pour lequel la contrainte est assertive
 570    *
 571    * @param maxLevel
 572    * le plus bas niveau pour lequel la contrainte est assertive
 573    * @return the highest level (smaller int) for which the constraint is assertive.
 574    */
 575  62462 public int getBacktrackLevel(int maxLevel) {
 576  62462 int litLevel;
 577  62462 int borneMax = maxLevel;
 578    // System.out.println(this);
 579    // System.out.println("assertive au niveau : " + maxLevel);
 580    assert isAssertive(borneMax);
 581  62462 int borneMin = -1;
 582    // on calcule borneMax,
 583    // le niveau le plus haut dans l'arbre ou la contrainte est assertive
 584  62462 for (int i = 0; i < lits.length; i++) {
 585  1959104 litLevel = voc.getLevel(lits[i]);
 586  1959104 if (litLevel < borneMax && litLevel > borneMin)
 587  146416 if (isAssertive(litLevel))
 588  2442 borneMax = litLevel;
 589    else
 590  143974 borneMin = litLevel;
 591    }
 592    // on retourne le niveau immediatement inferieur ? borneMax
 593    // pour lequel la contrainte possede un literal
 594  62462 int retour = 0;
 595  62462 for (int i = 0; i < lits.length; i++) {
 596  1959104 litLevel = voc.getLevel(lits[i]);
 597  1959104 if (litLevel > retour && litLevel < borneMax)
 598  141726 retour = litLevel;
 599    }
 600  62462 return retour;
 601    }
 602   
 603  62462 public void assertConstraint(UnitPropagationListener s) {
 604  62462 BigInteger tmp = slackConstraint();
 605  62462 for (int i = 0; i < lits.length; i++) {
 606  1959104 if (voc.isUnassigned(lits[i])
 607    && tmp.subtract(coefs[i]).signum() < 0) {
 608  72782 boolean ret = s.enqueue(lits[i], this);
 609    assert ret;
 610    }
 611    }
 612    }
 613   
 614    // protected abstract WatchPb watchPbNew(Lits voc, VecInt lits, VecInt
 615    // coefs, boolean moreThan, int degree, int[] indexer);
 616    /**
 617    * @return Returns the degree.
 618    */
 619  580023 public BigInteger getDegree() {
 620  580023 return degree;
 621    }
 622   
 623  62286 public void register() {
 624    assert learnt;
 625  62286 try {
 626  62286 computeWatches();
 627    } catch (ContradictionException e) {
 628  0 System.out.println(this);
 629    assert false;
 630    }
 631    }
 632   
 633  998672 protected static IVec<BigInteger> toVecBigInt(IVecInt vec) {
 634  998672 IVec<BigInteger> bigVec = new Vec<BigInteger>(vec.size());
 635  998672 for (int i = 0; i < vec.size(); ++i)
 636  3073048 bigVec.push(BigInteger.valueOf(vec.get(i)));
 637  998672 return bigVec;
 638    }
 639   
 640  998672 protected static BigInteger toBigInt(int i) {
 641  998672 return BigInteger.valueOf(i);
 642    }
 643   
 644  62490 protected Conflict createConflict() {
 645  62490 Map<Integer, BigInteger> m = new HashMap<Integer, BigInteger>();
 646  62490 for (int i = 0; i < lits.length; i++) {
 647    assert lits[i] != 0;
 648    assert coefs[i].signum() > 0;
 649  810098 m.put(lits[i], coefs[i]);
 650    }
 651  62490 return new Conflict(m, degree, voc);
 652    }
 653   
 654  580022 protected BigInteger[] getCoefs() {
 655  580022 BigInteger[] coefsBis = new BigInteger[coefs.length];
 656  580022 System.arraycopy(coefs, 0, coefsBis, 0, coefs.length);
 657  580022 return coefsBis;
 658    }
 659   
 660  580022 protected int[] getLits() {
 661  580022 int[] litsBis = new int[lits.length];
 662  580022 System.arraycopy(lits, 0, litsBis, 0, lits.length);
 663  580022 return litsBis;
 664    }
 665   
 666    }
 
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.