Clover coverage report -
Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 580   Methods: 36
NCLOC: 310   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
WatchPb.java 58,3% 66,7% 69,4% 64,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.pb;
 27   
 28    import java.math.BigInteger;
 29    import java.util.Random;
 30   
 31    import org.sat4j.core.Vec;
 32    import org.sat4j.core.VecInt;
 33    import org.sat4j.minisat.constraints.cnf.Lits;
 34    import org.sat4j.minisat.core.Constr;
 35    import org.sat4j.minisat.core.ILits;
 36    import org.sat4j.minisat.core.Undoable;
 37    import org.sat4j.minisat.core.UnitPropagationListener;
 38    import org.sat4j.specs.ContradictionException;
 39    import org.sat4j.specs.IVec;
 40    import org.sat4j.specs.IVecInt;
 41   
 42    public abstract class WatchPb implements PBConstr, Undoable {
 43   
 44    /**
 45    * constant for the initial type of inequality less than or equal
 46    */
 47    public static final boolean ATMOST = false;
 48   
 49    /**
 50    * constant for the initial type of inequality more than or equal
 51    */
 52    public static final boolean ATLEAST = true;
 53   
 54    /**
 55    * variable needed for the sort method
 56    */
 57    private static final Random rand = new Random(91648253);
 58   
 59    /**
 60    * constraint activity
 61    */
 62    protected double activity;
 63   
 64    /**
 65    * coefficients of the literals of the constraint
 66    */
 67    protected BigInteger[] coefs;
 68   
 69    /**
 70    * degree of the pseudo-boolean constraint
 71    */
 72    protected BigInteger degree;
 73   
 74    /**
 75    * literals of the constraint
 76    */
 77    protected int[] lits;
 78   
 79    /**
 80    * true if the constraint is a learned constraint
 81    */
 82    protected boolean learnt = false;
 83   
 84    /**
 85    * true if the constraint is the origin of unit propagation
 86    */
 87    protected boolean locked;
 88   
 89    /**
 90    * sum of the coefficients of the literals satisfied or unvalued
 91    */
 92    protected BigInteger watchCumul = BigInteger.ZERO;
 93   
 94    /**
 95    * constraint's vocabulary
 96    */
 97    protected ILits voc;
 98   
 99    /**
 100    * This constructor is only available for the serialization.
 101    */
 102  0 WatchPb() {
 103    }
 104   
 105  2473726 WatchPb(IDataStructurePB mpb) {
 106  2473726 int size = mpb.size();
 107  2473726 lits = new int[size];
 108  2473726 this.coefs = new BigInteger[size];
 109  2473726 mpb.buildConstraintFromMapPb(lits, coefs);
 110   
 111  2473726 this.degree = mpb.getDegree();
 112   
 113    // On peut trier suivant les coefficients
 114  2473726 sort();
 115    }
 116   
 117    /**
 118    * teste si la contrainte est assertive au niveau de d?cision > dl
 119    *
 120    * @param dl
 121    * @return true iff the constraint is assertive at decision level dl.
 122    */
 123  0 public boolean isAssertive(int dl) {
 124  0 BigInteger slack = BigInteger.ZERO;
 125  0 for (int i = 0; i < lits.length; i++) {
 126  0 if ((coefs[i].signum() > 0)
 127    && ((!voc.isFalsified(lits[i]) || voc.getLevel(lits[i]) >= dl)))
 128  0 slack = slack.add(coefs[i]);
 129    }
 130  0 slack = slack.subtract(degree);
 131  0 if (slack.signum() < 0)
 132  0 return false;
 133  0 for (int i = 0; i < lits.length; i++) {
 134  0 if ((coefs[i].signum() > 0)
 135    && (voc.isUnassigned(lits[i]) || voc.getLevel(lits[i]) >= dl)
 136    && (slack.subtract(coefs[i]).signum() < 0)) {
 137  0 return true;
 138    }
 139    }
 140  0 return false;
 141    }
 142   
 143    /**
 144    * Calcule la cause de l'affectation d'un litt???ral
 145    *
 146    * @param p
 147    * un litt???ral falsifi??? (ou Lit.UNDEFINED)
 148    * @param outReason
 149    * la liste des litt???raux falsifi???s dont la n???gation
 150    * correspond ??? la raison de l'affectation.
 151    * @see Constr#calcReason(int, IVecInt)
 152    */
 153  138226378 public void calcReason(int p, IVecInt outReason) {
 154  138226378 for (int q : lits) {
 155    if (voc.isFalsified(q)) {
 156  526763506 outReason.push(q ^ 1);
 157    }
 158    }
 159    }
 160   
 161    abstract protected void computeWatches() throws ContradictionException;
 162   
 163    abstract protected void computePropagation(UnitPropagationListener s)
 164    throws ContradictionException;
 165   
 166    /**
 167    * Permet d'obtenir le i-???me litt???ral de la contrainte
 168    *
 169    * @param i
 170    * indice du litt???ral recherch???
 171    * @return le litt???ral demand???
 172    */
 173  395984209 public int get(int i) {
 174  395984209 return lits[i];
 175    }
 176   
 177    /**
 178    * Permet d'obtenir le i-???me litt???ral de la contrainte
 179    *
 180    * @param i
 181    * indice du litt???ral recherch???
 182    * @return le litt???ral demand???
 183    */
 184  18684249 public BigInteger getCoef(int i) {
 185  18684249 return coefs[i];
 186    }
 187   
 188    /**
 189    * Obtenir la valeur de l'activit??? de la contrainte
 190    *
 191    * @return la valeur de l'activit??? de la contrainte
 192    * @see Constr#getActivity()
 193    */
 194  0 public double getActivity() {
 195  0 return activity;
 196    }
 197   
 198  2678797 public static IDataStructurePB niceParameters(IVecInt ps,
 199    IVec<BigInteger> bigCoefs, boolean moreThan, BigInteger bigDeg,
 200    ILits voc) throws ContradictionException {
 201    // Ajouter les simplifications quand la structure sera d?finitive
 202  2678797 if (ps.size() == 0) {
 203  0 throw new ContradictionException("Creating Empty clause ?");
 204  2678797 } else if (ps.size() != bigCoefs.size()) {
 205  0 throw new IllegalArgumentException(
 206    "Contradiction dans la taille des tableaux ps=" + ps.size()
 207    + " coefs=" + bigCoefs.size() + ".");
 208    }
 209  2678797 return niceCheckedParameters(ps, bigCoefs, moreThan, bigDeg, voc);
 210    }
 211   
 212  2945770 public static IDataStructurePB niceCheckedParameters(IVecInt ps,
 213    IVec<BigInteger> bigCoefs, boolean moreThan, BigInteger bigDeg,
 214    ILits voc) {
 215    assert ps.size() != 0 && ps.size()==bigCoefs.size();
 216  2945770 int[] lits = new int[ps.size()];
 217  2945770 ps.copyTo(lits);
 218  2945770 BigInteger[] bc = new BigInteger[bigCoefs.size()];
 219  2945770 bigCoefs.copyTo(bc);
 220  2945770 BigInteger bigDegree = bigDeg;
 221  2945770 if (!moreThan) {
 222  23863 for (int i = 0; i < lits.length; i++) {
 223  218106 bc[i] = bc[i].negate();
 224    }
 225  23863 bigDegree = bigDegree.negate();
 226    }
 227   
 228  2945770 for (int i = 0; i < bc.length; i++)
 229  24347399 if (bc[i].signum() < 0) {
 230  10197406 lits[i] = lits[i] ^ 1;
 231  10197406 bc[i] = bc[i].negate();
 232  10197406 bigDegree = bigDegree.add(bc[i]);
 233    }
 234   
 235  2945770 IDataStructurePB mpb = new ArrayPb(voc);
 236  2945768 if (bigDegree.signum() > 0)
 237  2945768 bigDegree = mpb.cuttingPlane(lits, bc, bigDegree);
 238  2945768 if (bigDegree.signum() > 0)
 239  2945768 bigDegree = mpb.saturation();
 240  2945768 if (bigDegree.signum() <= 0)
 241  0 return null;
 242  2945768 return mpb;
 243    }
 244   
 245    /**
 246    * Incr???mente la valeur de l'activit??? de la contrainte
 247    *
 248    * @see Constr#incActivity(double claInc)
 249    */
 250  0 public void incActivity(double claInc) {
 251  0 activity += claInc;
 252    }
 253   
 254    /**
 255    * Marge de la contrainte courante marge = poss - degre de la contrainte
 256    *
 257    * @return la marge
 258    */
 259  266973 public BigInteger slackConstraint() {
 260  266973 return recalcLeftSide().subtract(this.degree);
 261    }
 262   
 263    /**
 264    * Marge de la contrainte courante marge = poss - degre de la contrainte
 265    *
 266    * @param coefs
 267    * le tableau des coefficients de la contrainte consideree
 268    * @param degree
 269    * le degre de la contrainte consideree
 270    * @return la marge
 271    */
 272  1449059 public BigInteger slackConstraint(BigInteger[] coefs, BigInteger degree) {
 273  1449059 return recalcLeftSide(coefs).subtract(degree);
 274    }
 275   
 276    /**
 277    * somme des coefficients des litteraux satisfaits ou non assignes de la
 278    * resolvante
 279    *
 280    * @param coefs
 281    * le tableau des coefficients de la contrainte consid?r?e
 282    * @return cette somme (poss)
 283    */
 284  798876118 public BigInteger recalcLeftSide(BigInteger[] coefs) {
 285  798876118 BigInteger poss = BigInteger.ZERO;
 286    // Pour chaque litteral
 287  798876118 for (int i = 0; i < lits.length; i++)
 288    if (!voc.isFalsified(lits[i])) {
 289    assert coefs[i].signum() >= 0;
 290  391120883 poss = poss.add(coefs[i]);
 291    }
 292  798876118 return poss;
 293    }
 294   
 295    /**
 296    * somme des coefficients des litteraux satisfaits ou non assignes de la
 297    * resolvante
 298    *
 299    * @return cette somme (poss)
 300    */
 301  797427059 public BigInteger recalcLeftSide() {
 302  797427059 return recalcLeftSide(this.coefs);
 303    }
 304   
 305    /**
 306    * D?termine si la contrainte est toujours satisfiable
 307    *
 308    * @return la contrainte est encore satisfiable
 309    */
 310  11369928 protected boolean isSatisfiable() {
 311  11369928 return recalcLeftSide().compareTo(degree) >= 0;
 312    }
 313   
 314    /**
 315    * Dit si la contrainte est apprise
 316    *
 317    * @return true si la contrainte est apprise, false sinon
 318    * @see Constr#learnt()
 319    */
 320  138226378 public boolean learnt() {
 321  138226378 return learnt;
 322    }
 323   
 324    /**
 325    * La contrainte est la cause d'une propagation unitaire
 326    *
 327    * @return true si c'est le cas, false sinon
 328    * @see Constr#locked()
 329    */
 330  0 public boolean locked() {
 331  0 return true;
 332    }
 333   
 334    /**
 335    * Calcule le ppcm de deux nombres
 336    *
 337    * @param a
 338    * premier nombre de l'op?ration
 339    * @param b
 340    * second nombre de l'op?ration
 341    * @return le ppcm en question
 342    */
 343  0 protected static BigInteger ppcm(BigInteger a, BigInteger b) {
 344  0 return a.divide(a.gcd(b)).multiply(b);
 345    }
 346   
 347    /**
 348    * Permet le r??????chantillonage de l'activit??? de la contrainte
 349    *
 350    * @param d
 351    * facteur d'ajustement
 352    */
 353  0 public void rescaleBy(double d) {
 354  0 activity *= d;
 355    }
 356   
 357  3263219 void selectionSort(int from, int to) {
 358  3263219 int i, j, best_i;
 359  3263219 BigInteger tmp;
 360  3263219 int tmp2;
 361   
 362  3263219 for (i = from; i < to - 1; i++) {
 363  18887192 best_i = i;
 364  18887192 for (j = i + 1; j < to; j++) {
 365  94183341 if (coefs[j].compareTo(coefs[best_i]) > 0)
 366  1488975 best_i = j;
 367    }
 368  18887192 tmp = coefs[i];
 369  18887192 coefs[i] = coefs[best_i];
 370  18887192 coefs[best_i] = tmp;
 371  18887192 tmp2 = lits[i];
 372  18887192 lits[i] = lits[best_i];
 373  18887192 lits[best_i] = tmp2;
 374    }
 375    }
 376   
 377    /**
 378    * La contrainte est apprise
 379    */
 380  533746 public void setLearnt() {
 381  533746 learnt = true;
 382    }
 383   
 384    /**
 385    * Simplifie la contrainte(l'all???ge)
 386    *
 387    * @return true si la contrainte est satisfaite, false sinon
 388    */
 389  0 public boolean simplify() {
 390  0 BigInteger cumul = BigInteger.ZERO;
 391   
 392  0 int i = 0;
 393  0 while (i < lits.length && cumul.compareTo(degree) < 0) {
 394  0 if (voc.isSatisfied(lits[i])) {
 395    // Mesure pessimiste
 396  0 cumul = cumul.add(coefs[i]);
 397    }
 398  0 i++;
 399    }
 400   
 401  0 return (cumul.compareTo(degree) >= 0);
 402    }
 403   
 404  831601714 public int size() {
 405  831601714 return lits.length;
 406    }
 407   
 408    /**
 409    * Tri des tableaux
 410    */
 411  2473726 final protected void sort() {
 412    assert this.lits != null;
 413  2473726 if (coefs.length > 0) {
 414  2473726 this.sort(0, size());
 415  2473726 BigInteger buffInt = coefs[0];
 416  2473726 for (int i = 1; i < coefs.length; i++) {
 417    assert buffInt.compareTo(coefs[i]) >= 0;
 418  19676299 buffInt = coefs[i];
 419    }
 420   
 421    }
 422    }
 423   
 424    /**
 425    * Tri d'une partie des tableaux
 426    *
 427    * @param from
 428    * indice du d???but du tri
 429    * @param to
 430    * indice de fin du tri
 431    */
 432  4052712 final protected void sort(int from, int to) {
 433  4052712 int width = to - from;
 434  4052712 if (to - from <= 15)
 435  3263219 selectionSort(from, to);
 436   
 437    else {
 438  789493 BigInteger pivot = coefs[rand.nextInt(width) + from];
 439  789493 BigInteger tmp;
 440  789493 int i = from - 1;
 441  789493 int j = to;
 442  789493 int tmp2;
 443   
 444  789493 for (;;) {
 445  11938924 do
 446  15716617 i++;
 447  15716617 while (coefs[i].compareTo(pivot) > 0);
 448  11938924 do
 449  15802121 j--;
 450  15802121 while (pivot.compareTo(coefs[j]) > 0);
 451   
 452  11938924 if (i >= j)
 453  789493 break;
 454   
 455  11149431 tmp = coefs[i];
 456  11149431 coefs[i] = coefs[j];
 457  11149431 coefs[j] = tmp;
 458  11149431 tmp2 = lits[i];
 459  11149431 lits[i] = lits[j];
 460  11149431 lits[j] = tmp2;
 461    }
 462   
 463  789493 sort(from, i);
 464  789493 sort(i, to);
 465    }
 466   
 467    }
 468   
 469    /**
 470    * Cha???ne repr???sentant la contrainte
 471    *
 472    * @return Cha???ne repr???sentant la contrainte
 473    */
 474  0 @Override
 475    public String toString() {
 476  0 StringBuffer stb = new StringBuffer();
 477   
 478  0 if (lits.length > 0) {
 479  0 for (int i = 0; i < lits.length; i++) {
 480    // if (voc.isUnassigned(lits[i])) {
 481  0 stb.append(" + ");
 482  0 stb.append(this.coefs[i]);
 483  0 stb.append(".");
 484  0 stb.append(Lits.toString(this.lits[i]));
 485  0 stb.append("[");
 486  0 stb.append(voc.valueToString(lits[i]));
 487  0 stb.append("@");
 488  0 stb.append(voc.getLevel(lits[i]));
 489  0 stb.append("]");
 490  0 stb.append(" ");
 491    // }
 492    }
 493  0 stb.append(">= ");
 494  0 stb.append(this.degree);
 495    }
 496  0 return stb.toString();
 497    }
 498   
 499  266973 public void assertConstraint(UnitPropagationListener s) {
 500  266973 BigInteger tmp = slackConstraint();
 501  266973 for (int i = 0; i < lits.length; i++) {
 502  9390763 if (voc.isUnassigned(lits[i])
 503    && tmp.subtract(coefs[i]).signum() < 0) {
 504  282984 boolean ret = s.enqueue(lits[i], this);
 505    assert ret;
 506    }
 507    }
 508    }
 509   
 510    // protected abstract WatchPb watchPbNew(Lits voc, VecInt lits, VecInt
 511    // coefs, boolean moreThan, int degree, int[] indexer);
 512    /**
 513    * @return Returns the degree.
 514    */
 515  2061706 public BigInteger getDegree() {
 516  2061706 return degree;
 517    }
 518   
 519  266773 public void register() {
 520    assert learnt;
 521  266773 try {
 522  266773 computeWatches();
 523    } catch (ContradictionException e) {
 524  0 System.out.println(this);
 525    assert false;
 526    }
 527    }
 528   
 529  1003652 public static IVec<BigInteger> toVecBigInt(IVecInt vec) {
 530  1003652 IVec<BigInteger> bigVec = new Vec<BigInteger>(vec.size());
 531  1003652 for (int i = 0; i < vec.size(); ++i)
 532  3083848 bigVec.push(BigInteger.valueOf(vec.get(i)));
 533  1003652 return bigVec;
 534    }
 535   
 536  1003652 public static BigInteger toBigInt(int i) {
 537  1003652 return BigInteger.valueOf(i);
 538    }
 539   
 540  274271 public BigInteger[] getCoefs() {
 541  274271 BigInteger[] coefsBis = new BigInteger[coefs.length];
 542  274271 System.arraycopy(coefs, 0, coefsBis, 0, coefs.length);
 543  274271 return coefsBis;
 544    }
 545   
 546  240924 public int[] getLits() {
 547  240924 int[] litsBis = new int[lits.length];
 548  240924 System.arraycopy(lits, 0, litsBis, 0, lits.length);
 549  240924 return litsBis;
 550    }
 551   
 552  539664 public ILits getVocabulary() {
 553  539664 return voc;
 554    }
 555   
 556    /**
 557    * compute an implied clause on the literals with the greater coefficients
 558    */
 559  0 public IVecInt computeAnImpliedClause() {
 560  0 BigInteger cptCoefs = BigInteger.ZERO;
 561  0 int index = coefs.length;
 562  0 while ((cptCoefs.compareTo(degree) > 0) && (index > 0)) {
 563  0 cptCoefs = cptCoefs.add(coefs[--index]);
 564    }
 565  0 if (index > 0 && index < size() / 2) {
 566    // System.out.println(this);
 567    // System.out.println("index : "+index);
 568  0 IVecInt literals = new VecInt();
 569  0 for (int j = 0; j <= index; j++)
 570  0 literals.push(lits[j]);
 571  0 return literals;
 572    }
 573  0 return null;
 574    }
 575   
 576  0 public boolean coefficientsEqualToOne() {
 577  0 return false;
 578    }
 579   
 580    }
 
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.