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.minisat.core;
29
30 import java.io.FileWriter;
31 import java.io.IOException;
32 import java.io.ObjectInputStream;
33 import java.io.PrintWriter;
34 import java.io.Writer;
35 import java.util.Map;
36
37 import org.sat4j.core.Vec;
38 import org.sat4j.specs.IConstr;
39 import org.sat4j.specs.Lbool;
40 import org.sat4j.specs.SearchListener;
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55 public class DotSearchListener<T> implements SearchListener {
56
57
58
59
60 private static final long serialVersionUID = 1L;
61
62 private final Vec<String> pile;
63
64 private String currentNodeName = null;
65
66 private transient Writer out;
67
68 private boolean estOrange = false;
69
70 private final Map<Integer, T> mapping;
71
72
73
74
75 public DotSearchListener(final String fileNameToSave,
76 Map<Integer, T> mapping) {
77 pile = new Vec<String>();
78 this.mapping = mapping;
79 try {
80 out = new FileWriter(fileNameToSave);
81 } catch (IOException e) {
82 System.err.println("Problem when created file.");
83 }
84 }
85
86 private String node(int dimacs) {
87 if (mapping != null) {
88 int var = Math.abs(dimacs);
89 T t = mapping.get(var);
90 if (t != null) {
91 if (dimacs > 0)
92 return t.toString();
93 return "-" + t.toString();
94 }
95 }
96 return Integer.toString(dimacs);
97 }
98
99 public final void assuming(final int p) {
100 final int absP = Math.abs(p);
101 String newName;
102
103 if (currentNodeName == null) {
104 newName = "" + absP;
105 pile.push(newName);
106 saveLine(lineTab("\"" + newName + "\"" + "[label=\"" + node(p)
107 + "\", shape=circle, color=blue, style=filled]"));
108 } else {
109 newName = currentNodeName;
110 pile.push(newName);
111 saveLine(lineTab("\"" + newName + "\"" + "[label=\"" + node(p)
112 + "\", shape=circle, color=blue, style=filled]"));
113 }
114 currentNodeName = newName;
115 }
116
117
118
119
120 public final void propagating(final int p, IConstr reason) {
121 String newName = currentNodeName + "." + p;
122
123 if (currentNodeName == null) {
124 saveLine(lineTab("\"null\" [label=\"\", shape=point]"));
125 }
126 final String couleur = estOrange ? "orange" : "green";
127
128 saveLine(lineTab("\"" + newName + "\"" + "[label=\"" + node(p)
129 + "\",shape=point, color=black]"));
130 saveLine(lineTab("\"" + currentNodeName + "\"" + " -- " + "\""
131 + newName + "\"" + "[label=" + "\" " + node(p)
132 + "\", fontcolor =" + couleur + ", color = " + couleur
133 + ", style = bold]"));
134 currentNodeName = newName;
135 estOrange = false;
136 }
137
138 public final void backtracking(final int p) {
139 final String temp = pile.last();
140 pile.pop();
141 saveLine("\"" + temp + "\"" + "--" + "\"" + currentNodeName + "\""
142 + "[label=\"\", color=red, style=dotted]");
143 currentNodeName = temp;
144 }
145
146 public final void adding(final int p) {
147 estOrange = true;
148 }
149
150
151
152
153 public final void learn(final IConstr clause) {
154 }
155
156 public final void delete(final int[] clause) {
157 }
158
159
160
161
162 public final void conflictFound(IConstr confl) {
163 saveLine(lineTab("\"" + currentNodeName
164 + "\" [label=\"\", shape=box, color=\"red\", style=filled]"));
165 }
166
167
168
169
170 public final void conflictFound(int p) {
171 saveLine(lineTab("\"" + currentNodeName
172 + "\" [label=\"\", shape=box, color=\"red\", style=filled]"));
173 }
174
175 public final void solutionFound() {
176 saveLine(lineTab("\"" + currentNodeName
177 + "\" [label=\"\", shape=box, color=\"green\", style=filled]"));
178 }
179
180 public final void beginLoop() {
181 }
182
183 public final void start() {
184 saveLine("graph G {");
185 }
186
187
188
189
190 public final void end(Lbool result) {
191 saveLine("}");
192 }
193
194 private final String lineTab(final String line) {
195 return "\t" + line;
196 }
197
198 private final void saveLine(final String line) {
199 try {
200 out.write(line + '\n');
201 if ("}".equals(line)) {
202 out.close();
203 }
204 } catch (IOException e) {
205 e.printStackTrace();
206 }
207 }
208
209 private void readObject(ObjectInputStream stream) throws IOException,
210 ClassNotFoundException {
211
212 stream.defaultReadObject();
213 out = new PrintWriter(System.out);
214 }
215 }