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