Clover coverage report -

Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST

FRAMES NO FRAMES

file stats:	LOC:	187		Methods:	14
	NCLOC:	138		Classes:	1

Source file

Conditionals

Statements

Methods

TOTAL

MapPb.java

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.minisat.constraints.cnf.Lits;
14		import org.sat4j.specs.IVec;
15		import org.sat4j.specs.IVecInt;
16
17		/**
18		* @author parrain TODO To change the template for this generated type comment
19		* go to Window - Preferences - Java - Code Style - Code Templates
20		*/
21		public class MapPb implements IDataStructurePB {
22
23		/*
24		* During the process of cutting planes, pseudo-boolean constraints are
25		* coded with a HashMap <literal, coefficient> and a BigInteger for the
26		* degree.
27		*/
28		protected Map<Integer, BigInteger> coefs;
29
30		protected BigInteger degree;
31
32	0	MapPb(Map<Integer, BigInteger> m, BigInteger d) {
33	0	coefs = m;
34	0	degree = d;
35		}
36
37	0	MapPb() {
38	0	this(new HashMap<Integer, BigInteger>(), BigInteger.ZERO);
39		}
40
41	0	public BigInteger saturation() {
42		assert degree.signum() > 0;
43	0	BigInteger minimum = degree;
44	0	for (Map.Entry<Integer, BigInteger> e : coefs.entrySet()) {
45		assert e.getValue().signum() > 0;
46	0	e.setValue(degree.min(e.getValue()));
47		assert e.getValue().signum() > 0;
48	0	minimum = minimum.min(e.getValue());
49		}
50		// on a appris une clause
51	0	if (minimum.equals(degree) && minimum.compareTo(BigInteger.ONE) > 0) {
52	0	degree = BigInteger.ONE;
53	0	for (Integer i : coefs.keySet())
54	0	coefs.put(i, BigInteger.ONE);
55		}
56
57	0	return degree;
58		}
59
60	0	public BigInteger cuttingPlane(PBConstr cpb, BigInteger deg,
61		BigInteger[] reducedCoefs) {
62	0	return cuttingPlane(cpb, deg, reducedCoefs, BigInteger.ONE);
63		}
64
65	0	public BigInteger cuttingPlane(PBConstr cpb, BigInteger degreeCons,
66		BigInteger[] reducedCoefs, BigInteger coefMult) {
67	0	degree = degree.add(degreeCons);
68		assert degree.signum() > 0;
69
70	0	if (reducedCoefs == null)
71	0	for (int i = 0; i < cpb.size(); i++)
72	0	cuttingPlane(cpb.get(i), multiplyCoefficient(cpb.getCoef(i), coefMult));
73		else
74	0	for (int i = 0; i < cpb.size(); i++)
75	0	cuttingPlane(cpb.get(i), multiplyCoefficient(reducedCoefs[i], coefMult));
76
77	0	return degree;
78		}
79
80	0	public BigInteger cuttingPlane(int[] lits, BigInteger[] reducedCoefs,
81		BigInteger deg) {
82	0	return cuttingPlane(lits, reducedCoefs, deg, BigInteger.ONE);
83		}
84
85	0	public BigInteger cuttingPlane(int lits[], BigInteger[] reducedCoefs,
86		BigInteger degreeCons, BigInteger coefMult) {
87	0	degree = degree.add(degreeCons);
88		assert degree.signum() > 0;
89
90	0	for (int i = 0; i < lits.length; i++)
91	0	cuttingPlane(lits[i], reducedCoefs[i].multiply(coefMult));
92
93	0	return degree;
94		}
95
96	0	private void cuttingPlane(final int lit, final BigInteger coef) {
97		assert coef.signum() >= 0;
98	0	if (coef.signum() > 0) {
99	0	if (coefs.containsKey(lit ^ 1)) {
100		assert !coefs.containsKey(lit);
101	0	if (coefs.get(lit ^ 1).compareTo(coef) < 0) {
102	0	BigInteger tmp = coefs.get(lit ^ 1);
103	0	coefs.put(lit, coef.subtract(tmp));
104		assert coefs.get(lit).signum() > 0;
105	0	degree = degree.subtract(tmp);
106	0	coefs.remove(lit ^ 1);
107		} else {
108	0	if (coefs.get(lit ^ 1).equals(coef)) {
109	0	degree = degree.subtract(coef);
110	0	coefs.remove(lit ^ 1);
111		} else {
112	0	coefs.put(lit ^ 1, coefs.get(lit ^ 1).subtract(coef));
113		assert coefs.get(lit ^ 1).signum() > 0;
114	0	degree = degree.subtract(coef);
115		}
116		}
117		} else {
118		assert (!coefs.containsKey(lit))
119		\|\| (coefs.get(lit).signum() > 0);
120	0	coefs.put(lit, (coefs.containsKey(lit) ? coefs.get(lit)
121		: BigInteger.ZERO).add(coef));
122		assert coefs.get(lit).signum() > 0;
123		}
124		}
125		assert (!coefs.containsKey(lit ^ 1)) \|\| (!coefs.containsKey(lit));
126		}
127
128	0	public void buildConstraintFromConflict(IVecInt resLits,
129		IVec<BigInteger> resCoefs) {
130	0	resLits.clear();
131	0	resCoefs.clear();
132		// On recherche tous les litt?raux concern?s
133	0	for (Map.Entry<Integer, BigInteger> e : coefs.entrySet()) {
134	0	resLits.push(e.getKey());
135		assert e.getValue().signum() > 0;
136	0	resCoefs.push(e.getValue());
137		}
138		};
139
140	0	public void buildConstraintFromMapPb(int[] resLits, BigInteger[] resCoefs) {
141		// On recherche tous les litt?raux concern?s
142		assert resLits.length == resCoefs.length;
143		assert resLits.length == coefs.keySet().size();
144	0	int i = 0;
145	0	for (Map.Entry<Integer, BigInteger> e : coefs.entrySet()) {
146	0	resLits[i] = e.getKey();
147		assert e.getValue().signum() > 0;
148	0	resCoefs[i] = e.getValue();
149	0	i++;
150		}
151		};
152
153	0	public BigInteger getDegree() {
154	0	return degree;
155		}
156
157	0	public int size() {
158	0	return coefs.keySet().size();
159		}
160
161		/*
162		* (non-Javadoc)
163		*
164		* @see java.lang.Object#toString()
165		*/
166	0	@Override
167		public String toString() {
168	0	StringBuilder stb = new StringBuilder();
169	0	for (Map.Entry<Integer, BigInteger> entry : coefs.entrySet()) {
170	0	stb.append(entry.getValue());
171	0	stb.append(".");
172	0	stb.append(Lits.toString(entry.getKey()));
173	0	stb.append(" ");
174		}
175	0	return stb.toString() + " >= " + degree; //$NON-NLS-1$
176		}
177
178	0	private BigInteger multiplyCoefficient(BigInteger coef,
179		BigInteger mult) {
180	0	if (coef.equals(BigInteger.ONE))
181	0	return mult;
182		else
183	0	return coef.multiply(mult);
184		}
185
186
187		}