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