Clover coverage report -

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

FRAMES NO FRAMES

file stats:	LOC:	68		Methods:	3
	NCLOC:	47		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		public abstract class AbstractCardinalityDataStructure extends
22		AbstractDataStructureFactory {
23
24		/*
25		* Create a Cardinality Constraint from a PB format. The coefs should all be
26		* equal to 1.
27		*/
28	3123	@Override
29		public Constr createPseudoBooleanConstraint(IVecInt literals,
30		IVec<BigInteger> coefs, boolean moreThan, BigInteger degree)
31		throws ContradictionException {
32	3123	BigInteger diff = reduceToCard(coefs, literals);
33	3123	degree = degree.add(diff);
34		assert allAtOne(coefs);
35	3123	if (moreThan) {
36	2850	return AtLeast.atLeastNew(solver, getVocabulary(), literals, degree
37		.intValue());
38		}
39	273	for (int i = 0; i < literals.size(); i++) {
40	1932	literals.set(i, literals.get(i) ^ 1);
41		}
42	273	return AtLeast.atLeastNew(solver, getVocabulary(), literals, coefs
43		.size()
44		- degree.intValue());
45		}
46
47	3123	private boolean allAtOne(IVec<BigInteger> v) {
48	3123	for (int i = 0; i < v.size(); i++) {
49	55404	if (!v.get(i).equals(BigInteger.ONE))
50	0	return false;
51		}
52	3123	return true;
53		}
54
55	3123	private BigInteger reduceToCard(IVec<BigInteger> coefs, IVecInt literals) {
56	3123	int diff = 0;
57	3123	for (int i = 0; i < coefs.size(); i++) {
58		assert coefs.get(i).abs().equals(BigInteger.ONE);
59	55404	if (coefs.get(i).signum() < 0) {
60		assert coefs.get(i).equals(BigInteger.ONE.negate());
61	25380	diff++;
62	25380	literals.set(i, literals.get(i) ^ 1);
63	25380	coefs.set(i, BigInteger.ONE);
64		}
65		}
66	3123	return BigInteger.valueOf(diff);
67		}
68		}