Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
23   128   5   1,77
12   71   0,74   13
13     1,31  
1    
 
  AtLeastPB       Line # 36 23 5 60,4% 0.6041667
AtLeastPB(ILits,IVecInt,int)   AtLeastPB(ILits,IVecInt,int) 45 45 2.0 2 1.0 1 1.0 100% 1.0
atLeastNew(UnitPropagationListener,ILits,IVecInt,int) : AtLeastPB   atLeastNew(UnitPropagationListener,ILits,IVecInt,int) : AtLeastPB 50 50 4.0 4 2.0 2 0.6666667 66,7% 0.6666667
atLeastNew(ILits,IVecInt,int) : AtLeastPB   atLeastNew(ILits,IVecInt,int) : AtLeastPB 58 58 1.0 1 1.0 1 1.0 100% 1.0
getCoef(int) : BigInteger   getCoef(int) : BigInteger 62 62 1.0 1 1.0 1 1.0 100% 1.0
getDegree() : BigInteger   getDegree() : BigInteger 66 66 1.0 1 1.0 1 1.0 100% 1.0
getVocabulary() : ILits   getVocabulary() : ILits 70 70 1.0 1 1.0 1 1.0 100% 1.0
getLits() : int[]   getLits() : int[] 74 74 3.0 3 1.0 1 0.0 0% 0.0
getCoefs() : BigInteger[]   getCoefs() : BigInteger[] 80 80 4.0 4 2.0 2 0.0 0% 0.0
learnt() : boolean   learnt() : boolean 98 98 1.0 1 1.0 1 0.0 0% 0.0
setLearnt() : void   setLearnt() : void 103 103 1.0 1 1.0 1 1.0 100% 1.0
register() : void   register() : void 108 108 0.0 0 1.0 1 0.5 50% 0.5
assertConstraint(UnitPropagationListener) : void   assertConstraint(UnitPropagationListener) : void 114 114 3.0 3 3.0 3 0.8888889 88,9% 0.8888889
computeAnImpliedClause() : IVecInt   computeAnImpliedClause() : IVecInt 124 124 1.0 1 1.0 1 0.0 0% 0.0
 
  (43)
 
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    package org.sat4j.minisat.constraints.pb;
26   
27    import java.math.BigInteger;
28   
29    import org.sat4j.minisat.constraints.card.AtLeast;
30    import org.sat4j.minisat.core.Constr;
31    import org.sat4j.minisat.core.ILits;
32    import org.sat4j.minisat.core.UnitPropagationListener;
33    import org.sat4j.specs.ContradictionException;
34    import org.sat4j.specs.IVecInt;
35   
 
36    public class AtLeastPB extends AtLeast implements PBConstr {
37   
38    /**
39    *
40    */
41    private static final long serialVersionUID = 1L;
42   
43    private final BigInteger degree;
44   
 
45  9921 toggle private AtLeastPB(ILits voc, IVecInt ps, int degree) {
46  9921 super(voc, ps, degree);
47  9921 this.degree = BigInteger.valueOf(degree);
48    }
49   
 
50  9206 toggle public static AtLeastPB atLeastNew(UnitPropagationListener s, ILits voc,
51    IVecInt ps, int n) throws ContradictionException {
52  9206 int degree = niceParameters(s, voc, ps, n);
53  9206 if (degree == 0)
54  0 return null;
55  9206 return new AtLeastPB(voc, ps, degree);
56    }
57   
 
58  715 toggle public static AtLeastPB atLeastNew(ILits voc, IVecInt ps, int n) {
59  715 return new AtLeastPB(voc, ps, n);
60    }
61   
 
62  395797 toggle public BigInteger getCoef(int literal) {
63  395797 return BigInteger.ONE;
64    }
65   
 
66  10490 toggle public BigInteger getDegree() {
67  10490 return degree;
68    }
69   
 
70  203015 toggle public ILits getVocabulary() {
71  203015 return voc;
72    }
73   
 
74  0 toggle public int[] getLits() {
75  0 int[] tmp = new int[size()];
76  0 System.arraycopy(lits, 0, tmp, 0, size());
77  0 return tmp;
78    }
79   
 
80  0 toggle public BigInteger[] getCoefs() {
81  0 BigInteger[] tmp = new BigInteger[size()];
82  0 for (int i = 0; i < tmp.length; i++)
83  0 tmp[i] = BigInteger.ONE;
84  0 return tmp;
85    }
86   
87    /**
88    *
89    */
90    private boolean learnt = false;
91   
92    /**
93    * D?termine si la contrainte est apprise
94    *
95    * @return true si la contrainte est apprise, false sinon
96    * @see Constr#learnt()
97    */
 
98  0 toggle @Override
99    public boolean learnt() {
100  0 return learnt;
101    }
102   
 
103  715 toggle @Override
104    public void setLearnt() {
105  715 learnt = true;
106    }
107   
 
108  715 toggle @Override
109    public void register() {
110  715 assert learnt;
111    // countFalsified();
112    }
113   
 
114  715 toggle @Override
115    public void assertConstraint(UnitPropagationListener s) {
116  203060 for (int i = 0; i < size(); i++) {
117  202345 if (getVocabulary().isUnassigned(get(i))) {
118  8344 boolean ret = s.enqueue(get(i), this);
119  8344 assert ret;
120    }
121    }
122    }
123   
 
124  0 toggle public IVecInt computeAnImpliedClause() {
125  0 return null;
126    }
127   
128    }