Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
55   196   19   18,33
28   116   0,38   3
3     7  
1    
 
  ExtendedDimacsReader       Line # 44 55 19 0% 0.0
 
No Tests
 
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    package org.sat4j.reader;
26   
27    import java.io.IOException;
28    import java.io.LineNumberReader;
29    import java.util.Scanner;
30    import java.util.StringTokenizer;
31   
32    import org.sat4j.specs.ContradictionException;
33    import org.sat4j.specs.ISolver;
34    import org.sat4j.specs.IVecInt;
35    import org.sat4j.tools.GateTranslator;
36   
37    /**
38    * Reader for the Extended Dimacs format proposed by Fahiem Bacchus and Toby
39    * Walsh.
40    *
41    * @author leberre
42    *
43    */
 
44    public class ExtendedDimacsReader extends DimacsReader {
45   
46    public static final int FALSE = 1;
47   
48    public static final int TRUE = 2;
49   
50    public static final int NOT = 3;
51   
52    public static final int AND = 4;
53   
54    public static final int NAND = 5;
55   
56    public static final int OR = 6;
57   
58    public static final int NOR = 7;
59   
60    public static final int XOR = 8;
61   
62    public static final int XNOR = 9;
63   
64    public static final int IMPLIES = 10;
65   
66    public static final int IFF = 11;
67   
68    public static final int IFTHENELSE = 12;
69   
70    public static final int ATLEAST = 13;
71   
72    public static final int ATMOST = 14;
73   
74    public static final int COUNT = 15;
75   
76    /**
77    *
78    *
79    */
80    private static final long serialVersionUID = 1L;
81   
 
82  0 toggle public ExtendedDimacsReader(ISolver solver) {
83  0 super(new GateTranslator(solver));
84    }
85   
86    /**
87    * @param in
88    * the input stream
89    * @throws IOException
90    * iff an IO occurs
91    * @throws ParseFormatException
92    * if the input stream does not comply with the DIMACS format.
93    */
 
94  0 toggle @Override
95    protected void readProblemLine(LineNumberReader in) throws IOException,
96    ParseFormatException {
97   
98  0 String line = in.readLine();
99   
100  0 if (line == null) {
101  0 throw new ParseFormatException(
102    "premature end of file: <p noncnf ...> expected on line "
103    + in.getLineNumber());
104    }
105  0 StringTokenizer stk = new StringTokenizer(line);
106   
107  0 if (!(stk.hasMoreTokens() && stk.nextToken().equals("p")
108    && stk.hasMoreTokens() && stk.nextToken().equals("noncnf"))) {
109  0 throw new ParseFormatException(
110    "problem line expected (p noncnf ...) on line "
111    + in.getLineNumber());
112    }
113   
114  0 int vars;
115   
116    // reads the max var id
117  0 vars = Integer.parseInt(stk.nextToken());
118  0 assert vars > 0;
119  0 solver.newVar(vars);
120  0 try {
121  0 ((GateTranslator)solver).gateTrue(vars);
122    } catch (ContradictionException e) {
123    assert false;
124  0 System.err.println("Contradiction when asserting root variable?");
125    }
126  0 disableNumberOfConstraintCheck();
127    }
128   
129    /*
130    * (non-Javadoc)
131    *
132    * @see org.sat4j.reader.DimacsReader#handleConstr(java.lang.String,
133    * org.sat4j.specs.IVecInt)
134    */
 
135  0 toggle @Override
136    protected boolean handleConstr(String line, IVecInt literals)
137    throws ContradictionException {
138  0 boolean added = true;
139  0 assert literals.size() == 0;
140  0 Scanner scan = new Scanner(line);
141  0 GateTranslator gater = (GateTranslator)solver;
142  0 while (scan.hasNext()) {
143  0 int gateType = scan.nextInt();
144  0 assert gateType > 0;
145  0 int nbparam = scan.nextInt();
146  0 assert nbparam != 0;
147  0 assert nbparam == -1 || gateType >= ATLEAST;
148  0 for (int i = 0; i < nbparam; i++) {
149  0 scan.nextInt();
150    }
151    // readI/O until reaching ending 0
152  0 int y = scan.nextInt();
153  0 int x;
154  0 while ((x = scan.nextInt()) != 0) {
155  0 literals.push(x);
156    }
157  0 switch (gateType) {
158  0 case FALSE:
159  0 assert literals.size()==0;
160  0 gater.gateFalse(y);
161  0 break;
162  0 case TRUE:
163  0 assert literals.size()==0;
164  0 gater.gateTrue(y);
165  0 break;
166  0 case OR:
167  0 gater.or(y, literals);
168  0 break;
169  0 case NOT:
170  0 assert literals.size()==1;
171  0 gater.not(y, literals.get(0));
172  0 break;
173  0 case AND:
174  0 gater.and(y, literals);
175  0 break;
176  0 case XOR:
177  0 gater.xor(y, literals);
178  0 break;
179  0 case IFF:
180  0 gater.iff(y, literals);
181  0 break;
182  0 case IFTHENELSE:
183  0 assert literals.size()==3;
184  0 gater.ite(y, literals.get(0),literals.get(1),literals.get(2));
185  0 break;
186  0 default:
187  0 throw new UnsupportedOperationException("Gate type " + gateType
188    + " not handled yet");
189    }
190    }
191  0 literals.clear();
192  0 return added;
193    }
194   
195   
196    }
 
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.