Clover Coverage Report

Coverage timestamp: mer. juin 27 2007 07:27:16 CEST

FRAMES NO FRAMES SHOW HELP

Statistics for file SingleSolutionTest.java:
Stmts:	43		LOC:	90		Total cmp:	3		Stmts/Method:	10,75
Branches:	0		NCLOC:	71		Cmp density:	0,14		Methods/Class:	4
Methods:	4					Avg method cmp:	1,5
Classes:	1

Expand All

SingleSolutionTest

Line # 13

Total Statements 43

Complexity 3

TOTAL Coverage 95,7%

0.9574468

Show Tests (2) Select All Deselect All
Highlight	Test Contribution	Test	Result
	0.42553192	org.sat4j.SingleSolutionTest.testHasASingleSolution org.sat4j.SingleSolutionTest.testHasASingleSolution	1 PASS
	0.40425533	org.sat4j.SingleSolutionTest.testHasASingleSolutionIVecInt org.sat4j.SingleSolutionTest.testHasASingleSolutionIVecInt	1 PASS

Collapse All

1

package org.sat4j;

2

3

import junit.framework.TestCase;

4

5

import org.sat4j.core.VecInt;

6

import org.sat4j.minisat.SolverFactory;

7

import org.sat4j.specs.ContradictionException;

8

import org.sat4j.specs.ISolver;

9

import org.sat4j.specs.IVecInt;

10

import org.sat4j.specs.TimeoutException;

11

import org.sat4j.tools.SingleSolutionDetector;

12

13

public class SingleSolutionTest extends TestCase {

14

15

2

public SingleSolutionTest(String name) {

16

2

17

}

18

19

2

20

protected void setUp() throws Exception {

21

2

solver = SolverFactory.newMiniSAT();

22

2

detector = new SingleSolutionDetector(solver);

23

2

detector.newVar(3);

24

}

25

26

/*

27

* Test method for

28

* 'org.sat4j.tools.SingleSolutionDetector.hasASingleSolution()'

29

*/

30

1

public void testHasASingleSolution() throws ContradictionException,

31

TimeoutException {

32

1

IVecInt clause = new VecInt();

33

1

clause.push(1).push(2);

34

1

detector.addClause(clause);

35

1

clause.clear();

36

1

clause.push(-1).push(-2);

37

1

detector.addClause(clause);

38

1

assertTrue(detector.isSatisfiable());

39

1

assertFalse(detector.hasASingleSolution());

40

1

clause.clear();

41

1

clause.push(-1).push(2);

42

1

detector.addClause(clause);

43

1

assertTrue(detector.isSatisfiable());

44

1

assertTrue(detector.hasASingleSolution());

45

1

clause.clear();

46

1

clause.push(1).push(-2);

47

1

detector.addClause(clause);

48

1

assertFalse(detector.isSatisfiable());

49

1

50

1

assertFalse(detector.hasASingleSolution());

51

0

52

} catch (UnsupportedOperationException e) {

53

// OK

54

}

55

}

56

57

/*

58

* Test method for

59

* 'org.sat4j.tools.SingleSolutionDetector.hasASingleSolution(IVecInt)'

60

*/

61

1

public void testHasASingleSolutionIVecInt() throws ContradictionException,

62

TimeoutException {

63

1

IVecInt clause = new VecInt();

64

1

clause.push(1).push(2);

65

1

detector.addClause(clause);

66

1

IVecInt assumptions = new VecInt();

67

1

assumptions.push(1);

68

1

assertTrue(detector.isSatisfiable(assumptions));

69

1

assertFalse(detector.hasASingleSolution(assumptions));

70

1

clause.clear();

71

1

clause.push(-1).push(2);

72

1

detector.addClause(clause);

73

1

assertTrue(detector.isSatisfiable(assumptions));

74

1

assertTrue(detector.hasASingleSolution(assumptions));

75

1

clause.clear();

76

1

clause.push(-1).push(-2);

77

1

detector.addClause(clause);

78

1

assertFalse(detector.isSatisfiable(assumptions));

79

1

80

1

assertFalse(detector.hasASingleSolution(assumptions));

81

0

82

} catch (UnsupportedOperationException e) {

83

// OK

84

}

85

}

86

87

private ISolver solver;

88

89

private SingleSolutionDetector detector;

90

}