Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
17   93   6   4,25
10   42   0,53   4
4     2,25  
1    
 
  MixedDataStructureWithBinaryAndTernary       Line # 40 17 6 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.Lits23;
30    import org.sat4j.minisat.constraints.cnf.WLClause;
31    import org.sat4j.minisat.core.Constr;
32    import org.sat4j.minisat.core.ILits23;
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 MixedDataStructureWithBinaryAndTernary extends
41    AbstractDataStructureFactory<ILits23> {
42   
43    private static final long serialVersionUID = 1L;
44   
45   
46    /*
47    * (non-Javadoc)
48    *
49    * @see org.sat4j.minisat.DataStructureFactory#createClause(org.sat4j.datatype.VecInt)
50    */
 
51  251756 toggle public Constr createClause(IVecInt literals) throws ContradictionException {
52  251756 IVecInt v = WLClause.sanityCheck(literals, lits, solver);
53  251756 if (v == null)
54  13 return null;
55  251743 if (v.size() == 2) {
56  196980 lits.binaryClauses(v.get(0), v.get(1));
57  196980 return null;
58    }
59  54763 if (v.size() == 3) {
60  11129 lits.ternaryClauses(v.get(0), v.get(1), v.get(2));
61  11129 return null;
62    }
63  43634 return WLClause.brandNewClause(solver, lits, v);
64    }
65   
66    /*
67    * (non-Javadoc)
68    *
69    * @see org.sat4j.minisat.DataStructureFactory#learnContraint(org.sat4j.minisat.Constr)
70    */
 
71  57364 toggle @Override
72    public void learnConstraint(Constr constr) {
73  57364 if (constr.size() == 2) {
74  235 lits.binaryClauses(constr.get(0), constr.get(1));
75    // solver.getStats().learnedbinaryclauses++;
76  57129 } else if (constr.size() == 3) {
77  271 lits.ternaryClauses(constr.get(0), constr.get(1), constr.get(2));
78    // solver.getStats().learnedternaryclauses++;
79    } else {
80  56858 super.learnConstraint(constr);
81    }
82    }
83   
 
84  107 toggle @Override
85    protected ILits23 createLits() {
86  107 return new Lits23();
87    }
88   
 
89  8357383 toggle public Constr createUnregisteredClause(IVecInt literals) {
90  8357383 return new LearntWLClause(literals, getVocabulary());
91    }
92   
93    }
 
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.