Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
20   130   4   2
8   53   0,65   10
10     1,3  
1    
 
  MixableCBClausePB       Line # 34 20 4 55,3% 0.55263156
 
  (53)
 
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.cnf.MixableCBClause;
30    import org.sat4j.minisat.core.ILits;
31    import org.sat4j.minisat.core.UnitPropagationListener;
32    import org.sat4j.specs.IVecInt;
33   
 
34    public class MixableCBClausePB extends MixableCBClause implements PBConstr {
35   
36    /**
37    *
38    */
39    private static final long serialVersionUID = 1L;
40   
 
41  0 toggle public MixableCBClausePB(IVecInt ps, ILits voc, boolean learnt) {
42  0 super(ps, voc, learnt);
43    }
44   
 
45  96167 toggle public MixableCBClausePB(IVecInt ps, ILits voc) {
46  96167 super(ps, voc);
47    }
48   
 
49  73623 toggle public static MixableCBClausePB brandNewClause(UnitPropagationListener s,
50    ILits voc, IVecInt literals) {
51  73623 MixableCBClausePB c = new MixableCBClausePB(literals, voc);
52  73623 c.register();
53  73623 return c;
54    }
55   
56    /*
57    * (non-Javadoc)
58    *
59    * @see org.sat4j.minisat.constraints.pb.PBConstr#computeAnImpliedClause()
60    */
 
61  0 toggle public IVecInt computeAnImpliedClause() {
62  0 return null;
63    }
64   
65    /*
66    * (non-Javadoc)
67    *
68    * @see org.sat4j.minisat.constraints.pb.PBConstr#getCoef(int)
69    */
 
70  2927324 toggle public BigInteger getCoef(int literal) {
71  2927324 return BigInteger.ONE;
72    }
73   
74    /*
75    * (non-Javadoc)
76    *
77    * @see org.sat4j.minisat.constraints.pb.PBConstr#getCoefs()
78    */
 
79  0 toggle public BigInteger[] getCoefs() {
80  0 BigInteger[] tmp = new BigInteger[size()];
81  0 for (int i = 0; i < tmp.length; i++)
82  0 tmp[i] = BigInteger.ONE;
83  0 return tmp;
84    }
85   
86    /*
87    * (non-Javadoc)
88    *
89    * @see org.sat4j.minisat.constraints.pb.PBConstr#getDegree()
90    */
 
91  179932 toggle public BigInteger getDegree() {
92  179932 return BigInteger.ONE;
93    }
94   
95    /*
96    * (non-Javadoc)
97    *
98    * @see org.sat4j.minisat.constraints.pb.PBConstr#getLits()
99    */
 
100  0 toggle public int[] getLits() {
101  0 int[] tmp = new int[size()];
102  0 System.arraycopy(lits, 0, tmp, 0, size());
103  0 return tmp;
104    }
105   
106    /*
107    * (non-Javadoc)
108    *
109    * @see org.sat4j.minisat.constraints.pb.PBConstr#getVocabulary()
110    */
 
111  367880 toggle public ILits getVocabulary() {
112  367880 return voc;
113    }
114   
115    /*
116    * (non-Javadoc)
117    *
118    * @see org.sat4j.minisat.core.Constr#assertConstraint(org.sat4j.minisat.core.UnitPropagationListener)
119    */
 
120  22544 toggle @Override
121    public void assertConstraint(UnitPropagationListener s) {
122  344655 for (int i = 0; i < size(); i++)
123  344655 if (getVocabulary().isUnassigned(get(i))) {
124  22544 boolean ret = s.enqueue(get(i), this);
125  22544 assert ret;
126  22544 break;
127    }
128    }
129   
130    }