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