Clover coverage report -

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

FRAMES NO FRAMES

file stats:	LOC:	40		Methods:	3
	NCLOC:	24		Classes:	1

Source file

Conditionals

Statements

Methods

TOTAL

ConflictArrayClause.java

100%

100%

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 ConflictArrayClause extends ConflictArray {
8
9	29214	public ConflictArrayClause(int[] lits, BigInteger[] coefs, BigInteger d,
10		ILits voc) {
11	29214	super(lits, coefs, d, voc);
12		}
13
14	29214	public static IConflict createConflict(PBConstr cpb) {
15	29214	return new ConflictArrayClause(cpb.getLits(), cpb.getCoefs(), cpb
16		.getDegree(), cpb.getVocabulary());
17		}
18
19		/**
20		* reduces the constraint defined by wpb until the result of the cutting
21		* plane is a conflict. this reduction returns a clause.
22		*
23		* @param litImplied
24		* @param ind
25		* @param reducedCoefs
26		* @param wpb
27		* @return
28		*/
29	2500	protected BigInteger reduceUntilConflict(int litImplied, int ind,
30		BigInteger[] reducedCoefs, WatchPb wpb) {
31	2500	for (int i = 0; i < reducedCoefs.length; i++)
32	301240	if (i == ind \|\| wpb.getVocabulary().isFalsified(wpb.get(i)))
33	207003	reducedCoefs[i] = BigInteger.ONE;
34		else
35	94237	reducedCoefs[i] = BigInteger.ZERO;
36	2500	coefMultCons = coefs[litImplied ^ 1];
37	2500	coefMult = BigInteger.ONE;
38	2500	return BigInteger.ONE;
39		}
40		}