Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
34   224   13   2
24   94   0,85   17
17     1,71  
1    
 
  TernaryClauses       Line # 40 34 13 69,3% 0.6933333
 
  (79)
 
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.cnf;
27   
28    import java.io.Serializable;
29   
30    import org.sat4j.core.VecInt;
31    import org.sat4j.minisat.core.Constr;
32    import org.sat4j.minisat.core.ILits;
33    import org.sat4j.minisat.core.UnitPropagationListener;
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 TernaryClauses implements Constr, Serializable {
41   
42    private static final long serialVersionUID = 1L;
43   
44    private final IVecInt stubs = new VecInt();
45   
46    private final ILits voc;
47   
48    private final int phead;
49   
 
50  11621 toggle public TernaryClauses(ILits voc, int p) {
51  11621 this.voc = voc;
52  11621 this.phead = p;
53    }
54   
 
55  34200 toggle public void addTernaryClause(int a, int b) {
56  34200 stubs.push(a);
57  34200 stubs.push(b);
58    }
59   
60    /*
61    * (non-Javadoc)
62    *
63    * @see org.sat4j.minisat.Constr#remove()
64    */
 
65  0 toggle public void remove() {
66   
67    }
68   
69    /*
70    * (non-Javadoc)
71    *
72    * @see org.sat4j.minisat.Constr#propagate(org.sat4j.minisat.UnitPropagationListener,
73    * int)
74    */
 
75  139634 toggle public boolean propagate(UnitPropagationListener s, int p) {
76  139634 assert voc.isSatisfied(p);
77  139634 assert voc.isFalsified(phead);
78  139634 voc.watch(p, this);
79  483357 for (int i = 0; i < stubs.size(); i += 2) {
80  346284 int a = stubs.get(i);
81  346284 int b = stubs.get(i + 1);
82  346284 if (voc.isSatisfied(a) || voc.isSatisfied(b)) {
83  150645 continue;
84    }
85  195639 if (voc.isFalsified(a) && !s.enqueue(b, this)) {
86  2561 return false;
87  193078 } else if (voc.isFalsified(b) && !s.enqueue(a, this)) {
88  0 return false;
89    }
90    }
91  137073 return true;
92    }
93   
94    /*
95    * (non-Javadoc)
96    *
97    * @see org.sat4j.minisat.Constr#simplify()
98    */
 
99  0 toggle public boolean simplify() {
100  0 return false;
101    }
102   
103    /*
104    * (non-Javadoc)
105    *
106    * @see org.sat4j.minisat.Constr#undo(int)
107    */
 
108  0 toggle public void undo(int p) {
109    }
110   
111    /*
112    * (non-Javadoc)
113    *
114    * @see org.sat4j.minisat.Constr#calcReason(int, org.sat4j.datatype.VecInt)
115    */
 
116  34331 toggle public void calcReason(int p, IVecInt outReason) {
117  34331 assert voc.isFalsified(this.phead);
118  34331 if (p == ILits.UNDEFINED) {
119  2545 int i = 0;
120  5401 while (!voc.isFalsified(stubs.get(i))
121    || !voc.isFalsified(stubs.get(i + 1))) {
122  2856 i += 2;
123    }
124  2545 outReason.push(this.phead ^ 1);
125  2545 outReason.push(stubs.get(i) ^ 1);
126  2545 outReason.push(stubs.get(i + 1) ^ 1);
127    } else {
128  31786 outReason.push(this.phead ^ 1);
129  31786 int i = 0;
130  117583 while ((stubs.get(i) != p) || (!voc.isFalsified(stubs.get(i ^ 1)))) {
131  85797 i++;
132    }
133  31786 assert !voc.isFalsified(stubs.get(i));
134  31786 outReason.push(stubs.get(i ^ 1) ^ 1);
135  31786 assert voc.isFalsified(stubs.get(i ^ 1));
136    }
137   
138    }
139   
140    /*
141    * (non-Javadoc)
142    *
143    * @see org.sat4j.minisat.Constr#learnt()
144    */
 
145  34331 toggle public boolean learnt() {
146  34331 return false;
147    }
148   
149    /*
150    * (non-Javadoc)
151    *
152    * @see org.sat4j.minisat.Constr#incActivity(double)
153    */
 
154  0 toggle public void incActivity(double claInc) {
155    }
156   
157    /*
158    * (non-Javadoc)
159    *
160    * @see org.sat4j.minisat.Constr#getActivity()
161    */
 
162  0 toggle public double getActivity() {
163  0 return 0;
164    }
165   
166    /*
167    * (non-Javadoc)
168    *
169    * @see org.sat4j.minisat.Constr#locked()
170    */
 
171  0 toggle public boolean locked() {
172    // TODO Auto-generated method stub
173  0 return false;
174    }
175   
176    /*
177    * (non-Javadoc)
178    *
179    * @see org.sat4j.minisat.Constr#setLearnt()
180    */
 
181  0 toggle public void setLearnt() {
182   
183    }
184   
185    /*
186    * (non-Javadoc)
187    *
188    * @see org.sat4j.minisat.Constr#register()
189    */
 
190  0 toggle public void register() {
191   
192    }
193   
194    /*
195    * (non-Javadoc)
196    *
197    * @see org.sat4j.minisat.Constr#rescaleBy(double)
198    */
 
199  0 toggle public void rescaleBy(double d) {
200   
201    }
202   
203    /*
204    * (non-Javadoc)
205    *
206    * @see org.sat4j.minisat.Constr#size()
207    */
 
208  556762 toggle public int size() {
209  556762 return stubs.size();
210    }
211   
212    /*
213    * (non-Javadoc)
214    *
215    * @see org.sat4j.minisat.Constr#get(int)
216    */
 
217  0 toggle public int get(int i) {
218  0 throw new UnsupportedOperationException();
219    }
220   
 
221  0 toggle public void assertConstraint(UnitPropagationListener s) {
222  0 throw new UnsupportedOperationException();
223    }
224    }
 
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.