Clover coverage report -
Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 205   Methods: 17
NCLOC: 94   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
TernaryClauses.java 92,9% 82,4% 35,3% 72,3%
coverage coverage
 1    /*
 2    * Created on 1 juin 2004
 3    *
 4    * To change the template for this generated file go to Window - Preferences -
 5    * 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  11588 public TernaryClauses(ILits voc, int p) {
 32  11588 this.voc = voc;
 33  11588 this.phead = p;
 34    }
 35   
 36  33993 public void addTernaryClause(int a, int b) {
 37  33993 stubs.push(a);
 38  33993 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  59286 public boolean propagate(UnitPropagationListener s, int p) {
 57    assert voc.isSatisfied(p);
 58    assert voc.isFalsified(phead);
 59  59286 voc.watch(p, this);
 60  59286 for (int i = 0; i < stubs.size(); i += 2) {
 61  150346 int a = stubs.get(i);
 62  150346 int b = stubs.get(i + 1);
 63  150346 if (voc.isSatisfied(a) || voc.isSatisfied(b)) {
 64  68018 continue;
 65    }
 66  82328 if (voc.isFalsified(a) && !s.enqueue(b, this)) {
 67  1145 return false;
 68  81183 } else if (voc.isFalsified(b) && !s.enqueue(a, this)) {
 69  0 return false;
 70    }
 71    }
 72  58141 return true;
 73    }
 74   
 75    /*
 76    * (non-Javadoc)
 77    *
 78    * @see org.sat4j.minisat.Constr#simplify()
 79    */
 80  0 public boolean simplify() {
 81  0 return false;
 82    }
 83   
 84    /*
 85    * (non-Javadoc)
 86    *
 87    * @see org.sat4j.minisat.Constr#undo(int)
 88    */
 89  0 public void undo(int p) {
 90    }
 91   
 92    /*
 93    * (non-Javadoc)
 94    *
 95    * @see org.sat4j.minisat.Constr#calcReason(int, org.sat4j.datatype.VecInt)
 96    */
 97  14434 public void calcReason(int p, IVecInt outReason) {
 98    assert voc.isFalsified(this.phead);
 99  14434 if (p == ILits.UNDEFINED) {
 100  1123 int i = 0;
 101  1123 while (!voc.isFalsified(stubs.get(i))
 102    || !voc.isFalsified(stubs.get(i + 1))) {
 103  1509 i += 2;
 104    }
 105  1123 outReason.push(this.phead ^ 1);
 106  1123 outReason.push(stubs.get(i) ^ 1);
 107  1123 outReason.push(stubs.get(i + 1) ^ 1);
 108    } else {
 109  13311 outReason.push(this.phead ^ 1);
 110  13311 int i = 0;
 111  13311 while ((stubs.get(i) != p) || (!voc.isFalsified(stubs.get(i ^ 1)))) {
 112  37004 i++;
 113    }
 114    assert !voc.isFalsified(stubs.get(i));
 115  13311 outReason.push(stubs.get(i ^ 1) ^ 1);
 116    assert voc.isFalsified(stubs.get(i ^ 1));
 117    }
 118   
 119    }
 120   
 121    /*
 122    * (non-Javadoc)
 123    *
 124    * @see org.sat4j.minisat.Constr#learnt()
 125    */
 126  14434 public boolean learnt() {
 127  14434 return false;
 128    }
 129   
 130    /*
 131    * (non-Javadoc)
 132    *
 133    * @see org.sat4j.minisat.Constr#incActivity(double)
 134    */
 135  0 public void incActivity(double claInc) {
 136    }
 137   
 138    /*
 139    * (non-Javadoc)
 140    *
 141    * @see org.sat4j.minisat.Constr#getActivity()
 142    */
 143  0 public double getActivity() {
 144  0 return 0;
 145    }
 146   
 147    /*
 148    * (non-Javadoc)
 149    *
 150    * @see org.sat4j.minisat.Constr#locked()
 151    */
 152  0 public boolean locked() {
 153    // TODO Auto-generated method stub
 154  0 return false;
 155    }
 156   
 157    /*
 158    * (non-Javadoc)
 159    *
 160    * @see org.sat4j.minisat.Constr#setLearnt()
 161    */
 162  0 public void setLearnt() {
 163   
 164    }
 165   
 166    /*
 167    * (non-Javadoc)
 168    *
 169    * @see org.sat4j.minisat.Constr#register()
 170    */
 171  0 public void register() {
 172   
 173    }
 174   
 175    /*
 176    * (non-Javadoc)
 177    *
 178    * @see org.sat4j.minisat.Constr#rescaleBy(double)
 179    */
 180  0 public void rescaleBy(double d) {
 181   
 182    }
 183   
 184    /*
 185    * (non-Javadoc)
 186    *
 187    * @see org.sat4j.minisat.Constr#size()
 188    */
 189  234070 public int size() {
 190  234070 return stubs.size();
 191    }
 192   
 193    /*
 194    * (non-Javadoc)
 195    *
 196    * @see org.sat4j.minisat.Constr#get(int)
 197    */
 198  0 public int get(int i) {
 199  0 throw new UnsupportedOperationException();
 200    }
 201   
 202  0 public void assertConstraint(UnitPropagationListener s) {
 203  0 throw new UnsupportedOperationException();
 204    }
 205    }
 
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.