Clover coverage report -
Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST
file stats: LOC: 116   Methods: 5
NCLOC: 77   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
AbstractPBClauseCardConstrDataStructure.java 93,8% 92,3% 80% 91,5%
coverage coverage
 1    package org.sat4j.minisat.constraints;
 2   
 3    import java.math.BigInteger;
 4   
 5    import org.sat4j.core.Vec;
 6    import org.sat4j.core.VecInt;
 7    import org.sat4j.minisat.constraints.cnf.WLClause;
 8    import org.sat4j.minisat.constraints.pb.IDataStructurePB;
 9    import org.sat4j.minisat.constraints.pb.PBConstr;
 10    import org.sat4j.minisat.constraints.pb.WatchPb;
 11    import org.sat4j.specs.ContradictionException;
 12    import org.sat4j.specs.IVec;
 13    import org.sat4j.specs.IVecInt;
 14   
 15    public abstract class AbstractPBClauseCardConstrDataStructure extends
 16    AbstractPBDataStructureFactory {
 17   
 18    /*
 19    * (non-Javadoc)
 20    *
 21    * @see org.sat4j.minisat.constraints.AbstractPBDataStructureFactory#constraintFactory(org.sat4j.specs.VecInt,
 22    * org.sat4j.specs.VecInt, boolean, int)
 23    */
 24  4150 @Override
 25    protected PBConstr constraintFactory(IVecInt literals, IVecInt coefs,
 26    boolean moreThan, int degree) throws ContradictionException {
 27  4150 return constraintFactory(literals, WatchPb.toVecBigInt(coefs),
 28    moreThan, WatchPb.toBigInt(degree));
 29    }
 30   
 31    /*
 32    * (non-Javadoc)
 33    *
 34    * @see org.sat4j.minisat.constraints.AbstractPBDataStructureFactory#constraintFactory(org.sat4j.specs.VecInt,
 35    * org.sat4j.specs.VecInt, int)
 36    */
 37  0 @Override
 38    protected PBConstr constraintFactory(IVecInt literals, IVecInt coefs,
 39    int degree) {
 40  0 return constraintFactory(literals, WatchPb.toVecBigInt(coefs), WatchPb
 41    .toBigInt(degree));
 42    }
 43   
 44    /*
 45    * (non-Javadoc)
 46    *
 47    * @see org.sat4j.minisat.constraints.AbstractPBDataStructureFactory#constraintFactory(org.sat4j.specs.VecInt,
 48    * org.sat4j.specs.VecInt, boolean, int)
 49    */
 50  841834 @Override
 51    protected PBConstr constraintFactory(IVecInt literals,
 52    IVec<BigInteger> coefs, boolean moreThan, BigInteger degree)
 53    throws ContradictionException {
 54  841834 IDataStructurePB mpb = WatchPb.niceParameters(literals, coefs,
 55    moreThan, degree, getVocabulary());
 56  841834 if (mpb == null)
 57  0 return null;
 58  841834 int size = mpb.size();
 59  841834 int[] lits = new int[size];
 60  841834 BigInteger[] normCoefs = new BigInteger[size];
 61  841834 mpb.buildConstraintFromMapPb(lits, normCoefs);
 62  841834 if (mpb.getDegree().equals(BigInteger.ONE)) {
 63  444424 IVecInt v = WLClause.sanityCheck(new VecInt(lits), getVocabulary(),
 64    solver);
 65  444424 if (v == null)
 66  1026 return null;
 67  443398 return constructClause(v);
 68    }
 69  397410 if (coefficientsEqualToOne(new Vec<BigInteger>(normCoefs))) {
 70    assert mpb.getDegree().compareTo(new BigInteger(String.valueOf(Integer.MAX_VALUE))) < 0;
 71  27618 return constructCard(new VecInt(lits), mpb.getDegree().intValue());
 72    }
 73  369792 return constructPB(mpb);
 74    }
 75   
 76    /*
 77    * (non-Javadoc)
 78    *
 79    * @see org.sat4j.minisat.constraints.AbstractPBDataStructureFactory#constraintFactory(org.sat4j.specs.VecInt,
 80    * org.sat4j.specs.VecInt, int)
 81    */
 82  279930 @Override
 83    protected PBConstr constraintFactory(IVecInt literals,
 84    IVec<BigInteger> coefs, BigInteger degree) {
 85  279930 if (degree.equals(BigInteger.ONE)) {
 86  246930 return constructLearntClause(literals);
 87    }
 88  33000 if (coefficientsEqualToOne(coefs)) {
 89  5106 return constructLearntCard(literals, degree.intValue());
 90    }
 91  27894 return constructLearntPB(literals, coefs, degree);
 92    }
 93   
 94  430410 private static boolean coefficientsEqualToOne(IVec<BigInteger> coeffs) {
 95  430410 for (int i = 0; i < coeffs.size(); i++)
 96  3758679 if (!coeffs.get(i).equals(BigInteger.ONE))
 97  397686 return false;
 98  32724 return true;
 99    }
 100   
 101    abstract protected PBConstr constructClause(IVecInt v);
 102   
 103    abstract protected PBConstr constructCard(IVecInt lits, int degree)
 104    throws ContradictionException;
 105   
 106    abstract protected PBConstr constructPB(IDataStructurePB mpb)
 107    throws ContradictionException;
 108   
 109    abstract protected PBConstr constructLearntClause(IVecInt literals);
 110   
 111    abstract protected PBConstr constructLearntCard(IVecInt literals, int degree);
 112   
 113    abstract protected PBConstr constructLearntPB(IVecInt literals,
 114    IVec<BigInteger> coefs, BigInteger degree);
 115   
 116    }