Clover coverage report -

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

FRAMES NO FRAMES

file stats:	LOC:	46		Methods:	1
	NCLOC:	25		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		*/
14		public class RemiUtils {
15
16		/**
17		* Compute the set of literals common to all models of the formula.
18		*
19		* @param s
20		* a solver already feeded
21		* @return the set of literals common to all models of the formula contained
22		* in the solver, in dimacs format.
23		* @throws TimeoutException
24		*/
25	0	public static IVecInt backbone(ISolver s) throws TimeoutException {
26	0	IVecInt backbone = new VecInt();
27	0	int nvars = s.nVars();
28	0	for (int i = 1; i <= nvars; i++) {
29	0	backbone.push(i);
30	0	if (!s.isSatisfiable(backbone)) {
31		// -i is in the backbone
32	0	backbone.pop().push(-i);
33		} else {
34	0	backbone.pop().push(-i);
35	0	if (!s.isSatisfiable(backbone)) {
36		// -i is in the backbone
37	0	backbone.pop().push(i);
38		} else {
39	0	backbone.pop();
40		}
41		}
42		}
43	0	return backbone;
44		}
45
46		}