Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
35   193   12   2,69
22   91   0,69   13
13     1,85  
1    
 
  MinWatchCardPB       Line # 36 35 12 60% 0.6
 
  (43)
 
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    package org.sat4j.minisat.constraints.pb;
26   
27    import java.math.BigInteger;
28   
29    import org.sat4j.minisat.constraints.card.MinWatchCard;
30    import org.sat4j.minisat.core.Constr;
31    import org.sat4j.minisat.core.ILits;
32    import org.sat4j.minisat.core.UnitPropagationListener;
33    import org.sat4j.specs.ContradictionException;
34    import org.sat4j.specs.IVecInt;
35   
 
36    public class MinWatchCardPB extends MinWatchCard implements PBConstr {
37   
38    /**
39    *
40    */
41    private static final long serialVersionUID = 1L;
42   
43    private final BigInteger degree;
44   
 
45  1335 toggle public MinWatchCardPB(ILits voc, IVecInt ps, boolean moreThan, int degree) {
46  1335 super(voc, ps, moreThan, degree);
47  1335 this.degree = BigInteger.valueOf(degree);
48    }
49   
 
50  18412 toggle public MinWatchCardPB(ILits voc, IVecInt ps, int degree) {
51  18412 super(voc, ps, degree);
52  18412 this.degree = BigInteger.valueOf(degree);
53    }
54   
55    /*
56    * (non-Javadoc)
57    *
58    * @see org.sat4j.minisat.constraints.pb.PBConstr#getCoefficient(int)
59    */
 
60  676686 toggle public BigInteger getCoef(int literal) {
61  676686 return BigInteger.ONE;
62    }
63   
64    /*
65    * (non-Javadoc)
66    *
67    * @see org.sat4j.minisat.constraints.pb.PBConstr#getDegree()
68    */
 
69  14435 toggle public BigInteger getDegree() {
70  14435 return degree;
71    }
72   
 
73  0 toggle public BigInteger[] getCoefs() {
74  0 BigInteger[] tmp = new BigInteger[size()];
75  0 for (int i = 0; i < tmp.length; i++)
76  0 tmp[i] = BigInteger.ONE;
77  0 return tmp;
78    }
79   
80    /**
81    * Permet la cr?ation de contrainte de cardinalit? ? observation minimale
82    *
83    * @param s
84    * outil pour la propagation des litt?raux
85    * @param voc
86    * vocabulaire utilis? par la contrainte
87    * @param ps
88    * liste des litt?raux de la nouvelle contrainte
89    * @param degree
90    * fournit le degr? de la contrainte
91    * @return une nouvelle clause si tout va bien, null sinon
92    * @throws ContradictionException
93    */
 
94  18412 toggle public static MinWatchCardPB normalizedMinWatchCardPBNew(
95    UnitPropagationListener s, ILits voc, IVecInt ps, int degree)
96    throws ContradictionException {
97  18412 return minWatchCardPBNew(s, voc, ps, ATLEAST, degree, true);
98    }
99   
100    /**
101    * Permet la cr?ation de contrainte de cardinalit? ? observation minimale
102    *
103    * @param s
104    * outil pour la propagation des litt?raux
105    * @param voc
106    * vocabulaire utilis? par la contrainte
107    * @param ps
108    * liste des litt?raux de la nouvelle contrainte
109    * @param moreThan
110    * d?termine si c'est une sup?rieure ou ?gal ? l'origine
111    * @param degree
112    * fournit le degr? de la contrainte
113    * @return une nouvelle clause si tout va bien, null sinon
114    * @throws ContradictionException
115    */
 
116  0 toggle public static MinWatchCardPB minWatchCardPBNew(UnitPropagationListener s,
117    ILits voc, IVecInt ps, boolean moreThan, int degree)
118    throws ContradictionException {
119  0 return minWatchCardPBNew(s, voc, ps, moreThan, degree, false);
120    }
121   
 
122  18412 toggle private static MinWatchCardPB minWatchCardPBNew(UnitPropagationListener s,
123    ILits voc, IVecInt ps, boolean moreThan, int degree,
124    boolean normalized) throws ContradictionException {
125  18412 int mydegree = degree + linearisation(voc, ps);
126   
127  18412 if (ps.size() == 0 && mydegree > 0) {
128  0 throw new ContradictionException();
129  18412 } else if (ps.size() == mydegree || ps.size() <= 0) {
130  0 for (int i = 0; i < ps.size(); i++)
131  0 if (!s.enqueue(ps.get(i))) {
132  0 throw new ContradictionException();
133    }
134  0 return null;
135    }
136   
137    // constraint is now instanciated
138  18412 MinWatchCardPB retour = null;
139  18412 if (normalized)
140  18412 retour = new MinWatchCardPB(voc, ps, mydegree);
141    else
142  0 retour = new MinWatchCardPB(voc, ps, moreThan, mydegree);
143   
144  18412 if (retour.degree.signum() <= 0)
145  0 return null;
146   
147  18412 retour.computeWatches();
148   
149  18412 return ((MinWatchCardPB) retour.computePropagation(s));
150    }
151   
152    /**
153    *
154    */
155    private boolean learnt = false;
156   
157    /**
158    * D?termine si la contrainte est apprise
159    *
160    * @return true si la contrainte est apprise, false sinon
161    * @see Constr#learnt()
162    */
 
163  19747 toggle @Override
164    public boolean learnt() {
165  19747 return learnt;
166    }
167   
 
168  1335 toggle @Override
169    public void setLearnt() {
170  1335 learnt = true;
171    }
172   
 
173  1335 toggle @Override
174    public void register() {
175  1335 assert learnt;
176  1335 computeWatches();
177    }
178   
 
179  1335 toggle @Override
180    public void assertConstraint(UnitPropagationListener s) {
181  398528 for (int i = 0; i < size(); i++) {
182  397193 if (getVocabulary().isUnassigned(get(i))) {
183  16530 boolean ret = s.enqueue(get(i), this);
184  16530 assert ret;
185    }
186    }
187    }
188   
 
189  0 toggle public IVecInt computeAnImpliedClause() {
190  0 return null;
191    }
192   
193    }
 
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.