Clover coverage report -

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

FRAMES NO FRAMES

file stats:	LOC:	49		Methods:	2
	NCLOC:	27		Classes:	1

Source file

Conditionals

Statements

Methods

TOTAL

RemiUtils.java

1		package org.sat4j.tools;
2
3		import org.sat4j.core.VecInt;
4		import org.sat4j.specs.ISolver;
5		import org.sat4j.specs.IVecInt;
6		import org.sat4j.specs.TimeoutException;
7
8		/**
9		* Class dedicated to Rmi Coletta utility methods :-)
10		*
11		* @author leberre
12		*/
13		public class RemiUtils {
14
15	0	private RemiUtils() {
16		// no instanceof that class are expected to be used.
17		}
18
19		/**
20		* Compute the set of literals common to all models of the formula.
21		*
22		* @param s
23		* a solver already feeded
24		* @return the set of literals common to all models of the formula contained
25		* in the solver, in dimacs format.
26		* @throws TimeoutException
27		*/
28	0	public static IVecInt backbone(ISolver s) throws TimeoutException {
29	0	IVecInt backbone = new VecInt();
30	0	int nvars = s.nVars();
31	0	for (int i = 1; i <= nvars; i++) {
32	0	backbone.push(i);
33	0	if (s.isSatisfiable(backbone)) {
34	0	backbone.pop().push(-i);
35	0	if (s.isSatisfiable(backbone)) {
36	0	backbone.pop();
37		} else {
38		// -i is in the backbone
39	0	backbone.pop().push(i);
40		}
41		} else {
42		// -i is in the backbone
43	0	backbone.pop().push(-i);
44		}
45		}
46	0	return backbone;
47		}
48
49		}