Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
37   187   8   4,11
12   85   0,43   9
9     1,78  
1    
 
  PuebloMinWatchPb       Line # 38 37 8 72,4% 0.7241379
 
  (71)
 
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.pb;
27   
28    import java.math.BigInteger;
29   
30    import org.sat4j.core.Vec;
31    import org.sat4j.core.VecInt;
32    import org.sat4j.minisat.core.ILits;
33    import org.sat4j.minisat.core.UnitPropagationListener;
34    import org.sat4j.specs.ContradictionException;
35    import org.sat4j.specs.IVec;
36    import org.sat4j.specs.IVecInt;
37   
 
38    public class PuebloMinWatchPb extends MinWatchPb {
39   
40    private static final long serialVersionUID = 1L;
41   
42    /**
43    * Constructeur de base des contraintes
44    *
45    * @param voc
46    * Informations sur le vocabulaire employ???
47    * @param ps
48    * Liste des litt???raux
49    * @param coefs
50    * Liste des coefficients
51    * @param moreThan
52    * Indication sur le comparateur
53    * @param degree
54    * Stockage du degr??? de la contrainte
55    */
 
56  307879 toggle private PuebloMinWatchPb(ILits voc, IDataStructurePB mpb) {
57   
58  307879 super(voc, mpb);
59    }
60   
61    /**
62    * @param s
63    * outil pour la propagation des litt???raux
64    * @param ps
65    * liste des litt???raux de la nouvelle contrainte
66    * @param coefs
67    * liste des coefficients des litt???raux de la contrainte
68    * @param moreThan
69    * d???termine si c'est une sup???rieure ou ???gal ??? l'origine
70    * @param degree
71    * fournit le degr??? de la contrainte
72    * @return une nouvelle clause si tout va bien, ou null si un conflit est
73    * d???tect???
74    */
 
75  830 toggle public static PuebloMinWatchPb minWatchPbNew(UnitPropagationListener s,
76    ILits voc, IVecInt ps, IVecInt coefs, boolean moreThan, int degree)
77    throws ContradictionException {
78  830 return minWatchPbNew(s, voc, ps, toVecBigInt(coefs), moreThan,
79    toBigInt(degree));
80    }
81   
82    /**
83    * @param s
84    * outil pour la propagation des litt???raux
85    * @param ps
86    * liste des litt???raux de la nouvelle contrainte
87    * @param coefs
88    * liste des coefficients des litt???raux de la contrainte
89    * @param moreThan
90    * d???termine si c'est une sup???rieure ou ???gal ??? l'origine
91    * @param degree
92    * fournit le degr??? de la contrainte
93    * @return une nouvelle clause si tout va bien, ou null si un conflit est
94    * d???tect???
95    */
 
96  281099 toggle public static PuebloMinWatchPb minWatchPbNew(UnitPropagationListener s,
97    ILits voc, IVecInt ps, IVec<BigInteger> coefs, boolean moreThan,
98    BigInteger degree) throws ContradictionException {
99    // Il ne faut pas modifier les param?tres
100  281099 VecInt litsVec = new VecInt(ps.size());
101  281099 IVec<BigInteger> coefsVec = new Vec<BigInteger>(coefs.size());
102  281099 ps.copyTo(litsVec);
103  281099 coefs.copyTo(coefsVec);
104   
105    // Ajouter les simplifications quand la structure sera d???finitive
106  281099 IDataStructurePB mpb = niceParameters(litsVec, coefsVec, moreThan,
107    degree, voc);
108  281099 PuebloMinWatchPb outclause = new PuebloMinWatchPb(voc, mpb);
109   
110  281099 if (outclause.degree.signum() <= 0) {
111  0 return null;
112    }
113   
114  281099 outclause.computeWatches();
115   
116  281084 outclause.computePropagation(s);
117   
118  281084 return outclause;
119   
120    }
121   
 
122  0 toggle public static PuebloMinWatchPb minWatchPbNew(UnitPropagationListener s,
123    ILits voc, IDataStructurePB mpb) throws ContradictionException {
124  0 PuebloMinWatchPb outclause = new PuebloMinWatchPb(voc, mpb);
125   
126  0 if (outclause.degree.signum() <= 0) {
127  0 return null;
128    }
129   
130  0 outclause.computeWatches();
131   
132  0 outclause.computePropagation(s);
133   
134  0 return outclause;
135   
136    }
137   
138    /**
139    *
140    */
 
141  0 toggle public static WatchPb watchPbNew(ILits voc, IVecInt lits, IVecInt coefs,
142    boolean moreThan, int degree) {
143  0 return watchPbNew(voc, lits, toVecBigInt(coefs), moreThan,
144    toBigInt(degree));
145    }
146   
147    /**
148    *
149    */
 
150  26780 toggle public static WatchPb watchPbNew(ILits voc, IVecInt lits,
151    IVec<BigInteger> coefs, boolean moreThan, BigInteger degree) {
152  26780 IDataStructurePB mpb = null;
153  26780 mpb = niceCheckedParameters(lits, coefs, moreThan, degree, voc);
154  26780 return new PuebloMinWatchPb(voc, mpb);
155    }
156   
 
157  0 toggle public static WatchPb normalizedWatchPbNew(ILits voc, IDataStructurePB mpb) {
158  0 return new PuebloMinWatchPb(voc, mpb);
159    }
160   
 
161  100331732 toggle @Override
162    protected BigInteger maximalCoefficient(int pIndice) {
163  100331732 return coefs[0];
164    }
165   
 
166  100331732 toggle @Override
167    protected BigInteger updateWatched(BigInteger mc, int pIndice) {
168  100331732 BigInteger maxCoef = mc;
169  100331732 if (watchingCount < size()) {
170  83424453 BigInteger upWatchCumul = watchCumul.subtract(coefs[pIndice]);
171  83424453 BigInteger borneSup = degree.add(maxCoef);
172  1047897147 for (int ind = 0; ind < lits.length
173    && upWatchCumul.compareTo(borneSup) < 0; ind++) {
174  964472694 if (!voc.isFalsified(lits[ind]) && !watched[ind]) {
175  60557205 upWatchCumul = upWatchCumul.add(coefs[ind]);
176  60557205 watched[ind] = true;
177  60557205 assert watchingCount < size();
178  60557205 watching[watchingCount++] = ind;
179  60557205 voc.watch(lits[ind] ^ 1, this);
180    }
181    }
182  83424453 watchCumul = upWatchCumul.add(coefs[pIndice]);
183    }
184  100331732 return maxCoef;
185    }
186   
187    }
 
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.