Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
66   190   21   5,5
36   131   0,48   12
12     2,67  
1    
 
  AIGReader       Line # 38 66 21 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.InputStream;
29    import java.io.PrintWriter;
30   
31    import org.sat4j.core.VecInt;
32    import org.sat4j.specs.ContradictionException;
33    import org.sat4j.specs.IProblem;
34    import org.sat4j.specs.ISolver;
35    import org.sat4j.specs.IVecInt;
36    import org.sat4j.tools.GateTranslator;
37   
 
38    public class AIGReader extends Reader {
39   
40    private final static int FALSE = 0;
41   
42    private final static int TRUE = 1;
43   
44    private final GateTranslator solver;
45   
46    private int maxvarid;
47   
48    private int nbinputs;
49   
 
50  0 toggle AIGReader(ISolver s) {
51  0 solver = new GateTranslator(s);
52    }
53   
 
54  0 toggle @Override
55    public String decode(int[] model) {
56  0 StringBuffer stb = new StringBuffer();
57  0 for (int i = 0; i < nbinputs; i++) {
58  0 stb.append(model[i]>0?1:0);
59    }
60  0 return stb.toString();
61    }
62   
 
63  0 toggle @Override
64    public void decode(int[] model, PrintWriter out) {
65  0 for (int i = 0; i < nbinputs; i++) {
66  0 out.print(model[i]>0?1:0);
67    }
68    }
69   
 
70  0 toggle int parseInt(InputStream in, char expected) throws IOException,
71    ParseFormatException {
72  0 int res, ch;
73  0 ch = in.read();
74   
75  0 if (ch < '0' || ch > '9')
76  0 throw new ParseFormatException("expected digit");
77  0 res = ch - '0';
78   
79  0 while ((ch = in.read()) >= '0' && ch <= '9')
80  0 res = 10 * res + (ch - '0');
81   
82  0 if (ch != expected)
83  0 throw new ParseFormatException("unexpected character");
84   
85  0 return res;
86    }
87   
88    /*
89    * (non-Javadoc)
90    *
91    * @see org.sat4j.reader.Reader#parseInstance(java.io.InputStream)
92    */
 
93  0 toggle @Override
94    public IProblem parseInstance(InputStream in) throws ParseFormatException,
95    ContradictionException, IOException {
96  0 if (in.read() != 'a' || in.read() != 'i' || in.read() != 'g'
97    || in.read() != ' ') {
98  0 throw new ParseFormatException("AIG format only!");
99    }
100  0 maxvarid = parseInt(in, ' ');
101  0 nbinputs = parseInt(in, ' ');
102  0 int nblatches = parseInt(in, ' ');
103  0 if (nblatches > 0) {
104  0 throw new ParseFormatException(
105    "CNF conversion cannot handle latches!");
106    }
107  0 int nboutputs = parseInt(in, ' ');
108  0 if (nboutputs > 1) {
109  0 throw new ParseFormatException(
110    "CNF conversion allowed for single output circuit only!");
111    }
112  0 int nbands = parseInt(in, '\n');
113  0 solver.newVar(maxvarid + 1);
114  0 solver.setExpectedNumberOfClauses(3 * nbands + 2);
115  0 if (nboutputs > 0) {
116  0 assert nboutputs == 1;
117  0 int output0 = parseInt(in, '\n');
118  0 readAnd(nbands, output0, in, 2 * (nbinputs + 1));
119    }
120  0 readInputSymbols(in);
121  0 skipComments(in);
122  0 return solver;
123    }
124   
 
125  0 toggle private void skipComments(InputStream in) {
126    // TODO Auto-generated method stub
127   
128    }
129   
 
130  0 toggle private void readInputSymbols(InputStream in) {
131    // TODO Auto-generated method stub
132   
133    }
134   
 
135  0 toggle static int safeGet(InputStream in) throws IOException, ParseFormatException {
136  0 int ch = in.read();
137  0 if (ch == -1) {
138  0 throw new ParseFormatException("AIG Error, EOF met too early");
139    }
140  0 return ch;
141    }
142   
 
143  0 toggle static int decode(InputStream in) throws IOException, ParseFormatException {
144  0 int x = 0, i = 0;
145  0 int ch;
146   
147  0 while (((ch = safeGet(in)) & 0x80) > 0) {
148  0 System.out.println("=>" + ch);
149  0 x |= (ch & 0x7f) << (7 * i++);
150    }
151  0 return x | (ch << (7 * i));
152    }
153   
 
154  0 toggle private void readAnd(int nbands, int output0, InputStream in, int startid)
155    throws ContradictionException, IOException, ParseFormatException {
156  0 IVecInt clause = new VecInt();
157  0 int lhs = startid;
158  0 for (int i = 0; i < nbands; i++) {
159  0 int delta0 = decode(in);
160  0 int delta1 = decode(in);
161  0 int rhs0 = lhs - delta0;
162  0 int rhs1 = rhs0 - delta1;
163  0 solver.and(toDimacs(lhs), toDimacs(rhs0), toDimacs(rhs1));
164  0 lhs += 2;
165    }
166  0 solver.gateTrue(maxvarid + 1);
167  0 solver.gateTrue(toDimacs(output0));
168    }
169   
 
170  0 toggle private int toDimacs(int v) {
171  0 if (v == FALSE) {
172  0 return -(maxvarid + 1);
173    }
174  0 if (v == TRUE) {
175  0 return maxvarid + 1;
176    }
177  0 int var = v >> 1;
178  0 if ((v & 1) == 0) {
179  0 return var;
180    }
181  0 return -var;
182    }
183   
 
184  0 toggle @Override
185    public IProblem parseInstance(java.io.Reader in)
186    throws ParseFormatException, ContradictionException, IOException {
187  0 throw new UnsupportedOperationException();
188    }
189   
190    }
 
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.