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
 
  (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    }