Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
81   233   18   8,1
36   136   0,33   10
10     2,7  
1    
 
  OPBReader2007       Line # 22 81 18 0% 0.0
 
No Tests
 
1    /**
2    *
3    */
4    package org.sat4j.reader;
5   
6    import java.io.IOException;
7    import java.math.BigInteger;
8    import java.util.HashMap;
9    import java.util.Map;
10   
11    import org.sat4j.core.Vec;
12    import org.sat4j.core.VecInt;
13    import org.sat4j.specs.ContradictionException;
14    import org.sat4j.specs.ISolver;
15    import org.sat4j.specs.IVec;
16    import org.sat4j.specs.IVecInt;
17   
18    /**
19    * @author parrain
20    *
21    */
 
22    public class OPBReader2007 extends OPBReader2006 {
23   
24   
25    /**
26    *
27    */
28    private static final long serialVersionUID = 1L;
29   
30    private int nbProducts, productSize;
31    // MetaData: #products and productSize in file.
32   
33   
34    /**
35    * @param solver
36    */
 
37  0 toggle public OPBReader2007(ISolver solver) {
38  0 super(solver);
39    // TODO Auto-generated constructor stub
40    }
41   
42   
 
43  0 toggle @Override
44    protected boolean isGoodFirstCharacter(char c){
45  0 return Character.isLetter(c) || c == '_' || c=='~';
46    }
47   
 
48  0 toggle @Override
49    protected void checkId(StringBuffer s) throws ParseFormatException{
50    // Small check on the coefficient ID to make sure everything is ok
51  0 int cpt = 1;
52  0 if (s.charAt(0)=='~') cpt=2;
53  0 int varID = Integer.parseInt(s.substring(cpt));
54  0 if (varID > nbVars) {
55  0 throw new ParseFormatException(
56    "Variable identifier larger than #variables in metadata.");
57    }
58    }
59   
60    /**
61    * contains the number of new symbols generated to linearize products
62    */
63    private int nbNewSymbols;
64   
 
65  0 toggle @Override
66    protected void readTerm(StringBuffer coeff, StringBuffer var)
67    throws IOException, ParseFormatException, ContradictionException {
68  0 readInteger(coeff);
69   
70  0 skipSpaces();
71   
72  0 var.setLength(0);
73  0 IVec<String> tmpLit = new Vec<String>();
74  0 StringBuffer tmpVar = new StringBuffer();
75  0 while (readIdentifier(tmpVar)){
76  0 tmpLit = tmpLit.push(tmpVar.toString());
77  0 skipSpaces();
78    }
79  0 if (tmpLit.size() == 0)
80  0 throw new ParseFormatException("identifier expected");
81  0 if (tmpLit.size() == 1){
82    // it is a "normal" term
83  0 var.append(tmpLit.last());
84  0 tmpLit.pop();
85    }
86    else {
87    // it is a product term
88  0 var.append(linearizeProduct(tmpLit));
89    }
90    }
91   
92    /**
93    * callback called when we read a term of a constraint
94    *
95    * @param coeff:
96    * the coefficient of the term
97    * @param var:
98    * the identifier of the variable
99    */
 
100  0 toggle protected void literalInAProduct(String var, IVecInt lits) {
101  0 int beginning = ((var.charAt(0) == '~') ? 2 : 1 );
102  0 int id = Integer.parseInt(var.substring(beginning));
103  0 int lid = ((var.charAt(0) == '~') ? -1 : 1) * id;
104  0 lits.push(lid);
105    }
106   
107    /**
108    * callback called when we read a term of a constraint
109    *
110    * @param coeff:
111    * the coefficient of the term
112    * @param var:
113    * the identifier of the variable
114    */
 
115  0 toggle protected void negateLiteralInAProduct(String var, IVecInt lits) {
116  0 int beginning = ((var.charAt(0) == '~') ? 2 : 1 );
117  0 int id = Integer.parseInt(var.substring(beginning));
118  0 int lid = ((var.charAt(0) == '~') ? 1 : -1) * id;
119  0 lits.push(lid);
120    }
121   
122   
123    /**
124    * read the first comment line to get the number of variables and the number
125    * of constraints in the file calls metaData with the data that was read
126    *
127    * @throws IOException
128    * @throws ParseException
129    */
 
130  0 toggle @Override
131    protected void readMetaData() throws IOException, ParseFormatException {
132  0 char c;
133  0 String s;
134   
135    // get the number of variables and constraints
136  0 c = get();
137  0 if (c != '*')
138  0 throw new ParseFormatException(
139    "First line of input file should be a comment");
140   
141  0 s = readWord();
142  0 if (eof() || !"#variable=".equals(s))
143  0 throw new ParseFormatException(
144    "First line should contain #variable= as first keyword");
145   
146  0 nbVars = Integer.parseInt(readWord());
147  0 nbNewSymbols = nbVars+1;
148   
149  0 s = readWord();
150  0 if (eof() || !"#constraint=".equals(s))
151  0 throw new ParseFormatException(
152    "First line should contain #constraint= as second keyword");
153   
154  0 nbConstr = Integer.parseInt(readWord());
155   
156  0 s = readWord();
157    // if (eof() || !"#product=".equals(s))
158    // throw new ParseFormatException(
159    // "First line should contain #product= as third keyword");
160  0 if (s.equals("#product=")) {
161  0 nbProducts = Integer.parseInt(readWord());
162  0 nbVars += nbProducts;
163  0 nbConstr += 2*nbProducts;
164    }
165   
166  0 s = readWord();
167    // if (eof() || !"sizeproduct=".equals(s))
168    // throw new ParseFormatException(
169    // "First line should contain sizeproduct= as fourth keyword");
170   
171  0 if (s.equals("sizeproduct="))
172  0 productSize = Integer.parseInt(readWord());
173   
174    // skip the rest of the line
175  0 in.readLine();
176   
177    // callback to transmit the data
178  0 metaData(nbVars, nbConstr);
179    }
180   
 
181  0 toggle @Override
182    protected int translateVarToId(String var) {
183  0 int beginning = ((var.charAt(0) == '~') ? 2 : 1 );
184  0 int id = Integer.parseInt(var.substring(beginning));
185  0 return ((var.charAt(0) == '~') ? -1 : 1) * id;
186    }
187   
188   
 
189  0 toggle private String linearizeProduct(IVec<String> tmpLit)
190    throws ContradictionException {
191  0 tmpLit.sort(String.CASE_INSENSITIVE_ORDER);
192  0 String newVar = getProductVariable(tmpLit);
193  0 if (newVar == null) {
194    // generate a new symbol
195  0 newVar = "X" + String.valueOf(nbNewSymbols++);
196    // linearization proposed by O. Roussel (PB07)
197    // generate the clause
198    // product => newSymbol (this is a clause)
199    // not x1 or not x2 ... or not xn or newSymbol
200  0 productStore.put(newVar,tmpLit);
201  0 IVecInt newLits = new VecInt();
202  0 for(String lit : tmpLit)
203  0 negateLiteralInAProduct(lit,newLits);
204  0 literalInAProduct(newVar.toString(),newLits);
205  0 solver.addClause(newLits);
206    // generate the PB-constraint
207    // newSymbol => product translated as
208    // x1+x2+x3...+xn-n*newSymbol>=0
209  0 newLits.clear();
210  0 IVec<BigInteger> newCoefs = new Vec<BigInteger>();
211  0 for(String lit : tmpLit){
212  0 literalInAProduct(lit,newLits);
213  0 newCoefs.push(BigInteger.ONE);
214    }
215  0 literalInAProduct(newVar.toString(),newLits);
216  0 newCoefs.push(new BigInteger(String.valueOf(-tmpLit.size())));
217  0 solver.addPseudoBoolean(newLits, newCoefs, true, BigInteger.ZERO);
218  0 nbConstraintsRead += 2;
219    }
220  0 return newVar;
221    }
222   
223    private Map<String,IVec<String>> productStore = new HashMap<String,IVec<String>>();
224   
 
225  0 toggle private String getProductVariable(IVec<String> lits){
226  0 for(Map.Entry<String,IVec<String>> c : productStore.entrySet())
227  0 if (c.getValue().equals(lits))
228  0 return c.getKey();
229  0 return null;
230    }
231   
232   
233    }
 
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.