Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
12   83   4   3
6   36   0,58   4
4     1,75  
1    
 
  MixedDataStructureWithBinary       Line # 40 12 4 100% 1.0
 
  (101)
 
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   
26    package org.sat4j.minisat.constraints;
27   
28    import org.sat4j.minisat.constraints.cnf.LearntWLClause;
29    import org.sat4j.minisat.constraints.cnf.Lits2;
30    import org.sat4j.minisat.constraints.cnf.WLClause;
31    import org.sat4j.minisat.core.Constr;
32    import org.sat4j.minisat.core.ILits2;
33    import org.sat4j.specs.ContradictionException;
34    import org.sat4j.specs.IVecInt;
35   
36    /**
37    * @author leberre To change the template for this generated type comment go to
38    * Window>Preferences>Java>Code Generation>Code and Comments
39    */
 
40    public class MixedDataStructureWithBinary extends AbstractDataStructureFactory<ILits2> {
41   
42    private static final long serialVersionUID = 1L;
43   
 
44  207 toggle @Override
45    public ILits2 createLits() {
46  207 return new Lits2();
47    }
48   
49    /*
50    * (non-Javadoc)
51    *
52    * @see org.sat4j.minisat.DataStructureFactory#createClause(org.sat4j.datatype.VecInt)
53    */
 
54  500607 toggle public Constr createClause(IVecInt literals) throws ContradictionException {
55  500607 IVecInt v = WLClause.sanityCheck(literals, lits, solver);
56  500607 if (v == null)
57  26 return null;
58  500581 if (v.size() == 2) {
59  391125 lits.binaryClauses(v.get(0), v.get(1));
60  391125 return null;
61    }
62  109456 return WLClause.brandNewClause(solver, lits, v);
63    }
64   
65    /*
66    * (non-Javadoc)
67    *
68    * @see org.sat4j.minisat.DataStructureFactory#learnContraint(org.sat4j.minisat.Constr)
69    */
 
70  59691 toggle @Override
71    public void learnConstraint(Constr constr) {
72  59691 if (constr.size() == 2) {
73  496 lits.binaryClauses(constr.get(0), constr.get(1));
74    // solver.getStats().learnedbinaryclauses++;
75    } else {
76  59195 super.learnConstraint(constr);
77    }
78    }
79   
 
80  30578921 toggle public Constr createUnregisteredClause(IVecInt literals) {
81  30578921 return new LearntWLClause(literals, getVocabulary());
82    }
83    }
 
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.