Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
72   245   21   3,79
56   165   0,54   19
19     2,05  
1    
 
  MapPb       Line # 42 72 21 82,3% 0.82312924
 
  (181)
 
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    import java.util.HashMap;
30    import java.util.Map;
31   
32    import org.sat4j.minisat.constraints.cnf.Lits;
33    import org.sat4j.minisat.core.ILits;
34    import org.sat4j.minisat.core.VarActivityListener;
35    import org.sat4j.specs.IVec;
36    import org.sat4j.specs.IVecInt;
37   
38    /**
39    * @author parrain TODO To change the template for this generated type comment
40    * go to Window - Preferences - Java - Code Style - Code Templates
41    */
 
42    public class MapPb implements IDataStructurePB {
43   
44    /*
45    * During the process of cutting planes, pseudo-boolean constraints are
46    * coded with a HashMap <literal, coefficient> and a BigInteger for the
47    * degree.
48    */
49    protected Map<Integer, BigInteger> coefs;
50   
51    protected BigInteger degree;
52   
 
53  4179060 toggle MapPb(Map<Integer, BigInteger> m, BigInteger d) {
54  4179060 coefs = m;
55  4179060 degree = d;
56    }
57   
 
58  2897309 toggle MapPb(ILits lits) {
59  2897309 this();
60    }
61   
 
62  2897309 toggle MapPb() {
63  2897309 this(new HashMap<Integer, BigInteger>(), BigInteger.ZERO);
64    }
65   
 
66  12860111 toggle public BigInteger saturation() {
67  12860111 assert degree.signum() > 0;
68  12860111 BigInteger minimum = degree;
69  12860111 for (Map.Entry<Integer, BigInteger> e : coefs.entrySet()) {
70  304463204 assert e.getValue().signum() > 0;
71    // e.setValue(degree.min(e.getValue()));
72  304463204 if (degree.compareTo(e.getValue()) < 0)
73  48526689 setCoef(e.getKey(), degree);
74  304463204 assert e.getValue().signum() > 0;
75  304463204 minimum = minimum.min(e.getValue());
76    }
77    // on a appris une clause
78  12860111 if (minimum.equals(degree) && minimum.compareTo(BigInteger.ONE) > 0) {
79  128 degree = BigInteger.ONE;
80  128 for (Integer i : coefs.keySet())
81    // coefs.put(i, BigInteger.ONE);
82  236 setCoef(i, BigInteger.ONE);
83    }
84   
85  12860111 return degree;
86    }
87   
 
88  0 toggle public BigInteger cuttingPlane(PBConstr cpb, BigInteger deg,
89    BigInteger[] reducedCoefs, VarActivityListener val) {
90  0 return cuttingPlane(cpb, deg, reducedCoefs, BigInteger.ONE, val);
91    }
92   
 
93  9962802 toggle public BigInteger cuttingPlane(PBConstr cpb, BigInteger degreeCons,
94    BigInteger[] reducedCoefs, BigInteger coefMult,
95    VarActivityListener val) {
96  9962802 degree = degree.add(degreeCons);
97  9962802 assert degree.signum() > 0;
98   
99  9962802 if (reducedCoefs == null)
100  101359207 for (int i = 0; i < cpb.size(); i++) {
101  91406114 val.varBumpActivity(cpb.get(i));
102  91406114 cuttingPlaneStep(cpb.get(i), multiplyCoefficient(
103    cpb.getCoef(i), coefMult));
104    }
105    else
106  1304388 for (int i = 0; i < cpb.size(); i++) {
107  1294679 val.varBumpActivity(cpb.get(i));
108  1294679 cuttingPlaneStep(cpb.get(i), multiplyCoefficient(
109    reducedCoefs[i], coefMult));
110    }
111   
112  9962802 return degree;
113    }
114   
 
115  2897309 toggle public BigInteger cuttingPlane(int[] lits, BigInteger[] reducedCoefs,
116    BigInteger deg) {
117  2897309 return cuttingPlane(lits, reducedCoefs, deg, BigInteger.ONE);
118    }
119   
 
120  2897309 toggle public BigInteger cuttingPlane(int lits[], BigInteger[] reducedCoefs,
121    BigInteger degreeCons, BigInteger coefMult) {
122  2897309 degree = degree.add(degreeCons);
123  2897309 assert degree.signum() > 0;
124   
125  24340395 for (int i = 0; i < lits.length; i++)
126  21443086 cuttingPlaneStep(lits[i], reducedCoefs[i].multiply(coefMult));
127   
128  2897309 return degree;
129    }
130   
 
131  114143879 toggle private void cuttingPlaneStep(final int lit, final BigInteger coef) {
132  114143879 assert coef.signum() >= 0;
133  114143879 Integer blit = Integer.valueOf(lit);
134  114143879 Integer bnlit = Integer.valueOf(lit ^ 1);
135  114143879 if (coef.signum() > 0) {
136  113809097 if (coefs.containsKey(bnlit)) {
137  10300679 assert !coefs.containsKey(blit);
138  10300679 if (coefs.get(bnlit).compareTo(coef) < 0) {
139  54456 BigInteger tmp = coefs.get(bnlit);
140    // coefs.put(blit, coef.subtract(tmp));
141  54456 setCoef(blit, coef.subtract(tmp));
142  54456 assert coefs.get(blit).signum() > 0;
143  54456 degree = degree.subtract(tmp);
144    // coefs.remove(bnlit);
145  54456 removeCoef(bnlit);
146    } else {
147  10246223 if (coefs.get(bnlit).equals(coef)) {
148  10221495 degree = degree.subtract(coef);
149    // coefs.remove(bnlit);
150  10221495 removeCoef(bnlit);
151    } else {
152    // coefs.put(bnlit, coefs.get(bnlit).subtract(coef));
153  24728 decreaseCoef(bnlit, coef);
154  24728 assert coefs.get(bnlit).signum() > 0;
155  24728 degree = degree.subtract(coef);
156    }
157    }
158    } else {
159  103508418 assert (!coefs.containsKey(blit))
160    || (coefs.get(blit).signum() > 0);
161  103508418 if (coefs.containsKey(blit))
162  49412296 increaseCoef(blit, coef);
163    else
164  54096122 setCoef(blit, coef);
165    // coefs.put(blit, (coefs.containsKey(blit) ? coefs.get(blit)
166    // : BigInteger.ZERO).add(coef));
167  103508418 assert coefs.get(blit).signum() > 0;
168    }
169    }
170  114143879 assert (!coefs.containsKey(bnlit)) || (!coefs.containsKey(blit));
171    }
172   
 
173  1281751 toggle public void buildConstraintFromConflict(IVecInt resLits,
174    IVec<BigInteger> resCoefs) {
175  1281751 resLits.clear();
176  1281751 resCoefs.clear();
177    // On recherche tous les litt?raux concern?s
178  1281751 for (Map.Entry<Integer, BigInteger> e : coefs.entrySet()) {
179  38539982 resLits.push(e.getKey());
180  38539982 assert e.getValue().signum() > 0;
181  38539982 resCoefs.push(e.getValue());
182    }
183    };
184   
 
185  2897309 toggle public void buildConstraintFromMapPb(int[] resLits, BigInteger[] resCoefs) {
186    // On recherche tous les litt?raux concern?s
187  2897309 assert resLits.length == resCoefs.length;
188  2897309 assert resLits.length == coefs.keySet().size();
189  2897309 int i = 0;
190  2897309 for (Map.Entry<Integer, BigInteger> e : coefs.entrySet()) {
191  21443086 resLits[i] = e.getKey();
192  21443086 assert e.getValue().signum() > 0;
193  21443086 resCoefs[i] = e.getValue();
194  21443086 i++;
195    }
196    };
197   
 
198  4604088 toggle public BigInteger getDegree() {
199  4604088 return degree;
200    }
201   
 
202  2897309 toggle public int size() {
203  2897309 return coefs.keySet().size();
204    }
205   
206    /*
207    * (non-Javadoc)
208    *
209    * @see java.lang.Object#toString()
210    */
 
211  0 toggle @Override
212    public String toString() {
213  0 StringBuilder stb = new StringBuilder();
214  0 for (Map.Entry<Integer, BigInteger> entry : coefs.entrySet()) {
215  0 stb.append(entry.getValue());
216  0 stb.append(".");
217  0 stb.append(Lits.toString(entry.getKey()));
218  0 stb.append(" ");
219    }
220  0 return stb.toString() + " >= " + degree; //$NON-NLS-1$
221    }
222   
 
223  92700793 toggle private BigInteger multiplyCoefficient(BigInteger coef, BigInteger mult) {
224  92700793 if (coef.equals(BigInteger.ONE))
225  91947715 return mult;
226  753078 return coef.multiply(mult);
227    }
228   
 
229  49412296 toggle void increaseCoef(Integer lit, BigInteger incCoef) {
230  49412296 coefs.put(lit, coefs.get(lit).add(incCoef));
231    }
232   
 
233  24728 toggle void decreaseCoef(Integer lit, BigInteger decCoef) {
234  24728 coefs.put(lit, coefs.get(lit).subtract(decCoef));
235    }
236   
 
237  102975143 toggle void setCoef(Integer lit, BigInteger newValue) {
238  102975143 coefs.put(lit, newValue);
239    }
240   
 
241  10275951 toggle void removeCoef(Integer lit) {
242  10275951 coefs.remove(lit);
243    }
244   
245    }
 
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.