Clover coverage report -
Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 292   Methods: 19
NCLOC: 144   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
AtLeast.java 87,5% 64,4% 47,4% 67,7%
coverage coverage
 1    /*
 2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004 Daniel Le Berre
 3    *
 4    * Based on the original minisat specification from:
 5    *
 6    * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
 7    * Sixth International Conference on Theory and Applications of Satisfiability
 8    * Testing, LNCS 2919, pp 502-518, 2003.
 9    *
 10    * This library is free software; you can redistribute it and/or modify it under
 11    * the terms of the GNU Lesser General Public License as published by the Free
 12    * Software Foundation; either version 2.1 of the License, or (at your option)
 13    * any later version.
 14    *
 15    * This library is distributed in the hope that it will be useful, but WITHOUT
 16    * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
 17    * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
 18    * details.
 19    *
 20    * You should have received a copy of the GNU Lesser General Public License
 21    * along with this library; if not, write to the Free Software Foundation, Inc.,
 22    * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
 23    *
 24    */
 25   
 26    package org.sat4j.minisat.constraints.card;
 27   
 28    import java.io.Serializable;
 29   
 30    import org.sat4j.minisat.constraints.cnf.Lits;
 31    import org.sat4j.minisat.core.Constr;
 32    import org.sat4j.minisat.core.ILits;
 33    import org.sat4j.minisat.core.Undoable;
 34    import org.sat4j.minisat.core.UnitPropagationListener;
 35    import org.sat4j.specs.ContradictionException;
 36    import org.sat4j.specs.IVecInt;
 37   
 38    /*
 39    * Created on 8 janv. 2004 To change the template for this generated file go to
 40    * Window>Preferences>Java>Code Generation>Code and Comments
 41    */
 42   
 43    /**
 44    * @author leberre Contrainte de cardinalit?
 45    */
 46    public class AtLeast implements Constr, Undoable, Serializable {
 47   
 48    private static final long serialVersionUID = 1L;
 49   
 50    /** number of allowed falsified literal */
 51    protected int maxUnsatisfied;
 52   
 53    /** current number of falsified literals */
 54    private int counter;
 55   
 56    /**
 57    * constraint literals
 58    */
 59    protected final int[] lits;
 60   
 61    protected final ILits voc;
 62   
 63    /**
 64    * @param ps
 65    * a vector of literals
 66    * @param degree
 67    * the minimal number of satisfied literals
 68    */
 69  264508 protected AtLeast(ILits voc, IVecInt ps, int degree) {
 70  264508 maxUnsatisfied = ps.size() - degree;
 71  264508 this.voc = voc;
 72  264508 counter = 0;
 73  264508 lits = new int[ps.size()];
 74  264508 ps.moveTo(lits);
 75  264508 for (int q : lits) {
 76  1321963 voc.watch(q ^ 1, this);
 77    }
 78    }
 79   
 80  262023 protected static int niceParameters(UnitPropagationListener s, ILits voc,
 81    IVecInt ps, int deg) throws ContradictionException {
 82   
 83  262023 if (ps.size() < deg)
 84  40 throw new ContradictionException();
 85  261983 int degree = deg;
 86  261983 for (int i = 0; i < ps.size();) {
 87    // on verifie si le litteral est affecte
 88  1003320 if (voc.isUnassigned(ps.get(i))) {
 89    // go to next literal
 90  1002993 i++;
 91    } else {
 92    // Si le litteral est satisfait,
 93    // ?a revient ? baisser le degr?
 94  327 if (voc.isSatisfied(ps.get(i))) {
 95  153 degree--;
 96    }
 97    // dans tous les cas, s'il est assign?,
 98    // on enleve le ieme litteral
 99  327 ps.delete(i);
 100    }
 101    }
 102   
 103    // on trie le vecteur ps
 104  261983 ps.sortUnique();
 105    // ?limine les clauses tautologiques
 106    // deux litt?raux de signe oppos?s apparaissent dans la m?me
 107    // clause
 108   
 109  261983 if (ps.size() == degree) {
 110  22 for (int i = 0; i < ps.size(); i++) {
 111  387 if (!s.enqueue(ps.get(i))) {
 112  0 throw new ContradictionException();
 113    }
 114    }
 115  22 return 0;
 116    }
 117   
 118  261961 if (ps.size() < degree)
 119  15 throw new ContradictionException();
 120  261946 return degree;
 121   
 122    }
 123   
 124  252817 public static AtLeast atLeastNew(UnitPropagationListener s, ILits voc,
 125    IVecInt ps, int n) throws ContradictionException {
 126  252817 int degree = niceParameters(s, voc, ps, n);
 127  252762 if (degree == 0)
 128  22 return null;
 129  252740 return new AtLeast(voc, ps, degree);
 130    }
 131   
 132    /*
 133    * (non-Javadoc)
 134    *
 135    * @see Constr#remove(Solver)
 136    */
 137  0 public void remove() {
 138  0 for (int q : lits) {
 139  0 voc.watches(q ^ 1).remove(this);
 140    }
 141    }
 142   
 143    /*
 144    * (non-Javadoc)
 145    *
 146    * @see Constr#propagate(Solver, Lit)
 147    */
 148  509616882 public boolean propagate(UnitPropagationListener s, int p) {
 149    // remet la clause dans la liste des clauses regardees
 150  509616882 voc.watch(p, this);
 151   
 152  509616882 if (counter == maxUnsatisfied)
 153  19325851 return false;
 154   
 155  490291031 counter++;
 156  490291031 voc.undos(p).push(this);
 157   
 158    // If no more can be false, enqueue the rest:
 159  490291031 if (counter == maxUnsatisfied)
 160  303351675 for (int q : lits) {
 161  1705780121 if (voc.isUnassigned(q) && !s.enqueue(q, this)) {
 162  0 return false;
 163    }
 164    }
 165  490291031 return true;
 166    }
 167   
 168    /*
 169    * (non-Javadoc)
 170    *
 171    * @see Constr#simplify(Solver)
 172    */
 173  0 public boolean simplify() {
 174  0 return false;
 175    }
 176   
 177    /*
 178    * (non-Javadoc)
 179    *
 180    * @see Constr#undo(Solver, Lit)
 181    */
 182  490252002 public void undo(int p) {
 183  490252002 counter--;
 184    }
 185   
 186    /*
 187    * (non-Javadoc)
 188    *
 189    * @see Constr#calcReason(Solver, Lit, Vec)
 190    */
 191  172171062 public void calcReason(int p, IVecInt outReason) {
 192  172171062 int c = (p == ILits.UNDEFINED) ? -1 : 0;
 193  172171062 for (int q : lits) {
 194  1064707116 if (voc.isFalsified(q)) {
 195  617754540 outReason.push(q ^ 1);
 196  617754540 if (++c == maxUnsatisfied)
 197  172171062 return;
 198    }
 199    }
 200    }
 201   
 202    /*
 203    * (non-Javadoc)
 204    *
 205    * @see org.sat4j.minisat.datatype.Constr#learnt()
 206    */
 207  172171062 public boolean learnt() {
 208    // Ces contraintes ne sont pas apprises pour le moment.
 209  172171062 return false;
 210    }
 211   
 212    /*
 213    * (non-Javadoc)
 214    *
 215    * @see org.sat4j.minisat.datatype.Constr#getActivity()
 216    */
 217  0 public double getActivity() {
 218    // TODO Auto-generated method stub
 219  0 return 0;
 220    }
 221   
 222    /*
 223    * (non-Javadoc)
 224    *
 225    * @see org.sat4j.minisat.datatype.Constr#incActivity(double)
 226    */
 227  0 public void incActivity(double claInc) {
 228    // TODO Auto-generated method stub
 229   
 230    }
 231   
 232    /*
 233    * For learnt clauses only @author leberre
 234    */
 235  0 public boolean locked() {
 236    // FIXME need to be adapted to AtLeast
 237    // return lits[0].getReason() == this;
 238  0 return true;
 239    }
 240   
 241  0 public void setLearnt() {
 242  0 throw new UnsupportedOperationException();
 243    }
 244   
 245  0 public void register() {
 246  0 throw new UnsupportedOperationException();
 247    }
 248   
 249  1741810 public int size() {
 250  1741810 return lits.length;
 251    }
 252   
 253  2335556 public int get(int i) {
 254  2335556 return lits[i];
 255    }
 256   
 257  0 public void rescaleBy(double d) {
 258  0 throw new UnsupportedOperationException();
 259    }
 260   
 261  0 public void assertConstraint(UnitPropagationListener s) {
 262  0 throw new UnsupportedOperationException();
 263    }
 264   
 265    /**
 266    * Cha?ne repr?sentant la contrainte
 267    *
 268    * @return Cha?ne repr?sentant la contrainte
 269    */
 270  0 @Override
 271    public String toString() {
 272  0 StringBuffer stb = new StringBuffer();
 273  0 stb.append("Card (" + lits.length + ") : ");
 274  0 for (int i = 0; i < lits.length; i++) {
 275    // if (voc.isUnassigned(lits[i])) {
 276  0 stb.append(" + "); //$NON-NLS-1$
 277  0 stb.append(Lits.toString(this.lits[i]));
 278  0 stb.append("[");
 279  0 stb.append(voc.valueToString(lits[i]));
 280  0 stb.append("@");
 281  0 stb.append(voc.getLevel(lits[i]));
 282  0 stb.append("]");
 283  0 stb.append(" ");
 284  0 stb.append(" "); //$NON-NLS-1$
 285    }
 286  0 stb.append(">= "); //$NON-NLS-1$
 287  0 stb.append(size() - maxUnsatisfied);
 288   
 289  0 return stb.toString();
 290    }
 291   
 292    }
 
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.