Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
50   265   16   2,63
32   124   0,68   19
19     1,79  
1    
 
  CBClause       Line # 39 50 16 68,3% 0.6831683
 
  (154)
 
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.minisat.core.Constr;
31    import org.sat4j.minisat.core.ILits;
32    import org.sat4j.minisat.core.Undoable;
33    import org.sat4j.minisat.core.UnitPropagationListener;
34    import org.sat4j.specs.IVecInt;
35   
36    /**
37    * @author leberre
38    */
 
39    public class CBClause implements Constr, Undoable, Serializable {
40   
41    private static final long serialVersionUID = 1L;
42   
43    protected int falsified;
44   
45    private boolean learnt;
46   
47    protected final int[] lits;
48   
49    protected final ILits voc;
50   
51    private double activity;
52   
 
53  249668 toggle public static CBClause brandNewClause(UnitPropagationListener s, ILits voc,
54    IVecInt literals) {
55  249668 CBClause c = new CBClause(literals, voc);
56  249668 c.register();
57  249668 return c;
58    }
59   
60    /**
61    *
62    */
 
63  12089031 toggle public CBClause(IVecInt ps, ILits voc, boolean learnt) {
64  12089031 this.learnt = learnt;
65  12089031 this.lits = new int[ps.size()];
66  12089031 this.voc = voc;
67  12089031 ps.moveTo(this.lits);
68    }
69   
 
70  12089031 toggle public CBClause(IVecInt ps, ILits voc) {
71  12089031 this(ps, voc, false);
72    }
73   
74    /*
75    * (non-Javadoc)
76    *
77    * @see org.sat4j.minisat.core.Constr#remove()
78    */
 
79  0 toggle public void remove() {
80  0 for (int i = 0; i < lits.length; i++) {
81  0 voc.watches(lits[i] ^ 1).remove(this);
82    }
83    }
84   
85    /*
86    * (non-Javadoc)
87    *
88    * @see org.sat4j.minisat.core.Constr#propagate(org.sat4j.minisat.core.UnitPropagationListener,
89    * int)
90    */
 
91  1721812357 toggle public boolean propagate(UnitPropagationListener s, int p) {
92  1721812357 voc.undos(p).push(this);
93  1721812357 falsified++;
94  1721812357 assert falsified != lits.length;
95  1721812357 if (falsified == lits.length - 1) {
96    // find unassigned literal
97  1536385732 for (int i = 0; i < lits.length; i++) {
98  1515511964 if (!voc.isFalsified(lits[i])) {
99  707082471 return s.enqueue(lits[i], this);
100    }
101    }
102    // one of the variable in to be propagated to false.
103    // (which explains why the falsified counter has not
104    // been increased yet)
105  20873768 return false;
106    }
107  993856118 return true;
108    }
109   
110    /*
111    * (non-Javadoc)
112    *
113    * @see org.sat4j.minisat.core.Constr#simplify()
114    */
 
115  0 toggle public boolean simplify() {
116  0 for (int p : lits) {
117  0 if (voc.isSatisfied(p)) {
118  0 return true;
119    }
120    }
121  0 return false;
122    }
123   
124    /*
125    * (non-Javadoc)
126    *
127    * @see org.sat4j.minisat.core.Constr#undo(int)
128    */
 
129  1722452475 toggle public void undo(int p) {
130  1722452475 falsified--;
131    }
132   
133    /*
134    * (non-Javadoc)
135    *
136    * @see org.sat4j.minisat.core.Constr#calcReason(int,
137    * org.sat4j.specs.VecInt)
138    */
 
139  196586708 toggle public void calcReason(int p, IVecInt outReason) {
140  196586708 assert outReason.size() == 0;
141  196586708 for (int q : lits) {
142  1081018603 assert voc.isFalsified(q) || q == p;
143  1081018603 if (voc.isFalsified(q)) {
144  905282379 outReason.push(q ^ 1);
145    }
146    }
147  196586708 assert (p == ILits.UNDEFINED) || (outReason.size() == lits.length - 1);
148    }
149   
150    /*
151    * (non-Javadoc)
152    *
153    * @see org.sat4j.minisat.core.Constr#learnt()
154    */
 
155  196586708 toggle public boolean learnt() {