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