Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
69   227   10   2,76
28   150   0,49   25
25     1,36  
1    
 
  Lits       Line # 42 69 10 64,8% 0.647541
 
  (194)
 
1    /*
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 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.cnf;
27   
28    import java.io.Serializable;
29   
30    import org.sat4j.core.Vec;
31    import org.sat4j.minisat.core.Constr;
32    import org.sat4j.minisat.core.ILits;
33    import org.sat4j.minisat.core.Propagatable;
34    import org.sat4j.minisat.core.Undoable;
35    import org.sat4j.specs.IVec;
36   
37    /**
38    * @author laihem
39    * @author leberre To change the template for this generated type comment go to
40    * Window - Preferences - Java - Code Generation - Code and Comments
41    */
 
42    public class Lits implements Serializable, ILits {
43   
44    private static final long serialVersionUID = 1L;
45   
46    private boolean pool[] = new boolean[1];
47   
48    private int realnVars = 0;
49   
50    @SuppressWarnings("unchecked")
51    protected IVec<Propagatable>[] watches = new IVec[0];
52   
53    private int[] level = new int[0];
54   
55    private Constr[] reason = new Constr[0];
56   
57    @SuppressWarnings("unchecked")
58    private IVec<Undoable>[] undos = new IVec[0];
59   
60    private boolean[] falsified = new boolean[0];
61   
 
62  2541 toggle public Lits() {
63    }
64   
 
65  743427 toggle @SuppressWarnings( { "unchecked" })
66    public void init(int nvar) {
67  743427 assert nvar >= 0;
68    // let some space for unused 0 indexer.
69  743427 int nvars = nvar + 1;
70  743427 boolean[] npool = new boolean[nvars];
71  743427 System.arraycopy(pool, 0, npool, 0, pool.length);
72  743427 pool = npool;
73   
74  743427 level = new int[nvars];
75  743427 int[] nlevel = new int[nvars];
76  743427 System.arraycopy(level, 0, nlevel, 0, level.length);
77  743427 level = nlevel;
78   
79  743427 IVec<Propagatable>[] nwatches = new IVec[2 * nvars];
80  743427 System.arraycopy(watches, 0, nwatches, 0, watches.length);
81  743427 watches = nwatches;
82   
83  743427 IVec<Undoable>[] nundos = new IVec[nvars];
84  743427 System.arraycopy(undos, 0, nundos, 0, undos.length);
85  743427 undos = nundos;
86   
87  743427 Constr[] nreason = new Constr[nvars];
88  743427 System.arraycopy(reason, 0, nreason, 0, reason.length);
89  743427 reason = nreason;
90   
91  743427 boolean[] newFalsified = new boolean[2 * nvars];
92  743427 System.arraycopy(falsified, 0, newFalsified, 0, falsified.length);
93  743427 falsified = newFalsified;
94    }
95   
 
96  25167365 toggle public int getFromPool(int x) {
97  25167365 int var = Math.abs(x);
98  25167365 assert var < pool.length;
99   
100  25167365 int lit = ((x < 0) ? (var << 1) ^ 1 : (var << 1));
101  25167365 assert lit > 1;
102  25167365 if (!pool[var]) {
103  1151613 realnVars++;
104  1151613 pool[var] = true;
105  1151613 watches[var << 1] = new Vec<Propagatable>();
106  1151613 watches[(var << 1) | 1] = new Vec<Propagatable>();
107  1151613 undos[var] = new Vec<Undoable>();
108  1151613 level[var] = -1;
109  1151613 falsified[var << 1] = false; // because truthValue[var] is
110    // UNDEFINED
111  1151613 falsified[var << 1 | 1] = false; // because truthValue[var] is
112    // UNDEFINED
113    }
114  25167365 return lit;
115    }
116   
 
117  1642361 toggle public boolean belongsToPool(int x) {
118  1642361 assert x > 0;
119  1642361 return pool[x];
120    }
121   
 
122  5008 toggle public void resetPool() {
123  1161514 for (int i = 0; i < pool.length; i++) {
124  1156506 if (pool[i]) {
125  1151498 reset(i << 1);
126    }
127    }
128    }
129   
 
130  743415 toggle public void ensurePool(int howmany) {
131  743415 init(howmany);
132    }
133   
 
134    toggle public void unassign(int lit) {
135    assert falsified[lit] || falsified[lit ^ 1];
136    falsified[lit] = false;
137    falsified[lit ^ 1] = false;
138    }
139   
 
140    toggle public void satisfies(int lit) {
141    assert !falsified[lit] && !falsified[lit ^ 1];
142    falsified[lit] = false;
143    falsified[lit ^ 1] = true;
144    }
145   
 
146    toggle public boolean isSatisfied(int lit) {
147    return falsified[lit ^ 1];
148    }
149   
 
150  1015286766 toggle public final boolean isFalsified(int lit) {
151  1015286766 return falsified[lit];
152    }
153   
 
154    toggle public boolean isUnassigned(int lit) {
155    return !falsified[lit] && !falsified[lit ^ 1];
156    }
157   
 
158  0 toggle public String valueToString(int lit) {
159  0 if (isUnassigned(lit))
160  0 return "?"; //$NON-NLS-1$
161  0 if (isSatisfied(lit))
162  0 return "T"; //$NON-NLS-1$
163  0 return "F"; //$NON-NLS-1$
164    }
165   
 
166  33659686 toggle public int nVars() {
167  33659686 return pool.length - 1;
168    }
169   
 
170  0 toggle public int not(int lit) {
171  0 return lit ^ 1;
172    }
173   
 
174  2 toggle public static String toString(int lit) {
175  2 return ((lit & 1) == 0 ? "" : "-") + (lit >> 1); //$NON-NLS-1$//$NON-NLS-2$
176    }
177   
 
178  1151498 toggle public void reset(int lit) {
179  1151498 watches[lit].clear();
180  1151498 watches[lit ^ 1].clear();
181  1151498 level[lit >> 1] = -1;
182  1151498 reason[lit >> 1] = null;
183  1151498 undos[lit >> 1].clear();
184  1151498 falsified[lit] = false;
185  1151498 falsified[lit ^ 1] = false;
186    }
187   
 
188  2089743375 toggle public int getLevel(int lit) {
189  2089743375 return level[lit >> 1];
190    }
191   
 
192    toggle public void setLevel(int lit, int l) {
193    level[lit >> 1] = l;
194    }
195   
 
196  1919236338 toggle public Constr getReason(int lit) {
197  1919236338 return reason[lit >> 1];
198    }
199   
 
200    toggle public void setReason(int lit, Constr r) {
201    reason[lit >> 1] = r;
202    }
203   
 
204    toggle public IVec<Undoable> undos(int lit) {
205    return undos[lit >> 1];
206    }
207   
 
208  1634206530 toggle public void watch(int lit, Propagatable c) {
209  1634206530 watches[lit].push(c);
210    }
211   
 
212    toggle public IVec<Propagatable> watches(int lit) {
213    return watches[lit];
214    }
215   
 
216  0 toggle public boolean isImplied(int lit) {
217  0 int var = lit >> 1;
218  0 assert reason[var] == null || falsified[lit] || falsified[lit ^ 1];
219    // a literal is implied if it is a unit clause, ie
220    // propagated without reason at decision level 0.
221  0 return reason[var] != null || level[var] == 0;
222    }
223   
 
224  533963251 toggle public int realnVars() {
225  533963251 return realnVars;
226    }
227    }
 
CloverReport generated by Clover Code Coverage v2.0a5
mer. juin 27 2007 07:27:33 CEST.		   Beta Testers License registered to clover-support@cenqua.com. This license of Clover2 is provided for beta testing only. You have 5 day(s) before your Beta Tester License expires.