Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
15   105   4   2,14
8   42   0,67   7
7     1,43  
1    
 
  WLClausePB       Line # 34 15 4 63,3% 0.6333333
 
  (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.DefaultWLClause;
30    import org.sat4j.minisat.core.ILits;
31    import org.sat4j.minisat.core.UnitPropagationListener;
32    import org.sat4j.specs.IVecInt;
33   
 
34    public class WLClausePB extends DefaultWLClause implements PBConstr {
35   
36    /**
37    *
38    */
39    private static final long serialVersionUID = 1L;
40   
 
41  1414969 toggle public WLClausePB(IVecInt ps, ILits voc) {
42  1414969 super(ps, voc);
43    // TODO Auto-generated constructor stub
44    }
45   
46    /*
47    * (non-Javadoc)
48    *
49    * @see org.sat4j.minisat.constraints.pb.PBConstr#getCoefficient(int)
50    */
 
51  117599600 toggle public BigInteger getCoef(int literal) {
52  117599600 return BigInteger.ONE;
53    }
54   
55    /*
56    * (non-Javadoc)
57    *
58    * @see org.sat4j.minisat.constraints.pb.PBConstr#getDegree()
59    */
 
60  9070241 toggle public BigInteger getDegree() {
61  9070241 return BigInteger.ONE;
62    }
63   
 
64  0 toggle public BigInteger[] getCoefs() {
65  0 BigInteger[] tmp = new BigInteger[size()];
66  0 for (int i = 0; i < tmp.length; i++)
67  0 tmp[i] = BigInteger.ONE;
68  0 return tmp;
69    }
70   
71    /**
72    * Creates a brand new clause, presumably from external data. Performs all
73    * sanity checks.
74    *
75    * @param s
76    * the object responsible for unit propagation
77    * @param voc
78    * the vocabulary
79    * @param literals
80    * the literals to store in the clause
81    * @return the created clause or null if the clause should be ignored
82    * (tautology for example)
83    */
 
84  371435 toggle public static WLClausePB brandNewClause(UnitPropagationListener s,
85    ILits voc, IVecInt literals) {
86  371435 WLClausePB c = new WLClausePB(literals, voc);
87  371435 c.register();
88  371435 return c;
89    }
90   
 
91  1043534 toggle @Override
92    public void assertConstraint(UnitPropagationListener s) {
93  15642001 for (int i = 0; i < size(); i++)
94  15642001 if (getVocabulary().isUnassigned(get(i))) {
95  1043534 boolean ret = s.enqueue(get(i), this);
96  1043534 assert ret;
97  1043534 break;
98    }
99    }
100   
 
101  0 toggle public IVecInt computeAnImpliedClause() {
102  0 return null;
103    }
104   
105    }
 
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.