Clover coverage report -
Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 358   Methods: 21
NCLOC: 166   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
WLClause.java 82,5% 84% 90,5% 84,5%
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
 7    * the Sixth International Conference on Theory and Applications of
 8    * Satisfiability 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.cnf;
 27   
 28    import java.io.Serializable;
 29   
 30    import org.sat4j.minisat.core.Constr;
 31    import org.sat4j.minisat.core.ILits;
 32    import org.sat4j.minisat.core.UnitPropagationListener;
 33    import org.sat4j.specs.ContradictionException;
 34    import org.sat4j.specs.IVecInt;
 35   
 36    /*
 37    * Created on 16 oct. 2003 To change the template for this generated file go to
 38    * Window>Preferences>Java>Code Generation>Code and Comments
 39    */
 40   
 41    /**
 42    * Lazy data structure for clause using Watched Literals.
 43    *
 44    * @author leberre
 45    */
 46    public class WLClause implements Constr, Serializable {
 47   
 48    private static final long serialVersionUID = 1L;
 49   
 50    private boolean learnt;
 51   
 52    private double activity;
 53   
 54    private final int[] lits;
 55   
 56    private final ILits voc;
 57   
 58    /**
 59    * Creates a new basic clause
 60    *
 61    * @param voc the vocabulary of the formula
 62    * @param ps A VecInt that WILL BE EMPTY after calling that method.
 63    */
 64  132562418 public WLClause(IVecInt ps, ILits voc) {
 65  132562418 lits = new int[ps.size()];
 66  132562415 ps.moveTo(lits);
 67    assert ps.size() == 0;
 68  132562415 this.voc = voc;
 69  132562415 activity = 0;
 70  132562415 learnt = false;
 71    }
 72   
 73    /**
 74    * Perform some sanity check before constructing a clause a) if a literal is
 75    * assigned true, return null (the clause is satisfied) b) if a literal is
 76    * assigned false, remove it c) if a clause contains a literal and its
 77    * opposite (tautology) return null d) remove duplicate literals e) if the
 78    * clause is empty, return null f) if the clause if unit, transmit it to the
 79    * object responsible for unit propagation
 80    *
 81    * @param ps the list of literals
 82    * @param voc the vocabulary used
 83    * @param s the object responsible for unit propagation
 84    * @return null if the clause should be ignored, the (possibly modified)
 85    * list of literals otherwise
 86    * @throws ContradictionException if discovered by unit propagation
 87    */
 88  3704012 public static IVecInt sanityCheck(IVecInt ps, ILits voc,
 89    UnitPropagationListener s) throws ContradictionException {
 90    // si un litt???ral de ps est vrai, retourner vrai
 91    // enlever les litt???raux falsifi???s de ps
 92  3704012 for (int i = 0; i < ps.size();) {
 93    // on verifie si le litteral est affecte
 94  11674182 if (voc.isUnassigned(ps.get(i))) {
 95    // on passe au literal suivant
 96  11673207 i++;
 97    } else {
 98    // Si le litteral est satisfait, la clause est
 99    // satisfaite
 100  975 if (voc.isSatisfied(ps.get(i))) {
 101    // on retourne la clause
 102  774 return null;
 103    }
 104    // on enleve le ieme litteral
 105  201 ps.delete(i);
 106   
 107    }
 108    }
 109   
 110    // on trie le vecteur ps
 111  3703238 ps.sortUnique();
 112   
 113    // ???limine les clauses tautologiques
 114    // deux litt???raux de signe oppos???s apparaissent dans la m???me
 115    // clause
 116  3703238 for (int i = 0; i < ps.size() - 1; i++) {
 117  7969398 if (ps.get(i) == (ps.get(i + 1) ^ 1)) {
 118    // la clause est tautologique
 119  169 return null;
 120    }
 121    }
 122   
 123  3703069 if (propagationCheck(ps, s))
 124  254 return null;
 125   
 126  3702805 return ps;
 127    }
 128   
 129    /**
 130    * Check if this clause is null or unit
 131    *
 132    * @param p the list of literals (supposed to be clean as after a call to
 133    * sanityCheck())
 134    * @param s the object responsible for unit propagation
 135    * @return true iff the clause should be ignored (because it's unit)
 136    * @throws ContradictionException when detected by unit propagation
 137    */
 138  3703069 static boolean propagationCheck(IVecInt ps, UnitPropagationListener s)
 139    throws ContradictionException {
 140  3703069 if (ps.size() == 0) {
 141  10 throw new ContradictionException("Creating Empty clause ?"); //$NON-NLS-1$
 142  3703059 } else if (ps.size() == 1) {
 143  254 if (!s.enqueue(ps.get(0))) {
 144  0 throw new ContradictionException("Contradictory Unit Clauses"); //$NON-NLS-1$
 145    }
 146  254 return true;
 147    }
 148   
 149  3702805 return false;
 150    }
 151   
 152    /**
 153    * declares this clause as learnt
 154    *
 155    */
 156  134178490 public void setLearnt() {
 157  134178490 learnt = true;
 158    }
 159   
 160    /**
 161    * Register this clause which means watching the necessary literals If the
 162    * clause is learnt, setLearnt() must be called before a call to register()
 163    *
 164    * @see #setLearnt()
 165    */
 166  5167671 public void register() {
 167    assert lits.length > 1;
 168  5167671 if (learnt) {
 169    // prendre un deuxieme litt???ral ??? surveiller
 170  3391873 int maxi = 1;
 171  3391873 int maxlevel = voc.getLevel(lits[1]);
 172  3391873 for (int i = 2; i < lits.length; i++) {
 173  648698700 int level = voc.getLevel(lits[i]);
 174  648698700 if (level > maxlevel) {
 175  13215045 maxi = i;
 176  13215045 maxlevel = level;
 177    }
 178    }
 179  3391873 int l = lits[1];
 180  3391873 lits[1] = lits[maxi];
 181  3391873 lits[maxi] = l;
 182    }
 183   
 184    // ajoute la clause a la liste des clauses control???es.
 185  5167671 voc.watch(lits[0] ^ 1, this);
 186  5167671 voc.watch(lits[1] ^ 1, this);
 187    }
 188   
 189    /**
 190    * Creates a brand new clause, presumably from external data. Performs all
 191    * sanity checks.
 192    *
 193    * @param s the object responsible for unit propagation
 194    * @param voc the vocabulary
 195    * @param literals the literals to store in the clause
 196    * @return the created clause or null if the clause should be ignored
 197    * (tautology for example)
 198    */
 199  1406023 public static WLClause brandNewClause(UnitPropagationListener s, ILits voc,
 200    IVecInt literals) {
 201  1406023 WLClause c = new WLClause(literals, voc);
 202  1406023 c.register();
 203  1406023 return c;
 204    }
 205   
 206    /*
 207    * (non-Javadoc)
 208    *
 209    * @see Constr#calcReason(Solver, Lit, Vec)
 210    */
 211  664473658 public void calcReason(int p, IVecInt outReason) {
 212    assert outReason.size() == 0;
 213    assert (p == ILits.UNDEFINED) || (p == lits[0]);
 214  664473658 for (int i = (p == ILits.UNDEFINED) ? 0 : 1; i < lits.length; i++) {
 215    assert voc.isFalsified(lits[i]);
 216  2019639536 outReason.push(lits[i] ^ 1);
 217    }
 218    }
 219   
 220    /*
 221    * (non-Javadoc)
 222    *
 223    * @see Constr#remove(Solver)
 224    */
 225  689654 public void remove() {
 226  689654 voc.watches(lits[0] ^ 1).remove(this);
 227  689654 voc.watches(lits[1] ^ 1).remove(this);
 228    // la clause peut etre effacee
 229    }
 230   
 231    /*
 232    * (non-Javadoc)
 233    *
 234    * @see Constr#simplify(Solver)
 235    */
 236  0 public boolean simplify() {
 237  0 for (int i = 0; i < lits.length; i++) {
 238  0 if (voc.isSatisfied(lits[i])) {
 239  0 return true;
 240    }
 241    }
 242  0 return false;
 243    }
 244   
 245  1502339590 public boolean propagate(UnitPropagationListener s, int p) {
 246    // Lits[1] doit contenir le litt???ral falsifi???
 247  1502339590 if (lits[0] == (p ^ 1)) {
 248  1696734686 lits[0] = lits[1];
 249  1696734686 lits[1] = p ^ 1;
 250    }
 251    assert lits[1] == (p ^ 1);
 252    // // Si le premier litt???ral est satisfait, la clause est satisfaite
 253    // The solver appears to solve more benchmarks (while being sometimes slower)
 254    // if commenting those lines.
 255    // if (voc.isSatisfied(lits[0])) {
 256    // // reinsert la clause dans la liste des clauses surveillees
 257    // voc.watch(p, this);
 258    // return true;
 259    // }
 260   
 261    // Recherche un nouveau litt???ral ??? regarder
 262  1502339590 for (int i = 2; i < lits.length; i++) {
 263  1416202367 if (!voc.isFalsified(lits[i])) {
 264    lits[1] = lits[i];
 265    lits[i] = p ^ 1;
 266    voc.watch(lits[1] ^ 1, this);
 267    return true;
 268    }
 269    }
 270    assert voc.isFalsified(lits[1]);
 271    // La clause est unitaire ou nulle
 272    voc.watch(p, this);
 273    // avance pour la propagation
 274    return s.enqueue(lits[0], this);
 275    }
 276   
 277    /*
 278    * For learnt clauses only @author leberre
 279    */
 280  692708 public boolean locked() {
 281  692708 return voc.getReason(lits[0]) == this;
 282    }
 283   
 284    /**
 285    * @return the activity of the clause
 286    */
 287  168563774 public double getActivity() {
 288  168563774 return activity;
 289    }
 290   
 291  0 @Override
 292    public String toString() {
 293  0 StringBuffer stb = new StringBuffer();
 294  0 for (int i = 0; i < lits.length; i++) {
 295  0 stb.append(Lits.toString(lits[i]));
 296  0 stb.append("["); //$NON-NLS-1$
 297  0 stb.append(voc.valueToString(lits[i]));
 298  0 stb.append("]"); //$NON-NLS-1$
 299  0 stb.append(" "); //$NON-NLS-1$
 300    }
 301  0 return stb.toString();
 302    }
 303   
 304    /**
 305    * Retourne le ieme literal de la clause. Attention, cet ordre change durant
 306    * la recherche.
 307    *
 308    * @param i the index of the literal
 309    * @return the literal
 310    */
 311  449953113 public int get(int i) {
 312  449953113 return lits[i];
 313    }
 314   
 315    /**
 316    * @param claInc
 317    */
 318  123851794 public void incActivity(double claInc) {
 319  123851794 activity += claInc;
 320    }
 321   
 322    /**
 323    * @param d
 324    */
 325  1443472 public void rescaleBy(double d) {
 326  1443472 activity *= d;
 327    }
 328   
 329    /*
 330    * (non-Javadoc)
 331    *
 332    * @see org.sat4j.minisat.datatype.Constr#learnt()
 333    */
 334  664473658 public boolean learnt() {
 335  664473658 return learnt;
 336    }
 337   
 338  407922746 public int size() {
 339  407922746 return lits.length;
 340    }
 341   
 342  130558317 public void assertConstraint(UnitPropagationListener s) {
 343  130558317 boolean ret = s.enqueue(lits[0], this);
 344    assert ret;
 345    }
 346   
 347  3370177 public ILits getVocabulary(){
 348  3370177 return voc;
 349    }
 350   
 351  239387 public int[] getLits(){
 352  239387 int[] tmp = new int[size()];
 353  239387 System.arraycopy(lits, 0, tmp, 0, size());
 354  239387 return tmp;
 355    }
 356   
 357   
 358    }
 
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.