Clover coverage report -

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

FRAMES NO FRAMES

file stats:	LOC:	134		Methods:	4
	NCLOC:	74		Classes:	1

Source file

Conditionals

Statements

Methods

TOTAL

PBSolver.java

85,7%

87,9%

75%

86,3%

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.SearchParams;
20		import org.sat4j.minisat.core.Solver;
21		import org.sat4j.specs.IVec;
22		import org.sat4j.specs.IVecInt;
23
24		/**
25		* @author parrain To change the template for this generated type comment go to
26		* Window - Preferences - Java - Code Generation - Code and Comments
27		*/
28		public class PBSolver extends Solver {
29
30		private static final long serialVersionUID = 1L;
31
32		/**
33		* @param acg
34		* @param learner
35		* @param dsf
36		*/
37	696	public PBSolver(AssertingClauseGenerator acg, LearningStrategy learner,
38		DataStructureFactory dsf, IOrder order) {
39	696	super(acg, learner, dsf, new SearchParams(10000.0, 100), order);
40		}
41
42	519135	@Override
43		public int analyze(Constr myconfl, Handle<Constr> outLearntRef) {
44		// Logger logger = Logger.getLogger("org.sat4j.minisat.constraints.pb");
45
46	519135	IConflict confl = chooseConflict(myconfl);
47	519135	BigInteger resDegree = confl.getDegree();
48
49		// logger.fine("Analyse");
50		// logger.fine("Init " + confl);
51		// Premier litt?ral impliqu? dans le conflit
52
53	519135	int litImplied = trail.last();
54	519135	int currentLevel = voc.getLevel(litImplied);
55		assert confl.slackConflict().signum() < 0;
56
57	519135	while (!confl.isAssertive(currentLevel)) {
58		// logger.fine("Resolving on " + Lits.toString(litImplied) + "@"
59		// + currentLevel);
60
61		// On effectue la r?solution
62	10293008	PBConstr constraint = (PBConstr) voc.getReason(litImplied);
63	10293008	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	10170753	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	10293008	if (trail.size() == 1)
77	126	break;
78	10292882	undoOne();
79	10292882	if (decisionLevel() > 0) {
80	10292882	litImplied = trail.last();
81	10292882	if (voc.getLevel(litImplied) != currentLevel)
82	122129	trailLim.pop();
83	10292882	currentLevel = voc.getLevel(litImplied);
84		} else
85	0	break;
86		assert currentLevel == decisionLevel();
87		assert litImplied > 1;
88		}
89
90		assert currentLevel == decisionLevel();
91	519135	if (decisionLevel() == 0) {
92	0	outLearntRef.obj = null;
93	0	return -1;
94		}
95
96	519135	undoOne();
97
98		// On reprend les ?l?ments n?cessaires ? la construction d'une
99		// PB-contrainte
100		// ? partir du conflit
101	519135	IVecInt resLits = new VecInt();
102	519135	IVec<BigInteger> resCoefs = new Vec<BigInteger>();
103	519135	confl.buildConstraintFromConflict(resLits, resCoefs);
104
105		assert resLits.size() == resCoefs.size();
106
107	519135	if (resLits.size() == 0) {
108	126	outLearntRef.obj = null;
109	126	return -1;
110		}
111
112		// On construit la contrainte assertive et on la reference
113	519009	PBConstr resConstr = (PBConstr) dsfactory
114		.createUnregisteredPseudoBooleanConstraint(resLits, resCoefs,
115		resDegree);
116
117	519009	outLearntRef.obj = resConstr;
118		// on recupere le niveau de decision le plus haut qui est inferieur a
119		// currentlevel
120		assert confl.isAssertive(currentLevel);
121	519009	return confl.getBacktrackLevel(currentLevel);
122		}
123
124	464657	IConflict chooseConflict(Constr myconfl) {
125	464657	return ConflictArray.createConflict((PBConstr) myconfl);
126		}
127
128	0	@Override
129		public String toString(String prefix) {
130	0	return prefix+"Cutting planes based inference\n"+super.toString(prefix);
131		}
132
133
134		}