Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
27   224   7   1,59
16   83   0,85   17
17     1,35  
1    
 
  BinaryClauses       Line # 40 27 7 48,3% 0.48333332
 
  (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.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 BinaryClauses implements Constr, Serializable {
41   
42    private static final long serialVersionUID = 1L;
43   
44    private final ILits voc;
45   
46    private final IVecInt clauses = new VecInt();
47   
48    private final int reason;
49   
50    private int conflictindex = -1;
51   
52    /**
53    *
54    */
 
55  74457 toggle public BinaryClauses(ILits voc, int p) {
56  74457 this.voc = voc;
57  74457 this.reason = p;
58    }
59   
 
60  1177672 toggle public void addBinaryClause(int p) {
61  1177672 clauses.push(p);
62    }
63   
64    /*
65    * (non-Javadoc)
66    *
67    * @see org.sat4j.minisat.Constr#remove()
68    */
 
69  0 toggle public void remove() {
70    // do nothing
71    }
72   
73    /*
74    * (non-Javadoc)
75    *
76    * @see org.sat4j.minisat.Constr#propagate(org.sat4j.minisat.UnitPropagationListener,
77    * int)
78    */
 
79  179102904 toggle public boolean propagate(UnitPropagationListener s, int p) {
80  179102904 assert voc.isFalsified(this.reason);
81  179102904 voc.watch(p, this);
82  2054880611 for (int i = 0; i < clauses.size(); i++) {
83  1908942286 int q = clauses.get(i);
84  1908942286 if (!s.enqueue(q, this)) {
85  33164579 conflictindex = i;
86  33164579 return false;
87    }
88    }
89  145938325 return true;
90    }
91   
92    /*
93    * (non-Javadoc)
94    *
95    * @see org.sat4j.minisat.Constr#simplify()
96    */
 
97  0 toggle public boolean simplify() {
98  0 IVecInt locclauses = clauses;
99  0 final int size = clauses.size();
100  0 for (int i = 0; i < size; i++) {
101  0 if (voc.isSatisfied(locclauses.get(i))) {
102  0 return true;
103    }
104  0 if (voc.isFalsified(locclauses.get(i))) {
105  0 locclauses.delete(i);
106    }
107   
108    }
109  0 return false;
110    }
111   
112    /*
113    * (non-Javadoc)
114    *
115    * @see org.sat4j.minisat.Constr#undo(int)
116    */
 
117  0 toggle public void undo(int p) {
118    // no to do
119    }
120   
121    /*
122    * (non-Javadoc)
123    *
124    * @see org.sat4j.minisat.Constr#calcReason(int, org.sat4j.datatype.VecInt)
125    */
 
126  221414440 toggle public void calcReason(int p, IVecInt outReason) {
127  221414440 outReason.push(this.reason ^ 1);
128  221414440 if (p == ILits.UNDEFINED) {
129    // int i=0;
130    // while(!voc.isFalsified(clauses.get(i))) {
131    // i++;
132    // }
133  33164540 assert conflictindex > -1;
134  33164540 outReason.push(clauses.get(conflictindex) ^ 1);
135    }
136    }
137   
138    /*
139    * (non-Javadoc)
140    *
141    * @see org.sat4j.minisat.Constr#learnt()
142    */
 
143  221414440 toggle public boolean learnt() {
144  221414440 return false;
145    }
146   
147    /*
148    * (non-Javadoc)
149    *
150    * @see org.sat4j.minisat.Constr#incActivity(double)
151    */
 
152  0 toggle public void incActivity(double claInc) {
153    // TODO Auto-generated method stub
154    }
155   
156    /*
157    * (non-Javadoc)
158    *
159    * @see org.sat4j.minisat.Constr#getActivity()
160    */
 
161  0 toggle public double getActivity() {
162    // TODO Auto-generated method stub
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  0 return false;
173    }
174   
175    /*
176    * (non-Javadoc)
177    *
178    * @see org.sat4j.minisat.Constr#setLearnt()
179    */
 
180  0 toggle public void setLearnt() {
181    // TODO Auto-generated method stub
182    }
183   
184    /*
185    * (non-Javadoc)
186    *
187    * @see org.sat4j.minisat.Constr#register()
188    */
 
189  0 toggle public void register() {
190    // TODO Auto-generated method stub
191    }
192   
193    /*
194    * (non-Javadoc)
195    *
196    * @see org.sat4j.minisat.Constr#rescaleBy(double)
197    */
 
198  0 toggle public void rescaleBy(double d) {
199    // TODO Auto-generated method stub
200    }
201   
202    /*
203    * (non-Javadoc)
204    *
205    * @see org.sat4j.minisat.Constr#size()
206    */
 
207  156182406 toggle public int size() {
208  156182406 return clauses.size();
209    }
210   
211    /*
212    * (non-Javadoc)
213    *
214    * @see org.sat4j.minisat.Constr#get(int)
215    */
 
216  0 toggle public int get(int i) {
217    // TODO Auto-generated method stub
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.