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