Clover coverage report -

Coverage timestamp: jeu. sept. 29 2005 23:57:39 CEST

FRAMES NO FRAMES

file stats:	LOC:	129		Methods:	8
	NCLOC:	101		Classes:	1

Source file

Conditionals

Statements

Methods

TOTAL

MapPb.java

100%

97,7%

100%

98,5%

1		/*
2		* Created on Jan 20, 2005
3		*
4		* TODO To change the template for this generated file go to
5		* Window - Preferences - Java - Code Style - Code Templates
6		*/
7		package org.sat4j.minisat.constraints.pb;
8
9		import java.math.BigInteger;
10		import java.util.HashMap;
11		import java.util.Map;
12
13		import org.sat4j.specs.IVec;
14		import org.sat4j.specs.IVecInt;
15
16		/**
17		* @author parrain TODO To change the template for this generated type comment
18		* go to Window - Preferences - Java - Code Style - Code Templates
19		*/
20		class MapPb {
21
22		protected Map<Integer, BigInteger> coefs;
23
24		protected BigInteger degree;
25
26	1684360	MapPb(Map<Integer, BigInteger> m, BigInteger d) {
27	1684360	coefs = m;
28	1684360	degree = d;
29		}
30
31	1621870	MapPb() {
32	1621870	this(new HashMap<Integer, BigInteger>(), BigInteger.ZERO);
33		}
34
35	2201892	BigInteger saturation() {
36		assert degree.signum() > 0;
37	2201892	BigInteger minimum = degree;
38	2201892	for (Map.Entry<Integer, BigInteger> e : coefs.entrySet()) {
39		assert e.getValue().signum() > 0;
40	27202145	e.setValue(degree.min(e.getValue()));
41		assert e.getValue().signum() > 0;
42	27202145	minimum = minimum.min(e.getValue());
43		}
44		// on a appris une clause
45	2201892	if (minimum.equals(degree) && minimum.compareTo(BigInteger.ONE) > 0) {
46	28	degree = BigInteger.ONE;
47	28	for (Integer i : coefs.keySet())
48	0	coefs.put(i, BigInteger.ONE);
49		}
50
51	2201892	return degree;
52		}
53
54	1621870	BigInteger addCoeffNewConstraint(int[] lits, BigInteger[] coefsBis,
55		BigInteger deg) {
56	1621870	return addCoeffNewConstraint(lits, coefsBis, deg, BigInteger.ONE);
57		}
58
59	2201892	BigInteger addCoeffNewConstraint(int[] litsCons, BigInteger[] coefsCons,
60		BigInteger degreeCons, BigInteger coefMult) {
61	2201892	int lit;
62	2201892	BigInteger coef;
63	2201892	degree = degree.add(degreeCons);
64		assert degree.signum() > 0;
65	2201892	for (int i = 0; i < litsCons.length; i++) {
66	14111207	lit = litsCons[i];
67	14111207	coef = coefsCons[i].multiply(coefMult);
68		assert coef.signum() >= 0;
69	14111207	if (coef.signum() > 0) {
70	13982671	if (!coefs.containsKey(lit ^ 1)) {
71		assert (!coefs.containsKey(lit))
72		\|\| (coefs.get(lit).signum() > 0);
73	13308576	coefs.put(lit, (coefs.containsKey(lit) ? coefs.get(lit)
74		: BigInteger.ZERO).add(coef));
75		assert coefs.get(lit).signum() > 0;
76		} else {
77		assert !coefs.containsKey(lit);
78	674095	if (coefs.get(lit ^ 1).compareTo(coef) < 0) {
79	16238	coefs.put(lit, coef.subtract(coefs.get(lit ^ 1)));
80		assert coefs.get(lit).signum() > 0;
81	16238	degree = degree.subtract(coefs.get(lit ^ 1));
82	16238	coefs.remove(lit ^ 1);
83		} else {
84	657857	if (coefs.get(lit ^ 1).equals(coef)) {
85	649954	degree = degree.subtract(coef);
86	649954	coefs.remove(lit ^ 1);
87		} else {
88	7903	coefs.put(lit ^ 1, coefs.get(lit ^ 1)
89		.subtract(coef));
90		assert coefs.get(lit ^ 1).signum() > 0;
91	7903	degree = degree.subtract(coef);
92		}
93		}
94		}
95		}
96		assert (!coefs.containsKey(lit ^ 1)) \|\| (!coefs.containsKey(lit));
97		}
98	2201892	return degree;
99		}
100
101	62490	void buildConstraintFromConflict(IVecInt resLits, IVec<BigInteger> resCoefs) {
102	62490	resLits.clear();
103	62490	resCoefs.clear();
104		// On recherche tous les litt?raux concern?s
105	62490	for (Map.Entry<Integer, BigInteger> e : coefs.entrySet()) {
106	1959104	resLits.push(e.getKey());
107		assert e.getValue().signum() > 0;
108	1959104	resCoefs.push(e.getValue());
109		}
110		};
111
112	1621870	void buildConstraintFromMapPb(int[] resLits, BigInteger[] resCoefs) {
113		// On recherche tous les litt?raux concern?s
114		assert resLits.length == resCoefs.length;
115		assert resLits.length == coefs.keySet().size();
116	1621870	int i = 0;
117	1621870	for (Map.Entry<Integer, BigInteger> e : coefs.entrySet()) {
118	9064750	resLits[i] = e.getKey();
119		assert e.getValue().signum() > 0;
120	9064750	resCoefs[i] = e.getValue();
121	9064750	i++;
122		}
123		};
124
125	1621870	int size() {
126	1621870	return coefs.keySet().size();
127		}
128
129		}