Clover coverage report -
Coverage timestamp: jeu. sept. 29 2005 23:57:39 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 211   Methods: 17
NCLOC: 100   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
TernaryClauses.java 94,4% 83,3% 35,3% 74,6%
coverage coverage
 1    /*
 2    * Created on 1 juin 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 TernaryClauses implements Constr, Serializable {
 22   
 23    private static final long serialVersionUID = 1L;
 24   
 25    private final IVecInt stubs = new VecInt();
 26   
 27    private final ILits voc;
 28   
 29    private final int phead;
 30   
 31  11574 public TernaryClauses(ILits voc, int p) {
 32  11574 this.voc = voc;
 33  11574 this.phead = p;
 34    }
 35   
 36  33972 public void addTernaryClause(int a, int b) {
 37  33972 stubs.push(a);
 38  33972 stubs.push(b);
 39    }
 40   
 41    /*
 42    * (non-Javadoc)
 43    *
 44    * @see org.sat4j.minisat.Constr#remove()
 45    */
 46  0 public void remove() {
 47   
 48    }
 49   
 50    /*
 51    * (non-Javadoc)
 52    *
 53    * @see org.sat4j.minisat.Constr#propagate(org.sat4j.minisat.UnitPropagationListener,
 54    * int)
 55    */
 56  140270 public boolean propagate(UnitPropagationListener s, int p) {
 57    assert voc.isSatisfied(p);
 58    assert voc.isFalsified(phead);
 59  140270 voc.watch(p, this);
 60  140270 for (int i = 0; i < stubs.size(); i += 2) {
 61  312609 int a = stubs.get(i);
 62  312609 int b = stubs.get(i + 1);
 63  312609 if (voc.isSatisfied(a) || voc.isSatisfied(b)) {
 64  202553 continue;
 65    }
 66  110056 if (voc.isFalsified(a)) {
 67  22804 if (!s.enqueue(b, this)) {
 68  2267 return false;
 69    }
 70    } else {
 71  87252 if (voc.isFalsified(b)) {
 72  38217 if (!s.enqueue(a, this)) {
 73  0 return false;
 74    }
 75    }
 76    }
 77    }
 78  138003 return true;
 79    }
 80   
 81    /*
 82    * (non-Javadoc)
 83    *
 84    * @see org.sat4j.minisat.Constr#simplify()
 85    */
 86  0 public boolean simplify() {
 87  0 return false;
 88    }
 89   
 90    /*
 91    * (non-Javadoc)
 92    *
 93    * @see org.sat4j.minisat.Constr#undo(int)
 94    */
 95  0 public void undo(int p) {
 96    }
 97   
 98    /*
 99    * (non-Javadoc)
 100    *
 101    * @see org.sat4j.minisat.Constr#calcReason(int, org.sat4j.datatype.VecInt)
 102    */
 103  26736 public void calcReason(int p, IVecInt outReason) {
 104    assert voc.isFalsified(this.phead);
 105  26736 if (p == ILits.UNDEFINED) {
 106  2245 int i = 0;
 107  2245 while (!voc.isFalsified(stubs.get(i))
 108    || !voc.isFalsified(stubs.get(i + 1))) {
 109  2297 i += 2;
 110    }
 111  2245 outReason.push(this.phead ^ 1);
 112  2245 outReason.push(stubs.get(i) ^ 1);
 113  2245 outReason.push(stubs.get(i + 1) ^ 1);
 114    } else {
 115  24491 outReason.push(this.phead ^ 1);
 116  24491 int i = 0;
 117  24491 while ((stubs.get(i) != p) || (!voc.isFalsified(stubs.get(i ^ 1)))) {
 118  58040 i++;
 119    }
 120    assert !voc.isFalsified(stubs.get(i));
 121  24491 outReason.push(stubs.get(i ^ 1) ^ 1);
 122    assert voc.isFalsified(stubs.get(i ^ 1));
 123    }
 124   
 125    }
 126   
 127    /*
 128    * (non-Javadoc)
 129    *
 130    * @see org.sat4j.minisat.Constr#learnt()
 131    */
 132  26736 public boolean learnt() {
 133  26736 return false;
 134    }
 135   
 136    /*
 137    * (non-Javadoc)
 138    *
 139    * @see org.sat4j.minisat.Constr#incActivity(double)
 140    */
 141  0 public void incActivity(double claInc) {
 142    }
 143   
 144    /*
 145    * (non-Javadoc)
 146    *
 147    * @see org.sat4j.minisat.Constr#getActivity()
 148    */
 149  0 public double getActivity() {
 150  0 return 0;
 151    }
 152   
 153    /*
 154    * (non-Javadoc)
 155    *
 156    * @see org.sat4j.minisat.Constr#locked()
 157    */
 158  0 public boolean locked() {
 159    // TODO Auto-generated method stub
 160  0 return false;
 161    }
 162   
 163    /*
 164    * (non-Javadoc)
 165    *
 166    * @see org.sat4j.minisat.Constr#setLearnt()
 167    */
 168  0 public void setLearnt() {
 169   
 170    }
 171   
 172    /*
 173    * (non-Javadoc)
 174    *
 175    * @see org.sat4j.minisat.Constr#register()
 176    */
 177  0 public void register() {
 178   
 179    }
 180   
 181    /*
 182    * (non-Javadoc)
 183    *
 184    * @see org.sat4j.minisat.Constr#rescaleBy(double)
 185    */
 186  0 public void rescaleBy(double d) {
 187   
 188    }
 189   
 190    /*
 191    * (non-Javadoc)
 192    *
 193    * @see org.sat4j.minisat.Constr#size()
 194    */
 195  234071 public int size() {
 196  234071 return stubs.size();
 197    }
 198   
 199    /*
 200    * (non-Javadoc)
 201    *
 202    * @see org.sat4j.minisat.Constr#get(int)
 203    */
 204  0 public int get(int i) {
 205  0 throw new UnsupportedOperationException();
 206    }
 207   
 208  0 public void assertConstraint(UnitPropagationListener s) {
 209  0 throw new UnsupportedOperationException();
 210    }
 211    }
 
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.