Clover coverage report -

Coverage timestamp: ven. févr. 24 2006 06:59:02 CET

FRAMES NO FRAMES

file stats:	LOC:	150		Methods:	18
	NCLOC:	105		Classes:	1

Source file

Conditionals

Statements

Methods

TOTAL

Constraint.java

1		/**
2		*
3		*/
4		package org.sat4j.ubcsat.structure;
5
6		import org.sat4j.core.VecInt;
7		import org.sat4j.specs.IVecInt;
8		import org.sat4j.ubcsat.lit.Lits;
9
10		/**
11		* @author bourgeois
12		*/
13		public class Constraint {
14
15		private final static int INITIAL_CAPACITY_OF_VEC = 10;
16
17		// TODO Remplacer par Vec<VecInt>
18		private VecInt[] constr = new VecInt[INITIAL_CAPACITY_OF_VEC];
19
20		// TODO Remplacer par Vec<VecInt>
21		// litClause[j] = list of clauses literal j appears in
22		private VecInt[] litClause = new VecInt[INITIAL_CAPACITY_OF_VEC];
23
24		// TODO Remplacer par VecInt
25		// numLitOcc[j] = number of times literal j occurs
26		private int[] numLitOcc = new int[INITIAL_CAPACITY_OF_VEC];
27
28		// TODO Remplacer par VecInt
29		private int[] numTrueLit;
30
31		private int sizeVec = 0;
32
33		private int sizeLitClause = INITIAL_CAPACITY_OF_VEC;
34
35		private int sizeNumLitOcc = INITIAL_CAPACITY_OF_VEC;
36
37	0	public Constraint() {
38	0	for (int i = 0; i < INITIAL_CAPACITY_OF_VEC; i++) {
39	0	numLitOcc[i] = 0;
40	0	constr[i] = new VecInt();
41	0	litClause[i] = new VecInt();
42		}
43		}
44
45	0	private void growVec(int nClauses) {
46	0	if (nClauses > INITIAL_CAPACITY_OF_VEC) {
47	0	VecInt[] nConstr = new VecInt[nClauses];
48	0	System.arraycopy(constr, 0, nConstr, 0, sizeVec);
49	0	constr = nConstr;
50	0	constr[sizeVec] = new VecInt();
51		}
52		}
53
54		/*
55		* public void initNumLitOcc() { for(int i=0;i<numLitOcc.length;i++)
56		* numLitOcc[i] = 0; }
57		*/
58	0	private void createLitClause(IVecInt v) {
59	0	for (int i = 0; i < v.size(); i++) {
60	0	growLitClause(v.get(i));
61	0	growNumLitOcc(v.get(i));
62	0	numLitOcc[v.get(i)]++;
63		assert litClause[v.get(i)] != null;
64	0	litClause[v.get(i)].push(sizeVec);
65		}
66		}
67
68	0	private void growLitClause(int i) {
69	0	if (i >= sizeLitClause) {
70	0	VecInt[] nLitClause = new VecInt[i + 1];
71	0	System.arraycopy(litClause, 0, nLitClause, 0, sizeLitClause);
72	0	litClause = nLitClause;
73
74	0	for (int j = sizeLitClause; j <= i; j++)
75	0	litClause[j] = new VecInt();
76	0	sizeLitClause = i + 1;
77		}
78		}
79
80	0	private void growNumLitOcc(int i) {
81	0	if (i >= sizeNumLitOcc) {
82	0	int[] nNumLitOcc = new int[i + 1];
83	0	System.arraycopy(numLitOcc, 0, nNumLitOcc, 0, sizeNumLitOcc);
84	0	numLitOcc = nNumLitOcc;
85	0	for (int j = sizeNumLitOcc; j <= i; j++)
86	0	numLitOcc[j] = 0;
87	0	sizeNumLitOcc = i + 1;
88		}
89		}
90
91	0	public void addClause(IVecInt literals) {
92	0	growVec(sizeVec + 1);
93	0	IVecInt lit = convertLiterals(literals);
94	0	lit.sort();
95	0	createLitClause(lit);
96	0	constr[sizeVec++].pushAll(lit);
97		}
98
99	0	private IVecInt convertLiterals(IVecInt literals) {
100	0	IVecInt lit = new VecInt();
101	0	for (int i = 0; i < literals.size(); i++) {
102	0	lit.push(Lits.getLit(literals.get(i)));
103		}
104	0	return lit;
105		}
106
107	0	public int getConstrSize(int index) {
108	0	return constr[index].size();
109		}
110
111	0	public int getLit(int i, int j) {
112	0	return constr[i].get(j);
113		}
114
115	0	public void createNumTrueLit(int nClauses) {
116	0	numTrueLit = new int[nClauses];
117		}
118
119	0	public int getNumTrueLit(int index) {
120	0	return numTrueLit[index];
121		}
122
123	0	public void setNumTrueLit(int index, int val) {
124	0	numTrueLit[index] = val;
125		}
126
127	0	public void incNumTrueLit(int index) {
128	0	numTrueLit[index]++;
129		}
130
131	0	public void decNumTrueLit(int index) {
132	0	numTrueLit[index]--;
133		}
134
135	0	public IVecInt getOneConstr(int index) {
136	0	return constr[index];
137		}
138
139	0	public IVecInt getLitClause(int index) {
140	0	return litClause[index];
141		}
142
143	0	public int getNumLitOcc(int lit) {
144	0	return numLitOcc[lit];
145		}
146
147	0	public int size() {
148	0	return sizeVec;
149		}
150		}