Clover coverage report -

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

FRAMES NO FRAMES

file stats:	LOC:	126		Methods:	2
	NCLOC:	68		Classes:	1

Source file

Conditionals

Statements

Methods

TOTAL

PBSolver.java

85,7%

90,9%

100%

89,8%

1		/*
2		* Created on Jun 3, 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.minisat.constraints.pb;
8
9		import java.math.BigInteger;
10
11		import org.sat4j.core.Vec;
12		import org.sat4j.core.VecInt;
13		import org.sat4j.minisat.core.AssertingClauseGenerator;
14		import org.sat4j.minisat.core.Constr;
15		import org.sat4j.minisat.core.DataStructureFactory;
16		import org.sat4j.minisat.core.Handle;
17		import org.sat4j.minisat.core.IOrder;
18		import org.sat4j.minisat.core.LearningStrategy;
19		import org.sat4j.minisat.core.Solver;
20		import org.sat4j.specs.IVec;
21		import org.sat4j.specs.IVecInt;
22
23		/**
24		* @author parrain To change the template for this generated type comment go to
25		* Window - Preferences - Java - Code Generation - Code and Comments
26		*/
27		public class PBSolver extends Solver {
28
29		private static final long serialVersionUID = 1L;
30
31		/**
32		* @param acg
33		* @param learner
34		* @param dsf
35		*/
36	314	public PBSolver(AssertingClauseGenerator acg, LearningStrategy learner,
37		DataStructureFactory dsf,IOrder order) {
38	314	super(acg, learner, dsf,order);
39		}
40
41	62490	@Override
42		public int analyze(Constr myconfl, Handle<Constr> outLearntRef) {
43		// Logger logger = Logger.getLogger("org.sat4j.minisat.constraints.pb");
44
45	62490	Conflict confl = ((WatchPb) myconfl).createConflict();
46	62490	BigInteger resDegree = confl.getDegree();
47
48		// logger.fine("Analyse");
49		// logger.fine("Init " + confl);
50		// Premier litt?ral impliqu? dans le conflit
51
52	62490	int litImplied = trail.last();
53	62490	int currentLevel = voc.getLevel(litImplied);
54	62490	int originalLevel = currentLevel;
55		assert confl.slackConflict().signum() < 0;
56
57	62490	while (!confl.isAssertive(currentLevel)) {
58		// logger.fine("Resolving on " + Lits.toString(litImplied) + "@"
59		// + currentLevel);
60
61		// On effectue la r?solution
62	2611561	WatchPb constraint = (WatchPb) voc.getReason(litImplied);
63	2611561	if (constraint != null) {
64		// logger.fine("Res with " + Lits.toString(litImplied) + " on "
65		// + constraint);
66
67		// on effectue la resolution
68		// le resultat est dans le conflit
69	2584713	resDegree = confl.resolve(constraint, litImplied);
70		assert confl.slackConflict().signum() <= 0;
71		// assert !confl.isTriviallyUnsat();
72		// } else {
73		// logger.fine("No reason for " + Lits.toString(litImplied));
74		}
75		// On remonte l'arbre des implications
76	2611561	if (trail.size() == 1)
77	28	break;
78	2611533	undoOne();
79	2611533	if (decisionLevel() > 0) {
80	2611533	litImplied = trail.last();
81	2611533	if (voc.getLevel(litImplied) != currentLevel)
82	26820	trailLim.pop();
83	2611533	currentLevel = voc.getLevel(litImplied);
84		} else
85	0	break;
86		assert currentLevel == decisionLevel();
87		assert litImplied > 1;
88		}
89		assert currentLevel == decisionLevel();
90	62490	if (decisionLevel() == 0) {
91	0	outLearntRef.obj = null;
92	0	return -1;
93		}
94
95	62490	undoOne();
96
97		// On reprend les ?l?ments n?cessaires ? la construction d'une
98		// PB-contrainte
99		// ? partir du conflit
100	62490	IVecInt resLits = new VecInt();
101	62490	IVec<BigInteger> resCoefs = new Vec<BigInteger>();
102	62490	confl.buildConstraintFromConflict(resLits, resCoefs);
103
104		assert resLits.size() == resCoefs.size();
105
106	62490	if (resLits.size() == 0) {
107	28	outLearntRef.obj = null;
108	28	return -1;
109		}
110
111		// On construit la contrainte assertive et on la reference
112	62462	WatchPb resConstr = (WatchPb) dsfactory
113		.createUnregisteredPseudoBooleanConstraint(resLits, resCoefs,
114		resDegree);
115
116	62462	outLearntRef.obj = resConstr;
117		// logger.fine("Contrainte apprise : " + resConstr);
118		// on recupere le niveau de decision le plus haut qui est inferieur a
119		// currentlevel
120		assert confl.isAssertive(currentLevel);
121	62462	int bl = resConstr.getBacktrackLevel(currentLevel);
122		// logger.fine("Backtrack level : " + bl);
123	62462	return bl;
124		}
125
126		}