Clover coverage report -
Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 232   Methods: 26
NCLOC: 151   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
Lits.java 61,1% 76,1% 84,6% 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.cnf;
 29   
 30    import java.io.Serializable;
 31   
 32    import org.sat4j.core.Vec;
 33    import org.sat4j.minisat.core.Constr;
 34    import org.sat4j.minisat.core.ILits;
 35    import org.sat4j.minisat.core.Lbool;
 36    import org.sat4j.minisat.core.Propagatable;
 37    import org.sat4j.minisat.core.Undoable;
 38    import org.sat4j.specs.IVec;
 39   
 40    /**
 41    * @author laihem
 42    * @author leberre To change the template for this generated type comment go to
 43    * Window - Preferences - Java - Code Generation - Code and Comments
 44    */
 45    public class Lits implements Serializable, ILits {
 46   
 47    private static final long serialVersionUID = 1L;
 48   
 49    private boolean pool[] = new boolean[0];
 50   
 51    private int realnVars=0;
 52   
 53    @SuppressWarnings("unchecked")
 54    protected IVec<Propagatable>[] watches = new IVec[0];
 55   
 56    private int[] level = new int[0];
 57   
 58    public Lbool[] truthValue = new Lbool[1];
 59   
 60    private Constr[] reason = new Constr[0];
 61   
 62    @SuppressWarnings("unchecked")
 63    private IVec<Undoable>[] undos = new IVec[0];
 64   
 65  2846 public Lits() {
 66    }
 67   
 68  668338 @SuppressWarnings({"unchecked"})
 69    public void init(int nvar) {
 70    assert nvar >= 0;
 71    // let some space for unused 0 indexer.
 72  668338 int nvars = nvar + 1;
 73  668338 boolean[] npool = new boolean[nvars];
 74  668338 System.arraycopy(pool, 0, npool, 0, pool.length);
 75  668338 pool = npool;
 76   
 77  668338 level = new int[nvars];
 78  668338 int[] nlevel = new int[nvars];
 79  668335 System.arraycopy(level, 0, nlevel, 0, level.length);
 80  668335 level = nlevel;
 81   
 82  668335 IVec<Propagatable>[] nwatches = new IVec[2 * nvars];
 83  668325 System.arraycopy(watches, 0, nwatches, 0, watches.length);
 84  668325 watches = nwatches;
 85   
 86  668325 Lbool[] ntruthValue = new Lbool[nvars];
 87  668324 System.arraycopy(truthValue, 0, ntruthValue, 0, truthValue.length);
 88  668324 truthValue = ntruthValue;
 89   
 90  668324 IVec<Undoable>[] nundos = new IVec[nvars];
 91  668322 System.arraycopy(undos, 0, nundos, 0, undos.length);
 92  668322 undos = nundos;
 93   
 94  668322 Constr[] nreason = new Constr[nvars];
 95  668322 System.arraycopy(reason, 0, nreason, 0, reason.length);
 96  668322 reason = nreason;
 97    }
 98   
 99  24980868 public int getFromPool(int x) {
 100  24980868 int var = Math.abs(x);
 101    assert var < pool.length;
 102   
 103  24980868 int lit = ((x < 0) ? (var << 1) ^ 1 : (var << 1));
 104    assert lit > 1;
 105  24980868 if (!pool[var]) {
 106  1075169 realnVars++;
 107  1075169 pool[var] = true;
 108  1075169 watches[var << 1] = new Vec<Propagatable>();
 109  1075169 watches[(var << 1) | 1] = new Vec<Propagatable>();
 110  1075169 truthValue[var] = Lbool.UNDEFINED;
 111  1075169 undos[var] = new Vec<Undoable>();
 112  1075169 level[var] = -1;
 113    // reset(var);
 114   
 115    }
 116  24980868 return lit;
 117    }
 118   
 119  1538734 public boolean belongsToPool(int x) {
 120    assert x > 0;
 121  1538734 return pool[x];
 122    }
 123   
 124  2490 public void resetPool() {
 125  2490 for (int i = 0; i < pool.length; i++) {
 126  0 if (pool[i]) {
 127  0 reset(i);
 128    }
 129    }
 130    }
 131   
 132  668326 public void ensurePool(int howmany) {
 133  668326 init(howmany);
 134    }
 135   
 136    public void unassign(int lit) {
 137    assert truthValue[lit >> 1] != Lbool.UNDEFINED;
 138    truthValue[lit >> 1] = Lbool.UNDEFINED;
 139    }
 140   
 141    public void satisfies(int lit) {
 142    assert truthValue[lit >> 1] == Lbool.UNDEFINED;
 143    truthValue[lit >> 1] = satisfyingValue(lit);
 144    }
 145   
 146  2112944114 private static final Lbool satisfyingValue(int lit) {
 147  2112944114 return ((lit & 1) == 0) ? Lbool.TRUE : Lbool.FALSE;
 148    }
 149   
 150    public boolean isSatisfied(int lit) {
 151    return truthValue[lit >> 1] == satisfyingValue(lit);
 152    }
 153   
 154  1047041374 public boolean isFalsified(int lit) {
 155  1047041374 Lbool falsified = ((lit & 1) == 0) ? Lbool.FALSE : Lbool.TRUE;
 156  1047041374 return truthValue[lit >> 1] == falsified;
 157    }
 158   
 159  1886954653 public boolean isUnassigned(int lit) {
 160  1886954653 return truthValue[lit >> 1] == Lbool.UNDEFINED;
 161    }
 162   
 163  0 public String valueToString(int lit) {
 164  0 if (isUnassigned(lit))
 165  0 return "?"; //$NON-NLS-1$
 166  0 if (isSatisfied(lit))
 167  0 return "T"; //$NON-NLS-1$
 168  0 return "F"; //$NON-NLS-1$
 169    }
 170   
 171  36601957 public int nVars() {
 172  36601957 return truthValue.length - 1;
 173    }
 174   
 175  0 public int not(int lit) {
 176  0 return lit ^ 1;
 177    }
 178   
 179  2 public static String toString(int lit) {
 180  2 return ((lit & 1) == 0 ? "" : "-") + (lit >> 1); //$NON-NLS-1$//$NON-NLS-2$
 181    }
 182   
 183  0 public void reset(int lit) {
 184  0 watches[lit].clear();
 185  0 watches[lit ^ 1].clear();
 186  0 level[lit >> 1] = -1;
 187  0 truthValue[lit >> 1] = Lbool.UNDEFINED;
 188  0 reason[lit >> 1] = null;
 189  0 undos[lit >> 1].clear();
 190    }
 191   
 192  1263087438 public int getLevel(int lit) {
 193  1263087438 return level[lit >> 1];
 194    }
 195   
 196    public void setLevel(int lit, int l) {
 197    level[lit >> 1] = l;
 198    }
 199   
 200    public Constr getReason(int lit) {
 201    return reason[lit >> 1];
 202    }
 203   
 204    public void setReason(int lit, Constr r) {
 205    reason[lit >> 1] = r;
 206    }
 207   
 208  1819183493 public IVec<Undoable> undos(int lit) {
 209  1819183493 return undos[lit >> 1];
 210    }
 211   
 212  982880609 public void watch(int lit, Propagatable c) {
 213  982880609 watches[lit].push(c);
 214    }
 215   
 216    public IVec<Propagatable> watches(int lit) {
 217    return watches[lit];
 218    }
 219   
 220  0 public boolean isImplied(int lit) {
 221  0 int var = lit >> 1;
 222    // reason[lit] != null => truthValue[lit]!=Lbool.UNDEFINED
 223    assert reason[var] == null || truthValue[var] != Lbool.UNDEFINED;
 224    // a literal is implied if it is a unit clause, ie
 225    // propagated without reason at decision level 0.
 226  0 return reason[var] != null || level[var] == 0;
 227    }
 228   
 229  452572390 public int realnVars() {
 230  452572390 return realnVars;
 231    }
 232    }
 
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.