Clover coverage report -

Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST

FRAMES NO FRAMES

file stats:	LOC:	81		Methods:	4
	NCLOC:	44		Classes:	1

Source file

Conditionals

Statements

Methods

TOTAL

MixedDataStructureWithBinaryAndTernary.java

100%

100%

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		}