Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
50   265   16   2,63
32   124   0,68   19
19     1,79  
1    
 
  CBClause       Line # 39 50 16 68,3% 0.6831683
 
  (154)
 
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.minisat.core.Constr;
31    import org.sat4j.minisat.core.ILits;
32    import org.sat4j.minisat.core.Undoable;
33    import org.sat4j.minisat.core.UnitPropagationListener;
34    import org.sat4j.specs.IVecInt;
35   
36    /**
37    * @author leberre
38    */
 
39    public class CBClause implements Constr, Undoable, Serializable {
40   
41    private static final long serialVersionUID = 1L;
42   
43    protected int falsified;
44   
45    private boolean learnt;
46   
47    protected final int[] lits;
48   
49    protected final ILits voc;
50   
51    private double activity;
52   
 
53  249668 toggle public static CBClause brandNewClause(UnitPropagationListener s, ILits voc,
54    IVecInt literals) {
55  249668 CBClause c = new CBClause(literals, voc);
56  249668 c.register();
57  249668 return c;
58    }
59   
60    /**
61    *
62    */
 
63  12089031 toggle public CBClause(IVecInt ps, ILits voc, boolean learnt) {
64  12089031 this.learnt = learnt;
65  12089031 this.lits = new int[ps.size()];
66  12089031 this.voc = voc;
67  12089031 ps.moveTo(this.lits);
68    }
69   
 
70  12089031 toggle public CBClause(IVecInt ps, ILits voc) {
71  12089031 this(ps, voc, false);
72    }
73   
74    /*
75    * (non-Javadoc)
76    *
77    * @see org.sat4j.minisat.core.Constr#remove()
78    */
 
79  0 toggle public void remove() {
80  0 for (int i = 0; i < lits.length; i++) {
81  0 voc.watches(lits[i] ^ 1).remove(this);
82    }
83    }
84   
85    /*
86    * (non-Javadoc)
87    *
88    * @see org.sat4j.minisat.core.Constr#propagate(org.sat4j.minisat.core.UnitPropagationListener,
89    * int)
90    */
 
91  1721812357 toggle public boolean propagate(UnitPropagationListener s, int p) {
92  1721812357 voc.undos(p).push(this);
93  1721812357 falsified++;
94  1721812357 assert falsified != lits.length;
95  1721812357 if (falsified == lits.length - 1) {
96    // find unassigned literal
97  1536385732 for (int i = 0; i < lits.length; i++) {
98  1515511964 if (!voc.isFalsified(lits[i])) {
99  707082471 return s.enqueue(lits[i], this);
100    }
101    }
102    // one of the variable in to be propagated to false.
103    // (which explains why the falsified counter has not
104    // been increased yet)
105  20873768 return false;
106    }
107  993856118 return true;
108    }
109   
110    /*
111    * (non-Javadoc)
112    *
113    * @see org.sat4j.minisat.core.Constr#simplify()
114    */
 
115  0 toggle public boolean simplify() {
116  0 for (int p : lits) {
117  0 if (voc.isSatisfied(p)) {
118  0 return true;
119    }
120    }
121  0 return false;
122    }
123   
124    /*
125    * (non-Javadoc)
126    *
127    * @see org.sat4j.minisat.core.Constr#undo(int)
128    */
 
129  1722452475 toggle public void undo(int p) {
130  1722452475 falsified--;
131    }
132   
133    /*
134    * (non-Javadoc)
135    *
136    * @see org.sat4j.minisat.core.Constr#calcReason(int,
137    * org.sat4j.specs.VecInt)
138    */
 
139  196586708 toggle public void calcReason(int p, IVecInt outReason) {
140  196586708 assert outReason.size() == 0;
141  196586708 for (int q : lits) {
142  1081018603 assert voc.isFalsified(q) || q == p;
143  1081018603 if (voc.isFalsified(q)) {
144  905282379 outReason.push(q ^ 1);
145    }
146    }
147  196586708 assert (p == ILits.UNDEFINED) || (outReason.size() == lits.length - 1);
148    }
149   
150    /*
151    * (non-Javadoc)
152    *
153    * @see org.sat4j.minisat.core.Constr#learnt()
154    */
 
155  196586708 toggle public boolean learnt() {
156  196586708 return learnt;
157    }
158   
159    /*
160    * (non-Javadoc)
161    *
162    * @see org.sat4j.minisat.core.Constr#incActivity(double)
163    */
 
164  140177 toggle public void incActivity(double claInc) {
165  140177 activity += claInc;
166    }
167   
168    /*
169    * (non-Javadoc)
170    *
171    * @see org.sat4j.minisat.core.Constr#getActivity()
172    */
 
173  140177 toggle public double getActivity() {
174  140177 return activity;
175    }
176   
177    /*
178    * (non-Javadoc)
179    *
180    * @see org.sat4j.minisat.core.Constr#locked()
181    */
 
182  0 toggle public boolean locked() {
183  0 return voc.getReason(lits[0]) == this;
184    }
185   
186    /*
187    * (non-Javadoc)
188    *
189    * @see org.sat4j.minisat.core.Constr#setLearnt()
190    */
 
191  25424 toggle public void setLearnt() {
192  25424 learnt = true;
193    }
194   
195    /*
196    * (non-Javadoc)
197    *
198    * @see org.sat4j.minisat.core.Constr#register()
199    */
 
200  349960 toggle public void register() {
201  349960 for (int p : lits) {
202  1768809 voc.watch(p ^ 1, this);
203    }
204  349960 if (learnt) {
205  25424 for (int p : lits) {
206  722650 if (voc.isFalsified(p)) {
207  697226 voc.undos(p ^ 1).push(this);
208  697226 falsified++;
209    }
210    }
211  25424 assert falsified == lits.length - 1;
212    }
213    }
214   
215    /*
216    * (non-Javadoc)
217    *
218    * @see org.sat4j.minisat.core.Constr#rescaleBy(double)
219    */
 
220  2678398 toggle public void rescaleBy(double d) {
221  2678398 activity *= d;
222    }
223   
224    /*
225    * (non-Javadoc)
226    *
227    * @see org.sat4j.minisat.core.Constr#size()
228    */
 
229  309137286 toggle public int size() {
230  309137286 return lits.length;
231    }
232   
233    /*
234    * (non-Javadoc)
235    *
236    * @see org.sat4j.minisat.core.Constr#get(int)
237    */
 
238  288804396 toggle public int get(int i) {
239  288804396 return lits[i];
240    }
241   
242    /*
243    * (non-Javadoc)
244    *
245    * @see org.sat4j.minisat.core.Constr#assertConstraint(org.sat4j.minisat.core.UnitPropagationListener)
246    */
 
247  11741951 toggle public void assertConstraint(UnitPropagationListener s) {
248  11741951 assert voc.isUnassigned(lits[0]);
249  11741951 boolean ret = s.enqueue(lits[0], this);
250  11741951 assert ret;
251    }
252   
 
253  0 toggle @Override
254    public String toString() {
255  0 StringBuffer stb = new StringBuffer();
256  0 for (int i = 0; i < lits.length; i++) {
257  0 stb.append(lits[i]);
258  0 stb.append("["); //$NON-NLS-1$
259  0 stb.append(voc.valueToString(lits[i]));
260  0 stb.append("]"); //$NON-NLS-1$
261  0 stb.append(" "); //$NON-NLS-1$
262    }
263  0 return stb.toString();
264    }
265    }
 
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.