Clover coverage report -

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

FRAMES NO FRAMES

file stats:	LOC:	69		Methods:	3
	NCLOC:	48		Classes:	1

Source file

Conditionals

Statements

Methods

TOTAL

AbstractCardinalityDataStructure.java

91,7%

94,4%

100%

93,9%

1		/*
2		* Created on 16 avr. 2004
3		*
4		* To change the template for this generated file go to
5		* Window - Preferences - Java - Code Generation - Code and Comments
6		*/
7		package org.sat4j.minisat.constraints;
8
9		import java.math.BigInteger;
10
11		import org.sat4j.minisat.constraints.card.AtLeast;
12		import org.sat4j.minisat.core.Constr;
13		import org.sat4j.specs.ContradictionException;
14		import org.sat4j.specs.IVec;
15		import org.sat4j.specs.IVecInt;
16
17		/**
18		* @author leberre To change the template for this generated type comment go to
19		* Window - Preferences - Java - Code Generation - Code and Comments
20		*/
21		@SuppressWarnings("PMD")
22		public abstract class AbstractCardinalityDataStructure extends
23		AbstractDataStructureFactory {
24
25		/*
26		* Create a Cardinality Constraint from a PB format. The coefs should all be
27		* equal to 1.
28		*/
29	3123	@Override
30		public Constr createPseudoBooleanConstraint(IVecInt literals,
31		IVec<BigInteger> coefs, boolean moreThan, BigInteger degree)
32		throws ContradictionException {
33	3123	BigInteger diff = reduceToCard(coefs, literals);
34	3123	degree = degree.add(diff);
35		assert coefficientsEqualToOne(coefs);
36	3123	if (moreThan) {
37	2850	return AtLeast.atLeastNew(solver, getVocabulary(), literals, degree
38		.intValue());
39		}
40	273	for (int i = 0; i < literals.size(); i++) {
41	1932	literals.set(i, literals.get(i) ^ 1);
42		}
43	273	return AtLeast.atLeastNew(solver, getVocabulary(), literals, coefs
44		.size()
45		- degree.intValue());
46		}
47
48	3123	public static boolean coefficientsEqualToOne(IVec<BigInteger> v) {
49	3123	for (int i = 0; i < v.size(); i++) {
50	55404	if (!v.get(i).equals(BigInteger.ONE))
51	0	return false;
52		}
53	3123	return true;
54		}
55
56	3123	private BigInteger reduceToCard(IVec<BigInteger> coefs, IVecInt literals) {
57	3123	int diff = 0;
58	3123	for (int i = 0; i < coefs.size(); i++) {
59		assert coefs.get(i).abs().equals(BigInteger.ONE);
60	55404	if (coefs.get(i).signum() < 0) {
61		assert coefs.get(i).equals(BigInteger.ONE.negate());
62	25380	diff++;
63	25380	literals.set(i, literals.get(i) ^ 1);
64	25380	coefs.set(i, BigInteger.ONE);
65		}
66		}
67	3123	return BigInteger.valueOf(diff);
68		}
69		}