Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
30   143   5   5
30   80   0,33   6
6     1,67  
1    
 
  PBSolver       Line # 49 30 5 74,2% 0.74242425
 
  (135)
 
1    /*
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le Berre
3    *
4    * Based on the original minisat specification from:
5    *
6    * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
7    * Sixth International Conference on Theory and Applications of Satisfiability
8    * Testing, LNCS 2919, pp 502-518, 2003.
9    *
10    * This library is free software; you can redistribute it and/or modify it under
11    * the terms of the GNU Lesser General Public License as published by the Free
12    * Software Foundation; either version 2.1 of the License, or (at your option)
13    * any later version.
14    *
15    * This library is distributed in the hope that it will be useful, but WITHOUT
16    * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
17    * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
18    * details.
19    *
20    * You should have received a copy of the GNU Lesser General Public License
21    * along with this library; if not, write to the Free Software Foundation, Inc.,
22    * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
23    *
24    */
25   
26    package org.sat4j.minisat.constraints.pb;
27   
28    import java.math.BigInteger;
29   
30    import org.sat4j.core.Vec;
31    import org.sat4j.core.VecInt;
32    import org.sat4j.minisat.core.AssertingClauseGenerator;
33    import org.sat4j.minisat.core.Constr;
34    import org.sat4j.minisat.core.DataStructureFactory;
35    import org.sat4j.minisat.core.Handle;
36    import org.sat4j.minisat.core.ILits;
37    import org.sat4j.minisat.core.IOrder;
38    import org.sat4j.minisat.core.LearningStrategy;
39    import org.sat4j.minisat.core.RestartStrategy;
40    import org.sat4j.minisat.core.SearchParams;
41    import org.sat4j.minisat.core.Solver;
42    import org.sat4j.specs.IVec;
43    import org.sat4j.specs.IVecInt;
44   
45    /**
46    * @author parrain To change the template for this generated type comment go to
47    * Window - Preferences - Java - Code Generation - Code and Comments
48    */
 
49    public class PBSolver<L extends ILits> extends Solver<L> {
50   
51    private static final long serialVersionUID = 1L;
52   
53    /**
54    * @param acg
55    * @param learner
56    * @param dsf
57    */
 
58  699 toggle public PBSolver(AssertingClauseGenerator acg, LearningStrategy<L> learner,
59    DataStructureFactory<L> dsf, IOrder<L> order) {
60  699 super(acg, learner, dsf, new SearchParams(1.5, 100), order);
61    }
62   
 
63  0 toggle public PBSolver(AssertingClauseGenerator acg, LearningStrategy<L> learner, DataStructureFactory<L> dsf, SearchParams params, IOrder<L> order, RestartStrategy restarter) {
64  0 super(acg, learner, dsf, params, order, restarter);
65    }
66   
 
67  0 toggle public PBSolver(AssertingClauseGenerator acg, LearningStrategy<L> learner, DataStructureFactory<L> dsf, SearchParams params, IOrder<L> order) {
68  0 super(acg, learner, dsf, params, order);
69    }
70   
 
71  1281751 toggle @Override
72    public int analyze(Constr myconfl, Handle<Constr> outLearntRef) {
73   
74    // first literal implied in the conflict
75  1281751 int litImplied = trail.last();
76  1281751 int currentLevel = voc.getLevel(litImplied);
77   
78  1281751 IConflict confl = chooseConflict(myconfl, currentLevel);
79  1281751 BigInteger resDegree = confl.getDegree();
80  1281751 assert confl.slackConflict().signum() < 0;
81  20548149 while (!confl.isAssertive(currentLevel)) {
82  19266524 PBConstr constraint = (PBConstr) voc.getReason(litImplied);
83    // result of the resolution is in the conflict (confl)
84  19266524 resDegree = confl.resolve(constraint, litImplied, this);
85  19266524 assert confl.slackConflict().signum() <= 0;
86    // implication trail is reduced
87  19266524 if (trail.size() == 1)
88  126 break;
89  19266398 undoOne();
90  19266398 assert decisionLevel() > 0;
91  19266398 litImplied = trail.last();
92  19266398 if (voc.getLevel(litImplied) != currentLevel) {
93  121471 trailLim.pop();
94  121471 confl.updateSlack(voc.getLevel(litImplied));
95    }
96  19266398 assert voc.getLevel(litImplied) <= currentLevel;
97  19266398 currentLevel = voc.getLevel(litImplied);
98  19266398 assert confl.slackIsCorrect(currentLevel);
99  19266398 assert currentLevel == decisionLevel();
100  19266398 assert litImplied > 1;
101    }
102   
103  1281751 assert currentLevel == decisionLevel();
104  1281751 assert decisionLevel() != 0;
105   
106  1281751 undoOne();
107   
108    // necessary informations to build a PB-constrinat
109    // are kept from the conflict
110  1281751 IVecInt resLits = new VecInt();
111  1281751 IVec<BigInteger> resCoefs = new Vec<BigInteger>();
112  1281751 confl.buildConstraintFromConflict(resLits, resCoefs);
113   
114  1281751 assert resLits.size() == resCoefs.size();
115   
116  1281751 if (resLits.size() == 0) {
117  126 outLearntRef.obj = null;
118  126 return -1;
119    }
120   
121    // assertive PB-constraint is build and referenced
122  1281625 PBConstr resConstr = (PBConstr) dsfactory
123    .createUnregisteredPseudoBooleanConstraint(resLits, resCoefs,
124    resDegree);
125   
126  1281625 outLearntRef.obj = resConstr;
127    // the conflict give the highest decision level for the backtrack
128    // (which is less than current level)
129  1281625 assert confl.isAssertive(currentLevel);
130  1281625 return confl.getBacktrackLevel(currentLevel);
131    }
132   
 
133  1079520 toggle IConflict chooseConflict(Constr myconfl, int level) {
134  1079520 return ConflictMap.createConflict((PBConstr) myconfl, level);
135    }
136   
 
137  0 toggle @Override
138    public String toString(String prefix) {
139  0 return prefix + "Cutting planes based inference ("
140    + this.getClass().getName() + ")\n" + super.toString(prefix);
141    }
142   
143    }
 
CloverReport generated by Clover Code Coverage v2.0a5
mer. juin 27 2007 07:27:33 CEST.		   Beta Testers License registered to clover-support@cenqua.com. This license of Clover2 is provided for beta testing only. You have 5 day(s) before your Beta Tester License expires.