Clover coverage report -
Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST
file stats: LOC: 81   Methods: 4
NCLOC: 44   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
MixedDataStructureWithBinaryAndTernary.java 100% 100% 100% 100%
coverage
 1    /*
 2    * Created on 1 juin 2004
 3    *
 4    * To change the template for this generated file go to
 5    * Window>Preferences>Java>Code Generation>Code and Comments
 6    */
 7    package org.sat4j.minisat.constraints;
 8   
 9    import org.sat4j.minisat.constraints.cnf.Lits23;
 10    import org.sat4j.minisat.constraints.cnf.WLClause;
 11    import org.sat4j.minisat.core.Constr;
 12    import org.sat4j.minisat.core.ILits;
 13    import org.sat4j.minisat.core.ILits23;
 14    import org.sat4j.specs.ContradictionException;
 15    import org.sat4j.specs.IVecInt;
 16   
 17    /**
 18    * @author leberre To change the template for this generated type comment go to
 19    * Window>Preferences>Java>Code Generation>Code and Comments
 20    */
 21    public class MixedDataStructureWithBinaryAndTernary extends
 22    MixedDataStructureDaniel {
 23   
 24    private static final long serialVersionUID = 1L;
 25   
 26    private final ILits23 mlits = new Lits23();
 27   
 28  107 public MixedDataStructureWithBinaryAndTernary() {
 29  107 lits = mlits;
 30    }
 31   
 32    /*
 33    * (non-Javadoc)
 34    *
 35    * @see org.sat4j.minisat.DataStructureFactory#createVocabulary()
 36    */
 37  12047689 @Override
 38    public ILits getVocabulary() {
 39  12047689 return lits;
 40    }
 41   
 42    /*
 43    * (non-Javadoc)
 44    *
 45    * @see org.sat4j.minisat.DataStructureFactory#createClause(org.sat4j.datatype.VecInt)
 46    */
 47  251756 @Override
 48    public Constr createClause(IVecInt literals) throws ContradictionException {
 49  251756 IVecInt v = WLClause.sanityCheck(literals, lits, solver);
 50  251756 if (v == null)
 51  13 return null;
 52  251743 if (v.size() == 2) {
 53  196980 mlits.binaryClauses(v.get(0), v.get(1));
 54  196980 return null;
 55    }
 56  54763 if (v.size() == 3) {
 57  11129 mlits.ternaryClauses(v.get(0), v.get(1), v.get(2));
 58  11129 return null;
 59    }
 60  43634 return WLClause.brandNewClause(solver, lits, v);
 61    }
 62   
 63    /*
 64    * (non-Javadoc)
 65    *
 66    * @see org.sat4j.minisat.DataStructureFactory#learnContraint(org.sat4j.minisat.Constr)
 67    */
 68  57240 @Override
 69    public void learnConstraint(Constr constr) {
 70  57240 if (constr.size() == 2) {
 71  180 mlits.binaryClauses(constr.get(0), constr.get(1));
 72    // solver.getStats().learnedbinaryclauses++;
 73  57060 } else if (constr.size() == 3) {
 74  202 mlits.ternaryClauses(constr.get(0), constr.get(1), constr.get(2));
 75    // solver.getStats().learnedternaryclauses++;
 76    } else {
 77  56858 super.learnConstraint(constr);
 78    }
 79    }
 80   
 81    }