Clover coverage report -
Coverage timestamp: jeu. sept. 29 2005 23:57:39 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 203   Methods: 17
NCLOC: 81   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
BinaryClauses.java 50% 60% 35,3% 50%
coverage coverage
 1    /*
 2    * Created on 25 mai 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.core.VecInt;
 12    import org.sat4j.minisat.core.Constr;
 13    import org.sat4j.minisat.core.ILits;
 14    import org.sat4j.minisat.core.UnitPropagationListener;
 15    import org.sat4j.specs.IVecInt;
 16   
 17    /**
 18    * @author leberre To change the template for this generated type comment go to
 19    * Window>Preferences>Java>Code Generation>Code and Comments
 20    */
 21    public class BinaryClauses implements Constr, Serializable {
 22   
 23    private static final long serialVersionUID = 1L;
 24   
 25    private final ILits voc;
 26   
 27    private final IVecInt clauses = new VecInt();
 28   
 29    private final int reason;
 30   
 31    private int conflictindex = -1;
 32   
 33    /**
 34    *
 35    */
 36  74305 public BinaryClauses(ILits voc, int p) {
 37  74305 this.voc = voc;
 38  74305 this.reason = p;
 39    }
 40   
 41  1176730 public void addBinaryClause(int p) {
 42  1176730 clauses.push(p);
 43    }
 44   
 45    /*
 46    * (non-Javadoc)
 47    *
 48    * @see org.sat4j.minisat.Constr#remove()
 49    */
 50  0 public void remove() {
 51    // do nothing
 52    }
 53   
 54    /*
 55    * (non-Javadoc)
 56    *
 57    * @see org.sat4j.minisat.Constr#propagate(org.sat4j.minisat.UnitPropagationListener,
 58    * int)
 59    */
 60  270259858 public boolean propagate(UnitPropagationListener s, int p) {
 61    assert voc.isFalsified(this.reason);
 62  270259858 voc.watch(p, this);
 63  270259858 for (int i = 0; i < clauses.size(); i++) {
 64    int q = clauses.get(i);
 65    if (!s.enqueue(q,this)) {
 66  21337103 conflictindex = i;
 67  21337103 return false;
 68    }
 69    }
 70  248922755 return true;
 71    }
 72   
 73    /*
 74    * (non-Javadoc)
 75    *
 76    * @see org.sat4j.minisat.Constr#simplify()
 77    */
 78  0 public boolean simplify() {
 79  0 for (int i = 0; i < clauses.size(); i++) {
 80  0 if (voc.isSatisfied(clauses.get(i))) {
 81  0 return true;
 82    }
 83  0 if (voc.isFalsified(clauses.get(i))) {
 84  0 clauses.delete(i);
 85    }
 86   
 87    }
 88  0 return false;
 89    }
 90   
 91    /*
 92    * (non-Javadoc)
 93    *
 94    * @see org.sat4j.minisat.Constr#undo(int)
 95    */
 96  0 public void undo(int p) {
 97    // no to do
 98    }
 99   
 100    /*
 101    * (non-Javadoc)
 102    *
 103    * @see org.sat4j.minisat.Constr#calcReason(int, org.sat4j.datatype.VecInt)
 104    */
 105  165534019 public void calcReason(int p, IVecInt outReason) {
 106  165534019 outReason.push(this.reason ^ 1);
 107  165534019 if (p == ILits.UNDEFINED) {
 108    // int i=0;
 109    // while(!voc.isFalsified(clauses.get(i))) {
 110    // i++;
 111    // }
 112    assert conflictindex > -1;
 113  21337066 outReason.push(clauses.get(conflictindex) ^ 1);
 114    }
 115    }
 116   
 117    /*
 118    * (non-Javadoc)
 119    *
 120    * @see org.sat4j.minisat.Constr#learnt()
 121    */
 122  165534019 public boolean learnt() {
 123  165534019 return false;
 124    }
 125   
 126    /*
 127    * (non-Javadoc)
 128    *
 129    * @see org.sat4j.minisat.Constr#incActivity(double)
 130    */
 131  0 public void incActivity(double claInc) {
 132    // TODO Auto-generated method stub
 133    }
 134   
 135    /*
 136    * (non-Javadoc)
 137    *
 138    * @see org.sat4j.minisat.Constr#getActivity()
 139    */
 140  0 public double getActivity() {
 141    // TODO Auto-generated method stub
 142  0 return 0;
 143    }
 144   
 145    /*
 146    * (non-Javadoc)
 147    *
 148    * @see org.sat4j.minisat.Constr#locked()
 149    */
 150  0 public boolean locked() {
 151  0 return false;
 152    }
 153   
 154    /*
 155    * (non-Javadoc)
 156    *
 157    * @see org.sat4j.minisat.Constr#setLearnt()
 158    */
 159  0 public void setLearnt() {
 160    // TODO Auto-generated method stub
 161    }
 162   
 163    /*
 164    * (non-Javadoc)
 165    *
 166    * @see org.sat4j.minisat.Constr#register()
 167    */
 168  0 public void register() {
 169    // TODO Auto-generated method stub
 170    }
 171   
 172    /*
 173    * (non-Javadoc)
 174    *
 175    * @see org.sat4j.minisat.Constr#rescaleBy(double)
 176    */
 177  0 public void rescaleBy(double d) {
 178    // TODO Auto-generated method stub
 179    }
 180   
 181    /*
 182    * (non-Javadoc)
 183    *
 184    * @see org.sat4j.minisat.Constr#size()
 185    */
 186  475791979 public int size() {
 187  475791979 return clauses.size();
 188    }
 189   
 190    /*
 191    * (non-Javadoc)
 192    *
 193    * @see org.sat4j.minisat.Constr#get(int)
 194    */
 195  0 public int get(int i) {
 196    // TODO Auto-generated method stub
 197  0 throw new UnsupportedOperationException();
 198    }
 199   
 200  0 public void assertConstraint(UnitPropagationListener s) {
 201  0 throw new UnsupportedOperationException();
 202    }
 203    }
 
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.