Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
51   158   12   4,64
26   107   0,43   11
11     2  
1    
 
  AAGReader       Line # 38 51 12 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.PrintWriter;
29    import java.util.Scanner;
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 AAGReader 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 AAGReader(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 @Override
71    public IProblem parseInstance(java.io.Reader in)
72    throws ParseFormatException, ContradictionException, IOException {
73  0 Scanner scanner = new Scanner(in);
74  0 String prefix = scanner.next();
75  0 if (!"aag".equals(prefix)) {
76  0 throw new ParseFormatException("AAG format only!");
77    }
78  0 maxvarid = scanner.nextInt();
79  0 nbinputs = scanner.nextInt();
80  0 int nblatches = scanner.nextInt();
81  0 int nboutputs = scanner.nextInt();
82  0 if (nboutputs > 1) {
83  0 throw new ParseFormatException(
84    "CNF conversion allowed for single output circuit only!");
85    }
86  0 int nbands = scanner.nextInt();
87  0 solver.newVar(maxvarid + 1);
88  0 solver.setExpectedNumberOfClauses(3 * nbands + 2);
89  0 readInput(nbinputs, scanner);
90  0 readLatches(nblatches, scanner);
91  0 if (nboutputs > 0) {
92  0 int output0 = readOutput(nboutputs, scanner);
93  0 readAnd(nbands, output0, scanner);
94    }
95  0 readInputSymbols(scanner);
96  0 skipComments(scanner);
97  0 return solver;
98    }
99   
 
100  0 toggle private void skipComments(Scanner scanner) {
101    // TODO Auto-generated method stub
102   
103    }
104   
 
105  0 toggle private void readInputSymbols(Scanner scanner) {
106    // TODO Auto-generated method stub
107   
108    }
109   
 
110  0 toggle private void readAnd(int nbands, int output0, Scanner scanner)
111    throws ContradictionException {
112   
113  0 for (int i = 0; i < nbands; i++) {
114  0 int lhs = scanner.nextInt();
115  0 int rhs0 = scanner.nextInt();
116  0 int rhs1 = scanner.nextInt();
117  0 solver.and(toDimacs(lhs), toDimacs(rhs0), toDimacs(rhs1));
118    }
119  0 solver.gateTrue(maxvarid + 1);
120  0 solver.gateTrue(toDimacs(output0));
121    }
122   
 
123  0 toggle private int toDimacs(int v) {
124  0 if (v == FALSE) {
125  0 return -(maxvarid + 1);
126    }
127  0 if (v == TRUE) {
128  0 return maxvarid + 1;
129    }
130  0 int var = v >> 1;
131  0 if ((v & 1) == 0) {
132  0 return var;
133    }
134  0 return -var;
135    }
136   
 
137  0 toggle private int readOutput(int nboutputs, Scanner scanner) {
138  0 IVecInt outputs = new VecInt(nboutputs);
139  0 for (int i = 0; i < nboutputs; i++) {
140  0 outputs.push(scanner.nextInt());
141    }
142  0 return outputs.get(0);
143    }
144   
 
145  0 toggle private void readLatches(int nblatches, Scanner scanner) {
146    // TODO Auto-generated method stub
147   
148    }
149   
 
150  0 toggle private IVecInt readInput(int nbinputs, Scanner scanner) {
151  0 IVecInt inputs = new VecInt(nbinputs);
152  0 for (int i = 0; i < nbinputs; i++) {
153  0 inputs.push(scanner.nextInt());
154    }
155  0 return inputs;
156    }
157   
158    }
 
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.