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.PrintWriter;
32
33 import org.sat4j.core.VecInt;
34 import org.sat4j.specs.ContradictionException;
35 import org.sat4j.specs.IProblem;
36 import org.sat4j.specs.ISolver;
37 import org.sat4j.specs.IVecInt;
38 import org.sat4j.tools.GateTranslator;
39
40
41
42
43
44
45
46 public class AAGReader extends Reader {
47
48 private final static int FALSE = 0;
49
50 private final static int TRUE = 1;
51
52 private final GateTranslator solver;
53
54 private int maxvarid;
55
56 private int nbinputs;
57
58 AAGReader(ISolver s) {
59 solver = new GateTranslator(s);
60 }
61
62 @Override
63 public String decode(int[] model) {
64 StringBuffer stb = new StringBuffer();
65 for (int i = 0; i < nbinputs; i++) {
66 stb.append(model[i] > 0 ? 1 : 0);
67 }
68 return stb.toString();
69 }
70
71 @Override
72 public void decode(int[] model, PrintWriter out) {
73 for (int i = 0; i < nbinputs; i++) {
74 out.print(model[i] > 0 ? 1 : 0);
75 }
76 }
77
78 @Override
79 public IProblem parseInstance(java.io.InputStream in)
80 throws ParseFormatException, ContradictionException, IOException {
81 EfficientScanner scanner = new EfficientScanner(in);
82 String prefix = scanner.next();
83 if (!"aag".equals(prefix)) {
84 throw new ParseFormatException("AAG format only!");
85 }
86 maxvarid = scanner.nextInt();
87 nbinputs = scanner.nextInt();
88 int nblatches = scanner.nextInt();
89 int nboutputs = scanner.nextInt();
90 if (nboutputs > 1) {
91 throw new ParseFormatException(
92 "CNF conversion allowed for single output circuit only!");
93 }
94 int nbands = scanner.nextInt();
95 solver.newVar(maxvarid + 1);
96 solver.setExpectedNumberOfClauses(3 * nbands + 2);
97 readInput(nbinputs, scanner);
98 assert nblatches == 0;
99 if (nboutputs > 0) {
100 int output0 = readOutput(nboutputs, scanner);
101 readAnd(nbands, output0, scanner);
102 }
103 return solver;
104 }
105
106 private void readAnd(int nbands, int output0, EfficientScanner scanner)
107 throws ContradictionException, IOException, ParseFormatException {
108
109 for (int i = 0; i < nbands; i++) {
110 int lhs = scanner.nextInt();
111 int rhs0 = scanner.nextInt();
112 int rhs1 = scanner.nextInt();
113 solver.and(toDimacs(lhs), toDimacs(rhs0), toDimacs(rhs1));
114 }
115 solver.gateTrue(maxvarid + 1);
116 solver.gateTrue(toDimacs(output0));
117 }
118
119 private int toDimacs(int v) {
120 if (v == FALSE) {
121 return -(maxvarid + 1);
122 }
123 if (v == TRUE) {
124 return maxvarid + 1;
125 }
126 int var = v >> 1;
127 if ((v & 1) == 0) {
128 return var;
129 }
130 return -var;
131 }
132
133 private int readOutput(int nboutputs, EfficientScanner scanner)
134 throws IOException, ParseFormatException {
135 IVecInt outputs = new VecInt(nboutputs);
136 for (int i = 0; i < nboutputs; i++) {
137 outputs.push(scanner.nextInt());
138 }
139 return outputs.get(0);
140 }
141
142 private IVecInt readInput(int numberOfInputs, EfficientScanner scanner)
143 throws IOException, ParseFormatException {
144 IVecInt inputs = new VecInt(numberOfInputs);
145 for (int i = 0; i < numberOfInputs; i++) {
146 inputs.push(scanner.nextInt());
147 }
148 return inputs;
149 }
150 }