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