Clover coverage report -

Coverage timestamp: dim. nov. 12 2006 12:21:31 CET

FRAMES NO FRAMES

file stats:	LOC:	45		Methods:	3
	NCLOC:	26		Classes:	1

Source file

Conditionals

Statements

Methods

TOTAL

ConflictArrayCard.java

20%

66,7%

23,5%

1		package org.sat4j.minisat.constraints.pb;
2
3		import java.math.BigInteger;
4
5		import org.sat4j.minisat.core.ILits;
6
7		public class ConflictArrayCard extends ConflictArray {
8
9	23220	public ConflictArrayCard(int[] lits, BigInteger[] coefs, BigInteger d,
10		ILits voc, int level) {
11	23220	super(lits, coefs, d, voc, level);
12		// TODO Auto-generated constructor stub
13		}
14
15	23220	public static IConflict createConflict(PBConstr cpb, int level) {
16	23220	return new ConflictArrayCard(cpb.getLits(), cpb.getCoefs(), cpb
17		.getDegree(), cpb.getVocabulary(), level);
18		}
19
20		/**
21		* reduces the constraint defined by wpb until the result of the cutting
22		* plane is a conflict. this reduction returns a cardinality.
23		* !!!!!! this reduction is not correct !!!!!
24		* TO BE REWRITTEN
25		* @param litImplied
26		* @param ind
27		* @param reducedCoefs
28		* @param wpb
29		* @return
30		*/
31	0	@Override
32		protected BigInteger reduceUntilConflict(int litImplied, int ind,
33		BigInteger[] reducedCoefs, WatchPb wpb) {
34	0	BigInteger atleast = BigInteger.ZERO;
35	0	for (int i = 0; i < reducedCoefs.length; i++) {
36	0	if (!wpb.getVocabulary().isFalsified(wpb.get(i)))
37	0	atleast = atleast.add(BigInteger.ONE);
38	0	reducedCoefs[i] = BigInteger.ONE;
39		}
40	0	coefMultCons = coefs[litImplied ^ 1];
41	0	coefMult = BigInteger.ONE;
42	0	return atleast;
43		}
44
45		}