Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
26   147   9   5,2
18   81   0,5   5
5     2,6  
1    
 
  AbstractPBClauseCardConstrDataStructure       Line # 39 26 9 89,8% 0.8979592
 
  (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;
26   
27    import java.math.BigInteger;
28   
29    import org.sat4j.core.Vec;
30    import org.sat4j.core.VecInt;
31    import org.sat4j.minisat.constraints.cnf.WLClause;
32    import org.sat4j.minisat.constraints.pb.IDataStructurePB;
33    import org.sat4j.minisat.constraints.pb.PBConstr;
34    import org.sat4j.minisat.constraints.pb.WatchPb;
35    import org.sat4j.specs.ContradictionException;
36    import org.sat4j.specs.IVec;
37    import org.sat4j.specs.IVecInt;
38   
 
39    public abstract class AbstractPBClauseCardConstrDataStructure extends
40    AbstractPBDataStructureFactory {
41   
42    private static final BigInteger MAX_INT_VALUE = BigInteger
43    .valueOf(Integer.MAX_VALUE);
44   
45    /*
46    * (non-Javadoc)
47    *
48    * @see org.sat4j.minisat.constraints.AbstractPBDataStructureFactory#constraintFactory(org.sat4j.specs.VecInt,
49    * org.sat4j.specs.VecInt, boolean, int)
50    */
 
51  5810 toggle @Override
52    protected PBConstr constraintFactory(IVecInt literals, IVecInt coefs,
53    boolean moreThan, int degree) throws ContradictionException {
54  5810 return constraintFactory(literals, WatchPb.toVecBigInt(coefs),
55    moreThan, WatchPb.toBigInt(degree));
56    }
57   
58    /*
59    * (non-Javadoc)
60    *
61    * @see org.sat4j.minisat.constraints.AbstractPBDataStructureFactory#constraintFactory(org.sat4j.specs.VecInt,
62    * org.sat4j.specs.VecInt, int)
63    */
 
64  0 toggle @Override
65    protected PBConstr constraintFactory(IVecInt literals, IVecInt coefs,
66    int degree) {
67  0 return constraintFactory(literals, WatchPb.toVecBigInt(coefs), WatchPb
68    .toBigInt(degree));
69    }
70   
71    /*
72    * (non-Javadoc)
73    *
74    * @see org.sat4j.minisat.constraints.AbstractPBDataStructureFactory#constraintFactory(org.sat4j.specs.VecInt,
75    * org.sat4j.specs.VecInt, boolean, int)
76    */
 
77  843494 toggle @Override
78    protected PBConstr constraintFactory(IVecInt literals,
79    IVec<BigInteger> coefs, boolean moreThan, BigInteger degree)
80    throws ContradictionException {
81  843494 IDataStructurePB mpb = WatchPb.niceParameters(literals, coefs,
82    moreThan, degree, getVocabulary());
83  843494 if (mpb == null)
84  0 return null;
85  843494 int size = mpb.size();
86  843494 int[] lits = new int[size];
87  843494 BigInteger[] normCoefs = new BigInteger[size];
88  843494 mpb.buildConstraintFromMapPb(lits, normCoefs);
89  843494 if (mpb.getDegree().equals(BigInteger.ONE)) {
90  446084 IVecInt v = WLClause.sanityCheck(new VecInt(lits), getVocabulary(),
91    solver);
92  446084 if (v == null)
93  1026 return null;
94  445058 return constructClause(v);
95    }
96  397410 if (coefficientsEqualToOne(new Vec<BigInteger>(normCoefs))) {
97  27618 assert mpb.getDegree().compareTo(MAX_INT_VALUE) < 0;
98  27618 return constructCard(new VecInt(lits), mpb.getDegree().intValue());
99    }
100    //return constructPB(mpb);
101  369792 return constructPB(lits,normCoefs,mpb.getDegree());
102    }
103   
104    /*
105    * (non-Javadoc)
106    *
107    * @see org.sat4j.minisat.constraints.AbstractPBDataStructureFactory#constraintFactory(org.sat4j.specs.VecInt,
108    * org.sat4j.specs.VecInt, int)
109    */
 
110  1073794 toggle @Override
111    protected PBConstr constraintFactory(IVecInt literals,
112    IVec<BigInteger> coefs, BigInteger degree) {
113  1073794 if (degree.equals(BigInteger.ONE)) {
114  1066078 return constructLearntClause(literals);
115    }
116  7716 if (coefficientsEqualToOne(coefs)) {
117  2050 return constructLearntCard(literals, degree.intValue());
118    }
119  5666 return constructLearntPB(literals, coefs, degree);
120    }
121   
 
122  405126 toggle private static boolean coefficientsEqualToOne(IVec<BigInteger> coeffs) {
123  2628163 for (int i = 0; i < coeffs.size(); i++)
124  2598495 if (!coeffs.get(i).equals(BigInteger.ONE))
125  375458 return false;
126  29668 return true;
127    }
128   
129    abstract protected PBConstr constructClause(IVecInt v);
130   
131    abstract protected PBConstr constructCard(IVecInt lits, int degree)
132    throws ContradictionException;
133   
134    abstract protected PBConstr constructPB(IDataStructurePB mpb)
135    throws ContradictionException;
136   
137    abstract protected PBConstr constructPB(int[] lits, BigInteger[] coefs, BigInteger degree)
138    throws ContradictionException;
139   
140    abstract protected PBConstr constructLearntClause(IVecInt literals);
141   
142    abstract protected PBConstr constructLearntCard(IVecInt literals, int degree);
143   
144    abstract protected PBConstr constructLearntPB(IVecInt literals,
145    IVec<BigInteger> coefs, BigInteger degree);
146   
147    }
 
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.