Clover coverage report -
Coverage timestamp: jeu. sept. 29 2005 23:57:39 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 92,3% 82% 89,5% 86,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    private int falsified;
 25   
 26    private boolean learnt;
 27   
 28    private 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  5852244 public CBClause(IVecInt ps, ILits voc, boolean learnt) {
 45  5852244 this.learnt = learnt;
 46  5852244 this.lits = new int[ps.size()];
 47  5852244 this.voc = voc;
 48  5852244 ps.moveTo(this.lits);
 49    }
 50   
 51  5852244 public CBClause(IVecInt ps, ILits voc) {
 52  5852244 this(ps, voc, false);
 53    }
 54   
 55    /*
 56    * (non-Javadoc)
 57    *
 58    * @see org.sat4j.minisat.core.Constr#remove()
 59    */
 60  13111 public void remove() {
 61  13111 for (int i = 0; i < lits.length; i++) {
 62  66592 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  415170818 public boolean propagate(UnitPropagationListener s, int p) {
 73  415170818 voc.undos(p).push(this);
 74  415170818 falsified++;
 75    assert falsified != lits.length;
 76  415170818 if (falsified == lits.length - 1) {
 77    // find unassigned literal
 78  314148467 for (int i = 0; i < lits.length; i++) {
 79  669412393 if (!voc.isFalsified(lits[i])) {
 80  304758984 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  9389483 return false;
 87    }
 88  101022351 return true;
 89    }
 90   
 91    /*
 92    * (non-Javadoc)
 93    *
 94    * @see org.sat4j.minisat.core.Constr#simplify()
 95    */
 96  524892 public boolean simplify() {
 97  524892 for (int i = 0; i < lits.length; i++) {
 98  1744869 if (voc.isSatisfied(lits[i])) {
 99  13111 return true;
 100    }
 101    }
 102  511781 return false;
 103    }
 104   
 105    /*
 106    * (non-Javadoc)
 107    *
 108    * @see org.sat4j.minisat.core.Constr#undo(int)
 109    */
 110  415187620 public void undo(int p) {
 111  415187620 falsified--;
 112    }
 113   
 114    /*
 115    * (non-Javadoc)
 116    *
 117    * @see org.sat4j.minisat.core.Constr#calcReason(int,
 118    * org.sat4j.specs.VecInt)
 119    */
 120  88007894 public void calcReason(int p, IVecInt outReason) {
 121    assert outReason.size() == 0;
 122  88007894 for (int i = 0; i < lits.length; i++) {
 123    assert voc.isFalsified(lits[i]) || lits[i] == p;
 124  483377925 if (voc.isFalsified(lits[i])) {
 125  404759469 outReason.push(lits[i] ^ 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  88007894 public boolean learnt() {
 137  88007894 return learnt;
 138    }
 139   
 140    /*
 141    * (non-Javadoc)
 142    *
 143    * @see org.sat4j.minisat.core.Constr#incActivity(double)
 144    */
 145  5022347 public void incActivity(double claInc) {
 146  5022347 activity += claInc;
 147    }
 148   
 149    /*
 150    * (non-Javadoc)
 151    *
 152    * @see org.sat4j.minisat.core.Constr#getActivity()
 153    */
 154  5022347 public double getActivity() {
 155  5022347 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  5604525 public void setLearnt() {
 173  5604525 learnt = true;
 174    }
 175   
 176    /*
 177    * (non-Javadoc)
 178    *
 179    * @see org.sat4j.minisat.core.Constr#register()
 180    */
 181  253277 public void register() {
 182  253277 for (int i = 0; i < lits.length; i++) {
 183  814494 voc.watch(lits[i] ^ 1, this);
 184    }
 185  253277 if (learnt) {
 186  2779 for (int i = 0; i < lits.length; i++) {
 187  44432 if (voc.isFalsified(lits[i])) {
 188  41653 voc.undos(lits[i] ^ 1).push(this);
 189  41653 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  515 public void rescaleBy(double d) {
 202  515 activity *= d;
 203    }
 204   
 205    /*
 206    * (non-Javadoc)
 207    *
 208    * @see org.sat4j.minisat.core.Constr#size()
 209    */
 210  141451469 public int size() {
 211  141451469 return lits.length;
 212    }
 213   
 214    /*
 215    * (non-Javadoc)
 216    *
 217    * @see org.sat4j.minisat.core.Constr#get(int)
 218    */
 219  130245706 public int get(int i) {
 220  130245706 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  5601746 public void assertConstraint(UnitPropagationListener s) {
 229    assert voc.isUnassigned(lits[0]);
 230  5601746 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(" ");
 240  0 stb.append("[");
 241  0 stb.append(voc.valueToString(lits[i]));
 242  0 stb.append("]");
 243    }
 244  0 return stb.toString();
 245    }
 246    }
 
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.