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
36 import org.sat4j.core.Vec;
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51 public class DotSearchListener implements SearchListener {
52
53
54
55
56 private static final long serialVersionUID = 1L;
57
58 private final Vec<String> pile;
59
60 private String currentNodeName = null;
61
62 private transient Writer out;
63
64 private boolean estOrange = false;
65
66 public DotSearchListener(final String fileNameToSave) {
67 pile = new Vec<String>();
68 try {
69 out = new FileWriter(fileNameToSave);
70 } catch (IOException e) {
71 System.err.println("Problem when created file.");
72 }
73 }
74
75 public final void assuming(final int p) {
76 final int absP = Math.abs(p);
77 String newName;
78
79 if (currentNodeName == null) {
80 newName = ""+absP;
81 pile.push(newName);
82 saveLine(lineTab("\"" + newName + "\"" + "[label=\"" + newName
83 + "\", shape=circle, color=blue, style=filled]"));
84 } else {
85 newName = currentNodeName;
86 pile.push(newName);
87 saveLine(lineTab("\"" + newName + "\"" + "[label=\""
88 + absP
89 + "\", shape=circle, color=blue, style=filled]"));
90 }
91 currentNodeName = newName;
92 }
93
94 public final void propagating(final int p) {
95 String newName = currentNodeName + "." + p;
96
97 if (currentNodeName == null) {
98 saveLine(lineTab("\"null\" [label=\"\", shape=point]"));
99 }
100 final String couleur = estOrange ? "orange" : "green";
101
102 saveLine(lineTab("\"" + newName + "\"" + "[label=\""
103 + Integer.toString(p) + "\",shape=point, color=black]"));
104 saveLine(lineTab("\"" + currentNodeName + "\"" + " -- " + "\""
105 + newName + "\"" + "[label=" + "\" " + Integer.toString(p)
106 + "\", fontcolor =" + couleur + ", color = " + couleur
107 + ", style = bold]"));
108 currentNodeName = newName;
109 estOrange = false;
110 }
111
112 public final void backtracking(final int p) {
113 final String temp = pile.last();
114 pile.pop();
115 saveLine("\"" + temp + "\"" + "--" + "\"" + currentNodeName + "\""
116 + "[label=\"\", color=red, style=dotted]");
117 currentNodeName = temp;
118 }
119
120 public final void adding(final int p) {
121 estOrange = true;
122 }
123
124 public final void learn(final Constr clause) {
125 }
126
127 public final void delete(final int[] clause) {
128 }
129
130 public final void conflictFound() {
131 saveLine(lineTab("\"" + currentNodeName
132 + "\" [label=\"\", shape=box, color=\"red\", style=filled]"));
133 }
134
135 public final void solutionFound() {
136 saveLine(lineTab("\"" + currentNodeName
137 + "\" [label=\"\", shape=box, color=\"green\", style=filled]"));
138 }
139
140 public final void beginLoop() {
141 }
142
143 public final void start() {
144 saveLine("graph G {");
145 }
146
147 public final void end(Lbool result) {
148 saveLine("}");
149 }
150
151 private final String lineTab(final String line) {
152 return "\t" + line;
153 }
154
155 private final void saveLine(final String line) {
156 try {
157 out.write(line + '\n');
158 if ("}".equals(line)) {
159 out.close();
160 }
161 } catch (IOException e) {
162 e.printStackTrace();
163 }
164 }
165
166 private void readObject(ObjectInputStream stream) throws IOException,
167 ClassNotFoundException {
168
169 stream.defaultReadObject();
170 out = new PrintWriter(System.out);
171 }
172 }