Clover coverage report -

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

FRAMES NO FRAMES

file stats:	LOC:	73		Methods:	2
	NCLOC:	41		Classes:	1

Source file

Conditionals

Statements

Methods

TOTAL

Minimal4CardinalityModel.java

83,3%

94,4%

100%

92,3%

1		/*
2		* Created on 31 mars 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.tools;
8
9		import java.io.Serializable;
10
11		import org.sat4j.core.VecInt;
12		import org.sat4j.specs.ContradictionException;
13		import org.sat4j.specs.ISolver;
14		import org.sat4j.specs.IVecInt;
15		import org.sat4j.specs.TimeoutException;
16
17		/**
18		* Computes models with a minimal number (with respect to
19		* cardinality) of negative literals. This is done be adding a
20		* constraint on the number of negative literals each time a model if
21		* found (the number of negative literals occuring in the model minus
22		* one).
23		*
24		* @author leberre
25		* @see org.sat4j.specs.ISolver#addAtMost(IVecInt, int)
26		*/
27		public class Minimal4CardinalityModel extends SolverDecorator implements
28		Serializable {
29
30		private static final long serialVersionUID = 1L;
31
32		/**
33		* @param solver
34		*/
35	1	public Minimal4CardinalityModel(ISolver solver) {
36	1	super(solver);
37		}
38
39		/*
40		* (non-Javadoc)
41		*
42		* @see org.sat4j.ISolver#model()
43		*/
44	10	@Override
45		public int[] model() {
46	10	int[] prevmodel = null;
47	10	IVecInt vec = new VecInt();
48		// backUp();
49	10	try {
50	10	do {
51	13	prevmodel = super.model();
52	13	vec.clear();
53	13	for (int i = 1; i <= nVars(); i++) {
54	39	vec.push(-i);
55		}
56	13	int counter = 0;
57	13	for (int q : prevmodel) {
58	39	if (q < 0) {
59	6	counter++;
60		}
61		}
62	13	addAtMost(vec, counter - 1);
63	3	System.err.println(counter);
64	3	} while (isSatisfiable());
65		} catch (TimeoutException e) {
66	0	System.err.println("Solver timed out"); //$NON-NLS-1$
67		} catch (ContradictionException e) {
68	10	System.err.println("added trivial unsat clauses?" + vec); //$NON-NLS-1$
69		}
70		// restore();
71	10	return prevmodel;
72		}
73		}