Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
83   221   34   13,83
66   155   0,47   6
6     6,5  
1    
 
  GoodOPBReader       Line # 53 83 34 69% 0.6903226
 
  (83)
 
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.reader;
27   
28    import java.io.IOException;
29    import java.io.LineNumberReader;
30    import java.io.PrintWriter;
31    import java.io.Serializable;
32    import java.math.BigInteger;
33    import java.util.HashMap;
34    import java.util.Map;
35    import java.util.Scanner;
36   
37    import org.sat4j.core.Vec;
38    import org.sat4j.core.VecInt;
39    import org.sat4j.specs.ContradictionException;
40    import org.sat4j.specs.IProblem;
41    import org.sat4j.specs.ISolver;
42    import org.sat4j.specs.IVec;
43    import org.sat4j.specs.IVecInt;
44   
45    /**
46    * This class is a quick hack to read opb formatted files. The reader skip
47    * commented lines (beginning with COMMENT_SYMBOL) and expect constraints of the
48    * form: [name :] [[+|-]COEF] [*] [+|-]LIT >=|<=|= DEGREE where COEF and DEGREE
49    * are plain integer and LIT is an identifier.
50    *
51    * @author leberre
52    */
 
53    public class GoodOPBReader extends Reader implements Serializable {
54   
55    /**
56    * Comment for <code>serialVersionUID</code>
57    */
58    private static final long serialVersionUID = 1L;
59   
60    private static final String COMMENT_SYMBOL = "*";
61   
62    private final ISolver solver;
63   
64    private final Map<String, Integer> map = new HashMap<String, Integer>();
65   
66    private final IVec<String> decode = new Vec<String>();
67   
68    /**
69    *
70    */
 
71  840 toggle public GoodOPBReader(ISolver solver) {
72  840 this.solver = solver;
73    }
74   
 
75  840 toggle @Override
76    public final IProblem parseInstance(final java.io.Reader in)
77    throws ParseFormatException, ContradictionException, IOException {
78  840 return parseInstance(new LineNumberReader(in));
79    }
80   
 
81  840 toggle private IProblem parseInstance(LineNumberReader in)
82    throws ContradictionException, IOException {
83  840 solver.reset();
84  840 String line;
85  0 while ((line = in.readLine()) != null) {
86    // cannot trim is line is null
87  1660596 line = line.trim();
88  1660596 if (line.endsWith(";")) {
89  1659634 line = line.substring(0, line.length() - 1);
90    }
91  1660596 parseLine(line);
92    }
93  750 return solver;
94    }
95   
 
96  1660596 toggle void parseLine(String line) throws ContradictionException {
97    // Skip commented line
98  1660596 if (line.startsWith(COMMENT_SYMBOL))
99  946 return;
100  1659650 if (line.startsWith("p")) // ignore p cnf with pbchaff format
101  0 return;
102  1659650 if (line.startsWith("min:") || line.startsWith("min :"))
103  577 return; // we will use that case later
104  1659073 if (line.startsWith("max:") || line.startsWith("max :"))
105  2 return; // we will use that case later
106   
107    // skip name of constraints:
108  1659071 int index = line.indexOf(":");
109  1659071 if (index != -1) {
110  8432 line = line.substring(index + 1);
111    }
112   
113  1659071 IVecInt lits = new VecInt();
114  1659071 IVec<BigInteger> coeffs = new Vec<BigInteger>();
115  1659071 Scanner stk = new Scanner(line)
116    .useDelimiter("\\s*\\*\\s*|\\s*\\+\\s*|\\s+");
117  15195406 while (stk.hasNext()) {
118  13536425 String token = stk.next();
119  13536425 if (">=".equals(token) || "<=".equals(token) || "=".equals(token)) {
120  1659071 assert stk.hasNext();
121  1659071 String tok = stk.next();
122    // we need to remove + from the integer
123  1659071 if (tok.startsWith("+")) {
124  0 tok = tok.substring(1);
125    }
126  1659071 BigInteger d = new BigInteger(tok);
127   
128  1659071 try {
129  1659071 if (">=".equals(token) || "=".equals(token)) {
130  1657433 solver.addPseudoBoolean(lits, coeffs, true, d);
131    }
132  1658981 if ("<=".equals(token) || "=".equals(token)) {
133  24199 solver.addPseudoBoolean(lits, coeffs, false, d);
134    }
135    } catch (ContradictionException ce) {
136  90 System.out.println("c inconsistent constraint: " + line);
137  90 System.out.println("c lits: " + lits);
138  90 System.out.println("c coeffs: " + coeffs);
139  90 throw ce;
140    }
141    } else {
142    // on est toujours en train de lire la partie gauche de la
143    // contrainte
144  11877354 if ("+".equals(token)) {
145  0 assert stk.hasNext();
146  0 token = stk.next();
147  11877354 } else if ("-".equals(token)) {
148  0 assert stk.hasNext();
149  0 token = token + stk.next();
150    }
151  11877354 BigInteger coef;
152    // should contain a coef and a literal
153  11877354 try {
154    // we need to remove + from the integer
155  11877354 if (token.startsWith("+")) {
156  0 token = token.substring(1);
157    }
158  11877354 coef = new BigInteger(token);
159  11751053 assert stk.hasNext();
160  11751053 token = stk.next();
161    } catch (NumberFormatException nfe) {
162    // its only an identifier
163  126301 coef = BigInteger.ONE;
164    }
165  11877354 if ("-".equals(token) || "~".equals(token)) {
166  4 assert stk.hasNext();
167  4 token = token + stk.next();
168    }
169  11877354 boolean negative = false;
170  11877354 if (token.startsWith("+")) {
171  0 token = token.substring(1);
172  11877354 } else if (token.startsWith("-")) {
173  50763 token = token.substring(1);
174  50763 assert coef.equals(BigInteger.ONE);
175  50763 coef = BigInteger.ONE.negate();
176  11826591 } else if (token.startsWith("~")) {
177  8 token = token.substring(1);
178  8 negative = true;
179    }
180  11877354 Integer id = map.get(token);
181  11877354 if (id == null) {
182  741840 map.put(token, id = solver.newVar());
183  741840 decode.push(token);
184  741840 assert decode.size() == id.intValue();
185    }
186  11877354 coeffs.push(coef);
187  11877354 int lid = (negative ? -1 : 1) * id.intValue();
188  11877354 lits.push(lid);
189  11877354 assert coeffs.size() == lits.size();
190    }
191    }
192    }
193   
 
194  0 toggle @Override
195    public String decode(int[] model) {
196  0 StringBuffer stb = new StringBuffer();
197  0 for (int i = 0; i < model.length; i++) {
198  0 if (model[i] < 0) {
199  0 stb.append("-");
200  0 stb.append(decode.get(-model[i] - 1));
201    } else {
202  0 stb.append(decode.get(model[i] - 1));
203    }
204  0 stb.append(" ");
205    }
206  0 return stb.toString();
207    }
208   
 
209  0 toggle @Override
210    public void decode(int[] model, PrintWriter out) {
211  0 for (int i = 0; i < model.length; i++) {
212  0 if (model[i] < 0) {
213  0 out.print("-");
214  0 out.print(decode.get(-model[i] - 1));
215    } else {
216  0 out.print(decode.get(model[i] - 1));
217    }
218  0 out.print(" ");
219    }
220    }
221    }
 
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.