Clover coverage report -
Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 246   Methods: 19
NCLOC: 124   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
CBClause.java 66,7% 70% 78,9% 71,3%
coverage coverage
 1    /*
 2    * Created on 4 juil. 2004
 3    *
 4    * To change the template for this generated file go to
 5    * Window>Preferences>Java>Code Generation>Code and Comments
 6    */
 7    package org.sat4j.minisat.constraints.cnf;
 8   
 9    import java.io.Serializable;
 10   
 11    import org.sat4j.minisat.core.Constr;
 12    import org.sat4j.minisat.core.ILits;
 13    import org.sat4j.minisat.core.Undoable;
 14    import org.sat4j.minisat.core.UnitPropagationListener;
 15    import org.sat4j.specs.IVecInt;
 16   
 17    /**
 18    * @author leberre
 19    */
 20    public class CBClause implements Constr, Undoable, Serializable {
 21   
 22    private static final long serialVersionUID = 1L;
 23   
 24    protected int falsified;
 25   
 26    private boolean learnt;
 27   
 28    protected final int[] lits;
 29   
 30    protected final ILits voc;
 31   
 32    private double activity;
 33   
 34  249668 public static CBClause brandNewClause(UnitPropagationListener s, ILits voc,
 35    IVecInt literals) {
 36  249668 CBClause c = new CBClause(literals, voc);
 37  249668 c.register();
 38  249668 return c;
 39    }
 40   
 41    /**
 42    *
 43    */
 44  9056099 public CBClause(IVecInt ps, ILits voc, boolean learnt) {
 45  9056099 this.learnt = learnt;
 46  9056099 this.lits = new int[ps.size()];
 47  9056099 this.voc = voc;
 48  9056099 ps.moveTo(this.lits);
 49    }
 50   
 51  9056099 public CBClause(IVecInt ps, ILits voc) {
 52  9056099 this(ps, voc, false);
 53    }
 54   
 55    /*
 56    * (non-Javadoc)
 57    *
 58    * @see org.sat4j.minisat.core.Constr#remove()
 59    */
 60  0 public void remove() {
 61  0 for (int i = 0; i < lits.length; i++) {
 62  0 voc.watches(lits[i] ^ 1).remove(this);
 63    }
 64    }
 65   
 66    /*
 67    * (non-Javadoc)
 68    *
 69    * @see org.sat4j.minisat.core.Constr#propagate(org.sat4j.minisat.core.UnitPropagationListener,
 70    * int)
 71    */
 72  1162534493 public boolean propagate(UnitPropagationListener s, int p) {
 73  1162534493 voc.undos(p).push(this);
 74  1162534493 falsified++;
 75    assert falsified != lits.length;
 76  1162534493 if (falsified == lits.length - 1) {
 77    // find unassigned literal
 78  528741493 for (int i = 0; i < lits.length; i++) {
 79  1119182651 if (!voc.isFalsified(lits[i])) {
 80  513388719 return s.enqueue(lits[i], this);
 81    }
 82    }
 83    // one of the variable in to be propagated to false.
 84    // (which explains why the falsified counter has not
 85    // been increased yet)
 86  15352774 return false;
 87    }
 88  633793000 return true;
 89    }
 90   
 91    /*
 92    * (non-Javadoc)
 93    *
 94    * @see org.sat4j.minisat.core.Constr#simplify()
 95    */
 96  0 public boolean simplify() {
 97  0 for (int p : lits) {
 98  0 if (voc.isSatisfied(p)) {
 99  0 return true;
 100    }
 101    }
 102  0 return false;
 103    }
 104   
 105    /*
 106    * (non-Javadoc)
 107    *
 108    * @see org.sat4j.minisat.core.Constr#undo(int)
 109    */
 110  1162636243 public void undo(int p) {
 111  1162636243 falsified--;
 112    }
 113   
 114    /*
 115    * (non-Javadoc)
 116    *
 117    * @see org.sat4j.minisat.core.Constr#calcReason(int,
 118    * org.sat4j.specs.VecInt)
 119    */
 120  144099900 public void calcReason(int p, IVecInt outReason) {
 121    assert outReason.size() == 0;
 122  144099900 for (int q : lits) {
 123    assert voc.isFalsified(q) || q == p;
 124  790766230 if (voc.isFalsified(q)) {
 125  661994193 outReason.push(q ^ 1);
 126    }
 127    }
 128    assert (p == ILits.UNDEFINED) || (outReason.size() == lits.length - 1);
 129    }
 130   
 131    /*
 132    * (non-Javadoc)
 133    *
 134    * @see org.sat4j.minisat.core.Constr#learnt()
 135    */
 136  144099900 public boolean learnt() {
 137  144099900 return learnt;
 138    }
 139   
 140    /*
 141    * (non-Javadoc)
 142    *
 143    * @see org.sat4j.minisat.core.Constr#incActivity(double)
 144    */
 145  7779697 public void incActivity(double claInc) {
 146  7779697 activity += claInc;
 147    }
 148   
 149    /*
 150    * (non-Javadoc)
 151    *
 152    * @see org.sat4j.minisat.core.Constr#getActivity()
 153    */
 154  7779697 public double getActivity() {
 155  7779697 return activity;
 156    }
 157   
 158    /*
 159    * (non-Javadoc)
 160    *
 161    * @see org.sat4j.minisat.core.Constr#locked()
 162    */
 163  0 public boolean locked() {
 164  0 return voc.getReason(lits[0]) == this;
 165    }
 166   
 167    /*
 168    * (non-Javadoc)
 169    *
 170    * @see org.sat4j.minisat.core.Constr#setLearnt()
 171    */
 172  8753407 public void setLearnt() {
 173  8753407 learnt = true;
 174    }
 175   
 176    /*
 177    * (non-Javadoc)
 178    *
 179    * @see org.sat4j.minisat.core.Constr#register()
 180    */
 181  345550 public void register() {
 182  345550 for (int p : lits) {
 183  1568168 voc.watch(p ^ 1, this);
 184    }
 185  345550 if (learnt) {
 186  21429 for (int p : lits) {
 187  522909 if (voc.isFalsified(p)) {
 188  501480 voc.undos(p ^ 1).push(this);
 189  501480 falsified++;
 190    }
 191    }
 192    assert falsified == lits.length - 1;
 193    }
 194    }
 195   
 196    /*
 197    * (non-Javadoc)
 198    *
 199    * @see org.sat4j.minisat.core.Constr#rescaleBy(double)
 200    */
 201  1057 public void rescaleBy(double d) {
 202  1057 activity *= d;
 203    }
 204   
 205    /*
 206    * (non-Javadoc)
 207    *
 208    * @see org.sat4j.minisat.core.Constr#size()
 209    */
 210  227516682 public int size() {
 211  227516682 return lits.length;
 212    }
 213   
 214    /*
 215    * (non-Javadoc)
 216    *
 217    * @see org.sat4j.minisat.core.Constr#get(int)
 218    */
 219  211129550 public int get(int i) {
 220  211129550 return lits[i];
 221    }
 222   
 223    /*
 224    * (non-Javadoc)
 225    *
 226    * @see org.sat4j.minisat.core.Constr#assertConstraint(org.sat4j.minisat.core.UnitPropagationListener)
 227    */
 228  8713348 public void assertConstraint(UnitPropagationListener s) {
 229    assert voc.isUnassigned(lits[0]);
 230  8713348 boolean ret = s.enqueue(lits[0], this);
 231    assert ret;
 232    }
 233   
 234  0 @Override
 235    public String toString() {
 236  0 StringBuffer stb = new StringBuffer();
 237  0 for (int i = 0; i < lits.length; i++) {
 238  0 stb.append(lits[i]);
 239  0 stb.append("["); //$NON-NLS-1$
 240  0 stb.append(voc.valueToString(lits[i]));
 241  0 stb.append("]"); //$NON-NLS-1$
 242  0 stb.append(" "); //$NON-NLS-1$
 243    }
 244  0 return stb.toString();
 245    }
 246    }
 
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.