Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
73   292   21   3,84
32   144   0,53   19
19     2,05  
1    
 
  AtLeast       Line # 46 73 21 67,7% 0.67741936
 
  (163)
 
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.card;
27   
28    import java.io.Serializable;
29   
30    import org.sat4j.minisat.constraints.cnf.Lits;
31    import org.sat4j.minisat.core.Constr;
32    import org.sat4j.minisat.core.ILits;
33    import org.sat4j.minisat.core.Undoable;
34    import org.sat4j.minisat.core.UnitPropagationListener;
35    import org.sat4j.specs.ContradictionException;
36    import org.sat4j.specs.IVecInt;
37   
38    /*
39    * Created on 8 janv. 2004 To change the template for this generated file go to
40    * Window>Preferences>Java>Code Generation>Code and Comments
41    */
42   
43    /**
44    * @author leberre Contrainte de cardinalit?
45    */
 
46    public class AtLeast implements Constr, Undoable, Serializable {
47   
48    private static final long serialVersionUID = 1L;
49   
50    /** number of allowed falsified literal */
51    protected int maxUnsatisfied;
52   
53    /** current number of falsified literals */
54    private int counter;
55   
56    /**
57    * constraint literals
58    */
59    protected final int[] lits;
60   
61    protected final ILits voc;
62   
63    /**
64    * @param ps
65    * a vector of literals
66    * @param degree
67    * the minimal number of satisfied literals
68    */
 
69  262661 toggle protected AtLeast(ILits voc, IVecInt ps, int degree) {
70  262661 maxUnsatisfied = ps.size() - degree;
71  262661 this.voc = voc;
72  262661 counter = 0;
73  262661 lits = new int[ps.size()];
74  262661 ps.moveTo(lits);
75  262661 for (int q : lits) {
76  1204846 voc.watch(q ^ 1, this);
77    }
78    }
79   
 
80  262023 toggle protected static int niceParameters(UnitPropagationListener s, ILits voc,
81    IVecInt ps, int deg) throws ContradictionException {
82   
83  262023 if (ps.size() < deg)
84  40 throw new ContradictionException();
85  261983 int degree = deg;
86  1265303 for (int i = 0; i < ps.size();) {
87    // on verifie si le litteral est affecte
88  1003320 if (voc.isUnassigned(ps.get(i))) {
89    // go to next literal
90  1002993 i++;
91    } else {
92    // Si le litteral est satisfait,
93    // ?a revient ? baisser le degr?
94  327 if (voc.isSatisfied(ps.get(i))) {
95  153 degree--;
96    }
97    // dans tous les cas, s'il est assign?,
98    // on enleve le ieme litteral
99  327 ps.delete(i);
100    }
101    }
102   
103    // on trie le vecteur ps
104  261983 ps.sortUnique();
105    // ?limine les clauses tautologiques
106    // deux litt?raux de signe oppos?s apparaissent dans la m?me
107    // clause
108   
109  261983 if (ps.size() == degree) {
110  409 for (int i = 0; i < ps.size(); i++) {
111  387 if (!s.enqueue(ps.get(i))) {
112  0 throw new ContradictionException();
113    }
114    }
115  22 return 0;
116    }
117   
118  261961 if (ps.size() < degree)
119  15 throw new ContradictionException();
120  261946 return degree;
121   
122    }
123   
 
124  252817 toggle public static AtLeast atLeastNew(UnitPropagationListener s, ILits voc,
125    IVecInt ps, int n) throws ContradictionException {
126  252817 int degree = niceParameters(s, voc, ps, n);
127  252762 if (degree == 0)
128  22 return null;
129  252740 return new AtLeast(voc, ps, degree);
130    }
131   
132    /*
133    * (non-Javadoc)
134    *
135    * @see Constr#remove(Solver)
136    */
 
137  0 toggle public void remove() {
138  0 for (int q : lits) {
139  0 voc.watches(q ^ 1).remove(this);
140    }
141    }
142   
143    /*
144    * (non-Javadoc)
145    *
146    * @see Constr#propagate(Solver, Lit)
147    */
 
148  616062127 toggle public boolean propagate(UnitPropagationListener s, int p) {
149    // remet la clause dans la liste des clauses regardees
150  616062127 voc.watch(p, this);
151   
152  616062127 if (counter == maxUnsatisfied)
153  23408530 return false;
154   
155  592653597 counter++;
156  592653597 voc.undos(p).push(this);
157   
158    // If no more can be false, enqueue the rest:
159  592653597 if (counter == maxUnsatisfied)
160  371005830 for (int q : lits) {
161  2083632095 if (voc.isUnassigned(q) && !s.enqueue(q, this)) {
162  0 return false;
163    }
164    }
165  592653597 return true;
166    }
167   
168    /*
169    * (non-Javadoc)
170    *
171    * @see Constr#simplify(Solver)
172    */
 
173  0 toggle public boolean simplify() {
174  0 return false;
175    }
176   
177    /*
178    * (non-Javadoc)
179    *
180    * @see Constr#undo(Solver, Lit)
181    */
 
182  592614568 toggle public void undo(int p) {
183  592614568 counter--;
184    }
185   
186    /*
187    * (non-Javadoc)
188    *
189    * @see Constr#calcReason(Solver, Lit, Vec)
190    */
 
191  210121076 toggle public void calcReason(int p, IVecInt outReason) {
192  210121076 int c = (p == ILits.UNDEFINED) ? -1 : 0;
193  210121076 for (int q : lits) {
194  1301428297 if (voc.isFalsified(q)) {
195  756410115 outReason.push(q ^ 1);
196  756410115 if (++c == maxUnsatisfied)
197  210121076 return;
198    }
199    }
200    }
201   
202    /*
203    * (non-Javadoc)
204    *
205    * @see org.sat4j.minisat.datatype.Constr#learnt()
206    */
 
207  210121076 toggle public boolean learnt() {
208    // Ces contraintes ne sont pas apprises pour le moment.
209  210121076 return false;
210    }
211   
212    /*
213    * (non-Javadoc)
214    *
215    * @see org.sat4j.minisat.datatype.Constr#getActivity()
216    */
 
217  0 toggle public double getActivity() {
218    // TODO Auto-generated method stub
219  0 return 0;
220    }
221   
222    /*
223    * (non-Javadoc)
224    *
225    * @see org.sat4j.minisat.datatype.Constr#incActivity(double)
226    */
 
227  0 toggle public void incActivity(double claInc) {
228    // TODO Auto-generated method stub
229   
230    }
231   
232    /*
233    * For learnt clauses only @author leberre
234    */
 
235  0 toggle public boolean locked() {
236    // FIXME need to be adapted to AtLeast
237    // return lits[0].getReason() == this;
238  0 return true;
239    }
240   
 
241  0 toggle public void setLearnt() {
242  0 throw new UnsupportedOperationException();
243    }
244   
 
245  0 toggle public void register() {
246  0 throw new UnsupportedOperationException();
247    }
248   
 
249  785108 toggle public int size() {
250  785108 return lits.length;
251    }
252   
 
253  1370269 toggle public int get(int i) {
254  1370269 return lits[i];
255    }
256   
 
257  0 toggle public void rescaleBy(double d) {
258  0 throw new UnsupportedOperationException();
259    }
260   
 
261  0 toggle public void assertConstraint(UnitPropagationListener s) {
262  0 throw new UnsupportedOperationException();
263    }
264   
265    /**
266    * Cha?ne repr?sentant la contrainte
267    *
268    * @return Cha?ne repr?sentant la contrainte
269    */
 
270  0 toggle @Override
271    public String toString() {
272  0 StringBuffer stb = new StringBuffer();
273  0 stb.append("Card (" + lits.length + ") : ");
274  0 for (int i = 0; i < lits.length; i++) {
275    // if (voc.isUnassigned(lits[i])) {
276  0 stb.append(" + "); //$NON-NLS-1$
277  0 stb.append(Lits.toString(this.lits[i]));
278  0 stb.append("[");
279  0 stb.append(voc.valueToString(lits[i]));
280  0 stb.append("@");
281  0 stb.append(voc.getLevel(lits[i]));
282  0 stb.append("]");
283  0 stb.append(" ");
284  0 stb.append(" "); //$NON-NLS-1$
285    }
286  0 stb.append(">= "); //$NON-NLS-1$
287  0 stb.append(size() - maxUnsatisfied);
288   
289  0 return stb.toString();
290    }
291   
292    }
 
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.